diff options
Diffstat (limited to 'Source/Core/scanner.frame')
| -rw-r--r-- | Source/Core/scanner.frame | 377 |
1 files changed, 377 insertions, 0 deletions
diff --git a/Source/Core/scanner.frame b/Source/Core/scanner.frame new file mode 100644 index 00000000..3753c6e9 --- /dev/null +++ b/Source/Core/scanner.frame @@ -0,0 +1,377 @@ +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 -->namespace {
+
+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)]
+-->declarations
+
+ 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();
+-->initialization
+ }
+
+ 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;
+ }
+ }
+ }
+
+-->comment
+
+ static void CheckLiteral() {
+ switch (t.val) {
+-->literals
+ }
+ }
+
+ public static Token/*!*/ Scan() {
+ while (ignore[ch]) { NextCh(); }
+-->scan1
+ 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
+-->scan2
+ }
+ 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
+$$$
|