    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    }