From 1a685684d1a1e18bd0c57d15b023bd6584442fb4 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 20 Jun 2011 19:49:35 -0700 Subject: 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 --- Source/Dafny/Compiler.cs | 31 +++++--------- Source/Dafny/Dafny.atg | 39 +++++++++++------ Source/Dafny/Parser.cs | 94 +++++++++++++++++++++++------------------ Source/Dafny/Scanner.cs | 102 ++++++++++++++++++++++----------------------- Source/Dafny/Translator.cs | 14 +++++++ 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(); - 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(); - 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/*!*/ req, List/ ( "requires" Expression ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .) | "ensures" Expression ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .) ) - | "decreases" Expressions ";" + | "decreases" DecreasesList ";" ) . @@ -608,7 +608,7 @@ FunctionSpec<.List/*!*/ reqs, List/*!*/ r } ] ";" | "ensures" Expression ";" (. ens.Add(e); .) - | "decreases" Expressions ";" + | "decreases" DecreasesList ";" ) . @@ -866,17 +866,30 @@ LoopSpec<.out List invariants, out List(); decreases = new List(); .) - { (. isFree = false; .) - [ "free" (. isFree = true; .) - ] - "invariant" - Expression (. invariants.Add(new MaybeFreeExpression(e, isFree)); .) - ";" - | "decreases" - PossiblyWildExpression (. decreases.Add(e); .) - { "," PossiblyWildExpression (. decreases.Add(e); .) - } - ";" + { (. isFree = false; .) + [ "free" (. isFree = true; .) + ] + "invariant" + Expression (. invariants.Add(new MaybeFreeExpression(e, isFree)); .) + ";" + | "decreases" DecreasesList ";" + } + . + +DecreasesList<.List decreases, bool allowWildcard.> += (. Expression/*!*/ e; .) + PossiblyWildExpression (. if (!allowWildcard && e is WildcardExpr) { + SemErr(e.tok, "'decreases *' is only allowed on loops"); + } else { + decreases.Add(e); + } + .) + { "," PossiblyWildExpression (. 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= 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 theImports; @@ -788,7 +788,7 @@ List/*!*/ 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/*!*/ decreases) { fe = new FrameExpression(e, fieldName); } - void Expressions(List/*!*/ args) { - Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; - Expression(out e); - args.Add(e); + void DecreasesList(List 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/*!*/ 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/*!*/ decreases) { } else SynErr(123); } + void Expressions(List/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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() != 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() != 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() != 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(); } 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() { 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); -- cgit v1.2.3