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    }