From 993b589d660816ee013cdf0d5ab885f0a118df17 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Sat, 25 Feb 2023 21:01:06 +0100 Subject: [PATCH] fix: Override checks with `canCall` precondition (#3479) We strengthen this check by performing it on the visibility level of the implementing function, but restricting the enabled axiom to the callers of the trait. To achieve this, we add the canCall precondition to the axiom. Additionally, we consider imported trait functions when computing the visibility levels. Fixes #2500. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../DafnyCore/Compilers/Java/Compiler-java.cs | 6 +- Source/DafnyCore/Resolver/CallGraphBuilder.cs | 3 + .../Verifier/FunctionCallSubstituter.cs | 46 ++++--- .../Verifier/Translator.ClassMembers.cs | 101 +++++++------- Source/DafnyCore/Verifier/Translator.cs | 123 +++++++----------- Test/concurrency/01-InnerOuter.dfy | 2 +- Test/concurrency/01-InnerOuter.dfy.expect | 2 +- Test/concurrency/02-DoubleRead.dfy | 2 +- Test/concurrency/02-DoubleRead.dfy.expect | 2 +- Test/concurrency/03-SimpleCounter.dfy | 2 +- Test/concurrency/03-SimpleCounter.dfy.expect | 2 +- 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 | 81 ++++++++++++ Test/git-issues/git-issue-2500.dfy.expect | 6 + docs/dev/news/3479.fix | 1 + 19 files changed, 247 insertions(+), 168 deletions(-) create mode 100644 Test/git-issues/git-issue-2500.dfy create mode 100644 Test/git-issues/git-issue-2500.dfy.expect create mode 100644 docs/dev/news/3479.fix diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs index 03fd4a3bd9e..1d110cd315f 100644 --- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs @@ -1801,8 +1801,8 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { wr.Write($"public static{justTypeArgs} {DtT_protected} {DtCreateName(ctor)}("); WriteFormals("", ctor.Formals, wr); - var w = wr.NewBlock(")"); - w.Write($"return new {DtCtorDeclarationName(ctor, dt.TypeArgs)}({ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});"); + wr.NewBlock(")") + .WriteLine($"return new {DtCtorDeclarationName(ctor, dt.TypeArgs)}({ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});"); } if (dt.IsRecordType) { @@ -1813,7 +1813,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) { wr.Write($"public static{justTypeArgs} {DtT_protected} create_{ctor.CompileName}("); WriteFormals("", ctor.Formals, wr); wr.NewBlock(")") - .Write($"return create({ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});"); + .WriteLine($"return create({ctor.Formals.Where(f => !f.IsGhost).Comma(FormalName)});"); } // query properties diff --git a/Source/DafnyCore/Resolver/CallGraphBuilder.cs b/Source/DafnyCore/Resolver/CallGraphBuilder.cs index 1122c328080..d6377bfb229 100644 --- a/Source/DafnyCore/Resolver/CallGraphBuilder.cs +++ b/Source/DafnyCore/Resolver/CallGraphBuilder.cs @@ -295,6 +295,9 @@ public static void AddCallGraphEdge(IASTVisitorContext callingContext, ICallable ModuleDefinition calleeModule = callable is SpecialFunction ? null : callable.EnclosingModule; if (callerModule != calleeModule) { // inter-module call; don't record in call graph + if (callingContext is ICallable context && callable is Function { EnclosingClass: TraitDecl }) { + callerModule.CallGraph.AddEdge(context, callable); + } return; } diff --git a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs index be765714d9b..bea1d11dfae 100644 --- a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs +++ b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs @@ -1,30 +1,38 @@ using System.Collections.Generic; +using System.Linq; 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; + + // 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. + 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 || Tr.InheritedMembers.Contains(e.Function)) && 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..fa0aee6f06b 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); @@ -877,8 +877,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), 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 +920,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); } @@ -947,7 +945,6 @@ private void AddFunctionOverrideCheckImpl(Function f) { AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap, typeMap); //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); @@ -956,9 +953,9 @@ private void AddFunctionOverrideCheckImpl(Function f) { // emit the impl only when there are proof obligations. QKeyValue kv = etran.TrAttributes(f.Attributes, null); - var impl = AddImplementationWithVerboseName(f.tok, proc, - Util.Concat(Util.Concat(typeInParams, inParams_Heap), implInParams), - implOutParams, localVariables, stmts, kv); + AddImplementationWithVerboseName(f.tok, proc, + Util.Concat(Util.Concat(typeInParams, inParams_Heap), implInParams), + implOutParams, localVariables, stmts, kv); } if (InsertChecksums) { @@ -999,7 +996,7 @@ private void AddOverrideCheckTypeArgumentInstantiations(MemberDecl member, Boogi /// axiom (forall $heap: HeapType, typeArgs: Ty, this: ref, x#0: int, fuel: LayerType :: /// { J.F(fuel, $heap, G(typeArgs), this, x#0), C.F(fuel, $heap, typeArgs, this, x#0) } /// { J.F(fuel, $heap, G(typeArgs), this, x#0), $Is(this, C) } - /// this != null && $Is(this, C) + /// C.F#canCall(args) || (fh < FunctionContextHeight && this != null && $Is(this, C)) /// ==> /// J.F(fuel, $heap, G(typeArgs), this, x#0) == C.F(fuel, $heap, typeArgs, this, x#0)); /// (without the other usual antecedents). Essentially, the override gives a part of the body of the @@ -1043,19 +1040,20 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti argsJF.AddRange(GetTypeArguments(f, overridingFunction).ConvertAll(TypeToTy)); argsCF.AddRange(GetTypeArguments(overridingFunction, null).ConvertAll(TypeToTy)); + var moreArgsCF = new List(); + Expr layer = null; + // Add the fuel argument if (f.IsFuelAware()) { Contract.Assert(overridingFunction.IsFuelAware()); // f.IsFuelAware() ==> overridingFunction.IsFuelAware() var fuel = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, "$fuel", predef.LayerType)); forallFormals.Add(fuel); - var ly = new Boogie.IdentifierExpr(f.tok, fuel); - argsJF.Add(ly); - argsCF.Add(ly); + layer = new Boogie.IdentifierExpr(f.tok, fuel); + argsJF.Add(layer); } else if (overridingFunction.IsFuelAware()) { // We can't use a bound variable $fuel, because then one of the triggers won't be mentioning this $fuel. // Instead, we do the next best thing: use the literal $LZ. - var ly = new Boogie.IdentifierExpr(f.tok, "$LZ", predef.LayerType); // $LZ - argsCF.Add(ly); + layer = new Boogie.IdentifierExpr(f.tok, "$LZ", predef.LayerType); // $LZ } // Add heap arguments @@ -1063,7 +1061,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti Contract.Assert(bvPrevHeap != null); forallFormals.Add(bvPrevHeap); argsJF.Add(etran.Old.HeapExpr); - argsCF.Add(etran.Old.HeapExpr); + moreArgsCF.Add(etran.Old.HeapExpr); } if (AlwaysUseHeap || f.ReadsHeap || overridingFunction.ReadsHeap) { var heap = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType)); @@ -1072,7 +1070,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti argsJF.Add(new Boogie.IdentifierExpr(f.tok, heap)); } if (AlwaysUseHeap || overridingFunction.ReadsHeap) { - argsCF.Add(new Boogie.IdentifierExpr(overridingFunction.tok, heap)); + moreArgsCF.Add(new Boogie.IdentifierExpr(overridingFunction.tok, heap)); } } @@ -1082,10 +1080,12 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti forallFormals.Add(bvThis); var bvThisExpr = new Boogie.IdentifierExpr(f.tok, bvThis); argsJF.Add(bvThisExpr); - argsCF.Add(bvThisExpr); + moreArgsCF.Add(bvThisExpr); // $Is(this, C) var isOfSubtype = GetWhereClause(overridingFunction.tok, bvThisExpr, thisType, f is TwoStateFunction ? etran.Old : etran, IsAllocType.NEVERALLOC); + Bpl.Expr ante = Boogie.Expr.And(ReceiverNotNull(bvThisExpr), isOfSubtype); + // Add other arguments var typeMap = GetTypeArgumentSubstitutionMap(f, overridingFunction); foreach (Formal p in f.Formals) { @@ -1094,13 +1094,26 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti forallFormals.Add(bv); var jfArg = new Boogie.IdentifierExpr(p.tok, bv); argsJF.Add(ModeledAsBoxType(p.Type) ? BoxIfUnboxed(jfArg, pType) : jfArg); - argsCF.Add(new Boogie.IdentifierExpr(p.tok, bv)); + moreArgsCF.Add(new Boogie.IdentifierExpr(p.tok, bv)); } - // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight) - ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition; - Boogie.Expr useViaContext = !InVerificationScope(overridingFunction) ? (Boogie.Expr)Boogie.Expr.True : - Boogie.Expr.Neq(Boogie.Expr.Literal(mod.CallGraph.GetSCCRepresentativePredecessorCount(overridingFunction)), etran.FunctionContextHeight()); + // useViaContext: fh < FunctionContextHeight + Boogie.Expr useViaContext = !InVerificationScope(overridingFunction) + ? Boogie.Expr.True + : Boogie.Expr.Lt(Boogie.Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(overridingFunction)), etran.FunctionContextHeight()); + + // useViaCanCall: C.F#canCall(args) + Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(overridingFunction.tok, overridingFunction.FullSanitizedName + "#canCall", Bpl.Type.Bool); + Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), Concat(argsCF, moreArgsCF)); + + if (layer != null) { + argsCF.Add(layer); + } + + argsCF = Concat(argsCF, moreArgsCF); + + // ante := useViaCanCall || (useViaContext && this != null && $Is(this, C)) + ante = Bpl.Expr.Or(useViaCanCall, BplAnd(useViaContext, ante)); Boogie.Expr funcAppl; { @@ -1133,8 +1146,8 @@ 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); + Boogie.Expr.Imp(ante, synonyms)); + var activate = AxiomActivation(overridingFunction, 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); } @@ -1192,13 +1205,11 @@ private void AddMethodOverrideEnsChk(Method m, BoogieStmtListBuilder builder, Ex builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(en.E))); } //generating trait post-conditions with class variables + FunctionCallSubstituter sub = null; foreach (var en in m.OverriddenMethod.Ens) { - Expression postcond = Substitute(en.E, null, substMap, typeMap); - bool splitHappened; // we actually don't care - foreach (var s in TrSplitExpr(postcond, etran, false, out splitHappened)) { - if (s.IsChecked) { - builder.Add(Assert(m.tok, s.E, new PODesc.EnsuresStronger())); - } + sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassDecl)m.EnclosingClass); + foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) { + builder.Add(Assert(m.tok, s.E, new PODesc.EnsuresStronger())); } } } @@ -1211,18 +1222,14 @@ private void AddMethodOverrideReqsChk(Method m, BoogieStmtListBuilder builder, E Contract.Requires(etran != null); Contract.Requires(substMap != null); //generating trait pre-conditions with class variables + FunctionCallSubstituter sub = null; foreach (var req in m.OverriddenMethod.Req) { - Expression precond = Substitute(req.E, null, substMap, typeMap); - builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(precond))); + sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassDecl)m.EnclosingClass); + builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(sub.Substitute(req.E)))); } //generating class pre-conditions - foreach (var req in m.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(m.tok, s.E, new PODesc.RequiresWeaker())); - } - } + foreach (var s in m.Req.SelectMany(req => TrSplitExpr(req.E, etran, false, out _).Where(s => s.IsChecked))) { + builder.Add(Assert(m.tok, s.E, new PODesc.RequiresWeaker())); } } @@ -1381,7 +1388,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.cs b/Source/DafnyCore/Verifier/Translator.cs index 1fb4c2f1264..169864d8561 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -709,6 +709,7 @@ public Bpl.IdentifierExpr TrVar(IToken tok, IVariable var) { private Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { program = p; + this.forModule = forModule; Type.EnableScopes(); EstablishModuleScope(p.BuiltIns.SystemModule, forModule); @@ -2050,11 +2051,10 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis // // AXIOM_ACTIVATION // means: - // mh < ModuleContextHeight || - // (mh == ModuleContextHeight && fh <= FunctionContextHeight) + // 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 && @@ -2166,10 +2166,10 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis foreach (AttributedExpression req in f.Req) { pre = BplAnd(pre, etran.TrExpr(req.E)); } - // 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 + Expr useViaContext = !(InVerificationScope(f) || (f.EnclosingClass is TraitDecl)) + ? Bpl.Expr.True + : Bpl.Expr.Lt(Expr.Literal(forModule.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)); @@ -2276,11 +2276,9 @@ 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)) { return - Bpl.Expr.Le(Bpl.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight()); + Bpl.Expr.Le(Bpl.Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight()); } else { return Bpl.Expr.True; } @@ -2312,15 +2310,15 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { // // AXIOM_ACTIVATION // for visibility==ForeignModuleOnly, means: - // mh < ModuleContextHeight + // true // for visibility==IntraModuleOnly, means: - // mh == ModuleContextHeight && fh <= FunctionContextHeight + // fh <= FunctionContextHeight // // USE_VIA_CONTEXT // 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 && @@ -2525,12 +2523,11 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { return null; } - // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight) + // useViaContext: fh < FunctionContextHeight ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition; 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(Bpl.Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight()); // ante := (useViaContext && typeAnte && pre) ante = BplAnd(useViaContext, BplAnd(ante, pre)); @@ -3172,6 +3169,7 @@ Bpl.Expr InSeqRange(IToken tok, Bpl.Expr index, Type indexType, Bpl.Expr seq, bo } ModuleDefinition currentModule = null; // the module whose members are currently being translated + ModuleDefinition forModule = null; // the root module ICallable codeContext = null; // the method/iterator whose implementation is currently being translated or the function whose specification is being checked for well-formedness Bpl.LocalVariable yieldCountVariable = null; // non-null when an iterator body is being translated bool inBodyInitContext = false; // true during the translation of the .BodyInit portion of a divided constructor body @@ -3504,65 +3502,40 @@ 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 + FunctionCallSubstituter sub = null; 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))); - } + 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))); } } } @@ -3653,18 +3626,14 @@ private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builde Contract.Requires(etran != null); Contract.Requires(substMap != null); //generating trait pre-conditions with class variables + FunctionCallSubstituter sub = null; foreach (var req in f.OverriddenFunction.Req) { - Expression precond = Substitute(req.E, null, substMap, typeMap); - builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(precond))); + 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))); } } 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 a9bff354a68..00b90d095ff 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 ac2aca3197a..12f8f44288c 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 5598fa22a50..b2f99b05827 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..6764811860f --- /dev/null +++ b/Test/git-issues/git-issue-2500.dfy @@ -0,0 +1,81 @@ +// RUN: %exits-with 4 %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module M { + trait {:termination false} Top { + predicate ActuallyTrue() ensures ActuallyTrue() + } + trait {:termination false} Tr extends Top { + predicate True(): (ret: bool) ensures ret + predicate True'() ensures True'() + predicate ActuallyTrue'() ensures ActuallyTrue() + predicate ActuallyTrue''() ensures var alsoThis := this; alsoThis.ActuallyTrue() + predicate Other(x:nat, free: Tr) + ensures x != 0 && free.Other(x-1, free) ==> Other(x-1, free) + } + method X(tr: Tr) requires tr.ActuallyTrue() {} +} + +class Cl extends M.Tr { + constructor() {} + predicate True(): (ret: bool) + // Missing: ensures ret + { false } + predicate True'() + // Missing: ensures True'() + { false } + predicate ActuallyTrue() + ensures ActuallyTrue() + { true } + predicate ActuallyTrue'() + ensures ActuallyTrue() + { true } + predicate ActuallyTrue''() + // This is logically correct, but the disguised receiver in the Tr spec prevents the override check from passing. + ensures ActuallyTrue''() + { true } + predicate Other(x: nat, free: M.Tr) + // Different receiver + ensures x != 0 && Other(x-1, free) ==> Other(x-1, free) + { false } +} + +method Meh(tr: M.Tr) + requires tr.ActuallyTrue'() +{ + M.X(tr); +} + +module SSCinClass { + trait Trait { + predicate Even(i: nat) + predicate Odd(i: nat) + ensures i == 0 || (i % 2 == 1) == Even(i-1) + } + + class Class extends Trait { + predicate Even(i: nat) + { i == 0 || Odd(i-1) } + predicate Odd(i: nat) + ensures i == 0 || (i % 2 == 1) == Even(i-1) + { i != 0 && Even(i-1) } + } +} + +module SSCinBoth { + trait Trait { + predicate Even(i: nat) + ensures i == 0 || (i % 2 == 0) == Odd(i-1) + predicate Odd(i: nat) + ensures i == 0 || (i % 2 == 1) == Even(i-1) + } + + class Class extends Trait { + predicate Even(i: nat) + ensures i == 0 || (i % 2 == 0) == Odd(i-1) + { i == 0 || Odd(i-1) } + predicate Odd(i: nat) + ensures i == 0 || (i % 2 == 1) == Even(i-1) + { i != 0 && 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..64fcebbc922 --- /dev/null +++ b/Test/git-issues/git-issue-2500.dfy.expect @@ -0,0 +1,6 @@ +git-issue-2500.dfy(21,12): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue-2500.dfy(24,12): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue-2500.dfy(33,12): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue-2500.dfy(37,12): Error: the function must provide an equal or more detailed postcondition than in its parent trait + +Dafny program verifier finished with 26 verified, 4 errors diff --git a/docs/dev/news/3479.fix b/docs/dev/news/3479.fix new file mode 100644 index 00000000000..96e3176bae2 --- /dev/null +++ b/docs/dev/news/3479.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.