diff options
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 37 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 64 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 87 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 290 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 41 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 54 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 102 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 364 |
8 files changed, 700 insertions, 339 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 800585bd..6dabace1 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -716,7 +716,20 @@ namespace Microsoft.Dafny { Indent(indent); wr.WriteLine("else");
TrStmt(s.Els, indent);
}
-
+
+ } else if (stmt is AlternativeStmt) {
+ var s = (AlternativeStmt)stmt;
+ Indent(indent);
+ foreach (var alternative in s.Alternatives) {
+ wr.Write("if (");
+ TrExpr(alternative.Guard);
+ wr.WriteLine(") {");
+ TrStmtList(alternative.Body, indent);
+ Indent(indent);
+ wr.Write("} else ");
+ }
+ wr.WriteLine("{ /*unreachable alternative*/ }");
+
} else if (stmt is WhileStmt) {
WhileStmt s = (WhileStmt)stmt;
if (s.Guard == null) {
@@ -730,6 +743,26 @@ namespace Microsoft.Dafny { TrStmt(s.Body, indent);
}
+ } else if (stmt is AlternativeLoopStmt) {
+ var s = (AlternativeLoopStmt)stmt;
+ if (s.Alternatives.Count != 0) {
+ Indent(indent);
+ wr.WriteLine("while (true) {");
+ int ind = indent + IndentAmount;
+ Indent(ind);
+ foreach (var alternative in s.Alternatives) {
+ wr.Write("if (");
+ TrExpr(alternative.Guard);
+ wr.WriteLine(") {");
+ TrStmtList(alternative.Body, ind);
+ Indent(ind);
+ wr.Write("} else ");
+ }
+ wr.WriteLine("{ break; }");
+ Indent(indent);
+ wr.WriteLine("}");
+ }
+
} else if (stmt is ForeachStmt) {
ForeachStmt s = (ForeachStmt)stmt;
// List<Pair<TType,RhsType>> pendingUpdates = new List<Pair<TType,RhsType>>();
@@ -1127,7 +1160,7 @@ namespace Microsoft.Dafny { } else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
Contract.Assert(dtv.Ctor != null); // since dtv has been successfully resolved
- wr.Write("new {0}(new {0}", dtv.DatatypeName, DtCtorName(dtv.Ctor));
+ wr.Write("new {0}(new {1}", dtv.DatatypeName, DtCtorName(dtv.Ctor));
if (dtv.InferredTypeArgs.Count != 0) {
wr.Write("<{0}>", TypeNames(dtv.InferredTypeArgs));
}
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index f2a0a762..388ae8cd 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -881,29 +881,72 @@ IfStmt<out Statement/*!*/ ifStmt> Statement/*!*/ s;
Statement els = null;
IToken bodyStart, bodyEnd;
+ List<GuardedAlternative> alternatives;
+ ifStmt = dummyStmt; // to please the compiler
.)
"if" (. x = t; .)
- Guard<out guard>
- BlockStmt<out thn, out bodyStart, out bodyEnd>
- [ "else"
- ( IfStmt<out s> (. els = s; .)
- | BlockStmt<out s, out bodyStart, out bodyEnd> (. els = s; .)
- )
- ]
- (. ifStmt = new IfStmt(x, guard, thn, els); .)
+ (
+ Guard<out guard>
+ BlockStmt<out thn, out bodyStart, out bodyEnd>
+ [ "else"
+ ( IfStmt<out s> (. els = s; .)
+ | BlockStmt<out s, out bodyStart, out bodyEnd> (. els = s; .)
+ )
+ ]
+ (. ifStmt = new IfStmt(x, guard, thn, els); .)
+ |
+ AlternativeBlock<out alternatives>
+ (. ifStmt = new AlternativeStmt(x, alternatives); .)
+ )
+ .
+
+AlternativeBlock<.out List<GuardedAlternative> alternatives.>
+= (. alternatives = new List<GuardedAlternative>();
+ IToken x;
+ Expression e;
+ List<Statement> body;
+ .)
+ "{"
+ { "case" (. x = t; .)
+ Expression<out e>
+ "=>"
+ (. body = new List<Statement>(); .)
+ (. parseVarScope.PushMarker(); .)
+ { Stmt<body> }
+ (. parseVarScope.PopMarker(); .)
+ (. alternatives.Add(new GuardedAlternative(x, e, body)); .)
+ }
+ "}"
.
WhileStmt<out Statement/*!*/ stmt>
= (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
Expression guard;
- bool isFree; Expression/*!*/ e;
List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
List<Expression/*!*/> decreases = new List<Expression/*!*/>();
Statement/*!*/ body;
IToken bodyStart, bodyEnd;
+ List<GuardedAlternative> alternatives;
+ stmt = dummyStmt; // to please the compiler
.)
"while" (. x = t; .)
- Guard<out guard> (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
+ (
+ Guard<out guard> (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
+ LoopSpec<out invariants, out decreases>
+ BlockStmt<out body, out bodyStart, out bodyEnd>
+ (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .)
+ |
+ LoopSpec<out invariants, out decreases>
+ AlternativeBlock<out alternatives>
+ (. stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives); .)
+ )
+ .
+
+LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases.>
+= (. bool isFree; Expression/*!*/ e;
+ invariants = new List<MaybeFreeExpression/*!*/>();
+ decreases = new List<Expression/*!*/>();
+ .)
{ (. isFree = false; .)
[ "free" (. isFree = true; .)
]
@@ -916,7 +959,6 @@ WhileStmt<out Statement/*!*/ stmt> }
";"
}
- BlockStmt<out body, out bodyStart, out bodyEnd> (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .)
.
Guard<out Expression e> /* null represents demonic-choice */
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 04d92539..f0a58293 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1557,8 +1557,6 @@ namespace Microsoft.Dafny { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Thn != null);
-
-
Contract.Invariant(Els == null || Els is BlockStmt || Els is IfStmt);
}
public IfStmt(IToken tok, Expression guard, Statement thn, Statement els)
@@ -1574,36 +1572,103 @@ namespace Microsoft.Dafny { }
}
- public class WhileStmt : Statement {
+ public class GuardedAlternative
+ {
+ public readonly IToken Tok;
public readonly Expression Guard;
+ public readonly List<Statement> Body;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Tok != null);
+ Contract.Invariant(Guard != null);
+ Contract.Invariant(Body != null);
+ }
+ public GuardedAlternative(IToken tok, Expression guard, List<Statement> body)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(guard != null);
+ Contract.Requires(body != null);
+ this.Tok = tok;
+ this.Guard = guard;
+ this.Body = body;
+ }
+ }
+
+ public class AlternativeStmt : Statement
+ {
+ public readonly List<GuardedAlternative> Alternatives;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Alternatives != null);
+ }
+ public AlternativeStmt(IToken tok, List<GuardedAlternative> alternatives)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(alternatives != null);
+ this.Alternatives = alternatives;
+ }
+ }
+
+ public abstract class LoopStmt : Statement
+ {
public readonly List<MaybeFreeExpression/*!*/>/*!*/ Invariants;
public readonly List<Expression/*!*/>/*!*/ Decreases;
- public readonly Statement/*!*/ Body;
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Body != null);
Contract.Invariant(cce.NonNullElements(Invariants));
Contract.Invariant(cce.NonNullElements(Decreases));
}
+ public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases)
+ : base(tok)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(cce.NonNullElements(invariants));
+ Contract.Requires(cce.NonNullElements(decreases));
+ this.Invariants = invariants;
+ this.Decreases = decreases;
+ }
+ }
+
+ public class WhileStmt : LoopStmt
+ {
+ public readonly Expression Guard;
+ public readonly Statement/*!*/ Body;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Body != null);
+ }
public WhileStmt(IToken tok, Expression guard,
List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases,
Statement/*!*/ body)
- : base(tok) {
+ : base(tok, invariants, decreases) {
Contract.Requires(tok != null);
Contract.Requires(body != null);
- Contract.Requires(cce.NonNullElements(invariants));
- Contract.Requires(cce.NonNullElements(decreases));
this.Guard = guard;
- this.Invariants = invariants;
- this.Decreases = decreases;
this.Body = body;
+ }
+ }
+ public class AlternativeLoopStmt : LoopStmt
+ {
+ public readonly List<GuardedAlternative> Alternatives;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Alternatives != null);
+ }
+ public AlternativeLoopStmt(IToken tok,
+ List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases,
+ List<GuardedAlternative> alternatives)
+ : base(tok, invariants, decreases) {
+ Contract.Requires(tok != null);
+ Contract.Requires(alternatives != null);
+ this.Alternatives = alternatives;
}
}
- public class ForeachStmt : Statement {
+ public class ForeachStmt : Statement
+ {
public readonly BoundVar/*!*/ BoundVar;
public readonly Expression/*!*/ Collection;
public readonly Expression/*!*/ Range;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index e707d859..aa02c796 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -25,7 +25,7 @@ public class Parser { const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -161,10 +161,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);
}
@@ -177,15 +177,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 {
@@ -209,7 +209,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -1267,62 +1267,54 @@ List<Expression/*!*/>/*!*/ decreases) { Statement/*!*/ s;
Statement els = null;
IToken bodyStart, bodyEnd;
+ List<GuardedAlternative> alternatives;
+ ifStmt = dummyStmt; // to please the compiler
Expect(57);
x = t;
- Guard(out guard);
- BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 58) {
- Get();
- if (la.kind == 57) {
- IfStmt(out s);
- els = s;
- } else if (la.kind == 7) {
- BlockStmt(out s, out bodyStart, out bodyEnd);
- els = s;
- } else SynErr(124);
- }
- ifStmt = new IfStmt(x, guard, thn, els);
+ if (la.kind == 32) {
+ Guard(out guard);
+ BlockStmt(out thn, out bodyStart, out bodyEnd);
+ if (la.kind == 58) {
+ Get();
+ if (la.kind == 57) {
+ IfStmt(out s);
+ els = s;
+ } else if (la.kind == 7) {
+ BlockStmt(out s, out bodyStart, out bodyEnd);
+ els = s;
+ } else SynErr(124);
+ }
+ ifStmt = new IfStmt(x, guard, thn, els);
+ } else if (la.kind == 7) {
+ AlternativeBlock(out alternatives);
+ ifStmt = new AlternativeStmt(x, alternatives);
+ } else SynErr(125);
}
void WhileStmt(out Statement/*!*/ stmt) {
Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
Expression guard;
- bool isFree; Expression/*!*/ e;
List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
List<Expression/*!*/> decreases = new List<Expression/*!*/>();
Statement/*!*/ body;
IToken bodyStart, bodyEnd;
+ List<GuardedAlternative> alternatives;
+ stmt = dummyStmt; // to please the compiler
Expect(59);
x = t;
- Guard(out guard);
- Contract.Assume(guard == null || cce.Owner.None(guard));
- while (la.kind == 28 || la.kind == 31 || la.kind == 60) {
- if (la.kind == 28 || la.kind == 60) {
- isFree = false;
- if (la.kind == 28) {
- Get();
- isFree = true;
- }
- Expect(60);
- Expression(out e);
- invariants.Add(new MaybeFreeExpression(e, isFree));
- Expect(15);
- } else {
- Get();
- PossiblyWildExpression(out e);
- decreases.Add(e);
- while (la.kind == 19) {
- Get();
- PossiblyWildExpression(out e);
- decreases.Add(e);
- }
- Expect(15);
- }
- }
- BlockStmt(out body, out bodyStart, out bodyEnd);
- stmt = new WhileStmt(x, guard, invariants, decreases, body);
+ if (la.kind == 32) {
+ Guard(out guard);
+ Contract.Assume(guard == null || cce.Owner.None(guard));
+ LoopSpec(out invariants, out decreases);
+ BlockStmt(out body, out bodyStart, out bodyEnd);
+ stmt = new WhileStmt(x, guard, invariants, decreases, body);
+ } else if (StartOf(12)) {
+ LoopSpec(out invariants, out decreases);
+ AlternativeBlock(out alternatives);
+ stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives);
+ } else SynErr(126);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -1382,13 +1374,13 @@ List<Expression/*!*/>/*!*/ decreases) { if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
}
}
- if (StartOf(12)) {
+ if (StartOf(13)) {
AssignStmt(out s, false);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
} else if (la.kind == 56) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else SynErr(125);
+ } else SynErr(127);
Expect(8);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1444,7 +1436,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out e);
ee = new List<Expression>() { e };
- } else SynErr(126);
+ } else SynErr(128);
if (ee == null && ty == null) { ee = new List<Expression>() { dummyExpr}; }
}
@@ -1454,7 +1446,7 @@ List<Expression/*!*/>/*!*/ decreases) { IdentOrFuncExpression(out e);
} else if (la.kind == 32 || la.kind == 99 || la.kind == 100) {
ObjectExpression(out e);
- } else SynErr(127);
+ } else SynErr(129);
while (la.kind == 52 || la.kind == 54) {
SelectOrCallSuffix(ref e);
}
@@ -1501,10 +1493,63 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(128);
+ } else SynErr(130);
Expect(33);
}
+ void AlternativeBlock(out List<GuardedAlternative> alternatives) {
+ alternatives = new List<GuardedAlternative>();
+ IToken x;
+ Expression e;
+ List<Statement> body;
+
+ Expect(7);
+ while (la.kind == 45) {
+ Get();
+ x = t;
+ Expression(out e);
+ Expect(46);
+ body = new List<Statement>();
+ parseVarScope.PushMarker();
+ while (StartOf(9)) {
+ Stmt(body);
+ }
+ parseVarScope.PopMarker();
+ alternatives.Add(new GuardedAlternative(x, e, body));
+ }
+ Expect(8);
+ }
+
+ void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases) {
+ bool isFree; Expression/*!*/ e;
+ invariants = new List<MaybeFreeExpression/*!*/>();
+ decreases = new List<Expression/*!*/>();
+
+ while (la.kind == 28 || la.kind == 31 || la.kind == 60) {
+ if (la.kind == 28 || la.kind == 60) {
+ isFree = false;
+ if (la.kind == 28) {
+ Get();
+ isFree = true;
+ }
+ Expect(60);
+ Expression(out e);
+ invariants.Add(new MaybeFreeExpression(e, isFree));
+ Expect(15);
+ } else {
+ Get();
+ PossiblyWildExpression(out e);
+ decreases.Add(e);
+ while (la.kind == 19) {
+ Get();
+ PossiblyWildExpression(out e);
+ decreases.Add(e);
+ }
+ Expect(15);
+ }
+ }
+ }
+
void CaseStatement(out MatchCaseStmt/*!*/ c) {
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ x, id, arg;
@@ -1544,7 +1589,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 32 || la.kind == 99 || la.kind == 100) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else SynErr(129);
+ } else SynErr(131);
while (la.kind == 52 || la.kind == 54) {
SelectOrCallSuffix(ref e);
}
@@ -1558,7 +1603,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(130);
+ } else SynErr(132);
}
void EquivExpression(out Expression/*!*/ e0) {
@@ -1588,13 +1633,13 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 69) {
Get();
- } else SynErr(131);
+ } else SynErr(133);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
- if (StartOf(13)) {
+ if (StartOf(14)) {
if (la.kind == 72 || la.kind == 73) {
AndOp();
x = t;
@@ -1626,13 +1671,13 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 71) {
Get();
- } else SynErr(132);
+ } else SynErr(134);
}
void RelationalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Term(out e0);
- if (StartOf(14)) {
+ if (StartOf(15)) {
RelOp(out x, out op);
Term(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1644,7 +1689,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 73) {
Get();
- } else SynErr(133);
+ } else SynErr(135);
}
void OrOp() {
@@ -1652,7 +1697,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 75) {
Get();
- } else SynErr(134);
+ } else SynErr(136);
}
void Term(out Expression/*!*/ e0) {
@@ -1728,7 +1773,7 @@ List<Expression/*!*/>/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(135); break;
+ default: SynErr(137); break;
}
}
@@ -1750,7 +1795,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 86) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(136);
+ } else SynErr(138);
}
void UnaryExpression(out Expression/*!*/ e) {
@@ -1765,11 +1810,11 @@ List<Expression/*!*/>/*!*/ decreases) { x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
- } else if (StartOf(12)) {
+ } else if (StartOf(13)) {
SelectExpression(out e);
- } else if (StartOf(15)) {
+ } else if (StartOf(16)) {
ConstAtomExpression(out e);
- } else SynErr(137);
+ } else SynErr(139);
}
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
@@ -1783,7 +1828,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 88) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(138);
+ } else SynErr(140);
}
void NegOp() {
@@ -1791,7 +1836,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 90) {
Get();
- } else SynErr(139);
+ } else SynErr(141);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -1902,7 +1947,7 @@ List<Expression/*!*/>/*!*/ decreases) { ComprehensionExpr(out e);
break;
}
- default: SynErr(140); break;
+ default: SynErr(142); break;
}
}
@@ -1933,7 +1978,7 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 103 || la.kind == 104) {
Exists();
x = t;
- } else SynErr(141);
+ } else SynErr(143);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -1984,6 +2029,7 @@ List<Expression/*!*/>/*!*/ decreases) { QSep();
Expression(out body);
}
+ if (body == null && bvars.Count != 1) { SemErr(t, "a set comprehension with more than one bound variable must have a term expression"); }
q = new SetComprehension(x, bvars, range, body);
parseVarScope.PopMarker();
@@ -2027,7 +2073,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
Expression(out e);
Expect(33);
- } else SynErr(142);
+ } else SynErr(144);
}
void SelectOrCallSuffix(ref Expression/*!*/ e) {
@@ -2077,12 +2123,12 @@ List<Expression/*!*/>/*!*/ decreases) { multipleIndices.Add(ee);
}
- } else SynErr(143);
+ } else SynErr(145);
} else if (la.kind == 98) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(144);
+ } else SynErr(146);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -2106,7 +2152,7 @@ List<Expression/*!*/>/*!*/ decreases) { }
Expect(53);
- } else SynErr(145);
+ } else SynErr(147);
}
void Forall() {
@@ -2114,7 +2160,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 102) {
Get();
- } else SynErr(146);
+ } else SynErr(148);
}
void Exists() {
@@ -2122,7 +2168,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 104) {
Get();
- } else SynErr(147);
+ } else SynErr(149);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -2135,7 +2181,7 @@ List<Expression/*!*/>/*!*/ decreases) { es = new List<Expression/*!*/>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(148);
+ } else SynErr(150);
Expect(8);
}
@@ -2144,7 +2190,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 106) {
Get();
- } else SynErr(149);
+ } else SynErr(151);
}
void AttributeBody(ref Attributes attrs) {
@@ -2155,7 +2201,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(22);
Expect(1);
aName = t.val;
- if (StartOf(16)) {
+ if (StartOf(17)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 19) {
@@ -2171,13 +2217,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,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
@@ -2191,6 +2237,7 @@ List<Expression/*!*/>/*!*/ decreases) { {x,T,x,x, x,x,x,T, x,x,x,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, T,x,x,T, T,T,x,x, x,x,x,x, T,T,x,T, x,T,T,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,T, T,x,x,x, x,x,x,x, x},
{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,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,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,T, T,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, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,x,x, x,x,x,x, T,T,x,T, x,T,T,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,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, 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,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,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, 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,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,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,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,T, x,x,x,x, x,x,x,x, x,x,x,x, 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},
@@ -2204,18 +2251,20 @@ 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;
@@ -2343,35 +2392,37 @@ public class Errors { case 122: s = "invalid Stmt"; break;
case 123: s = "invalid OneStmt"; break;
case 124: s = "invalid IfStmt"; break;
- case 125: s = "invalid ForeachStmt"; break;
- case 126: s = "invalid AssignRhs"; break;
- case 127: s = "invalid SelectExpression"; break;
- case 128: s = "invalid Guard"; break;
- case 129: s = "invalid CallStmtSubExpr"; break;
- case 130: s = "invalid AttributeArg"; break;
- case 131: s = "invalid EquivOp"; break;
- case 132: s = "invalid ImpliesOp"; break;
- case 133: s = "invalid AndOp"; break;
- case 134: s = "invalid OrOp"; break;
- case 135: s = "invalid RelOp"; break;
- case 136: s = "invalid AddOp"; break;
- case 137: s = "invalid UnaryExpression"; break;
- case 138: s = "invalid MulOp"; break;
- case 139: s = "invalid NegOp"; break;
- case 140: s = "invalid ConstAtomExpression"; break;
- case 141: s = "invalid QuantifierGuts"; break;
- case 142: s = "invalid ObjectExpression"; break;
- case 143: s = "invalid SelectOrCallSuffix"; break;
- case 144: s = "invalid SelectOrCallSuffix"; break;
+ case 125: s = "invalid IfStmt"; break;
+ case 126: s = "invalid WhileStmt"; break;
+ case 127: s = "invalid ForeachStmt"; break;
+ case 128: s = "invalid AssignRhs"; break;
+ case 129: s = "invalid SelectExpression"; break;
+ case 130: s = "invalid Guard"; break;
+ case 131: s = "invalid CallStmtSubExpr"; break;
+ case 132: s = "invalid AttributeArg"; break;
+ case 133: s = "invalid EquivOp"; break;
+ case 134: s = "invalid ImpliesOp"; break;
+ case 135: s = "invalid AndOp"; break;
+ case 136: s = "invalid OrOp"; break;
+ case 137: s = "invalid RelOp"; break;
+ case 138: s = "invalid AddOp"; break;
+ case 139: s = "invalid UnaryExpression"; break;
+ case 140: s = "invalid MulOp"; break;
+ case 141: s = "invalid NegOp"; break;
+ case 142: s = "invalid ConstAtomExpression"; break;
+ case 143: s = "invalid QuantifierGuts"; break;
+ case 144: s = "invalid ObjectExpression"; break;
case 145: s = "invalid SelectOrCallSuffix"; break;
- case 146: s = "invalid Forall"; break;
- case 147: s = "invalid Exists"; break;
- case 148: s = "invalid AttributeOrTrigger"; break;
- case 149: s = "invalid QSep"; break;
+ case 146: s = "invalid SelectOrCallSuffix"; break;
+ case 147: s = "invalid SelectOrCallSuffix"; break;
+ case 148: s = "invalid Forall"; break;
+ case 149: s = "invalid Exists"; break;
+ case 150: s = "invalid AttributeOrTrigger"; break;
+ case 151: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2379,8 +2430,9 @@ 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 d3c7ecea..2dd2724f 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -507,6 +507,13 @@ namespace Microsoft.Dafny { break;
}
}
+
+ } else if (stmt is AlternativeStmt) {
+ var s = (AlternativeStmt)stmt;
+ wr.WriteLine("if {");
+ PrintAlternatives(indent, s.Alternatives);
+ Indent(indent);
+ wr.Write("}");
} else if (stmt is WhileStmt) {
WhileStmt s = (WhileStmt)stmt;
@@ -514,12 +521,23 @@ namespace Microsoft.Dafny { PrintGuard(s.Guard);
wr.WriteLine(")");
- int ind = indent + IndentAmount;
- PrintSpec("invariant", s.Invariants, ind);
- PrintSpecLine("decreases", s.Decreases, indent);
+ PrintSpec("invariant", s.Invariants, indent + IndentAmount);
+ PrintSpecLine("decreases", s.Decreases, indent + IndentAmount);
Indent(indent);
PrintStatement(s.Body, indent);
-
+
+ } else if (stmt is AlternativeLoopStmt) {
+ var s = (AlternativeLoopStmt)stmt;
+ wr.WriteLine("while");
+ PrintSpec("invariant", s.Invariants, indent + IndentAmount);
+ PrintSpecLine("decreases", s.Decreases, indent + IndentAmount);
+
+ Indent(indent);
+ wr.WriteLine("{");
+ PrintAlternatives(indent, s.Alternatives);
+ Indent(indent);
+ wr.Write("}");
+
} else if (stmt is ForeachStmt) {
ForeachStmt s = (ForeachStmt)stmt;
wr.Write("foreach ({0} in ", s.BoundVar.Name);
@@ -572,6 +590,21 @@ namespace Microsoft.Dafny { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
}
+
+ void PrintAlternatives(int indent, List<GuardedAlternative> alternatives) {
+ int caseInd = indent + IndentAmount;
+ foreach (var alternative in alternatives) {
+ Indent(caseInd);
+ wr.Write("case ");
+ PrintExpression(alternative.Guard);
+ wr.WriteLine(" =>");
+ foreach (Statement s in alternative.Body) {
+ Indent(caseInd + IndentAmount);
+ PrintStatement(s, caseInd + IndentAmount);
+ wr.WriteLine();
+ }
+ }
+ }
void PrintDeterminedRhs(DeterminedAssignmentRhs rhs) {
Contract.Requires(rhs != null);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index eb40ac82..3549d0db 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1317,7 +1317,11 @@ namespace Microsoft.Dafny { if (s.Els != null) {
ResolveStatement(s.Els, branchesAreSpecOnly, method);
}
-
+
+ } else if (stmt is AlternativeStmt) {
+ var s = (AlternativeStmt)stmt;
+ s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, method);
+
} else if (stmt is WhileStmt) {
WhileStmt s = (WhileStmt)stmt;
bool bodyMustBeSpecOnly = specContextOnly;
@@ -1349,7 +1353,25 @@ namespace Microsoft.Dafny { }
s.IsGhost = bodyMustBeSpecOnly;
ResolveStatement(s.Body, bodyMustBeSpecOnly, method);
-
+
+ } else if (stmt is AlternativeLoopStmt) {
+ var s = (AlternativeLoopStmt)stmt;
+ s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, method);
+ foreach (MaybeFreeExpression inv in s.Invariants) {
+ ResolveExpression(inv.E, true, true);
+ Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(inv.E.Type, Type.Bool)) {
+ Error(inv.E, "invariant is expected to be of type {0}, but is {1}", Type.Bool, inv.E.Type);
+ }
+ }
+ foreach (Expression e in s.Decreases) {
+ ResolveExpression(e, true, true);
+ if (s.IsGhost && e is WildcardExpr) {
+ Error(e, "'decreases *' is not allowed on ghost loops");
+ }
+ // any type is fine
+ }
+
} else if (stmt is ForeachStmt) {
ForeachStmt s = (ForeachStmt)stmt;
@@ -1491,6 +1513,34 @@ namespace Microsoft.Dafny { }
}
+ bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, Method method) {
+ Contract.Requires(alternatives != null);
+ Contract.Requires(method != null);
+
+ bool isGhost = specContextOnly;
+ // first, resolve the guards, which tells us whether or not the entire statement is a ghost statement
+ foreach (var alternative in alternatives) {
+ int prevErrorCount = ErrorCount;
+ ResolveExpression(alternative.Guard, true, true);
+ Contract.Assert(alternative.Guard.Type != null); // follows from postcondition of ResolveExpression
+ bool successfullyResolved = ErrorCount == prevErrorCount;
+ if (!UnifyTypes(alternative.Guard.Type, Type.Bool)) {
+ Error(alternative.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, alternative.Guard.Type);
+ }
+ if (!specContextOnly && successfullyResolved) {
+ isGhost = isGhost || UsesSpecFeatures(alternative.Guard);
+ }
+ }
+ foreach (var alternative in alternatives) {
+ scope.PushMarker();
+ foreach (Statement ss in alternative.Body) {
+ ResolveStatement(ss, isGhost, method);
+ }
+ scope.PopMarker();
+ }
+ return isGhost;
+ }
+
void ResolveCallStmt(CallStmt s, bool specContextOnly, Method method, Type receiverType) {
Contract.Requires(s != null);
Contract.Requires(method != null);
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 0af254f3..817df6cd 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,15 +31,17 @@ 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;
@@ -51,12 +53,12 @@ void ObjectInvariant(){ 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;
@@ -73,14 +75,14 @@ void ObjectInvariant(){ }
~Buffer() { Close(); }
-
+
protected void Close() {
if (!isUserStream && stream != null) {
stream.Close();
//stream = null;
}
}
-
+
public virtual int Read () {
if (bufPos < bufLen) {
return buf[bufPos++];
@@ -100,7 +102,7 @@ void ObjectInvariant(){ Pos = curPos;
return ch;
}
-
+
public string/*!*/ GetString (int beg, int end) {
Contract.Ensures(Contract.Result<string>() != null);
int len = 0;
@@ -139,7 +141,7 @@ void ObjectInvariant(){ }
}
}
-
+
// 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.
@@ -213,19 +215,20 @@ public class Scanner { const int noSym = 107;
-[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
@@ -236,13 +239,13 @@ void objectInvariant(){ 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;
@@ -291,9 +294,9 @@ void objectInvariant(){ 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;
@@ -303,15 +306,14 @@ void objectInvariant(){ 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);
@@ -320,10 +322,9 @@ void objectInvariant(){ buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
this.Filename = fileName;
-
Init();
}
-
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
@@ -344,11 +345,11 @@ void objectInvariant(){ 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 +360,7 @@ void objectInvariant(){ }
void NextCh() {
- if (oldEols > 0) { ch = EOL; oldEols--; }
+ if (oldEols > 0) { ch = EOL; oldEols--; }
else {
// pos = buffer.Pos;
// ch = buffer.Read(); col++;
@@ -367,9 +368,9 @@ void objectInvariant(){ // // 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 +420,7 @@ void objectInvariant(){ return;
}
-
+
}
}
@@ -558,10 +559,13 @@ void objectInvariant(){ t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
- if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
+ if (start.ContainsKey(ch)) {
+ Contract.Assert(start[ch] != null);
+ state = (int) start[ch];
+ }
else { state = 0; }
tlen = 0; AddCh();
-
+
switch (state) {
case -1: { t.kind = eofSym; break; } // NextCh already done
case 0: {
@@ -769,14 +773,14 @@ void objectInvariant(){ 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);
@@ -797,7 +801,7 @@ void objectInvariant(){ }
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index b529b984..e338c0ca 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2139,15 +2139,16 @@ namespace Microsoft.Dafny { return decr;
}
- List<Expression> LoopDecreasesWithDefault(WhileStmt s, out bool inferredDecreases) {
- Contract.Requires(s != null);
+ List<Expression> LoopDecreasesWithDefault(IToken tok, Expression Guard, List<Expression> Decreases, out bool inferredDecreases) {
+ Contract.Requires(tok != null);
+ Contract.Requires(Decreases != null);
- List<Expression> theDecreases = s.Decreases;
+ List<Expression> theDecreases = Decreases;
inferredDecreases = false;
- if (theDecreases.Count == 0 && s.Guard != null) {
+ if (theDecreases.Count == 0 && Guard != null) {
theDecreases = new List<Expression>();
Expression prefix = null;
- foreach (Expression guardConjunct in Conjuncts(s.Guard)) {
+ foreach (Expression guardConjunct in Conjuncts(Guard)) {
Expression guess = null;
BinaryExpr bin = guardConjunct as BinaryExpr;
if (bin != null) {
@@ -2155,23 +2156,23 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.Lt:
case BinaryExpr.ResolvedOpcode.Le:
// for A < B and A <= B, use the decreases B - A
- guess = CreateIntSub(s.Tok, bin.E1, bin.E0);
+ guess = CreateIntSub(tok, bin.E1, bin.E0);
break;
case BinaryExpr.ResolvedOpcode.Ge:
case BinaryExpr.ResolvedOpcode.Gt:
// for A >= B and A > B, use the decreases A - B
- guess = CreateIntSub(s.Tok, bin.E0, bin.E1);
+ guess = CreateIntSub(tok, bin.E0, bin.E1);
break;
case BinaryExpr.ResolvedOpcode.NeqCommon:
if (bin.E0.Type is IntType) {
// for A != B where A and B are integers, use the absolute difference between A and B (that is: if 0 <= A-B then A-B else B-A)
- Expression AminusB = CreateIntSub(s.Tok, bin.E0, bin.E1);
- Expression BminusA = CreateIntSub(s.Tok, bin.E1, bin.E0);
- Expression zero = CreateIntLiteral(s.Tok, 0);
- BinaryExpr test = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Le, zero, AminusB);
+ Expression AminusB = CreateIntSub(tok, bin.E0, bin.E1);
+ Expression BminusA = CreateIntSub(tok, bin.E1, bin.E0);
+ Expression zero = CreateIntLiteral(tok, 0);
+ BinaryExpr test = new BinaryExpr(tok, BinaryExpr.Opcode.Le, zero, AminusB);
test.ResolvedOp = BinaryExpr.ResolvedOpcode.Le; // resolve here
test.Type = Type.Bool; // resolve here
- guess = CreateIntITE(s.Tok, test, AminusB, BminusA);
+ guess = CreateIntITE(tok, test, AminusB, BminusA);
}
break;
default:
@@ -2181,8 +2182,8 @@ namespace Microsoft.Dafny { if (guess != null) {
if (prefix != null) {
// Make the following guess: if prefix then guess else -1
- Expression negativeOne = CreateIntLiteral(s.Tok, -1);
- guess = CreateIntITE(s.Tok, prefix, guess, negativeOne);
+ Expression negativeOne = CreateIntLiteral(tok, -1);
+ guess = CreateIntITE(tok, prefix, guess, negativeOne);
}
theDecreases.Add(guess);
inferredDecreases = true;
@@ -2191,7 +2192,7 @@ namespace Microsoft.Dafny { if (prefix == null) {
prefix = guardConjunct;
} else {
- BinaryExpr and = new BinaryExpr(s.Tok, BinaryExpr.Opcode.And, prefix, guardConjunct);
+ BinaryExpr and = new BinaryExpr(tok, BinaryExpr.Opcode.And, prefix, guardConjunct);
and.ResolvedOp = BinaryExpr.ResolvedOpcode.And; // resolve here
and.Type = Type.Bool; // resolve here
prefix = and;
@@ -3013,134 +3014,28 @@ namespace Microsoft.Dafny { }
}
builder.Add(new Bpl.IfCmd(stmt.Tok, guard, thn, elsIf, els));
-
+
+ } else if (stmt is AlternativeStmt) {
+ AddComment(builder, stmt, "alternative statement");
+ var s = (AlternativeStmt)stmt;
+ var elseCase = Assert(s.Tok, Bpl.Expr.False, "alternative cases fail to cover all possibilties");
+ TrAlternatives(s.Alternatives, elseCase, null, builder, locals, etran);
+
} else if (stmt is WhileStmt) {
AddComment(builder, stmt, "while statement");
- WhileStmt s = (WhileStmt)stmt;
- int loopId = loopHeapVarCount;
- loopHeapVarCount++;
-
- // use simple heuristics to create a default decreases clause, if none is given
- bool inferredDecreases;
- List<Expression> theDecreases = LoopDecreasesWithDefault(s, out inferredDecreases);
-
- Bpl.LocalVariable preLoopHeapVar = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$PreLoopHeap" + loopId, predef.HeapType));
- locals.Add(preLoopHeapVar);
- Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(stmt.Tok, preLoopHeapVar);
- ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap);
- builder.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, preLoopHeap, etran.HeapExpr)); // TODO: does this screw up labeled breaks for this loop?
-
- List<Bpl.Expr> initDecr = null;
- if (!Contract.Exists(theDecreases, e => e is WildcardExpr)) {
- initDecr = RecordDecreasesValue(theDecreases, builder, locals, etran, "$decr" + loopId + "$init$");
- }
-
- // the variable w is used to coordinate the definedness checking of the loop invariant
- Bpl.LocalVariable wVar = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$w" + loopId, Bpl.Type.Bool));
- Bpl.IdentifierExpr w = new Bpl.IdentifierExpr(stmt.Tok, wVar);
- locals.Add(wVar);
- // havoc w;
- builder.Add(new Bpl.HavocCmd(stmt.Tok, new Bpl.IdentifierExprSeq(w)));
-
- List<Bpl.PredicateCmd> invariants = new List<Bpl.PredicateCmd>();
- Bpl.StmtListBuilder invDefinednessBuilder = new Bpl.StmtListBuilder();
- foreach (MaybeFreeExpression loopInv in s.Invariants) {
- TrStmt_CheckWellformed(loopInv.E, invDefinednessBuilder, locals, etran, false);
- invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));
-
- invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran))));
- if (loopInv.IsFree) {
- invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));
- } else {
- bool splitHappened;
- var ss = TrSplitExpr(loopInv.E, etran, out splitHappened);
- if (!splitHappened) {
- var wInv = Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E));
- invariants.Add(Assert(loopInv.E.tok, wInv, "loop invariant violation"));
- } else {
- foreach (var split in ss) {
- var wInv = Bpl.Expr.Binary(split.E.tok, BinaryOperator.Opcode.Imp, w, split.E);
- if (split.IsFree) {
- invariants.Add(new Bpl.AssumeCmd(split.E.tok, wInv));
- } else {
- invariants.Add(Assert(split.E.tok, wInv, "loop invariant violation")); // TODO: it would be fine to have this use {:subsumption 0}
- }
- }
- }
- }
- }
- // check definedness of decreases clause
- // TODO: can this check be omitted if the decreases clause is inferred?
- foreach (Expression e in theDecreases) {
- TrStmt_CheckWellformed(e, invDefinednessBuilder, locals, etran, true);
- }
- // include boilerplate invariants
- foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(stmt.Tok, currentMethod, etranPreLoop, etran)) {
- if (tri.IsFree) {
- invariants.Add(new Bpl.AssumeCmd(stmt.Tok, tri.Expr));
- } else {
- Contract.Assert(tri.ErrorMessage != null); // follows from BoilerplateTriple invariant
- invariants.Add(Assert(stmt.Tok, tri.Expr, tri.ErrorMessage));
- }
- }
- // include a free invariant that says that all completed iterations so far have only decreased the termination metric
- if (initDecr != null) {
- List<IToken> toks = new List<IToken>();
- List<Type> types = new List<Type>();
- List<Bpl.Expr> decrs = new List<Bpl.Expr>();
- foreach (Expression e in theDecreases) {
- toks.Add(e.tok);
- types.Add(cce.NonNull(e.Type));
- decrs.Add(etran.TrExpr(e));
- }
- Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, initDecr, etran, null, null, true, false);
- invariants.Add(new Bpl.AssumeCmd(stmt.Tok, decrCheck));
- }
-
- Bpl.StmtListBuilder loopBodyBuilder = new Bpl.StmtListBuilder();
- // as the first thing inside the loop, generate: if (!w) { assert IsTotal(inv); assume false; }
- invDefinednessBuilder.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.False));
- loopBodyBuilder.Add(new Bpl.IfCmd(stmt.Tok, Bpl.Expr.Not(w), invDefinednessBuilder.Collect(stmt.Tok), null, null));
- // generate: assert IsTotal(guard); if (!guard) { break; }
- Bpl.Expr guard = null;
- if (s.Guard != null) {
- TrStmt_CheckWellformed(s.Guard, loopBodyBuilder, locals, etran, true);
- guard = Bpl.Expr.Not(etran.TrExpr(s.Guard));
- }
- Bpl.StmtListBuilder guardBreak = new Bpl.StmtListBuilder();
- guardBreak.Add(new Bpl.BreakCmd(s.Tok, null));
- loopBodyBuilder.Add(new Bpl.IfCmd(s.Tok, guard, guardBreak.Collect(s.Tok), null, null));
-
- loopBodyBuilder.Add(CaptureState(stmt.Tok, "loop entered"));
- // termination checking
- if (Contract.Exists(theDecreases, e => e is WildcardExpr)) {
- // omit termination checking for this loop
- TrStmt(s.Body, loopBodyBuilder, locals, etran);
- } else {
- List<Bpl.Expr> oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr" + loopId + "$");
- // time for the actual loop body
- TrStmt(s.Body, loopBodyBuilder, locals, etran);
- // check definedness of decreases expressions
- List<IToken> toks = new List<IToken>();
- List<Type> types = new List<Type>();
- List<Bpl.Expr> decrs = new List<Bpl.Expr>();
- foreach (Expression e in theDecreases) {
- toks.Add(e.tok);
- types.Add(cce.NonNull(e.Type));
- decrs.Add(etran.TrExpr(e));
- }
- Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, oldBfs, etran, loopBodyBuilder, " at end of loop iteration", false, false);
- loopBodyBuilder.Add(Assert(stmt.Tok, decrCheck, inferredDecreases ? "cannot prove termination; try supplying a decreases clause for the loop" : "decreases expression might not decrease"));
- }
- // Finally, assume the well-formedness of the invariant (which has been checked once and for all above), so that the check
- // of invariant-maintenance can use the appropriate canCall predicates.
- foreach (MaybeFreeExpression loopInv in s.Invariants) {
- loopBodyBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, CanCallAssumption(loopInv.E, etran)));
- }
- Bpl.StmtList body = loopBodyBuilder.Collect(stmt.Tok);
-
- builder.Add(new Bpl.WhileCmd(stmt.Tok, Bpl.Expr.True, invariants, body));
- builder.Add(CaptureState(stmt.Tok, "loop exit"));
+ var s = (WhileStmt)stmt;
+ TrLoop(s, s.Guard,
+ delegate(Bpl.StmtListBuilder bld) { TrStmt(s.Body, bld, locals, etran); },
+ builder, locals, etran);
+
+ } else if (stmt is AlternativeLoopStmt) {
+ AddComment(builder, stmt, "alternative loop statement");
+ var s = (AlternativeLoopStmt)stmt;
+ var tru = new LiteralExpr(s.Tok, true);
+ tru.Type = Type.Bool; // resolve here
+ TrLoop(s, tru,
+ delegate(Bpl.StmtListBuilder bld) { TrAlternatives(s.Alternatives, null, new Bpl.BreakCmd(s.Tok, null), bld, locals, etran); },
+ builder, locals, etran);
} else if (stmt is ForeachStmt) {
AddComment(builder, stmt, "foreach statement");
@@ -3332,6 +3227,193 @@ namespace Microsoft.Dafny { }
}
+ delegate void BodyTranslator(Bpl.StmtListBuilder builder);
+
+ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator bodyTr,
+ Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran) {
+ Contract.Requires(s != null);
+ Contract.Requires(bodyTr != null);
+ Contract.Requires(builder != null);
+ Contract.Requires(locals != null);
+ Contract.Requires(etran != null);
+
+ int loopId = loopHeapVarCount;
+ loopHeapVarCount++;
+
+ // use simple heuristics to create a default decreases clause, if none is given
+ bool inferredDecreases;
+ List<Expression> theDecreases = LoopDecreasesWithDefault(s.Tok, Guard, s.Decreases, out inferredDecreases);
+
+ Bpl.LocalVariable preLoopHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$PreLoopHeap" + loopId, predef.HeapType));
+ locals.Add(preLoopHeapVar);
+ Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(s.Tok, preLoopHeapVar);
+ ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap);
+ builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr)); // TODO: does this screw up labeled breaks for this loop?
+
+ List<Bpl.Expr> initDecr = null;
+ if (!Contract.Exists(theDecreases, e => e is WildcardExpr)) {
+ initDecr = RecordDecreasesValue(theDecreases, builder, locals, etran, "$decr" + loopId + "$init$");
+ }
+
+ // the variable w is used to coordinate the definedness checking of the loop invariant
+ Bpl.LocalVariable wVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$w" + loopId, Bpl.Type.Bool));
+ Bpl.IdentifierExpr w = new Bpl.IdentifierExpr(s.Tok, wVar);
+ locals.Add(wVar);
+ // havoc w;
+ builder.Add(new Bpl.HavocCmd(s.Tok, new Bpl.IdentifierExprSeq(w)));
+
+ List<Bpl.PredicateCmd> invariants = new List<Bpl.PredicateCmd>();
+ Bpl.StmtListBuilder invDefinednessBuilder = new Bpl.StmtListBuilder();
+ foreach (MaybeFreeExpression loopInv in s.Invariants) {
+ TrStmt_CheckWellformed(loopInv.E, invDefinednessBuilder, locals, etran, false);
+ invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));
+
+ invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran))));
+ if (loopInv.IsFree) {
+ invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));
+ } else {
+ bool splitHappened;
+ var ss = TrSplitExpr(loopInv.E, etran, out splitHappened);
+ if (!splitHappened) {
+ var wInv = Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E));
+ invariants.Add(Assert(loopInv.E.tok, wInv, "loop invariant violation"));
+ } else {
+ foreach (var split in ss) {
+ var wInv = Bpl.Expr.Binary(split.E.tok, BinaryOperator.Opcode.Imp, w, split.E);
+ if (split.IsFree) {
+ invariants.Add(new Bpl.AssumeCmd(split.E.tok, wInv));
+ } else {
+ invariants.Add(Assert(split.E.tok, wInv, "loop invariant violation")); // TODO: it would be fine to have this use {:subsumption 0}
+ }
+ }
+ }
+ }
+ }
+ // check definedness of decreases clause
+ // TODO: can this check be omitted if the decreases clause is inferred?
+ foreach (Expression e in theDecreases) {
+ TrStmt_CheckWellformed(e, invDefinednessBuilder, locals, etran, true);
+ }
+ // include boilerplate invariants
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, currentMethod, etranPreLoop, etran)) {
+ if (tri.IsFree) {
+ invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));
+ } else {
+ Contract.Assert(tri.ErrorMessage != null); // follows from BoilerplateTriple invariant
+ invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage));
+ }
+ }
+ // include a free invariant that says that all completed iterations so far have only decreased the termination metric
+ if (initDecr != null) {
+ List<IToken> toks = new List<IToken>();
+ List<Type> types = new List<Type>();
+ List<Bpl.Expr> decrs = new List<Bpl.Expr>();
+ foreach (Expression e in theDecreases) {
+ toks.Add(e.tok);
+ types.Add(cce.NonNull(e.Type));
+ decrs.Add(etran.TrExpr(e));
+ }
+ Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, initDecr, etran, null, null, true, false);
+ invariants.Add(new Bpl.AssumeCmd(s.Tok, decrCheck));
+ }
+
+ Bpl.StmtListBuilder loopBodyBuilder = new Bpl.StmtListBuilder();
+ // as the first thing inside the loop, generate: if (!w) { assert IsTotal(inv); assume false; }
+ invDefinednessBuilder.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
+ loopBodyBuilder.Add(new Bpl.IfCmd(s.Tok, Bpl.Expr.Not(w), invDefinednessBuilder.Collect(s.Tok), null, null));
+ // generate: assert IsTotal(guard); if (!guard) { break; }
+ Bpl.Expr guard = null;
+ if (Guard != null) {
+ TrStmt_CheckWellformed(Guard, loopBodyBuilder, locals, etran, true);
+ guard = Bpl.Expr.Not(etran.TrExpr(Guard));
+ }
+ Bpl.StmtListBuilder guardBreak = new Bpl.StmtListBuilder();
+ guardBreak.Add(new Bpl.BreakCmd(s.Tok, null));
+ loopBodyBuilder.Add(new Bpl.IfCmd(s.Tok, guard, guardBreak.Collect(s.Tok), null, null));
+
+ loopBodyBuilder.Add(CaptureState(s.Tok, "loop entered"));
+ // termination checking
+ if (Contract.Exists(theDecreases, e => e is WildcardExpr)) {
+ // omit termination checking for this loop
+ bodyTr(loopBodyBuilder);
+ } else {
+ List<Bpl.Expr> oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr" + loopId + "$");
+ // time for the actual loop body
+ bodyTr(loopBodyBuilder);
+ // check definedness of decreases expressions
+ List<IToken> toks = new List<IToken>();
+ List<Type> types = new List<Type>();
+ List<Bpl.Expr> decrs = new List<Bpl.Expr>();
+ foreach (Expression e in theDecreases) {
+ toks.Add(e.tok);
+ types.Add(cce.NonNull(e.Type));
+ decrs.Add(etran.TrExpr(e));
+ }
+ Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, oldBfs, etran, loopBodyBuilder, " at end of loop iteration", false, false);
+ loopBodyBuilder.Add(Assert(s.Tok, decrCheck, inferredDecreases ? "cannot prove termination; try supplying a decreases clause for the loop" : "decreases expression might not decrease"));
+ }
+ // Finally, assume the well-formedness of the invariant (which has been checked once and for all above), so that the check
+ // of invariant-maintenance can use the appropriate canCall predicates.
+ foreach (MaybeFreeExpression loopInv in s.Invariants) {
+ loopBodyBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, CanCallAssumption(loopInv.E, etran)));
+ }
+ Bpl.StmtList body = loopBodyBuilder.Collect(s.Tok);
+
+ builder.Add(new Bpl.WhileCmd(s.Tok, Bpl.Expr.True, invariants, body));
+ builder.Add(CaptureState(s.Tok, "loop exit"));
+ }
+
+ void TrAlternatives(List<GuardedAlternative> alternatives, Bpl.Cmd elseCase0, Bpl.StructuredCmd elseCase1,
+ Bpl.StmtListBuilder builder, VariableSeq locals, ExpressionTranslator etran) {
+ Contract.Requires(alternatives != null);
+ Contract.Requires((elseCase0 == null) == (elseCase1 == null)); // ugly way of doing a type union
+ Contract.Requires(builder != null);
+ Contract.Requires(locals != null);
+ Contract.Requires(etran != null);
+
+ if (alternatives.Count == 0) {
+ if (elseCase0 != null) {
+ builder.Add(elseCase0);
+ } else {
+ builder.Add(elseCase1);
+ }
+ return;
+ }
+
+ // build the negation of the disjunction of all guards (that is, the conjunction of their negations)
+ Bpl.Expr noGuard = Bpl.Expr.True;
+ foreach (var alternative in alternatives) {
+ noGuard = BplAnd(noGuard, Bpl.Expr.Not(etran.TrExpr(alternative.Guard)));
+ }
+
+ var b = new Bpl.StmtListBuilder();
+ var elseTok = elseCase0 != null ? elseCase0.tok : elseCase1.tok;
+ b.Add(new Bpl.AssumeCmd(elseTok, noGuard));
+ if (elseCase0 != null) {
+ b.Add(elseCase0);
+ } else {
+ b.Add(elseCase1);
+ }
+ Bpl.StmtList els = b.Collect(elseTok);
+
+ Bpl.IfCmd elsIf = null;
+ for (int i = alternatives.Count; 0 <= --i; ) {
+ Contract.Assert(elsIf == null || els == null); // loop invariant
+ var alternative = alternatives[i];
+ b = new Bpl.StmtListBuilder();
+ TrStmt_CheckWellformed(alternative.Guard, b, locals, etran, true);
+ b.Add(new AssumeCmd(alternative.Guard.tok, etran.TrExpr(alternative.Guard)));
+ foreach (var s in alternative.Body) {
+ TrStmt(s, b, locals, etran);
+ }
+ Bpl.StmtList thn = b.Collect(alternative.Tok);
+ elsIf = new Bpl.IfCmd(alternative.Tok, null, thn, elsIf, els);
+ els = null;
+ }
+ Contract.Assert(elsIf != null && els == null); // follows from loop invariant and the fact that there's more than one alternative
+ builder.Add(elsIf);
+ }
+
void TrCallStmt(CallStmt s, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran, Bpl.Expr actualReceiver) {
Contract.Requires(s != null);
Contract.Requires(builder != null);
|