Dafny: better error message when "decreases *" is attempted on a function or method

Dafny: fixed compilation bug with parallel assignment involving a ghost LHS
Dafny: added sequence-to-set conversion if a function's reads clause is used implicitly as the decreases clause

5 files changed, 152 insertions, 128 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index b2dda7de..35f81605 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -653,36 +653,25 @@ namespace Microsoft.Dafny {
           Contract.Assert(s.Lhss.Count == resolved.Count);

           Contract.Assert(s.Rhss.Count == resolved.Count);

           var lvalues = new List<string>();

-          int i = 0;

-          foreach (var lhs in s.Lhss) {

-            if (!resolved[i].IsGhost) {

-              lvalues.Add(CreateLvalue(lhs, indent));

-            }

-            i++;

-          }

-          int N = i;

           var rhss = new List<string>();

-          i = 0;

-          foreach (var rhs in s.Rhss) {

+          for (int i = 0; i < resolved.Count; i++) {

             if (!resolved[i].IsGhost) {

-              if (rhs is HavocRhs) {

-                rhss.Add(null);

-              } else {

+              var lhs = s.Lhss[i];

+              var rhs = s.Rhss[i];

+              if (!(rhs is HavocRhs)) {

+                lvalues.Add(CreateLvalue(lhs, indent));

+

                 string target = "_rhs" + tmpVarCount;

                 tmpVarCount++;

                 rhss.Add(target);

                 TrRhs("var " + target, null, rhs, indent);

               }

             }

-            i++;

           }

-          Contract.Assert(lvalues.Count == N);

-          Contract.Assert(rhss.Count == N);

-          for (i = 0; i < N; i++) {

-            if (rhss[i] != null) {

-              Indent(indent);

-              wr.WriteLine("{0} = {1};", lvalues[i], rhss[i]);

-            }

+          Contract.Assert(lvalues.Count == rhss.Count);

+          for (int i = 0; i < lvalues.Count; i++) {

+            Indent(indent);

+            wr.WriteLine("{0} = {1};", lvalues[i], rhss[i]);

           }

         }

 

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 10314038..071dbd64 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -472,7 +472,7 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
     ( "requires" Expression<out e> ";"                       (. req.Add(new MaybeFreeExpression(e, isFree)); .)

     | "ensures" Expression<out e> ";"                        (. ens.Add(new MaybeFreeExpression(e, isFree)); .)

     )

-  | "decreases" Expressions<decreases> ";"

+  | "decreases" DecreasesList<decreases, false> ";"

   )

   .

 

@@ -608,7 +608,7 @@ FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ r
               }

 	        ] ";"

   | "ensures" Expression<out e> ";"      (. ens.Add(e); .)

-  | "decreases" Expressions<decreases> ";"

+  | "decreases" DecreasesList<decreases, false> ";"

   )

   .

 

@@ -866,17 +866,30 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
      invariants = new List<MaybeFreeExpression/*!*/>();

      decreases = new List<Expression/*!*/>();

   .)

-  {                          (. isFree = false; .)

-     [ "free"                (. isFree = true; .)

-     ]

-     "invariant"

-     Expression<out e>       (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)

-     ";"

-   | "decreases"

-     PossiblyWildExpression<out e>          (. decreases.Add(e); .)

-     { "," PossiblyWildExpression<out e>    (. decreases.Add(e); .)

-     }

-     ";"

+  {                         (. isFree = false; .)

+    [ "free"                (. isFree = true; .)

+    ]

+    "invariant"

+    Expression<out e>       (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)

+    ";"

+  | "decreases" DecreasesList<decreases, true> ";"

+  }

+  .

+

+DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>

+= (. Expression/*!*/ e; .)

+  PossiblyWildExpression<out e>          (. if (!allowWildcard && e is WildcardExpr) {

+                                              SemErr(e.tok, "'decreases *' is only allowed on loops");

+                                            } else {

+                                              decreases.Add(e);

+                                            }

+                                         .)

+  { "," PossiblyWildExpression<out e>    (. if (!allowWildcard && e is WildcardExpr) {

+                                              SemErr(e.tok, "'decreases *' is only allowed on loops");

+                                            } else {

+                                              decreases.Add(e);

+                                            }

+                                         .)

   }

   .

 

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index c3648310..41fc89c5 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;

 

@@ -144,10 +144,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (errDist >= 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);

 	}

 

