View Javadoc

1   // PAResultSelector.java, created Nov 3, 2003 12:34:24 AM by joewhaley
2   // Copyright (C) 2003 John Whaley <jwhaley@alum.mit.edu>
3   // Licensed under the terms of the GNU LGPL; see COPYING for details.
4   package joeq.Compiler.Analysis.IPA;
5   
6   import java.util.Collection;
7   import java.util.HashSet;
8   import java.util.Iterator;
9   import java.util.LinkedList;
10  import java.util.Set;
11  import java.math.BigInteger;
12  import joeq.Class.jq_Field;
13  import joeq.Class.jq_Method;
14  import joeq.Class.jq_Type;
15  import joeq.Compiler.Analysis.FlowInsensitive.MethodSummary.Node;
16  import jwutil.util.Assert;
17  import net.sf.javabdd.BDD;
18  import net.sf.javabdd.BDDDomain;
19  import net.sf.javabdd.TypedBDDFactory.TypedBDD;
20  
21  /***
22   * A helper class for PAResults.
23   * @see PAResults
24   * */
25  public class PAResultSelector {
26      private PAResults _results;
27      private PA r;
28      private boolean _verbose = false;
29  
30      public PAResultSelector(PAResults results){
31          _results = results;
32          r = results.r;    
33      }
34      
35      public TypedBDD getReturnBDD(jq_Method method) {
36          // lookup in MRet
37          int idx = r.Mmap.get(method);
38          BDD i   = r.M.ithVar(idx);
39          BDD restricted = r.Mret.restrictWith(i);
40          
41          //System.out.println("In getReturnBDD: " + _results.toString((TypedBDD) restricted, -1));
42          
43          return (TypedBDD)restricted.replaceWith(r.bdd.makePair(r.V2, r.V1));
44      }
45      
46      public TypedBDD getFormalParamBDD(jq_Method method, int index) {
47          // lookup in MRet
48          int idx = r.Mmap.get(method);
49          BDD i   = r.M.ithVar(idx);
50      
51          // formal is in MxZxV1
52          return (TypedBDD)r.formal.restrictWith(i).restrictWith(r.Z.ithVar(index));
53      }
54      
55      public BDD addAllContextToVar(BDD bdd) {
56          TypedBDD tbdd = (TypedBDD)bdd;
57          Set domains = tbdd.getDomainSet();
58  
59          Assert._assert(domains.size() == 1);
60          BDDDomain dom = (BDDDomain)domains.iterator().next();
61          Assert._assert(dom != r.V1c[0] && dom != r.V2c[0]);        
62          
63          tbdd.setDomains(dom, r.V1c[0]);
64          //BDD result = (TypedBDD)tbd q  d.and(r.V1c.set());
65          //tbdd.free();
66          
67          //return result;
68          return tbdd;
69      }
70  
71      protected Collection getUses(TypedBDD bdd) {
72          bdd = (TypedBDD)addAllContextToVar(bdd);
73          TypedBDD reach = (TypedBDD)_results.calculateDefUse(bdd);
74          BDD vars = reach.exist(r.V1cset);
75          
76          Collection result = new LinkedList();
77          for(Iterator iter = ( (TypedBDD)vars ).iterator(); iter.hasNext(); ) {
78              TypedBDD var = (TypedBDD)iter.next();
79              
80              result.add(getNode(var));
81          }
82          return result; 
83      }
84      
85      protected Collection getUses(Node node) {
86          TypedBDD bdd = (TypedBDD)r.V1.ithVar(_results.getVariableIndex(node));
87          
88          return getUses(bdd);
89      }
90      
91      public Node getNode(TypedBDD var) {              
92          BigInteger[] indeces = r.V1.getVarIndices(var);
93          Assert._assert(indeces.length == 1, "There are " + indeces.length + " indeces in " + var.toStringWithDomains());
94          BigInteger index = indeces[0];        
95          Node node = _results.getVariableNode(index.intValue());
96          
97          return node;
98      }
99      
100     public void collectReachabilityTraces(TypedBDD start, TypedBDD stop) {
101         /*
102         try {
103             //_results.printDefUseChain(bdd.andWith(r.V1c.set()));
104             _results.defUseGraph(bdd.andWith(r.V1c.set()), true, new DataOutputStream(System.out));
105         } catch (IOException e) {
106             e.printStackTrace();
107             System.exit(1);
108         }
109         */
110         
111         LinkedList results = new LinkedList();
112         Node root = getNode(start);
113         Node sink = getNode(stop);
114         System.out.println("Starting with " + root + ", looking for " + sink);
115         collectReachabilityTraces(new PAReachabilityTrace(), root, sink, results);
116         
117         int i = 0;
118         for(Iterator iter = results.iterator(); iter.hasNext(); i++) {
119             PAReachabilityTrace trace = (PAReachabilityTrace)iter.next();
120             
121             System.out.println("Trace " + i + ": " + trace.toStringLong());
122         }           
123     }
124     
125     protected void collectReachabilityTraces(PAReachabilityTrace trace, Node last, Node stop, Collection results) {
126         if(trace.contains(last)){
127             if(_verbose) System.err.println("Already seen " + last + " in the trace " + trace.toString());
128             results.add(trace); return; 
129         }
130         trace.addNode(last);
131         if(stop == last) {
132             if(_verbose) System.err.println("Found " + stop);
133             results.add(trace); return;
134         }
135         Collection c = getUses(last);
136         if(c.isEmpty()) {
137             if(_verbose) System.err.println("Finished with " + last);
138             results.add(trace); return;
139         }
140         
141         if(_verbose) {
142             System.err.println("Node " + last + " has " + c.size() + " successor(s): " + c +
143                         "\t trace: " + trace);
144         }
145         
146         for(Iterator iter = c.iterator(); iter.hasNext();) {
147             Node node = (Node)iter.next();
148             
149             PAReachabilityTrace newTrace = (PAReachabilityTrace)trace.clone();
150             collectReachabilityTraces(newTrace, node, stop, results);
151         }
152     }
153     
154     class PAReachabilityTrace {
155         LinkedList/*Node*/ _nodes;
156         
157         PAReachabilityTrace(){
158             _nodes = new LinkedList();
159         }
160         public boolean contains(Node node) {
161             return _nodes.contains(node);
162         }
163         void addNode(Node node) {
164             _nodes.addLast(node);
165         }
166         public String toString() {
167             StringBuffer buf = new StringBuffer(size() + " [");
168             int i = 1;
169             for(Iterator iter = _nodes.iterator(); iter.hasNext(); i++) {
170                 Node node = (Node)iter.next();
171                 
172                 buf.append(" (" + i + ")");
173                 buf.append(node.toString_short());                
174             }
175             buf.append("]");
176             return buf.toString();
177         }
178         public String toStringLong() {
179             StringBuffer buf = new StringBuffer(size() + " [\n");
180             int i = 1;
181             for(Iterator iter = _nodes.iterator(); iter.hasNext(); i++) {
182                 Node node = (Node)iter.next();
183         
184                 buf.append("\t(" + i + ")");
185                 buf.append(node.toString_long());
186                 buf.append("\n");                
187             }
188             buf.append("]");
189             return buf.toString();
190         }
191         public Object clone() {
192             PAReachabilityTrace result = new PAReachabilityTrace();
193             for(Iterator iter = _nodes.iterator(); iter.hasNext(); ) {
194                 result.addNode((Node)iter.next());
195             } 
196             Assert._assert(size() == result.size());
197             return result;
198         }
199         int size() {return _nodes.size();}
200     }
201 
202     public void collectReachabilityTraces2(BDD bdd) {
203         bdd = addAllContextToVar(bdd);
204         int i = 0;
205         BDD reach;
206         Assert._assert(_results != null);
207         do {
208             BDD vars = bdd.exist(r.V1cset);
209             System.err.print("Generation " + i + ": ");
210             for(Iterator li = ((TypedBDD)vars).iterator(); li.hasNext(); ) {
211                 System.err.print(((TypedBDD)li.next()).toStringWithDomains() + " ");
212             }
213             System.err.print("\n");
214                         
215             // ((TypedBDD)bdd).satCount()
216             //System.err.println("Generation " + i + ": " + bdd.toStringWithDomains() /*_pa.toString((TypedBDD)bdd, -1)*/ + "\n");
217             reach = _results.calculateDefUse(bdd);
218             bdd = reach;
219             i++;                
220         } while(i < 10 && !bdd.isZero());        
221     }
222     
223     /***
224      * @param f pointed to 
225      * @return Set of types of objects f could point to
226      */
227     public Set getFieldPointeeTypes(jq_Field f){
228         // Do the bdd magic to produce the answer
229         // 1. project f out of H1xFxH2, get a set of H1xH2 pairs, h1 pointing to h2
230         int fieldIndex = r.getResults().getFieldIndex(f);
231         BDD fBDD = r.F.ithVar(fieldIndex); // F            
232         
233         // 2. project out H1, get all H2 elements
234         BDD h2 = r.hP.relprod(fBDD, r.H1set.union(r.Fset)); // H2
235         
236         // 3. get all types of H2 elements
237         TypedBDD typesOfH2 = (TypedBDD) h2.replace(r.H2toH1).relprod(r.hT, r.H1set);
238 
239         // 4. return them as a set             
240         Set result = new HashSet();            
241         for(Iterator typeIter = typesOfH2.iterator(); typeIter.hasNext();) {
242             TypedBDD typeBDD = (TypedBDD)((TypedBDD)typeIter.next()); // T
243             
244             BigInteger[] indeces = r.T1.getVarIndices(typeBDD);
245             Assert._assert(indeces.length == 1, "There are " + indeces.length + " indeces in " + typeBDD.toStringWithDomains());
246             BigInteger index = indeces[0];        
247             jq_Type type = r.getResults().getType(index.intValue());
248             Assert._assert(type != null);
249             
250             result.add(type);
251         }
252         
253         // TODO: test this
254         return result;
255     }
256 }