00001
00005 package edu.mit.csail.sdg.squander.engine;
00006
00007 import java.lang.reflect.Method;
00008 import java.util.Collections;
00009 import java.util.HashSet;
00010 import java.util.Iterator;
00011 import java.util.Set;
00012
00013 import edu.mit.csail.sdg.squander.annotations.Options;
00014 import edu.mit.csail.sdg.squander.engine.ISquanderResult.IEvaluator;
00015 import edu.mit.csail.sdg.squander.log.Log;
00016 import edu.mit.csail.sdg.squander.spec.JMethod;
00017 import edu.mit.csail.sdg.squander.spec.Spec;
00018 import edu.mit.csail.sdg.squander.spec.Spec.SpecCase;
00019 import edu.mit.csail.sdg.squander.utils.ReflectionUtils;
00020 import edu.mit.csail.sdg.util.collections.Iterators;
00021 import forge.cfg.ForgeCFG;
00022 import forge.program.ForgeExpression;
00023 import forge.program.GlobalVariable;
00024 import forge.solve.ForgeSolver;
00025 import forge.util.ExpressionUtil;
00026
00033 public class SquanderImpl implements ISquander {
00034
00035 private ISquanderResult lastResult;
00036 private Spec spec;
00037
00038 protected SquanderReporter reporter;
00039
00040 public SquanderImpl() { }
00041
00042
00043
00044
00045
00066 @SuppressWarnings("unchecked")
00067 public <R> R magic(Object caller, String clsName, String methodName, Class<?>[] methodParams, Object[] methodArgs) {
00068 return (R) magic(caller, convToJMethod(caller, clsName, methodName, methodParams), methodArgs);
00069 }
00070
00071 @SuppressWarnings("unchecked")
00072 public <R> R magic(Object caller, Method method, Object[] methodArgs) {
00073 JMethod jmethod = JMethod.forJavaMethod(method);
00074 return (R) magic(caller, jmethod, methodArgs);
00075 }
00076
00077 @SuppressWarnings("unchecked")
00078 public <R> R magic(Object caller, JMethod method, Object[] methodArgs) {
00079 SquanderReporter reporter = SquanderReporter.INSTANCE;
00080 Iterator<? extends ISquanderResult> results = exeMethod(reporter, caller, method, methodArgs);
00081
00082 if (!results.hasNext()) {
00083 throw new RuntimeException("No results");
00084 }
00085 ISquanderResult result = results.next();
00086 lastResult = result;
00087
00088 Log.debug("===============================================");
00089 Log.debug(" -------------------- Trace -------------------");
00090 Log.debug("===============================================");
00091 Log.debug(result.getTrace());
00092 if (!result.hasSolution()) {
00093 System.err.println(result.unsatCore());
00094 throw new RuntimeException("No solution.");
00095 }
00096 reporter.restoringJavaHeap();
00097 result.restoreJavaHeap();
00098 reporter.finishedAnalysis();
00099 return (R) result.getReturnValue();
00100 }
00101
00102
00103
00104
00105
00106
00107
00108
00109
00110
00111
00112
00113
00114
00115
00116
00117
00118 public ISquanderResult getLastResult() {
00119 return lastResult;
00120 }
00121
00122
00123
00124
00125
00126 protected JMethod convToJMethod(Object caller, String clsName, String methodName, Class<?>[] methodParams) {
00127 Class<?> clz;
00128 try {
00129 if (caller != null)
00130 clz = caller.getClass();
00131 else
00132 clz = Class.forName(clsName);
00133 Method method = ReflectionUtils.findMethod(clz, methodName, methodParams);
00134 return JMethod.forJavaMethod(method);
00135 } catch (NoSuchMethodException e) {
00136 throw new RuntimeException("method " + methodName + " doesn't exist", e);
00137 } catch (ClassNotFoundException e) {
00138 throw new RuntimeException("class " + clsName + " doesn't exist", e);
00139 }
00140 }
00141
00148 protected Iterator<? extends ISquanderResult> exeMethod(SquanderReporter reporter,
00149 Object caller, JMethod m, Object[] methodArgs) {
00150 this.reporter = reporter;
00151 Object[] roots = new Object[methodArgs.length + 1];
00152 roots[0] = caller;
00153 for (int i = 0; i < methodArgs.length; i++) roots[i+1] = methodArgs[i];
00154 ForgeConverter fconv = new ForgeConverter(reporter, roots);
00155 fconv.setCallContext(caller, m, methodArgs);
00156 Spec spec = getSpec(fconv);
00157
00158
00159 boolean predSat = false;
00160 IEvaluator precondEval = null;
00161 for (SpecCase cs : spec.cases()) {
00162 precondEval = checkPre(cs, fconv);
00163 reporter.restoringSpecFields();
00164 if (precondEval.hasSolution()) {
00165 Log.debug(precondEval.trace());
00166 predSat = true;
00167 fconv.boundSpecFields(precondEval);
00168 Iterator<? extends ISquanderResult> res = ensurePost(cs, fconv);
00169 if (res.hasNext())
00170 return res;
00171 }
00172 }
00173 if (!predSat) {
00174 System.err.println("Unsat core: ");
00175 System.err.println(precondEval.unsatCore());
00176 throw new RuntimeException("pre-condition is not satisfied");
00177 }
00178 else
00179 throw new RuntimeException("no solution");
00180 }
00181
00192 protected final IEvaluator checkPre(SpecCase cs, ForgeConverter fconv) {
00193 ForgeExpression pre = getPreSpec(cs);
00194 Log.debug("===============================================");
00195 Log.log (" --------- Checking pre-condition -------------");
00196 Log.debug("===============================================");
00197 Log.debug(ExpressionUtil.prettyPrint(pre));
00198 Log.debug("===============================================");
00199 Log.debug("------------------- Bounds --------------------");
00200 Log.debug("===============================================");
00201 Log.debug(fconv.printBounds());
00202
00203 Set<GlobalVariable> modifies = Collections.<GlobalVariable>emptySet();
00204 return exeSpec(pre, modifies, fconv);
00205 }
00206
00219 protected final Iterator<? extends ISquanderResult> ensurePost(SpecCase cs, ForgeConverter fconv) {
00220 ForgeExpression post = getPostSpec(cs, fconv);
00221
00222 Log.debug("===============================================");
00223 Log.log ("----------- Ensuring post-condition -----------");
00224 Log.debug("===============================================");
00225 Log.debug(ExpressionUtil.prettyPrint(post));
00226 Log.debug("===============================================");
00227 Log.debug("----------------- Modifies --------------------");
00228 Log.debug("===============================================");
00229 Log.debug(cs.frame().modifiable().toString());
00230 Log.debug("===============================================");
00231 Log.debug("------------------- Bounds --------------------");
00232 Log.debug("===============================================");
00233 Log.debug(fconv.printBounds());
00234
00235 Set<GlobalVariable> modifiable = cs.frame().modifiable();
00236 Set<GlobalVariable> mod = getModsForPostState(fconv, cs);
00237 IEvaluator ie = exeSpec(post, mod, fconv);
00238 return Iterators.singleton(new SquanderResult(ie, fconv, modifiable));
00239 }
00240
00241 protected Set<GlobalVariable> getModsForPostState(ForgeConverter fconv, SpecCase sc) {
00242
00243
00244
00245
00246 return fconv.forgeScene().program().globalVariables();
00247 }
00248
00249 protected ForgeExpression getPreSpec(SpecCase cs) {
00250 return cs.pre().and(cs.spec().abstractConstraint());
00251 }
00252
00253 protected ForgeExpression getPostSpec(SpecCase cs, ForgeConverter fconv) {
00254 HashSet<GlobalVariable> unmod = new HashSet<GlobalVariable>();
00255 unmod.addAll(fconv.forgeScene().program().globalVariables());
00256 unmod.removeAll(cs.frame().modifiable());
00257 return cs.spec().abstractConstraint()
00258 .and(cs.spec().funcConstraint())
00259 .and(cs.post())
00260 .and(cs.frame().condition())
00261 .and(cs.spec().wellformedPost(unmod));
00262 }
00263
00264 protected Spec getSpec(ForgeConverter fconv) {
00265 if (spec == null) {
00266 spec = fconv.getSpec();
00267 }
00268 return spec;
00269 }
00270
00274 protected IEvaluator exeSpec(ForgeExpression spec, Set<GlobalVariable> modifies, ForgeConverter fconv) {
00275 ForgeCFG.Spec fs = ForgeCFG.specification(fconv.proc(), modifies, spec);
00276 ForgeSolver solver = new ForgeSolver(fs, fconv.forgeOptions());
00277 Options opts = fconv.javaScene().methodSpec().options();
00278 if (opts != null && opts.solveAll()) {
00279 return new ForgeEval(solver.runAll(fs, fconv.forgeBounds()), fconv);
00280 } else {
00281 return new ForgeEval(Collections.singleton(solver.run(fconv.forgeBounds())).iterator(), fconv);
00282 }
00283 }
00284
00285 }