From f08bf65f0c319ea266e75bf4ebb8448ab91d2ae8 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Thu, 2 Dec 2010 14:35:21 +0000 Subject: Factored out the ParserHelper class into a separate project and updated the files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#. --- Source/ParserHelper/ParserHelper.cs | 250 ++++++++++++++++++++++++++++++++ Source/ParserHelper/ParserHelper.csproj | 92 ++++++++++++ 2 files changed, 342 insertions(+) create mode 100644 Source/ParserHelper/ParserHelper.cs create mode 100644 Source/ParserHelper/ParserHelper.csproj (limited to 'Source/ParserHelper') diff --git a/Source/ParserHelper/ParserHelper.cs b/Source/ParserHelper/ParserHelper.cs new file mode 100644 index 00000000..465b9245 --- /dev/null +++ b/Source/ParserHelper/ParserHelper.cs @@ -0,0 +1,250 @@ +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 IToken/*!*/ NoToken = new Token(); + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(NoToken != null); + } + + + public Token() { + this._val = "anything so that it is nonnull"; + } + public Token(int linenum, int colnum) + : base() {//BASEMOVE DANGER + this._line = linenum; + this._col = colnum; + this._val = "anything so that it is nonnull"; + //: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; + } + } + + + } + + 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/*!*/ 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/*!*/ defines) { + Contract.Requires(stream != null); + Contract.Requires(cce.NonNullElements(defines)); + Contract.Ensures(Contract.Result() != null); + StreamReader/*!*/ reader = new StreamReader(stream); + return Fill(reader, defines); + } + public static string Fill(TextReader reader, List/*!*/ defines) { + Contract.Requires(reader != null); + Contract.Requires(cce.NonNullElements(defines)); + Contract.Ensures(Contract.Result() != null); + StringBuilder sb = new StringBuilder(); + List/*!*/ readState = new List(); // 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 diff --git a/Source/ParserHelper/ParserHelper.csproj b/Source/ParserHelper/ParserHelper.csproj new file mode 100644 index 00000000..405a3d75 --- /dev/null +++ b/Source/ParserHelper/ParserHelper.csproj @@ -0,0 +1,92 @@ + + + + Debug + AnyCPU + 8.0.30703 + 2.0 + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + Library + Properties + ParserHelper + ParserHelper + v3.5 + 512 + + 1 + + + true + full + false + ..\..\Binaries\ + TRACE;DEBUG + prompt + 4 + False + True + False + True + False + True + True + True + True + True + True + True + False + False + + + + + + ..\..\baseline.xml + Full + %28none%29 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + + + true + + + ..\InterimKey.snk + + + + False + ..\..\Binaries\Microsoft.Contracts.dll + + + + + + + + + + + + + + {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} + CodeContractsExtender + + + + + \ No newline at end of file -- cgit v1.2.3