001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.pa;
004    
005    import java.util.Hashtable;
006    import java.util.Enumeration;
007    import java.util.Vector;
008    import java.io.*;
009    
010    import javafe.ast.*;
011    import javafe.util.Set;
012    import javafe.util.Location;
013    import javafe.util.Assert;
014    import javafe.util.StackVector;
015    import javafe.tc.Types;
016    
017    import escjava.*;
018    import escjava.ast.*;
019    import escjava.ast.TagConstants;
020    import escjava.ast.Modifiers;
021    import escjava.translate.*;
022    import escjava.sp.SPVC;
023    import escjava.sp.*;
024    import escjava.prover.*;
025    import escjava.pa.generic.*;
026    
027    import mocha.wrappers.jbdd.*;
028    
029    public class PredicateAbstraction
030    {
031        public static /*@ non_null @*/ ASTDecoration paDecoration = new ASTDecoration("paDecoration");
032        
033        static GuardedCmd abstractLoop(LoopCmd g, GuardedCmd context, Set env) {
034            PredicateAbstraction pa = (PredicateAbstraction) paDecoration.get(g);   
035            if (pa == null) {
036                pa = new PredicateAbstraction(g, env);
037                paDecoration.set(g, pa);
038            }
039            return pa.abstractLoopHelper(context, env);
040        }
041    
042        private static boolean quantifyAssumptions = 
043            !Boolean.getBoolean("PAnoQuantifyAssumptions");
044        ExprVec invariants = ExprVec.make();
045        private /*@ non_null @*/ jbddManager bddManager;
046        public  /*@ non_null @*/ Abstractor abstractor;
047        private /*@ non_null @*/ LocalVarDeclVec skolemConstants;
048        private /*@ non_null @*/ ExprVec loopPredicates;
049        private GuardedCmd body;
050        private /*@ non_null @*/ GuardedCmd bodyDesugared = GC.fail();
051        private GuardedCmd havoc;
052        private int startLoc;
053        public int nQueries=0;
054        long milliSecsUsed;
055        GCProver perfCount;
056        
057        private final /*@ non_null @*/ StackVector code = new StackVector();
058        private final /*@ non_null @*/ GenericVarDeclVec temporaries = GenericVarDeclVec.make();
059    
060        PredicateAbstraction(/*@ non_null @*/ LoopCmd g, Set env) {
061    
062            body = GC.seq(g.guard, g.body);
063            startLoc = g.getStartLoc();
064    
065            Set vds = Targets.normal(body);
066    
067            if( Main.options().inferPredicates ) {
068                //System.out.println("Before inf: "+g.predicates);
069                inferPredicates(g, env, vds);
070                //System.out.println("After inf: "+g.predicates);
071            }
072            
073            this.skolemConstants = g.skolemConstants;
074            this.loopPredicates = g.predicates;
075            this.bddManager = new jbddManager( loopPredicates.size() );
076    
077            if( System.getProperty("PABDT") != null ) {
078                this.abstractor = new BinaryDecisionTreeAbstractor(bddManager);
079            } else if( System.getProperty("PA3n") != null ) {
080                this.abstractor = new EnumClausesAbstractor(bddManager);
081            } else if( System.getProperty("PANK") != null ) {
082                this.abstractor = new EnumNFindK(bddManager,
083                                                 Integer.parseInt(System.getProperty("PANK")));
084            } else {
085                this.abstractor = new EnumMaxClausesFindMinAbstractor(bddManager);
086            }
087    
088            code.push();
089    
090            Translate translate = (new Translate());
091            GuardedCmd modifyGc = translate.modify(vds, g.locStart);
092    
093            if( Main.options().preciseTargets ) {
094                Set aTargets = ATarget.compute( VarInCmd.make(g.tempVars, g ));
095                modifyGc = translate.modifyATargets( aTargets, g.getStartLoc());
096            }
097    
098            code.addElement(modifyGc);
099    
100            for (Enumeration e = vds.elements(); e.hasMoreElements();) {
101                GenericVarDecl vd = (GenericVarDecl)e.nextElement();
102                
103                if (!vd.id.toString().endsWith("@init")) {
104                    code.addElement(GC.assume(TrAnExpr.targetTypeCorrect(vd, g.oldmap)));
105                }
106            }
107            
108            for (int i = 0; i < g.invariants.size(); i++) {
109                Condition cond = g.invariants.elementAt(i);
110                code.addElement(GC.assume(cond.pred));
111            }
112    
113            havoc = GC.seq(GuardedCmdVec.popFromStackVector(code));
114        }
115    
116        private GuardedCmd abstractLoopHelper(GuardedCmd context, Set env) {
117            int step = 0;
118            milliSecsUsed -= java.lang.System.currentTimeMillis();
119    
120            code.push();
121            for(int j=0; j<skolemConstants.size();j++) {
122                LocalVarDecl sc = skolemConstants.elementAt(j);
123                code.addElement(GC.assume(TrAnExpr.typeAndNonNullCorrectAs(sc, sc.type, null, true, null)));
124            }
125            context = GC.seq( context, 
126                              GC.seq( GuardedCmdVec.popFromStackVector(code)));
127    
128    
129            System.out.println("Step " + step + ": Computing for loop at "
130                               +Location.toString( startLoc )
131                               +" num preds = "+loopPredicates.size()
132                               + "....");
133    
134            perfCount = new GCProver(bddManager, loopPredicates, GC.skip(), null);
135            
136            GCProver p = new GCProver(bddManager, loopPredicates, context, null);
137            boolean atfixpoint = abstractor.union(p);
138            p.done();
139            perfCount.addPerfCounters(p);
140    
141            System.out.println("  reachable size: "+p.size(abstractor.get()));
142            
143            while (!atfixpoint) {
144                ExprVec invs = p.concretize(abstractor.getClauses());
145    
146                if( quantifyAssumptions ) {
147                    invs = skolemQuantInvariants(skolemConstants, invs,
148                                                 Location.NULL, Location.NULL);
149                }
150    
151                System.out.println("Step " + ++step + ": Computing....");
152                GuardedCmd c = GC.seq( context, havoc, 
153                                       GC.assume(GC.and(invs)));
154                // from shaz
155                // c = GC.seq( context, havoc, GC.assume(e) );
156                milliSecsUsed += java.lang.System.currentTimeMillis();
157                bodyDesugared = Traverse.computeHelper(body, c, env);       
158                milliSecsUsed -= java.lang.System.currentTimeMillis();
159    
160                if( Main.options().pgc ) {
161                    System.out.println("\n**** Guarded Command c:");
162                    ((EscPrettyPrint)PrettyPrint.inst).print(System.out, 0, c);
163                    System.out.println("");
164                    System.out.println("\n**** Guarded Command body:");
165                    ((EscPrettyPrint)PrettyPrint.inst).print(System.out, 0, body);
166                    System.out.println("");
167                    System.out.println("\n**** Guarded Command bodyDesugared:");
168                    ((EscPrettyPrint)PrettyPrint.inst).print(System.out, 0, bodyDesugared);
169                    System.out.println("");
170                }
171                p = new GCProver(bddManager, loopPredicates, GC.seq(c, bodyDesugared), p);
172                atfixpoint = abstractor.union(p);
173                p.done();
174                perfCount.addPerfCounters(p);
175    
176                System.out.println("  reachable size: "+p.size(abstractor.get()));
177            }
178    
179            invariants = skolemQuantInvariants(skolemConstants,
180                                               p.concretize(abstractor.getClauses()),
181                                               Location.NULL,
182                                               Location.NULL);
183    
184            milliSecsUsed += java.lang.System.currentTimeMillis();
185            System.out.println("Finished loop at "
186                               +Location.toString( startLoc ) );
187            return VarInCmd.make(temporaries, 
188                                 GC.seq(havoc, 
189                                        GC.assume(GC.and(invariants)),
190                                        bodyDesugared,
191                                        GC.fail()));
192        }
193    
194        public static ExprVec skolemQuantInvariants(LocalVarDeclVec skolemConstants,
195                                                    ExprVec invs,
196                                                    int sloc, int eloc) {
197                                      
198            // Now, assume the inferred invariants at the beginning of the loop,
199            // universally quantified by the skolem constants
200                
201            ExprVec r = ExprVec.make();
202    
203            for(int i=0; i<invs.size(); i++) {
204                Expr inv = invs.elementAt(i);
205                
206                GenericVarDeclVec decls = GenericVarDeclVec.make();
207                ExprVec ttc = ExprVec.make();
208                for(int j=0; j<skolemConstants.size();j++) {
209                    LocalVarDecl sc = skolemConstants.elementAt(j);
210                    if( mentions( inv, sc ) ) {
211                        decls.addElement(sc);
212                        ttc.addElement( TrAnExpr.typeAndNonNullCorrectAs(sc, sc.type, null, true, null) );
213                    }
214                }
215    
216                Expr f = GC.quantifiedExpr( sloc, eloc,
217                                            TagConstants.FORALL,
218                                            decls,
219                                            GC.truelit,
220                                            GC.implies( GC.and( ttc ),
221                                                        inv ),
222                                                null, null );
223                r.addElement( f );
224            }
225            
226            return r;
227        }
228    
229        private static boolean mentions(/*@ non_null @*/ Expr e, GenericVarDecl d) {
230            if( e instanceof VariableAccess ) {
231                return ((VariableAccess)e).decl == d;
232            } else {
233                for(int i=0; i<e.childCount(); i++) {
234                    Object c = e.childAt(i);
235                    if( c instanceof Expr && mentions((Expr)c,d) ) {
236                        return true;
237                    }
238                }
239                return false;
240            }
241        }
242    
243    /* Unused.
244        private void inferPredicatesOld(LoopCmd g, Set env, Set targets) {
245            Set t = new Set(targets.elements());
246            t.intersect(env);
247    
248            for (Enumeration e = t.elements(); e.hasMoreElements();) {
249                GenericVarDecl vd = (GenericVarDecl)e.nextElement();
250                if( vd.type != null ) {
251                    if( escjava.tc.Types.isIntegralType( vd.type ) ) {
252                        // guess vd >= 0
253                        ExprVec vec = ExprVec.make();
254                        int loc = g.getStartLoc();
255                        vec.addElement( VariableAccess.make(vd.id, loc, vd) );
256                        vec.addElement( LiteralExpr.make( TagConstants.INTLIT,
257                                                                       new Integer(0),
258                                                                       loc ));
259                        
260                        Expr pred = NaryExpr.make( loc, loc, TagConstants.INTEGRALGE, null, vec );
261                        g.predicates.addElement( pred );
262                    }
263    
264                    if ( escjava.tc.Types.isReferenceType( vd.type ) ) {
265                        // guess vd != null
266                        ExprVec vec = ExprVec.make();
267                        int loc = g.getStartLoc();
268                        vec.addElement( VariableAccess.make(vd.id, loc, vd) );
269                        vec.addElement( LiteralExpr.make( TagConstants.NULLLIT,
270                                                                       null,
271                                                                       loc ));
272                        
273                        Expr pred = NaryExpr.make( loc, loc, TagConstants.REFNE, null, vec );
274                        g.predicates.addElement( pred );                
275                    }
276                }
277            }
278        }
279    */
280    
281        private void inferPredicates(/*@ non_null @*/ LoopCmd g, 
282                                     /*@ non_null @*/ Set env, 
283                                     Set targets) 
284        {
285            int loc = g.getStartLoc();
286    
287            LocalVarDecl sc = LocalVarDecl.make(Modifiers.NONE, null, Identifier.intern("sc"),
288                                                Types.intType, loc, null, loc);
289    
290            boolean useSC = false;
291            ExprVec boundsSC = ExprVec.make();
292            VariableAccess sca = VariableAccess.make(sc.id, loc, sc);
293    
294            //System.out.println("Getting targets for : "+g);
295            Set t = ATarget.compute(g); 
296            //System.out.println("Targets: "+t);
297            
298    
299            // predicates based on environment
300          outerLoop:
301            for (Enumeration e = env.elements(); e.hasMoreElements();) {
302                GenericVarDecl vd = (GenericVarDecl)e.nextElement();
303                if( vd.id.toString().indexOf('@') != -1 ) {
304                    // not a user var
305                    continue;
306                }
307                for (Enumeration e2 = t.elements(); e2.hasMoreElements();) {
308                    ATarget at = (ATarget)e2.nextElement();
309                    if( at.x == vd ) {
310                        // a target; will deal with below
311                        continue outerLoop;
312                    }
313                }
314                if( vd.type != null ) {
315                    if( escjava.tc.Types.isIntegralType( vd.type ) ) {
316                        // guess sc < vd
317                        boundsSC.addElement( GC.nary( loc, loc, TagConstants.INTEGRALLT,
318                                                      sca,
319                                                      VariableAccess.make(vd.id, loc, vd)));
320                    }
321                }
322            }
323    
324            for (Enumeration e = t.elements(); e.hasMoreElements();) {
325                ATarget at = (ATarget)e.nextElement();
326                VariableAccess va = VariableAccess.make( at.x.id, Location.NULL, at.x );
327                Expr vaOld = (Expr)g.oldmap.get(at.x);
328                
329                switch( at.indices.length ) {
330                  case 0:
331                    {
332                        if( at.x.type != null ) {
333                            guessPredicate( va, vaOld, at.x.type, g.predicates, loc, sca, boundsSC);
334                        }
335                    }
336                    break;
337    
338                  case 1:
339                    {
340                        if( at.x instanceof FieldDecl && at.x.type != null && at.indices[0] != null ) {
341                            guessPredicate( GC.select( va, at.indices[0]),
342                                            GC.select( vaOld, at.indices[0]),
343                                            at.x.type, g.predicates, loc, sca, boundsSC);
344                        }
345                    }
346                    break;
347    
348                  case 2:
349                    { // elems[..][..]
350                        if( at.indices[0] != null ) {
351                            Type type = null;
352                            switch( at.indices[0].getTag() ) {
353                                case TagConstants.VARIABLEACCESS:
354                                    {
355                                        GenericVarDecl vd = ((VariableAccess)at.indices[0]).decl;
356                                        if( vd.type != null ) {
357                                            Assert.notFalse( vd.type instanceof ArrayType );
358                                            type = ((ArrayType)vd.type).elemType;
359                                        }
360                                    }
361                                    break;
362    
363                              case TagConstants.SELECT:
364                                  {
365                                      NaryExpr ne = (NaryExpr)at.indices[0];
366                                      Expr arg0 = ne.exprs.elementAt(0);
367                                      if( arg0 instanceof VariableAccess ) {
368                                          GenericVarDecl vd = ((VariableAccess)arg0).decl;
369                                          if( vd.type != null ) {
370                                              Assert.notFalse( vd.type instanceof ArrayType );
371                                              type = ((ArrayType)vd.type).elemType;
372                                          }
373                                      }
374                                  }
375                                  break;
376                            }
377    
378                            if( type != null ) {
379                                Expr index;
380                                if(at.indices[1] == null ) {
381                                    index = sca;
382                                    useSC = true;
383                                } else {
384                                    index = at.indices[1];
385                                }
386                                guessPredicate( GC.select( GC.select( va, at.indices[0]), index),
387                                                null,
388                                                type, g.predicates, loc, sca, boundsSC);
389                            }
390                        }
391                    }
392                    break;
393                }
394            }
395    
396            if( useSC ) {
397                    g.skolemConstants.addElement(sc);
398                    // guess sc >= 0
399                    g.predicates.addElement( GC.nary( loc, loc, TagConstants.INTEGRALGE, sca,
400                                                      LiteralExpr.make(TagConstants.INTLIT, new Integer(0),
401                                                                       loc) ) );
402                    g.predicates.append(boundsSC);
403            }
404        }
405    
406        private void guessPredicate( Expr e, Expr eOld, Type type, 
407                                     ExprVec predicates, int loc, 
408                                     Expr sca, ExprVec boundsSC ) {
409    
410            if( type != null ) {
411                Expr pred;
412                
413                if( Types.isIntegralType( type ) ) {
414                    if( eOld != null) {
415                        // guess e >= eOld and e <= eOld
416                        
417                        pred = GC.nary( loc, loc, TagConstants.INTEGRALGE, e, eOld );
418                        predicates.addElement( pred );
419                        pred = GC.nary( loc, loc, TagConstants.INTEGRALLE, e, eOld );
420                        predicates.addElement( pred );
421                    } else {
422                        // guess e >= 0
423                        pred = GC.nary( loc, loc, TagConstants.INTEGRALGE, e,
424                                        LiteralExpr.make( TagConstants.INTLIT,
425                                                                       new Integer(0),
426                                                                       loc ));
427                        predicates.addElement( pred );
428                    }
429                    // guess sc < e
430                    pred = GC.nary( loc, loc, TagConstants.INTEGRALLT, sca, e );
431                    boundsSC.addElement( pred );
432                }
433                
434                if ( Types.isReferenceType( type ) ) {
435                    // guess e != null
436                    pred = GC.nary( loc, loc, TagConstants.REFNE, e,
437                                    LiteralExpr.make( TagConstants.NULLLIT,
438                                                      null, loc ) );
439                    predicates.addElement( pred ); 
440                }
441            }
442        }
443                    
444        /*
445        private void computeMentionsSet(ASTNode n, Set s) {
446            if( n instanceof VariableAccess ) {
447                VariableAccess va = (VariableAccess)n;
448                if( n.decl != null ) {
449                    s.add(n.decl);
450                }
451            }
452            for(int i=0; i<n.childCount(); i++) {
453                Object c = n.childAt(i);
454                computeMentionsSet(c,s);
455            }
456        }
457        */
458    }