From 0cdec2c1932e0ffeb144077f54dd64660bae9d37 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 31 Jan 2023 04:49:40 +0100 Subject: [PATCH] chore: Revert "fix: Cross-modular override check (#3223)" (#3419) This reverts PR #3223. It introduced an completeness issue. --- .../Compilers/Python/Compiler-python.cs | 1 - .../Verifier/FunctionCallSubstituter.cs | 20 +-- .../Verifier/Translator.ClassMembers.cs | 27 ++-- .../Translator.ExpressionTranslator.cs | 7 +- Source/DafnyCore/Verifier/Translator.cs | 116 ++++++++++-------- Test/concurrency/10-SequenceInvariant.dfy | 4 +- Test/concurrency/11-MutexGuard2.dfy | 4 +- Test/concurrency/12-MutexLifetime-short.dfy | 4 +- Test/dafny4/git-issue245.dfy | 18 +-- Test/dafny4/git-issue245.dfy.expect | 6 +- Test/git-issues/git-issue-2500.dfy | 29 ----- Test/git-issues/git-issue-2500.dfy.expect | 6 - docs/dev/news/3223.fix | 1 - 13 files changed, 111 insertions(+), 132 deletions(-) delete mode 100644 Test/git-issues/git-issue-2500.dfy delete mode 100644 Test/git-issues/git-issue-2500.dfy.expect delete mode 100644 docs/dev/news/3223.fix diff --git a/Source/DafnyCore/Compilers/Python/Compiler-python.cs b/Source/DafnyCore/Compilers/Python/Compiler-python.cs index d83b8359f81..9b3ce5fb206 100644 --- a/Source/DafnyCore/Compilers/Python/Compiler-python.cs +++ b/Source/DafnyCore/Compilers/Python/Compiler-python.cs @@ -1740,6 +1740,5 @@ protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageV exceptBlock.WriteLine($"{IdProtect(haltMessageVarName)} = e.message"); TrStmt(recoveryBody, exceptBlock); } - } } diff --git a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs index db582f56305..be765714d9b 100644 --- a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs +++ b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs @@ -3,26 +3,26 @@ namespace Microsoft.Dafny { public class FunctionCallSubstituter : Substituter { public readonly Function A, B; - public FunctionCallSubstituter(Expression receiverReplacement, Dictionary/*!*/ substMap, Dictionary typeMap, Function a, Function b) - : base(receiverReplacement, substMap, typeMap) { + public FunctionCallSubstituter(Expression receiverReplacement, Dictionary/*!*/ substMap, Function a, Function b) + : base(receiverReplacement, substMap, new Dictionary()) { A = a; B = b; } public override Expression Substitute(Expression expr) { - if (expr is FunctionCallExpr e) { - var receiver = Substitute(e.Receiver); - var newArgs = SubstituteExprList(e.Args); - var newFce = new FunctionCallExpr(e.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel); - if (e.Function == A && e.Receiver is ThisExpr && receiver is ThisExpr) { + 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. - receiver.Type = Resolver.GetThisType(B.tok, (TopLevelDeclWithMembers)B.EnclosingClass); } else { newFce.Function = e.Function; newFce.Type = e.Type; } - newFce.TypeApplication_AtEnclosingClass = SubstituteTypeList(e.TypeApplication_AtEnclosingClass); // resolve here - newFce.TypeApplication_JustFunction = SubstituteTypeList(e.TypeApplication_JustFunction); // resolve here + newFce.TypeApplication_AtEnclosingClass = e.TypeApplication_AtEnclosingClass; // resolve here + newFce.TypeApplication_JustFunction = e.TypeApplication_JustFunction; // resolve here newFce.IsByMethodCall = e.IsByMethodCall; return newFce; } diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 6ccb0204787..10c96e1a5c3 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -213,8 +213,7 @@ private void AddAllocationAxiom(Boogie.Declaration fieldDeclaration, Field f, To AddWellformednessCheck(cf); if (InVerificationScope(cf)) { var etran = new ExpressionTranslator(this, predef, f.tok); - var visibilityLevel = cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf); - heightAntecedent = Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight()); + heightAntecedent = Bpl.Expr.Lt(Bpl.Expr.Literal(cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf)), etran.FunctionContextHeight()); } } @@ -878,8 +877,8 @@ private void AddFunctionOverrideCheckImpl(Function f) { } // the procedure itself var req = new List(); - // free requires fh == FunctionContextHeight; - req.Add(Requires(f.tok, true, etran.HeightContext(f, true), null, null)); + // free requires mh == ModuleContextHeight && fh == FunctionContextHeight; + req.Add(Requires(f.tok, true, etran.HeightContext(f.OverriddenFunction), null, null)); if (f is TwoStateFunction) { // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); @@ -921,16 +920,18 @@ private void AddFunctionOverrideCheckImpl(Function f) { } var substMap = new Dictionary(); - 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); + 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); } if (f.OverriddenFunction.Result != null) { Contract.Assert(pOut != null); - // get corresponding formal in the class - var ie = new IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator)) { Var = pOut, Type = pOut.Type }; + //get corresponsing formal in the class + var ie = new IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator)); + ie.Var = pOut; ie.Type = ie.Var.Type; substMap.Add(f.OverriddenFunction.Result, ie); } @@ -945,8 +946,8 @@ private void AddFunctionOverrideCheckImpl(Function f) { //adding assert W <= Frame’ AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap, typeMap); - //adding assume Q; - //assert Post’; + //adding assume Q; assert Post’; + //adding assume J.F(ins) == C.F(ins); AddFunctionOverrideEnsChk(f, builder, etran, substMap, typeMap, implInParams, implOutParams.Count == 0 ? null : implOutParams[0]); var stmts = builder.Collect(f.tok); @@ -1133,7 +1134,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(overridingFunction, etran, true); + var activate = AxiomActivation(f, etran); string comment = "override axiom for " + f.FullSanitizedName + " in class " + overridingFunction.EnclosingClass.FullSanitizedName; return new Boogie.Axiom(f.tok, Boogie.Expr.Imp(activate, ax), comment); } diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs index 35c1b85f727..d4e5a6ededf 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs @@ -258,11 +258,12 @@ public Boogie.IdentifierExpr FunctionContextHeight() { return new Boogie.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Boogie.Type.Int); } - public Boogie.Expr HeightContext(ICallable m, bool intermediateScope = false) { + public Boogie.Expr HeightContext(ICallable m) { Contract.Requires(m != null); // free requires fh == FunctionContextHeight; - var visibilityLevel = m.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(m); - Boogie.Expr context = Boogie.Expr.Eq(MkFunctionHeight(visibilityLevel, intermediateScope), FunctionContextHeight()); + var module = m.EnclosingModule; + Boogie.Expr context = + Boogie.Expr.Eq(Boogie.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(m)), FunctionContextHeight()); return context; } diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 4adeb7b2324..426863fff9d 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 - // fh < FunctionContextHeight && + // (mh != ModuleContextHeight || fh != FunctionContextHeight) && // GOOD_PARAMETERS // where GOOD_PARAMETERS means: // $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types && @@ -2157,9 +2157,10 @@ 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: fh < FunctionContextHeight - var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f.OverriddenFunction ?? f); - Expr useViaContext = Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight()); + // 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()); // 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)); @@ -2254,14 +2255,15 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis return (olderParameterCount, olderCondition); } - Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran, bool requiresFullScope = false) { + Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran) { Contract.Requires(f != null); Contract.Requires(etran != null); Contract.Requires(VisibleInScope(f)); + var module = f.EnclosingClass.EnclosingModuleDefinition; if (InVerificationScope(f)) { - var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f); - return Expr.Le(MkFunctionHeight(visibilityLevel, !requiresFullScope), etran.FunctionContextHeight()); + return + Bpl.Expr.Le(Bpl.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight()); } else { return Bpl.Expr.True; } @@ -2301,7 +2303,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 && @@ -2506,11 +2508,12 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { return null; } - // useViaContext: fh < FunctionContextHeight - var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f); + // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight) + ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition; Bpl.Expr useViaContext = !InVerificationScope(f) - ? Bpl.Expr.True - : Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight()); + ? (Bpl.Expr)Bpl.Expr.True + : Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(f)), + etran.FunctionContextHeight()); // ante := (useViaContext && typeAnte && pre) ante = BplAnd(useViaContext, BplAnd(ante, pre)); @@ -3480,42 +3483,65 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(en.E))); } - //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); + //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))); - argsC.AddRange(implInParams.Select(var => new Bpl.IdentifierExpr(f.tok, var))); - - var funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC); + //generating assume C.F(ins) == out, if a result variable was given + if (resultVariable != null) { 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) { - // 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(null, substMap, typeMap, f.OverriddenFunction, f); - 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))); + 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))); + } } } } @@ -4739,7 +4765,7 @@ Bpl.Expr CanCallAssumption(Expression expr, ExpressionTranslator etran) { Contract.Requires(predef != null); Contract.Ensures(Contract.Result() != null); - if (expr is LiteralExpr or ThisExpr or IdentifierExpr or WildcardExpr or BoogieWrapper) { + if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) { return Bpl.Expr.True; } else if (expr is DisplayExpression) { DisplayExpression e = (DisplayExpression)expr; @@ -10726,14 +10752,6 @@ 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/10-SequenceInvariant.dfy b/Test/concurrency/10-SequenceInvariant.dfy index 4bd942e9e2c..09f540e7947 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 * ensures localInv() ==> objectGlobalBaseInv() { + predicate localInv() reads * { && objectGlobalBaseInv() } predicate inv() reads * ensures inv() ==> localInv() { @@ -322,7 +322,7 @@ trait OwnedObject extends Object { assert owner in universe.content; } - predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() { + predicate localInv() reads * { && objectGlobalBaseInv() && localUserInv() } diff --git a/Test/concurrency/11-MutexGuard2.dfy b/Test/concurrency/11-MutexGuard2.dfy index c1927624ef4..07d8ed4a8bc 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 * ensures localInv() ==> objectGlobalBaseInv() { + predicate localInv() reads * { && objectGlobalBaseInv() } predicate inv() reads * ensures inv() ==> localInv() { @@ -332,7 +332,7 @@ trait OwnedObject extends Object { && unchangedNonvolatileUserFields() } - predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() { + predicate localInv() reads * { && objectGlobalBaseInv() && localUserInv() } diff --git a/Test/concurrency/12-MutexLifetime-short.dfy b/Test/concurrency/12-MutexLifetime-short.dfy index 18fba5266c5..cb1b97ccbf6 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 * ensures localInv() ==> objectGlobalBaseInv() { + predicate localInv() reads * { && objectGlobalBaseInv() } predicate inv() reads * ensures inv() ==> localInv() { @@ -439,7 +439,7 @@ trait OwnedObject extends Object { && unchangedNonvolatileUserFields() } - predicate localInv() reads * ensures localInv() ==> objectGlobalBaseInv() { + predicate localInv() reads * { && objectGlobalBaseInv() && this in lifetime.elements && (lifetime.alive() ==> owner != null) diff --git a/Test/dafny4/git-issue245.dfy b/Test/dafny4/git-issue245.dfy index a5458a2cd7c..187cef8bc42 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 stronger than that in T +// class D is like C, but in each case, the spec is NOT weaker 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 stronger + ensures d(y) < 20 + y // error: specification is not weaker { 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 stronger + ensures result < 20 + y // error: specification is not weaker { 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 stronger + ensures result < 20 + y // error: specification is not weaker { 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 stronger + ensures h(y) < 20 + y // error: specification is not weaker { 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 // error: specification is not stronger + ensures d(y) < 20 + y { 5 + 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 stronger + ensures result < 20 + y { 5 + y } // g names the result in just the class function method g(y: nat): (result: nat) - ensures result < 20 + y // error: specification is not stronger + ensures result < 20 + y { 5 + y } // h names the result in just the trait function method h(y: nat): nat - ensures h(y) < 20 + y // error: specification is not stronger + ensures h(y) < 20 + y { 5 + y } } diff --git a/Test/dafny4/git-issue245.dfy.expect b/Test/dafny4/git-issue245.dfy.expect index 52dc0dd66b2..f154a354f05 100644 --- a/Test/dafny4/git-issue245.dfy.expect +++ b/Test/dafny4/git-issue245.dfy.expect @@ -2,10 +2,6 @@ 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. @@ -15,4 +11,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 24 verified, 12 errors +Dafny program verifier finished with 28 verified, 8 errors diff --git a/Test/git-issues/git-issue-2500.dfy b/Test/git-issues/git-issue-2500.dfy deleted file mode 100644 index 0066c9df862..00000000000 --- a/Test/git-issues/git-issue-2500.dfy +++ /dev/null @@ -1,29 +0,0 @@ -// 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 Class 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 } -} diff --git a/Test/git-issues/git-issue-2500.dfy.expect b/Test/git-issues/git-issue-2500.dfy.expect deleted file mode 100644 index 6b05539973a..00000000000 --- a/Test/git-issues/git-issue-2500.dfy.expect +++ /dev/null @@ -1,6 +0,0 @@ -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 6 verified, 4 errors diff --git a/docs/dev/news/3223.fix b/docs/dev/news/3223.fix deleted file mode 100644 index 96e3176bae2..00000000000 --- a/docs/dev/news/3223.fix +++ /dev/null @@ -1 +0,0 @@ -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.