From c4eb22c363b65823fbb38ab618df3c28ffa59bbd Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 12 May 2011 18:01:59 -0700 Subject: Dafny: fixed bugs in resolution of multi-dimensional arrays --- Source/Dafny/Dafny.atg | 2 + Source/Dafny/Parser.cs | 51 ++++++++++++------------ Source/Dafny/Resolver.cs | 4 +- Source/Dafny/Scanner.cs | 102 +++++++++++++++++++++++------------------------ 4 files changed, 78 insertions(+), 81 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 23582495..8e999553 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1312,6 +1312,8 @@ SelectOrCallSuffix ) (. if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); + // make sure an array class with this dimensionality exists + UserDefinedType tmp = theBuiltIns.ArrayType(multipleIndices.Count, new IntType(), true); } else { if (!anyDots && e0 == null) { /* a parsing error occurred */ diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 180f15ab..db33283b 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; @@ -161,10 +161,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); } @@ -177,15 +177,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List theImports; @@ -2047,6 +2047,8 @@ List/*!*/ decreases) { } else SynErr(144); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); + // make sure an array class with this dimensionality exists + UserDefinedType tmp = theBuiltIns.ArrayType(multipleIndices.Count, new IntType(), true); } else { if (!anyDots && e0 == null) { /* a parsing error occurred */ @@ -2131,13 +2133,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,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, @@ -2164,20 +2166,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; @@ -2333,7 +2333,7 @@ public class Errors { default: s = "error " + n; break; } - return s; + return s; } public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors @@ -2341,9 +2341,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/Resolver.cs b/Source/Dafny/Resolver.cs index 972c82ab..00cabd1d 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -960,7 +960,7 @@ namespace Microsoft.Dafny { if (!UnifyTypes(iProxy.Arg, ((SeqType)t).Arg)) { return false; } - } else if (t.IsArrayType) { + } else if (t.IsArrayType && (t.AsArrayType).Dims == 1) { Type elType = UserDefinedType.ArrayElementType(t); if (!UnifyTypes(iProxy.Arg, elType)) { return false; @@ -1909,7 +1909,7 @@ namespace Microsoft.Dafny { Contract.Assert(e.Array.Type != null); // follows from postcondition of ResolveExpression Type elementType = new InferredTypeProxy(); if (!UnifyTypes(e.Array.Type, builtIns.ArrayType(e.Indices.Count, elementType))) { - Error(e.Array, "array selection requires an array (got {0})", e.Array.Type); + Error(e.Array, "array selection requires an array{0} (got {1})", e.Indices.Count, e.Array.Type); } int i = 0; foreach (Expression idx in e.Indices) { diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 817df6cd..0af254f3 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 = 107; - [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; @@ -294,9 +291,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; @@ -306,14 +303,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); @@ -322,9 +320,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; @@ -345,11 +344,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; @@ -360,7 +359,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++; @@ -368,9 +367,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 @@ -420,7 +419,7 @@ public class Scanner { return; } - + } } @@ -559,13 +558,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: { @@ -773,14 +769,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); @@ -801,7 +797,7 @@ public class Scanner { } pt = pt.next; } while (pt.kind > maxT); // skip pragmas - + return pt; } -- cgit v1.2.3