diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index 726e79e17a3..5e755e2d8f8 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; @@ -38,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; @@ -53,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; @@ -92,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)); @@ -124,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()); } } } @@ -252,7 +253,7 @@ void CheckWellformed(Expression expr, WFOptions wfOptions, List locals Contract.Requires(builder != null); Contract.Requires(etran != null); Contract.Requires(predef != null); - CheckWellformedWithResult(expr, wfOptions, null, null, locals, builder, etran); + CheckWellformedWithResult(expr, wfOptions, null, locals, builder, etran); } /// @@ -262,8 +263,16 @@ void CheckWellformed(Expression expr, WFOptions wfOptions, List locals /// assume the equivalent of "result == expr". /// See class WFOptions for descriptions of the specified options. /// - void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result, Type resultType, List locals, - BoogieStmtListBuilder builder, ExpressionTranslator etran, string resultDescription = null) { + void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, + CheckPostcondition checkPostcondition, + List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, + string resultDescription = null) { + Contract.Requires(expr != null); + Contract.Requires(wfOptions != null); + Contract.Requires(locals != null); + Contract.Requires(builder != null); + Contract.Requires(etran != null); + Contract.Requires(predef != null); var origOptions = wfOptions; if (wfOptions.LValueContext) { // Turn off LValueContext for any recursive call @@ -275,7 +284,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result 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; @@ -669,12 +678,6 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result 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(); @@ -685,14 +688,21 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result 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) { @@ -1127,135 +1137,16 @@ void CheckOperand(Expression operand) { break; } case LetExpr letExpr: - CheckWellformedLetExprWithResult(letExpr, wfOptions, result, resultType, locals, builder, etran, true); - result = null; + 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, rangeType, locals, b, comprehensionEtran, "lambda expression"); - }); - - 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")); + CheckWellformedComprehensionExpression(wfOptions, locals, builder, etran, comprehensionExpr); break; } case StmtExpr stmtExpr: - CheckWellformedStmtExpr(stmtExpr, wfOptions, result, resultType, locals, builder, etran); - result = null; + CheckWellformedStmtExpr(stmtExpr, wfOptions, checkPostcondition, locals, builder, etran); + checkPostcondition = null; break; case ITEExpr iteExpr: { ITEExpr e = iteExpr; @@ -1268,18 +1159,18 @@ 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, 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, "if expression then branch"); } - CheckWellformedWithResult(e.Els, wfOptions, result, resultType, locals, bElse, etran, "if expression else branch"); + 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))); - result = null; + checkPostcondition = null; break; } case MatchExpr matchExpr: - result = TrMatchExpr(matchExpr, wfOptions, result, resultType, locals, builder, etran); - resultDescription = "match expression"; + TrMatchExpr(matchExpr, wfOptions, checkPostcondition, locals, builder, etran); + checkPostcondition = null; break; case DatatypeUpdateExpr updateExpr: { var e = updateExpr; @@ -1296,19 +1187,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, resultDescription); + 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, resultDescription); + 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, resultDescription); + checkPostcondition = null; break; case BoogieFunctionCall call: { var e = call; @@ -1328,20 +1219,157 @@ 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); - 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, expr, true, resultDescription); + } + } + + 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; + } + + CheckPostcondition checkPostcondition = (innerBuilder, innerBody, adaptBox, prefix) => { + if (rangeType != null) { + CheckSubsetType(etran, innerBody, resultIe, rangeType, innerBuilder, adaptBox, prefix); + } + }; + 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, bool adaptBoxing, 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 ? 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 Expr TrMatchExpr(MatchExpr me, WFOptions wfOptions, Expr result, Type resultType, List locals, + private void TrMatchExpr(MatchExpr me, WFOptions wfOptions, CheckPostcondition checkPostcondition, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { FillMissingCases(me); @@ -1380,30 +1408,45 @@ private Expr TrMatchExpr(MatchExpr me, WFOptions wfOptions, Expr result, Type re var b = new BoogieStmtListBuilder(this, options, builder.Context); 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"); + + // TODO: + // resultDescription = "match expression"; + CheckWellformedWithResult(mc.Body, wfOptions, checkPostcondition, locals, b, etran, "match expression branch result"); 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, Expr result, Type resultType, List locals, + private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions wfOptions, CheckPostcondition checkPostcondition, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { + + 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)); + () => { + foreach (var statement in statements) { + TrStmt(statement, builder, locals, etran); + } + }); } else { - TrStmt(stmtExpr.S, builder, locals, etran); + foreach (var statement in statements) { + TrStmt(statement, builder, locals, etran); + } } - CheckWellformedWithResult(stmtExpr.E, options, result, resultType, locals, builder, etran, "statement expression result"); + CheckWellformedWithResult(expression, wfOptions, checkPostcondition, locals, builder, etran, "statement expression result"); } /// @@ -1474,7 +1517,10 @@ void CheckWellformedSpecialFunction(FunctionCallExpr expr, WFOptions options, Bp } } - void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr result, Type resultType, 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"); @@ -1483,16 +1529,21 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r 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); - CheckWellformedWithResult(e.RHSs[i], wfOptions, rIe, pat.Expr.Type, locals, builder, etran, "let expression binding RHS well-formed"); + + 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, 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")); } - CheckWellformedWithResult(Substitute(e.Body, null, substMap), wfOptions, result, resultType, locals, builder, etran, "let expression result"); + CheckWellformedWithResult(Substitute(e.Body, null, substMap), wfOptions, checkPostcondition, locals, builder, etran, "let expression result"); } else { // CheckWellformed(var b :| RHS(b); Body(b)) = @@ -1526,17 +1577,17 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r 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()))); } @@ -1545,14 +1596,8 @@ 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, letBody, false, "let expression"); } } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs new file mode 100644 index 00000000000..c2ab37131d0 --- /dev/null +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -0,0 +1,403 @@ +using System; +using System.Collections.Generic; +using System.Collections.Immutable; +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; + + 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 procedureParameters = GetParameters(f, etran); + var outParams = GetWellformednessProcedureOutParameters(f, etran); + var requires = GetWellformednessProcedureRequires(f, etran); + requires.AddRange(additionalRequires); + + // modifies $Heap + 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, ens, 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 + 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 locals = new List(); + var builder = new BoogieStmtListBuilder(generator, generator.options, context); + var builderInitializationArea = new BoogieStmtListBuilder(generator, generator.options, context); + 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 => { + 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(require.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). + builder.Add(new CommentCmd("Check Wfness of the reads clause")); + delayer.DoWithDelayedReadsChecks(false, + wfo => { generator.CheckFrameWellFormed(wfo, f.Reads.Expressions, locals, builder, etran); }); + + 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); + CheckBodyAndEnsuresClauseWellformedness(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 CheckBodyAndEnsuresClauseWellformedness(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 + // 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) + var postCheckBuilder = GetPostCheckBuilder(f, etran, locals); + + // Here goes the body (and include both termination checks and reads checks) + var bodyCheckBuilder = GetBodyCheckBuilder(f, etran, inParams, locals, builderInitializationArea); + + // 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))); + } + + private BoogieStmtListBuilder GetBodyCheckBuilder(Function f, ExpressionTranslator etran, + List parameters, + List locals, BoogieStmtListBuilder builderInitializationArea) { + var selfCall = GetSelfCall(f, etran, parameters); + var context = new BodyTranslationContext(f.ContainsHide); + 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 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) { + // 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) { + 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"); + + // 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)); + + return bodyCheckBuilder; + } + + 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 (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 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 context = new BodyTranslationContext(f.ContainsHide); + var postCheckBuilder = new BoogieStmtListBuilder(generator, generator.options, context); + 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) { + 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 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)); + + 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 41058d9ba78..5e61813a2c1 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs @@ -13,296 +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(); - var context = new BodyTranslationContext(f.ContainsHide); - foreach (AttributedExpression ensures in f.Ens) { - var functionHeight = currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); - var splits = new List(); - bool splitHappened /*we actually don't care*/ = TrSplitExpr(context, ensures.E, splits, true, functionHeight, true, true, etran); - var (errorMessage, successMessage) = CustomErrorMessage(ensures.Attributes); - foreach (var s in splits) { - if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, currentModule)) { - AddEnsures(ens, EnsuresWithDependencies(s.Tok, false, ensures.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, context); - var builderInitializationArea = new BoogieStmtListBuilder(this, options, context); - 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, context); - // 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, context); - 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); Contract.Requires(body != null); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index 972d1375a27..bb8baa41705 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 812d169679b..f9c1134045f 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -367,30 +367,11 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, TrStmt(nestedMatchStmt.Flattened, builder, locals, etran); } else if (stmt is MatchStmt matchStmt) { TrMatchStmt(matchStmt, builder, locals, etran); - } else if (stmt is VarDeclStmt varDeclStmt) { - TrVarDeclStmt(varDeclStmt, builder, locals, etran); - } else if (stmt is 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")); + } else if (stmt is VarDeclStmt) { + var s = (VarDeclStmt)stmt; + TrVarDeclStmt(s, builder, locals, etran); + } 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 @@ -401,6 +382,51 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, } } + + private void TranslateVariableDeclaration(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); + + CheckPostcondition checkPostcondition = (b, body, adaptBoxing, prefix) => { + Contract.Assert(pat.Expr.Type != null); + 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 ? AdaptBoxing(rhs.tok, e, rhs.Type, pat.Expr.Type) : e), + prefix)); + }; + 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))); + + 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 TrUpdateStmt(BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, UpdateStmt statement) { // This UpdateStmt can be single-target assignment, a multi-assignment, a call statement, or // an array-range update. Handle the multi-assignment here and handle the others as for .ResolvedStatements. @@ -434,7 +460,8 @@ private void TrUpdateStmt(BoogieStmtListBuilder builder, List locals, } } - private void TrVarDeclStmt(VarDeclStmt varDeclStmt, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran) { + void TrVarDeclStmt(VarDeclStmt varDeclStmt, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran) { + var newLocalIds = new List(); int i = 0; foreach (var local in varDeclStmt.Locals) { @@ -1795,7 +1822,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)) { @@ -2598,10 +2625,18 @@ 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); + 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, _, _, _) => { + if (cre != null) { + b.Add(Assert(tok, cre, desc)); + } + }); + if (cre != null) { + builder.Add(new AssumeCmd(tok, cre)); //e.tok, MkIs(bRhs, rhsTypeConstraint))); + } - Bpl.Expr bRhs = etran.TrExpr(e.Expr); - CheckSubrange(tok, bRhs, e.Expr.Type, rhsTypeConstraint, e.Expr, builder); if (bGivenLhs != null) { Contract.Assert(bGivenLhs == bLhs); // box the RHS, then do the assignment @@ -2849,7 +2884,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); @@ -2874,7 +2910,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/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs index 7ec946ea67e..17d699b7859 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,34 @@ 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/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index e30bd6c6a5e..9fd96bf5f21 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/DafnyCore/Verifier/BoogieStmtListBuilder.cs b/Source/DafnyCore/Verifier/BoogieStmtListBuilder.cs index 641543b9f16..dc8aeb1a07d 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 BodyTranslationContext Context { get; set; } public StmtListBuilder builder; 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); 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..ef31e255dbb --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy @@ -0,0 +1,36 @@ +// 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 + } +} + +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 new file mode 100644 index 00000000000..8eaf561c25b --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/functions/ensuresReporting.dfy.expect @@ -0,0 +1,10 @@ +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 +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, 4 errors 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 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 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 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 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-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 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 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..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 @@ -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); + assert P(x); // No longer verifies since we scoped expression proofs x } \ No newline at end of file