View Javadoc

1   // Copyright (C) 2004 John Whaley <jwhaley@alum.mit.edu>
2   // Licensed under the terms of the GNU LGPL; see COPYING for details.
3   package joeq.Compiler.Analysis.BDD;
4   
5   import java.util.HashMap;
6   import java.util.Iterator;
7   import java.util.LinkedList;
8   import java.util.List;
9   import java.util.Map;
10  import java.io.BufferedReader;
11  import java.io.BufferedWriter;
12  import java.io.FileReader;
13  import java.io.FileWriter;
14  import java.io.IOException;
15  import java.math.BigInteger;
16  import joeq.Class.jq_Field;
17  import joeq.Class.jq_Method;
18  import joeq.Compiler.Analysis.IPA.ProgramLocation;
19  import joeq.Compiler.Quad.CodeCache;
20  import joeq.Compiler.Quad.ControlFlowGraph;
21  import joeq.Compiler.Quad.ControlFlowGraphVisitor;
22  import joeq.Compiler.Quad.Operand;
23  import joeq.Compiler.Quad.Operator;
24  import joeq.Compiler.Quad.Quad;
25  import joeq.Compiler.Quad.QuadIterator;
26  import joeq.Compiler.Quad.Operand.ConstOperand;
27  import joeq.Compiler.Quad.Operand.FieldOperand;
28  import joeq.Compiler.Quad.Operand.MethodOperand;
29  import joeq.Compiler.Quad.Operand.RegisterOperand;
30  import joeq.Compiler.Quad.Operand.TargetOperand;
31  import joeq.Compiler.Quad.Operand.TypeOperand;
32  import joeq.Compiler.Quad.Operator.Invoke;
33  import joeq.Compiler.Quad.Operator.New;
34  import joeq.Compiler.Quad.Operator.NewArray;
35  import joeq.Compiler.Quad.RegisterFactory.Register;
36  import joeq.Compiler.Quad.SSA.EnterSSA;
37  import jwutil.collections.IndexMap;
38  import jwutil.util.Assert;
39  import net.sf.javabdd.BDD;
40  import net.sf.javabdd.BDDDomain;
41  import net.sf.javabdd.BDDFactory;
42  import net.sf.javabdd.BDDVarSet;
43  
44  /***
45   * BuildBDDIR
46   * 
47   * @author jwhaley
48   * @version $Id: BuildBDDIR.java 2475 2006-12-24 09:44:50Z joewhaley $
49   */
50  public class BuildBDDIR implements ControlFlowGraphVisitor {
51      
52      IndexMap methodMap;
53      IndexMap opMap;
54      IndexMap quadMap;
55      IndexMap quadLineMap;
56      //IndexMap regMap;
57      IndexMap memberMap;
58      IndexMap constantMap;
59      
60      Map/*ProgramLocation,Quad*/ invokeMap;
61      Map/*ProgramLocation,Quad*/ allocMap;
62      
63      String dumpDir = System.getProperty("bdddumpdir", "");
64      boolean DUMP_TUPLES = !System.getProperty("dumptuples", "no").equals("no");
65  
66      String varOrderDesc = "method_quadxtargetxfallthrough_member_constant_opc_srcs_dest_srcNum";
67      
68      int methodBits = 14, quadBits = 19, opBits = 9, regBits = 7, constantBits = 14, memberBits = 15, varargsBits = 4;
69  
70      BDDFactory bdd;
71      BDDDomain method, quad, opc, dest, src1, src2, constant, fallthrough, target, member, srcNum, srcs;
72      BDD methodToQuad;
73      BDD methodEntries;
74      BDD nullConstant;
75      BDD nonNullConstants;
76      BDD allQuads;
77      BDD currentQuad;
78      
79      Object theDummyObject;
80      
81      int totalQuads;
82      
83      boolean ZERO_FIELDS = !System.getProperty("zerofields", "yes").equals("no");
84      boolean GLOBAL_QUAD_NUMBERS = !System.getProperty("globalquadnumber", "yes").equals("no");
85      boolean SSA = !System.getProperty("ssa", "no").equals("no");
86      boolean USE_SRC12 = !System.getProperty("src12", "no").equals("no");
87      
88      boolean ENTER_SSA;
89      
90      public BuildBDDIR()
91      {
92          bdd = BDDFactory.init(1000000, 50000);
93          theDummyObject = new Object();
94          methodMap = new IndexMap("method");
95          methodMap.get(theDummyObject);
96          method = makeDomain("method", methodBits);
97          initialize();
98          System.out.println("Using variable ordering "+varOrderDesc);
99          int [] varOrder = bdd.makeVarOrdering(true, varOrderDesc);
100         bdd.setVarOrder(varOrder);
101         //bdd.setMaxIncrease(500000);
102         bdd.setIncreaseFactor(2);
103         ENTER_SSA = true;
104     }
105     
106     public BuildBDDIR(BDDFactory bddFactory, BDDDomain methodDomain, IndexMap _methodMap, Object dummy)
107     {
108         bdd = bddFactory;
109         method = methodDomain;
110         methodMap = _methodMap;
111         theDummyObject = dummy;
112         initialize();
113         int index = varOrderDesc.indexOf("method_");
114         varOrderDesc = varOrderDesc.substring(0, index) + varOrderDesc.substring(index + "method_".length());
115         ENTER_SSA = false;
116     }
117     
118     protected void initialize()
119     {
120         if (!GLOBAL_QUAD_NUMBERS) {
121             quadBits = 13;
122         }
123         if (SSA) {
124             regBits = 11;
125             varargsBits = 7;
126             int index = varOrderDesc.indexOf("xtargetxfallthrough");
127             varOrderDesc = varOrderDesc.substring(0, index) + varOrderDesc.substring(index + "xtargetxfallthrough".length());
128             
129             varOrderDesc = "method_memberxquad_constant_opc_srcs_dest_srcNum";
130         }
131         if (USE_SRC12) {
132             int index = varOrderDesc.indexOf("_srcs");
133             varOrderDesc = varOrderDesc.substring(0, index) + "_src2_src1" + varOrderDesc.substring(index);
134         }
135         loadOpMap();
136         quadMap = new IndexMap("quad");
137         quadLineMap = new IndexMap("quadloc");
138         quadMap.get(theDummyObject);
139         quadLineMap.get(theDummyObject);
140         //regMap = new IndexMap("reg");
141         memberMap = new IndexMap("member");
142         memberMap.get(theDummyObject);
143         constantMap = new IndexMap("constant");
144         constantMap.get(theDummyObject);
145         opc = makeDomain("opc", opBits);
146         quad = makeDomain("quad", quadBits);
147         dest = makeDomain("dest", regBits);
148         if (USE_SRC12) {
149             src1 = makeDomain("src1", regBits);
150             src2 = makeDomain("src2", regBits);
151         }
152         constant = makeDomain("constant", constantBits);
153         if (!SSA) {
154             fallthrough = makeDomain("fallthrough", quadBits);
155             target = makeDomain("target", quadBits);
156         }
157         member = makeDomain("member", memberBits);
158         srcNum = makeDomain("srcNum", varargsBits);
159         srcs = makeDomain("srcs", regBits);
160         allQuads = bdd.zero();
161         methodToQuad = bdd.zero();
162         methodEntries = bdd.zero();
163         nullConstant = bdd.zero();
164         nonNullConstants = bdd.zero();
165         invokeMap = new HashMap();
166         allocMap = new HashMap();
167     }
168     
169     BDDDomain makeDomain(String name, int bits) {
170         Assert._assert(bits < 64);
171         BDDDomain d = bdd.extDomain(new long[] { 1L << bits })[0];
172         d.setName(name);
173         return d;
174     }
175     
176     void loadOpMap() {
177         String fileName = "op.map";
178         try {
179             BufferedReader in = new BufferedReader(new FileReader(fileName));
180             opMap = IndexMap.loadStringMap("op", in);
181             in.close();
182         } catch (IOException x) {
183             System.out.println("Cannot load op map "+fileName);
184             opMap = new IndexMap("op");
185             opMap.get(new Object());
186         }
187     }
188     
189     /* (non-Javadoc)
190      * @see joeq.Compiler.Quad.ControlFlowGraphVisitor#visitCFG(joeq.Compiler.Quad.ControlFlowGraph)
191      */
192     public void visitCFG(ControlFlowGraph cfg) {
193         if (SSA && ENTER_SSA) {
194             new EnterSSA().visitCFG(cfg);
195         }
196         QuadIterator i = new QuadIterator(cfg);
197         jq_Method m = cfg.getMethod();
198         int methodID = getMethodID(m);
199         
200         if (!GLOBAL_QUAD_NUMBERS) quadMap.clear();
201         
202         long time = System.currentTimeMillis();
203         
204         boolean firstQuad = true;
205         
206         while (i.hasNext()) {
207             Quad q = i.nextQuad();
208             currentQuad = bdd.one();
209             int quadID = getQuadID(q);
210             addQuadLoc(m, q);
211             //System.out.println("Quad id: "+quadID);
212             
213             // first quad visited is the entry point
214             if (firstQuad) {
215                 methodEntries.orWith(method.ithVar(methodID).and(quad.ithVar(quadID)));
216                 firstQuad = false;
217             }
218             
219             currentQuad.andWith(quad.ithVar(quadID));
220             if (!GLOBAL_QUAD_NUMBERS) {
221                 currentQuad.andWith(method.ithVar(methodID));
222                 methodToQuad.orWith(currentQuad.id());
223             } else {
224                 methodToQuad.orWith(currentQuad.and(method.ithVar(methodID)));
225             }
226             int opID = getOpID(q.getOperator());
227             currentQuad.andWith(opc.ithVar(opID));
228             handleQuad(q, m);
229             if (!SSA) {
230                 BDD succ = bdd.zero();
231                 Iterator j = i.successors();
232                 if (!j.hasNext()) {
233                     succ.orWith(fallthrough.ithVar(0));
234                 } else do {
235                     Quad q2 = (Quad) j.next();
236                     int quad2ID = getQuadID(q2);
237                     succ.orWith(fallthrough.ithVar(quad2ID));
238                 } while (j.hasNext());
239                 currentQuad.andWith(succ);
240             }
241             //printQuad(currentQuad);
242             allQuads.orWith(currentQuad);
243         }
244         
245         time = System.currentTimeMillis() - time;
246         totalTime += time;
247         System.out.println("Method: " + cfg.getMethod() + " time: " + time);
248         //int qSize = totalQuads;
249         //int nodes = allQuads.nodeCount();
250         //System.out.println("Quads: " +qSize+", nodes: "+nodes+", average:
251         // "+(float)nodes/qSize);
252     }
253     
254     long totalTime;
255     
256     public String toString() {
257         buildNullConstantBdds();
258         
259         System.out.println("Total time spent building representation: "+totalTime);
260         System.out.println("allQuads, node count: " + allQuads.nodeCount());
261         System.out.println("methodToQuad, node count: " + methodToQuad.nodeCount());
262         
263         System.out.println("methodMap size: " + methodMap.size());
264         System.out.println("opMap size: " + opMap.size());
265         System.out.println("quadMap size: " + quadMap.size());
266         System.out.println("quadLineMap size: " + quadLineMap.size());
267         //System.out.println("regMap size: " + regMap.size());
268         System.out.println("memberMap size: " + memberMap.size());
269         System.out.println("constantMap size: " + constantMap.size());
270         
271         try {
272             //print();
273             dump();
274         } catch (IOException x) {
275         }
276         return ("BuildBDDIR, node count: " + allQuads.nodeCount());
277     }
278     
279     public int getMethodID(jq_Method m) {
280         int x = methodMap.get(m);
281         Assert._assert(x > 0);
282         return x;
283     }
284     
285     public int getRegisterID(Register r) {
286         int x = r.getNumber() + 1;
287         return x;
288     }
289     
290     public int getConstantID(Object c) {
291         int x = constantMap.get(c);
292         Assert._assert(x > 0);
293         return x;
294     }
295     
296     public int getQuadID(Quad r) {
297         int x = quadMap.get(r);
298         Assert._assert(x > 0);
299         return x;
300     }
301     
302     public void addQuadLoc(jq_Method m, Quad q) {        
303         Map map = CodeCache.getBCMap(m);            
304         Integer j = (Integer) map.get(q);
305         if (j == null) {
306             //Assert.UNREACHABLE("Error: no mapping for quad "+q);
307             // some, like PHI nodes may not have a mapping
308             return;
309         }
310         int bcIndex = j.intValue();
311         ProgramLocation quadLoc = new ProgramLocation.BCProgramLocation(m, bcIndex);
312         quadLineMap.get(q + " @ " + quadLoc.toStringLong());
313     }
314     
315     public int getMemberID(Object r) {
316         int x = memberMap.get(r);
317         Assert._assert(x > 0);
318         return x;
319     }
320     
321     public int getOpID(Operator r) {
322         int x = opMap.get(r.toString());
323         Assert._assert(x > 0);
324         return x;
325     }
326     
327     void handleQuad(Quad q, jq_Method m) {
328         //System.out.println("handling quad: "+q);
329         int quadID=0, opcID=0, destID=0, src1ID=0, src2ID=0, constantID=0, targetID=0, memberID=0;
330         List srcsID = null;
331         quadID = getQuadID(q);
332         opcID = getOpID(q.getOperator());
333         Iterator i = q.getDefinedRegisters().iterator();
334         if (i.hasNext()) {
335             RegisterOperand ro = (RegisterOperand) i.next();
336             //System.out.println("destination register is "+ro.getRegister());
337             destID = getRegisterID(ro.getRegister());
338             //System.out.println("destination register id "+destID);
339             Assert._assert(!i.hasNext());
340         }
341         i = q.getUsedRegisters().iterator();
342         if (USE_SRC12 && i.hasNext()) {
343             RegisterOperand rop;
344             rop = (RegisterOperand) i.next();
345             if (rop != null) src1ID = getRegisterID(rop.getRegister());
346             if (i.hasNext()) {
347                 rop = (RegisterOperand) i.next();
348                 if (rop != null) src2ID = getRegisterID(rop.getRegister());
349             }
350         }
351         if (i.hasNext()) {
352             srcsID = new LinkedList();
353             do {
354                 RegisterOperand rop = (RegisterOperand) i.next();
355                 //System.out.println("source register is "+rop.getRegister());                
356                 if (rop != null) srcsID.add(new Integer(getRegisterID(rop.getRegister())));
357                 //System.out.println("source register id "+getRegisterID(rop.getRegister()));
358             } while (i.hasNext());
359         }
360         i = q.getAllOperands().iterator();
361         while (i.hasNext()) {
362             Operand op = (Operand) i.next();
363             if (op instanceof RegisterOperand) continue;
364             else if (op instanceof ConstOperand) {
365                 constantID = getConstantID(((ConstOperand) op).getWrapped());
366             } else if (op instanceof TargetOperand) {
367                 if (!SSA)
368                     targetID = getQuadID(((TargetOperand) op).getTarget().getQuad(0));
369             } else if (op instanceof FieldOperand) {
370                 memberID = getMemberID(((FieldOperand) op).getField());
371             } else if (op instanceof MethodOperand) {
372                 memberID = getMemberID(((MethodOperand) op).getMethod());
373             } else if (op instanceof TypeOperand) {
374                 memberID = getMemberID(((TypeOperand) op).getType());
375             }
376         }
377         //System.out.println("quadID "+quadID+" destID "+destID);
378         if (ZERO_FIELDS || quadID != 0) currentQuad.andWith(quad.ithVar(quadID));
379         if (ZERO_FIELDS || opcID != 0) currentQuad.andWith(opc.ithVar(opcID));
380         if (ZERO_FIELDS || destID != 0) currentQuad.andWith(dest.ithVar(destID));
381         if (USE_SRC12) {
382             if (ZERO_FIELDS || src1ID != 0) currentQuad.andWith(src1.ithVar(src1ID));
383             if (ZERO_FIELDS || src2ID != 0) currentQuad.andWith(src2.ithVar(src2ID));
384         }
385         if (ZERO_FIELDS || constantID != 0) currentQuad.andWith(constant.ithVar(((long)constantID) & 0xFFFFFFFFL));
386         if (!SSA) {
387             if (ZERO_FIELDS || targetID != 0) currentQuad.andWith(target.ithVar(targetID));
388         }
389         if (ZERO_FIELDS || memberID != 0) currentQuad.andWith(member.ithVar(memberID));
390         if (srcsID != null && !srcsID.isEmpty()) {
391             BDD temp = bdd.zero();
392             int j = 1;
393             for (i = srcsID.iterator(); i.hasNext(); ++j) {
394                 int srcID = ((Integer) i.next()).intValue();
395                 //System.out.println("source "+j+" srcID "+srcID);
396                 if (ZERO_FIELDS || srcID != 0) {
397                     BDD temp2 = srcNum.ithVar(j);
398                     temp2.andWith(srcs.ithVar(srcID));
399                     temp.orWith(temp2);
400                 }
401             }
402             if (!temp.isZero())
403                 currentQuad.andWith(temp);
404             else
405                 temp.free();
406         } else if (ZERO_FIELDS) {
407             BDD temp2 = srcNum.ithVar(0);
408             temp2.andWith(srcs.ithVar(0));
409             currentQuad.andWith(temp2);
410         }
411         
412         Operator quadOp = q.getOperator();
413         if (quadOp instanceof Invoke ||
414             quadOp instanceof New ||
415             quadOp instanceof NewArray) {
416             ProgramLocation quadLoc;
417             Map map = CodeCache.getBCMap(m);            
418             Integer j = (Integer) map.get(q);
419             if (j == null) {
420                 Assert.UNREACHABLE("Error: no mapping for quad "+q);
421             }
422             int bcIndex = j.intValue();
423             quadLoc = new ProgramLocation.BCProgramLocation(m, bcIndex);
424 
425             if (quadOp instanceof Invoke) {
426                 invokeMap.put(quadLoc, q);
427             }
428             else {
429                 allocMap.put(quadLoc, q);
430             }
431         }
432         ++totalQuads;
433     }
434     
435     public void dump() throws IOException {
436         System.out.println("Var order: "+varOrderDesc);
437         dumpMap(quadMap, dumpDir+"quad.map");
438         dumpMap(quadLineMap, dumpDir+"quadloc.map");
439         dumpMap(opMap, dumpDir+"op.map");
440         //dumpMap(regMap, dumpDir+"reg.map");
441         dumpMap(memberMap, dumpDir+"member.map");
442         dumpMap(constantMap, dumpDir+"constant.map");
443         
444         String relationName;
445         if (SSA) {
446             relationName = "ssa";
447         }
448         else {
449             relationName = "cfg";
450         }
451         
452         dumpBDDConfig(dumpDir+"bdd."+relationName);
453         dumpFieldDomains(dumpDir+"fielddomains."+relationName);
454         dumpRelations(dumpDir+"relations."+relationName);            
455         
456         System.out.print("Saving BDDs...");
457         bdd.save(dumpDir+relationName+".bdd", allQuads);
458         bdd.save(dumpDir+"m2q.bdd", methodToQuad);
459         bdd.save(dumpDir+"entries.bdd", methodEntries);
460         bdd.save(dumpDir+"nullconstant.bdd", nullConstant);
461         bdd.save(dumpDir+"nonnullconstants.bdd", nonNullConstants);
462         System.out.println("done.");
463         
464         if (DUMP_TUPLES) {
465             System.out.println("Saving tuples....");
466             dumpTuples(bdd, dumpDir+relationName+".tuples", allQuads);
467             dumpTuples(bdd, dumpDir+"m2q.tuples", methodToQuad);
468             dumpTuples(bdd, dumpDir+"entries.tuples", methodEntries);
469             dumpTuples(bdd, dumpDir+"nullconstant.tuples", nullConstant);
470             dumpTuples(bdd, dumpDir+"nonnullconstants.tuples", nonNullConstants);
471             System.out.println("done.");
472         }
473     }
474     
475     void dumpBDDConfig(String fileName) throws IOException {
476         BufferedWriter dos = null;
477         try {
478             dos = new BufferedWriter(new FileWriter(fileName));
479             for (int i = 0; i < bdd.numberOfDomains(); ++i) {
480                 BDDDomain d = bdd.getDomain(i);
481                 dos.write(d.getName()+" "+d.size()+"\n");
482             }
483         } finally {
484             if (dos != null) dos.close();
485         }
486     }
487     
488     public void dumpFieldDomains(BufferedWriter dos) throws IOException {
489         dos.write("method "+(1L<<methodBits)+"\n");
490         dos.write("quad "+(1L<<quadBits)+"\n");
491         dos.write("op "+(1L<<opBits)+" op.map\n");
492         dos.write("reg "+(1L<<regBits)+"\n");
493         dos.write("constant "+(1L<<constantBits)+" constant.map\n");
494         dos.write("member "+(1L<<memberBits)+"\n");
495         dos.write("varargs "+(1L<<varargsBits)+"\n");
496     }
497     
498     public void dumpFieldDomains(String fileName) throws IOException {
499         BufferedWriter dos = null;
500         try {
501             dos = new BufferedWriter(new FileWriter(fileName));
502             dumpFieldDomains(dos);
503         } finally {
504             if (dos != null) dos.close();
505         }
506     }
507     
508     void dumpRelation(BufferedWriter dos, String name, BDD relation) throws IOException {
509         BDDDomain[] a = relation.support().getDomains();
510         dos.write(name+" ( ");
511         for (int i = 0; i < a.length; ++i) {
512             if (i > 0) dos.write(", ");
513             BDDDomain d = a[i];
514             dos.write(d.toString()+" : ");
515             if (d == quad || d == fallthrough || d == target) dos.write("quad ");
516             else if (d == method) dos.write("method ");
517             else if (d == opc) dos.write("op ");
518             else if (d == dest || d == srcs || d == src1 || d == src2) dos.write("reg ");
519             else if (d == constant) dos.write("constant ");
520             else if (d == member) dos.write("member ");
521             else if (d == srcNum) dos.write("varargs ");
522             else dos.write("??? ");
523         }
524         dos.write(")\n");
525     }
526     
527     void dumpRelations(String fileName) throws IOException {
528         BufferedWriter dos = new BufferedWriter(new FileWriter(fileName));
529         dumpRelation(dos, "m2q", methodToQuad);
530         if (SSA) {
531             dumpRelation(dos, "ssa", allQuads);
532         } else {
533             dumpRelation(dos, "cfg", allQuads);
534         }
535         dumpRelation(dos, "entries", methodEntries);
536         dumpRelation(dos, "nullconstant", nullConstant);
537         dumpRelation(dos, "nonnullconstants", nonNullConstants);
538         dos.close();
539     }
540     
541     void dumpMap(IndexMap map, String fileName) throws IOException {
542         BufferedWriter dos = null;
543         try {
544             dos = new BufferedWriter(new FileWriter(fileName));
545             for (int i = 0; i < map.size(); ++i) {
546                 Object o = map.get(i);
547                 String s;
548                 if (o != null) {
549                    s = o.toString();
550                 }
551                 else {
552                    s = "(null)"; 
553                 }
554                 // suppress nonprintables in the output
555                 StringBuffer sb = new StringBuffer(s);
556                 for (int j=0; j<sb.length(); ++j) {
557                     if (sb.charAt(j) < 32) {
558                         sb.setCharAt(j, ' ');
559                     }
560                     else if (sb.charAt(j) > 127) {
561                         sb.setCharAt(j, ' ');
562                     }
563                 }
564                 s = new String(sb);
565                 dos.write(s + "\n");
566             }
567         } finally {
568             if (dos != null) dos.close();
569         }
570     }
571     
572     public static void dumpTuples(BDDFactory bdd, String fileName, BDD relation) throws IOException {
573         BufferedWriter dos = null;
574         try {
575             dos = new BufferedWriter(new FileWriter(fileName));
576             if (relation.isZero()) {
577                 return;
578             }
579             Assert._assert(!relation.isOne());
580             BDDVarSet rsup = relation.support();
581             BDDDomain[] a = rsup.getDomains();
582             rsup.free();
583             BDDVarSet allDomains = bdd.emptySet();
584             BDDDomain primaryDomain = null;
585             BDDVarSet allButPrimary = bdd.emptySet();
586             System.out.print(fileName+" domains {");
587             dos.write("#");
588             for (int i = 0; i < a.length; ++i) {
589                 BDDDomain d = a[i];
590                 System.out.print(" "+d.toString());
591                 dos.write(" "+d.toString()+":"+d.varNum());
592                 allDomains.unionWith(d.set());
593                 if (i == 0)
594                     primaryDomain = d;
595                 else
596                     allButPrimary.unionWith(d.set());
597             }
598             dos.write("\n");
599             System.out.println(" } = "+relation.nodeCount()+" nodes");
600             int lines = 0;
601             BDD foo = relation.exist(allButPrimary);
602             for (Iterator i = foo.iterator(primaryDomain.set()); i.hasNext(); ) {
603                 BDD q = (BDD) i.next();
604                 q.andWith(relation.id());
605                 while (!q.isZero()) {
606                     BDD sat = q.satOne(allDomains, false);
607                     BDDVarSet sup = q.support();
608                     BDDDomain[] b = sup.getDomains();
609                     sup.free();
610                     BigInteger[] v = sat.scanAllVar();
611                     sat.free();
612                     BDD t = bdd.one();
613                     for (int j = 0, k = 0, l = 0; j < bdd.numberOfDomains(); ++j) {
614                         BDDDomain d = bdd.getDomain(j);
615                         if (k >= a.length || a[k].getIndex() != j) {
616                             Assert._assert(v[j].signum() == 0, "v["+j+"] is "+v[j]);
617                             //dos.write("* ");
618                             t.andWith(d.domain());
619                             continue;
620                         } else {
621                             ++k;
622                         }
623                         if (l >= b.length || b[l].getIndex() != j) {
624                             Assert._assert(v[j].signum() == 0, "v["+j+"] is "+v[j]);
625                             dos.write("* ");
626                             t.andWith(d.domain());
627                             continue;
628                         } else {
629                             ++l;
630                         }
631                         dos.write(v[j]+" ");
632                         t.andWith(d.ithVar(v[j]));
633                     }
634                     q.applyWith(t, BDDFactory.diff);
635                     dos.write("\n");
636                     ++lines;
637                 }
638                 q.free();
639             }
640             System.out.println("Done printing "+lines+" lines.");
641         } finally {
642             if (dos != null) dos.close();
643         }
644     }
645     
646     void print() {
647         for (int i = 0; i < quadMap.size(); ++i) {
648             BDD q = quad.ithVar(i).andWith(allQuads.id());
649             printQuad(q);
650         }
651     }
652     
653     void printQuad(BDD q) {
654         BigInteger id = q.scanVar(quad);
655         if (id.signum() < 0) return;
656         System.out.println("Quad id "+id);
657         System.out.println("        "+quadMap.get(id.intValue()));
658         System.out.println(q.toStringWithDomains());
659     }
660     
661     void buildNullConstantBdds() {
662         for (int i = 0; i < constantMap.size(); ++i) {
663             Object c = constantMap.get(i);
664             if (c == null) {
665                 nullConstant.orWith(constant.ithVar(i));
666             }
667             else if (!(c instanceof Integer) &&
668                      !(c instanceof Float) &&
669                      !(c instanceof Long) &&
670                      !(c instanceof Double) &&
671                      c != theDummyObject) {
672                 nonNullConstants.orWith(constant.ithVar(i));                    
673             }
674         }
675     }
676     
677     public String getVarOrderDesc() {
678         return varOrderDesc;
679     }
680     
681     public BDDDomain getDestDomain() {
682         return dest;
683     }
684     
685     public BDDDomain getQuadDomain() {
686         return quad;
687     }
688     
689     public String getDomainName(BDDDomain d) {
690         if (d == quad || d == fallthrough || d == target) return "quad";
691         else if (d == method) return "method";
692         else if (d == opc) return "op";
693         else if (d == dest || d == srcs || d == src1 || d == src2) return "reg";
694         else if (d == constant) return "constant";
695         else if (d == member) return "member";
696         else if (d == srcNum) return "varargs";
697         else return d.getName();
698     }
699     
700     public int quadIdFromInvokeBCLocation(ProgramLocation.BCProgramLocation bc) {
701         Object o = invokeMap.get(bc);
702         if (o == null) {
703             Assert.UNREACHABLE(bc+" has no mapping");
704         }
705         return quadMap.get(o);
706     }
707     
708     public int quadIdFromAllocBCLocation(ProgramLocation.BCProgramLocation bc) {
709         Object o = allocMap.get(bc);
710         Assert._assert(o != null);
711         return quadMap.get(o);
712     }
713     
714     public int memberIdFromField(jq_Field f) {
715         if (memberMap.contains(f)) {
716             return memberMap.get(f);
717         }
718         else {
719             return 0;
720         }
721     }
722 
723      public BDDDomain getMemberDomain() {
724         return member;
725     }
726 }