00001
00005 package edu.mit.csail.sdg.squander.spec;
00006
00007 import java.util.ArrayList;
00008 import java.util.Collection;
00009 import java.util.Collections;
00010 import java.util.HashMap;
00011 import java.util.HashSet;
00012 import java.util.IdentityHashMap;
00013 import java.util.List;
00014 import java.util.Map;
00015 import java.util.Set;
00016 import java.util.Map.Entry;
00017
00018 import edu.mit.csail.sdg.squander.serializer.special.ArraySer;
00019 import edu.mit.csail.sdg.squander.spec.constant.ConstRels;
00020 import edu.mit.csail.sdg.squander.utils.Counter;
00021 import edu.mit.csail.sdg.squander.utils.Utils;
00022 import forge.program.ForgeDomain;
00023 import forge.program.ForgeExpression;
00024 import forge.program.ForgeLiteral;
00025 import forge.program.ForgeProgram;
00026 import forge.program.ForgeType;
00027 import forge.program.ForgeVariable;
00028 import forge.program.GlobalVariable;
00029 import forge.program.InstanceDomain;
00030 import forge.program.InstanceLiteral;
00031 import forge.program.LocalDecls;
00032 import forge.program.LocalVariable;
00033 import forge.util.ExpressionUtil;
00034
00035 public class ForgeScene {
00036
00037 public static class ArrayVars {
00038 public final Class<?> cls;
00039 public final GlobalVariable elems;
00040 public final GlobalVariable length;
00041
00042 public ArrayVars(Class<?> cls, GlobalVariable elems, GlobalVariable length) {
00043 this.cls = cls;
00044 this.elems = elems;
00045 this.length = length;
00046 }
00047 }
00048
00049 private final Counter<JType.Unary> counter = new Counter<JType.Unary>();
00050 private final Counter<InstanceDomain> litCnt = new Counter<InstanceDomain>();
00051
00052 private final JavaScene javaScene;
00053 private final ForgeProgram program;
00054 private final InstanceDomain nullType;
00055 private final InstanceLiteral nullLit;
00056
00058 private final IdentityHashMap<Object, InstanceLiteral> obj2lit = new IdentityHashMap<Object, InstanceLiteral>();
00060 private final HashMap<String, InstanceLiteral> str2lit = new HashMap<String, InstanceLiteral>();
00061
00066 private final Map<String, Object> lit2obj = new HashMap<String, Object>();
00067
00069 private final Map<JType.Unary, ForgeDomain> cls2dom = new HashMap<JType.Unary, ForgeDomain>();
00070
00072 private final Map<String, GlobalVariable> globals = new HashMap<String, GlobalVariable>();
00074 private final Map<String, LocalVariable> locals = new HashMap<String, LocalVariable>();
00075
00076 private final Map<String, GlobalVariable> consts = new HashMap<String, GlobalVariable>();
00077
00078 private final Map<GlobalVariable, Set<JField>> var2fld = new HashMap<GlobalVariable, Set<JField>>();
00079
00081 private final Set<Integer> ints = new HashSet<Integer>(64);
00082
00084 private boolean ensureAllInts = false;
00085
00087 private Map<String, ForgeType> numTypes = new HashMap<String, ForgeType>();
00088
00089 private Map<String, ForgeType.Unary> usedTypes = new HashMap<String, ForgeType.Unary>();
00090
00091 private LocalVariable throwVar;
00092 private LocalVariable returnVar;
00093 private LocalVariable thisVar;
00094 private LocalVariable[] args = new LocalVariable[0];
00095
00096 public ForgeScene(JavaScene javaScene) {
00097 this.javaScene = javaScene;
00098 this.program = new ForgeProgram();
00099 this.nullType = program.newInstanceDomain("Null");
00100 this.nullLit = program.newInstanceLiteral("null", nullType);
00101 litCnt.incrementAndGet(nullType);
00102 lit2obj.put(nullLit.name(), null);
00103 cls2dom.put(JType.Factory.instance.integerType(), program.integerDomain());
00104 cls2dom.put(JType.Factory.instance.booleanType(), program.booleanDomain());
00105 addUsedType(program.integerDomain());
00106 addUsedType(program.booleanDomain());
00107 addUsedType(this.nullType);
00108 }
00109
00110 public void createLocalsForMethod(JMethod m) {
00111 {
00112
00113 if (m.returnType().clazz() != void.class) {
00114 String name = m.name() + "_ret";
00115 ForgeType type = typeForCls(m.returnType(), true);
00116 returnVar = program.newLocalVariable(name, type);
00117 locals.put(returnVar.name(), returnVar);
00118 }
00119 }
00120 {
00121
00122 if (!m.isStatic()) {
00123 thisVar = newThisVariable(m.declaringClass());
00124 locals.put(thisVar.name(), thisVar);
00125 }
00126 }
00127 {
00128
00129 Map<String, JType.Unary> params = m.params();
00130 args = new LocalVariable[params.size()];
00131 int i = 0;
00132 for (Entry<String, JType.Unary> e : params.entrySet()) {
00133 ForgeType type = typeForCls(e.getValue(), true);
00134 args[i] = program.newLocalVariable(e.getKey(), type);
00135 locals.put(args[i].name(), args[i]);
00136 i++;
00137 }
00138 }
00139 }
00140
00141 public LocalVariable newThisVariable(JType.Unary type) {
00142 String name = type.simpleName() + "_this";
00143 ForgeType ftype = typeForCls(type, false);
00144 return program.newLocalVariable(name, ftype);
00145 }
00146
00147 public ForgeEnv getEnv(LocalVariable thisVar) {
00148 Map<String, LocalVariable> locals = new HashMap<String, LocalVariable>();
00149 for (LocalVariable var : args) {
00150 locals.put(var.name(), var);
00151 }
00152 return new MyEnv(thisVar, locals);
00153 }
00154
00155 public ForgeProgram program() { return program; }
00156 public LocalVariable thisVar() { return thisVar; }
00157 public LocalVariable returnVar() { return returnVar; }
00158 public LocalVariable throwVar() { return throwVar; }
00159 public LocalVariable[] args() { return args; }
00160 public InstanceLiteral nullLit() { return nullLit; }
00161 public InstanceDomain nullType() { return nullType; }
00162 public Set<InstanceDomain> domains() { return program.instanceDomains(); }
00163 public GlobalVariable global(String name) { return globals.get(name); }
00164 public GlobalVariable global(JField fld) { return globals.get(fld.fullName()); }
00165 public Collection<GlobalVariable> consts() { return consts.values(); }
00166 public boolean isConst(GlobalVariable var) { return consts.containsKey(var.name()); }
00167 public ForgeVariable findVar(String name) {
00168 ForgeVariable var = global(name);
00169 if (var == null)
00170 var = consts.get(name);
00171 if (var == null)
00172 var = locals.get(name);
00173 return var;
00174 }
00175
00176 public Set<JField> fields(GlobalVariable var) {
00177 return var2fld.get(var);
00178 }
00179
00180 public boolean isSpecField(GlobalVariable var) {
00181 Set<JField> fields = fields(var);
00182 if (fields == null || fields.isEmpty())
00183 return false;
00184
00185 return fields.iterator().next().isSpec();
00186 }
00187
00188 public boolean isOneField(GlobalVariable var) {
00189
00190 Set<JField> fields = fields(var);
00191 if (fields.isEmpty())
00192 throw new RuntimeException("No such field: " + var.name());
00193
00194 JField f = fields.iterator().next();
00195 if (!f.isSpec())
00196 return true;
00197 else {
00198 return f.getBound().expr.toString().startsWith("(one (");
00199 }
00200 }
00201
00202 public Collection<? extends GlobalVariable> nonAbstractSpecFields() {
00203 List<GlobalVariable> specFields = new ArrayList<GlobalVariable>();
00204 for (GlobalVariable g : globals.values())
00205 if (isSpecField(g) && !isPureAbstractSpecField(g))
00206 specFields.add(g);
00207 return specFields;
00208 }
00209
00210
00211 public boolean isPureAbstractSpecField(GlobalVariable var) {
00212 Set<JField> fields = fields(var);
00213 if (fields.isEmpty())
00214 return false;
00215 for (JField f : fields) {
00216 if (!f.getAbsFun().expr.equals(program.trueLiteral()))
00217 return false;
00218 }
00219 return true;
00220 }
00221
00222 public ForgeDomain findDomain(JType.Unary clz) { return cls2dom.get(clz); }
00223
00224 public ForgeDomain ensureDomain(JType.Unary clz) {
00225 ForgeDomain dom = cls2dom.get(clz);
00226 if (dom == null) {
00227 dom = program.newInstanceDomain(clz.simpleName());
00228 cls2dom.put(clz, dom);
00229 addUsedType(dom);
00230 }
00231 return dom;
00232 }
00233
00234 public JType.Unary findClassForDomain(ForgeDomain dom) {
00235 for (Entry<JType.Unary, ForgeDomain> e : cls2dom.entrySet()) {
00236 if (e.getValue().equals(dom))
00237 return e.getKey();
00238 }
00239 return null;
00240 }
00241
00242 public void ensureInt(int i) { ints.add(i); }
00244 public Set<Integer> ints() { return ints; }
00245 public boolean isEnsureAllInts() { return ensureAllInts; }
00246 public void ensureAllInts(boolean b) { ensureAllInts = b; }
00247 public Collection<ForgeType> numTypes() { return numTypes.values(); }
00248 public Set<ForgeType.Unary> usedTypes() { return Collections.unmodifiableSet(new HashSet<ForgeType.Unary>(usedTypes.values())); }
00249
00250 public GlobalVariable ensureGlobal(JField field) {
00251 String name = field.fullName();
00252 GlobalVariable global = globals.get(name);
00253 if (global == null) {
00254 global = createGlobalVar(field, name);
00255 globals.put(name, global);
00256 Set<JField> fields = new HashSet<JField>();
00257 fields.add(field);
00258 var2fld.put(global, fields);
00259 } else {
00260 Set<JField> fields = var2fld.get(global);
00261 assert !fields.isEmpty();
00262 assert field.isSpec() == fields.iterator().next().isSpec();
00263 fields.add(field);
00264 }
00265 return global;
00266 }
00267
00268 public GlobalVariable ensureConst(String name) {
00269 GlobalVariable var = consts.get(name);
00270 if (var == null) {
00271 ForgeType type = convertToForgeType(ConstRels.findRel(name).type(), true);
00272 var = program.newGlobalVariable(name, type);
00273 consts.put(name, var);
00274 }
00275 return var;
00276 }
00277
00278 public InstanceLiteral createLiteral(Object object) {
00279 JType.Unary cls = javaScene.jtypeForObj(object);
00280 InstanceDomain instanceDomain = (InstanceDomain) ensureDomain(cls);
00281 int cnt = counter.incrementAndGet(cls);
00282 InstanceLiteral lit = program.newInstanceLiteral(cls.simpleName() + "_" + cnt, instanceDomain);
00283 litCnt.incrementAndGet(instanceDomain);
00284 if (object instanceof String)
00285 str2lit.put((String)object, lit);
00286 else
00287 obj2lit.put(object, lit);
00288 lit2obj.put(lit.name(), object);
00289 return lit;
00290 }
00291
00292 public int numLiteralsFor(InstanceDomain id) {
00293 return litCnt.getCount(id);
00294 }
00295
00296 @SuppressWarnings("unchecked")
00297 public ForgeType.Unary typeForCls(JType.Unary cls, boolean includeNull) {
00298 if (Utils.isPrimitive(cls.clazz()))
00299 return ensureDomain(cls);
00300 else {
00301 ForgeType.Unary t = ensureDomain(cls);
00302 for (ClassSpec sub : javaScene.subTypes(cls)) {
00303 ForgeDomain d = findDomain(sub.jtype());
00304 if (d == null && !sub.isEmpty())
00305 d = ensureDomain(sub.jtype());
00306 if (d != null)
00307 t = t.union(ensureDomain(sub.jtype()));
00308 }
00309 if (cls.clazz().isAssignableFrom(Integer.class))
00310 t = t.union(program.integerDomain());
00311 if (includeNull)
00312 t = t.union(nullType);
00313 addUsedType(t);
00314 return t;
00315 }
00316 }
00317
00318 public Object objForLit(String litName) {
00319 return lit2obj.get(litName);
00320 }
00321
00322 public ForgeLiteral forgeLitForObj(Object obj) {
00323 if (obj instanceof Integer)
00324 return program.integerLiteral((Integer) obj);
00325 if (obj instanceof Boolean) {
00326 boolean b = (Boolean) obj;
00327 if (b)
00328 return program.trueLiteral();
00329 else
00330 return program.falseLiteral();
00331 }
00332 return instLitForObj(obj);
00333 }
00334
00335 public InstanceLiteral instLitForObj(Object obj) {
00336 if (obj == null)
00337 return nullLit;
00338 if (obj.getClass() == String.class)
00339 return str2lit.get(obj);
00340 return obj2lit.get(obj);
00341 }
00342
00343 public InstanceLiteral litForName(String name) {
00344 for (InstanceLiteral il : program.instanceLiterals())
00345 if (il.name().equals(name))
00346 return il;
00347 return null;
00348 }
00349
00350
00351
00352
00353
00354 private void addUsedType(ForgeType.Unary t) {
00355 usedTypes.put(t.toString(), t);
00356 }
00357
00358 private ForgeType getRangeForField(JField field) {
00359 if (field.isSpec()) {
00360 return convertToForgeType(field.type(), true);
00361 } else {
00362
00363 return typeForCls(field.type().range(), true);
00364 }
00365 }
00366
00367 private ForgeType convertToForgeType(JType jtype, boolean includeNull) {
00368 ForgeType t = typeForCls(jtype.domain(), includeNull);
00369 for (int i = 1; i < jtype.arity(); i++) {
00370 t = t.product(typeForCls(jtype.projection(i), includeNull));
00371 }
00372 return t;
00373 }
00374
00375 private GlobalVariable createGlobalVar(JField field, String name) {
00376 ForgeType domain = convertToForgeType(field.owningType(), false);
00377 ForgeType range = getRangeForField(field);
00378 ForgeType type = domain.product(range);
00379 return program.newGlobalVariable(name, type);
00380 }
00381
00382
00383
00384
00385
00386 private class MyEnv implements ForgeEnv {
00387
00388 private final ForgeEnv.State state;
00389 private final Map<String, LocalVariable> locals;
00390 private LocalVariable myThisVar;
00391
00392 MyEnv(LocalVariable thisVar, Map<String, LocalVariable> locals) {
00393 this(ForgeEnv.State.POST, thisVar, locals);
00394 }
00395
00396 private MyEnv(State state, LocalVariable thisVar, Map<String, LocalVariable> locals) {
00397 this.state = state;
00398 this.myThisVar = thisVar;
00399 this.locals = locals;
00400 }
00401
00402 @Override
00403 public ForgeExpression arg(int i) {
00404 return args[i];
00405 }
00406
00407 @Override
00408 public JType.Unary classForDomain(ForgeDomain domain) {
00409 return findClassForDomain(domain);
00410 }
00411
00412 @Override
00413 public ForgeExpression arrayElems(JType type) {
00414 Class<?> arrCls = type.domain().clazz();
00415 GlobalVariable var = ensureGlobal(javaScene.findSpec(arrCls, true).findField(ArraySer.ELEMS));
00416 return state == State.PRE? ExpressionUtil.bringGlobalsToPreState(var) : var;
00417 }
00418
00419 @Override
00420 public ForgeExpression arrayLength(JType type) {
00421 Class<?> arrCls = type.domain().clazz();
00422 GlobalVariable var = ensureGlobal(javaScene.findSpec(arrCls, true).findField(ArraySer.LENGTH));
00423 return state == State.PRE? ExpressionUtil.bringGlobalsToPreState(var) : var;
00424 }
00425
00426 @Override
00427 public ForgeExpression globalVar(GlobalVariable var) {
00428 if (state == ForgeEnv.State.PRE)
00429 return var.old();
00430 else
00431 return var;
00432 }
00433
00434 @Override
00435 public LocalVariable newLocalVar(String name, ForgeType type) {
00436 return program.newLocalVariable(name, type);
00437 }
00438
00439 @Override public ForgeType integerType() { return program.integerDomain(); }
00440 @Override public ForgeType nullType() { return nullType; }
00441 @Override public ForgeExpression intExpr(int i) { ensureInt(i); return program.integerLiteral(i); }
00442 @Override public ForgeType booleanType() { return program.booleanDomain(); }
00443 @Override public ForgeExpression trueExpr() { return program.trueLiteral(); }
00444 @Override public ForgeExpression falseExpr() { return program.falseLiteral(); }
00445 @Override public LocalDecls emptyDecls() { return program.emptyDecls(); }
00446
00447 @Override public ForgeExpression returnVar() { return returnVar; }
00448 @Override public LocalVariable thisVar() { return myThisVar; }
00449 @Override public ForgeExpression throwVar() { return getThrowVar(); }
00450
00451 @Override
00452 public ForgeEnv setPreStateMode() {
00453 if (state == State.PRE)
00454 throw new RuntimeException("re-entered PRE mode");
00455 return new MyEnv(State.PRE, myThisVar, locals);
00456 }
00457
00458 @Override
00459 public ForgeExpression stringExpr(String text) {
00460 InstanceLiteral lit = str2lit.get(text);
00461 if (lit == null) {
00462 InstanceDomain stringType = (InstanceDomain) stringType();
00463 lit = program.newInstanceLiteral("text", stringType);
00464 litCnt.incrementAndGet(stringType);
00465 str2lit.put(text, lit);
00466 }
00467 return lit;
00468 }
00469
00470 @Override
00471 public ForgeType stringType() {
00472 return ensureDomain(JType.Factory.instance.stringType());
00473 }
00474
00475 @Override
00476 public ForgeEnv addLocal(LocalVariable var) {
00477 Map<String, LocalVariable> newLocals = new HashMap<String, LocalVariable>();
00478 newLocals.putAll(locals);
00479 newLocals.put(var.name(), var);
00480 return new MyEnv(state, myThisVar, newLocals);
00481 }
00482
00483 @Override
00484 public ForgeDomain.Unary ensureDomain(JType.Unary clz) {
00485 return ForgeScene.this.ensureDomain(clz);
00486 }
00487
00488 @Override
00489 public ForgeDomain.Unary typeForCls(JType.Unary clz, boolean includeNull) {
00490 return ForgeScene.this.typeForCls(clz, includeNull);
00491 }
00492
00493 @Override
00494 public GlobalVariable ensureGlobal(JField field) {
00495 return ForgeScene.this.ensureGlobal(field);
00496 }
00497
00498 @Override
00499 public GlobalVariable ensureConst(String name) {
00500 return ForgeScene.this.ensureConst(name);
00501 }
00502
00503 @Override
00504 public LocalVariable findLocal(String name) {
00505 return locals.get(name);
00506 }
00507
00508 @Override
00509 public void ensureAllInts() {
00510 ensureAllInts = true;
00511 }
00512
00513 @Override
00514 public void ensureInt(int i) {
00515 ForgeScene.this.ensureInt(i);
00516 }
00517
00518 @Override
00519 public void ensureNum(ForgeType type) {
00520 numTypes.put(type.toString(), type);
00521 }
00522
00523 private ForgeExpression getThrowVar() {
00524 if (throwVar == null) {
00525 String name = "throw";
00526 ForgeType type = typeForCls(JType.Factory.instance.throwableType(), true);
00527 throwVar = program.newLocalVariable(name, type);
00528 locals.put(throwVar.name(), throwVar);
00529 }
00530 return throwVar;
00531 }
00532 }
00533
00534 }