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