1
2
3
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
37 int idx = r.Mmap.get(method);
38 BDD i = r.M.ithVar(idx);
39 BDD restricted = r.Mret.restrictWith(i);
40
41
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
48 int idx = r.Mmap.get(method);
49 BDD i = r.M.ithVar(idx);
50
51
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
65
66
67
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
103
104
105
106
107
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
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
216
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
229
230 int fieldIndex = r.getResults().getFieldIndex(f);
231 BDD fBDD = r.F.ithVar(fieldIndex);
232
233
234 BDD h2 = r.hP.relprod(fBDD, r.H1set.union(r.Fset));
235
236
237 TypedBDD typesOfH2 = (TypedBDD) h2.replace(r.H2toH1).relprod(r.hT, r.H1set);
238
239
240 Set result = new HashSet();
241 for(Iterator typeIter = typesOfH2.iterator(); typeIter.hasNext();) {
242 TypedBDD typeBDD = (TypedBDD)((TypedBDD)typeIter.next());
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
254 return result;
255 }
256 }