    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.sp;
    004
    005    import escjava.translate.GC;
    006    import java.util.Hashtable;
    007    import java.util.Enumeration;
    008
    009    import javafe.ast.*;
    010    import escjava.ast.*;
    011    import escjava.ast.TagConstants;
    012
    013    import javafe.util.Location;
    014    import javafe.util.Assert;
    015    import javafe.util.Set;
    016
    017    import escjava.Main;
    018
    019    class NXW
    020    {
    021        /* predicate for normal, exceptional, and wrong outcomes of a command */
    022        public Expr n,x,w;
    023    }
    024
    025    public class SPVC
    026    {
    027        public static Expr compute(GuardedCmd g) {
    028            SPVC spvc = new SPVC();
    029            return spvc.computeNotWrong(g);
    030        }
    031
    032        private Hashtable cache = new Hashtable();
    033        private Set cacheHit = new Set();
    034        private DefPredVec preds = DefPredVec.make();
    035        private static int predNum = 0;
    036
    037        private Expr name(Expr e) {
    038            if( Main.options().useDefpred && Util.size(e) >= Main.options().namePCsize) {
    039                Identifier predId = Identifier.intern("PREDN"+predNum);
    040                predNum++;
    041                preds.addElement( DefPred.make( predId, GenericVarDeclVec.make(), e ));
    042                return DefPredApplExpr.make( predId, ExprVec.make() );
    043            } else {
    044                return e;
    045            }
    046        }
    047
    048        private Expr computeNotWrong(GuardedCmd root) {
    049            Expr r = GC.nary(TagConstants.BOOLNOT, calcNxw(root).w);
    050            if( Main.options().useDefpred ) {
    051                return DefPredLetExpr.make( preds, r);
    052            } else {
    053                return r;
    054            }
    055        }
    056
    057        public static Expr computeN(GuardedCmd g) {
    058            SPVC spvc = new SPVC();
    059            return spvc.calcNxw(g).n;
    060        }
    061
    062        private NXW calcNxw(GuardedCmd g) {
    063
    064            NXW nxw = (NXW)cache.get(g);
    065            if (nxw != null) {
    066                cacheHit.add(g);
    067                return nxw;
    068            }
    069            nxw = new NXW();
    070
    071            switch (g.getTag()) {
    072                case TagConstants.SKIPCMD:
    073                    /* norm(skip) == true
    074                     exc(skip) == false
    075                     wrong(skip) == false
    076                     */
    077                    nxw.n = GC.truelit;
    078                    nxw.x = GC.falselit;
    079                    nxw.w = GC.falselit;
    080                    break;
    081
    082                case TagConstants.RAISECMD:
    083                    /* norm(raise) == false
    084                     exc(raise) == true
    085                     wrong(raise) == false
    086                     */
    087                    nxw.n = GC.falselit;
    088                    nxw.x = GC.truelit;
    089                    nxw.w = GC.falselit;
    090                    break;
    091
    092                case TagConstants.ASSERTCMD:
    093                    /* norm(assert E) == E
    094                     exc(assert E) == false
    095                     wrong(assert E) == !E
    096                     */
    097                    {
    098                        ExprCmd ec = (ExprCmd)g;
    099                        if (Main.options().strongAssertPost == 2 ||
    100                            (Main.options().strongAssertPost == 1 && isSimpleConjunction(ec.pred))) {
    101                            nxw.n = ec.pred;
    102                        } else {
    103                            nxw.n = GC.truelit;
    104                        }
    105                        nxw.x = GC.falselit;
    106                        nxw.w = GC.nary(TagConstants.BOOLNOT, ec.pred);
    107                        break;
    108                    }
    109
    110                case TagConstants.ASSUMECMD:
    111                    /* norm(assume E) == E
    112                     exc(assume E) == false
    113                     wrong(assume E) == false
    114                     */
    115                    {
    116                        ExprCmd ec = (ExprCmd)g;
    117                        nxw.n = ec.pred;
    118                        nxw.x = GC.falselit;
    119                        nxw.w = GC.falselit;
    120                        break;
    121                    }
    122
    123                case TagConstants.CHOOSECMD:
    124                    /* norm(A [] B) == norm(A) | norm(B)
    125                     exc(A [] B) == exc(A) | exc(B)
    126                     wrong(A [] B) == wrong(A) | wrong(B)
    127                     */
    128                    {
    129                        CmdCmdCmd cc = (CmdCmdCmd)g;
    130                        NXW a = calcNxw(cc.g1);
    131                        NXW b = calcNxw(cc.g2);
    132                        nxw.n = GC.or(a.n, b.n);
    133                        nxw.x = GC.or(a.x, b.x);
    134                        nxw.w = GC.or(a.w, b.w);
    135                        break;
    136                    }
    137
    138                case TagConstants.TRYCMD:
    139                    /* norm(A ! B) == norm(A) | (exc(A) & norm(B )
    140                     exc(A ! B) == exc(A) & exc(B)
    141                     wrong(A ! B) == wrong(A) | (exc(A) & wrong(B))
    142                     */
    143                    {
    144                        CmdCmdCmd cc = (CmdCmdCmd)g;
    145                        NXW a = calcNxw(cc.g1);
    146                        NXW b = calcNxw(cc.g2);
    147                        Expr ax = name(a.x);
    148                        nxw.n = GC.or(a.n, GC.and(ax, b.n));
    149                        nxw.x = GC.and(ax, b.x);
    150                        nxw.w = GC.or(a.w, GC.and(ax, b.w));
    151                        break;
    152                    }
    153
    154                case TagConstants.SEQCMD:
    155                    /* norm(A ; B) == norm(A) & norm(B)
    156                     exc(A ; B) == exc(A) | (norm(A) & exc(B))
    157                     wrong(A ; B) == wrong(A) | (norm(A) & wrong(B))
    158                     */
    159                    {
    160                        SeqCmd sc = (SeqCmd)g;
    161
    162                        nxw.n = GC.truelit;
    163                        nxw.x = GC.falselit;
    164                        nxw.w = GC.falselit;
    165
    166
    167                        for (int i = sc.cmds.size() -1; 0 <= i; i--) {
    168                            NXW temp = calcNxw(sc.cmds.elementAt(i));
    169                            Expr tempn = name(temp.n);
    170                            Expr n = GC.and(tempn, nxw.n);
    171                            Expr x = GC.or(temp.x, GC.and(tempn, nxw.x));
    172                            Expr w = GC.or(temp.w, GC.and(tempn, nxw.w));
    173                            nxw.n = n;
    174                            nxw.x = x;
    175                            nxw.w = w;
    176                        }
    177                        break;
    178                    }
    179
    180                default:
    181                    //@ unreachable;
    182                    Assert.fail("Fall thru on "+g);
    183                    return null;
    184            }
    185
    186            cache.put(g, nxw);
    187            return nxw;
    188
    189        }
    190
    191        public static boolean isSimpleConjunction(Expr e) {
    192            if (e instanceof NaryExpr) {
    193                NaryExpr ne = (NaryExpr)e;
    194                if (ne.op == TagConstants.BOOLAND || ne.op == TagConstants.BOOLANDX) {
    195                    for (int i = 0; i < ne.exprs.size(); i++) {
    196                        if (! isSimpleExpr(ne.exprs.elementAt(i))) {
    197                            return false;
    198                        }
    199                    }
    200                    return true;
    201                }
    202            }
    203            return isSimpleExpr(e);
    204        }
    205
    206        private static boolean isSimpleExpr(Expr e) {
    207            switch (e.getTag()) {
    208                case TagConstants.LABELEXPR:
    209                    {
    210                        LabelExpr le = (LabelExpr)e;
    211                        return isSimpleExpr(le.expr);
    212                    }
    213
    214                case TagConstants.GUARDEXPR:
    215                    {
    216                        GuardExpr ge = (GuardExpr)e;
    217                        return isSimpleExpr(ge.expr);
    218                    }
    219
    220                case TagConstants.FORALL:
    221                case TagConstants.EXISTS:
    222                    return false;
    223
    224                case TagConstants.TYPEEXPR:
    225                case TagConstants.LOCKSETEXPR:
    226                case TagConstants.RESEXPR:
    227                case TagConstants.WILDREFEXPR:
    228                case TagConstants.ARRAYRANGEREFEXPR:
    229                case TagConstants.THISEXPR:
    230                case TagConstants.CLASSLITERAL:
    231
    232                case TagConstants.BOOLEANLIT:
    233                case TagConstants.CHARLIT:
    234                case TagConstants.DOUBLELIT:
    235                case TagConstants.FLOATLIT:
    236                case TagConstants.INTLIT:
    237                case TagConstants.LONGLIT:
    238                case TagConstants.NULLLIT:
    239                case TagConstants.STRINGLIT:
    240                case TagConstants.SYMBOLLIT:
    241
    242                case TagConstants.VARIABLEACCESS:
    243                    return true;
    244
    245                case TagConstants.BOOLAND:
    246                case TagConstants.BOOLANDX:
    247                case TagConstants.BOOLOR:
    248                case TagConstants.DTTFSA:
    249                    return false;
    250
    251                case TagConstants.SUBSTEXPR:
    252                    { SubstExpr se = (SubstExpr)e ;
    253                        return isSimpleExpr(se.target) && isSimpleExpr(se.val) ;
    254                    }
    255
    256                default:
    257                    {
    258                        if (e instanceof NaryExpr) {
    259                            NaryExpr ne = (NaryExpr)e;
    260                            for (int i = 0; i < ne.exprs.size(); i++) {
    261                                if (! isSimpleExpr(ne.exprs.elementAt(i))) {
    262                                    return false;
    263                                }
    264                            }
    265                            return true;
    266                        } else {
    267                            Assert.fail("Unexpected expr in SPVC.isSimpleExpr: "+e);
    268                            return false; // dummy return
    269                        }
    270                    }
    271            }
    272        }
    273    }