00001
00005 package edu.mit.csail.sdg.squander.engine.kk;
00006
00007 import java.util.ArrayList;
00008 import java.util.HashMap;
00009 import java.util.Iterator;
00010 import java.util.LinkedList;
00011 import java.util.List;
00012 import java.util.Set;
00013 import java.util.Map.Entry;
00014
00015 import kodkod.ast.Expression;
00016 import kodkod.ast.Formula;
00017 import kodkod.ast.IntConstant;
00018 import kodkod.ast.IntExpression;
00019 import kodkod.ast.Relation;
00020 import kodkod.ast.Variable;
00021 import kodkod.engine.Solution;
00022 import kodkod.instance.Bounds;
00023 import kodkod.instance.TupleFactory;
00024 import kodkod.instance.TupleSet;
00025 import kodkod.instance.Universe;
00026 import edu.mit.csail.sdg.squander.absstate.ObjTuple;
00027 import edu.mit.csail.sdg.squander.absstate.ObjTupleSet;
00028 import edu.mit.csail.sdg.squander.engine.ForgeConverter;
00029 import edu.mit.csail.sdg.squander.engine.ISquander;
00030 import edu.mit.csail.sdg.squander.engine.SquanderEval2;
00031 import edu.mit.csail.sdg.squander.engine.ISquanderResult.IEvaluator;
00032 import edu.mit.csail.sdg.squander.log.Log;
00033 import edu.mit.csail.sdg.squander.spec.Spec.SpecCase;
00034 import forge.program.ForgeExpression;
00035 import forge.program.ForgeLiteral;
00036 import forge.program.ForgeType;
00037 import forge.program.ForgeVariable;
00038 import forge.program.GlobalVariable;
00039 import forge.program.InstanceLiteral;
00040 import forge.program.LocalVariable;
00041 import forge.program.ForgeType.Unary;
00042
00049 public class SquanderKodkod2Impl extends SquanderKodkodImpl {
00050
00051 static class FldRelElem {
00052 InstanceLiteral l;
00053 GlobalVariable g;
00054 Relation rel;
00055 Relation rel_pre;
00056
00057 FldRelElem(InstanceLiteral l, GlobalVariable g, Relation rel, Relation rel_pre) {
00058 this.l = l;
00059 this.g = g;
00060 this.rel = rel;
00061 this.rel_pre = rel_pre;
00062 }
00063
00064 Relation preRel() { return rel_pre != null ? rel_pre : rel; }
00065 Relation postRel() { return rel; }
00066 boolean isMod() { return rel_pre != null; }
00067
00068 }
00069
00070
00071
00072 private HashMap<String, FldRelElem> fldRels;
00073
00074 public SquanderKodkod2Impl() { }
00075
00076 @Override
00077 protected Set<GlobalVariable> getModsForPostState(ForgeConverter fconv, SpecCase sc) {
00078 return sc.frame().modifiable();
00079 }
00080
00081 @Override
00082 protected ForgeExpression getPreSpec(SpecCase cs) {
00083 this.cs = cs;
00084 return cs.pre().and(cs.spec().abstractConstraint());
00085 }
00086
00087 @Override
00088 protected ForgeExpression getPostSpec(SpecCase cs, ForgeConverter fconv) {
00089 this.cs = cs;
00090 return cs.spec().abstractConstraint()
00091 .and(cs.spec().funcConstraint())
00092 .and(cs.post());
00093 }
00094
00095 @Override
00096 protected Formula convertSpec(ForgeExpression spec) {
00097 Formula f = super.convertSpec(spec);
00098 f = f.and(wellformed());
00099 return f;
00100 }
00101
00102 @Override
00103 protected IEvaluator getEval(Iterator<Solution> solutions) {
00104 return new KodkodEval(solutions);
00105 }
00106
00107 @Override
00108 protected void init() {
00109 super.init();
00110 fldRels = new HashMap<String, FldRelElem>();
00111 }
00112
00113 private Formula wellformed() {
00114 Formula f = Formula.TRUE;
00115 for (FldRelElem fre : fldRels.values()) {
00116 if (!modifies.contains(fre.g))
00117 continue;
00118 if (forgeScene.isSpecField(fre.g))
00119 continue;
00120 String varName = fre.g.name();
00121 if (varName.endsWith("[].elems"))
00122 f = f.and(arrElemsConstr(fre));
00123 else if (varName.endsWith("[].length"))
00124 f = f.and(arrLenConstr(fre));
00125 else
00126 f = f.and(one(fre.postRel()));
00127 }
00128
00129 if (forgeScene.returnVar() != null)
00130 f = f.and(one(var2rel.get(relName(forgeScene.returnVar()))));
00131 return f;
00132 }
00133
00134 private Formula one(Expression rel) {
00135 return rel.one();
00136 }
00137
00138 private Formula arrLenConstr(FldRelElem fre) {
00139 Relation postRel = fre.postRel();
00140 return one(postRel).and(postRel.sum().gte(IntConstant.constant(0)));
00141 }
00142
00143 private Formula arrElemsConstr(FldRelElem fre) {
00144 Relation postRel = fre.postRel();
00145 String lenVarName = postRel.name().replace("[].elems", "[].length");
00146 Relation lenRel = fldRels.get(lenVarName).postRel();
00147 Variable idxVar = Variable.unary("i");
00148 IntExpression idx = idxVar.sum();
00149 IntExpression len = lenRel.sum();
00150 Formula cond = idx.lt(len).and(idx.gte(IntConstant.constant(0)));
00151 Formula thenCond = one(idxVar.join(postRel));
00152 Formula elseCond = idxVar.join(postRel).no();
00153 return cond.implies(thenCond).and(cond.not().implies(elseCond)).forAll(idxVar.oneOf(intsExpr()));
00154 }
00155
00156 private Expression intsExpr() {
00157 return Expression.INTS;
00158 }
00159
00160 @Override
00161 protected void createRelations() {
00162
00163
00164 List<ForgeLiteral> literals = new LinkedList<ForgeLiteral>();
00165 literals.addAll(program.instanceLiterals());
00166 literals.add(program.trueLiteral());
00167 literals.add(program.falseLiteral());
00168 for (ForgeLiteral lit : literals) {
00169 Relation rel = Relation.unary(lit.name());
00170 lit2rel.put(lit.name(), rel);
00171 Expression domType = type2expr.get(lit.type());
00172 if (domType == null)
00173 domType = rel;
00174 else
00175 domType = domType.union(rel);
00176 type2expr.put(lit.type(), domType);
00177 }
00178 this.trueRelation = lit2rel.get(program.trueLiteral().name());
00179 this.falseRelation = lit2rel.get(program.falseLiteral().name());
00180
00181
00182 for (GlobalVariable g : program.globalVariables()) {
00183 if (forgeScene.isConst(g))
00184 continue;
00185 ForgeExpression expr = cs.frame().instSelector(g);
00186 List<InstanceLiteral> modLits = new LinkedList<InstanceLiteral>();
00187 if (modifies.contains(g))
00188 modLits = getModLits(g, expr);
00189 ForgeType t = g.type();
00190 assert t.arity() >= 2 : "static fields not supported yet";
00191 ForgeType colType = t.projectType(0);
00192 List<InstanceLiteral> instLiterals = fconv.findInstLiteralsForType((Unary) colType);
00193 if (instLiterals.isEmpty()) {
00194 Expression emptyRel = Relation.NONE;
00195 for (int i = 1; i < g.arity(); i++)
00196 emptyRel = emptyRel.product(Relation.NONE);
00197 addRelForVar(relName(g), emptyRel);
00198 } else {
00199 for (InstanceLiteral l : instLiterals) {
00200 addFldRel(l, g, modLits);
00201 }
00202 }
00203 }
00204
00205
00206 if (forgeScene.thisVar() != null)
00207 addRelForVar(forgeScene.thisVar(), relName(forgeScene.thisVar()));
00208 for (LocalVariable var : forgeScene.args())
00209 addRelForVar(var, relName(var));
00210 if (forgeScene.returnVar() != null)
00211 addRelForVar(forgeScene.returnVar(), relName(forgeScene.returnVar()));
00212
00213 for (GlobalVariable g : forgeScene.consts()) {
00214 addRelForVar(g, g.name());
00215 }
00216 }
00217
00218 private List<InstanceLiteral> getModLits(GlobalVariable g, ForgeExpression expr) {
00219 if (expr == null)
00220 return fconv.findInstLiteralsForType((Unary) g.type().projectType(0));
00221 try {
00222 SquanderEval2 se = new SquanderEval2();
00223 ObjTupleSet fc = se.eval(expr, fconv);
00224 List<InstanceLiteral> lits = new ArrayList<InstanceLiteral>();
00225 for (ObjTuple t : fc.tuples()) {
00226 if (t.arity() == 1) {
00227 InstanceLiteral l = forgeScene.instLitForObj(t.get(0));
00228 if (l != null)
00229 lits.add(l);
00230 }
00231 }
00232 return lits;
00233 } catch (Throwable t) {
00234 Log.warn("could not evaluate: " + expr + ". Reason: " + t.getMessage());
00235 return fconv.findInstLiteralsForType((Unary) g.type().projectType(0));
00236 }
00237 }
00238
00239
00240
00241 protected void addRelForVar(ForgeVariable var, String name) {
00242 addRelForVar(name, Relation.nary(name, var.arity()));
00243 }
00244
00245 private void addRelForVar(String name, Expression expr) {
00246 Expression varRel = var2rel.get(name);
00247 if (varRel == null)
00248 varRel = expr;
00249 else
00250 varRel = varRel.union(expr);
00251 var2rel.put(name, varRel);
00252 }
00253
00254 private void addFldRel(InstanceLiteral l, GlobalVariable g, List<InstanceLiteral> modLits) {
00255 String varName = relName(g);
00256 String name = l.name() + "_" + varName;
00257 Relation rel = Relation.nary(name, g.arity() - 1);
00258 Relation rel_pre = null;
00259 if (modLits.contains(l))
00260 rel_pre = Relation.nary(name + "_pre", g.arity() - 1);
00261 FldRelElem fre = new FldRelElem(l, g, rel, rel_pre);
00262 fldRels.put(rel.name(), fre);
00263 addRelForVar(varName, lit2rel.get(l.name()).product(rel));
00264 if (modifies.contains(g))
00265 addRelForVar(varName + "_pre", lit2rel.get(l.name()).product(fre.preRel()));
00266 }
00267
00268 private List<FldRelElem> findFldRelsForVar(GlobalVariable var) {
00269 List<FldRelElem> l = new LinkedList<FldRelElem>();
00270 for (FldRelElem e : fldRels.values()) {
00271 if (e.g == var)
00272 l.add(e);
00273 }
00274 return l;
00275 }
00276
00277 @Override
00278 protected Bounds createBounds() {
00279 Universe univ = createUniverse();
00280 TupleFactory f = univ.factory();
00281 Bounds b = new Bounds(univ);
00282
00283
00284 for (Entry<String, Relation> e : lit2rel.entrySet()) {
00285 b.boundExactly(e.getValue(), f.setOf(e.getKey()));
00286 }
00287
00288
00289 for (GlobalVariable var : program.globalVariables()) {
00290 ObjTupleSet[] lowup = getBounds(var);
00291 if (forgeScene.isConst(var)) {
00292 Expression rel = var2rel.get(relName(var));
00293 b.boundExactly((Relation)rel, conv2tuples(lowup[0], f));
00294 } else {
00295 List<FldRelElem> fldRelsForVar = findFldRelsForVar(var);
00296 if (!fldRelsForVar.isEmpty()) {
00297 for (FldRelElem fldRelElem : fldRelsForVar) {
00298 Object atom = fconv.lit2obj(fldRelElem.l);
00299 ObjTupleSet ots = ObjTupleSet.singleTuple(atom);
00300 TupleSet lowerTupleSet = conv2tuples(ots.join(lowup[0]), f);
00301 TupleSet upperTupleSet = conv2tuples(ots.join(lowup[1]), f);
00302 b.bound(fldRelElem.preRel(), lowerTupleSet, upperTupleSet);
00303 if (fldRelElem.isMod()) {
00304 b.bound(fldRelElem.postRel(), conv2tuples(ots.join(getExtent(var)), f));
00305 }
00306 }
00307 }
00308 }
00309 }
00310
00311
00312 boundLocalVar(forgeScene.thisVar(), f, b);
00313 for (LocalVariable var : forgeScene.args())
00314 boundLocalVar(var, f, b);
00315 boundLocalVar(forgeScene.returnVar(), f, b);
00316
00317
00318 for (Integer i : ints) {
00319 b.boundExactly(i, f.setOf(i));
00320 }
00321
00322 return b;
00323 }
00324
00325 protected void boundLocalVar(LocalVariable var, TupleFactory f, Bounds b) {
00326 if (var == null)
00327 return;
00328 ObjTupleSet[] lowup = getBounds(var);
00329 TupleSet lowerBound = conv2tuples(lowup[0], f);
00330 TupleSet upperBound = conv2tuples(lowup[1], f);
00331 Relation rel = (Relation) var2rel.get(relName(var));
00332 b.bound(rel, lowerBound, upperBound);
00333 }
00334
00335 private ObjTupleSet[] getBounds(ForgeVariable var) {
00336 ObjTupleSet[] result = new ObjTupleSet[2];
00337 ObjTupleSet bnd = fconv.heap2Lit().bounds().get(var.name());
00338 ObjTupleSet lowerTupleSet;
00339 ObjTupleSet upperTupleSet;
00340 if (bnd != null) {
00341 lowerTupleSet = bnd;
00342 upperTupleSet = lowerTupleSet;
00343 } else {
00344 lowerTupleSet = new ObjTupleSet(var.arity());
00345 upperTupleSet = getExtent(var);
00346 }
00347 result[0] = lowerTupleSet;
00348 result[1] = upperTupleSet;
00349 return result;
00350 }
00351
00352 private ObjTupleSet getExtent(ForgeVariable var) {
00353
00354 ForgeType t = var.type();
00355 ObjTupleSet result = null;
00356 for (int i = 0; i < t.arity(); i++) {
00357 ForgeType.Unary colType = (Unary) t.projectType(i);
00358 ObjTupleSet tuple = new ObjTupleSet(1);
00359 for (ForgeLiteral lit : fconv.findLiteralsForType(colType)) {
00360 tuple.add(new ObjTuple(fconv.lit2obj(lit)));
00361 }
00362 if (result == null)
00363 result = tuple;
00364 else
00365 result = result.product(tuple);
00366 }
00367 if (result == null)
00368 result = new ObjTupleSet(var.arity());
00369 return result;
00370 }
00371
00372 }