From 1f0d29bd25fda01c9c1da3c9842c085273f285df Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 24 Nov 2022 18:53:56 +0100 Subject: [PATCH 01/16] skip equality generation in the check --- Source/DafnyCore/Compilers/Compiler-js.cs | 2 +- Source/DafnyCore/Compilers/Compiler-python.cs | 5 +--- .../Verifier/Translator.ClassMembers.cs | 20 +++++++------- Source/DafnyCore/Verifier/Translator.cs | 27 +++++++++++++++++-- 4 files changed, 38 insertions(+), 16 deletions(-) diff --git a/Source/DafnyCore/Compilers/Compiler-js.cs b/Source/DafnyCore/Compilers/Compiler-js.cs index f3a4f508efd..043f5eb7357 100644 --- a/Source/DafnyCore/Compilers/Compiler-js.cs +++ b/Source/DafnyCore/Compilers/Compiler-js.cs @@ -2527,9 +2527,9 @@ bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, str var psi = new ProcessStartInfo("node", "") { RedirectStandardInput = true, - StandardInputEncoding = Encoding.UTF8, RedirectStandardOutput = true, RedirectStandardError = true, + StandardInputEncoding = Encoding.UTF8, }; try { diff --git a/Source/DafnyCore/Compilers/Compiler-python.cs b/Source/DafnyCore/Compilers/Compiler-python.cs index 0f339170e59..2a6a98cd561 100644 --- a/Source/DafnyCore/Compilers/Compiler-python.cs +++ b/Source/DafnyCore/Compilers/Compiler-python.cs @@ -1752,10 +1752,7 @@ private static string FindModuleName(string externFilename) { } } rd.Close(); - if (externFilename.EndsWith(".py")) { - return externFilename.Substring(0, externFilename.Length - 3); - } - return null; + return externFilename.EndsWith(".py") ? externFilename[..^3] : null; } static bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextWriter outputWriter) { diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index feaf321a2cd..3ac9746ca34 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -920,18 +920,19 @@ 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 +947,9 @@ private void AddFunctionOverrideCheckImpl(Function f) { //adding assert W <= Frame’ AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap, typeMap); - //adding assume Q; assert Post’; + //adding assume Q; //adding assume J.F(ins) == C.F(ins); + //assert Post’; AddFunctionOverrideEnsChk(f, builder, etran, substMap, typeMap, implInParams, implOutParams.Count == 0 ? null : implOutParams[0]); var stmts = builder.Collect(f.tok); diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index e6c0308856b..acee206c8a8 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -3487,6 +3487,7 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder } //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(); @@ -3530,9 +3531,32 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder 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) { + Bpl.FunctionCall funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType))); + List 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))); + + Bpl.Expr 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))); } @@ -3540,8 +3564,7 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder //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)) { + foreach (var s in TrSplitExpr(postcond, etran, false, out _)) { if (s.IsChecked) { builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true))); } From b99bff814d34700d953d9d33fb3c4177fa722532 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 24 Nov 2022 18:56:39 +0100 Subject: [PATCH 02/16] delete dead code --- Source/DafnyCore/Verifier/Translator.cs | 47 ------------------------- 1 file changed, 47 deletions(-) diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index acee206c8a8..dabc29ca843 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -3486,53 +3486,6 @@ 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) { Bpl.FunctionCall funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType))); From 342be576b64c06730c099f5410d04545d2836881 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 20 Dec 2022 01:06:59 +0100 Subject: [PATCH 03/16] hide override axiom --- Source/DafnyCore/Substituter.cs | 2 +- .../Verifier/FunctionCallSubstituter.cs | 8 ++++---- .../Verifier/Translator.ClassMembers.cs | 6 +++--- .../Translator.ExpressionTranslator.cs | 4 ++-- Source/DafnyCore/Verifier/Translator.cs | 20 +++++++++---------- 5 files changed, 19 insertions(+), 21 deletions(-) diff --git a/Source/DafnyCore/Substituter.cs b/Source/DafnyCore/Substituter.cs index b353994c2f3..b583402407a 100644 --- a/Source/DafnyCore/Substituter.cs +++ b/Source/DafnyCore/Substituter.cs @@ -54,7 +54,7 @@ public virtual Expression Substitute(Expression expr) { } else if (expr is WildcardExpr) { // nothing to substitute } else if (expr is ThisExpr) { - return receiverReplacement == null ? expr : receiverReplacement; + return receiverReplacement ?? expr; } else if (expr is IdentifierExpr) { IdentifierExpr e = (IdentifierExpr)expr; Expression substExpr; diff --git a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs index be765714d9b..2fb42955230 100644 --- a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs +++ b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs @@ -3,8 +3,8 @@ 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()) { + public FunctionCallSubstituter(Expression receiverReplacement, Dictionary/*!*/ substMap, Dictionary typeMap, Function a, Function b) + : base(receiverReplacement, substMap, typeMap) { A = a; B = b; } @@ -21,8 +21,8 @@ public override Expression Substitute(Expression expr) { newFce.Function = e.Function; newFce.Type = e.Type; } - newFce.TypeApplication_AtEnclosingClass = e.TypeApplication_AtEnclosingClass; // resolve here - newFce.TypeApplication_JustFunction = e.TypeApplication_JustFunction; // resolve here + newFce.TypeApplication_AtEnclosingClass = SubstituteTypeList(e.TypeApplication_AtEnclosingClass); // resolve here + newFce.TypeApplication_JustFunction = SubstituteTypeList(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 3ac9746ca34..d7e6a3c483b 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -213,7 +213,7 @@ 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()); + heightAntecedent = Bpl.Expr.Lt(Bpl.Expr.Literal(cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf) * 2 + 1), etran.FunctionContextHeight()); } } @@ -878,7 +878,7 @@ 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)); + req.Add(Requires(f.tok, true, etran.HeightContext(f.OverriddenFunction, true), null, null)); if (f is TwoStateFunction) { // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); @@ -1136,7 +1136,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); } diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs index b5391b4dc38..54cd2dcf7dd 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs @@ -258,12 +258,12 @@ 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 reducedScope = 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()); + Boogie.Expr.Eq(Boogie.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(m) * 2 + (reducedScope ? 0 : 1)), FunctionContextHeight()); return context; } diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index f9acf2721d1..595e6432350 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -2159,7 +2159,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis // 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()); + (Bpl.Expr)Bpl.Expr.Le(Bpl.Expr.Literal((mod.CallGraph.GetSCCRepresentativePredecessorCount(f) + 1) * 2), 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,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 hidden = 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()); + return Expr.Le(Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(f) * 2 + (hidden ? 1 : 0)), etran.FunctionContextHeight()); } else { return Bpl.Expr.True; } @@ -2511,7 +2510,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { 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)), + : Bpl.Expr.Le(Bpl.Expr.Literal((mod.CallGraph.GetSCCRepresentativePredecessorCount(f) + 1) * 2), etran.FunctionContextHeight()); // ante := (useViaContext && typeAnte && pre) ante = BplAnd(useViaContext, BplAnd(ante, pre)); @@ -3516,11 +3515,10 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder //generating trait post-conditions with class variables foreach (var en in f.OverriddenFunction.Ens) { - Expression postcond = Substitute(en.E, null, substMap, typeMap); - foreach (var s in TrSplitExpr(postcond, etran, false, out _)) { - if (s.IsChecked) { - builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true))); - } + var sub = new FunctionCallSubstituter(new ImplicitThisExpr(f.tok) { Type = Resolver.GetThisType(f.tok, (TopLevelDeclWithMembers)f.EnclosingClass) }, substMap, typeMap, f.OverriddenFunction, f); + Expression postcond = sub.Substitute(en.E); + foreach (var s in TrSplitExpr(postcond, etran, false, out _).Where(s => s.IsChecked)) { + builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true))); } } } @@ -4744,7 +4742,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; From d37cf046d886d05df8a0e382de98ce54c98f7696 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 20 Dec 2022 01:39:47 +0100 Subject: [PATCH 04/16] tuned --- .../Verifier/Translator.ClassMembers.cs | 5 +---- Source/DafnyCore/Verifier/Translator.cs | 21 ++++++++++--------- 2 files changed, 12 insertions(+), 14 deletions(-) diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index d7e6a3c483b..66f46824b8b 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -922,10 +922,7 @@ 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 - }; + var ie = new IdentifierExpr(formal.tok, formal.AssignUniqueName(f.IdGenerator)) { Var = formal, Type = formal.Type }; substMap.Add(overriddenFormal, ie); } diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 595e6432350..8de286df26b 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -2156,10 +2156,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.Le(Bpl.Expr.Literal((mod.CallGraph.GetSCCRepresentativePredecessorCount(f) + 1) * 2), etran.FunctionContextHeight()); + // useViaContext: fh < FunctionContextHeight + var lowerBound = (f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f) + 1) * 2; + Expr useViaContext = !InVerificationScope(f) ? Bpl.Expr.True : Expr.Le(Expr.Literal(lowerBound), 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)); @@ -2261,7 +2260,8 @@ Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran, bool hidden = f var module = f.EnclosingClass.EnclosingModuleDefinition; if (InVerificationScope(f)) { - return Expr.Le(Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(f) * 2 + (hidden ? 1 : 0)), etran.FunctionContextHeight()); + var lowerBound = module.CallGraph.GetSCCRepresentativePredecessorCount(f) * 2 + (hidden ? 1 : 0); + return Expr.Le(Expr.Literal(lowerBound), etran.FunctionContextHeight()); } else { return Bpl.Expr.True; } @@ -3487,8 +3487,8 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder //generating assume C.F(ins) == out, if a result variable was given if (resultVariable != null) { - Bpl.FunctionCall funcIdC = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType))); - List argsC = new List(); + var funcIdC = new FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType))); + List argsC = new List(); // add type arguments argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy)); @@ -3508,14 +3508,15 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder argsC.AddRange(implInParams.Select(var => new Bpl.IdentifierExpr(f.tok, var))); - Bpl.Expr funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC); + Expr 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))); + builder.Add(TrAssumeCmd(f.tok, Expr.Eq(funcExpC, resultVar))); } //generating trait post-conditions with class variables foreach (var en in f.OverriddenFunction.Ens) { - var sub = new FunctionCallSubstituter(new ImplicitThisExpr(f.tok) { Type = Resolver.GetThisType(f.tok, (TopLevelDeclWithMembers)f.EnclosingClass) }, substMap, typeMap, f.OverriddenFunction, f); + var receiver = new ImplicitThisExpr(f.tok) { Type = Resolver.GetThisType(f.tok, (TopLevelDeclWithMembers)f.EnclosingClass) }; + var sub = new FunctionCallSubstituter(receiver, substMap, typeMap, f.OverriddenFunction, f); Expression postcond = sub.Substitute(en.E); foreach (var s in TrSplitExpr(postcond, etran, false, out _).Where(s => s.IsChecked)) { builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true))); From d1eb5a88c87b868e5bf78a6bc8570f2f95fe5f2b Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 21 Dec 2022 01:21:25 +0100 Subject: [PATCH 05/16] review --- .../Verifier/Translator.ClassMembers.cs | 6 +-- .../Translator.ExpressionTranslator.cs | 5 +-- Source/DafnyCore/Verifier/Translator.cs | 38 +++++++++++-------- Test/git-issues/git-issue-2500.dfy | 22 +++++++++++ Test/git-issues/git-issue-2500.dfy.expect | 3 ++ docs/dev/news/3223.fix | 1 + 6 files changed, 53 insertions(+), 22 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/3223.fix diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 66f46824b8b..54e1b6393b0 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -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) * 2 + 1), etran.FunctionContextHeight()); + var visibilityLevel = cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf); + heightAntecedent = Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight()); } } @@ -877,7 +878,7 @@ private void AddFunctionOverrideCheckImpl(Function f) { } // the procedure itself var req = new List(); - // free requires mh == ModuleContextHeight && fh == FunctionContextHeight; + // free requires fh == FunctionContextHeight; req.Add(Requires(f.tok, true, etran.HeightContext(f.OverriddenFunction, true), null, null)); if (f is TwoStateFunction) { // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) @@ -945,7 +946,6 @@ private void AddFunctionOverrideCheckImpl(Function f) { AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap, typeMap); //adding assume Q; - //adding assume J.F(ins) == C.F(ins); //assert Post’; AddFunctionOverrideEnsChk(f, builder, etran, substMap, typeMap, implInParams, implOutParams.Count == 0 ? null : implOutParams[0]); diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs index 54cd2dcf7dd..e8052706bba 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs @@ -261,9 +261,8 @@ public Boogie.IdentifierExpr FunctionContextHeight() { public Boogie.Expr HeightContext(ICallable m, bool reducedScope = 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) * 2 + (reducedScope ? 0 : 1)), FunctionContextHeight()); + var visibilityLevel = m.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(m); + Boogie.Expr context = Boogie.Expr.Eq(MkFunctionHeight(visibilityLevel, reducedScope), FunctionContextHeight()); return context; } diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 8de286df26b..79e95334eb8 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -2053,7 +2053,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,8 +2157,8 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis pre = BplAnd(pre, etran.TrExpr(Substitute(req.E, null, substMap))); } // useViaContext: fh < FunctionContextHeight - var lowerBound = (f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f) + 1) * 2; - Expr useViaContext = !InVerificationScope(f) ? Bpl.Expr.True : Expr.Le(Expr.Literal(lowerBound), etran.FunctionContextHeight()); + var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f); + Expr useViaContext = !InVerificationScope(f) ? Bpl.Expr.True : 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)); @@ -2253,15 +2253,14 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis return (olderParameterCount, olderCondition); } - Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran, bool hidden = false) { + 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)) { - var lowerBound = module.CallGraph.GetSCCRepresentativePredecessorCount(f) * 2 + (hidden ? 1 : 0); - return Expr.Le(Expr.Literal(lowerBound), etran.FunctionContextHeight()); + var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f); + return Expr.Le(MkFunctionHeight(visibilityLevel, !requiresFullScope), etran.FunctionContextHeight()); } else { return Bpl.Expr.True; } @@ -2301,7 +2300,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,12 +2505,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.Le(Bpl.Expr.Literal((mod.CallGraph.GetSCCRepresentativePredecessorCount(f) + 1) * 2), - etran.FunctionContextHeight()); + ? Bpl.Expr.True + : Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight()); // ante := (useViaContext && typeAnte && pre) ante = BplAnd(useViaContext, BplAnd(ante, pre)); @@ -3488,7 +3486,7 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder //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))); - List argsC = new List(); + var argsC = new List(); // add type arguments argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy)); @@ -3508,9 +3506,9 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder argsC.AddRange(implInParams.Select(var => new Bpl.IdentifierExpr(f.tok, var))); - Expr funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC); + var funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC); var resultVar = new Bpl.IdentifierExpr(resultVariable.tok, resultVariable); - builder.Add(TrAssumeCmd(f.tok, Expr.Eq(funcExpC, resultVar))); + builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, resultVar))); } //generating trait post-conditions with class variables @@ -10722,6 +10720,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/git-issues/git-issue-2500.dfy b/Test/git-issues/git-issue-2500.dfy new file mode 100644 index 00000000000..5a81b0976b4 --- /dev/null +++ b/Test/git-issues/git-issue-2500.dfy @@ -0,0 +1,22 @@ +// RUN: %dafny_0 /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module A { + trait {:termination false} Trait { + function TotallyNotZero() : (ret: int) + ensures ret != 0 + } +} + +module B { + import opened A + + class Class extends Trait { + constructor() {} + function TotallyNotZero() : (ret: int) + // Missing: ensures ret != 0 + { + 0 + } + } +} \ No newline at end of file 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..615348f4ff4 --- /dev/null +++ b/Test/git-issues/git-issue-2500.dfy.expect @@ -0,0 +1,3 @@ +git-issue-2500.dfy(16,13): Error: the function must provide an equal or more detailed postcondition than in its parent trait + +Dafny program verifier finished with 1 verified, 1 error diff --git a/docs/dev/news/3223.fix b/docs/dev/news/3223.fix new file mode 100644 index 00000000000..96e3176bae2 --- /dev/null +++ b/docs/dev/news/3223.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. From 117585e9f7355d13560150db043a5f4702a27188 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 21 Dec 2022 01:22:17 +0100 Subject: [PATCH 06/16] \n --- Test/git-issues/git-issue-2500.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/git-issues/git-issue-2500.dfy b/Test/git-issues/git-issue-2500.dfy index 5a81b0976b4..7745855f2a1 100644 --- a/Test/git-issues/git-issue-2500.dfy +++ b/Test/git-issues/git-issue-2500.dfy @@ -19,4 +19,4 @@ module B { 0 } } -} \ No newline at end of file +} From 922049d2834cc4273cdea7eb83eeabde0ca9c60e Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 4 Jan 2023 03:16:42 +0100 Subject: [PATCH 07/16] restict substitutions to occurences where `this` is the receiver --- .../DafnyCore/Verifier/FunctionCallSubstituter.cs | 13 +++++++------ Source/DafnyCore/Verifier/Translator.cs | 6 ++---- 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs index 2fb42955230..63facf64f58 100644 --- a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs +++ b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs @@ -9,14 +9,15 @@ public FunctionCallSubstituter(Expression receiverReplacement, Dictionary newArgs = SubstituteExprList(e.Args); - FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, e.CloseParen, newArgs, e.AtLabel); - if (e.Function == A) { + 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) { newFce.Function = B; newFce.Type = e.Type; // TODO: this may not work with type parameters. + //update receiver type + receiver.Type = Resolver.GetThisType(B.tok, (TopLevelDeclWithMembers)B.EnclosingClass); } else { newFce.Function = e.Function; newFce.Type = e.Type; diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 79e95334eb8..dfeb6bf1717 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -3513,10 +3513,8 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder //generating trait post-conditions with class variables foreach (var en in f.OverriddenFunction.Ens) { - var receiver = new ImplicitThisExpr(f.tok) { Type = Resolver.GetThisType(f.tok, (TopLevelDeclWithMembers)f.EnclosingClass) }; - var sub = new FunctionCallSubstituter(receiver, substMap, typeMap, f.OverriddenFunction, f); - Expression postcond = sub.Substitute(en.E); - foreach (var s in TrSplitExpr(postcond, etran, false, out _).Where(s => s.IsChecked)) { + 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))); } } From 1dc1ed41045299d36d11742099c80889387ca7ec Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Wed, 4 Jan 2023 03:27:08 +0100 Subject: [PATCH 08/16] use correct hight --- Source/DafnyCore/Verifier/Translator.ClassMembers.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index 54e1b6393b0..0a708d1c48a 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -879,7 +879,7 @@ 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.OverriddenFunction, true), null, null)); + 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); From 0a3d964ad01945b19f28dce9dc7f6d00745c8113 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 5 Jan 2023 02:27:42 +0100 Subject: [PATCH 09/16] fix tests --- Test/concurrency/10-SequenceInvariant.dfy | 4 ++-- Test/concurrency/11-MutexGuard2.dfy | 4 ++-- Test/concurrency/12-MutexLifetime-short.dfy | 4 ++-- Test/dafny4/git-issue245.dfy | 8 ++++---- Test/dafny4/git-issue245.dfy.expect | 6 +++++- Test/git-issues/git-issue-2500.dfy | 2 +- 6 files changed, 16 insertions(+), 12 deletions(-) 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..995728a0aaf 100644 --- a/Test/dafny4/git-issue245.dfy +++ b/Test/dafny4/git-issue245.dfy @@ -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 weaker { 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 weaker { 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 weaker { 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 weaker { 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 index 7745855f2a1..cab41145a0c 100644 --- a/Test/git-issues/git-issue-2500.dfy +++ b/Test/git-issues/git-issue-2500.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny_0 /compile:0 "%s" > "%t" +// RUN: %exits-with 4 %dafny /compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" module A { From 2ee54f7f985e48861ea8ae0a22b274689b4a6c2a Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 5 Jan 2023 03:20:54 +0100 Subject: [PATCH 10/16] add tests --- Test/git-issues/git-issue-2500.dfy | 32 ++++++++++++----------- Test/git-issues/git-issue-2500.dfy.expect | 6 +++-- 2 files changed, 21 insertions(+), 17 deletions(-) diff --git a/Test/git-issues/git-issue-2500.dfy b/Test/git-issues/git-issue-2500.dfy index cab41145a0c..16a9f172758 100644 --- a/Test/git-issues/git-issue-2500.dfy +++ b/Test/git-issues/git-issue-2500.dfy @@ -1,22 +1,24 @@ // RUN: %exits-with 4 %dafny /compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -module A { - trait {:termination false} Trait { - function TotallyNotZero() : (ret: int) - ensures ret != 0 +module M { + trait {:termination false} Tr { + function True(): (ret: bool) ensures ret + function True'(): (ret: bool) ensures True'() + function Other(x:nat, free: Tr): bool + ensures x != 0 && free.Other(x-1, free) ==> Other(x-1, free) } } -module B { - import opened A - - class Class extends Trait { - constructor() {} - function TotallyNotZero() : (ret: int) - // Missing: ensures ret != 0 - { - 0 - } - } +class Class extends M.Tr { + function True(): (ret: bool) + // Missing: ensures ret != 0 + { false } + function True'(): (ret: bool) + // Missing: ensures True'() + { false } + 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 index 615348f4ff4..d98b7a4102d 100644 --- a/Test/git-issues/git-issue-2500.dfy.expect +++ b/Test/git-issues/git-issue-2500.dfy.expect @@ -1,3 +1,5 @@ -git-issue-2500.dfy(16,13): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue-2500.dfy(14,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue-2500.dfy(17,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait +git-issue-2500.dfy(20,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait -Dafny program verifier finished with 1 verified, 1 error +Dafny program verifier finished with 4 verified, 3 errors From 0c3cb41c9e84c4bf1b16cc66d9fefc14de9ed3a4 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 5 Jan 2023 03:41:13 +0100 Subject: [PATCH 11/16] typo --- Test/git-issues/git-issue-2500.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/git-issues/git-issue-2500.dfy b/Test/git-issues/git-issue-2500.dfy index 16a9f172758..d221871a1d0 100644 --- a/Test/git-issues/git-issue-2500.dfy +++ b/Test/git-issues/git-issue-2500.dfy @@ -18,7 +18,7 @@ class Class extends M.Tr { // Missing: ensures True'() { false } function Other(x: nat, free: M.Tr): bool - // Different Receiver + // Different receiver ensures x != 0 && Other(x-1, free) ==> Other(x-1, free) { false } } From 54e1cfdaf96694468ec7267fa770cf17c0627f11 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 5 Jan 2023 03:45:50 +0100 Subject: [PATCH 12/16] remove comment --- Source/DafnyCore/Verifier/FunctionCallSubstituter.cs | 1 - 1 file changed, 1 deletion(-) diff --git a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs index 63facf64f58..db582f56305 100644 --- a/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs +++ b/Source/DafnyCore/Verifier/FunctionCallSubstituter.cs @@ -16,7 +16,6 @@ public override Expression Substitute(Expression expr) { if (e.Function == A && e.Receiver is ThisExpr && receiver is ThisExpr) { newFce.Function = B; newFce.Type = e.Type; // TODO: this may not work with type parameters. - //update receiver type receiver.Type = Resolver.GetThisType(B.tok, (TopLevelDeclWithMembers)B.EnclosingClass); } else { newFce.Function = e.Function; From 923f38a710712e3f8594bb754f14ee71f7e691b1 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 5 Jan 2023 04:05:36 +0100 Subject: [PATCH 13/16] add comment about incompleteness of the encoding --- Source/DafnyCore/Verifier/Translator.cs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 3df44ca8bac..c6b45ab2541 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -3514,6 +3514,9 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder //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))); From d9ae00aef01340be3955527c872189d09ddf7606 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 19 Jan 2023 21:11:31 +0100 Subject: [PATCH 14/16] weaker -> stronger --- Test/dafny4/git-issue245.dfy | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/Test/dafny4/git-issue245.dfy b/Test/dafny4/git-issue245.dfy index 995728a0aaf..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 // error: specification is not weaker + 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 // error: specification is not weaker + 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 // error: specification is not weaker + 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 // error: specification is not weaker + ensures h(y) < 20 + y // error: specification is not stronger { 5 + y } } From ee6c02d28b78cf7e0c921952a1623ec37ca28beb Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 20 Jan 2023 03:02:37 +0100 Subject: [PATCH 15/16] document deficiency of the encoding --- Source/DafnyCore/Verifier/Translator.cs | 4 ++-- Test/git-issues/git-issue-2500.dfy | 7 ++++++- Test/git-issues/git-issue-2500.dfy.expect | 9 +++++---- 3 files changed, 13 insertions(+), 7 deletions(-) diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index c6b45ab2541..ff9cd2f1dfe 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -2158,8 +2158,8 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis pre = BplAnd(pre, etran.TrExpr(Substitute(req.E, null, substMap))); } // useViaContext: fh < FunctionContextHeight - var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f); - Expr useViaContext = !InVerificationScope(f) ? Bpl.Expr.True : Expr.Lt(MkFunctionHeight(visibilityLevel), etran.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)); diff --git a/Test/git-issues/git-issue-2500.dfy b/Test/git-issues/git-issue-2500.dfy index d221871a1d0..0066c9df862 100644 --- a/Test/git-issues/git-issue-2500.dfy +++ b/Test/git-issues/git-issue-2500.dfy @@ -5,6 +5,7 @@ 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) } @@ -12,11 +13,15 @@ module M { class Class extends M.Tr { function True(): (ret: bool) - // Missing: ensures ret != 0 + // 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) diff --git a/Test/git-issues/git-issue-2500.dfy.expect b/Test/git-issues/git-issue-2500.dfy.expect index d98b7a4102d..6b05539973a 100644 --- a/Test/git-issues/git-issue-2500.dfy.expect +++ b/Test/git-issues/git-issue-2500.dfy.expect @@ -1,5 +1,6 @@ -git-issue-2500.dfy(14,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait -git-issue-2500.dfy(17,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait -git-issue-2500.dfy(20,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait +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 4 verified, 3 errors +Dafny program verifier finished with 6 verified, 4 errors From a86643c190f5251147df9e0c70135786cdfc3918 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 20 Jan 2023 03:12:30 +0100 Subject: [PATCH 16/16] rename --- Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs index f72f6a633b5..35c1b85f727 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs @@ -258,11 +258,11 @@ public Boogie.IdentifierExpr FunctionContextHeight() { return new Boogie.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Boogie.Type.Int); } - public Boogie.Expr HeightContext(ICallable m, bool reducedScope = false) { + public Boogie.Expr HeightContext(ICallable m, bool intermediateScope = false) { Contract.Requires(m != null); // free requires fh == FunctionContextHeight; var visibilityLevel = m.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(m); - Boogie.Expr context = Boogie.Expr.Eq(MkFunctionHeight(visibilityLevel, reducedScope), FunctionContextHeight()); + Boogie.Expr context = Boogie.Expr.Eq(MkFunctionHeight(visibilityLevel, intermediateScope), FunctionContextHeight()); return context; }