diff options
| author |  tabarbe <unknown> | 2010-08-20 22:29:44 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-20 22:29:44 +0000 |
| commit | b617dda87871573b826dada4af73fc48dce94f15 (patch) | |
| tree | 453088d59b99376c0b14035e76463a4561d6ec1c /Source/Core/Util.cs | |
| parent | 0d77cf304b9bd2b2152fe1a733e4533536c883c0 (diff) | |
Boogie: Renaming core sources in preparation for port commit
Diffstat (limited to 'Source/Core/Util.cs')
| -rw-r--r-- | Source/Core/Util.cs | 481 |
1 files changed, 481 insertions, 0 deletions
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs new file mode 100644 index 00000000..87323eb5 --- /dev/null +++ b/Source/Core/Util.cs @@ -0,0 +1,481 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.Boogie
+{
+ using System;
+ using System.IO;
+ using System.Collections;
+ using Microsoft.Contracts;
+
+ public class TokenTextWriter : IDisposable
+ {
+ string! filename;
+ TextWriter! writer;
+ bool writerOpenedHere = false;
+ bool setTokens = true;
+ int line = 1;
+ int col;
+
+ private const int indent_size = 2;
+ protected static string! Indent (int level)
+ {
+ return new string(' ', (indent_size * level));
+ }
+
+
+ // Keywords, this array *must* be sorted
+ public static readonly string[]! BplKeywords =
+ {
+ "assert",
+ "assume",
+ "axiom",
+ "bool",
+ "break",
+ "call",
+ "cast",
+ "const",
+ "else",
+ "ensures",
+ "exists",
+ "false",
+ "forall",
+ "free",
+ "function",
+ "goto",
+ "havoc",
+ "if",
+ "implementation",
+ "int",
+ "invariant",
+ "modifies",
+ "old",
+ "procedure",
+ "public",
+ "requires",
+ "return",
+ "returns",
+ "true",
+ "type",
+ "unique",
+ "var",
+ "where",
+ "while",
+ };
+
+ private IToken! CurrentToken
+ {
+ get
+ {
+ Token token = new Token();
+ token.filename = filename;
+ token.line = line;
+ token.col = col;
+ return token;
+ }
+ }
+
+ public void SetToken(Absy! absy)
+ {
+ this.SetToken(ref absy.tok);
+ }
+
+ public void SetToken(ref IToken! tok)
+ {
+ if (this.setTokens) {
+ tok = this.CurrentToken;
+ }
+ }
+
+ public static string! SanitizeIdentifier (string! name)
+ {
+ int index = Array.BinarySearch(TokenTextWriter.BplKeywords, name);
+ if (index >= 0) {
+ return "\\" + name;
+ } else if (name.Length > 2 && name[0] == 'b' && name[1] == 'v') {
+ int dummy;
+ return int.TryParse(name.Substring(2), out dummy) ? "\\" + name : name;
+ } else {
+ return name;
+ }
+ }
+
+ public TokenTextWriter(string! filename)
+ {
+ this.filename = filename;
+ this.writer = new StreamWriter(filename);
+ this.writerOpenedHere = true;
+ base();
+ }
+
+ public TokenTextWriter(string! filename, TextWriter! writer, bool setTokens)
+ {
+ this.filename = filename;
+ this.writer = writer;
+ this.setTokens = setTokens;
+ base();
+ }
+
+ public TokenTextWriter(string! filename, TextWriter! writer)
+ {
+ this.filename = filename;
+ this.writer = writer;
+ base();
+ }
+
+ public TokenTextWriter(TextWriter! writer)
+ {
+ this.filename = "<no file>";
+ this.writer = writer;
+ base();
+ }
+
+ public void Write(string! text)
+ {
+ this.writer.Write(text);
+ this.col += text.Length;
+ }
+
+ public void WriteIndent(int level)
+ {
+ this.Write(Indent(level));
+ }
+
+ public void Write(string! text, params object[] args)
+ {
+ this.Write(string.Format(text, args));
+ }
+
+ public void Write(int level, string! text)
+ {
+ this.WriteIndent(level);
+ this.Write(text);
+ }
+
+ public void Write(int level, string! text, params object[] args)
+ {
+ this.WriteIndent(level);
+ this.Write(text, args);
+ }
+
+ public void Write(Absy! node, string! text)
+ {
+ this.SetToken(node);
+ this.Write(text);
+ }
+
+ public void Write(Absy! node, string! text, params string[] args)
+ {
+ this.SetToken(node);
+ this.Write(text, args);
+ }
+
+ public void Write(Absy! node, int level, string! text)
+ {
+ this.WriteIndent(level);
+ this.SetToken(node);
+ this.Write(text);
+ }
+
+ public void Write(Absy! node, int level, string! text, params object[] args)
+ {
+ this.WriteIndent(level);
+ this.SetToken(node);
+ this.Write(text, args);
+ }
+
+ public void WriteLine()
+ {
+ this.writer.WriteLine();
+ this.line++;
+ this.col = 0;
+ }
+
+ public void WriteLine(string! text)
+ {
+ this.writer.WriteLine(text);
+ this.line++;
+ this.col = 0;
+ }
+
+ public void WriteText(string! text) {
+ int processed = 0;
+ while (true) {
+ int n = text.IndexOf('\n', processed);
+ if (n == -1) {
+ this.writer.Write(text);
+ this.col += text.Length - processed;
+ return;
+ }
+ processed = n + 1;
+ this.line++;
+ this.col = 0;
+ }
+ }
+
+ public void WriteLine(string! text, params object[] args)
+ {
+ this.WriteLine(string.Format(text, args));
+ }
+
+ public void WriteLine(int level, string! text)
+ {
+ this.WriteIndent(level);
+ this.WriteLine(text);
+ }
+
+ public void WriteLine(int level, string! text, params object[] args)
+ {
+ this.WriteIndent(level);
+ this.WriteLine(text, args);
+ }
+
+ public void WriteLine(Absy! node, string! text)
+ {
+ this.SetToken(node);
+ this.WriteLine(text);
+ }
+
+ public void WriteLine(Absy! node, int level, string! text)
+ {
+ this.SetToken(node);
+ this.WriteLine(level, text);
+ }
+
+ public void WriteLine(Absy! node, int level, string! text, params object[] args)
+ {
+ this.SetToken(node);
+ this.WriteLine(level, text, args);
+ }
+
+ public void Close()
+ {
+ this.writer.Close();
+ }
+
+ public void Dispose()
+ {
+ this.Close();
+ }
+ }
+
+ public class Helpers {
+ public static string! BeautifyBplString (string! s) {
+ // strip "^" if it is the first character, change "$result" to "result"
+ if (s.StartsWith("^") || s == "$result") {
+ s = s.Substring(1);
+ } else if (s.StartsWith("call")) {
+ s = s.Substring(s.IndexOf('@') + 1);
+ if (s.StartsWith("formal@")) {
+ s = "(value of formal parameter: " + s.Substring(7) +")";
+ }
+ }
+ // strip "$in" from the end of identifier names
+ if (s.EndsWith("$in")) {
+ return "(initial value of: " + s.Substring(0, s.Length-3) +")";
+ } else {
+ return s;
+ }
+ }
+ public static string! PrettyPrintBplExpr (Expr! e) {
+ // anything that is unknown will just be printed via ToString
+ // OldExpr and QuantifierExpr, BvExtractExpr, BvConcatExpr are ignored for now
+ // LiteralExpr is printed as itself by ToString
+ if (e is IdentifierExpr) {
+ string s = e.ToString();
+ return Helpers.BeautifyBplString(s);
+ }
+ else if (e is NAryExpr) {
+ NAryExpr ne = (NAryExpr) e;
+ IAppliable fun = ne.Fun;
+ ExprSeq eSeq = ne.Args;
+ if (fun != null) {
+ if ((fun.FunctionName == "$Length" || fun.FunctionName == "$StringLength" ) && eSeq.Length == 1) {
+ Expr e0 = eSeq[0];
+ if (e0 != null) {
+ string s0 = PrettyPrintBplExpr(e0);
+ return s0 + ".Length";
+ }
+ //unexpected, just fall outside to the default
+ } else if (fun.FunctionName == "$typeof" && eSeq.Length == 1) {
+ Expr e0 = eSeq[0];
+ if (e0 != null) {
+ string s0 = PrettyPrintBplExpr(e0);
+ return "(the dynamic type of: " + s0 + ")";
+ }
+ //unexpected, just fall outside to the default
+ } else if (fun.FunctionName == "IntArrayGet" && eSeq.Length == 2) {
+ Expr e0 = eSeq[0];
+ Expr e1 = eSeq[1];
+ if (e0 != null && e1 != null) {
+ string s0 = PrettyPrintBplExpr(e0);
+ string s1 = PrettyPrintBplExpr(e1);
+ return s0 + "[" + s1 + "]";
+ }
+ //unexpected, just fall outside to the default
+ } else if (fun.FunctionName == "$Is" && eSeq.Length == 2) {
+ Expr e0 = eSeq[0];
+ Expr e1 = eSeq[1];
+ if (e0 != null && e1 != null) {
+ string s0 = PrettyPrintBplExpr(e0);
+ string s1 = PrettyPrintBplExpr(e1);
+ return "(" + s0 + " == null || (" + s0 + " is " + s1 + "))";
+ }
+ //unexpected, just fall outside to the default
+ } else if (fun.FunctionName == "$IsNotNull" && eSeq.Length == 2) {
+ Expr e0 = eSeq[0];
+ Expr e1 = eSeq[1];
+ if (e0 != null && e1 != null) {
+ string s0 = PrettyPrintBplExpr(e0);
+ string s1 = PrettyPrintBplExpr(e1);
+ return "(" + s0 + " is " + s1 +")";
+ }
+ //unexpected, just fall outside to the default
+ } else if (fun is MapSelect && eSeq.Length <= 3) {
+ // only maps with up to two arguments are supported right now (here)
+ if (((!)eSeq[0]).ToString() == "$Heap") {
+ //print Index0.Index1, unless Index1 is "$elements", then just print Index0
+ string s0 = PrettyPrintBplExpr((!)eSeq[1]);
+ if (eSeq.Length > 2) {
+ string s1 = PrettyPrintBplExpr((!)eSeq[2]);
+ if (s1 == "$elements") {
+ return s0;
+ } else {
+ if (eSeq[2] is IdentifierExpr) {
+ // strip the class name out of a fieldname
+ s1 = s1.Substring(s1.LastIndexOf('.') + 1);
+ }
+ return s0 + "." + s1;
+ }
+ }
+ }
+ //unexpected, just fall outside to the default
+ } else if (fun is Microsoft.Boogie.BinaryOperator && eSeq.Length == 2) {
+ Microsoft.Boogie.BinaryOperator f = (Microsoft.Boogie.BinaryOperator) fun;
+ Expr e0 = eSeq[0];
+ Expr e1 = eSeq[1];
+ if (e0 != null && e1 != null) {
+ string s0 = PrettyPrintBplExpr(e0);
+ string s1 = PrettyPrintBplExpr(e1);
+ string op = "";
+ switch (f.Op) {
+ case Microsoft.Boogie.BinaryOperator.Opcode.Add:
+ op = " + ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.And:
+ op = " && ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Div:
+ op = " / ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Eq:
+ op = " == ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Ge:
+ op = " >= ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Gt:
+ op = " > ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Iff:
+ op = " <==> ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Imp:
+ op = " ==> ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Le:
+ op = " <= ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Lt:
+ op = " < ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Mod:
+ op = " % ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Mul:
+ op = " * ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Neq:
+ op = " != ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Or:
+ op = " || ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Sub:
+ op = " - ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Subtype:
+ op = " <: ";
+ break;
+ default: op = " ";
+ break;
+ }
+ return "(" + s0 + op + s1 + ")";
+ }
+ //unexpected, just fall outside to the default
+ } else {
+ string s = fun.FunctionName + "(";
+ for (int i = 0; i < eSeq.Length; i++) {
+ Expr ex = eSeq[i];
+ assume ex != null;
+ if (i>0) {
+ s += ", ";
+ }
+ string t = PrettyPrintBplExpr(ex);
+ if (t.StartsWith("(") && t.EndsWith(")")) {
+ t = t.Substring(1, t.Length -2);
+ }
+ s += t;
+ }
+ s += ")";
+ return s;
+ //unexpected, just fall outside to the default
+ }
+ }
+ }
+
+ return e.ToString();
+ }
+
+ private static readonly DateTime StartUp = DateTime.Now;
+
+ public static void ExtraTraceInformation(string! point) {
+ if (CommandLineOptions.Clo.TraceTimes) {
+ DateTime now = DateTime.Now;
+ TimeSpan timeSinceStartUp = now - StartUp;
+ Console.WriteLine(">>> {0} [{1} s]", point, timeSinceStartUp.TotalSeconds);
+ }
+ }
+
+ // Substitute @PROC@ in a filename with the given descName
+ public static string! SubstituteAtPROC(string! descName, string! fileName) {
+ System.Text.StringBuilder! sb =
+ new System.Text.StringBuilder(descName.Length);
+ // quote the name, characters like ^ cause trouble in CMD
+ // while $ could cause trouble in SH
+ foreach (char c in descName) {
+ if (Char.IsLetterOrDigit(c) || c == '.') {
+ sb.Append(c);
+ } else {
+ sb.Append('_');
+ }
+ }
+ string pn = sb.ToString();
+ // We attempt to avoid filenames that are too long, but we only
+ // do it by truncating the @PROC@ replacement, which leaves unchanged
+ // any filename extension specified by the user. We base our
+ // calculations on that there is at most one occurrence of @PROC@.
+ if (180 <= fileName.Length - 6 + pn.Length) {
+ pn = pn.Substring(0, max{180 - (fileName.Length - 6), 0}) + "-n" + sequenceNumber;
+ sequenceNumber++;
+ }
+
+ return fileName.Replace("@PROC@", pn);
+ }
+
+ private static int sequenceNumber = 0;
+
+ }
+}
|