00001
00005 package edu.mit.csail.sdg.squander.spec;
00006
00007 import java.util.ArrayList;
00008 import java.util.Collection;
00009 import java.util.HashSet;
00010 import java.util.List;
00011 import java.util.Set;
00012
00013 import edu.mit.csail.sdg.squander.spec.ClassSpec.Invariant;
00014 import edu.mit.csail.sdg.squander.spec.JType.Unary;
00015 import forge.program.ForgeExpression;
00016 import forge.program.ForgeProgram;
00017 import forge.program.ForgeType;
00018 import forge.program.ForgeVariable;
00019 import forge.program.GlobalVariable;
00020 import forge.program.LocalVariable;
00021 import forge.util.ExpressionUtil;
00022
00032 public final class Spec {
00033
00041 public final class SpecCase {
00042 private final ForgeExpression pre;
00043 private final ForgeExpression post;
00044 private final Frame frame;
00045 private final boolean helper;
00046
00047 private SpecCase(ForgeExpression requires, ForgeExpression ensures, Frame frame, boolean helper) {
00048 this.pre = ExpressionUtil.bringGlobalsToPostState(requires);
00049 this.post = ensures;
00050 this.frame = frame;
00051 this.helper = helper;
00052 }
00053
00054 public ForgeExpression preOnly() { return pre; }
00055 public ForgeExpression postOnly() { return post; }
00056 public ForgeExpression pre() { return pre; }
00057 public ForgeExpression post() { return helper ? post : post.and(invariant()); }
00058
00059 public Frame frame() { return frame; }
00060 public Spec spec() { return Spec.this; }
00061
00062 @Override
00063 public String toString() {
00064 StringBuilder sb = new StringBuilder();
00065 if (helper) sb.append("@Helper").append("\n");
00066 sb.append("@Requires:").append("\n").append(ExpressionUtil.prettyPrint(pre()));
00067 sb.append("@Ensures:").append("\n").append(ExpressionUtil.prettyPrint(post()));
00068 sb.append("@Modifies:").append("\n").append(frame);
00069 return sb.toString();
00070 }
00071 }
00072
00073 private static int fieldCounter = 0;
00074
00075 private final JavaScene javaScene;
00076 private final ForgeScene forgeScene;
00077 private final List<SpecCase> cases;
00078
00079
00080
00081
00082
00083 public Spec(JavaScene javaScene, ForgeScene forgeScene) {
00084 this.javaScene = javaScene;
00085 this.forgeScene = forgeScene;
00086 this.cases = new ArrayList<SpecCase>();
00087 }
00088
00089
00090
00091
00092
00093
00094 public JavaScene javaScene() { return javaScene; }
00095 public ForgeScene forgeScene() { return forgeScene; }
00096 public Collection<SpecCase> cases() { return cases; }
00097 public boolean isEmpty() { return cases.isEmpty(); }
00098
00099
00100
00101
00102
00103 public void addCase(ForgeExpression requires, ForgeExpression ensures, Frame frame, boolean helper) {
00104 assert requires != null && ensures != null && frame != null;
00105 cases.add(new SpecCase(requires, ensures, frame, helper));
00106 }
00107
00112
00113
00114
00115
00116
00117
00118
00119
00120
00121
00122
00123
00124
00125
00126
00127
00128
00129
00130
00131
00132
00133
00134
00135
00136
00137
00138
00139
00140
00141
00142
00143
00150 public ForgeExpression invariant() {
00151 ForgeProgram program = forgeScene.program();
00152 ForgeExpression result = program.trueLiteral();
00153 for (ClassSpec clsSpec : javaScene.classSpecs()) {
00154 if (clsSpec.isEmpty())
00155 continue;
00156 Class<?> clazz = clsSpec.clz();
00157 ForgeExpression invariant = program.trueLiteral();
00158 String varName = clazz.getSimpleName() + "0";
00159 ForgeType domain = forgeScene.typeForCls(clsSpec.jtype(), false);
00160 LocalVariable quant = program.newLocalVariable(varName, domain);
00161 for (Invariant inv : clsSpec.invariants()) {
00162 invariant = invariant.and(inv.replaceThis(quant));
00163 }
00164
00165 result = result.and(invariant.forAll(quant));
00166 }
00167 return result;
00168 }
00169
00172 public ForgeExpression wellformedPre(Set<GlobalVariable> modifiable) {
00173
00174 ForgeExpression contract = forgeScene.program().trueLiteral();
00175
00176 Set<ForgeVariable> singletons = new HashSet<ForgeVariable>();
00177 if (forgeScene.thisVar() != null) singletons.add(forgeScene.thisVar());
00178 for (LocalVariable arg : forgeScene.args())
00179 singletons.add(arg);
00180 for (ForgeVariable var : singletons)
00181 contract = contract.and(var.one());
00182
00183
00184 contract = contract.and(concreteConstraint(modifiable));
00185
00186 return contract;
00187 }
00188
00189
00193 public ForgeExpression wellformedPost(Set<GlobalVariable> modifiable) {
00194
00195 ForgeExpression contract = forgeScene.program().trueLiteral();
00196
00197 if (forgeScene.returnVar() != null) contract = contract.and(forgeScene.returnVar().one());
00198 if (forgeScene.throwVar() != null) contract = contract.and(forgeScene.throwVar().one());
00199
00200
00201 contract = contract.and(concreteConstraint(modifiable));
00202 return contract;
00203 }
00204
00208 public ForgeExpression concreteConstraint(Set<GlobalVariable> unmodifiable) {
00209 ForgeProgram program = forgeScene.program();
00210 ForgeExpression result = program.trueLiteral();
00211
00212
00213 for (ClassSpec clsSpec : javaScene.classSpecs()) {
00214 for (JField field : clsSpec.usedFields()) {
00215 if (field.isSpec())
00216 continue;
00217 if (unmodifiable.contains(forgeScene.global(field)))
00218 continue;
00219 result = result.and(fieldConstraint(field));
00220 }
00221 }
00222
00223 return result;
00224 }
00225
00226 public ForgeExpression abstractConstraint() {
00227 ForgeExpression result = forgeScene.program().trueLiteral();
00228 for (ClassSpec clsSpec : javaScene.classSpecs()) {
00229 for (JField field : clsSpec.usedFields()) {
00230 if (!field.isSpec() || field.isFunc())
00231 continue;
00232 result = result.and(fieldConstraint(field));
00233 }
00234 }
00235 return result;
00236 }
00237
00238 public ForgeExpression funcConstraint() {
00239 ForgeExpression result = forgeScene.program().trueLiteral();
00240 for (ClassSpec clsSpec : javaScene.classSpecs()) {
00241 for (JField field : clsSpec.usedFields()) {
00242 if (!field.isFunc())
00243 continue;
00244 result = result.and(fieldConstraint(field));
00245 }
00246 }
00247 return result;
00248 }
00249
00250 @Override
00251 public String toString() {
00252 StringBuilder sb = new StringBuilder();
00253 int i = 0;
00254 for (SpecCase cs : cases)
00255 sb.append("Case #" + ++i).append('\n').append(cs);
00256
00257 sb.append("\n");
00258 sb.append("Abstraction function:");
00259 sb.append("\n");
00260 sb.append(ExpressionUtil.prettyPrint(abstractConstraint()));
00261
00262 sb.append("\n");
00263 sb.append("Func function:");
00264 sb.append("\n");
00265 sb.append(ExpressionUtil.prettyPrint(funcConstraint()));
00266
00267 sb.append("\n");
00268 sb.append("Concrete constraint:");
00269 sb.append("\n");
00270 sb.append(ExpressionUtil.prettyPrint(concreteConstraint(new HashSet<GlobalVariable>())));
00271
00272 return sb.toString();
00273 }
00274
00275 private ForgeExpression fieldConstraint(JField field) {
00276 fieldCounter++;
00277 GlobalVariable var = forgeScene.global(field);
00278 ForgeProgram program = forgeScene.program();
00279 Unary ownerClz = field.owningType();
00280 Unary domClz = field.declaringType();
00281 if (field.isSpec()) {
00282 ForgeExpression condition = forgeScene.program().trueLiteral();
00283 {
00284 String name = "l_" + domClz.clazz().getSimpleName();
00285 LocalVariable x = program.newLocalVariable(name, forgeScene.typeForCls(domClz, false));
00286 condition = condition.and(field.getAbsFun().replaceThis(x).forAll(x));
00287 }
00288 {
00289 if (ownerClz == domClz) {
00290 String name = "l_" + ownerClz.clazz().getSimpleName();
00291 LocalVariable x = program.newLocalVariable(name, forgeScene.typeForCls(ownerClz, false));
00292 condition = condition.and(field.getBound().replaceThis(x).forAll(x));
00293 } else {
00294
00295 }
00296 }
00297 return condition;
00298 } else {
00299 if (field.isStatic())
00300 return var.one();
00301 else {
00302 String name = "l_" + domClz.clazz().getSimpleName();
00303 ForgeType domain = forgeScene.typeForCls(domClz, false);
00304 LocalVariable quant = forgeScene.program().newLocalVariable(name , domain);
00305 return quant.join(var).one().forAll(quant);
00306 }
00307 }
00308 }
00309
00310 }