diff options
Diffstat (limited to 'Source/ParserHelper/ParserHelper.cs')
-rw-r--r-- | Source/ParserHelper/ParserHelper.cs | 486 |
1 files changed, 243 insertions, 243 deletions
diff --git a/Source/ParserHelper/ParserHelper.cs b/Source/ParserHelper/ParserHelper.cs index 111b836b..81644b7f 100644 --- a/Source/ParserHelper/ParserHelper.cs +++ b/Source/ParserHelper/ParserHelper.cs @@ -1,244 +1,244 @@ -using System.Text;
-using System.Collections.Generic;
-using System.IO;
-using System.Diagnostics.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 {
- public int _kind; // token kind
- string _filename; // token file
- public int _pos; // token position in the source text (starting at 0)
- public int _col; // token column (starting at 1)
- public int _line; // token line (starting at 1)
- public string/*!*/ _val; // token value
- public Token next; // ML 2005-03-11 Tokens are kept in linked list
-
- public static readonly IToken/*!*/ NoToken = new Token();
-
- public Token() {
- this._val = "anything so that it is nonnull";
- }
- public Token(int linenum, int colnum)
- : base() {
- this._line = linenum;
- this._col = colnum;
- this._val = "anything so that it is nonnull";
- }
-
- 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;
- }
- }
-
-
- }
-
- public static class ParserHelper {
- struct ReadState {
- public bool hasSeenElse;
- public bool mayStillIncludeAnotherAlternative;
- public ReadState(bool hasSeenElse, bool mayStillIncludeAnotherAlternative) {
- this.hasSeenElse = hasSeenElse;
- this.mayStillIncludeAnotherAlternative = mayStillIncludeAnotherAlternative;
- }
- }
- // "arg" is assumed to be trimmed
- private static bool IfdefConditionSaysToInclude(string arg, List<string/*!*/>/*!*/ defines) {
- Contract.Requires(arg != null);
- Contract.Requires(cce.NonNullElements(defines));
- bool sense = true;
- while (arg.StartsWith("!")) {
- sense = !sense;
- arg = arg.Substring(1).TrimStart();
- }
- return defines.Contains(arg) == sense;
- }
-
- public static string Fill(Stream stream, List<string/*!*/>/*!*/ defines) {
- Contract.Requires(stream != null);
- Contract.Requires(cce.NonNullElements(defines));
- Contract.Ensures(Contract.Result<string>() != null);
- StreamReader/*!*/ reader = new StreamReader(stream);
- return Fill(reader, defines);
- }
- public static string Fill(TextReader reader, List<string/*!*/>/*!*/ defines) {
- Contract.Requires(reader != null);
- Contract.Requires(cce.NonNullElements(defines));
- Contract.Ensures(Contract.Result<string>() != null);
- 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
- //Contract.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
- //Contract.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
- }
- }
-
- return sb.ToString();
- }
- }
+using System.Text; +using System.Collections.Generic; +using System.IO; +using System.Diagnostics.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 { + public int _kind; // token kind + string _filename; // token file + public int _pos; // token position in the source text (starting at 0) + public int _col; // token column (starting at 1) + public int _line; // token line (starting at 1) + public string/*!*/ _val; // token value + public Token next; // ML 2005-03-11 Tokens are kept in linked list + + public static readonly IToken/*!*/ NoToken = new Token(); + + public Token() { + this._val = "anything so that it is nonnull"; + } + public Token(int linenum, int colnum) + : base() { + this._line = linenum; + this._col = colnum; + this._val = "anything so that it is nonnull"; + } + + 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; + } + } + + + } + + public static class ParserHelper { + struct ReadState { + public bool hasSeenElse; + public bool mayStillIncludeAnotherAlternative; + public ReadState(bool hasSeenElse, bool mayStillIncludeAnotherAlternative) { + this.hasSeenElse = hasSeenElse; + this.mayStillIncludeAnotherAlternative = mayStillIncludeAnotherAlternative; + } + } + // "arg" is assumed to be trimmed + private static bool IfdefConditionSaysToInclude(string arg, List<string/*!*/>/*!*/ defines) { + Contract.Requires(arg != null); + Contract.Requires(cce.NonNullElements(defines)); + bool sense = true; + while (arg.StartsWith("!")) { + sense = !sense; + arg = arg.Substring(1).TrimStart(); + } + return defines.Contains(arg) == sense; + } + + public static string Fill(Stream stream, List<string/*!*/>/*!*/ defines) { + Contract.Requires(stream != null); + Contract.Requires(cce.NonNullElements(defines)); + Contract.Ensures(Contract.Result<string>() != null); + StreamReader/*!*/ reader = new StreamReader(stream); + return Fill(reader, defines); + } + public static string Fill(TextReader reader, List<string/*!*/>/*!*/ defines) { + Contract.Requires(reader != null); + Contract.Requires(cce.NonNullElements(defines)); + Contract.Ensures(Contract.Result<string>() != null); + 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 + //Contract.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 + //Contract.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 + } + } + + return sb.ToString(); + } + } }
\ No newline at end of file |