summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/Absy.cs12
-rw-r--r--Source/Core/AbsyExpr.cs9
-rw-r--r--Source/Core/AbsyQuant.cs7
-rw-r--r--Source/Core/CommandLineOptions.cs12
-rw-r--r--Source/Core/Util.cs101
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs14
-rw-r--r--Test/test0/PrettyPrint.bpl2
-rw-r--r--Test/test20/TypeSynonyms2.bpl2
8 files changed, 144 insertions, 15 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 0026a3fe..82c5cc59 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -1862,8 +1862,10 @@ namespace Microsoft.Boogie {
Contract.Requires(stream != null);
Type.EmitOptionalTypeParams(stream, TypeParameters);
stream.Write("(");
+ stream.push();
InParams.Emit(stream, true);
stream.Write(")");
+ stream.sep();
if (shortRet) {
Contract.Assert(OutParams.Count == 1);
@@ -1874,6 +1876,7 @@ namespace Microsoft.Boogie {
OutParams.Emit(stream, true);
stream.Write(")");
}
+ stream.pop();
}
// Register all type parameters at the resolution context
@@ -3293,14 +3296,17 @@ namespace Microsoft.Boogie {
public void Emit(TokenTextWriter stream) {
Contract.Requires(stream != null);
stream.SetToken(this);
+ stream.push();
if (this.Name != NoName) {
stream.Write("{0}: ", TokenTextWriter.SanitizeIdentifier(this.Name));
}
this.Type.Emit(stream);
if (this.WhereExpr != null) {
+ stream.sep();
stream.Write(" where ");
this.WhereExpr.Emit(stream);
}
+ stream.pop();
}
public override void Resolve(ResolutionContext rc) {
//Contract.Requires(rc != null);
@@ -3374,12 +3380,15 @@ namespace Microsoft.Boogie {
public static void Emit(this List<Expr> ts, TokenTextWriter stream) {
Contract.Requires(stream != null);
string sep = "";
+ stream.push();
foreach (Expr/*!*/ e in ts) {
Contract.Assert(e != null);
stream.Write(sep);
sep = ", ";
+ stream.sep();
e.Emit(stream);
}
+ stream.pop();
}
public static void Emit(this List<IdentifierExpr> ids, TokenTextWriter stream, bool printWhereComments) {
@@ -3402,12 +3411,15 @@ namespace Microsoft.Boogie {
public static void Emit(this List<Variable> vs, TokenTextWriter stream, bool emitAttributes) {
Contract.Requires(stream != null);
string sep = "";
+ stream.push();
foreach (Variable/*!*/ v in vs) {
Contract.Assert(v != null);
stream.Write(sep);
sep = ", ";
+ stream.sep();
v.EmitVitals(stream, 0, emitAttributes);
}
+ stream.pop();
}
public static void Emit(this List<Type> tys, TokenTextWriter stream, string separator) {
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 70b445b1..d6dd17c9 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1418,15 +1418,18 @@ namespace Microsoft.Boogie {
bool parensNeeded = opBS < ctxtBS ||
(opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));
+ var pop = stream.push(FunctionName);
if (parensNeeded) {
stream.Write("(");
}
cce.NonNull(args[0]).Emit(stream, opBindingStrength, fragileLeftContext);
+ stream.sep();
stream.Write(" {0} ", FunctionName);
cce.NonNull(args[1]).Emit(stream, opBindingStrength, fragileRightContext);
if (parensNeeded) {
stream.Write(")");
}
+ stream.pop(pop);
}
public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
//Contract.Requires(subjectForErrorReporting != null);
@@ -2521,13 +2524,17 @@ namespace Microsoft.Boogie {
//Contract.Requires(args != null);
stream.SetToken(ref this.tok);
Contract.Assert(args.Count == 3);
- stream.Write("(if ");
+ stream.push();
+ stream.Write("(if ");
cce.NonNull(args[0]).Emit(stream, 0x00, false);
+ stream.sep();
stream.Write(" then ");
cce.NonNull(args[1]).Emit(stream, 0x00, false);
+ stream.sep();
stream.Write(" else ");
cce.NonNull(args[2]).Emit(stream, 0x00, false);
stream.Write(")");
+ stream.pop();
}
public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 397d8eba..c9e8f210 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -113,20 +113,24 @@ namespace Microsoft.Boogie {
public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
//Contract.Requires(stream != null);
+ stream.push();
stream.Write(this, "({0}", Kind.ToString().ToLower());
this.EmitTypeHint(stream);
Type.EmitOptionalTypeParams(stream, TypeParameters);
stream.Write(this, " ");
this.Dummies.Emit(stream, true);
stream.Write(" :: ");
+ stream.sep();
for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next) {
kv.Emit(stream);
stream.Write(" ");
}
this.EmitTriggers(stream);
+ stream.sep();
this.Body.Emit(stream);
stream.Write(")");
+ stream.pop();
}
protected virtual void ResolveTriggers(ResolutionContext rc) {
@@ -542,10 +546,13 @@ namespace Microsoft.Boogie {
protected override void EmitTriggers(TokenTextWriter stream) {
//Contract.Requires(stream != null);
+ stream.push();
for (Trigger tr = this.Triggers; tr != null; tr = tr.Next) {
tr.Emit(stream);
stream.Write(" ");
+ stream.sep();
}
+ stream.pop();
}
// if the user says ( forall x :: forall y :: ... ) and specifies *no* triggers, we transform it to
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4f9488a3..65554a1e 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -421,6 +421,8 @@ namespace Microsoft.Boogie {
public string CVC4ExecutablePath = null;
public int KInductionDepth = -1;
+ public bool PrettyPrint = true;
+
public enum ProverWarnings {
None,
Stdout,
@@ -741,6 +743,13 @@ namespace Microsoft.Boogie {
}
return true;
+ case "pretty":
+ int val = 1;
+ if (ps.GetNumericArgument(ref val, 2)) {
+ PrettyPrint = val == 1;
+ }
+ return true;
+
case "OwickiGries":
if (ps.ConfirmArgumentCount(1)) {
OwickiGriesDesugaredOutputFile = args[ps.i];
@@ -1657,6 +1666,9 @@ namespace Microsoft.Boogie {
/print:<file> : print Boogie program after parsing it
(use - as <file> to print to console)
+ /pretty:<n>
+ 0 - print each Boogie statement on one line (faster).
+ 1 (default) - pretty-print with some line breaks.
/printWithUniqueIds : print augmented information that uniquely
identifies variables
/printUnstructured : with /print option, desugars all structured statements
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index c14cb82e..66eefd8c 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -127,6 +127,90 @@ namespace Microsoft.Boogie {
"while",
};
+ // "Pretty" printing: not very efficient, and not necessarily very pretty, but helps a bit
+ private readonly bool pretty;
+
+ // The stack of writers in a current separator-block.
+ // The string is an optional identifier that allows you
+ // to not start a new indentation for e.g. "&&" in "a && b && c".
+ // When the pretty printing is finished, this should be empty.
+ Stack<KeyValuePair<string, List<TextWriter>>> wstk;
+
+ // The original writer: where everything should finally end up.
+ TextWriter actual_writer;
+
+ public bool push(string type = null) {
+ if (pretty) {
+ if (wstk == null) {
+ wstk = new Stack<KeyValuePair<string, List<TextWriter>>>();
+ actual_writer = writer;
+ }
+ if (wstk.Count > 0 && wstk.Peek().Key == type && type != null) {
+ sep();
+ return false; // don't actually pop this thing (send this bool to pop)
+ } else {
+ wstk.Push(new KeyValuePair<string, List<TextWriter>>(type, new List<TextWriter> { }));
+ sep();
+ return true; // this needs to be popped
+ }
+ } else {
+ return false;
+ }
+ }
+
+ public void pop(bool do_it = true) {
+ if (pretty) {
+ if (do_it) {
+ List<TextWriter> ws = wstk.Pop().Value;
+ // try to figure out if you should insert line breaks between
+ // them or print them on one single line
+ // this breaks down when there are newlines inserted
+ List<String> ss = new List<String>();
+ int len = 0;
+ foreach (TextWriter w in ws) {
+ foreach (String s in w.ToString().Split(new String[] { "\r\n", "\n" }, StringSplitOptions.None)) {
+ if (s.Length > 0) {
+ ss.Add(s);
+ len += s.Length;
+ // len = Math.Max(len, s.Length);
+ }
+ }
+ }
+ // figure out which is the next writer to use
+ List<TextWriter> tw = wstk.Count > 0 ? wstk.Peek().Value : null;
+ if (tw == null) {
+ writer = actual_writer;
+ } else {
+ writer = tw.Last();
+ }
+ // write the strings (we would like to know WHERE we are in the document here)
+ if (len > 80 /* - wstk.Count * 2 */) {
+ for (int i = 0; i < ss.Count; i++) {
+ if (i != ss.Count - 1) {
+ writer.WriteLine(ss[i]);
+ writer.Write(" ");
+ } else {
+ writer.Write(ss[i]);
+ }
+ }
+ } else {
+ foreach (String s in ss) {
+ writer.Write(s);
+ }
+ }
+ }
+ }
+ }
+
+ public void sep() {
+ if (pretty) {
+ List<TextWriter> ws = wstk.Peek().Value;
+
+ writer = new StringWriter();
+ wstk.Peek().Value.Add(writer);
+ }
+ }
+
private IToken/*!*/ CurrentToken {
get {
Contract.Ensures(Contract.Result<IToken>() != null);
@@ -160,46 +244,53 @@ namespace Microsoft.Boogie {
} else if (name.Length > 2 && name[0] == 'b' && name[1] == 'v') {
int dummy;
return int.TryParse(name.Substring(2), out dummy) ? "\\" + name : name;
+ } else if (name.Contains('@')) {
+ return SanitizeIdentifier(name.Replace("@", "#AT#"));
} else {
return name;
}
}
- public TokenTextWriter(string filename)
+ public TokenTextWriter(string filename, bool pretty = false)
: base() {
Contract.Requires(filename != null);
+ this.pretty = pretty;
this.filename = filename;
this.writer = new StreamWriter(filename);
}
- public TokenTextWriter(string filename, bool setTokens)
+ public TokenTextWriter(string filename, bool setTokens, bool pretty = false)
: base() {
Contract.Requires(filename != null);
+ this.pretty = pretty;
this.filename = filename;
this.writer = new StreamWriter(filename);
this.setTokens = setTokens;
}
- public TokenTextWriter(string filename, TextWriter writer, bool setTokens)
+ public TokenTextWriter(string filename, TextWriter writer, bool setTokens, bool pretty = false)
: base() {
Contract.Requires(writer != null);
Contract.Requires(filename != null);
+ this.pretty = pretty;
this.filename = filename;
this.writer = writer;
this.setTokens = setTokens;
}
- public TokenTextWriter(string filename, TextWriter writer)
+ public TokenTextWriter(string filename, TextWriter writer, bool pretty = false)
: base() {
Contract.Requires(writer != null);
Contract.Requires(filename != null);
+ this.pretty = pretty;
this.filename = filename;
this.writer = writer;
}
- public TokenTextWriter(TextWriter writer)
+ public TokenTextWriter(TextWriter writer, bool pretty = false)
: base() {
Contract.Requires(writer != null);
+ this.pretty = pretty;
this.filename = "<no file>";
this.writer = writer;
}
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 925b414b..cac56c4b 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -476,7 +476,7 @@ namespace Microsoft.Boogie
return;
if (CommandLineOptions.Clo.PrintFile != null)
{
- PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);
+ PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false, true, CommandLineOptions.Clo.PrettyPrint);
}
LinearTypeChecker linearTypeChecker;
@@ -511,7 +511,7 @@ namespace Microsoft.Boogie
{
int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
CommandLineOptions.Clo.PrintUnstructured = 1;
- PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false);
+ PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false, CommandLineOptions.Clo.PrettyPrint);
CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
}
}
@@ -559,7 +559,7 @@ namespace Microsoft.Boogie
}
- public static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring, bool setTokens = true)
+ public static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring, bool setTokens = true, bool pretty = false)
{
Contract.Requires(program != null);
Contract.Requires(filename != null);
@@ -569,8 +569,8 @@ namespace Microsoft.Boogie
CommandLineOptions.Clo.PrintDesugarings = false;
}
using (TokenTextWriter writer = filename == "-" ?
- new TokenTextWriter("<console>", Console.Out, setTokens) :
- new TokenTextWriter(filename, setTokens))
+ new TokenTextWriter("<console>", Console.Out, setTokens, pretty) :
+ new TokenTextWriter(filename, setTokens, pretty))
{
if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never)
{
@@ -729,7 +729,7 @@ namespace Microsoft.Boogie
if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings)
{
// if PrintDesugaring option is engaged, print the file here, after resolution and type checking
- PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true);
+ PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true, true, CommandLineOptions.Clo.PrettyPrint);
}
return PipelineOutcome.ResolvedAndTypeChecked;
@@ -838,7 +838,7 @@ namespace Microsoft.Boogie
if (CommandLineOptions.Clo.PrintInstrumented)
{
- program.Emit(new TokenTextWriter(Console.Out));
+ program.Emit(new TokenTextWriter(Console.Out, CommandLineOptions.Clo.PrettyPrint));
}
#endregion
diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl
index 8aa25d33..c79eff80 100644
--- a/Test/test0/PrettyPrint.bpl
+++ b/Test/test0/PrettyPrint.bpl
@@ -1,4 +1,4 @@
-// RUN: %boogie -noVerify -printInstrumented "%s" > "%t"
+// RUN: %boogie -pretty:0 -noVerify -printInstrumented "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
const x: int;
const y: int;
diff --git a/Test/test20/TypeSynonyms2.bpl b/Test/test20/TypeSynonyms2.bpl
index 472b1e96..1cb6e781 100644
--- a/Test/test20/TypeSynonyms2.bpl
+++ b/Test/test20/TypeSynonyms2.bpl
@@ -1,6 +1,6 @@
// RUN: %boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-// RUN: %boogie -noVerify -print:- -env:0 -printDesugared "%s" > "%t"
+// RUN: %boogie -noVerify -print:- -pretty:0 -env:0 -printDesugared "%s" > "%t"
// RUN: %diff "%s.print.expect" "%t"
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 10:46:33 +0000