diff options
Diffstat (limited to 'Source/VCExpr/VCExprASTPrinter.cs')
| -rw-r--r-- | Source/VCExpr/VCExprASTPrinter.cs | 247 |
1 files changed, 247 insertions, 0 deletions
diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs new file mode 100644 index 00000000..796a2b4e --- /dev/null +++ b/Source/VCExpr/VCExprASTPrinter.cs @@ -0,0 +1,247 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using Microsoft.Contracts;
+using Microsoft.Basetypes;
+
+// A simple visitor for turning a VCExpr into a human-readable string
+// (S-expr syntax)
+
+namespace Microsoft.Boogie.VCExprAST
+{
+
+ public class VCExprPrinter : IVCExprVisitor<bool, TextWriter!> {
+ private VCExprOpPrinter OpPrinterVar = null;
+ private VCExprOpPrinter! OpPrinter { get {
+ if (OpPrinterVar == null)
+ OpPrinterVar = new VCExprOpPrinter(this);
+ return OpPrinterVar;
+ } }
+
+ public void Print(VCExpr! expr, TextWriter! wr) {
+ expr.Accept<bool, TextWriter!>(this, wr);
+ }
+
+ public bool Visit(VCExprLiteral! node, TextWriter! wr) {
+ if (node == VCExpressionGenerator.True)
+ wr.Write("true");
+ else if (node == VCExpressionGenerator.False)
+ wr.Write("false");
+ else if (node is VCExprIntLit) {
+ wr.Write(((VCExprIntLit)node).Val);
+ } else
+ assert false;
+ return true;
+ }
+ public bool Visit(VCExprNAry! node, TextWriter! wr) {
+ VCExprOp! op = node.Op;
+
+ if (op.Equals(VCExpressionGenerator.AndOp) ||
+ op.Equals(VCExpressionGenerator.OrOp)) {
+ // handle these operators without recursion
+
+ wr.Write("({0}",
+ op.Equals(VCExpressionGenerator.AndOp) ? "And" : "Or");
+ IEnumerator! enumerator = new VCExprNAryUniformOpEnumerator (node);
+ while (enumerator.MoveNext()) {
+ VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
+ if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+ wr.Write(" ");
+ Print((VCExpr!)enumerator.Current, wr);
+ }
+ }
+
+ wr.Write(")");
+
+ return true;
+ }
+
+ return node.Accept<bool, TextWriter!>(OpPrinter, wr);
+ }
+ public bool Visit(VCExprVar! node, TextWriter! wr) {
+ wr.Write(node.Name);
+ return true;
+ }
+ public bool Visit(VCExprQuantifier! node, TextWriter! wr) {
+ string! quan = node.Quan == Quantifier.ALL ? "Forall" : "Exists";
+
+ wr.Write("({0} ", quan);
+
+ if (node.TypeParameters.Count > 0) {
+ wr.Write("<");
+ string! sep = "";
+ foreach (TypeVariable! v in node.TypeParameters) {
+ wr.Write(sep);
+ sep = ", ";
+ wr.Write("{0}", v.Name);
+ }
+ wr.Write("> ");
+ }
+
+ if (node.BoundVars.Count > 0) {
+ string! sep = "";
+ foreach (VCExprVar! v in node.BoundVars) {
+ wr.Write(sep);
+ sep = ", ";
+ Print(v, wr);
+ }
+ wr.Write(" ");
+ }
+
+ wr.Write(":: ");
+
+ if (node.Triggers.Count > 0) {
+ wr.Write("{0} ", "{");
+ string! sep = "";
+ foreach (VCTrigger! t in node.Triggers) {
+ wr.Write(sep);
+ sep = ", ";
+ string! sep2 = "";
+ foreach (VCExpr! e in t.Exprs) {
+ wr.Write(sep2);
+ sep2 = "+";
+ Print(e, wr);
+ }
+ }
+ wr.Write(" {0} ", "}");
+ }
+
+ Print(node.Body, wr);
+ wr.Write(")");
+ return true;
+ }
+ public bool Visit(VCExprLet! node, TextWriter! wr) {
+ wr.Write("(Let ");
+
+ string! sep = "";
+ foreach (VCExprLetBinding! b in node) {
+ wr.Write(sep);
+ sep = ", ";
+ Print(b.V, wr);
+ wr.Write(" = ");
+ Print(b.E, wr);
+ }
+ wr.Write(" ");
+
+ Print(node.Body, wr);
+ wr.Write(")");
+ return true;
+ }
+ }
+
+ public class VCExprOpPrinter : IVCExprOpVisitor<bool, TextWriter!> {
+ private VCExprPrinter! ExprPrinter;
+
+ public VCExprOpPrinter(VCExprPrinter! exprPrinter) {
+ this.ExprPrinter = exprPrinter;
+ }
+
+ private bool PrintNAry(string! op, VCExprNAry! node, TextWriter! wr) {
+ wr.Write("({0}", op);
+ foreach (VCExpr! arg in node) {
+ wr.Write(" ");
+ ExprPrinter.Print(arg, wr);
+ }
+ wr.Write(")");
+ return true;
+ }
+
+ public bool VisitNotOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("!", node, wr);
+ }
+ public bool VisitEqOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("==", node, wr);
+ }
+ public bool VisitNeqOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("!=", node, wr);
+ }
+ public bool VisitAndOp (VCExprNAry! node, TextWriter! wr) {
+ assert false;
+ }
+ public bool VisitOrOp (VCExprNAry! node, TextWriter! wr) {
+ assert false;
+ }
+ public bool VisitImpliesOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("Implies", node, wr);
+ }
+ public bool VisitDistinctOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("Distinct", node, wr);
+ }
+ public bool VisitLabelOp (VCExprNAry! node, TextWriter! wr) {
+ VCExprLabelOp! op = (VCExprLabelOp)node.Op;
+ return PrintNAry("Label " + op.label, node, wr);
+ }
+ public bool VisitSelectOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("Select", node, wr);
+ }
+ public bool VisitStoreOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("Store", node, wr);
+ }
+ public bool VisitBvOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("Bv", node, wr);
+ }
+ public bool VisitBvExtractOp(VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("BvExtract", node, wr);
+ }
+ public bool VisitBvConcatOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("BvConcat", node, wr);
+ }
+ public bool VisitIfThenElseOp(VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("if-then-else", node, wr);
+ }
+ public bool VisitCustomOp(VCExprNAry! node, TextWriter! wr) {
+ VCExprCustomOp op = (VCExprCustomOp)node.Op;
+ return PrintNAry(op.Name, node, wr);
+ }
+ public bool VisitAddOp (VCExprNAry! node, TextWriter! wr) {
+ if (CommandLineOptions.Clo.ReflectAdd) {
+ return PrintNAry("Reflect$Add", node, wr);
+ } else {
+ return PrintNAry("+", node, wr);
+ }
+ }
+ public bool VisitSubOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("-", node, wr);
+ }
+ public bool VisitMulOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("*", node, wr);
+ }
+ public bool VisitDivOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("/", node, wr);
+ }
+ public bool VisitModOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("%", node, wr);
+ }
+ public bool VisitLtOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("<", node, wr);
+ }
+ public bool VisitLeOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("<=", node, wr);
+ }
+ public bool VisitGtOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry(">", node, wr);
+ }
+ public bool VisitGeOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry(">=", node, wr);
+ }
+ public bool VisitSubtypeOp (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("<:", node, wr);
+ }
+ public bool VisitSubtype3Op (VCExprNAry! node, TextWriter! wr) {
+ return PrintNAry("<::", node, wr);
+ }
+ public bool VisitBoogieFunctionOp (VCExprNAry! node, TextWriter! wr) {
+ VCExprBoogieFunctionOp! op = (VCExprBoogieFunctionOp)node.Op;
+ return PrintNAry(op.Func.Name, node, wr);
+ }
+ }
+
+
+}
|