From f7a0a55e08bc620c40c1990b3b3999a1fc91764a Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Mon, 12 Aug 2024 17:28:39 +0200 Subject: [PATCH] feat: Method calls with a by-proof (#5662) Fixes #5582. To enable this, we split method calls into two separate calls on the boogie level. ``` TODAY: // check termination... call z := Call$$MyMethod(u); AFTER SPLITTING Call$$, we have: // check termination... call Call_Pre$$MyMethod(u); call z := Call_Post$$MyMethod(u); FOR CALL-BY, WE HAVE: // check termination... if (*) { // include the proof here LemmaAboutP(); call Call_Pre$$MyMethod(u); assume false; } call z := Call_Post$$MyMethod(u); ``` --- .../AST/Grammar/Printer/Printer.Statement.cs | 19 ++- .../Assignment/AssignOrReturnStmt.cs | 11 +- .../AST/Statements/Assignment/UpdateStmt.cs | 15 ++- .../AST/Statements/Methods/CallStmt.cs | 9 +- .../AST/Statements/Verification/AssertStmt.cs | 11 +- Source/DafnyCore/Dafny.atg | 30 +++-- .../Resolver/GhostInterestVisitor.cs | 3 + Source/DafnyCore/Resolver/ModuleResolver.cs | 15 +++ .../PreType/PreTypeResolve.Statements.cs | 32 +++-- .../Verifier/BoogieGenerator.Iterators.cs | 2 +- .../Verifier/BoogieGenerator.Methods.cs | 124 ++++++++++++------ .../Verifier/BoogieGenerator.TrStatement.cs | 58 +++++--- Source/DafnyCore/Verifier/BoogieGenerator.cs | 16 ++- .../AddImplementationForCallsRewriter.cs | 4 +- .../LitTests/LitTest/dafny0/CallBy.dfy | 67 ++++++++++ .../LitTests/LitTest/dafny0/CallBy.dfy.expect | 8 ++ .../LitTests/LitTest/dafny0/CallByHide.dfy | 16 +++ .../LitTest/dafny0/CallByHide.dfy.expect | 3 + .../LitTest/dafny0/CallByResolution0.dfy | 11 ++ .../dafny0/CallByResolution0.dfy.expect | 3 + .../LitTest/dafny0/CallByResolution1.dfy | 13 ++ .../dafny0/CallByResolution1.dfy.expect | 2 + .../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 ++-- .../LitTest/git-issues/git-issue-3855.dfy | 2 - .../git-issues/git-issue-3855.dfy.expect | 10 +- docs/DafnyRef/Statements.16.expect | 3 + docs/DafnyRef/Statements.md | 32 +++++ docs/dev/news/5662.feat | 1 + 32 files changed, 438 insertions(+), 158 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy.expect 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 create mode 100644 docs/DafnyRef/Statements.16.expect create mode 100644 docs/dev/news/5662.feat diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs index 26227fae09a..ef97d0be06f 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,20 @@ public void PrintStatement(Statement stmt, int indent) { } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement } + + void PrintBy(ConcreteUpdateStatement statement) { + BlockStmt proof = statement switch { + UpdateStmt updateStmt => updateStmt.Proof, + AssignOrReturnStmt returnStmt => returnStmt.Proof, + _ => null + }; + if (proof != null) { + wr.Write(" by "); + PrintStatement(proof, indent); + } else { + wr.Write(";"); + } + } } private void PrintHideReveal(HideRevealStmt revealStmt) { diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs index 0b6199ae2bb..a598f530af8 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 { @@ -22,7 +23,7 @@ public override IToken Tok { } } - public override IEnumerable Children => ResolvedStatements; + public override IEnumerable Children => ResolvedStatements.Concat(Proof?.Children ?? new List()); public override IEnumerable PreResolveSubStatements => Enumerable.Empty(); [ContractInvariantMethod] @@ -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,8 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti return; } + ModuleResolver.ResolveByProof(resolver, Proof, resolutionContext); + Expression lhsExtract = null; if (expectExtract) { if (resolutionContext.CodeContext is Method caller && caller.Outs.Count == 0 && KeywordToken == null) { @@ -285,7 +290,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..0b61df6ab30 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 { @@ -22,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(); @@ -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,9 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti resolver.ResolveAttributes(rhs, resolutionContext); } + // resolve proof + ModuleResolver.ResolveByProof(resolver, Proof, resolutionContext); + // figure out what kind of UpdateStmt this is if (firstEffectfulRhs == null) { if (Lhss.Count == 0) { @@ -178,7 +185,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/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) { diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 7c9eaa7c000..d069d01cb73 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -2297,6 +2297,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; @@ -2334,10 +2335,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"); @@ -2352,18 +2359,21 @@ UpdateStmt { Attribute } (. exceptionRhs = new ExprRhs(exceptionExpr, attrs); .) { "," Rhs (. rhss.Add(r); .) } - ";" (. endTok = t; .) + ( + "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); } } .) @@ -2463,6 +2473,7 @@ VarDeclStatement<.out Statement/*!*/ s.> ExprRhs exceptionRhs = null; Attributes attrs = null; Attributes tokenAttrs = null; + BlockStmt proof = null; IToken endTok; IToken startToken = null; s = dummyStmt; @@ -2499,7 +2510,10 @@ VarDeclStatement<.out Statement/*!*/ s.> { "," Rhs (. rhss.Add(r); .) } ] - SYNC ";" (. endTok = t; .) + SYNC ( "by" + BlockStmt + | ";" (. endTok = t; .) + ) (. ConcreteUpdateStatement update; var lhsExprs = new List(); if (isGhost || (rhss.Count == 0 && exceptionRhs == null && suchThat == null)) { // explicitly ghost or no init @@ -2516,11 +2530,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/GhostInterestVisitor.cs b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs index df6868accd8..149e330a040 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, "a 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..18d48daf379 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -3311,6 +3311,21 @@ internal LetExpr LetVarIn(IToken tok, string name, Type tp, Expression rhs, Expr return LetPatIn(tok, lhs, rhs, body); } + 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; + } + /// /// 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 3764e520a4d..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; } @@ -650,13 +652,17 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo ResolveAttributes(rhs, resolutionContext, false); } + // resolve proof + 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) @@ -669,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."); @@ -689,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]); @@ -703,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); + 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,8 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r return; } + ModuleResolver.ResolveByProof(this, s.Proof, resolutionContext); + Expression lhsExtract = null; if (expectExtract) { if (enclosingMethod.Outs.Count == 0 && s.KeywordToken == null) { @@ -991,7 +1005,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]; } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs index b08bf91f8a4..6ba4aef2c77 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(new BodyTranslationContext(false), 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 972d1375a27..b50c0d48353 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -193,13 +193,17 @@ 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 // 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 @@ -1696,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); @@ -1710,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) { @@ -1761,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)); @@ -1794,7 +1810,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")))); @@ -1816,9 +1832,31 @@ 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(); + req = GetRequires(); + break; + case MethodTranslationKind.CallPost: + 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)); AddVerboseNameAttribute(proc, m.FullDafnyName, kind); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 812d169679b..64b4d1271fe 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -1771,20 +1771,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); @@ -1980,22 +1977,41 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E } } + 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(); + AddCall(callBuilder); + PathAsideBlock(cs.Tok, callBuilder, builder); + } + + 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")); - // Make the call - AddReferencedMember(callee); - Bpl.CallCmd call = Call(tok, MethodName(callee, kind), ins, outs); - 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; - } - builder.Add(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++) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index e30bd6c6a5e..6a4da1fa878 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -2855,13 +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, Call, CoCall, Implementation, OverrideCheck } + enum MethodTranslationKind { SpecWellformedness, CallPre, CallPost, CoCallPre, CoCallPost, Implementation, OverrideCheck } private static readonly Dictionary kindSanitizedPrefix = new() { { MethodTranslationKind.SpecWellformedness, "CheckWellFormed" }, - { MethodTranslationKind.Call, "Call" }, - { MethodTranslationKind.CoCall, "CoCall" }, + { MethodTranslationKind.CallPre, "CallPre" }, + { MethodTranslationKind.CallPost, "CallPost" }, + { MethodTranslationKind.CoCallPre, "CoCallPre" }, + { MethodTranslationKind.CoCallPost, "CoCallPost" }, { MethodTranslationKind.Implementation, "Impl" }, { MethodTranslationKind.OverrideCheck, "OverrideCheck" }, }; @@ -2874,8 +2876,10 @@ static string MethodName(ICodeContext m, MethodTranslationKind kind) { private static readonly Dictionary kindDescription = new Dictionary() { {MethodTranslationKind.SpecWellformedness, "well-formedness"}, - {MethodTranslationKind.Call, "call"}, - {MethodTranslationKind.CoCall, "co-call"}, + {MethodTranslationKind.CallPre, "call precondtion"}, + {MethodTranslationKind.CallPost, "call postcondition"}, + {MethodTranslationKind.CoCallPre, "co-call precondtion"}, + {MethodTranslationKind.CoCallPost, "co-call postcondition"}, {MethodTranslationKind.Implementation, "correctness"}, {MethodTranslationKind.OverrideCheck, "override check"}, }; @@ -4586,7 +4590,7 @@ List TrSplitExprForMethodSpec(BodyTranslationContext context, Exp var splits = new List(); var applyInduction = kind == MethodTranslationKind.Implementation; bool splitHappened; // we don't actually care - splitHappened = TrSplitExpr(context, expr, splits, true, int.MaxValue, kind != MethodTranslationKind.Call, applyInduction, etran); + splitHappened = TrSplitExpr(context, expr, splits, true, int.MaxValue, kind != MethodTranslationKind.CallPost, applyInduction, etran); return splits; } diff --git a/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs b/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs index d6844fa3c7b..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 "Call$$" 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 = "Call$$"; + private const string CallPrefix = "CallPost$$"; private readonly DafnyOptions options; private List implsToAdd = new(); 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..6d83e1da819 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy @@ -0,0 +1,67 @@ +// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --standard-libraries + +import opened Std.Wrappers + +opaque predicate P() { true } + +lemma ProveP() ensures P() { + reveal P(); +} + +method NeedsP() + requires P() +{} + +method NeedsPAndReturns3() returns (r: int) + requires P() + ensures r == 3 +{ r := 3; } + +method NeedsPAndReturnsNone() returns (r: Option) + requires P() +{ r := None; } + +method A() { + NeedsP() by { ProveP(); } + assert P(); // Should fail +} + +method B() { + var v: int; + v := NeedsPAndReturns3() by { reveal P(); } + assert P(); // Should fail +} + +method C() { + assert p: P() by { ProveP(); } + var v := NeedsPAndReturns3() by { reveal p; } + assert v == 3; // should pass + assert P(); // should fail +} + +method D() returns (r: Option){ + var v: int; + 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 :- NeedsPAndReturnsNone() by { reveal P(); } + 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 new file mode 100644 index 00000000000..b4849841fcd --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect @@ -0,0 +1,8 @@ +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 +CallBy.dfy(66,10): Error: assertion might not hold + +Dafny program verifier finished with 3 verified, 6 errors 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 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 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..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 @@ -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 "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 a2ef2d3d341..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 @@ -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 "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 768491421f5..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,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 "id6"} 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 "id5"} _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 "id9"} 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 "id8"} _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 "id14"} 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 "id18"} 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 "id17"} _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 "id21"} 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 "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 5566f116ad4..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 @@ -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 "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 "id12"} (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 "id13"} (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 "id14"} (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 0b3564e7be2..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 @@ -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 "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 "id10"} 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 "id11"} 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 "id24"} 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 "id12"} 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 "id13"} 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 "id17$id14$requires"} {:id "id14"} 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 "id15"} 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 "id23"} 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 "id21"} 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/git-issues/git-issue-3855.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy index 9c23169829f..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); 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/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