00001
00005 package edu.mit.csail.sdg.squander.engine;
00006
00007 import java.lang.reflect.Field;
00008 import java.util.ArrayList;
00009 import java.util.Collection;
00010 import java.util.Collections;
00011 import java.util.Comparator;
00012 import java.util.HashMap;
00013 import java.util.HashSet;
00014 import java.util.IdentityHashMap;
00015 import java.util.LinkedList;
00016 import java.util.List;
00017 import java.util.Map;
00018 import java.util.Set;
00019 import java.util.Map.Entry;
00020
00021 import kodkod.util.collections.IdentityHashSet;
00022 import edu.mit.csail.sdg.squander.absstate.ObjTuple;
00023 import edu.mit.csail.sdg.squander.absstate.ObjTupleSet;
00024 import edu.mit.csail.sdg.squander.annotations.Options;
00025 import edu.mit.csail.sdg.squander.engine.Heap2Bounds.Pair;
00026 import edu.mit.csail.sdg.squander.engine.ISquanderResult.IEvaluator;
00027 import edu.mit.csail.sdg.squander.log.Log;
00028 import edu.mit.csail.sdg.squander.serializer.AbstractHeapListener;
00029 import edu.mit.csail.sdg.squander.serializer.special.ObjSerFactory;
00030 import edu.mit.csail.sdg.squander.spec.ForgeScene;
00031 import edu.mit.csail.sdg.squander.spec.JField;
00032 import edu.mit.csail.sdg.squander.spec.JMethod;
00033 import edu.mit.csail.sdg.squander.spec.JType;
00034 import edu.mit.csail.sdg.squander.spec.JavaScene;
00035 import edu.mit.csail.sdg.squander.spec.MethodSpec;
00036 import edu.mit.csail.sdg.squander.spec.Spec;
00037 import edu.mit.csail.sdg.squander.spec.JType.Unary;
00038 import edu.mit.csail.sdg.squander.spec.MethodSpec.CaseSource;
00039 import edu.mit.csail.sdg.squander.spec.constant.ConstRel;
00040 import edu.mit.csail.sdg.squander.spec.constant.ConstRel2Bound;
00041 import edu.mit.csail.sdg.squander.spec.constant.ConstRels;
00042 import edu.mit.csail.sdg.squander.utils.Utils;
00043 import forge.program.BooleanDomain;
00044 import forge.program.BooleanLiteral;
00045 import forge.program.ForgeDomain;
00046 import forge.program.ForgeLiteral;
00047 import forge.program.ForgeProcedure;
00048 import forge.program.ForgeProgram;
00049 import forge.program.ForgeType;
00050 import forge.program.ForgeVariable;
00051 import forge.program.GlobalVariable;
00052 import forge.program.InstanceDomain;
00053 import forge.program.InstanceLiteral;
00054 import forge.program.IntegerDomain;
00055 import forge.program.IntegerLiteral;
00056 import forge.program.LocalDecls;
00057 import forge.program.LocalVariable;
00058 import forge.program.ForgeType.Tuple;
00059 import forge.solve.BooleanAtom;
00060 import forge.solve.ForgeAtom;
00061 import forge.solve.ForgeBounds;
00062 import forge.solve.ForgeConstant;
00063 import forge.solve.IntegerAtom;
00064 import forge.solve.SolveOptions;
00065 import forge.solve.SolveOptions.SatSolver;
00066
00074 public class ForgeConverter {
00075
00076 private final SquanderReporter reporter;
00077 private final Heap heap;
00078 private final JavaScene javaScene;
00079 private ForgeScene forgeScene;
00080
00081 private Heap2Bounds heap2lit;
00082 private ForgeBounds forgeBounds;
00083
00084 private boolean finished = false;
00085
00089 public ForgeConverter(SquanderReporter reporter, Object ... heapRootObjects) {
00090 this.reporter = reporter;
00091 this.heap = new Heap(heapRootObjects);
00092 this.javaScene = new JavaScene();
00093 }
00094
00098 public void setCallContext(Object caller, JMethod m, Object[] methodArgs) {
00099 assert !finished : "don't add stuff after calling finish()";
00100 createFreshObjects(m.spec());
00101 initJavaScene();
00102 javaScene.setCaller(caller);
00103 javaScene.setArgs(methodArgs);
00104 for (int i = 0; i < methodArgs.length; i++) {
00105 obj2typeparams.put(methodArgs[i], m.paramTypes().get(i).typeParams());
00106 }
00107 javaScene.setMethod(m);
00108 javaScene.finish();
00109 forgeScene = new ForgeScene(javaScene);
00110
00111 finish();
00112 }
00113
00118 public void boundSpecFields(IEvaluator eval) {
00119 for (JField fld : javaScene.specFields()) {
00120 GlobalVariable mod = forgeScene.global(fld);
00121 ObjTupleSet val = eval.evaluate(mod);
00122 heap2lit.addBound(fld.fullName(), val);
00123 if (forgeBounds != null) {
00124 ForgeConstant fc = conv2fc(val, forgeBounds);
00125 forgeBounds.boundInitial(mod, fc, fc);
00126 }
00127 }
00128 }
00129
00130 public JavaScene javaScene() { assert finished : "call finish() first"; return javaScene; }
00131 public ForgeScene forgeScene() { assert finished : "call finish() first"; return forgeScene; }
00132 public Heap2Bounds heap2Lit() { assert finished : "call finish() first"; return heap2lit; }
00133 public ForgeBounds forgeBounds() {
00134 assert finished : "call finish() first";
00135 if (forgeBounds == null)
00136 forgeBounds = makeForgeBounds(heap2lit);
00137 return forgeBounds;
00138 }
00139
00140 private void finish() {
00141 assert !finished : "don't call finish() twice";
00142
00143
00144 reporter.traversingHeap();
00145 heap2lit = new Heap2Bounds(javaScene);
00146 List<Object> heapObjects = heap.getHeapObjects();
00147 List<Pair> rootObjects = new ArrayList<Pair>(heapObjects.size());
00148 for (Object o : heapObjects)
00149 rootObjects.add(new Pair(o, obj2typeparams.get(o)));
00150 heap2lit.traverse(rootObjects);
00151 for (Object o : heap2lit.reachableObjects()) {
00152 if (!Utils.isPrimitive(o.getClass()))
00153 forgeScene.createLiteral(o);
00154 else if (o instanceof Integer)
00155 forgeScene.ensureInt((Integer) o);
00156 }
00157
00158 forgeScene.createLocalsForMethod(javaScene.method());
00159
00160
00161 reporter.translatingSpecs();
00162 javaScene.translateSpecs(forgeScene);
00163
00164
00165 Options opts = javaScene.methodSpec().options();
00166 if (opts != null) {
00167 forgeScene.ensureAllInts(opts.ensureAllInts());
00168 }
00169
00170
00171 for (ForgeType ft : forgeScene.numTypes()) {
00172 int max = getMaxAtomsForType(ft);
00173 for (int i = 0; i <= max; i++) {
00174 heap2lit.ensureAdequateIntBitWidth(i);
00175 forgeScene.ensureInt(i);
00176 }
00177 }
00178
00179 finished = true;
00180
00181
00182 boundOtherStuff();
00183 reporter.end();
00184
00185 Log.log(printUniverseStats());
00186 }
00187
00188 private Map<Object, JType.Unary[]> obj2typeparams = new IdentityHashMap<Object, Unary[]>();
00189
00190 private void createFreshObjects(MethodSpec ms) {
00191 reporter.creatingFreshObjects();
00192 if (ms != null) {
00193 for (Entry<JType.Unary, Integer> e : ms.freshObjects().entrySet()) {
00194 Integer num = e.getValue();
00195 Class<?> cls = e.getKey().clazz();
00196 for (int i = 0; i < num; i++) {
00197 Object obj = ObjSerFactory.factory.getSerForCls(cls).newInstance(cls);
00198 heap.addObject(obj);
00199 obj2typeparams.put(obj, e.getKey().typeParams());
00200 }
00201 }
00202 }
00203 }
00204
00205 private Map<ForgeType, Integer> maxAtomsCache = new HashMap<ForgeType, Integer>();
00206
00207 private int getMaxAtomsForType(ForgeType ft) {
00208 Integer result = maxAtomsCache.get(ft);
00209 if (result == null) {
00210 int max = -1;
00211 for (Tuple t : ft.tupleTypes()) {
00212 int tupleSize = 1;
00213 for (ForgeDomain d : t.domains()) {
00214 tupleSize *= maxSize(d);
00215 }
00216 if (tupleSize > max)
00217 max = tupleSize;
00218 }
00219 result = max;
00220 maxAtomsCache.put(ft, result);
00221 }
00222 return result;
00223 }
00224
00225 private int maxSize(ForgeDomain d) {
00226 if (d instanceof BooleanDomain)
00227 return 2;
00228 if (d instanceof IntegerDomain) {
00229 if (!forgeScene.isEnsureAllInts())
00230 return forgeScene.ints().size() - 1;
00231 else
00232 return 1;
00233 }
00234 InstanceDomain id = (InstanceDomain) d;
00235 int num = forgeScene.numLiteralsFor(id);
00236 return num;
00237 }
00238
00239 public String printBounds() {
00240 StringBuilder sb = new StringBuilder();
00241 for (Entry<String, ObjTupleSet> e : heap2lit.bounds().entrySet()) {
00242 sb.append(e.getKey() + ": " + printObjSet(e.getValue())).append("\n");
00243 }
00244 return sb.toString();
00245 }
00246
00247 private String printObjSet(ObjTupleSet objSet) {
00248 StringBuilder sb = new StringBuilder();
00249 sb.append("[");
00250 int c = 0;
00251 for (ObjTuple t : objSet.tuples()) {
00252 if (c != 0)
00253 sb.append("; ");
00254 sb.append("[");
00255 for (int i = 0; i < t.arity(); i++) {
00256 if (i != 0)
00257 sb.append(", ");
00258 sb.append(forgeScene.forgeLitForObj(t.get(i)));
00259 }
00260 sb.append("]");
00261 c++;
00262 }
00263 sb.append("]");
00264 return sb.toString();
00265 }
00266
00267 public ForgeProcedure proc() {
00268 assert finished : "call finish() first";
00269 String name = "forge_proc";
00270 if (javaScene.methodSpec() != null)
00271 name = javaScene.method().name();
00272 ForgeProgram prog = forgeScene.program();
00273 LocalDecls ins = prog.emptyDecls();
00274 LocalDecls outs = prog.emptyDecls();
00275 if (forgeScene.thisVar() != null)
00276 ins = ins.and(forgeScene.thisVar());
00277 for (LocalVariable var : forgeScene.args())
00278 ins = ins.and(var);
00279 if (forgeScene.returnVar() != null)
00280 outs = outs.and(forgeScene.returnVar());
00281 return prog.newProcedure(name, ins, outs);
00282 }
00283
00284 public Spec getSpec() {
00285 Spec spec = new Spec(javaScene, forgeScene);
00286 for (CaseSource cs : javaScene.methodSpec().cases()) {
00287 spec.addCase(cs.pre(), cs.post(), cs.frame(), javaScene.methodSpec().isHelper());
00288 }
00289 return spec;
00290 }
00291
00292 public SolveOptions forgeOptions() {
00293 assert finished : "call finish() first";
00294 SatSolver satSolver = SatSolver.valueOf("SAT4J");
00295 return new SolveOptions.Builder()
00296 .reporter(reporter)
00297 .satSolver(satSolver)
00298 .build();
00299 }
00300
00301 private Set<Integer> allInts = null;
00302 public Iterable<Integer> allInts() {
00303 if (allInts != null)
00304 return allInts;
00305 allInts = new HashSet<Integer>();
00306 int minInt = minInt();
00307 int maxInt = maxInt();
00308 if (forgeScene.isEnsureAllInts()) {
00309 for (int i = minInt; i <= maxInt; i++)
00310 allInts.add(i);
00311 } else {
00312 for (int i : forgeScene.ints())
00313 if (i >= minInt && i <= maxInt)
00314 allInts.add(i);
00315 }
00316 return allInts;
00317 }
00318
00319 private Map<ForgeType.Unary, List<InstanceLiteral>> instLitsCache = new HashMap<ForgeType.Unary, List<InstanceLiteral>>();
00320 public List<InstanceLiteral> findInstLiteralsForType(ForgeType.Unary colType) {
00321 List<InstanceLiteral> res = instLitsCache.get(colType);
00322 if (res == null) {
00323 ForgeProgram program = forgeScene.program();
00324 List<InstanceLiteral> lits = new LinkedList<InstanceLiteral>();
00325 for (InstanceLiteral l : program.instanceLiterals()) {
00326 if (l.type().subtypeOf(colType))
00327 lits.add(l);
00328 }
00329 res = Collections.unmodifiableList(lits);
00330 if (finished)
00331 instLitsCache.put(colType, res);
00332 }
00333 return res;
00334 }
00335
00336 private Map<ForgeType.Unary, List<ForgeLiteral>> litsCache = new HashMap<ForgeType.Unary, List<ForgeLiteral>>();
00338 public List<ForgeLiteral> findLiteralsForType(ForgeType.Unary colType) {
00339 List<ForgeLiteral> res = litsCache.get(colType);
00340 if (res == null) {
00341 ForgeProgram program = forgeScene.program();
00342 LinkedList<ForgeLiteral> lits = new LinkedList<ForgeLiteral>();
00343 lits.addAll(findInstLiteralsForType(colType));
00344 if (program.booleanDomain().subtypeOf(colType)) {
00345 lits.add(program.trueLiteral());
00346 lits.add(program.falseLiteral());
00347 }
00348 if (program.integerDomain().subtypeOf(colType)) {
00349 for (int i : allInts())
00350 lits.add(program.integerLiteral(i));
00351 }
00352 res = Collections.unmodifiableList(lits);
00353 if (finished)
00354 litsCache.put(colType, res);
00355 }
00356 return res;
00357 }
00358
00359 public ObjTupleSet extent(ForgeType t) {
00360
00361 ObjTupleSet result = null;
00362 for (int i = 0; i < t.arity(); i++) {
00363 ForgeType.Unary colType = (ForgeType.Unary) t.projectType(i);
00364 ObjTupleSet ots = new ObjTupleSet(1);
00365 for (ForgeLiteral lit : findLiteralsForType(colType)) {
00366 ots.add(new ObjTuple(lit2obj(lit)));
00367 }
00368 if (result == null)
00369 result = ots;
00370 else
00371 result = result.product(ots);
00372 }
00373 if (result == null)
00374 result = new ObjTupleSet(t.arity());
00375 return result;
00376 }
00377
00378
00379
00383 public Object atom2obj(ForgeAtom atom) {
00384 if (atom instanceof IntegerAtom) {
00385 return mapToInt(atom);
00386 } else if (atom instanceof BooleanAtom) {
00387 return mapToBoolean(atom);
00388 } else {
00389 Object obj = forgeScene.objForLit(atom.name());
00390 assert obj != null || "null".equals(atom.name()) : "cannot find object for atom " + atom.name();
00391 return obj;
00392 }
00393 }
00394
00398 public Object lit2obj(ForgeLiteral lit) {
00399 if (lit instanceof IntegerLiteral)
00400 return ((IntegerLiteral) lit).value();
00401 if (lit instanceof BooleanLiteral)
00402 return ((BooleanLiteral) lit).value();
00403 else {
00404 Object obj = forgeScene.objForLit(lit.name());
00405 assert obj != null || "null".equals(lit.name()) : "cannot find object for literal " + lit.name();
00406 return obj;
00407 }
00408 }
00409
00410 public static Object mapToBoolean(final ForgeAtom atom) {
00411 return ((BooleanAtom) atom).value();
00412 }
00413
00414 public static int mapToInt(final ForgeAtom atom) {
00415 return ((IntegerAtom) atom).value();
00416 }
00417
00419 public int minInt() {
00420 assert finished : "Must call finish() first";
00421 return -(int)Math.pow(2, heap2lit.minBW() - 1);
00422 }
00423
00425 public int maxInt() {
00426 assert finished : "Must call finish() first";
00427 return (int)Math.pow(2, heap2lit.minBW() - 1) - 1;
00428 }
00429
00433
00434 public ForgeConstant conv2fc(ObjTupleSet objTupleSet, ForgeBounds bounds) {
00435 ForgeConstant result = bounds.empty(objTupleSet.arity());
00436 for (ObjTuple t : objTupleSet) {
00437 ForgeConstant fc = obj2atom(t.get(0), bounds);
00438 for (int i = 1; i < t.arity(); i++)
00439 fc = fc.product(obj2atom(t.get(i), bounds));
00440 result = result.union(fc);
00441 }
00442 return result;
00443 }
00444
00448 public ForgeAtom obj2atom(Object obj, ForgeBounds bounds) {
00449 if (obj == null)
00450 return bounds.instanceAtom(forgeScene.nullLit());
00451 if (obj instanceof Integer)
00452 return bounds.intAtom((Integer) obj);
00453 if (obj instanceof Boolean)
00454 return bounds.boolAtom((Boolean) obj);
00455 return bounds.instanceAtom(forgeScene.instLitForObj(obj));
00456 }
00457
00458
00459
00460
00461
00462 private void initJavaScene() {
00463 reporter.loadingJavaScene();
00464 final Set<Object> visitedObjects = new IdentityHashSet<Object>();
00465 final Map<Object, Unary[]> typeParams = new IdentityHashMap<Object, Unary[]>();
00466 final Map<Object, Field> flds = new IdentityHashMap<Object, Field>();
00467
00468 heap.serialize(new AbstractHeapListener() {
00469 @Override public void newObject(Object obj) {
00470 visitedObjects.add(obj);
00471 }
00472 @Override public void visitRefField(Field field, Object source, Object value) {
00473 Unary[] tp = JField.newJavaField(field).getTypeParams()[0];
00474 typeParams.put(value, tp);
00475 flds.put(value, field);
00476 }
00477 });
00478 for (Object obj : visitedObjects) {
00479 Unary[] tp = typeParams.get(obj);
00480 if (obj instanceof Collection<?> && tp == null)
00481 continue;
00482 if (tp == null)
00483 javaScene.ensureClass(obj.getClass());
00484 else
00485 javaScene.ensureClass(JType.Factory.instance.newJType(obj.getClass(), tp));
00486 }
00487 }
00488
00489 private void boundOtherStuff() {
00490
00491 for (GlobalVariable constVar : forgeScene.consts()) {
00492 ConstRel rel = ConstRels.findRel(constVar.name());
00493 ObjTupleSet bound = rel.accept(new ConstRel2Bound(this));
00494 heap2lit.addBound(constVar.name(), bound);
00495 }
00496
00497
00498 LocalVariable thisVar = forgeScene.thisVar();
00499 if (thisVar != null) {
00500 ObjTuple callerObjAtom = new ObjTuple(javaScene.caller());
00501 heap2lit.addBound(thisVar.name(), callerObjAtom);
00502 }
00503
00504
00505 LocalVariable[] params = forgeScene.args();
00506 Object[] methodArgs = javaScene.methodArgs();
00507 assert methodArgs.length == params.length;
00508 for (int i = 0; i < params.length; i++) {
00509 ObjTuple argAtom = new ObjTuple(methodArgs[i]);
00510 heap2lit.addBound(params[i].name(), argAtom);
00511 }
00512 }
00513
00514 private ForgeBounds makeForgeBounds(Heap2Bounds heap2lit) {
00515 reporter.creatingBounds();
00516
00517 HashMap<InstanceDomain, Integer> scopes = new HashMap<InstanceDomain, Integer>();
00518
00519
00520
00521
00522 for (InstanceDomain idom : forgeScene.domains()) {
00523 scopes.put(idom, 0);
00524 }
00525
00526 int bw = heap2lit.minBW();
00527 ForgeBounds bounds = new ForgeBounds(forgeScene.program(), bw, scopes);
00528
00529
00530 for (Entry<String, ObjTupleSet> e : heap2lit.bounds().entrySet()) {
00531 ForgeVariable var = forgeScene.findVar(e.getKey());
00532 ForgeConstant fc = conv2fc(e.getValue(), bounds);
00533 bounds.boundInitial(var, fc, fc);
00534 }
00535
00536 return bounds;
00537 }
00538
00539 private String printUniverseStats() {
00540 Map<InstanceDomain, Integer> nums = new HashMap<InstanceDomain, Integer>();
00541 for (InstanceLiteral lit : forgeScene.program().instanceLiterals()) {
00542 Integer cnt = nums.get(lit.type());
00543 if (cnt == null)
00544 cnt = 0;
00545 nums.put(lit.type(), cnt + 1);
00546 }
00547 List<Entry<InstanceDomain, Integer>> cnts = new ArrayList<Entry<InstanceDomain, Integer>>(nums.entrySet());
00548 Collections.sort(cnts, new Comparator<Entry<InstanceDomain, Integer>>() {
00549 @Override
00550 public int compare(Entry<InstanceDomain, Integer> o1, Entry<InstanceDomain, Integer> o2) {
00551 if (o1.getValue() == o2.getValue())
00552 return 0;
00553 if (o1.getValue() > o2.getValue())
00554 return -1;
00555 else
00556 return 1;
00557 }
00558 });
00559 StringBuilder sb = new StringBuilder();
00560 sb.append("Universe stats: \n");
00561 sb.append("-----------------------------------------------------\n");
00562 for (Entry<InstanceDomain, Integer> e : cnts) {
00563 sb.append(String.format("%40s : %s\n", e.getKey(), e.getValue()));
00564 }
00565 sb.append("=====================================================\n");
00566 sb.append(String.format("%40s : %s\n", "Total", forgeScene.program().instanceLiterals().size()));
00567 return sb.toString();
00568 }
00569
00570 }