00001
00005 package edu.mit.csail.sdg.squander.engine;
00006
00007 import java.util.Arrays;
00008 import java.util.HashMap;
00009 import java.util.LinkedList;
00010 import java.util.List;
00011 import java.util.Map;
00012 import java.util.Set;
00013
00014 import edu.mit.csail.sdg.squander.absstate.FieldValue;
00015 import edu.mit.csail.sdg.squander.absstate.ObjTuple;
00016 import edu.mit.csail.sdg.squander.absstate.ObjTupleSet;
00017 import edu.mit.csail.sdg.squander.options.GlobalOptions;
00018 import edu.mit.csail.sdg.squander.serializer.special.IObjSer;
00019 import edu.mit.csail.sdg.squander.serializer.special.ObjSerFactory;
00020 import edu.mit.csail.sdg.squander.spec.ClassSpec;
00021 import edu.mit.csail.sdg.squander.spec.JType;
00022 import edu.mit.csail.sdg.squander.spec.JavaScene;
00023 import edu.mit.csail.sdg.squander.spec.JType.Unary;
00024 import edu.mit.csail.sdg.squander.utils.Utils;
00025 import forge.program.ForgeVariable;
00026
00027 import kodkod.util.collections.IdentityHashSet;
00028
00029
00030
00031
00032
00039 public class Heap2Bounds {
00040
00044 public static class Pair {
00045 Object obj;
00046 JType.Unary[] actualTypeArgs;
00047
00048 public Pair(Object obj) {
00049 init(obj);
00050 }
00051
00052 public Pair(Object obj, Unary[] actualTypeArgs) {
00053 if (actualTypeArgs == null)
00054 init(obj);
00055 else
00056 init(obj, actualTypeArgs);
00057 }
00058
00059 @Override
00060 public String toString() {
00061 return String.format("(%s, %s)", obj, Arrays.toString(actualTypeArgs));
00062 }
00063
00064 private void init(Object obj) {
00065 this.obj = obj;
00066 this.actualTypeArgs = new Unary[obj.getClass().getTypeParameters().length];
00067 for (int i = 0; i < actualTypeArgs.length; i++)
00068 actualTypeArgs[i] = JType.Factory.instance.newJType(Object.class);
00069 }
00070
00071 private void init(Object obj, Unary[] actualTypeArgs) {
00072 assert actualTypeArgs.length == obj.getClass().getTypeParameters().length;
00073 this.obj = obj;
00074 this.actualTypeArgs = actualTypeArgs;
00075 }
00076 }
00077
00078 private final JavaScene javaScene;
00079 private final Set<Object> visited = new IdentityHashSet<Object>();
00080
00081 private Map<String, ObjTupleSet> varName2Const = new HashMap<String, ObjTupleSet>();
00082 private int rbw = GlobalOptions.INSTANCE.min_bitwidth;
00083
00084 public Heap2Bounds(JavaScene javaScene) {
00085 this.javaScene = javaScene;
00086 }
00087
00089 public int minBW() { return rbw; }
00091 public Map<String, ObjTupleSet> bounds() { return varName2Const; }
00093 public ObjTupleSet getBound(ForgeVariable var) { return varName2Const.get(var.name()); }
00095 public Set<Object> reachableObjects() { return visited; }
00096
00098 public void ensureAdequateIntBitWidth(int x) {
00099 int bw = 1 + (32 - Integer.numberOfLeadingZeros(Math.abs(x)));
00100 rbw = Math.max(rbw, bw);
00101 }
00102
00108 public void traverse(List<Pair> rootObjects) {
00109 List<Pair> workList = new LinkedList<Pair>();
00110 for (Pair p : rootObjects)
00111 workList.add(new Pair(p.obj, p.actualTypeArgs));
00112 ObjSerFactory f = ObjSerFactory.factory;
00113 while (!workList.isEmpty()) {
00114 Pair p = workList.remove(0);
00115 if (!visited.add(p.obj))
00116 continue;
00117 newObject(p.obj, p.actualTypeArgs);
00118 IObjSer ser = f.getSerForObj(p.obj);
00119 List<FieldValue> vals = ser.absFunc(javaScene, p.obj);
00120 for (FieldValue val : vals) {
00121 Unary[][] tparams = val.jfield().getTypeParams();
00122 assert tparams.length == val.jfield().type().arity();
00123 addBound(val.jfield().fullName(), val.tupleSet());
00124 for (ObjTuple ot : val.tupleSet()) {
00125 for (int i = 0; i < ot.arity(); i++) {
00126 Object atom = ot.get(i);
00127 if (atom == null)
00128 continue;
00129 workList.add(new Pair(atom, i == 0 ? null : tparams[i-1]));
00130 }
00131 }
00132 }
00133 }
00134 }
00135
00136 void addBound(String varName, ObjTuple value) {
00137 ObjTupleSet ots = new ObjTupleSet(value.arity());
00138 ots.add(value);
00139 addBound(varName, ots);
00140 }
00141
00142 void addBound(String varName, ObjTupleSet value) {
00143 ObjTupleSet curVal = varName2Const.get(varName);
00144 if (curVal == null) {
00145 curVal = new ObjTupleSet(value.arity());
00146 varName2Const.put(varName, curVal);
00147 }
00148 for (ObjTuple ot : value)
00149 curVal.add(ot);
00150 }
00151
00152
00153
00154
00155
00156 private void newObject(Object object, Unary[] actualTypeParams) {
00157 if (object == null)
00158 return;
00159 ensureAdequateBitWidth(object);
00160 Class<?> cls = object.getClass();
00161 ClassSpec cs = javaScene.ensureClass(JType.Factory.instance.newJType(cls, actualTypeParams));
00162 javaScene.addObj2spec(object, cs);
00163 if (Utils.isPrimitive(cls))
00164 visitPrimitive(object);
00165 }
00166
00167 private void visitPrimitive(Object obj) {
00168 if (obj.getClass() == Integer.class) {
00169 int intVal = (Integer) obj;
00170 ensureAdequateIntBitWidth(intVal);
00171 }
00172 }
00173
00174 private void ensureAdequateBitWidth(final Object obj) {
00175 if (obj == null)
00176 return;
00177 final Class<?> cls = obj.getClass();
00178 if (cls.isArray()) {
00179
00180 if (cls.getComponentType().isPrimitive()) {
00181
00182 if (cls.getComponentType().equals(int.class)) {
00183 int[] a = (int[]) obj;
00184 for (int x : a) {
00185 ensureAdequateBitWidth(x);
00186 }
00187 }
00188 } else {
00189
00190 }
00191 } else {
00192
00193 if (obj instanceof Integer || obj.getClass().equals(int.class)) {
00194 ensureAdequateIntBitWidth((Integer) obj);
00195 }
00196 }
00197 }
00198
00199 }
00200
00201
00202