diff --git a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs index be765714d9b..2ce733bb404 100644 --- a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs +++ b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs @@ -2,29 +2,32 @@ namespace Microsoft.Dafny { public class FunctionCallSubstituter : Substituter { - public readonly Function A, B; - public FunctionCallSubstituter(Expression receiverReplacement, Dictionary/*!*/ substMap, Function a, Function b) - : base(receiverReplacement, substMap, new Dictionary()) { - A = a; - B = b; + public readonly TraitDecl Tr; + public readonly ClassDecl Cl; + + public FunctionCallSubstituter(Dictionary/*!*/ substMap, Dictionary typeMap, TraitDecl Tr, ClassDecl Cl) + : base(null, substMap, typeMap) { + this.Tr = Tr; + this.Cl = Cl; } public override Expression Substitute(Expression expr) { - if (expr is FunctionCallExpr) { - FunctionCallExpr e = (FunctionCallExpr)expr; - Expression receiver = Substitute(e.Receiver); - List newArgs = SubstituteExprList(e.Args); - FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel); - if (e.Function == A) { - newFce.Function = B; - newFce.Type = e.Type; // TODO: this may not work with type parameters. + if (expr is FunctionCallExpr e) { + var receiver = Substitute(e.Receiver); + var newArgs = SubstituteExprList(e.Args); + Function function; + if (e.Function.EnclosingClass == Tr && e.Receiver is ThisExpr && receiver is ThisExpr && Cl.Members.Find(m => m.OverriddenMember == e.Function) is { } f) { + receiver = new ThisExpr((TopLevelDeclWithMembers)f.EnclosingClass); + function = (Function)f; } else { - newFce.Function = e.Function; - newFce.Type = e.Type; + function = e.Function; } - newFce.TypeApplication_AtEnclosingClass = e.TypeApplication_AtEnclosingClass; // resolve here - newFce.TypeApplication_JustFunction = e.TypeApplication_JustFunction; // resolve here - newFce.IsByMethodCall = e.IsByMethodCall; - return newFce; + return new FunctionCallExpr(e.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel) { + Function = function, + Type = e.Type, // TODO: this may not work with type parameters. + TypeApplication_AtEnclosingClass = SubstituteTypeList(e.TypeApplication_AtEnclosingClass), // resolve here + TypeApplication_JustFunction = SubstituteTypeList(e.TypeApplication_JustFunction), // resolve here + IsByMethodCall = e.IsByMethodCall + }; } return base.Substitute(expr); } diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 10c96e1a5c3..07d692a8af7 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -173,7 +173,7 @@ void AddMethod_Top(Method m, bool isByMethod, bool includeAllMethods) { AddMethodImpl(m, proc, true); } } - if (m.OverriddenMethod != null && InVerificationScope(m)) //method has overrided a parent method + if (m.OverriddenMethod != null && InVerificationScope(m)) //method has overridden a parent method { var procOverrideChk = AddMethod(m, MethodTranslationKind.OverrideCheck); sink.AddTopLevelDeclaration(procOverrideChk); @@ -213,7 +213,8 @@ private void AddAllocationAxiom(Boogie.Declaration fieldDeclaration, Field f, To AddWellformednessCheck(cf); if (InVerificationScope(cf)) { var etran = new ExpressionTranslator(this, predef, f.tok); - heightAntecedent = Bpl.Expr.Lt(Bpl.Expr.Literal(cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf)), etran.FunctionContextHeight()); + var visibilityLevel = cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf); + heightAntecedent = Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight()); } } @@ -877,8 +878,8 @@ private void AddFunctionOverrideCheckImpl(Function f) { } // the procedure itself var req = new List(); - // free requires mh == ModuleContextHeight && fh == FunctionContextHeight; - req.Add(Requires(f.tok, true, etran.HeightContext(f.OverriddenFunction), null, null)); + // free requires fh == FunctionContextHeight; + req.Add(Requires(f.tok, true, etran.HeightContext(f, true), null, null)); if (f is TwoStateFunction) { // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); @@ -920,18 +921,16 @@ private void AddFunctionOverrideCheckImpl(Function f) { } var substMap = new Dictionary(); - for (int i = 0; i < f.Formals.Count; i++) { - //get corresponsing formal in the class - var ie = new IdentifierExpr(f.Formals[i].tok, f.Formals[i].AssignUniqueName(f.IdGenerator)); - ie.Var = f.Formals[i]; ie.Type = ie.Var.Type; - substMap.Add(f.OverriddenFunction.Formals[i], ie); + foreach (var (formal, overriddenFormal) in f.Formals.Zip(f.OverriddenFunction.Formals, Tuple.Create)) { + // get corresponding formal in the class + var ie = new IdentifierExpr(formal.tok, formal.AssignUniqueName(f.IdGenerator)) { Var = formal, Type = formal.Type }; + substMap.Add(overriddenFormal, ie); } if (f.OverriddenFunction.Result != null) { Contract.Assert(pOut != null); - //get corresponsing formal in the class - var ie = new IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator)); - ie.Var = pOut; ie.Type = ie.Var.Type; + // get corresponding formal in the class + var ie = new IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator)) { Var = pOut, Type = pOut.Type }; substMap.Add(f.OverriddenFunction.Result, ie); } @@ -946,8 +945,8 @@ private void AddFunctionOverrideCheckImpl(Function f) { //adding assert W <= Frame’ AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap, typeMap); - //adding assume Q; assert Post’; - //adding assume J.F(ins) == C.F(ins); + //adding assume Q; + //assert Post’; AddFunctionOverrideEnsChk(f, builder, etran, substMap, typeMap, implInParams, implOutParams.Count == 0 ? null : implOutParams[0]); var stmts = builder.Collect(f.tok); @@ -1134,7 +1133,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti // The axiom Boogie.Expr ax = BplForall(f.tok, new List(), forallFormals, null, tr, Boogie.Expr.Imp(Boogie.Expr.And(ReceiverNotNull(bvThisExpr), isOfSubtype), synonyms)); - var activate = AxiomActivation(f, etran); + var activate = AxiomActivation(overridingFunction, etran, true); string comment = "override axiom for " + f.FullSanitizedName + " in class " + overridingFunction.EnclosingClass.FullSanitizedName; return new Boogie.Axiom(f.tok, Boogie.Expr.Imp(activate, ax), comment); } @@ -1381,7 +1380,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { // FREE PRECONDITIONS if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation || kind == MethodTranslationKind.OverrideCheck) { // the other cases have no need for a free precondition // free requires mh == ModuleContextHeight && fh == FunctionContextHeight; - req.Add(Requires(m.tok, true, etran.HeightContext(kind == MethodTranslationKind.OverrideCheck ? m.OverriddenMethod : m), null, null)); + req.Add(Requires(m.tok, true, etran.HeightContext(m), null, null)); if (m is TwoStateLemma) { // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs index d4e5a6ededf..35c1b85f727 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs @@ -258,12 +258,11 @@ public Boogie.IdentifierExpr FunctionContextHeight() { return new Boogie.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Boogie.Type.Int); } - public Boogie.Expr HeightContext(ICallable m) { + public Boogie.Expr HeightContext(ICallable m, bool intermediateScope = false) { Contract.Requires(m != null); // free requires fh == FunctionContextHeight; - var module = m.EnclosingModule; - Boogie.Expr context = - Boogie.Expr.Eq(Boogie.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(m)), FunctionContextHeight()); + var visibilityLevel = m.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(m); + Boogie.Expr context = Boogie.Expr.Eq(MkFunctionHeight(visibilityLevel, intermediateScope), FunctionContextHeight()); return context; } diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index f4d3bef4783..ced5c08906d 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -2054,7 +2054,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis // (mh == ModuleContextHeight && fh <= FunctionContextHeight) // // USE_VIA_CONTEXT - // (mh != ModuleContextHeight || fh != FunctionContextHeight) && + // fh < FunctionContextHeight && // GOOD_PARAMETERS // where GOOD_PARAMETERS means: // $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types && @@ -2157,10 +2157,9 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis foreach (AttributedExpression req in f.Req) { pre = BplAnd(pre, etran.TrExpr(Substitute(req.E, null, substMap))); } - // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight) - var mod = f.EnclosingClass.EnclosingModuleDefinition; - Bpl.Expr useViaContext = !InVerificationScope(f) ? Bpl.Expr.True : - (Bpl.Expr)Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight()); + // useViaContext: fh < FunctionContextHeight + var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f.OverriddenFunction ?? f); + Expr useViaContext = Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight()); // useViaCanCall: f#canCall(args) Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool); Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs, args)); @@ -2255,15 +2254,14 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis return (olderParameterCount, olderCondition); } - Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran) { + Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran, bool requiresFullScope = false) { Contract.Requires(f != null); Contract.Requires(etran != null); Contract.Requires(VisibleInScope(f)); - var module = f.EnclosingClass.EnclosingModuleDefinition; if (InVerificationScope(f)) { - return - Bpl.Expr.Le(Bpl.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight()); + var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f); + return Expr.Le(MkFunctionHeight(visibilityLevel, !requiresFullScope), etran.FunctionContextHeight()); } else { return Bpl.Expr.True; } @@ -2303,7 +2301,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { // for visibility==ForeignModuleOnly, means: // GOOD_PARAMETERS // for visibility==IntraModuleOnly, means: - // fh != FunctionContextHeight && + // fh < FunctionContextHeight && // GOOD_PARAMETERS // where GOOD_PARAMETERS means: // $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types && @@ -2508,12 +2506,11 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { return null; } - // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight) - ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition; + // useViaContext: fh < FunctionContextHeight + var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f); Bpl.Expr useViaContext = !InVerificationScope(f) - ? (Bpl.Expr)Bpl.Expr.True - : Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(f)), - etran.FunctionContextHeight()); + ? Bpl.Expr.True + : Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight()); // ante := (useViaContext && typeAnte && pre) ante = BplAnd(useViaContext, BplAnd(ante, pre)); @@ -3483,65 +3480,42 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(en.E))); } - //generating assume J.F(ins) == C.F(ins) - Bpl.FunctionCall funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType))); - Bpl.FunctionCall funcIdT = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.OverriddenFunction.tok, f.OverriddenFunction.FullSanitizedName, TrType(f.OverriddenFunction.ResultType))); - List argsC = new List(); - List argsT = new List(); - // add type arguments - argsT.AddRange(GetTypeArguments(f.OverriddenFunction, f).ConvertAll(TypeToTy)); - argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy)); - // add fuel arguments - if (f.IsFuelAware()) { - argsC.Add(etran.layerInterCluster.GetFunctionFuel(f)); - } - if (f.OverriddenFunction.IsFuelAware()) { - argsT.Add(etran.layerInterCluster.GetFunctionFuel(f)); - } - // add heap arguments - if (f is TwoStateFunction) { - argsC.Add(etran.Old.HeapExpr); - argsT.Add(etran.Old.HeapExpr); - } - if (AlwaysUseHeap || f.ReadsHeap) { - argsC.Add(etran.HeapExpr); - } - if (AlwaysUseHeap || f.OverriddenFunction.ReadsHeap) { - argsT.Add(etran.HeapExpr); - } - // add "ordinary" parameters (including "this", if any) - var prefixCount = implInParams.Count - f.Formals.Count; - for (var i = 0; i < implInParams.Count; i++) { - Bpl.Expr cParam = new Bpl.IdentifierExpr(f.tok, implInParams[i]); - Bpl.Expr tParam = new Bpl.IdentifierExpr(f.OverriddenFunction.tok, implInParams[i]); - if (prefixCount <= i && ModeledAsBoxType(f.OverriddenFunction.Formals[i - prefixCount].Type)) { - tParam = BoxIfNecessary(f.tok, tParam, f.Formals[i - prefixCount].Type); - } - argsC.Add(cParam); - argsT.Add(tParam); - } - Bpl.Expr funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC); - Bpl.Expr funcExpT = new Bpl.NAryExpr(f.OverriddenFunction.tok, funcIdT, argsT); - var funcExpCPossiblyBoxed = funcExpC; - if (ModeledAsBoxType(f.OverriddenFunction.ResultType)) { - funcExpCPossiblyBoxed = BoxIfUnboxed(funcExpCPossiblyBoxed, f.ResultType); - } - builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpCPossiblyBoxed, funcExpT))); - //generating assume C.F(ins) == out, if a result variable was given if (resultVariable != null) { + var funcIdC = new FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType))); + var argsC = new List(); + + // add type arguments + argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy)); + + // add fuel arguments + if (f.IsFuelAware()) { + argsC.Add(etran.layerInterCluster.GetFunctionFuel(f)); + } + + // add heap arguments + if (f is TwoStateFunction) { + argsC.Add(etran.Old.HeapExpr); + } + if (AlwaysUseHeap || f.ReadsHeap) { + argsC.Add(etran.HeapExpr); + } + + argsC.AddRange(implInParams.Select(var => new Bpl.IdentifierExpr(f.tok, var))); + + var funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC); var resultVar = new Bpl.IdentifierExpr(resultVariable.tok, resultVariable); builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, resultVar))); } //generating trait post-conditions with class variables foreach (var en in f.OverriddenFunction.Ens) { - Expression postcond = Substitute(en.E, null, substMap, typeMap); - bool splitHappened; // we don't actually care - foreach (var s in TrSplitExpr(postcond, etran, false, out splitHappened)) { - if (s.IsChecked) { - builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true))); - } + // We replace all occurrences of the trait version of the function with the class version. This is only allowed + // if the receiver is `this`. We underapproximate this by looking for a `ThisExpr`, which misses more complex + // expressions that evaluate to one. + var sub = new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (ClassDecl)f.EnclosingClass); + foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) { + builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true))); } } } @@ -3633,17 +3607,15 @@ private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builde Contract.Requires(substMap != null); //generating trait pre-conditions with class variables foreach (var req in f.OverriddenFunction.Req) { - Expression precond = Substitute(req.E, null, substMap, typeMap); - builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(precond))); + // We replace all occurrences of the trait version of the function with the class version. This is only allowed + // if the receiver is `this`. We underapproximate this by looking for a `ThisExpr`, which misses more complex + // expressions that evaluate to one. + var sub = new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (ClassDecl)f.EnclosingClass); + builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(sub.Substitute(req.E)))); } //generating class pre-conditions - foreach (var req in f.Req) { - bool splitHappened; // we actually don't care - foreach (var s in TrSplitExpr(req.E, etran, false, out splitHappened)) { - if (s.IsChecked) { - builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(false))); - } - } + foreach (var s in f.Req.SelectMany(req => TrSplitExpr(req.E, etran, false, out _).Where(s => s.IsChecked))) { + builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(false))); } } @@ -4765,7 +4737,7 @@ Bpl.Expr CanCallAssumption(Expression expr, ExpressionTranslator etran) { Contract.Requires(predef != null); Contract.Ensures(Contract.Result() != null); - if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) { + if (expr is LiteralExpr or ThisExpr or IdentifierExpr or WildcardExpr or BoogieWrapper) { return Bpl.Expr.True; } else if (expr is DisplayExpression) { DisplayExpression e = (DisplayExpression)expr; @@ -10757,6 +10729,14 @@ List MkTyParamFormals(List args, bool includeWhereClaus return null; } + // We use the $FunctionContextHeight to restrict the applicability of certain axioms. The entity at the end of a + // dependency chain has the highest number. To get more granular control over the visibility, we extend every + // visibility level by a precursory intermediate level. This additional level is helpful for proofs that would be + // disturbed by axioms that are visible the the final level. + static Bpl.Expr MkFunctionHeight(int visibilityLevel, bool intermediateScope = false) { + return Expr.Literal(visibilityLevel * 2 + (intermediateScope ? 0 : 1)); + } + public static void MapM(IEnumerable xs, Action K) { Contract.Requires(xs != null); Contract.Requires(K != null); diff --git a/Test/concurrency/01-InnerOuter.dfy b/Test/concurrency/01-InnerOuter.dfy index 62ac4f891f8..ce833e2bcfd 100644 --- a/Test/concurrency/01-InnerOuter.dfy +++ b/Test/concurrency/01-InnerOuter.dfy @@ -84,7 +84,7 @@ class Inner extends O { && old(data) <= data } - twostate lemma adm() {} + twostate lemma adm() requires admPre() {} constructor (ghost s: S, initial_data: int) requires s.i() diff --git a/Test/concurrency/01-InnerOuter.dfy.expect b/Test/concurrency/01-InnerOuter.dfy.expect index 5ed0d97333e..b49c1470365 100644 --- a/Test/concurrency/01-InnerOuter.dfy.expect +++ b/Test/concurrency/01-InnerOuter.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 31 verified, 0 errors +Dafny program verifier finished with 32 verified, 0 errors diff --git a/Test/concurrency/02-DoubleRead.dfy b/Test/concurrency/02-DoubleRead.dfy index 11a3a86ab27..ae119a45d8d 100644 --- a/Test/concurrency/02-DoubleRead.dfy +++ b/Test/concurrency/02-DoubleRead.dfy @@ -111,7 +111,7 @@ class ArcAtomicIsize extends Object { } // Admissibility proof - twostate lemma adm() {} + twostate lemma adm() requires admPre() {} constructor (ghost universe: Universe, initial_data: int) requires universe.i() diff --git a/Test/concurrency/02-DoubleRead.dfy.expect b/Test/concurrency/02-DoubleRead.dfy.expect index a61fd92d975..3e2e11e1866 100644 --- a/Test/concurrency/02-DoubleRead.dfy.expect +++ b/Test/concurrency/02-DoubleRead.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 39 verified, 0 errors +Dafny program verifier finished with 40 verified, 0 errors diff --git a/Test/concurrency/03-SimpleCounter.dfy b/Test/concurrency/03-SimpleCounter.dfy index d6a78609235..e0b01497246 100644 --- a/Test/concurrency/03-SimpleCounter.dfy +++ b/Test/concurrency/03-SimpleCounter.dfy @@ -112,7 +112,7 @@ class ArcAtomicIsize extends Object { } // Admissibility proof - twostate lemma adm() {} + twostate lemma adm() requires admPre() {} constructor (ghost universe: Universe, initial_data: int) requires universe.i() diff --git a/Test/concurrency/03-SimpleCounter.dfy.expect b/Test/concurrency/03-SimpleCounter.dfy.expect index bba7f9e68b7..1b45cf86b6a 100644 --- a/Test/concurrency/03-SimpleCounter.dfy.expect +++ b/Test/concurrency/03-SimpleCounter.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 41 verified, 0 errors +Dafny program verifier finished with 42 verified, 0 errors diff --git a/Test/concurrency/10-SequenceInvariant.dfy b/Test/concurrency/10-SequenceInvariant.dfy index 09f540e7947..4bd942e9e2c 100644 --- a/Test/concurrency/10-SequenceInvariant.dfy +++ b/Test/concurrency/10-SequenceInvariant.dfy @@ -256,7 +256,7 @@ class Thread extends Object { } twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {} - predicate localInv() reads * { + predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() { && objectGlobalBaseInv() } predicate inv() reads * ensures inv() ==> localInv() { @@ -322,7 +322,7 @@ trait OwnedObject extends Object { assert owner in universe.content; } - predicate localInv() reads * { + predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() { && objectGlobalBaseInv() && localUserInv() } diff --git a/Test/concurrency/11-MutexGuard2.dfy b/Test/concurrency/11-MutexGuard2.dfy index 07d8ed4a8bc..c1927624ef4 100644 --- a/Test/concurrency/11-MutexGuard2.dfy +++ b/Test/concurrency/11-MutexGuard2.dfy @@ -261,7 +261,7 @@ class Thread extends Object { } twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {} - predicate localInv() reads * { + predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() { && objectGlobalBaseInv() } predicate inv() reads * ensures inv() ==> localInv() { @@ -332,7 +332,7 @@ trait OwnedObject extends Object { && unchangedNonvolatileUserFields() } - predicate localInv() reads * { + predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() { && objectGlobalBaseInv() && localUserInv() } diff --git a/Test/concurrency/12-MutexLifetime-short.dfy b/Test/concurrency/12-MutexLifetime-short.dfy index cb1b97ccbf6..18fba5266c5 100644 --- a/Test/concurrency/12-MutexLifetime-short.dfy +++ b/Test/concurrency/12-MutexLifetime-short.dfy @@ -365,7 +365,7 @@ class Thread extends Object { } twostate lemma baseFieldsInvMonotonicity() requires old(baseFieldsInv()) && old(universe.content) <= universe.content && unchanged(this) ensures baseFieldsInv() {} - predicate localInv() reads * { + predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() { && objectGlobalBaseInv() } predicate inv() reads * ensures inv() ==> localInv() { @@ -439,7 +439,7 @@ trait OwnedObject extends Object { && unchangedNonvolatileUserFields() } - predicate localInv() reads * { + predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() { && objectGlobalBaseInv() && this in lifetime.elements && (lifetime.alive() ==> owner != null) diff --git a/Test/dafny4/git-issue245.dfy b/Test/dafny4/git-issue245.dfy index 187cef8bc42..a5458a2cd7c 100644 --- a/Test/dafny4/git-issue245.dfy +++ b/Test/dafny4/git-issue245.dfy @@ -37,23 +37,23 @@ class C extends T { { 5 + y } } -// class D is like C, but in each case, the spec is NOT weaker than that in T +// class D is like C, but in each case, the spec is NOT stronger than that in T class D extends T { // d does not name the result in either trait or class function method d(y: nat): nat - ensures d(y) < 20 + y // error: specification is not weaker + ensures d(y) < 20 + y // error: specification is not stronger { 11 + y } // f names the result in both trait and class function method f(y: nat): (result: nat) - ensures result < 20 + y // error: specification is not weaker + ensures result < 20 + y // error: specification is not stronger { 11 + y } // g names the result in just the class function method g(y: nat): (result: nat) - ensures result < 20 + y // error: specification is not weaker + ensures result < 20 + y // error: specification is not stronger { 11 + y } // h names the result in just the trait function method h(y: nat): nat - ensures h(y) < 20 + y // error: specification is not weaker + ensures h(y) < 20 + y // error: specification is not stronger { 11 + y } } @@ -62,19 +62,19 @@ class D extends T { class E extends T { // d does not name the result in either trait or class function method d(y: nat): nat - ensures d(y) < 20 + y + ensures d(y) < 20 + y // error: specification is not stronger { 5 + y } // f names the result in both trait and class function method f(y: nat): (result: nat) - ensures result < 20 + y + ensures result < 20 + y // error: specification is not stronger { 5 + y } // g names the result in just the class function method g(y: nat): (result: nat) - ensures result < 20 + y + ensures result < 20 + y // error: specification is not stronger { 5 + y } // h names the result in just the trait function method h(y: nat): nat - ensures h(y) < 20 + y + ensures h(y) < 20 + y // error: specification is not stronger { 5 + y } } diff --git a/Test/dafny4/git-issue245.dfy.expect b/Test/dafny4/git-issue245.dfy.expect index f154a354f05..52dc0dd66b2 100644 --- a/Test/dafny4/git-issue245.dfy.expect +++ b/Test/dafny4/git-issue245.dfy.expect @@ -2,6 +2,10 @@ git-issue245.dfy(43,18): Error: the function must provide an equal or more detai git-issue245.dfy(47,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait git-issue245.dfy(51,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait git-issue245.dfy(55,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue245.dfy(64,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue245.dfy(68,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue245.dfy(72,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue245.dfy(76,18): Error: the function must provide an equal or more detailed postcondition than in its parent trait git-issue245.dfy(84,18): Error: A postcondition might not hold on this return path. git-issue245.dfy(85,17): Related location: This is the postcondition that might not hold. git-issue245.dfy(88,18): Error: A postcondition might not hold on this return path. @@ -11,4 +15,4 @@ git-issue245.dfy(93,19): Related location: This is the postcondition that might git-issue245.dfy(96,18): Error: A postcondition might not hold on this return path. git-issue245.dfy(97,17): Related location: This is the postcondition that might not hold. -Dafny program verifier finished with 28 verified, 8 errors +Dafny program verifier finished with 24 verified, 12 errors diff --git a/Test/git-issues/git-issue-2500.dfy b/Test/git-issues/git-issue-2500.dfy new file mode 100644 index 00000000000..0ccb37a33a0 --- /dev/null +++ b/Test/git-issues/git-issue-2500.dfy @@ -0,0 +1,42 @@ +// RUN: %exits-with 4 %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module M { + trait {:termination false} Tr { + function True(): (ret: bool) ensures ret + function True'(): (ret: bool) ensures True'() + function ActuallyTrue(): (ret: bool) ensures var alsoThis := this; alsoThis.ActuallyTrue() + function Other(x:nat, free: Tr): bool + ensures x != 0 && free.Other(x-1, free) ==> Other(x-1, free) + } +} + +class Cl extends M.Tr { + function True(): (ret: bool) + // Missing: ensures ret + { false } + function True'(): (ret: bool) + // Missing: ensures True'() + { false } + function ActuallyTrue(): (ret: bool) + // This is logically correct, but the disguised receiver in the Tr spec prevents the override check from passing. + ensures ActuallyTrue() + { true } + function Other(x: nat, free: M.Tr): bool + // Different receiver + ensures x != 0 && Other(x-1, free) ==> Other(x-1, free) + { false } +} + +trait Trait { + predicate Even(i: nat) + predicate Odd(i: nat) + ensures if i == 0 then true else (i % 2 == 1) == Even(i-1) +} + +class Class extends Trait { + predicate Even(i: nat) { if i == 0 then true else Odd(i-1) } + predicate Odd(i: nat) + ensures if i == 0 then true else (i % 2 == 1) == Even(i-1) + { if i == 0 then false else Even(i-1) } +} diff --git a/Test/git-issues/git-issue-2500.dfy.expect b/Test/git-issues/git-issue-2500.dfy.expect new file mode 100644 index 00000000000..6aaef370ac0 --- /dev/null +++ b/Test/git-issues/git-issue-2500.dfy.expect @@ -0,0 +1,6 @@ +git-issue-2500.dfy(15,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue-2500.dfy(18,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue-2500.dfy(21,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue-2500.dfy(25,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait + +Dafny program verifier finished with 11 verified, 4 errors diff --git a/docs/dev/news/3431.fix b/docs/dev/news/3431.fix new file mode 100644 index 00000000000..96e3176bae2 --- /dev/null +++ b/docs/dev/news/3431.fix @@ -0,0 +1 @@ +To ensure that a `class` correctly implements a `trait`, we perform an override check. This check was previously faulty across `module`s, but works unconditionally now.