diff options
Diffstat (limited to 'Chalice/src/main/scala/PrettyPrinter.scala')
| -rw-r--r-- | Chalice/src/main/scala/PrettyPrinter.scala | 396 |
1 files changed, 0 insertions, 396 deletions
diff --git a/Chalice/src/main/scala/PrettyPrinter.scala b/Chalice/src/main/scala/PrettyPrinter.scala deleted file mode 100644 index a54173df..00000000 --- a/Chalice/src/main/scala/PrettyPrinter.scala +++ /dev/null @@ -1,396 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-package chalice;
-object PrintProgram {
- def P(prog: List[TopLevelDecl]) =
- for (decl <- prog) decl match {
- case cl: Class =>
- if (cl.IsExternal)
- print("external ")
- println("class " + cl.id + " module " + cl.module + (if (cl.IsRefinement) " refines " + cl.refinesId else "") + " {")
- cl.members foreach Member
- println("}")
- case ch: Channel =>
- println("channel " + ch.id + " where " + Expr(ch.where) + Semi)
- }
- def Semi = ";"
- def Member(m: Member) = m match {
- case MonitorInvariant(e) =>
- print(" invariant "); Expr(e); println(Semi)
- case f@ Field(id, t, ghost) =>
- println(" " + (if (ghost) "ghost " else "") + "var " + id + ": " + t.FullName + Semi)
- case m: Method =>
- print(" method " + m.id)
- print("("); VarList(m.ins); print(")")
- if (m.outs != Nil) {
- print(" returns ("); VarList(m.outs); print(")")
- }
- println
- PrintSpec(m.Spec)
- println(" {")
- for (s <- m.body) {
- Spaces(4); Stmt(s, 4)
- }
- println(" }")
- case Condition(id, optE) =>
- print(" condition " + id)
- optE match {
- case None =>
- case Some(e) => print(" where "); Expr(e)
- }
- println(Semi)
- case Predicate(id, definition) =>
- print(" predicate " + id + " { "); Expr(definition); println(" }")
- case Function(id, ins, out, specs, e) =>
- print(" function " + id + "("); VarList(ins); print("): " + out.FullName);
- println
- PrintSpec(specs)
- e match {
- case Some(e) => print(" { "); Expr(e); println(" }");
- case None =>
- }
- case m: MethodTransform =>
- print(" method " + m.id);
- print("("); VarList(m.ins); print(")")
- if (m.outs != Nil) {
- print(" returns ("); VarList(m.outs); print(")")
- }
- println;
- if (m.refines != null) PrintSpec(m.Spec);
- println(" {");
- if (m.body == null)
- println(" // body transform is not resolved")
- else
- for (s <- m.body) {
- Spaces(4); Stmt(s, 4)
- }
- println(" }")
- case CouplingInvariant(ids, e) =>
- print(" replaces "); Commas(ids); print(" by "); Expr(e); println(Semi);
-
- }
- def PrintSpec(specs: List[Specification]) {
- specs foreach {
- case Precondition(e) => print(" requires "); Expr(e); println(Semi)
- case Postcondition(e) => print(" ensures "); Expr(e); println(Semi)
- case LockChange(ee) => print(" lockchange "); ExprList(ee); println(Semi)
- }
- }
- def Stmt(s: Statement, indent: Int): Unit = s match {
- case a@Assert(e) =>
- print("assert "); Expr(e);
- if (!a.smokeErrorNr.isEmpty)
- println(Semi + " // smoke assertion: " + SmokeTest.smokeWarningMessage(a.smokeErrorNr.get))
- else
- println(Semi)
- case Assume(e) =>
- print("assume "); Expr(e); println(Semi)
- case BlockStmt(ss) =>
- PrintBlockStmt(ss, indent); println
- case RefinementBlock(ss, old) =>
- println("/* begin of refinement block")
- for (s <- old) {
- Spaces(indent + 2); Stmt(s, indent + 2)
- }
- Spaces(indent); println("end of abstract code */")
- for (s <- ss) {
- Spaces(indent); Stmt(s, indent)
- }
- Spaces(indent); println("// end of refinement block")
- case IfStmt(guard, BlockStmt(thn), els) =>
- print("if ("); Expr(guard); print(") ")
- PrintBlockStmt(thn, indent)
- els match {
- case None => println
- case Some(s) => print(" else "); Stmt(s, indent)
- }
- case w @ WhileStmt(guard, _, _, lkch, body) =>
- print("while ("); Expr(guard); println(")")
- for (inv <- w.oldInvs) {
- Spaces(indent+2)
- print("invariant "); Expr(inv); println(Semi)
- }
- for (inv <- w.newInvs) {
- Spaces(indent+2)
- print("invariant "); Expr(inv); print(Semi); println(" // refined");
- }
- for (l <- lkch) {
- Spaces(indent+2)
- print("lockchange "); Expr(l); println(Semi)
- }
- Spaces(indent); Stmt(body, indent)
- case Assign(lhs,rhs) =>
- Expr(lhs); print(" := "); Rhs(rhs); println(Semi)
- case FieldUpdate(lhs,rhs) =>
- Expr(lhs); print(" := "); Rhs(rhs); println(Semi)
- case LocalVar(v,rhs) =>
- print(v + ": " + v.t.FullName)
- rhs match { case None => case Some(rhs) => print(" := "); Rhs(rhs) }
- println(Semi)
- case SpecStmt(lhs, locals, pre, post) =>
- if (locals.size > 0) {
- if (locals(0).isGhost) print("ghost ");
- if (locals(0).isImmutable) print("const ") else print("var ")
- } else
- print("var ");
- VarList(locals);
- var first = (locals.size == 0);
- for (l <- lhs)
- if (! locals.exists(v => v.id == l.id)) {
- if (first) first = false else print(", ");
- print(l.id);
- }
- print(" ["); Expr(pre); print(", "); Expr(post); print("]"); println(Semi);
- case Call(_, outs, obj, id, args) =>
- print("call ")
- outs match {
- case Nil =>
- case x :: xs => Expr(x); xs foreach { x => print(", "); Expr(x) }; print(" := ")
- }
- MemberSelect(obj,id,0,false)
- print("(")
- ExprList(args)
- println(");")
- case Install(obj,lower,upper) =>
- print("reorder ")
- Expr(obj)
- PrintBounds(lower, upper)
- println(Semi)
- case Share(obj,lower,upper) =>
- print("share ")
- Expr(obj)
- PrintBounds(lower, upper)
- println(Semi)
- case Unshare(e) =>
- print("unshare "); Expr(e); println(Semi)
- case Acquire(e) =>
- print("acquire "); Expr(e); println(Semi)
- case Release(e) =>
- print("release "); Expr(e); println(Semi)
- case RdAcquire(e) =>
- print("rd acquire "); Expr(e); println(Semi)
- case RdRelease(e) =>
- print("rd release "); Expr(e); println(Semi)
- case Lock(e, b, rdLock) =>
- if (rdLock) print("rd lock (") else print("lock (")
- Expr(e); print(") ")
- Stmt(b, indent)
- case Downgrade(e) =>
- print("downgrade "); Expr(e); println(Semi)
- case Free(e) =>
- print("free "); Expr(e); println(Semi)
- case Fold(e) =>
- print("fold "); Expr(e); println(Semi)
- case Unfold(e) =>
- print("unfold "); Expr(e); println(Semi)
- case CallAsync(declaresLocal, token, obj, name, args) =>
- print("fork ");
- if (token != null) {
- Expr(token); print(" := ");
- }
- Expr(obj); print("."); print(name); print("("); ExprList(args); print(")");
- case JoinAsync(lhs, token) =>
- print("join ");
- if (lhs != null && !lhs.isEmpty) {
- ExprList(lhs);
- print(" := ");
- }
- Expr(token);
- println(Semi)
- case Wait(obj, id) =>
- print("wait ")
- MemberSelect(obj, id, 0, false)
- println(Semi)
- case Signal(obj, id, all) =>
- print("signal "); if (all) { print(" forall") }
- MemberSelect(obj, id, 0, false)
- println(Semi)
- case Send(ch, args) =>
- print("send "); Expr(ch); print("("); ExprList(args); print(")"); println(Semi)
- case Receive(_, ch, outs) =>
- print("receive ")
- outs match {
- case Nil =>
- case x :: xs => Expr(x); xs foreach { x => print(", "); Expr(x) }; print(" := ")
- }
- Expr(ch); println(Semi)
- }
- def PrintBounds(lower: List[Expression], upper: List[Expression]) = {
- if (lower == Nil && upper == Nil) {
- } else if (lower == Nil) {
- print(" below "); ExprList(upper)
- } else if (upper == Nil) {
- print(" above "); ExprList(lower)
- } else {
- print(" between "); ExprList(lower); print(" and "); ExprList(upper)
- }
- }
- def PrintBlockStmt(ss: List[Statement], indent: Int) = {
- println("{")
- for (s <- ss) {
- Spaces(indent+2); Stmt(s, indent+2)
- }
- Spaces(indent); print("}")
- }
- def VarList(vv: List[Variable]) = Commas(vv map {v => v.id + ": " + v.t.FullName})
- def Commas(ss: List[String]) = ss match {
- case Nil =>
- case s :: rest =>
- print(s); rest foreach {s => print(", " + s)}
- }
- def ExprList(ee: List[Expression]) = ee match {
- case Nil =>
- case e :: rest =>
- Expr(e)
- rest foreach { e => print(", "); Expr(e) }
- }
- def Rhs(e: RValue) = e match {
- case NewRhs(id, initialization, lower, upper) =>
- print("new " + id);
- if(0 < initialization.length) {
- print(" {"); print(initialization(0).id); print(":="); Expr(initialization(0).e); initialization.foreach({ init => print(", "); print(init.id); print(":="); Expr(init.e); }); print("}");
- }
- PrintBounds(lower, upper)
- case e: Expression => Expr(e)
- }
- def Expr(e: Expression): Unit = Expr(e, 0, false)
- def Expr(e: Expression, contextBindingPower: Int, fragileContext: Boolean): Unit = e match {
- case BoogieExpr(_) => throw new InternalErrorException("unexpected in pretty printer")
- case IntLiteral(n) => print(n)
- case BoolLiteral(b) => print(b)
- case NullLiteral() => print("null")
- case StringLiteral(s) => print("\"" + s + "\"")
- case MaxLockLiteral() => print("waitlevel")
- case LockBottomLiteral() => print("lockbottom")
- case _:ThisExpr => print("this")
- case _:Result => print("result")
- case VariableExpr(id) => print(id)
- case MemberAccess(e,f) => MemberSelect(e,f,contextBindingPower,fragileContext)
- case Full => print("100");
- case Epsilon => print("rd");
- case MethodEpsilon => print("rd");
- case Frac(e) => Expr(e);
- case Star => print("rd(*)")
- case ChannelEpsilon(None) | PredicateEpsilon(None) | MonitorEpsilon(None) => print("rd");
- case ChannelEpsilon(Some(e)) => print("rd("); Expr(e); print(")");
- case PredicateEpsilon(Some(e)) => print("rd("); Expr(e); print(")");
- case MonitorEpsilon(Some(e)) => print("rd("); Expr(e); print(")");
- case ForkEpsilon(tk) => print("rd("); Expr(tk); print(")");
- case PermPlus(e0, e1) => BinExpr(e0, e1, "+", 0x50, false, false, contextBindingPower, fragileContext)
- case PermMinus(e0, e1) => BinExpr(e0, e1, "-", 0x50, false, true, contextBindingPower, fragileContext)
- case PermTimes(e0, e1) => BinExpr(e0, e1, "*", 0x60, false, false, contextBindingPower, fragileContext)
- case IntPermTimes(n, p) => BinExpr(n, p, "*", 0x60, false, false, contextBindingPower, fragileContext)
- case Epsilons(e) => print("rd("); Expr(e); print(")");
- case Access(e, p) => print("acc("); Expr(e); print(", "); Expr(p); print(")")
- case AccessAll(obj, p) => print("acc("); Expr(obj); print(".*"); print(", "); Expr(p); print(")")
- case AccessSeq(s, f, p) => print("acc("); Expr(s); print(", "); print("[*].");
- f match { case None => print("*"); case Some(x) => print(x)}
- Expr(p); print(")")
- case Credit(e, n) =>
- print("credit("); Expr(e)
- n match { case None => case Some(n) => print(", "); Expr(n) }
- print(")")
- case Holds(e) =>
- print("holds("); Expr(e); print(")")
- case RdHolds(e) =>
- print("rd holds("); Expr(e); print(")")
- case Assigned(id) => print("assigned(" + id + ")")
- case Old(e) =>
- print("old("); Expr(e); print(")")
- case IfThenElse(con, then, els) =>
- print("("); Expr(con); print(" ? "); Expr(then); print(" : "); Expr(els); print(")");
- case Not(e) => print("!"); Expr(e, 0x80, false)
- case FunctionApplication(obj, id, ins) =>
- Expr(obj); print("."); print(id); print("("); ExprList(ins); print(")");
- case Unfolding(pred, e) =>
- print("unfolding "); Expr(pred); print(" in "); Expr(e);
- case e:Iff => BinExpr(e, e.OpName, 0x10, false, false, contextBindingPower, fragileContext)
- case e:Implies => BinExpr(e, e.OpName, 0x20, true, false, contextBindingPower, fragileContext)
- case e:And => BinExpr(e, e.OpName, 0x30, false, false, contextBindingPower, fragileContext)
- case e:Or => BinExpr(e, e.OpName, 0x31, false, false, contextBindingPower, fragileContext)
- case e:Eq => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
- case e:Neq => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
- case e:Less => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
- case e:AtMost => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
- case e:AtLeast => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
- case e:Greater => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
- case e:LockBelow => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
- case e:Plus => BinExpr(e, e.OpName, 0x50, false, false, contextBindingPower, fragileContext)
- case e:Minus => BinExpr(e, e.OpName, 0x50, false, true, contextBindingPower, fragileContext)
- case e:Times => BinExpr(e, e.OpName, 0x60, false, false, contextBindingPower, fragileContext)
- case e:Div => BinExpr(e, e.OpName, 0x60, false, true, contextBindingPower, fragileContext)
- case e:Mod => BinExpr(e, e.OpName, 0x60, false, true, contextBindingPower, fragileContext)
- case q:Quantification =>
- print("(" + (q.Q match {case Forall => "forall"; case Exists => "exists"}) + " ");
- q.Is match {
- case Nil =>
- case i :: rest => print(i); rest foreach { v => print(", " + v) }
- }
- q match {
- case q: SeqQuantification => print(" in "); Expr(q.seq);
- case q: TypeQuantification => print(": "); print(q.t.typ.FullName);
- }
- print(" :: "); Expr(q.E); print(")");
- case EmptySeq(t) =>
- print("nil<"); print(t.FullName); print(">");
- case ExplicitSeq(es) =>
- print("["); ExprList(es); print("]");
- case Range(min, max) =>
- print("["); Expr(min); print(":"); Expr(max); print("]");
- case Length(e)=>
- print("|"); Expr(e); print("|");
- case At(s, n) =>
- Expr(s); print("["); Expr(n); print("]");
- case e:Append =>
- BinExpr(e, e.OpName, 0x45, true, true, contextBindingPower, fragileContext)
- case Drop(s, n) =>
- Expr(s); print("["); Expr(n); print(" ..]");
- case Take(s, n) =>
- Expr(s); print("[.. "); Expr(n); print("]");
- case e:Contains => BinExpr(e, e.OpName, 0x40, true, true, contextBindingPower, fragileContext)
- case Eval(h, e) =>
- print("eval("); (h match
- {
- case AcquireState(obj) => Expr(obj); print(".acquire");
- case ReleaseState(obj) => Expr(obj); print(".release");
- case CallState(token, obj, id, args) => Expr(token); print(".fork"); print(" "); Expr(obj); print("." + id + "("); ExprList(args); print(")");
- }); print(", "); Expr(e); print(")");
- }
- def MemberSelect(e: Expression, f: String, contextBindingPower: Int, fragileContext: Boolean) = e match {
- case e:ImplicitThisExpr => print(f)
- case _ =>
- ParenExpr(0x90, contextBindingPower, fragileContext, { Expr(e,0x90,false); print("." + f) })
- }
- def BinExpr(bin: BinaryExpr, op: String, power: Int, fragileLeft: Boolean, fragileRight: Boolean,
- context: Int, fragileContext: Boolean) = {
- ParenExpr(power, context, fragileContext,
- { Expr(bin.E0, power, fragileLeft); print(" " + op + " "); Expr(bin.E1, power, fragileRight) })
- }
- def BinExpr(left: Expression, right: Expression, op: String, power: Int, fragileLeft: Boolean, fragileRight: Boolean,
- context: Int, fragileContext: Boolean) = {
- ParenExpr(power, context, fragileContext,
- { Expr(left, power, fragileLeft); print(" " + op + " "); Expr(right, power, fragileRight) })
- }
- def ParenExpr(power: Int, context: Int, fragileContext: Boolean, pe: =>Unit) {
- val ap = power & 0xF0;
- val cp = context & 0xF0;
- val parensNeeded = ap < cp || (ap == cp && (power != context || fragileContext));
- if (parensNeeded) { print("(") }
- pe
- if (parensNeeded) { print(")") }
- }
- def Spaces(N: Int) = {
- val abunchaSpaces = " "
- var n = N
- while (abunchaSpaces.length <= n) {
- print(abunchaSpaces)
- n = n - abunchaSpaces.length
- }
- if (0 < n) {
- print(abunchaSpaces.substring(0, n))
- }
- }
-}
|