summaryrefslogtreecommitdiff
path: root/Source/Dafny
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Dafny')
-rw-r--r--Source/Dafny/Compiler.cs35
-rw-r--r--Source/Dafny/Dafny.atg18
-rw-r--r--Source/Dafny/DafnyAst.cs49
-rw-r--r--Source/Dafny/Parser.cs131
-rw-r--r--Source/Dafny/Printer.cs21
-rw-r--r--Source/Dafny/Resolver.cs120
-rw-r--r--Source/Dafny/Translator.cs13
7 files changed, 232 insertions, 155 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index fdab9ab9..82604794 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -609,14 +609,9 @@ namespace Microsoft.Dafny {
wr.WriteLine(");");
}
} else if (stmt is BreakStmt) {
- BreakStmt s = (BreakStmt)stmt;
+ var s = (BreakStmt)stmt;
Indent(indent);
- if (s.TargetLabel == null) {
- // use the scoping rules of C#
- wr.WriteLine("break;");
- } else {
- wr.WriteLine("goto after_{0};", s.TargetLabel);
- }
+ wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.UniqueId);
} else if (stmt is ReturnStmt) {
Indent(indent);
wr.WriteLine("return;");
@@ -927,29 +922,11 @@ namespace Microsoft.Dafny {
}
void TrStmtList(List<Statement/*!*/>/*!*/ stmts, int indent) {Contract.Requires(cce.NonNullElements(stmts));
- List<string/*!*/> currentLabels = null;
foreach (Statement ss in stmts) {
- if (ss is LabelStmt) {
- LabelStmt s = (LabelStmt)ss;
- if (currentLabels == null) {
- currentLabels = new List<string>();
- }
- currentLabels.Add(s.Label);
- } else {
- TrStmt(ss, indent + IndentAmount);
- SpillLabels(currentLabels, indent);
- currentLabels = null;
- }
- }
- SpillLabels(currentLabels, indent);
- }
-
- void SpillLabels(List<string> labels, int indent) {
- Contract.Requires(cce.NonNullElements(labels));
- if (labels != null) {
- foreach (string label in labels) {
- Indent(indent);
- wr.WriteLine("after_{0}: ;", label);
+ TrStmt(ss, indent + IndentAmount);
+ if (ss.Labels != null) {
+ Indent(indent); // labels are not indented as much as the statements
+ wr.WriteLine("after_{0}: ;", ss.Labels.UniqueId);
}
}
}
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index b7b81d44..e3761d57 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -434,7 +434,7 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
{ Attribute<ref attrs> }
Ident<out id>
[ GenericParameters<typeArgs> ]
- Formals<true, true, ins>
+ Formals<true, !mmod.IsGhost, ins>
[ "returns"
Formals<false, true, outs>
]
@@ -579,7 +579,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
{ Attribute<ref attrs> }
Ident<out id>
[ GenericParameters<typeArgs> ]
- Formals<true, false, formals>
+ Formals<true, isFunctionMethod, formals>
":"
Type<out returnType>
( ";"
@@ -710,6 +710,7 @@ OneStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; IToken/*!*/ id; string label = null;
s = dummyStmt; /* to please the compiler */
IToken bodyStart, bodyEnd;
+ int breakCount;
.)
/* This list does not contain BlockStmt, see comment above in Stmt production. */
( BlockStmt<out s, out bodyStart, out bodyEnd>
@@ -725,10 +726,14 @@ OneStmt<out Statement/*!*/ s>
| MatchStmt<out s>
| ForeachStmt<out s>
| "label" (. x = t; .)
- Ident<out id> ":" (. s = new LabelStmt(x, id.val); .)
- | "break" (. x = t; .)
- [ Ident<out id> (. label = id.val; .)
- ] ";" (. s = new BreakStmt(x, label); .)
+ Ident<out id> ":"
+ OneStmt<out s> (. s.Labels = new LabelNode(x, id.val, s.Labels); .)
+ | "break" (. x = t; breakCount = 1; label = null; .)
+ ( Ident<out id> (. label = id.val; .)
+ | { "break" (. breakCount++; .)
+ }
+ )
+ ";" (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)
| "return" (. x = t; .)
";" (. s = new ReturnStmt(x); .)
)
@@ -751,6 +756,7 @@ UpdateStmt<out Statement/*!*/ s>
{ "," Rhs<out r, lhs0> (. rhss.Add(r); .)
}
";"
+ | ":" (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)
)
(. s = new UpdateStmt(x, lhss, rhss); .)
.
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 8d1143af..bb5f4f67 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1141,6 +1141,8 @@ namespace Microsoft.Dafny {
public abstract class Statement {
public readonly IToken Tok;
+ public LabelNode Labels; // mutable during resolution
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Tok != null);
@@ -1153,7 +1155,25 @@ namespace Microsoft.Dafny {
}
}
- public abstract class PredicateStmt : Statement {
+ public class LabelNode
+ {
+ public readonly IToken Tok;
+ public readonly string Label;
+ public readonly int UniqueId;
+ public readonly LabelNode Next;
+ static int nodes = 0;
+
+ public LabelNode(IToken tok, string label, LabelNode next) {
+ Contract.Requires(tok != null);
+ Tok = tok;
+ Label = label;
+ Next = next;
+ UniqueId = nodes++;
+ }
+ }
+
+ public abstract class PredicateStmt : Statement
+ {
[Peer]
public readonly Expression Expr;
[ContractInvariantMethod]
@@ -1255,31 +1275,25 @@ namespace Microsoft.Dafny {
}
}
- public class LabelStmt : Statement {
- public readonly string Label;
+ public class BreakStmt : Statement {
+ public readonly string TargetLabel;
+ public readonly int BreakCount;
+ public Statement TargetStmt; // filled in during resolution
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Label != null);
+ Contract.Invariant(TargetLabel == null || 1 <= BreakCount);
}
- public LabelStmt(IToken/*!*/ tok, string/*!*/ label)
+ public BreakStmt(IToken tok, string targetLabel)
: base(tok) {
Contract.Requires(tok != null);
- Contract.Requires(label != null);
- this.Label = label;
-
+ this.TargetLabel = targetLabel;
}
- }
-
- public class BreakStmt : Statement {
- public readonly string TargetLabel;
- public Statement TargetStmt; // filled in during resolution
-
- public BreakStmt(IToken tok, string targetLabel)
+ public BreakStmt(IToken tok, int breakCount)
: base(tok) {
Contract.Requires(tok != null);
- this.TargetLabel = targetLabel;
-
+ Contract.Requires(1 <= breakCount);
+ this.BreakCount = breakCount;
}
}
@@ -1287,7 +1301,6 @@ namespace Microsoft.Dafny {
public ReturnStmt(IToken tok)
: base(tok) {
Contract.Requires(tok != null);
-
}
}
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 2fa88a69..1d7eb3e6 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -466,7 +466,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (la.kind == 23) {
GenericParameters(typeArgs);
}
- Formals(true, false, formals);
+ Formals(true, isFunctionMethod, formals);
Expect(22);
Type(out returnType);
if (la.kind == 15) {
@@ -518,7 +518,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (la.kind == 23) {
GenericParameters(typeArgs);
}
- Formals(true, true, ins);
+ Formals(true, !mmod.IsGhost, ins);
if (la.kind == 26) {
Get();
Formals(false, true, outs);
@@ -996,6 +996,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; IToken/*!*/ id; string label = null;
s = dummyStmt; /* to please the compiler */
IToken bodyStart, bodyEnd;
+ int breakCount;
if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
@@ -1026,22 +1027,28 @@ List<Expression/*!*/>/*!*/ decreases) {
x = t;
Ident(out id);
Expect(22);
- s = new LabelStmt(x, id.val);
+ OneStmt(out s);
+ s.Labels = new LabelNode(x, id.val, s.Labels);
} else if (la.kind == 48) {
Get();
- x = t;
+ x = t; breakCount = 1; label = null;
if (la.kind == 1) {
Ident(out id);
label = id.val;
- }
+ } else if (la.kind == 15 || la.kind == 48) {
+ while (la.kind == 48) {
+ Get();
+ breakCount++;
+ }
+ } else SynErr(120);
Expect(15);
- s = new BreakStmt(x, label);
+ s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
} else if (la.kind == 49) {
Get();
x = t;
Expect(15);
s = new ReturnStmt(x);
- } else SynErr(120);
+ } else SynErr(121);
}
void AssertStmt(out Statement/*!*/ s) {
@@ -1117,7 +1124,10 @@ List<Expression/*!*/>/*!*/ decreases) {
rhss.Add(r);
}
Expect(15);
- } else SynErr(121);
+ } else if (la.kind == 22) {
+ Get();
+ SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
+ } else SynErr(122);
s = new UpdateStmt(x, lhss, rhss);
}
@@ -1199,13 +1209,13 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(122);
+ } else SynErr(123);
}
ifStmt = new IfStmt(x, guard, thn, els);
} else if (la.kind == 7) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(123);
+ } else SynErr(124);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1230,7 +1240,7 @@ List<Expression/*!*/>/*!*/ decreases) {
LoopSpec(out invariants, out decreases);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives);
- } else SynErr(124);
+ } else SynErr(125);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -1295,7 +1305,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 56) {
HavocStmt(out s);
bodyAssign = s;
- } else SynErr(125);
+ } else SynErr(126);
Expect(8);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1319,7 +1329,7 @@ List<Expression/*!*/>/*!*/ decreases) {
while (la.kind == 52 || la.kind == 54) {
Suffix(ref e);
}
- } else SynErr(126);
+ } else SynErr(127);
}
void Rhs(out DeterminedAssignmentRhs r, Expression receiverForInitCall) {
@@ -1369,7 +1379,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(8)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(127);
+ } else SynErr(128);
}
void Guard(out Expression e) {
@@ -1381,7 +1391,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(128);
+ } else SynErr(129);
Expect(33);
}
@@ -1471,7 +1481,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(8)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(129);
+ } else SynErr(130);
}
void EquivExpression(out Expression/*!*/ e0) {
@@ -1501,7 +1511,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 68) {
Get();
- } else SynErr(130);
+ } else SynErr(131);
}
void LogicalExpression(out Expression/*!*/ e0) {
@@ -1539,7 +1549,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 70) {
Get();
- } else SynErr(131);
+ } else SynErr(132);
}
void RelationalExpression(out Expression/*!*/ e0) {
@@ -1557,7 +1567,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 72) {
Get();
- } else SynErr(132);
+ } else SynErr(133);
}
void OrOp() {
@@ -1565,7 +1575,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 74) {
Get();
- } else SynErr(133);
+ } else SynErr(134);
}
void Term(out Expression/*!*/ e0) {
@@ -1641,7 +1651,7 @@ List<Expression/*!*/>/*!*/ decreases) {
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(134); break;
+ default: SynErr(135); break;
}
}
@@ -1663,7 +1673,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(135);
+ } else SynErr(136);
}
void UnaryExpression(out Expression/*!*/ e) {
@@ -1690,7 +1700,7 @@ List<Expression/*!*/>/*!*/ decreases) {
while (la.kind == 52 || la.kind == 54) {
Suffix(ref e);
}
- } else SynErr(136);
+ } else SynErr(137);
}
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
@@ -1704,7 +1714,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 87) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(137);
+ } else SynErr(138);
}
void NegOp() {
@@ -1712,7 +1722,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 89) {
Get();
- } else SynErr(138);
+ } else SynErr(139);
}
void EndlessExpression(out Expression e) {
@@ -1733,7 +1743,7 @@ List<Expression/*!*/>/*!*/ decreases) {
QuantifierGuts(out e);
} else if (la.kind == 37) {
ComprehensionExpr(out e);
- } else SynErr(139);
+ } else SynErr(140);
}
void DottedIdentifiersAndFunction(out Expression e) {
@@ -1806,12 +1816,12 @@ List<Expression/*!*/>/*!*/ decreases) {
multipleIndices.Add(ee);
}
- } else SynErr(140);
+ } else SynErr(141);
} else if (la.kind == 98) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(141);
+ } else SynErr(142);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -1835,7 +1845,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
Expect(53);
- } else SynErr(142);
+ } else SynErr(143);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -1932,7 +1942,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(33);
break;
}
- default: SynErr(143); break;
+ default: SynErr(144); break;
}
}
@@ -1963,7 +1973,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 101 || la.kind == 102) {
Exists();
x = t;
- } else SynErr(144);
+ } else SynErr(145);
IdentTypeOptional(out bv);
bvars.Add(bv);
while (la.kind == 19) {
@@ -2021,7 +2031,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 100) {
Get();
- } else SynErr(145);
+ } else SynErr(146);
}
void Exists() {
@@ -2029,7 +2039,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 102) {
Get();
- } else SynErr(146);
+ } else SynErr(147);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -2042,7 +2052,7 @@ List<Expression/*!*/>/*!*/ decreases) {
es = new List<Expression/*!*/>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(147);
+ } else SynErr(148);
Expect(8);
}
@@ -2051,7 +2061,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 104) {
Get();
- } else SynErr(148);
+ } else SynErr(149);
}
void AttributeBody(ref Attributes attrs) {
@@ -2250,34 +2260,35 @@ public class Errors {
case 118: s = "invalid PossiblyWildExpression"; break;
case 119: s = "invalid MatchOrExpr"; break;
case 120: s = "invalid OneStmt"; break;
- case 121: s = "invalid UpdateStmt"; break;
- case 122: s = "invalid IfStmt"; break;
+ case 121: s = "invalid OneStmt"; break;
+ case 122: s = "invalid UpdateStmt"; break;
case 123: s = "invalid IfStmt"; break;
- case 124: s = "invalid WhileStmt"; break;
- case 125: s = "invalid ForeachStmt"; break;
- case 126: s = "invalid Lhs"; break;
- case 127: s = "invalid Rhs"; break;
- case 128: s = "invalid Guard"; break;
- case 129: s = "invalid AttributeArg"; break;
- case 130: s = "invalid EquivOp"; break;
- case 131: s = "invalid ImpliesOp"; break;
- case 132: s = "invalid AndOp"; break;
- case 133: s = "invalid OrOp"; break;
- case 134: s = "invalid RelOp"; break;
- case 135: s = "invalid AddOp"; break;
- case 136: s = "invalid UnaryExpression"; break;
- case 137: s = "invalid MulOp"; break;
- case 138: s = "invalid NegOp"; break;
- case 139: s = "invalid EndlessExpression"; break;
- case 140: s = "invalid Suffix"; break;
+ case 124: s = "invalid IfStmt"; break;
+ case 125: s = "invalid WhileStmt"; break;
+ case 126: s = "invalid ForeachStmt"; break;
+ case 127: s = "invalid Lhs"; break;
+ case 128: s = "invalid Rhs"; break;
+ case 129: s = "invalid Guard"; 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 EndlessExpression"; break;
case 141: s = "invalid Suffix"; break;
case 142: s = "invalid Suffix"; break;
- case 143: s = "invalid ConstAtomExpression"; break;
- case 144: s = "invalid QuantifierGuts"; break;
- case 145: s = "invalid Forall"; break;
- case 146: s = "invalid Exists"; break;
- case 147: s = "invalid AttributeOrTrigger"; break;
- case 148: s = "invalid QSep"; break;
+ case 143: s = "invalid Suffix"; break;
+ case 144: s = "invalid ConstAtomExpression"; break;
+ case 145: s = "invalid QuantifierGuts"; 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;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index f5fba723..c92b477a 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -396,6 +396,13 @@ namespace Microsoft.Dafny {
/// </summary>
public void PrintStatement(Statement stmt, int indent) {
Contract.Requires(stmt != null);
+ for (LabelNode label = stmt.Labels; label != null; label = label.Next) {
+ if (label.Label != null) {
+ wr.WriteLine("label {0}:", label.Label);
+ Indent(indent);
+ }
+ }
+
if (stmt is AssertStmt) {
wr.Write("assert ");
PrintExpression(((AssertStmt)stmt).Expr);
@@ -417,15 +424,17 @@ namespace Microsoft.Dafny {
PrintAttributeArgs(s.Args);
wr.Write(";");
- } else if (stmt is LabelStmt) {
- wr.Write("label {0}:", ((LabelStmt)stmt).Label);
-
} else if (stmt is BreakStmt) {
BreakStmt s = (BreakStmt)stmt;
- if (s.TargetLabel == null) {
- wr.Write("break;");
- } else {
+ if (s.TargetLabel != null) {
wr.Write("break {0};", s.TargetLabel);
+ } else {
+ string sep = "";
+ for (int i = 0; i < s.BreakCount; i++) {
+ wr.Write("{0}break", sep);
+ sep = " ";
+ }
+ wr.Write(";");
}
} else if (stmt is ReturnStmt) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index a7fe06ec..3eb3bd34 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -277,6 +277,8 @@ namespace Microsoft.Dafny {
readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();
readonly Scope<IVariable>/*!*/ scope = new Scope<IVariable>();
readonly Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();
+ readonly List<Statement> loopStack = new List<Statement>(); // the enclosing loops (from which it is possible to break out)
+ readonly Dictionary<Statement, bool> inSpecOnlyContext = new Dictionary<Statement, bool>(); // invariant: domain contain union of the domains of "labeledStatements" and "loopStack"
/// <summary>
/// Assumes type parameters have already been pushed
@@ -1118,11 +1120,14 @@ namespace Microsoft.Dafny {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type
}
}
-
+
+ /// <summary>
+ /// "specContextOnly" means that the statement must be erasable, that is, it should be okay to omit it
+ /// at run time. That means it must not have any side effects on non-ghost variables, for example.
+ /// </summary>
public void ResolveStatement(Statement stmt, bool specContextOnly, Method method) {
Contract.Requires(stmt != null);
Contract.Requires(method != null);
- Contract.Requires(!(stmt is LabelStmt)); // these should be handled inside lists of statements
if (stmt is UseStmt) {
UseStmt s = (UseStmt)stmt;
s.IsGhost = true;
@@ -1153,21 +1158,36 @@ namespace Microsoft.Dafny {
}
} else if (stmt is BreakStmt) {
- BreakStmt s = (BreakStmt)stmt;
+ var s = (BreakStmt)stmt;
if (s.TargetLabel != null) {
Statement target = labeledStatements.Find(s.TargetLabel);
if (target == null) {
Error(s, "break label is undefined or not in scope: {0}", s.TargetLabel);
} else {
s.TargetStmt = target;
+ bool targetIsLoop = target is WhileStmt || target is AlternativeLoopStmt;
+ if (specContextOnly && !s.TargetStmt.IsGhost && !inSpecOnlyContext[s.TargetStmt]) {
+ Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost " + (targetIsLoop ? "loop" : "structure"));
+ }
+ }
+ } else {
+ if (loopStack.Count < s.BreakCount) {
+ Error(s, "trying to break out of more loop levels than there are enclosing loops");
+ } else {
+ Statement target = loopStack[loopStack.Count - s.BreakCount];
+ if (target.Labels == null) {
+ // make sure there is a label, because the compiler and translator will want to see a unique ID
+ target.Labels = new LabelNode(target.Tok, null, null);
+ }
+ s.TargetStmt = target;
+ if (specContextOnly && !target.IsGhost && !inSpecOnlyContext[target]) {
+ Error(stmt, "ghost-context break statement is not allowed to break out of non-ghost loop");
+ }
}
- }
- if (specContextOnly) {
- Error(stmt, "break statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
} else if (stmt is ReturnStmt) {
- if (specContextOnly) {
+ if (specContextOnly && !method.IsGhost) {
Error(stmt, "return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
@@ -1301,7 +1321,7 @@ namespace Microsoft.Dafny {
if (var == null) {
// the LHS didn't resolve correctly; some error would already have been reported
} else {
- lvalueIsGhost = var.IsGhost;
+ lvalueIsGhost = var.IsGhost || method.IsGhost;
if (!var.IsMutable) {
Error(stmt, "LHS of assignment must denote a mutable variable or field");
}
@@ -1441,7 +1461,7 @@ namespace Microsoft.Dafny {
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
- s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, method);
+ s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, null, method);
} else if (stmt is WhileStmt) {
WhileStmt s = (WhileStmt)stmt;
@@ -1473,11 +1493,16 @@ namespace Microsoft.Dafny {
// any type is fine
}
s.IsGhost = bodyMustBeSpecOnly;
+ loopStack.Add(s); // push
+ if (s.Labels == null) { // otherwise, "s" is already in "inSpecOnlyContext" map
+ inSpecOnlyContext.Add(s, specContextOnly);
+ }
ResolveStatement(s.Body, bodyMustBeSpecOnly, method);
+ loopStack.RemoveAt(loopStack.Count-1); // pop
} else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
- s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, method);
+ s.IsGhost = ResolveAlternatives(s.Alternatives, specContextOnly, s, method);
foreach (MaybeFreeExpression inv in s.Invariants) {
ResolveExpression(inv.E, true);
Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression
@@ -1643,7 +1668,7 @@ namespace Microsoft.Dafny {
}
}
- bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, Method method) {
+ bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, Method method) {
Contract.Requires(alternatives != null);
Contract.Requires(method != null);
@@ -1661,6 +1686,13 @@ namespace Microsoft.Dafny {
isGhost = isGhost || UsesSpecFeatures(alternative.Guard);
}
}
+
+ if (loopToCatchBreaks != null) {
+ loopStack.Add(loopToCatchBreaks); // push
+ if (loopToCatchBreaks.Labels == null) { // otherwise, "loopToCatchBreak" is already in "inSpecOnlyContext" map
+ inSpecOnlyContext.Add(loopToCatchBreaks, specContextOnly);
+ }
+ }
foreach (var alternative in alternatives) {
scope.PushMarker();
foreach (Statement ss in alternative.Body) {
@@ -1668,6 +1700,10 @@ namespace Microsoft.Dafny {
}
scope.PopMarker();
}
+ if (loopToCatchBreaks != null) {
+ loopStack.RemoveAt(loopStack.Count - 1); // pop
+ }
+
return isGhost;
}
@@ -1795,25 +1831,33 @@ namespace Microsoft.Dafny {
}
}
}
-
+
void ResolveBlockStatement(BlockStmt blockStmt, bool specContextOnly, Method method)
{
Contract.Requires(blockStmt != null);
Contract.Requires(method != null);
- int labelsToPop = 0;
+
foreach (Statement ss in blockStmt.Body) {
- if (ss is LabelStmt) {
- LabelStmt ls = (LabelStmt)ss;
- labeledStatements.PushMarker();
- bool b = labeledStatements.Push(ls.Label, ls);
- Contract.Assert(b); // since we just pushed a marker, we expect the Push to succeed
- labelsToPop++;
- } else {
- ResolveStatement(ss, specContextOnly, method);
- for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }
+ labeledStatements.PushMarker();
+ // push labels
+ for (var lnode = ss.Labels; lnode != null; lnode = lnode.Next) {
+ Contract.Assert(lnode.Label != null); // LabelNode's with .Label==null are added only during resolution of the break statements with 'stmt' as their target, which hasn't happened yet
+ var prev = labeledStatements.Find(lnode.Label);
+ if (prev == ss) {
+ Error(lnode.Tok, "duplicate label");
+ } else if (prev != null) {
+ Error(lnode.Tok, "label shadows an enclosing label");
+ } else {
+ bool b = labeledStatements.Push(lnode.Label, ss);
+ Contract.Assert(b); // since we just checked for duplicates, we expect the Push to succeed
+ if (lnode == ss.Labels) { // add it only once
+ inSpecOnlyContext.Add(ss, specContextOnly);
+ }
+ }
}
+ ResolveStatement(ss, specContextOnly, method);
+ labeledStatements.PopMarker();
}
- for (; 0 < labelsToPop; labelsToPop--) { labeledStatements.PopMarker(); }
}
Type ResolveTypeRhs(TypeRhs rr, Statement stmt, bool specContextOnly, Method method) {
@@ -2544,25 +2588,43 @@ namespace Microsoft.Dafny {
Contract.Requires(expr.Type != null); // this check approximates the requirement that "expr" be resolved
if (expr is IdentifierExpr) {
- IdentifierExpr e = (IdentifierExpr)expr;
+ var e = (IdentifierExpr)expr;
if (e.Var != null && e.Var.IsGhost) {
Error(expr, "ghost variables are allowed only in specification contexts");
return;
}
} else if (expr is FieldSelectExpr) {
- FieldSelectExpr e = (FieldSelectExpr)expr;
+ var e = (FieldSelectExpr)expr;
if (e.Field != null && e.Field.IsGhost) {
Error(expr, "ghost fields are allowed only in specification contexts");
return;
}
} else if (expr is FunctionCallExpr) {
- FunctionCallExpr e = (FunctionCallExpr)expr;
+ var e = (FunctionCallExpr)expr;
if (e.Function != null && e.Function.IsGhost) {
Error(expr, "function calls are allowed only in specification contexts (consider declaring the function a 'function method')");
return;
}
+ // function is okay, so check all NON-ghost arguments
+ CheckIsNonGhost(e.Receiver);
+ for (int i = 0; i < e.Function.Formals.Count; i++) {
+ if (!e.Function.Formals[i].IsGhost) {
+ CheckIsNonGhost(e.Args[i]);
+ }
+ }
+ return;
+
+ } else if (expr is DatatypeValue) {
+ var e = (DatatypeValue)expr;
+ // check all NON-ghost arguments
+ for (int i = 0; i < e.Ctor.Formals.Count; i++) {
+ if (!e.Ctor.Formals[i].IsGhost) {
+ CheckIsNonGhost(e.Arguments[i]);
+ }
+ }
+ return;
} else if (expr is OldExpr) {
Error(expr, "old expressions are allowed only in specification and ghost contexts");
@@ -2577,7 +2639,7 @@ namespace Microsoft.Dafny {
return;
} else if (expr is BinaryExpr) {
- BinaryExpr e = (BinaryExpr)expr;
+ var e = (BinaryExpr)expr;
switch (e.ResolvedOp) {
case BinaryExpr.ResolvedOpcode.RankGt:
case BinaryExpr.ResolvedOpcode.RankLt:
@@ -2588,7 +2650,7 @@ namespace Microsoft.Dafny {
}
} else if (expr is QuantifierExpr) {
- QuantifierExpr e = (QuantifierExpr)expr;
+ var e = (QuantifierExpr)expr;
if (e.MissingBounds != null) {
foreach (var bv in e.MissingBounds) {
Error(expr, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
@@ -3454,7 +3516,7 @@ namespace Microsoft.Dafny {
return Contract.Exists( me.Cases,mc=> UsesSpecFeatures(mc.Body));
} else if (expr is ConcreteSyntaxExpression) {
var e = (ConcreteSyntaxExpression)expr;
- return UsesSpecFeatures(e.ResolvedExpression);
+ return e.ResolvedExpression != null && UsesSpecFeatures(e.ResolvedExpression);
} else {
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index eb1d1cca..50e7965c 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2899,7 +2899,6 @@ namespace Microsoft.Dafny {
Contract.Requires(etran != null);
Contract.Requires(currentMethod != null && predef != null);
Contract.Ensures(Contract.Result<Bpl.StmtList>() != null);
-
return TrStmt2StmtList(new Bpl.StmtListBuilder(), block, locals, etran);
}
@@ -2912,7 +2911,6 @@ namespace Microsoft.Dafny {
Contract.Requires(etran != null);
Contract.Requires(currentMethod != null && predef != null);
Contract.Ensures(Contract.Result<Bpl.StmtList>() != null);
-
TrStmt(block, builder, locals, etran);
return builder.Collect(block.Tok); // TODO: would be nice to have an end-curly location for "block"
@@ -2961,12 +2959,10 @@ namespace Microsoft.Dafny {
}
}
- } else if (stmt is LabelStmt) {
- AddComment(builder, stmt, "label statement"); // TODO: ouch, comments probably mess up what the label labels in the Boogie program
- builder.AddLabelCmd(((LabelStmt)stmt).Label);
} else if (stmt is BreakStmt) {
AddComment(builder, stmt, "break statement");
- builder.Add(new Bpl.BreakCmd(stmt.Tok, ((BreakStmt)stmt).TargetLabel)); // TODO: handle name clashes of labels
+ var s = (BreakStmt)stmt;
+ builder.Add(new GotoCmd(s.Tok, new StringSeq("after_" + s.TargetStmt.Labels.UniqueId)));
} else if (stmt is ReturnStmt) {
AddComment(builder, stmt, "return statement");
builder.Add(new Bpl.ReturnCmd(stmt.Tok));
@@ -2988,6 +2984,9 @@ namespace Microsoft.Dafny {
} else if (stmt is BlockStmt) {
foreach (Statement ss in ((BlockStmt)stmt).Body) {
TrStmt(ss, builder, locals, etran);
+ if (ss.Labels != null) {
+ builder.AddLabelCmd("after_" + ss.Labels.UniqueId);
+ }
}
} else if (stmt is IfStmt) {
AddComment(builder, stmt, "if statement");
@@ -3259,7 +3258,7 @@ namespace Microsoft.Dafny {
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?
+ builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr));
List<Bpl.Expr> initDecr = null;
if (!Contract.Exists(theDecreases, e => e is WildcardExpr)) {
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-01 13:03:38 +0000