From 84edbb50f42361e7adb650ad8f3b9747f5fb4654 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 14 Nov 2011 23:47:59 -0800 Subject: Dafny: added let expressions (syntax: "var x := E0; E1") Dafny: firmed up semantics of assert/assume expressions (the condition is now good for all program control paths that pass through the expression) Dafny: various implementation clean-ups --- Dafny/Compiler.cs | 11 +++ Dafny/Dafny.atg | 33 +++++-- Dafny/DafnyAst.cs | 21 ++++ Dafny/Parser.cs | 93 +++++++++++------- Dafny/Printer.cs | 19 +++- Dafny/Resolver.cs | 24 +++++ Dafny/Scanner.cs | 102 ++++++++++--------- Dafny/Translator.cs | 247 +++++++++++++++++++++++++++++------------------ Test/dafny0/Answer | 27 +++++- Test/dafny0/LetExpr.dfy | 109 +++++++++++++++++++++ Test/dafny0/PredExpr.dfy | 30 +++++- Test/dafny0/runtest.bat | 2 +- 12 files changed, 524 insertions(+), 194 deletions(-) create mode 100644 Test/dafny0/LetExpr.dfy diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index de863e39..d0e0cb0e 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -1667,6 +1667,17 @@ namespace Microsoft.Dafny { wr.Write(")"); } + } else if (expr is LetExpr) { + var e = (LetExpr)expr; + // Since there are no OldExpr's in an expression to be compiled, we can just do a regular substitution + // without having to worry about old-capture. + var substMap = new Dictionary(); + Contract.Assert(e.Vars.Count == e.RHSs.Count); // checked by resolution + for (int i = 0; i < e.Vars.Count; i++) { + substMap.Add(e.Vars[i], e.RHSs[i]); + } + TrExpr(Translator.Substitute(e.Body, null, substMap)); + } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; Contract.Assert(e.Bounds != null); // for non-ghost quantifiers, the resolver would have insisted on finding bounds diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 8a9108f0..2eaaca7f 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -716,7 +716,7 @@ Rhs VarDeclStatement<.out Statement/*!*/ s.> = (. IToken x = null, assignTok = null; bool isGhost = false; VarDecl/*!*/ d; - AssignmentRhs r; Expression lhs0; + AssignmentRhs r; IdentifierExpr lhs0; List lhss = new List(); List rhss = new List(); .) @@ -727,7 +727,10 @@ VarDeclStatement<.out Statement/*!*/ s.> { "," LocalIdentTypeOptional (. lhss.Add(d); .) } - [ ":=" (. assignTok = t; lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); .) + [ ":=" (. assignTok = t; + lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); + lhs0.Var = lhss[0]; lhs0.Type = lhss[0].OptionalType; // resolve here + .) Rhs (. rhss.Add(r); .) { "," Rhs (. rhss.Add(r); .) } @@ -1204,20 +1207,34 @@ EndlessExpression = (. IToken/*!*/ x; Expression e0, e1; e = dummyExpr; + BoundVar d; + List letVars; List letRHSs; .) - ( "if" (. x = t; .) + ( "if" (. x = t; .) Expression "then" Expression - "else" Expression (. e = new ITEExpr(x, e, e0, e1); .) + "else" Expression (. e = new ITEExpr(x, e, e0, e1); .) | MatchExpression | QuantifierGuts | ComprehensionExpr - | "assert" (. x = t; .) + | "assert" (. x = t; .) Expression ";" - Expression (. e = new AssertExpr(x, e0, e1); .) - | "assume" (. x = t; .) + Expression (. e = new AssertExpr(x, e0, e1); .) + | "assume" (. x = t; .) Expression ";" - Expression (. e = new AssumeExpr(x, e0, e1); .) + Expression (. e = new AssumeExpr(x, e0, e1); .) + | "var" (. x = t; + letVars = new List(); + letRHSs = new List(); .) + IdentTypeOptional (. letVars.Add(d); .) + { "," IdentTypeOptional (. letVars.Add(d); .) + } + ":=" + Expression (. letRHSs.Add(e); .) + { "," Expression (. letRHSs.Add(e); .) + } + ";" + Expression (. e = new LetExpr(x, letVars, letRHSs, e); .) ) . MatchExpression diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index e07c6f1d..8272736c 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -2593,6 +2593,27 @@ namespace Microsoft.Dafny { } } + public class LetExpr : Expression + { + public readonly List Vars; + public readonly List RHSs; + public readonly Expression Body; + public LetExpr(IToken tok, List vars, List rhss, Expression body) + : base(tok) { + Vars = vars; + RHSs = rhss; + Body = body; + } + public override IEnumerable SubExpressions { + get { + foreach (var rhs in RHSs) { + yield return rhs; + } + yield return Body; + } + } + } + /// /// A ComprehensionExpr has the form: /// BINDER x Attributes | Range(x) :: Term(x) diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index 0dc30e8a..583fcc61 100644 --- a/Dafny/Parser.cs +++ b/Dafny/Parser.cs @@ -23,7 +23,7 @@ public class Parser { const bool T = true; const bool x = false; const int minErrDist = 2; - + public Scanner/*!*/ scanner; public Errors/*!*/ errors; @@ -134,10 +134,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List= minErrDist) errors.SemErr(t, msg); errDist = 0; } - - public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { - Contract.Requires(tok != null); - Contract.Requires(msg != null); + + public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); errors.SemErr(tok, msg); } @@ -150,15 +150,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List theImports; @@ -1100,7 +1100,7 @@ List/*!*/ decreases) { void VarDeclStatement(out Statement/*!*/ s) { IToken x = null, assignTok = null; bool isGhost = false; VarDecl/*!*/ d; - AssignmentRhs r; Expression lhs0; + AssignmentRhs r; IdentifierExpr lhs0; List lhss = new List(); List rhss = new List(); @@ -1119,7 +1119,10 @@ List/*!*/ decreases) { } if (la.kind == 49) { Get(); - assignTok = t; lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); + assignTok = t; + lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name); + lhs0.Var = lhss[0]; lhs0.Type = lhss[0].OptionalType; // resolve here + Rhs(out r, lhs0); rhss.Add(r); while (la.kind == 19) { @@ -1789,7 +1792,7 @@ List/*!*/ decreases) { e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); break; } - case 38: case 55: case 61: case 62: case 63: case 98: case 99: case 100: case 101: { + case 18: case 38: case 55: case 61: case 62: case 63: case 98: case 99: case 100: case 101: { EndlessExpression(out e); break; } @@ -1845,6 +1848,8 @@ List/*!*/ decreases) { IToken/*!*/ x; Expression e0, e1; e = dummyExpr; + BoundVar d; + List letVars; List letRHSs; switch (la.kind) { case 55: { @@ -1888,6 +1893,31 @@ List/*!*/ decreases) { e = new AssumeExpr(x, e0, e1); break; } + case 18: { + Get(); + x = t; + letVars = new List(); + letRHSs = new List(); + IdentTypeOptional(out d); + letVars.Add(d); + while (la.kind == 19) { + Get(); + IdentTypeOptional(out d); + letVars.Add(d); + } + Expect(49); + Expression(out e); + letRHSs.Add(e); + while (la.kind == 19) { + Get(); + Expression(out e); + letRHSs.Add(e); + } + Expect(17); + Expression(out e); + e = new LetExpr(x, letVars, letRHSs, e); + break; + } default: SynErr(133); break; } } @@ -2277,13 +2307,13 @@ List/*!*/ decreases) { public void Parse() { la = new Token(); - la.val = ""; + la.val = ""; Get(); Dafny(); - Expect(0); + Expect(0); } - + static readonly bool[,]/*!*/ set = { {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, @@ -2291,17 +2321,17 @@ List/*!*/ decreases) { {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}, + {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}, {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}, + {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}, {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}, + {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}, {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, T,T,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,x,x, T,T,T,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x}, - {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x} + {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x} }; } // end Parser @@ -2310,20 +2340,18 @@ List/*!*/ decreases) { public class Errors { public int count = 0; // number of errors detected public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream - public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text - public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text - + public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text + public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text + public void SynErr(string filename, int line, int col, int n) { - SynErr(filename, line, col, GetSyntaxErrorString(n)); - } - - public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) { - Contract.Requires(msg != null); + SynErr(filename, line, col, GetSyntaxErrorString(n)); + } + public virtual void SynErr(string filename, int line, int col, string msg) { + Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col, msg); count++; - } - - string GetSyntaxErrorString(int n) { + } + string GetSyntaxErrorString(int n) { string s; switch (n) { case 0: s = "EOF expected"; break; @@ -2473,7 +2501,7 @@ public class Errors { default: s = "error " + n; break; } - return s; + return s; } public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors @@ -2481,9 +2509,8 @@ public class Errors { Contract.Requires(msg != null); SemErr(tok.filename, tok.line, tok.col, msg); } - public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) { - Contract.Requires(msg != null); + Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col, msg); count++; } diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs index 10099bf4..5b9ba1d6 100644 --- a/Dafny/Printer.cs +++ b/Dafny/Printer.cs @@ -1014,6 +1014,23 @@ namespace Microsoft.Dafny { } if (parensNeeded) { wr.Write(")"); } + } else if (expr is LetExpr) { + var e = (LetExpr)expr; + bool parensNeeded = !isRightmost; + if (parensNeeded) { wr.Write("("); } + string sep = ""; + foreach (var v in e.Vars) { + wr.Write("{0}{1}", sep, v.Name); + PrintType(": ", v.Type); + sep = ", "; + } + wr.Write(" := "); + PrintExpressionList(e.RHSs); + wr.Write("; "); + PrintExpression(e.Body); + if (parensNeeded) { wr.Write(")"); } + + } else if (expr is QuantifierExpr) { QuantifierExpr e = (QuantifierExpr)expr; bool parensNeeded = !isRightmost; @@ -1106,8 +1123,8 @@ namespace Microsoft.Dafny { string sep = ""; foreach (BoundVar bv in boundVars) { wr.Write("{0}{1}", sep, bv.Name); - sep = ", "; PrintType(": ", bv.Type); + sep = ", "; } PrintAttributes(attrs); if (range != null) { diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index b6bc4059..81216f32 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -2751,6 +2751,30 @@ namespace Microsoft.Dafny { } e.ResolvedOp = ResolveOp(e.Op, e.E1.Type); + } else if (expr is LetExpr) { + var e = (LetExpr)expr; + foreach (var rhs in e.RHSs) { + ResolveExpression(rhs, twoState); + } + scope.PushMarker(); + if (e.Vars.Count != e.RHSs.Count) { + Error(expr, "let expression must have same number of bound variables (found {0}) as RHSs (found {1})", e.Vars.Count, e.RHSs.Count); + } + int i = 0; + foreach (var v in e.Vars) { + if (!scope.Push(v.Name, v)) { + Error(v, "Duplicate let-variable name: {0}", v.Name); + } + ResolveType(v.tok, v.Type); + if (i < e.RHSs.Count && !UnifyTypes(v.Type, e.RHSs[i].Type)) { + Error(e.RHSs[i].tok, "type of RHS ({0}) does not match type of bound variable ({1})", e.RHSs[i].Type, v.Type); + } + i++; + } + ResolveExpression(e.Body, twoState); + scope.PopMarker(); + expr.Type = e.Body.Type; + } else if (expr is QuantifierExpr) { QuantifierExpr e = (QuantifierExpr)expr; int prevErrorCount = ErrorCount; diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs index 634abf45..1ab06974 100644 --- a/Dafny/Scanner.cs +++ b/Dafny/Scanner.cs @@ -19,7 +19,7 @@ public class Buffer { // a) whole stream in buffer // b) part of stream in buffer // 2) non seekable stream (network, console) - + public const int EOF = 65535 + 1; // char.MaxValue + 1; const int MIN_BUFFER_LENGTH = 1024; // 1KB const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB @@ -31,17 +31,15 @@ public class Buffer { Stream/*!*/ stream; // input stream (seekable) bool isUserStream; // was the stream opened by the user? - [ContractInvariantMethod] - void ObjectInvariant(){ - Contract.Invariant(buf != null); - Contract.Invariant(stream != null); - } - -// [NotDelayed] - public Buffer (Stream/*!*/ s, bool isUserStream) : base() { +[ContractInvariantMethod] +void ObjectInvariant(){ + Contract.Invariant(buf != null); + Contract.Invariant(stream != null);} + [NotDelayed] + public Buffer (Stream/*!*/ s, bool isUserStream) :base() { Contract.Requires(s != null); stream = s; this.isUserStream = isUserStream; - + int fl, bl; if (s.CanSeek) { fl = (int) s.Length; @@ -53,12 +51,12 @@ public class Buffer { buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH]; fileLen = fl; bufLen = bl; - + if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start) else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid if (bufLen == fileLen && s.CanSeek) Close(); } - + protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor Contract.Requires(b != null); buf = b.buf; @@ -75,14 +73,14 @@ public class Buffer { } ~Buffer() { Close(); } - + protected void Close() { if (!isUserStream && stream != null) { stream.Close(); //stream = null; } } - + public virtual int Read () { if (bufPos < bufLen) { return buf[bufPos++]; @@ -102,7 +100,7 @@ public class Buffer { Pos = curPos; return ch; } - + public string/*!*/ GetString (int beg, int end) { Contract.Ensures(Contract.Result() != null); int len = 0; @@ -141,7 +139,7 @@ public class Buffer { } } } - + // Read the next chunk of bytes from the stream, increases the buffer // if needed and updates the fields fileLen and bufLen. // Returns the number of bytes read. @@ -215,20 +213,19 @@ public class Scanner { const int noSym = 104; - [ContractInvariantMethod] - void objectInvariant(){ - Contract.Invariant(buffer!=null); - Contract.Invariant(t != null); - Contract.Invariant(start != null); - Contract.Invariant(tokens != null); - Contract.Invariant(pt != null); - Contract.Invariant(tval != null); - Contract.Invariant(Filename != null); - Contract.Invariant(errorHandler != null); - } - +[ContractInvariantMethod] +void objectInvariant(){ + Contract.Invariant(buffer!=null); + Contract.Invariant(t != null); + Contract.Invariant(start != null); + Contract.Invariant(tokens != null); + Contract.Invariant(pt != null); + Contract.Invariant(tval != null); + Contract.Invariant(Filename != null); + Contract.Invariant(errorHandler != null); +} public Buffer/*!*/ buffer; // scanner buffer - + Token/*!*/ t; // current token int ch; // current input character int pos; // byte position of current character @@ -239,13 +236,13 @@ public class Scanner { Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy) Token/*!*/ pt; // current peek token - + char[]/*!*/ tval = new char[128]; // text of current token int tlen; // length of current token - + private string/*!*/ Filename; private Errors/*!*/ errorHandler; - + static Scanner() { start = new Hashtable(128); for (int i = 39; i <= 39; ++i) start[i] = 1; @@ -293,9 +290,9 @@ public class Scanner { start[Buffer.EOF] = -1; } - -// [NotDelayed] - public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() { + + [NotDelayed] + public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){ Contract.Requires(fileName != null); Contract.Requires(errorHandler != null); this.errorHandler = errorHandler; @@ -305,14 +302,15 @@ public class Scanner { Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read); buffer = new Buffer(stream, false); Filename = fileName; + Init(); } catch (IOException) { throw new FatalError("Cannot open file " + fileName); } } - -// [NotDelayed] - public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() { + + [NotDelayed] + public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){ Contract.Requires(s != null); Contract.Requires(errorHandler != null); Contract.Requires(fileName != null); @@ -321,9 +319,10 @@ public class Scanner { buffer = new Buffer(s, true); this.errorHandler = errorHandler; this.Filename = fileName; + Init(); } - + void Init() { pos = -1; line = 1; col = 0; oldEols = 0; @@ -344,11 +343,11 @@ public class Scanner { Contract.Ensures(Contract.Result() != null); int p = buffer.Pos; int ch = buffer.Read(); - // replace isolated '\r' by '\n' in order to make + // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; while (ch != EOL && ch != Buffer.EOF){ - ch = buffer.Read(); + ch = buffer.Read(); // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; @@ -359,7 +358,7 @@ public class Scanner { } void NextCh() { - if (oldEols > 0) { ch = EOL; oldEols--; } + if (oldEols > 0) { ch = EOL; oldEols--; } else { // pos = buffer.Pos; // ch = buffer.Read(); col++; @@ -367,9 +366,9 @@ public class Scanner { // // eol handling uniform across Windows, Unix and Mac // if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; // if (ch == EOL) { line++; col = 0; } - + while (true) { - pos = buffer.Pos; + pos = buffer.Pos; ch = buffer.Read(); col++; // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac @@ -419,7 +418,7 @@ public class Scanner { return; } - + } } @@ -557,13 +556,10 @@ public class Scanner { t.pos = pos; t.col = col; t.line = line; t.filename = this.Filename; int state; - if (start.ContainsKey(ch)) { - Contract.Assert(start[ch] != null); - state = (int) start[ch]; - } + if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); } else { state = 0; } tlen = 0; AddCh(); - + switch (state) { case -1: { t.kind = eofSym; break; } // NextCh already done case 0: { @@ -763,14 +759,14 @@ public class Scanner { t.val = new String(tval, 0, tlen); return t; } - + private void SetScannerBehindT() { buffer.Pos = t.pos; NextCh(); line = t.line; col = t.col; for (int i = 0; i < tlen; i++) NextCh(); } - + // get the next token (possibly a token already seen during peeking) public Token/*!*/ Scan () { Contract.Ensures(Contract.Result() != null); @@ -791,7 +787,7 @@ public class Scanner { } pt = pt.next; } while (pt.kind > maxT); // skip pragmas - + return pt; } diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 028891b5..f3373736 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -1738,7 +1738,7 @@ namespace Microsoft.Dafny { return r; } else if (expr is OldExpr) { OldExpr e = (OldExpr)expr; - return new Bpl.OldExpr(expr.tok, IsTotal(e.E, etran)); + return IsTotal(e.E, etran.Old); } else if (expr is MultiSetFormingExpr) { MultiSetFormingExpr e = (MultiSetFormingExpr)expr; return IsTotal(e.E, etran); @@ -1780,6 +1780,14 @@ namespace Microsoft.Dafny { } Bpl.Expr r = BplAnd(t0, t1); return z == null ? r : BplAnd(r, z); + } else if (expr is LetExpr) { + var e = (LetExpr)expr; + Bpl.Expr total = Bpl.Expr.True; + foreach (var rhs in e.RHSs) { + total = BplAnd(total, IsTotal(rhs, etran)); + } + return BplAnd(total, IsTotal(etran.GetSubstitutedBody(e), etran)); + } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; var total = IsTotal(e.Term, etran); @@ -1797,7 +1805,7 @@ namespace Microsoft.Dafny { Bpl.Expr gTotal = IsTotal(e.Guard, etran); Bpl.Expr g = etran.TrExpr(e.Guard); Bpl.Expr bTotal = IsTotal(e.Body, etran); - if (e is AssertExpr) { + if (e is AssertExpr || CommandLineOptions.Clo.DisallowSoundnessCheating) { return BplAnd(gTotal, BplAnd(g, bTotal)); } else { return BplAnd(gTotal, Bpl.Expr.Imp(g, bTotal)); @@ -1896,7 +1904,7 @@ namespace Microsoft.Dafny { return CanCallAssumption(dtv.Arguments, etran); } else if (expr is OldExpr) { OldExpr e = (OldExpr)expr; - return new Bpl.OldExpr(expr.tok, CanCallAssumption(e.E, etran)); + return CanCallAssumption(e.E, etran.Old); } else if (expr is MultiSetFormingExpr) { MultiSetFormingExpr e = (MultiSetFormingExpr)expr; return CanCallAssumption(e.E, etran); @@ -1926,6 +1934,14 @@ namespace Microsoft.Dafny { break; } return BplAnd(t0, t1); + } else if (expr is LetExpr) { + var e = (LetExpr)expr; + Bpl.Expr canCall = Bpl.Expr.True; + foreach (var rhs in e.RHSs) { + canCall = BplAnd(canCall, CanCallAssumption(rhs, etran)); + } + return BplAnd(canCall, CanCallAssumption(etran.GetSubstitutedBody(e), etran)); + } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; var total = CanCallAssumption(e.Term, etran); @@ -1941,11 +1957,11 @@ namespace Microsoft.Dafny { } else if (expr is PredicateExpr) { var e = (PredicateExpr)expr; Bpl.Expr gCanCall = CanCallAssumption(e.Guard, etran); - Bpl.Expr g = etran.TrExpr(e.Guard); Bpl.Expr bCanCall = CanCallAssumption(e.Body, etran); - if (e is AssertExpr) { - return BplAnd(gCanCall, BplAnd(g, bCanCall)); + if (e is AssertExpr || CommandLineOptions.Clo.DisallowSoundnessCheating) { + return BplAnd(gCanCall, bCanCall); } else { + Bpl.Expr g = etran.TrExpr(e.Guard); return BplAnd(gCanCall, Bpl.Expr.Imp(g, bCanCall)); } } else if (expr is ITEExpr) { @@ -2328,6 +2344,13 @@ namespace Microsoft.Dafny { break; } + } else if (expr is LetExpr) { + var e = (LetExpr)expr; + foreach (var rhs in e.RHSs) { + CheckWellformed(rhs, options, locals, builder, etran); + } + CheckWellformedWithResult(etran.GetSubstitutedBody(e), options, result, resultType, locals, builder, etran); + } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran); @@ -2346,7 +2369,7 @@ namespace Microsoft.Dafny { } else if (expr is PredicateExpr) { var e = (PredicateExpr)expr; CheckWellformed(e.Guard, options, locals, builder, etran); - if (e is AssertExpr) { + if (e is AssertExpr || CommandLineOptions.Clo.DisallowSoundnessCheating) { bool splitHappened; var ss = TrSplitExpr(e.Guard, etran, out splitHappened); if (!splitHappened) { @@ -4146,7 +4169,7 @@ namespace Microsoft.Dafny { Contract.Requires(locals != null); Contract.Requires(etran != null); - Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver); + Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver, dafnyReceiver.Type); Bpl.ExprSeq ins = new Bpl.ExprSeq(); if (!method.IsStatic) { if (bReceiver == null) { @@ -5002,11 +5025,13 @@ namespace Microsoft.Dafny { internal class BoogieWrapper : Expression { public readonly Bpl.Expr Expr; - public BoogieWrapper(Bpl.Expr expr) + public BoogieWrapper(Bpl.Expr expr, Type dafnyType) : base(expr.tok) { Contract.Requires(expr != null); + Contract.Requires(dafnyType != null); Expr = expr; + Type = dafnyType; // resolve immediately } } @@ -5016,7 +5041,7 @@ namespace Microsoft.Dafny { public readonly PredefinedDecls predef; public readonly Translator translator; public readonly string This; - public readonly string modifiesFrame = "$_Frame"; // the name of the context's frame variable. + public readonly string modifiesFrame; // the name of the context's frame variable. readonly Function applyLimited_CurrentFunction; public readonly int layerOffset = 0; public int Statistics_CustomLayerFunctionCount = 0; @@ -5027,66 +5052,60 @@ namespace Microsoft.Dafny { Contract.Invariant(predef != null); Contract.Invariant(translator != null); Contract.Invariant(This != null); + Contract.Invariant(modifiesFrame != null); Contract.Invariant(layerOffset == 0 || layerOffset == 1); Contract.Invariant(0 <= Statistics_CustomLayerFunctionCount); } - public ExpressionTranslator(Translator translator, PredefinedDecls predef, IToken heapToken) { + /// + /// This is the most general constructor. It is private and takes all the parameters. Whenever + /// one ExpressionTranslator is constructed from another, unchanged parameters are just copied in. + /// + ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar, + Function applyLimited_CurrentFunction, int layerOffset, string modifiesFrame) { + Contract.Requires(translator != null); Contract.Requires(predef != null); - Contract.Requires(heapToken != null); + Contract.Requires(heap != null); + Contract.Requires(thisVar != null); + Contract.Invariant(layerOffset == 0 || layerOffset == 1); + Contract.Invariant(modifiesFrame != null); + this.translator = translator; this.predef = predef; - this.HeapExpr = new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType); - this.This = "this"; + this.HeapExpr = heap; + this.This = thisVar; + this.applyLimited_CurrentFunction = applyLimited_CurrentFunction; + this.layerOffset = layerOffset; + this.modifiesFrame = modifiesFrame; } - public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap) { + public ExpressionTranslator(Translator translator, PredefinedDecls predef, IToken heapToken) + : this(translator, predef, new Bpl.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType)) { Contract.Requires(translator != null); Contract.Requires(predef != null); - Contract.Requires(heap != null); - this.translator = translator; - this.predef = predef; - this.HeapExpr = heap; - this.This = "this"; + Contract.Requires(heapToken != null); } - public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar) { + public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap) + : this(translator, predef, heap, "this") { Contract.Requires(translator != null); Contract.Requires(predef != null); Contract.Requires(heap != null); - Contract.Requires(thisVar != null); - this.translator = translator; - this.predef = predef; - this.HeapExpr = heap; - this.This = thisVar; } - ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction, int layerOffset) - { - Contract.Requires(translator != null); - Contract.Requires(predef != null); - Contract.Requires(heap != null); - this.translator = translator; - this.predef = predef; - this.HeapExpr = heap; - this.applyLimited_CurrentFunction = applyLimited_CurrentFunction; - this.This = "this"; - this.layerOffset = layerOffset; + public ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, string thisVar) + : this(translator, predef, heap, thisVar, null, 0, "$_Frame") { + Contract.Requires(translator != null); + Contract.Requires(predef != null); + Contract.Requires(heap != null); + Contract.Requires(thisVar != null); } public ExpressionTranslator(ExpressionTranslator etran, string modifiesFrame) - { - Contract.Requires(etran != null); - Contract.Requires(modifiesFrame != null); - this.translator = etran.translator; - this.HeapExpr = etran.HeapExpr; - this.predef = etran.predef; - this.This = etran.This; - this.applyLimited_CurrentFunction = etran.applyLimited_CurrentFunction; - this.layerOffset = etran.layerOffset; - this.oldEtran = etran.oldEtran; - this.modifiesFrame = modifiesFrame; + : this(etran.translator, etran.predef, etran.HeapExpr, etran.This, etran.applyLimited_CurrentFunction, etran.layerOffset, modifiesFrame) { + Contract.Requires(etran != null); + Contract.Requires(modifiesFrame != null); } ExpressionTranslator oldEtran; @@ -5095,7 +5114,7 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.Result() != null); if (oldEtran == null) { - oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), applyLimited_CurrentFunction, layerOffset); + oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerOffset, modifiesFrame); } return oldEtran; } @@ -5111,7 +5130,7 @@ namespace Microsoft.Dafny { Contract.Requires(applyLimited_CurrentFunction != null); Contract.Ensures(Contract.Result() != null); - return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction, layerOffset); + return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset, modifiesFrame); } public ExpressionTranslator LayerOffset(int offset) { @@ -5119,7 +5138,7 @@ namespace Microsoft.Dafny { Contract.Requires(layerOffset + offset <= 1); Contract.Ensures(Contract.Result() != null); - return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction, layerOffset + offset); + return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset + offset, modifiesFrame); } public Bpl.IdentifierExpr TheFrame(IToken tok) @@ -5131,7 +5150,7 @@ namespace Microsoft.Dafny { Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "beta"); Bpl.Type fieldAlpha = predef.FieldName(tok, alpha); Bpl.Type ty = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.TypeSeq(predef.RefType, fieldAlpha), Bpl.Type.Bool); - return new Bpl.IdentifierExpr(tok, this.modifiesFrame ?? "$_Frame", ty); + return new Bpl.IdentifierExpr(tok, this.modifiesFrame, ty); } public Bpl.IdentifierExpr Tick() { @@ -5141,24 +5160,33 @@ namespace Microsoft.Dafny { return new Bpl.IdentifierExpr(Token.NoToken, "$Tick", predef.TickType); } - public Bpl.IdentifierExpr ModuleContextHeight() - { - Contract.Ensures(Contract.Result().Type != null); + public Bpl.IdentifierExpr ModuleContextHeight() { + Contract.Ensures(Contract.Result().Type != null); return new Bpl.IdentifierExpr(Token.NoToken, "$ModuleContextHeight", Bpl.Type.Int); } - public Bpl.IdentifierExpr FunctionContextHeight() - { - Contract.Ensures(Contract.Result().Type != null); + public Bpl.IdentifierExpr FunctionContextHeight() { + Contract.Ensures(Contract.Result().Type != null); return new Bpl.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Bpl.Type.Int); } - public Bpl.IdentifierExpr InMethodContext() - { - Contract.Ensures(Contract.Result().Type != null); + public Bpl.IdentifierExpr InMethodContext() { + Contract.Ensures(Contract.Result().Type != null); return new Bpl.IdentifierExpr(Token.NoToken, "$InMethodContext", Bpl.Type.Bool); } + public Expression GetSubstitutedBody(LetExpr e) { + Contract.Requires(e != null); + var substMap = new Dictionary(); + Contract.Assert(e.Vars.Count == e.RHSs.Count); // checked by resolution + for (int i = 0; i < e.Vars.Count; i++) { + Expression rhs = e.RHSs[i]; + substMap.Add(e.Vars[i], new BoogieWrapper(TrExpr(rhs), rhs.Type)); + } + return Translator.Substitute(e.Body, null, substMap); + } + + /// /// Translates Dafny expression "expr" into a Boogie expression. If the type of "expr" can be a boolean, then the /// token (source location) of the resulting expression is filled in (it wouldn't hurt if the token were always @@ -5329,7 +5357,7 @@ namespace Microsoft.Dafny { } else if (expr is OldExpr) { OldExpr e = (OldExpr)expr; - return new Bpl.OldExpr(expr.tok, TrExpr(e.E)); + return Old.TrExpr(e.E); } else if (expr is MultiSetFormingExpr) { MultiSetFormingExpr e = (MultiSetFormingExpr)expr; @@ -5344,7 +5372,6 @@ namespace Microsoft.Dafny { } else if (expr is FreshExpr) { FreshExpr e = (FreshExpr)expr; - Bpl.Expr oldHeap = new Bpl.OldExpr(expr.tok, HeapExpr); if (e.E.Type is SetType) { // generate: (forall $o: ref :: $o != null && X[Box($o)] ==> !old($Heap)[$o,alloc]) // TODO: trigger? @@ -5352,7 +5379,7 @@ namespace Microsoft.Dafny { Bpl.Expr o = new Bpl.IdentifierExpr(expr.tok, oVar); Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null); Bpl.Expr oInSet = TrInSet(expr.tok, o, e.E, ((SetType)e.E.Type).Arg); - Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, o, oldHeap)); + Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, o)); Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(oNotNull, oInSet), oIsFresh); return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(oVar), body); } else if (e.E.Type is SeqType) { @@ -5362,14 +5389,14 @@ namespace Microsoft.Dafny { Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar); Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), true, null, false); Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i); - Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, XsubI, oldHeap)); + Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, XsubI)); Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI), predef.Null); Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(iBounds, xsubiNotNull), oIsFresh); return new Bpl.ForallExpr(expr.tok, new Bpl.VariableSeq(iVar), body); } else { // generate: x == null || !old($Heap)[x] Bpl.Expr oNull = Bpl.Expr.Eq(TrExpr(e.E), predef.Null); - Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, TrExpr(e.E), oldHeap)); + Bpl.Expr oIsFresh = Bpl.Expr.Not(Old.IsAlloced(expr.tok, TrExpr(e.E))); return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.Or, oNull, oIsFresh); } @@ -5546,6 +5573,10 @@ namespace Microsoft.Dafny { } return Bpl.Expr.Binary(expr.tok, bOpcode, e0, e1); + } else if (expr is LetExpr) { + var e = (LetExpr)expr; + return TrExpr(GetSubstitutedBody(e)); + } else if (expr is QuantifierExpr) { QuantifierExpr e = (QuantifierExpr)expr; Bpl.VariableSeq bvars = new Bpl.VariableSeq(); @@ -5930,16 +5961,7 @@ namespace Microsoft.Dafny { Contract.Requires(e != null); Contract.Ensures(Contract.Result() != null); - return IsAlloced(tok, e, HeapExpr); - } - - Bpl.Expr IsAlloced(IToken tok, Bpl.Expr e, Bpl.Expr heap) { - Contract.Requires(tok != null); - Contract.Requires(e != null); - Contract.Requires(heap != null); - Contract.Ensures(Contract.Result() != null); - - return ReadHeap(tok, heap, e, predef.Alloc(tok)); + return ReadHeap(tok, HeapExpr, e, predef.Alloc(tok)); } public Bpl.Expr GoodRef(IToken tok, Bpl.Expr e, Type type) { @@ -6401,9 +6423,9 @@ namespace Microsoft.Dafny { var e = (ConcreteSyntaxExpression)expr; return TrSplitExpr(e.ResolvedExpression, splits, position, expandFunctions, etran); - } else if (expr is PredicateExpr) { - var e = (PredicateExpr)expr; - return TrSplitExpr(e.Body, splits, position, expandFunctions, etran); + } else if (expr is LetExpr) { + var e = (LetExpr)expr; + return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, expandFunctions, etran); } else if (expr is UnaryExpr) { var e = (UnaryExpr)expr; @@ -6474,15 +6496,33 @@ namespace Microsoft.Dafny { return true; } - } else if (expr is OldExpr) { - var e = (OldExpr)expr; - var ss = new List(); - if (TrSplitExpr(e.E, ss, position, expandFunctions, etran)) { + } else if (expr is PredicateExpr) { + var e = (PredicateExpr)expr; + // For a predicate expression in split position, the predicate can be used as an assumption. Unfortunately, + // this assumption is not generated in non-split positions (because I don't know how.) + // So, treat "assert/assume P; E" like "P ==> E". + if (position) { + var guard = etran.TrExpr(e.Guard); + var ss = new List(); + TrSplitExpr(e.Body, ss, position, expandFunctions, etran); + foreach (var s in ss) { + // as the source location in the following implication, use that of the translated "s" + splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, guard, s.E))); + } + } else { + var ss = new List(); + TrSplitExpr(e.Guard, ss, !position, expandFunctions, etran); + var rhs = etran.TrExpr(e.Body); foreach (var s in ss) { - splits.Add(new SplitExprInfo(s.IsFree, new Bpl.OldExpr(s.E.tok, s.E))); + // as the source location in the following implication, use that of the translated "s" + splits.Add(new SplitExprInfo(s.IsFree, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, s.E, rhs))); } - return true; } + return true; + + } else if (expr is OldExpr) { + var e = (OldExpr)expr; + return TrSplitExpr(e.E, splits, position, expandFunctions, etran.Old); } else if (expandFunctions && position && expr is FunctionCallExpr) { var fexp = (FunctionCallExpr)expr; @@ -6845,9 +6885,6 @@ namespace Microsoft.Dafny { var e = (DatatypeValue)expr; var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent; // prominent status continues, if we're looking for a variable whose type is a datatype return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q)); - } else if (expr is OldExpr) { - var e = (OldExpr)expr; - return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent); // prominent status continues } else if (expr is UnaryExpr) { var e = (UnaryExpr)expr; // both Not and SeqLength preserve prominence @@ -6965,7 +7002,7 @@ namespace Microsoft.Dafny { } } - static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary/*!*/ substMap) { + public static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary/*!*/ substMap) { Contract.Requires(expr != null); Contract.Requires(cce.NonNullDictionaryAndValues(substMap)); Contract.Ensures(Contract.Result() != null); @@ -7051,7 +7088,11 @@ namespace Microsoft.Dafny { } else if (expr is OldExpr) { OldExpr e = (OldExpr)expr; - Expression se = Substitute(e.E, receiverReplacement, substMap); // TODO: whoa, won't this do improper variable capture? + // Note, it is up to the caller to avoid variable capture. In most cases, this is not a + // problem, since variables have unique declarations. However, it is an issue if the substitution + // takes place inside an OldExpr. In those cases (see LetExpr), the caller can use a + // BoogieWrapper before calling Substitute. + Expression se = Substitute(e.E, receiverReplacement, substMap); if (se != e.E) { newExpr = new OldExpr(expr.tok, se); } @@ -7083,6 +7124,22 @@ namespace Microsoft.Dafny { newExpr = newBin; } + } else if (expr is LetExpr) { + var e = (LetExpr)expr; + var rhss = new List(); + bool anythingChanged = false; + foreach (var rhs in e.RHSs) { + var r = Substitute(rhs, receiverReplacement, substMap); + if (r != rhs) { + anythingChanged = true; + } + rhss.Add(r); + } + var body = Substitute(e.Body, receiverReplacement, substMap); + if (anythingChanged || body != e.Body) { + newExpr = new LetExpr(e.tok, e.Vars, rhss, body); + } + } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; Expression newRange = e.Range == null ? null : Substitute(e.Range, receiverReplacement, substMap); @@ -7109,10 +7166,12 @@ namespace Microsoft.Dafny { var e = (PredicateExpr)expr; Expression g = Substitute(e.Guard, receiverReplacement, substMap); Expression b = Substitute(e.Body, receiverReplacement, substMap); - if (expr is AssertExpr) { - newExpr = new AssertExpr(e.tok, g, b); - } else { - newExpr = new AssumeExpr(e.tok, g, b); + if (g != e.Guard || b != e.Body) { + if (expr is AssertExpr) { + newExpr = new AssertExpr(e.tok, g, b); + } else { + newExpr = new AssumeExpr(e.tok, g, b); + } } } else if (expr is ITEExpr) { diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 50c238fc..15cec24f 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1321,12 +1321,33 @@ CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost Dafny program verifier finished with 22 verified, 0 errors -------------------- PredExpr.dfy -------------------- -PredExpr.dfy(23,15): Error: value assigned to a nat must be non-negative +PredExpr.dfy(4,12): Error: condition in assert expression might not hold +Execution trace: + (0,0): anon3_Else +PredExpr.dfy(36,15): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon6_Else (0,0): anon7_Else -PredExpr.dfy(36,17): Error: condition in assert expression might not hold +PredExpr.dfy(49,17): Error: condition in assert expression might not hold +Execution trace: + (0,0): anon0 +PredExpr.dfy(74,14): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon8_Else + (0,0): anon3 + PredExpr.dfy(73,20): anon10_Else + (0,0): anon6 + +Dafny program verifier finished with 11 verified, 4 errors + +-------------------- LetExpr.dfy -------------------- +LetExpr.dfy(5,12): Error: assertion violation Execution trace: (0,0): anon0 +LetExpr.dfy(104,21): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon11_Then -Dafny program verifier finished with 9 verified, 2 errors +Dafny program verifier finished with 13 verified, 2 errors diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy new file mode 100644 index 00000000..703813d2 --- /dev/null +++ b/Test/dafny0/LetExpr.dfy @@ -0,0 +1,109 @@ +method M0(n: int) + requires var f := 100; n < f; +{ + assert n < 200; + assert 0 <= n; // error +} + +method M1() +{ + assert var f := 54; var g := f + 1; g == 55; +} + +method M2() +{ + assert var f := 54; var f := f + 1; f == 55; +} + +function method Fib(n: nat): nat +{ + if n < 2 then n else Fib(n-1) + Fib(n-2) +} + +method M3(a: array) returns (r: int) + requires a != null && forall i :: 0 <= i < a.Length ==> a[i] == 6; + ensures (r + var t := r; t*2) == 3*r; +{ + assert Fib(2) + Fib(4) == Fib(0) + Fib(1) + Fib(2) + Fib(3); + + { + var x,y := Fib(8), Fib(11); + assume x == 21; + assert Fib(7) == 3 ==> Fib(9) == 24; + assume Fib(1000) == 1000; + assume Fib(9) - Fib(8) == 13; + assert Fib(9) <= Fib(10); + assert y == 89; + } + + assert Fib(1000) == 1000; // does it still know this? + + parallel (i | 0 <= i < a.Length) ensures true; { + var j := i+1; + assert j < a.Length ==> a[i] == a[j]; + } +} + +// M4 is pretty much the same as M3, except with things rolled into expressions. +method M4(a: array) returns (r: int) + requires a != null && forall i :: 0 <= i < a.Length ==> a[i] == 6; + ensures (r + var t := r; t*2) == 3*r; +{ + assert Fib(2) + Fib(4) == Fib(0) + Fib(1) + Fib(2) + Fib(3); + assert + var x,y := Fib(8), Fib(11); + assume x == 21; + assert Fib(7) == 3 ==> Fib(9) == 24; + assume Fib(1000) == 1000; + assume Fib(9) - Fib(8) == 13; + assert Fib(9) <= Fib(10); + y == 89; + assert Fib(1000) == 1000; // still known, because the assume was on the path here + assert forall i :: 0 <= i < a.Length ==> var j := i+1; j < a.Length ==> a[i] == a[j]; +} + +var index: int; +method P(a: array) returns (b: bool, ii: int) + requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19; + modifies this, a; + ensures ii == index; + // The following uses a variable with a non-old definition inside an old expression: + ensures 0 <= index < a.Length && old(a[ii]) == 19; + ensures 0 <= index < a.Length && var newIndex := index; old(a[newIndex]) == 19; + // The following places both the variable and the body inside an old: + ensures b ==> old(var oldIndex := index; 0 <= oldIndex < a.Length && a[oldIndex] == 17); + // Here, the definition of the variable is old, and it's used both inside and + // inside an old expression: + ensures var oi := old(index); oi == index ==> a[oi] == 21 && old(a[oi]) == 19; +{ + b := 0 <= index < a.Length && a[index] == 17; + var i, j := 0, -1; + while (i < a.Length) + invariant 0 <= i <= a.Length; + invariant forall k :: 0 <= k < i ==> a[k] == 21; + invariant forall k :: i <= k < a.Length ==> a[k] == old(a[k]); + invariant (0 <= j < i && old(a[j]) == 19) || + (j == -1 && exists k :: i <= k < a.Length && a[k] == 19); + { + if (a[i] == 19) { j := i; } + i, a[i] := i + 1, 21; + } + index := j; + ii := index; +} + +method PMain(a: array) + requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19; + modifies this, a; +{ + var s := a[..]; + var b17, ii := P(a); + assert s == old(a[..]); + assert s[index] == 19; + if (*) { + assert a[index] == 19; // error (a can have changed in P) + } else { + assert b17 ==> 0 <= old(index) < a.Length && old(a[index]) == 17; + assert index == old(index) ==> a[index] == 21 && old(a[index]) == 19; + } +} diff --git a/Test/dafny0/PredExpr.dfy b/Test/dafny0/PredExpr.dfy index 740c2308..96561ebd 100644 --- a/Test/dafny0/PredExpr.dfy +++ b/Test/dafny0/PredExpr.dfy @@ -1,3 +1,16 @@ +function SimpleAssert(n: int): int + ensures n < 100; +{ + assert n == 58; // error: assert violation + n // but postcondition is fine +} + +function SimpleAssume(n: int): int + ensures n < 100; +{ + assume n == 58; n // all is fine +} + function Subonacci(n: nat): nat { if 2 <= n then @@ -18,7 +31,7 @@ function F(n: int): nat function G(n: int, b: bool): nat { if b then - Subonacci(assume 0 <= n; n) + Subonacci(assume 0 <= n; n) + n // the last n is also affected by the assume else Subonacci(n) // error: n may not be a nat } @@ -49,3 +62,18 @@ function method FuncMeth(): int { // PredicateExpr is not included in compilation 15 } + +method M5(a: int, b: int) +{ + var k := if a < 0 then + assume b < 0; 5 + else + 5; + if (*) { + assert a == -7 ==> b < 0; + assert b < 0; // error: this condition does not hold on every path here + } else { + assert assume a == -7; b < 0; // note, this is different than the ==> above + assert b < 0; // this condition does hold on all paths to here + } +} diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 32a60340..18c23e55 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -20,7 +20,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy Refinement.dfy RefinementErrors.dfy LoopModifies.dfy ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy - CallStmtTests.dfy MultiSets.dfy PredExpr.dfy) do ( + CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy) do ( echo. echo -------------------- %%f -------------------- %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f -- cgit v1.2.3