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    }