@@ -160,15 +160,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			la = t;

 		}

 	}

-

+	

 	void Expect (int n) {

 		if (la.kind==n) Get(); else { SynErr(n); }

 	}

-

+	

 	bool StartOf (int s) {

 		return set[s, la.kind];

 	}

-

+	

 	void ExpectWeak (int n, int follow) {

 		if (la.kind == n) Get();

 		else {

@@ -192,7 +192,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}

 	}

 

-

+	

 	void Dafny() {

 		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;

 		Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;

@@ -788,7 +788,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			} else SynErr(110);

 		} else if (la.kind == 32) {

 			Get();

-			Expressions(decreases);

+			DecreasesList(decreases, false);

 			Expect(17);

 		} else SynErr(111);

 	}

@@ -818,14 +818,24 @@ List<Expression/*!*/>/*!*/ decreases) {
 		fe = new FrameExpression(e, fieldName); 

 	}

 

-	void Expressions(List<Expression/*!*/>/*!*/ args) {

-		Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; 

-		Expression(out e);

-		args.Add(e); 

+	void DecreasesList(List<Expression/*!*/> decreases, bool allowWildcard) {

+		Expression/*!*/ e; 

+		PossiblyWildExpression(out e);

+		if (!allowWildcard && e is WildcardExpr) {

+		 SemErr(e.tok, "'decreases *' is only allowed on loops");

+		} else {

+		  decreases.Add(e);

+		}

+		

 		while (la.kind == 19) {

 			Get();

-			Expression(out e);

-			args.Add(e); 

+			PossiblyWildExpression(out e);

+			if (!allowWildcard && e is WildcardExpr) {

+			 SemErr(e.tok, "'decreases *' is only allowed on loops");

+			} else {

+			  decreases.Add(e);

+			}

+			

 		}

 	}

 

@@ -900,7 +910,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			ens.Add(e); 

 		} else if (la.kind == 32) {

 			Get();

-			Expressions(decreases);

+			DecreasesList(decreases, false);

 			Expect(17);

 		} else SynErr(113);

 	}

@@ -1333,6 +1343,17 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else SynErr(123);

 	}

 

+	void Expressions(List<Expression/*!*/>/*!*/ args) {

+		Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; 

+		Expression(out e);

+		args.Add(e); 

+		while (la.kind == 19) {

+			Get();

+			Expression(out e);

+			args.Add(e); 

+		}

+	}

+

 	void Guard(out Expression e) {

 		Expression/*!*/ ee;  e = null; 

 		Expect(33);

@@ -1385,13 +1406,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Expect(17);

 			} else {

 				Get();

-				PossiblyWildExpression(out e);

-				decreases.Add(e); 

-				while (la.kind == 19) {

-					Get();

-					PossiblyWildExpression(out e);

-					decreases.Add(e); 

-				}

+				DecreasesList(decreases, true);

 				Expect(17);

 			}

 		}

@@ -2164,13 +2179,13 @@ List<Expression/*!*/>/*!*/ 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,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,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},

@@ -2197,20 +2212,18 @@ List<Expression/*!*/>/*!*/ 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;

@@ -2362,7 +2375,7 @@ public class Errors {
 

 			default: s = "error " + n; break;

 		}

-		return s;

+    return s;

 	}

 

 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

@@ -2370,9 +2383,8 @@ 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/Scanner.cs b/Source/Dafny/Scanner.cs
index 81f556c8..19157a32 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,17 +31,15 @@ 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;

