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 }