Initial implementation of return statments with parameters.

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;