00001
00005 package edu.mit.csail.sdg.squander.engine;
00006
00007 import java.lang.reflect.Array;
00008 import java.util.ArrayList;
00009 import java.util.Collection;
00010 import java.util.Iterator;
00011 import java.util.List;
00012 import java.util.Set;
00013
00014 import kodkod.util.collections.IdentityHashSet;
00015 import edu.mit.csail.sdg.squander.absstate.FieldValue;
00016 import edu.mit.csail.sdg.squander.absstate.ObjTuple;
00017 import edu.mit.csail.sdg.squander.absstate.ObjTupleSet;
00018 import edu.mit.csail.sdg.squander.serializer.special.ObjSerFactory;
00019 import edu.mit.csail.sdg.squander.spec.ForgeScene;
00020 import edu.mit.csail.sdg.squander.spec.JField;
00021 import edu.mit.csail.sdg.squander.utils.Utils;
00022 import edu.mit.csail.sdg.util.collections.Iterators;
00023 import forge.program.ForgeDomain;
00024 import forge.program.ForgeLiteral;
00025 import forge.program.ForgeProgram;
00026 import forge.program.ForgeType;
00027 import forge.program.GlobalVariable;
00028 import forge.program.LocalVariable;
00029 import forge.program.ForgeType.Unary;
00030
00036 public final class SquanderResult implements ISquanderResult {
00037
00038 private final ForgeConverter fconv;
00039 private final Collection<GlobalVariable> modifiable;
00040 private IEvaluator eval;
00041
00042 public SquanderResult(IEvaluator eval, ForgeConverter fconv, Collection<GlobalVariable> mod) {
00043 this.eval = eval;
00044 this.fconv = fconv;
00045 this.modifiable = mod;
00046 }
00047
00048 public ForgeProgram program() { return fconv.forgeScene().program(); }
00049 public LocalVariable self() { return fconv.forgeScene().thisVar(); }
00050 public LocalVariable returnVar() { return fconv.forgeScene().returnVar(); }
00051
00052 public boolean hasSolution() { return eval.hasSolution(); }
00053 public String getTrace() { return eval.trace(); }
00054 public String getStats() { return eval.stats(); }
00055
00056 public String unsatCore() { return eval.unsatCore(); }
00057
00058 public boolean findNext() {
00059 if (!eval.hasSolution())
00060 return false;
00061 eval = eval.nextSolution();
00062 if (!eval.hasSolution())
00063 return false;
00064 restoreJavaHeap();
00065 return true;
00066 }
00067
00068 @SuppressWarnings("unchecked")
00069 public <R> R getReturnValue() {
00070 if (returnVar() == null) {
00071 return null;
00072 } else {
00073 Class<?> retType = fconv.javaScene().method().returnType().clazz();
00074 assert retType != null;
00075 ObjTupleSet returnVal = eval.evaluate(returnVar());
00076 assert returnVal.tuples().size() == 1 : "return value should not be a set: " + returnVal;
00077 ForgeDomain arrDom = Utils.getArrayDomain(returnVar());
00078 if (arrDom != null) {
00079 GlobalVariable elems = fconv.forgeScene().global(arrDom + "__elems");
00080 returnVal = returnVal.join(eval.evaluate(elems));
00081 return (R) convertForgeSetToJavaArray(returnVal, retType);
00082 }
00083 return (R) returnVal.tuples().iterator().next().get(0);
00084 }
00085 }
00086
00087 public void restoreJavaHeap() {
00088 ForgeScene forgeScene = fconv.forgeScene();
00089 for (GlobalVariable mod : modifiable) {
00090 ObjTupleSet fldVal = eval.evaluate(mod);
00091 IdentityHashSet<Object> visited = new IdentityHashSet<Object>();
00092 if (fldVal.isEmpty()) {
00093 restoreEmpty(mod);
00094 continue;
00095 }
00096 for (ObjTuple ot : fldVal.tuples()) {
00097 Object obj = ot.get(0);
00098 if (obj == null)
00099 continue;
00100 if (!visited.add(obj))
00101 continue;
00102 JField jf = getJFieldForVar(forgeScene, mod);
00103 FieldValue fv = new FieldValue(jf, mod.arity());
00104 ObjTupleSet objFldVal = ObjTupleSet.filter(fldVal, 0, obj);
00105 fv.addAllTuples(objFldVal);
00106 ObjSerFactory.factory.getSerForObj(obj).concrFunc(obj, fv);
00107 }
00108 }
00109 }
00110
00111 @Deprecated
00112 public Iterator<Object> getSpecField(String specFieldName) {
00113
00114 ObjTupleSet self = eval.evaluate(self());
00115 GlobalVariable v = fconv.forgeScene().global(specFieldName);
00116 if (v == null) throw new NullPointerException("couldn't find forge global variable " + specFieldName);
00117 ObjTupleSet evaluate = eval.evaluate(v);
00118 System.out.println("evaluate: " + evaluate);
00119 ObjTupleSet thisSpecFieldValue = ObjTupleSet.join(self, evaluate);
00120 Set<ObjTuple> tuples = thisSpecFieldValue.tuples();
00121
00122 if (tuples.size() == 0) {
00123 return Iterators.empty();
00124 } else if (thisSpecFieldValue.arity() == 0) {
00125
00126 return Iterators.empty();
00127
00128 } else if (thisSpecFieldValue.arity() == 1) {
00129 final Iterator<ObjTuple> it = tuples.iterator();
00130
00131 return new Iterator<Object>() {
00132 @Override public boolean hasNext() { return it.hasNext(); }
00133 @Override public Object next() { return it.next().get(0); }
00134 @Override public void remove() {
00135 throw new UnsupportedOperationException();
00136 }
00137
00138 };
00139
00140 } else if (thisSpecFieldValue.arity() == 2) {
00141
00142
00143 List<Object> seq = new ArrayList<Object>(tuples.size());
00144 for (int i = 0; i < tuples.size(); i++) {
00145 seq.add(null);
00146 }
00147 for (ObjTuple t : tuples) {
00148 int index = (Integer) t.get(0);
00149 Object javaObject = t.get(1);
00150 assert seq.get(index) == null : "seq already has something at index " + index + " " + seq.get(index);
00151 seq.set(index, javaObject);
00152 }
00153
00154 return seq.iterator();
00155 } else {
00156
00157 throw new UnsupportedOperationException("spec field has a weird arity: " + thisSpecFieldValue.arity() + " " + v);
00158 }
00159 }
00160
00161
00162
00163
00164
00165 private JField getJFieldForVar(ForgeScene forgeScene, GlobalVariable mod) {
00166 return forgeScene.fields(mod).iterator().next();
00167 }
00168
00169 private void restoreEmpty(GlobalVariable mod) {
00170 ForgeType.Unary dom = (Unary) mod.type().projectType(0);
00171 for (ForgeLiteral lit : fconv.findLiteralsForType(dom)) {
00172 Object obj = fconv.lit2obj(lit);
00173 JField jf = getJFieldForVar(fconv.forgeScene(), mod);
00174 FieldValue fv = new FieldValue(jf, mod.arity());
00175 ObjSerFactory.factory.getSerForObj(obj).concrFunc(obj, fv);
00176 }
00177 }
00178
00179 private Object convertForgeSetToJavaArray(ObjTupleSet ots, Class<?> arrCls) {
00180 int n = ots.size();
00181 Object arrObj = Array.newInstance(arrCls.getComponentType(), n);
00182 int idx = 0;
00183 for (ObjTuple tuple : ots.tuples()) {
00184 if (tuple.arity() == 1) {
00185 Array.set(arrObj, idx++, tuple.get(0));
00186 } else {
00187 Integer index = (Integer) tuple.get(0);
00188 Array.set(arrObj, index, tuple.get(1));
00189 }
00190 }
00191
00192 return arrObj;
00193 }
00194
00195 }