Source code: Compil3r/Quad/IPA/CSPAResults.java
1 // CSPAResults.java, created Aug 7, 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 Compil3r.Quad.IPA;
5
6 import java.io.*;
7 import java.util.ArrayList;
8 import java.util.Arrays;
9 import java.util.Collections;
10 import java.util.Comparator;
11 import java.util.Iterator;
12 import java.util.List;
13 import java.util.Set;
14 import java.util.StringTokenizer;
15
16 import org.sf.javabdd.*;
17
18 import Clazz.jq_Reference;
19 import Compil3r.Quad.MethodSummary;
20 import Compil3r.Quad.MethodSummary.Node;
21 import Main.HostedVM;
22 import Util.Assert;
23 import Util.Strings;
24 import Util.Collections.IndexMap;
25 import Util.Collections.SortedArraySet;
26
27 /**
28 * Records results for context-sensitive pointer analysis. The results can
29 * be saved and reloaded. This class also provides methods to query the results.
30 *
31 * @author John Whaley
32 * @version $Id: CSPAResults.java,v 1.2 2003/08/08 08:11:32 joewhaley Exp $
33 */
34 public class CSPAResults {
35
36 /** BDD factory object, to perform BDD operations. */
37 BDDFactory bdd;
38
39 /** Map between variables and indices in the V1o domain. */
40 IndexMap variableIndexMap;
41 /** Map between heap objects and indices in the H1o domain. */
42 IndexMap heapobjIndexMap;
43
44 /** BDD domain for context number of variable. */
45 BDDDomain V1c;
46 /** BDD domain for variable number. */
47 BDDDomain V1o;
48 /** BDD domain for context number of heap object. */
49 BDDDomain H1c;
50 /** BDD domain for heap object number. */
51 BDDDomain H1o;
52
53 /** Points-to BDD: V1c x V1o x H1c x H1o.
54 * This contains the result of the points-to analysis.
55 * A relation (V,H) is in the BDD if variable V can point to heap object H.
56 */
57 BDD pointsTo;
58
59 public static class SetOfContexts {
60
61 }
62
63 BDD getAliasedLocations(Node variable) {
64 BDD context = V1c.set();
65 context.andWith(H1c.set());
66 BDD ci_pointsTo = pointsTo.exist(context);
67 context.free();
68 int i = variableIndexMap.get(variable);
69 BDD a = V1o.ithVar(i);
70 BDD heapObjs = ci_pointsTo.restrict(a);
71 a.free();
72 BDD result = ci_pointsTo.relprod(heapObjs, H1o.set());
73 heapObjs.free();
74 return result;
75 }
76
77 BDD getAllHeapOfType(jq_Reference type) {
78 int j=0;
79 BDD result = bdd.zero();
80 for (Iterator i=heapobjIndexMap.iterator(); i.hasNext(); ++j) {
81 Node n = (Node) i.next();
82 Assert._assert(this.heapobjIndexMap.get(n) == j);
83 if (n.getDeclaredType() == type)
84 result.orWith(V1o.ithVar(j));
85 }
86 return result;
87 /*
88 {
89 int i = typeIndexMap.get(type);
90 BDD a = T2.ithVar(i);
91 BDD result = aC.restrict(a);
92 a.free();
93 return result;
94 }
95 */
96 }
97
98 /** Get a context-insensitive version of the points-to information.
99 * It achieves this by merging all of the contexts together. The
100 * returned BDD is: V1o x H1o.
101 */
102 public BDD getContextInsensitivePointsTo() {
103 BDD context = V1c.set();
104 context.andWith(H1c.set());
105 return pointsTo.exist(context);
106 }
107
108 /** Load points-to results from the given file name prefix.
109 */
110 public void load(String fn) throws IOException {
111 DataInput di;
112
113 di = new DataInputStream(new FileInputStream(fn+".config"));
114 readConfig(di);
115
116 this.pointsTo = bdd.load(fn+".bdd");
117
118 di = new DataInputStream(new FileInputStream(fn+".vars"));
119 variableIndexMap = readIndexMap("Variable", di);
120
121 di = new DataInputStream(new FileInputStream(fn+".heap"));
122 heapobjIndexMap = readIndexMap("Heap", di);
123 }
124
125 private void readConfig(DataInput in) throws IOException {
126 String s = in.readLine();
127 StringTokenizer st = new StringTokenizer(s);
128 int VARBITS = Integer.parseInt(st.nextToken());
129 int HEAPBITS = Integer.parseInt(st.nextToken());
130 int FIELDBITS = Integer.parseInt(st.nextToken());
131 int CLASSBITS = Integer.parseInt(st.nextToken());
132 int CONTEXTBITS = Integer.parseInt(st.nextToken());
133 int[] domainBits;
134 int[] domainSpos;
135 BDDDomain[] bdd_domains;
136 domainBits = new int[] {VARBITS, CONTEXTBITS,
137 VARBITS, CONTEXTBITS,
138 FIELDBITS,
139 HEAPBITS, CONTEXTBITS,
140 HEAPBITS, CONTEXTBITS};
141 domainSpos = new int[domainBits.length];
142
143 long[] domains = new long[domainBits.length];
144 for (int i=0; i<domainBits.length; ++i) {
145 domains[i] = (1L << domainBits[i]);
146 }
147 bdd_domains = bdd.extDomain(domains);
148 V1o = bdd_domains[0];
149 V1c = bdd_domains[1];
150 H1o = bdd_domains[5];
151 H1c = bdd_domains[6];
152
153 boolean reverseLocal = System.getProperty("bddreverse", "true").equals("true");
154 String ordering = System.getProperty("bddordering", "FD_H2cxH2o_V2cxV1cxV2oxV1o_H1cxH1o");
155
156 int[] varorder = CSPA.makeVarOrdering(bdd, domainBits, domainSpos,
157 reverseLocal, ordering);
158 bdd.setVarOrder(varorder);
159 bdd.enableReorder();
160 }
161
162 private IndexMap readIndexMap(String name, DataInput in) throws IOException {
163 int size = Integer.parseInt(in.readLine());
164 IndexMap m = new IndexMap(name, size);
165 for (int i=0; i<size; ++i) {
166 String s = in.readLine();
167 StringTokenizer st = new StringTokenizer(s);
168 Node n = MethodSummary.readNode(st);
169 int j = m.get(n);
170 //System.out.println(i+" = "+n);
171 Assert._assert(i == j);
172 }
173 return m;
174 }
175
176 public static void main(String[] args) throws IOException {
177 HostedVM.initialize();
178
179 int nodeCount = 1000000;
180 int cacheSize = 100000;
181 BDDFactory bdd = BDDFactory.init(nodeCount, cacheSize);
182 bdd.setMaxIncrease(nodeCount/4);
183 CSPAResults r = new CSPAResults(bdd);
184 r.load("cspa");
185 r.interactive();
186 }
187
188 public static String domainName(BDDDomain d) {
189 switch (d.getIndex()) {
190 case 0: return "V1o";
191 case 1: return "V1c";
192 case 5: return "H1o";
193 case 6: return "H1c";
194 default: return "???";
195 }
196 }
197
198 public String elementToString(BDDDomain d, int i) {
199 if (d == V1o) return "V1o("+i+"): "+variableIndexMap.get(i);
200 if (d == H1o) return "H1o("+i+"): "+heapobjIndexMap.get(i);
201 return domainName(d)+"("+i+")";
202 }
203
204 public static String domainNames(Set dom) {
205 StringBuffer sb = new StringBuffer();
206 for (Iterator i=dom.iterator(); i.hasNext(); ) {
207 BDDDomain d = (BDDDomain) i.next();
208 sb.append(domainName(d));
209 if (i.hasNext()) sb.append(',');
210 }
211 return sb.toString();
212 }
213
214 public static final Comparator domain_comparator = new Comparator() {
215
216 public int compare(Object arg0, Object arg1) {
217 BDDDomain d1 = (BDDDomain) arg0;
218 BDDDomain d2 = (BDDDomain) arg1;
219 if (d1.getIndex() < d2.getIndex()) return -1;
220 else if (d1.getIndex() > d2.getIndex()) return 1;
221 else return 0;
222 }
223
224 };
225
226 public class TypedBDD {
227 BDD bdd;
228 Set dom;
229
230 /**
231 * @param pointsTo
232 * @param domains
233 */
234 public TypedBDD(BDD bdd, BDDDomain[] domains) {
235 this.bdd = bdd;
236 this.dom = SortedArraySet.FACTORY.makeSet(domain_comparator);
237 this.dom.addAll(Arrays.asList(domains));
238 }
239
240 public TypedBDD(BDD bdd, Set domains) {
241 this.bdd = bdd;
242 this.dom = domains;
243 }
244
245 public TypedBDD(BDD bdd, BDDDomain d) {
246 this.bdd = bdd;
247 this.dom = SortedArraySet.FACTORY.makeSet(domain_comparator);
248 this.dom.add(d);
249 }
250
251 public TypedBDD(BDD bdd, BDDDomain d1, BDDDomain d2) {
252 this.bdd = bdd;
253 this.dom = SortedArraySet.FACTORY.makeSet(domain_comparator);
254 this.dom.add(d1);
255 this.dom.add(d2);
256 }
257
258 public TypedBDD relprod(TypedBDD bdd1, TypedBDD set) {
259 Set newDom = SortedArraySet.FACTORY.makeSet(domain_comparator);
260 newDom.addAll(dom);
261 newDom.addAll(bdd1.dom);
262 if (!newDom.containsAll(set.dom)) {
263 System.err.println("Warning! Quantifying domain that doesn't exist: "+domainNames(set.dom));
264 }
265 newDom.removeAll(set.dom);
266 System.out.println("Resulting domains: "+domainNames(newDom));
267 return new TypedBDD(bdd.relprod(bdd1.bdd, set.bdd), newDom);
268 }
269
270 public TypedBDD restrict(TypedBDD bdd1) {
271 Set newDom = SortedArraySet.FACTORY.makeSet(domain_comparator);
272 newDom.addAll(dom);
273 if (!newDom.containsAll(bdd1.dom)) {
274 System.err.println("Warning! Restricting domain that doesn't exist: "+domainNames(bdd1.dom));
275 }
276 if (bdd1.satCount() > 1.0) {
277 System.err.println("Warning! Using restrict with more than one value");
278 }
279 newDom.removeAll(bdd1.dom);
280 System.out.println("Resulting domains: "+domainNames(newDom));
281 return new TypedBDD(bdd.restrict(bdd1.bdd), newDom);
282 }
283
284 public TypedBDD exist(TypedBDD set) {
285 Set newDom = SortedArraySet.FACTORY.makeSet(domain_comparator);
286 newDom.addAll(dom);
287 if (!newDom.containsAll(set.dom)) {
288 System.err.println("Warning! Quantifying domain that doesn't exist: "+domainNames(set.dom));
289 }
290 newDom.removeAll(set.dom);
291 System.out.println("Resulting domains: "+domainNames(newDom));
292 return new TypedBDD(bdd.exist(set.bdd), newDom);
293 }
294
295 public TypedBDD and(TypedBDD bdd1) {
296 Set newDom = SortedArraySet.FACTORY.makeSet(domain_comparator);
297 newDom.addAll(dom);
298 newDom.addAll(bdd1.dom);
299 System.out.println("Resulting domains: "+domainNames(newDom));
300 return new TypedBDD(bdd.and(bdd1.bdd), newDom);
301 }
302
303 public TypedBDD or(TypedBDD bdd1) {
304 Set newDom = SortedArraySet.FACTORY.makeSet(domain_comparator);
305 newDom.addAll(dom);
306 if (!newDom.equals(bdd1.dom)) {
307 System.err.println("Warning! Or'ing BDD with different domains: "+domainNames(bdd1.dom));
308 }
309 newDom.addAll(bdd1.dom);
310 System.out.println("Resulting domains: "+domainNames(newDom));
311 return new TypedBDD(bdd.or(bdd1.bdd), newDom);
312 }
313
314 BDD getDomains() {
315 BDDFactory f = bdd.getFactory();
316 BDD r = f.one();
317 for (Iterator i=dom.iterator(); i.hasNext(); ) {
318 BDDDomain d = (BDDDomain) i.next();
319 r.andWith(d.set());
320 }
321 return r;
322 }
323
324 public double satCount() {
325 return bdd.satCount(getDomains());
326 }
327
328 public String toString() {
329 BDD dset = getDomains();
330 double s = bdd.satCount(dset);
331 if (s == 0.) return "<empty>";
332 BDD b = bdd.id();
333 StringBuffer sb = new StringBuffer();
334 int j = 0;
335 while (!b.isZero()) {
336 if (j > 5) {
337 sb.append("\tand "+(long)b.satCount(dset)+" others.");
338 sb.append(Strings.lineSep);
339 break;
340 }
341 int[] val = b.scanAllVar();
342 sb.append("\t(");
343 BDD temp = b.getFactory().one();
344 for (Iterator i=dom.iterator(); i.hasNext(); ) {
345 BDDDomain d = (BDDDomain) i.next();
346 int e = val[d.getIndex()];
347 sb.append(elementToString(d, e));
348 if (i.hasNext()) sb.append(' ');
349 temp.andWith(d.ithVar(e));
350 }
351 sb.append(')');
352 b.applyWith(temp, BDDFactory.diff);
353 ++j;
354 sb.append(Strings.lineSep);
355 }
356 //sb.append(bdd.toStringWithDomains());
357 return sb.toString();
358 }
359 }
360
361 TypedBDD parseBDD(List a, String s) {
362 if (s.equals("pointsTo")) {
363 return new TypedBDD(pointsTo,
364 new BDDDomain[] { V1c, V1o, H1c, H1o });
365 }
366 if (s.startsWith("V1(")) {
367 int x = Integer.parseInt(s.substring(3, s.length()-1));
368 return new TypedBDD(V1o.ithVar(x), V1o);
369 }
370 if (s.startsWith("H1(")) {
371 int x = Integer.parseInt(s.substring(3, s.length()-1));
372 return new TypedBDD(H1o.ithVar(x), H1o);
373 }
374 BDDDomain d = parseDomain(s);
375 if (d != null) {
376 return new TypedBDD(d.domain(), d);
377 }
378 int i = Integer.parseInt(s)-1;
379 return (TypedBDD) a.get(i);
380 }
381
382 TypedBDD parseBDDset(List a, String s) {
383 if (s.equals("V1")) {
384 BDD b = V1o.set(); b.andWith(V1c.set());
385 return new TypedBDD(b, V1c, V1o);
386 }
387 if (s.equals("H1")) {
388 BDD b = H1o.set(); b.andWith(H1c.set());
389 return new TypedBDD(b, H1c, H1o);
390 }
391 if (s.equals("C")) {
392 BDD b = V1c.set(); b.andWith(H1c.set());
393 return new TypedBDD(b, V1c, H1c);
394 }
395 BDDDomain d = parseDomain(s);
396 if (d != null) {
397 return new TypedBDD(d.set(), d);
398 }
399 int i = Integer.parseInt(s)-1;
400 return (TypedBDD) a.get(i);
401 }
402
403 BDDDomain parseDomain(String dom) {
404 if (dom.equals("V1c")) return V1c;
405 if (dom.equals("V1o")) return V1o;
406 if (dom.equals("H1c")) return H1c;
407 if (dom.equals("H1o")) return H1o;
408 return null;
409 }
410
411 void interactive() {
412 try {
413 int i = 1;
414 List results = new ArrayList();
415 DataInput in = new DataInputStream(System.in);
416 for (;;) {
417 System.out.print(i+"> ");
418 String s = in.readLine();
419 if (s == null) return;
420 StringTokenizer st = new StringTokenizer(s);
421 String command = st.nextToken();
422 if (command.equals("relprod")) {
423 TypedBDD bdd1 = parseBDD(results, st.nextToken());
424 TypedBDD bdd2 = parseBDD(results, st.nextToken());
425 TypedBDD set = parseBDDset(results, st.nextToken());
426 TypedBDD r = bdd1.relprod(bdd2, set);
427 results.add(r);
428 } else if (command.equals("restrict")) {
429 TypedBDD bdd1 = parseBDD(results, st.nextToken());
430 TypedBDD bdd2 = parseBDD(results, st.nextToken());
431 TypedBDD r = bdd1.restrict(bdd2);
432 results.add(r);
433 } else if (command.equals("exist")) {
434 TypedBDD bdd1 = parseBDD(results, st.nextToken());
435 TypedBDD set = parseBDDset(results, st.nextToken());
436 TypedBDD r = bdd1.exist(set);
437 results.add(r);
438 } else if (command.equals("and")) {
439 TypedBDD bdd1 = parseBDD(results, st.nextToken());
440 TypedBDD bdd2 = parseBDD(results, st.nextToken());
441 TypedBDD r = bdd1.and(bdd2);
442 results.add(r);
443 } else if (command.equals("or")) {
444 TypedBDD bdd1 = parseBDD(results, st.nextToken());
445 TypedBDD bdd2 = parseBDD(results, st.nextToken());
446 TypedBDD r = bdd1.or(bdd2);
447 results.add(r);
448 } else if (command.equals("var")) {
449 int z = Integer.parseInt(st.nextToken());
450 TypedBDD r = new TypedBDD(V1o.ithVar(z), V1o);
451 results.add(r);
452 } else if (command.equals("heap")) {
453 int z = Integer.parseInt(st.nextToken());
454 TypedBDD r = new TypedBDD(H1o.ithVar(z), H1o);
455 results.add(r);
456 } else {
457 results.add(new TypedBDD(bdd.zero(), Collections.EMPTY_SET));
458 }
459 TypedBDD r = (TypedBDD) results.get(i-1);
460 System.out.println(i+" -> "+r);
461 Assert._assert(i == results.size());
462 ++i;
463 }
464 } catch (IOException x) {
465 x.printStackTrace();
466 }
467 }
468
469 public CSPAResults(BDDFactory bdd) {
470 this.bdd = bdd;
471 }
472
473 }