00001
00005 package edu.mit.csail.sdg.squander.spec;
00006
00007 import java.util.ArrayList;
00008 import java.util.Collections;
00009 import java.util.HashMap;
00010 import java.util.List;
00011 import java.util.Map;
00012
00013 import edu.mit.csail.sdg.squander.annotations.Options;
00014 import edu.mit.csail.sdg.squander.spec.JType.Unary;
00015 import forge.program.ForgeExpression;
00016
00027 public class MethodSpec {
00028
00030 public class CaseSource {
00031 private Source preSrc;
00032 private Source pstSrc;
00033 private Source frmSrc;
00034 private boolean exceptional;
00035
00036 private ForgeExpression pre;
00037 private ForgeExpression pst;
00038 private Frame frm;
00039
00040 public Source preSrc() { return preSrc; }
00041 public Source postSrc() { return pstSrc; }
00042 public Source frameSrc() { return frmSrc; }
00043 public boolean exceptional() { return exceptional; }
00044
00045 public ForgeExpression pre() { return pre; }
00046 public ForgeExpression post() { return pst; }
00047 public Frame frame() { return frm; }
00048
00049 CaseSource(Source requires, Source ensures, Source modifies, boolean exceptional) {
00050 this.preSrc = requires;
00051 this.pstSrc = ensures;
00052 this.frmSrc = modifies;
00053 this.exceptional = exceptional;
00054 }
00055 }
00056
00057 private final List<CaseSource> cases;
00058 private final Map<String, CaseSource> pre2cs = new HashMap<String, CaseSource>();
00059 private final Map<JType.Unary, Integer> freshObj = new HashMap<JType.Unary, Integer>();
00060 private Options options;
00061
00062 private boolean helper;
00063 private boolean pure;
00064
00065 public Options options() { return options; }
00066 public boolean isHelper() { return helper; }
00067 public boolean isPure() { return pure; }
00068 public List<CaseSource> cases() { return Collections.unmodifiableList(cases); }
00069 public boolean isTrivial() { return !pure && cases.size() == 0; }
00070
00071 public Map<JType.Unary, Integer> freshObjects() { return freshObj; }
00072
00073 MethodSpec() {
00074 this.cases = new ArrayList<CaseSource>();
00075 this.helper = false;
00076 this.pure = false;
00077 }
00078
00079 public void typecheck(JavaScene javaScene) {
00080 TypeChecker checker = new TypeChecker(javaScene);
00081 for (CaseSource cs : cases) {
00082 cs.preSrc().typecheck(checker);
00083 cs.postSrc().typecheck(checker);
00084 cs.frameSrc().typecheck(checker);
00085 }
00086 }
00087
00088 public void translateSpecs(ForgeEnv env, ForgeScene forgeScene) {
00089 Tr tr = new Tr();
00090 for (CaseSource cs : cases) {
00091 cs.pre = cs.preSrc().translate(tr, env);
00092 cs.pst = cs.postSrc().translate(tr, env);
00093 cs.frm = new Frame(forgeScene);
00094 Tr.FrameConstructor fc = new Tr.FrameConstructor(cs.frm, forgeScene);
00095 cs.frameSrc().translate(fc, env);
00096 }
00097 }
00098
00099 public void addOptions(Options opt) {
00100 this.options = opt;
00101 }
00102
00103 void addFreshObj(Class<?> cls, Class<?>[] typeParams, int num) {
00104 Unary newJType;
00105 if (typeParams == null || typeParams.length == 0) {
00106 newJType = JType.Factory.instance.newJType(cls);
00107 } else {
00108 newJType = JType.Factory.instance.newJType(cls, typeParams);
00109 }
00110 freshObj.put(newJType, num);
00111
00112 }
00113
00114 void addCase(Source requires, Source ensures, Source modifies, boolean exceptional) {
00115
00116 CaseSource cs = pre2cs.get(requires.source);
00117 if (cs == null) {
00118 cs = new CaseSource(requires, ensures, modifies, exceptional);
00119 cases.add(cs);
00120 pre2cs.put(requires.source, cs);
00121 } else {
00122 cases.remove(cs);
00123 String post = String.format("(%s) && (%s)", cs.postSrc().source, ensures.source);
00124 Source newEnsures = new Source(post, ensures.ns, ensures.rule);
00125 String mod;
00126 if (cs.frmSrc.source.length() == 0)
00127 mod = ensures.source;
00128 else if (ensures.source.length() == 0)
00129 mod = cs.frmSrc.source;
00130 else
00131 mod = String.format("%s, %s", cs.frmSrc.source, modifies.source);
00132 Source newModifies = new Source(mod, modifies.ns, modifies.rule);
00133 boolean newExceptional = cs.exceptional || exceptional;
00134 CaseSource newCs = new CaseSource(requires, newEnsures, newModifies, newExceptional);
00135 cases.add(newCs);
00136 pre2cs.put(requires.source, newCs);
00137 }
00138 }
00139
00140 void mergeCasesWith(MethodSpec ms) {
00141 for (CaseSource c : ms.cases)
00142 cases.add(c);
00143 }
00144
00145 void makeHelper() {
00146 helper = true;
00147 }
00148
00149 void makePure() {
00150 pure = true;
00151 }
00152
00153 }