From 918aadf5c467e68f93b8d898496b62e6334ab122 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 17 Dec 2013 18:20:36 -0800 Subject: Fixed pretty printing of calc statements to use the new(-since-long) format. Disallow dangling operator in calc (which had also allowed soundness bug). Don't reprove the test files in dafny0 after testing their pretty printing. --- Source/Dafny/Dafny.atg | 21 ++-- Source/Dafny/Parser.cs | 19 ++-- Source/Dafny/Printer.cs | 35 ++++--- Test/dafny0/Answer | 238 +++++-------------------------------------- Test/dafny0/Calculations.dfy | 154 ++++++++++++++++++---------- Test/dafny0/runtest.bat | 6 +- 6 files changed, 176 insertions(+), 297 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 2a7aec1e..9432b54d 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1451,9 +1451,10 @@ CalcStmt Expression/*!*/ e; BlockStmt/*!*/ h; IToken opTok; + IToken danglingOperator = null; .) "calc" (. x = t; .) - [ CalcOp (. maybeOp = calcOp.ResultOp(calcOp); // guard against non-trasitive calcOp (like !=) + [ CalcOp (. maybeOp = calcOp.ResultOp(calcOp); // guard against non-transitive calcOp (like !=) if (maybeOp == null) { SemErr(opTok, "the main operator of a calculation must be transitive"); } @@ -1461,26 +1462,32 @@ CalcStmt .) ] "{" - { Expression (. lines.Add(e); stepOp = calcOp; .) + { Expression (. lines.Add(e); stepOp = calcOp; danglingOperator = null; .) ";" [ CalcOp (. maybeOp = resOp.ResultOp(op); if (maybeOp == null) { SemErr(opTok, "this operator cannot continue this calculation"); } else { stepOp = op; - resOp = maybeOp; + resOp = maybeOp; + danglingOperator = opTok; } .) ] (. stepOps.Add(stepOp); .) - Hint (. hints.Add(h); .) + Hint (. hints.Add(h); + if (h.Body.Count != 0) { danglingOperator = null; } + .) } "}" (. + if (danglingOperator != null) { + SemErr(danglingOperator, "a calculation cannot end with an operator"); + } if (lines.Count > 0) { - // Repeat the last line to create a dummy line for the dangling hint - lines.Add(lines[lines.Count - 1]); + // Repeat the last line to create a dummy line for the dangling hint + lines.Add(lines[lines.Count - 1]); } - s = new CalcStmt(x, calcOp, lines, hints, stepOps, resOp); + s = new CalcStmt(x, calcOp, lines, hints, stepOps, resOp); .) . CalcOp diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 9f7e96bb..4e0611f7 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1989,12 +1989,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ e; BlockStmt/*!*/ h; IToken opTok; + IToken danglingOperator = null; Expect(85); x = t; if (StartOf(21)) { CalcOp(out opTok, out calcOp); - maybeOp = calcOp.ResultOp(calcOp); // guard against non-trasitive calcOp (like !=) + maybeOp = calcOp.ResultOp(calcOp); // guard against non-transitive calcOp (like !=) if (maybeOp == null) { SemErr(opTok, "the main operator of a calculation must be transitive"); } @@ -2004,7 +2005,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(8); while (StartOf(16)) { Expression(out e); - lines.Add(e); stepOp = calcOp; + lines.Add(e); stepOp = calcOp; danglingOperator = null; Expect(7); if (StartOf(21)) { CalcOp(out opTok, out op); @@ -2013,18 +2014,24 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo SemErr(opTok, "this operator cannot continue this calculation"); } else { stepOp = op; - resOp = maybeOp; + resOp = maybeOp; + danglingOperator = opTok; } } stepOps.Add(stepOp); Hint(out h); - hints.Add(h); + hints.Add(h); + if (h.Body.Count != 0) { danglingOperator = null; } + } Expect(9); + if (danglingOperator != null) { + SemErr(danglingOperator, "a calculation cannot end with an operator"); + } if (lines.Count > 0) { - // Repeat the last line to create a dummy line for the dangling hint - lines.Add(lines[lines.Count - 1]); + // Repeat the last line to create a dummy line for the dangling hint + lines.Add(lines[lines.Count - 1]); } s = new CalcStmt(x, calcOp, lines, hints, stepOps, resOp); diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 868d73f5..a7ca8f96 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -669,27 +669,34 @@ namespace Microsoft.Dafny { } wr.WriteLine("{"); int lineInd = indent + IndentAmount; - if (s.Lines.Count > 0) { + int lineCount = s.Lines.Count == 0 ? 0 : s.Lines.Count - 1; // if nonempty, .Lines always contains a duplicated last line + // The number of op/hints is commonly one less than the number of lines, but + // it can also equal the number of lines for empty calc's and for calc's with + // a dangling hint. + int hintCount = s.Lines.Count != 0 && s.Hints.Last().Body.Count == 0 ? lineCount - 1 : lineCount; + for (var i = 0; i < lineCount; i++) { + var e = s.Lines[i]; + var op = s.StepOps[i]; + var h = s.Hints[i]; + // print the line Indent(lineInd); - PrintExpression(s.Lines.First(), lineInd); + PrintExpression(e, lineInd); wr.WriteLine(";"); - } - for (var i = 1; i < s.Lines.Count; i++){ - var e = s.Lines[i]; - var h = s.Hints[i - 1]; - var op = s.StepOps[i - 1]; + if (i == hintCount) { + break; + } + // print the operator, if any + if (!s.Op.Equals(op)) { + Indent(indent); // this lines up with the "calc" + PrintCalcOp(op); + wr.WriteLine(); + } + // print the hints foreach (var st in h.Body) { Indent(lineInd); PrintStatement(st, lineInd); wr.WriteLine(); } - Indent(lineInd); - if (!s.Op.Equals(op)) { - PrintCalcOp(op); - wr.Write(" "); - } - PrintExpression(e, lineInd); - wr.WriteLine(";"); } Indent(indent); wr.Write("}"); diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index a1dd639f..045900ae 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1824,34 +1824,6 @@ TailCalls.dfy(42,12): Error: 'decreases *' is allowed only on tail-recursive met TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive methods 5 resolution/type errors detected in TailCalls.dfy --------------------- Calculations.dfy -------------------- -Calculations.dfy(3,4): Error: index out of range -Execution trace: - (0,0): anon0 - (0,0): anon24_Then -Calculations.dfy(8,13): Error: index out of range -Execution trace: - (0,0): anon0 - (0,0): anon26_Then -Calculations.dfy(8,17): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon26_Then -Calculations.dfy(52,11): Error: assertion violation -Execution trace: - (0,0): anon0 - Calculations.dfy(47,2): anon5_Else -Calculations.dfy(75,13): Error: index out of range -Execution trace: - (0,0): anon0 - (0,0): anon12_Then -Calculations.dfy(75,17): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon12_Then - -Dafny program verifier finished with 6 verified, 6 errors - -------------------- IteratorResolution.dfy -------------------- IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int) @@ -2259,209 +2231,51 @@ Execution trace: (0,0): anon0 Dafny program verifier finished with 87 verified, 33 errors -out.tmp.dfy(33,11): Error: index out of range -Execution trace: - (0,0): anon0 -out.tmp.dfy(69,37): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon12_Then -out.tmp.dfy(70,52): Error: possible division by zero -Execution trace: - (0,0): anon0 - (0,0): anon12_Else - (0,0): anon3 - (0,0): anon13_Else -out.tmp.dfy(71,22): Error: target object may be null -Execution trace: - (0,0): anon0 - (0,0): anon12_Then - (0,0): anon3 - (0,0): anon13_Then - (0,0): anon6 -out.tmp.dfy(88,24): Error: target object may be null -Execution trace: - (0,0): anon0 - out.tmp.dfy(87,5): anon8_LoopHead - (0,0): anon8_LoopBody - (0,0): anon9_Then -out.tmp.dfy(122,5): Error: call may violate context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon4_Else - (0,0): anon3 -out.tmp.dfy(135,9): Error: call may violate context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Then -out.tmp.dfy(137,9): Error: call may violate context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -out.tmp.dfy(177,9): Error: assignment may update an object field not in the enclosing context's modifies clause -Execution trace: - (0,0): anon0 - (0,0): anon22_Else - (0,0): anon24_Else - (0,0): anon26_Else - (0,0): anon28_Then - (0,0): anon29_Then - (0,0): anon19 -out.tmp.dfy(199,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Then -out.tmp.dfy(205,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon3 - (0,0): anon7_Then -out.tmp.dfy(207,14): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon6_Else - (0,0): anon3 - (0,0): anon7_Else -out.tmp.dfy(245,24): Error BP5002: A precondition for this call might not hold. -out.tmp.dfy(226,30): Related location: This is the precondition that might not hold. -Execution trace: - (0,0): anon0 - out.tmp.dfy(242,19): anon3_Else - (0,0): anon2 -out.tmp.dfy(265,12): Error: assertion violation -Execution trace: - (0,0): anon0 -out.tmp.dfy(275,12): Error: assertion violation -Execution trace: - (0,0): anon0 -out.tmp.dfy(285,6): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -out.tmp.dfy(388,14): Error: assertion violation + +Dafny program verifier finished with 0 verified, 0 errors + +-------------------- LetExpr.dfy -------------------- +LetExpr.dfy(5,12): Error: assertion violation Execution trace: (0,0): anon0 - out.tmp.dfy(384,5): anon7_LoopHead - (0,0): anon7_LoopBody - out.tmp.dfy(384,5): anon8_Else - (0,0): anon9_Then -out.tmp.dfy(414,14): Error: assertion violation +LetExpr.dfy(104,21): Error: assertion violation Execution trace: (0,0): anon0 - (0,0): anon7_Then - (0,0): anon8_Then - (0,0): anon3 -out.tmp.dfy(451,3): Error BP5003: A postcondition might not hold on this return path. -out.tmp.dfy(445,11): Related location: This is the postcondition that might not hold. + (0,0): anon11_Then + +Dafny program verifier finished with 28 verified, 2 errors + +Dafny program verifier finished with 0 verified, 0 errors + +-------------------- Calculations.dfy -------------------- +Calculations.dfy(3,6): Error: index out of range Execution trace: (0,0): anon0 - (0,0): anon18_Else - (0,0): anon23_Then (0,0): anon24_Then - (0,0): anon15 - (0,0): anon25_Else -out.tmp.dfy(475,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon7 -out.tmp.dfy(480,10): Error: assertion violation +Calculations.dfy(8,15): Error: index out of range Execution trace: (0,0): anon0 -out.tmp.dfy(490,4): Error: cannot prove termination; try supplying a decreases clause -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -out.tmp.dfy(498,10): Error BP5003: A postcondition might not hold on this return path. -out.tmp.dfy(499,41): Related location: This is the postcondition that might not hold. -Execution trace: - (0,0): anon0 - (0,0): anon6_Else -out.tmp.dfy(544,12): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon3_Then - (0,0): anon2 -out.tmp.dfy(558,20): Error: left-hand sides 0 and 1 may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon27_Then - (0,0): anon28_Then - (0,0): anon4 - (0,0): anon29_Then - (0,0): anon30_Then - (0,0): anon9 - (0,0): anon31_Then - (0,0): anon32_Then - (0,0): anon12 -out.tmp.dfy(560,15): Error: left-hand sides 1 and 2 may refer to the same location -Execution trace: - (0,0): anon0 - (0,0): anon27_Then - out.tmp.dfy(553,17): anon28_Else - (0,0): anon4 - (0,0): anon29_Else - (0,0): anon30_Then - (0,0): anon9 - (0,0): anon31_Else - (0,0): anon35_Then - (0,0): anon36_Then - (0,0): anon37_Then - (0,0): anon22 - (0,0): anon38_Then -out.tmp.dfy(567,25): Error: target object may be null -Execution trace: - (0,0): anon0 -out.tmp.dfy(580,10): Error: assertion violation -Execution trace: - (0,0): anon0 -out.tmp.dfy(606,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 -out.tmp.dfy(625,10): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon8_Then - (0,0): anon9_Then - (0,0): anon4 - (0,0): anon10_Then - (0,0): anon7 -out.tmp.dfy(639,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Execution trace: - (0,0): anon0 - (0,0): anon5_Then - (0,0): anon6_Then - (0,0): anon3 -out.tmp.dfy(641,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate + (0,0): anon26_Then +Calculations.dfy(8,19): Error: assertion violation Execution trace: (0,0): anon0 - (0,0): anon5_Else -out.tmp.dfy(655,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate + (0,0): anon26_Then +Calculations.dfy(52,12): Error: assertion violation Execution trace: (0,0): anon0 - -Dafny program verifier finished with 87 verified, 33 errors - --------------------- LetExpr.dfy -------------------- -LetExpr.dfy(5,12): Error: assertion violation + Calculations.dfy(47,3): anon5_Else +Calculations.dfy(75,15): Error: index out of range Execution trace: (0,0): anon0 -LetExpr.dfy(104,21): Error: assertion violation + (0,0): anon12_Then +Calculations.dfy(75,19): Error: assertion violation Execution trace: (0,0): anon0 - (0,0): anon11_Then + (0,0): anon12_Then -Dafny program verifier finished with 28 verified, 2 errors -out.tmp.dfy(66,12): Error: assertion violation -Execution trace: - (0,0): anon0 -out.tmp.dfy(157,21): Error: assertion violation -Execution trace: - (0,0): anon0 - (0,0): anon11_Then +Dafny program verifier finished with 9 verified, 6 errors -Dafny program verifier finished with 28 verified, 2 errors +Dafny program verifier finished with 0 verified, 0 errors Dafny program verifier finished with 37 verified, 0 errors Compiled assembly into Compilation.exe diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy index 59191ac3..f10d2e45 100644 --- a/Test/dafny0/Calculations.dfy +++ b/Test/dafny0/Calculations.dfy @@ -1,29 +1,29 @@ method CalcTest0(s: seq) { - calc { - s[0]; // error: ill-formed line - } - - calc { - 2; - { assert s[0] == 1; } // error: ill-formed hint - 1 + 1; - } - - if (|s| > 0) { - calc { - s[0]; // OK: well-formed in this context - <= { assert s[0] == s[0]; } - s[0]; - } - } - assume forall x :: x in s ==> x >= 0; - calc { - 0 < |s|; - ==> { assert s[0] >= 0; } // OK: well-formed after previous line - s[0] >= 0; // OK: well-formed after previous line + calc { + s[0]; // error: ill-formed line + } + + calc { + 2; + { assert s[0] == 1; } // error: ill-formed hint + 1 + 1; + } + + if (|s| > 0) { + calc { + s[0]; // OK: well-formed in this context + <= { assert s[0] == s[0]; } + s[0]; + } + } + assume forall x :: x in s ==> x >= 0; + calc { + 0 < |s|; + ==> { assert s[0] >= 0; } // OK: well-formed after previous line + s[0] >= 0; // OK: well-formed after previous line <==> { assert s[0] >= 0; } // OK: well-formed when the previous line is well-formed s[0] > 0 || s[0] == 0; // OK: well-formed when the previous line is well-formed - } + } calc { // same as the last one, but well-formedness is checked in reverse order s[0] + 1 > 0; @@ -35,48 +35,92 @@ method CalcTest0(s: seq) { } method CalcTest1(x: int, y: int) { - calc { - x + y; - { assume x == 0; } - y; - } - assert x == 0; // OK: follows from x + y == y; + calc { + x + y; + { assume x == 0; } + y; + } + assert x == 0; // OK: follows from x + y == y; } method CalcTest2(x: int, y: int) { - calc { - x + y; - { assume x == 0; } - y + x; - } - assert x == 0; // error: even though assumed above, is not exported by the calculation + calc { + x + y; + { assume x == 0; } + y + x; + } + assert x == 0; // error: even though assumed above, is not exported by the calculation } // calc expression: function CalcTest3(s: seq): int { - calc < { - 0; - { assume |s| == 5; } - |s|; - } - s[0] + calc < { + 0; + { assume |s| == 5; } + |s|; + } + s[0] } // dangling hints: method CalcTest4(s: seq) - requires forall n | n in s :: n > 0; + requires forall n | n in s :: n > 0; { - calc { - 1 + 1; - { assert 1 + 1 == 2; } - } - calc { - 2; - { assert s[0] > 0; } // error: ill-formed hint - } - calc { - |s| > 0; - ==> { assert s[0] > 0; } // okay - } - + calc { + 1 + 1; + { assert 1 + 1 == 2; } + } + calc { + 2; + { assert s[0] > 0; } // error: ill-formed hint + } + calc { + |s| > 0; + ==> { assert s[0] > 0; } // okay + } + } + +// ------------- tests for the pretty printer ------------- + +lemma CalcPrinting() +{ + calc < { + 2; + <= { SubLemma(); } + 3; + 5; + < { assert 5 < 6 <= 5+1; SubLemma(); assert 6 < 7; } + 7; + 11; + { SubLemma(); } // dangling hint + } + calc < { + 13; + } + calc { + 17; + == { SubLemma(); } // dangling hint, following operator + } + calc <= { + 19; + <= + { SubLemma(); } + { assert 19 + 23 == 42; } + calc { 811; } + { assert 42 < 100; } + 23; + { calc < { + 71; { assert 71 % 19 != 0; } 73; + } } + 29; + calc < { + 311; 313; 331; + } + 31; + } + calc { + } +} + +lemma SubLemma() diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 61f7c2c2..ae80dc89 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -26,7 +26,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy Predicates.dfy Skeletons.dfy OpaqueFunctions.dfy Maps.dfy LiberalEquality.dfy RefinementModificationChecking.dfy TailCalls.dfy - Calculations.dfy IteratorResolution.dfy Iterators.dfy + IteratorResolution.dfy Iterators.dfy RankPos.dfy RankNeg.dfy Computations.dfy ComputationsNeg.dfy Include.dfy) do ( @@ -41,11 +41,11 @@ for %%f in (Superposition.dfy) do ( %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp /tracePOs %* %%f ) -for %%f in (SmallTests.dfy LetExpr.dfy) do ( +for %%f in (SmallTests.dfy LetExpr.dfy Calculations.dfy) do ( echo. echo -------------------- %%f -------------------- %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.tmp.dfy %* %%f - %DAFNY_EXE% /compile:0 %* out.tmp.dfy + %DAFNY_EXE% /noVerify /compile:0 %* out.tmp.dfy ) %DAFNY_EXE% %* Compilation.dfy -- cgit v1.2.3