From 3397cdc9427cce7e0349b4c0fcfdbc959a304250 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 2 Aug 2024 00:04:55 +0200 Subject: [PATCH 01/19] parsing, printing, and resolution --- .../AST/Grammar/Printer/Printer.Statement.cs | 20 +++++++++++-- .../Assignment/AssignOrReturnStmt.cs | 18 ++++++++++-- .../AST/Statements/Assignment/UpdateStmt.cs | 22 ++++++++++++-- .../AST/Statements/Methods/CallStmt.cs | 9 ++++-- Source/DafnyCore/Dafny.atg | 29 ++++++++++++++----- .../PreType/PreTypeResolve.Statements.cs | 27 +++++++++++++++-- 6 files changed, 105 insertions(+), 20 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs index 7188e4da1f7..bac82478960 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs @@ -363,7 +363,7 @@ public void PrintStatement(Statement stmt, int indent) { wr.Write(" "); } PrintUpdateRHS(s, indent); - wr.Write(";"); + PrintBy(s); } else if (stmt is CallStmt) { // Most calls are printed from their concrete syntax given in the input. However, recursive calls to @@ -395,8 +395,7 @@ public void PrintStatement(Statement stmt, int indent) { wr.Write(" "); PrintUpdateRHS(s.Update, indent); } - wr.Write(";"); - + PrintBy(s.Update); } else if (stmt is VarDeclPattern) { var s = (VarDeclPattern)stmt; if (s.tok is AutoGeneratedToken) { @@ -455,6 +454,21 @@ public void PrintStatement(Statement stmt, int indent) { } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement } + + void PrintBy(ConcreteUpdateStatement s) + { + BlockStmt proof = s switch { + UpdateStmt updateStmt => updateStmt.Proof, + AssignOrReturnStmt returnStmt => returnStmt.Proof, + _ => null + }; + if (proof != null) { + wr.Write(" by "); + PrintStatement(proof, indent); + } else { + wr.Write(";"); + } + } } private void PrintRevealStmt(RevealStmt revealStmt) { diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs index 0b6199ae2bb..3b92730a0c2 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs @@ -9,6 +9,7 @@ public class AssignOrReturnStmt : ConcreteUpdateStatement, ICloneable Rhss; public readonly AttributedToken KeywordToken; + public readonly BlockStmt Proof; [FilledInDuringResolution] public readonly List ResolvedStatements = new List(); public override IEnumerable SubStatements => ResolvedStatements; public override IToken Tok { @@ -43,13 +44,14 @@ public AssignOrReturnStmt(Cloner cloner, AssignOrReturnStmt original) : base(clo Rhs = (ExprRhs)cloner.CloneRHS(original.Rhs); Rhss = original.Rhss.ConvertAll(cloner.CloneRHS); KeywordToken = cloner.AttributedTok(original.KeywordToken); + Proof = cloner.CloneBlockStmt(original.Proof); if (cloner.CloneResolvedFields) { ResolvedStatements = original.ResolvedStatements.Select(stmt => cloner.CloneStmt(stmt, false)).ToList(); } } - public AssignOrReturnStmt(RangeToken rangeToken, List lhss, ExprRhs rhs, AttributedToken keywordToken, List rhss) + public AssignOrReturnStmt(RangeToken rangeToken, List lhss, ExprRhs rhs, AttributedToken keywordToken, List rhss, BlockStmt proof = null) : base(rangeToken, lhss) { Contract.Requires(rangeToken != null); Contract.Requires(lhss != null); @@ -59,6 +61,7 @@ public AssignOrReturnStmt(RangeToken rangeToken, List lhss, ExprRhs Rhs = rhs; Rhss = rhss; KeywordToken = keywordToken; + Proof = proof; } public override IEnumerable PreResolveSubExpressions { @@ -190,6 +193,17 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti return; } + if (Proof != null) { + // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body + var prevLblStmts = resolver.EnclosingStatementLabels; + var prevLoopStack = resolver.LoopStack; + resolver.EnclosingStatementLabels = new Scope(resolver.Options); + resolver.LoopStack = new List(); + resolver.ResolveStatement(Proof, resolutionContext); + resolver.EnclosingStatementLabels = prevLblStmts; + resolver.LoopStack = prevLoopStack; + } + Expression lhsExtract = null; if (expectExtract) { if (resolutionContext.CodeContext is Method caller && caller.Outs.Count == 0 && KeywordToken == null) { @@ -285,7 +299,7 @@ private void DesugarElephantStatement(bool expectExtract, Expression lhsExtract, } } // " temp, ... := MethodOrExpression, ...;" - UpdateStmt up = new UpdateStmt(RangeToken, lhss2, rhss2); + UpdateStmt up = new UpdateStmt(RangeToken, lhss2, rhss2, Proof); if (expectExtract) { up.OriginalInitialLhs = Lhss.Count == 0 ? null : Lhss[0]; } diff --git a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs index cc3fe0507f1..7600c8cf2c3 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs @@ -8,6 +8,7 @@ public class UpdateStmt : ConcreteUpdateStatement, ICloneable, ICanR public readonly List Rhss; public readonly bool CanMutateKnownState; public Expression OriginalInitialLhs = null; + public readonly BlockStmt Proof; public override IToken Tok { get { @@ -45,26 +46,29 @@ public UpdateStmt Clone(Cloner cloner) { public UpdateStmt(Cloner cloner, UpdateStmt original) : base(cloner, original) { Rhss = original.Rhss.Select(cloner.CloneRHS).ToList(); CanMutateKnownState = original.CanMutateKnownState; + Proof = cloner.CloneBlockStmt(original.Proof); if (cloner.CloneResolvedFields) { ResolvedStatements = original.ResolvedStatements.Select(stmt => cloner.CloneStmt(stmt, false)).ToList(); } } - public UpdateStmt(RangeToken rangeToken, List lhss, List rhss) + public UpdateStmt(RangeToken rangeToken, List lhss, List rhss, BlockStmt proof = null) : base(rangeToken, lhss) { Contract.Requires(cce.NonNullElements(lhss)); Contract.Requires(cce.NonNullElements(rhss)); Contract.Requires(lhss.Count != 0 || rhss.Count == 1); Rhss = rhss; CanMutateKnownState = false; + Proof = proof; } - public UpdateStmt(RangeToken rangeToken, List lhss, List rhss, bool mutate) + public UpdateStmt(RangeToken rangeToken, List lhss, List rhss, bool mutate, BlockStmt proof = null) : base(rangeToken, lhss) { Contract.Requires(cce.NonNullElements(lhss)); Contract.Requires(cce.NonNullElements(rhss)); Contract.Requires(lhss.Count != 0 || rhss.Count == 1); Rhss = rhss; CanMutateKnownState = mutate; + Proof = proof; } public override IEnumerable PreResolveSubExpressions { @@ -123,6 +127,18 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti resolver.ResolveAttributes(rhs, resolutionContext); } + // resolve proof + if (Proof != null) { + // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body + var prevLblStmts = resolver.EnclosingStatementLabels; + var prevLoopStack = resolver.LoopStack; + resolver.EnclosingStatementLabels = new Scope(resolver.Options); + resolver.LoopStack = new List(); + resolver.ResolveStatement(Proof, resolutionContext); + resolver.EnclosingStatementLabels = prevLblStmts; + resolver.LoopStack = prevLoopStack; + } + // figure out what kind of UpdateStmt this is if (firstEffectfulRhs == null) { if (Lhss.Count == 0) { @@ -178,7 +194,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti foreach (var ll in Lhss) { resolvedLhss.Add(ll.Resolved); } - CallStmt a = new CallStmt(RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok); + CallStmt a = new CallStmt(RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok, Proof); a.OriginalInitialLhs = OriginalInitialLhs; ResolvedStatements.Add(a); } diff --git a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs index fc52debc2a6..41348dae006 100644 --- a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs +++ b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs @@ -25,11 +25,12 @@ void ObjectInvariant() { public readonly ActualBindings Bindings; public List Args => Bindings.Arguments; public Expression OriginalInitialLhs = null; + public readonly BlockStmt Proof; public Expression Receiver { get { return MethodSelect.Obj; } } public Method Method { get { return (Method)MethodSelect.Member; } } - public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr memSel, List args, IToken overrideToken = null) + public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr memSel, List args, IToken overrideToken = null, BlockStmt proof = null) : base(rangeToken) { Contract.Requires(rangeToken != null); Contract.Requires(cce.NonNullElements(lhs)); @@ -41,6 +42,7 @@ public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr me this.MethodSelect = memSel; this.overrideToken = overrideToken; this.Bindings = new ActualBindings(args); + Proof = proof; } public CallStmt Clone(Cloner cloner) { @@ -52,14 +54,15 @@ public CallStmt(Cloner cloner, CallStmt original) : base(cloner, original) { Lhs = original.Lhs.Select(cloner.CloneExpr).ToList(); Bindings = new ActualBindings(cloner, original.Bindings); overrideToken = original.overrideToken; + Proof = cloner.CloneBlockStmt(original.Proof); } /// /// This constructor is intended to be used when constructing a resolved CallStmt. The "args" are expected /// to be already resolved, and are all given positionally. /// - public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr memSel, List args) - : this(rangeToken, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e))) { + public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr memSel, List args, BlockStmt proof = null) + : this(rangeToken, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e)), proof: proof) { Bindings.AcceptArgumentExpressionsAsExactParameterList(); } diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 7ab991a715d..1571264c933 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -2288,6 +2288,7 @@ UpdateStmt List rhss = new List(); Expression e; AssignmentRhs r; + BlockStmt proof = null; IToken x = Token.NoToken; IToken endTok = Token.NoToken; IToken startToken = Token.NoToken; @@ -2325,10 +2326,16 @@ UpdateStmt { "," Rhs (. rhss.Add(r); .) } ) - ";" (. endTok = t; .) + ( + "by" BlockStmt + | ";" + ) | ":" (. SemErr(ErrorId.p_invalid_colon, new RangeToken(startToken, t), "invalid statement beginning here (is a 'label' keyword missing? or a 'const' or 'var' keyword?)"); .) | { Attribute } (. endToken = t; .) - ";" (. endTok = t; rhss.Add(new ExprRhs(e, attrs) { RangeToken = new RangeToken(e.StartToken, endToken) }); .) + ( + "by" BlockStmt + | ";" + ) (. endTok = t; rhss.Add(new ExprRhs(e, attrs) { RangeToken = new RangeToken(e.StartToken, endToken) }); .) | { Attribute } (. endToken = t; .) (. endTok = t; rhss.Add(new ExprRhs(e, attrs) { RangeToken = new RangeToken(e.StartToken, endToken) }); SemErr(ErrorId.p_missing_semicolon, new RangeToken(startToken, t), "missing semicolon at end of statement"); @@ -2343,18 +2350,22 @@ UpdateStmt { Attribute } (. exceptionRhs = new ExprRhs(exceptionExpr, attrs); .) { "," Rhs (. rhss.Add(r); .) } + ( + "by" BlockStmt + | ";" + ) ";" (. endTok = t; .) ) (. var rangeToken = new RangeToken(startToken, t); if (suchThat != null) { s = new AssignSuchThatStmt(rangeToken, lhss, suchThat, suchThatAssume, null); } else if (exceptionRhs != null) { - s = new AssignOrReturnStmt(rangeToken, lhss, exceptionRhs, keywordToken, rhss); + s = new AssignOrReturnStmt(rangeToken, lhss, exceptionRhs, keywordToken, rhss, proof); } else { if (lhss.Count == 0 && rhss.Count == 0) { s = new BlockStmt(rangeToken, new List()); // error, give empty statement } else { - s = new UpdateStmt(rangeToken, lhss, rhss); + s = new UpdateStmt(rangeToken, lhss, rhss, proof); } } .) @@ -2454,6 +2465,7 @@ VarDeclStatement<.out Statement/*!*/ s.> ExprRhs exceptionRhs = null; Attributes attrs = null; Attributes tokenAttrs = null; + BlockStmt proof = null; IToken endTok; IToken startToken = null; s = dummyStmt; @@ -2490,7 +2502,10 @@ VarDeclStatement<.out Statement/*!*/ s.> { "," Rhs (. rhss.Add(r); .) } ] - SYNC ";" (. endTok = t; .) + ( "by" + BlockStmt + | SYNC ";" (. endTok = t; .) + ) (. ConcreteUpdateStatement update; var lhsExprs = new List(); if (isGhost || (rhss.Count == 0 && exceptionRhs == null && suchThat == null)) { // explicitly ghost or no init @@ -2507,11 +2522,11 @@ VarDeclStatement<.out Statement/*!*/ s.> if (suchThat != null) { update = new AssignSuchThatStmt(updateRangeToken, lhsExprs, suchThat, suchThatAssume, attrs); } else if (exceptionRhs != null) { - update = new AssignOrReturnStmt(updateRangeToken, lhsExprs, exceptionRhs, keywordToken, rhss); + update = new AssignOrReturnStmt(updateRangeToken, lhsExprs, exceptionRhs, keywordToken, rhss, proof); } else if (rhss.Count == 0) { update = null; } else { - update = new UpdateStmt(updateRangeToken, lhsExprs, rhss); + update = new UpdateStmt(updateRangeToken, lhsExprs, rhss, proof); } s = new VarDeclStmt(rangeToken, lhss, update); .) diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index 87482480380..ef53afef95e 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -650,6 +650,18 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo ResolveAttributes(rhs, resolutionContext, false); } + // resolve proof + if (update.Proof != null) { + // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body + var prevLblStmts = resolver.EnclosingStatementLabels; + var prevLoopStack = resolver.LoopStack; + resolver.EnclosingStatementLabels = new Scope(resolver.Options); + resolver.LoopStack = new List(); + resolver.ResolveStatement(update.Proof, resolutionContext); + resolver.EnclosingStatementLabels = prevLblStmts; + resolver.LoopStack = prevLoopStack; + } + // figure out what kind of UpdateStmt this is if (firstEffectfulRhs == null) { if (update.Lhss.Count == 0) { @@ -703,7 +715,7 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo } else if (ErrorCount == errorCountBeforeCheckingStmt) { // a call statement var resolvedLhss = update.Lhss.ConvertAll(ll => ll.Resolved); - var a = new CallStmt(update.RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok); + var a = new CallStmt(update.RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok, update.Proof); a.OriginalInitialLhs = update.OriginalInitialLhs; update.ResolvedStatements.Add(a); } @@ -929,6 +941,17 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r return; } + if (s.Proof != null) { + // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body + var prevLblStmts = resolver.EnclosingStatementLabels; + var prevLoopStack = resolver.LoopStack; + resolver.EnclosingStatementLabels = new Scope(resolver.Options); + resolver.LoopStack = new List(); + resolver.ResolveStatement(s.Proof, resolutionContext); + resolver.EnclosingStatementLabels = prevLblStmts; + resolver.LoopStack = prevLoopStack; + } + Expression lhsExtract = null; if (expectExtract) { if (enclosingMethod.Outs.Count == 0 && s.KeywordToken == null) { @@ -991,7 +1014,7 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r } } // " temp, ... := MethodOrExpression, ...;" - UpdateStmt up = new UpdateStmt(s.RangeToken, lhss2, rhss2); + UpdateStmt up = new UpdateStmt(s.RangeToken, lhss2, rhss2, s.Proof); if (expectExtract) { up.OriginalInitialLhs = s.Lhss.Count == 0 ? null : s.Lhss[0]; } From 12edb9e2e5e4456a2fa89a62379dbbe02c842ed8 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 6 Aug 2024 12:37:55 +0200 Subject: [PATCH 02/19] fixes --- Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs | 3 +-- Source/DafnyCore/Dafny.atg | 5 ++--- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs index bac82478960..43e4aeeb79e 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs @@ -455,8 +455,7 @@ public void PrintStatement(Statement stmt, int indent) { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement } - void PrintBy(ConcreteUpdateStatement s) - { + void PrintBy(ConcreteUpdateStatement s) { BlockStmt proof = s switch { UpdateStmt updateStmt => updateStmt.Proof, AssignOrReturnStmt returnStmt => returnStmt.Proof, diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 1571264c933..c226669085d 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -2352,9 +2352,8 @@ UpdateStmt } ( "by" BlockStmt - | ";" - ) - ";" (. endTok = t; .) + | ";" (. endTok = t; .) + ) ) (. var rangeToken = new RangeToken(startToken, t); if (suchThat != null) { From cad8d068b8641e3f6cc45c1282cf223922546a83 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Tue, 6 Aug 2024 20:26:22 +0200 Subject: [PATCH 03/19] review and parser tweaks --- Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs | 4 ++-- Source/DafnyCore/Dafny.atg | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs index 43e4aeeb79e..f51bf358b59 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs @@ -455,8 +455,8 @@ public void PrintStatement(Statement stmt, int indent) { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement } - void PrintBy(ConcreteUpdateStatement s) { - BlockStmt proof = s switch { + void PrintBy(ConcreteUpdateStatement statement) { + BlockStmt proof = statement switch { UpdateStmt updateStmt => updateStmt.Proof, AssignOrReturnStmt returnStmt => returnStmt.Proof, _ => null diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index c226669085d..5a4b33aa199 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -2501,9 +2501,9 @@ VarDeclStatement<.out Statement/*!*/ s.> { "," Rhs (. rhss.Add(r); .) } ] - ( "by" + SYNC ( "by" BlockStmt - | SYNC ";" (. endTok = t; .) + | ";" (. endTok = t; .) ) (. ConcreteUpdateStatement update; var lhsExprs = new List(); From 0d9ce65c22900e4e351011552e9bcd773e146e84 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 8 Aug 2024 20:16:50 +0200 Subject: [PATCH 04/19] verifier changes --- .../Verifier/BoogieGenerator.Iterators.cs | 2 +- .../Verifier/BoogieGenerator.Methods.cs | 18 ++++++++-- .../Verifier/BoogieGenerator.TrStatement.cs | 33 ++++++++++++++----- Source/DafnyCore/Verifier/BoogieGenerator.cs | 10 +++--- 4 files changed, 47 insertions(+), 16 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs index 8d31c39e580..85a1bd6253f 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs @@ -95,7 +95,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { p.Label.E = etran.Old.TrExpr(p.E); } else { foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) { - if (kind == MethodTranslationKind.Call && RefinementToken.IsInherited(s.Tok, currentModule)) { + if (kind == MethodTranslationKind.CallPre && RefinementToken.IsInherited(s.Tok, currentModule)) { // this precondition was inherited into this module, so just ignore it } else { req.Add(Requires(s.Tok, s.IsOnlyFree, p.E, s.E, errorMessage, successMessage, comment)); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index 8bd75fda710..1193d3e87aa 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -193,7 +193,9 @@ void AddMethod_Top(Method m, bool isByMethod, bool includeAllMethods) { } // the method spec itself if (!isByMethod) { - sink.AddTopLevelDeclaration(AddMethod(m, MethodTranslationKind.Call)); + sink.AddTopLevelDeclaration(AddMethod(m, MethodTranslationKind.CallPre)); + sink.AddTopLevelDeclaration(AddMethod(m, MethodTranslationKind.CallPost)); + } if (m is ExtremeLemma) { // Let the CoCall and Impl forms to use m.PrefixLemma signature and specification (and @@ -1793,7 +1795,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { } } } - if (m is Constructor && kind == MethodTranslationKind.Call) { + if (m is Constructor && kind == MethodTranslationKind.CallPost) { var dafnyFresh = new OldExpr(Token.NoToken, new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Not, new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Allocated, new IdentifierExpr(Token.NoToken, "this")))); @@ -1818,6 +1820,18 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { } var name = MethodName(m, kind); + switch (kind) { + case MethodTranslationKind.CallPre: + outParams = new List(); + mod = new List(); + ens = new List(); + break; + case MethodTranslationKind.CallPost: + req = new List(); + break; + default: + break; + } var proc = new Boogie.Procedure(m.tok, name, new List(), inParams, outParams, false, req, mod, ens, etran.TrAttributes(m.Attributes, null)); AddVerboseNameAttribute(proc, m.FullDafnyName, kind); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 52e95ec4edb..5f8270c9f2c 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -1740,20 +1740,17 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E } } - MethodTranslationKind kind; + bool isCoCall = false; var callee = method; if (method is ExtremeLemma && isRecursiveCall) { - kind = MethodTranslationKind.CoCall; + isCoCall = true; callee = ((ExtremeLemma)method).PrefixLemma; } else if (method is PrefixLemma) { // an explicit call to a prefix lemma is allowed only inside the SCC of the corresponding greatest lemma, // so we consider this to be a co-call - kind = MethodTranslationKind.CoCall; - } else { - kind = MethodTranslationKind.Call; + isCoCall = true; } - var ins = new List(); if (callee is TwoStateLemma) { ins.Add(etran.OldAt(atLabel).HeapExpr); @@ -1949,10 +1946,19 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E } } - builder.Add(new CommentCmd("ProcessCallStmt: Make the call")); + var callBuilder = builder; + if (cs.Proof != null) { + callBuilder = new BoogieStmtListBuilder(this, options); + AddComment(callBuilder, cs, "call statement proof"); + CurrentIdGenerator.Push(); + TrStmt(cs.Proof, callBuilder, locals, etran); + CurrentIdGenerator.Pop(); + } + + callBuilder.Add(new CommentCmd($"ProcessCallStmt: {(isCoCall ? "Make the call" : "Check precondition")}")); // Make the call AddReferencedMember(callee); - Bpl.CallCmd call = Call(tok, MethodName(callee, kind), ins, outs); + Bpl.CallCmd call = Call(tok, MethodName(callee, isCoCall ? MethodTranslationKind.CoCall : MethodTranslationKind.CallPre), ins, isCoCall ? outs : new List()); proofDependencies?.AddProofDependencyId(call, tok, new CallDependency(cs)); if ( (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) || @@ -1964,7 +1970,16 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E // of the predicate. call.IsFree = true; } - builder.Add(call); + callBuilder.Add(call); + if (cs.Proof != null) { + PathAsideBlock(cs.Tok, callBuilder, builder); + } + if (!isCoCall) { + builder.Add(new CommentCmd("ProcessCallStmt: Make the call")); + CallCmd post = Call(tok, MethodName(callee, MethodTranslationKind.CallPost), ins, outs); + proofDependencies?.AddProofDependencyId(post, tok, new CallDependency(cs)); + builder.Add(post); + } // Unbox results as needed for (int i = 0; i < Lhss.Count; i++) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 387ded18d39..be66b74b30d 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -2854,12 +2854,13 @@ Bpl.Function GetOrCreateFunction(Function f) { /// Note that SpecWellformedness and Implementation have procedure implementations /// but no callers, and vice versa for InterModuleCall, IntraModuleCall, and CoCall. /// - enum MethodTranslationKind { SpecWellformedness, Call, CoCall, Implementation, OverrideCheck } + enum MethodTranslationKind { SpecWellformedness, CallPre, CallPost, CoCall, Implementation, OverrideCheck } private static readonly Dictionary kindSanitizedPrefix = new() { { MethodTranslationKind.SpecWellformedness, "CheckWellFormed" }, - { MethodTranslationKind.Call, "Call" }, + { MethodTranslationKind.CallPre, "CallPre" }, + { MethodTranslationKind.CallPost, "CallPost" }, { MethodTranslationKind.CoCall, "CoCall" }, { MethodTranslationKind.Implementation, "Impl" }, { MethodTranslationKind.OverrideCheck, "OverrideCheck" }, @@ -2873,7 +2874,8 @@ static string MethodName(ICodeContext m, MethodTranslationKind kind) { private static readonly Dictionary kindDescription = new Dictionary() { {MethodTranslationKind.SpecWellformedness, "well-formedness"}, - {MethodTranslationKind.Call, "call"}, + {MethodTranslationKind.CallPre, "call precondtion"}, + {MethodTranslationKind.CallPost, "call postcondition"}, {MethodTranslationKind.CoCall, "co-call"}, {MethodTranslationKind.Implementation, "correctness"}, {MethodTranslationKind.OverrideCheck, "override check"}, @@ -4583,7 +4585,7 @@ List TrSplitExprForMethodSpec(Expression expr, ExpressionTranslat var splits = new List(); var applyInduction = kind == MethodTranslationKind.Implementation; TrSplitExpr(expr, splits, true, int.MaxValue, - kind != MethodTranslationKind.Call, applyInduction, etran); + kind != MethodTranslationKind.CallPre && kind != MethodTranslationKind.CallPost, applyInduction, etran); return splits; } From 8c70eedbc48894e2858fcdaaa07f6b3677069b7f Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 8 Aug 2024 20:31:14 +0200 Subject: [PATCH 05/19] Empty-Commit From 7e901001cc35cdead6f7830838661d7f3571f3d5 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 8 Aug 2024 20:45:16 +0200 Subject: [PATCH 06/19] fix merge --- Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index a96d43f85ad..6b2388c240b 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -1979,7 +1979,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E var callBuilder = builder; if (cs.Proof != null) { - callBuilder = new BoogieStmtListBuilder(this, options); + callBuilder = new BoogieStmtListBuilder(this, options, builder.Context); AddComment(callBuilder, cs, "call statement proof"); CurrentIdGenerator.Push(); TrStmt(cs.Proof, callBuilder, locals, etran); From cf45a175412053a144bf44b193298abd416a9507 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 8 Aug 2024 22:11:34 +0200 Subject: [PATCH 07/19] add tests --- .../AST/Statements/Assignment/UpdateStmt.cs | 2 +- .../PreType/PreTypeResolve.Statements.cs | 28 +++---- .../LitTests/LitTest/dafny0/CallBy.dfy | 75 +++++++++++++++++++ .../LitTests/LitTest/dafny0/CallBy.dfy.expect | 7 ++ 4 files changed, 97 insertions(+), 15 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect diff --git a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs index 7600c8cf2c3..42b02a1ff88 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs @@ -23,7 +23,7 @@ public override IToken Tok { } [FilledInDuringResolution] public List ResolvedStatements; - public override IEnumerable SubStatements => Children.OfType(); + public override IEnumerable SubStatements => Children.OfType().Concat(Proof != null ? Proof.SubStatements : new List()); public override IEnumerable NonSpecificationSubExpressions => ResolvedStatements == null ? Rhss.SelectMany(r => r.NonSpecificationSubExpressions) : Enumerable.Empty(); diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index 8d4be81153f..bc20876e0f6 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -653,13 +653,13 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo // resolve proof if (update.Proof != null) { // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body - var prevLblStmts = resolver.EnclosingStatementLabels; - var prevLoopStack = resolver.LoopStack; - resolver.EnclosingStatementLabels = new Scope(resolver.Options); - resolver.LoopStack = new List(); - resolver.ResolveStatement(update.Proof, resolutionContext); - resolver.EnclosingStatementLabels = prevLblStmts; - resolver.LoopStack = prevLoopStack; + var prevLblStmts = EnclosingStatementLabels; + var prevLoopStack = LoopStack; + EnclosingStatementLabels = new Scope(resolver.Options); + LoopStack = new List(); + ResolveStatement(update.Proof, resolutionContext); + EnclosingStatementLabels = prevLblStmts; + LoopStack = prevLoopStack; } // figure out what kind of UpdateStmt this is @@ -943,13 +943,13 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r if (s.Proof != null) { // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body - var prevLblStmts = resolver.EnclosingStatementLabels; - var prevLoopStack = resolver.LoopStack; - resolver.EnclosingStatementLabels = new Scope(resolver.Options); - resolver.LoopStack = new List(); - resolver.ResolveStatement(s.Proof, resolutionContext); - resolver.EnclosingStatementLabels = prevLblStmts; - resolver.LoopStack = prevLoopStack; + var prevLblStmts = EnclosingStatementLabels; + var prevLoopStack = LoopStack; + EnclosingStatementLabels = new Scope(Options); + LoopStack = new List(); + ResolveStatement(s.Proof, resolutionContext); + EnclosingStatementLabels = prevLblStmts; + LoopStack = prevLoopStack; } Expression lhsExtract = null; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy new file mode 100644 index 00000000000..86f4c8c742a --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy @@ -0,0 +1,75 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --standard-libraries + +datatype Option<+T> = None | Some(value: T) { + function UnwrapOr(default: T): T { + match this + case Some(v) => v + case None() => default + } + + predicate IsFailure() { + None? + } + + function PropagateFailure(): Option + requires None? + { + None + } + + function Extract(): T + requires Some? + { + value + } +} + +opaque predicate P() { true } + +lemma ProveP() ensures P() { + reveal P(); +} + +method M() + requires P() +{} + +method M'() returns (r: int) + requires P() + ensures r == 3 +{ r := 3; } + +method M''() returns (r: Option) + requires P() +{ r := None; } + +method A() { + M() by { ProveP(); } + assert P(); // Should fail +} + +method B() { + var v: int; + v := M'() by { reveal P(); } + assert P(); // Should fail +} + +method C() { + assert p: P() by { ProveP(); } + var v' := M'() by { reveal p; } + assert v' == 3; // should pass + assert P(); // should fail +} + +method D() returns (r: Option){ + var v: int; + v :- M''() by { ProveP(); } + assert P(); // should fail + r := None; +} + +method E() returns (r: Option){ + var v' :- M''() by { reveal P(); } + assert P(); // should fail + r := None; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect new file mode 100644 index 00000000000..64983e95f0c --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect @@ -0,0 +1,7 @@ +CallBy.dfy(48,10): Error: assertion might not hold +CallBy.dfy(54,10): Error: assertion might not hold +CallBy.dfy(61,10): Error: assertion might not hold +CallBy.dfy(67,10): Error: assertion might not hold +CallBy.dfy(73,10): Error: assertion might not hold + +Dafny program verifier finished with 4 verified, 5 errors From 2a8e1dfbfcfc582aecf7e9433d74093da11c468c Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 8 Aug 2024 22:39:49 +0200 Subject: [PATCH 08/19] docs --- docs/DafnyRef/Statements.16.expect | 3 +++ docs/DafnyRef/Statements.md | 32 ++++++++++++++++++++++++++++++ docs/dev/news/5662.feat | 1 + 3 files changed, 36 insertions(+) create mode 100644 docs/DafnyRef/Statements.16.expect create mode 100644 docs/dev/news/5662.feat diff --git a/docs/DafnyRef/Statements.16.expect b/docs/DafnyRef/Statements.16.expect new file mode 100644 index 00000000000..6bbd3b36f5b --- /dev/null +++ b/docs/DafnyRef/Statements.16.expect @@ -0,0 +1,3 @@ +text.dfy(17,10): Error: assertion might not hold + +Dafny program verifier finished with 2 verified, 1 error diff --git a/docs/DafnyRef/Statements.md b/docs/DafnyRef/Statements.md index ef2fc664708..f85787e2e22 100644 --- a/docs/DafnyRef/Statements.md +++ b/docs/DafnyRef/Statements.md @@ -257,6 +257,38 @@ Note that the syntax is interpreted as a label in which the user forgot the `label` keyword. +### 8.5.6. Method call with a `by` proof + +The purpose of this form of a method call is to seperate the called method's +precondition and its proof from the rest of the correctness proof of the +calling method. + + +```dafny +opaque predicate P() { true } + +lemma ProveP() ensures P() { + reveal P(); +} + +method M(i: int) returns (r: int) + requires P() + ensures r == i +{ r := i; } + +method C() { + var v := M(1/3) by { // We prove 3 != 0 outside of the by proof + ProveP(); // Prove precondtion + } + assert v == 0; // Use postcondition + assert P(); // Fails +} +``` + +By placing the call to lemma `ProveP` inside of the by block, we can not use +`P` after the method call. The well-formedness checks of the arguments to the +method call are not subject to the separation. + ## 8.6. Update with Failure Statement (`:-`) ([grammar](#g-update-with-failure-statement)) {#sec-update-with-failure-statement} See the subsections below for examples. diff --git a/docs/dev/news/5662.feat b/docs/dev/news/5662.feat new file mode 100644 index 00000000000..15c238b1d5e --- /dev/null +++ b/docs/dev/news/5662.feat @@ -0,0 +1 @@ +Method calls get an optional by-proof that hides the precondtion and its proof From 7fc015aa00ff202f6f079fb04cb5204d37cfb258 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 8 Aug 2024 23:02:48 +0200 Subject: [PATCH 09/19] obvious test fixes --- .../dafny0/TriggerInPredicate.dfy.expect | 1 + .../Snapshots0.run.legacy.dfy.expect | 12 +++++----- .../Snapshots1.run.legacy.dfy.expect | 6 ++--- .../Snapshots2.run.legacy.dfy.expect | 22 +++++++++---------- .../Snapshots5.run.legacy.dfy.expect | 14 ++++++------ .../Snapshots8.run.legacy.dfy.expect | 22 +++++++++---------- .../Snapshots9.run.legacy.dfy.expect | 8 +++---- .../triggers-prevent-some-inlining.dfy.expect | 2 ++ 8 files changed, 45 insertions(+), 42 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect index e47d3f949d8..0e1599f1f50 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect @@ -1,4 +1,5 @@ TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined. TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined. +TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect index e1e675464dc..711eb590f99 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect @@ -1,13 +1,13 @@ -Processing command (at Snapshots0.v0.dfy(4,10)) assert {:id "id1"} Lit(false); +Processing command (at Snapshots0.v0.dfy(4,10)) assert {:id "id2"} Lit(false); >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 0 errors -Processing call to procedure bar (call) in implementation foo (correctness) (at Snapshots0.v1.dfy(3,6)): +Processing call to procedure bar (call precondtion) in implementation foo (correctness) (at Snapshots0.v1.dfy(3,6)): + >>> added after: a##cached##0 := a##cached##0 && true; +Processing call to procedure bar (call postcondition) in implementation foo (correctness) (at Snapshots0.v1.dfy(3,6)): >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##1(call0old#AT#$Heap, $Heap) } ##extracted_function##1(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall $o: ref :: { $Heap[$o] } $o != null && $Unbox(read(call0old#AT#$Heap, $o, alloc)): bool ==> $Heap[$o] == call0old#AT#$Heap[$o]) && $HeapSucc(call0old#AT#$Heap, $Heap))) - >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap); -Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap); - >>> AssumeNegationOfAssumptionVariable -Processing command (at Snapshots0.v1.dfy(4,10)) assert {:id "id5"} Lit(false); + >>> added after: a##cached##1 := a##cached##1 && ##extracted_function##1(call0old#AT#$Heap, $Heap); +Processing command (at Snapshots0.v1.dfy(4,10)) assert {:id "id8"} Lit(false); >>> MarkAsPartiallyVerified Snapshots0.v1.dfy(4,9): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect index a2ef2d3d341..79adfe82043 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect @@ -1,10 +1,10 @@ -Processing command (at Snapshots1.v0.dfy(4,10)) assert {:id "id1"} Lit(false); +Processing command (at Snapshots1.v0.dfy(4,10)) assert {:id "id2"} Lit(false); >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 0 errors -Processing call to procedure N (call) in implementation M (correctness) (at Snapshots1.v1.dfy(3,4)): +Processing call to procedure N (call postcondition) in implementation M (correctness) (at Snapshots1.v1.dfy(3,4)): >>> added after: a##cached##0 := a##cached##0 && false; -Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id6"} Lit(false); +Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id9"} Lit(false); >>> DoNothingToAssert Snapshots1.v1.dfy(4,9): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect index 768491421f5..b4b0df2dd7c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect @@ -1,31 +1,31 @@ -Processing command (at Snapshots2.v0.dfy(4,10)) assert {:id "id1"} Lit(false); +Processing command (at Snapshots2.v0.dfy(4,10)) assert {:id "id2"} Lit(false); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id5"} Lit(true); +Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id7"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(11,15)) assert {:id "id4"} _module.__default.P() <==> _module.__default.Q(); +Processing command (at Snapshots2.v0.dfy(11,15)) assert {:id "id6"} _module.__default.P() <==> _module.__default.Q(); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id8"} Lit(true); +Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id10"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id7"} _module.__default.Q() <==> Lit(_module.__default.R()); +Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id9"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert Dafny program verifier finished with 3 verified, 0 errors -Processing call to procedure N (call) in implementation M (correctness) (at Snapshots2.v1.dfy(3,4)): +Processing call to procedure N (call postcondition) in implementation M (correctness) (at Snapshots2.v1.dfy(3,4)): >>> added after: a##cached##0 := a##cached##0 && false; Processing implementation P (well-formedness) (at Snapshots2.v1.dfy(10,11)): >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; Processing implementation Q (well-formedness) (at Snapshots2.v1.dfy(13,11)): >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; -Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id12"} Lit(false); +Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id15"} Lit(false); >>> DoNothingToAssert Snapshots2.v1.dfy(4,9): Error: assertion might not hold -Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id16"} Lit(true); +Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id20"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id15"} _module.__default.P() <==> _module.__default.Q(); +Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id19"} _module.__default.P() <==> _module.__default.Q(); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id19"} Lit(true); +Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id23"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id18"} _module.__default.Q() <==> Lit(_module.__default.R()); +Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id22"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert Dafny program verifier finished with 2 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect index 5566f116ad4..1df0bbd2479 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect @@ -2,11 +2,11 @@ Snapshots5.v0.dfy(10,12): Warning: Could not find a trigger for this quantifier. Snapshots5.v0.dfy(13,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Snapshots5.v0.dfy(20,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Snapshots5.v0.dfy(26,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. -Processing command (at Snapshots5.v0.dfy(10,40)) assert {:id "id1"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0; +Processing command (at Snapshots5.v0.dfy(10,40)) assert {:id "id2"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0; >>> DoNothingToAssert -Processing command (at Snapshots5.v0.dfy(13,38)) assert {:id "id3"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3; +Processing command (at Snapshots5.v0.dfy(13,38)) assert {:id "id5"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3; >>> DoNothingToAssert -Processing command (at Snapshots5.v0.dfy(20,40)) assert {:id "id4"} (forall b#3_1: bool :: b#3_1 || !b#3_1) || 1 != 1; +Processing command (at Snapshots5.v0.dfy(20,40)) assert {:id "id6"} (forall b#3_1: bool :: b#3_1 || !b#3_1) || 1 != 1; >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 0 errors @@ -15,13 +15,13 @@ Snapshots5.v1.dfy(13,10): Warning: Could not find a trigger for this quantifier. Snapshots5.v1.dfy(20,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Snapshots5.v1.dfy(22,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Snapshots5.v1.dfy(27,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. -Processing command (at Snapshots5.v1.dfy(10,40)) assert {:id "id10"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0; +Processing command (at Snapshots5.v1.dfy(10,40)) assert {:id "id14"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0; >>> MarkAsFullyVerified -Processing command (at Snapshots5.v1.dfy(13,38)) assert {:id "id12"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3; +Processing command (at Snapshots5.v1.dfy(13,38)) assert {:id "id17"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3; >>> MarkAsFullyVerified -Processing command (at Snapshots5.v1.dfy(20,37)) assert {:id "id13"} (exists b#3_1: bool :: Lit(true)) || 4 != 4; +Processing command (at Snapshots5.v1.dfy(20,37)) assert {:id "id18"} (exists b#3_1: bool :: Lit(true)) || 4 != 4; >>> DoNothingToAssert -Processing command (at Snapshots5.v1.dfy(22,35)) assert {:id "id14"} (exists b#3: bool :: Lit(true)) || 5 != 5; +Processing command (at Snapshots5.v1.dfy(22,35)) assert {:id "id19"} (exists b#3: bool :: Lit(true)) || 5 != 5; >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect index 0b3564e7be2..9a5c564e0d7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect @@ -3,40 +3,40 @@ Processing command (at Snapshots8.v0.dfy(2,37)) assert {:id "id0"} x#0 < 20 || L >>> DoNothingToAssert Processing command (at Snapshots8.v0.dfy(3,12)) assert {:id "id1"} x#0 < 10; >>> DoNothingToAssert -Processing command (at Snapshots8.v0.dfy(4,8)) assert {:id "id4$id2$requires"} {:id "id2"} LitInt(0) <= call0formal#AT#y#0; +Processing command (at Snapshots8.v0.dfy(4,8)) assert {:id "id5$id2$requires"} {:id "id2"} LitInt(0) <= call0formal#AT#y#0; >>> DoNothingToAssert Snapshots8.v0.dfy(3,11): Error: assertion might not hold Snapshots8.v0.dfy(4,7): Error: a precondition for this call could not be proved Snapshots8.v0.dfy(8,13): Related location: this is the precondition that could not be proved -Processing command (at Snapshots8.v0.dfy(13,13)) assert {:id "id8"} LitInt(2) <= z#0; +Processing command (at Snapshots8.v0.dfy(13,13)) assert {:id "id11"} LitInt(2) <= z#0; >>> DoNothingToAssert Snapshots8.v0.dfy(17,9): Error: a postcondition could not be proved on this return path Snapshots8.v0.dfy(13,12): Related location: this is the postcondition that could not be proved -Processing command (at Snapshots8.v0.dfy(23,12)) assert {:id "id10"} u#0 != 53; +Processing command (at Snapshots8.v0.dfy(23,12)) assert {:id "id13"} u#0 != 53; >>> DoNothingToAssert Snapshots8.v0.dfy(23,11): Error: assertion might not hold -Processing command (at Snapshots8.v0.dfy(28,10)) assert {:id "id11"} Lit(true); +Processing command (at Snapshots8.v0.dfy(28,10)) assert {:id "id14"} Lit(true); >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 4 errors -Processing command (at Snapshots8.v1.dfy(30,17)) assert {:id "id24"} u#0 != 53; +Processing command (at Snapshots8.v1.dfy(30,17)) assert {:id "id30"} u#0 != 53; >>> RecycleError Snapshots8.v1.dfy(30,16): Error: assertion might not hold -Processing command (at Snapshots8.v1.dfy(3,15)) assert {:id "id12"} x#0 < 20 || LitInt(10) <= x#0; +Processing command (at Snapshots8.v1.dfy(3,15)) assert {:id "id15"} x#0 < 20 || LitInt(10) <= x#0; >>> MarkAsFullyVerified -Processing command (at Snapshots8.v1.dfy(5,17)) assert {:id "id13"} x#0 < 10; +Processing command (at Snapshots8.v1.dfy(5,17)) assert {:id "id16"} x#0 < 10; >>> RecycleError -Processing command (at Snapshots8.v1.dfy(6,8)) assert {:id "id17$id14$requires"} {:id "id14"} LitInt(0) <= call0formal#AT#y#0; +Processing command (at Snapshots8.v1.dfy(6,8)) assert {:id "id21$id17$requires"} {:id "id17"} LitInt(0) <= call0formal#AT#y#0; >>> RecycleError -Processing command (at Snapshots8.v1.dfy(7,12)) assert {:id "id15"} x#0 == LitInt(7); +Processing command (at Snapshots8.v1.dfy(7,12)) assert {:id "id19"} x#0 == LitInt(7); >>> DoNothingToAssert Snapshots8.v1.dfy(5,16): Error: assertion might not hold Snapshots8.v1.dfy(6,7): Error: a precondition for this call could not be proved Snapshots8.v1.dfy(12,20): Related location: this is the precondition that could not be proved Snapshots8.v1.dfy(7,11): Error: assertion might not hold -Processing command (at Snapshots8.v1.dfy(23,12)) assert {:id "id23"} Lit(true); +Processing command (at Snapshots8.v1.dfy(23,12)) assert {:id "id29"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots8.v1.dfy(19,13)) assert {:id "id21"} LitInt(2) <= z#0; +Processing command (at Snapshots8.v1.dfy(19,13)) assert {:id "id27"} LitInt(2) <= z#0; >>> DoNothingToAssert Snapshots8.v1.dfy(24,9): Error: a postcondition could not be proved on this return path Snapshots8.v1.dfy(19,12): Related location: this is the postcondition that could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect index 36e8d43cba9..dc5172019fd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect @@ -1,19 +1,19 @@ Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format -Processing command (at Snapshots9.v0.dfy(2,11)) assert {:id "id2"} ok#0; +Processing command (at Snapshots9.v0.dfy(2,11)) assert {:id "id3"} ok#0; >>> DoNothingToAssert Snapshots9.v0.dfy(4,7): Error: a postcondition could not be proved on this return path Snapshots9.v0.dfy(2,10): Related location: this is the postcondition that could not be proved -Processing command (at Snapshots9.v0.dfy(12,11)) assert {:id "id7"} ok#0; +Processing command (at Snapshots9.v0.dfy(12,11)) assert {:id "id9"} ok#0; >>> DoNothingToAssert Snapshots9.v0.dfy(13,0): Error: a postcondition could not be proved on this return path Snapshots9.v0.dfy(12,10): Related location: this is the postcondition that could not be proved Dafny program verifier finished with 0 verified, 2 errors -Processing command (at Snapshots9.v1.dfy(6,11)) assert {:id "id10"} ok#0; +Processing command (at Snapshots9.v1.dfy(6,11)) assert {:id "id13"} ok#0; >>> RecycleError Snapshots9.v1.dfy(8,7): Error: a postcondition could not be proved on this return path Snapshots9.v1.dfy(6,10): Related location: this is the postcondition that could not be proved -Processing command (at Snapshots9.v1.dfy(19,11)) assert {:id "id15"} ok#0; +Processing command (at Snapshots9.v1.dfy(19,11)) assert {:id "id19"} ok#0; >>> RecycleError Snapshots9.v1.dfy(21,0): Error: a postcondition could not be proved on this return path Snapshots9.v1.dfy(19,10): Related location: this is the postcondition that could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect index 89c40cc572a..2d3fea2d577 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect @@ -3,5 +3,7 @@ triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call are triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call are not inlined. triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call are not inlined. triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call are not inlined. +triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call are not inlined. +triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call are not inlined. Dafny program verifier finished with 1 verified, 0 errors From fef9ecab010bead85c2536584ac61c272300b92f Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 8 Aug 2024 23:11:11 +0200 Subject: [PATCH 10/19] remove unnecessary assert --- .../TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy index 9c23169829f..179b97547b7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy @@ -468,7 +468,7 @@ assert heapExternalsZeroOrOneEdges(xedges); assert ObjectsAreValid({o}); - assert edges(objects) == old( edges(objects) ) + {Edge(o,f,t)}; + // assert edges(objects) == old( edges(objects) ) + {Edge(o,f,t)}; var zedges := edges(objects); //or could hand in if necessary? var zisos := justTheIsos(objects); From 50ceba077ec619b4afa6825ecee3d7e4d80afbf2 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Thu, 8 Aug 2024 23:38:33 +0200 Subject: [PATCH 11/19] fix TestGeneration --- .../Inlining/AddImplementationForCallsRewriter.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs b/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs index d6844fa3c7b..2056a841d90 100644 --- a/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs +++ b/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs @@ -15,13 +15,13 @@ namespace DafnyTestGeneration.Inlining; /// -/// Create implementations for all "Call$$" procedures by making them +/// Create implementations for all "CallPre$$" procedures by making them /// call the respective "Impl$$ implementations. This allows to implement /// inlining of Dafny methods further down the road. /// public class AddImplementationsForCallsRewriter : ReadOnlyVisitor { - private const string CallPrefix = "Call$$"; + private const string CallPrefix = "CallPre$$"; private readonly DafnyOptions options; private List implsToAdd = new(); From 67c612a8ce59db3e20771c5a68dedd72a8f50218 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 9 Aug 2024 01:16:19 +0200 Subject: [PATCH 12/19] use actual call for test generation --- .../Inlining/AddImplementationForCallsRewriter.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs b/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs index 2056a841d90..9513ddb806f 100644 --- a/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs +++ b/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs @@ -15,13 +15,13 @@ namespace DafnyTestGeneration.Inlining; /// -/// Create implementations for all "CallPre$$" procedures by making them +/// Create implementations for all "CallPost$$" procedures by making them /// call the respective "Impl$$ implementations. This allows to implement /// inlining of Dafny methods further down the road. /// public class AddImplementationsForCallsRewriter : ReadOnlyVisitor { - private const string CallPrefix = "CallPre$$"; + private const string CallPrefix = "CallPost$$"; private readonly DafnyOptions options; private List implsToAdd = new(); From 5b9833f5fb5cd75396b198874c110710e11ce240 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 9 Aug 2024 14:13:33 +0200 Subject: [PATCH 13/19] review --- .../Assignment/AssignOrReturnStmt.cs | 13 +---- .../AST/Statements/Assignment/UpdateStmt.cs | 11 +---- .../Resolver/GhostInterestVisitor.cs | 3 ++ Source/DafnyCore/Resolver/ModuleResolver.cs | 13 +++++ .../PreType/PreTypeResolve.Statements.cs | 36 +++++++------- .../LitTests/LitTest/dafny0/CallBy.dfy | 47 ++++++------------- .../LitTests/LitTest/dafny0/CallBy.dfy.expect | 12 ++--- 7 files changed, 56 insertions(+), 79 deletions(-) diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs index 3b92730a0c2..4b66d9d2a1f 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs @@ -23,7 +23,7 @@ public override IToken Tok { } } - public override IEnumerable Children => ResolvedStatements; + public override IEnumerable Children => ResolvedStatements.Concat(Proof != null ? Proof.Children : new List()); public override IEnumerable PreResolveSubStatements => Enumerable.Empty(); [ContractInvariantMethod] @@ -193,16 +193,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti return; } - if (Proof != null) { - // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body - var prevLblStmts = resolver.EnclosingStatementLabels; - var prevLoopStack = resolver.LoopStack; - resolver.EnclosingStatementLabels = new Scope(resolver.Options); - resolver.LoopStack = new List(); - resolver.ResolveStatement(Proof, resolutionContext); - resolver.EnclosingStatementLabels = prevLblStmts; - resolver.LoopStack = prevLoopStack; - } + resolver.ResolveByProof(Proof, resolutionContext); Expression lhsExtract = null; if (expectExtract) { diff --git a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs index 42b02a1ff88..564637054de 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs @@ -128,16 +128,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti } // resolve proof - if (Proof != null) { - // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body - var prevLblStmts = resolver.EnclosingStatementLabels; - var prevLoopStack = resolver.LoopStack; - resolver.EnclosingStatementLabels = new Scope(resolver.Options); - resolver.LoopStack = new List(); - resolver.ResolveStatement(Proof, resolutionContext); - resolver.EnclosingStatementLabels = prevLblStmts; - resolver.LoopStack = prevLoopStack; - } + resolver.ResolveByProof(Proof, resolutionContext); // figure out what kind of UpdateStmt this is if (firstEffectfulRhs == null) { diff --git a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs index df6868accd8..3981c741d8a 100644 --- a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs +++ b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs @@ -145,6 +145,9 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC var s = (UpdateStmt)stmt; s.ResolvedStatements.ForEach(ss => Visit(ss, mustBeErasable, proofContext)); s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost); + if (s.Proof != null) { + Visit(s.Proof, true, "an call-by body"); + } } else if (stmt is AssignOrReturnStmt) { var s = (AssignOrReturnStmt)stmt; diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 22d0c818442..86ebc075ae0 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -3311,6 +3311,19 @@ internal LetExpr LetVarIn(IToken tok, string name, Type tp, Expression rhs, Expr return LetPatIn(tok, lhs, rhs, body); } + internal void ResolveByProof(BlockStmt proof, ResolutionContext resolutionContext) { + if (proof != null) { + // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body + var prevLblStmts = EnclosingStatementLabels; + var prevLoopStack = LoopStack; + EnclosingStatementLabels = new Scope(Options); + LoopStack = new List(); + ResolveStatement(proof, resolutionContext); + EnclosingStatementLabels = prevLblStmts; + LoopStack = prevLoopStack; + } + } + /// /// If expr.Lhs != null: Desugars "var x: T :- E; F" into "var temp := E; if temp.IsFailure() then temp.PropagateFailure() else var x: T := temp.Extract(); F" /// If expr.Lhs == null: Desugars " :- E; F" into "var temp := E; if temp.IsFailure() then temp.PropagateFailure() else F" diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index bc20876e0f6..3a28d1febff 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -651,16 +651,7 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo } // resolve proof - if (update.Proof != null) { - // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body - var prevLblStmts = EnclosingStatementLabels; - var prevLoopStack = LoopStack; - EnclosingStatementLabels = new Scope(resolver.Options); - LoopStack = new List(); - ResolveStatement(update.Proof, resolutionContext); - EnclosingStatementLabels = prevLblStmts; - LoopStack = prevLoopStack; - } + ResolveByProof(update.Proof, resolutionContext); // figure out what kind of UpdateStmt this is if (firstEffectfulRhs == null) { @@ -726,6 +717,20 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo } } + private void ResolveByProof(BlockStmt proof, ResolutionContext resolutionContext) + { + if (proof != null) { + // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body + var prevLblStmts = EnclosingStatementLabels; + var prevLoopStack = LoopStack; + EnclosingStatementLabels = new Scope(resolver.Options); + LoopStack = new List(); + ResolveStatement(proof, resolutionContext); + EnclosingStatementLabels = prevLblStmts; + LoopStack = prevLoopStack; + } + } + private void ResolveLoopSpecificationComponents(List invariants, Specification decreases, Specification modifies, ResolutionContext resolutionContext) { @@ -941,16 +946,7 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r return; } - if (s.Proof != null) { - // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body - var prevLblStmts = EnclosingStatementLabels; - var prevLoopStack = LoopStack; - EnclosingStatementLabels = new Scope(Options); - LoopStack = new List(); - ResolveStatement(s.Proof, resolutionContext); - EnclosingStatementLabels = prevLblStmts; - LoopStack = prevLoopStack; - } + ResolveByProof(s.Proof, resolutionContext); Expression lhsExtract = null; if (expectExtract) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy index 86f4c8c742a..e32c596064a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy @@ -1,28 +1,6 @@ // RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --standard-libraries -datatype Option<+T> = None | Some(value: T) { - function UnwrapOr(default: T): T { - match this - case Some(v) => v - case None() => default - } - - predicate IsFailure() { - None? - } - - function PropagateFailure(): Option - requires None? - { - None - } - - function Extract(): T - requires Some? - { - value - } -} +import opened Std.Wrappers opaque predicate P() { true } @@ -30,46 +8,51 @@ lemma ProveP() ensures P() { reveal P(); } -method M() +method NeedsP() requires P() {} -method M'() returns (r: int) +method NeedsPAndReturns3() returns (r: int) requires P() ensures r == 3 { r := 3; } -method M''() returns (r: Option) +method NeedsPAndReturnsNone() returns (r: Option) requires P() { r := None; } method A() { - M() by { ProveP(); } + NeedsP() by { ProveP(); } assert P(); // Should fail } method B() { var v: int; - v := M'() by { reveal P(); } + v := NeedsPAndReturns3() by { reveal P(); } assert P(); // Should fail } method C() { assert p: P() by { ProveP(); } - var v' := M'() by { reveal p; } - assert v' == 3; // should pass + var v := NeedsPAndReturns3() by { reveal p; } + assert v == 3; // should pass assert P(); // should fail } method D() returns (r: Option){ var v: int; - v :- M''() by { ProveP(); } + v :- NeedsPAndReturnsNone() by { + match false { + case true => assert true; + case false => ProveP(); + } + } assert P(); // should fail r := None; } method E() returns (r: Option){ - var v' :- M''() by { reveal P(); } + var v :- NeedsPAndReturnsNone() by { reveal P(); } assert P(); // should fail r := None; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect index 64983e95f0c..13436c6a151 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect @@ -1,7 +1,7 @@ -CallBy.dfy(48,10): Error: assertion might not hold -CallBy.dfy(54,10): Error: assertion might not hold -CallBy.dfy(61,10): Error: assertion might not hold -CallBy.dfy(67,10): Error: assertion might not hold -CallBy.dfy(73,10): Error: assertion might not hold +CallBy.dfy(26,10): Error: assertion might not hold +CallBy.dfy(32,10): Error: assertion might not hold +CallBy.dfy(39,10): Error: assertion might not hold +CallBy.dfy(50,10): Error: assertion might not hold +CallBy.dfy(56,10): Error: assertion might not hold -Dafny program verifier finished with 4 verified, 5 errors +Dafny program verifier finished with 3 verified, 5 errors From 1b463a6067e750f81e0661ddd1015f62012b19bb Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 9 Aug 2024 14:15:17 +0200 Subject: [PATCH 14/19] resolution tests --- .../LitTests/LitTest/dafny0/CallByResolution0.dfy | 11 +++++++++++ .../LitTest/dafny0/CallByResolution0.dfy.expect | 3 +++ .../LitTests/LitTest/dafny0/CallByResolution1.dfy | 13 +++++++++++++ .../LitTest/dafny0/CallByResolution1.dfy.expect | 2 ++ 4 files changed, 29 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy new file mode 100644 index 00000000000..b41b04b16ea --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy @@ -0,0 +1,11 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" + +method M() {} + +method A() { + var i: int := 0; + M() by { + i := 1; + return; + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy.expect new file mode 100644 index 00000000000..d6ed0c40058 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy.expect @@ -0,0 +1,3 @@ +CallByResolution0.dfy(8,6): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +CallByResolution0.dfy(9,4): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) +2 resolution/type errors detected in CallByResolution0.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy new file mode 100644 index 00000000000..334dacf2fa7 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy @@ -0,0 +1,13 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" + +method M() {} + +method B() { + var i := 0; + while i < 3 { + M() by { + break; + } + i := i + 1; + } +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy.expect new file mode 100644 index 00000000000..66d1c739208 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy.expect @@ -0,0 +1,2 @@ +CallByResolution1.dfy(9,6): Error: a non-labeled 'break' statement is allowed only in loops +1 resolution/type errors detected in CallByResolution1.dfy From 50d4d10a6809863ae36494b32923bbed6e2bab65 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 9 Aug 2024 19:23:57 +0200 Subject: [PATCH 15/19] review --- .../Assignment/AssignOrReturnStmt.cs | 4 +- .../AST/Statements/Assignment/UpdateStmt.cs | 2 +- .../Resolver/GhostInterestVisitor.cs | 2 +- Source/DafnyCore/Resolver/ModuleResolver.cs | 22 ++-- .../PreType/PreTypeResolve.Statements.cs | 43 +++---- .../Verifier/BoogieGenerator.Methods.cs | 112 +++++++++++------- .../Verifier/BoogieGenerator.TrStatement.cs | 62 +++++----- Source/DafnyCore/Verifier/BoogieGenerator.cs | 8 +- .../LitTests/LitTest/dafny0/CallBy.dfy | 9 ++ .../LitTests/LitTest/dafny0/CallBy.dfy.expect | 3 +- .../LitTest/git-issues/git-issue-3855.dfy | 2 - 11 files changed, 154 insertions(+), 115 deletions(-) diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs index 4b66d9d2a1f..a598f530af8 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs @@ -23,7 +23,7 @@ public override IToken Tok { } } - public override IEnumerable Children => ResolvedStatements.Concat(Proof != null ? Proof.Children : new List()); + public override IEnumerable Children => ResolvedStatements.Concat(Proof?.Children ?? new List()); public override IEnumerable PreResolveSubStatements => Enumerable.Empty(); [ContractInvariantMethod] @@ -193,7 +193,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti return; } - resolver.ResolveByProof(Proof, resolutionContext); + ModuleResolver.ResolveByProof(resolver, Proof, resolutionContext); Expression lhsExtract = null; if (expectExtract) { diff --git a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs index 564637054de..0b61df6ab30 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs @@ -128,7 +128,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti } // resolve proof - resolver.ResolveByProof(Proof, resolutionContext); + ModuleResolver.ResolveByProof(resolver, Proof, resolutionContext); // figure out what kind of UpdateStmt this is if (firstEffectfulRhs == null) { diff --git a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs index 3981c741d8a..149e330a040 100644 --- a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs +++ b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs @@ -146,7 +146,7 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC s.ResolvedStatements.ForEach(ss => Visit(ss, mustBeErasable, proofContext)); s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost); if (s.Proof != null) { - Visit(s.Proof, true, "an call-by body"); + Visit(s.Proof, true, "a call-by body"); } } else if (stmt is AssignOrReturnStmt) { diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 86ebc075ae0..18d48daf379 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -3311,17 +3311,19 @@ internal LetExpr LetVarIn(IToken tok, string name, Type tp, Expression rhs, Expr return LetPatIn(tok, lhs, rhs, body); } - internal void ResolveByProof(BlockStmt proof, ResolutionContext resolutionContext) { - if (proof != null) { - // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body - var prevLblStmts = EnclosingStatementLabels; - var prevLoopStack = LoopStack; - EnclosingStatementLabels = new Scope(Options); - LoopStack = new List(); - ResolveStatement(proof, resolutionContext); - EnclosingStatementLabels = prevLblStmts; - LoopStack = prevLoopStack; + internal static void ResolveByProof(INewOrOldResolver resolver, BlockStmt proof, ResolutionContext resolutionContext) { + if (proof == null) { + return; } + + // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body + var prevLblStmts = resolver.EnclosingStatementLabels; + var prevLoopStack = resolver.LoopStack; + resolver.EnclosingStatementLabels = new Scope(resolver.Options); + resolver.LoopStack = new List(); + resolver.ResolveStatement(proof, resolutionContext); + resolver.EnclosingStatementLabels = prevLblStmts; + resolver.LoopStack = prevLoopStack; } /// diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index 3a28d1febff..129978be951 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -621,7 +621,8 @@ void ResolveAssignmentRhs(AssignmentRhs rhs, Statement enclosingStmt, Resolution /// errorCountBeforeCheckingStmt is passed in so that this method can determine if any resolution errors were found during /// LHS or RHS checking, because only if no errors were found is update.ResolvedStmt changed. /// - private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionContext, int errorCountBeforeCheckingStmt) { + private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionContext, + int errorCountBeforeCheckingStmt) { Contract.Requires(update != null); Contract.Requires(resolutionContext != null); IToken firstEffectfulRhs = null; @@ -643,6 +644,7 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo isEffectful = false; } } + if (isEffectful && firstEffectfulRhs == null) { firstEffectfulRhs = rhs.Tok; } @@ -651,15 +653,16 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo } // resolve proof - ResolveByProof(update.Proof, resolutionContext); + ModuleResolver.ResolveByProof(this, update.Proof, resolutionContext); // figure out what kind of UpdateStmt this is if (firstEffectfulRhs == null) { if (update.Lhss.Count == 0) { - Contract.Assert(update.Rhss.Count == 1); // guaranteed by the parser + Contract.Assert(update.Rhss.Count == 1); // guaranteed by the parser ReportError(update, "expected method call, found expression"); } else if (update.Lhss.Count != update.Rhss.Count) { - ReportError(update, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", + ReportError(update, + "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", update.Lhss.Count, update.Rhss.Count); } else if (ErrorCount == errorCountBeforeCheckingStmt) { // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translate properly as multi-assignment) @@ -672,7 +675,8 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo } else if (update.CanMutateKnownState) { if (1 < update.Rhss.Count) { ReportError(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement."); - } else { // it might be ok, if it is a TypeRhs + } else { + // it might be ok, if it is a TypeRhs Contract.Assert(update.Rhss.Count == 1); if (methodCallInfo != null) { ReportError(methodCallInfo.Tok, "cannot have method call in return statement."); @@ -692,12 +696,16 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo } else { // if there was an effectful RHS, that must be the only RHS if (update.Rhss.Count != 1) { - ReportError(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS"); + ReportError(firstEffectfulRhs, + "an update statement is allowed an effectful RHS only if there is just one RHS"); } else if (methodCallInfo == null) { // must be a single TypeRhs if (update.Lhss.Count != 1) { - Contract.Assert(2 <= update.Lhss.Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs) - ReportError(update.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", + Contract.Assert(2 <= + update.Lhss + .Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs) + ReportError(update.Lhss[1].tok, + "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", update.Lhss.Count, update.Rhss.Count); } else if (ErrorCount == errorCountBeforeCheckingStmt) { var a = new AssignStmt(update.RangeToken, update.Lhss[0].Resolved, update.Rhss[0]); @@ -706,7 +714,8 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo } else if (ErrorCount == errorCountBeforeCheckingStmt) { // a call statement var resolvedLhss = update.Lhss.ConvertAll(ll => ll.Resolved); - var a = new CallStmt(update.RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok, update.Proof); + var a = new CallStmt(update.RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, + methodCallInfo.Tok, update.Proof); a.OriginalInitialLhs = update.OriginalInitialLhs; update.ResolvedStatements.Add(a); } @@ -717,20 +726,6 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo } } - private void ResolveByProof(BlockStmt proof, ResolutionContext resolutionContext) - { - if (proof != null) { - // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body - var prevLblStmts = EnclosingStatementLabels; - var prevLoopStack = LoopStack; - EnclosingStatementLabels = new Scope(resolver.Options); - LoopStack = new List(); - ResolveStatement(proof, resolutionContext); - EnclosingStatementLabels = prevLblStmts; - LoopStack = prevLoopStack; - } - } - private void ResolveLoopSpecificationComponents(List invariants, Specification decreases, Specification modifies, ResolutionContext resolutionContext) { @@ -946,7 +941,7 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r return; } - ResolveByProof(s.Proof, resolutionContext); + ModuleResolver.ResolveByProof(this, s.Proof, resolutionContext); Expression lhsExtract = null; if (expectExtract) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index eb06ada4235..b50c0d48353 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -201,7 +201,9 @@ void AddMethod_Top(Method m, bool isByMethod, bool includeAllMethods) { // Let the CoCall and Impl forms to use m.PrefixLemma signature and specification (and // note that m.PrefixLemma.Body == m.Body. m = ((ExtremeLemma)m).PrefixLemma; - sink.AddTopLevelDeclaration(AddMethod(m, MethodTranslationKind.CoCall)); + sink.AddTopLevelDeclaration(AddMethod(m, MethodTranslationKind.CoCallPre)); + sink.AddTopLevelDeclaration(AddMethod(m, MethodTranslationKind.CoCallPost)); + } if (!m.HasVerifyFalseAttribute && m.Body != null && InVerificationScope(m)) { // ...and its implementation @@ -1698,6 +1700,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { var ordinaryEtran = new ExpressionTranslator(this, predef, m.tok, m); ExpressionTranslator etran; var inParams = new List(); + var bodyKind = kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation; if (m is TwoStateLemma) { var prevHeapVar = new Boogie.Formal(m.tok, new Boogie.TypedIdent(m.tok, "previous$Heap", predef.HeapType), true); var currHeapVar = new Boogie.Formal(m.tok, new Boogie.TypedIdent(m.tok, "current$Heap", predef.HeapType), true); @@ -1712,49 +1715,48 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { GenerateMethodParameters(m.tok, m, kind, etran, inParams, out var outParams); - var req = new List(); - var mod = new List(); - var ens = new List(); - // 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, null, etran.HeightContext(m), null, null, null)); - if (m is TwoStateLemma) { - // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) - var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); - var a1 = HeapSucc(prevHeap, currHeap); - var a2 = FunctionCall(m.tok, BuiltinFunction.IsGoodHeap, null, currHeap); - req.Add(Requires(m.tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null)); - } + List GetRequires() { + var req = new List(); + // 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, null, etran.HeightContext(m), null, null, null)); + if (m is TwoStateLemma) { + // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) + var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); + var a1 = HeapSucc(prevHeap, currHeap); + var a2 = FunctionCall(m.tok, BuiltinFunction.IsGoodHeap, null, currHeap); + req.Add(Requires(m.tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null)); + } - foreach (var typeBoundAxiom in TypeBoundAxioms(m.tok, Concat(m.EnclosingClass.TypeArgs, m.TypeArgs))) { - req.Add(Requires(m.tok, true, null, typeBoundAxiom, null, null, null)); + foreach (var typeBoundAxiom in TypeBoundAxioms(m.tok, Concat(m.EnclosingClass.TypeArgs, m.TypeArgs))) { + req.Add(Requires(m.tok, true, null, typeBoundAxiom, null, null, null)); + } } - } - if (m is TwoStateLemma) { - // Checked preconditions that old parameters really existed in previous state - var index = 0; - foreach (var formal in m.Ins) { - if (formal.IsOld) { - var dafnyFormalIdExpr = new IdentifierExpr(formal.tok, formal); - var pIdx = m.Ins.Count == 1 ? "" : " at index " + index; - var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'", - "in the two-state lemma's previous state" + PODesc.IsAllocated.HelperFormal(formal), - dafnyFormalIdExpr - ); - var require = Requires(formal.tok, false, null, MkIsAlloc(etran.TrExpr(dafnyFormalIdExpr), formal.Type, prevHeap), - desc.FailureDescription, desc.SuccessDescription, null); - require.Description = desc; - req.Add(require); + if (m is TwoStateLemma) { + // Checked preconditions that old parameters really existed in previous state + var index = 0; + foreach (var formal in m.Ins) { + if (formal.IsOld) { + var dafnyFormalIdExpr = new IdentifierExpr(formal.tok, formal); + var pIdx = m.Ins.Count == 1 ? "" : " at index " + index; + var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'", + "in the two-state lemma's previous state" + PODesc.IsAllocated.HelperFormal(formal), + dafnyFormalIdExpr + ); + var require = Requires(formal.tok, false, null, MkIsAlloc(etran.TrExpr(dafnyFormalIdExpr), formal.Type, prevHeap), + desc.FailureDescription, desc.SuccessDescription, null); + require.Description = desc; + req.Add(require); + } + index++; } - index++; } - } - mod.Add(ordinaryEtran.HeapCastToIdentifierExpr); - var bodyKind = kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation; + if (kind is MethodTranslationKind.SpecWellformedness or MethodTranslationKind.OverrideCheck) { + return req; + } - if (kind != MethodTranslationKind.SpecWellformedness && kind != MethodTranslationKind.OverrideCheck) { // USER-DEFINED SPECIFICATIONS var comment = "user-defined preconditions"; foreach (var p in m.Req) { @@ -1763,20 +1765,32 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { // don't include this precondition here, but record it for later use p.Label.E = (m is TwoStateLemma ? ordinaryEtran : etran.Old).TrExpr(p.E); } else { - foreach (var s in TrSplitExprForMethodSpec(new BodyTranslationContext(m.ContainsHide), p.E, etran, kind)) { + foreach (var s in TrSplitExprForMethodSpec(new BodyTranslationContext(m.ContainsHide), p.E, etran, + kind)) { if (s.IsOnlyChecked && bodyKind) { // don't include in split } else if (s.IsOnlyFree && !bodyKind) { // don't include in split -- it would be ignored, anyhow } else { - req.Add(RequiresWithDependencies(s.Tok, s.IsOnlyFree, p.E, s.E, errorMessage, successMessage, comment)); + req.Add( + RequiresWithDependencies(s.Tok, s.IsOnlyFree, p.E, s.E, errorMessage, successMessage, comment)); comment = null; // the free here is not linked to the free on the original expression (this is free things generated in the splitting.) } } } } - comment = "user-defined postconditions"; + return req; + } + + List GetEnsures() { + var ens = new List(); + if (kind is MethodTranslationKind.SpecWellformedness or MethodTranslationKind.OverrideCheck) { + return ens; + } + + // USER-DEFINED SPECIFICATIONS + var comment = "user-defined postconditions"; foreach (var p in m.Ens) { var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes); AddEnsures(ens, Ensures(p.E.tok, true, p.E, etran.CanCallAssumption(p.E), errorMessage, successMessage, comment)); @@ -1818,19 +1832,29 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { } } } + return ens; } + var req = new List(); + var mod = new List(); + var ens = new List(); + var name = MethodName(m, kind); switch (kind) { case MethodTranslationKind.CallPre: + case MethodTranslationKind.CoCallPre: outParams = new List(); - mod = new List(); - ens = new List(); + req = GetRequires(); break; case MethodTranslationKind.CallPost: - req = new List(); + case MethodTranslationKind.CoCallPost: + mod.Add(ordinaryEtran.HeapCastToIdentifierExpr); + ens = GetEnsures(); break; default: + req = GetRequires(); + mod.Add(ordinaryEtran.HeapCastToIdentifierExpr); + ens = GetEnsures(); break; } var proc = new Boogie.Procedure(m.tok, name, new List(), inParams, outParams, false, req, mod, ens, etran.TrAttributes(m.Attributes, null)); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 6b2388c240b..ebe4dd48996 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -1977,41 +1977,49 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E } } - var callBuilder = builder; - if (cs.Proof != null) { - callBuilder = new BoogieStmtListBuilder(this, options, builder.Context); + if (cs.Proof == null) { + AddCall(builder); + } else { + var callBuilder = new BoogieStmtListBuilder(this, options, builder.Context); AddComment(callBuilder, cs, "call statement proof"); CurrentIdGenerator.Push(); TrStmt(cs.Proof, callBuilder, locals, etran); CurrentIdGenerator.Pop(); - } - - callBuilder.Add(new CommentCmd($"ProcessCallStmt: {(isCoCall ? "Make the call" : "Check precondition")}")); - // Make the call - AddReferencedMember(callee); - Bpl.CallCmd call = Call(tok, MethodName(callee, isCoCall ? MethodTranslationKind.CoCall : MethodTranslationKind.CallPre), ins, isCoCall ? outs : new List()); - proofDependencies?.AddProofDependencyId(call, tok, new CallDependency(cs)); - if ( - (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) || - (module != currentModule && RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify))) { - // The call statement is inherited, so the refined module already checked that the precondition holds. Note, - // preconditions are not allowed to be strengthened, except if they use a predicate whose body has been strengthened. - // But if the callee sits in a different module, then any predicate it uses will be treated as opaque (that is, - // uninterpreted) anyway, so the refined module will have checked the call precondition for all possible definitions - // of the predicate. - call.IsFree = true; - } - callBuilder.Add(call); - if (cs.Proof != null) { + AddCall(callBuilder); PathAsideBlock(cs.Tok, callBuilder, builder); } - if (!isCoCall) { - builder.Add(new CommentCmd("ProcessCallStmt: Make the call")); - CallCmd post = Call(tok, MethodName(callee, MethodTranslationKind.CallPost), ins, outs); - proofDependencies?.AddProofDependencyId(post, tok, new CallDependency(cs)); - builder.Add(post); + + void AddCall(BoogieStmtListBuilder callBuilder) { + callBuilder.Add(new CommentCmd($"ProcessCallStmt: Check precondition")); + // Make the call + AddReferencedMember(callee); + Bpl.CallCmd call = Call(tok, MethodName(callee, isCoCall ? MethodTranslationKind.CoCallPre : MethodTranslationKind.CallPre), ins, new List()); + proofDependencies?.AddProofDependencyId(call, tok, new CallDependency(cs)); + if ( + (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) || + (module != currentModule && RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify))) { + // The call statement is inherited, so the refined module already checked that the precondition holds. Note, + // preconditions are not allowed to be strengthened, except if they use a predicate whose body has been strengthened. + // But if the callee sits in a different module, then any predicate it uses will be treated as opaque (that is, + // uninterpreted) anyway, so the refined module will have checked the call precondition for all possible definitions + // of the predicate. + call.IsFree = true; + } + callBuilder.Add(call); } + + + + + + + builder.Add(new CommentCmd("ProcessCallStmt: Make the call")); + CallCmd post = Call(tok, MethodName(callee, isCoCall ? MethodTranslationKind.CoCallPost : MethodTranslationKind.CallPost), ins, outs); + proofDependencies?.AddProofDependencyId(post, tok, new CallDependency(cs)); + builder.Add(post); + + // Unbox results as needed for (int i = 0; i < Lhss.Count; i++) { Bpl.IdentifierExpr bLhs = Lhss[i]; diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index eb6198acb18..6a4da1fa878 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -2855,14 +2855,15 @@ Bpl.Function GetOrCreateFunction(Function f) { /// Note that SpecWellformedness and Implementation have procedure implementations /// but no callers, and vice versa for InterModuleCall, IntraModuleCall, and CoCall. /// - enum MethodTranslationKind { SpecWellformedness, CallPre, CallPost, CoCall, Implementation, OverrideCheck } + enum MethodTranslationKind { SpecWellformedness, CallPre, CallPost, CoCallPre, CoCallPost, Implementation, OverrideCheck } private static readonly Dictionary kindSanitizedPrefix = new() { { MethodTranslationKind.SpecWellformedness, "CheckWellFormed" }, { MethodTranslationKind.CallPre, "CallPre" }, { MethodTranslationKind.CallPost, "CallPost" }, - { MethodTranslationKind.CoCall, "CoCall" }, + { MethodTranslationKind.CoCallPre, "CoCallPre" }, + { MethodTranslationKind.CoCallPost, "CoCallPost" }, { MethodTranslationKind.Implementation, "Impl" }, { MethodTranslationKind.OverrideCheck, "OverrideCheck" }, }; @@ -2877,7 +2878,8 @@ static string MethodName(ICodeContext m, MethodTranslationKind kind) { {MethodTranslationKind.SpecWellformedness, "well-formedness"}, {MethodTranslationKind.CallPre, "call precondtion"}, {MethodTranslationKind.CallPost, "call postcondition"}, - {MethodTranslationKind.CoCall, "co-call"}, + {MethodTranslationKind.CoCallPre, "co-call precondtion"}, + {MethodTranslationKind.CoCallPost, "co-call postcondition"}, {MethodTranslationKind.Implementation, "correctness"}, {MethodTranslationKind.OverrideCheck, "override check"}, }; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy index e32c596064a..6d83e1da819 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy @@ -56,3 +56,12 @@ method E() returns (r: Option){ assert P(); // should fail r := None; } + +greatest predicate G(x: int) { x == 0 || G(x-2) } + +greatest lemma F(x: int) + ensures G(x) +{ + F(x-2) by { ProveP(); } + assert P(); // should fail +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect index 13436c6a151..b4849841fcd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect @@ -3,5 +3,6 @@ CallBy.dfy(32,10): Error: assertion might not hold CallBy.dfy(39,10): Error: assertion might not hold CallBy.dfy(50,10): Error: assertion might not hold CallBy.dfy(56,10): Error: assertion might not hold +CallBy.dfy(66,10): Error: assertion might not hold -Dafny program verifier finished with 3 verified, 5 errors +Dafny program verifier finished with 3 verified, 6 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy index 179b97547b7..d1bc619d003 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy @@ -467,8 +467,6 @@ assert heapExternalsZeroOrOneEdges(xedges); o.fields := o.fields[f := t]; ///who designed this fucking syntax? assert ObjectsAreValid({o}); - - // assert edges(objects) == old( edges(objects) ) + {Edge(o,f,t)}; var zedges := edges(objects); //or could hand in if necessary? var zisos := justTheIsos(objects); From bec0763cc3b19ec8d10348b5f224ceea83e46467 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 9 Aug 2024 20:21:18 +0200 Subject: [PATCH 16/19] adjust ids again --- .../dafny0/TriggerInPredicate.dfy.expect | 1 - .../Snapshots0.run.legacy.dfy.expect | 2 +- .../Snapshots1.run.legacy.dfy.expect | 2 +- .../Snapshots2.run.legacy.dfy.expect | 18 ++++++++--------- .../Snapshots5.run.legacy.dfy.expect | 8 ++++---- .../Snapshots8.run.legacy.dfy.expect | 20 +++++++++---------- .../Snapshots9.run.legacy.dfy.expect | 8 ++++---- .../git-issues/git-issue-3855.dfy.expect | 10 +++++----- .../triggers-prevent-some-inlining.dfy.expect | 2 -- 9 files changed, 34 insertions(+), 37 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect index 0e1599f1f50..e47d3f949d8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect @@ -1,5 +1,4 @@ TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined. TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined. -TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect index 711eb590f99..bc7f9c7e992 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect @@ -7,7 +7,7 @@ Processing call to procedure bar (call precondtion) in implementation foo (corre Processing call to procedure bar (call postcondition) in implementation foo (correctness) (at Snapshots0.v1.dfy(3,6)): >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##1(call0old#AT#$Heap, $Heap) } ##extracted_function##1(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall $o: ref :: { $Heap[$o] } $o != null && $Unbox(read(call0old#AT#$Heap, $o, alloc)): bool ==> $Heap[$o] == call0old#AT#$Heap[$o]) && $HeapSucc(call0old#AT#$Heap, $Heap))) >>> added after: a##cached##1 := a##cached##1 && ##extracted_function##1(call0old#AT#$Heap, $Heap); -Processing command (at Snapshots0.v1.dfy(4,10)) assert {:id "id8"} Lit(false); +Processing command (at Snapshots0.v1.dfy(4,10)) assert {:id "id7"} Lit(false); >>> MarkAsPartiallyVerified Snapshots0.v1.dfy(4,9): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect index 79adfe82043..6c278ab5388 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect @@ -4,7 +4,7 @@ Processing command (at Snapshots1.v0.dfy(4,10)) assert {:id "id2"} Lit(false); Dafny program verifier finished with 1 verified, 0 errors Processing call to procedure N (call postcondition) in implementation M (correctness) (at Snapshots1.v1.dfy(3,4)): >>> added after: a##cached##0 := a##cached##0 && false; -Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id9"} Lit(false); +Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id8"} Lit(false); >>> DoNothingToAssert Snapshots1.v1.dfy(4,9): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect index b4b0df2dd7c..401acbc1f66 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect @@ -1,12 +1,12 @@ Processing command (at Snapshots2.v0.dfy(4,10)) assert {:id "id2"} Lit(false); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id7"} Lit(true); +Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id6"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(11,15)) assert {:id "id6"} _module.__default.P() <==> _module.__default.Q(); +Processing command (at Snapshots2.v0.dfy(11,15)) assert {:id "id5"} _module.__default.P() <==> _module.__default.Q(); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id10"} Lit(true); +Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id9"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id9"} _module.__default.Q() <==> Lit(_module.__default.R()); +Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id8"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert Dafny program verifier finished with 3 verified, 0 errors @@ -16,16 +16,16 @@ Processing implementation P (well-formedness) (at Snapshots2.v1.dfy(10,11)): >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; Processing implementation Q (well-formedness) (at Snapshots2.v1.dfy(13,11)): >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false; -Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id15"} Lit(false); +Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id14"} Lit(false); >>> DoNothingToAssert Snapshots2.v1.dfy(4,9): Error: assertion might not hold -Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id20"} Lit(true); +Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id18"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id19"} _module.__default.P() <==> _module.__default.Q(); +Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id17"} _module.__default.P() <==> _module.__default.Q(); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id23"} Lit(true); +Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id21"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id22"} _module.__default.Q() <==> Lit(_module.__default.R()); +Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id20"} _module.__default.Q() <==> Lit(_module.__default.R()); >>> DoNothingToAssert Dafny program verifier finished with 2 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect index 1df0bbd2479..8a6d82c8b15 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect @@ -15,13 +15,13 @@ Snapshots5.v1.dfy(13,10): Warning: Could not find a trigger for this quantifier. Snapshots5.v1.dfy(20,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Snapshots5.v1.dfy(22,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Snapshots5.v1.dfy(27,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. -Processing command (at Snapshots5.v1.dfy(10,40)) assert {:id "id14"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0; +Processing command (at Snapshots5.v1.dfy(10,40)) assert {:id "id13"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0; >>> MarkAsFullyVerified -Processing command (at Snapshots5.v1.dfy(13,38)) assert {:id "id17"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3; +Processing command (at Snapshots5.v1.dfy(13,38)) assert {:id "id16"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3; >>> MarkAsFullyVerified -Processing command (at Snapshots5.v1.dfy(20,37)) assert {:id "id18"} (exists b#3_1: bool :: Lit(true)) || 4 != 4; +Processing command (at Snapshots5.v1.dfy(20,37)) assert {:id "id17"} (exists b#3_1: bool :: Lit(true)) || 4 != 4; >>> DoNothingToAssert -Processing command (at Snapshots5.v1.dfy(22,35)) assert {:id "id19"} (exists b#3: bool :: Lit(true)) || 5 != 5; +Processing command (at Snapshots5.v1.dfy(22,35)) assert {:id "id18"} (exists b#3: bool :: Lit(true)) || 5 != 5; >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect index 9a5c564e0d7..114c1a89a2e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect @@ -8,35 +8,35 @@ Processing command (at Snapshots8.v0.dfy(4,8)) assert {:id "id5$id2$requires"} { Snapshots8.v0.dfy(3,11): Error: assertion might not hold Snapshots8.v0.dfy(4,7): Error: a precondition for this call could not be proved Snapshots8.v0.dfy(8,13): Related location: this is the precondition that could not be proved -Processing command (at Snapshots8.v0.dfy(13,13)) assert {:id "id11"} LitInt(2) <= z#0; +Processing command (at Snapshots8.v0.dfy(13,13)) assert {:id "id9"} LitInt(2) <= z#0; >>> DoNothingToAssert Snapshots8.v0.dfy(17,9): Error: a postcondition could not be proved on this return path Snapshots8.v0.dfy(13,12): Related location: this is the postcondition that could not be proved -Processing command (at Snapshots8.v0.dfy(23,12)) assert {:id "id13"} u#0 != 53; +Processing command (at Snapshots8.v0.dfy(23,12)) assert {:id "id11"} u#0 != 53; >>> DoNothingToAssert Snapshots8.v0.dfy(23,11): Error: assertion might not hold -Processing command (at Snapshots8.v0.dfy(28,10)) assert {:id "id14"} Lit(true); +Processing command (at Snapshots8.v0.dfy(28,10)) assert {:id "id12"} Lit(true); >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 4 errors -Processing command (at Snapshots8.v1.dfy(30,17)) assert {:id "id30"} u#0 != 53; +Processing command (at Snapshots8.v1.dfy(30,17)) assert {:id "id26"} u#0 != 53; >>> RecycleError Snapshots8.v1.dfy(30,16): Error: assertion might not hold -Processing command (at Snapshots8.v1.dfy(3,15)) assert {:id "id15"} x#0 < 20 || LitInt(10) <= x#0; +Processing command (at Snapshots8.v1.dfy(3,15)) assert {:id "id13"} x#0 < 20 || LitInt(10) <= x#0; >>> MarkAsFullyVerified -Processing command (at Snapshots8.v1.dfy(5,17)) assert {:id "id16"} x#0 < 10; +Processing command (at Snapshots8.v1.dfy(5,17)) assert {:id "id14"} x#0 < 10; >>> RecycleError -Processing command (at Snapshots8.v1.dfy(6,8)) assert {:id "id21$id17$requires"} {:id "id17"} LitInt(0) <= call0formal#AT#y#0; +Processing command (at Snapshots8.v1.dfy(6,8)) assert {:id "id19$id15$requires"} {:id "id15"} LitInt(0) <= call0formal#AT#y#0; >>> RecycleError -Processing command (at Snapshots8.v1.dfy(7,12)) assert {:id "id19"} x#0 == LitInt(7); +Processing command (at Snapshots8.v1.dfy(7,12)) assert {:id "id17"} x#0 == LitInt(7); >>> DoNothingToAssert Snapshots8.v1.dfy(5,16): Error: assertion might not hold Snapshots8.v1.dfy(6,7): Error: a precondition for this call could not be proved Snapshots8.v1.dfy(12,20): Related location: this is the precondition that could not be proved Snapshots8.v1.dfy(7,11): Error: assertion might not hold -Processing command (at Snapshots8.v1.dfy(23,12)) assert {:id "id29"} Lit(true); +Processing command (at Snapshots8.v1.dfy(23,12)) assert {:id "id25"} Lit(true); >>> DoNothingToAssert -Processing command (at Snapshots8.v1.dfy(19,13)) assert {:id "id27"} LitInt(2) <= z#0; +Processing command (at Snapshots8.v1.dfy(19,13)) assert {:id "id23"} LitInt(2) <= z#0; >>> DoNothingToAssert Snapshots8.v1.dfy(24,9): Error: a postcondition could not be proved on this return path Snapshots8.v1.dfy(19,12): Related location: this is the postcondition that could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect index dc5172019fd..36e8d43cba9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots9.run.legacy.dfy.expect @@ -1,19 +1,19 @@ Warning: this way of using the CLI is deprecated. Use 'dafny --help' to see help for the new Dafny CLI format -Processing command (at Snapshots9.v0.dfy(2,11)) assert {:id "id3"} ok#0; +Processing command (at Snapshots9.v0.dfy(2,11)) assert {:id "id2"} ok#0; >>> DoNothingToAssert Snapshots9.v0.dfy(4,7): Error: a postcondition could not be proved on this return path Snapshots9.v0.dfy(2,10): Related location: this is the postcondition that could not be proved -Processing command (at Snapshots9.v0.dfy(12,11)) assert {:id "id9"} ok#0; +Processing command (at Snapshots9.v0.dfy(12,11)) assert {:id "id7"} ok#0; >>> DoNothingToAssert Snapshots9.v0.dfy(13,0): Error: a postcondition could not be proved on this return path Snapshots9.v0.dfy(12,10): Related location: this is the postcondition that could not be proved Dafny program verifier finished with 0 verified, 2 errors -Processing command (at Snapshots9.v1.dfy(6,11)) assert {:id "id13"} ok#0; +Processing command (at Snapshots9.v1.dfy(6,11)) assert {:id "id10"} ok#0; >>> RecycleError Snapshots9.v1.dfy(8,7): Error: a postcondition could not be proved on this return path Snapshots9.v1.dfy(6,10): Related location: this is the postcondition that could not be proved -Processing command (at Snapshots9.v1.dfy(19,11)) assert {:id "id19"} ok#0; +Processing command (at Snapshots9.v1.dfy(19,11)) assert {:id "id15"} ok#0; >>> RecycleError Snapshots9.v1.dfy(21,0): Error: a postcondition could not be proved on this return path Snapshots9.v1.dfy(19,10): Related location: this is the postcondition that could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect index efc7dd6b97d..1ba70097ea1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect @@ -1,10 +1,10 @@ -git-issue-3855.dfy(801,0): Warning: attribute :ignore is deprecated -git-issue-3855.dfy(801,11): Error: Verification of 'Memory.dynMove' timed out after seconds -git-issue-3855.dfy(944,17): Error: a precondition for this call could not be proved +git-issue-3855.dfy(799,0): Warning: attribute :ignore is deprecated +git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after seconds +git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved git-issue-3855.dfy(430,29): Related location: this is the precondition that could not be proved -git-issue-3855.dfy(944,17): Error: a precondition for this call could not be proved +git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved git-issue-3855.dfy(434,36): Related location: this is the precondition that could not be proved -git-issue-3855.dfy(1337,20): Error: a precondition for this call could not be proved +git-issue-3855.dfy(1335,20): Error: a precondition for this call could not be proved git-issue-3855.dfy(434,36): Related location: this is the precondition that could not be proved Dafny program verifier finished with 101 verified, 3 errors, 1 time out diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect index 2d3fea2d577..89c40cc572a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/triggers-prevent-some-inlining.dfy.expect @@ -3,7 +3,5 @@ triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call are triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call are not inlined. triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call are not inlined. triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call are not inlined. -triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call are not inlined. -triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call are not inlined. Dafny program verifier finished with 1 verified, 0 errors From f93e007e007fab9037026cf037b202464c415dd7 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Sat, 10 Aug 2024 10:59:12 +0200 Subject: [PATCH 17/19] dedup --- .../AST/Statements/Verification/AssertStmt.cs | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs index 295803e9e6e..306f1d4815b 100644 --- a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs @@ -89,16 +89,7 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext co base.GenResolve(resolver, context); - if (Proof != null) { - // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave a the proof body - var prevLblStmts = resolver.EnclosingStatementLabels; - var prevLoopStack = resolver.LoopStack; - resolver.EnclosingStatementLabels = new Scope(resolver.Options); - resolver.LoopStack = new List(); - resolver.ResolveStatement(Proof, context); - resolver.EnclosingStatementLabels = prevLblStmts; - resolver.LoopStack = prevLoopStack; - } + ModuleResolver.ResolveByProof(resolver, Proof, context); } public bool HasAssertOnlyAttribute(out AssertOnlyKind assertOnlyKind) { From 056a6583d1112e18f926f29c6d91250a74453810 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Sun, 11 Aug 2024 13:59:18 +0200 Subject: [PATCH 18/19] remove whitespace --- Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs | 7 ------- 1 file changed, 7 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index ebe4dd48996..64b4d1271fe 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -2008,18 +2008,11 @@ void AddCall(BoogieStmtListBuilder callBuilder) { callBuilder.Add(call); } - - - - - - builder.Add(new CommentCmd("ProcessCallStmt: Make the call")); CallCmd post = Call(tok, MethodName(callee, isCoCall ? MethodTranslationKind.CoCallPost : MethodTranslationKind.CallPost), ins, outs); proofDependencies?.AddProofDependencyId(post, tok, new CallDependency(cs)); builder.Add(post); - // Unbox results as needed for (int i = 0; i < Lhss.Count; i++) { Bpl.IdentifierExpr bLhs = Lhss[i]; From 27cded39a470b4d05735c232ab0573ce990c681c Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Mon, 12 Aug 2024 15:55:23 +0200 Subject: [PATCH 19/19] add test for hide --- .../LitTests/LitTest/dafny0/CallByHide.dfy | 16 ++++++++++++++++ .../LitTest/dafny0/CallByHide.dfy.expect | 3 +++ 2 files changed, 19 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy new file mode 100644 index 00000000000..31e5fe5fb51 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy @@ -0,0 +1,16 @@ +// RUN: ! %verify --type-system-refresh %s > %t +// RUN: %diff "%s.expect" "%t" + +predicate P() { true } + +method NeedsP() + requires P() +{} + +method M() + ensures P() +{ + hide P; + NeedsP() by { reveal P(); } + assert P(); // should fail +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy.expect new file mode 100644 index 00000000000..ef939499206 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy.expect @@ -0,0 +1,3 @@ +CallByHide.dfy(15,10): Error: assertion might not hold + +Dafny program verifier finished with 0 verified, 1 error