diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 6 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 19 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 27 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 70 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 12 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 101 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 4 |
7 files changed, 179 insertions, 60 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 35f81605..920105a9 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -641,8 +641,10 @@ namespace Microsoft.Dafny { Indent(indent);
wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.UniqueId);
} else if (stmt is ReturnStmt) {
- Indent(indent);
- wr.WriteLine("return;");
+ var s = (ReturnStmt)stmt;
+ if (s.hiddenUpdate != null)
+ TrStmt(s.hiddenUpdate, indent);
+ Indent(indent); wr.WriteLine("return;");
} else if (stmt is UpdateStmt) {
var s = (UpdateStmt)stmt;
var resolved = s.ResolvedStatements;
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 033bc239..c69a6838 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -26,7 +26,7 @@ static BuiltIns theBuiltIns; static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
-static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken);
+static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");
static int anonymousIds = 0;
@@ -696,11 +696,24 @@ OneStmt<out Statement/*!*/ s> }
)
";" (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)
- | "return" (. x = t; .)
- ";" (. s = new ReturnStmt(x); .)
+ | ReturnStmt<out s>
)
.
+ReturnStmt<out Statement/*!*/ s>
+= (.
+ IToken returnTok = null;
+ List<AssignmentRhs> rhss = null;
+ AssignmentRhs r;
+ .)
+ "return" (. returnTok = t; .)
+ [
+ Rhs<out r, null> (. rhss = new List<AssignmentRhs>(); rhss.Add(r); .)
+ { "," Rhs<out r, null> (. rhss.Add(r); .)
+ }
+ ]
+ ";" (. s = new ReturnStmt(returnTok, rhss); .)
+ .
UpdateStmt<out Statement/*!*/ s>
= (. List<Expression> lhss = new List<Expression>();
List<AssignmentRhs> rhss = new List<AssignmentRhs>();
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 0fd83011..0b3435e8 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1302,9 +1302,13 @@ namespace Microsoft.Dafny { }
public class ReturnStmt : Statement {
- public ReturnStmt(IToken tok)
+ public List<AssignmentRhs> rhss;
+ public UpdateStmt hiddenUpdate;
+ public ReturnStmt(IToken tok, List<AssignmentRhs> rhss)
: base(tok) {
Contract.Requires(tok != null);
+ this.rhss = rhss;
+ hiddenUpdate = null;
}
}
@@ -1337,7 +1341,7 @@ namespace Microsoft.Dafny { {
public readonly Type EType;
public readonly List<Expression> ArrayDimensions;
- public readonly CallStmt InitCall; // may be null (and is definitely null for arrays)
+ public CallStmt InitCall; // may be null (and is definitely null for arrays)
public Type Type; // filled in during resolution
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -1407,6 +1411,7 @@ namespace Microsoft.Dafny { this.MethodName = methodName;
this.Args = args;
}
+ // TODO: Investigate this. For an initialization, this is true. But for existing objects, this is not true.
public override bool CanAffectPreviouslyKnownExpressions {
get {
foreach (var mod in Method.Mod) {
@@ -1458,6 +1463,7 @@ namespace Microsoft.Dafny { {
public readonly List<Expression> Lhss;
public readonly List<AssignmentRhs> Rhss;
+ public bool secretlyReturnStatment;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Lhss));
@@ -1472,6 +1478,18 @@ namespace Microsoft.Dafny { Contract.Requires(lhss.Count != 0 || rhss.Count == 1);
Lhss = lhss;
Rhss = rhss;
+ secretlyReturnStatment = false;
+ }
+ public UpdateStmt(IToken tok, List<Expression> lhss, List<AssignmentRhs> rhss, bool srs)
+ : base(tok)
+ {
+ Contract.Requires(tok != null);
+ Contract.Requires(cce.NonNullElements(lhss));
+ Contract.Requires(cce.NonNullElements(rhss));
+ Contract.Requires(lhss.Count != 0 || rhss.Count == 1);
+ Lhss = lhss;
+ Rhss = rhss;
+ secretlyReturnStatment = srs;
}
}
@@ -1558,14 +1576,14 @@ namespace Microsoft.Dafny { public class CallStmt : Statement {
[ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(Receiver != null);
+ //Contract.Invariant(Receiver != null);
Contract.Invariant(MethodName != null);
Contract.Invariant(cce.NonNullElements(Lhs));
Contract.Invariant(cce.NonNullElements(Args));
}
public readonly List<Expression/*!*/>/*!*/ Lhs;
- public readonly Expression/*!*/ Receiver;
+ public Expression/*!*/ Receiver;
public readonly string/*!*/ MethodName;
public readonly List<Expression/*!*/>/*!*/ Args;
public Method Method; // filled in by resolution
@@ -1575,7 +1593,6 @@ namespace Microsoft.Dafny { : base(tok) {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(lhs));
- Contract.Requires(receiver != null);
Contract.Requires(methodName != null);
Contract.Requires(cce.NonNullElements(args));
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index b77f5e65..f9bb0768 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -39,7 +39,7 @@ static BuiltIns theBuiltIns; static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
-static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken);
+static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");
static int anonymousIds = 0;
@@ -1025,10 +1025,7 @@ List<Expression/*!*/>/*!*/ decreases) { break;
}
case 47: {
- Get();
- x = t;
- Expect(17);
- s = new ReturnStmt(x);
+ ReturnStmt(out s);
break;
}
default: SynErr(117); break;
@@ -1274,21 +1271,24 @@ List<Expression/*!*/>/*!*/ decreases) { }
- void Lhs(out Expression e) {
- e = null; // to please the compiler
+ void ReturnStmt(out Statement/*!*/ s) {
+ IToken returnTok = null;
+ List<AssignmentRhs> rhss = null;
+ AssignmentRhs r;
- if (la.kind == 1) {
- DottedIdentifiersAndFunction(out e);
- while (la.kind == 50 || la.kind == 52) {
- Suffix(ref e);
- }
- } else if (StartOf(12)) {
- ConstAtomExpression(out e);
- Suffix(ref e);
- while (la.kind == 50 || la.kind == 52) {
- Suffix(ref e);
+ Expect(47);
+ returnTok = t;
+ if (StartOf(12)) {
+ Rhs(out r, null);
+ rhss = new List<AssignmentRhs>(); rhss.Add(r);
+ while (la.kind == 19) {
+ Get();
+ Rhs(out r, null);
+ rhss.Add(r);
}
- } else SynErr(122);
+ }
+ Expect(17);
+ s = new ReturnStmt(returnTok, rhss);
}
void Rhs(out AssignmentRhs r, Expression receiverForInitCall) {
@@ -1341,6 +1341,23 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (StartOf(8)) {
Expression(out e);
r = new ExprRhs(e);
+ } else SynErr(122);
+ }
+
+ void Lhs(out Expression e) {
+ e = null; // to please the compiler
+
+ if (la.kind == 1) {
+ DottedIdentifiersAndFunction(out e);
+ while (la.kind == 50 || la.kind == 52) {
+ Suffix(ref e);
+ }
+ } else if (StartOf(13)) {
+ ConstAtomExpression(out e);
+ Suffix(ref e);
+ while (la.kind == 50 || la.kind == 52) {
+ Suffix(ref e);
+ }
} else SynErr(123);
}
@@ -1395,7 +1412,7 @@ List<Expression/*!*/>/*!*/ decreases) { decreases = new List<Expression/*!*/>();
mod = null;
- while (StartOf(13)) {
+ while (StartOf(14)) {
if (la.kind == 29 || la.kind == 59) {
isFree = false;
if (la.kind == 29) {
@@ -1498,7 +1515,7 @@ List<Expression/*!*/>/*!*/ decreases) { void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
- if (StartOf(14)) {
+ if (StartOf(15)) {
if (la.kind == 70 || la.kind == 71) {
AndOp();
x = t;
@@ -1546,12 +1563,12 @@ List<Expression/*!*/>/*!*/ decreases) { Term(out e0);
e = e0;
- if (StartOf(15)) {
+ if (StartOf(16)) {
RelOp(out x, out op);
firstOpTok = x;
Term(out e1);
e = new BinaryExpr(x, op, e0, e1);
- while (StartOf(15)) {
+ while (StartOf(16)) {
if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -1803,7 +1820,7 @@ List<Expression/*!*/>/*!*/ decreases) { e = new ITEExpr(x, e, e0, e1);
} else if (la.kind == 60) {
MatchExpression(out e);
- } else if (StartOf(16)) {
+ } else if (StartOf(17)) {
QuantifierGuts(out e);
} else if (la.kind == 38) {
ComprehensionExpr(out e);
@@ -2178,7 +2195,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(22);
Expect(1);
aName = t.val;
- if (StartOf(17)) {
+ if (StartOf(18)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 19) {
@@ -2214,6 +2231,7 @@ List<Expression/*!*/>/*!*/ decreases) { {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,T,x, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,T, x,x,x,x, x,x,T,x, x,x,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, T,x,x,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,T, x,x,x,x, x,T,T,x, x,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, T,x,x,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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},
@@ -2366,8 +2384,8 @@ public class Errors { case 119: s = "invalid IfStmt"; break;
case 120: s = "invalid IfStmt"; break;
case 121: s = "invalid WhileStmt"; break;
- case 122: s = "invalid Lhs"; break;
- case 123: s = "invalid Rhs"; break;
+ case 122: s = "invalid Rhs"; break;
+ case 123: s = "invalid Lhs"; break;
case 124: s = "invalid Guard"; break;
case 125: s = "invalid AttributeArg"; break;
case 126: s = "invalid EquivOp"; break;
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 9970d61a..e49ce6e9 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -424,7 +424,17 @@ namespace Microsoft.Dafny { }
} else if (stmt is ReturnStmt) {
- wr.Write("return;");
+ var s = (ReturnStmt) stmt;
+ wr.Write("return");
+ if (s.rhss != null) {
+ var sep = " ";
+ foreach (var rhs in s.rhss) {
+ wr.Write(sep);
+ PrintRhs(rhs);
+ sep = ", ";
+ }
+ }
+ wr.Write(";");
} else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index c0bf4392..24732dac 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1203,9 +1203,42 @@ namespace Microsoft.Dafny { } else if (stmt is ReturnStmt) {
if (specContextOnly && !method.IsGhost) {
+ // TODO: investigate. This error message is suspicious. It seems that a return statement is only
+ // disallowed from a ghost if or while in a non-ghost method, which is not what this says.
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)");
}
-
+ ReturnStmt s = (ReturnStmt) stmt;
+ if (s.rhss != null) {
+ if (method.Outs.Count != s.rhss.Count)
+ Error(s, "number of return parameters does not match declaration (found {0}, expected {1})", s.rhss.Count, method.Outs.Count);
+ else {
+ Contract.Assert(s.rhss.Count > 0);
+ // Create a hidden update statement using the out-parameter formals, resolve the RHS, and check that the RHS is good.
+ List<Expression> formals = new List<Expression>();
+ int i = 0;
+ foreach (Formal f in method.Outs) {
+ IdentifierExpr ident = new IdentifierExpr(f.tok, f.Name);
+ ident.Var = f;
+ ident.Type = ident.Var.Type;
+ Contract.Assert(f.Type != null);
+ formals.Add(ident);
+ // link the reciever parameter properly:
+ if (s.rhss[i] is TypeRhs) {
+ var r = (TypeRhs)s.rhss[i];
+ if (r.InitCall != null) {
+ r.InitCall.Receiver = ident;
+ }
+ }
+ i++;
+ }
+ s.hiddenUpdate = new UpdateStmt(s.Tok, formals, s.rhss, true);
+ ResolveStatement(s.hiddenUpdate, specContextOnly, method);
+ // resolving the update statement will check for return statement specifics.
+ }
+ }
+ else {// this is a regular return statement.
+ s.hiddenUpdate = null;
+ }
} else if (stmt is UpdateStmt) {
var s = (UpdateStmt)stmt;
int prevErrorCount = ErrorCount;
@@ -1224,6 +1257,7 @@ namespace Microsoft.Dafny { }
IToken firstEffectfulRhs = null;
CallRhs callRhs = null;
+ // Resolve RHSs
foreach (var rhs in s.Rhss) {
bool isEffectful;
if (rhs is TypeRhs) {
@@ -1281,29 +1315,50 @@ namespace Microsoft.Dafny { }
}
} else {
- // if there was an effectful RHS, that must be the only RHS
- if (s.Rhss.Count != 1) {
- Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");
- } else if (arrayRangeLhs != null) {
- Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");
- } else if (callRhs == null) {
- // must be a single TypeRhs
- if (s.Lhss.Count != 1) {
- Contract.Assert(2 <= s.Lhss.Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)
- Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);
- } else if (ErrorCount == prevErrorCount) {
- var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, s.Rhss[0]);
- s.ResolvedStatements.Add(a);
+ if (s.secretlyReturnStatment) {
+ if (1 < s.Rhss.Count)
+ Error(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");
+ else { // it might be ok, if it is a TypeExpr
+ Contract.Assert(s.Rhss.Count == 1);
+ if (callRhs != null) {
+ Error(callRhs.Tok, "cannot have method call in return statement.");
+ }
+ else {
+ // we have a TypeExpr
+ Contract.Assert(s.Rhss[0] is TypeRhs);
+ var tr = (TypeRhs)s.Rhss[0];
+ Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call.
+ if (tr.CanAffectPreviouslyKnownExpressions) {
+ Error(tr.Tok, "can only have initialization methods which modify at most 'this'.");
+ }
+ }
}
- } else {
- // a call statement
- if (ErrorCount == prevErrorCount) {
- var resolvedLhss = new List<Expression>();
- foreach (var ll in s.Lhss) {
- resolvedLhss.Add(ll.Resolved);
+ }
+ else {
+ // if there was an effectful RHS, that must be the only RHS
+ if (s.Rhss.Count != 1) {
+ Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");
+ } else if (arrayRangeLhs != null) {
+ Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");
+ } else if (callRhs == null) {
+ // must be a single TypeRhs
+ if (s.Lhss.Count != 1) {
+ Contract.Assert(2 <= s.Lhss.Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)
+ Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, s.Rhss.Count);
+ } else if (ErrorCount == prevErrorCount) {
+ var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, s.Rhss[0]);
+ s.ResolvedStatements.Add(a);
+ }
+ } else {
+ // a call statement
+ if (ErrorCount == prevErrorCount) {
+ var resolvedLhss = new List<Expression>();
+ foreach (var ll in s.Lhss) {
+ resolvedLhss.Add(ll.Resolved);
+ }
+ var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);
+ s.ResolvedStatements.Add(a);
}
- var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);
- s.ResolvedStatements.Add(a);
}
}
}
@@ -1311,7 +1366,7 @@ namespace Microsoft.Dafny { foreach (var a in s.ResolvedStatements) {
ResolveStatement(a, specContextOnly, method);
}
-
+ // end of UpdateStmt
} else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
foreach (var vd in s.Lhss) {
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index b2c46c8a..e16470c3 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3036,7 +3036,11 @@ namespace Microsoft.Dafny { var s = (BreakStmt)stmt;
builder.Add(new GotoCmd(s.Tok, new StringSeq("after_" + s.TargetStmt.Labels.UniqueId)));
} else if (stmt is ReturnStmt) {
+ var s = (ReturnStmt)stmt;
AddComment(builder, stmt, "return statement");
+ if (s.hiddenUpdate != null) {
+ TrStmt(s.hiddenUpdate, builder, locals, etran);
+ }
builder.Add(new Bpl.ReturnCmd(stmt.Tok));
} else if (stmt is UpdateStmt) {
var s = (UpdateStmt)stmt;
|