1
2
3
4 package joeq.Compiler.Analysis.Primitive;
5
6 import java.util.AbstractMap;
7 import java.util.ArrayList;
8 import java.util.Arrays;
9 import java.util.Collection;
10 import java.util.Collections;
11 import java.util.Comparator;
12 import java.util.HashMap;
13 import java.util.HashSet;
14 import java.util.Iterator;
15 import java.util.List;
16 import java.util.Map;
17 import java.util.Properties;
18 import java.util.Set;
19 import java.util.TreeSet;
20 import java.io.BufferedReader;
21 import java.io.BufferedWriter;
22 import java.io.File;
23 import java.io.FileNotFoundException;
24 import java.io.FileReader;
25 import java.io.FileWriter;
26 import java.io.FilenameFilter;
27 import java.io.IOException;
28 import java.io.PrintStream;
29 import java.io.PrintWriter;
30 import java.lang.reflect.Field;
31 import java.lang.reflect.InvocationTargetException;
32 import java.lang.reflect.Method;
33 import java.math.BigInteger;
34 import joeq.Class.PrimordialClassLoader;
35 import joeq.Class.jq_Array;
36 import joeq.Class.jq_Class;
37 import joeq.Class.jq_FakeInstanceMethod;
38 import joeq.Class.jq_Field;
39 import joeq.Class.jq_Initializer;
40 import joeq.Class.jq_InstanceField;
41 import joeq.Class.jq_InstanceMethod;
42 import joeq.Class.jq_Method;
43 import joeq.Class.jq_MethodVisitor;
44 import joeq.Class.jq_NameAndDesc;
45 import joeq.Class.jq_Reference;
46 import joeq.Class.jq_Type;
47 import joeq.Class.jq_Reference.jq_NullType;
48 import joeq.Compiler.Analysis.BDD.BuildBDDIR;
49 import joeq.Compiler.Analysis.FlowInsensitive.BogusSummaryProvider;
50 import joeq.Compiler.Analysis.FlowInsensitive.MethodSummary;
51 import joeq.Compiler.Analysis.FlowInsensitive.ReflectionInformationProvider;
52 import joeq.Compiler.Analysis.IPA.ObjectCreationGraph;
53 import joeq.Compiler.Analysis.IPA.PA;
54 import joeq.Compiler.Analysis.IPA.ProgramLocation;
55 import joeq.Compiler.Analysis.Primitive.PrimitiveMethodSummary.ConcreteObjectNode;
56 import joeq.Compiler.Analysis.Primitive.PrimitiveMethodSummary.ConcreteTypeNode;
57 import joeq.Compiler.Analysis.Primitive.PrimitiveMethodSummary.GlobalNode;
58 import joeq.Compiler.Analysis.Primitive.PrimitiveMethodSummary.Node;
59 import joeq.Compiler.Analysis.Primitive.PrimitiveMethodSummary.ParamNode;
60 import joeq.Compiler.Analysis.Primitive.PrimitiveMethodSummary.UnknownTypeNode;
61 import joeq.Compiler.Quad.CachedCallGraph;
62 import joeq.Compiler.Quad.CallGraph;
63 import joeq.Compiler.Quad.CodeCache;
64 import joeq.Compiler.Quad.ControlFlowGraph;
65 import joeq.Compiler.Quad.ControlFlowGraphVisitor;
66 import joeq.Compiler.Quad.LoadedCallGraph;
67 import joeq.Compiler.Quad.Quad;
68 import joeq.Compiler.Quad.Operand.RegisterOperand;
69 import joeq.Compiler.Quad.Operator.Invoke;
70 import joeq.Compiler.Quad.RegisterFactory.Register;
71 import joeq.Main.HostedVM;
72 import joeq.UTF.Utf8;
73 import joeq.Util.NameMunger;
74 import jwutil.collections.IndexMap;
75 import jwutil.collections.IndexedMap;
76 import jwutil.collections.Pair;
77 import jwutil.graphs.GlobalPathNumbering;
78 import jwutil.graphs.Navigator;
79 import jwutil.graphs.PathNumbering;
80 import jwutil.graphs.RootPathNumbering;
81 import jwutil.graphs.SCCPathNumbering;
82 import jwutil.graphs.SCCTopSortedGraph;
83 import jwutil.graphs.SCComponent;
84 import jwutil.graphs.Traversals;
85 import jwutil.graphs.PathNumbering.Range;
86 import jwutil.graphs.PathNumbering.Selector;
87 import jwutil.io.SystemProperties;
88 import jwutil.io.Textualizable;
89 import jwutil.io.Textualizer;
90 import jwutil.util.Assert;
91 import net.sf.javabdd.BDD;
92 import net.sf.javabdd.BDDBitVector;
93 import net.sf.javabdd.BDDDomain;
94 import net.sf.javabdd.BDDFactory;
95 import net.sf.javabdd.BDDPairing;
96 import net.sf.javabdd.BDDVarSet;
97 import net.sf.javabdd.TypedBDDFactory;
98 import net.sf.javabdd.TypedBDDFactory.TypedBDD;
99 /***
100 * Pointer analysis using BDDs. Includes both context-insensitive and context-sensitive
101 * analyses. This version corresponds exactly to the description in the paper.
102 * All of the inference rules are direct copies.
103 *
104 * @author John Whaley
105 * @version $Id: PrimitivePA.java 2470 2006-07-17 05:20:48Z joewhaley $
106 */
107 public class PrimitivePA {
108
109 static { SystemProperties.read("pa.properties"); }
110
111 public static final boolean VerifyAssertions = false;
112
113 static boolean WRITE_PARESULTS_BATCHFILE = !System.getProperty("pa.writeparesults", "yes").equals("no");
114
115 boolean TRACE = !System.getProperty("pa.trace", "no").equals("no");
116 boolean TRACE_SOLVER = !System.getProperty("pa.tracesolver", "no").equals("no");
117 boolean TRACE_BIND = !System.getProperty("pa.tracebind", "no").equals("no");
118 boolean TRACE_RELATIONS = !System.getProperty("pa.tracerelations", "no").equals("no");
119 boolean TRACE_OBJECT = !System.getProperty("pa.traceobject", "no").equals("no");
120 boolean TRACE_CONTEXT = !System.getProperty("pa.tracecontext", "no").equals("no");
121 boolean TRACE_PLACEHOLDERS = !System.getProperty("pa.traceplaceholders", "no").equals("no");
122 boolean TRACE_SELECTORS = !System.getProperty("pa.traceselectors", "no").equals("no");
123 PrintStream out = System.out;
124 boolean DUMP_INITIAL = !System.getProperty("pa.dumpinitial", "no").equals("no");
125 boolean DUMP_RESULTS = !System.getProperty("pa.dumpresults", "yes").equals("no");
126 boolean DUMP_FLY = !System.getProperty("pa.dumpfly", "no").equals("no");
127 boolean DUMP_SSA = !System.getProperty("pa.dumpssa", "no").equals("no");
128 boolean SKIP_SOLVE = !System.getProperty("pa.skipsolve", "no").equals("no");
129 static boolean USE_JOEQ_CLASSLIBS = !System.getProperty("pa.usejoeqclasslibs", "no").equals("no");
130
131 boolean INCREMENTAL1 = !System.getProperty("pa.inc1", "yes").equals("no");
132 boolean INCREMENTAL2 = !System.getProperty("pa.inc2", "yes").equals("no");
133 boolean INCREMENTAL3 = !System.getProperty("pa.inc3", "yes").equals("no");
134
135 boolean ADD_CLINIT = !System.getProperty("pa.clinit", "yes").equals("no");
136 boolean ADD_THREADS = !System.getProperty("pa.threads", "yes").equals("no");
137 boolean ADD_FINALIZERS = !System.getProperty("pa.finalizers", "yes").equals("no");
138 boolean IGNORE_EXCEPTIONS = !System.getProperty("pa.ignoreexceptions", "no").equals("no");
139 boolean FILTER_VP = !System.getProperty("pa.vpfilter", "yes").equals("no");
140 boolean FILTER_HP = !System.getProperty("pa.hpfilter", "no").equals("no");
141 boolean CARTESIAN_PRODUCT = !System.getProperty("pa.cp", "no").equals("no");
142 boolean THREAD_SENSITIVE = !System.getProperty("pa.ts", "no").equals("no");
143 boolean OBJECT_SENSITIVE = !System.getProperty("pa.os", "no").equals("no");
144 boolean CONTEXT_SENSITIVE = !System.getProperty("pa.cs", "no").equals("no");
145 boolean BETTER_CONTEXT_NUMBERING = !System.getProperty("pa.bettercontextnumbering", "no").equals("no");
146 boolean USE_STRING_METHOD_SELECTOR = !System.getProperty("pa.stringmethodselector", "no").equals("no");
147 boolean CS_CALLGRAPH = !System.getProperty("pa.cscg", "no").equals("no");
148 boolean DISCOVER_CALL_GRAPH = !System.getProperty("pa.discover", "no").equals("no");
149 boolean PRINT_CALL_GRAPH_SCCS = !System.getProperty("pa.printsccs", "no").equals("no");
150 boolean AUTODISCOVER_CALL_GRAPH = !System.getProperty("pa.autodiscover", "yes").equals("no");
151 boolean DUMP_DOTGRAPH = !System.getProperty("pa.dumpdotgraph", "no").equals("no");
152 boolean FILTER_NULL = !System.getProperty("pa.filternull", "yes").equals("no");
153 boolean LONG_LOCATIONS = !System.getProperty("pa.longlocations", "no").equals("no");
154 boolean DUMP_UNMUNGED_NAMES = !System.getProperty("pa.dumpunmunged", "no").equals("no");
155 boolean INCLUDE_UNKNOWN_TYPES = !System.getProperty("pa.unknowntypes", "yes").equals("no");
156 boolean INCLUDE_ALL_UNKNOWN_TYPES = !System.getProperty("pa.allunknowntypes", "no").equals("no");
157 boolean ADD_SUPERTYPES = !System.getProperty("pa.addsupertypes", "no").equals("no");
158 int ADD_ROOT_PLACEHOLDERS = Integer.parseInt(System.getProperty("pa.addrootplaceholders", "0"));
159 int PUBLIC_PLACEHOLDERS = Integer.parseInt(System.getProperty("pa.publicplaceholders", "0"));
160 boolean FULL_CHA = !System.getProperty("pa.fullcha", "no").equals("no");
161 static boolean ADD_INSTANCE_METHODS = !System.getProperty("pa.addinstancemethods", "no").equals("no");
162 boolean USE_BOGUS_SUMMARIES = !System.getProperty("pa.usebogussummaries", "no").equals("no");
163 boolean USE_REFLECTION_PROVIDER = !System.getProperty("pa.usereflectionprovider", "no").equals("no");
164 boolean RESOLVE_REFLECTION = !System.getProperty("pa.resolvereflection", "no").equals("no");
165 boolean USE_CASTS_FOR_REFLECTION = !System.getProperty("pa.usecastsforreflection", "no").equals("no");
166 boolean RESOLVE_FORNAME = !System.getProperty("pa.resolveforname", "no").equals("no");
167 boolean TRACE_BOGUS = !System.getProperty("pa.tracebogus", "no").equals("no");
168 boolean FIX_NO_DEST = !System.getProperty("pa.fixnodest", "no").equals("no");
169 boolean TRACE_NO_DEST = !System.getProperty("pa.tracenodest", "no").equals("no");
170 boolean REFLECTION_STAT = !System.getProperty("pa.reflectionstat", "no").equals("no");
171 boolean FORNAME_STAT = !System.getProperty("pa.fornamestat", "no").equals("no");
172 String REFLECTION_STAT_FILE = System.getProperty("pa.reflectionstatfile", "reflection.txt");
173 String FORNAME_STAT_FILE = System.getProperty("pa.fornamestatfile", "forname.txt");
174 public static boolean TRACE_REFLECTION = !System.getProperty("pa.tracereflection", "no").equals("no");
175 public static boolean TRACE_REFLECTION_DOMAINS = !System.getProperty("pa.tracereflectiondomains", "no").equals("no");
176 boolean TRACE_FORNAME = !System.getProperty("pa.traceforname", "no").equals("no");
177 int MAX_PARAMS = Integer.parseInt(System.getProperty("pa.maxparams", "4"));
178
179 int bddnodes = Integer.parseInt(System.getProperty("bddnodes", "2500000"));
180 int bddcache = Integer.parseInt(System.getProperty("bddcache", "200000"));
181 double bddminfree = Double.parseDouble(System.getProperty("bddminfree", ".20"));
182 static String resultsFileName = System.getProperty("pa.results", "pa");
183 static String callgraphFileName = System.getProperty("pa.callgraph", "callgraph");
184 static String initialCallgraphFileName = System.getProperty("pa.icallgraph", callgraphFileName);
185
186 boolean USE_VCONTEXT;
187 boolean USE_HCONTEXT;
188
189 Map newMethodSummaries = new HashMap();
190 Set rootMethods = new HashSet();
191
192 CallGraph cg;
193 ObjectCreationGraph ocg;
194
195 BDDFactory bdd;
196
197 BDDDomain V1, V2, I, I2, H1, H2, Z, F, T1, T2, N, M, M2;
198 BDDDomain V1c[], V2c[], H1c[], H2c[];
199
200 int V_BITS=19, I_BITS=19, H_BITS=16, Z_BITS=6, F_BITS=14, T_BITS=14, N_BITS=16, M_BITS=16;
201 int VC_BITS=0, HC_BITS=0;
202 int MAX_VC_BITS = Integer.parseInt(System.getProperty("pa.maxvc", "61"));
203 int MAX_HC_BITS = Integer.parseInt(System.getProperty("pa.maxhc", "0"));
204
205 IndexMap
206 IndexMap
207 IndexedMap
208 IndexMap
209 IndexMap
210 IndexMap
211 IndexMap
212 PathNumbering vCnumbering;
213 PathNumbering hCnumbering;
214 PathNumbering oCnumbering;
215
216 BDD A;
217 BDD vP;
218 BDD S;
219 BDD L;
220 BDD vT;
221 BDD hT;
222 BDD aT;
223 BDD cha;
224 BDD actual;
225 BDD formal;
226 BDD Iret;
227 BDD Mret;
228 BDD Ithr;
229 BDD Mthr;
230 BDD mI;
231 BDD mV;
232 BDD sync;
233 BDD mSync;
234
235 BDD fT;
236 BDD fC;
237
238 BDD hP;
239 BDD IEcs;
240 BDD IE;
241 BDD vPfilter;
242 BDD hPfilter;
243 BDD NNfilter;
244 BDD IEfilter;
245
246 BDD visited;
247
248 BDD forNameMap;
249 BuildBDDIR bddIRBuilder;
250 BDD vReg;
251 BDD iQuad;
252 BDD hQuad;
253 BDD fMember;
254 BDD staticCalls;
255
256 boolean reverseLocal = System.getProperty("bddreverse", "true").equals("true");
257 String varorder = System.getProperty("bddordering");
258
259 BDDPairing V1toV2, V2toV1, H1toH2, ItoI2, I2toI, H2toH1, V1H1toV2H2, V2H2toV1H1;
260 BDDPairing V1ctoV2c, V1cV2ctoV2cV1c, V1cH1ctoV2cV1c;
261 BDDPairing T2toT1, T1toT2;
262 BDDPairing H1toV1c[], V1ctoH1[]; BDDVarSet V1csets[]; BDD V1cH1equals[];
263 BDDVarSet V1set, V2set, H1set, H2set, T1set, T2set, Fset, Mset, Nset, Iset, I2set, Zset;
264 BDDVarSet V1V2set, V1Fset, V2Fset, V1FV2set, V1H1set, H1Fset, H2Fset, H1H2set, H1FH2set;
265 BDDVarSet IMset, INset, INH1set, INT2set, T2Nset, MZset;
266 BDDVarSet V1cset, V2cset, H1cset, H2cset, V1cV2cset, V1cH1cset, H1cH2cset;
267 BDD V1cdomain, V2cdomain, H1cdomain, H2cdomain;
268
269 BDDDomain makeDomain(String name, int bits) {
270 Assert._assert(bits < 64);
271 BDDDomain d = bdd.extDomain(new long[] { 1L << bits })[0];
272 d.setName(name);
273 return d;
274 }
275 IndexMap makeMap(String name, int bits) {
276 return new IndexMap(name, 1 << bits);
277 }
278
279 public void initializeBDD(String bddfactory) {
280 USE_VCONTEXT = VC_BITS > 0;
281 USE_HCONTEXT = HC_BITS > 0;
282
283 if (USE_VCONTEXT || USE_HCONTEXT) bddnodes *= 2;
284
285 if (bddfactory == null)
286 bdd = BDDFactory.init(bddnodes, bddcache);
287 else
288 bdd = BDDFactory.init(bddfactory, bddnodes, bddcache);
289
290 bdd.setIncreaseFactor(2);
291 bdd.setMinFreeNodes(bddminfree);
292
293 V1 = makeDomain("V1", V_BITS);
294 V2 = makeDomain("V2", V_BITS);
295 I = makeDomain("I", I_BITS);
296 I2 = makeDomain("I2", I_BITS);
297 H1 = makeDomain("H1", H_BITS);
298 H2 = makeDomain("H2", H_BITS);
299 Z = makeDomain("Z", Z_BITS);
300 F = makeDomain("F", F_BITS);
301 T1 = makeDomain("T1", T_BITS);
302 T2 = makeDomain("T2", T_BITS);
303 N = makeDomain("N", N_BITS);
304 M = makeDomain("M", M_BITS);
305 M2 = makeDomain("M2", M_BITS);
306
307 if (CONTEXT_SENSITIVE || OBJECT_SENSITIVE || THREAD_SENSITIVE) {
308 V1c = new BDDDomain[1];
309 V2c = new BDDDomain[1];
310 V1c[0] = makeDomain("V1c", VC_BITS);
311 V2c[0] = makeDomain("V2c", VC_BITS);
312 } else if (CARTESIAN_PRODUCT && false) {
313 V1c = new BDDDomain[MAX_PARAMS];
314 V2c = new BDDDomain[MAX_PARAMS];
315 for (int i = 0; i < V1c.length; ++i) {
316 V1c[i] = makeDomain("V1c"+i, H_BITS + HC_BITS);
317 }
318 for (int i = 0; i < V2c.length; ++i) {
319 V2c[i] = makeDomain("V2c"+i, H_BITS + HC_BITS);
320 }
321 } else {
322 V1c = V2c = new BDDDomain[0];
323 }
324 if (USE_HCONTEXT) {
325 H1c = new BDDDomain[] { makeDomain("H1c", HC_BITS) };
326 H2c = new BDDDomain[] { makeDomain("H2c", HC_BITS) };
327 } else {
328 H1c = H2c = new BDDDomain[0];
329 }
330
331 if (TRACE) out.println("Variable context domains: "+V1c.length);
332 if (TRACE) out.println("Heap context domains: "+H1c.length);
333
334 if (varorder == null) {
335
336 if (CONTEXT_SENSITIVE || THREAD_SENSITIVE || OBJECT_SENSITIVE) {
337 if (HC_BITS > 0) {
338 varorder = "N_F_Z_I_I2_M2_M_T1_V2xV1_V2cxV1c_H2xH2c_T2_H1xH1c";
339 } else {
340
341 varorder = "N_F_I_I2_M2_M_Z_V2xV1_V2cxV1c_T1_H2_T2_H1";
342 }
343 } else if (CARTESIAN_PRODUCT && false) {
344 varorder = "N_F_Z_I_I2_M2_M_T1_V2xV1_T2_H2xH1";
345 for (int i = 0; i < V1c.length; ++i) {
346 varorder += "xV1c"+i+"xV2c"+i;
347 }
348 } else {
349
350 varorder = "N_F_I_I2_M2_M_Z_V2xV1_T1_H2_T2_H1";
351 }
352 }
353
354 System.out.println("Using variable ordering "+varorder);
355 int[] ordering = bdd.makeVarOrdering(reverseLocal, varorder);
356 bdd.setVarOrder(ordering);
357
358 V1ctoV2c = bdd.makePair();
359 V1ctoV2c.set(V1c, V2c);
360 V1cV2ctoV2cV1c = bdd.makePair();
361 V1cV2ctoV2cV1c.set(V1c, V2c);
362 V1cV2ctoV2cV1c.set(V2c, V1c);
363 if (OBJECT_SENSITIVE) {
364 V1cH1ctoV2cV1c = bdd.makePair();
365 V1cH1ctoV2cV1c.set(V1c, V2c);
366 V1cH1ctoV2cV1c.set(H1c, V1c);
367 }
368 T2toT1 = bdd.makePair(T2, T1);
369 T1toT2 = bdd.makePair(T1, T2);
370 V1toV2 = bdd.makePair();
371 V1toV2.set(V1, V2);
372 V1toV2.set(V1c, V2c);
373 V2toV1 = bdd.makePair();
374 V2toV1.set(V2, V1);
375 V2toV1.set(V2c, V1c);
376 H1toH2 = bdd.makePair();
377 H1toH2.set(H1, H2);
378 H1toH2.set(H1c, H2c);
379 ItoI2 = bdd.makePair();
380 ItoI2.set(I, I2);
381 I2toI = bdd.makePair();
382 I2toI.set(I2, I);
383 H2toH1 = bdd.makePair();
384 H2toH1.set(H2, H1);
385 H2toH1.set(H2c, H1c);
386 V1H1toV2H2 = bdd.makePair();
387 V1H1toV2H2.set(V1, V2);
388 V1H1toV2H2.set(H1, H2);
389 V1H1toV2H2.set(V1c, V2c);
390 V1H1toV2H2.set(H1c, H2c);
391 V2H2toV1H1 = bdd.makePair();
392 V2H2toV1H1.set(V2, V1);
393 V2H2toV1H1.set(H2, H1);
394 V2H2toV1H1.set(V2c, V1c);
395 V2H2toV1H1.set(H2c, H1c);
396
397 V1set = V1.set();
398 if (V1c.length > 0) {
399 V1cset = bdd.emptySet();
400 V1cdomain = bdd.one();
401 for (int i = 0; i < V1c.length; ++i) {
402 V1cset.unionWith(V1c[i].set());
403 V1cdomain.andWith(V1c[i].domain());
404 }
405 V1set.unionWith(V1cset.id());
406 }
407 V2set = V2.set();
408 if (V2c.length > 0) {
409 V2cset = bdd.emptySet();
410 V2cdomain = bdd.one();
411 for (int i = 0; i < V2c.length; ++i) {
412 V2cset.unionWith(V2c[i].set());
413 V2cdomain.andWith(V2c[i].domain());
414 }
415 V2set.unionWith(V2cset.id());
416 }
417 H1set = H1.set();
418 if (H1c.length > 0) {
419 H1cset = bdd.emptySet();
420 H1cdomain = bdd.one();
421 for (int i = 0; i < H1c.length; ++i) {
422 H1cset.unionWith(H1c[i].set());
423 H1cdomain.andWith(H1c[i].domain());
424 }
425 H1set.unionWith(H1cset.id());
426 }
427 H2set = H2.set();
428 if (H2c.length > 0) {
429 H2cset = bdd.emptySet();
430 H2cdomain = bdd.one();
431 for (int i = 0; i < H2c.length; ++i) {
432 H2cset.unionWith(H2c[i].set());
433 H2cdomain.andWith(H2c[i].domain());
434 }
435 H2set.unionWith(H2cset.id());
436 }
437 T1set = T1.set();
438 T2set = T2.set();
439 Fset = F.set();
440 Mset = M.set();
441 Nset = N.set();
442 Iset = I.set();
443 I2set = I2.set();
444 Zset = Z.set();
445 V1cV2cset = (V1c.length > 0) ? V1cset.union(V2cset) : bdd.emptySet();
446 H1cH2cset = (H1c.length > 0) ? H1cset.union(H2cset) : bdd.emptySet();
447 if (V1c.length > 0) {
448 V1cH1cset = (H1c.length > 0) ? V1cset.union(H1cset) : V1cset;
449 } else {
450 V1cH1cset = (H1c.length > 0) ? H1cset : bdd.emptySet();
451 }
452 V1V2set = V1set.union(V2set);
453 V1FV2set = V1V2set.union(Fset);
454 V1H1set = V1set.union(H1set);
455 V1Fset = V1set.union(Fset);
456 V2Fset = V2set.union(Fset);
457 IMset = Iset.union(Mset);
458 INset = Iset.union(Nset);
459 INH1set = INset.union(H1set);
460 INT2set = INset.union(T2set);
461 H1Fset = H1set.union(Fset);
462 H2Fset = H2set.union(Fset);
463 H1H2set = H1set.union(H2set);
464 H1FH2set = H1Fset.union(H2set);
465 T2Nset = T2set.union(Nset);
466 MZset = Mset.union(Zset);
467
468 A = bdd.zero();
469 vP = bdd.zero();
470 S = bdd.zero();
471 L = bdd.zero();
472 vT = bdd.zero();
473 hT = bdd.zero();
474 aT = bdd.zero();
475 if (FILTER_HP) {
476 fT = bdd.zero();
477 fC = bdd.zero();
478 }
479 cha = bdd.zero();
480 actual = bdd.zero();
481 formal = bdd.zero();
482 Iret = bdd.zero();
483 Mret = bdd.zero();
484 Ithr = bdd.zero();
485 Mthr = bdd.zero();
486 mI = bdd.zero();
487 mV = bdd.zero();
488 sync = bdd.zero();
489 mSync = bdd.zero();
490 IE = bdd.zero();
491 hP = bdd.zero();
492 visited = bdd.zero();
493 forNameMap = bdd.zero();
494
495 if (OBJECT_SENSITIVE || CARTESIAN_PRODUCT) staticCalls = bdd.zero();
496
497 if (THREAD_SENSITIVE) threadRuns = bdd.zero();
498
499 if (INCREMENTAL1) {
500 old1_A = bdd.zero();
501 old1_S = bdd.zero();
502 old1_L = bdd.zero();
503 old1_vP = bdd.zero();
504 old1_hP = bdd.zero();
505 }
506 if (INCREMENTAL2) {
507 old2_myIE = bdd.zero();
508 old2_visited = bdd.zero();
509 }
510 if (INCREMENTAL3) {
511 old3_t3 = bdd.zero();
512 old3_vP = bdd.zero();
513 old3_t4 = bdd.zero();
514 old3_hT = bdd.zero();
515 old3_t6 = bdd.zero();
516 old3_t9 = new BDD[MAX_PARAMS];
517 for (int i = 0; i < old3_t9.length; ++i) {
518 old3_t9[i] = bdd.zero();
519 }
520 }
521
522 reflectiveCalls = bdd.zero();
523
524 if (CARTESIAN_PRODUCT && false) {
525 H1toV1c = new BDDPairing[MAX_PARAMS];
526 V1ctoH1 = new BDDPairing[MAX_PARAMS];
527 V1csets = new BDDVarSet[MAX_PARAMS];
528 V1cH1equals = new BDD[MAX_PARAMS];
529 for (int i = 0; i < MAX_PARAMS; ++i) {
530 H1toV1c[i] = bdd.makePair(H1, V1c[i]);
531 V1ctoH1[i] = bdd.makePair(V1c[i], H1);
532 V1csets[i] = V1c[i].set();
533 V1cH1equals[i] = H1.buildEquals(V1c[i]);
534 }
535 }
536
537 if (USE_VCONTEXT) {
538 IEcs = bdd.zero();
539 }
540 }
541
542 void initializeMaps() {
543 Vmap = makeMap("Vars", V_BITS);
544 Imap = makeMap("Invokes", I_BITS);
545 Hmap = makeMap("Heaps", H_BITS);
546 Fmap = makeMap("Fields", F_BITS);
547 Tmap = makeMap("Types", T_BITS);
548 Nmap = makeMap("Names", N_BITS);
549 Mmap = makeMap("Methods", M_BITS);
550 Mmap.get(new Dummy());
551 if (ADD_THREADS) {
552 PrimordialClassLoader.getJavaLangThread().prepare();
553 PrimordialClassLoader.loader.getOrCreateBSType("Ljava/lang/Runnable;").prepare();
554 }
555 }
556
557 void addToVisited(BDD M_bdd) {
558 if (TRACE_RELATIONS) out.println("Adding to visited: "+M_bdd.toStringWithDomains());
559 visited.orWith(M_bdd.id());
560 }
561
562 public void addToForNameMap(ConcreteTypeNode h, BDD i_bdd) {
563 BDD H_i = H1.ithVar(Hmap.get(h));
564 H_i.andWith(i_bdd.id());
565 forNameMap.orWith(H_i);
566
567
568 }
569
570 void addToFormal(BDD M_bdd, int z, Node v) {
571 BDD bdd1 = Z.ithVar(z);
572 int V_i = Vmap.get(v);
573 bdd1.andWith(V1.ithVar(V_i));
574 bdd1.andWith(M_bdd.id());
575 if (TRACE_RELATIONS) out.println("Adding to formal: "+bdd1.toStringWithDomains());
576 formal.orWith(bdd1);
577 }
578
579 void addToIE(BDD I_bdd, jq_Method target) {
580 int M2_i = Mmap.get(target);
581 BDD bdd1 = M.ithVar(M2_i);
582 bdd1.andWith(I_bdd.id());
583 if (TRACE_RELATIONS) out.println("Adding to IE: "+bdd1.toStringWithDomains());
584 if (USE_VCONTEXT && IEfilter != null) {
585
586
587
588 IEcs.orWith(bdd1.and(IEfilter));
589 }
590 IE.orWith(bdd1);
591 }
592
593 /***
594 * Finds all invocation sites with no targets and tries to create targets from them.
595 * */
596 void analyzeIE(){
597 int noTargetCalls = 0;
598 for(Iterator iter = Imap.iterator(); iter.hasNext();){
599 ProgramLocation mc = (ProgramLocation) iter.next();
600 int I_i = Imap.get(mc);
601 BDD I_bdd = (BDD) I.ithVar(I_i);
602 BDD t = IE.relprod(I_bdd, Iset);
603
604 if(t.isZero()){
605 if(TRACE_NO_DEST) {
606 System.out.println("No destination for " + mc.toStringLong());
607 }
608 BDD V_bdd = actual.relprod(I_bdd, Iset).restrictWith(Z.ithVar(0));
609 int V_i = V_bdd.scanVar(V2).intValue();
610 if(V_i == -1){
611 System.out.println("Index " + V_i + " is scanning " + V_bdd.toStringWithDomains(TS));
612 continue;
613 }
614 if(V_i >= Vmap.size()) {
615
616 System.out.println("Index " + V_i + " is greater than the map size: " + Vmap.size());
617 continue;
618 }
619 Node n = (Node) Vmap.get(V_i);
620 jq_Type type = n.getDeclaredType();
621 if (type instanceof jq_Class) {
622 jq_Class c = (jq_Class) type;
623 c.prepare();
624 if(!provideStubsFor.contains(c)){
625 continue;
626 }
627 }else{
628 continue;
629 }
630 ConcreteTypeNode h = ConcreteTypeNode.get(type, mc);
631 addToVP(V_bdd.replace(V2toV1), h);
632 V_bdd.free();
633 noTargetCalls++;
634 }
635 t.free();
636 I_bdd.free();
637 }
638 if(TRACE_NO_DEST) {
639 System.out.println("There are " + noTargetCalls + " calls without destinations.");
640 }
641
642
643 iterate();
644
645 if(TRACE_NO_DEST) {
646
647 for(Iterator iter = Imap.iterator(); iter.hasNext();){
648 ProgramLocation mc = (ProgramLocation) iter.next();
649 int I_i = Imap.get(mc);
650 BDD I_bdd = (BDD) I.ithVar(I_i);
651 BDD t = IE.relprod(I_bdd, Iset);
652
653 if(t.isZero()){
654 System.out.println("Still no destination for " + mc.toStringLong());
655
656 }
657 t.free();
658 I_bdd.free();
659 }
660 }
661 }
662
663 void addToMI(BDD M_bdd, BDD I_bdd, jq_Method target) {
664 int N_i = Nmap.get(target);
665 BDD bdd1 = N.ithVar(N_i);
666 bdd1.andWith(M_bdd.id());
667 bdd1.andWith(I_bdd.id());
668 if (TRACE_RELATIONS) out.println("Adding to mI: "+bdd1.toStringWithDomains());
669 mI.orWith(bdd1);
670 }
671
672 void addToActual(BDD I_bdd, int z, Set s) {
673 BDD bdd1 = bdd.zero();
674 for (Iterator j = s.iterator(); j.hasNext(); ) {
675 int V_i = Vmap.get(j.next());
676 bdd1.orWith(V2.ithVar(V_i));
677 }
678 bdd1.andWith(Z.ithVar(z));
679 bdd1.andWith(I_bdd.id());
680 if (TRACE_RELATIONS) out.println("Adding to actual: "+bdd1.toStringWithDomains());
681 actual.orWith(bdd1);
682 }
683
684 void addEmptyActual(BDD I_bdd, int z) {
685 if (CARTESIAN_PRODUCT) {
686 BDD bdd1 = V2.ithVar(0);
687 bdd1.andWith(Z.ithVar(z));
688 bdd1.andWith(I_bdd.id());
689 if (TRACE_RELATIONS) out.println("Adding empty to actual: "+bdd1.toStringWithDomains());
690 actual.orWith(bdd1);
691 }
692 }
693
694 void addToIret(BDD I_bdd, Node v) {
695 int V_i = Vmap.get(v);
696 BDD bdd1 = V1.ithVar(V_i);
697 bdd1.andWith(I_bdd.id());
698 if (TRACE_RELATIONS) out.println("Adding to Iret: "+bdd1.toStringWithDomains());
699 Iret.orWith(bdd1);
700 }
701
702 void addToIthr(BDD I_bdd, Node v) {
703 int V_i = Vmap.get(v);
704 BDD bdd1 = V1.ithVar(V_i);
705 bdd1.andWith(I_bdd.id());
706 if (TRACE_RELATIONS) out.println("Adding to Ithr: "+bdd1.toStringWithDomains());
707 Ithr.orWith(bdd1);
708 }
709
710 void addToMV(BDD M_bdd, BDD V_bdd) {
711 BDD bdd1 = M_bdd.id();
712 bdd1.andWith(V_bdd.id());
713 if (TRACE_RELATIONS) out.println("Adding to mV: "+bdd1.toStringWithDomains());
714 mV.orWith(bdd1);
715 }
716
717 void addToMret(BDD M_bdd, Node v) {
718 addToMret(M_bdd, Vmap.get(v));
719 }
720
721 void addToMret(BDD M_bdd, int V_i) {
722 BDD bdd1 = V2.ithVar(V_i);
723 bdd1.andWith(M_bdd.id());
724 if (TRACE_RELATIONS) out.println("Adding to Mret: "+bdd1.toStringWithDomains());
725 Mret.orWith(bdd1);
726 }
727
728 void addToMthr(BDD M_bdd, int V_i) {
729 BDD bdd1 = V2.ithVar(V_i);
730 bdd1.andWith(M_bdd.id());
731 if (TRACE_RELATIONS) out.println("Adding to Mthr: "+bdd1.toStringWithDomains());
732 Mthr.orWith(bdd1);
733 }
734
735 void addToVP(Node p, int H_i) {
736 BDD context = bdd.one();
737 if (USE_VCONTEXT) context.andWith(V1cdomain.id());
738 if (USE_HCONTEXT) context.andWith(H1cdomain.id());
739 addToVP(context, p, H_i);
740 context.free();
741 }
742
743 void addToVP(BDD V1H1context, Node p, int H_i) {
744 int V1_i = Vmap.get(p);
745 BDD bdd1 = V1.ithVar(V1_i);
746 bdd1.andWith(H1.ithVar(H_i));
747 if (V1H1context != null) bdd1.andWith(V1H1context.id());
748 if (TRACE_RELATIONS) out.println("Adding to vP: "+bdd1.toStringWithDomains(TS));
749 vP.orWith(bdd1);
750 }
751
752 void addToVP(BDD V_bdd, Node h) {
753 BDD context = bdd.one();
754 if (USE_VCONTEXT) context.andWith(V1cdomain.id());
755 if (USE_HCONTEXT) context.andWith(H1cdomain.id());
756 addToVP(context, V_bdd, h);
757 context.free();
758 }
759
760 void addToVP(BDD V1H1context, BDD V_bdd, Node h) {
761 if(TRACE_REFLECTION_DOMAINS) {
762 out.println("V_bdd: " + getBDDDomains(V_bdd));
763 }
764 int H_i = Hmap.get(h);
765 BDD bdd1 = H1.ithVar(H_i);
766 bdd1.andWith(V_bdd.id());
767 if (V1H1context != null) bdd1.andWith(V1H1context.id());
768 if (TRACE_RELATIONS)
769 out.println("Adding to vP: "+bdd1.toStringWithDomains(TS));
770 vP.orWith(bdd1);
771 }
772
773 void addToHP(int H_i, int F_i, int H2_i) {
774 BDD bdd1 = H1.ithVar(H_i);
775 bdd1.andWith(F.ithVar(F_i));
776 bdd1.andWith(H2.ithVar(H2_i));
777 if (TRACE_RELATIONS) out.println("Adding to hP: "+bdd1.toStringWithDomains());
778 hP.orWith(bdd1);
779 }
780 void addToA(int V1_i, int V2_i) {
781 BDD context = USE_VCONTEXT ? V1cdomain.and(V2cdomain) : null;
782 addToA(context, V1_i, V2_i);
783 if (USE_VCONTEXT) context.free();
784 }
785
786 void addToA(BDD V1V2context, int V1_i, int V2_i) {
787 BDD V_bdd = V1.ithVar(V1_i);
788 addToA(V1V2context, V_bdd, V2_i);
789 V_bdd.free();
790 }
791
792 void addToA(BDD V_bdd, int V2_i) {
793 BDD context = USE_VCONTEXT ? V1cdomain.and(V2cdomain) : null;
794 addToA(context, V_bdd, V2_i);
795 if (USE_VCONTEXT) context.free();
796 }
797
798 void addToA(BDD V1V2context, BDD V_bdd, int V2_i) {
799 BDD bdd1 = V2.ithVar(V2_i);
800 bdd1.andWith(V_bdd.id());
801 if (USE_VCONTEXT) bdd1.andWith(V1V2context.id());
802 if (TRACE_RELATIONS) out.println("Adding to A: "+bdd1.toStringWithDomains());
803 A.orWith(bdd1);
804 }
805
806 void addToS(BDD V_bdd, jq_Field f, Collection c) {
807 BDD context = USE_VCONTEXT ? V1cdomain.and(V2cdomain) : null;
808 addToS(context, V_bdd, f, c);
809 if (USE_VCONTEXT) context.free();
810 }
811
812 void addToS(BDD V1V2context, BDD V_bdd, jq_Field f, Collection c) {
813 int F_i = Fmap.get(f);
814 BDD F_bdd = F.ithVar(F_i);
815 for (Iterator k = c.iterator(); k.hasNext(); ) {
816 Node node2 = (Node) k.next();
817 if (FILTER_NULL && isNullConstant(node2))
818 continue;
819
820 int V2_i = Vmap.get(node2);
821 BDD bdd1 = V2.ithVar(V2_i);
822 bdd1.andWith(F_bdd.id());
823 bdd1.andWith(V_bdd.id());
824 if (USE_VCONTEXT) bdd1.andWith(V1V2context.id());
825 if (TRACE_RELATIONS) out.println("Adding to S: "+bdd1.toStringWithDomains());
826 S.orWith(bdd1);
827 }
828 F_bdd.free();
829 }
830
831 void addToL(BDD V1V2context, BDD V_bdd, jq_Field f, Collection c) {
832 int F_i = Fmap.get(f);
833 BDD F_bdd = F.ithVar(F_i);
834 for (Iterator k = c.iterator(); k.hasNext(); ) {
835 Node node2 = (Node) k.next();
836 int V2_i = Vmap.get(node2);
837 BDD bdd1 = V2.ithVar(V2_i);
838 bdd1.andWith(F_bdd.id());
839 bdd1.andWith(V_bdd.id());
840 if (USE_VCONTEXT) bdd1.andWith(V1V2context.id());
841 if (TRACE_RELATIONS) out.println("Adding to L: "+bdd1.toStringWithDomains());
842 L.orWith(bdd1);
843 }
844 F_bdd.free();
845 }
846
847 void addToSync(Node n) {
848 int V_i = Vmap.get(n);
849 BDD bdd1 = V1.ithVar(V_i);
850 if (TRACE_RELATIONS) out.println("Adding to sync: "+bdd1.toStringWithDomains());
851 sync.orWith(bdd1);
852 }
853
854 void addToMSync(jq_Method m) {
855 mSync.orWith(M.ithVar(Mmap.get(m)));
856 }
857
858 BDD getVC(ProgramLocation mc, jq_Method callee) {
859 if (CONTEXT_SENSITIVE || THREAD_SENSITIVE) {
860 Pair p = new Pair(LoadedCallGraph.mapCall(mc), callee);
861 Range r_edge = vCnumbering.getEdge(p);
862 Range r_caller = vCnumbering.getRange(mc.getMethod());
863 if (r_edge == null) {
864 out.println("Cannot find edge "+p);
865 return V1cdomain.and(V2cdomain);
866 }
867 BDD context = buildContextMap(V2c[0],
868 PathNumbering.toBigInt(r_caller.low),
869 PathNumbering.toBigInt(r_caller.high),
870 V1c[0],
871 PathNumbering.toBigInt(r_edge.low),
872 PathNumbering.toBigInt(r_edge.high));
873 return context;
874 } else if (OBJECT_SENSITIVE) {
875
876 boolean one_to_one;
877 jq_Method caller = mc.getMethod();
878 jq_Method target = mc.getTargetMethod();
879 if (target.isStatic()) {
880 one_to_one = caller.isStatic();
881 } else {
882 Quad q = ((ProgramLocation.QuadProgramLocation) mc).getQuad();
883 RegisterOperand rop = Invoke.getParam(q, 0);
884 System.out.println("rop = "+rop);
885 one_to_one = rop.getType() == caller.getDeclaringClass();
886 }
887 jq_Class c;
888 if (caller.isStatic()) c = null;
889 else c = caller.getDeclaringClass();
890 Range r = (Range) rangeMap.get(c);
891 System.out.println("Method call: "+mc);
892 System.out.println("Range of "+c+" = "+r);
893 BDD V1V2context;
894 if (r == null) {
895 System.out.println("Warning: when getting VC, "+c+" is not in object creation graph.");
896 V1V2context = V1cdomain.and(V2cdomain);
897 return V1V2context;
898 }
899 if (one_to_one) {
900 int bits = BigInteger.valueOf(r.high.longValue()).bitLength();
901 V1V2context = V1c[0].buildAdd(V2c[0], bits, 0L);
902 V1V2context.andWith(V1c[0].varRange(r.low.longValue(), r.high.longValue()));
903 } else {
904 V1V2context = V1c[0].varRange(r.low.longValue(), r.high.longValue());
905 V1V2context.andWith(V2c[0].varRange(r.low.longValue(), r.high.longValue()));
906 }
907 return V1V2context;
908 } else if (CARTESIAN_PRODUCT) {
909 throw new Error();
910 } else {
911 return null;
912 }
913 }
914
915 public static BDD buildContextMap(BDDDomain d1, BigInteger startD1, BigInteger endD1,
916 BDDDomain d2, BigInteger startD2, BigInteger endD2) {
917 BDD r;
918 BigInteger sizeD1 = endD1.subtract(startD1);
919 BigInteger sizeD2 = endD2.subtract(startD2);
920 if (sizeD1.signum() == -1) {
921 r = d2.varRange(startD2.longValue(), endD2.longValue());
922 r.andWith(d1.ithVar(0));
923 } else if (sizeD2.signum() == -1) {
924 r = d1.varRange(startD1.longValue(), endD1.longValue());
925 r.andWith(d2.ithVar(0));
926 } else {
927 int bits;
928 if (endD1.compareTo(endD2) >= 0) {
929 bits = endD1.bitLength();
930 } else {
931 bits = endD2.bitLength();
932 }
933 long val = startD2.subtract(startD1).longValue();
934 r = d1.buildAdd(d2, bits, val);
935 if (sizeD2.compareTo(sizeD1) >= 0) {
936
937 r.andWith(d1.varRange(startD1.longValue(), endD1.longValue()));
938 } else {
939
940 r.andWith(d2.varRange(startD2.longValue(), endD2.longValue()));
941 }
942 }
943 return r;
944 }
945
946 public boolean alreadyVisited(jq_Method m) {
947 int M_i = Mmap.get(m);
948 BDD M_bdd = M.ithVar(M_i);
949 M_bdd.andWith(visited.id());
950 boolean result = !M_bdd.isZero();
951 M_bdd.free();
952 return result;
953 }
954
955 int opn;
956
957 ConcreteTypeNode addPlaceholderObject(jq_Type type, int depth, ProgramLocation.PlaceholderParameterProgramLocation location) {
958 ConcreteTypeNode h = ConcreteTypeNode.get(type, location, new Integer(++opn));
959 if(TRACE_PLACEHOLDERS) System.out.println("Initializing " + location.getLocationLabel() + " of type " + type + " at depth " + depth);
960 if (depth > 0) {
961 if (type.isClassType()) {
962 jq_Class c = (jq_Class) type;
963 c.prepare();
964 jq_InstanceField[] fields = c.getInstanceFields();
965 for (int i = 0; i < fields.length; ++i) {
966 jq_Type ft = fields[i].getType();
967 if (ft.isReferenceType() && !ft.isAddressType()) {
968 Node h2 = addPlaceholderObject((jq_Reference) ft, depth-1,
969 new ProgramLocation.PlaceholderParameterProgramLocation(location, "." + fields[i].getName()));
970 int H_i = Hmap.get(h);
971 int F_i = Fmap.get(fields[i]);
972 int H2_i = Hmap.get(h2);
973 addToHP(H_i, F_i, H2_i);
974 }
975 }
976 } else if (type.isArrayType()) {
977 jq_Type at = ((jq_Array) type).getElementType();
978 if (at.isReferenceType() && !at.isAddressType()) {
979 Node h2 = addPlaceholderObject((jq_Reference) at, depth-1,
980 new ProgramLocation.PlaceholderParameterProgramLocation(location, "[]"));
981 int H_i = Hmap.get(h);
982 int F_i = Fmap.get(null);
983 int H2_i = Hmap.get(h2);
984 addToHP(H_i, F_i, H2_i);
985 }
986 }
987 }
988 return h;
989 }
990
991 public void addPlaceholdersForParams(jq_Method m, int depth) {
992 if (m.getBytecode() == null) return;
993 PrimitiveMethodSummary ms = PrimitiveMethodSummary.getSummary(m);
994 opn = 1;
995 for (int i = 0; i < ms.getNumOfParams(); ++i) {
996 ParamNode pn = ms.getParamNode(i);
997 if (pn == null) continue;
998
999 ConcreteTypeNode h = addPlaceholderObject(pn.getDeclaredType(), depth-1,
1000 new ProgramLocation.PlaceholderParameterProgramLocation(m, "param#" + i));
1001 int H_i = Hmap.get(h);
1002 addToVP(pn, H_i);
1003 if(TRACE_PLACEHOLDERS) System.out.println("Placeholder object for "+pn+": "+h);
1004 }
1005 }
1006
1007 public void visitMethod(jq_Method m) {
1008 if (alreadyVisited(m)) return;
1009 if (VerifyAssertions && cg != null)
1010 Assert._assert(cg.getAllMethods().contains(m), m.toString());
1011 PrimitivePAMethodSummary s = new PrimitivePAMethodSummary(this, m);
1012 if (VerifyAssertions) Assert._assert(newMethodSummaries.get(m) == s);
1013 }
1014
1015 public void addAllMethods() {
1016 if (DUMP_FLY) return;
1017 for (Iterator i = newMethodSummaries.entrySet().iterator(); i.hasNext(); ) {
1018 Map.Entry e = (Map.Entry) i.next();
1019 jq_Method m = (jq_Method) e.getKey();
1020 PrimitivePAMethodSummary s = (PrimitivePAMethodSummary) e.getValue();
1021 BDD V1V2context = getV1V2Context(m);
1022 BDD V1H1context = getV1H1Context(m);
1023 s.registerRelations(V1V2context, V1H1context);
1024 if (V1V2context != null) V1V2context.free();
1025 if (V1H1context != null) V1H1context.free();
1026 s.free();
1027 i.remove();
1028 }
1029 }
1030
1031 Map rangeMap;
1032
1033 public BDD getV1V2Context(jq_Method m) {
1034 if (THREAD_SENSITIVE) {
1035 BDD b = (BDD) V1H1correspondence.get(m);
1036 BDD c = b.replace(V1ctoV2c);
1037 return c.andWith(b.id());
1038 } else if (CONTEXT_SENSITIVE) {
1039 Range r = vCnumbering.getRange(m);
1040 if (r == null) {
1041 System.out.println("Warning: "+m+" is not in the call graph. The call graph might not match the code.");
1042 return bdd.one();
1043 }
1044 int bits = BigInteger.valueOf(r.high.longValue()).bitLength();
1045 if (TRACE_CONTEXT) out.println("Range to "+m+" = "+r+" ("+bits+" bits)");
1046 BDD V1V2context = V1c[0].buildAdd(V2c[0], bits, 0L);
1047 V1V2context.andWith(V1c[0].varRange(r.low.longValue(), r.high.longValue()));
1048 return V1V2context;
1049 } else if (OBJECT_SENSITIVE) {
1050 jq_Class c;
1051 if (m.isStatic()) c = null;
1052 else c = m.getDeclaringClass();
1053 Range r = (Range) rangeMap.get(c);
1054 if (TRACE_OBJECT) out.println("Range to "+c+" = "+r);
1055 BDD V1V2context;
1056 if (r == null) {
1057 System.out.println("Warning: when getting V1V2, "+c+" is not in object creation graph! Assuming global only.");
1058 V1V2context = V1c[0].ithVar(0);
1059 V1V2context.andWith(V2c[0].ithVar(0));
1060 return V1V2context;
1061 }
1062 int bits = BigInteger.valueOf(r.high.longValue()).bitLength();
1063 V1V2context = V1c[0].buildAdd(V2c[0], bits, 0L);
1064 V1V2context.andWith(V1c[0].varRange(r.low.longValue(), r.high.longValue()));
1065 return V1V2context;
1066 } else if (CARTESIAN_PRODUCT && false) {
1067 BDD V1V2context = bdd.one();
1068 for (int i = 0; i < MAX_PARAMS; ++i) {
1069 V1V2context.andWith(V1c[i].buildEquals(V2c[i]));
1070 }
1071 return V1V2context;
1072 } else {
1073 return null;
1074 }
1075 }
1076
1077 public void visitGlobalNode(Node node) {
1078 if (TRACE) out.println("Visiting node "+node);
1079
1080 int V_i = Vmap.get(node);
1081 BDD V_bdd = V1.ithVar(V_i);
1082
1083 if (VerifyAssertions)
1084 Assert._assert(node instanceof ConcreteObjectNode ||
1085 node instanceof UnknownTypeNode ||
1086 node == GlobalNode.GLOBAL);
1087 addToVP(V_bdd, node);
1088
1089 for (Iterator j = node.getAllEdges().iterator(); j.hasNext(); ) {
1090 Map.Entry e = (Map.Entry) j.next();
1091 jq_Field f = (jq_Field) e.getKey();
1092 Collection c;
1093 if (e.getValue() instanceof Collection)
1094 c = (Collection) e.getValue();
1095 else
1096 c = Collections.singleton(e.getValue());
1097 addToS(V_bdd, f, c);
1098 }
1099
1100 if (VerifyAssertions)
1101 Assert._assert(!node.hasAccessPathEdges());
1102 }
1103
1104 public boolean isNullConstant(Node node) {
1105 if (node instanceof ConcreteTypeNode || node instanceof ConcreteObjectNode) {
1106 jq_Type type = node.getDeclaredType();
1107 if (type == null || type == jq_NullType.NULL_TYPE) {
1108 if (TRACE) out.println("Skipping null constant");
1109 return true;
1110 }
1111 }
1112 return false;
1113 }
1114
1115 void addToVT(int V_i, jq_Type type) {
1116 BDD bdd1 = V1.ithVar(V_i);
1117 int T_i = Tmap.get(type);
1118 bdd1.andWith(T1.ithVar(T_i));
1119 if (TRACE_RELATIONS) out.println("Adding to vT: "+bdd1.toStringWithDomains());
1120 vT.orWith(bdd1);
1121 }
1122
1123 void addToHT(int H_i, jq_Type type) {
1124
1125
1126
1127
1128
1129 int T_i = Tmap.get(type);
1130 BDD T_bdd = T2.ithVar(T_i);
1131 addToHT(H_i, T_bdd);
1132 T_bdd.free();
1133 }
1134
1135 void addToHT(int H_i, BDD T_bdd) {
1136 BDD bdd1 = H1.ithVar(H_i);
1137 bdd1.andWith(T_bdd.id());
1138 if (TRACE_RELATIONS) out.println("Adding to hT: "+bdd1.toStringWithDomains());
1139 hT.orWith(bdd1);
1140 }
1141
1142 void addToAT(BDD T1_bdd, int T2_i) {
1143 BDD bdd1 = T2.ithVar(T2_i);
1144 bdd1.andWith(T1_bdd.id());
1145 if (TRACE_RELATIONS) out.println("Adding to aT: "+bdd1.toStringWithDomains());
1146 aT.orWith(bdd1);
1147 }
1148
1149 void addToFC(BDD T2_bdd, int F_i) {
1150 BDD bdd1 = F.ithVar(F_i);
1151 bdd1.andWith(T2_bdd.id());
1152 if (TRACE_RELATIONS) out.println("Adding to fC: "+bdd1.toStringWithDomains(TS));
1153 fC.orWith(bdd1);
1154 }
1155
1156 void addToFT(BDD F_bdd, BDD T2_bdd) {
1157 BDD bdd1 = F_bdd.and(T2_bdd);
1158 if (TRACE_RELATIONS) out.println("Adding to fT: "+bdd1.toStringWithDomains(TS));
1159 fT.orWith(bdd1);
1160 }
1161
1162 void addToCHA(BDD T_bdd, int N_i, jq_Method m) {
1163 BDD bdd1 = N.ithVar(N_i);
1164 int M_i = Mmap.get(m);
1165 bdd1.andWith(M.ithVar(M_i));
1166 bdd1.andWith(T_bdd.id());
1167 if (TRACE_RELATIONS) out.println("Adding to cha: "+bdd1.toStringWithDomains());
1168 cha.orWith(bdd1);
1169 }
1170
1171 jq_Class object_class = PrimordialClassLoader.getJavaLangObject();
1172 jq_Method javaLangObject_clone;
1173 {
1174 object_class.prepare();
1175 javaLangObject_clone = object_class.getDeclaredInstanceMethod(new jq_NameAndDesc("clone", "()Ljava/lang/Object;"));
1176 }
1177
1178 jq_Class class_class = PrimordialClassLoader.getJavaLangClass();
1179 jq_Method javaLangClass_newInstance;
1180 {
1181 class_class.prepare();
1182 javaLangClass_newInstance = class_class.getDeclaredInstanceMethod(new jq_NameAndDesc("newInstance", "()Ljava/lang/Object;"));
1183 Assert._assert(javaLangClass_newInstance != null);
1184 }
1185
1186 jq_Class cloneable_class = (jq_Class) PrimordialClassLoader.loader.getOrCreateBSType("Ljava/lang/Cloneable;");
1187 jq_Class throwable_class = (jq_Class) PrimordialClassLoader.getJavaLangThrowable();
1188 public static String fakeCloneName = "fake$clone";
1189 jq_Method javaLangObject_fakeclone = jq_FakeInstanceMethod.fakeMethod(object_class,
1190 fakeCloneName, "()Ljava/lang/Object;");
1191
1192 private jq_Method fakeCloneIfNeeded(jq_Type t) {
1193 jq_Method m = javaLangObject_clone;
1194 if (t instanceof jq_Class) {
1195 jq_Class c = (jq_Class)t;
1196 if (!c.isInterface() && c.implementsInterface(cloneable_class)) {
1197 m = jq_FakeInstanceMethod.fakeMethod(c, MethodSummary.fakeCloneName, "()"+t.getDesc());
1198 boolean mustvisit = (cg != null) ? cg.getAllMethods().contains(m) : true;
1199 if (mustvisit)
1200 visitMethod(m);
1201 }
1202 }
1203
1204 return m;
1205 }
1206
1207 int last_V = 0;
1208 int last_H = 0;
1209 int last_T = 0;
1210 int last_N = 0;
1211 int last_F = 0;
1212
1213 private static BogusSummaryProvider bogusSummaryProvider = null;
1214
1215 public static BogusSummaryProvider getBogusSummaryProvider() {
1216 if(bogusSummaryProvider == null) {
1217 bogusSummaryProvider = new BogusSummaryProvider();
1218 }
1219
1220 return bogusSummaryProvider;
1221 }
1222
1223 public void buildTypes() {
1224
1225 int Vsize = Vmap.size();
1226 for (int V_i = last_V; V_i < Vsize; ++V_i) {
1227 Node n = (Node) Vmap.get(V_i);
1228 jq_Type type = n.getDeclaredType();
1229 if (type != null) type.prepare();
1230 addToVT(V_i, type);
1231 }
1232
1233
1234 if (!FILTER_NULL && NNfilter == null) NNfilter = bdd.zero();
1235 int Hsize = Hmap.size();
1236 for (int H_i = last_H; H_i < Hsize; ++H_i) {
1237 Node n = (Node) Hmap.get(H_i);
1238
1239 if (!FILTER_NULL && !isNullConstant(n))
1240 NNfilter.orWith(H1.ithVar(H_i));
1241
1242 jq_Type type = n.getDeclaredType();
1243 if (type != null) {
1244 type.prepare();
1245 if (n instanceof ConcreteTypeNode && type instanceof jq_Class) {
1246 addClassInitializer((jq_Class) type);
1247 addFinalizer((jq_Class) type, n);
1248 }
1249 if (ADD_THREADS && type != jq_NullType.NULL_TYPE &&
1250 (type.isSubtypeOf(PrimordialClassLoader.getJavaLangThread()) ||
1251 type.isSubtypeOf(PrimordialClassLoader.loader.getOrCreateBSType("Ljava/lang/Runnable;")))) {
1252 addThreadRun(n.getDefiningMethod(), n, (jq_Class) type);
1253 }
1254 }
1255 if (!INCLUDE_UNKNOWN_TYPES && (n instanceof UnknownTypeNode) ) {
1256 if(TRACE) out.println("Skipping unknown type node: " + n);
1257 continue;
1258 }
1259 addToHT(H_i, type);
1260 }
1261
1262 if (ADD_SUPERTYPES) {
1263 for (int T_i = 0; T_i < Tmap.size(); ++T_i) {
1264 jq_Type t1 = (jq_Type) Tmap.get(T_i);
1265 if (t1 == null || t1 instanceof jq_NullType) continue;
1266 t1.prepare();
1267
1268 if(t1 instanceof jq_Reference) {
1269 jq_Reference t0 = (jq_Reference) t1;
1270 jq_Reference t2 = t0.getDirectPrimarySupertype();
1271 if (t2 != null) {
1272 t2.prepare();
1273 Tmap.get(t2);
1274 }
1275 jq_Class[] c = t0.getInterfaces();
1276 for (int i = 0; i < c.length; ++i) {
1277 Tmap.get(c[i]);
1278 }
1279 }
1280 }
1281 }
1282
1283 int Fsize = Fmap.size();
1284 int Tsize = Tmap.size();
1285
1286 for (int T1_i = 0; T1_i < Tsize; ++T1_i) {
1287 jq_Type t1 = (jq_Type) Tmap.get(T1_i);
1288 int start = (T1_i < last_T)?last_T:0;
1289 BDD T1_bdd = T1.ithVar(T1_i);
1290 for (int T2_i = start; T2_i < Tsize; ++T2_i) {
1291 jq_Type t2 = (jq_Type) Tmap.get(T2_i);
1292 if (t2 == null || (t1 != null && t2.isSubtypeOf(t1))) {
1293 addToAT(T1_bdd, T2_i);
1294 }
1295 }
1296 if (FILTER_HP) {
1297 BDD T2_bdd = T2.ithVar(T1_i);
1298 if (T1_i >= last_T && t1 == null) {
1299 BDD Fdom = F.domain();
1300 addToFT(Fdom, T2_bdd);
1301 Fdom.free();
1302 }
1303 int start2 = (T1_i < last_T)?last_F:0;
1304 for (int F_i = start2; F_i < Fsize; ++F_i) {
1305 jq_Field f = (jq_Field) Fmap.get(F_i);
1306 if (f != null) {
1307 f.getDeclaringClass().prepare();
1308 f.getType().prepare();
1309 }
1310 BDD F_bdd = F.ithVar(F_i);
1311 if ((t1 == null && f != null && f.isStatic()) ||
1312 (t1 != null && ((f == null && t1 instanceof jq_Array && ((jq_Array) t1).getElementType().isReferenceType()) ||
1313 (f != null && t1.isSubtypeOf(f.getDeclaringClass()))))) {
1314 addToFC(T2_bdd, F_i);
1315 }
1316 if (f != null && t1 != null && t1.isSubtypeOf(f.getType())) {
1317 addToFT(F_bdd, T2_bdd);
1318 }
1319 }
1320 T2_bdd.free();
1321 }
1322 T1_bdd.free();
1323 }
1324
1325
1326 if (INCLUDE_UNKNOWN_TYPES) {
1327 for (int H_i = last_H; H_i < Hsize; ++H_i) {
1328 Node n = (Node) Hmap.get(H_i);
1329 if (!(n instanceof UnknownTypeNode))
1330 continue;
1331 jq_Type type = n.getDeclaredType();
1332 if (type == null)
1333 continue;
1334 if (!INCLUDE_ALL_UNKNOWN_TYPES && (type == object_class || type == throwable_class || type == class_class)) {
1335 System.out.println("warning: excluding UnknownTypeNode "+type.getName()+"* from hT: H1("+H_i+")");
1336 } else {
1337
1338 BDD T_i = T1.ithVar(Tmap.get(type));
1339 BDD Tsub = aT.relprod(T_i, T1set);
1340 addToHT(H_i, Tsub);
1341 Tsub.free();
1342 T_i.free();
1343 }
1344 }
1345 }
1346
1347
1348 if (FILTER_VP) {
1349 if (vPfilter != null) vPfilter.free();
1350 BDD t1 = vT.relprod(aT, T1set);
1351 vPfilter = t1.relprod(hT, T2set);
1352 t1.free();
1353 }
1354
1355 if (FILTER_HP) {
1356 for (int F_i = last_F; F_i < Fsize; ++F_i) {
1357 jq_Field f = (jq_Field) Fmap.get(F_i);
1358 if (f == null) {
1359 BDD F_bdd = F.ithVar(F_i);
1360 BDD T2dom = T2.domain();
1361 addToFT(F_bdd, T2dom);
1362 T2dom.free();
1363 F_bdd.free();
1364 }
1365 }
1366 if (hPfilter != null) hPfilter.free();
1367 BDD t1 = hT.relprod(fC, T2set);
1368 hPfilter = hT.relprod(fT, T2set);
1369 hPfilter.replaceWith(H1toH2);
1370 hPfilter.andWith(t1);
1371 }
1372
1373
1374 int Nsize = Nmap.size();
1375 for (int T_i = 0; T_i < Tsize; ++T_i) {
1376 jq_Type t = (jq_Type) Tmap.get(T_i);
1377 BDD T_bdd = T2.ithVar(T_i);
1378 int start = (T_i < last_T)?last_N:0;
1379 for (int N_i = start; N_i < Nsize; ++N_i) {
1380 jq_Method n = (jq_Method) Nmap.get(N_i);
1381 if (n == null) continue;
1382 n.getDeclaringClass().prepare();
1383 jq_Method m;
1384 if (n.isStatic()) {
1385 if (t != null) continue;
1386 m = n;
1387 } else {
1388 if (t == null || t == jq_NullType.NULL_TYPE || !t.isSubtypeOf(n.getDeclaringClass())) {
1389 continue;
1390 }
1391 m = ((jq_Reference)t).getVirtualMethod(n.getNameAndDesc());
1392 }
1393 if ((m == javaLangObject_clone && t != object_class) || n == javaLangObject_fakeclone) {
1394 m = fakeCloneIfNeeded(t);
1395 addToCHA(T_bdd, Nmap.get(javaLangObject_fakeclone), m);
1396 }
1397 if (m == null) continue;
1398
1399
1400 if(USE_BOGUS_SUMMARIES && m != null) {
1401 jq_Method replacement = getBogusSummaryProvider().getReplacementMethod(m);
1402 if(replacement != null) {
1403 if(TRACE_BOGUS) System.out.println("Replacing a call to " + m +
1404 " with a call to "+ replacement);
1405
1406 addToCHA(T_bdd, Nmap.get(replacement), replacement);
1407 continue;
1408 }
1409 }
1410
1411 if(USE_REFLECTION_PROVIDER && m != null && ReflectionInformationProvider.isNewInstance(n)){
1412 if(TRACE_REFLECTION) System.out.println("Found a reflective call to " + m);
1413 Collection
1414 if(targets != null){
1415 for(Iterator iter = targets.iterator(); iter.hasNext();){
1416 jq_Method target = (jq_Method) iter.next();
1417 if(TRACE_REFLECTION) System.out.println(
1418 "Adding a call to " + target + " instead of "+ m);
1419
1420 addToCHA(T_bdd, Nmap.get(target), target);
1421 }
1422
1423 }else{
1424 if(TRACE_REFLECTION) System.out.println("No reflective targets for a call to " + m);
1425 }
1426 }
1427
1428
1429
1430 addToCHA(T_bdd, N_i, m);
1431 }
1432 T_bdd.free();
1433 }
1434 last_V = Vsize;
1435 last_H = Hsize;
1436 last_T = Tsize;
1437 last_N = Nsize;
1438 last_F = Fsize;
1439 if (Vsize != Vmap.size() ||
1440 Hsize != Hmap.size() ||
1441 Tsize != Tmap.size() ||
1442 Nsize != Nmap.size() ||
1443 Fsize != Fmap.size()) {
1444 if (TRACE) out.println("Elements added, recalculating types...");
1445 buildTypes();
1446 }
1447 }
1448 static ReflectionInformationProvider reflectionInformationProvider = null;
1449 public static ReflectionInformationProvider getReflectionProvider() {
1450 if(reflectionInformationProvider == null){
1451 reflectionInformationProvider = new ReflectionInformationProvider.CribSheetReflectionInformationProvider();
1452 }
1453 return reflectionInformationProvider;
1454 }
1455 public void addClassInitializer(jq_Class c) {
1456 if (!ADD_CLINIT) return;
1457 jq_Method m = c.getClassInitializer();
1458 if (m != null) {
1459 visitMethod(m);
1460 rootMethods.add(m);
1461 }
1462 }
1463
1464 jq_NameAndDesc finalizer_method = new jq_NameAndDesc("finalize", "()V");
1465 public void addFinalizer(jq_Class c, Node h) {
1466 if (!ADD_FINALIZERS) return;
1467 jq_Method m = c.getVirtualMethod(finalizer_method);
1468 if (m != null && m.getBytecode() != null) {
1469 visitMethod(m);
1470 if (rootMethods.add(m)) {
1471
1472 if (ADD_ROOT_PLACEHOLDERS > 0) {
1473 addPlaceholdersForParams(m, ADD_ROOT_PLACEHOLDERS);
1474 }
1475 }
1476 Node p = PrimitiveMethodSummary.getSummary(m).getParamNode(0);
1477 int H_i = Hmap.get(h);
1478 addToVP(p, H_i);
1479 }
1480 }
1481
1482 BDD threadRuns;
1483
1484 static jq_NameAndDesc main_method = new jq_NameAndDesc("main", "([Ljava/lang/String;)V");
1485 static jq_NameAndDesc run_method = new jq_NameAndDesc("run", "()V");
1486 public void addThreadRun(jq_Method caller, Node h, jq_Class c) {
1487 if (!ADD_THREADS) return;
1488 int H_i = Hmap.get(h);
1489 jq_Method m = c.getVirtualMethod(run_method);
1490 if (m != null && m.getBytecode() != null) {
1491 visitMethod(m);
1492 if (rootMethods.add(m)) {
1493
1494 if (ADD_ROOT_PLACEHOLDERS > 0) {
1495 addPlaceholdersForParams(m, ADD_ROOT_PLACEHOLDERS);
1496 }
1497 }
1498 Node p = PrimitiveMethodSummary.getSummary(m).getParamNode(0);
1499 BDD context = null;
1500 if (THREAD_SENSITIVE) {
1501 int context_j = getThreadRunIndex(m, h);
1502 if (context_j == -1) {
1503 System.out.println("Unknown thread node "+h+" method "+m);
1504 return;
1505 }
1506 BDD hcontext = getV1H1Context(caller).exist(V1cset);
1507 int V_i = Vmap.get(p);
1508 System.out.println("Thread "+h+" contexts "+hcontext.toStringWithDomains()+" matches vcontext "+context_j+" "+p);
1509 hcontext.andWith(V1c[0].ithVar(context_j));
1510 hcontext.andWith(H1.ithVar(H_i));
1511 hcontext.andWith(V1.ithVar(V_i));
1512 threadRuns.orWith(hcontext.id());
1513 if (!DUMP_INITIAL) vP.orWith(hcontext);
1514 } else if (CONTEXT_SENSITIVE && MAX_HC_BITS > 1) {
1515 int context_i = getThreadRunIndex(m, h);
1516 int context_j = context_i + vCnumbering.getRange(m).low.intValue();
1517 System.out.println("Thread "+h+" index "+context_j);
1518
1519 context = H1cdomain.id();
1520
1521 context.andWith(V1cdomain.id());
1522 addToVP(context, p, H_i);
1523 context.free();
1524 } else {
1525 addToVP(p, H_i);
1526 }
1527 }
1528 }
1529
1530 public void solvePointsTo() {
1531 if (INCREMENTAL1) {
1532 solvePointsTo_incremental();
1533 return;
1534 }
1535
1536 BDD old_vP;
1537 BDD old_hP = bdd.zero();
1538 for (int outer = 1; ; ++outer) {
1539 for (int inner = 1; ; ++inner) {
1540 old_vP = vP.id();
1541
1542
1543 BDD t1 = vP.replace(V1toV2);
1544 if (TRACE_SOLVER) out.println("Inner #"+inner+": rename V1toV2: vP "+vP.nodeCount()+" -> "+t1.nodeCount());
1545 BDD t2 = A.relprod(t1, V2set);
1546 if (TRACE_SOLVER) out.println("Inner #"+inner+": relprod A "+A.nodeCount()+" -> "+t2.nodeCount());
1547 t1.free();
1548 if (FILTER_VP) t2.andWith(vPfilter.id());
1549 if (FILTER_VP && TRACE_SOLVER) out.println("Inner #"+inner+": and vPfilter "+vPfilter.nodeCount()+" -> "+t2.nodeCount());
1550 if (TRACE_SOLVER) out.print("Inner #"+inner+": or vP "+vP.nodeCount()+" -> ");
1551 vP.orWith(t2);
1552 if (TRACE_SOLVER) out.println(vP.nodeCount());
1553
1554 boolean done = vP.equals(old_vP);
1555 old_vP.free();
1556 if (done) break;
1557 }
1558
1559
1560 BDD t3 = S.relprod(vP, V1set);
1561 if (!FILTER_NULL) t3.andWith(NNfilter.id());
1562 BDD t4 = vP.replace(V1H1toV2H2);
1563 BDD t5 = t3.relprod(t4, V2set);
1564 t3.free(); t4.free();
1565 if (FILTER_HP) t5.andWith(hPfilter.id());
1566 hP.orWith(t5);
1567
1568 if (TRACE_SOLVER) out.println("Outer #"+outer+": hP "+hP.nodeCount());
1569
1570 boolean done = hP.equals(old_hP);
1571 old_hP.free();
1572 if (done) break;
1573 old_hP = hP.id();
1574
1575
1576 BDD t6 = L.relprod(vP, V1set);
1577 BDD t7 = t6.relprod(hP, H1Fset);
1578 t6.free();
1579 t7.replaceWith(V2H2toV1H1);
1580 if (FILTER_VP) t7.andWith(vPfilter.id());
1581 vP.orWith(t7);
1582 if (TRACE_SOLVER) out.println("Outer #"+outer+": vP "+vP.nodeCount());
1583 }
1584 }
1585
1586 BDD old1_A;
1587 BDD old1_S;
1588 BDD old1_L;
1589 BDD old1_vP;
1590 BDD old1_hP;
1591
1592 public void solvePointsTo_incremental() {
1593
1594
1595 BDD new_A = A.apply(old1_A, BDDFactory.diff);
1596 old1_A.free();
1597 if (!new_A.isZero()) {
1598 if (TRACE_SOLVER) out.println("New A: "+new_A.nodeCount());
1599 BDD t1 = vP.replace(V1toV2);
1600 if (TRACE_SOLVER) out.println("New A: rename V1toV2: vP "+vP.nodeCount()+" -> "+t1.nodeCount());
1601 BDD t2 = new_A.relprod(t1, V2set);
1602 if (TRACE_SOLVER) out.println("New A: relprod new_A "+new_A.nodeCount()+" -> "+t2.nodeCount());
1603 new_A.free(); t1.free();
1604 if (FILTER_VP) t2.andWith(vPfilter.id());
1605 if (FILTER_VP && TRACE_SOLVER) out.println("New A: and vPfilter "+vPfilter.nodeCount()+" -> "+t2.nodeCount());
1606 if (TRACE_SOLVER) out.print("New A: or vP "+vP.nodeCount()+" -> ");
1607 vP.orWith(t2);
1608 if (TRACE_SOLVER) out.println(vP.nodeCount());
1609 }
1610 old1_A = A.id();
1611
1612
1613 BDD new_S = S.apply(old1_S, BDDFactory.diff);
1614 old1_S.free();
1615 if (!new_S.isZero()) {
1616 if (TRACE_SOLVER) out.println("New S: "+new_S.nodeCount());
1617 BDD t3 = new_S.relprod(vP, V1set);
1618 if (TRACE_SOLVER) out.println("New S: relprod: vP "+vP.nodeCount()+" -> "+t3.nodeCount());
1619 new_S.free();
1620 if (!FILTER_NULL) t3.andWith(NNfilter.id());
1621 if (!FILTER_NULL && TRACE_SOLVER) out.println("New S: and NNfilter "+NNfilter.nodeCount()+" -> "+t3.nodeCount());
1622 BDD t4 = vP.replace(V1H1toV2H2);
1623 if (TRACE_SOLVER) out.println("New S: replace vP "+vP.nodeCount()+" -> "+t4.nodeCount());
1624 BDD t5 = t3.relprod(t4, V2set);
1625 if (TRACE_SOLVER) out.println("New S: relprod -> "+t5.nodeCount());
1626 t3.free(); t4.free();
1627 if (FILTER_HP) t5.andWith(hPfilter.id());
1628 if (FILTER_HP && TRACE_SOLVER) out.println("New S: and hPfilter "+hPfilter.nodeCount()+" -> "+t5.nodeCount());
1629 if (TRACE_SOLVER) out.print("New S: or hP "+hP.nodeCount()+" -> ");
1630 hP.orWith(t5);
1631 if (TRACE_SOLVER) out.println(hP.nodeCount());
1632 }
1633 old1_S = S.id();
1634
1635
1636 BDD new_L = L.apply(old1_L, BDDFactory.diff);
1637 old1_L.free();
1638 if (!new_L.isZero()) {
1639 if (TRACE_SOLVER) out.println("New L: "+new_L.nodeCount());
1640 BDD t6 = new_L.relprod(vP, V1set);
1641 if (TRACE_SOLVER) out.println("New L: relprod: vP "+vP.nodeCount()+" -> "+t6.nodeCount());
1642 BDD t7 = t6.relprod(hP, H1Fset);
1643 if (TRACE_SOLVER) out.println("New L: relprod: hP "+hP.nodeCount()+" -> "+t7.nodeCount());
1644 t6.free();
1645 t7.replaceWith(V2H2toV1H1);
1646 if (TRACE_SOLVER) out.println("New L: replace: "+t7.nodeCount());
1647 if (FILTER_VP) t7.andWith(vPfilter.id());
1648 if (TRACE_SOLVER) out.print("New L: or vP "+vP.nodeCount()+" -> ");
1649 vP.orWith(t7);
1650 if (TRACE_SOLVER) out.println(vP.nodeCount());
1651 }
1652 old1_L = L.id();
1653
1654 for (int outer = 1; ; ++outer) {
1655 BDD new_vP_inner = vP.apply(old1_vP, BDDFactory.diff);
1656 int inner;
1657 for (inner = 1; !new_vP_inner.isZero() && inner < 256; ++inner) {
1658 if (TRACE_SOLVER)
1659 out.println("Inner #"+inner+": new vP "+new_vP_inner.nodeCount());
1660
1661
1662 BDD t1 = new_vP_inner.replace(V1toV2);
1663 if (TRACE_SOLVER) out.println("Inner #"+inner+": rename V1toV2: "+t1.nodeCount());
1664 new_vP_inner.free();
1665 BDD t2 = A.relprod(t1, V2set);
1666 if (TRACE_SOLVER) out.println("Inner #"+inner+": relprod A: "+A.nodeCount()+" -> "+t2.nodeCount());
1667 t1.free();
1668 if (FILTER_VP) t2.andWith(vPfilter.id());
1669 if (FILTER_VP && TRACE_SOLVER) out.println("Inner #"+inner+": and vPfilter "+vPfilter.nodeCount()+" -> "+t2.nodeCount());
1670
1671 BDD old_vP_inner = vP.id();
1672 vP.orWith(t2);
1673 if (TRACE_SOLVER) out.println("Inner #"+inner+": or vP "+old_vP_inner.nodeCount()+" -> "+vP.nodeCount());
1674 new_vP_inner = vP.apply(old_vP_inner, BDDFactory.diff);
1675 if (TRACE_SOLVER) out.println("Inner #"+inner+": diff vP -> "+new_vP_inner.nodeCount());
1676 old_vP_inner.free();
1677 }
1678
1679 BDD new_vP = vP.apply(old1_vP, BDDFactory.diff);
1680 if (TRACE_SOLVER) out.println("Outer #"+outer+": diff vP "+vP.nodeCount()+" - "+old1_vP.nodeCount()+" = "+new_vP.nodeCount());
1681 old1_vP.free();
1682
1683 {
1684
1685 BDD t3 = S.relprod(new_vP, V1set);
1686 if (TRACE_SOLVER) out.println("Outer #"+outer+" S: relprod "+S.nodeCount()+" -> "+t3.nodeCount());
1687 if (!FILTER_NULL) t3.andWith(NNfilter.id());
1688 if (!FILTER_NULL && TRACE_SOLVER) out.println("Outer #"+outer+" S: and NNfilter "+NNfilter.nodeCount()+" -> "+t3.nodeCount());
1689 BDD t4 = vP.replace(V1H1toV2H2);
1690 if (TRACE_SOLVER) out.println("Outer #"+outer+" S: replace "+vP.nodeCount()+" -> "+t4.nodeCount());
1691 BDD t5 = t3.relprod(t4, V2set);
1692 if (TRACE_SOLVER) out.println("Outer #"+outer+" S: relprod -> "+t5.nodeCount());
1693 t3.free(); t4.free();
1694 if (FILTER_HP) t5.andWith(hPfilter.id());
1695 if (FILTER_HP && TRACE_SOLVER) out.println("Outer #"+outer+" S: and hPfilter "+hPfilter.nodeCount()+" -> "+t5.nodeCount());
1696 if (TRACE_SOLVER) out.print("Outer #"+outer+" S: or hP "+hP.nodeCount()+" -> ");
1697 hP.orWith(t5);
1698 if (TRACE_SOLVER) out.println(hP.nodeCount());
1699 }
1700 {
1701
1702 BDD t3 = S.relprod(vP, V1set);
1703 if (TRACE_SOLVER) out.println("Outer #"+outer+" S': relprod "+S.nodeCount()+", "+vP.nodeCount()+" -> "+t3.nodeCount());
1704 if (!FILTER_NULL) t3.andWith(NNfilter.id());
1705 if (!FILTER_NULL && TRACE_SOLVER) out.println("Outer #"+outer+" S': and NNfilter "+NNfilter.nodeCount()+" -> "+t3.nodeCount());
1706 BDD t4 = new_vP.replace(V1H1toV2H2);
1707 if (TRACE_SOLVER) out.println("Outer #"+outer+" S': replace "+new_vP.nodeCount()+" -> "+t4.nodeCount());
1708 BDD t5 = t3.relprod(t4, V2set);
1709 if (TRACE_SOLVER) out.println("Outer #"+outer+" S': relprod -> "+t5.nodeCount());
1710 t3.free(); t4.free();
1711 if (FILTER_HP) t5.andWith(hPfilter.id());
1712 if (FILTER_HP && TRACE_SOLVER) out.println("Outer #"+outer+" S': and hPfilter "+hPfilter.nodeCount()+" -> "+t5.nodeCount());
1713 if (TRACE_SOLVER) out.print("Outer #"+outer+" S': or hP "+hP.nodeCount()+" -> ");
1714 hP.orWith(t5);
1715 if (TRACE_SOLVER) out.println(hP.nodeCount());
1716 }
1717
1718 old1_vP = vP.id();
1719
1720 BDD new_hP = hP.apply(old1_hP, BDDFactory.diff);
1721 if (TRACE_SOLVER) out.println("Outer #"+outer+": diff hP "+hP.nodeCount()+" - "+old1_hP.nodeCount()+" = "+new_hP.nodeCount());
1722 if (new_hP.isZero() && new_vP.isZero() && inner < 256) break;
1723 old1_hP = hP.id();
1724
1725 {
1726
1727 BDD t6 = L.relprod(new_vP, V1set);
1728 if (TRACE_SOLVER) out.println("Outer #"+outer+" L: relprod "+L.nodeCount()+", "+new_vP.nodeCount()+" -> "+t6.nodeCount());
1729 BDD t7 = t6.relprod(hP, H1Fset);
1730 if (TRACE_SOLVER) out.println("Outer #"+outer+" L: relprod "+hP.nodeCount()+" -> "+t7.nodeCount());
1731 t6.free();
1732 t7.replaceWith(V2H2toV1H1);
1733 if (TRACE_SOLVER) out.println("Outer #"+outer+" L: replace "+t7.nodeCount());
1734 if (FILTER_VP) t7.andWith(vPfilter.id());
1735 if (FILTER_VP && TRACE_SOLVER) out.println("Outer #"+outer+" L: and vPfilter "+vPfilter.nodeCount()+" -> "+t7.nodeCount());
1736 if (TRACE_SOLVER) out.print("Outer #"+outer+" L: or vP "+vP.nodeCount()+" -> ");
1737 vP.orWith(t7);
1738 if (TRACE_SOLVER) out.println(vP.nodeCount());
1739 }
1740 {
1741
1742 BDD t6 = L.relprod(vP, V1set);
1743 if (TRACE_SOLVER) out.println("Outer #"+outer+" L': relprod "+L.nodeCount()+", "+vP.nodeCount()+" -> "+t6.nodeCount());
1744 BDD t7 = t6.relprod(new_hP, H1Fset);
1745 if (TRACE_SOLVER) out.println("Outer #"+outer+" L': relprod "+new_hP.nodeCount()+" -> "+t7.nodeCount());
1746 t6.free();
1747 t7.replaceWith(V2H2toV1H1);
1748 if (TRACE_SOLVER) out.println("Outer #"+outer+" L': replace "+t7.nodeCount());
1749 if (FILTER_VP) t7.andWith(vPfilter.id());
1750 if (FILTER_VP && TRACE_SOLVER) out.println("Outer #"+outer+" L': and vPfilter "+vPfilter.nodeCount()+" -> "+t7.nodeCount());
1751 if (TRACE_SOLVER) out.print("Outer #"+outer+" L': or vP "+vP.nodeCount()+" -> ");
1752 vP.orWith(t7);
1753 if (TRACE_SOLVER) out.println(vP.nodeCount());
1754 }
1755 }
1756 }
1757
1758 public void dumpWithV1c(BDD z, BDDVarSet set) {
1759 BDD a = z.exist(V1cset);
1760 for (Iterator i = a.iterator(set); i.hasNext(); ) {
1761 BDD b = (BDD) i.next();
1762 System.out.println(b.toStringWithDomains(TS));
1763 b.andWith(z.id());
1764 BDD c = b.exist(set);
1765 if (c.isOne()) {
1766 System.out.println(" under all contexts");
1767 } else {
1768 System.out.print(" under context ");
1769 Assert._assert(!c.isZero());
1770 for (int j = 0; j < V1csets.length; ++j) {
1771 BDD d = c.id();
1772 for (int k = 0; k < V1csets.length; ++k) {
1773 if (k == j) continue;
1774 BDD e = d.exist(V1csets[k]);
1775 d.free();
1776 d = e;
1777 }
1778 if (d.isOne()) System.out.print("*");
1779 else if (d.isZero()) System.out.print("0");
1780 else if (d.satCount(V1csets[j]) > 10) System.out.print("many");
1781 else for (Iterator k = d.iterator(V1csets[j]); k.hasNext(); ) {
1782 BDD e = (BDD) k.next();
1783 BigInteger v = e.scanVar(V1c[j]);
1784 BigInteger mask = BigInteger.ONE.shiftLeft(H_BITS).subtract(BigInteger.ONE);
1785 BigInteger val = v.and(mask);
1786 if (val.signum() != 0) System.out.print(TS.elementName(H1.getIndex(), val));
1787 else System.out.print('_');
1788 if (k.hasNext()) System.out.print(',');
1789 }
1790 if (j < MAX_PARAMS-1) System.out.print("|");
1791 }
1792 System.out.println();
1793 }
1794 }
1795 }
1796
1797 public void dumpIEcs() {
1798 for (Iterator i = IEcs.iterator(Iset); i.hasNext(); ) {
1799 BDD q = (BDD) i.next();
1800 BigInteger I_i = q.scanVar(I);
1801 System.out.println("Invocation site "+TS.elementName(I.getIndex(), I_i));
1802 BDD a = q.exist(IMset.union(V1cset));
1803 Iterator k = null;
1804 boolean bool1;
1805 if (a.isOne()) {
1806 System.out.println(" under all contexts");
1807 bool1 = true;
1808 } else if (a.satCount(V2cset) > 16) {
1809 System.out.println(" under many contexts");
1810 bool1 = true;
1811 } else {
1812 k = q.iterator(V2cset);
1813 bool1 = false;
1814 }
1815 if (bool1) k = Collections.singleton(q).iterator();
1816
1817 for ( ; k.hasNext(); ) {
1818 BDD s = (BDD) k.next();
1819 if (!bool1) {
1820 System.out.println(" under context "+s.exist(IMset.union(V1cset)).toStringWithDomains(TS));
1821 }
1822 for (Iterator j = s.iterator(Mset); j.hasNext(); ) {
1823 BDD r = (BDD) j.next();
1824 BigInteger M_i = r.scanVar(M);
1825 System.out.println(" calls "+TS.elementName(M.getIndex(), M_i));
1826 BDD b = r.exist(IMset.union(V2cset));
1827 if (b.isOne()) {
1828 System.out.println(" all contexts");
1829 } else if (b.satCount(V1cset) > 16) {
1830 System.out.println(" many contexts");
1831 } else {
1832 for (Iterator m = r.iterator(V1cset); m.hasNext(); ) {
1833 BDD t = (BDD) m.next();
1834 System.out.println(" context "+t.exist(IMset.union(V2cset)).toStringWithDomains(TS));
1835 }
1836 }
1837 }
1838 }
1839 }
1840 }
1841
1842 public void dumpVP(BDD my_vP) {
1843 for (Iterator i = my_vP.iterator(V1.set()); i.hasNext(); ) {
1844 BDD q = (BDD) i.next();
1845 BigInteger V_i = q.scanVar(V1);
1846 System.out.println("Variable "+TS.elementName(V1.getIndex(), V_i)+" points to:");
1847 for (Iterator j = q.iterator(H1.set()); j.hasNext(); ) {
1848 BDD r = (BDD) j.next();
1849 BigInteger H_i = r.scanVar(H1);
1850 System.out.println(" "+TS.elementName(H1.getIndex(), H_i));
1851 if (USE_VCONTEXT) {
1852 BDD a = r.exist(V1.set().union(H1set));
1853 if (a.isOne()) {
1854 System.out.println(" under all contexts");
1855 } else {
1856 System.out.print(" under context ");
1857 for (int m = 0; m < MAX_PARAMS; ++m) {
1858 if (m > 0) System.out.print("|");
1859 BDD b = a.id();
1860 for (int k = 0; k < V1csets.length; ++k) {
1861 if (k == m) continue;
1862 BDD c = b.exist(V1csets[k]);
1863 b.free();
1864 b = c;
1865 }
1866 if (b.isOne()) {
1867 System.out.print("*");
1868 } else if (b.satCount(V1csets[m]) > 100) {
1869 System.out.print("many");
1870 } else for (Iterator k = b.iterator(V1csets[m]); k.hasNext(); ) {
1871 BDD s = (BDD) k.next();
1872 BigInteger foo = s.scanVar(V1c[m]);
1873 System.out.print(TS.elementName(H1.getIndex(), foo));
1874 if (k.hasNext()) System.out.print(",");
1875 }
1876 }
1877 System.out.println();
1878 }
1879 }
1880 }
1881 }
1882 }
1883
1884
1885
1886
1887
1888
1889
1890 /*** Uses points-to information to bind virtual call sites. (Adds to IE/IEcs.) */
1891 public void bindInvocations() {
1892 if (INCREMENTAL3 && !OBJECT_SENSITIVE) {
1893 bindInvocations_incremental();
1894 return;
1895 }
1896 BDD t1 = actual.restrict(Z.ithVar(0));
1897 if (USE_VCONTEXT) t1.andWith(V2cdomain.id());
1898 t1.replaceWith(V2toV1);
1899 BDD t3 = t1.relprod(mI, Mset);
1900 t1.free();
1901 BDD t4;
1902 if (CS_CALLGRAPH) {
1903
1904 t4 = t3.relprod(vP, V1.set());
1905 } else {
1906
1907 t4 = t3.relprod(vP, V1set);
1908 }
1909
1910 BDD t5 = t4.relprod(hT, H1set);
1911 t4.free();
1912 BDD t6 = t5.relprod(cha, T2Nset);
1913 t5.free();
1914
1915 if (TRACE_SOLVER) out.println("Call graph edges before: "+IE.satCount(IMset));
1916 if (CS_CALLGRAPH) {
1917 IE.orWith(t6.exist(V1cset));
1918 }else {
1919 IE.orWith(t6.id());
1920 }
1921 if (TRACE_SOLVER) out.println("Call graph edges after: "+IE.satCount(IMset));
1922
1923 if (CONTEXT_SENSITIVE || THREAD_SENSITIVE) {
1924
1925 if (CS_CALLGRAPH) t6.replaceWith(V1ctoV2c);
1926 t6.andWith(IEfilter.id());
1927 IEcs.orWith(t6.id());
1928 } else if (OBJECT_SENSITIVE) {
1929
1930 t4 = t3.relprod(vP, V1.set());
1931 t5 = t4.relprod(hT, H1.set());
1932 t4.free();
1933 BDD t7 = t5.relprod(cha, T2Nset);
1934 t5.free();
1935 t7.replaceWith(V1cH1ctoV2cV1c);
1936 IEcs.orWith(t7);
1937
1938
1939 BDD t8 = staticCalls.relprod(vP, V1.set().union(H1.set()));
1940 t8.replaceWith(V1cH1ctoV2cV1c);
1941 IEcs.orWith(t8);
1942 } else if (CARTESIAN_PRODUCT) {
1943
1944
1945
1946
1947
1948
1949
1950
1951
1952
1953
1954
1955
1956
1957
1958
1959
1960 BDD statics = staticCalls.exist(V1.set());
1961 if (CS_CALLGRAPH) statics.andWith(V1cdomain.id());
1962 t6.orWith(statics);
1963
1964
1965 if (CS_CALLGRAPH) t6.replaceWith(V1ctoV2c);
1966
1967 BDD context = bdd.one();
1968
1969 BDD newPt = bdd.zero();
1970 for (int i = MAX_PARAMS - 1; i >= 0; --i) {
1971 if (TRACE_BIND) System.out.println("Param "+i+":");
1972 BDD t8 = actual.restrict(Z.ithVar(i)).and(V2cdomain);
1973 t8.replaceWith(V2toV1);
1974 if (TRACE_BIND) System.out.println("t8 = "+t8.toStringWithDomains());
1975 BDD t9 = t8.relprod(vP, V1.set());
1976 if (TRACE_BIND) {
1977 System.out.println("t9 =");
1978 dumpWithV1c(t9, Iset.union(H1set));
1979 }
1980 t8.free();
1981
1982 t9.replaceWith(V1ctoV2c);
1983 BDD ta = t9.replace(H1toV1c[i]);
1984
1985
1986 context.andWith(ta);
1987
1988
1989 t9.andWith(V1cH1equals[i].id());
1990 BDD tb = t9.relprod(t6, V2cset);
1991 t9.free();
1992 BDD formal_i = formal.restrict(Z.ithVar(i));
1993 BDD tc = tb.relprod(formal_i, Mset);
1994 formal_i.free(); tb.free();
1995 for (int j = 0; j < MAX_PARAMS; ++j) {
1996 if (i == j) continue;
1997 tc.andWith(V1c[j].domain());
1998 }
1999 if (TRACE_BIND) dumpVP(tc.exist(Iset));
2000 newPt.orWith(tc);
2001 }
2002
2003
2004
2005
2006 BDD newPt2 = newPt.relprod(context, V2cset.union(Iset));
2007 newPt.free();
2008 if (TRACE_BIND) dumpVP(newPt2);
2009
2010 if (FILTER_VP) newPt2.andWith(vPfilter.id());
2011 vP.orWith(newPt2);
2012
2013 context.andWith(t6.id());
2014 if (TRACE_BIND) System.out.println("context = "+context.toStringWithDomains());
2015 IEcs.orWith(context);
2016 }
2017 t3.free();
2018 t6.free();
2019 }
2020
2021 Map missingClasses = new HashMap();
2022 Map missingConst = new HashMap();
2023 Map noConstrClasses = new HashMap();
2024 Map cantCastTypes = new HashMap();
2025 Map circularClasses = new HashMap();
2026 Map wellFormedClasses = new HashMap();
2027 Set unresolvedCalls = new HashSet();
2028
2029 BDD reflectiveCalls;
2030
2031 public String getBDDDomains(BDD r) {
2032 if (r.isZero() || r.isOne()) return "[]";
2033
2034 BDDFactory bdd = r.getFactory();
2035 StringBuffer sb = new StringBuffer();
2036 int[] set = new int[bdd.varNum()];
2037 printed = 0;
2038 fdd_printset_rec(bdd, sb, r, set);
2039 return sb.toString();
2040 }
2041 private static int printed = 0;
2042
2043 private PrimitiveSubtypeHelper _subtypeHelper;
2044 private static void fdd_printset_rec(BDDFactory bdd, StringBuffer sb, BDD r, int[] set) {
2045 int fdvarnum = bdd.numberOfDomains();
2046
2047 int n, m, i;
2048 boolean used = false;
2049 int[] var;
2050 boolean first;
2051
2052 if (r.isZero())
2053 return;
2054 else if (r.isOne()) {
2055 if(printed > 0) return;
2056 sb.append('<');
2057 first = true;
2058
2059 for (n=0 ; n<fdvarnum ; n++) {
2060 used = false;
2061
2062 BDDDomain domain_n = bdd.getDomain(n);
2063
2064 int[] domain_n_ivar = domain_n.vars();
2065 int domain_n_varnum = domain_n_ivar.length;
2066 for (m=0 ; m<domain_n_varnum ; m++)
2067 if (set[domain_n_ivar[m]] != 0)
2068 used = true;
2069
2070 if (used) {
2071 if (!first)
2072 sb.append(", ");
2073 first = false;
2074 sb.append(domain_n.getName());
2075
2076 var = domain_n_ivar;
2077
2078 BigInteger pos = BigInteger.ZERO;
2079 int maxSkip = -1;
2080 boolean hasDontCare = false;
2081 for (i=0; i<domain_n_varnum; ++i) {
2082 int val = set[var[i]];
2083 if (val == 0) {
2084 hasDontCare = true;
2085 if (maxSkip == i-1)
2086 maxSkip = i;
2087 }
2088 }
2089 for (i=domain_n_varnum-1; i>=0; --i) {
2090 pos = pos.shiftLeft(1);
2091 int val = set[var[i]];
2092 if (val == 2) {
2093 pos = pos.setBit(0);
2094 }
2095 }
2096 }
2097 }
2098
2099 sb.append('>');
2100 printed = 1;
2101 } else {
2102 set[r.var()] = 1;
2103 BDD lo = r.low();
2104 fdd_printset_rec(bdd, sb, lo, set);
2105 lo.free();
2106
2107 set[r.var()] = 2;
2108 BDD hi = r.high();
2109 fdd_printset_rec(bdd, sb, hi, set);
2110 hi.free();
2111
2112 set[r.var()] = 0;
2113 }
2114 }
2115
2116 static BDD buildEquals(BDDDomain thiz, BDDDomain that){
2117 Assert._assert(thiz.size().equals(that.size()));
2118 BDDFactory factory = thiz.getFactory();
2119 BDD e = factory.one();
2120
2121 int[] this_ivar = thiz.vars();
2122 int[] that_ivar = that.vars();
2123
2124 for (int n = 0; n < thiz.varNum(); n++) {
2125 BDD a = factory.ithVar(this_ivar[n]);
2126 BDD b = factory.ithVar(that_ivar[n]);
2127 a.biimpWith(b);
2128 e.andWith(a);
2129 }
2130
2131 return e;
2132 }
2133
2134
2135 /*** Updates IE/IEcs with new edges obtained from resolving reflective invocations */
2136 public boolean bindReflection(){
2137 BDD t1 = actual.restrict(Z.ithVar(0));
2138 if (USE_VCONTEXT) t1.andWith(V2cdomain.id());
2139 BDD t2 = t1.replaceWith(V2toV1);
2140 BDD t11 = IE.restrict(M.ithVar(Mmap.get(javaLangClass_newInstance)));
2141 if(t11.isZero()){
2142
2143 t11.free();
2144
2145 return false;
2146 }
2147 if(REFLECTION_STAT){
2148 System.out.println("There are " + (int)t11.satCount(Iset) + " calls to Class.newInstance");
2149 }
2150 BDD t3 = t2.and(t11);
2151 t11.free();
2152 t1.free();
2153 BDD t31 = t3.replace(ItoI2);
2154 if(TRACE_REFLECTION && TRACE) out.println("t31: " + t31.toStringWithDomains(TS));
2155
2156 BDD t4;
2157 if (CS_CALLGRAPH) {
2158
2159 t4 = t31.relprod(vP, V1.set());
2160 } else {
2161
2162 t4 = t31.relprod(vP, V1set);
2163 }
2164
2165 if(TRACE_REFLECTION && TRACE) out.println("t4: " + t4.toStringWithDomains(TS) + " of size " + t4.satCount(Iset));
2166 BDD t41 = t4.relprod(forNameMap, Nset);
2167 t4.free();
2168 if(TRACE_REFLECTION && TRACE) out.println("t41: " + t41.toStringWithDomains(TS) + " of size " + t41.satCount(Iset));
2169
2170 BDD t6 = t41.relprod(actual, Iset.union(H1set));
2171 if(TRACE_REFLECTION_DOMAINS) out.println("t6: " + getBDDDomains(t6));
2172 t41.free();
2173 BDD t7 = t6.restrict(Z.ithVar(1));
2174 if(TRACE_REFLECTION_DOMAINS) out.println("t7: " + getBDDDomains(t7));
2175 t6.free();
2176 if(TRACE_REFLECTION && TRACE) out.println("t7: " + t7.toStringWithDomains(TS) + " of size " + t7.satCount(Iset));
2177
2178 BDD t8 = t7.replace(V2toV1);
2179 if(TRACE_REFLECTION_DOMAINS) out.println("t8: " + getBDDDomains(t8));
2180 t7.free();
2181 BDD t9 = t8.relprod(vP, V1set);
2182 t8.free();
2183
2184 if(TRACE_REFLECTION && TRACE) out.println("t9: " + t9.toStringWithDomains(TS) + " of size " + t9.satCount(Iset));
2185 if(TRACE_REFLECTION_DOMAINS) {
2186 out.println("vP: " + getBDDDomains(vP));
2187 out.println("t9: " + getBDDDomains(t9));
2188 }
2189 BDD constructorIE = bdd.zero();
2190 for(Iterator iter = t9.iterator(H1set.union(I2set)); iter.hasNext();){
2191 BDD h = (BDD) iter.next();
2192
2193 int h_i = h.scanVar(H1).intValue();
2194 Object node = Hmap.get(h_i);
2195 int i_i = h.scanVar(I2).intValue();
2196 ProgramLocation mc = (ProgramLocation) Imap.get(i_i);
2197 if(!(node instanceof ConcreteTypeNode)) {
2198
2199 continue;
2200 }
2201 boolean unresolved = false;
2202 PrimitiveMethodSummary.ConcreteTypeNode n = (ConcreteTypeNode) node;
2203 String stringConst = (String) PrimitiveMethodSummary.stringNodes2Values.get(n);
2204 if(stringConst == null){
2205 unresolved = true;
2206 if(missingConst.get(n) == null){
2207 if(TRACE_REFLECTION) {
2208 System.err.println("No constant string for " +
2209 n + " at " + h.toStringWithDomains(TS));
2210 }
2211 missingConst.put(n, new Integer(0));
2212 }
2213 continue;
2214 }
2215
2216 jq_Class c = null;
2217 try {
2218 if(!isWellFormed(stringConst)) {
2219 if(wellFormedClasses.get(stringConst) == null){
2220 if(TRACE_REFLECTION) out.println(stringConst + " is not well-formed.");
2221 wellFormedClasses.put(stringConst, new Integer(0));
2222 }
2223
2224 continue;
2225 }
2226 jq_Type clazz = jq_Type.parseType(stringConst);
2227 if( clazz instanceof jq_Class && clazz != null){
2228 c = (jq_Class) clazz;
2229
2230 if(TRACE_REFLECTION) out.println("Calling class by name: " + stringConst);
2231 c.load();
2232 c.prepare();
2233 Assert._assert(c != null);
2234 }else{
2235 if(cantCastTypes.get(clazz) == null){
2236 if(TRACE_REFLECTION) System.err.println("Can't cast " + clazz + " to jq_Class at " + h.toStringWithDomains(TS) + " -- stringConst: " + stringConst);
2237 cantCastTypes.put(clazz, new Integer(0));
2238 }
2239 continue;
2240 }
2241 } catch(NoClassDefFoundError e) {
2242 if(missingClasses.get(stringConst) == null){
2243 if(TRACE_REFLECTION) System.err.println("Resolving reflection: unable to load " + stringConst +
2244 " at " + h.toStringWithDomains(TS));
2245 missingClasses.put(stringConst, new Integer(0));
2246 }
2247 continue;
2248 } catch(java.lang.ClassCircularityError e) {
2249 if(circularClasses.get(stringConst) == null){
2250 if(TRACE_REFLECTION) System.err.println("Resolving reflection: circularity error " + stringConst +
2251 " at " + h.toStringWithDomains(TS));
2252 circularClasses.put(stringConst, new Integer(0));
2253 }
2254 continue;
2255 }
2256 Assert._assert(c != null);
2257
2258 jq_Method constructor = (jq_Method) c.getDeclaredMember(
2259 new jq_NameAndDesc(
2260 Utf8.get("<init>"),
2261 Utf8.get("()V")));
2262
2263 if(constructor == null){
2264 if(noConstrClasses.get(c) == null){
2265 if(TRACE_REFLECTION) System.err.println("No constructor in class " + c);
2266 noConstrClasses.put(c, new Integer(0));
2267 }
2268 continue;
2269 }
2270
2271 BDD constructorCall = M.ithVar(Mmap.get(constructor)).and(h);
2272 constructorIE.orWith(constructorCall);
2273 if(unresolved){
2274 unresolvedCalls.add(mc);
2275 }
2276 }
2277
2278 BDD old_reflectiveCalls = reflectiveCalls.id();
2279 reflectiveCalls = constructorIE.exist(H1set).replace(I2toI);
2280 constructorIE.free();
2281 if(TRACE_REFLECTION && !reflectiveCalls.isZero()){
2282 out.println("reflectiveCalls: " + reflectiveCalls.toStringWithDomains(TS) +
2283 " of size " + reflectiveCalls.satCount(Iset.union(Mset)));
2284 }
2285
2286 BDD new_reflectiveCalls = reflectiveCalls.apply(old_reflectiveCalls, BDDFactory.diff);
2287 old_reflectiveCalls.free();
2288
2289 if(!new_reflectiveCalls.isZero()){
2290 if(TRACE_REFLECTION) {
2291 out.println("Discovered new_reflectiveCalls: " +
2292 new_reflectiveCalls.toStringWithDomains(TS) +
2293 " of size " + new_reflectiveCalls.satCount(Iset.union(H1set)));
2294 }
2295
2296
2297 for(Iterator iter = new_reflectiveCalls.iterator(Iset.union(Mset)); iter.hasNext();){
2298 BDD i_bdd = (BDD) iter.next();
2299 int I_i = i_bdd.scanVar(I).intValue();
2300 ProgramLocation mc = (ProgramLocation) Imap.get(I_i);
2301 int M_i = new_reflectiveCalls.relprod(i_bdd, Iset).scanVar(M).intValue();
2302 jq_Method target = (jq_Method) Mmap.get(M_i);
2303 jq_Initializer constructor = (jq_Initializer) target;
2304 jq_Type type = constructor.getDeclaringClass();
2305
2306 visitMethod(target);
2307
2308 PrimitiveMethodSummary ms = PrimitiveMethodSummary.getSummary(mc.getMethod());
2309 Node node = ms.getRVN(mc);
2310 if (node != null) {
2311 PrimitiveMethodSummary.ConcreteTypeNode h = ConcreteTypeNode.get(type, mc);
2312 int H_i = Hmap.get(h);
2313 int V_i = Vmap.get(node);
2314 BDD V_arg = V1.ithVar(V_i);
2315
2316 if(TRACE_REFLECTION_DOMAINS) {
2317 out.println("V_arg: " + getBDDDomains(V_arg));
2318 }
2319
2320 addToVP(V_arg, h);
2321 }
2322 }
2323
2324 if (CS_CALLGRAPH){
2325 IE.orWith(new_reflectiveCalls.exist(V1cset));
2326 } else {
2327 IE.orWith(new_reflectiveCalls);
2328 if (TRACE_SOLVER) {
2329 out.println("Call graph edges after: "+IE.satCount(IMset));
2330 }
2331 }
2332 if(TRACE_REFLECTION) out.println("Call graph edges after: "+IE.satCount(IMset));
2333
2334 return true;
2335 } else {
2336 return false;
2337 }
2338 }
2339
2340 PrimitiveSubtypeHelper retrieveSubtypeHelper(){
2341 if(this._subtypeHelper == null){
2342 this._subtypeHelper = PrimitiveSubtypeHelper.newSubtypeHelper(
2343 this, System.getProperty("pa.subtypehelpertype"));
2344 }
2345
2346 return this._subtypeHelper;
2347 }
2348
2349 private boolean bindReflectionsWithCasts() {
2350 if(TRACE_REFLECTION) out.println("Call graph edges before: "+IE.satCount(IMset));
2351 BDD t1 = IE.restrict(M.ithVar(Mmap.get(javaLangClass_newInstance)));
2352 if(t1.isZero()){
2353
2354 t1.free();
2355 return false;
2356 }
2357 if(REFLECTION_STAT){
2358 System.out.println("There are " + (int)t1.satCount(Iset) + " calls to Class.newInstance");
2359 }
2360 BDD t3 = Iret.and(t1).replace(V1toV2);
2361 BDD t32 = t3.and(A);
2362
2363 Assert._assert(T1.size().equals(T2.size()));
2364 BDD notEqualTypes = (buildEquals(T1, T2)).not();
2365 BDD t33 = t32.and(vT);
2366
2367 BDD t34 = t33.and(vT.replace(V1toV2).replace(T1toT2));
2368
2369 BDD tuples = t34.relprod(notEqualTypes, T2set);
2370
2371 t1.free(); t3.free(); t32.free(); t33.free(); t34.free();
2372
2373 BDD constructorIE = bdd.zero();
2374 for(Iterator iter = tuples.iterator(V1set.union(V2set).union(Iset).union(T1set)); iter.hasNext();){
2375 BDD tuple = (BDD) iter.next();
2376 int V1_i = tuple.scanVar(V1).intValue();
2377 int V2_i = tuple.scanVar(V2).intValue();
2378 int I_i = tuple.scanVar(I).intValue();
2379 int T1_i = tuple.scanVar(T1).intValue();
2380
2381 Node v1 = (Node) Vmap.get(V1_i);
2382 Node v2 = (Node) Vmap.get(V2_i);
2383 ProgramLocation mc = (ProgramLocation) Imap.get(I_i);
2384 jq_Reference t = (jq_Reference) Tmap.get(T1_i);
2385 if(!(t instanceof jq_Class)){
2386 System.err.println("Casting to a non-class type: " + t + ", skipping.");
2387 continue;
2388 }
2389 if(TRACE_REFLECTION) {
2390 System.out.println("The result of a call at " + mc.toStringLong() +
2391 " variable " + v2 +
2392 " is cast at " + v1 +
2393 " to type " + t);
2394 }
2395
2396 PrimitiveSubtypeHelper subtypeHelper = retrieveSubtypeHelper();
2397 Collection subtypes = subtypeHelper.getSubtypes((jq_Class) t);
2398 if(subtypes == null){
2399 System.err.println("No subtypes for class " + t.getName());
2400 continue;
2401 }
2402
2403 for(Iterator typeIter = subtypes.iterator(); typeIter.hasNext();){
2404 jq_Class c = (jq_Class) typeIter.next();
2405 jq_Method constructor = (jq_Method) c.getDeclaredMember(
2406 new jq_NameAndDesc(
2407 Utf8.get("<init>"),
2408 Utf8.get("()V")));
2409
2410 if(constructor == null){
2411 if(noConstrClasses.get(c) == null){
2412 if(TRACE_REFLECTION) System.err.println("No constructor in class " + c);
2413 noConstrClasses.put(c, new Integer(0));
2414 }
2415 continue;
2416 }
2417
2418 BDD constructorCall = I.ithVar(I_i).andWith(M.ithVar(Mmap.get(constructor)));
2419 constructorIE.orWith(constructorCall);
2420 }
2421 }
2422
2423 BDD old_reflectiveCalls = reflectiveCalls.id();
2424 reflectiveCalls = constructorIE;
2425
2426 if(TRACE_REFLECTION && !reflectiveCalls.isZero()){
2427 out.println("reflectiveCalls: " + reflectiveCalls.toStringWithDomains(TS) +
2428 " of size " + reflectiveCalls.satCount(Iset.union(Mset)));
2429 }
2430
2431 BDD new_reflectiveCalls = reflectiveCalls.apply(old_reflectiveCalls, BDDFactory.diff);
2432 old_reflectiveCalls.free();
2433
2434 if(!new_reflectiveCalls.isZero()){
2435 if(TRACE_REFLECTION) {
2436 out.println("Discovered new_reflectiveCalls: " +
2437 new_reflectiveCalls.toStringWithDomains(TS) +
2438 " of size " + new_reflectiveCalls.satCount(Iset.union(Mset)));
2439 }
2440
2441
2442 for(Iterator iter = new_reflectiveCalls.iterator(Iset.union(Mset)); iter.hasNext();){
2443 BDD i_bdd = (BDD) iter.next();
2444 int I_i = i_bdd.scanVar(I).intValue();
2445 ProgramLocation mc = (ProgramLocation) Imap.get(I_i);
2446 int M_i = i_bdd.scanVar(M).intValue();
2447 jq_Method target = (jq_Method) Mmap.get(M_i);
2448 jq_Initializer constructor = (jq_Initializer) target;
2449 jq_Type type = constructor.getDeclaringClass();
2450 if(TRACE_REFLECTION){
2451 System.out.println("Adding a call from " + mc.toStringLong() + " to " + constructor);
2452 }
2453
2454 visitMethod(target);
2455
2456 PrimitiveMethodSummary ms = PrimitiveMethodSummary.getSummary(mc.getMethod());
2457 Node node = ms.getRVN(mc);
2458 if (node != null) {
2459 PrimitiveMethodSummary.ConcreteTypeNode h = ConcreteTypeNode.get((jq_Reference) type, mc);
2460 int H_i = Hmap.get(h);
2461 int V_i = Vmap.get(node);
2462 BDD V_arg = V1.ithVar(V_i);
2463
2464 if(TRACE_REFLECTION_DOMAINS) {
2465 out.println("V_arg: " + getBDDDomains(V_arg));
2466 }
2467
2468 addToVP(V_arg, h);
2469 }
2470 }
2471
2472 if (CS_CALLGRAPH){
2473 IE.orWith(new_reflectiveCalls.exist(V1cset));
2474 } else {
2475 IE.orWith(new_reflectiveCalls);
2476 if (TRACE_SOLVER) {
2477 out.println("Call graph edges after: "+IE.satCount(IMset));
2478 }
2479 }
2480 if(TRACE_REFLECTION) out.println("Call graph edges after: "+IE.satCount(IMset));
2481 return true;
2482 } else {
2483 if(TRACE_REFLECTION) out.println("Call graph edges after: "+IE.satCount(IMset));
2484 return false;
2485 }
2486 }
2487
2488 boolean bindForName(){
2489 jq_Method forNameMethod = class_class.getDeclaredMethod("forName");
2490 Assert._assert(forNameMethod != null);
2491 int M_i = Mmap.get(forNameMethod);
2492 BDD M_bdd = M.ithVar(M_i);
2493 BDD I = IE.relprod(M_bdd, Mset);
2494 boolean change = false;
2495 for(Iterator iter = I.iterator(Iset); iter.hasNext();){
2496 BDD I_bdd = (BDD) iter.next();
2497 if(TRACE_FORNAME){
2498 System.out.println("Resolving a forName call at " + I_bdd.toStringWithDomains(TS));
2499 }
2500
2501 BDD t = actual.relprod(I_bdd, Iset);
2502
2503 BDD t1 = t.restrictWith(Z.ithVar(1)).replace(V2toV1);
2504 t.free();
2505
2506 BDD t2 = vP.relprod(t1, V1set);
2507 t1.free();
2508
2509 if(!t2.isZero()){
2510
2511 for(Iterator iter2 = t2.iterator(H1set); iter2.hasNext();){
2512 int h_i = ((BDD) iter2.next()).scanVar(H1).intValue();
2513 Node n = (Node) Hmap.get(h_i);
2514 if(n instanceof PrimitiveMethodSummary.ConcreteTypeNode){
2515 ConcreteTypeNode cn = (ConcreteTypeNode) n;
2516 String stringConst = (String) PrimitiveMethodSummary.stringNodes2Values.get(n);
2517 if(stringConst != null){
2518
2519 if(stringConst == null){
2520 if(missingConst.get(stringConst) == null){
2521 if(TRACE_FORNAME) System.err.println("No constant string for " + n + " at " + n);
2522 missingConst.put(stringConst, new Integer(0));
2523 }
2524 continue;
2525 }
2526
2527 jq_Class c = null;
2528 try {
2529 if(!isWellFormed(stringConst)) {
2530 if(wellFormedClasses.get(stringConst) == null){
2531 if(TRACE_FORNAME) out.println(stringConst + " is not well-formed.");
2532 wellFormedClasses.put(stringConst, new Integer(0));
2533 }
2534
2535 continue;
2536 }
2537 jq_Type clazz = jq_Type.parseType(stringConst);
2538 if( clazz instanceof jq_Class && clazz != null){
2539 c = (jq_Class) clazz;
2540
2541
2542 c.load();
2543 c.prepare();
2544 Assert._assert(c != null);
2545 }else{
2546 if(cantCastTypes.get(clazz) == null){
2547 if(TRACE_FORNAME) System.err.println("Can't cast " + clazz + " to jq_Class at " + I_bdd.toStringWithDomains(TS) + " -- stringConst: " + stringConst);
2548 cantCastTypes.put(clazz, new Integer(0));
2549 }
2550 continue;
2551 }
2552 } catch(NoClassDefFoundError e) {
2553 if(missingClasses.get(stringConst) == null){
2554 if(TRACE_FORNAME) System.err.println("Resolving reflection: unable to load " + stringConst +
2555 " at " + I_bdd.toStringWithDomains(TS));
2556 missingClasses.put(stringConst, new Integer(0));
2557 }
2558 continue;
2559 } catch(java.lang.ClassCircularityError e) {
2560 if(circularClasses.get(stringConst) == null){
2561 if(TRACE_FORNAME) System.err.println("Resolving reflection: circularity error " + stringConst +
2562 " at " + I_bdd.toStringWithDomains(TS));
2563 circularClasses.put(stringConst, new Integer(0));
2564 }
2565 continue;
2566 }
2567 Assert._assert(c != null);
2568
2569 jq_Method constructor = c.getClassInitializer();
2570
2571 if(constructor != null){
2572 int M2_i = Mmap.get(constructor);
2573 BDD t11 = M.ithVar(M2_i);
2574 BDD t22 = t11.andWith(I_bdd.id());
2575
2576 if(IE.and(t22).isZero()){
2577 IE.orWith(t22);
2578 if(TRACE_FORNAME) {
2579 System.out.println("Calling " + constructor + " as a side-effect of Class.forName at " +
2580 I_bdd.toStringWithDomains(TS));
2581 }
2582 change = true;
2583 }else{
2584 t22.free();
2585 }
2586 }else{
2587 if(TRACE_FORNAME) {
2588 System.out.println("No class constructor in " + c);
2589 }
2590 }
2591 }
2592 }
2593 }
2594 }else{
2595 if(TRACE_FORNAME){
2596 System.out.println("No points-to set at " + I_bdd.toStringWithDomains(TS));
2597 }
2598 }
2599 I_bdd.free();
2600 t2.free();
2601 }
2602 M_bdd.free();
2603 I.free();
2604
2605 return change;
2606 }
2607
2608 private boolean isWellFormed(String stringConst) {
2609 if(stringConst.equals(".")) {
2610 return false;
2611 }
2612 int dotCount = 0;
2613 for(int i = 0; i < stringConst.length(); i++){
2614 char ch = stringConst.charAt(i);
2615
2616 if(ch == '.'){
2617 dotCount++;
2618 } else {
2619 if(ch != '$' && ch != '_' && !Character.isLetterOrDigit(ch)){
2620 return false;
2621 }
2622 }
2623 }
2624
2625
2626
2627 return true;
2628 }
2629
2630 BDD old3_t3;
2631 BDD old3_vP;
2632 BDD old3_t4;
2633 BDD old3_hT;
2634 BDD old3_t6;
2635 BDD old3_t9[];
2636
2637
2638
2639
2640
2641
2642
2643
2644
2645
2646
2647
2648
2649
2650
2651
2652
2653
2654 public void bindInvocations_incremental() {
2655 BDD t1 = actual.restrict(Z.ithVar(0));
2656 if (USE_VCONTEXT) t1.andWith(V2cdomain.id());
2657 t1.replaceWith(V2toV1);
2658 BDD t3 = t1.relprod(mI, Mset);
2659 t1.free();
2660 BDD new_t3 = t3.apply(old3_t3, BDDFactory.diff);
2661 old3_t3.free();
2662 if (false) out.println("New invokes: "+new_t3.toStringWithDomains());
2663 BDD new_vP = vP.apply(old3_vP, BDDFactory.diff);
2664 old3_vP.free();
2665 if (false) out.println("New vP: "+new_vP.toStringWithDomains());
2666 BDD t4, new_t4;
2667 if (CS_CALLGRAPH) {
2668
2669 t4 = t3.relprod(new_vP, V1.set());
2670 old3_t3 = t3;
2671 t4.orWith(new_t3.relprod(vP, V1.set()));
2672 new_t3.free();
2673 new_t4 = t4.apply(old3_t4, BDDFactory.diff);
2674 old3_t4.free();
2675 } else {
2676
2677 t4 = t3.relprod(new_vP, V1set);
2678 old3_t3 = t3;
2679 t4.orWith(new_t3.relprod(vP, V1set));
2680 new_t3.free();
2681 new_t4 = t4.apply(old3_t4, BDDFactory.diff);
2682 old3_t4.free();
2683 }
2684 if (false) out.println("New 'this' objects: "+new_t4.toStringWithDomains());
2685 BDD new_hT = hT.apply(old3_hT, BDDFactory.diff);
2686 old3_hT.free();
2687 BDD t5 = t4.relprod(new_hT, H1set);
2688 new_hT.free();
2689 old3_t4 = t4;
2690 t5.orWith(new_t4.relprod(hT, H1set));
2691 new_t4.free();
2692 BDD t6 = t5.relprod(cha, T2Nset);
2693 t5.free();
2694
2695 if (TRACE_SOLVER) out.println("Call graph edges before: "+IE.satCount(IMset));
2696 if (CS_CALLGRAPH) IE.orWith(t6.exist(V1cset));
2697 else IE.orWith(t6.id());
2698 if (TRACE_SOLVER) out.println("Call graph edges after: "+IE.satCount(IMset));
2699
2700 old3_vP = vP.id();
2701 old3_hT = hT.id();
2702
2703 if (CONTEXT_SENSITIVE) {
2704 if (CS_CALLGRAPH) t6.replaceWith(V1ctoV2c);
2705 t6.andWith(IEfilter.id());
2706 IEcs.orWith(t6);
2707 } else if (OBJECT_SENSITIVE) {
2708 throw new Error();
2709 } else if (CARTESIAN_PRODUCT) {
2710
2711
2712
2713
2714
2715
2716
2717
2718
2719
2720
2721
2722
2723
2724
2725
2726
2727
2728
2729
2730
2731 BDD statics = staticCalls.exist(V1.set());
2732 if (CS_CALLGRAPH) statics.andWith(V1cdomain.id());
2733 t6.orWith(statics);
2734
2735
2736 if (CS_CALLGRAPH) t6.replaceWith(V1ctoV2c);
2737
2738 BDD new_t6 = t6.apply(old3_t6, BDDFactory.diff);
2739
2740
2741 BDD newContext = bdd.one();
2742
2743 BDD newPt = bdd.zero();
2744 for (int i = MAX_PARAMS - 1; i >= 0; --i) {
2745 if (TRACE_BIND) System.out.println("Param "+i+":");
2746 BDD t8_i = actual.restrict(Z.ithVar(i)).and(V2cdomain);
2747 t8_i.replaceWith(V2toV1);
2748 if (TRACE_BIND) System.out.println("t8 = "+t8_i.toStringWithDomains());
2749 BDD t9_i = t8_i.relprod(vP, V1.set());
2750 if (TRACE_BIND) {
2751 System.out.println("t9 =");
2752 dumpWithV1c(t9_i, Iset.union(H1set));
2753 }
2754 t8_i.free();
2755
2756 t9_i.replaceWith(V1ctoV2c);
2757 BDD new_t9_i = t9_i.apply(old3_t9[i], BDDFactory.diff);
2758 old3_t9[i] = t9_i.id();
2759
2760
2761 newContext.andWith(new_t9_i.replace(H1toV1c[i]));
2762
2763
2764 new_t9_i.andWith(V1cH1equals[i].id());
2765 t9_i.andWith(V1cH1equals[i].id());
2766 BDD tb_i = new_t9_i.relprod(t6, V2cset);
2767 tb_i.orWith(t9_i.relprod(new_t6, V2cset));
2768 BDD formal_i = formal.restrict(Z.ithVar(i));
2769 BDD tc_i = tb_i.relprod(formal_i, Mset);
2770 formal_i.free(); tb_i.free();
2771 for (int j = 0; j < MAX_PARAMS; ++j) {
2772 if (i == j) continue;
2773 tc_i.andWith(V1c[j].domain());
2774 }
2775 if (TRACE_BIND) dumpVP(tc_i.exist(Iset));
2776 newPt.orWith(tc_i);
2777 }
2778
2779
2780
2781
2782 BDD newPt2 = newPt.relprod(newContext, V2cset.union(Iset));
2783 newPt.free();
2784 if (TRACE_BIND) dumpVP(newPt2);
2785
2786 if (FILTER_VP) newPt2.andWith(vPfilter.id());
2787 vP.orWith(newPt2);
2788
2789 newContext.andWith(t6.id());
2790 old3_t6 = t6;
2791 if (TRACE_BIND) System.out.println("context = "+newContext.toStringWithDomains());
2792 IEcs.orWith(newContext);
2793 }
2794 }
2795
2796 public boolean handleNewTargets() {
2797 if (TRACE_SOLVER) out.println("Handling new target methods...");
2798 BDD targets = IE.exist(Iset);
2799 targets.applyWith(visited.id(), BDDFactory.diff);
2800 if (targets.isZero()) return false;
2801 if (TRACE_SOLVER) out.println("New target methods: "+targets.satCount(Mset));
2802 while (!targets.isZero()) {
2803 BDD target = targets.satOne(Mset, false);
2804 int M_i = target.scanVar(M).intValue();
2805 jq_Method method = (jq_Method) Mmap.get(M_i);
2806 if(method != null){
2807 if (TRACE) out.println("New target method: "+method);
2808 visitMethod(method);
2809 } else {
2810 System.err.println("NULL method in handleNewTargets");
2811 }
2812 targets.applyWith(target, BDDFactory.diff);
2813 }
2814 return true;
2815 }
2816
2817 public void bindParameters() {
2818 if (INCREMENTAL2) {
2819 bindParameters_incremental();
2820 return;
2821 }
2822
2823 if (TRACE_SOLVER) out.println("Binding parameters...");
2824
2825 BDD my_IE = USE_VCONTEXT ? IEcs : IE;
2826
2827 if (TRACE_SOLVER) out.println("Call graph edges: "+my_IE.nodeCount());
2828
2829 BDD my_formal = CARTESIAN_PRODUCT ? formal.and(Z.varRange(0, MAX_PARAMS-1).not()) : formal;
2830 BDD my_actual = CARTESIAN_PRODUCT ? actual.and(Z.varRange(0, MAX_PARAMS-1).not()) : actual;
2831
2832 BDD t1 = my_IE.relprod(my_actual, Iset);
2833 BDD t2 = t1.relprod(my_formal, MZset);
2834 t1.free();
2835 if (TRACE_SOLVER) out.println("A before param bind: "+A.nodeCount());
2836 A.orWith(t2);
2837 if (TRACE_SOLVER) out.println("A after param bind: "+A.nodeCount());
2838
2839 if (TRACE_SOLVER) out.println("Binding return values...");
2840 BDD my_IEr = USE_VCONTEXT ? IEcs.replace(V1cV2ctoV2cV1c) : IE;
2841 BDD t3 = my_IEr.relprod(Iret, Iset);
2842 BDD t4 = t3.relprod(Mret, Mset);
2843 t3.free();
2844 if (TRACE_SOLVER) out.println("A before return bind: "+A.nodeCount());
2845 A.orWith(t4);
2846 if (TRACE_SOLVER) out.println("A after return bind: "+A.nodeCount());
2847
2848 if (TRACE_SOLVER) out.println("Binding exceptions...");
2849 BDD t5 = my_IEr.relprod(Ithr, Iset);
2850 if (USE_VCONTEXT) my_IEr.free();
2851 BDD t6 = t5.relprod(Mthr, Mset);
2852 t5.free();
2853 if (TRACE_SOLVER) out.println("A before exception bind: "+A.nodeCount());
2854 A.orWith(t6);
2855 if (TRACE_SOLVER) out.println("A after exception bind: "+A.nodeCount());
2856
2857 }
2858
2859 BDD old2_myIE;
2860 BDD old2_visited;
2861
2862 public void bindParameters_incremental() {
2863
2864 BDD my_IE = USE_VCONTEXT ? IEcs : IE;
2865 BDD new_myIE = my_IE.apply(old2_myIE, BDDFactory.diff);
2866
2867 BDD new_visited = visited.apply(old2_visited, BDDFactory.diff);
2868
2869
2870 new_myIE.orWith(old2_myIE.and(new_visited));
2871 old2_myIE.free();
2872 old2_visited.free();
2873 new_visited.free();
2874
2875 if (TRACE_SOLVER) out.println("New call graph edges: "+new_myIE.nodeCount());
2876
2877 BDD my_formal = CARTESIAN_PRODUCT ? formal.and(Z.varRange(0, MAX_PARAMS-1).not()) : formal;
2878 BDD my_actual = CARTESIAN_PRODUCT ? actual.and(Z.varRange(0, MAX_PARAMS-1).not()) : actual;
2879
2880 if (TRACE_SOLVER) out.println("Binding parameters...");
2881
2882 BDD t1 = new_myIE.relprod(my_actual, Iset);
2883 BDD t2 = t1.relprod(my_formal, MZset);
2884 t1.free();
2885 if (TRACE_SOLVER) out.println("A before param bind: "+A.nodeCount());
2886 A.orWith(t2);
2887 if (TRACE_SOLVER) out.println("A after param bind: "+A.nodeCount());
2888
2889 if (TRACE_SOLVER) out.println("Binding return values...");
2890 BDD new_myIEr = USE_VCONTEXT ? new_myIE.replace(V1cV2ctoV2cV1c) : new_myIE;
2891 BDD t3 = new_myIEr.relprod(Iret, Iset);
2892 BDD t4 = t3.relprod(Mret, Mset);
2893 t3.free();
2894 if (TRACE_SOLVER) out.println("A before return bind: "+A.nodeCount());
2895 A.orWith(t4);
2896 if (TRACE_SOLVER) out.println("A after return bind: "+A.nodeCount());
2897
2898 if (TRACE_SOLVER) out.println("Binding exceptions...");
2899 BDD t5 = new_myIEr.relprod(Ithr, Iset);
2900 if (USE_VCONTEXT) new_myIEr.free();
2901 BDD t6 = t5.relprod(Mthr, Mset);
2902 t5.free();
2903 if (TRACE_SOLVER) out.println("A before exception bind: "+A.nodeCount());
2904 A.orWith(t6);
2905 if (TRACE_SOLVER) out.println("A after exception bind: "+A.nodeCount());
2906
2907 new_myIE.free();
2908 old2_myIE = my_IE.id();
2909 old2_visited = visited.id();
2910 }
2911
2912 public void assumeKnownCallGraph() {
2913 if (VerifyAssertions)
2914 Assert._assert(!IE.isZero());
2915 handleNewTargets();
2916 addAllMethods();
2917 buildTypes();
2918 bindParameters();
2919 long time = System.currentTimeMillis();
2920 solvePointsTo();
2921 System.out.println("Solve points-to alone took "+(System.currentTimeMillis()-time)/1000.+"s");
2922 }
2923
2924 public void iterate() {
2925 BDD vP_old = vP.id();
2926 BDD IE_old = IE.id();
2927 boolean change;
2928 for (int major = 1; ; ++major) {
2929 change = false;
2930
2931 out.println("Discovering call graph, iteration "+major+": "+(int)visited.satCount(Mset)+" methods.");
2932 long time = System.currentTimeMillis();
2933 buildTypes();
2934 solvePointsTo();
2935 bindInvocations();
2936 if(RESOLVE_REFLECTION){
2937 if(USE_CASTS_FOR_REFLECTION){
2938 if(bindReflectionsWithCasts()){
2939 change = true;
2940 }
2941 }else{
2942 if(bindReflection()){
2943 change = true;
2944 }
2945 }
2946 }
2947 if(RESOLVE_FORNAME){
2948 if(bindForName()){
2949 change = true;
2950 }
2951 }
2952 if (handleNewTargets())
2953 change = true;
2954 if (!change && vP.equals(vP_old) && IE.equals(IE_old)) {
2955 if (TRACE_SOLVER) out.println("Finished after "+major+" iterations.");
2956 break;
2957 }
2958 vP_old.free(); vP_old = vP.id();
2959 IE_old.free(); IE_old = IE.id();
2960 addAllMethods();
2961 bindParameters();
2962 if (TRACE_SOLVER)
2963 out.println("Time spent: "+(System.currentTimeMillis()-time)/1000.);
2964 }
2965 }
2966
2967 public void numberPaths(CallGraph cg, ObjectCreationGraph ocg, boolean updateBits) {
2968 System.out.print("Counting size of call graph...");
2969 long time = System.currentTimeMillis();
2970 vCnumbering = countCallGraph(cg, ocg, updateBits);
2971 if(PRINT_CALL_GRAPH_SCCS){
2972 SCCPathNumbering sccNumbering = (SCCPathNumbering) vCnumbering;
2973 SCCTopSortedGraph sccGraph = sccNumbering.getSCCGraph();
2974 System.out.println("Printing the SCC in the call graph (" + sccGraph.list().size()+ ")");
2975 for(Iterator iter = sccGraph.list().iterator(); iter.hasNext(); ){
2976 SCComponent component = (SCComponent) iter.next();
2977
2978 if(component.size() < 2) continue;
2979 if(component.nodes() == null) continue;
2980
2981 System.out.print("\t" + component.getId() + "\t: " + component.nodes().length + "\t");
2982
2983 for(int i = 0; i < component.nodes().length; i++){
2984 Object node = component.nodes()[i];
2985 System.out.print(node.toString() + " ");
2986 }
2987 System.out.println("");
2988 }
2989 System.out.println("Done.");
2990 }
2991
2992 if (OBJECT_SENSITIVE) {
2993 oCnumbering = new SCCPathNumbering(objectPathSelector);
2994 BigInteger paths = (BigInteger) oCnumbering.countPaths(ocg);
2995 if (updateBits) {
2996 HC_BITS = VC_BITS = paths.bitLength();
2997 System.out.print("Object paths="+paths+" ("+VC_BITS+" bits), ");
2998 }
2999 }
3000 if (CONTEXT_SENSITIVE && MAX_HC_BITS > 1) {
3001 hCnumbering = countHeapNumbering(cg, updateBits);
3002 }
3003 time = System.currentTimeMillis() - time;
3004 System.out.println("done. ("+time/1000.+" seconds)");
3005 }
3006
3007 static CallGraph loadCallGraph(Collection roots) {
3008 if (new File(initialCallgraphFileName).exists()) {
3009 try {
3010 System.out.print("Loading initial call graph...");
3011 long time = System.currentTimeMillis();
3012 CallGraph cg = new LoadedCallGraph(initialCallgraphFileName);
3013 time = System.currentTimeMillis() - time;
3014 System.out.println("done. ("+time/1000.+" seconds)");
3015 if (cg.getRoots().containsAll(roots)) {
3016 roots = cg.getRoots();
3017
3018 return cg;
3019 } else {
3020 System.out.println("Call graph doesn't match named class, rebuilding...");
3021 cg = null;
3022 }
3023 } catch (IOException x) {
3024 x.printStackTrace();
3025 }
3026 }
3027 return null;
3028 }
3029
3030 public void addDefaults() {
3031
3032
3033 System.out.println("Adding default static variables.");
3034
3035
3036 GlobalNode.GLOBAL.addDefaultStatics();
3037
3038
3039 this.ocg = null;
3040
3041
3042
3043
3044
3045
3046
3047
3048
3049
3050 }
3051
3052 public void run(CallGraph cg, Collection rootMethods) throws IOException {
3053 run(null, cg, rootMethods);
3054 }
3055 public void run(String bddfactory, CallGraph cg, Collection rootMethods) throws IOException {
3056 addDefaults();
3057 initializeStubs();
3058
3059
3060 if (cg != null) {
3061 numberPaths(cg, ocg, true);
3062 }
3063
3064 if (CARTESIAN_PRODUCT && false) {
3065 VC_BITS = (HC_BITS + H_BITS) * MAX_PARAMS;
3066 System.out.println("Variable context bits = ("+HC_BITS+"+"+H_BITS+")*"+MAX_PARAMS+"="+VC_BITS);
3067 }
3068
3069
3070 initializeBDD(bddfactory);
3071 initializeMaps();
3072 this.rootMethods.addAll(rootMethods);
3073
3074 if (DUMP_SSA) {
3075 String dumppath = System.getProperty("pa.dumppath");
3076 if (dumppath != null) System.setProperty("bdddumpdir", dumppath);
3077 Object dummy = new Object();
3078 bddIRBuilder = new BuildBDDIR(bdd, M, Mmap, dummy);
3079 varorder += "_" + bddIRBuilder.getVarOrderDesc();
3080 System.out.println("Using variable ordering " + varorder);
3081 int[] ordering = bdd.makeVarOrdering(reverseLocal, varorder);
3082 bdd.setVarOrder(ordering);
3083 } else {
3084 bddIRBuilder = null;
3085 }
3086
3087
3088 if (cg != null) {
3089 System.out.print("Calculating call graph relation...");
3090 long time = System.currentTimeMillis();
3091 calculateIEfilter(cg);
3092 time = System.currentTimeMillis() - time;
3093 System.out.println("done. ("+time/1000.+" seconds)");
3094
3095
3096 if (CONTEXT_SENSITIVE && HC_BITS > 1) {
3097 System.out.print("Building var-heap context correspondence...");
3098 time = System.currentTimeMillis();
3099 buildVarHeapCorrespondence(cg);
3100 time = System.currentTimeMillis() - time;
3101 System.out.println("done. ("+time/1000.+" seconds)");
3102 } else if (THREAD_SENSITIVE) {
3103 buildThreadV1H1(thread_runs, cg);
3104 }
3105
3106
3107 if (!DISCOVER_CALL_GRAPH) {
3108 if (VerifyAssertions)
3109 Assert._assert(IEfilter != null);
3110 if (USE_VCONTEXT) {
3111 IEcs = IEfilter;
3112 IE = IEcs.exist(V1cV2cset);
3113 } else {
3114 IE = IEfilter;
3115 }
3116 }
3117 }
3118
3119
3120 long time = System.currentTimeMillis();
3121
3122
3123 visitGlobalNode(GlobalNode.GLOBAL);
3124 for (Iterator i = ConcreteObjectNode.getAll().iterator(); i.hasNext(); ) {
3125 ConcreteObjectNode con = (ConcreteObjectNode) i.next();
3126 visitGlobalNode(con);
3127 }
3128
3129
3130 for (Iterator i = rootMethods.iterator(); i.hasNext(); ) {
3131 jq_Method m = (jq_Method) i.next();
3132
3133
3134 if (ADD_ROOT_PLACEHOLDERS > 0) {
3135 addPlaceholdersForParams(m, ADD_ROOT_PLACEHOLDERS);
3136 }
3137
3138 visitMethod(m);
3139 }
3140
3141
3142 if (PUBLIC_PLACEHOLDERS > 0) {
3143 Iterator i;
3144 if (cg != null) i = cg.getAllMethods().iterator();
3145 else i = rootMethods.iterator();
3146 while (i.hasNext()) {
3147 jq_Method m = (jq_Method) i.next();
3148 if (!m.isPublic()) continue;
3149 addPlaceholdersForParams(m, PUBLIC_PLACEHOLDERS);
3150 }
3151 }
3152
3153
3154 handleNewTargets();
3155
3156
3157 if (OBJECT_SENSITIVE) {
3158 buildTypes();
3159 buildObjectSensitiveV1H1(ocg);
3160 }
3161
3162
3163
3164 addAllMethods();
3165
3166 System.out.println("Time spent initializing: "+(System.currentTimeMillis()-time)/1000.);
3167
3168 if (DISCOVER_CALL_GRAPH || OBJECT_SENSITIVE || CARTESIAN_PRODUCT && false) {
3169 Assert._assert(!SKIP_SOLVE);
3170 time = System.currentTimeMillis();
3171 iterate();
3172 System.out.println("Time spent solving: "+(System.currentTimeMillis()-time)/1000.);
3173 } else {
3174 if (DUMP_INITIAL) {
3175 buildTypes();
3176 try {
3177 long time2 = System.currentTimeMillis();
3178 dumpBDDRelations();
3179 System.out.println("Dump took "+(System.currentTimeMillis()-time2)/1000.+"s");
3180 if (DUMP_SSA) dumpSSA();
3181 } catch (IOException x) {}
3182 }
3183 if (SKIP_SOLVE) return;
3184 time = System.currentTimeMillis();
3185 assumeKnownCallGraph();
3186 System.out.println("Time spent solving: "+(System.currentTimeMillis()-time)/1000.);
3187 }
3188
3189 if(FIX_NO_DEST){
3190 analyzeIE();
3191 }
3192 if(REFLECTION_STAT){
3193 saveReflectionStats();
3194 }
3195 if(FORNAME_STAT){
3196 saveForNameStats();
3197 }
3198
3199
3200 printSizes();
3201
3202 System.out.println("Writing call graph...");
3203 time = System.currentTimeMillis();
3204 dumpCallGraph();
3205 System.out.println("Time spent writing: " + (System.currentTimeMillis() - time) / 1000.);
3206
3207 if (DUMP_RESULTS) {
3208 System.out.println("Writing results...");
3209 time = System.currentTimeMillis();
3210 dumpResults(resultsFileName);
3211 System.out.println("Time spent writing: "+(System.currentTimeMillis()-time)/1000.);
3212 }
3213 }
3214
3215 void saveReflectionStats() throws IOException {
3216 PrintWriter w = null;
3217 try {
3218 out.println("Saving reflection statistics in " + REFLECTION_STAT_FILE);
3219 w = new PrintWriter(new FileWriter(REFLECTION_STAT_FILE));
3220 BDD newInstanceCalls = IE.restrict(M.ithVar(Mmap.get(javaLangClass_newInstance)));
3221
3222 if(RESOLVE_REFLECTION){
3223 w.println("Used " + (USE_CASTS_FOR_REFLECTION ? "casts" : "strings") + " for reflection resolution.");
3224 }else{
3225 w.println("Reflection wasn't resolved.");
3226 }
3227 w.println("There are " + newInstanceCalls.satCount(Iset) + " calls to Class.newInstance");
3228
3229 int pos = 1;
3230 for(Iterator iter = newInstanceCalls.iterator(Iset); iter.hasNext(); pos++){
3231 BDD i = (BDD)iter.next();
3232 int i_i = i.scanVar(I).intValue();
3233 ProgramLocation mc = (ProgramLocation)Imap.get(i_i);
3234
3235 BDD callees = IE.relprod(i, Iset);
3236 if(!callees.isZero()){
3237 w.println("[" + pos + "]\t" + mc.toStringLong() + ": " +
3238
3239 (unresolvedCalls.contains(mc) ? "UNRESOLVED":""));
3240 for(Iterator iter2 = callees.iterator(Mset); iter2.hasNext();){
3241 BDD callee = (BDD)iter2.next();
3242
3243 int m_i = callee.scanVar(M).intValue();
3244 jq_Method m = (jq_Method)Mmap.get(m_i);
3245
3246 w.println("\t" + m.toString());
3247 }
3248 w.println();
3249 }
3250 }
3251 }finally{
3252 if(w != null) w.close();
3253 }
3254 }
3255
3256 void saveForNameStats() throws IOException {
3257 PrintWriter w = null;
3258 try {
3259 out.println("Saving forName statistics in " + FORNAME_STAT_FILE);
3260 w = new PrintWriter(new FileWriter(FORNAME_STAT_FILE));
3261 jq_Method forNameMethod = class_class.getDeclaredMethod("forName");
3262 BDD forNameCalls = IE.restrict(M.ithVar(Mmap.get(forNameMethod)));
3263
3264 if(RESOLVE_REFLECTION){
3265 w.println("Used " + (USE_CASTS_FOR_REFLECTION ? "casts" : "strings") + " for reflection resolution.");
3266 }else{
3267 w.println("Reflection wasn't resolved.");
3268 }
3269 w.println("There are " + forNameCalls.satCount(Iset) + " calls to Class.forName");
3270
3271 int pos = 1;
3272 for(Iterator iter = forNameCalls.iterator(Iset); iter.hasNext(); pos++){
3273 BDD i = (BDD)iter.next();
3274 int i_i = i.scanVar(I).intValue();
3275 ProgramLocation mc = (ProgramLocation)Imap.get(i_i);
3276
3277 BDD callees = IE.relprod(i, Iset);
3278 if(!callees.isZero()){
3279 w.println("[" + pos + "]\t" + mc.toStringLong() + ": " +
3280 (callees.satCount(Mset)==1 ? "UNRESOLVED":""));
3281
3282 for(Iterator iter2 = callees.iterator(Mset); iter2.hasNext();){
3283 BDD callee = (BDD)iter2.next();
3284
3285 int m_i = callee.scanVar(M).intValue();
3286 jq_Method m = (jq_Method)Mmap.get(m_i);
3287
3288 w.println("\t" + m.toString());
3289 }
3290 w.println();
3291 }
3292 }
3293 }finally{
3294 if(w != null) w.close();
3295 }
3296 }
3297
3298 Set provideStubsFor = new HashSet();
3299 /***
3300 * Initializes provideStubsFor.
3301 */
3302 private void initializeStubs() {
3303 {
3304 jq_Type c = jq_Class.parseType("java.sql.Connection");
3305 c.prepare();
3306 provideStubsFor.add(c);
3307 }
3308
3309 {
3310 jq_Type c = jq_Class.parseType("java.sql.Statement");
3311 c.prepare();
3312 provideStubsFor.add(c);
3313 }
3314 }
3315 static Collection readClassesFromFile(String fname) throws IOException {
3316 BufferedReader r = null;
3317 try {
3318 r = new BufferedReader(new FileReader(fname));
3319 Collection rootMethods = new ArrayList();
3320 String s = null;
3321 while ((s = r.readLine()) != null) {
3322 jq_Class c = (jq_Class) jq_Type.parseType(s);
3323 c.prepare();
3324 rootMethods.addAll(Arrays.asList(c.getDeclaredStaticMethods()));
3325 if (ADD_INSTANCE_METHODS)
3326 rootMethods.addAll(Arrays.asList(c.getDeclaredInstanceMethods()));
3327 }
3328 return rootMethods;
3329 } finally {
3330 if (r != null) r.close();
3331 }
3332 }
3333
3334 public static void main(String[] args) throws IOException {
3335 if (USE_JOEQ_CLASSLIBS) {
3336 System.setProperty("joeq.classlibinterface", "joeq.ClassLib.pa.Interface");
3337 joeq.ClassLib.ClassLibInterface.useJoeqClasslib(true);
3338 }
3339 HostedVM.initialize();
3340 CodeCache.AlwaysMap = true;
3341
3342 Collection rootMethods = null;
3343 if (args[0].startsWith("@")) {
3344 rootMethods = readClassesFromFile(args[0].substring(1));
3345 } else {
3346 jq_Class c = (jq_Class) jq_Type.parseType(args[0]);
3347 c.prepare();
3348
3349 rootMethods = Arrays.asList(c.getDeclaredStaticMethods());
3350 if (ADD_INSTANCE_METHODS) {
3351 jq_InstanceMethod[] ms = c.getDeclaredInstanceMethods();
3352 rootMethods = new ArrayList(rootMethods);
3353 rootMethods.addAll(Arrays.asList(ms));
3354 }
3355 }
3356
3357 if (args.length > 1) {
3358 for (Iterator i = rootMethods.iterator(); i.hasNext(); ) {
3359 jq_Method sm = (jq_Method) i.next();
3360 if (args[1].equals(sm.getName().toString())) {
3361 rootMethods = Collections.singleton(sm);
3362 break;
3363 }
3364 }
3365 }
3366
3367 PrimitivePA dis = new PrimitivePA();
3368 dis.cg = null;
3369 if (dis.CONTEXT_SENSITIVE || !dis.DISCOVER_CALL_GRAPH) {
3370 dis.cg = loadCallGraph(rootMethods);
3371 if (dis.cg == null && dis.AUTODISCOVER_CALL_GRAPH) {
3372 if (dis.CONTEXT_SENSITIVE || dis.OBJECT_SENSITIVE || dis.THREAD_SENSITIVE ||
3373 dis.SKIP_SOLVE) {
3374 System.out.println("Discovering call graph first...");
3375 dis.CONTEXT_SENSITIVE = false;
3376 dis.OBJECT_SENSITIVE = false;
3377 dis.THREAD_SENSITIVE = false;
3378 dis.CARTESIAN_PRODUCT = false;
3379 dis.DISCOVER_CALL_GRAPH = true;
3380 dis.CS_CALLGRAPH = false;
3381 dis.DUMP_INITIAL = false;
3382 dis.DUMP_RESULTS = false;
3383 dis.SKIP_SOLVE = false;
3384 dis.DUMP_FLY = false;
3385 dis.run("java", dis.cg, rootMethods);
3386 System.out.println("Finished discovering call graph.");
3387 dis = new PrimitivePA();
3388 initialCallgraphFileName = callgraphFileName;
3389 dis.cg = loadCallGraph(rootMethods);
3390 rootMethods = dis.cg.getRoots();
3391 } else if (!dis.DISCOVER_CALL_GRAPH) {
3392 System.out.println("Call graph doesn't exist yet, so turning on call graph discovery.");
3393 dis.DISCOVER_CALL_GRAPH = true;
3394 }
3395 } else if (dis.cg != null) {
3396 rootMethods = dis.cg.getRoots();
3397 }
3398 }
3399 dis.run(dis.cg, rootMethods);
3400
3401 if (WRITE_PARESULTS_BATCHFILE)
3402 writePAResultsBatchFile("runparesults");
3403 }
3404
3405 /***
3406 * write a file that when executed by shell runs PAResults in proper environment.
3407 */
3408 static void writePAResultsBatchFile(String batchfilename) throws IOException {
3409 PrintWriter w = null;
3410 try {
3411 w = new PrintWriter(new FileWriter(batchfilename));
3412 Properties p = System.getProperties();
3413 w.print(p.getProperty("java.home") + File.separatorChar + "bin" + File.separatorChar + "java");
3414 w.print(" -Xmx512M");
3415 w.print(" -classpath \"" + System.getProperty("java.class.path")+"\"");
3416 w.print(" -Djava.library.path=\"" + System.getProperty("java.library.path")+"\"");
3417 for (Iterator i = p.entrySet().iterator(); i.hasNext(); ) {
3418 Map.Entry e = (Map.Entry)i.next();
3419 String key = (String)e.getKey();
3420 String val = (String)e.getValue();
3421 if (key.startsWith("ms.") || key.startsWith("pa.")) {
3422 w.print(" -D" + key + "=" + val);
3423 }
3424 }
3425 w.println(" joeq.Compiler.Analysis.IPA.PAResults");
3426 } finally {
3427 if (w != null) w.close();
3428 }
3429 }
3430
3431 public void printSizes() {
3432 System.out.println("V = "+Vmap.size()+", bits = "+
3433 BigInteger.valueOf(Vmap.size()).bitLength());
3434 System.out.println("I = "+Imap.size()+", bits = "+
3435 BigInteger.valueOf(Imap.size()).bitLength());
3436 System.out.println("H = "+Hmap.size()+", bits = "+
3437 BigInteger.valueOf(Hmap.size()).bitLength());
3438 System.out.println("F = "+Fmap.size()+", bits = "+
3439 BigInteger.valueOf(Fmap.size()).bitLength());
3440 System.out.println("T = "+Tmap.size()+", bits = "+
3441 BigInteger.valueOf(Tmap.size()).bitLength());
3442 System.out.println("N = "+Nmap.size()+", bits = "+
3443 BigInteger.valueOf(Nmap.size()).bitLength());
3444 System.out.println("M = "+Mmap.size()+", bits = "+
3445 BigInteger.valueOf(Mmap.size()).bitLength());
3446 }
3447
3448 ToString TS = new ToString();
3449
3450
3451 public String longForm(Object o) {
3452 if (o == null || !LONG_LOCATIONS)
3453 return "";
3454
3455
3456 if (o instanceof ProgramLocation) {
3457 return " in "+((ProgramLocation)o).toStringLong();
3458 } else {
3459 try {
3460 Class c = o.getClass();
3461 try {
3462
3463 Method m = c.getMethod("getLocation", new Class[] {});
3464 ProgramLocation pl = (ProgramLocation)m.invoke(o, null);
3465 if (pl == null)
3466 throw new NoSuchMethodException();
3467 return " in "+pl.toStringLong();
3468 } catch (NoSuchMethodException _1) {
3469 try {
3470
3471 Method m = c.getMethod("getMethod", new Class[] {});
3472 return " " + m.invoke(o, null);
3473 } catch (NoSuchMethodException _2) {
3474 try {
3475
3476 Method m = c.getMethod("getDefiningMethod", new Class[] {});
3477 return " " + m.invoke(o, null);
3478 } catch (NoSuchMethodException _3) {
3479 }
3480 }
3481 }
3482 } catch (InvocationTargetException _) {
3483 } catch (IllegalAccessException _) {
3484 }
3485 }
3486 return "";
3487 }
3488
3489 String findInMap(IndexedMap map, int j) {
3490 String jp = "("+j+")";
3491 if (j < map.size() && j >= 0) {
3492 Object o = map.get(j);
3493 jp += o + longForm(o);
3494 return jp;
3495 } else {
3496 return jp+"<index not in map>";
3497 }
3498 }
3499
3500 public class ToString extends BDD.BDDToString {
3501 public String elementName(int i, BigInteger j) {
3502 switch (i) {
3503 case 0:
3504 case 1: return findInMap(Vmap, j.intValue());
3505 case 2: return findInMap(Imap, j.intValue());
3506 case 3: return findInMap(Imap, j.intValue());
3507 case 4: return findInMap(Hmap, j.intValue());
3508 case 5: return j.toString();
3509 case 6: return findInMap(Fmap, j.intValue());
3510 case 7:
3511 case 8: return findInMap(Tmap, j.intValue());
3512 case 9: return findInMap(Nmap, j.intValue());
3513 case 10: return findInMap(Mmap, j.intValue());
3514 case 11: return findInMap(Mmap, j.intValue());
3515 default: return "("+j+")"+"??";
3516 }
3517 }
3518 public String elementNames(int i, BigInteger j, BigInteger k) {
3519
3520 return super.elementNames(i, j, k);
3521 }
3522 }
3523
3524 private void dumpCallGraphAsDot(CallGraph cg, String dotFileName) throws IOException {
3525 PathNumbering pn = countCallGraph(cg, null, false);
3526 dumpCallGraphAsDot(pn, cg, dotFileName);
3527 }
3528 private void dumpCallGraphAsDot(PathNumbering pn, CallGraph cg, String dotFileName) throws IOException {
3529 if (pn != null) {
3530 BufferedWriter dos = null;
3531 try {
3532 dos = new BufferedWriter(new FileWriter(dotFileName));
3533 pn.dotGraph(dos, cg.getRoots(), cg.getCallSiteNavigator());
3534 } finally {
3535 if (dos != null) dos.close();
3536 }
3537 }
3538 }
3539
3540 public void dumpCallGraph() throws IOException {
3541
3542 CallGraph callgraph = new CachedCallGraph(new PrimitivePACallGraph(this));
3543
3544 BufferedWriter dos = null;
3545 try {
3546 dos = new BufferedWriter(new FileWriter(callgraphFileName));
3547 LoadedCallGraph.write(callgraph, dos);
3548 } finally {
3549 if (dos != null) dos.close();
3550 }
3551
3552 }
3553
3554 public static List activeDomains(BDD r) {
3555 BDDVarSet s = r.support();
3556 BDDDomain[] a = s.getDomains();
3557 s.free();
3558 List result = Arrays.asList(a);
3559 return result;
3560 }
3561
3562 public static String getName(BDDDomain d) {
3563 String s = d.getName();
3564 if (s.equals("V1c")) return "VC0";
3565 if (s.equals("V2c")) return "VC1";
3566 if (s.endsWith("2")) return s.substring(0, s.length()-1)+"1";
3567 if (s.endsWith("1")) return s.substring(0, s.length()-1)+"0";
3568 return s+"0";
3569 }
3570
3571 public static void bdd_save(String filename, BDD b) throws IOException {
3572 List ds = activeDomains(b);
3573 if (ds == null) {
3574 b.getFactory().save(filename, b);
3575 } else {
3576 bdd_save(filename, b, ds);
3577 }
3578 }
3579
3580 public static void bdd_save(String filename, BDD b, List ds) throws IOException {
3581 BufferedWriter out = null;
3582 try {
3583 out = new BufferedWriter(new FileWriter(filename));
3584 out.write('#');
3585 for (Iterator i = ds.iterator(); i.hasNext(); ) {
3586 BDDDomain d = (BDDDomain) i.next();
3587 out.write(' ');
3588 out.write(getName(d));
3589 out.write(':');
3590 out.write(Integer.toString(d.varNum()));
3591 }
3592 out.write('\n');
3593 for (Iterator i = ds.iterator(); i.hasNext(); ) {
3594 BDDDomain d = (BDDDomain) i.next();
3595 out.write('#');
3596 int[] vars = d.vars();
3597 for (int j = 0; j < vars.length; ++j) {
3598 out.write(' ');
3599 out.write(Integer.toString(vars[j]));
3600 }
3601 out.write('\n');
3602 }
3603 b.getFactory().save(out, b);
3604 } finally {
3605 if (out != null) try { out.close(); } catch (IOException _) { }
3606 }
3607 }
3608
3609 public void dumpResults(String dumpfilename) throws IOException {
3610
3611 System.out.println("A: "+(long) A.satCount(V1V2set)+" relations, "+A.nodeCount()+" nodes");
3612 bdd_save(dumpfilename+".A", A);
3613 System.out.println("vP: "+(long) vP.satCount(V1H1set)+" relations, "+vP.nodeCount()+" nodes");
3614 bdd_save(dumpfilename+".vP", vP);
3615
3616 System.out.println("S: "+(long) S.satCount(V1FV2set)+" relations, "+S.nodeCount()+" nodes");
3617 bdd_save(dumpfilename+".S", S);
3618 System.out.println("L: "+(long) L.satCount(V1FV2set)+" relations, "+L.nodeCount()+" nodes");
3619 bdd_save(dumpfilename+".L", L);
3620 System.out.println("vT: "+(long) vT.satCount(V1.set().union(T1set))+" relations, "+vT.nodeCount()+" nodes");
3621 bdd_save(dumpfilename+".vT", vT);
3622 System.out.println("hT: "+(long) hT.satCount(H1.set().union(T2set))+" relations, "+hT.nodeCount()+" nodes");
3623 bdd_save(dumpfilename+".hT", hT);
3624 System.out.println("aT: "+(long) aT.satCount(T1set.union(T2set))+" relations, "+aT.nodeCount()+" nodes");
3625 bdd_save(dumpfilename+".aT", aT);
3626 System.out.println("cha: "+(long) cha.satCount(T2Nset.union(Mset))+" relations, "+cha.nodeCount()+" nodes");
3627 bdd_save(dumpfilename+".cha", cha);
3628 System.out.println("actual: "+(long) actual.satCount(Iset.union(Zset).union(V2.set()))+" relations, "+actual.nodeCount()+" nodes");
3629 bdd_save(dumpfilename+".actual", actual);
3630 System.out.println("formal: "+(long) formal.satCount(MZset.union(V1.set()))+" relations, "+formal.nodeCount()+" nodes");
3631 bdd_save(dumpfilename+".formal", formal);
3632 System.out.println("Iret: "+(long) Iret.satCount(Iset.union(V1.set()))+" relations, "+Iret.nodeCount()+" nodes");
3633 bdd_save(dumpfilename+".Iret", Iret);
3634 System.out.println("Mret: "+(long) Mret.satCount(Mset.union(V2.set()))+" relations, "+Mret.nodeCount()+" nodes");
3635 bdd_save(dumpfilename+".Mret", Mret);
3636 System.out.println("Ithr: "+(long) Ithr.satCount(Iset.union(V1.set()))+" relations, "+Ithr.nodeCount()+" nodes");
3637 bdd_save(dumpfilename+".Ithr", Ithr);
3638 System.out.println("Mthr: "+(long) Mthr.satCount(Mset.union(V2.set()))+" relations, "+Mthr.nodeCount()+" nodes");
3639 bdd_save(dumpfilename+".Mthr", Mthr);
3640 System.out.println("mI: "+(long) mI.satCount(INset.union(Mset))+" relations, "+mI.nodeCount()+" nodes");
3641 bdd_save(dumpfilename+".mI", mI);
3642 System.out.println("mV: "+(long) mV.satCount(Mset.union(V1.set()))+" relations, "+mV.nodeCount()+" nodes");
3643 bdd_save(dumpfilename+".mV", mV);
3644 System.out.println("sync: "+(long) sync.satCount(V1.set())+" relations, "+sync.nodeCount()+" nodes");
3645 bdd_save(dumpfilename+".sync", sync);
3646
3647 System.out.println("hP: "+(long) hP.satCount(H1FH2set)+" relations, "+hP.nodeCount()+" nodes");
3648 bdd_save(dumpfilename+".hP", hP);
3649
3650 System.out.println("IE: "+(long) IE.satCount(IMset)+" relations, "+IE.nodeCount()+" nodes");
3651 bdd_save(dumpfilename+".IE", IE);
3652 BuildBDDIR.dumpTuples(bdd, dumpfilename+".IE.tuples", IE);
3653 if (IEcs != null) {
3654 System.out.println("IEcs: "+(long) IEcs.satCount(IMset.union(V1cV2cset))+" relations, "+IEcs.nodeCount()+" nodes");
3655 bdd_save(dumpfilename+".IEcs", IEcs);
3656 }
3657 if (vPfilter != null) {
3658 System.out.println("vPfilter: "+(long) vPfilter.satCount(V1.set().union(H1.set()))+" relations, "+vPfilter.nodeCount()+" nodes");
3659 bdd_save(dumpfilename+".vPfilter", vPfilter);
3660 }
3661 if (hPfilter != null) {
3662 System.out.println("hPfilter: "+(long) hPfilter.satCount(H1.set().union(Fset).union(H1.set()))+" relations, "+hPfilter.nodeCount()+" nodes");
3663 bdd_save(dumpfilename+".hPfilter", hPfilter);
3664 }
3665 if (IEfilter != null) {
3666 System.out.println("IEfilter: "+IEfilter.nodeCount()+" nodes");
3667 bdd_save(dumpfilename+".IEfilter", IEfilter);
3668 }
3669 if (NNfilter != null) {
3670 System.out.println("NNfilter: "+NNfilter.nodeCount()+" nodes");
3671 bdd_save(dumpfilename+".NNfilter", NNfilter);
3672 }
3673 System.out.println("visited: "+(long) visited.satCount(Mset)+" relations, "+visited.nodeCount()+" nodes");
3674 bdd_save(dumpfilename+".visited", visited);
3675
3676 BufferedWriter dos = null;
3677 try {
3678 dos = new BufferedWriter(new FileWriter(dumpfilename+".config"));
3679 dumpConfig(dos);
3680 } finally {
3681 if (dos != null) dos.close();
3682 }
3683
3684 System.out.print("Dumping maps...");
3685 dos = null;
3686 try {
3687 dos = new BufferedWriter(new FileWriter(dumpfilename+".Vmap"));
3688 Vmap.dump(dos);
3689 } finally {
3690 if (dos != null) dos.close();
3691 }
3692 dos = null;
3693 try {
3694 dos = new BufferedWriter(new FileWriter(dumpfilename+".Imap"));
3695 Imap.dump(dos);
3696 } finally {
3697 if (dos != null) dos.close();
3698 }
3699 dos = null;
3700 try {
3701 dos = new BufferedWriter(new FileWriter(dumpfilename+".Hmap"));
3702 Hmap.dump(dos);
3703 } finally {
3704 if (dos != null) dos.close();
3705 }
3706 dos = null;
3707 try {
3708 dos = new BufferedWriter(new FileWriter(dumpfilename+".Fmap"));
3709 Fmap.dump(dos);
3710 } finally {
3711 if (dos != null) dos.close();
3712 }
3713 dos = null;
3714 try {
3715 dos = new BufferedWriter(new FileWriter(dumpfilename+".Tmap"));
3716 Tmap.dump(dos);
3717 } finally {
3718 if (dos != null) dos.close();
3719 }
3720 dos = null;
3721 try {
3722 dos = new BufferedWriter(new FileWriter(dumpfilename+".Nmap"));
3723 Nmap.dump(dos);
3724 } finally {
3725 if (dos != null) dos.close();
3726 }
3727 dos = null;
3728 try {
3729 dos = new BufferedWriter(new FileWriter(dumpfilename+".Mmap"));
3730 Mmap.dump(dos);
3731 } finally {
3732 if (dos != null) dos.close();
3733 }
3734 System.out.println("done.");
3735 }
3736
3737 public static PrimitivePA loadResults(String bddfactory, String loaddir, String loadfilename) throws IOException {
3738 PrimitivePA pa = new PrimitivePA();
3739 BufferedReader di = null;
3740 try {
3741 di = new BufferedReader(new FileReader(loaddir+loadfilename+".config"));
3742 pa.loadConfig(di);
3743 } finally {
3744 if (di != null) di.close();
3745 }
3746 System.out.print("Initializing...");
3747 pa.initializeBDD(bddfactory);
3748 System.out.println("done.");
3749
3750 System.out.print("Loading results from "+loaddir+loadfilename+"...");
3751 if (loaddir.length() == 0) loaddir = "."+System.getProperty("file.separator");
3752 File dir = new File(loaddir);
3753 final String prefix = loadfilename + ".";
3754 File[] files = dir.listFiles(new FilenameFilter() {
3755 public boolean accept(File dir, String name) {
3756 return name.startsWith(prefix);
3757 }
3758 });
3759 for (int i = 0; i < files.length; ++i) {
3760 File f = files[i];
3761 if (f.isDirectory()) continue;
3762 String name = f.getName().substring(prefix.length());
3763 try {
3764 Field field = PA.class.getDeclaredField(name);
3765 if (field == null) continue;
3766 if (field.getType() == net.sf.javabdd.BDD.class) {
3767 System.out.print(name+": ");
3768 BDD b = pa.bdd.load(f.getAbsolutePath());
3769 System.out.print(b.nodeCount()+" nodes, ");
3770 field.set(pa, b);
3771 } else if (field.getType() == IndexMap.class) {
3772 System.out.print(name+": ");
3773 di = null;
3774 try {
3775 di = new BufferedReader(new FileReader(f));
3776 IndexMap m = IndexMap.load(name, di);
3777 System.out.print(m.size()+" entries, ");
3778 field.set(pa, m);
3779 } finally {
3780 if (di != null) di.close();
3781 }
3782 } else {
3783 System.out.println();
3784 System.out.println("Cannot load field: "+field);
3785 }
3786 } catch (NoSuchFieldException e) {
3787 } catch (IllegalArgumentException e) {
3788 Assert.UNREACHABLE();
3789 } catch (IllegalAccessException e) {
3790 Assert.UNREACHABLE();
3791 }
3792 }
3793 System.out.println("done.");
3794
3795
3796 if (pa.A instanceof TypedBDD) {
3797 Set set = TypedBDDFactory.makeSet();
3798 set.add(pa.V1); set.add(pa.V2);
3799 set.addAll(Arrays.asList(pa.V1c)); set.addAll(Arrays.asList(pa.V2c));
3800 ((TypedBDD) pa.A).setDomains(set);
3801 }
3802 if (pa.vP instanceof TypedBDD) {
3803 Set set = TypedBDDFactory.makeSet();
3804 set.add(pa.V1); set.add(pa.H1);
3805 set.addAll(Arrays.asList(pa.V1c)); set.addAll(Arrays.asList(pa.H1c));
3806 ((TypedBDD) pa.vP).setDomains(set);
3807 }
3808 if (pa.S instanceof TypedBDD) {
3809 Set set = TypedBDDFactory.makeSet();
3810 set.add(pa.V1); set.add(pa.V2); set.add(pa.F);
3811 set.addAll(Arrays.asList(pa.V1c)); set.addAll(Arrays.asList(pa.V2c));
3812 ((TypedBDD) pa.S).setDomains(set);
3813 }
3814 if (pa.L instanceof TypedBDD) {
3815 Set set = TypedBDDFactory.makeSet();
3816 set.add(pa.V1); set.add(pa.V2); set.add(pa.F);
3817 set.addAll(Arrays.asList(pa.V1c)); set.addAll(Arrays.asList(pa.V2c));
3818 ((TypedBDD) pa.L).setDomains(set);
3819 }
3820 if (pa.vT instanceof TypedBDD)
3821 ((TypedBDD) pa.vT).setDomains(pa.V1, pa.T1);
3822 if (pa.hT instanceof TypedBDD)
3823 ((TypedBDD) pa.hT).setDomains(pa.H1, pa.T2);
3824 if (pa.aT instanceof TypedBDD)
3825 ((TypedBDD) pa.aT).setDomains(pa.T1, pa.T2);
3826 if (pa.cha instanceof TypedBDD)
3827 ((TypedBDD) pa.cha).setDomains(pa.T2, pa.N, pa.M);
3828 if (pa.actual instanceof TypedBDD)
3829 ((TypedBDD) pa.actual).setDomains(pa.I, pa.Z, pa.V2);
3830 if (pa.formal instanceof TypedBDD)
3831 ((TypedBDD) pa.formal).setDomains(pa.M, pa.Z, pa.V1);
3832 if (pa.Iret instanceof TypedBDD)
3833 ((TypedBDD) pa.Iret).setDomains(pa.I, pa.V1);
3834 if (pa.Mret instanceof TypedBDD)
3835 ((TypedBDD) pa.Mret).setDomains(pa.M, pa.V2);
3836 if (pa.Ithr instanceof TypedBDD)
3837 ((TypedBDD) pa.Ithr).setDomains(pa.I, pa.V1);
3838 if (pa.Mthr instanceof TypedBDD)
3839 ((TypedBDD) pa.Mthr).setDomains(pa.M, pa.V2);
3840 if (pa.mI instanceof TypedBDD)
3841 ((TypedBDD) pa.mI).setDomains(pa.M, pa.I, pa.N);
3842 if (pa.mV instanceof TypedBDD)
3843 ((TypedBDD) pa.mV).setDomains(pa.M, pa.V1);
3844 if (pa.sync instanceof TypedBDD)
3845 ((TypedBDD) pa.sync).setDomains(pa.V1);
3846 if (pa.mSync instanceof TypedBDD)
3847 ((TypedBDD) pa.sync).setDomains(pa.M);
3848
3849 if (pa.fT instanceof TypedBDD)
3850 ((TypedBDD) pa.fT).setDomains(pa.F, pa.T2);
3851 if (pa.fC instanceof TypedBDD)
3852 ((TypedBDD) pa.fC).setDomains(pa.F, pa.T2);
3853
3854 if (pa.hP instanceof TypedBDD) {
3855 Set set = TypedBDDFactory.makeSet();
3856 set.add(pa.H1); set.add(pa.H2); set.add(pa.F);
3857 set.addAll(Arrays.asList(pa.H1c)); set.addAll(Arrays.asList(pa.H2c));
3858 ((TypedBDD) pa.hP).setDomains(set);
3859 }
3860 if (pa.IE instanceof TypedBDD)
3861 ((TypedBDD) pa.IE).setDomains(pa.I, pa.M);
3862 if (pa.IEcs instanceof TypedBDD) {
3863 Set set = TypedBDDFactory.makeSet();
3864 set.add(pa.I); set.add(pa.M);
3865 set.addAll(Arrays.asList(pa.V2c)); set.addAll(Arrays.asList(pa.V1c));
3866 ((TypedBDD) pa.IEcs).setDomains(set);
3867 }
3868 if (pa.vPfilter instanceof TypedBDD)
3869 ((TypedBDD) pa.vPfilter).setDomains(pa.V1, pa.H1);
3870 if (pa.hPfilter instanceof TypedBDD)
3871 ((TypedBDD) pa.hPfilter).setDomains(pa.H1, pa.F, pa.H2);
3872 if (pa.IEfilter instanceof TypedBDD) {
3873 Set set = TypedBDDFactory.makeSet();
3874 set.add(pa.I); set.add(pa.M);
3875 set.addAll(Arrays.asList(pa.V2c)); set.addAll(Arrays.asList(pa.V1c));
3876 ((TypedBDD) pa.IEfilter).setDomains(set);
3877 }
3878 if (pa.NNfilter instanceof TypedBDD)
3879 ((TypedBDD) pa.NNfilter).setDomains(pa.H1);
3880
3881 if (pa.visited instanceof TypedBDD)
3882 ((TypedBDD) pa.visited).setDomains(pa.M);
3883
3884 return pa;
3885 }
3886
3887 private void dumpConfig(BufferedWriter out) throws IOException {
3888 out.write("V="+V_BITS+"\n");
3889 out.write("I="+I_BITS+"\n");
3890 out.write("H="+H_BITS+"\n");
3891 out.write("Z="+Z_BITS+"\n");
3892 out.write("F="+F_BITS+"\n");
3893 out.write("T="+T_BITS+"\n");
3894 out.write("N="+N_BITS+"\n");
3895 out.write("M="+M_BITS+"\n");
3896 out.write("VC="+VC_BITS+"\n");
3897 out.write("HC="+HC_BITS+"\n");
3898 out.write("CS="+(CONTEXT_SENSITIVE?"yes":"no")+"\n");
3899 out.write("OS="+(OBJECT_SENSITIVE?"yes":"no")+"\n");
3900 out.write("TS="+(THREAD_SENSITIVE?"yes":"no")+"\n");
3901 out.write("CP="+(CARTESIAN_PRODUCT?"yes":"no")+"\n");
3902 out.write("Order="+varorder+"\n");
3903 out.write("Reverse="+reverseLocal+"\n");
3904 }
3905
3906 private void loadConfig(BufferedReader in) throws IOException {
3907 for (;;) {
3908 String s = in.readLine();
3909 if (s == null) break;
3910 int index = s.indexOf('=');
3911 if (index == -1) index = s.length();
3912 String s1 = s.substring(0, index);
3913 String s2 = index < s.length() ? s.substring(index+1) : null;
3914 if (s1.equals("V")) {
3915 V_BITS = Integer.parseInt(s2);
3916 } else if (s1.equals("I")) {
3917 I_BITS = Integer.parseInt(s2);
3918 } else if (s1.equals("H")) {
3919 H_BITS = Integer.parseInt(s2);
3920 } else if (s1.equals("Z")) {
3921 Z_BITS = Integer.parseInt(s2);
3922 } else if (s1.equals("F")) {
3923 F_BITS = Integer.parseInt(s2);
3924 } else if (s1.equals("T")) {
3925 T_BITS = Integer.parseInt(s2);
3926 } else if (s1.equals("N")) {
3927 N_BITS = Integer.parseInt(s2);
3928 } else if (s1.equals("M")) {
3929 M_BITS = Integer.parseInt(s2);
3930 } else if (s1.equals("VC")) {
3931 VC_BITS = Integer.parseInt(s2);
3932 } else if (s1.equals("HC")) {
3933 HC_BITS = Integer.parseInt(s2);
3934 } else if (s1.equals("CS")) {
3935 CONTEXT_SENSITIVE = s2.equals("yes");
3936 } else if (s1.equals("OS")) {
3937 OBJECT_SENSITIVE = s2.equals("yes");
3938 } else if (s1.equals("TS")) {
3939 THREAD_SENSITIVE = s2.equals("yes");
3940 } else if (s1.equals("CP")) {
3941 CARTESIAN_PRODUCT = s2.equals("yes");
3942 } else if (s1.equals("Order")) {
3943 varorder = s2;
3944 } else if (s1.equals("Reverse")) {
3945 reverseLocal = s2.equals("true");
3946 } else {
3947 System.err.println("Unknown config option "+s);
3948 }
3949 }
3950 if (VC_BITS > 1 || HC_BITS > 1) {
3951 MAX_VC_BITS = VC_BITS;
3952 MAX_HC_BITS = HC_BITS;
3953 }
3954 }
3955
3956 public static class ThreadRootMap extends AbstractMap {
3957 Map map;
3958 ThreadRootMap(Map s) {
3959 map = s;
3960 }
3961 public Object get(Object o) {
3962 Set s = (Set) map.get(o);
3963 if (s == null) return new Integer(0);
3964 return new Integer(s.size()-1);
3965 }
3966
3967
3968
3969 public Set entrySet() {
3970 HashMap m = new HashMap();
3971 for (Iterator i = map.keySet().iterator(); i.hasNext(); ) {
3972 Object o = i.next();
3973 m.put(o, get(o));
3974 }
3975 return m.entrySet();
3976 }
3977 }
3978
3979
3980 static Map thread_runs = new HashMap();
3981 IndexMap threadNumbers;
3982
3983 public int getThreadRunIndex(jq_Method m, Node n) {
3984 if (!threadNumbers.contains(n)) {
3985
3986 return -1;
3987 }
3988 return threadNumbers.get(n);
3989 }
3990
3991 public PathNumbering countCallGraph(CallGraph cg, ObjectCreationGraph ocg, boolean updateBits) {
3992 jq_Class jlt = PrimordialClassLoader.getJavaLangThread();
3993 jlt.prepare();
3994 jq_Class jlr = (jq_Class) PrimordialClassLoader.loader.getOrCreateBSType("Ljava/lang/Runnable;");
3995 jlr.prepare();
3996 Set fields = new HashSet();
3997 IndexMap classes = new IndexMap("classes");
3998 int vars = 0, heaps = 0, bcodes = 0, methods = 0, calls = 0;
3999 int threads = 0;
4000 for (Iterator i = cg.getAllMethods().iterator(); i.hasNext(); ) {
4001 jq_Method m = (jq_Method) i.next();
4002 if (TRACE_OBJECT) out.println("Counting "+m);
4003 ++methods;
4004 jq_Class c = m.isStatic() ? null : m.getDeclaringClass();
4005 if (m.getBytecode() == null) {
4006 jq_Type retType = m.getReturnType();
4007 if (retType instanceof jq_Reference) {
4008 boolean b = !classes.contains(retType);
4009 classes.get(retType);
4010 if (b)
4011 ++heaps;
4012
4013
4014
4015 }
4016 continue;
4017 }
4018 bcodes += m.getBytecode().length;
4019 PrimitiveMethodSummary ms = PrimitiveMethodSummary.getSummary(m);
4020 for (Iterator j = ms.nodeIterator(); j.hasNext(); ) {
4021 Node n = (Node) j.next();
4022 ++vars;
4023 if (n instanceof ConcreteTypeNode ||
4024 n instanceof UnknownTypeNode ||
4025 n instanceof ConcreteObjectNode) {
4026 ++heaps;
4027 jq_Type type = n.getDeclaredType();
4028 if (type != null && type != jq_NullType.NULL_TYPE) {
4029 type.prepare();
4030 if (type.isSubtypeOf(jlt) ||
4031 type.isSubtypeOf(jlr)) {
4032 jq_Method rm = ((jq_Class)type).getVirtualMethod(run_method);
4033 Set s = (Set) thread_runs.get(rm);
4034 if (s == null) thread_runs.put(rm, s = new HashSet());
4035 s.add(n);
4036 ++threads;
4037 }
4038
4039
4040
4041 }
4042 }
4043 fields.addAll(n.getAccessPathEdgeFields());
4044 fields.addAll(n.getNonEscapingEdgeFields());
4045 if (n instanceof GlobalNode) continue;
4046 jq_Type r = (jq_Type) n.getDeclaredType();
4047 classes.get(r);
4048 }
4049 calls += ms.getCalls().size()*8;
4050 }
4051 if (ADD_SUPERTYPES) {
4052 for (int i = 0; i < classes.size(); ++i) {
4053 jq_Type t1 = (jq_Type) classes.get(i);
4054 if (t1 == null || t1 instanceof jq_NullType || !(t1 instanceof jq_Reference)) continue;
4055 t1.prepare();
4056 jq_Reference t0 = (jq_Reference) t1;
4057 jq_Reference t2 = t0.getDirectPrimarySupertype();
4058 if (t2 != null) {
4059 t2.prepare();
4060 classes.get(t2);
4061 }
4062 jq_Class[] c = t0.getInterfaces();
4063 for (int j = 0; j < c.length; ++j) {
4064 classes.get(c[j]);
4065 }
4066 }
4067 }
4068 System.out.println();
4069 System.out.println("Methods="+methods+" Bytecodes="+bcodes+" Call sites="+calls);
4070 System.out.println("Vars="+vars+" Heaps="+heaps+" Classes="+classes.size()+" Fields="+fields.size());
4071 PathNumbering pn = null;
4072 if (CONTEXT_SENSITIVE) {
4073 if(BETTER_CONTEXT_NUMBERING){
4074 Set sccs = SCComponent.buildSCC(cg);
4075 SCCTopSortedGraph graph = SCCTopSortedGraph.topSort(sccs);
4076
4077 Selector selector = null;
4078 if(USE_STRING_METHOD_SELECTOR) {
4079 System.err.println("Using a StringMethodSelector");
4080 selector = new StringMethodSelector(graph);
4081 } else {
4082 System.err.println("Using a VarPathSelector");
4083 selector = varPathSelector;
4084 }
4085 System.err.println("Using GlobalPathNumbering");
4086 pn = new GlobalPathNumbering(selector);
4087 } else {
4088 pn = new SCCPathNumbering(varPathSelector);
4089 }
4090 } else {
4091 pn = null;
4092 }
4093 Map initialCounts = null;
4094 BigInteger paths = null;
4095 if (pn != null) {
4096 paths = (BigInteger) pn.countPaths(cg.getRoots(), cg.getCallSiteNavigator(), initialCounts);
4097 }
4098 if (updateBits) {
4099 V_BITS = BigInteger.valueOf(vars+256).bitLength();
4100 I_BITS = BigInteger.valueOf(calls).bitLength();
4101 H_BITS = BigInteger.valueOf(heaps).bitLength()+2;
4102 F_BITS = BigInteger.valueOf(fields.size()+64).bitLength();
4103 T_BITS = BigInteger.valueOf(classes.size()+64).bitLength();
4104 N_BITS = I_BITS;
4105 M_BITS = BigInteger.valueOf(methods).bitLength() + 1;
4106 if (CONTEXT_SENSITIVE) {
4107 System.out.println("Thread runs="+thread_runs);
4108 VC_BITS = paths.bitLength();
4109 if (VC_BITS > MAX_VC_BITS)
4110 System.out.println("Trimming var context bits from "+VC_BITS);
4111 VC_BITS = Math.min(MAX_VC_BITS, VC_BITS);
4112 System.out.println("Paths="+paths+", Var context bits="+VC_BITS);
4113 } else if (THREAD_SENSITIVE) {
4114 ++threads;
4115 VC_BITS = HC_BITS = BigInteger.valueOf(threads).bitLength();
4116 System.out.println("Threads="+threads+", context bits="+VC_BITS);
4117 }
4118 System.out.println(" V="+V_BITS+" I="+I_BITS+" H="+H_BITS+
4119 " F="+F_BITS+" T="+T_BITS+" N="+N_BITS+
4120 " M="+M_BITS+" VC="+VC_BITS);
4121 }
4122 if (DUMP_DOTGRAPH) {
4123 try {
4124 dumpCallGraphAsDot(pn, cg, callgraphFileName + ".dot");
4125 } catch (IOException x) {
4126 x.printStackTrace();
4127 }
4128 }
4129
4130 return pn;
4131 }
4132
4133 public final VarPathSelector varPathSelector = new VarPathSelector(MAX_VC_BITS);
4134
4135 public static boolean THREADS_ONLY = false;
4136 public static class VarPathSelector implements Selector {
4137
4138 int maxBits;
4139
4140 VarPathSelector(int max_bits) {
4141 this.maxBits = max_bits;
4142 }
4143
4144
4145
4146
4147 public boolean isImportant(Object a, Object b, BigInteger num) {
4148 if (num.bitLength() > maxBits) return false;
4149 if (THREADS_ONLY) {
4150 if (b instanceof ProgramLocation) return true;
4151 jq_Method m = (jq_Method) a;
4152 if (m.getNameAndDesc() == main_method) return true;
4153 if (m.getNameAndDesc() == run_method) return true;
4154 return false;
4155 }
4156 return true;
4157 }
4158
4159
4160
4161
4162 public boolean isImportant(SCComponent scc1, SCComponent scc2, BigInteger num) {
4163 if (num.bitLength() > maxBits) return false;
4164 if (THREADS_ONLY) {
4165 Set s = scc2.nodeSet();
4166 Iterator i = s.iterator();
4167 Object o = i.next();
4168 if (i.hasNext()) return false;
4169 jq_Method m = (jq_Method) scc1.nodes()[0];
4170 return isImportant(m, o, num);
4171 }
4172 return true;
4173 }
4174 }
4175
4176 public final HeapPathSelector heapPathSelector = new HeapPathSelector();
4177
4178 static Set polyClasses;
4179 static void initPolyClasses() {
4180 if (polyClasses != null) return;
4181 polyClasses = new HashSet();
4182 File f = new File("polyclasses");
4183 if (f.exists()) {
4184 BufferedReader in = null;
4185 try {
4186 in = new BufferedReader(new FileReader(f));
4187 for (;;) {
4188 String s = in.readLine();
4189 if (s == null) break;
4190 polyClasses.add(jq_Type.parseType(s));
4191 }
4192 } catch (FileNotFoundException e) {
4193 e.printStackTrace();
4194 } catch (IOException e) {
4195 e.printStackTrace();
4196 } finally {
4197 if (in != null) try { in.close(); } catch (IOException _) {}
4198 }
4199 }
4200 }
4201
4202 public static boolean MATCH_FACTORY = false;
4203
4204 public class HeapPathSelector implements Selector {
4205
4206 jq_Class collection_class = (jq_Class) PrimordialClassLoader.loader.getOrCreateBSType("Ljava/util/Collection;");
4207 jq_Class map_class = (jq_Class) PrimordialClassLoader.loader.getOrCreateBSType("Ljava/util/Map;");
4208 jq_Class throwable_class = (jq_Class) PrimordialClassLoader.getJavaLangThrowable();
4209 HeapPathSelector() {
4210 initPolyClasses();
4211 collection_class.prepare();
4212 map_class.prepare();
4213 throwable_class.prepare();
4214 }
4215
4216
4217
4218
4219 public boolean isImportant(SCComponent scc1, SCComponent scc2, BigInteger num) {
4220 if (num.bitLength() > MAX_HC_BITS) return false;
4221 Set s = scc2.nodeSet();
4222 Iterator i = s.iterator();
4223 Object o = i.next();
4224 if (i.hasNext()) return false;
4225 return isImportant(scc1, o, num);
4226 }
4227
4228
4229
4230
4231 public boolean isImportant(Object p, Object o, BigInteger num) {
4232 if (num.bitLength() > MAX_HC_BITS) return false;
4233 if (o instanceof ProgramLocation) return true;
4234 jq_Method m = (jq_Method) o;
4235 if (m.getNameAndDesc() == main_method) return true;
4236 if (m.getNameAndDesc() == run_method) return true;
4237 if (m.getBytecode() == null) return false;
4238 if (MATCH_FACTORY) {
4239 if (!m.getReturnType().isReferenceType()) return false;
4240 PrimitiveMethodSummary ms = PrimitiveMethodSummary.getSummary(CodeCache.getCode(m));
4241 for (Iterator i = ms.getReturned().iterator(); i.hasNext(); ) {
4242 Node n = (Node) i.next();
4243 if (!(n instanceof ConcreteTypeNode)) {
4244
4245 }
4246 jq_Type type = n.getDeclaredType();
4247 if (type == null) {
4248 return false;
4249 }
4250 type.prepare();
4251 if (!polyClasses.isEmpty() && !polyClasses.contains(type))
4252 return false;
4253 if (type.isSubtypeOf(throwable_class))
4254 return false;
4255
4256
4257
4258 }
4259 }
4260 return true;
4261 }
4262 }
4263
4264 public final ObjectPathSelector objectPathSelector = new ObjectPathSelector();
4265
4266 public class ObjectPathSelector implements Selector {
4267
4268 jq_Class throwable_class = (jq_Class) PrimordialClassLoader.getJavaLangThrowable();
4269 ObjectPathSelector() {
4270 throwable_class.prepare();
4271 }
4272
4273
4274
4275
4276 public boolean isImportant(Object p, Object o, BigInteger num) {
4277 if (o instanceof jq_Array) {
4278 if (!((jq_Array) o).getElementType().isReferenceType()) {
4279 if (TRACE_OBJECT) out.println("No object sensitivity for "+o+": PRIMITIVE ARRAY");
4280 return false;
4281 }
4282 } else if (o instanceof jq_Class) {
4283 jq_Class c = (jq_Class) o;
4284 if (c == PrimordialClassLoader.getJavaLangString()) {
4285 if (TRACE_OBJECT) out.println("No object sensitivity for "+c+": STRING");
4286 return false;
4287 }
4288 c.prepare();
4289 if (c.isSubtypeOf(throwable_class)) {
4290 if (TRACE_OBJECT) out.println("No object sensitivity for "+c+": THROWABLE");
4291 return false;
4292 }
4293 boolean hasReferenceMember = false;
4294 jq_InstanceField[] f = c.getInstanceFields();
4295 for (int j = 0; j < f.length; ++j) {
4296 if (f[j].getType().isReferenceType()) {
4297 hasReferenceMember = true;
4298 break;
4299 }
4300 }
4301 if (!hasReferenceMember) {
4302 if (TRACE_OBJECT) out.println("No object sensitivity for "+c+": NO REF FIELDS");
4303 return false;
4304 }
4305 }
4306 return true;
4307 }
4308
4309
4310
4311
4312 public boolean isImportant(SCComponent scc1, SCComponent scc2, BigInteger num) {
4313 Set s = scc2.nodeSet();
4314 Iterator i = s.iterator();
4315 Object o = i.next();
4316 if (i.hasNext()) {
4317 if (TRACE_OBJECT) out.println("No object sensitivity for "+s+": CYCLE");
4318 return false;
4319 }
4320 return isImportant(scc1, o, num);
4321 }
4322 }
4323
4324 public class StringMethodSelector implements Selector {
4325 SCComponent select;
4326
4327 StringMethodSelector(SCCTopSortedGraph sccGraph){
4328 this.select = getSelectSCC(sccGraph);
4329 }
4330
4331 private SCComponent getSelectSCC(SCCTopSortedGraph sccGraph) {
4332 jq_Class string_buffer_class = (jq_Class) PrimordialClassLoader.loader.getOrCreateBSType("Ljava/lang/StringBuffer;");
4333 Assert._assert(string_buffer_class != null);
4334 string_buffer_class.prepare();
4335 jq_InstanceMethod string_buffer_append = null;
4336 jq_InstanceMethod[] methods = string_buffer_class.getDeclaredInstanceMethods();
4337
4338 for(int i = 0; i < methods.length; i++) {
4339 jq_InstanceMethod m = methods[i];
4340 if(m.getNameAndDesc().toString().equals("append (Ljava/lang/String;)Ljava/lang/StringBuffer;")) {
4341 string_buffer_append = m;
4342 break;
4343 }else{
4344
4345 }
4346 }
4347 Assert._assert(string_buffer_append != null, "No append method found in " + string_buffer_class);
4348
4349
4350 SCComponent string_buffer_append_scc = null;
4351 for(SCComponent c = sccGraph.getFirst(); c.nextTopSort() != null; c = c.nextTopSort()) {
4352
4353 if(c.contains(string_buffer_append)) {
4354 string_buffer_append_scc = c;
4355 break;
4356 }
4357 }
4358 Assert._assert(string_buffer_append_scc != null, "Can't find method " + string_buffer_append + " in any SCC");
4359 if(TRACE_SELECTORS) System.err.println("SCC # " + string_buffer_append_scc + " contains " + string_buffer_append);
4360
4361 return string_buffer_append_scc;
4362 }
4363
4364 StringMethodSelector(SCComponent select){
4365 this.select = select;
4366 }
4367 /***
4368 * Return true if the edge scc1->scc2 is important.
4369 */
4370 public boolean isImportant(SCComponent scc1, SCComponent scc2, BigInteger num) {
4371 Assert._assert(false);
4372
4373 return false;
4374 }
4375
4376 /***
4377 * Return true if the edge a->b is important.
4378 */
4379 public boolean isImportant(Object a, Object b, BigInteger num) {
4380 boolean result;
4381
4382 if (b instanceof ProgramLocation) {
4383 result = true;
4384 } else {
4385 jq_Method m = (jq_Method) b;
4386 result = select.contains(m);
4387 }
4388 if(TRACE_SELECTORS && result) System.err.println("isImportant(" + a + ", " + b + ") = " + result);
4389
4390 return result;
4391 }
4392 }
4393
4394 public PathNumbering countHeapNumbering(CallGraph cg, boolean updateBits) {
4395 if (VerifyAssertions)
4396 Assert._assert(CONTEXT_SENSITIVE);
4397 PathNumbering pn;
4398 if (THREAD_SENSITIVE) pn = new RootPathNumbering();
4399 else pn = new SCCPathNumbering(heapPathSelector);
4400 Map initialCounts = null;
4401 BigInteger paths = (BigInteger) pn.countPaths(cg.getRoots(), cg.getCallSiteNavigator(), initialCounts);
4402 System.out.println("Number of paths for heap context sensitivity: "+paths);
4403 if (updateBits) {
4404 HC_BITS = paths.bitLength();
4405 if (HC_BITS > MAX_HC_BITS)
4406 System.out.println("Trimming heap context bits from "+HC_BITS);
4407 HC_BITS = Math.min(HC_BITS, MAX_HC_BITS);
4408 System.out.println("Heap context bits="+HC_BITS);
4409 }
4410 return pn;
4411 }
4412
4413 void calculateIEfilter(CallGraph cg) {
4414 IEfilter = bdd.zero();
4415 IEcs = bdd.zero();
4416 for (Iterator i = cg.getAllCallSites().iterator(); i.hasNext(); ) {
4417 ProgramLocation mc = (ProgramLocation) i.next();
4418 mc = LoadedCallGraph.mapCall(mc);
4419
4420 int I_i = Imap.get(mc);
4421 for (Iterator j = cg.getTargetMethods(mc).iterator(); j.hasNext(); ) {
4422 jq_Method callee = (jq_Method) j.next();
4423 int M_i = Mmap.get(callee);
4424 BDD context;
4425 if (CONTEXT_SENSITIVE) {
4426 Pair p = new Pair(mc, callee);
4427 Range r_edge = vCnumbering.getEdge(p);
4428 Range r_caller = vCnumbering.getRange(mc.getMethod());
4429 Assert._assert(r_edge != null, "No edge for " + p);
4430 Assert._assert(r_caller != null, "No range for " + mc.getMethod());
4431 context = buildContextMap(V2c[0],
4432 PathNumbering.toBigInt(r_caller.low),
4433 PathNumbering.toBigInt(r_caller.high),
4434 V1c[0],
4435 PathNumbering.toBigInt(r_edge.low),
4436 PathNumbering.toBigInt(r_edge.high));
4437 } else {
4438 if (USE_VCONTEXT) context = V1cdomain.and(V2cdomain);
4439 else context = bdd.one();
4440 }
4441 context.andWith(I.ithVar(I_i));
4442 context.andWith(M.ithVar(M_i));
4443 IEfilter.orWith(context);
4444 }
4445 }
4446 }
4447
4448 BDDPairing V1ctoH1c;
4449 public BDD getV1H1Context(jq_Method m) {
4450 if (THREAD_SENSITIVE) {
4451 BDD b = (BDD) V1H1correspondence.get(m);
4452 if (b == null) System.out.println("Unknown method "+m);
4453 if (V1ctoH1c == null) V1ctoH1c = bdd.makePair(V1c[0], H1c[0]);
4454 BDD c = b.replace(V1ctoH1c);
4455 return c.andWith(b.id());
4456 } else if (CONTEXT_SENSITIVE) {
4457 if (V1H1correspondence != null)
4458 return (BDD) V1H1correspondence.get(m);
4459 Range r1 = vCnumbering.getRange(m);
4460 BDD b = V1c[0].varRange(r1.low.longValue(), r1.high.longValue());
4461 if (USE_HCONTEXT)
4462 b.andWith(H1c[0].ithVar(0));
4463 return b;
4464 } else if (OBJECT_SENSITIVE) {
4465 jq_Class c = m.isStatic() ? null : m.getDeclaringClass();
4466 BDD result = (BDD) V1H1correspondence.get(c);
4467 if (result == null) {
4468 if (TRACE_OBJECT) out.println("Note: "+c+" is not in object creation graph.");
4469
4470
4471 return result;
4472 }
4473 return result.id();
4474 } else if (CARTESIAN_PRODUCT && false) {
4475
4476 BDD context;
4477 if (USE_HCONTEXT) context = V1cdomain.and(H1cdomain);
4478 else context = V1cdomain.id();
4479 return context;
4480 } else {
4481 return null;
4482 }
4483 }
4484
4485 public void buildThreadV1H1(Map threadNodes, CallGraph g) {
4486 out.println("Building thread map.");
4487 threadNumbers = new IndexMap("Thread");
4488 V1H1correspondence = new HashMap();
4489 Navigator nav = g.getMethodNavigator();
4490 threadNumbers.get("main");
4491 for (Iterator i = g.getRoots().iterator(); i.hasNext(); ) {
4492 Object o = i.next();
4493 if (threadNodes.containsKey(o)) continue;
4494 BDD b = V1c[0].ithVar(0);
4495 V1H1correspondence.put(o, b);
4496 }
4497 for (Iterator i = threadNodes.entrySet().iterator(); i.hasNext(); ) {
4498 Map.Entry e = (Map.Entry) i.next();
4499 Object o = e.getKey();
4500 BDD b;
4501 V1H1correspondence.put(o, b = bdd.zero());
4502 Collection s = (Collection) e.getValue();
4503 for (Iterator j = s.iterator(); j.hasNext(); ) {
4504 Node n = (Node) j.next();
4505 int k = threadNumbers.get(n);
4506 if (TRACE) System.out.println("Thread "+k+": "+n);
4507 b.orWith(V1c[0].ithVar(k));
4508 }
4509 }
4510 boolean change;
4511 do {
4512 change = false;
4513 for (Iterator i = Traversals.reversePostOrder(nav, g.getRoots()).iterator(); i.hasNext(); ) {
4514 Object o = i.next();
4515 BDD b = (BDD) V1H1correspondence.get(o);
4516 if (b == null) {
4517 V1H1correspondence.put(o, b = bdd.zero());
4518 Assert._assert(!threadNodes.containsKey(o));
4519 change = true;
4520 }
4521 for (Iterator j2 = nav.prev(o).iterator(); j2.hasNext(); ) {
4522 Object o2 = j2.next();
4523 BDD b2 = (BDD) V1H1correspondence.get(o2);
4524 if (b2 != null) {
4525 BDD old = b.id();
4526 b.orWith(b2.id());
4527 change |= !old.equals(b);
4528 old.free();
4529 }
4530 }
4531 if (TRACE) out.println("Map for "+o+": "+b.toStringWithDomains());
4532 }
4533 } while (change);
4534
4535 V1H1correspondence.put(null, V1c[0].ithVar(0));
4536 }
4537
4538 public void buildObjectSensitiveV1H1(ObjectCreationGraph g) {
4539 if (TRACE_OBJECT) out.println("Building object-sensitive V1H1");
4540 V1H1correspondence = new HashMap();
4541 rangeMap = new HashMap();
4542 rangeMap.put(null, new Range(BigInteger.ZERO, BigInteger.ZERO));
4543 Navigator nav = g.getNavigator();
4544 for (Iterator i = Traversals.reversePostOrder(nav, g.getRoots()).iterator();
4545 i.hasNext(); ) {
4546 Object o = i.next();
4547 if (o instanceof Node) {
4548 if (TRACE_OBJECT) out.println("Skipping "+o);
4549 continue;
4550 }
4551 jq_Reference c1 = (jq_Reference) o;
4552 Range r1 = oCnumbering.getRange(c1);
4553 if (c1 instanceof jq_Class) {
4554 jq_Class c = (jq_Class) c1;
4555 while (c != null) {
4556 Range r = (Range) rangeMap.get(c);
4557 if (r == null || r.high.longValue() < r1.high.longValue()) {
4558 rangeMap.put(c, r1);
4559 }
4560 c = c.getSuperclass();
4561 }
4562 }
4563 if (TRACE_OBJECT) out.println(c1+" Range "+r1);
4564
4565 BDD b = bdd.zero();
4566 for (Iterator j = nav.next(c1).iterator(); j.hasNext(); ) {
4567 Object p = j.next();
4568 Node node;
4569 jq_Reference c2;
4570 Range r2;
4571 if (TRACE_OBJECT) out.println("Edge "+c1+" -> "+p);
4572 if (p instanceof jq_Reference) {
4573
4574 node = null;
4575 c2 = (jq_Reference) p;
4576 r2 = oCnumbering.getEdge(c1, c2);
4577 } else {
4578 node = (Node) p;
4579 Collection next = nav.next(node);
4580 if (VerifyAssertions)
4581 Assert._assert(next.size() == 1);
4582 if (VerifyAssertions)
4583 Assert._assert(r1.equals(oCnumbering.getEdge(c1, node)));
4584 c2 = (jq_Reference) next.iterator().next();
4585 r2 = oCnumbering.getEdge(node, c2);
4586 }
4587
4588 int T_i = Tmap.get(c2);
4589
4590 BDD T_bdd = T2.ithVar(T_i);
4591 BDD heap;
4592 if (node == null) {
4593
4594
4595 heap = hT.restrict(T_bdd);
4596 if (VerifyAssertions)
4597 Assert._assert(!heap.isZero(), c2.toString());
4598 } else {
4599 int H_i = Hmap.get(node);
4600 heap = H1.ithVar(H_i);
4601 }
4602 T_bdd.free();
4603 if (TRACE_OBJECT) out.println(c1+" creation site "+node+" "+c2+" Range: "+r2);
4604 BDD cm;
4605 cm = buildContextMap(V1c[0],
4606 PathNumbering.toBigInt(r1.low),
4607 PathNumbering.toBigInt(r1.high),
4608 H1c[0],
4609 PathNumbering.toBigInt(r2.low),
4610 PathNumbering.toBigInt(r2.high));
4611 cm.andWith(heap);
4612 b.orWith(cm);
4613 }
4614 if (TRACE_OBJECT) out.println("Registering V1H1 for "+c1);
4615 V1H1correspondence.put(c1, b);
4616 }
4617 }
4618
4619 public void buildObjectSensitiveV1H1_(ObjectCreationGraph g) {
4620 V1H1correspondence = new HashMap();
4621 rangeMap = new HashMap();
4622 rangeMap.put(null, new Range(BigInteger.ZERO, BigInteger.ZERO));
4623 Navigator nav = g.getNavigator();
4624 for (Iterator i = Traversals.reversePostOrder(nav, g.getRoots()).iterator();
4625 i.hasNext(); ) {
4626 jq_Reference c1 = (jq_Reference) i.next();
4627 Range r1 = oCnumbering.getRange(c1);
4628 if (c1 instanceof jq_Class) {
4629 jq_Class c = (jq_Class) c1;
4630 while (c != null) {
4631 Range r = (Range) rangeMap.get(c);
4632 if (r == null || r.high.longValue() < r1.high.longValue()) {
4633 rangeMap.put(c, r1);
4634 }
4635 c = c.getSuperclass();
4636 }
4637 }
4638
4639 BDD b = bdd.zero();
4640 for (Iterator j = nav.next(c1).iterator(); j.hasNext(); ) {
4641 jq_Reference c2 = (jq_Reference) j.next();
4642 int T_i = Tmap.get(c2);
4643
4644 BDD T_bdd = T2.ithVar(T_i);
4645 BDD heap = hT.restrict(T_bdd);
4646 T_bdd.free();
4647 Range r2 = oCnumbering.getEdge(c1, c2);
4648 BDD cm;
4649 cm = buildContextMap(V1c[0],
4650 PathNumbering.toBigInt(r1.low),
4651 PathNumbering.toBigInt(r1.high),
4652 H1c[0],
4653 PathNumbering.toBigInt(r2.low),
4654 PathNumbering.toBigInt(r2.high));
4655 cm.andWith(heap);
4656 b.orWith(cm);
4657 }
4658 V1H1correspondence.put(c1, b);
4659 }
4660 }
4661
4662 Map V1H1correspondence;
4663
4664 public void buildVarHeapCorrespondence(CallGraph cg) {
4665 if (VerifyAssertions)
4666 Assert._assert(CONTEXT_SENSITIVE);
4667 BDDPairing V2cH2ctoV1cH1c = bdd.makePair();
4668 V2cH2ctoV1cH1c.set(V2c, V1c);
4669 V2cH2ctoV1cH1c.set(H2c, H1c);
4670
4671 V1H1correspondence = new HashMap();
4672 for (Iterator i = cg.getAllMethods().iterator(); i.hasNext(); ) {
4673 jq_Method m = (jq_Method) i.next();
4674 Range r1 = vCnumbering.getRange(m);
4675 Range r2 = hCnumbering.getRange(m);
4676 BDD relation;
4677 if (r1.equals(r2)) {
4678 relation = V1c[0].buildAdd(H1c[0], BigInteger.valueOf(r1.high.longValue()).bitLength(), 0);
4679 relation.andWith(V1c[0].varRange(r1.low.longValue(), r1.high.longValue()));
4680 } else {
4681 long v_val = r1.high.longValue()+1;
4682 long h_val = r2.high.longValue()+1;
4683
4684 if (h_val == 1L) {
4685 relation = V1c[0].varRange(r1.low.longValue(), r1.high.longValue());
4686 relation.andWith(H1c[0].ithVar(0));
4687 } else {
4688 int v_bits = BigInteger.valueOf(v_val).bitLength();
4689 int h_bits = BigInteger.valueOf(h_val).bitLength();
4690
4691 h_val = 1 << h_bits;
4692
4693 int[] v = new int[v_bits];
4694 for (int j = 0; j < v_bits; ++j) {
4695 v[j] = V1c[0].vars()[j];
4696 }
4697 BDDBitVector v_vec = bdd.buildVector(v);
4698 BDDBitVector z = v_vec.divmod(h_val, false);
4699
4700
4701
4702
4703
4704
4705
4706 BDDBitVector h_vec = bdd.buildVector(H1c[0]);
4707
4708 relation = bdd.one();
4709 int n;
4710 for (n = 0; n < h_vec.size() || n < v_vec.size(); n++) {
4711 BDD a = (n < v_vec.size()) ? z.getBit(n) : bdd.zero();
4712 BDD b = (n < h_vec.size()) ? h_vec.getBit(n) : bdd.zero();
4713 relation.andWith(a.biimp(b));
4714 }
4715 for ( ; n < V1c[0].varNum() || n < H1c[0].varNum(); n++) {
4716 if (n < V1c[0].varNum())
4717 relation.andWith(bdd.nithVar(V1c[0].vars()[n]));
4718 if (n < H1c[0].varNum())
4719 relation.andWith(bdd.nithVar(H1c[0].vars()[n]));
4720 }
4721 relation.andWith(V1c[0].varRange(r1.low.longValue(), r1.high.longValue()));
4722
4723 v_vec.free(); h_vec.free(); z.free();
4724 }
4725 }
4726 V1H1correspondence.put(m, relation);
4727 }
4728 }
4729
4730 public void buildExactVarHeapCorrespondence(CallGraph cg) {
4731 if (VerifyAssertions)
4732 Assert._assert(CONTEXT_SENSITIVE);
4733 BDDPairing V2cH2ctoV1cH1c = bdd.makePair();
4734 V2cH2ctoV1cH1c.set(V2c, V1c);
4735 V2cH2ctoV1cH1c.set(H2c, H1c);
4736 BDDPairing V2ctoV1c = bdd.makePair();
4737 V2ctoV1c.set(V2c, V1c);
4738 BDDPairing H2ctoH1c = bdd.makePair();
4739 H2ctoH1c.set(H2c, H1c);
4740
4741 V1H1correspondence = new HashMap();
4742 for (Iterator i = cg.getRoots().iterator(); i.hasNext(); ) {
4743 jq_Method root = (jq_Method) i.next();
4744 Range r1 = vCnumbering.getRange(root);
4745 Range r2 = hCnumbering.getRange(root);
4746 BDD relation;
4747 if (r1.equals(r2)) {
4748 relation = V1c[0].buildAdd(H1c[0], BigInteger.valueOf(r1.high.longValue()).bitLength(), 0);
4749 relation.andWith(V1c[0].varRange(r1.low.longValue(), r1.high.longValue()));
4750 System.out.println("Root "+root+" numbering: "+relation.toStringWithDomains());
4751 } else {
4752 System.out.println("Root numbering doesn't match: "+root);
4753
4754 relation = V1c[0].varRange(r1.low.longValue(), r1.high.longValue());
4755 relation.andWith(H1c[0].varRange(r2.low.longValue(), r2.high.longValue()));
4756 }
4757 V1H1correspondence.put(root, relation);
4758 }
4759 List rpo = Traversals.reversePostOrder(cg.getMethodNavigator(), cg.getRoots());
4760 for (Iterator i = rpo.iterator(); i.hasNext(); ) {
4761 jq_Method callee = (jq_Method) i.next();
4762
4763 BDD calleeRelation;
4764 calleeRelation = (BDD) V1H1correspondence.get(callee);
4765 if (calleeRelation == null)
4766 calleeRelation = bdd.zero();
4767 for (Iterator j = cg.getCallers(callee).iterator(); j.hasNext(); ) {
4768 ProgramLocation cs = (ProgramLocation) j.next();
4769 jq_Method caller = cs.getMethod();
4770 BDD callerRelation = (BDD) V1H1correspondence.get(caller);
4771 if (callerRelation == null) continue;
4772 Range r1_caller = vCnumbering.getRange(caller);
4773 Range r1_edge = vCnumbering.getEdge(cs, callee);
4774 Range r2_caller = hCnumbering.getRange(caller);
4775 Range r2_edge = hCnumbering.getEdge(cs, callee);
4776 BDD cm1;
4777 BDD tmpRel;
4778 boolean r1_same = r1_caller.equals(r1_edge);
4779 boolean r2_same = r2_caller.equals(r2_edge);
4780 if (!r1_same) {
4781 cm1 = buildContextMap(V1c[0],
4782 PathNumbering.toBigInt(r1_caller.low),
4783 PathNumbering.toBigInt(r1_caller.high),
4784 V2c[0],
4785 PathNumbering.toBigInt(r1_edge.low),
4786 PathNumbering.toBigInt(r1_edge.high));
4787 tmpRel = callerRelation.relprod(cm1, V1cset);
4788 cm1.free();
4789 } else {
4790 tmpRel = callerRelation.id();
4791 }
4792 BDD tmpRel2;
4793 if (!r2_same) {
4794 cm1 = buildContextMap(H1c[0],
4795 PathNumbering.toBigInt(r2_caller.low),
4796 PathNumbering.toBigInt(r2_caller.high),
4797 H2c[0],
4798 PathNumbering.toBigInt(r2_edge.low),
4799 PathNumbering.toBigInt(r2_edge.high));
4800 tmpRel2 = tmpRel.relprod(cm1, H1cset);
4801 tmpRel.free();
4802 cm1.free();
4803 } else {
4804 tmpRel2 = tmpRel;
4805 }
4806 if (!r1_same) {
4807 if (!r2_same) {
4808 tmpRel2.replaceWith(V2cH2ctoV1cH1c);
4809 } else {
4810 tmpRel2.replaceWith(V2ctoV1c);
4811 }
4812 } else if (!r2_same) {
4813 tmpRel2.replaceWith(H2ctoH1c);
4814 }
4815 calleeRelation.orWith(tmpRel2);
4816 }
4817 V1H1correspondence.put(callee, calleeRelation);
4818 }
4819 }
4820
4821 BDD mS;
4822 BDD mL;
4823 BDD mvP;
4824 BDD mIE;
4825 BDD visitedFly;
4826 void initFly() {
4827 mS = bdd.zero();
4828 mL = bdd.zero();
4829 mvP = bdd.zero();
4830 mIE = bdd.zero();
4831 visitedFly = bdd.zero();
4832 for (Iterator i = rootMethods.iterator(); i.hasNext(); ) {
4833 jq_Method m = (jq_Method) i.next();
4834 int m_i = Mmap.get(m);
4835 visitedFly.orWith(M.ithVar(m_i));
4836 }
4837
4838 for (Iterator i = newMethodSummaries.entrySet().iterator(); i.hasNext(); ) {
4839 Map.Entry e = (Map.Entry) i.next();
4840 jq_Method m = (jq_Method) e.getKey();
4841 PrimitivePAMethodSummary s = (PrimitivePAMethodSummary) e.getValue();
4842 int m_i = Mmap.get(m);
4843 BDD b = M.ithVar(m_i);
4844 mS.orWith(b.and(s.S));
4845 mL.orWith(b.and(s.L));
4846 mvP.orWith(b.and(s.vP));
4847 mIE.orWith(b.and(s.IE));
4848 s.free(); b.free();
4849 }
4850 }
4851
4852 BDD getRoots() {
4853 BDD b = bdd.zero();
4854 if (cg == null) {
4855 return b;
4856 }
4857 for (Iterator i = cg.getRoots().iterator(); i.hasNext(); ) {
4858 jq_Method m = (jq_Method) i.next();
4859 b.orWith(M.ithVar(Mmap.get(m)));
4860 }
4861 return b;
4862 }
4863
4864 void addToNmap(jq_Method m) {
4865 Assert._assert(!m.isStatic());
4866 Assert._assert(!m.isPrivate());
4867 Nmap.get(m);
4868 jq_Class c = m.getDeclaringClass().getSuperclass();
4869 if (c != null) {
4870 jq_Method m2 = c.getVirtualMethod(m.getNameAndDesc());
4871 if (m2 != null) addToNmap(m2);
4872 }
4873 jq_Class[] cs = m.getDeclaringClass().getDeclaredInterfaces();
4874 for (int i = 0; i < cs.length; ++i) {
4875 jq_Class interf = cs[i];
4876 jq_Method m3 = interf.getVirtualMethod(m.getNameAndDesc());
4877 if (m3 != null) addToNmap(m3);
4878 }
4879 }
4880
4881 public void dumpBDDRelations() throws IOException {
4882
4883 if (FULL_CHA) {
4884 for (Iterator i = Mmap.iterator(); i.hasNext(); ) {
4885 Object o = i.next();
4886 if (o instanceof jq_Method) {
4887 jq_Method m = (jq_Method) o;
4888 if (m.isStatic() || m.isPrivate()) continue;
4889 addToNmap(m);
4890 }
4891 }
4892 buildTypes();
4893 }
4894
4895
4896 BDD S0 = S.exist(V1cV2cset);
4897 BDD L0 = L.exist(V1cV2cset);
4898 BDD IE0 = IE.exist(V1cV2cset);
4899 BDD vP0 = vP.exist(V1cH1cset);
4900
4901 String dumpPath = System.getProperty("pa.dumppath", "");
4902 if (dumpPath.length() > 0) {
4903 File f = new File(dumpPath);
4904 if (!f.exists()) f.mkdirs();
4905 String sep = System.getProperty("file.separator", "/");
4906 if (!dumpPath.endsWith(sep))
4907 dumpPath += sep;
4908 }
4909 System.out.println("Dumping to path "+dumpPath);
4910
4911 BufferedWriter dos = null;
4912 try {
4913 dos = new BufferedWriter(new FileWriter(dumpPath+"bddinfo"));
4914 for (int i = 0; i < bdd.numberOfDomains(); ++i) {
4915 BDDDomain d = bdd.getDomain(i);
4916 if (d == V1 || d == V2)
4917 dos.write("V\n");
4918 else if (d == H1 || d == H2)
4919 dos.write("H\n");
4920 else if (d == T1 || d == T2)
4921 dos.write("T\n");
4922 else if (d == F)
4923 dos.write("F\n");
4924 else if (d == I || d == I2)
4925 dos.write("I\n");
4926 else if (d == Z)
4927 dos.write("Z\n");
4928 else if (d == N)
4929 dos.write("N\n");
4930 else if (d == M || d == M2)
4931 dos.write("M\n");
4932 else if (Arrays.asList(V1c).contains(d)
4933 || Arrays.asList(V2c).contains(d))
4934 dos.write("VC\n");
4935 else if (Arrays.asList(H1c).contains(d)
4936 || Arrays.asList(H2c).contains(d))
4937 dos.write("HC\n");
4938 else if (DUMP_SSA) {
4939 dos.write(bddIRBuilder.getDomainName(d)+"\n");
4940 } else
4941 dos.write(d.toString() + "\n");
4942 }
4943 } finally {
4944 if (dos != null) dos.close();
4945 }
4946
4947 dos = null;
4948 try {
4949 dos = new BufferedWriter(new FileWriter(dumpPath+"fielddomains.pa"));
4950 dos.write("V "+(1L<<V_BITS)+" var.map\n");
4951 dos.write("H "+(1L<<H_BITS)+" heap.map\n");
4952 dos.write("T "+(1L<<T_BITS)+" type.map\n");
4953 dos.write("F "+(1L<<F_BITS)+" field.map\n");
4954 dos.write("I "+(1L<<I_BITS)+" invoke.map\n");
4955 dos.write("Z "+(1L<<Z_BITS)+"\n");
4956 dos.write("N "+(1L<<N_BITS)+" name.map\n");
4957 dos.write("M "+(1L<<M_BITS)+" method.map\n");
4958 dos.write("VC "+(1L<<VC_BITS)+"\n");
4959 dos.write("HC "+(1L<<HC_BITS)+"\n");
4960 if (bddIRBuilder != null) bddIRBuilder.dumpFieldDomains(dos);
4961 } finally {
4962 if (dos != null) dos.close();
4963 }
4964
4965 BDD mC = bdd.zero();
4966 for (Iterator i = visited.iterator(Mset); i.hasNext(); ) {
4967 BDD m = (BDD) i.next();
4968 int m_i = m.scanVar(M).intValue();
4969 jq_Method method = (jq_Method) Mmap.get(m_i);
4970 BDD c = getV1V2Context(method);
4971 if (c != null) {
4972 BDD d = c.exist(V2cset); c.free();
4973 m.andWith(d);
4974 }
4975 mC.orWith(m);
4976 }
4977
4978 bdd_save(dumpPath+"vP0.bdd", vP0);
4979 bdd_save(dumpPath+"hP0.bdd", hP);
4980 bdd_save(dumpPath+"L.bdd", L0);
4981 bdd_save(dumpPath+"S.bdd", S0);
4982 if (CONTEXT_SENSITIVE) {
4983 bdd_save(dumpPath+"cA.bdd", A, Arrays.asList(new BDDDomain[] { V1, V2, V1c[0], V2c[0] }));
4984 } else {
4985 bdd_save(dumpPath+"A.bdd", A);
4986 }
4987 bdd_save(dumpPath+"vT.bdd", vT);
4988 bdd_save(dumpPath+"hT.bdd", hT);
4989 bdd_save(dumpPath+"aT.bdd", aT);
4990 bdd_save(dumpPath+"cha.bdd", cha);
4991 bdd_save(dumpPath+"actual.bdd", actual);
4992 bdd_save(dumpPath+"formal.bdd", formal);
4993 bdd_save(dumpPath+"mV.bdd", mV);
4994 bdd_save(dumpPath+"mC.bdd", mC);
4995 bdd_save(dumpPath+"mI.bdd", mI);
4996 bdd_save(dumpPath+"Mret.bdd", Mret);
4997 bdd_save(dumpPath+"Mthr.bdd", Mthr);
4998 bdd_save(dumpPath+"Iret.bdd", Iret);
4999 bdd_save(dumpPath+"Ithr.bdd", Ithr);
5000 bdd_save(dumpPath+"IE0.bdd", IE0);
5001 bdd_save(dumpPath+"sync.bdd", sync);
5002 bdd_save(dumpPath+"mSync.bdd", mSync);
5003 if (threadRuns != null)
5004 bdd_save(dumpPath+"threadRuns.bdd", threadRuns);
5005 if (IEfilter != null)
5006 bdd_save(dumpPath+"IEfilter.bdd", IEfilter);
5007 bdd_save(dumpPath+"roots.bdd", getRoots());
5008
5009 if (V1c.length > 0 && H1c.length > 0) {
5010 bdd_save(dumpPath+"eq.bdd", V1c[0].buildEquals(H1c[0]));
5011 }
5012
5013 if (DUMP_FLY) {
5014 initFly();
5015 bdd_save(dumpPath+"visited.bdd", visitedFly);
5016 bdd_save(dumpPath+"mS.bdd", mS);
5017 bdd_save(dumpPath+"mL.bdd", mL);
5018 bdd_save(dumpPath+"mvP.bdd", mvP);
5019 bdd_save(dumpPath+"mIE.bdd", mIE);
5020 }
5021
5022 dos = null;
5023 try {
5024 dos = new BufferedWriter(new FileWriter(dumpPath+"var.map"));
5025 for (int j = 0; j < Vmap.size(); ++j) {
5026 Node o = (Node)Vmap.get(j);
5027 dos.write(o.id+": "+o+"\n");
5028 }
5029 } finally {
5030 if (dos != null) dos.close();
5031 }
5032
5033 dos = null;
5034 try {
5035 dos = new BufferedWriter(new FileWriter(dumpPath+"heap.map"));
5036
5037 for (int j = 0; j < Hmap.size(); ++j) {
5038 Node o = (Node) Hmap.get(j);
5039 dos.write(o.id+": "+o+"\n");
5040 }
5041 } finally {
5042 if (dos != null) dos.close();
5043 }
5044
5045 dos = null;
5046 try {
5047 dos = new BufferedWriter(new FileWriter(dumpPath+"type.map"));
5048 for (int j = 0; j < Tmap.size(); ++j) {
5049 jq_Type o = (jq_Type) Tmap.get(j);
5050 dos.write(NameMunger.mungeTypeName2(o)+"\n");
5051 }
5052 } finally {
5053 if (dos != null) dos.close();
5054 }
5055
5056 dos = null;
5057 try {
5058 dos = new BufferedWriter(new FileWriter(dumpPath+"field.map"));
5059 for (int j = 0; j < Fmap.size(); ++j) {
5060 jq_Field o = (jq_Field) Fmap.get(j);
5061 dos.write(NameMunger.mungeFieldName(o)+"\n");
5062 }
5063 } finally {
5064 if (dos != null) dos.close();
5065 }
5066
5067 dos = null;
5068 try {
5069 dos = new BufferedWriter(new FileWriter(dumpPath+"invoke.map"));
5070
5071 for (int j = 0; j < Imap.size(); ++j) {
5072 ProgramLocation o = (ProgramLocation)Imap.get(j);
5073 dos.write(o.hashCode()+": "+o+"\n");
5074 }
5075 } finally {
5076 if (dos != null) dos.close();
5077 }
5078
5079 dos = null;
5080 try {
5081 dos = new BufferedWriter(new FileWriter(dumpPath+"name.map"));
5082 for (int j = 0; j < Nmap.size(); ++j) {
5083 jq_Method o = (jq_Method) Nmap.get(j);
5084 dos.write(NameMunger.mungeMethodName(o)+"\n");
5085 }
5086 } finally {
5087 if (dos != null) dos.close();
5088 }
5089
5090 dos = null;
5091 try {
5092 dos = new BufferedWriter(new FileWriter(dumpPath+"method.map"));
5093 for (int j = 0; j < Mmap.size(); ++j) {
5094 Object o = Mmap.get(j);
5095 if (o instanceof Dummy) {
5096 dos.write(o.toString()+"\n");
5097 continue;
5098 }
5099 jq_Method m = (jq_Method) o;
5100 dos.write(NameMunger.mungeMethodName(m)+"\n");
5101 }
5102 } finally {
5103 if (dos != null) dos.close();
5104 }
5105
5106 if(DUMP_UNMUNGED_NAMES) {
5107 dos = null;
5108 try {
5109 dos = new BufferedWriter(new FileWriter(dumpPath+"unmunged_method.map"));
5110 for (int j = 0; j < Mmap.size(); ++j) {
5111 Object o = Mmap.get(j);
5112 if (o instanceof Dummy) {
5113 dos.write(o.toString()+"\n");
5114 continue;
5115 }
5116 jq_Method m = (jq_Method) o;
5117 dos.write(NameMunger.getJavadocSignature(m) + "\n");
5118 }
5119 } finally {
5120 if (dos != null) dos.close();
5121 }
5122 dos = null;
5123 try {
5124 dos = new BufferedWriter(new FileWriter(dumpPath+"unmunged_name.map"));
5125 for (int j = 0; j < Nmap.size(); ++j) {
5126 Object o = Nmap.get(j);
5127 if (o instanceof Dummy) {
5128 dos.write(o.toString()+"\n");
5129 continue;
5130 }
5131 jq_Method m = (jq_Method) o;
5132 dos.write(NameMunger.getJavadocSignature(m) + "\n");
5133 }
5134 } finally {
5135 if (dos != null) dos.close();
5136 }
5137 }
5138
5139 }
5140
5141 class Dummy implements Textualizable {
5142 public void addEdge(String edge, Textualizable t) {
5143 }
5144 public void write(Textualizer t) throws IOException {
5145 t.writeString("(dummy object)");
5146 }
5147 public void writeEdges(Textualizer t) throws IOException {
5148 }
5149 public String toString() {
5150 return "DummyMethod";
5151 }
5152 }
5153
5154 private void makeVRegbdd(CallGraph callgraph) {
5155 vReg = bdd.zero();
5156 BDDDomain reg = bddIRBuilder.getDestDomain();
5157 Collection s = new TreeSet(new Comparator() {
5158 public int compare(Object o1, Object o2) {
5159 return o1.toString().compareTo(o2.toString());
5160 }
5161 });
5162 s.addAll(callgraph.getAllMethods());
5163 for (Iterator i = s.iterator(); i.hasNext();) {
5164 BDD b = bdd.zero();
5165 jq_Method m = (jq_Method) i.next();
5166 if (m.getBytecode() == null)
5167 continue;
5168 ControlFlowGraph cfg = joeq.Compiler.Quad.CodeCache.getCode(m);
5169
5170
5171
5172 PrimitiveMethodSummary ms = PrimitiveMethodSummary.getSummary(m);
5173
5174 for (Iterator j = cfg.getRegisterFactory().iterator(); j.hasNext();) {
5175 Register r = (Register) j.next();
5176 if (r == null) {
5177
5178 continue;
5179 }
5180
5181 Collection nodes = ms.getRegisterAtLocation(cfg.exit(), null, r);
5182 if (nodes == null)
5183 continue;
5184 for (Iterator ni = nodes.iterator(); ni.hasNext();) {
5185 Node n = (Node) ni.next();
5186 b.orWith(reg.ithVar(bddIRBuilder.getRegisterID(r)).and(
5187 V1.ithVar(Vmap.get(n))));
5188 }
5189 }
5190 b.andWith(M.ithVar(Mmap.get(m)));
5191 vReg.orWith(b);
5192 }
5193 }
5194 private void makeIQuadbdd() {
5195 iQuad = bdd.zero();
5196 BDDDomain quad = bddIRBuilder.getQuadDomain();
5197 ProgramLocation pl;
5198 BDD b;
5199 for (int i = 0; i < Imap.size(); ++i) {
5200 pl = (ProgramLocation) Imap.get(i);
5201 ProgramLocation.BCProgramLocation bcpl = (ProgramLocation.BCProgramLocation) LoadedCallGraph
5202 .mapCall(pl);
5203 int quadID = bddIRBuilder.quadIdFromInvokeBCLocation(bcpl);
5204 b = I.ithVar(i);
5205 b.andWith(quad.ithVar(quadID));
5206 iQuad.orWith(b);
5207 }
5208 }
5209
5210 private void makeHQuadbdd() {
5211 Assert.UNREACHABLE();
5212
5213
5214 hQuad = bdd.zero();
5215 BDDDomain quad = bddIRBuilder.getQuadDomain();
5216 BDD b;
5217 for (int i = 0; i < Hmap.size(); ++i) {
5218 ProgramLocation pl = (ProgramLocation) Imap.get(i);
5219 ProgramLocation.BCProgramLocation bcpl = (ProgramLocation.BCProgramLocation) LoadedCallGraph
5220 .mapCall(pl);
5221 int quadID = bddIRBuilder.quadIdFromAllocBCLocation(bcpl);
5222 b = I.ithVar(i);
5223 b.andWith(quad.ithVar(quadID));
5224 iQuad.orWith(b);
5225 }
5226 }
5227
5228 private void makeFMemberbdd() {
5229 fMember = bdd.zero();
5230 BDDDomain member = bddIRBuilder.getMemberDomain();
5231 BDD b;
5232 for (int i = 0; i < Fmap.size(); ++i) {
5233 Object o = Fmap.get(i);
5234 if (o instanceof jq_Field) {
5235 int memberID = bddIRBuilder.memberIdFromField((jq_Field)o);
5236 if (memberID == 0) continue;
5237 b = F.ithVar(i).and(member.ithVar(memberID));
5238 fMember.orWith(b);
5239 }
5240 }
5241 }
5242
5243 private void dumpSSA() throws IOException {
5244 Assert._assert(DUMP_SSA);
5245 String dumpPath = System.getProperty("pa.dumppath", "");
5246 jq_MethodVisitor mv = null;
5247 ControlFlowGraphVisitor cfgv = null;
5248 Assert._assert(bddIRBuilder != null);
5249 mv = new ControlFlowGraphVisitor.CodeCacheVisitor(bddIRBuilder,
5250 true);
5251
5252 Collection s = new TreeSet(new Comparator() {
5253 public int compare(Object o1, Object o2) {
5254 return o1.toString().compareTo(o2.toString());
5255 }
5256 });
5257 CallGraph callgraph = new CachedCallGraph(new PrimitivePACallGraph(this));
5258 if (callgraph.getAllMethods() == null) {
5259 System.out.println("call graph has no methods!");
5260 }
5261 s.addAll(callgraph.getAllMethods());
5262 for (Iterator i = s.iterator(); i.hasNext();) {
5263 jq_Method m = (jq_Method) i.next();
5264 try {
5265 m.accept(mv);
5266 } catch (LinkageError le) {
5267 System.err
5268 .println("Linkage error occurred while executing pass on "
5269 + m + " : " + le);
5270 le.printStackTrace(System.err);
5271 } catch (Exception x) {
5272 System.err
5273 .println("Runtime exception occurred while executing pass on "
5274 + m + " : " + x);
5275 x.printStackTrace(System.err);
5276 }
5277 }
5278 System.err.println("Completed pass! " + bddIRBuilder);
5279 makeVRegbdd(callgraph);
5280 makeIQuadbdd();
5281 makeFMemberbdd();
5282
5283 BDDDomain reg = bddIRBuilder.getDestDomain();
5284 BDDDomain quad = bddIRBuilder.getQuadDomain();
5285 BDDDomain member = bddIRBuilder.getMemberDomain();
5286 System.out.println("vReg: "
5287 + (long) vReg.satCount(V1.set().union(reg.set().union(M.set())))
5288 + " relations, " + vReg.nodeCount() + " nodes");
5289 bdd_save(dumpPath + "/vReg.bdd", vReg);
5290 System.out.println("iQuad: "
5291 + (long) iQuad.satCount(I.set().union(quad.set()))
5292 + " relations, " + iQuad.nodeCount() + " nodes");
5293 bdd_save(dumpPath + "/iQuad.bdd", iQuad);
5294 System.out.println("fMember: "
5295 + (long) fMember.satCount(F.set().union(member.set()))
5296 + " relations, " + fMember.nodeCount() + " nodes");
5297 bdd_save(dumpPath + "/fMember.bdd", fMember);
5298
5299
5300 }
5301 }