001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.pa;
004
005 import escjava.*;
006 import escjava.prover.*;
007 import java.io.*;
008
009 import javafe.util.Set;
010 import javafe.ast.*;
011 import escjava.ast.*;
012 import escjava.ast.TagConstants;
013 import escjava.translate.*;
014
015 import javafe.util.Location;
016 import javafe.util.Assert;
017
018 public class Traverse
019 {
020 public static void compute(GuardedCmd g, InitialState initState, Translate tr) {
021 ProverManager.push(initState.getInitialState());
022 /*
023 PrintStream ps = Main.prover.subProcessToStream();
024 ps.print("\n(BG_PUSH ");
025 VcToString.compute(initState.getInitialState(), ps);
026 ps.println(")");
027 Main.prover.sendCommands("");
028 */
029 Set env = new Set();
030 GuardedCmd h = computeHelper(g, GC.skip(), env);
031 ProverManager.pop();
032 //Main.prover.sendCommand("(BG_POP)");
033 desugarLoops(g, tr);
034 }
035
036 private static void desugarLoops(GuardedCmd g, Translate tr) {
037 switch (g.getTag()) {
038 case TagConstants.SKIPCMD:
039 case TagConstants.RAISECMD:
040 case TagConstants.ASSERTCMD:
041 case TagConstants.ASSUMECMD:
042 case TagConstants.GETSCMD:
043 case TagConstants.SUBGETSCMD:
044 case TagConstants.SUBSUBGETSCMD:
045 case TagConstants.RESTOREFROMCMD:
046 return;
047 case TagConstants.CALL: {
048 desugarLoops(((Call) g).desugared, tr);
049 return;
050 }
051 case TagConstants.VARINCMD: {
052 desugarLoops(((VarInCmd) g).g, tr);
053 return;
054 }
055 case TagConstants.DYNINSTCMD: {
056 desugarLoops(((DynInstCmd) g).g, tr);
057 return;
058 }
059 case TagConstants.SEQCMD: {
060 SeqCmd sc = (SeqCmd) g;
061 for (int i = 0; i < sc.cmds.size(); i++) {
062 desugarLoops(sc.cmds.elementAt(i), tr);
063 }
064 return;
065 }
066 case TagConstants.TRYCMD: {
067 CmdCmdCmd tc = (CmdCmdCmd)g;
068 desugarLoops(tc.g1, tr);
069 desugarLoops(tc.g2, tr);
070 return;
071 }
072 case TagConstants.CHOOSECMD: {
073 CmdCmdCmd tc = (CmdCmdCmd)g;
074 desugarLoops(tc.g1, tr);
075 desugarLoops(tc.g2, tr);
076 return;
077 }
078 case TagConstants.LOOPCMD: {
079 LoopCmd loop = (LoopCmd) g;
080 PredicateAbstraction pa = (PredicateAbstraction) PredicateAbstraction.paDecoration.get(loop);
081 Assert.notNull(pa);
082
083 ExprVec invs = pa.invariants;
084
085 System.out.println("Loop invariant at "+
086 Location.toString( loop.getStartLoc() )+
087 ", " + invs.size() +" invariants, "+
088 pa.milliSecsUsed+" ms, "+
089 pa.perfCount.report() +" = "
090 );
091
092 for(int i=0; i<invs.size(); i++) {
093 Expr inv = invs.elementAt(i);
094 System.out.println(" "+PrettyPrint.inst.toString(inv));
095 Condition cond = GC.condition(TagConstants.CHKLOOPINVARIANT,
096 inv,
097 loop.getStartLoc());
098 loop.invariants.addElement(cond);
099 }
100
101 // System.out.println("Loop invariant compact: "+pa.set.concretize2());
102 //System.out.println("Loop invariant as expr: "+PrettyPrint.inst.toString(pa.set.get()));
103
104
105 tr.desugarLoopSafe(loop,ExprVec.make());
106 desugarLoops(loop.desugared, tr);
107 return;
108 }
109
110 default:
111 //@ unreachable;
112 Assert.fail("Fall through on "+g);
113 return;
114 }
115 }
116
117 static /*@ non_null @*/ GuardedCmd computeHelper(/*@ non_null @*/ GuardedCmd g,
118 GuardedCmd context, Set env)
119 {
120 switch (g.getTag()) {
121 case TagConstants.SKIPCMD:
122 case TagConstants.RAISECMD:
123 case TagConstants.ASSERTCMD:
124 case TagConstants.ASSUMECMD:
125 case TagConstants.GETSCMD:
126 case TagConstants.SUBGETSCMD:
127 case TagConstants.SUBSUBGETSCMD:
128 case TagConstants.RESTOREFROMCMD:
129 return g;
130
131 case TagConstants.CALL:
132 {
133 Call call = (Call)g;
134 return computeHelper( call.desugared, context, env );
135 }
136
137 case TagConstants.VARINCMD:
138 {
139 VarInCmd vc = (VarInCmd)g;
140 Set env2 = new Set(env.elements());
141 for(int i=0; i<vc.v.size(); i++) {
142 env2.add(vc.v.elementAt(i));
143 }
144 return VarInCmd.make(vc.v, computeHelper(vc.g, context, env2));
145 }
146
147 case TagConstants.DYNINSTCMD:
148 {
149 DynInstCmd dc = (DynInstCmd)g;
150 return DynInstCmd.make(dc.s, computeHelper(dc.g, context, env));
151 }
152
153 case TagConstants.SEQCMD:
154 {
155 SeqCmd sc = (SeqCmd)g;
156 GuardedCmd t = GC.skip();
157 for (int i = 0; i < sc.cmds.size(); i++) {
158 GuardedCmd r = computeHelper(sc.cmds.elementAt(i), GC.seq(context, t), env);
159 t = GC.seq(t, r);
160 }
161 return t;
162 }
163
164 case TagConstants.TRYCMD:
165 {
166 CmdCmdCmd tc = (CmdCmdCmd)g;
167 GuardedCmd t1 = computeHelper(tc.g1, context, env);
168 GuardedCmd t2 = computeHelper(tc.g2, GC.seq(context, GC.trycmd(GC.seq(t1, GC.fail()), GC.skip())), env);
169 return GC.trycmd(t1, t2);
170 }
171
172 case TagConstants.CHOOSECMD:
173 {
174 CmdCmdCmd cc = (CmdCmdCmd)g;
175 return GC.choosecmd(computeHelper(cc.g1, context, env), computeHelper(cc.g2, context, env));
176 }
177
178 case TagConstants.LOOPCMD:
179 {
180 LoopCmd lp = (LoopCmd)g;
181 return PredicateAbstraction.abstractLoop( lp, context, env );
182 }
183
184 default:
185 //@ unreachable;
186 Assert.fail("Fall through on "+g);
187 return null;
188 }
189 }
190 }