From 7ca1c590659d2c11a67b138b8251cf5dffc03b38 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 19 May 2011 17:29:04 -0700 Subject: Dafny: added alternative statement and alternative-loop statement --- Source/Dafny/Compiler.cs | 37 ++++- Source/Dafny/Dafny.atg | 64 ++++++-- Source/Dafny/DafnyAst.cs | 87 +++++++++-- Source/Dafny/Parser.cs | 290 +++++++++++++++++++++--------------- Source/Dafny/Printer.cs | 41 ++++- Source/Dafny/Resolver.cs | 54 ++++++- Source/Dafny/Scanner.cs | 102 +++++++------ Source/Dafny/Translator.cs | 364 +++++++++++++++++++++++++++------------------ 8 files changed, 700 insertions(+), 339 deletions(-) (limited to 'Source') 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> pendingUpdates = new List>(); @@ -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 Statement/*!*/ s; Statement els = null; IToken bodyStart, bodyEnd; + List alternatives; + ifStmt = dummyStmt; // to please the compiler .) "if" (. x = t; .) - Guard - BlockStmt - [ "else" - ( IfStmt (. els = s; .) - | BlockStmt (. els = s; .) - ) - ] - (. ifStmt = new IfStmt(x, guard, thn, els); .) + ( + Guard + BlockStmt + [ "else" + ( IfStmt (. els = s; .) + | BlockStmt (. els = s; .) + ) + ] + (. ifStmt = new IfStmt(x, guard, thn, els); .) + | + AlternativeBlock + (. ifStmt = new AlternativeStmt(x, alternatives); .) + ) + . + +AlternativeBlock<.out List alternatives.> += (. alternatives = new List(); + IToken x; + Expression e; + List body; + .) + "{" + { "case" (. x = t; .) + Expression + "=>" + (. body = new List(); .) + (. parseVarScope.PushMarker(); .) + { Stmt } + (. parseVarScope.PopMarker(); .) + (. alternatives.Add(new GuardedAlternative(x, e, body)); .) + } + "}" . WhileStmt = (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x; Expression guard; - bool isFree; Expression/*!*/ e; List invariants = new List(); List decreases = new List(); Statement/*!*/ body; IToken bodyStart, bodyEnd; + List alternatives; + stmt = dummyStmt; // to please the compiler .) "while" (. x = t; .) - Guard (. Contract.Assume(guard == null || cce.Owner.None(guard)); .) + ( + Guard (. Contract.Assume(guard == null || cce.Owner.None(guard)); .) + LoopSpec + BlockStmt + (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .) + | + LoopSpec + AlternativeBlock + (. stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives); .) + ) + . + +LoopSpec<.out List invariants, out List decreases.> += (. bool isFree; Expression/*!*/ e; + invariants = new List(); + decreases = new List(); + .) { (. isFree = false; .) [ "free" (. isFree = true; .) ] @@ -916,7 +959,6 @@ WhileStmt } ";" } - BlockStmt (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .) . Guard /* 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 Body; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Tok != null); + Contract.Invariant(Guard != null); + Contract.Invariant(Body != null); + } + public GuardedAlternative(IToken tok, Expression guard, List 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 Alternatives; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Alternatives != null); + } + public AlternativeStmt(IToken tok, List alternatives) + : base(tok) { + Contract.Requires(tok != null); + Contract.Requires(alternatives != null); + this.Alternatives = alternatives; + } + } + + public abstract class LoopStmt : Statement + { public readonly List/*!*/ Invariants; public readonly List/*!*/ 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/*!*/ invariants, List/*!*/ 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/*!*/ invariants, List/*!*/ 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 Alternatives; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Alternatives != null); + } + public AlternativeLoopStmt(IToken tok, + List/*!*/ invariants, List/*!*/ decreases, + List 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= 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 theImports; @@ -1267,62 +1267,54 @@ List/*!*/ decreases) { Statement/*!*/ s; Statement els = null; IToken bodyStart, bodyEnd; + List 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 invariants = new List(); List decreases = new List(); Statement/*!*/ body; IToken bodyStart, bodyEnd; + List 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/*!*/ 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/*!*/ decreases) { } else if (StartOf(8)) { Expression(out e); ee = new List() { e }; - } else SynErr(126); + } else SynErr(128); if (ee == null && ty == null) { ee = new List() { dummyExpr}; } } @@ -1454,7 +1446,7 @@ List/*!*/ 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/*!*/ decreases) { } else if (StartOf(8)) { Expression(out ee); e = ee; - } else SynErr(128); + } else SynErr(130); Expect(33); } + void AlternativeBlock(out List alternatives) { + alternatives = new List(); + IToken x; + Expression e; + List body; + + Expect(7); + while (la.kind == 45) { + Get(); + x = t; + Expression(out e); + Expect(46); + body = new List(); + parseVarScope.PushMarker(); + while (StartOf(9)) { + Stmt(body); + } + parseVarScope.PopMarker(); + alternatives.Add(new GuardedAlternative(x, e, body)); + } + Expect(8); + } + + void LoopSpec(out List invariants, out List decreases) { + bool isFree; Expression/*!*/ e; + invariants = new List(); + decreases = new List(); + + 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ decreases) { Get(); } else if (la.kind == 73) { Get(); - } else SynErr(133); + } else SynErr(135); } void OrOp() { @@ -1652,7 +1697,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 75) { Get(); - } else SynErr(134); + } else SynErr(136); } void Term(out Expression/*!*/ e0) { @@ -1728,7 +1773,7 @@ List/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(135); break; + default: SynErr(137); break; } } @@ -1750,7 +1795,7 @@ List/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ decreases) { Get(); } else if (la.kind == 90) { Get(); - } else SynErr(139); + } else SynErr(141); } void ConstAtomExpression(out Expression/*!*/ e) { @@ -1902,7 +1947,7 @@ List/*!*/ decreases) { ComprehensionExpr(out e); break; } - default: SynErr(140); break; + default: SynErr(142); break; } } @@ -1933,7 +1978,7 @@ List/*!*/ 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/*!*/ 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/*!*/ decreases) { Get(); Expression(out e); Expect(33); - } else SynErr(142); + } else SynErr(144); } void SelectOrCallSuffix(ref Expression/*!*/ e) { @@ -2077,12 +2123,12 @@ List/*!*/ 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/*!*/ decreases) { } Expect(53); - } else SynErr(145); + } else SynErr(147); } void Forall() { @@ -2114,7 +2160,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 102) { Get(); - } else SynErr(146); + } else SynErr(148); } void Exists() { @@ -2122,7 +2168,7 @@ List/*!*/ 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/*!*/ decreases) { es = new List(); Expressions(es); trigs = new Triggers(es, trigs); - } else SynErr(148); + } else SynErr(150); Expect(8); } @@ -2144,7 +2190,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 106) { Get(); - } else SynErr(149); + } else SynErr(151); } void AttributeBody(ref Attributes attrs) { @@ -2155,7 +2201,7 @@ List/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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 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 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() != 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() != 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() != 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 LoopDecreasesWithDefault(WhileStmt s, out bool inferredDecreases) { - Contract.Requires(s != null); + List LoopDecreasesWithDefault(IToken tok, Expression Guard, List Decreases, out bool inferredDecreases) { + Contract.Requires(tok != null); + Contract.Requires(Decreases != null); - List theDecreases = s.Decreases; + List theDecreases = Decreases; inferredDecreases = false; - if (theDecreases.Count == 0 && s.Guard != null) { + if (theDecreases.Count == 0 && Guard != null) { theDecreases = new List(); 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 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 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 invariants = new List(); - 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 toks = new List(); - List types = new List(); - List decrs = new List(); - 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 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 toks = new List(); - List types = new List(); - List decrs = new List(); - 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 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 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 invariants = new List(); + 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 toks = new List(); + List types = new List(); + List decrs = new List(); + 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 oldBfs = RecordDecreasesValue(theDecreases, loopBodyBuilder, locals, etran, "$decr" + loopId + "$"); + // time for the actual loop body + bodyTr(loopBodyBuilder); + // check definedness of decreases expressions + List toks = new List(); + List types = new List(); + List decrs = new List(); + 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 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); -- cgit v1.2.3