diff options
author | 2011-06-29 16:21:35 -0700 | |
---|---|---|
committer | 2011-06-29 16:21:35 -0700 | |
commit | 3bb828b02a76167cc8aa25284663f1524e2b929b (patch) | |
tree | ea1379a5f9c4737379c46219ca054ccbdaea3f04 | |
parent | b043af23c8ea53af582b0d59f557c150c0cfc1e6 (diff) |
Initial implementation of return statments with parameters.
-rw-r--r-- | Source/Dafny/Compiler.cs | 2 | ||||
-rw-r--r-- | Source/Dafny/Dafny.atg | 19 | ||||
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 20 | ||||
-rw-r--r-- | Source/Dafny/Parser.cs | 70 | ||||
-rw-r--r-- | Source/Dafny/Resolver.cs | 34 | ||||
-rw-r--r-- | Source/Dafny/Translator.cs | 4 |
6 files changed, 118 insertions, 31 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 35f81605..1f9208db 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -641,7 +641,9 @@ namespace Microsoft.Dafny { Indent(indent);
wr.WriteLine("goto after_{0};", s.TargetStmt.Labels.UniqueId);
} else if (stmt is ReturnStmt) {
+ var s = (ReturnStmt)stmt;
Indent(indent);
+ TrStmt(s.hiddenUpdate, indent);
wr.WriteLine("return;");
} else if (stmt is UpdateStmt) {
var s = (UpdateStmt)stmt;
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..7253e866 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;
}
}
@@ -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;
}
}
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/Resolver.cs b/Source/Dafny/Resolver.cs index c0bf4392..fe026335 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1203,9 +1203,41 @@ 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 {
+ // 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>();
+ 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);
+ }
+ s.hiddenUpdate = new UpdateStmt(s.Tok, formals, s.rhss, true);
+ int prevErrorCount = ErrorCount;
+ ResolveStatement(s.hiddenUpdate, specContextOnly, method);
+ if (ErrorCount != prevErrorCount) {
+ // success. but we still need to check the RHS is not bad.
+ foreach (AssignmentRhs rhs in s.hiddenUpdate.Rhss) {
+ if (rhs.CanAffectPreviouslyKnownExpressions) {
+ Error(rhs.Tok, "cannot have effectful parameter in return statement.");
+ break; // only report one error
+ }
+ }
+ } // else we have failure.
+ }
+ }
+ else {// this is a regular return statement.
+ s.hiddenUpdate = null;
+ }
} else if (stmt is UpdateStmt) {
var s = (UpdateStmt)stmt;
int prevErrorCount = ErrorCount;
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;
|