diff options
Diffstat (limited to 'Source/Core/Scanner.ssc')
| -rw-r--r-- | Source/Core/Scanner.ssc | 720 |
1 files changed, 720 insertions, 0 deletions
diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc new file mode 100644 index 00000000..eb0c8b04 --- /dev/null +++ b/Source/Core/Scanner.ssc @@ -0,0 +1,720 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using System.Text;
+using Microsoft.Contracts;
+
+
+namespace Microsoft.Boogie {
+
+ [Immutable]
+ public interface IToken {
+ int kind {get; set; } // token kind
+ string filename {get; set; } // token file
+ int pos {get; set; } // token position in the source text (starting at 0)
+ int col {get; set; } // token column (starting at 0)
+ int line {get; set; } // token line (starting at 1)
+ string/*!*/ val {get; set; } // token value
+
+ bool IsValid { get; }
+ }
+
+ [Immutable]
+ public class Token : IToken {
+ int _kind; // token kind
+ string _filename; // token file
+ int _pos; // token position in the source text (starting at 0)
+ int _col; // token column (starting at 0)
+ int _line; // token line (starting at 1)
+ string/*!*/ _val = "foo"; // token value
+
+ public static IToken! NoToken = new Token();
+
+ public Token();
+ public Token(int linenum, int colnum) {
+ this._line = linenum;
+ this._col = colnum;
+ base();
+ }
+
+ public int kind {
+ get { return this._kind; }
+ set { this._kind = value; }
+ }
+
+ public string filename{
+ get { return this._filename; }
+ set { this._filename = value; }
+ }
+
+ public int pos{
+ get { return this._pos; }
+ set { this._pos = value; }
+ }
+
+ public int col{
+ get { return this._col; }
+ set { this._col = value; }
+ }
+
+ public int line{
+ get { return this._line; }
+ set { this._line = value; }
+ }
+
+ public string/*!*/ val{
+ get { return this._val; }
+ set { this._val = value; }
+ }
+
+ public bool IsValid { get { return this._filename != null; } }
+ }
+
+}
+
+namespace BoogiePL {
+
+using Microsoft.Boogie;
+
+public class Buffer {
+ static string/*!*/ buf;
+ static int bufLen;
+ static int pos;
+ public const int eof = '\uffff';
+
+ public static void Fill(StreamReader! reader) {
+ List<string!> defines = new List<string!>();
+ Fill(reader, defines);
+ }
+
+ struct ReadState {
+ public bool hasSeenElse;
+ public bool mayStillIncludeAnotherAlternative;
+ public ReadState(bool hasSeenElse, bool mayStillIncludeAnotherAlternative) {
+ this.hasSeenElse = hasSeenElse;
+ this.mayStillIncludeAnotherAlternative = mayStillIncludeAnotherAlternative;
+ }
+ }
+
+ public static void Fill(StreamReader! reader, List<string!>! defines) {
+ StringBuilder sb = new StringBuilder();
+ List<ReadState>! readState = new List<ReadState>(); // readState.Count is the current nesting level of #if's
+ int ignoreCutoff = -1; // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n
+ while (true)
+ invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count;
+ {
+ string s = reader.ReadLine();
+ if (s == null) {
+ if (readState.Count != 0) {
+ sb.AppendLine("#MalformedInput: missing #endif");
+ }
+ break;
+ }
+ string t = s.Trim();
+ if (t.StartsWith("#if")) {
+ ReadState rs = new ReadState(false, false);
+ if (ignoreCutoff != -1) {
+ // we're already in a state of ignoring, so continue to ignore
+ } else if (IfdefConditionSaysToInclude(t.Substring(3).TrimStart(), defines)) {
+ // include this branch
+ } else {
+ ignoreCutoff = readState.Count; // start ignoring
+ rs.mayStillIncludeAnotherAlternative = true; // allow some later "elsif" or "else" branch to be included
+ }
+ readState.Add(rs);
+ sb.AppendLine(); // ignore the #if line
+
+ } else if (t.StartsWith("#elsif")) {
+ ReadState rs;
+ if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) {
+ sb.AppendLine("#MalformedInput: misplaced #elsif"); // malformed input
+ break;
+ }
+ if (ignoreCutoff == -1) {
+ // we had included the previous branch
+ assert !rs.mayStillIncludeAnotherAlternative;
+ ignoreCutoff = readState.Count-1; // start ignoring
+ } else if (rs.mayStillIncludeAnotherAlternative && IfdefConditionSaysToInclude(t.Substring(6).TrimStart(), defines)) {
+ // include this branch, but no subsequent branch at this level
+ ignoreCutoff = -1;
+ rs.mayStillIncludeAnotherAlternative = false;
+ readState[readState.Count-1] = rs;
+ }
+ sb.AppendLine(); // ignore the #elsif line
+
+ } else if (t == "#else") {
+ ReadState rs;
+ if (readState.Count == 0 || (rs = readState[readState.Count-1]).hasSeenElse) {
+ sb.AppendLine("#MalformedInput: misplaced #else"); // malformed input
+ break;
+ }
+ rs.hasSeenElse = true;
+ if (ignoreCutoff == -1) {
+ // we had included the previous branch
+ assert !rs.mayStillIncludeAnotherAlternative;
+ ignoreCutoff = readState.Count-1; // start ignoring
+ } else if (rs.mayStillIncludeAnotherAlternative) {
+ // include this branch
+ ignoreCutoff = -1;
+ rs.mayStillIncludeAnotherAlternative = false;
+ }
+ readState[readState.Count-1] = rs;
+ sb.AppendLine(); // ignore the #else line
+
+ } else if (t == "#endif") {
+ if (readState.Count == 0) {
+ sb.AppendLine("#MalformedInput: misplaced #endif"); // malformed input
+ break;
+ }
+ readState.RemoveAt(readState.Count-1); // pop
+ if (ignoreCutoff == readState.Count) {
+ // we had ignored the branch that ends here; so, now we start including again
+ ignoreCutoff = -1;
+ }
+ sb.AppendLine(); // ignore the #endif line
+
+ } else if (ignoreCutoff == -1) {
+ sb.AppendLine(s); // included line
+
+ } else {
+ sb.AppendLine(); // ignore the line
+ }
+ }
+
+ Fill(sb.ToString());
+ }
+
+ // "arg" is assumed to be trimmed
+ private static bool IfdefConditionSaysToInclude(string! arg, List<string!>! defines) {
+ bool sense = true;
+ while (arg.StartsWith("!")) {
+ sense = !sense;
+ arg = arg.Substring(1).TrimStart();
+ }
+ return defines.Contains(arg) == sense;
+ }
+
+ public static void Fill(string! text) {
+ buf = text;
+ bufLen = buf.Length;
+ pos = 0;
+ }
+
+ public static int Read() {
+ if (pos < bufLen) {
+ return buf[pos++];
+ } else {
+ return eof;
+ }
+ }
+
+ public static string/*!*/ ReadToEOL() {
+ int x = buf.IndexOf('\n', pos);
+ if (x == -1) {
+ string s = buf.Substring(pos);
+ pos = buf.Length;
+ return s;
+ } else {
+ string s = buf.Substring(pos, x+1 - pos); // also include the '\n'
+ pos = x+1;
+ return s;
+ }
+ }
+
+ public static int Pos {
+ get { return pos; }
+ set {
+ if (value < 0) pos = 0; else if (value >= bufLen) pos = bufLen; else pos = value;
+ }
+ }
+}
+
+
+
+public class Scanner {
+ const char EOF = '\0';
+ const char CR = '\r';
+ const char LF = '\n';
+ [Microsoft.Contracts.Verify(false)]
+ static Scanner() {
+ start[0] = 57;
+ start[33] = 41;
+ start[34] = 6;
+ start[35] = 2;
+ start[36] = 2;
+ start[37] = 51;
+ start[38] = 34;
+ start[39] = 2;
+ start[40] = 11;
+ start[41] = 12;
+ start[42] = 24;
+ start[43] = 47;
+ start[44] = 14;
+ start[45] = 49;
+ start[46] = 2;
+ start[47] = 50;
+ start[48] = 9;
+ start[49] = 9;
+ start[50] = 9;
+ start[51] = 9;
+ start[52] = 9;
+ start[53] = 9;
+ start[54] = 9;
+ start[55] = 9;
+ start[56] = 9;
+ start[57] = 9;
+ start[58] = 13;
+ start[59] = 10;
+ start[60] = 17;
+ start[61] = 21;
+ start[62] = 18;
+ start[63] = 2;
+ start[65] = 2;
+ start[66] = 2;
+ start[67] = 2;
+ start[68] = 2;
+ start[69] = 2;
+ start[70] = 2;
+ start[71] = 2;
+ start[72] = 2;
+ start[73] = 2;
+ start[74] = 2;
+ start[75] = 2;
+ start[76] = 2;
+ start[77] = 2;
+ start[78] = 2;
+ start[79] = 2;
+ start[80] = 2;
+ start[81] = 2;
+ start[82] = 2;
+ start[83] = 2;
+ start[84] = 2;
+ start[85] = 2;
+ start[86] = 2;
+ start[87] = 2;
+ start[88] = 2;
+ start[89] = 2;
+ start[90] = 2;
+ start[91] = 15;
+ start[92] = 1;
+ start[93] = 16;
+ start[94] = 2;
+ start[95] = 2;
+ start[96] = 2;
+ start[97] = 2;
+ start[98] = 2;
+ start[99] = 2;
+ start[100] = 2;
+ start[101] = 2;
+ start[102] = 2;
+ start[103] = 2;
+ start[104] = 2;
+ start[105] = 2;
+ start[106] = 2;
+ start[107] = 2;
+ start[108] = 2;
+ start[109] = 2;
+ start[110] = 2;
+ start[111] = 2;
+ start[112] = 2;
+ start[113] = 2;
+ start[114] = 2;
+ start[115] = 2;
+ start[116] = 2;
+ start[117] = 2;
+ start[118] = 2;
+ start[119] = 2;
+ start[120] = 2;
+ start[121] = 2;
+ start[122] = 2;
+ start[123] = 19;
+ start[124] = 37;
+ start[125] = 20;
+ start[126] = 2;
+ start[172] = 52;
+ start[8226] = 56;
+ start[8656] = 33;
+ start[8658] = 32;
+ start[8660] = 29;
+ start[8704] = 53;
+ start[8707] = 54;
+ start[8743] = 36;
+ start[8744] = 39;
+ start[8800] = 44;
+ start[8804] = 45;
+ start[8805] = 46;
+ }
+ const int noSym = 85;
+ static short[] start = new short[16385];
+
+
+ static Token/*!*/ t; // current token
+ static char ch; // current input character
+ static int pos; // column number of current character
+ static int line; // line number of current character
+ static int lineStart; // start position of current line
+ static Queue! oldEols; // EOLs that appeared in a comment;
+ static BitArray/*!*/ ignore; // set of characters to be ignored by the scanner
+ static string Filename;
+
+ ///<summary>
+ ///Initializes the scanner. Note: first fill the Buffer.
+ ///</summary>
+ ///<param name="filename">File name used for error reporting</param>
+ public static void Init (string filename) {
+ Filename = filename;
+ pos = -1; line = 1; lineStart = 0;
+ oldEols = new Queue();
+ NextCh();
+ ignore = new BitArray(16384);
+ ignore[9] = true; ignore[10] = true; ignore[13] = true; ignore[32] = true;
+
+ }
+
+ private static void NextCh() {
+ if (oldEols.Count > 0) {
+ ch = (char) ((!)oldEols.Dequeue());
+ } else {
+ while (true) {
+ ch = (char)Buffer.Read(); pos++;
+ if (ch == Buffer.eof) {
+ ch = EOF;
+ } else if (ch == LF) {
+ line++;
+ lineStart = pos + 1;
+
+ } else if (ch == '#' && pos == lineStart) {
+ int prLine = line;
+ int prColumn = pos - lineStart; // which is 0
+
+ string hashLine = Buffer.ReadToEOL(); pos += hashLine.Length;
+ line++;
+ lineStart = pos + 1;
+
+ hashLine = hashLine.TrimEnd(null);
+ if (hashLine.StartsWith("line ") || hashLine == "line") {
+ // parse #line pragma: #line num [filename]
+ string h = hashLine.Substring(4).TrimStart(null);
+ int x = h.IndexOf(' ');
+ if (x == -1) {
+ x = h.Length; // this will be convenient below when we look for a filename
+ }
+ try {
+ int li = int.Parse(h.Substring(0, x));
+
+ h = h.Substring(x).Trim();
+
+ // act on #line
+ line = li;
+ if (h.Length != 0) {
+ // a filename was specified
+ Filename = h;
+ }
+ continue; // successfully parsed and acted on the #line pragma
+
+ } catch (FormatException) {
+ // just fall down through to produce an error message
+ }
+ Errors.SemErr(Filename, prLine, prColumn, "Malformed (#line num [filename]) pragma: #" + hashLine);
+ continue;
+ }
+
+ Errors.SemErr(Filename, prLine, prColumn, "Unrecognized pragma: #" + hashLine);
+ continue;
+ }
+ return;
+ }
+ }
+ }
+
+
+ static bool Comment0() {
+ int level = 1, line0 = line, lineStart0 = lineStart;
+ NextCh();
+ if (ch == '/') {
+ NextCh();
+ for(;;) {
+ if (ch == 10) {
+ level--;
+ if (level == 0) {
+ while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;}
+ NextCh(); return true;
+ }
+ NextCh();
+ } else if (ch == EOF) return false;
+ else NextCh();
+ }
+ } else {
+ if (ch==CR) {line--; lineStart = lineStart0;}
+ pos = pos - 2; Buffer.Pos = pos+1; NextCh();
+ }
+ return false;
+ }
+
+ static bool Comment1() {
+ int level = 1, line0 = line, lineStart0 = lineStart;
+ NextCh();
+ if (ch == '*') {
+ NextCh();
+ for(;;) {
+ if (ch == '*') {
+ NextCh();
+ if (ch == '/') {
+ level--;
+ if (level == 0) {
+ while(line0 < line) {oldEols.Enqueue('\r'); oldEols.Enqueue('\n'); line0++;}
+ NextCh(); return true;
+ }
+ NextCh();
+ }
+ } else if (ch == '/') {
+ NextCh();
+ if (ch == '*') {
+ level++; NextCh();
+ }
+ } else if (ch == EOF) return false;
+ else NextCh();
+ }
+ } else {
+ if (ch==CR) {line--; lineStart = lineStart0;}
+ pos = pos - 2; Buffer.Pos = pos+1; NextCh();
+ }
+ return false;
+ }
+
+
+ static void CheckLiteral() {
+ switch (t.val) {
+ case "var": t.kind = 6; break;
+ case "where": t.kind = 12; break;
+ case "int": t.kind = 13; break;
+ case "bool": t.kind = 14; break;
+ case "const": t.kind = 19; break;
+ case "unique": t.kind = 20; break;
+ case "extends": t.kind = 21; break;
+ case "complete": t.kind = 22; break;
+ case "function": t.kind = 23; break;
+ case "returns": t.kind = 24; break;
+ case "axiom": t.kind = 27; break;
+ case "type": t.kind = 28; break;
+ case "procedure": t.kind = 30; break;
+ case "implementation": t.kind = 31; break;
+ case "modifies": t.kind = 32; break;
+ case "free": t.kind = 33; break;
+ case "requires": t.kind = 34; break;
+ case "ensures": t.kind = 35; break;
+ case "goto": t.kind = 38; break;
+ case "return": t.kind = 39; break;
+ case "if": t.kind = 40; break;
+ case "else": t.kind = 41; break;
+ case "while": t.kind = 42; break;
+ case "invariant": t.kind = 43; break;
+ case "break": t.kind = 45; break;
+ case "assert": t.kind = 46; break;
+ case "assume": t.kind = 47; break;
+ case "havoc": t.kind = 48; break;
+ case "call": t.kind = 50; break;
+ case "forall": t.kind = 51; break;
+ case "false": t.kind = 77; break;
+ case "true": t.kind = 78; break;
+ case "old": t.kind = 79; break;
+ case "exists": t.kind = 81; break;
+ default: break;
+
+ }
+ }
+
+ public static Token/*!*/ Scan() {
+ while (ignore[ch]) { NextCh(); }
+ if (ch == '/' && Comment0() || ch == '/' && Comment1() ) return Scan();
+ t = new Token();
+ t.pos = pos; t.col = pos - lineStart + 1; t.line = line; t.filename = Filename;
+ int state = (/*^ (!) ^*/ start)[ch];
+ StringBuilder buf = new StringBuilder(16);
+ buf.Append(ch); NextCh();
+
+ switch (state) {
+ case 0: {t.kind = noSym; goto done;} // NextCh already done
+ case 1:
+ if ((ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~')) {buf.Append(ch); NextCh(); goto case 2;}
+ else {t.kind = noSym; goto done;}
+ case 2:
+ if ((ch >= '#' && ch <= '$' || ch == 39 || ch == '.' || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch >= '^' && ch <= 'z' || ch == '~')) {buf.Append(ch); NextCh(); goto case 2;}
+ else {t.kind = 1; t.val = buf.ToString(); CheckLiteral(); return t;}
+ case 3:
+ if (ch == 'v') {buf.Append(ch); NextCh(); goto case 4;}
+ else {t.kind = noSym; goto done;}
+ case 4:
+ if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 5;}
+ else {t.kind = noSym; goto done;}
+ case 5:
+ if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 5;}
+ else {t.kind = 2; goto done;}
+ case 6:
+ if ((ch == '"')) {buf.Append(ch); NextCh(); goto case 7;}
+ else if ((ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~')) {buf.Append(ch); NextCh(); goto case 6;}
+ else {t.kind = noSym; goto done;}
+ case 7:
+ {t.kind = 4; goto done;}
+ case 8:
+ if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 8;}
+ else {t.kind = 5; goto done;}
+ case 9:
+ if ((ch >= '0' && ch <= '9')) {buf.Append(ch); NextCh(); goto case 9;}
+ else if (ch == 'b') {buf.Append(ch); NextCh(); goto case 3;}
+ else if (ch == '.') {buf.Append(ch); NextCh(); goto case 8;}
+ else {t.kind = 3; goto done;}
+ case 10:
+ {t.kind = 7; goto done;}
+ case 11:
+ {t.kind = 8; goto done;}
+ case 12:
+ {t.kind = 9; goto done;}
+ case 13:
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 25;}
+ else if (ch == ':') {buf.Append(ch); NextCh(); goto case 55;}
+ else {t.kind = 10; goto done;}
+ case 14:
+ {t.kind = 11; goto done;}
+ case 15:
+ {t.kind = 15; goto done;}
+ case 16:
+ {t.kind = 16; goto done;}
+ case 17:
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 26;}
+ else if (ch == ':') {buf.Append(ch); NextCh(); goto case 43;}
+ else {t.kind = 17; goto done;}
+ case 18:
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 40;}
+ else {t.kind = 18; goto done;}
+ case 19:
+ if (ch == '{') {buf.Append(ch); NextCh(); goto case 22;}
+ else {t.kind = 25; goto done;}
+ case 20:
+ if (ch == '}') {buf.Append(ch); NextCh(); goto case 23;}
+ else {t.kind = 26; goto done;}
+ case 21:
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 30;}
+ else {t.kind = 29; goto done;}
+ case 22:
+ {t.kind = 36; goto done;}
+ case 23:
+ {t.kind = 37; goto done;}
+ case 24:
+ {t.kind = 44; goto done;}
+ case 25:
+ {t.kind = 49; goto done;}
+ case 26:
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 27;}
+ else {t.kind = 63; goto done;}
+ case 27:
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 28;}
+ else {t.kind = 56; goto done;}
+ case 28:
+ {t.kind = 52; goto done;}
+ case 29:
+ {t.kind = 53; goto done;}
+ case 30:
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 31;}
+ else {t.kind = 62; goto done;}
+ case 31:
+ {t.kind = 54; goto done;}
+ case 32:
+ {t.kind = 55; goto done;}
+ case 33:
+ {t.kind = 57; goto done;}
+ case 34:
+ if (ch == '&') {buf.Append(ch); NextCh(); goto case 35;}
+ else {t.kind = noSym; goto done;}
+ case 35:
+ {t.kind = 58; goto done;}
+ case 36:
+ {t.kind = 59; goto done;}
+ case 37:
+ if (ch == '|') {buf.Append(ch); NextCh(); goto case 38;}
+ else {t.kind = noSym; goto done;}
+ case 38:
+ {t.kind = 60; goto done;}
+ case 39:
+ {t.kind = 61; goto done;}
+ case 40:
+ {t.kind = 64; goto done;}
+ case 41:
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 42;}
+ else {t.kind = 75; goto done;}
+ case 42:
+ {t.kind = 65; goto done;}
+ case 43:
+ {t.kind = 66; goto done;}
+ case 44:
+ {t.kind = 67; goto done;}
+ case 45:
+ {t.kind = 68; goto done;}
+ case 46:
+ {t.kind = 69; goto done;}
+ case 47:
+ if (ch == '+') {buf.Append(ch); NextCh(); goto case 48;}
+ else {t.kind = 71; goto done;}
+ case 48:
+ {t.kind = 70; goto done;}
+ case 49:
+ {t.kind = 72; goto done;}
+ case 50:
+ {t.kind = 73; goto done;}
+ case 51:
+ {t.kind = 74; goto done;}
+ case 52:
+ {t.kind = 76; goto done;}
+ case 53:
+ {t.kind = 80; goto done;}
+ case 54:
+ {t.kind = 82; goto done;}
+ case 55:
+ {t.kind = 83; goto done;}
+ case 56:
+ {t.kind = 84; goto done;}
+ case 57: {t.kind = 0; goto done;}
+ }
+ done:
+ t.val = buf.ToString();
+ return t;
+ }
+
+} // end Scanner
+
+
+public delegate void ErrorProc(int n, string filename, int line, int col);
+
+public class Errors {
+ public static int count = 0; // number of errors detected
+ public static ErrorProc/*!*/ SynErr; // syntactic errors
+
+ public static void SemErr(string filename, int line, int col, string! msg) { // semantic errors
+ ConsoleColor color = Console.ForegroundColor;
+ Console.ForegroundColor = ConsoleColor.Red;
+ Console.WriteLine("{0}({1},{2}): Error: {3}", filename, line, col, msg);
+ Console.ForegroundColor = color;
+ count++;
+ }
+
+ public static void SemErr(IToken! tok, string! msg) { // semantic errors
+ SemErr(tok.filename, tok.line, tok.col, msg);
+ }
+
+ public static void Exception (string s) {
+ ConsoleColor color = Console.ForegroundColor;
+ Console.ForegroundColor = ConsoleColor.Red;
+ Console.WriteLine(s);
+ Console.ForegroundColor = color;
+ System.Environment.Exit(0);
+ }
+
+} // Errors
+
+} // end namespace
|