From b732961c4e4f174a184c34749d694e289d1e4f25 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 15 Jun 2015 14:42:44 -0700 Subject: More tests of reads-clause checking --- Test/dafny0/Reads.dfy | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) (limited to 'Test/dafny0/Reads.dfy') diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy index 645494cb..6ae07d53 100644 --- a/Test/dafny0/Reads.dfy +++ b/Test/dafny0/Reads.dfy @@ -55,3 +55,39 @@ function ok5(r : R):() reads if r != null then {r, r.r} else {}; {()} +// Reads checking where there are circularities among the expressions + +class CircularChecking { + var Repr: set + + function F(): int + reads this, Repr + + function F'(): int + reads Repr, this // this is also fine + + function G0(): int + reads this + requires Repr == {} && F() == 100 + + function G1(): int + reads this + requires F() == 100 // error: it is not known (yet) that the rest of what F() reads (namely, Repr) is empty + requires Repr == {} + + function H0(cell: Cell): int + reads Repr // error: reads is not self-framing (unless "this in Repr") + requires this in Repr // lo and behold! So, reads clause is fine, if we can assume the precondition + + function H1(cell: Cell): int + reads this, Repr + requires cell in Repr + requires cell != null && cell.data == 10 + + function H2(cell: Cell): int + reads this, Repr + requires cell != null && cell.data == 10 // error: it is not known (yet) that "cell in Repr" + requires cell in Repr +} + +class Cell { var data: int } -- cgit v1.2.3 From 2edb5e1ba0f8c9c79364d0f0415713f0ddfdeadd Mon Sep 17 00:00:00 2001 From: leino Date: Mon, 15 Jun 2015 15:04:18 -0700 Subject: Postpone reads checks of function preconditions until after the entire precondition has otherwise been checked for well-formedness --- Source/Dafny/Translator.cs | 70 +++++++++++++++------------ Test/dafny0/Array.dfy.expect | 30 ++++++------ Test/dafny0/AutoReq.dfy.expect | 6 +-- Test/dafny0/Backticks.dfy.expect | 2 +- Test/dafny0/BadFunction.dfy.expect | 2 +- Test/dafny0/ComputationsLoop.dfy.expect | 2 +- Test/dafny0/ComputationsLoop2.dfy.expect | 4 +- Test/dafny0/ComputationsNeg.dfy.expect | 2 +- Test/dafny0/ControlStructures.dfy.expect | 4 +- Test/dafny0/Corecursion.dfy.expect | 20 ++++---- Test/dafny0/Datatypes.dfy.expect | 20 ++++---- Test/dafny0/Definedness.dfy.expect | 8 +-- Test/dafny0/DeterministicPick.dfy.expect | 2 +- Test/dafny0/FunctionSpecifications.dfy.expect | 30 ++++++------ Test/dafny0/Include.dfy.expect | 2 +- Test/dafny0/LetExpr.dfy.expect | 4 +- Test/dafny0/NatTypes.dfy.expect | 6 +-- Test/dafny0/PredExpr.dfy.expect | 4 +- Test/dafny0/RankNeg.dfy.expect | 16 +++--- Test/dafny0/Reads.dfy | 4 +- Test/dafny0/Reads.dfy.expect | 19 +++----- Test/dafny0/Refinement.dfy.expect | 2 +- Test/dafny0/SmallTests.dfy.expect | 12 ++--- Test/dafny0/StatementExpressions.dfy.expect | 4 +- Test/dafny0/Superposition.dfy.expect | 10 ++-- Test/dafny0/Termination.dfy.expect | 10 ++-- Test/hofs/Classes.dfy.expect | 6 +-- Test/hofs/Naked.dfy.expect | 14 +++--- Test/hofs/ReadsReads.dfy.expect | 8 +-- Test/hofs/Simple.dfy.expect | 8 +-- Test/hofs/Twice.dfy.expect | 4 +- 31 files changed, 170 insertions(+), 165 deletions(-) (limited to 'Test/dafny0/Reads.dfy') diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index e93e91df..c4bc6cdd 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4021,6 +4021,7 @@ namespace Microsoft.Dafny { var implInParams = Bpl.Formal.StripWhereClauses(inParams); var locals = new List(); var builder = new Bpl.StmtListBuilder(); + var builderInitializationArea = new Bpl.StmtListBuilder(); builder.Add(new CommentCmd("AddWellformednessCheck for function " + f)); builder.Add(CaptureState(f.tok, false, "initial state")); @@ -4028,19 +4029,17 @@ namespace Microsoft.Dafny { // check well-formedness of the preconditions (including termination, and reads checks), and then // assume each one of them - var wfo = new WFOptions(null, true, true /* do delayed reads checks over requires */); // check well-formedness of the reads clause + var wfo = new WFOptions(null, true, true /* do delayed reads checks over requires */); CheckFrameWellFormed(wfo, f.Reads, locals, builder, etran); + wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, builder); - // check the reads of the preconditions now - foreach (var a in wfo.Asserts) { - builder.Add(a); - } - + wfo = new WFOptions(null, true, true /* do delayed reads checks */); foreach (Expression p in f.Req) { - CheckWellformedAndAssume(p, new WFOptions(null, true /* do reads checks */), locals, builder, etran); + CheckWellformedAndAssume(p, wfo, locals, builder, etran); } + wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, builder); // check well-formedness of the decreases clauses (including termination, but no reads checks) foreach (Expression p in f.Decreases.Expressions) @@ -4119,16 +4118,12 @@ namespace Microsoft.Dafny { postCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False)); builder.Add(new Bpl.IfCmd(f.tok, null, postCheckBuilder.Collect(f.tok), null, bodyCheckBuilder.Collect(f.tok))); - // var b$reads_guards_requires#0 : bool - locals.AddRange(wfo.Locals); - // This ugly way seems to be the way to add things at the start of a builder: - StmtList sl = builder.Collect(f.tok); - // b$reads_guards_requires#0 := true ... - sl.BigBlocks[0].simpleCmds.InsertRange(0, wfo.AssignLocals); - + 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); Bpl.Implementation impl = new Bpl.Implementation(f.tok, proc.Name, typeParams, Concat(typeInParams, implInParams), new List(), - locals, sl, etran.TrAttributes(f.Attributes, null)); + locals, implBody, etran.TrAttributes(f.Attributes, null)); sink.AddTopLevelDeclaration(impl); if (InsertChecksums) @@ -4582,7 +4577,11 @@ namespace Microsoft.Dafny { /// like it. This is useful in function postconditions, where the result of the function is /// syntactically given as what looks like a recursive call with the same arguments. /// "DoReadsChecks" indicates whether or not to perform reads checks. If so, the generated code - /// will make references to $_Frame. + /// will make references to $_Frame. If "saveReadsChecks" is true, then the reads checks will + /// be recorded but postponsed. In particular, CheckWellformed will append to .Locals a list of + /// fresh local variables and will append to .Assert assertions with appropriate error messages + /// that can be used later. As a convenience, the ProcessSavedReadsChecks will make use of .Locals + /// and .Asserts (and AssignLocals) and update a given StmtListBuilder. /// private class WFOptions { @@ -4596,6 +4595,7 @@ namespace Microsoft.Dafny { } public WFOptions(Function selfCallsAllowance, bool doReadsChecks, bool saveReadsChecks = false) { + Contract.Requires(!saveReadsChecks || doReadsChecks); // i.e., saveReadsChecks ==> doReadsChecks SelfCallsAllowance = selfCallsAllowance; DoReadsChecks = doReadsChecks; if (saveReadsChecks) { @@ -4629,6 +4629,24 @@ namespace Microsoft.Dafny { ); } } + + public void ProcessSavedReadsChecks(List locals, StmtListBuilder builderInitializationArea, StmtListBuilder builder) { + Contract.Requires(locals != null); + Contract.Requires(builderInitializationArea != null); + Contract.Requires(builder != null); + Contract.Requires(Locals != null && Asserts != null); // ProcessSavedReadsChecks should be called only if the constructor was called with saveReadsChecks + + // var b$reads_guards#0 : bool ... + locals.AddRange(Locals); + // b$reads_guards#0 := true ... + foreach (var cmd in AssignLocals) { + builderInitializationArea.Add(cmd); + } + // assert b$reads_guards#0; ... + foreach (var a in Asserts) { + builder.Add(a); + } + } } void TrStmt_CheckWellformed(Expression expr, Bpl.StmtListBuilder builder, List locals, ExpressionTranslator etran, bool subsumption) { @@ -4636,6 +4654,7 @@ namespace Microsoft.Dafny { Contract.Requires(builder != null); Contract.Requires(locals != null); Contract.Requires(etran != null); + Contract.Requires(predef != null); Bpl.QKeyValue kv; if (subsumption) { @@ -4738,10 +4757,13 @@ namespace Microsoft.Dafny { return; } // resort to the behavior of simply checking well-formedness followed by assuming the translated expression - CheckWellformedWithResult(expr, options, null, null, locals, builder, etran); + CheckWellformed(expr, options, locals, builder, etran); builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(expr))); } + /// + /// Check the well-formedness of "expr" (but don't leave hanging around any assumptions that affect control flow) + /// void CheckWellformed(Expression expr, WFOptions options, List locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) { Contract.Requires(expr != null); Contract.Requires(options != null); @@ -5292,21 +5314,9 @@ namespace Microsoft.Dafny { // Check frame WF and that it read covers itself newOptions = new WFOptions(options.SelfCallsAllowance, true /* check reads clauses */, true /* delay reads checks */); - CheckFrameWellFormed(newOptions, reads, locals, newBuilder, newEtran); - // new options now contains the delayed reads checks - locals.AddRange(newOptions.Locals); - // assign locals to true, but at a scope above - Contract.Assert(newBuilder != builder); - foreach (var a in newOptions.AssignLocals) { - builder.Add(a); - } - - // add asserts to the current builder (right after frame WF) - foreach (var a in newOptions.Asserts) { - newBuilder.Add(a); - } + newOptions.ProcessSavedReadsChecks(locals, builder, newBuilder); // continue doing reads checks, but don't delay them newOptions = new WFOptions(options.SelfCallsAllowance, true, false); diff --git a/Test/dafny0/Array.dfy.expect b/Test/dafny0/Array.dfy.expect index bf4da25f..ff05137b 100644 --- a/Test/dafny0/Array.dfy.expect +++ b/Test/dafny0/Array.dfy.expect @@ -44,43 +44,43 @@ Execution trace: Array.dfy(120,8): Error: insufficient reads clause to read the indicated range of array elements Execution trace: (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then + (0,0): anon10_Else (0,0): anon11_Then (0,0): anon12_Then + (0,0): anon13_Then Array.dfy(122,8): Error: insufficient reads clause to read the indicated range of array elements Execution trace: (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then + (0,0): anon10_Else (0,0): anon11_Then - (0,0): anon12_Else + (0,0): anon12_Then + (0,0): anon13_Else Array.dfy(123,8): Error: insufficient reads clause to read the indicated range of array elements Execution trace: (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then + (0,0): anon10_Else (0,0): anon11_Then - (0,0): anon12_Else + (0,0): anon12_Then + (0,0): anon13_Else Array.dfy(124,8): Error: insufficient reads clause to read the indicated range of array elements Execution trace: (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then + (0,0): anon10_Else (0,0): anon11_Then - (0,0): anon12_Else + (0,0): anon12_Then + (0,0): anon13_Else Array.dfy(163,6): Error: insufficient reads clause to read array element Execution trace: (0,0): anon0 - (0,0): anon7_Else - (0,0): anon8_Then + (0,0): anon8_Else (0,0): anon9_Then + (0,0): anon10_Then Array.dfy(171,6): Error: insufficient reads clause to read array element Execution trace: (0,0): anon0 - (0,0): anon7_Else - (0,0): anon8_Then + (0,0): anon8_Else (0,0): anon9_Then + (0,0): anon10_Then Array.dfy(187,6): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: (0,0): anon0 diff --git a/Test/dafny0/AutoReq.dfy.expect b/Test/dafny0/AutoReq.dfy.expect index 547b676d..8486716d 100644 --- a/Test/dafny0/AutoReq.dfy.expect +++ b/Test/dafny0/AutoReq.dfy.expect @@ -2,17 +2,17 @@ AutoReq.dfy(247,5): Error: possible violation of function precondition AutoReq.dfy(239,14): Related location Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else AutoReq.dfy(13,3): Error: possible violation of function precondition AutoReq.dfy(5,14): Related location Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else AutoReq.dfy(25,3): Error: possible violation of function precondition AutoReq.dfy(5,14): Related location Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else AutoReq.dfy(38,12): Error: assertion violation AutoReq.dfy(31,13): Related location AutoReq.dfy(7,5): Related location diff --git a/Test/dafny0/Backticks.dfy.expect b/Test/dafny0/Backticks.dfy.expect index ab2bbc52..6657cd8c 100644 --- a/Test/dafny0/Backticks.dfy.expect +++ b/Test/dafny0/Backticks.dfy.expect @@ -1,8 +1,8 @@ Backticks.dfy(38,5): Error: insufficient reads clause to invoke function Execution trace: (0,0): anon0 - (0,0): anon5_Else (0,0): anon6_Else + (0,0): anon7_Else Backticks.dfy(77,8): Error: call may violate context's modifies clause Execution trace: (0,0): anon0 diff --git a/Test/dafny0/BadFunction.dfy.expect b/Test/dafny0/BadFunction.dfy.expect index 7127b60b..9c4ae81d 100644 --- a/Test/dafny0/BadFunction.dfy.expect +++ b/Test/dafny0/BadFunction.dfy.expect @@ -1,6 +1,6 @@ BadFunction.dfy(9,3): Error: failure to decrease termination measure Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Dafny program verifier finished with 2 verified, 1 error diff --git a/Test/dafny0/ComputationsLoop.dfy.expect b/Test/dafny0/ComputationsLoop.dfy.expect index d9d48024..91dc2af9 100644 --- a/Test/dafny0/ComputationsLoop.dfy.expect +++ b/Test/dafny0/ComputationsLoop.dfy.expect @@ -1,7 +1,7 @@ ComputationsLoop.dfy(7,3): Error: failure to decrease termination measure Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else ComputationsLoop.dfy(12,26): Error: assertion violation Execution trace: (0,0): anon0 diff --git a/Test/dafny0/ComputationsLoop2.dfy.expect b/Test/dafny0/ComputationsLoop2.dfy.expect index 0a45e6d0..816cbd31 100644 --- a/Test/dafny0/ComputationsLoop2.dfy.expect +++ b/Test/dafny0/ComputationsLoop2.dfy.expect @@ -1,11 +1,11 @@ ComputationsLoop2.dfy(6,3): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else ComputationsLoop2.dfy(11,3): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else ComputationsLoop2.dfy(16,26): Error: assertion violation Execution trace: (0,0): anon0 diff --git a/Test/dafny0/ComputationsNeg.dfy.expect b/Test/dafny0/ComputationsNeg.dfy.expect index 16c8963f..a6318087 100644 --- a/Test/dafny0/ComputationsNeg.dfy.expect +++ b/Test/dafny0/ComputationsNeg.dfy.expect @@ -1,7 +1,7 @@ ComputationsNeg.dfy(7,3): Error: failure to decrease termination measure Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else ComputationsNeg.dfy(11,1): Error BP5003: A postcondition might not hold on this return path. ComputationsNeg.dfy(10,17): Related location: This is the postcondition that might not hold. Execution trace: diff --git a/Test/dafny0/ControlStructures.dfy.expect b/Test/dafny0/ControlStructures.dfy.expect index 43124912..3f4dce92 100644 --- a/Test/dafny0/ControlStructures.dfy.expect +++ b/Test/dafny0/ControlStructures.dfy.expect @@ -26,11 +26,11 @@ Execution trace: ControlStructures.dfy(54,3): Error: missing case in case statement: Red Execution trace: (0,0): anon0 - (0,0): anon8_Else (0,0): anon9_Else (0,0): anon10_Else (0,0): anon11_Else - (0,0): anon12_Then + (0,0): anon12_Else + (0,0): anon13_Then ControlStructures.dfy(75,3): Error: alternative cases fail to cover all possibilties Execution trace: (0,0): anon0 diff --git a/Test/dafny0/Corecursion.dfy.expect b/Test/dafny0/Corecursion.dfy.expect index e30f6f1a..62b67cc3 100644 --- a/Test/dafny0/Corecursion.dfy.expect +++ b/Test/dafny0/Corecursion.dfy.expect @@ -1,36 +1,36 @@ Corecursion.dfy(17,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively) Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Corecursion.dfy(23,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without any ensures clause can be called co-recursively) Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Corecursion.dfy(58,5): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Corecursion.dfy(71,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context) Execution trace: (0,0): anon0 - (0,0): anon5_Else + (0,0): anon6_Else Corecursion.dfy(93,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) Execution trace: (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then + (0,0): anon6_Else + (0,0): anon7_Then Corecursion.dfy(103,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) Execution trace: (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then + (0,0): anon6_Else + (0,0): anon7_Then Corecursion.dfy(148,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Corecursion.dfy(161,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Dafny program verifier finished with 20 verified, 8 errors diff --git a/Test/dafny0/Datatypes.dfy.expect b/Test/dafny0/Datatypes.dfy.expect index 874df45e..4c0b1e96 100644 --- a/Test/dafny0/Datatypes.dfy.expect +++ b/Test/dafny0/Datatypes.dfy.expect @@ -16,27 +16,27 @@ Execution trace: Datatypes.dfy(349,5): Error: missing case in case statement: Cons Execution trace: (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Then + (0,0): anon7_Else + (0,0): anon8_Then Datatypes.dfy(349,5): Error: missing case in case statement: Nil Execution trace: (0,0): anon0 - (0,0): anon6_Else (0,0): anon7_Else - (0,0): anon8_Then + (0,0): anon8_Else + (0,0): anon9_Then Datatypes.dfy(356,8): Error: missing case in case statement: Cons Execution trace: (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then + (0,0): anon10_Else (0,0): anon11_Then + (0,0): anon12_Then Datatypes.dfy(356,8): Error: missing case in case statement: Nil Execution trace: (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Else - (0,0): anon12_Then + (0,0): anon10_Else + (0,0): anon11_Then + (0,0): anon12_Else + (0,0): anon13_Then Datatypes.dfy(82,20): Error: assertion violation Execution trace: (0,0): anon0 diff --git a/Test/dafny0/Definedness.dfy.expect b/Test/dafny0/Definedness.dfy.expect index 5d823616..af5b62b9 100644 --- a/Test/dafny0/Definedness.dfy.expect +++ b/Test/dafny0/Definedness.dfy.expect @@ -1,7 +1,7 @@ Definedness.dfy(11,7): Error: possible division by zero Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Definedness.dfy(18,16): Error: possible division by zero Execution trace: (0,0): anon0 @@ -161,15 +161,15 @@ Definedness.dfy(215,10): Error BP5003: A postcondition might not hold on this re Definedness.dfy(217,46): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Definedness.dfy(224,22): Error: target object may be null Execution trace: (0,0): anon0 - (0,0): anon3_Then + (0,0): anon4_Then Definedness.dfy(237,10): Error BP5003: A postcondition might not hold on this return path. Definedness.dfy(240,24): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Dafny program verifier finished with 21 verified, 37 errors diff --git a/Test/dafny0/DeterministicPick.dfy.expect b/Test/dafny0/DeterministicPick.dfy.expect index f8b779ef..0999294e 100644 --- a/Test/dafny0/DeterministicPick.dfy.expect +++ b/Test/dafny0/DeterministicPick.dfy.expect @@ -1,6 +1,6 @@ DeterministicPick.dfy(13,5): Error: to be compilable, the value of a let-such-that expression must be uniquely determined Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Dafny program verifier finished with 6 verified, 1 error diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect index f5112bfe..6d4bdfbb 100644 --- a/Test/dafny0/FunctionSpecifications.dfy.expect +++ b/Test/dafny0/FunctionSpecifications.dfy.expect @@ -2,27 +2,27 @@ FunctionSpecifications.dfy(35,25): Error BP5003: A postcondition might not hold FunctionSpecifications.dfy(31,13): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon8_Else (0,0): anon9_Else - (0,0): anon10_Then - (0,0): anon11_Else + (0,0): anon10_Else + (0,0): anon11_Then + (0,0): anon12_Else FunctionSpecifications.dfy(45,3): Error BP5003: A postcondition might not hold on this return path. FunctionSpecifications.dfy(40,24): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon13_Else - (0,0): anon16_Else - (0,0): anon17_Then + (0,0): anon14_Else + (0,0): anon17_Else + (0,0): anon18_Then FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon9_Then - (0,0): anon4 + (0,0): anon10_Then + (0,0): anon5 FunctionSpecifications.dfy(59,10): Error BP5003: A postcondition might not hold on this return path. FunctionSpecifications.dfy(60,22): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon6_Else + (0,0): anon7_Else FunctionSpecifications.dfy(108,23): Error: assertion violation Execution trace: (0,0): anon0 @@ -40,28 +40,28 @@ Execution trace: FunctionSpecifications.dfy(158,3): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else FunctionSpecifications.dfy(167,11): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else FunctionSpecifications.dfy(135,20): Error BP5003: A postcondition might not hold on this return path. FunctionSpecifications.dfy(137,29): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else FunctionSpecifications.dfy(146,3): Error: failure to decrease termination measure Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else FunctionSpecifications.dfy(153,3): Error: failure to decrease termination measure Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else FunctionSpecifications.dfy(174,3): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else FunctionSpecifications.dfy(171,20): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 diff --git a/Test/dafny0/Include.dfy.expect b/Test/dafny0/Include.dfy.expect index cb329398..0921cec9 100644 --- a/Test/dafny0/Include.dfy.expect +++ b/Test/dafny0/Include.dfy.expect @@ -2,7 +2,7 @@ Include.dfy(19,19): Error BP5003: A postcondition might not hold on this return Includee.dfy(17,20): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Includee.dfy[Concrete](22,16): Error: assertion violation Execution trace: (0,0): anon0 diff --git a/Test/dafny0/LetExpr.dfy.expect b/Test/dafny0/LetExpr.dfy.expect index c6df95b8..66dc2764 100644 --- a/Test/dafny0/LetExpr.dfy.expect +++ b/Test/dafny0/LetExpr.dfy.expect @@ -24,11 +24,11 @@ Execution trace: LetExpr.dfy(305,42): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon0 - (0,0): anon6_Else + (0,0): anon7_Else LetExpr.dfy(307,12): Error: assertion violation Execution trace: (0,0): anon0 - (0,0): anon6_Else + (0,0): anon7_Else LetExpr.dfy(317,12): Error: to be compilable, the value of a let-such-that expression must be uniquely determined Execution trace: (0,0): anon0 diff --git a/Test/dafny0/NatTypes.dfy.expect b/Test/dafny0/NatTypes.dfy.expect index 99fa16e5..abc253c1 100644 --- a/Test/dafny0/NatTypes.dfy.expect +++ b/Test/dafny0/NatTypes.dfy.expect @@ -32,12 +32,12 @@ Execution trace: NatTypes.dfy(109,45): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon0 - (0,0): anon6_Else (0,0): anon7_Else - (0,0): anon8_Then + (0,0): anon8_Else + (0,0): anon9_Then NatTypes.dfy(132,35): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon0 - (0,0): anon3_Then + (0,0): anon4_Then Dafny program verifier finished with 15 verified, 9 errors diff --git a/Test/dafny0/PredExpr.dfy.expect b/Test/dafny0/PredExpr.dfy.expect index 07bd5f20..744b091a 100644 --- a/Test/dafny0/PredExpr.dfy.expect +++ b/Test/dafny0/PredExpr.dfy.expect @@ -1,12 +1,12 @@ PredExpr.dfy(7,12): Error: assertion violation Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else PredExpr.dfy(39,15): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon0 - (0,0): anon5_Else (0,0): anon6_Else + (0,0): anon7_Else PredExpr.dfy(52,17): Error: assertion violation Execution trace: (0,0): anon0 diff --git a/Test/dafny0/RankNeg.dfy.expect b/Test/dafny0/RankNeg.dfy.expect index d740f8a0..cf077cc4 100644 --- a/Test/dafny0/RankNeg.dfy.expect +++ b/Test/dafny0/RankNeg.dfy.expect @@ -1,22 +1,22 @@ RankNeg.dfy(10,26): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then + (0,0): anon6_Else + (0,0): anon7_Then RankNeg.dfy(15,28): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then + (0,0): anon6_Else + (0,0): anon7_Then RankNeg.dfy(22,31): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then + (0,0): anon6_Else + (0,0): anon7_Then RankNeg.dfy(32,25): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then + (0,0): anon6_Else + (0,0): anon7_Then Dafny program verifier finished with 1 verified, 4 errors diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy index 6ae07d53..545c9a18 100644 --- a/Test/dafny0/Reads.dfy +++ b/Test/dafny0/Reads.dfy @@ -72,7 +72,7 @@ class CircularChecking { function G1(): int reads this - requires F() == 100 // error: it is not known (yet) that the rest of what F() reads (namely, Repr) is empty + requires F() == 100 // fine, since the next line tells us that Repr is empty requires Repr == {} function H0(cell: Cell): int @@ -86,7 +86,7 @@ class CircularChecking { function H2(cell: Cell): int reads this, Repr - requires cell != null && cell.data == 10 // error: it is not known (yet) that "cell in Repr" + requires cell != null && cell.data == 10 // this is okay, too, since reads checks are postponed requires cell in Repr } diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect index 0b6a2d5a..9873f811 100644 --- a/Test/dafny0/Reads.dfy.expect +++ b/Test/dafny0/Reads.dfy.expect @@ -1,10 +1,4 @@ -Reads.dfy(75,14): Error: insufficient reads clause to invoke function -Execution trace: - (0,0): anon0 Reads.dfy(79,11): Error: insufficient reads clause to read field -Execution trace: - (0,0): anon0 -Reads.dfy(89,35): Error: insufficient reads clause to read field Execution trace: (0,0): anon0 Reads.dfy(9,30): Error: insufficient reads clause to read field @@ -13,19 +7,20 @@ Execution trace: Reads.dfy(18,30): Error: insufficient reads clause to read field Execution trace: (0,0): anon0 - (0,0): anon9_Then - (0,0): anon3 + (0,0): anon10_Then + (0,0): anon4 Reads.dfy(28,50): Error: insufficient reads clause to read field Execution trace: (0,0): anon0 Reads.dfy(37,43): Error: insufficient reads clause to read field Execution trace: (0,0): anon0 - (0,0): anon6_Then + (0,0): anon7_Then + (0,0): anon4 Reads.dfy(51,30): Error: insufficient reads clause to read field Execution trace: (0,0): anon0 - (0,0): anon9_Then - (0,0): anon3 + (0,0): anon10_Then + (0,0): anon4 -Dafny program verifier finished with 9 verified, 8 errors +Dafny program verifier finished with 11 verified, 6 errors diff --git a/Test/dafny0/Refinement.dfy.expect b/Test/dafny0/Refinement.dfy.expect index 93d59873..d03b9412 100644 --- a/Test/dafny0/Refinement.dfy.expect +++ b/Test/dafny0/Refinement.dfy.expect @@ -16,7 +16,7 @@ Refinement.dfy(99,12): Error BP5003: A postcondition might not hold on this retu Refinement.dfy(78,15): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Refinement.dfy(102,3): Error BP5003: A postcondition might not hold on this return path. Refinement.dfy(83,15): Related location: This is the postcondition that might not hold. Execution trace: diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index b475502a..3df8118a 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -4,18 +4,18 @@ Execution trace: SmallTests.dfy(65,36): Error: possible division by zero Execution trace: (0,0): anon0 - (0,0): anon12_Then + (0,0): anon13_Then SmallTests.dfy(66,51): Error: possible division by zero Execution trace: (0,0): anon0 - (0,0): anon12_Else (0,0): anon13_Else + (0,0): anon14_Else SmallTests.dfy(67,22): Error: target object may be null Execution trace: (0,0): anon0 - (0,0): anon12_Then (0,0): anon13_Then (0,0): anon14_Then + (0,0): anon15_Then SmallTests.dfy(86,24): Error: target object may be null Execution trace: (0,0): anon0 @@ -91,7 +91,7 @@ Execution trace: SmallTests.dfy(386,6): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else SmallTests.dfy(691,14): Error: assertion violation Execution trace: (0,0): anon0 @@ -125,12 +125,12 @@ Execution trace: SmallTests.dfy(354,4): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else SmallTests.dfy(398,10): Error BP5003: A postcondition might not hold on this return path. SmallTests.dfy(401,41): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon6_Else + (0,0): anon7_Else SmallTests.dfy(562,12): Error: assertion violation Execution trace: (0,0): anon0 diff --git a/Test/dafny0/StatementExpressions.dfy.expect b/Test/dafny0/StatementExpressions.dfy.expect index 313c8884..9de6a5d1 100644 --- a/Test/dafny0/StatementExpressions.dfy.expect +++ b/Test/dafny0/StatementExpressions.dfy.expect @@ -11,11 +11,11 @@ Execution trace: StatementExpressions.dfy(77,6): Error: possible division by zero Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else StatementExpressions.dfy(88,5): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else StatementExpressions.dfy(98,18): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 diff --git a/Test/dafny0/Superposition.dfy.expect b/Test/dafny0/Superposition.dfy.expect index eccb16b0..6497c712 100644 --- a/Test/dafny0/Superposition.dfy.expect +++ b/Test/dafny0/Superposition.dfy.expect @@ -14,7 +14,7 @@ Superposition.dfy(27,15): Error BP5003: A postcondition might not hold on this r Superposition.dfy(28,26): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon6_Else + (0,0): anon7_Else Verifying CheckWellformed$$_0_M0.C.R ... [5 proof obligations] error @@ -22,7 +22,7 @@ Superposition.dfy(33,15): Error BP5003: A postcondition might not hold on this r Superposition.dfy(34,26): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon6_Else + (0,0): anon7_Else Verifying CheckWellformed$$_1_M1.C.M ... [0 proof obligations] verified @@ -36,9 +36,9 @@ Superposition.dfy(50,25): Error BP5003: A postcondition might not hold on this r Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon8_Else - (0,0): anon10_Then - (0,0): anon7 + (0,0): anon9_Else + (0,0): anon11_Then + (0,0): anon8 Verifying CheckWellformed$$_1_M1.C.Q ... [0 proof obligations] verified diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect index 98aa0cd8..bc59c722 100644 --- a/Test/dafny0/Termination.dfy.expect +++ b/Test/dafny0/Termination.dfy.expect @@ -4,9 +4,9 @@ Execution trace: Termination.dfy(361,47): Error: failure to decrease termination measure Execution trace: (0,0): anon0 - (0,0): anon7_Else - (0,0): anon8_Then - (0,0): anon9_Else + (0,0): anon8_Else + (0,0): anon9_Then + (0,0): anon10_Else Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop Execution trace: (0,0): anon0 @@ -44,9 +44,9 @@ Execution trace: Termination.dfy(255,35): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon6_Else (0,0): anon7_Else - (0,0): anon8_Then + (0,0): anon8_Else + (0,0): anon9_Then Termination.dfy(296,3): Error: decreases expression might not decrease Execution trace: Termination.dfy(296,3): anon9_LoopHead diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect index 3c933bae..880dcc47 100644 --- a/Test/hofs/Classes.dfy.expect +++ b/Test/hofs/Classes.dfy.expect @@ -1,10 +1,10 @@ Classes.dfy(41,6): Error: possible violation of function precondition Execution trace: (0,0): anon0 - (0,0): anon11_Then - (0,0): anon3 (0,0): anon12_Then - (0,0): anon13_Else + (0,0): anon4 + (0,0): anon13_Then (0,0): anon14_Else + (0,0): anon15_Else Dafny program verifier finished with 6 verified, 1 error diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect index 62c035b2..a38dc560 100644 --- a/Test/hofs/Naked.dfy.expect +++ b/Test/hofs/Naked.dfy.expect @@ -1,20 +1,20 @@ Naked.dfy(9,16): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Execution trace: (0,0): anon0 - (0,0): anon7_Else (0,0): anon8_Else - (0,0): anon9_Then + (0,0): anon9_Else + (0,0): anon10_Then Naked.dfy(12,8): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Execution trace: (0,0): anon0 - (0,0): anon7_Else (0,0): anon8_Else (0,0): anon9_Else + (0,0): anon10_Else Naked.dfy(17,53): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Execution trace: (0,0): anon0 - (0,0): anon5_Else (0,0): anon6_Else + (0,0): anon7_Else Naked.dfy(22,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Execution trace: (0,0): anon0 @@ -24,12 +24,12 @@ Execution trace: Naked.dfy(29,30): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Naked.dfy(29,30): Error: possible violation of function precondition Naked.dfy(32,14): Related location Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Naked.dfy(32,15): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Execution trace: (0,0): anon0 @@ -42,7 +42,7 @@ Execution trace: Naked.dfy(45,30): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else Naked.dfy(48,11): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Execution trace: (0,0): anon0 diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect index 73002b73..cd013630 100644 --- a/Test/hofs/ReadsReads.dfy.expect +++ b/Test/hofs/ReadsReads.dfy.expect @@ -1,19 +1,19 @@ ReadsReads.dfy(31,7): Error: insufficient reads clause to invoke function Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else ReadsReads.dfy(36,5): Error: insufficient reads clause to invoke function Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else ReadsReads.dfy(47,12): Error: insufficient reads clause to invoke function Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else ReadsReads.dfy(58,7): Error: insufficient reads clause to invoke function Execution trace: (0,0): anon0 - (0,0): anon3_Else + (0,0): anon4_Else ReadsReads.dfy(87,50): Error: assertion violation Execution trace: (0,0): anon0 diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect index b3c126d5..1a1027ae 100644 --- a/Test/hofs/Simple.dfy.expect +++ b/Test/hofs/Simple.dfy.expect @@ -1,13 +1,13 @@ Simple.dfy(14,10): Error: possible division by zero Execution trace: (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then + (0,0): anon6_Else + (0,0): anon7_Then Simple.dfy(27,10): Error: possible division by zero Execution trace: (0,0): anon0 - (0,0): anon5_Else - (0,0): anon6_Then + (0,0): anon6_Else + (0,0): anon7_Then Simple.dfy(37,9): Error: possible violation of function precondition Execution trace: (0,0): anon0 diff --git a/Test/hofs/Twice.dfy.expect b/Test/hofs/Twice.dfy.expect index 5ba4b47b..2476b945 100644 --- a/Test/hofs/Twice.dfy.expect +++ b/Test/hofs/Twice.dfy.expect @@ -5,7 +5,7 @@ Execution trace: Twice.dfy(35,32): Error: possible violation of function precondition Execution trace: (0,0): anon0 - (0,0): anon9_Else - (0,0): anon10_Then + (0,0): anon10_Else + (0,0): anon11_Then Dafny program verifier finished with 4 verified, 2 errors -- cgit v1.2.3 From 8e6ed9af8dc779f4468d9ccc5ababcdd91f45672 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 15 Jun 2015 15:12:34 -0700 Subject: More reads tests --- Test/dafny0/Reads.dfy | 21 +++++++++++++++++++++ Test/dafny0/Reads.dfy.expect | 2 +- 2 files changed, 22 insertions(+), 1 deletion(-) (limited to 'Test/dafny0/Reads.dfy') diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy index 545c9a18..23064f54 100644 --- a/Test/dafny0/Reads.dfy +++ b/Test/dafny0/Reads.dfy @@ -91,3 +91,24 @@ class CircularChecking { } class Cell { var data: int } + +// Test the benefits of the new reads checking for function checking + +function ApplyToSet(S: set, f: X -> X): set + requires forall x :: x in S ==> f.reads(x) == {} && f.requires(x) +{ + if S == {} then {} else + var x :| x in S; + ApplyToSet(S - {x}, f) + {f(x)} +} + +function ApplyToSet_AltSignature0(S: set, f: X -> X): set + requires forall x :: x in S ==> f.requires(x) && f.reads(x) == {} + +function ApplyToSet_AltSignature1(S: set, f: X -> X): set + requires forall x :: x in S ==> f.reads(x) == {} + requires forall x :: x in S ==> f.requires(x) + +function ApplyToSet_AltSignature2(S: set, f: X -> X): set + requires (forall x :: x in S ==> f.reads(x) == {}) ==> forall x :: x in S ==> f.requires(x) + // (this precondition would not be good enough to check the body above) diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect index 9873f811..4dd1e947 100644 --- a/Test/dafny0/Reads.dfy.expect +++ b/Test/dafny0/Reads.dfy.expect @@ -23,4 +23,4 @@ Execution trace: (0,0): anon10_Then (0,0): anon4 -Dafny program verifier finished with 11 verified, 6 errors +Dafny program verifier finished with 15 verified, 6 errors -- cgit v1.2.3 From 7f89a05ae627b7c5498b82deaea34cabc465aaa6 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 15 Jun 2015 15:20:38 -0700 Subject: Some more reads tests --- Test/dafny0/Reads.dfy | 14 ++++++++++++++ Test/dafny0/Reads.dfy.expect | 15 ++++++++++++++- 2 files changed, 28 insertions(+), 1 deletion(-) (limited to 'Test/dafny0/Reads.dfy') diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy index 23064f54..f1c840c3 100644 --- a/Test/dafny0/Reads.dfy +++ b/Test/dafny0/Reads.dfy @@ -112,3 +112,17 @@ function ApplyToSet_AltSignature1(S: set, f: X -> X): set function ApplyToSet_AltSignature2(S: set, f: X -> X): set requires (forall x :: x in S ==> f.reads(x) == {}) ==> forall x :: x in S ==> f.requires(x) // (this precondition would not be good enough to check the body above) + +function FunctionInQuantifier0(): int + requires exists f: int -> int :: f(10) == 100 // error (x2): precondition violation and insufficient reads + +function FunctionInQuantifier1(): int + requires exists f: int -> int :: f.requires(10) && f(10) == 100 // error: insufficient reads + +function FunctionInQuantifier2(): int + requires exists f: int -> int :: f.reads(10) == {} && f.requires(10) && f(10) == 100 + ensures FunctionInQuantifier2() == 100 +{ + var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100; // error: insufficient reads for f.reads(10) + f(10) +} diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect index 4dd1e947..79d290da 100644 --- a/Test/dafny0/Reads.dfy.expect +++ b/Test/dafny0/Reads.dfy.expect @@ -22,5 +22,18 @@ Execution trace: (0,0): anon0 (0,0): anon10_Then (0,0): anon4 +Reads.dfy(117,36): Error: insufficient reads clause to invoke function +Execution trace: + (0,0): anon0 +Reads.dfy(117,36): Error: possible violation of function precondition +Execution trace: + (0,0): anon0 +Reads.dfy(120,38): Error: insufficient reads clause to invoke function +Execution trace: + (0,0): anon0 +Reads.dfy(126,26): Error: insufficient reads clause to invoke function +Execution trace: + (0,0): anon0 + (0,0): anon8_Else -Dafny program verifier finished with 15 verified, 6 errors +Dafny program verifier finished with 15 verified, 10 errors -- cgit v1.2.3 From 58d639bff25a2d4dadf6febb81b1438e957c43cd Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 15 Jun 2015 16:19:11 -0700 Subject: Do postponsed reads checking also for the body of functions -- see Test/dafny0/Reads.dfy for benefits. (Unfortunately, this loses track of the "postcondition might not hold on this return path" locations, see Test/dafny0/FunctionSpecifications.dfy.) --- Source/Dafny/Translator.cs | 4 +++- Test/dafny0/Array.dfy.expect | 6 ++++++ Test/dafny0/Backticks.dfy.expect | 3 ++- Test/dafny0/Corecursion.dfy.expect | 10 +++++----- Test/dafny0/FunctionSpecifications.dfy.expect | 20 +++++++++++--------- Test/dafny0/NatTypes.dfy.expect | 4 ++-- Test/dafny0/PredExpr.dfy.expect | 2 +- Test/dafny0/RankNeg.dfy.expect | 16 ++++++++-------- Test/dafny0/Reads.dfy | 2 +- Test/dafny0/Reads.dfy.expect | 6 +----- Test/dafny0/Termination.dfy.expect | 10 +++++----- Test/hofs/Classes.dfy.expect | 6 +++--- Test/hofs/Naked.dfy.expect | 8 ++++---- 13 files changed, 52 insertions(+), 45 deletions(-) (limited to 'Test/dafny0/Reads.dfy') diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index c4bc6cdd..8bb628a8 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4112,7 +4112,9 @@ namespace Microsoft.Dafny { * makes reads clauses also guard the requires */ , null); - CheckWellformedWithResult(f.Body, new WFOptions(null, true), funcAppl, f.ResultType, locals, bodyCheckBuilder, etran); + wfo = new WFOptions(null, true, true /* do delayed reads checks */); + CheckWellformedWithResult(f.Body, wfo, funcAppl, f.ResultType, locals, bodyCheckBuilder, etran); + wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, bodyCheckBuilder); } // Combine the two, letting the postcondition be checked on after the "bodyCheckBuilder" branch postCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False)); diff --git a/Test/dafny0/Array.dfy.expect b/Test/dafny0/Array.dfy.expect index ff05137b..59dcb4bf 100644 --- a/Test/dafny0/Array.dfy.expect +++ b/Test/dafny0/Array.dfy.expect @@ -48,6 +48,7 @@ Execution trace: (0,0): anon11_Then (0,0): anon12_Then (0,0): anon13_Then + (0,0): anon9 Array.dfy(122,8): Error: insufficient reads clause to read the indicated range of array elements Execution trace: (0,0): anon0 @@ -55,6 +56,7 @@ Execution trace: (0,0): anon11_Then (0,0): anon12_Then (0,0): anon13_Else + (0,0): anon9 Array.dfy(123,8): Error: insufficient reads clause to read the indicated range of array elements Execution trace: (0,0): anon0 @@ -62,6 +64,7 @@ Execution trace: (0,0): anon11_Then (0,0): anon12_Then (0,0): anon13_Else + (0,0): anon9 Array.dfy(124,8): Error: insufficient reads clause to read the indicated range of array elements Execution trace: (0,0): anon0 @@ -69,18 +72,21 @@ Execution trace: (0,0): anon11_Then (0,0): anon12_Then (0,0): anon13_Else + (0,0): anon9 Array.dfy(163,6): Error: insufficient reads clause to read array element Execution trace: (0,0): anon0 (0,0): anon8_Else (0,0): anon9_Then (0,0): anon10_Then + (0,0): anon7 Array.dfy(171,6): Error: insufficient reads clause to read array element Execution trace: (0,0): anon0 (0,0): anon8_Else (0,0): anon9_Then (0,0): anon10_Then + (0,0): anon7 Array.dfy(187,6): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: (0,0): anon0 diff --git a/Test/dafny0/Backticks.dfy.expect b/Test/dafny0/Backticks.dfy.expect index 6657cd8c..57761ab4 100644 --- a/Test/dafny0/Backticks.dfy.expect +++ b/Test/dafny0/Backticks.dfy.expect @@ -1,8 +1,9 @@ Backticks.dfy(38,5): Error: insufficient reads clause to invoke function Execution trace: (0,0): anon0 - (0,0): anon6_Else (0,0): anon7_Else + (0,0): anon8_Else + (0,0): anon6 Backticks.dfy(77,8): Error: call may violate context's modifies clause Execution trace: (0,0): anon0 diff --git a/Test/dafny0/Corecursion.dfy.expect b/Test/dafny0/Corecursion.dfy.expect index 62b67cc3..619a9c84 100644 --- a/Test/dafny0/Corecursion.dfy.expect +++ b/Test/dafny0/Corecursion.dfy.expect @@ -13,17 +13,17 @@ Execution trace: Corecursion.dfy(71,16): Error: cannot prove termination; try supplying a decreases clause (note that calls cannot be co-recursive in this context) Execution trace: (0,0): anon0 - (0,0): anon6_Else + (0,0): anon7_Else Corecursion.dfy(93,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) Execution trace: (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Then + (0,0): anon7_Else + (0,0): anon8_Then Corecursion.dfy(103,15): Error: cannot prove termination; try supplying a decreases clause (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) Execution trace: (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Then + (0,0): anon7_Else + (0,0): anon8_Then Corecursion.dfy(148,13): Error: failure to decrease termination measure (note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts) Execution trace: (0,0): anon0 diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect index 6d4bdfbb..9f76313a 100644 --- a/Test/dafny0/FunctionSpecifications.dfy.expect +++ b/Test/dafny0/FunctionSpecifications.dfy.expect @@ -1,22 +1,24 @@ -FunctionSpecifications.dfy(35,25): Error BP5003: A postcondition might not hold on this return path. +FunctionSpecifications.dfy(29,10): Error BP5003: A postcondition might not hold on this return path. FunctionSpecifications.dfy(31,13): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon9_Else (0,0): anon10_Else - (0,0): anon11_Then - (0,0): anon12_Else -FunctionSpecifications.dfy(45,3): Error BP5003: A postcondition might not hold on this return path. + (0,0): anon11_Else + (0,0): anon12_Then + (0,0): anon13_Else + (0,0): anon9 +FunctionSpecifications.dfy(38,10): Error BP5003: A postcondition might not hold on this return path. FunctionSpecifications.dfy(40,24): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 - (0,0): anon14_Else - (0,0): anon17_Else - (0,0): anon18_Then + (0,0): anon15_Else + (0,0): anon18_Else + (0,0): anon19_Then + (0,0): anon14 FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon10_Then + (0,0): anon11_Then (0,0): anon5 FunctionSpecifications.dfy(59,10): Error BP5003: A postcondition might not hold on this return path. FunctionSpecifications.dfy(60,22): Related location: This is the postcondition that might not hold. diff --git a/Test/dafny0/NatTypes.dfy.expect b/Test/dafny0/NatTypes.dfy.expect index abc253c1..5af90253 100644 --- a/Test/dafny0/NatTypes.dfy.expect +++ b/Test/dafny0/NatTypes.dfy.expect @@ -32,9 +32,9 @@ Execution trace: NatTypes.dfy(109,45): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon0 - (0,0): anon7_Else (0,0): anon8_Else - (0,0): anon9_Then + (0,0): anon9_Else + (0,0): anon10_Then NatTypes.dfy(132,35): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon0 diff --git a/Test/dafny0/PredExpr.dfy.expect b/Test/dafny0/PredExpr.dfy.expect index 744b091a..18d5d73f 100644 --- a/Test/dafny0/PredExpr.dfy.expect +++ b/Test/dafny0/PredExpr.dfy.expect @@ -5,8 +5,8 @@ Execution trace: PredExpr.dfy(39,15): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon0 - (0,0): anon6_Else (0,0): anon7_Else + (0,0): anon8_Else PredExpr.dfy(52,17): Error: assertion violation Execution trace: (0,0): anon0 diff --git a/Test/dafny0/RankNeg.dfy.expect b/Test/dafny0/RankNeg.dfy.expect index cf077cc4..b2686b43 100644 --- a/Test/dafny0/RankNeg.dfy.expect +++ b/Test/dafny0/RankNeg.dfy.expect @@ -1,22 +1,22 @@ RankNeg.dfy(10,26): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Then + (0,0): anon7_Else + (0,0): anon8_Then RankNeg.dfy(15,28): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Then + (0,0): anon7_Else + (0,0): anon8_Then RankNeg.dfy(22,31): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Then + (0,0): anon7_Else + (0,0): anon8_Then RankNeg.dfy(32,25): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon6_Else - (0,0): anon7_Then + (0,0): anon7_Else + (0,0): anon8_Then Dafny program verifier finished with 1 verified, 4 errors diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy index f1c840c3..7e0ca1c4 100644 --- a/Test/dafny0/Reads.dfy +++ b/Test/dafny0/Reads.dfy @@ -123,6 +123,6 @@ function FunctionInQuantifier2(): int requires exists f: int -> int :: f.reads(10) == {} && f.requires(10) && f(10) == 100 ensures FunctionInQuantifier2() == 100 { - var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100; // error: insufficient reads for f.reads(10) + var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100; // fine :) :) f(10) } diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect index 79d290da..0b599f3f 100644 --- a/Test/dafny0/Reads.dfy.expect +++ b/Test/dafny0/Reads.dfy.expect @@ -31,9 +31,5 @@ Execution trace: Reads.dfy(120,38): Error: insufficient reads clause to invoke function Execution trace: (0,0): anon0 -Reads.dfy(126,26): Error: insufficient reads clause to invoke function -Execution trace: - (0,0): anon0 - (0,0): anon8_Else -Dafny program verifier finished with 15 verified, 10 errors +Dafny program verifier finished with 16 verified, 9 errors diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect index bc59c722..77a9e70e 100644 --- a/Test/dafny0/Termination.dfy.expect +++ b/Test/dafny0/Termination.dfy.expect @@ -4,9 +4,9 @@ Execution trace: Termination.dfy(361,47): Error: failure to decrease termination measure Execution trace: (0,0): anon0 - (0,0): anon8_Else - (0,0): anon9_Then - (0,0): anon10_Else + (0,0): anon9_Else + (0,0): anon10_Then + (0,0): anon11_Else Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop Execution trace: (0,0): anon0 @@ -44,9 +44,9 @@ Execution trace: Termination.dfy(255,35): Error: cannot prove termination; try supplying a decreases clause Execution trace: (0,0): anon0 - (0,0): anon7_Else (0,0): anon8_Else - (0,0): anon9_Then + (0,0): anon9_Else + (0,0): anon10_Then Termination.dfy(296,3): Error: decreases expression might not decrease Execution trace: Termination.dfy(296,3): anon9_LoopHead diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect index 880dcc47..21188d62 100644 --- a/Test/hofs/Classes.dfy.expect +++ b/Test/hofs/Classes.dfy.expect @@ -1,10 +1,10 @@ Classes.dfy(41,6): Error: possible violation of function precondition Execution trace: (0,0): anon0 - (0,0): anon12_Then - (0,0): anon4 (0,0): anon13_Then - (0,0): anon14_Else + (0,0): anon4 + (0,0): anon14_Then (0,0): anon15_Else + (0,0): anon16_Else Dafny program verifier finished with 6 verified, 1 error diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect index a38dc560..b4dfc561 100644 --- a/Test/hofs/Naked.dfy.expect +++ b/Test/hofs/Naked.dfy.expect @@ -1,20 +1,20 @@ Naked.dfy(9,16): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Execution trace: (0,0): anon0 - (0,0): anon8_Else (0,0): anon9_Else - (0,0): anon10_Then + (0,0): anon10_Else + (0,0): anon11_Then Naked.dfy(12,8): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Execution trace: (0,0): anon0 - (0,0): anon8_Else (0,0): anon9_Else (0,0): anon10_Else + (0,0): anon11_Else Naked.dfy(17,53): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Execution trace: (0,0): anon0 - (0,0): anon6_Else (0,0): anon7_Else + (0,0): anon8_Else Naked.dfy(22,13): Error: cannot use naked function in recursive setting. Possible solution: eta expansion. Execution trace: (0,0): anon0 -- cgit v1.2.3 From cc0a7cae53c068993e3b3004049629dd396cb649 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 15 Jun 2015 17:00:04 -0700 Subject: Changed logical order of requires and reads clauses on functions. Reads clauses can now assume the precondition (as had also been the case back in the days when reads clauses had to be self framing). --- Source/Dafny/Translator.cs | 21 ++++++++++++--------- Test/dafny0/Reads.dfy | 16 +++++++++++++--- Test/dafny0/Reads.dfy.expect | 6 ++---- Test/hofs/Classes.dfy | 9 ++++----- Test/hofs/Classes.dfy.expect | 9 +++------ 5 files changed, 34 insertions(+), 27 deletions(-) (limited to 'Test/dafny0/Reads.dfy') diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 8bb628a8..90d0b11c 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4027,20 +4027,23 @@ namespace Microsoft.Dafny { DefineFrame(f.tok, f.Reads, builder, locals, null); - // check well-formedness of the preconditions (including termination, and reads checks), and then - // assume each one of them - - // check well-formedness of the reads clause - var wfo = new WFOptions(null, true, true /* do delayed reads checks over requires */); - CheckFrameWellFormed(wfo, f.Reads, locals, builder, etran); - wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, builder); - - wfo = new WFOptions(null, true, true /* do delayed reads checks */); + // 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. + var wfo = new WFOptions(null, true, true /* do delayed reads checks */); foreach (Expression p in f.Req) { CheckWellformedAndAssume(p, wfo, locals, builder, etran); } wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, builder); + // 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). + wfo = new WFOptions(null, true, true /* do delayed reads checks */); + CheckFrameWellFormed(wfo, f.Reads, locals, builder, etran); + wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, builder); + // check well-formedness of the decreases clauses (including termination, but no reads checks) foreach (Expression p in f.Decreases.Expressions) { diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy index 7e0ca1c4..6dedbada 100644 --- a/Test/dafny0/Reads.dfy +++ b/Test/dafny0/Reads.dfy @@ -58,7 +58,7 @@ function ok5(r : R):() // Reads checking where there are circularities among the expressions class CircularChecking { - var Repr: set + ghost var Repr: set function F(): int reads this, Repr @@ -76,8 +76,8 @@ class CircularChecking { requires Repr == {} function H0(cell: Cell): int - reads Repr // error: reads is not self-framing (unless "this in Repr") - requires this in Repr // lo and behold! So, reads clause is fine, if we can assume the precondition + reads Repr // by itself, this reads is not self-framing + requires this in Repr // lo and behold! So, reads clause is fine after all function H1(cell: Cell): int reads this, Repr @@ -126,3 +126,13 @@ function FunctionInQuantifier2(): int var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100; // fine :) :) f(10) } + +class DynamicFramesIdiom { + ghost var Repr: set + predicate IllFormed_Valid() + reads Repr // error: reads is not self framing (notice the absence of "this") + { + this in Repr // this says that the predicate returns true if "this in Repr", but the + // predicate can also be invoked in a state where its body will evaluate to false + } +} diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect index 0b599f3f..1199797f 100644 --- a/Test/dafny0/Reads.dfy.expect +++ b/Test/dafny0/Reads.dfy.expect @@ -1,4 +1,4 @@ -Reads.dfy(79,11): Error: insufficient reads clause to read field +Reads.dfy(133,11): Error: insufficient reads clause to read field Execution trace: (0,0): anon0 Reads.dfy(9,30): Error: insufficient reads clause to read field @@ -7,8 +7,6 @@ Execution trace: Reads.dfy(18,30): Error: insufficient reads clause to read field Execution trace: (0,0): anon0 - (0,0): anon10_Then - (0,0): anon4 Reads.dfy(28,50): Error: insufficient reads clause to read field Execution trace: (0,0): anon0 @@ -32,4 +30,4 @@ Reads.dfy(120,38): Error: insufficient reads clause to invoke function Execution trace: (0,0): anon0 -Dafny program verifier finished with 16 verified, 9 errors +Dafny program verifier finished with 17 verified, 9 errors diff --git a/Test/hofs/Classes.dfy b/Test/hofs/Classes.dfy index 2b892b35..0ceb46f1 100644 --- a/Test/hofs/Classes.dfy +++ b/Test/hofs/Classes.dfy @@ -30,15 +30,14 @@ function B(t : T) : int -> int } function J(t : T) : int - requires t != null; - requires t.h.reads(0) == {}; - reads t; - reads if t != null then t.h.reads(0) else {}; + requires t != null + reads t + reads t.h.reads(0) { if t.h.requires(0) then B(t)(0) else - B(t)(0) // fail + B(t)(0) // error: precondition violation } method U(t : T) diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect index 21188d62..e490dbe0 100644 --- a/Test/hofs/Classes.dfy.expect +++ b/Test/hofs/Classes.dfy.expect @@ -1,10 +1,7 @@ -Classes.dfy(41,6): Error: possible violation of function precondition +Classes.dfy(40,6): Error: possible violation of function precondition Execution trace: (0,0): anon0 - (0,0): anon13_Then - (0,0): anon4 - (0,0): anon14_Then - (0,0): anon15_Else - (0,0): anon16_Else + (0,0): anon7_Else + (0,0): anon8_Else Dafny program verifier finished with 6 verified, 1 error -- cgit v1.2.3