From 21a92460cc756285022c0211e67eb1d215a11e8c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 15 Jul 2024 12:39:27 +0200 Subject: [PATCH 01/32] Add tests --- .../ast/expressions/statementExpressions.dfy | 27 +++++++++++++++++++ .../statementExpressions.dfy.expect | 0 2 files changed, 27 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy new file mode 100644 index 00000000000..e6d4da7a062 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy @@ -0,0 +1,27 @@ +// RUN: %verify --type-system-refresh --allow-axioms --bprint:%t.bpl --isolate-assertions --boogie "/printPruned:%S/pruned" %s > %t +// RUN: %diff "%s.expect" "%t" + +function StmtExprValueAndEnsures(): int + ensures ValueAndEnsures() == 42 +{ + assert true; 42 +} + +function ExpressionWFVersusFunctionEnsures(): int + ensures 10 == 11 // no error, since the statement expression can be used for the ensures clause +{ + assume false; 10 +} + +function ExpressionWFAndLet(): int +{ + var x := assume false; 10; + assert false; // error, since the statement expression does not leak outside of the let. + x +} + +method Bar() { + var x := assume false; 3; + assert false; // error +} + diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy.expect new file mode 100644 index 00000000000..e69de29bb2d From 0ec4c02a2379c7bad556f79e42a43dab7d4ab566 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 15 Jul 2024 12:43:28 +0200 Subject: [PATCH 02/32] Fix test --- .../ast/expressions/statementExpressions.dfy | 22 ++++++++++++++----- .../statementExpressions.dfy.expect | 2 ++ 2 files changed, 19 insertions(+), 5 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy index e6d4da7a062..127135beb3d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy @@ -1,18 +1,30 @@ -// RUN: %verify --type-system-refresh --allow-axioms --bprint:%t.bpl --isolate-assertions --boogie "/printPruned:%S/pruned" %s > %t +// RUN: ! %verify --type-system-refresh --allow-axioms --bprint:%t.bpl --isolate-assertions %s > %t // RUN: %diff "%s.expect" "%t" -function StmtExprValueAndEnsures(): int - ensures ValueAndEnsures() == 42 +function StatementExpressionValueAndEnsures(): int + ensures StatementExpressionValueAndEnsures() == 42 { assert true; 42 } -function ExpressionWFVersusFunctionEnsures(): int +function StatementExpressionAssumeAndFunctionEnsures(): int ensures 10 == 11 // no error, since the statement expression can be used for the ensures clause { assume false; 10 } +function StatementExpressionAndSubsetResult(): nat + // no error, since the statement expression can be used for the return type subset constraint +{ + assume -1 > 0; -1 +} + +method StatementExpressionAndSubsetLocal() + // no error, since the statement expression can be used for the return type subset constraint +{ + var x: nat := assume -1 > 0; -1; +} + function ExpressionWFAndLet(): int { var x := assume false; 10; @@ -20,7 +32,7 @@ function ExpressionWFAndLet(): int x } -method Bar() { +method StatementExpressionAssumeDoesNotEscapeExpression() { var x := assume false; 3; assert false; // error } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy.expect index e69de29bb2d..0471f345c93 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 12 verified, 2 errors From a0d6c9dd13a6e92ac67fdc5208110869d46efd5c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 25 Jul 2024 13:19:22 +0200 Subject: [PATCH 03/32] Update test --- ...ressions.dfy => statementExpressionScope.dfy} | 16 ++++++++++++---- ...xpect => statementExpressionScope.dfy.expect} | 0 2 files changed, 12 insertions(+), 4 deletions(-) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/{statementExpressions.dfy => statementExpressionScope.dfy} (65%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/{statementExpressions.dfy.expect => statementExpressionScope.dfy.expect} (100%) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy similarity index 65% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy index 127135beb3d..c420b478a94 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy @@ -20,20 +20,28 @@ function StatementExpressionAndSubsetResult(): nat } method StatementExpressionAndSubsetLocal() - // no error, since the statement expression can be used for the return type subset constraint + // no error, since the statement expression can be used for the local variable type subset constraint { var x: nat := assume -1 > 0; -1; } -function ExpressionWFAndLet(): int +predicate P(x: int) +method NeedsP(x: int) requires P(x) + +method StatementExpressionAndPrecondition(x: int) +{ + NeedsP(assume P(x); x); // no error, since the statement expression can be used for the requires clause +} + +function StatementExpressionAssumeDoesNotEscapeLetBinding(): int { var x := assume false; 10; assert false; // error, since the statement expression does not leak outside of the let. x } -method StatementExpressionAssumeDoesNotEscapeExpression() { +method StatementExpressionAssumeDoesNotEscapeAssignment() { var x := assume false; 3; - assert false; // error + assert false; // error, since the statement expression does not leak outside of the assignment. } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressions.dfy.expect rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect From 42faecaccbb4009189fb7a8c13ef86ca3d174c8e Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 Jul 2024 17:15:37 +0200 Subject: [PATCH 04/32] Put function wellformedness check in a separate file, and extract some methods --- .../BoogieGenerator.ExpressionWellformed.cs | 1 + ...oogieGenerator.Functions.Wellformedness.cs | 353 ++++++++++++++++++ .../Verifier/BoogieGenerator.Functions.cs | 287 -------------- .../Verifier/BoogieGenerator.Methods.cs | 2 +- .../Verifier/BoogieGenerator.TrStatement.cs | 49 +-- 5 files changed, 382 insertions(+), 310 deletions(-) create mode 100644 Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 8de7eacb036..917aee73bf9 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -1336,6 +1336,7 @@ void CheckOperand(Expression operand) { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression } + if (result != null) { Contract.Assert(resultType != null); var bResult = etran.TrExpr(expr); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs new file mode 100644 index 00000000000..81b42013a70 --- /dev/null +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -0,0 +1,353 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using DafnyCore.Verifier; +using Microsoft.Boogie; +using static Microsoft.Dafny.Util; +using Bpl = Microsoft.Boogie; +using PODesc = Microsoft.Dafny.ProofObligationDescription; + +namespace Microsoft.Dafny; + +public partial class BoogieGenerator { + class FunctionWellformednessChecker { + private readonly BoogieGenerator generator; + + public FunctionWellformednessChecker(BoogieGenerator generator) { + this.generator = generator; + } + + public void Check(Function f) { + + Contract.Assert(generator.InVerificationScope(f)); + + generator.proofDependencies.SetCurrentDefinition(MethodVerboseName(f.FullDafnyName, + MethodTranslationKind.SpecWellformedness)); + generator.currentModule = f.EnclosingClass.EnclosingModuleDefinition; + generator.codeContext = f; + + Expr prevHeap = null; + Expr currHeap = null; + var ordinaryEtran = new ExpressionTranslator(generator, generator.predef, f.tok, f); + ExpressionTranslator etran; + var inParams_Heap = new List(); + if (f is TwoStateFunction) { + var prevHeapVar = new Bpl.Formal(f.tok, new TypedIdent(f.tok, "previous$Heap", generator.predef.HeapType), true); + var currHeapVar = new Bpl.Formal(f.tok, new TypedIdent(f.tok, "current$Heap", generator.predef.HeapType), true); + inParams_Heap.Add(prevHeapVar); + inParams_Heap.Add(currHeapVar); + prevHeap = new Bpl.IdentifierExpr(f.tok, prevHeapVar); + currHeap = new Bpl.IdentifierExpr(f.tok, currHeapVar); + etran = new ExpressionTranslator(generator, generator.predef, currHeap, prevHeap, f); + } else { + etran = ordinaryEtran; + } + + // parameters of the procedure + var typeInParams = generator.MkTyParamFormals(GetTypeParams(f), true); + var inParams = GetParameters(f, etran); + var outParams = GetWellformednessProcedureOutParameters(f, etran); + var requires = GetWellformednessProcedureRequires(f, etran, prevHeap, ordinaryEtran, currHeap); + + // modifies $Heap + var mod = new List { + ordinaryEtran.HeapCastToIdentifierExpr, + }; + var ensures = GetWellformnessProcedureEnsures(f, etran); + + var proc = new Procedure(f.tok, "CheckWellformed" + NameSeparator + f.FullSanitizedName, + new List(), + Concat(Concat(typeInParams, inParams_Heap), inParams), outParams, + false, requires, mod, ensures, etran.TrAttributes(f.Attributes, null)); + AddVerboseNameAttribute(proc, f.FullDafnyName, MethodTranslationKind.SpecWellformedness); + generator.sink.AddTopLevelDeclaration(proc); + + if (generator.InsertChecksums) { + generator.InsertChecksum(f, proc, true); + } + + Contract.Assert(proc.InParams.Count == typeInParams.Count + inParams_Heap.Count + inParams.Count); + // Changed the next line to strip from inParams instead of proc.InParams + // They should be the same, but hence the added contract + var implInParams = Bpl.Formal.StripWhereClauses(inParams); + var implOutParams = Bpl.Formal.StripWhereClauses(outParams); + var locals = new List(); + var builder = new BoogieStmtListBuilder(generator, generator.options); + var builderInitializationArea = new BoogieStmtListBuilder(generator, generator.options); + builder.Add(new CommentCmd("AddWellformednessCheck for function " + f)); + if (f is TwoStateFunction) { + // $Heap := current$Heap; + var heap = ordinaryEtran.HeapCastToIdentifierExpr; + builder.Add(Cmd.SimpleAssign(f.tok, heap, etran.HeapExpr)); + etran = ordinaryEtran; // we no longer need the special heap names + } + + builder.AddCaptureState(f.tok, false, "initial state"); + + generator.DefineFrame(f.tok, etran.ReadsFrame(f.tok), f.Reads.Expressions, builder, locals, null); + generator.InitializeFuelConstant(f.tok, builder, etran); + + var delayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, builder); + + // Check well-formedness of any default-value expressions (before assuming preconditions). + delayer.DoWithDelayedReadsChecks(true, wfo => { + foreach (var formal in f.Ins.Where(formal => formal.DefaultValue != null)) { + var e = formal.DefaultValue; + generator.CheckWellformed(e, wfo, locals, builder, + etran.WithReadsFrame(etran.readsFrame, null)); // No frame scope for default values + builder.Add(new AssumeCmd(e.tok, etran.CanCallAssumption(e))); + generator.CheckSubrange(e.tok, etran.TrExpr(e), e.Type, formal.Type, e, builder); + + if (formal.IsOld) { + Expr wh = generator.GetWhereClause(e.tok, etran.TrExpr(e), e.Type, etran.Old, ISALLOC, true); + if (wh != null) { + var desc = new PODesc.IsAllocated("default value", "in the two-state function's previous state", e); + builder.Add(generator.Assert(generator.GetToken(e), wh, desc)); + } + } + } + }); + + // Check well-formedness of the preconditions (including termination), and then + // assume each one of them. After all that (in particular, after assuming all + // of them), do the postponed reads checks. + delayer.DoWithDelayedReadsChecks(false, wfo => { + foreach (AttributedExpression p in f.Req) { + if (p.Label != null) { + p.Label.E = (f is TwoStateFunction ? ordinaryEtran : etran.Old).TrExpr(p.E); + generator.CheckWellformed(p.E, wfo, locals, builder, etran); + } else { + generator.CheckWellformedAndAssume(p.E, wfo, locals, builder, etran, "requires clause"); + } + } + }); + + // Check well-formedness of the reads clause. Note that this is done after assuming + // the preconditions. In other words, the well-formedness of the reads clause is + // allowed to assume the precondition (yet, the requires clause is checked to + // read only those things indicated in the reads clause). + delayer.DoWithDelayedReadsChecks(false, + wfo => { generator.CheckFrameWellFormed(wfo, f.Reads.Expressions, locals, builder, etran); }); + + // If the function is marked as {:concurrent}, check that the reads clause is empty. + if (Attributes.Contains(f.Attributes, Attributes.ConcurrentAttributeName)) { + var desc = new PODesc.ConcurrentFrameEmpty(f, "reads"); + generator.CheckFrameEmpty(f.tok, etran, etran.ReadsFrame(f.tok), builder, desc, null); + } + + // check well-formedness of the decreases clauses (including termination, but no reads checks) + foreach (Expression p in f.Decreases.Expressions) { + generator.CheckWellformed(p, new WFOptions(null, false), locals, builder, etran); + } + + // Generate: + // if (*) { + // check well-formedness of postcondition + // assume false; // don't go on to check the postconditions + // } else { + // check well-formedness of body + // // fall through to check the postconditions themselves + // } + // Here go the postconditions (termination checks included, but no reads checks) + BoogieStmtListBuilder postCheckBuilder = new BoogieStmtListBuilder(generator, generator.options); + // Assume the type returned by the call itself respects its type (this matters if the type is "nat", for example) + { + var args = new List(); + foreach (var p in GetTypeParams(f)) { + args.Add(generator.TrTypeParameter(p)); + } + + if (f.IsFuelAware()) { + args.Add(etran.layerInterCluster.GetFunctionFuel(f)); + } + + if (f.IsOpaque || f.IsMadeImplicitlyOpaque(generator.options)) { + args.Add(generator.GetRevealConstant(f)); + } + + if (f is TwoStateFunction) { + args.Add(etran.Old.HeapExpr); + } + + if (f.ReadsHeap) { + args.Add(etran.HeapExpr); + } + + if (!f.IsStatic) { + args.Add(new Bpl.IdentifierExpr(f.tok, etran.This)); + } + + foreach (var p in f.Ins) { + args.Add(new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(f.IdGenerator), generator.TrType(p.Type))); + } + + Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, generator.TrType(f.ResultType)); + Expr funcAppl = new NAryExpr(f.tok, new FunctionCall(funcID), args); + + var wh = generator.GetWhereClause(f.tok, funcAppl, f.ResultType, etran, NOALLOC); + if (wh != null) { + postCheckBuilder.Add(TrAssumeCmd(f.tok, wh)); + } + } + // Now for the ensures clauses + foreach (AttributedExpression p in f.Ens) { + // assume the postcondition for the benefit of checking the remaining postconditions + generator.CheckWellformedAndAssume(p.E, new WFOptions(f, false), locals, postCheckBuilder, etran, "ensures clause"); + } + + // Here goes the body (and include both termination checks and reads checks) + BoogieStmtListBuilder bodyCheckBuilder = new BoogieStmtListBuilder(generator, generator.options); + if (f.Body == null || !generator.RevealedInScope(f)) { + // don't fall through to postcondition checks + bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Expr.False)); + } else { + var funcID = new FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, generator.TrType(f.ResultType))); + var args = new List(); + foreach (var p in GetTypeParams(f)) { + args.Add(generator.TrTypeParameter(p)); + } + + if (f.IsFuelAware()) { + args.Add(etran.layerInterCluster.GetFunctionFuel(f)); + } + + if (f.IsOpaque || f.IsMadeImplicitlyOpaque(generator.options)) { + args.Add(generator.GetRevealConstant(f)); + } + + if (f is TwoStateFunction) { + args.Add(etran.Old.HeapExpr); + } + + if (f.ReadsHeap) { + args.Add(etran.HeapExpr); + } + + foreach (Variable p in implInParams) { + args.Add(new Bpl.IdentifierExpr(f.tok, p)); + } + + Expr funcAppl = new NAryExpr(f.tok, funcID, args); + + var bodyCheckDelayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, bodyCheckBuilder); + bodyCheckDelayer.DoWithDelayedReadsChecks(false, wfo => { + generator.CheckWellformedWithResult(f.Body, wfo, funcAppl, f.ResultType, locals, bodyCheckBuilder, etran, + "function call result"); + if (f.Result != null) { + var cmd = TrAssumeCmd(f.tok, Expr.Eq(funcAppl, generator.TrVar(f.tok, f.Result))); + generator.proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); + bodyCheckBuilder.Add(cmd); + } + }); + + // Enforce 'older' conditions + var (olderParameterCount, olderCondition) = generator.OlderCondition(f, funcAppl, implInParams); + if (olderParameterCount != 0) { + bodyCheckBuilder.Add(generator.Assert(f.tok, olderCondition, + new PODesc.IsOlderProofObligation(olderParameterCount, f.Ins.Count + (f.IsStatic ? 0 : 1)))); + } + } + + // Combine the two, letting the postcondition be checked on after the "bodyCheckBuilder" branch + postCheckBuilder.Add(TrAssumeCmd(f.tok, Expr.False)); + builder.Add(new IfCmd(f.tok, null, postCheckBuilder.Collect(f.tok), null, bodyCheckBuilder.Collect(f.tok))); + + var s0 = builderInitializationArea.Collect(f.tok); + var s1 = builder.Collect(f.tok); + var implBody = new StmtList(new List(s0.BigBlocks.Concat(s1.BigBlocks)), f.tok); + + if (generator.EmitImplementation(f.Attributes)) { + // emit the impl only when there are proof obligations. + QKeyValue kv = etran.TrAttributes(f.Attributes, null); + var impl = generator.AddImplementationWithAttributes(generator.GetToken(f), proc, + Concat(Concat(Bpl.Formal.StripWhereClauses(typeInParams), inParams_Heap), implInParams), + implOutParams, + locals, implBody, kv); + if (generator.InsertChecksums) { + generator.InsertChecksum(f, impl); + } + } + + Contract.Assert(generator.currentModule == f.EnclosingClass.EnclosingModuleDefinition); + Contract.Assert(generator.codeContext == f); + generator.Reset(); + } + + private List GetWellformednessProcedureOutParameters(Function f, ExpressionTranslator etran) { + var outParams = new List(); + if (f.Result != null) { + Formal p = f.Result; + Contract.Assert(!p.IsOld); + Bpl.Type varType = generator.TrType(p.Type); + Expr wh = generator.GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(f.IdGenerator), varType), + p.Type, etran, NOALLOC); + outParams.Add(new Bpl.Formal(p.tok, new TypedIdent(p.tok, p.AssignUniqueName(f.IdGenerator), varType, wh), + true)); + } + + return outParams; + } + + private List GetWellformnessProcedureEnsures(Function f, ExpressionTranslator etran) { + var ens = new List(); + foreach (AttributedExpression p in f.Ens) { + var functionHeight = generator.currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); + var splits = new List(); + bool splitHappened /*we actually don't care*/ = + generator.TrSplitExpr(p.E, splits, true, functionHeight, true, true, etran); + var (errorMessage, successMessage) = generator.CustomErrorMessage(p.Attributes); + foreach (var s in splits) { + if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, generator.currentModule)) { + generator.AddEnsures(ens, generator.EnsuresWithDependencies(s.Tok, false, p.E, s.E, errorMessage, successMessage, null)); + } + } + } + + return ens; + } + + private List GetWellformednessProcedureRequires(Function f, ExpressionTranslator etran, + Expr prevHeap, + ExpressionTranslator ordinaryEtran, Expr currHeap) { + var requires = new List(); + // free requires mh == ModuleContextHeight && fh == FunctionContextHeight; + requires.Add(generator.Requires(f.tok, true, null, etran.HeightContext(f), null, null, null)); + if (f is TwoStateFunction) { + // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) + var a0 = Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); + var a1 = generator.HeapSucc(prevHeap, currHeap); + var a2 = generator.FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, currHeap); + requires.Add(generator.Requires(f.tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null)); + } + + foreach (var typeBoundAxiom in generator.TypeBoundAxioms(f.tok, Concat(f.EnclosingClass.TypeArgs, f.TypeArgs))) { + requires.Add(generator.Requires(f.tok, true, null, typeBoundAxiom, null, null, null)); + } + + return requires; + } + + private List GetParameters(Function f, ExpressionTranslator etran) { + var inParams = new List(); + if (!f.IsStatic) { + var th = new Bpl.IdentifierExpr(f.tok, "this", generator.TrReceiverType(f)); + Expr wh = BplAnd( + generator.ReceiverNotNull(th), + (f is TwoStateFunction ? etran.Old : etran).GoodRef(f.tok, th, ModuleResolver.GetReceiverType(f.tok, f))); + Bpl.Formal thVar = new Bpl.Formal(f.tok, new TypedIdent(f.tok, "this", generator.TrReceiverType(f), wh), true); + inParams.Add(thVar); + } + + foreach (Formal parameter in f.Ins) { + Bpl.Type varType = generator.TrType(parameter.Type); + Expr wh = generator.GetWhereClause(parameter.tok, + new Bpl.IdentifierExpr(parameter.tok, parameter.AssignUniqueName(f.IdGenerator), varType), parameter.Type, + parameter.IsOld ? etran.Old : etran, f is TwoStateFunction ? ISALLOC : NOALLOC); + inParams.Add(new Bpl.Formal(parameter.tok, + new TypedIdent(parameter.tok, parameter.AssignUniqueName(f.IdGenerator), varType, wh), true)); + } + + return inParams; + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs index 2dd812c60b9..272766a91ee 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs @@ -13,293 +13,6 @@ namespace Microsoft.Dafny; public partial class BoogieGenerator { - void AddWellformednessCheck(Function f) { - Contract.Requires(f != null); - Contract.Requires(sink != null && predef != null); - Contract.Requires(f.EnclosingClass != null); - Contract.Requires(currentModule == null && codeContext == null && isAllocContext != null); - Contract.Ensures(currentModule == null && codeContext == null && isAllocContext != null); - - Contract.Assert(InVerificationScope(f)); - - proofDependencies.SetCurrentDefinition(MethodVerboseName(f.FullDafnyName, MethodTranslationKind.SpecWellformedness)); - currentModule = f.EnclosingClass.EnclosingModuleDefinition; - codeContext = f; - - Bpl.Expr prevHeap = null; - Bpl.Expr currHeap = null; - var ordinaryEtran = new ExpressionTranslator(this, predef, f.tok, f); - ExpressionTranslator etran; - var inParams_Heap = new List(); - if (f is TwoStateFunction) { - var prevHeapVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "previous$Heap", predef.HeapType), true); - var currHeapVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "current$Heap", predef.HeapType), true); - inParams_Heap.Add(prevHeapVar); - inParams_Heap.Add(currHeapVar); - prevHeap = new Bpl.IdentifierExpr(f.tok, prevHeapVar); - currHeap = new Bpl.IdentifierExpr(f.tok, currHeapVar); - etran = new ExpressionTranslator(this, predef, currHeap, prevHeap, f); - } else { - etran = ordinaryEtran; - } - - // parameters of the procedure - var typeInParams = MkTyParamFormals(GetTypeParams(f), true); - var inParams = new List(); - var outParams = new List(); - if (!f.IsStatic) { - var th = new Bpl.IdentifierExpr(f.tok, "this", TrReceiverType(f)); - Bpl.Expr wh = BplAnd( - ReceiverNotNull(th), - (f is TwoStateFunction ? etran.Old : etran).GoodRef(f.tok, th, ModuleResolver.GetReceiverType(f.tok, f))); - Bpl.Formal thVar = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", TrReceiverType(f), wh), true); - inParams.Add(thVar); - } - foreach (Formal p in f.Ins) { - Bpl.Type varType = TrType(p.Type); - Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(f.IdGenerator), varType), p.Type, - p.IsOld ? etran.Old : etran, f is TwoStateFunction ? ISALLOC : NOALLOC); - inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(f.IdGenerator), varType, wh), true)); - } - if (f.Result != null) { - Formal p = f.Result; - Contract.Assert(!p.IsOld); - Bpl.Type varType = TrType(p.Type); - Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(f.IdGenerator), varType), p.Type, etran, NOALLOC); - outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(f.IdGenerator), varType, wh), true)); - } - // the procedure itself - var req = new List(); - // free requires mh == ModuleContextHeight && fh == FunctionContextHeight; - req.Add(Requires(f.tok, true, null, etran.HeightContext(f), null, null, null)); - if (f is TwoStateFunction) { - // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) - var a0 = Bpl.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); - var a1 = HeapSucc(prevHeap, currHeap); - var a2 = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, currHeap); - req.Add(Requires(f.tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null)); - } - - foreach (var typeBoundAxiom in TypeBoundAxioms(f.tok, Concat(f.EnclosingClass.TypeArgs, f.TypeArgs))) { - req.Add(Requires(f.tok, true, null, typeBoundAxiom, null, null, null)); - } - - // modifies $Heap - var mod = new List { - ordinaryEtran.HeapCastToIdentifierExpr, - }; - // check that postconditions hold - var ens = new List(); - foreach (AttributedExpression p in f.Ens) { - var functionHeight = currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); - var splits = new List(); - bool splitHappened /*we actually don't care*/ = TrSplitExpr(p.E, splits, true, functionHeight, true, true, etran); - var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes); - foreach (var s in splits) { - if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, currentModule)) { - AddEnsures(ens, EnsuresWithDependencies(s.Tok, false, p.E, s.E, errorMessage, successMessage, null)); - } - } - } - var proc = new Bpl.Procedure(f.tok, "CheckWellformed" + NameSeparator + f.FullSanitizedName, new List(), - Concat(Concat(typeInParams, inParams_Heap), inParams), outParams, - false, req, mod, ens, etran.TrAttributes(f.Attributes, null)); - AddVerboseNameAttribute(proc, f.FullDafnyName, MethodTranslationKind.SpecWellformedness); - sink.AddTopLevelDeclaration(proc); - - if (InsertChecksums) { - InsertChecksum(f, proc, true); - } - - Contract.Assert(proc.InParams.Count == typeInParams.Count + inParams_Heap.Count + inParams.Count); - // Changed the next line to strip from inParams instead of proc.InParams - // They should be the same, but hence the added contract - var implInParams = Bpl.Formal.StripWhereClauses(inParams); - var implOutParams = Bpl.Formal.StripWhereClauses(outParams); - var locals = new List(); - var builder = new BoogieStmtListBuilder(this, options); - var builderInitializationArea = new BoogieStmtListBuilder(this, options); - builder.Add(new CommentCmd("AddWellformednessCheck for function " + f)); - if (f is TwoStateFunction) { - // $Heap := current$Heap; - var heap = ordinaryEtran.HeapCastToIdentifierExpr; - builder.Add(Bpl.Cmd.SimpleAssign(f.tok, heap, etran.HeapExpr)); - etran = ordinaryEtran; // we no longer need the special heap names - } - builder.AddCaptureState(f.tok, false, "initial state"); - - DefineFrame(f.tok, etran.ReadsFrame(f.tok), f.Reads.Expressions, builder, locals, null); - InitializeFuelConstant(f.tok, builder, etran); - - var delayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, builder); - - // Check well-formedness of any default-value expressions (before assuming preconditions). - delayer.DoWithDelayedReadsChecks(true, wfo => { - foreach (var formal in f.Ins.Where(formal => formal.DefaultValue != null)) { - var e = formal.DefaultValue; - CheckWellformed(e, wfo, locals, builder, etran.WithReadsFrame(etran.readsFrame, null)); // No frame scope for default values - builder.Add(new Bpl.AssumeCmd(e.tok, etran.CanCallAssumption(e))); - CheckSubrange(e.tok, etran.TrExpr(e), e.Type, formal.Type, e, builder); - - if (formal.IsOld) { - Bpl.Expr wh = GetWhereClause(e.tok, etran.TrExpr(e), e.Type, etran.Old, ISALLOC, true); - if (wh != null) { - var desc = new PODesc.IsAllocated("default value", "in the two-state function's previous state", e); - builder.Add(Assert(GetToken(e), wh, desc)); - } - } - } - }); - - // Check well-formedness of the preconditions (including termination), and then - // assume each one of them. After all that (in particular, after assuming all - // of them), do the postponed reads checks. - delayer.DoWithDelayedReadsChecks(false, wfo => { - foreach (AttributedExpression p in f.Req) { - if (p.Label != null) { - p.Label.E = (f is TwoStateFunction ? ordinaryEtran : etran.Old).TrExpr(p.E); - CheckWellformed(p.E, wfo, locals, builder, etran); - } else { - CheckWellformedAndAssume(p.E, wfo, locals, builder, etran, "requires clause"); - } - } - }); - - // Check well-formedness of the reads clause. Note that this is done after assuming - // the preconditions. In other words, the well-formedness of the reads clause is - // allowed to assume the precondition (yet, the requires clause is checked to - // read only those things indicated in the reads clause). - delayer.DoWithDelayedReadsChecks(false, wfo => { - CheckFrameWellFormed(wfo, f.Reads.Expressions, locals, builder, etran); - }); - - // If the function is marked as {:concurrent}, check that the reads clause is empty. - if (Attributes.Contains(f.Attributes, Attributes.ConcurrentAttributeName)) { - var desc = new PODesc.ConcurrentFrameEmpty(f, "reads"); - CheckFrameEmpty(f.tok, etran, etran.ReadsFrame(f.tok), builder, desc, null); - } - - // check well-formedness of the decreases clauses (including termination, but no reads checks) - foreach (Expression p in f.Decreases.Expressions) { - CheckWellformed(p, new WFOptions(null, false), locals, builder, etran); - } - // Generate: - // if (*) { - // check well-formedness of postcondition - // assume false; // don't go on to check the postconditions - // } else { - // check well-formedness of body - // // fall through to check the postconditions themselves - // } - // Here go the postconditions (termination checks included, but no reads checks) - BoogieStmtListBuilder postCheckBuilder = new BoogieStmtListBuilder(this, options); - // Assume the type returned by the call itself respects its type (this matters if the type is "nat", for example) - { - var args = new List(); - foreach (var p in GetTypeParams(f)) { - args.Add(TrTypeParameter(p)); - } - if (f.IsFuelAware()) { - args.Add(etran.layerInterCluster.GetFunctionFuel(f)); - } - - if (f.IsOpaque || f.IsMadeImplicitlyOpaque(options)) { - args.Add(GetRevealConstant(f)); - } - if (f is TwoStateFunction) { - args.Add(etran.Old.HeapExpr); - } - if (f.ReadsHeap) { - args.Add(etran.HeapExpr); - } - if (!f.IsStatic) { - args.Add(new Bpl.IdentifierExpr(f.tok, etran.This)); - } - foreach (var p in f.Ins) { - args.Add(new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(f.IdGenerator), TrType(p.Type))); - } - Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)); - Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), args); - - var wh = GetWhereClause(f.tok, funcAppl, f.ResultType, etran, NOALLOC); - if (wh != null) { - postCheckBuilder.Add(TrAssumeCmd(f.tok, wh)); - } - } - // Now for the ensures clauses - foreach (AttributedExpression p in f.Ens) { - // assume the postcondition for the benefit of checking the remaining postconditions - CheckWellformedAndAssume(p.E, new WFOptions(f, false), locals, postCheckBuilder, etran, "ensures clause"); - } - // Here goes the body (and include both termination checks and reads checks) - BoogieStmtListBuilder bodyCheckBuilder = new BoogieStmtListBuilder(this, options); - if (f.Body == null || !RevealedInScope(f)) { - // don't fall through to postcondition checks - bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Bpl.Expr.False)); - } else { - var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType))); - var args = new List(); - foreach (var p in GetTypeParams(f)) { - args.Add(TrTypeParameter(p)); - } - if (f.IsFuelAware()) { - args.Add(etran.layerInterCluster.GetFunctionFuel(f)); - } - - if (f.IsOpaque || f.IsMadeImplicitlyOpaque(options)) { - args.Add(GetRevealConstant(f)); - } - if (f is TwoStateFunction) { - args.Add(etran.Old.HeapExpr); - } - if (f.ReadsHeap) { - args.Add(etran.HeapExpr); - } - foreach (Variable p in implInParams) { - args.Add(new Bpl.IdentifierExpr(f.tok, p)); - } - Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args); - - var bodyCheckDelayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, bodyCheckBuilder); - bodyCheckDelayer.DoWithDelayedReadsChecks(false, wfo => { - CheckWellformedWithResult(f.Body, wfo, funcAppl, f.ResultType, locals, bodyCheckBuilder, etran, "function call result"); - if (f.Result != null) { - var cmd = TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcAppl, TrVar(f.tok, f.Result))); - proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); - bodyCheckBuilder.Add(cmd); - } - }); - - // Enforce 'older' conditions - var (olderParameterCount, olderCondition) = OlderCondition(f, funcAppl, implInParams); - if (olderParameterCount != 0) { - bodyCheckBuilder.Add(Assert(f.tok, olderCondition, new PODesc.IsOlderProofObligation(olderParameterCount, f.Ins.Count + (f.IsStatic ? 0 : 1)))); - } - } - // Combine the two, letting the postcondition be checked on after the "bodyCheckBuilder" branch - postCheckBuilder.Add(TrAssumeCmd(f.tok, Bpl.Expr.False)); - builder.Add(new Bpl.IfCmd(f.tok, null, postCheckBuilder.Collect(f.tok), null, bodyCheckBuilder.Collect(f.tok))); - - var s0 = builderInitializationArea.Collect(f.tok); - var s1 = builder.Collect(f.tok); - var implBody = new StmtList(new List(s0.BigBlocks.Concat(s1.BigBlocks)), f.tok); - - if (EmitImplementation(f.Attributes)) { - // emit the impl only when there are proof obligations. - QKeyValue kv = etran.TrAttributes(f.Attributes, null); - var impl = AddImplementationWithAttributes(GetToken(f), proc, - Concat(Concat(Bpl.Formal.StripWhereClauses(typeInParams), inParams_Heap), implInParams), - implOutParams, - locals, implBody, kv); - if (InsertChecksums) { - InsertChecksum(f, impl); - } - } - - Contract.Assert(currentModule == f.EnclosingClass.EnclosingModuleDefinition); - Contract.Assert(codeContext == f); - Reset(); - } void AddFunctionAxiom(Bpl.Function boogieFunction, Function f, Expression body) { Contract.Requires(f != null); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index 8bd75fda710..f537becf2dc 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -148,7 +148,7 @@ void AddFunction_Top(Function f, bool includeAllMethods) { AddClassMember_Function(f); if (InVerificationScope(f)) { - AddWellformednessCheck(f); + new FunctionWellformednessChecker(this).Check(f); if (f.OverriddenFunction != null) { //it means that f is overriding its associated parent function AddFunctionOverrideCheckImpl(f); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 52e95ec4edb..25c7d142853 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -497,28 +497,8 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List { bIe })); - Bpl.Expr wh = GetWhereClause(local.Tok, bIe, local.Type, etran, isAllocContext.Var(stmt.IsGhost, local)); - if (wh != null) { - builder.Add(TrAssumeCmd(local.Tok, wh)); - } - } - var varNameGen = CurrentIdGenerator.NestedFreshIdGenerator("let#"); - var pat = s.LHS; - var rhs = s.RHS; - var nm = varNameGen.FreshId(string.Format("#{0}#", 0)); - var r = new Bpl.LocalVariable(pat.tok, new Bpl.TypedIdent(pat.tok, nm, TrType(rhs.Type))); - locals.Add(r); - var rIe = new Bpl.IdentifierExpr(rhs.tok, r); - CheckWellformedWithResult(rhs, new WFOptions(null, false, false), rIe, pat.Expr.Type, locals, builder, etran, "variable declaration RHS"); - CheckCasePatternShape(pat, rhs, rIe, rhs.tok, pat.Expr.Type, builder); - builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, s.tok, pat.Expr, e => Expr.Eq(e, rIe), "variable declaration")); + } else if (stmt is VarDeclPattern varDeclPattern) { + TranslateVariableDeclaration(builder, locals, etran, varDeclPattern); } else if (stmt is TryRecoverStatement haltRecoveryStatement) { // try/recover statements are currently internal-only AST nodes that cannot be // directly used in user Dafny code. They are only generated by rewriters, and verifying @@ -529,6 +509,31 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, + VarDeclPattern varDeclPattern) + { + foreach (var dafnyLocal in varDeclPattern.LocalVars) { + var boogieLocal = new Bpl.LocalVariable(dafnyLocal.Tok, new Bpl.TypedIdent(dafnyLocal.Tok, dafnyLocal.AssignUniqueName(currentDeclaration.IdGenerator), TrType(dafnyLocal.Type))); + locals.Add(boogieLocal); + var variableReference = new Bpl.IdentifierExpr(boogieLocal.tok, boogieLocal); + builder.Add(new Bpl.HavocCmd(dafnyLocal.Tok, new List { variableReference })); + var wh = GetWhereClause(dafnyLocal.Tok, variableReference, dafnyLocal.Type, etran, isAllocContext.Var(varDeclPattern.IsGhost, dafnyLocal)); + if (wh != null) { + builder.Add(TrAssumeCmd(dafnyLocal.Tok, wh)); + } + } + var varNameGen = CurrentIdGenerator.NestedFreshIdGenerator("let#"); + var pat = varDeclPattern.LHS; + var rhs = varDeclPattern.RHS; + var nm = varNameGen.FreshId("#0#"); + var boogieTupleLocal = new Bpl.LocalVariable(pat.tok, new TypedIdent(pat.tok, nm, TrType(rhs.Type))); + locals.Add(boogieTupleLocal); + var boogieTupleReference = new Bpl.IdentifierExpr(rhs.tok, boogieTupleLocal); + CheckWellformedWithResult(rhs, new WFOptions(null, false, false), boogieTupleReference, pat.Expr.Type, locals, builder, etran, "variable declaration RHS"); + CheckCasePatternShape(pat, rhs, boogieTupleReference, rhs.tok, pat.Expr.Type, builder); + builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, varDeclPattern.tok, pat.Expr, e => Expr.Eq(e, boogieTupleReference), "variable declaration")); + } + private void TrCalcStmt(CalcStmt stmt, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran) { Contract.Requires(stmt != null); Contract.Requires(builder != null); From eae6238aa1c94b0b2ec1f0a26adad4a8cf8ce1ec Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 Jul 2024 18:29:55 +0200 Subject: [PATCH 05/32] Refactoring --- ...oogieGenerator.Functions.Wellformedness.cs | 321 ++++++++++-------- 1 file changed, 182 insertions(+), 139 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index 81b42013a70..ac26ff06192 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -1,4 +1,5 @@ using System.Collections.Generic; +using System.Collections.Immutable; using System.Diagnostics.Contracts; using System.Linq; using DafnyCore.Verifier; @@ -26,29 +27,16 @@ public void Check(Function f) { generator.currentModule = f.EnclosingClass.EnclosingModuleDefinition; generator.codeContext = f; - Expr prevHeap = null; - Expr currHeap = null; - var ordinaryEtran = new ExpressionTranslator(generator, generator.predef, f.tok, f); - ExpressionTranslator etran; - var inParams_Heap = new List(); - if (f is TwoStateFunction) { - var prevHeapVar = new Bpl.Formal(f.tok, new TypedIdent(f.tok, "previous$Heap", generator.predef.HeapType), true); - var currHeapVar = new Bpl.Formal(f.tok, new TypedIdent(f.tok, "current$Heap", generator.predef.HeapType), true); - inParams_Heap.Add(prevHeapVar); - inParams_Heap.Add(currHeapVar); - prevHeap = new Bpl.IdentifierExpr(f.tok, prevHeapVar); - currHeap = new Bpl.IdentifierExpr(f.tok, currHeapVar); - etran = new ExpressionTranslator(generator, generator.predef, currHeap, prevHeap, f); - } else { - etran = ordinaryEtran; - } + ExpressionTranslator ordinaryEtran = new ExpressionTranslator(generator, generator.predef, f.tok, f); + var etran = GetExpressionTranslator(f, ordinaryEtran, out var additionalRequires, out var heapParameters); // parameters of the procedure var typeInParams = generator.MkTyParamFormals(GetTypeParams(f), true); - var inParams = GetParameters(f, etran); + var procedureParameters = GetParameters(f, etran); var outParams = GetWellformednessProcedureOutParameters(f, etran); - var requires = GetWellformednessProcedureRequires(f, etran, prevHeap, ordinaryEtran, currHeap); - + var requires = GetWellformednessProcedureRequires(f, etran); + requires.AddRange(additionalRequires); + // modifies $Heap var mod = new List { ordinaryEtran.HeapCastToIdentifierExpr, @@ -57,7 +45,7 @@ public void Check(Function f) { var proc = new Procedure(f.tok, "CheckWellformed" + NameSeparator + f.FullSanitizedName, new List(), - Concat(Concat(typeInParams, inParams_Heap), inParams), outParams, + Concat(Concat(typeInParams, heapParameters), procedureParameters), outParams, false, requires, mod, ensures, etran.TrAttributes(f.Attributes, null)); AddVerboseNameAttribute(proc, f.FullDafnyName, MethodTranslationKind.SpecWellformedness); generator.sink.AddTopLevelDeclaration(proc); @@ -66,15 +54,12 @@ public void Check(Function f) { generator.InsertChecksum(f, proc, true); } - Contract.Assert(proc.InParams.Count == typeInParams.Count + inParams_Heap.Count + inParams.Count); + Contract.Assert(proc.InParams.Count == typeInParams.Count + heapParameters.Count + procedureParameters.Count); // Changed the next line to strip from inParams instead of proc.InParams // They should be the same, but hence the added contract - var implInParams = Bpl.Formal.StripWhereClauses(inParams); - var implOutParams = Bpl.Formal.StripWhereClauses(outParams); var locals = new List(); var builder = new BoogieStmtListBuilder(generator, generator.options); var builderInitializationArea = new BoogieStmtListBuilder(generator, generator.options); - builder.Add(new CommentCmd("AddWellformednessCheck for function " + f)); if (f is TwoStateFunction) { // $Heap := current$Heap; var heap = ordinaryEtran.HeapCastToIdentifierExpr; @@ -112,12 +97,13 @@ public void Check(Function f) { // assume each one of them. After all that (in particular, after assuming all // of them), do the postponed reads checks. delayer.DoWithDelayedReadsChecks(false, wfo => { - foreach (AttributedExpression p in f.Req) { - if (p.Label != null) { - p.Label.E = (f is TwoStateFunction ? ordinaryEtran : etran.Old).TrExpr(p.E); - generator.CheckWellformed(p.E, wfo, locals, builder, etran); + builder.Add(new CommentCmd("Check Wfness of preconditions, and then assume them")); + foreach (AttributedExpression require in f.Req) { + if (require.Label != null) { + require.Label.E = (f is TwoStateFunction ? ordinaryEtran : etran.Old).TrExpr(require.E); + generator.CheckWellformed(require.E, wfo, locals, builder, etran); } else { - generator.CheckWellformedAndAssume(p.E, wfo, locals, builder, etran, "requires clause"); + generator.CheckWellformedAndAssume(require.E, wfo, locals, builder, etran, "requires clause"); } } }); @@ -126,20 +112,57 @@ public void Check(Function f) { // the preconditions. In other words, the well-formedness of the reads clause is // allowed to assume the precondition (yet, the requires clause is checked to // read only those things indicated in the reads clause). + builder.Add(new CommentCmd("Check Wfness of the reads clause")); delayer.DoWithDelayedReadsChecks(false, wfo => { generator.CheckFrameWellFormed(wfo, f.Reads.Expressions, locals, builder, etran); }); - // If the function is marked as {:concurrent}, check that the reads clause is empty. - if (Attributes.Contains(f.Attributes, Attributes.ConcurrentAttributeName)) { - var desc = new PODesc.ConcurrentFrameEmpty(f, "reads"); - generator.CheckFrameEmpty(f.tok, etran, etran.ReadsFrame(f.tok), builder, desc, null); - } + ConcurrentAttributeCheck(f, etran, builder); // check well-formedness of the decreases clauses (including termination, but no reads checks) + builder.Add(new CommentCmd("Check Wfness of the decreases clause")); foreach (Expression p in f.Decreases.Expressions) { generator.CheckWellformed(p, new WFOptions(null, false), locals, builder, etran); } + + var implementationParameters = Bpl.Formal.StripWhereClauses(procedureParameters); + CheckBodyAndEnsuresClauses(f, etran, locals, implementationParameters, builderInitializationArea, builder); + + if (generator.EmitImplementation(f.Attributes)) { + var s0 = builderInitializationArea.Collect(f.tok); + var s1 = builder.Collect(f.tok); + var implBody = new StmtList(new List(s0.BigBlocks.Concat(s1.BigBlocks)), f.tok); + + // emit the impl only when there are proof obligations. + QKeyValue kv = etran.TrAttributes(f.Attributes, null); + var parameters = Concat(Concat(Bpl.Formal.StripWhereClauses(typeInParams), heapParameters), implementationParameters); + var impl = generator.AddImplementationWithAttributes(generator.GetToken(f), proc, + parameters, + Bpl.Formal.StripWhereClauses(outParams), + locals, implBody, kv); + if (generator.InsertChecksums) { + generator.InsertChecksum(f, impl); + } + } + + Contract.Assert(generator.currentModule == f.EnclosingClass.EnclosingModuleDefinition); + Contract.Assert(generator.codeContext == f); + generator.Reset(); + } + // TODO should be moved so its injected + private void ConcurrentAttributeCheck(Function f, ExpressionTranslator etran, BoogieStmtListBuilder builder) + { + // If the function is marked as {:concurrent}, check that the reads clause is empty. + if (Attributes.Contains(f.Attributes, Attributes.ConcurrentAttributeName)) { + var desc = new PODesc.ConcurrentFrameEmpty(f, "reads"); + generator.CheckFrameEmpty(f.tok, etran, etran.ReadsFrame(f.tok), builder, desc, null); + } + } + + private void CheckBodyAndEnsuresClauses(Function f, ExpressionTranslator etran, List locals, List inParams, + BoogieStmtListBuilder builderInitializationArea, BoogieStmtListBuilder builder) + { + builder.Add(new CommentCmd("Check body and ensures clauses")); // Generate: // if (*) { // check well-formedness of postcondition @@ -149,128 +172,157 @@ public void Check(Function f) { // // fall through to check the postconditions themselves // } // Here go the postconditions (termination checks included, but no reads checks) - BoogieStmtListBuilder postCheckBuilder = new BoogieStmtListBuilder(generator, generator.options); - // Assume the type returned by the call itself respects its type (this matters if the type is "nat", for example) - { - var args = new List(); - foreach (var p in GetTypeParams(f)) { - args.Add(generator.TrTypeParameter(p)); - } + var postCheckBuilder = GetPostCheckBuilder(f, etran, locals); - if (f.IsFuelAware()) { - args.Add(etran.layerInterCluster.GetFunctionFuel(f)); - } - - if (f.IsOpaque || f.IsMadeImplicitlyOpaque(generator.options)) { - args.Add(generator.GetRevealConstant(f)); - } - - if (f is TwoStateFunction) { - args.Add(etran.Old.HeapExpr); - } - - if (f.ReadsHeap) { - args.Add(etran.HeapExpr); - } - - if (!f.IsStatic) { - args.Add(new Bpl.IdentifierExpr(f.tok, etran.This)); - } - - foreach (var p in f.Ins) { - args.Add(new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(f.IdGenerator), generator.TrType(p.Type))); - } - - Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, generator.TrType(f.ResultType)); - Expr funcAppl = new NAryExpr(f.tok, new FunctionCall(funcID), args); + // Here goes the body (and include both termination checks and reads checks) + var bodyCheckBuilder = GetBodyCheckBuilder(f, etran, inParams, locals, builderInitializationArea); - var wh = generator.GetWhereClause(f.tok, funcAppl, f.ResultType, etran, NOALLOC); - if (wh != null) { - postCheckBuilder.Add(TrAssumeCmd(f.tok, wh)); - } - } - // Now for the ensures clauses - foreach (AttributedExpression p in f.Ens) { - // assume the postcondition for the benefit of checking the remaining postconditions - generator.CheckWellformedAndAssume(p.E, new WFOptions(f, false), locals, postCheckBuilder, etran, "ensures clause"); - } + // Combine the two, letting the postcondition be checked on after the "bodyCheckBuilder" branch + builder.Add(new IfCmd(f.tok, null, postCheckBuilder.Collect(f.tok), null, bodyCheckBuilder.Collect(f.tok))); + } - // Here goes the body (and include both termination checks and reads checks) - BoogieStmtListBuilder bodyCheckBuilder = new BoogieStmtListBuilder(generator, generator.options); + private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslator etran, + List parameters, + List locals, BoogieStmtListBuilder builderInitializationArea) + { + var selfCall = GetSelfCall(f, etran, parameters); + var bodyCheckBuilder = new BoogieStmtListBuilder(generator, generator.options); + bodyCheckBuilder.Add(new CommentCmd("Check Wfness of body, result subset type constraint, and return to check the postcondition")); if (f.Body == null || !generator.RevealedInScope(f)) { // don't fall through to postcondition checks bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Expr.False)); } else { - var funcID = new FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, generator.TrType(f.ResultType))); - var args = new List(); - foreach (var p in GetTypeParams(f)) { - args.Add(generator.TrTypeParameter(p)); - } - - if (f.IsFuelAware()) { - args.Add(etran.layerInterCluster.GetFunctionFuel(f)); - } - - if (f.IsOpaque || f.IsMadeImplicitlyOpaque(generator.options)) { - args.Add(generator.GetRevealConstant(f)); - } - - if (f is TwoStateFunction) { - args.Add(etran.Old.HeapExpr); - } - - if (f.ReadsHeap) { - args.Add(etran.HeapExpr); - } - - foreach (Variable p in implInParams) { - args.Add(new Bpl.IdentifierExpr(f.tok, p)); - } - - Expr funcAppl = new NAryExpr(f.tok, funcID, args); - var bodyCheckDelayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, bodyCheckBuilder); bodyCheckDelayer.DoWithDelayedReadsChecks(false, wfo => { - generator.CheckWellformedWithResult(f.Body, wfo, funcAppl, f.ResultType, locals, bodyCheckBuilder, etran, + generator.CheckWellformedWithResult(f.Body, wfo, selfCall, f.ResultType, locals, bodyCheckBuilder, etran, "function call result"); if (f.Result != null) { - var cmd = TrAssumeCmd(f.tok, Expr.Eq(funcAppl, generator.TrVar(f.tok, f.Result))); + var cmd = TrAssumeCmd(f.tok, Expr.Eq(selfCall, generator.TrVar(f.tok, f.Result))); generator.proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); bodyCheckBuilder.Add(cmd); } }); // Enforce 'older' conditions - var (olderParameterCount, olderCondition) = generator.OlderCondition(f, funcAppl, implInParams); + var (olderParameterCount, olderCondition) = generator.OlderCondition(f, selfCall, parameters); if (olderParameterCount != 0) { bodyCheckBuilder.Add(generator.Assert(f.tok, olderCondition, new PODesc.IsOlderProofObligation(olderParameterCount, f.Ins.Count + (f.IsStatic ? 0 : 1)))); } } - // Combine the two, letting the postcondition be checked on after the "bodyCheckBuilder" branch - postCheckBuilder.Add(TrAssumeCmd(f.tok, Expr.False)); - builder.Add(new IfCmd(f.tok, null, postCheckBuilder.Collect(f.tok), null, bodyCheckBuilder.Collect(f.tok))); + return bodyCheckBuilder; + } - var s0 = builderInitializationArea.Collect(f.tok); - var s1 = builder.Collect(f.tok); - var implBody = new StmtList(new List(s0.BigBlocks.Concat(s1.BigBlocks)), f.tok); + private Expr GetSelfCall(Function f, ExpressionTranslator etran, List parameters) + { + var funcId = new FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, generator.TrType(f.ResultType))); + var args = new List(); + foreach (var p in GetTypeParams(f)) { + args.Add(generator.TrTypeParameter(p)); + } - if (generator.EmitImplementation(f.Attributes)) { - // emit the impl only when there are proof obligations. - QKeyValue kv = etran.TrAttributes(f.Attributes, null); - var impl = generator.AddImplementationWithAttributes(generator.GetToken(f), proc, - Concat(Concat(Bpl.Formal.StripWhereClauses(typeInParams), inParams_Heap), implInParams), - implOutParams, - locals, implBody, kv); - if (generator.InsertChecksums) { - generator.InsertChecksum(f, impl); - } + if (f.IsFuelAware()) { + args.Add(etran.layerInterCluster.GetFunctionFuel(f)); } - Contract.Assert(generator.currentModule == f.EnclosingClass.EnclosingModuleDefinition); - Contract.Assert(generator.codeContext == f); - generator.Reset(); + if (f.IsOpaque || f.IsMadeImplicitlyOpaque(generator.options)) { + args.Add(generator.GetRevealConstant(f)); + } + + if (f is TwoStateFunction) { + args.Add(etran.Old.HeapExpr); + } + + if (f.ReadsHeap) { + args.Add(etran.HeapExpr); + } + + foreach (Variable parameter in parameters) { + args.Add(new Bpl.IdentifierExpr(f.tok, parameter)); + } + + Expr funcAppl = new NAryExpr(f.tok, funcId, args); + return funcAppl; + } + + private BoogieStmtListBuilder GetPostCheckBuilder(Function f, ExpressionTranslator etran, List locals) + { + var postCheckBuilder = new BoogieStmtListBuilder(generator, generator.options); + postCheckBuilder.Add(new CommentCmd("Check Wfness of postcondition and assume false")); + + // Assume the type returned by the call itself respects its type (this matters if the type is "nat", for example) + var args = new List(); + foreach (var p in GetTypeParams(f)) { + args.Add(generator.TrTypeParameter(p)); + } + + if (f.IsFuelAware()) { + args.Add(etran.layerInterCluster.GetFunctionFuel(f)); + } + + if (f.IsOpaque || f.IsMadeImplicitlyOpaque(generator.options)) { + args.Add(generator.GetRevealConstant(f)); + } + + if (f is TwoStateFunction) { + args.Add(etran.Old.HeapExpr); + } + + if (f.ReadsHeap) { + args.Add(etran.HeapExpr); + } + + if (!f.IsStatic) { + args.Add(new Bpl.IdentifierExpr(f.tok, etran.This)); + } + + foreach (var p in f.Ins) { + args.Add(new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(f.IdGenerator), generator.TrType(p.Type))); + } + + Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, generator.TrType(f.ResultType)); + Expr funcAppl = new NAryExpr(f.tok, new FunctionCall(funcID), args); + + var wh = generator.GetWhereClause(f.tok, funcAppl, f.ResultType, etran, NOALLOC); + if (wh != null) { + postCheckBuilder.Add(TrAssumeCmd(f.tok, wh)); + } + // Now for the ensures clauses + foreach (AttributedExpression p in f.Ens) { + // assume the postcondition for the benefit of checking the remaining postconditions + generator.CheckWellformedAndAssume(p.E, new WFOptions(f, false), locals, postCheckBuilder, etran, "ensures clause"); + } + + postCheckBuilder.Add(TrAssumeCmd(f.tok, Expr.False)); + return postCheckBuilder; + } + + private ExpressionTranslator GetExpressionTranslator(Function f, ExpressionTranslator ordinaryEtran, + out List additionalRequires, out List inParams_Heap) + { + ExpressionTranslator etran; + additionalRequires = new(); + inParams_Heap = new List(); + if (f is TwoStateFunction) { + var prevHeapVar = new Bpl.Formal(f.tok, new TypedIdent(f.tok, "previous$Heap", generator.predef.HeapType), true); + var currHeapVar = new Bpl.Formal(f.tok, new TypedIdent(f.tok, "current$Heap", generator.predef.HeapType), true); + inParams_Heap.Add(prevHeapVar); + inParams_Heap.Add(currHeapVar); + Expr prevHeap = new Bpl.IdentifierExpr(f.tok, prevHeapVar); + Expr currHeap = new Bpl.IdentifierExpr(f.tok, currHeapVar); + etran = new ExpressionTranslator(generator, generator.predef, currHeap, prevHeap, f); + + // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) + var a0 = Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); + var a1 = generator.HeapSucc(prevHeap, currHeap); + var a2 = generator.FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, currHeap); + additionalRequires.Add(generator.Requires(f.tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null)); + } else { + etran = ordinaryEtran; + } + + return etran; } private List GetWellformednessProcedureOutParameters(Function f, ExpressionTranslator etran) { @@ -306,19 +358,10 @@ private List GetWellformnessProcedureEnsures(Function f, ExpressionTran return ens; } - private List GetWellformednessProcedureRequires(Function f, ExpressionTranslator etran, - Expr prevHeap, - ExpressionTranslator ordinaryEtran, Expr currHeap) { + private List GetWellformednessProcedureRequires(Function f, ExpressionTranslator etran) { var requires = new List(); // free requires mh == ModuleContextHeight && fh == FunctionContextHeight; requires.Add(generator.Requires(f.tok, true, null, etran.HeightContext(f), null, null, null)); - if (f is TwoStateFunction) { - // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) - var a0 = Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); - var a1 = generator.HeapSucc(prevHeap, currHeap); - var a2 = generator.FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, currHeap); - requires.Add(generator.Requires(f.tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null)); - } foreach (var typeBoundAxiom in generator.TypeBoundAxioms(f.tok, Concat(f.EnclosingClass.TypeArgs, f.TypeArgs))) { requires.Add(generator.Requires(f.tok, true, null, typeBoundAxiom, null, null, null)); From 3e142d9435ab24b691196baefe3919c2bd43a825 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 Jul 2024 22:36:05 +0200 Subject: [PATCH 06/32] Add test --- .../LitTest/ast/expressions/statementExpressionScope.dfy | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy index c420b478a94..0fed01f610c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy @@ -13,6 +13,12 @@ function StatementExpressionAssumeAndFunctionEnsures(): int assume false; 10 } +function StatementExpressionAssumeAndFunctionEnsures(): int + ensures 10 == 11 // error, since the assume false does not leak +{ + var x := (assume false; 10); x +} + function StatementExpressionAndSubsetResult(): nat // no error, since the statement expression can be used for the return type subset constraint { From 2c93cf48f3021e08b3ef096c7cd12432b83c0016 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 Jul 2024 22:39:55 +0200 Subject: [PATCH 07/32] Move function ensures clause check from procedure ensures clause to implementation assertion --- ...oogieGenerator.Functions.Wellformedness.cs | 35 ++++++++----------- 1 file changed, 15 insertions(+), 20 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index ac26ff06192..a344b9120a4 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -41,12 +41,11 @@ public void Check(Function f) { var mod = new List { ordinaryEtran.HeapCastToIdentifierExpr, }; - var ensures = GetWellformnessProcedureEnsures(f, etran); var proc = new Procedure(f.tok, "CheckWellformed" + NameSeparator + f.FullSanitizedName, new List(), Concat(Concat(typeInParams, heapParameters), procedureParameters), outParams, - false, requires, mod, ensures, etran.TrAttributes(f.Attributes, null)); + false, requires, mod, new List(), etran.TrAttributes(f.Attributes, null)); AddVerboseNameAttribute(proc, f.FullDafnyName, MethodTranslationKind.SpecWellformedness); generator.sink.AddTopLevelDeclaration(proc); @@ -202,6 +201,20 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat bodyCheckBuilder.Add(cmd); } }); + + foreach (AttributedExpression e in f.Ens) { + var functionHeight = generator.currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); + var splits = new List(); + bool splitHappened /*we actually don't care*/ = + generator.TrSplitExpr(e.E, splits, true, functionHeight, true, true, etran); + var (errorMessage, successMessage) = generator.CustomErrorMessage(e.Attributes); + foreach (var s in splits) { + if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, generator.currentModule)) { + var ensures = generator.EnsuresWithDependencies(s.Tok, false, e.E, s.E, errorMessage, successMessage, null); + bodyCheckBuilder.Add(new AssertCmd(ensures.tok, ensures.Condition, ensures.Description, ensures.Attributes)); + } + } + } // Enforce 'older' conditions var (olderParameterCount, olderCondition) = generator.OlderCondition(f, selfCall, parameters); @@ -340,24 +353,6 @@ private List GetWellformednessProcedureOutParameters(Function f, Expre return outParams; } - private List GetWellformnessProcedureEnsures(Function f, ExpressionTranslator etran) { - var ens = new List(); - foreach (AttributedExpression p in f.Ens) { - var functionHeight = generator.currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); - var splits = new List(); - bool splitHappened /*we actually don't care*/ = - generator.TrSplitExpr(p.E, splits, true, functionHeight, true, true, etran); - var (errorMessage, successMessage) = generator.CustomErrorMessage(p.Attributes); - foreach (var s in splits) { - if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, generator.currentModule)) { - generator.AddEnsures(ens, generator.EnsuresWithDependencies(s.Tok, false, p.E, s.E, errorMessage, successMessage, null)); - } - } - } - - return ens; - } - private List GetWellformednessProcedureRequires(Function f, ExpressionTranslator etran) { var requires = new List(); // free requires mh == ModuleContextHeight && fh == FunctionContextHeight; From c6c2bc397437e5eceb8d91e1000104f43e05c396 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 Jul 2024 23:01:33 +0200 Subject: [PATCH 08/32] Prepare for injecting the function postcondition into the StmtExpr PathAsideBlock --- .../BoogieGenerator.ExpressionWellformed.cs | 81 ++++++++++--------- ...oogieGenerator.Functions.Wellformedness.cs | 8 +- .../Verifier/BoogieGenerator.TrStatement.cs | 6 +- .../Verifier/BoogieStmtListBuilder.cs | 2 +- 4 files changed, 56 insertions(+), 41 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 917aee73bf9..01f812e4256 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -251,7 +251,7 @@ void CheckWellformed(Expression expr, WFOptions options, List locals, Contract.Requires(builder != null); Contract.Requires(etran != null); Contract.Requires(predef != null); - CheckWellformedWithResult(expr, options, null, null, locals, builder, etran); + CheckWellformedWithResult(expr, options, null, locals, builder, etran); } /// @@ -261,12 +261,11 @@ void CheckWellformed(Expression expr, WFOptions options, List locals, /// assume the equivalent of "result == expr". /// See class WFOptions for descriptions of the specified options. /// - void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr result, Type resultType, - List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, - string resultDescription = null) { + void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, + Action checkPostcondition, + List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { Contract.Requires(expr != null); Contract.Requires(wfOptions != null); - Contract.Requires((result == null) == (resultType == null)); Contract.Requires(locals != null); Contract.Requires(builder != null); Contract.Requires(etran != null); @@ -283,7 +282,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re switch (expr) { case StaticReceiverExpr stexpr: { if (stexpr.ObjectToDiscard != null) { - CheckWellformedWithResult(stexpr.ObjectToDiscard, wfOptions, null, null, locals, builder, etran); + CheckWellformedWithResult(stexpr.ObjectToDiscard, wfOptions, null, locals, builder, etran); } break; @@ -1135,8 +1134,8 @@ void CheckOperand(Expression operand) { break; } case LetExpr letExpr: - CheckWellformedLetExprWithResult(letExpr, wfOptions, result, resultType, locals, builder, etran, true); - result = null; + CheckWellformedLetExprWithResult(letExpr, wfOptions, checkPostcondition, resultType, locals, builder, etran, true); + checkPostcondition = null; break; case ComprehensionExpr comprehensionExpr: { var e = comprehensionExpr; @@ -1211,7 +1210,7 @@ void CheckOperand(Expression operand) { resultIe = new Bpl.IdentifierExpr(body.tok, resultVar); rangeType = lam.Type.AsArrowType.Result; } - CheckWellformedWithResult(body, newOptions, resultIe, rangeType, locals, b, comprehensionEtran, "lambda expression"); + CheckWellformedWithResult(body, newOptions, resultIe, locals, b, comprehensionEtran); }); if (mc != null) { @@ -1262,8 +1261,10 @@ void CheckOperand(Expression operand) { break; } case StmtExpr stmtExpr: - CheckWellformedStmtExpr(stmtExpr, wfOptions, result, resultType, locals, builder, etran); - result = null; + var bodyBuilder = new BoogieStmtListBuilder(this, builder.Options); + PathAsideBlock(stmtExpr.tok, bodyBuilder, builder); + CheckWellformedStmtExpr(stmtExpr, wfOptions, checkPostcondition, locals, bodyBuilder, etran); + checkPostcondition = null; break; case ITEExpr iteExpr: { ITEExpr e = iteExpr; @@ -1276,17 +1277,17 @@ void CheckOperand(Expression operand) { // has already been checked in e.Test var letExpr = (LetExpr)e.Thn; Contract.Assert(letExpr != null); - CheckWellformedLetExprWithResult(letExpr, wfOptions, result, resultType, locals, bThen, etran, false); + CheckWellformedLetExprWithResult(letExpr, wfOptions, checkPostcondition, resultType, locals, bThen, etran, false); } else { - CheckWellformedWithResult(e.Thn, wfOptions, result, resultType, locals, bThen, etran, "if expression then branch"); + CheckWellformedWithResult(e.Thn, wfOptions, checkPostcondition, locals, bThen, etran); } - CheckWellformedWithResult(e.Els, wfOptions, result, resultType, locals, bElse, etran, "if expression else branch"); + CheckWellformedWithResult(e.Els, wfOptions, checkPostcondition, locals, bElse, etran); builder.Add(new Bpl.IfCmd(iteExpr.tok, etran.TrExpr(e.Test), bThen.Collect(iteExpr.tok), null, bElse.Collect(iteExpr.tok))); - result = null; + checkPostcondition = null; break; } case MatchExpr matchExpr: - result = TrMatchExpr(matchExpr, wfOptions, result, resultType, locals, builder, etran); + checkPostcondition = TrMatchExpr(matchExpr, wfOptions, checkPostcondition, resultType, locals, builder, etran); resultDescription = "match expression"; break; case DatatypeUpdateExpr updateExpr: { @@ -1304,19 +1305,19 @@ void CheckOperand(Expression operand) { CheckNotGhostVariant(e.InCompiledContext, updateExpr, e.Root, "update of", e.Members, e.LegalSourceConstructors, builder, etran); - CheckWellformedWithResult(e.ResolvedExpression, wfOptions, result, resultType, locals, builder, etran, resultDescription); - result = null; + CheckWellformedWithResult(e.ResolvedExpression, wfOptions, checkPostcondition, locals, builder, etran); + checkPostcondition = null; break; } case ConcreteSyntaxExpression expression: { var e = expression; - CheckWellformedWithResult(e.ResolvedExpression, wfOptions, result, resultType, locals, builder, etran, resultDescription); - result = null; + CheckWellformedWithResult(e.ResolvedExpression, wfOptions, checkPostcondition, locals, builder, etran); + checkPostcondition = null; break; } case NestedMatchExpr nestedMatchExpr: - CheckWellformedWithResult(nestedMatchExpr.Flattened, wfOptions, result, resultType, locals, builder, etran, resultDescription); - result = null; + CheckWellformedWithResult(nestedMatchExpr.Flattened, wfOptions, checkPostcondition, locals, builder, etran); + checkPostcondition = null; break; case BoogieFunctionCall call: { var e = call; @@ -1337,19 +1338,25 @@ void CheckOperand(Expression operand) { } - if (result != null) { - Contract.Assert(resultType != null); - var bResult = etran.TrExpr(expr); - CheckSubrange(expr.tok, bResult, expr.Type, resultType, expr, builder); - builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, expr.tok, expr, - e => Bpl.Expr.Eq(result, AdaptBoxing(expr.tok, e, expr.Type, resultType)), - resultDescription)); - builder.Add(TrAssumeCmd(expr.tok, etran.CanCallAssumption(expr))); - builder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); - builder.Add(TrAssumeCmd(expr.tok, MkIs(result, resultType))); + if (checkPostcondition != null) { + checkPostcondition(builder); } } + public void CheckSubsetType(ExpressionTranslator etran, Expression expr, Bpl.Expr selfCall, Type resultType, + BoogieStmtListBuilder builder, string resultDescription = null) { + + Contract.Assert(resultType != null); + var bResult = etran.TrExpr(expr); + CheckSubrange(expr.tok, bResult, expr.Type, resultType, expr, builder); + builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, expr.tok, expr, + e => Bpl.Expr.Eq(selfCall, AdaptBoxing(expr.tok, e, expr.Type, resultType)), + resultDescription)); + builder.Add(TrAssumeCmd(expr.tok, etran.CanCallAssumption(expr))); + builder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); + builder.Add(TrAssumeCmd(expr.tok, MkIs(selfCall, resultType))); + } + private Expr TrMatchExpr(MatchExpr me, WFOptions wfOptions, Expr result, Type resultType, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { FillMissingCases(me); @@ -1389,7 +1396,7 @@ private Expr TrMatchExpr(MatchExpr me, WFOptions wfOptions, Expr result, Type re BoogieStmtListBuilder b = new BoogieStmtListBuilder(this, options); Bpl.Expr ct = CtorInvocation(mc, me.Source.Type, etran, locals, b, NOALLOC, false); // generate: if (src == ctor(args)) { assume args-is-well-typed; mc.Body is well-formed; assume Result == TrExpr(case); } else ... - CheckWellformedWithResult(mc.Body, wfOptions, result, resultType, locals, b, etran, "match expression branch result"); + CheckWellformedWithResult(mc.Body, wfOptions, result, locals, b, etran); ifCmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifCmd, els); els = null; } @@ -1399,7 +1406,7 @@ private Expr TrMatchExpr(MatchExpr me, WFOptions wfOptions, Expr result, Type re return result; } - private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions options, Expr result, Type resultType, List locals, + private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions options, Action checkPostcondition, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { // If we're inside an "old" expression, then "etran" will know how to translate // expressions. However, here, we're also having to translate e.S, which is a @@ -1412,7 +1419,7 @@ private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions options, Expr TrStmt(stmtExpr.S, builder, locals, etran); } - CheckWellformedWithResult(stmtExpr.E, options, result, resultType, locals, builder, etran, "statement expression result"); + CheckWellformedWithResult(stmtExpr.E, options, checkPostcondition, locals, builder, etran); } /// @@ -1496,12 +1503,12 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r var r = new Bpl.LocalVariable(pat.tok, new Bpl.TypedIdent(pat.tok, nm, TrType(pat.Expr.Type))); locals.Add(r); var rIe = new Bpl.IdentifierExpr(rhs.tok, r); - CheckWellformedWithResult(e.RHSs[i], wfOptions, rIe, pat.Expr.Type, locals, builder, etran, "let expression binding RHS well-formed"); + CheckWellformedWithResult(e.RHSs[i], wfOptions, rIe, locals, builder, etran); CheckCasePatternShape(pat, rhs, rIe, rhs.tok, pat.Expr.Type, builder); var substExpr = Substitute(pat.Expr, null, substMap); builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, e.tok, substExpr, e => Bpl.Expr.Eq(e, rIe), "let expression binding")); } - CheckWellformedWithResult(Substitute(e.Body, null, substMap), wfOptions, result, resultType, locals, builder, etran, "let expression result"); + CheckWellformedWithResult(Substitute(e.Body, null, substMap), wfOptions, result, locals, builder, etran); } else { // CheckWellformed(var b :| RHS(b); Body(b)) = diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index a344b9120a4..a44915f7c05 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -1,3 +1,4 @@ +using System; using System.Collections.Generic; using System.Collections.Immutable; using System.Diagnostics.Contracts; @@ -193,8 +194,11 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat } else { var bodyCheckDelayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, bodyCheckBuilder); bodyCheckDelayer.DoWithDelayedReadsChecks(false, wfo => { - generator.CheckWellformedWithResult(f.Body, wfo, selfCall, f.ResultType, locals, bodyCheckBuilder, etran, - "function call result"); + + Action checkPostcondition = b => { + generator.CheckSubsetType(etran, f.Body, selfCall, f.ResultType, b, "variable declaration RHS"); + }; + generator.CheckWellformedWithResult(f.Body, wfo, checkPostcondition, locals, bodyCheckBuilder, etran); if (f.Result != null) { var cmd = TrAssumeCmd(f.tok, Expr.Eq(selfCall, generator.TrVar(f.tok, f.Result))); generator.proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 25c7d142853..0dc8c0d2618 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -529,7 +529,11 @@ private void TranslateVariableDeclaration(BoogieStmtListBuilder builder, List checkPostcondition = b => { + CheckSubsetType(etran, rhs, boogieTupleReference, pat.Expr.Type, b, "variable declaration RHS"); + }; + CheckWellformedWithResult(rhs, new WFOptions(null, false, false), checkPostcondition, locals, builder, etran); CheckCasePatternShape(pat, rhs, boogieTupleReference, rhs.tok, pat.Expr.Type, builder); builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, varDeclPattern.tok, pat.Expr, e => Expr.Eq(e, boogieTupleReference), "variable declaration")); } diff --git a/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs b/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs index f3f3b247447..0d826b98c10 100644 --- a/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs +++ b/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs @@ -2,7 +2,7 @@ using Microsoft.Boogie; namespace Microsoft.Dafny { - internal class BoogieStmtListBuilder { + public class BoogieStmtListBuilder { public DafnyOptions Options { get; } public StmtListBuilder builder; public BoogieGenerator tran; From 1ecd423c964280e01c458aacdad609db36ada524 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Sat, 27 Jul 2024 09:09:09 +0200 Subject: [PATCH 09/32] Change with bugs --- .../BoogieGenerator.ExpressionWellformed.cs | 297 +++++++++--------- ...oogieGenerator.Functions.Wellformedness.cs | 44 +-- .../Verifier/BoogieGenerator.TrStatement.cs | 11 +- 3 files changed, 191 insertions(+), 161 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 01f812e4256..1944c076b2b 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -1134,132 +1134,13 @@ void CheckOperand(Expression operand) { break; } case LetExpr letExpr: - CheckWellformedLetExprWithResult(letExpr, wfOptions, checkPostcondition, resultType, locals, builder, etran, true); + CheckWellformedLetExprWithResult(letExpr, wfOptions, checkPostcondition, locals, builder, etran, true); checkPostcondition = null; break; case ComprehensionExpr comprehensionExpr: { - var e = comprehensionExpr; - var lam = e as LambdaExpr; - var mc = e as MapComprehension; - if (mc is { IsGeneralMapComprehension: false }) { - mc = null; // mc will be non-null when "e" is a general map comprehension - } - - // This is a WF check, so we look at the original quantifier, not the split one. - // This ensures that cases like forall x :: x != null && f(x.a) do not fail to verify. - - builder.Add(new Bpl.CommentCmd("Begin Comprehension WF check")); - BplIfIf(e.tok, lam != null, null, builder, nextBuilder => { - var comprehensionEtran = etran; - if (lam != null) { - // Havoc heap - locals.Add(BplLocalVar(CurrentIdGenerator.FreshId((etran.UsesOldHeap ? "$Heap_at_" : "") + "$lambdaHeap#"), predef.HeapType, out var lambdaHeap)); - comprehensionEtran = new ExpressionTranslator(comprehensionEtran, lambdaHeap); - nextBuilder.Add(new HavocCmd(expr.tok, Singleton((Bpl.IdentifierExpr)comprehensionEtran.HeapExpr))); - nextBuilder.Add(new AssumeCmd(expr.tok, FunctionCall(expr.tok, BuiltinFunction.IsGoodHeap, null, comprehensionEtran.HeapExpr))); - nextBuilder.Add(new AssumeCmd(expr.tok, HeapSameOrSucc(etran.HeapExpr, comprehensionEtran.HeapExpr))); - } - - var substMap = SetupBoundVarsAsLocals(e.BoundVars, out var typeAntecedents, nextBuilder, locals, comprehensionEtran); - BplIfIf(e.tok, true, typeAntecedents, nextBuilder, newBuilder => { - var s = new Substituter(null, substMap, new Dictionary()); - var body = Substitute(e.Term, null, substMap); - var bodyLeft = mc != null ? Substitute(mc.TermLeft, null, substMap) : null; - var substMapPrime = mc != null ? SetupBoundVarsAsLocals(e.BoundVars, newBuilder, locals, comprehensionEtran, "#prime") : null; - var bodyLeftPrime = mc != null ? Substitute(mc.TermLeft, null, substMapPrime) : null; - var bodyPrime = mc != null ? Substitute(e.Term, null, substMapPrime) : null; - List reads = null; - - var newOptions = wfOptions; - if (lam != null) { - // Set up a new frame - var frameName = CurrentIdGenerator.FreshId("$_Frame#l"); - reads = lam.Reads.Expressions.ConvertAll(s.SubstFrameExpr); - comprehensionEtran = comprehensionEtran.WithReadsFrame(frameName, lam); - DefineFrame(e.tok, comprehensionEtran.ReadsFrame(e.tok), reads, newBuilder, locals, frameName, comprehensionEtran); - - // Check frame WF and that it read covers itself - var delayer = new ReadsCheckDelayer(comprehensionEtran, wfOptions.SelfCallsAllowance, locals, builder, newBuilder); - delayer.DoWithDelayedReadsChecks(false, wfo => { - CheckFrameWellFormed(wfo, reads, locals, newBuilder, comprehensionEtran); - }); - - // continue doing reads checks, but don't delay them - newOptions = new WFOptions(wfOptions.SelfCallsAllowance, true, false); - } - - // check requires/range - Bpl.Expr guard = null; - if (e.Range != null) { - var range = Substitute(e.Range, null, substMap); - CheckWellformed(range, newOptions, locals, newBuilder, comprehensionEtran); - guard = comprehensionEtran.TrExpr(range); - } - - if (mc != null) { - Contract.Assert(bodyLeft != null); - BplIfIf(e.tok, guard != null, guard, newBuilder, b => { CheckWellformed(bodyLeft, newOptions, locals, b, comprehensionEtran); }); - } - BplIfIf(e.tok, guard != null, guard, newBuilder, b => { - Bpl.Expr resultIe = null; - Type rangeType = null; - if (lam != null) { - var resultName = CurrentIdGenerator.FreshId("lambdaResult#"); - var resultVar = new Bpl.LocalVariable(body.tok, new Bpl.TypedIdent(body.tok, resultName, TrType(body.Type))); - locals.Add(resultVar); - resultIe = new Bpl.IdentifierExpr(body.tok, resultVar); - rangeType = lam.Type.AsArrowType.Result; - } - CheckWellformedWithResult(body, newOptions, resultIe, locals, b, comprehensionEtran); - }); - - if (mc != null) { - Contract.Assert(substMapPrime != null); - Contract.Assert(bodyLeftPrime != null); - Contract.Assert(bodyPrime != null); - Bpl.Expr guardPrime = null; - if (guard != null) { - Contract.Assert(e.Range != null); - var rangePrime = Substitute(e.Range, null, substMapPrime); - guardPrime = comprehensionEtran.TrExpr(rangePrime); - } - BplIfIf(e.tok, guard != null, BplAnd(guard, guardPrime), newBuilder, b => { - var different = BplOr( - Bpl.Expr.Neq(comprehensionEtran.TrExpr(bodyLeft), comprehensionEtran.TrExpr(bodyLeftPrime)), - Bpl.Expr.Eq(comprehensionEtran.TrExpr(body), comprehensionEtran.TrExpr(bodyPrime))); - b.Add(Assert(GetToken(mc.TermLeft), different, new PODesc.ComprehensionNoAlias(mc.BoundVars, mc.Range, mc.TermLeft, mc.Term))); - }); - } - }); - - if (lam != null) { - // assume false (heap was havoced inside an if) - Contract.Assert(nextBuilder != builder); - nextBuilder.Add(new AssumeCmd(e.tok, Bpl.Expr.False)); - } - }); - - bool needTypeConstraintCheck; - if (lam == null) { - needTypeConstraintCheck = true; - } else { - // omit constraint check if the type is according to the syntax of the expression - var arrowType = (UserDefinedType)e.Type.NormalizeExpandKeepConstraints(); - if (ArrowType.IsPartialArrowTypeName(arrowType.Name)) { - needTypeConstraintCheck = lam.Reads.Expressions.Count != 0; - } else if (ArrowType.IsTotalArrowTypeName(arrowType.Name)) { - needTypeConstraintCheck = lam.Reads.Expressions.Count != 0 || lam.Range != null; - } else { - needTypeConstraintCheck = true; - } - } - if (needTypeConstraintCheck) { - CheckResultToBeInType(e.tok, e, e.Type, locals, builder, etran); - } - - builder.Add(new Bpl.CommentCmd("End Comprehension WF check")); - break; - } + CheckWellformedComprehensionExpression(wfOptions, locals, builder, etran, comprehensionExpr); + break; + } case StmtExpr stmtExpr: var bodyBuilder = new BoogieStmtListBuilder(this, builder.Options); PathAsideBlock(stmtExpr.tok, bodyBuilder, builder); @@ -1277,7 +1158,7 @@ void CheckOperand(Expression operand) { // has already been checked in e.Test var letExpr = (LetExpr)e.Thn; Contract.Assert(letExpr != null); - CheckWellformedLetExprWithResult(letExpr, wfOptions, checkPostcondition, resultType, locals, bThen, etran, false); + CheckWellformedLetExprWithResult(letExpr, wfOptions, checkPostcondition, locals, bThen, etran, false); } else { CheckWellformedWithResult(e.Thn, wfOptions, checkPostcondition, locals, bThen, etran); } @@ -1287,8 +1168,8 @@ void CheckOperand(Expression operand) { break; } case MatchExpr matchExpr: - checkPostcondition = TrMatchExpr(matchExpr, wfOptions, checkPostcondition, resultType, locals, builder, etran); - resultDescription = "match expression"; + TrMatchExpr(matchExpr, wfOptions, checkPostcondition, locals, builder, etran); + checkPostcondition = null; break; case DatatypeUpdateExpr updateExpr: { var e = updateExpr; @@ -1343,6 +1224,134 @@ void CheckOperand(Expression operand) { } } + private void CheckWellformedComprehensionExpression(WFOptions wfOptions, List locals, + BoogieStmtListBuilder builder, ExpressionTranslator etran, ComprehensionExpr expr) { + var lam = expr as LambdaExpr; + var mc = expr as MapComprehension; + if (mc is { IsGeneralMapComprehension: false }) { + mc = null; // mc will be non-null when "e" is a general map comprehension + } + + // This is a WF check, so we look at the original quantifier, not the split one. + // This ensures that cases like forall x :: x != null && f(x.a) do not fail to verify. + + builder.Add(new Bpl.CommentCmd("Begin Comprehension WF check")); + BplIfIf(expr.tok, lam != null, null, builder, nextBuilder => { + var comprehensionEtran = etran; + if (lam != null) { + // Havoc heap + locals.Add(BplLocalVar(CurrentIdGenerator.FreshId((etran.UsesOldHeap ? "$Heap_at_" : "") + "$lambdaHeap#"), predef.HeapType, out var lambdaHeap)); + comprehensionEtran = new ExpressionTranslator(comprehensionEtran, lambdaHeap); + nextBuilder.Add(new HavocCmd(expr.tok, Singleton((Bpl.IdentifierExpr)comprehensionEtran.HeapExpr))); + nextBuilder.Add(new AssumeCmd(expr.tok, FunctionCall(expr.tok, BuiltinFunction.IsGoodHeap, null, comprehensionEtran.HeapExpr))); + nextBuilder.Add(new AssumeCmd(expr.tok, HeapSameOrSucc(etran.HeapExpr, comprehensionEtran.HeapExpr))); + } + + var substMap = SetupBoundVarsAsLocals(expr.BoundVars, out var typeAntecedents, nextBuilder, locals, comprehensionEtran); + BplIfIf(expr.tok, true, typeAntecedents, nextBuilder, newBuilder => { + var s = new Substituter(null, substMap, new Dictionary()); + var body = Substitute(expr.Term, null, substMap); + var bodyLeft = mc != null ? Substitute(mc.TermLeft, null, substMap) : null; + var substMapPrime = mc != null ? SetupBoundVarsAsLocals(expr.BoundVars, newBuilder, locals, comprehensionEtran, "#prime") : null; + var bodyLeftPrime = mc != null ? Substitute(mc.TermLeft, null, substMapPrime) : null; + var bodyPrime = mc != null ? Substitute(expr.Term, null, substMapPrime) : null; + List reads = null; + + var newOptions = wfOptions; + if (lam != null) { + // Set up a new frame + var frameName = CurrentIdGenerator.FreshId("$_Frame#l"); + reads = lam.Reads.Expressions.ConvertAll(s.SubstFrameExpr); + comprehensionEtran = comprehensionEtran.WithReadsFrame(frameName, lam); + DefineFrame(expr.tok, comprehensionEtran.ReadsFrame(expr.tok), reads, newBuilder, locals, frameName, comprehensionEtran); + + // Check frame WF and that it read covers itself + var delayer = new ReadsCheckDelayer(comprehensionEtran, wfOptions.SelfCallsAllowance, locals, builder, newBuilder); + delayer.DoWithDelayedReadsChecks(false, wfo => { + CheckFrameWellFormed(wfo, reads, locals, newBuilder, comprehensionEtran); + }); + + // continue doing reads checks, but don't delay them + newOptions = new WFOptions(wfOptions.SelfCallsAllowance, true, false); + } + + // check requires/range + Bpl.Expr guard = null; + if (expr.Range != null) { + var range = Substitute(expr.Range, null, substMap); + CheckWellformed(range, newOptions, locals, newBuilder, comprehensionEtran); + guard = comprehensionEtran.TrExpr(range); + } + + if (mc != null) { + Contract.Assert(bodyLeft != null); + BplIfIf(expr.tok, guard != null, guard, newBuilder, b => { CheckWellformed(bodyLeft, newOptions, locals, b, comprehensionEtran); }); + } + BplIfIf(expr.tok, guard != null, guard, newBuilder, b => { + Bpl.Expr resultIe = null; + Type rangeType = null; + if (lam != null) { + var resultName = CurrentIdGenerator.FreshId("lambdaResult#"); + var resultVar = new Bpl.LocalVariable(body.tok, new Bpl.TypedIdent(body.tok, resultName, TrType(body.Type))); + locals.Add(resultVar); + resultIe = new Bpl.IdentifierExpr(body.tok, resultVar); + rangeType = lam.Type.AsArrowType.Result; + } + + Action checkPostcondition = builder => { + CheckSubsetType(etran, body, resultIe, rangeType, builder); + }; + CheckWellformedWithResult(body, newOptions, checkPostcondition, locals, b, comprehensionEtran); + }); + + if (mc != null) { + Contract.Assert(substMapPrime != null); + Contract.Assert(bodyLeftPrime != null); + Contract.Assert(bodyPrime != null); + Bpl.Expr guardPrime = null; + if (guard != null) { + Contract.Assert(expr.Range != null); + var rangePrime = Substitute(expr.Range, null, substMapPrime); + guardPrime = comprehensionEtran.TrExpr(rangePrime); + } + BplIfIf(expr.tok, guard != null, BplAnd(guard, guardPrime), newBuilder, b => { + var different = BplOr( + Bpl.Expr.Neq(comprehensionEtran.TrExpr(bodyLeft), comprehensionEtran.TrExpr(bodyLeftPrime)), + Bpl.Expr.Eq(comprehensionEtran.TrExpr(body), comprehensionEtran.TrExpr(bodyPrime))); + b.Add(Assert(GetToken(mc.TermLeft), different, new PODesc.ComprehensionNoAlias(mc.BoundVars, mc.Range, mc.TermLeft, mc.Term))); + }); + } + }); + + if (lam != null) { + // assume false (heap was havoced inside an if) + Contract.Assert(nextBuilder != builder); + nextBuilder.Add(new AssumeCmd(expr.tok, Bpl.Expr.False)); + } + }); + + bool needTypeConstraintCheck; + if (lam == null) { + needTypeConstraintCheck = true; + } else { + // omit constraint check if the type is according to the syntax of the expression + var arrowType = (UserDefinedType)expr.Type.NormalizeExpandKeepConstraints(); + if (ArrowType.IsPartialArrowTypeName(arrowType.Name)) { + needTypeConstraintCheck = lam.Reads.Expressions.Count != 0; + } else if (ArrowType.IsTotalArrowTypeName(arrowType.Name)) { + needTypeConstraintCheck = lam.Reads.Expressions.Count != 0 || lam.Range != null; + } else { + needTypeConstraintCheck = true; + } + } + if (needTypeConstraintCheck) { + CheckResultToBeInType(expr.tok, expr, expr.Type, locals, builder, etran); + } + + builder.Add(new Bpl.CommentCmd("End Comprehension WF check")); + return; + } + public void CheckSubsetType(ExpressionTranslator etran, Expression expr, Bpl.Expr selfCall, Type resultType, BoogieStmtListBuilder builder, string resultDescription = null) { @@ -1357,7 +1366,7 @@ public void CheckSubsetType(ExpressionTranslator etran, Expression expr, Bpl.Exp builder.Add(TrAssumeCmd(expr.tok, MkIs(selfCall, resultType))); } - private Expr TrMatchExpr(MatchExpr me, WFOptions wfOptions, Expr result, Type resultType, List locals, + private void TrMatchExpr(MatchExpr me, WFOptions wfOptions, Action checkPostcondition, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { FillMissingCases(me); @@ -1396,14 +1405,15 @@ private Expr TrMatchExpr(MatchExpr me, WFOptions wfOptions, Expr result, Type re BoogieStmtListBuilder b = new BoogieStmtListBuilder(this, options); Bpl.Expr ct = CtorInvocation(mc, me.Source.Type, etran, locals, b, NOALLOC, false); // generate: if (src == ctor(args)) { assume args-is-well-typed; mc.Body is well-formed; assume Result == TrExpr(case); } else ... - CheckWellformedWithResult(mc.Body, wfOptions, result, locals, b, etran); + + // TODO: + // resultDescription = "match expression"; + CheckWellformedWithResult(mc.Body, wfOptions, checkPostcondition, locals, b, etran); ifCmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifCmd, els); els = null; } builder.Add(ifCmd); - result = null; - return result; } private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions options, Action checkPostcondition, List locals, @@ -1490,7 +1500,7 @@ void CheckWellformedSpecialFunction(FunctionCallExpr expr, WFOptions options, Bp } } - void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr result, Type resultType, List locals, + void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Action checkPostcondition, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, bool checkRhs) { if (e.Exact) { var substMap = SetupBoundVarsAsLocals(e.BoundVars.ToList(), builder, locals, etran, "#Z"); @@ -1503,12 +1513,16 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r var r = new Bpl.LocalVariable(pat.tok, new Bpl.TypedIdent(pat.tok, nm, TrType(pat.Expr.Type))); locals.Add(r); var rIe = new Bpl.IdentifierExpr(rhs.tok, r); - CheckWellformedWithResult(e.RHSs[i], wfOptions, rIe, locals, builder, etran); + var unModifiedI = i; + Action checkPostconditionForLhs = innerBuilder => { + CheckSubsetType(etran, e.RHSs[unModifiedI], rIe, pat.Expr.Type, innerBuilder, "let expression binding RHS well-formed"); + }; + CheckWellformedWithResult(e.RHSs[i], wfOptions, checkPostconditionForLhs, locals, builder, etran); CheckCasePatternShape(pat, rhs, rIe, rhs.tok, pat.Expr.Type, builder); var substExpr = Substitute(pat.Expr, null, substMap); builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, e.tok, substExpr, e => Bpl.Expr.Eq(e, rIe), "let expression binding")); } - CheckWellformedWithResult(Substitute(e.Body, null, substMap), wfOptions, result, locals, builder, etran); + CheckWellformedWithResult(Substitute(e.Body, null, substMap), wfOptions, checkPostcondition, locals, builder, etran); } else { // CheckWellformed(var b :| RHS(b); Body(b)) = @@ -1561,14 +1575,15 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r var info = letSuchThatExprInfo[e]; builder.Add(new Bpl.AssumeCmd(e.tok, info.CanCallFunctionCall(this, etran))); // If we are supposed to assume "result" to equal this expression, then use the body of the let-such-that, not the generated $let#... function - if (result != null) { - Contract.Assert(resultType != null); - var bResult = etran.TrExpr(letBody); - CheckSubrange(letBody.tok, bResult, letBody.Type, resultType, letBody, builder); - builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, e.tok, letBody, e => Expr.Eq(result, e), "let expression")); - builder.Add(TrAssumeCmd(letBody.tok, etran.CanCallAssumption(letBody))); - builder.Add(new CommentCmd("CheckWellformedWithResult: Let expression")); - builder.Add(TrAssumeCmd(letBody.tok, MkIs(result, resultType))); + if (checkPostcondition != null) { + checkPostcondition(builder); + // Contract.Assert(resultType != null); + // var bResult = etran.TrExpr(letBody); + // CheckSubrange(letBody.tok, bResult, letBody.Type, resultType, letBody, builder); + // builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, e.tok, letBody, e => Expr.Eq(checkPostcondition, e), "let expression")); + // builder.Add(TrAssumeCmd(letBody.tok, etran.CanCallAssumption(letBody))); + // builder.Add(new CommentCmd("CheckWellformedWithResult: Let expression")); + // builder.Add(TrAssumeCmd(letBody.tok, MkIs(checkPostcondition, resultType))); } } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index a44915f7c05..ab6910cf6b5 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -188,37 +188,43 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat var selfCall = GetSelfCall(f, etran, parameters); var bodyCheckBuilder = new BoogieStmtListBuilder(generator, generator.options); bodyCheckBuilder.Add(new CommentCmd("Check Wfness of body, result subset type constraint, and return to check the postcondition")); - if (f.Body == null || !generator.RevealedInScope(f)) { - // don't fall through to postcondition checks - bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Expr.False)); - } else { + if (f.Body != null && generator.RevealedInScope(f)) { var bodyCheckDelayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, bodyCheckBuilder); bodyCheckDelayer.DoWithDelayedReadsChecks(false, wfo => { - Action checkPostcondition = b => { - generator.CheckSubsetType(etran, f.Body, selfCall, f.ResultType, b, "variable declaration RHS"); + Contract.Assert(f.ResultType != null); + var bResult = etran.TrExpr(f.Body); + generator.CheckSubrange(f.Body.tok, bResult, f.Body.Type, f.ResultType, f.Body, b); }; generator.CheckWellformedWithResult(f.Body, wfo, checkPostcondition, locals, bodyCheckBuilder, etran); + bodyCheckBuilder.Add(generator.TrAssumeCmdWithDependenciesAndExtend(etran, f.Body.tok, f.Body, + e => Bpl.Expr.Eq(selfCall, generator.AdaptBoxing(f.Body.tok, e, f.Body.Type, f.ResultType)), + "function call result")); + bodyCheckBuilder.Add(TrAssumeCmd(f.Body.tok, etran.CanCallAssumption(f.Body))); + bodyCheckBuilder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); + bodyCheckBuilder.Add(TrAssumeCmd(f.Body.tok, generator.MkIs(selfCall, f.ResultType))); if (f.Result != null) { var cmd = TrAssumeCmd(f.tok, Expr.Eq(selfCall, generator.TrVar(f.tok, f.Result))); generator.proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); bodyCheckBuilder.Add(cmd); } - }); - - foreach (AttributedExpression e in f.Ens) { - var functionHeight = generator.currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); - var splits = new List(); - bool splitHappened /*we actually don't care*/ = - generator.TrSplitExpr(e.E, splits, true, functionHeight, true, true, etran); - var (errorMessage, successMessage) = generator.CustomErrorMessage(e.Attributes); - foreach (var s in splits) { - if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, generator.currentModule)) { - var ensures = generator.EnsuresWithDependencies(s.Tok, false, e.E, s.E, errorMessage, successMessage, null); - bodyCheckBuilder.Add(new AssertCmd(ensures.tok, ensures.Condition, ensures.Description, ensures.Attributes)); + + foreach (AttributedExpression e in f.Ens) { + var functionHeight = generator.currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); + var splits = new List(); + bool splitHappened /*we actually don't care*/ = + generator.TrSplitExpr(e.E, splits, true, functionHeight, true, true, etran); + var (errorMessage, successMessage) = generator.CustomErrorMessage(e.Attributes); + foreach (var s in splits) { + if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, generator.currentModule)) { + var ensures = + generator.EnsuresWithDependencies(s.Tok, false, e.E, s.E, errorMessage, successMessage, null); + bodyCheckBuilder.Add(new AssertCmd(ensures.tok, ensures.Condition, ensures.Description, + ensures.Attributes)); + } } } - } + }); // Enforce 'older' conditions var (olderParameterCount, olderCondition) = generator.OlderCondition(f, selfCall, parameters); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 0dc8c0d2618..3f91d74a48c 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -531,9 +531,18 @@ private void TranslateVariableDeclaration(BoogieStmtListBuilder builder, List checkPostcondition = b => { - CheckSubsetType(etran, rhs, boogieTupleReference, pat.Expr.Type, b, "variable declaration RHS"); + Contract.Assert(pat.Expr.Type != null); + var bResult = etran.TrExpr(rhs); + CheckSubrange(rhs.tok, bResult, rhs.Type, pat.Expr.Type, rhs, b); + b.Add(TrAssumeCmdWithDependenciesAndExtend(etran, rhs.tok, rhs, + e => Bpl.Expr.Eq(boogieTupleReference, AdaptBoxing(rhs.tok, e, rhs.Type, pat.Expr.Type)), + "variable declaration RHS")); }; CheckWellformedWithResult(rhs, new WFOptions(null, false, false), checkPostcondition, locals, builder, etran); + builder.Add(TrAssumeCmd(rhs.tok, etran.CanCallAssumption(rhs))); + builder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); + builder.Add(TrAssumeCmd(rhs.tok, MkIs(boogieTupleReference, pat.Expr.Type))); + CheckCasePatternShape(pat, rhs, boogieTupleReference, rhs.tok, pat.Expr.Type, builder); builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, varDeclPattern.tok, pat.Expr, e => Expr.Eq(e, boogieTupleReference), "variable declaration")); } From 6d757b40d810f012ac56810aeaec08dd372d66fd Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Sat, 27 Jul 2024 09:35:09 +0200 Subject: [PATCH 10/32] Slightly better behavior --- .../BoogieGenerator.ExpressionWellformed.cs | 59 ++++++++--------- ...oogieGenerator.Functions.Wellformedness.cs | 64 ++++++++++--------- .../Verifier/BoogieGenerator.TrStatement.cs | 10 +-- .../expressions/statementExpressionScope.dfy | 6 +- .../statementExpressionScope.dfy.expect | 5 +- 5 files changed, 73 insertions(+), 71 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 1944c076b2b..9e3c487a676 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -13,6 +13,7 @@ using DafnyCore.Verifier; using Bpl = Microsoft.Boogie; using Microsoft.Boogie; +using Std.Wrappers; using static Microsoft.Dafny.Util; using PODesc = Microsoft.Dafny.ProofObligationDescription; @@ -262,8 +263,9 @@ void CheckWellformed(Expression expr, WFOptions options, List locals, /// See class WFOptions for descriptions of the specified options. /// void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, - Action checkPostcondition, - List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { + CheckPostcondition checkPostcondition, + List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, + string resultDescription = null) { Contract.Requires(expr != null); Contract.Requires(wfOptions != null); Contract.Requires(locals != null); @@ -1143,8 +1145,8 @@ void CheckOperand(Expression operand) { } case StmtExpr stmtExpr: var bodyBuilder = new BoogieStmtListBuilder(this, builder.Options); - PathAsideBlock(stmtExpr.tok, bodyBuilder, builder); CheckWellformedStmtExpr(stmtExpr, wfOptions, checkPostcondition, locals, bodyBuilder, etran); + PathAsideBlock(stmtExpr.tok, bodyBuilder, builder); checkPostcondition = null; break; case ITEExpr iteExpr: { @@ -1160,9 +1162,9 @@ void CheckOperand(Expression operand) { Contract.Assert(letExpr != null); CheckWellformedLetExprWithResult(letExpr, wfOptions, checkPostcondition, locals, bThen, etran, false); } else { - CheckWellformedWithResult(e.Thn, wfOptions, checkPostcondition, locals, bThen, etran); + CheckWellformedWithResult(e.Thn, wfOptions, checkPostcondition, locals, bThen, etran, "if expression then branch"); } - CheckWellformedWithResult(e.Els, wfOptions, checkPostcondition, locals, bElse, etran); + CheckWellformedWithResult(e.Els, wfOptions, checkPostcondition, locals, bElse, etran, "if expression else branch"); builder.Add(new Bpl.IfCmd(iteExpr.tok, etran.TrExpr(e.Test), bThen.Collect(iteExpr.tok), null, bElse.Collect(iteExpr.tok))); checkPostcondition = null; break; @@ -1186,18 +1188,18 @@ void CheckOperand(Expression operand) { CheckNotGhostVariant(e.InCompiledContext, updateExpr, e.Root, "update of", e.Members, e.LegalSourceConstructors, builder, etran); - CheckWellformedWithResult(e.ResolvedExpression, wfOptions, checkPostcondition, locals, builder, etran); + CheckWellformedWithResult(e.ResolvedExpression, wfOptions, checkPostcondition, locals, builder, etran, resultDescription); checkPostcondition = null; break; } case ConcreteSyntaxExpression expression: { var e = expression; - CheckWellformedWithResult(e.ResolvedExpression, wfOptions, checkPostcondition, locals, builder, etran); + CheckWellformedWithResult(e.ResolvedExpression, wfOptions, checkPostcondition, locals, builder, etran, resultDescription); checkPostcondition = null; break; } case NestedMatchExpr nestedMatchExpr: - CheckWellformedWithResult(nestedMatchExpr.Flattened, wfOptions, checkPostcondition, locals, builder, etran); + CheckWellformedWithResult(nestedMatchExpr.Flattened, wfOptions, checkPostcondition, locals, builder, etran, resultDescription); checkPostcondition = null; break; case BoogieFunctionCall call: { @@ -1220,7 +1222,7 @@ void CheckOperand(Expression operand) { if (checkPostcondition != null) { - checkPostcondition(builder); + checkPostcondition(builder, expr, true, resultDescription); } } @@ -1298,8 +1300,8 @@ private void CheckWellformedComprehensionExpression(WFOptions wfOptions, List checkPostcondition = builder => { - CheckSubsetType(etran, body, resultIe, rangeType, builder); + CheckPostcondition checkPostcondition = (innerBuilder, innerBody, adaptBox, prefix) => { + CheckSubsetType(etran, innerBody, resultIe, rangeType, innerBuilder, adaptBox, prefix); }; CheckWellformedWithResult(body, newOptions, checkPostcondition, locals, b, comprehensionEtran); }); @@ -1353,20 +1355,20 @@ private void CheckWellformedComprehensionExpression(WFOptions wfOptions, List Bpl.Expr.Eq(selfCall, AdaptBoxing(expr.tok, e, expr.Type, resultType)), + e => Bpl.Expr.Eq(selfCall, adaptBoxing ? AdaptBoxing(expr.tok, e, expr.Type, resultType) : e), resultDescription)); builder.Add(TrAssumeCmd(expr.tok, etran.CanCallAssumption(expr))); builder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); builder.Add(TrAssumeCmd(expr.tok, MkIs(selfCall, resultType))); } - private void TrMatchExpr(MatchExpr me, WFOptions wfOptions, Action checkPostcondition, List locals, + private void TrMatchExpr(MatchExpr me, WFOptions wfOptions, CheckPostcondition checkPostcondition, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { FillMissingCases(me); @@ -1408,7 +1410,7 @@ private void TrMatchExpr(MatchExpr me, WFOptions wfOptions, Action checkPostcondition, List locals, + private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions wfOptions, CheckPostcondition checkPostcondition, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { // If we're inside an "old" expression, then "etran" will know how to translate // expressions. However, here, we're also having to translate e.S, which is a @@ -1429,7 +1431,7 @@ private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions options, Actio TrStmt(stmtExpr.S, builder, locals, etran); } - CheckWellformedWithResult(stmtExpr.E, options, checkPostcondition, locals, builder, etran); + CheckWellformedWithResult(stmtExpr.E, wfOptions, checkPostcondition, locals, builder, etran, "statement expression result"); } /// @@ -1500,7 +1502,10 @@ void CheckWellformedSpecialFunction(FunctionCallExpr expr, WFOptions options, Bp } } - void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Action checkPostcondition, List locals, + delegate void CheckPostcondition(BoogieStmtListBuilder builder, Expression body, bool adaptBox, + string errorMessagePrefix); + + void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, CheckPostcondition checkPostcondition, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, bool checkRhs) { if (e.Exact) { var substMap = SetupBoundVarsAsLocals(e.BoundVars.ToList(), builder, locals, etran, "#Z"); @@ -1513,16 +1518,15 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Action checkPostconditionForLhs = innerBuilder => { - CheckSubsetType(etran, e.RHSs[unModifiedI], rIe, pat.Expr.Type, innerBuilder, "let expression binding RHS well-formed"); + CheckPostcondition checkPostconditionForLhs = (innerBuilder, body, adaptBoxing, prefix) => { + CheckSubsetType(etran, body, rIe, pat.Expr.Type, innerBuilder, adaptBoxing, prefix); }; - CheckWellformedWithResult(e.RHSs[i], wfOptions, checkPostconditionForLhs, locals, builder, etran); + CheckWellformedWithResult(e.RHSs[i], wfOptions, checkPostconditionForLhs, locals, builder, etran, "let expression binding RHS well-formed"); CheckCasePatternShape(pat, rhs, rIe, rhs.tok, pat.Expr.Type, builder); var substExpr = Substitute(pat.Expr, null, substMap); builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, e.tok, substExpr, e => Bpl.Expr.Eq(e, rIe), "let expression binding")); } - CheckWellformedWithResult(Substitute(e.Body, null, substMap), wfOptions, checkPostcondition, locals, builder, etran); + CheckWellformedWithResult(Substitute(e.Body, null, substMap), wfOptions, checkPostcondition, locals, builder, etran, "let expression result"); } else { // CheckWellformed(var b :| RHS(b); Body(b)) = @@ -1576,14 +1580,7 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Action Expr.Eq(checkPostcondition, e), "let expression")); - // builder.Add(TrAssumeCmd(letBody.tok, etran.CanCallAssumption(letBody))); - // builder.Add(new CommentCmd("CheckWellformedWithResult: Let expression")); - // builder.Add(TrAssumeCmd(letBody.tok, MkIs(checkPostcondition, resultType))); + checkPostcondition(builder, letBody, false, "let expression"); } } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index ab6910cf6b5..a5bcfeae717 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -187,43 +187,45 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat { var selfCall = GetSelfCall(f, etran, parameters); var bodyCheckBuilder = new BoogieStmtListBuilder(generator, generator.options); - bodyCheckBuilder.Add(new CommentCmd("Check Wfness of body, result subset type constraint, and return to check the postcondition")); + bodyCheckBuilder.Add(new CommentCmd("Check Wfness of body and result subset type constraint")); if (f.Body != null && generator.RevealedInScope(f)) { var bodyCheckDelayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, bodyCheckBuilder); bodyCheckDelayer.DoWithDelayedReadsChecks(false, wfo => { - Action checkPostcondition = b => { - Contract.Assert(f.ResultType != null); - var bResult = etran.TrExpr(f.Body); - generator.CheckSubrange(f.Body.tok, bResult, f.Body.Type, f.ResultType, f.Body, b); - }; - generator.CheckWellformedWithResult(f.Body, wfo, checkPostcondition, locals, bodyCheckBuilder, etran); - bodyCheckBuilder.Add(generator.TrAssumeCmdWithDependenciesAndExtend(etran, f.Body.tok, f.Body, - e => Bpl.Expr.Eq(selfCall, generator.AdaptBoxing(f.Body.tok, e, f.Body.Type, f.ResultType)), - "function call result")); - bodyCheckBuilder.Add(TrAssumeCmd(f.Body.tok, etran.CanCallAssumption(f.Body))); - bodyCheckBuilder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); - bodyCheckBuilder.Add(TrAssumeCmd(f.Body.tok, generator.MkIs(selfCall, f.ResultType))); - if (f.Result != null) { - var cmd = TrAssumeCmd(f.tok, Expr.Eq(selfCall, generator.TrVar(f.tok, f.Result))); - generator.proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); - bodyCheckBuilder.Add(cmd); - } + CheckPostcondition checkPostcondition = (b, innerBody, adaptBoxing, prefix) => { + generator.CheckSubsetType(etran, innerBody, selfCall, f.Body.Type, b, adaptBoxing, prefix); + // Contract.Assert(f.ResultType != null); + // var bResult = etran.TrExpr(innerBody); + // generator.CheckSubrange(f.Body.tok, bResult, f.Body.Type, f.ResultType, f.Body, b); + // + // bodyCheckBuilder.Add(generator.TrAssumeCmdWithDependenciesAndExtend(etran, f.Body.tok, f.Body, + // e => Bpl.Expr.Eq(selfCall, generator.AdaptBoxing(f.Body.tok, e, f.Body.Type, f.ResultType)), + // prefix)); + // bodyCheckBuilder.Add(TrAssumeCmd(f.Body.tok, etran.CanCallAssumption(f.Body))); + // bodyCheckBuilder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); + // bodyCheckBuilder.Add(TrAssumeCmd(f.Body.tok, generator.MkIs(selfCall, f.ResultType))); + if (f.Result != null) { + var cmd = TrAssumeCmd(f.tok, Expr.Eq(selfCall, generator.TrVar(f.tok, f.Result))); + generator.proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); + b.Add(cmd); + } - foreach (AttributedExpression e in f.Ens) { - var functionHeight = generator.currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); - var splits = new List(); - bool splitHappened /*we actually don't care*/ = - generator.TrSplitExpr(e.E, splits, true, functionHeight, true, true, etran); - var (errorMessage, successMessage) = generator.CustomErrorMessage(e.Attributes); - foreach (var s in splits) { - if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, generator.currentModule)) { - var ensures = - generator.EnsuresWithDependencies(s.Tok, false, e.E, s.E, errorMessage, successMessage, null); - bodyCheckBuilder.Add(new AssertCmd(ensures.tok, ensures.Condition, ensures.Description, - ensures.Attributes)); + foreach (AttributedExpression e in f.Ens) { + var functionHeight = generator.currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); + var splits = new List(); + bool splitHappened /*we actually don't care*/ = + generator.TrSplitExpr(e.E, splits, true, functionHeight, true, true, etran); + var (errorMessage, successMessage) = generator.CustomErrorMessage(e.Attributes); + foreach (var s in splits) { + if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, generator.currentModule)) { + var ensures = + generator.EnsuresWithDependencies(s.Tok, false, e.E, s.E, errorMessage, successMessage, null); + b.Add(new AssertCmd(ensures.tok, ensures.Condition, ensures.Description, + ensures.Attributes)); + } } } - } + }; + generator.CheckWellformedWithResult(f.Body, wfo, checkPostcondition, locals, bodyCheckBuilder, etran, "function call result"); }); // Enforce 'older' conditions diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 3f91d74a48c..2f773fd5a3b 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -530,15 +530,15 @@ private void TranslateVariableDeclaration(BoogieStmtListBuilder builder, List checkPostcondition = b => { + CheckPostcondition checkPostcondition = (b, body, adaptBoxing, prefix) => { Contract.Assert(pat.Expr.Type != null); - var bResult = etran.TrExpr(rhs); + var bResult = etran.TrExpr(body); CheckSubrange(rhs.tok, bResult, rhs.Type, pat.Expr.Type, rhs, b); b.Add(TrAssumeCmdWithDependenciesAndExtend(etran, rhs.tok, rhs, - e => Bpl.Expr.Eq(boogieTupleReference, AdaptBoxing(rhs.tok, e, rhs.Type, pat.Expr.Type)), - "variable declaration RHS")); + e => Bpl.Expr.Eq(boogieTupleReference, adaptBoxing ? AdaptBoxing(rhs.tok, e, rhs.Type, pat.Expr.Type) : e), + prefix)); }; - CheckWellformedWithResult(rhs, new WFOptions(null, false, false), checkPostcondition, locals, builder, etran); + CheckWellformedWithResult(rhs, new WFOptions(null, false, false), checkPostcondition, locals, builder, etran, "variable declaration RHS"); builder.Add(TrAssumeCmd(rhs.tok, etran.CanCallAssumption(rhs))); builder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); builder.Add(TrAssumeCmd(rhs.tok, MkIs(boogieTupleReference, pat.Expr.Type))); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy index 0fed01f610c..0f3a062562e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy @@ -10,11 +10,11 @@ function StatementExpressionValueAndEnsures(): int function StatementExpressionAssumeAndFunctionEnsures(): int ensures 10 == 11 // no error, since the statement expression can be used for the ensures clause { - assume false; 10 + assume false; 42 } -function StatementExpressionAssumeAndFunctionEnsures(): int - ensures 10 == 11 // error, since the assume false does not leak +function StatementExpressionAssumeInLetAndFunctionEnsures(): int + ensures 10 == 11 // error, since the assume false does not leak from a let { var x := (assume false; 10); x } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect index 0471f345c93..529ffa2c168 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect @@ -1,2 +1,5 @@ +statementExpressionScope.dfy(17,13): Error: this is the postcondition that could not be proved +statementExpressionScope.dfy(45,9): Error: assertion might not hold +statementExpressionScope.dfy(51,9): Error: assertion might not hold -Dafny program verifier finished with 12 verified, 2 errors +Dafny program verifier finished with 12 verified, 3 errors From cbb8b9b5dd95827b7f6de11f0029e379d90f88df Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Sat, 27 Jul 2024 09:41:26 +0200 Subject: [PATCH 11/32] Update test --- .../LitTest/ast/expressions/statementExpressionScope.dfy | 8 ++++++++ .../ast/expressions/statementExpressionScope.dfy.expect | 4 ++-- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy index 0f3a062562e..9b985e35115 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy @@ -31,6 +31,14 @@ method StatementExpressionAndSubsetLocal() var x: nat := assume -1 > 0; -1; } +method StatementExpressionAndSubsetLocal2() + // no error, since the statement expression can be used for the local variable type subset constraint +{ + var x: nat := assume -1 > 0; -1; + assert x >= 0; // no error; + assert StatementExpressionAndSubsetResult() >= 0; // no error +} + predicate P(x: int) method NeedsP(x: int) requires P(x) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect index 529ffa2c168..54d13e6d8a7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect @@ -1,5 +1,5 @@ statementExpressionScope.dfy(17,13): Error: this is the postcondition that could not be proved -statementExpressionScope.dfy(45,9): Error: assertion might not hold -statementExpressionScope.dfy(51,9): Error: assertion might not hold +statementExpressionScope.dfy(53,9): Error: assertion might not hold +statementExpressionScope.dfy(59,9): Error: assertion might not hold Dafny program verifier finished with 12 verified, 3 errors From 0726bc5ec06b1030a8ee09f1379c43f2302f67f6 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Sat, 27 Jul 2024 09:51:42 +0200 Subject: [PATCH 12/32] One more passing test --- .../Verifier/BoogieGenerator.TrStatement.cs | 15 ++++++++++----- .../ast/expressions/statementExpressionScope.dfy | 2 +- 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 2f773fd5a3b..f72b3b1a23c 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -2585,10 +2585,14 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs if (rhs is ExprRhs) { var e = (ExprRhs)rhs; - TrStmt_CheckWellformed(e.Expr, builder, locals, etran, true); + TrStmt_CheckWellformed(e.Expr, builder, locals, etran, true, checkPostcondition: + (b, innerBody, adaptBoxing, prefix) => { + Bpl.Expr bRhs = etran.TrExpr(innerBody); + CheckSubrange(tok, bRhs, e.Expr.Type, rhsTypeConstraint, e.Expr, b); + }); - Bpl.Expr bRhs = etran.TrExpr(e.Expr); - CheckSubrange(tok, bRhs, e.Expr.Type, rhsTypeConstraint, e.Expr, builder); + var bRhs = etran.TrExpr(e.Expr); + builder.Add(TrAssumeCmd(e.tok, MkIs(bRhs, lhsType))); if (bGivenLhs != null) { Contract.Assert(bGivenLhs == bLhs); // box the RHS, then do the assignment @@ -2798,7 +2802,8 @@ void TrStmtList(List stmts, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, bool subsumption, bool lValueContext = false) { + void TrStmt_CheckWellformed(Expression expr, BoogieStmtListBuilder builder, List locals, + ExpressionTranslator etran, bool subsumption, bool lValueContext = false, CheckPostcondition checkPostcondition = null) { Contract.Requires(expr != null); Contract.Requires(builder != null); Contract.Requires(locals != null); @@ -2823,7 +2828,7 @@ void TrStmt_CheckWellformed(Expression expr, BoogieStmtListBuilder builder, List if (lValueContext) { options = options.WithLValueContext(true); } - CheckWellformed(expr, options, locals, builder, etran); + CheckWellformedWithResult(expr, options, checkPostcondition, locals, builder, etran); builder.Add(TrAssumeCmd(expr.tok, etran.CanCallAssumption(expr))); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy index 9b985e35115..3881556b9e4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy @@ -36,7 +36,7 @@ method StatementExpressionAndSubsetLocal2() { var x: nat := assume -1 > 0; -1; assert x >= 0; // no error; - assert StatementExpressionAndSubsetResult() >= 0; // no error + // really weird that this changes things // assert StatementExpressionAndSubsetResult() >= 0; // no error } predicate P(x: int) From ae1309171333abb27ed6a4fcc728f73ad2736009 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 29 Jul 2024 12:45:38 +0200 Subject: [PATCH 13/32] Ran formatter --- .../BoogieGenerator.ExpressionWellformed.cs | 14 ++++---- ...oogieGenerator.Functions.Wellformedness.cs | 32 ++++++++----------- .../Verifier/BoogieGenerator.TrStatement.cs | 9 +++--- .../expressions/statementExpressionScope.dfy | 4 ++- .../statementExpressionScope.dfy.expect | 9 ++++-- 5 files changed, 33 insertions(+), 35 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 9e3c487a676..0a0bfee970d 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -1140,9 +1140,9 @@ void CheckOperand(Expression operand) { checkPostcondition = null; break; case ComprehensionExpr comprehensionExpr: { - CheckWellformedComprehensionExpression(wfOptions, locals, builder, etran, comprehensionExpr); - break; - } + CheckWellformedComprehensionExpression(wfOptions, locals, builder, etran, comprehensionExpr); + break; + } case StmtExpr stmtExpr: var bodyBuilder = new BoogieStmtListBuilder(this, builder.Options); CheckWellformedStmtExpr(stmtExpr, wfOptions, checkPostcondition, locals, bodyBuilder, etran); @@ -1220,7 +1220,7 @@ void CheckOperand(Expression operand) { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression } - + if (checkPostcondition != null) { checkPostcondition(builder, expr, true, resultDescription); } @@ -1356,7 +1356,7 @@ private void CheckWellformedComprehensionExpression(WFOptions wfOptions, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, bool checkRhs) { if (e.Exact) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index a5bcfeae717..493c8da1a38 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -37,7 +37,7 @@ public void Check(Function f) { var outParams = GetWellformednessProcedureOutParameters(f, etran); var requires = GetWellformednessProcedureRequires(f, etran); requires.AddRange(additionalRequires); - + // modifies $Heap var mod = new List { ordinaryEtran.HeapCastToIdentifierExpr, @@ -123,15 +123,15 @@ public void Check(Function f) { foreach (Expression p in f.Decreases.Expressions) { generator.CheckWellformed(p, new WFOptions(null, false), locals, builder, etran); } - + var implementationParameters = Bpl.Formal.StripWhereClauses(procedureParameters); CheckBodyAndEnsuresClauses(f, etran, locals, implementationParameters, builderInitializationArea, builder); - + if (generator.EmitImplementation(f.Attributes)) { var s0 = builderInitializationArea.Collect(f.tok); var s1 = builder.Collect(f.tok); var implBody = new StmtList(new List(s0.BigBlocks.Concat(s1.BigBlocks)), f.tok); - + // emit the impl only when there are proof obligations. QKeyValue kv = etran.TrAttributes(f.Attributes, null); var parameters = Concat(Concat(Bpl.Formal.StripWhereClauses(typeInParams), heapParameters), implementationParameters); @@ -150,8 +150,7 @@ public void Check(Function f) { } // TODO should be moved so its injected - private void ConcurrentAttributeCheck(Function f, ExpressionTranslator etran, BoogieStmtListBuilder builder) - { + private void ConcurrentAttributeCheck(Function f, ExpressionTranslator etran, BoogieStmtListBuilder builder) { // If the function is marked as {:concurrent}, check that the reads clause is empty. if (Attributes.Contains(f.Attributes, Attributes.ConcurrentAttributeName)) { var desc = new PODesc.ConcurrentFrameEmpty(f, "reads"); @@ -160,8 +159,7 @@ private void ConcurrentAttributeCheck(Function f, ExpressionTranslator etran, Bo } private void CheckBodyAndEnsuresClauses(Function f, ExpressionTranslator etran, List locals, List inParams, - BoogieStmtListBuilder builderInitializationArea, BoogieStmtListBuilder builder) - { + BoogieStmtListBuilder builderInitializationArea, BoogieStmtListBuilder builder) { builder.Add(new CommentCmd("Check body and ensures clauses")); // Generate: // if (*) { @@ -183,8 +181,7 @@ private void CheckBodyAndEnsuresClauses(Function f, ExpressionTranslator etran, private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslator etran, List parameters, - List locals, BoogieStmtListBuilder builderInitializationArea) - { + List locals, BoogieStmtListBuilder builderInitializationArea) { var selfCall = GetSelfCall(f, etran, parameters); var bodyCheckBuilder = new BoogieStmtListBuilder(generator, generator.options); bodyCheckBuilder.Add(new CommentCmd("Check Wfness of body and result subset type constraint")); @@ -239,8 +236,7 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat return bodyCheckBuilder; } - private Expr GetSelfCall(Function f, ExpressionTranslator etran, List parameters) - { + private Expr GetSelfCall(Function f, ExpressionTranslator etran, List parameters) { var funcId = new FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, generator.TrType(f.ResultType))); var args = new List(); foreach (var p in GetTypeParams(f)) { @@ -271,11 +267,10 @@ private Expr GetSelfCall(Function f, ExpressionTranslator etran, List return funcAppl; } - private BoogieStmtListBuilder GetPostCheckBuilder(Function f, ExpressionTranslator etran, List locals) - { + private BoogieStmtListBuilder GetPostCheckBuilder(Function f, ExpressionTranslator etran, List locals) { var postCheckBuilder = new BoogieStmtListBuilder(generator, generator.options); postCheckBuilder.Add(new CommentCmd("Check Wfness of postcondition and assume false")); - + // Assume the type returned by the call itself respects its type (this matters if the type is "nat", for example) var args = new List(); foreach (var p in GetTypeParams(f)) { @@ -311,7 +306,7 @@ private BoogieStmtListBuilder GetPostCheckBuilder(Function f, ExpressionTranslat var wh = generator.GetWhereClause(f.tok, funcAppl, f.ResultType, etran, NOALLOC); if (wh != null) { - postCheckBuilder.Add(TrAssumeCmd(f.tok, wh)); + postCheckBuilder.Add(TrAssumeCmd(f.tok, wh)); } // Now for the ensures clauses foreach (AttributedExpression p in f.Ens) { @@ -324,8 +319,7 @@ private BoogieStmtListBuilder GetPostCheckBuilder(Function f, ExpressionTranslat } private ExpressionTranslator GetExpressionTranslator(Function f, ExpressionTranslator ordinaryEtran, - out List additionalRequires, out List inParams_Heap) - { + out List additionalRequires, out List inParams_Heap) { ExpressionTranslator etran; additionalRequires = new(); inParams_Heap = new List(); @@ -337,7 +331,7 @@ private ExpressionTranslator GetExpressionTranslator(Function f, ExpressionTrans Expr prevHeap = new Bpl.IdentifierExpr(f.tok, prevHeapVar); Expr currHeap = new Bpl.IdentifierExpr(f.tok, currHeapVar); etran = new ExpressionTranslator(generator, generator.predef, currHeap, prevHeap, f); - + // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) var a0 = Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); var a1 = generator.HeapSucc(prevHeap, currHeap); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index f72b3b1a23c..9ea4e65d067 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -510,8 +510,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, - VarDeclPattern varDeclPattern) - { + VarDeclPattern varDeclPattern) { foreach (var dafnyLocal in varDeclPattern.LocalVars) { var boogieLocal = new Bpl.LocalVariable(dafnyLocal.Tok, new Bpl.TypedIdent(dafnyLocal.Tok, dafnyLocal.AssignUniqueName(currentDeclaration.IdGenerator), TrType(dafnyLocal.Type))); locals.Add(boogieLocal); @@ -542,7 +541,7 @@ private void TranslateVariableDeclaration(BoogieStmtListBuilder builder, List Expr.Eq(e, boogieTupleReference), "variable declaration")); } @@ -1782,7 +1781,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E // Translate receiver argument, if any Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver, dafnyReceiver.Type); - if (!method.IsStatic && !(method is Constructor)) { + if (!method.IsStatic && method is not Constructor) { if (bReceiver == null) { TrStmt_CheckWellformed(dafnyReceiver, builder, locals, etran, true); if (!(dafnyReceiver is ThisExpr)) { @@ -2802,7 +2801,7 @@ void TrStmtList(List stmts, BoogieStmtListBuilder builder, List locals, + void TrStmt_CheckWellformed(Expression expr, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, bool subsumption, bool lValueContext = false, CheckPostcondition checkPostcondition = null) { Contract.Requires(expr != null); Contract.Requires(builder != null); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy index 3881556b9e4..5f1a9808c16 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy @@ -40,11 +40,13 @@ method StatementExpressionAndSubsetLocal2() } predicate P(x: int) +method NeedsNat(x: nat) method NeedsP(x: int) requires P(x) method StatementExpressionAndPrecondition(x: int) { - NeedsP(assume P(x); x); // no error, since the statement expression can be used for the requires clause + NeedsNat(assume x > 0; x); // error, altough it could be nice not to have it + NeedsP(assume P(x); x); // error, since the statement expression can not be used for the requires clause } function StatementExpressionAssumeDoesNotEscapeLetBinding(): int diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect index 54d13e6d8a7..18b1c94a5b9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect @@ -1,5 +1,8 @@ statementExpressionScope.dfy(17,13): Error: this is the postcondition that could not be proved -statementExpressionScope.dfy(53,9): Error: assertion might not hold -statementExpressionScope.dfy(59,9): Error: assertion might not hold +statementExpressionScope.dfy(48,11): Error: value does not satisfy the subset constraints of 'nat' +statementExpressionScope.dfy(49,8): Error: a precondition for this call could not be proved +statementExpressionScope.dfy(44,31): Related location: this is the precondition that could not be proved +statementExpressionScope.dfy(55,9): Error: assertion might not hold +statementExpressionScope.dfy(61,9): Error: assertion might not hold -Dafny program verifier finished with 12 verified, 3 errors +Dafny program verifier finished with 15 verified, 5 errors From fb1ab6e7032e664e996b3cfe5a7e38632b5aebe2 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 30 Jul 2024 11:00:01 +0200 Subject: [PATCH 14/32] Remove unused code --- .../Synchronization/VerificationStatusTest.cs | 2 -- 1 file changed, 2 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs index 90ffba0e032..86803500d0e 100644 --- a/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs +++ b/Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs @@ -25,8 +25,6 @@ await SetUp(options => { Directory.CreateDirectory(directory); await File.WriteAllTextAsync(Path.Combine(directory, "dfyconfig.toml"), ""); await File.WriteAllTextAsync(Path.Combine(directory, "a.dfy"), "module A {}"); - // var project = CreateAndOpenTestDocument("", Path.Combine(directory, "dfyconfig.toml")); - // var a = CreateAndOpenTestDocument("module A {}", Path.Combine(directory, "a.dfy")); var b = CreateAndOpenTestDocument("module A.B { \n method Test() { assert true; }\n}", Path.Combine(directory, "b.dfy")); var methodHeader = new Position(1, 11); From 837f5871acf324f4f447b1c9af5bd3819005ff7a Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 31 Jul 2024 14:20:53 +0200 Subject: [PATCH 15/32] Add test-case --- .../TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy | 3 +++ .../LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy index a68e222f887..b22a059f208 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy @@ -55,6 +55,9 @@ method FunctionSubsetResult() { hide *; var x: nat := Natty(); assert x >= 0; // no error + + var y: int := Natty(); + assert y >= 0; // no error } function Natty(): nat { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect index fe0885c997b..56a5eda7b47 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect @@ -2,4 +2,4 @@ revealFunctions.dfy(15,12): Error: assertion might not hold revealFunctions.dfy(22,12): Error: assertion might not hold revealFunctions.dfy(49,21): Error: assertion might not hold -Dafny program verifier finished with 26 verified, 3 errors +Dafny program verifier finished with 25 verified, 3 errors From b460fb6b102bf7b06c8259043a9bc29ac31433ff Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 31 Jul 2024 15:24:05 +0200 Subject: [PATCH 16/32] Fixes --- .../BoogieGenerator.ExpressionWellformed.cs | 4 +- .../Verifier/BoogieGenerator.TrStatement.cs | 74 +------------------ 2 files changed, 4 insertions(+), 74 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index e732d95b827..d13335a60e9 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -1301,7 +1301,9 @@ private void CheckWellformedComprehensionExpression(WFOptions wfOptions, List { - CheckSubsetType(etran, innerBody, resultIe, rangeType, innerBuilder, adaptBox, prefix); + if (rangeType != null) { + CheckSubsetType(etran, innerBody, resultIe, rangeType, innerBuilder, adaptBox, prefix); + } }; CheckWellformedWithResult(body, newOptions, checkPostcondition, locals, b, comprehensionEtran); }); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 060df197c0f..ca4891ad0cf 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -386,28 +386,6 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, private void TranslateVariableDeclaration(BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, VarDeclPattern varDeclPattern) { - - // var s = (VarDeclPattern)stmt; - // foreach (var local in s.LocalVars) { - // Bpl.LocalVariable bvar = new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), TrType(local.Type))); - // locals.Add(bvar); - // var bIe = new Bpl.IdentifierExpr(bvar.tok, bvar); - // builder.Add(new Bpl.HavocCmd(local.Tok, new List { bIe })); - // Bpl.Expr wh = GetWhereClause(local.Tok, bIe, local.Type, etran, isAllocContext.Var(stmt.IsGhost, local)); - // if (wh != null) { - // builder.Add(TrAssumeCmd(local.Tok, wh)); - // } - // } - // var varNameGen = CurrentIdGenerator.NestedFreshIdGenerator("let#"); - // var pat = s.LHS; - // var rhs = s.RHS; - // var nm = varNameGen.FreshId(string.Format("#{0}#", 0)); - // var r = new Bpl.LocalVariable(pat.tok, new Bpl.TypedIdent(pat.tok, nm, TrType(rhs.Type))); - // locals.Add(r); - // var rIe = new Bpl.IdentifierExpr(rhs.tok, r); - // CheckWellformedWithResult(rhs, new WFOptions(null, false, false), rIe, pat.Expr.Type, locals, builder, etran, "variable declaration RHS"); - // CheckCasePatternShape(pat, rhs, rIe, rhs.tok, pat.Expr.Type, builder); - // builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, s.tok, pat.Expr, e => Expr.Eq(e, rIe), "variable declaration")); foreach (var dafnyLocal in varDeclPattern.LocalVars) { var boogieLocal = new Bpl.LocalVariable(dafnyLocal.Tok, new Bpl.TypedIdent(dafnyLocal.Tok, dafnyLocal.AssignUniqueName(currentDeclaration.IdGenerator), @@ -483,56 +461,6 @@ private void TrUpdateStmt(BoogieStmtListBuilder builder, List locals, } void TrVarDeclStmt(VarDeclStmt varDeclStmt, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran) { - // var newLocalIds = new List(); - // int i = 0; - // foreach (var local in s.Locals) { - // Bpl.Type varType = TrType(local.Type); - // Bpl.Expr wh = GetWhereClause(local.Tok, - // new Bpl.IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), varType), - // local.Type, etran, isAllocContext.Var(stmt.IsGhost, local)); - // // if needed, register definite-assignment tracking for this local - // var needDefiniteAssignmentTracking = s.Update == null || s.Update is AssignSuchThatStmt; - // if (s.Update is UpdateStmt) { - // // there is an initial assignment, but we need to look out for "*" being that assignment - // var us = (UpdateStmt)s.Update; - // if (i < us.Rhss.Count && us.Rhss[i] is HavocRhs) { - // needDefiniteAssignmentTracking = true; - // } - // } - // if (!local.Type.IsNonempty) { - // // This prevents generating an unsatisfiable where clause for possibly empty types - // needDefiniteAssignmentTracking = true; - // } - // if (needDefiniteAssignmentTracking) { - // var defassExpr = AddDefiniteAssignmentTracker(local, locals); - // if (wh != null && defassExpr != null) { - // // make the "where" expression be "defass ==> wh", because we don't want to assume anything - // // before the variable has been assigned (for a variable that needs definite-assignment tracking - // // in the first place) - // wh = BplImp(defassExpr, wh); - // } - // } - // // create the variable itself (now that "wh" may mention the definite-assignment tracker) - // Bpl.LocalVariable var = new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), varType, wh)); - // var.Attributes = etran.TrAttributes(local.Attributes, null); - // newLocalIds.Add(new Bpl.IdentifierExpr(local.Tok, var)); - // locals.Add(var); - // i++; - // } - // if (s.Update == null) { - // // it is necessary to do a havoc here in order to give the variable the correct allocation state - // builder.Add(new HavocCmd(s.Tok, newLocalIds)); - // } - // // processing of "assumption" variables happens after the variable is possibly havocked above - // foreach (var local in s.Locals) { - // if (Attributes.Contains(local.Attributes, "assumption")) { - // Bpl.Type varType = TrType(local.Type); - // builder.Add(new AssumeCmd(local.Tok, new Bpl.IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), varType), new QKeyValue(local.Tok, "assumption_variable_initialization", new List(), null))); - // } - // } - // if (s.Update != null) { - // TrStmt(s.Update, builder, locals, etran); - // } var newLocalIds = new List(); int i = 0; @@ -2704,7 +2632,7 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs }); var bRhs = etran.TrExpr(e.Expr); - builder.Add(TrAssumeCmd(e.tok, MkIs(bRhs, lhsType))); + builder.Add(TrAssumeCmd(e.tok, MkIs(bRhs, e.Expr.Type))); if (bGivenLhs != null) { Contract.Assert(bGivenLhs == bLhs); // box the RHS, then do the assignment From 4a5bc5c69b4ace84f851a4a552e6b9013c7a2b26 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 31 Jul 2024 15:33:14 +0200 Subject: [PATCH 17/32] Fix --- .../Verifier/BoogieGenerator.TrStatement.cs | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index ca4891ad0cf..f9c1134045f 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -2625,14 +2625,18 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs if (rhs is ExprRhs) { var e = (ExprRhs)rhs; + var bRhs = etran.TrExpr(e.Expr); + var cre = GetSubrangeCheck(tok, bRhs, e.Expr.Type, rhsTypeConstraint, e.Expr, null, out var desc, ""); TrStmt_CheckWellformed(e.Expr, builder, locals, etran, true, checkPostcondition: - (b, innerBody, adaptBoxing, prefix) => { - Bpl.Expr bRhs = etran.TrExpr(innerBody); - CheckSubrange(tok, bRhs, e.Expr.Type, rhsTypeConstraint, e.Expr, b); + (b, _, _, _) => { + if (cre != null) { + b.Add(Assert(tok, cre, desc)); + } }); + if (cre != null) { + builder.Add(new AssumeCmd(tok, cre)); //e.tok, MkIs(bRhs, rhsTypeConstraint))); + } - var bRhs = etran.TrExpr(e.Expr); - builder.Add(TrAssumeCmd(e.tok, MkIs(bRhs, e.Expr.Type))); if (bGivenLhs != null) { Contract.Assert(bGivenLhs == bLhs); // box the RHS, then do the assignment From d8fa9c569a933ecbdf328f857accda088255a567 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 8 Aug 2024 17:07:37 +0200 Subject: [PATCH 18/32] Fixes --- ...oogieGenerator.Functions.Wellformedness.cs | 49 +++++++++---------- 1 file changed, 24 insertions(+), 25 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index 9813631cfa6..960422e41c6 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -42,11 +42,25 @@ public void Check(Function f) { var mod = new List { ordinaryEtran.HeapCastToIdentifierExpr, }; + + var context = new BodyTranslationContext(f.ContainsHide); + var ens = new List(); + foreach (AttributedExpression ensures in f.Ens) { + var functionHeight = generator.currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); + var splits = new List(); + bool splitHappened /*we actually don't care*/ = generator.TrSplitExpr(context, ensures.E, splits, true, functionHeight, true, true, etran); + var (errorMessage, successMessage) = generator.CustomErrorMessage(ensures.Attributes); + foreach (var s in splits) { + if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, generator.currentModule)) { + generator.AddEnsures(ens, generator.EnsuresWithDependencies(s.Tok, false, ensures.E, s.E, errorMessage, successMessage, null)); + } + } + } var proc = new Procedure(f.tok, "CheckWellformed" + NameSeparator + f.FullSanitizedName, new List(), Concat(Concat(typeInParams, heapParameters), procedureParameters), outParams, - false, requires, mod, new List(), etran.TrAttributes(f.Attributes, null)); + false, requires, mod, ens, etran.TrAttributes(f.Attributes, null)); AddVerboseNameAttribute(proc, f.FullDafnyName, MethodTranslationKind.SpecWellformedness); generator.sink.AddTopLevelDeclaration(proc); @@ -57,7 +71,6 @@ public void Check(Function f) { Contract.Assert(proc.InParams.Count == typeInParams.Count + heapParameters.Count + procedureParameters.Count); // Changed the next line to strip from inParams instead of proc.InParams // They should be the same, but hence the added contract - var context = new BodyTranslationContext(f.ContainsHide); var locals = new List(); var builder = new BoogieStmtListBuilder(generator, generator.options, context); var builderInitializationArea = new BoogieStmtListBuilder(generator, generator.options, context); @@ -126,7 +139,7 @@ public void Check(Function f) { } var implementationParameters = Bpl.Formal.StripWhereClauses(procedureParameters); - CheckBodyAndEnsuresClauses(f, etran, locals, implementationParameters, builderInitializationArea, builder); + CheckBodyAndEnsuresClauseWellformedness(f, etran, locals, implementationParameters, builderInitializationArea, builder); if (generator.EmitImplementation(f.Attributes)) { var s0 = builderInitializationArea.Collect(f.tok); @@ -159,7 +172,7 @@ private void ConcurrentAttributeCheck(Function f, ExpressionTranslator etran, Bo } } - private void CheckBodyAndEnsuresClauses(Function f, ExpressionTranslator etran, List locals, List inParams, + private void CheckBodyAndEnsuresClauseWellformedness(Function f, ExpressionTranslator etran, List locals, List inParams, BoogieStmtListBuilder builderInitializationArea, BoogieStmtListBuilder builder) { builder.Add(new CommentCmd("Check body and ensures clauses")); // Generate: @@ -190,8 +203,8 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat if (f.Body != null && generator.RevealedInScope(f)) { var bodyCheckDelayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, bodyCheckBuilder); bodyCheckDelayer.DoWithDelayedReadsChecks(false, wfo => { - CheckPostcondition checkPostcondition = (b, innerBody, adaptBoxing, prefix) => { - generator.CheckSubsetType(etran, innerBody, selfCall, f.Body.Type, b, adaptBoxing, prefix); + void CheckPostcondition(BoogieStmtListBuilder innerBuilder, Expression innerBody, bool adaptBoxing, string prefix) { + generator.CheckSubsetType(etran, innerBody, selfCall, f.Body.Type, innerBuilder, adaptBoxing, prefix); // Contract.Assert(f.ResultType != null); // var bResult = etran.TrExpr(innerBody); // generator.CheckSubrange(f.Body.tok, bResult, f.Body.Type, f.ResultType, f.Body, b); @@ -205,29 +218,14 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat if (f.Result != null) { var cmd = TrAssumeCmd(f.tok, Expr.Eq(selfCall, generator.TrVar(f.tok, f.Result))); generator.proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); - b.Add(cmd); + innerBuilder.Add(cmd); } + } - var context = new BodyTranslationContext(f.ContainsHide); - foreach (AttributedExpression e in f.Ens) { - var functionHeight = generator.currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); - var splits = new List(); - bool splitHappened /*we actually don't care*/ = - generator.TrSplitExpr(context, e.E, splits, true, functionHeight, true, true, etran); - var (errorMessage, successMessage) = generator.CustomErrorMessage(e.Attributes); - foreach (var s in splits) { - if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, generator.currentModule)) { - var ensures = - generator.EnsuresWithDependencies(s.Tok, false, e.E, s.E, errorMessage, successMessage, null); - b.Add(new AssertCmd(ensures.tok, ensures.Condition, ensures.Description, - ensures.Attributes)); - } - } - } - }; - generator.CheckWellformedWithResult(f.Body, wfo, checkPostcondition, locals, bodyCheckBuilder, etran, "function call result"); + generator.CheckWellformedWithResult(f.Body, wfo, CheckPostcondition, locals, bodyCheckBuilder, etran, "function call result"); }); + // Enforce 'older' conditions var (olderParameterCount, olderCondition) = generator.OlderCondition(f, selfCall, parameters); if (olderParameterCount != 0) { @@ -235,6 +233,7 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat new PODesc.IsOlderProofObligation(olderParameterCount, f.Ins.Count + (f.IsStatic ? 0 : 1)))); } } + bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Expr.False)); return bodyCheckBuilder; } From bbe156c1a936debe9eae1b77e24401f954b472e6 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 12:33:57 +0200 Subject: [PATCH 19/32] Add testcase for ensures clause on function reporting --- .../ast/functions/ensuresReporting.dfy | 0 .../ast/functions/ensuresReporting.dfy.expect | 29 +++++++++++++++++++ 2 files changed, 29 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy new file mode 100644 index 00000000000..e69de29bb2d diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect new file mode 100644 index 00000000000..0aea0607093 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect @@ -0,0 +1,29 @@ +// RUN: ! %verify %s &> "%t" +// RUN: %diff "%s.expect" "%t" + +function ElseError(x: int): int + ensures ElseErorr(x) == 0 +{ + if x == 0 then + 0 + else + 1 +} +function ThenError(x: int): int + ensures ThenError(x) == 0 +{ + if x == 0 then + 0 + else + 1 +} + +function CaseError(x: int): int + ensures CaseError(x) == 1 +{ + match x { + case 0 => 0 + case 1 => 1 + case 2 => 2 + } +} \ No newline at end of file From fffe0ee72eb12fac54e7e26587a216b3605f4ca6 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 12:35:32 +0200 Subject: [PATCH 20/32] Fixes --- ...oogieGenerator.Functions.Wellformedness.cs | 2 +- .../ast/functions/ensuresReporting.dfy | 29 +++++++++++++++ .../ast/functions/ensuresReporting.dfy.expect | 35 ++++--------------- .../LitTest/dafny0/Definedness.dfy.expect | 4 +-- .../dafny0/FunctionSpecifications.dfy.expect | 8 ++--- .../LitTest/dafny0/Refinement.dfy.expect | 2 +- 6 files changed, 44 insertions(+), 36 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index 960422e41c6..2d38e8e7887 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -220,11 +220,11 @@ void CheckPostcondition(BoogieStmtListBuilder innerBuilder, Expression innerBody generator.proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); innerBuilder.Add(cmd); } + innerBuilder.Add(new ReturnCmd(innerBody.Tok)); } generator.CheckWellformedWithResult(f.Body, wfo, CheckPostcondition, locals, bodyCheckBuilder, etran, "function call result"); }); - // Enforce 'older' conditions var (olderParameterCount, olderCondition) = generator.OlderCondition(f, selfCall, parameters); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy index e69de29bb2d..299b8bfb5d9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy @@ -0,0 +1,29 @@ +// RUN: ! %verify %s &> "%t" +// RUN: %diff "%s.expect" "%t" + +function ElseError(x: int): int + ensures ElseError(x) == 0 +{ + if x == 0 then + 0 + else + 1 // error +} +function ThenError(x: int): int + ensures ThenError(x) == 0 +{ + if x == 0 then + 1 // error + else + 0 +} + +function CaseError(x: int): int + ensures CaseError(x) == 1 +{ + match x { + case 0 => 1 + case 1 => 0 // error + case _ => 1 + } +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect index 0aea0607093..c5df2f77b15 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect @@ -1,29 +1,8 @@ -// RUN: ! %verify %s &> "%t" -// RUN: %diff "%s.expect" "%t" +ensuresReporting.dfy(10,4): Error: a postcondition could not be proved on this return path +ensuresReporting.dfy(5,23): Related location: this is the postcondition that could not be proved +ensuresReporting.dfy(16,4): Error: a postcondition could not be proved on this return path +ensuresReporting.dfy(13,23): Related location: this is the postcondition that could not be proved +ensuresReporting.dfy(26,14): Error: a postcondition could not be proved on this return path +ensuresReporting.dfy(22,23): Related location: this is the postcondition that could not be proved -function ElseError(x: int): int - ensures ElseErorr(x) == 0 -{ - if x == 0 then - 0 - else - 1 -} -function ThenError(x: int): int - ensures ThenError(x) == 0 -{ - if x == 0 then - 0 - else - 1 -} - -function CaseError(x: int): int - ensures CaseError(x) == 1 -{ - match x { - case 0 => 0 - case 1 => 1 - case 2 => 2 - } -} \ No newline at end of file +Dafny program verifier finished with 0 verified, 3 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Definedness.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Definedness.dfy.expect index 22b363ea16b..9a6e1e5b3d8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Definedness.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Definedness.dfy.expect @@ -45,10 +45,10 @@ Definedness.dfy(196,18): Error: possible division by zero Definedness.dfy(196,22): Error: this loop invariant could not be proved on entry Related message: loop invariant violation Definedness.dfy(196,27): Error: possible division by zero -Definedness.dfy(215,15): Error: a postcondition could not be proved on this return path +Definedness.dfy(219,2): Error: a postcondition could not be proved on this return path Definedness.dfy(217,45): Related location: this is the postcondition that could not be proved Definedness.dfy(224,21): Error: target object might be null -Definedness.dfy(237,15): Error: a postcondition could not be proved on this return path +Definedness.dfy(242,2): Error: a postcondition could not be proved on this return path Definedness.dfy(240,23): Related location: this is the postcondition that could not be proved Dafny program verifier finished with 9 verified, 37 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy.expect index 6bc52c3a0c8..b20a56e2f1c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/FunctionSpecifications.dfy.expect @@ -1,15 +1,15 @@ -FunctionSpecifications.dfy(35,24): Error: a postcondition could not be proved on this return path +FunctionSpecifications.dfy(35,45): Error: a postcondition could not be proved on this return path FunctionSpecifications.dfy(31,12): Related location: this is the postcondition that could not be proved -FunctionSpecifications.dfy(45,2): Error: a postcondition could not be proved on this return path +FunctionSpecifications.dfy(45,16): Error: a postcondition could not be proved on this return path FunctionSpecifications.dfy(40,23): Related location: this is the postcondition that could not be proved FunctionSpecifications.dfy(61,10): Error: cannot prove termination; try supplying a decreases clause -FunctionSpecifications.dfy(68,15): Error: a postcondition could not be proved on this return path +FunctionSpecifications.dfy(71,4): Error: a postcondition could not be proved on this return path FunctionSpecifications.dfy(69,21): Related location: this is the postcondition that could not be proved FunctionSpecifications.dfy(117,22): Error: assertion might not hold FunctionSpecifications.dfy(120,22): Error: assertion might not hold FunctionSpecifications.dfy(135,26): Error: assertion might not hold FunctionSpecifications.dfy(139,26): Error: assertion might not hold -FunctionSpecifications.dfy(144,25): Error: a postcondition could not be proved on this return path +FunctionSpecifications.dfy(148,4): Error: a postcondition could not be proved on this return path FunctionSpecifications.dfy(146,28): Related location: this is the postcondition that could not be proved FunctionSpecifications.dfy(155,2): Error: decreases clause might not decrease FunctionSpecifications.dfy(162,2): Error: decreases clause might not decrease diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Refinement.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Refinement.dfy.expect index fa7229dd7ca..eba5fb51b86 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Refinement.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Refinement.dfy.expect @@ -22,7 +22,7 @@ Refinement.dfy[B](15,4): Error: a postcondition could not be proved on this retu Refinement.dfy(33,19): Related location: this is the postcondition that could not be proved Refinement.dfy(69,15): Error: assertion might not hold Refinement.dfy(80,16): Error: assertion might not hold -Refinement.dfy(99,17): Error: a postcondition could not be proved on this return path +Refinement.dfy(100,4): Error: a postcondition could not be proved on this return path Refinement.dfy(78,14): Related location: this is the postcondition that could not be proved Refinement.dfy(102,2): Error: a postcondition could not be proved on this return path Refinement.dfy(83,14): Related location: this is the postcondition that could not be proved From e2514f55bffef2ffc7197d3774155cfb8c40ef62 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 13:14:43 +0200 Subject: [PATCH 21/32] Fix witness expression proofs --- .../Verifier/BoogieGenerator.Types.cs | 88 +++++++++++-------- .../ast/functions/ensuresReporting.dfy | 7 ++ .../ast/functions/ensuresReporting.dfy.expect | 4 +- 3 files changed, 63 insertions(+), 36 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs index 7ec946ea67e..5165d55b670 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs @@ -1486,12 +1486,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { // } // check well-formedness of the constraint (including termination, and delayed reads checks) - var constraintCheckBuilder = new BoogieStmtListBuilder(this, options, context); - var builderInitializationArea = new BoogieStmtListBuilder(this, options, context); - var delayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, constraintCheckBuilder); - delayer.DoWithDelayedReadsChecks(false, wfo => { - CheckWellformedAndAssume(decl.Constraint, wfo, locals, constraintCheckBuilder, etran, "predicate subtype constraint"); - }); + var builderInitializationArea = CheckConstraintWellformedness(decl, context, etran, locals, builder); // Check that the type is inhabited. // Note, the possible witness in this check should be coordinated with the compiler, so the compiler knows how to do the initialization @@ -1502,15 +1497,22 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { // check well-formedness of the witness expression (including termination, and reads checks) var ghostCodeContext = codeContext; codeContext = decl.WitnessKind == SubsetTypeDecl.WKind.Compiled ? new CallableWrapper(decl, false) : ghostCodeContext; - CheckWellformed(decl.Witness, new WFOptions(null, true), locals, witnessCheckBuilder, etran); + CheckWellformedWithResult(decl.Witness, new WFOptions(null, true), (innerBuilder, innerWitness, _, _) => { + // check that the witness is assignable to the type of the given bound variable + if (decl is SubsetTypeDecl) { + // Note, for new-types, this has already been checked by CheckWellformed. + CheckResultToBeInType(decl.Witness.tok, innerWitness, decl.Var.Type, locals, innerBuilder, etran); + } + + // check that the witness expression checks out + witnessExpr = Substitute(decl.Constraint, decl.Var, innerWitness); + witnessExpr.tok = decl.Witness.Tok; + var desc = new PODesc.WitnessCheck(witnessString, witnessExpr); + + SplitAndAssertExpression(innerBuilder, witnessExpr, etran, context, desc); + }, locals, witnessCheckBuilder, etran); codeContext = ghostCodeContext; - // check that the witness is assignable to the type of the given bound variable - if (decl is SubsetTypeDecl) { - // Note, for new-types, this has already been checked by CheckWellformed. - CheckResultToBeInType(decl.Witness.tok, decl.Witness, decl.Var.Type, locals, witnessCheckBuilder, etran); - } - // check that the witness expression checks out - witnessExpr = Substitute(decl.Constraint, decl.Var, decl.Witness); + } else if (decl.WitnessKind == SubsetTypeDecl.WKind.CompiledZero) { var witness = Zero(decl.tok, decl.Var.Type); if (witness == null) { @@ -1521,29 +1523,13 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { witnessString = Printer.ExprToString(options, witness); CheckResultToBeInType(decl.tok, witness, decl.Var.Type, locals, witnessCheckBuilder, etran, $"trying witness {witnessString}: "); witnessExpr = Substitute(decl.Constraint, decl.Var, witness); + + witnessExpr.tok = decl.tok; + var desc = new PODesc.WitnessCheck(witnessString, witnessExpr); + SplitAndAssertExpression(witnessCheckBuilder, witnessExpr, etran, context, desc); } } - if (witnessExpr != null) { - var witnessCheckTok = decl.Witness != null ? GetToken(decl.Witness) : decl.tok; - witnessCheckBuilder.Add(new Bpl.AssumeCmd(witnessCheckTok, etran.CanCallAssumption(witnessExpr))); - var witnessCheck = etran.TrExpr(witnessExpr); - - bool splitHappened; - var ss = TrSplitExpr(context, witnessExpr, etran, true, out splitHappened); - var desc = new PODesc.WitnessCheck(witnessString, witnessExpr); - if (!splitHappened) { - witnessCheckBuilder.Add(Assert(witnessCheckTok, etran.TrExpr(witnessExpr), desc)); - } else { - foreach (var split in ss) { - if (split.IsChecked) { - var tok = witnessCheckTok is IToken t ? new NestedToken(t, split.Tok) : witnessCheckTok; - witnessCheckBuilder.Add(AssertNS(tok, split.E, desc)); - } - } - } - } - - builder.Add(new Bpl.IfCmd(decl.tok, null, constraintCheckBuilder.Collect(decl.tok), null, witnessCheckBuilder.Collect(decl.tok))); + PathAsideBlock(decl.Tok, witnessCheckBuilder, builder); var s0 = builderInitializationArea.Collect(decl.tok); var s1 = builder.Collect(decl.tok); @@ -1563,4 +1549,36 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { isAllocContext = null; Reset(); } + + private void SplitAndAssertExpression(BoogieStmtListBuilder witnessCheckBuilder, Expression witnessExpr, + ExpressionTranslator etran, BodyTranslationContext context, PODesc.WitnessCheck desc) + { + witnessCheckBuilder.Add(new Bpl.AssumeCmd(witnessExpr.tok, etran.CanCallAssumption(witnessExpr))); + var witnessCheck = etran.TrExpr(witnessExpr); + + var ss = TrSplitExpr(context, witnessExpr, etran, true, out var splitHappened); + if (!splitHappened) { + witnessCheckBuilder.Add(Assert(witnessExpr.tok, etran.TrExpr(witnessExpr), desc)); + } else { + foreach (var split in ss) { + if (split.IsChecked) { + var tok = witnessExpr.tok is { } t ? new NestedToken(t, split.Tok) : witnessExpr.tok; + witnessCheckBuilder.Add(AssertNS(tok, split.E, desc)); + } + } + } + } + + private BoogieStmtListBuilder CheckConstraintWellformedness(RedirectingTypeDecl decl, BodyTranslationContext context, + ExpressionTranslator etran, List locals, BoogieStmtListBuilder builder) + { + var constraintCheckBuilder = new BoogieStmtListBuilder(this, options, context); + var builderInitializationArea = new BoogieStmtListBuilder(this, options, context); + var delayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, constraintCheckBuilder); + delayer.DoWithDelayedReadsChecks(false, wfo => { + CheckWellformedAndAssume(decl.Constraint, wfo, locals, constraintCheckBuilder, etran, "predicate subtype constraint"); + }); + PathAsideBlock(decl.Tok, constraintCheckBuilder, builder); + return builderInitializationArea; + } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy index 299b8bfb5d9..ef31e255dbb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy @@ -26,4 +26,11 @@ function CaseError(x: int): int case 1 => 0 // error case _ => 1 } +} + +function LetError(x: int): int + ensures LetError(x) == 1 +{ + var r := 3; + r } \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect index c5df2f77b15..8eaf561c25b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect @@ -4,5 +4,7 @@ ensuresReporting.dfy(16,4): Error: a postcondition could not be proved on this r ensuresReporting.dfy(13,23): Related location: this is the postcondition that could not be proved ensuresReporting.dfy(26,14): Error: a postcondition could not be proved on this return path ensuresReporting.dfy(22,23): Related location: this is the postcondition that could not be proved +ensuresReporting.dfy(35,2): Error: a postcondition could not be proved on this return path +ensuresReporting.dfy(32,22): Related location: this is the postcondition that could not be proved -Dafny program verifier finished with 0 verified, 3 errors +Dafny program verifier finished with 0 verified, 4 errors From 813a5fec1b504716d5e9a5db86303d92534667d2 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 13:17:21 +0200 Subject: [PATCH 22/32] Fix expect file --- .../git-issues/git-issue-1180b.dfy.expect | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1180b.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1180b.dfy.expect index e7c31658280..531ba00737a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1180b.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1180b.dfy.expect @@ -1,40 +1,40 @@ -git-issue-1180b.dfy(28,15): Error: a postcondition could not be proved on this return path +git-issue-1180b.dfy(28,32): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(12,21): Related location: this is the postcondition that could not be proved git-issue-1180b.dfy(29,40): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(15,18): Related location: this is the postcondition that could not be proved -git-issue-1180b.dfy(34,15): Error: a postcondition could not be proved on this return path +git-issue-1180b.dfy(34,32): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(12,21): Related location: this is the postcondition that could not be proved git-issue-1180b.dfy(35,40): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(15,18): Related location: this is the postcondition that could not be proved -git-issue-1180b.dfy(40,15): Error: a postcondition could not be proved on this return path +git-issue-1180b.dfy(40,32): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(12,21): Related location: this is the postcondition that could not be proved git-issue-1180b.dfy(41,40): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(15,18): Related location: this is the postcondition that could not be proved -git-issue-1180b.dfy(46,15): Error: a postcondition could not be proved on this return path +git-issue-1180b.dfy(46,32): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(12,21): Related location: this is the postcondition that could not be proved git-issue-1180b.dfy(47,40): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(15,18): Related location: this is the postcondition that could not be proved -git-issue-1180b.dfy(56,15): Error: a postcondition could not be proved on this return path +git-issue-1180b.dfy(56,32): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(12,21): Related location: this is the postcondition that could not be proved git-issue-1180b.dfy(57,40): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(15,18): Related location: this is the postcondition that could not be proved -git-issue-1180b.dfy(63,15): Error: a postcondition could not be proved on this return path +git-issue-1180b.dfy(63,32): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(12,21): Related location: this is the postcondition that could not be proved git-issue-1180b.dfy(64,40): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(15,18): Related location: this is the postcondition that could not be proved -git-issue-1180b.dfy(83,15): Error: a postcondition could not be proved on this return path +git-issue-1180b.dfy(83,32): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(75,21): Related location: this is the postcondition that could not be proved git-issue-1180b.dfy(84,40): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(78,18): Related location: this is the postcondition that could not be proved -git-issue-1180b.dfy(103,15): Error: a postcondition could not be proved on this return path +git-issue-1180b.dfy(103,32): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(95,21): Related location: this is the postcondition that could not be proved git-issue-1180b.dfy(104,40): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(98,18): Related location: this is the postcondition that could not be proved -git-issue-1180b.dfy(123,15): Error: a postcondition could not be proved on this return path +git-issue-1180b.dfy(123,32): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(115,21): Related location: this is the postcondition that could not be proved git-issue-1180b.dfy(124,40): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(118,18): Related location: this is the postcondition that could not be proved -git-issue-1180b.dfy(143,15): Error: a postcondition could not be proved on this return path +git-issue-1180b.dfy(143,32): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(135,21): Related location: this is the postcondition that could not be proved git-issue-1180b.dfy(144,40): Error: a postcondition could not be proved on this return path git-issue-1180b.dfy(138,18): Related location: this is the postcondition that could not be proved From 50319de01484c64f8d57dec103ff5a04b0a72306 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 14:09:15 +0200 Subject: [PATCH 23/32] Fix subset type check --- .../BoogieGenerator.Functions.Wellformedness.cs | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index 2d38e8e7887..5a8018c5261 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -204,17 +204,7 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat var bodyCheckDelayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, bodyCheckBuilder); bodyCheckDelayer.DoWithDelayedReadsChecks(false, wfo => { void CheckPostcondition(BoogieStmtListBuilder innerBuilder, Expression innerBody, bool adaptBoxing, string prefix) { - generator.CheckSubsetType(etran, innerBody, selfCall, f.Body.Type, innerBuilder, adaptBoxing, prefix); - // Contract.Assert(f.ResultType != null); - // var bResult = etran.TrExpr(innerBody); - // generator.CheckSubrange(f.Body.tok, bResult, f.Body.Type, f.ResultType, f.Body, b); - // - // bodyCheckBuilder.Add(generator.TrAssumeCmdWithDependenciesAndExtend(etran, f.Body.tok, f.Body, - // e => Bpl.Expr.Eq(selfCall, generator.AdaptBoxing(f.Body.tok, e, f.Body.Type, f.ResultType)), - // prefix)); - // bodyCheckBuilder.Add(TrAssumeCmd(f.Body.tok, etran.CanCallAssumption(f.Body))); - // bodyCheckBuilder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); - // bodyCheckBuilder.Add(TrAssumeCmd(f.Body.tok, generator.MkIs(selfCall, f.ResultType))); + generator.CheckSubsetType(etran, innerBody, selfCall, f.ResultType, innerBuilder, adaptBoxing, prefix); if (f.Result != null) { var cmd = TrAssumeCmd(f.tok, Expr.Eq(selfCall, generator.TrVar(f.tok, f.Result))); generator.proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); From 597000c6c9354f8d0745d6601129ce3bc3b4bcc3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 14:33:06 +0200 Subject: [PATCH 24/32] Cleanup WF check for StmtExpr, to reduce nesting --- .../BoogieGenerator.ExpressionWellformed.cs | 30 ++++++++++++++----- .../LitTest/git-issues/git-issue-3804c.dfy | 6 ++-- 2 files changed, 26 insertions(+), 10 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index d13335a60e9..2bb5d48fbbb 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -1144,9 +1144,7 @@ void CheckOperand(Expression operand) { break; } case StmtExpr stmtExpr: - var bodyBuilder = new BoogieStmtListBuilder(this, builder.Options, builder.Context); - CheckWellformedStmtExpr(stmtExpr, wfOptions, checkPostcondition, locals, bodyBuilder, etran); - PathAsideBlock(stmtExpr.tok, bodyBuilder, builder); + CheckWellformedStmtExpr(stmtExpr, wfOptions, checkPostcondition, locals, builder, etran); checkPostcondition = null; break; case ITEExpr iteExpr: { @@ -1422,18 +1420,36 @@ private void TrMatchExpr(MatchExpr me, WFOptions wfOptions, CheckPostcondition c private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions wfOptions, CheckPostcondition checkPostcondition, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { + + var bodyBuilder = new BoogieStmtListBuilder(this, builder.Options, builder.Context); + + var statements = new List() { stmtExpr.S }; + Expression expression = stmtExpr.E; + while (expression is StmtExpr nestedStmtExpr) { + statements.Add(nestedStmtExpr.S); + expression = nestedStmtExpr.E; + } + // If we're inside an "old" expression, then "etran" will know how to translate // expressions. However, here, we're also having to translate e.S, which is a // Statement. Since statement translation (in particular, translation of CallStmt's) // work directly on the global variable $Heap, we temporarily change its value here. if (etran.UsesOldHeap) { - BuildWithHeapAs(stmtExpr.S.Tok, etran.HeapExpr, "StmtExpr#", locals, builder, - () => TrStmt(stmtExpr.S, builder, locals, etran)); + BuildWithHeapAs(stmtExpr.S.Tok, etran.HeapExpr, "StmtExpr#", locals, bodyBuilder, + () => { + foreach (var statement in statements) { + TrStmt(statement, bodyBuilder, locals, etran); + } + }); } else { - TrStmt(stmtExpr.S, builder, locals, etran); + foreach (var statement in statements) { + TrStmt(statement, bodyBuilder, locals, etran); + } } - CheckWellformedWithResult(stmtExpr.E, wfOptions, checkPostcondition, locals, builder, etran, "statement expression result"); + CheckWellformedWithResult(expression, wfOptions, checkPostcondition, locals, bodyBuilder, etran, "statement expression result"); + + PathAsideBlock(stmtExpr.tok, bodyBuilder, builder); } /// diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804c.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804c.dfy index cbf89f9392c..ec453e7ad8d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804c.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804c.dfy @@ -8,7 +8,7 @@ function Test(x: bool): int { assert p1: x ==> P(1) by { reveal r; } assert p2: !x ==> P(2) by { reveal r; } - var x := + var y := match x { case true => assert p11: P(1) by { reveal p1; } @@ -21,6 +21,6 @@ function Test(x: bool): int assert P(2) by { reveal p21; } // p21 can be revealed and this assertion is visible outside. 2 }; - assert P(x); - x + assert P(y); + y } \ No newline at end of file From 243c5478325da73ad8ccd9ad5e522265c2795522 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 14:44:14 +0200 Subject: [PATCH 25/32] Refactoring --- .../BoogieGenerator.ExpressionWellformed.cs | 28 ++++++++++--------- 1 file changed, 15 insertions(+), 13 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 2bb5d48fbbb..6c4e3758c3b 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -1532,14 +1532,16 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, CheckPostc for (int i = 0; i < e.LHSs.Count; i++) { var pat = e.LHSs[i]; var rhs = e.RHSs[i]; - var nm = varNameGen.FreshId(string.Format("#{0}#", i)); + var nm = varNameGen.FreshId($"#{i}#"); var r = new Bpl.LocalVariable(pat.tok, new Bpl.TypedIdent(pat.tok, nm, TrType(pat.Expr.Type))); locals.Add(r); var rIe = new Bpl.IdentifierExpr(rhs.tok, r); - CheckPostcondition checkPostconditionForLhs = (innerBuilder, body, adaptBoxing, prefix) => { + + void CheckPostconditionForRhs(BoogieStmtListBuilder innerBuilder, Expression body, bool adaptBoxing, string prefix) { CheckSubsetType(etran, body, rIe, pat.Expr.Type, innerBuilder, adaptBoxing, prefix); - }; - CheckWellformedWithResult(e.RHSs[i], wfOptions, checkPostconditionForLhs, locals, builder, etran, "let expression binding RHS well-formed"); + } + + CheckWellformedWithResult(e.RHSs[i], wfOptions, CheckPostconditionForRhs, locals, builder, etran, "let expression binding RHS well-formed"); CheckCasePatternShape(pat, rhs, rIe, rhs.tok, pat.Expr.Type, builder); var substExpr = Substitute(pat.Expr, null, substMap); builder.Add(TrAssumeCmdWithDependenciesAndExtend(etran, e.tok, substExpr, e => Bpl.Expr.Eq(e, rIe), "let expression binding")); @@ -1578,17 +1580,17 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, CheckPostc var letBody = Substitute(e.Body, null, substMap); CheckWellformed(letBody, wfOptions, locals, builder, etran); if (e.Constraint_Bounds != null) { - var substMap_prime = SetupBoundVarsAsLocals(lhsVars, builder, locals, etran); - var nonGhostMap_prime = new Dictionary(); + var substMapPrime = SetupBoundVarsAsLocals(lhsVars, builder, locals, etran); + var nonGhostMapPrime = new Dictionary(); foreach (BoundVar bv in lhsVars) { - nonGhostMap_prime.Add(bv, bv.IsGhost ? substMap[bv] : substMap_prime[bv]); + nonGhostMapPrime.Add(bv, bv.IsGhost ? substMap[bv] : substMapPrime[bv]); } - var rhs_prime = Substitute(e.RHSs[0], null, nonGhostMap_prime); - var letBody_prime = Substitute(e.Body, null, nonGhostMap_prime); - builder.Add(TrAssumeCmd(e.tok, etran.CanCallAssumption(rhs_prime))); - builder.Add(TrAssumeCmdWithDependencies(etran, e.tok, rhs_prime, "assign-such-that constraint")); - builder.Add(TrAssumeCmd(e.tok, etran.CanCallAssumption(letBody_prime))); - var eq = Expression.CreateEq(letBody, letBody_prime, e.Body.Type); + var rhsPrime = Substitute(e.RHSs[0], null, nonGhostMapPrime); + var letBodyPrime = Substitute(e.Body, null, nonGhostMapPrime); + builder.Add(TrAssumeCmd(e.tok, etran.CanCallAssumption(rhsPrime))); + builder.Add(TrAssumeCmdWithDependencies(etran, e.tok, rhsPrime, "assign-such-that constraint")); + builder.Add(TrAssumeCmd(e.tok, etran.CanCallAssumption(letBodyPrime))); + var eq = Expression.CreateEq(letBody, letBodyPrime, e.Body.Type); builder.Add(Assert(GetToken(e), etran.TrExpr(eq), new PODesc.LetSuchThatUnique(e.RHSs[0], e.BoundVars.ToList()))); } From aa43a4fc9c608bc99e503a0948a66a050c8d8de3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 16:10:48 +0200 Subject: [PATCH 26/32] Fix bug --- .../BoogieGenerator.ExpressionWellformed.cs | 20 ++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 6c4e3758c3b..f24bf73bf20 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -678,12 +678,6 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, builder.Add(new Bpl.CommentCmd("assume allocatedness for receiver argument to function")); builder.Add(TrAssumeCmd(e.Receiver.tok, MkIsAllocBox(BoxIfNecessary(e.Receiver.tok, etran.TrExpr(e.Receiver), e.Receiver.Type), et, etran.HeapExpr))); } - // check well-formedness of the other parameters - foreach (Expression arg in e.Args) { - if (!(arg is DefaultValueExpression)) { - CheckWellformed(arg, wfOptions, locals, builder, etran); - } - } // create a local variable for each formal parameter, and assign each actual parameter to the corresponding local Dictionary substMap = new Dictionary(); Dictionary directSubstMap = new Dictionary(); @@ -694,14 +688,22 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Type et = p.Type.Subst(e.GetTypeArgumentSubstitutions()); LocalVariable local = new LocalVariable(p.RangeToken, "##" + p.Name, et, p.IsGhost); local.type = local.SyntacticType; // resolve local here - IdentifierExpr ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator)); - ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here + var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator)) + { + Var = local + }; + ie.Type = ie.Var.Type; // resolve ie here substMap.Add(p, ie); locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), TrType(local.Type)))); Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified? Expression ee = e.Args[i]; directSubstMap.Add(p, ee); - CheckSubrange(ee.tok, etran.TrExpr(ee), ee.Type, et, ee, builder); + + if (!(ee is DefaultValueExpression)) { + CheckWellformedWithResult(ee, wfOptions, (innerBuilder, innerBody, _, _) => { + CheckSubrange(innerBody.tok, etran.TrExpr(innerBody), ee.Type, et, ee, innerBuilder); + }, locals, builder, etran); + } Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, AdaptBoxing(p.tok, etran.TrExpr(ee), cce.NonNull(ee.Type), et)); builder.Add(cmd); if (!etran.UsesOldHeap) { From 0d08aefc15913461f21e78d728563a6e4d5d499c Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 17:05:49 +0200 Subject: [PATCH 27/32] Fixes --- ...oogieGenerator.Functions.Wellformedness.cs | 40 ++++++++++--------- .../func-depth-fail.dfy.expect | 2 +- 2 files changed, 23 insertions(+), 19 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index 5a8018c5261..cc613f79275 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -201,27 +201,31 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat var bodyCheckBuilder = new BoogieStmtListBuilder(generator, generator.options, context); bodyCheckBuilder.Add(new CommentCmd("Check Wfness of body and result subset type constraint")); if (f.Body != null && generator.RevealedInScope(f)) { - var bodyCheckDelayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, bodyCheckBuilder); - bodyCheckDelayer.DoWithDelayedReadsChecks(false, wfo => { - void CheckPostcondition(BoogieStmtListBuilder innerBuilder, Expression innerBody, bool adaptBoxing, string prefix) { - generator.CheckSubsetType(etran, innerBody, selfCall, f.ResultType, innerBuilder, adaptBoxing, prefix); - if (f.Result != null) { - var cmd = TrAssumeCmd(f.tok, Expr.Eq(selfCall, generator.TrVar(f.tok, f.Result))); - generator.proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); - innerBuilder.Add(cmd); - } - innerBuilder.Add(new ReturnCmd(innerBody.Tok)); + var doReadsChecks = etran.readsFrame != null; + var wfo = new WFOptions(null, doReadsChecks, doReadsChecks, false); + + void CheckPostcondition(BoogieStmtListBuilder innerBuilder, Expression innerBody, bool adaptBoxing, string prefix) { + generator.CheckSubsetType(etran, innerBody, selfCall, f.ResultType, innerBuilder, adaptBoxing, prefix); + if (f.Result != null) { + var cmd = TrAssumeCmd(f.tok, Expr.Eq(selfCall, generator.TrVar(f.tok, f.Result))); + generator.proofDependencies?.AddProofDependencyId(cmd, f.tok, new FunctionDefinitionDependency(f)); + innerBuilder.Add(cmd); + } + if (doReadsChecks) { + wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, innerBuilder); } - - generator.CheckWellformedWithResult(f.Body, wfo, CheckPostcondition, locals, bodyCheckBuilder, etran, "function call result"); - }); - // Enforce 'older' conditions - var (olderParameterCount, olderCondition) = generator.OlderCondition(f, selfCall, parameters); - if (olderParameterCount != 0) { - bodyCheckBuilder.Add(generator.Assert(f.tok, olderCondition, - new PODesc.IsOlderProofObligation(olderParameterCount, f.Ins.Count + (f.IsStatic ? 0 : 1)))); + // Enforce 'older' conditions + var (olderParameterCount, olderCondition) = generator.OlderCondition(f, selfCall, parameters); + if (olderParameterCount != 0) { + innerBuilder.Add(generator.Assert(f.tok, olderCondition, + new PODesc.IsOlderProofObligation(olderParameterCount, f.Ins.Count + (f.IsStatic ? 0 : 1)))); + } + innerBuilder.Add(new ReturnCmd(innerBody.Tok)); } + + generator.CheckWellformedWithResult(f.Body, wfo, CheckPostcondition, locals, bodyCheckBuilder, etran, "function call result"); + } bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Expr.False)); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/autoRevealDependencies/func-depth-fail.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/autoRevealDependencies/func-depth-fail.dfy.expect index 49a66e17ae7..2f69d3fbc83 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/autoRevealDependencies/func-depth-fail.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/autoRevealDependencies/func-depth-fail.dfy.expect @@ -1,4 +1,4 @@ -func-depth-fail.dfy(9,37): Error: a postcondition could not be proved on this return path +func-depth-fail.dfy(12,2): Error: a postcondition could not be proved on this return path func-depth-fail.dfy(10,10): Related location: this is the postcondition that could not be proved Dafny program verifier finished with 3 verified, 1 error From 1374af24ef7aff9dddae0bbc23f06cba16b6243b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 17:13:48 +0200 Subject: [PATCH 28/32] Fix for default parameters --- Source/DafnyCore/Verifier/BoogieGenerator.cs | 10 ++++++---- .../LitTest/dafny0/DefaultParameters.dfy.expect | 2 +- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index e30bd6c6a5e..e5714f40317 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -2338,10 +2338,12 @@ void AddWellformednessCheck(DatatypeCtor ctor) { // check well-formedness of each default-value expression foreach (var formal in ctor.Formals.Where(formal => formal.DefaultValue != null)) { var e = formal.DefaultValue; - CheckWellformed(e, new WFOptions(null, true, - false, true), locals, builder, etran); - builder.Add(new Bpl.AssumeCmd(e.tok, etran.CanCallAssumption(e))); - CheckSubrange(e.tok, etran.TrExpr(e), e.Type, formal.Type, e, builder); + CheckWellformedWithResult(e, new WFOptions(null, true, + false, true), + (innerBuilder, innerExpr, _, _) => { + builder.Add(new Bpl.AssumeCmd(e.tok, etran.CanCallAssumption(e))); + CheckSubrange(innerExpr.tok, etran.TrExpr(innerExpr), e.Type, formal.Type, e, innerBuilder); + } ,locals, builder, etran); } if (EmitImplementation(ctor.Attributes)) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy.expect index 374679dc3f9..91e6a31a26e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy.expect @@ -28,7 +28,7 @@ DefaultParameters.dfy(178,41): Error: value does not satisfy the subset constrai DefaultParameters.dfy(179,33): Error: value does not satisfy the subset constraints of 'nat' DefaultParameters.dfy(180,35): Error: value does not satisfy the subset constraints of 'nat' DefaultParameters.dfy(180,35): Error: value does not satisfy the subset constraints of 'nat' -DefaultParameters.dfy(181,40): Error: value does not satisfy the subset constraints of 'nat' +DefaultParameters.dfy(181,37): Error: value does not satisfy the subset constraints of 'nat' DefaultParameters.dfy(194,39): Error: default-value expression is not allowed to involve recursive or mutually recursive calls DefaultParameters.dfy(200,40): Error: default-value expression is not allowed to involve recursive or mutually recursive calls DefaultParameters.dfy(211,62): Error: default-value expression is not allowed to involve recursive or mutually recursive calls From d92ebf79ea00a805d3d1ca75a17478c3cb193834 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 9 Aug 2024 17:26:19 +0200 Subject: [PATCH 29/32] Fix some expect files --- .../LitTests/LitTest/dafny0/SmallTests.dfy.expect | 2 +- .../LitTest/dafny0/Superposition.legacy.dfy.expect | 4 ++-- .../LitTests/LitTest/dafny4/git-issue245.dfy.expect | 8 ++++---- .../LitTest/git-issues/git-issue-3804b.dfy.expect | 4 ++-- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy.expect index 2759917e76c..13af3fb09b0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy.expect @@ -41,7 +41,7 @@ SmallTests.dfy(396,3): Error: cannot prove termination; try supplying a decrease SmallTests.dfy(408,11): Error: assertion might not hold SmallTests.dfy(418,11): Error: assertion might not hold SmallTests.dfy(428,5): Error: cannot prove termination; try supplying a decreases clause -SmallTests.dfy(440,15): Error: a postcondition could not be proved on this return path +SmallTests.dfy(445,2): Error: a postcondition could not be proved on this return path SmallTests.dfy(443,40): Related location: this is the postcondition that could not be proved SmallTests.dfy(604,11): Error: assertion might not hold SmallTests.dfy(618,19): Error: left-hand sides n.next and n.next.next might refer to the same location diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Superposition.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Superposition.legacy.dfy.expect index c6273819d6e..d2c642f6533 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Superposition.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Superposition.legacy.dfy.expect @@ -6,12 +6,12 @@ Verifying M0.C.M (correctness) ... Verifying M0.C.Q (well-formedness) ... [3 proof obligations] error -Superposition.legacy.dfy(20,20): Error: a postcondition could not be proved on this return path +Superposition.legacy.dfy(23,6): Error: a postcondition could not be proved on this return path Superposition.legacy.dfy(21,25): Related location: this is the postcondition that could not be proved Verifying M0.C.R (well-formedness) ... [3 proof obligations] error -Superposition.legacy.dfy(26,20): Error: a postcondition could not be proved on this return path +Superposition.legacy.dfy(29,6): Error: a postcondition could not be proved on this return path Superposition.legacy.dfy(27,25): Related location: this is the postcondition that could not be proved Verifying M1.C.M (correctness) ... diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue245.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue245.dfy.expect index 3e75899048f..78d5583cf15 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue245.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue245.dfy.expect @@ -6,13 +6,13 @@ git-issue245.dfy(64,11): Error: the function must provide an equal or more detai git-issue245.dfy(68,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait git-issue245.dfy(72,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait git-issue245.dfy(76,11): Error: the function must provide an equal or more detailed postcondition than in its parent trait -git-issue245.dfy(84,11): Error: a postcondition could not be proved on this return path +git-issue245.dfy(86,7): Error: a postcondition could not be proved on this return path git-issue245.dfy(85,17): Related location: this is the postcondition that could not be proved -git-issue245.dfy(88,11): Error: a postcondition could not be proved on this return path +git-issue245.dfy(90,7): Error: a postcondition could not be proved on this return path git-issue245.dfy(89,19): Related location: this is the postcondition that could not be proved -git-issue245.dfy(92,11): Error: a postcondition could not be proved on this return path +git-issue245.dfy(94,7): Error: a postcondition could not be proved on this return path git-issue245.dfy(93,19): Related location: this is the postcondition that could not be proved -git-issue245.dfy(96,11): Error: a postcondition could not be proved on this return path +git-issue245.dfy(98,7): Error: a postcondition could not be proved on this return path git-issue245.dfy(97,17): Related location: this is the postcondition that could not be proved Dafny program verifier finished with 24 verified, 12 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804b.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804b.dfy.expect index 04076ef15b3..4f107c71bec 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804b.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804b.dfy.expect @@ -1,6 +1,6 @@ -git-issue-3804b.dfy(14,9): Error: a postcondition could not be proved on this return path +git-issue-3804b.dfy(18,2): Error: a postcondition could not be proved on this return path git-issue-3804b.dfy(16,12): Related location: this is the postcondition that could not be proved -git-issue-3804b.dfy(23,9): Error: a postcondition could not be proved on this return path +git-issue-3804b.dfy(27,2): Error: a postcondition could not be proved on this return path git-issue-3804b.dfy(25,12): Related location: this is the postcondition that could not be proved git-issue-3804b.dfy(40,20): Error: assertion might not hold git-issue-3804b.dfy(48,21): Error: assertion might not hold From 75f8b7209a43680ee5c70bd8f672b9d5042027c6 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Sat, 10 Aug 2024 16:19:56 +0200 Subject: [PATCH 30/32] Fixed reads bug --- .../BoogieGenerator.ExpressionWellformed.cs | 25 +++++++++---------- ...oogieGenerator.Functions.Wellformedness.cs | 19 ++++++++++---- .../Verifier/BoogieGenerator.Types.cs | 14 +++++------ Source/DafnyCore/Verifier/BoogieGenerator.cs | 2 +- .../Verifier/ProofDependencyManager.cs | 8 ++++++ .../LitTest/git-issues/git-issue-3804c.dfy | 6 ++--- 6 files changed, 44 insertions(+), 30 deletions(-) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index f24bf73bf20..98bdf4d0050 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -39,7 +39,7 @@ private class WFOptions { public readonly bool DoReadsChecks; public readonly bool DoOnlyCoarseGrainedTerminationChecks; // termination checks don't look at decreases clause, but reports errors for any intra-SCC call (this is used in default-value expressions) public readonly List Locals; - public readonly List Asserts; + public readonly List> Asserts; public readonly bool LValueContext; public readonly Bpl.QKeyValue AssertKv; @@ -54,12 +54,12 @@ public WFOptions(Function selfCallsAllowance, bool doReadsChecks, DoOnlyCoarseGrainedTerminationChecks = doOnlyCoarseGrainedTerminationChecks; if (saveReadsChecks) { Locals = new List(); - Asserts = new List(); + Asserts = new(); } } private WFOptions(Function selfCallsAllowance, bool doReadsChecks, bool doOnlyCoarseGrainedTerminationChecks, - List locals, List asserts, bool lValueContext, Bpl.QKeyValue assertKv) { + List locals, List> asserts, bool lValueContext, Bpl.QKeyValue assertKv) { SelfCallsAllowance = selfCallsAllowance; DoReadsChecks = doReadsChecks; DoOnlyCoarseGrainedTerminationChecks = doOnlyCoarseGrainedTerminationChecks; @@ -93,7 +93,7 @@ public WFOptions WithLValueContext(bool lValueContext) { return (t, e, d, qk) => { if (Locals != null) { var b = BplLocalVar(tran.CurrentIdGenerator.FreshId("b$reqreads#"), Bpl.Type.Bool, Locals); - Asserts.Add(tran.Assert(t, b, d, qk)); + Asserts.Add(() => tran.Assert(t, b, d, qk)); builder.Add(Bpl.Cmd.SimpleAssign(e.tok, (Bpl.IdentifierExpr)b, e)); } else { builder.Add(tran.Assert(t, e, d, qk)); @@ -125,7 +125,7 @@ public void ProcessSavedReadsChecks(List locals, BoogieStmtListBuilder } // assert b$reads_guards#0; ... foreach (var a in Asserts) { - builder.Add(a); + builder.Add(a()); } } } @@ -688,17 +688,16 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Type et = p.Type.Subst(e.GetTypeArgumentSubstitutions()); LocalVariable local = new LocalVariable(p.RangeToken, "##" + p.Name, et, p.IsGhost); local.type = local.SyntacticType; // resolve local here - var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator)) - { - Var = local - }; + var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator)) { + Var = local + }; ie.Type = ie.Var.Type; // resolve ie here substMap.Add(p, ie); locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), TrType(local.Type)))); Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified? Expression ee = e.Args[i]; directSubstMap.Add(p, ee); - + if (!(ee is DefaultValueExpression)) { CheckWellformedWithResult(ee, wfOptions, (innerBuilder, innerBody, _, _) => { CheckSubrange(innerBody.tok, etran.TrExpr(innerBody), ee.Type, et, ee, innerBuilder); @@ -1422,7 +1421,7 @@ private void TrMatchExpr(MatchExpr me, WFOptions wfOptions, CheckPostcondition c private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions wfOptions, CheckPostcondition checkPostcondition, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { - + var bodyBuilder = new BoogieStmtListBuilder(this, builder.Options, builder.Context); var statements = new List() { stmtExpr.S }; @@ -1431,7 +1430,7 @@ private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions wfOptions, Che statements.Add(nestedStmtExpr.S); expression = nestedStmtExpr.E; } - + // If we're inside an "old" expression, then "etran" will know how to translate // expressions. However, here, we're also having to translate e.S, which is a // Statement. Since statement translation (in particular, translation of CallStmt's) @@ -1450,7 +1449,7 @@ private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions wfOptions, Che } CheckWellformedWithResult(expression, wfOptions, checkPostcondition, locals, bodyBuilder, etran, "statement expression result"); - + PathAsideBlock(stmtExpr.tok, bodyBuilder, builder); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index cc613f79275..c2ab37131d0 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -42,7 +42,7 @@ public void Check(Function f) { var mod = new List { ordinaryEtran.HeapCastToIdentifierExpr, }; - + var context = new BodyTranslationContext(f.ContainsHide); var ens = new List(); foreach (AttributedExpression ensures in f.Ens) { @@ -203,7 +203,7 @@ private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslat if (f.Body != null && generator.RevealedInScope(f)) { var doReadsChecks = etran.readsFrame != null; var wfo = new WFOptions(null, doReadsChecks, doReadsChecks, false); - + void CheckPostcondition(BoogieStmtListBuilder innerBuilder, Expression innerBody, bool adaptBoxing, string prefix) { generator.CheckSubsetType(etran, innerBody, selfCall, f.ResultType, innerBuilder, adaptBoxing, prefix); if (f.Result != null) { @@ -212,9 +212,12 @@ void CheckPostcondition(BoogieStmtListBuilder innerBuilder, Expression innerBody innerBuilder.Add(cmd); } if (doReadsChecks) { - wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, innerBuilder); + // assert b$reads_guards#0; ... + foreach (var a in wfo.Asserts) { + innerBuilder.Add(a()); + } } - + // Enforce 'older' conditions var (olderParameterCount, olderCondition) = generator.OlderCondition(f, selfCall, parameters); if (olderParameterCount != 0) { @@ -225,7 +228,13 @@ void CheckPostcondition(BoogieStmtListBuilder innerBuilder, Expression innerBody } generator.CheckWellformedWithResult(f.Body, wfo, CheckPostcondition, locals, bodyCheckBuilder, etran, "function call result"); - + + // var b$reads_guards#0 : bool ... + locals.AddRange(wfo.Locals); + // b$reads_guards#0 := true ... + foreach (var cmd in wfo.AssignLocals) { + builderInitializationArea.Add(cmd); + } } bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Expr.False)); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs index 5165d55b670..17d699b7859 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs @@ -1503,16 +1503,16 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { // Note, for new-types, this has already been checked by CheckWellformed. CheckResultToBeInType(decl.Witness.tok, innerWitness, decl.Var.Type, locals, innerBuilder, etran); } - + // check that the witness expression checks out witnessExpr = Substitute(decl.Constraint, decl.Var, innerWitness); witnessExpr.tok = decl.Witness.Tok; var desc = new PODesc.WitnessCheck(witnessString, witnessExpr); - + SplitAndAssertExpression(innerBuilder, witnessExpr, etran, context, desc); }, locals, witnessCheckBuilder, etran); codeContext = ghostCodeContext; - + } else if (decl.WitnessKind == SubsetTypeDecl.WKind.CompiledZero) { var witness = Zero(decl.tok, decl.Var.Type); if (witness == null) { @@ -1523,7 +1523,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { witnessString = Printer.ExprToString(options, witness); CheckResultToBeInType(decl.tok, witness, decl.Var.Type, locals, witnessCheckBuilder, etran, $"trying witness {witnessString}: "); witnessExpr = Substitute(decl.Constraint, decl.Var, witness); - + witnessExpr.tok = decl.tok; var desc = new PODesc.WitnessCheck(witnessString, witnessExpr); SplitAndAssertExpression(witnessCheckBuilder, witnessExpr, etran, context, desc); @@ -1551,8 +1551,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { } private void SplitAndAssertExpression(BoogieStmtListBuilder witnessCheckBuilder, Expression witnessExpr, - ExpressionTranslator etran, BodyTranslationContext context, PODesc.WitnessCheck desc) - { + ExpressionTranslator etran, BodyTranslationContext context, PODesc.WitnessCheck desc) { witnessCheckBuilder.Add(new Bpl.AssumeCmd(witnessExpr.tok, etran.CanCallAssumption(witnessExpr))); var witnessCheck = etran.TrExpr(witnessExpr); @@ -1570,8 +1569,7 @@ private void SplitAndAssertExpression(BoogieStmtListBuilder witnessCheckBuilder, } private BoogieStmtListBuilder CheckConstraintWellformedness(RedirectingTypeDecl decl, BodyTranslationContext context, - ExpressionTranslator etran, List locals, BoogieStmtListBuilder builder) - { + ExpressionTranslator etran, List locals, BoogieStmtListBuilder builder) { var constraintCheckBuilder = new BoogieStmtListBuilder(this, options, context); var builderInitializationArea = new BoogieStmtListBuilder(this, options, context); var delayer = new ReadsCheckDelayer(etran, null, locals, builderInitializationArea, constraintCheckBuilder); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index e5714f40317..9fd96bf5f21 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -2343,7 +2343,7 @@ void AddWellformednessCheck(DatatypeCtor ctor) { (innerBuilder, innerExpr, _, _) => { builder.Add(new Bpl.AssumeCmd(e.tok, etran.CanCallAssumption(e))); CheckSubrange(innerExpr.tok, etran.TrExpr(innerExpr), e.Type, formal.Type, e, innerBuilder); - } ,locals, builder, etran); + }, locals, builder, etran); } if (EmitImplementation(ctor.Attributes)) { diff --git a/Source/DafnyCore/Verifier/ProofDependencyManager.cs b/Source/DafnyCore/Verifier/ProofDependencyManager.cs index 52ec364eeb2..5145a148fa9 100644 --- a/Source/DafnyCore/Verifier/ProofDependencyManager.cs +++ b/Source/DafnyCore/Verifier/ProofDependencyManager.cs @@ -32,6 +32,14 @@ public string GetProofDependencyId(ProofDependency dep) { return idString; } + public ProofDependency GetProofDependency(ICarriesAttributes declaration) { + var id = QKeyValue.FindStringAttribute(declaration.Attributes, idAttributeName); + if (id == null) { + return null; + } + return ProofDependenciesById[id]; + } + public void SetCurrentDefinition(string verificationScopeId) { currentDefinition = verificationScopeId; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804c.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804c.dfy index ec453e7ad8d..0552545b9f1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804c.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3804c.dfy @@ -8,7 +8,7 @@ function Test(x: bool): int { assert p1: x ==> P(1) by { reveal r; } assert p2: !x ==> P(2) by { reveal r; } - var y := + var x := match x { case true => assert p11: P(1) by { reveal p1; } @@ -21,6 +21,6 @@ function Test(x: bool): int assert P(2) by { reveal p21; } // p21 can be revealed and this assertion is visible outside. 2 }; - assert P(y); - y + assert P(x); // No longer verifies since we scoped expression proofs + x } \ No newline at end of file From 3823092fbb9534815fcbec45ebce8cd87a890ae7 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 12 Aug 2024 13:26:22 +0200 Subject: [PATCH 31/32] Remove unused method --- Source/DafnyCore/Verifier/ProofDependencyManager.cs | 8 -------- 1 file changed, 8 deletions(-) diff --git a/Source/DafnyCore/Verifier/ProofDependencyManager.cs b/Source/DafnyCore/Verifier/ProofDependencyManager.cs index 5145a148fa9..52ec364eeb2 100644 --- a/Source/DafnyCore/Verifier/ProofDependencyManager.cs +++ b/Source/DafnyCore/Verifier/ProofDependencyManager.cs @@ -32,14 +32,6 @@ public string GetProofDependencyId(ProofDependency dep) { return idString; } - public ProofDependency GetProofDependency(ICarriesAttributes declaration) { - var id = QKeyValue.FindStringAttribute(declaration.Attributes, idAttributeName); - if (id == null) { - return null; - } - return ProofDependenciesById[id]; - } - public void SetCurrentDefinition(string verificationScopeId) { currentDefinition = verificationScopeId; } From c2859db7c625b658350f88353b49e720ce1e257b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 12 Aug 2024 13:30:03 +0200 Subject: [PATCH 32/32] Removed PathAside for StmtExpr, and remove statementExpressionScope.dfy test --- .../BoogieGenerator.ExpressionWellformed.cs | 12 ++-- .../expressions/statementExpressionScope.dfy | 63 ------------------- .../statementExpressionScope.dfy.expect | 8 --- 3 files changed, 4 insertions(+), 79 deletions(-) delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 98bdf4d0050..5e755e2d8f8 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -1422,8 +1422,6 @@ private void TrMatchExpr(MatchExpr me, WFOptions wfOptions, CheckPostcondition c private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions wfOptions, CheckPostcondition checkPostcondition, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { - var bodyBuilder = new BoogieStmtListBuilder(this, builder.Options, builder.Context); - var statements = new List() { stmtExpr.S }; Expression expression = stmtExpr.E; while (expression is StmtExpr nestedStmtExpr) { @@ -1436,21 +1434,19 @@ private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions wfOptions, Che // Statement. Since statement translation (in particular, translation of CallStmt's) // work directly on the global variable $Heap, we temporarily change its value here. if (etran.UsesOldHeap) { - BuildWithHeapAs(stmtExpr.S.Tok, etran.HeapExpr, "StmtExpr#", locals, bodyBuilder, + BuildWithHeapAs(stmtExpr.S.Tok, etran.HeapExpr, "StmtExpr#", locals, builder, () => { foreach (var statement in statements) { - TrStmt(statement, bodyBuilder, locals, etran); + TrStmt(statement, builder, locals, etran); } }); } else { foreach (var statement in statements) { - TrStmt(statement, bodyBuilder, locals, etran); + TrStmt(statement, builder, locals, etran); } } - CheckWellformedWithResult(expression, wfOptions, checkPostcondition, locals, bodyBuilder, etran, "statement expression result"); - - PathAsideBlock(stmtExpr.tok, bodyBuilder, builder); + CheckWellformedWithResult(expression, wfOptions, checkPostcondition, locals, builder, etran, "statement expression result"); } /// diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy deleted file mode 100644 index 5f1a9808c16..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy +++ /dev/null @@ -1,63 +0,0 @@ -// RUN: ! %verify --type-system-refresh --allow-axioms --bprint:%t.bpl --isolate-assertions %s > %t -// RUN: %diff "%s.expect" "%t" - -function StatementExpressionValueAndEnsures(): int - ensures StatementExpressionValueAndEnsures() == 42 -{ - assert true; 42 -} - -function StatementExpressionAssumeAndFunctionEnsures(): int - ensures 10 == 11 // no error, since the statement expression can be used for the ensures clause -{ - assume false; 42 -} - -function StatementExpressionAssumeInLetAndFunctionEnsures(): int - ensures 10 == 11 // error, since the assume false does not leak from a let -{ - var x := (assume false; 10); x -} - -function StatementExpressionAndSubsetResult(): nat - // no error, since the statement expression can be used for the return type subset constraint -{ - assume -1 > 0; -1 -} - -method StatementExpressionAndSubsetLocal() - // no error, since the statement expression can be used for the local variable type subset constraint -{ - var x: nat := assume -1 > 0; -1; -} - -method StatementExpressionAndSubsetLocal2() - // no error, since the statement expression can be used for the local variable type subset constraint -{ - var x: nat := assume -1 > 0; -1; - assert x >= 0; // no error; - // really weird that this changes things // assert StatementExpressionAndSubsetResult() >= 0; // no error -} - -predicate P(x: int) -method NeedsNat(x: nat) -method NeedsP(x: int) requires P(x) - -method StatementExpressionAndPrecondition(x: int) -{ - NeedsNat(assume x > 0; x); // error, altough it could be nice not to have it - NeedsP(assume P(x); x); // error, since the statement expression can not be used for the requires clause -} - -function StatementExpressionAssumeDoesNotEscapeLetBinding(): int -{ - var x := assume false; 10; - assert false; // error, since the statement expression does not leak outside of the let. - x -} - -method StatementExpressionAssumeDoesNotEscapeAssignment() { - var x := assume false; 3; - assert false; // error, since the statement expression does not leak outside of the assignment. -} - diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect deleted file mode 100644 index 18b1c94a5b9..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/expressions/statementExpressionScope.dfy.expect +++ /dev/null @@ -1,8 +0,0 @@ -statementExpressionScope.dfy(17,13): Error: this is the postcondition that could not be proved -statementExpressionScope.dfy(48,11): Error: value does not satisfy the subset constraints of 'nat' -statementExpressionScope.dfy(49,8): Error: a precondition for this call could not be proved -statementExpressionScope.dfy(44,31): Related location: this is the precondition that could not be proved -statementExpressionScope.dfy(55,9): Error: assertion might not hold -statementExpressionScope.dfy(61,9): Error: assertion might not hold - -Dafny program verifier finished with 15 verified, 5 errors