diff options
| -rw-r--r-- | Source/Dafny/Compiler.cs | 11 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 33 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 21 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 93 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 19 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 24 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 102 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 247 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 27 | ||||
| -rw-r--r-- | Test/dafny0/LetExpr.dfy | 109 | ||||
| -rw-r--r-- | Test/dafny0/PredExpr.dfy | 30 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 |
12 files changed, 524 insertions, 194 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index de863e39..d0e0cb0e 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/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<IVariable, Expression>();
+ 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/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 8a9108f0..2eaaca7f 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -716,7 +716,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall> VarDeclStatement<.out Statement/*!*/ s.>
= (. IToken x = null, assignTok = null; bool isGhost = false;
VarDecl/*!*/ d;
- AssignmentRhs r; Expression lhs0;
+ AssignmentRhs r; IdentifierExpr lhs0;
List<VarDecl> lhss = new List<VarDecl>();
List<AssignmentRhs> rhss = new List<AssignmentRhs>();
.)
@@ -727,7 +727,10 @@ VarDeclStatement<.out Statement/*!*/ s.> { ","
LocalIdentTypeOptional<out d, isGhost> (. 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<out r, lhs0> (. rhss.Add(r); .)
{ "," Rhs<out r, lhs0> (. rhss.Add(r); .)
}
@@ -1204,20 +1207,34 @@ EndlessExpression<out Expression e> = (. IToken/*!*/ x;
Expression e0, e1;
e = dummyExpr;
+ BoundVar d;
+ List<BoundVar> letVars; List<Expression> letRHSs;
.)
- ( "if" (. x = t; .)
+ ( "if" (. x = t; .)
Expression<out e>
"then" Expression<out e0>
- "else" Expression<out e1> (. e = new ITEExpr(x, e, e0, e1); .)
+ "else" Expression<out e1> (. e = new ITEExpr(x, e, e0, e1); .)
| MatchExpression<out e>
| QuantifierGuts<out e>
| ComprehensionExpr<out e>
- | "assert" (. x = t; .)
+ | "assert" (. x = t; .)
Expression<out e0> ";"
- Expression<out e1> (. e = new AssertExpr(x, e0, e1); .)
- | "assume" (. x = t; .)
+ Expression<out e1> (. e = new AssertExpr(x, e0, e1); .)
+ | "assume" (. x = t; .)
Expression<out e0> ";"
- Expression<out e1> (. e = new AssumeExpr(x, e0, e1); .)
+ Expression<out e1> (. e = new AssumeExpr(x, e0, e1); .)
+ | "var" (. x = t;
+ letVars = new List<BoundVar>();
+ letRHSs = new List<Expression>(); .)
+ IdentTypeOptional<out d> (. letVars.Add(d); .)
+ { "," IdentTypeOptional<out d> (. letVars.Add(d); .)
+ }
+ ":="
+ Expression<out e> (. letRHSs.Add(e); .)
+ { "," Expression<out e> (. letRHSs.Add(e); .)
+ }
+ ";"
+ Expression<out e> (. e = new LetExpr(x, letVars, letRHSs, e); .)
)
.
MatchExpression<out Expression/*!*/ e>
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index e07c6f1d..8272736c 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2593,6 +2593,27 @@ namespace Microsoft.Dafny { }
}
+ public class LetExpr : Expression
+ {
+ public readonly List<BoundVar> Vars;
+ public readonly List<Expression> RHSs;
+ public readonly Expression Body;
+ public LetExpr(IToken tok, List<BoundVar> vars, List<Expression> rhss, Expression body)
+ : base(tok) {
+ Vars = vars;
+ RHSs = rhss;
+ Body = body;
+ }
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ foreach (var rhs in RHSs) {
+ yield return rhs;
+ }
+ yield return Body;
+ }
+ }
+ }
+
/// <summary>
/// A ComprehensionExpr has the form:
/// BINDER x Attributes | Range(x) :: Term(x)
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 0dc30e8a..583fcc61 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/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<ModuleDecl/*! if (errDist >= 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<ModuleDecl/*! la = t;
}
}
-
+
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
-
+
bool StartOf (int s) {
return set[s, la.kind];
}
-
+
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
@@ -182,7 +182,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -1100,7 +1100,7 @@ List<Expression/*!*/>/*!*/ 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<VarDecl> lhss = new List<VarDecl>();
List<AssignmentRhs> rhss = new List<AssignmentRhs>();
@@ -1119,7 +1119,10 @@ List<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ decreases) { IToken/*!*/ x;
Expression e0, e1;
e = dummyExpr;
+ BoundVar d;
+ List<BoundVar> letVars; List<Expression> letRHSs;
switch (la.kind) {
case 55: {
@@ -1888,6 +1893,31 @@ List<Expression/*!*/>/*!*/ decreases) { e = new AssumeExpr(x, e0, e1);
break;
}
+ case 18: {
+ Get();
+ x = t;
+ letVars = new List<BoundVar>();
+ letRHSs = new List<Expression>();
+ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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<Expression/*!*/>/*!*/ 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/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 10099bf4..5b9ba1d6 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/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/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index b6bc4059..81216f32 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/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/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 634abf45..1ab06974 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/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<string>() != 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<string>() != 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<Token>() != null);
@@ -791,7 +787,7 @@ public class Scanner { }
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 028891b5..f3373736 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/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) {
+ /// <summary>
+ /// 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.
+ /// </summary>
+ 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<ExpressionTranslator>() != 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<ExpressionTranslator>() != 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<ExpressionTranslator>() != 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<Bpl.IdentifierExpr>().Type != null);
+ public Bpl.IdentifierExpr ModuleContextHeight() {
+ Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);
return new Bpl.IdentifierExpr(Token.NoToken, "$ModuleContextHeight", Bpl.Type.Int);
}
- public Bpl.IdentifierExpr FunctionContextHeight()
- {
- Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);
+ public Bpl.IdentifierExpr FunctionContextHeight() {
+ Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);
return new Bpl.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Bpl.Type.Int);
}
- public Bpl.IdentifierExpr InMethodContext()
- {
- Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);
+ public Bpl.IdentifierExpr InMethodContext() {
+ Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().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<IVariable, Expression>();
+ 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);
+ }
+
+
/// <summary>
/// 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<Bpl.Expr>() != 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<Bpl.Expr>() != 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<SplitExprInfo>();
- 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<SplitExprInfo>();
+ 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<SplitExprInfo>();
+ 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<IVariable, Expression/*!*/>/*!*/ substMap) {
+ public static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {
Contract.Requires(expr != null);
Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(Contract.Result<Expression>() != 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<Expression>();
+ 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<int>) 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<int>) 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<int>) 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<int>)
+ 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
|