00001
00005 package edu.mit.csail.sdg.squander.spec;
00006
00007 import java.util.HashMap;
00008 import java.util.HashSet;
00009 import java.util.Map;
00010 import java.util.Set;
00011
00012 import forge.program.ForgeExpression;
00013 import forge.program.ForgeVariable;
00014 import forge.program.GlobalVariable;
00015 import forge.program.LocalVariable;
00016 import forge.transform.ExpressionReplacer;
00017 import forge.util.ExpressionUtil;
00018
00027 public class Frame {
00028 private final ForgeScene forgeScene;
00029 private final Map<GlobalVariable, ForgeExpression> locations;
00030 private final Map<GlobalVariable, ForgeExpression> selectors;
00031 private final Map<GlobalVariable, ForgeExpression> lowerBounds;
00032 private final Map<GlobalVariable, ForgeExpression> upperBounds;
00033
00034 private Set<GlobalVariable> mods = null;
00035
00036 public Frame(ForgeScene scene) {
00037 this.forgeScene = scene;
00038 this.locations = new HashMap<GlobalVariable, ForgeExpression>();
00039 this.selectors = new HashMap<GlobalVariable, ForgeExpression>();
00040 this.lowerBounds = new HashMap<GlobalVariable, ForgeExpression>();
00041 this.upperBounds = new HashMap<GlobalVariable, ForgeExpression>();
00042 }
00043
00044 public Set<GlobalVariable> locations() {
00045 return locations.keySet();
00046 }
00047
00048 public ForgeExpression instSelector(GlobalVariable g) { return selectors.get(g); }
00049 public ForgeExpression lowerBound(GlobalVariable g) { return lowerBounds.get(g); }
00050 public ForgeExpression upperBound(GlobalVariable g) { return upperBounds.get(g); }
00051
00060 public void add(GlobalVariable var, ForgeExpression location, ForgeExpression sel, ForgeExpression lower, ForgeExpression upper) {
00061 assert var != null;
00062 assert location != null;
00063 assert var.arity() > 1 : "static global variables in frame are not yet supported";
00064
00065 final ForgeExpression heap = ExpressionUtil.bringGlobalsToPreState(location);
00066 if (locations.containsKey(var))
00067 locations.put(var, locations.get(var).union(heap));
00068 else
00069 locations.put(var, heap);
00070
00071 if (sel == null)
00072 sel = location;
00073 else
00074 sel = sel.intersection(location);
00075
00076 sel = ExpressionUtil.bringGlobalsToPreState(sel);
00077 if (selectors.containsKey(var))
00078 selectors.put(var, selectors.get(var).union(sel));
00079 else
00080 selectors.put(var, sel);
00081
00082 if (lower != null) {
00083 if (lowerBounds.containsKey(var))
00084 throw new RuntimeException("Can't add frame for the same variable twice");
00085 lower = ExpressionUtil.bringGlobalsToPreState(lower);
00086 lowerBounds.put(var, lower);
00087 }
00088
00089 if (upper != null) {
00090 if (upperBounds.containsKey(var))
00091 throw new RuntimeException("Can't add frame for the same variable twice");
00092 upper = ExpressionUtil.bringGlobalsToPreState(upper);
00093 upperBounds.put(var, upper);
00094 }
00095
00096
00097
00098
00099 for (final JField abs : forgeScene.fields(var)) {
00100 Frame frame = abs.getFrame();
00101 if (frame == null)
00102 continue;
00103 for (GlobalVariable dep : frame.locations.keySet()) {
00104 ForgeExpression depHeap = ExpressionUtil.bringGlobalsToPostState(frame.locations.get(dep));
00105 depHeap = depHeap.accept(new ExpressionReplacer() {
00106 @Override protected ForgeExpression visit(ForgeVariable expr) {
00107 ForgeExpression result = expr.equals(abs.getAbsFun().thisVar) ? heap : expr;
00108 super.putCache(expr, result);
00109 return result;
00110 }
00111 });
00112 add(dep, depHeap, null, null, null);
00113 }
00114 }
00115 }
00116
00126 public ForgeExpression condition() {
00127 ForgeExpression result = forgeScene.program().trueLiteral();
00128 Set<GlobalVariable> modifiable = modifiable();
00129 for (GlobalVariable var : forgeScene.program().globalVariables()) {
00130 if (var.arity() == 1) continue;
00131 LocalVariable quant = forgeScene.program().newLocalVariable(var.name() + "_mod", var.type().domain());
00132 if (!(modifiable.contains(var))) {
00133 result = result.and(quant.join(var).eq(quant.join(var.old())).forAll(quant));
00134 } else {
00135 ForgeExpression instSel = selectors.get(var);
00136 if (instSel != null)
00137 result = result.and(modCond(var, instSel, quant));
00138 }
00139 }
00140 return result;
00141 }
00142
00143 public ForgeExpression modCond() {
00144 ForgeExpression result = forgeScene.program().trueLiteral();
00145 for (GlobalVariable var : forgeScene.program().globalVariables()) {
00146 if (var.arity() == 1) continue;
00147 result = result.and(modCond(var));
00148 }
00149 return result;
00150 }
00151
00152 public ForgeExpression modCond(GlobalVariable var) {
00153 ForgeExpression result = forgeScene.program().trueLiteral();
00154 LocalVariable quant = forgeScene.program().newLocalVariable(var.name() + "_mod", var.type().domain());
00155 ForgeExpression instSel = selectors.get(var);
00156 if (instSel != null)
00157 result = result.and(modCond(var, instSel, quant));
00158 return result;
00159 }
00160
00161 public ForgeExpression lowerCond(GlobalVariable var) {
00162 ForgeExpression instSel = selectors.get(var);
00163 ForgeExpression lower = lowerBounds.get(var);
00164 if (instSel == null || lower == null)
00165 return null;
00166 return instSel.product(lower).in(var);
00167 }
00168
00169 public ForgeExpression upperCond(GlobalVariable var) {
00170
00171 ForgeExpression instSel = selectors.get(var);
00172 ForgeExpression upper = upperBounds.get(var);
00173 if (instSel == null || upper == null)
00174 return null;
00175 return var.in(instSel.product(upper));
00176
00177 }
00178
00179 private ForgeExpression modCond(GlobalVariable var, ForgeExpression instSel, LocalVariable l) {
00180 return l.in(instSel).not().implies(l.join(var).eq(l.join(var.old()))).forAll(l);
00181 }
00182
00188 public Set<GlobalVariable> modifiable() {
00189 if (mods == null) {
00190 mods = new HashSet<GlobalVariable>();
00191
00192 mods.addAll(locations.keySet());
00193 boolean changed = true;
00194 while (changed) {
00195 changed = false;
00196 l: for (GlobalVariable var : forgeScene.nonAbstractSpecFields()) {
00197 if (mods.contains(var)) {
00198
00199
00200
00201
00202
00203
00204
00205
00206
00207
00208
00209 } else {
00210
00211
00212 for (JField sf : forgeScene.fields(var)) {
00213 if (sf.getAbsFun() == null)
00214 continue;
00215 FrameInference fi = new FrameInference();
00216 sf.getAbsFun().expr.accept(fi);
00217 Set<GlobalVariable> vars = fi.globals();
00218 for (GlobalVariable v : vars) {
00219 if (mods.contains(v)) {
00220 changed = true;
00221 mods.add(var);
00222 continue l;
00223 }
00224 }
00225 }
00226 }
00227 }
00228 }
00229 }
00230 return mods;
00231 }
00232
00233 @Override
00234 public String toString() {
00235 StringBuilder sb = new StringBuilder();
00236 sb.append("modify");
00237 for (GlobalVariable var : modifiable()) sb.append(' ').append(var);
00238 sb.append(":").append("\n");
00239 sb.append(ExpressionUtil.prettyPrint(condition()));
00240 return sb.toString();
00241 }
00242
00243 }