@@ -53,12 +51,12 @@ public class Buffer {
 

 		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;

@@ -75,14 +73,14 @@ public class Buffer {
 	}

 

 	~Buffer() { Close(); }

-

+	

 	protected void Close() {

 		if (!isUserStream && stream != null) {

 			stream.Close();

 			//stream = null;

 		}

 	}

-

+	

 	public virtual int Read () {

 		if (bufPos < bufLen) {

 			return buf[bufPos++];

@@ -102,7 +100,7 @@ public class Buffer {
 		Pos = curPos;

 		return ch;

 	}

-

+	

 	public string/*!*/ GetString (int beg, int end) {

 	  Contract.Ensures(Contract.Result<string>() != null);

 		int len = 0;

@@ -141,7 +139,7 @@ public class Buffer {
 			}

 		}

 	}

-

+	

 	// 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.

@@ -215,20 +213,19 @@ public class Scanner {
 	const int noSym = 104;

 

 

-	[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

@@ -239,13 +236,13 @@ public class Scanner {
 

 	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;

@@ -293,9 +290,9 @@ public class Scanner {
 		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;

@@ -305,14 +302,15 @@ public class Scanner {
 			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);

@@ -321,9 +319,10 @@ public class Scanner {
 		buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

 		this.Filename = fileName;

+		

 		Init();

 	}

-

+	

 	void Init() {

 		pos = -1; line = 1; col = 0;

 		oldEols = 0;

@@ -344,11 +343,11 @@ public class Scanner {
 	Contract.Ensures(Contract.Result<string>() != 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 +358,7 @@ public class Scanner {
 	}

 

 	void NextCh() {

-		if (oldEols > 0) { ch = EOL; oldEols--; }

+		if (oldEols > 0) { ch = EOL; oldEols--; } 

 		else {

 //			pos = buffer.Pos;

 //			ch = buffer.Read(); col++;

@@ -367,9 +366,9 @@ public class Scanner {
 //			// 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 +418,7 @@ public class Scanner {
 				return;

 			  }

 

-

+			

 		}

 

 	}

@@ -556,13 +555,10 @@ public class Scanner {
 		t.pos = pos; t.col = col; t.line = line;

 		t.filename = this.Filename;

 		int state;

-		if (start.ContainsKey(ch)) {

-			Contract.Assert(start[ch] != null);

-			state = (int) start[ch];

-		}

+		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }

 		else { state = 0; }

 		tlen = 0; AddCh();

-

+		

 		switch (state) {

 			case -1: { t.kind = eofSym; break; } // NextCh already done

 			case 0: {

@@ -768,14 +764,14 @@ public class Scanner {
 		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<Token>() != null);

@@ -796,7 +792,7 @@ public class Scanner {
 			}

 			pt = pt.next;

 		} while (pt.kind > maxT); // skip pragmas

-

+	

 		return pt;

 	}

 

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index f3c48ab2..dbe5f2ed 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2267,6 +2267,20 @@ namespace Microsoft.Dafny {
               singletons = new List<Expression>();

             }

             singletons.Add(e);

+          } else if (e.Type is SeqType) {

+            // e represents a sequence

+            // Add:  set x :: x in e

+            var bv = new BoundVar(e.tok, "_s2s_" + otherTmpVarCount, ((SeqType)e.Type).Arg);

+            otherTmpVarCount++;  // use this counter, but for a Dafny name (the idea being that the number and the initial "_" in the name might avoid name conflicts)

+            var bvIE = new IdentifierExpr(e.tok, bv.Name);

+            bvIE.Var = bv;  // resolve here

+            bvIE.Type = bv.Type;  // resolve here

+            var sInE = new BinaryExpr(e.tok, BinaryExpr.Opcode.In, bvIE, e);

+            sInE.ResolvedOp = BinaryExpr.ResolvedOpcode.InSeq;  // resolve here

+            sInE.Type = Type.Bool;  // resolve here

+            var s = new SetComprehension(e.tok, new List<BoundVar>() { bv }, sInE, bvIE);

+            s.Type = new SetType(new ObjectType());  // resolve here

+            sets.Add(s);

           } else {

             // e is already a set

             Contract.Assert(e.Type is SetType);