00001
00005 package edu.mit.csail.sdg.squander.spec;
00006
00007 import java.lang.reflect.Field;
00008 import java.util.ArrayList;
00009 import java.util.Collection;
00010 import java.util.HashMap;
00011 import java.util.LinkedList;
00012 import java.util.List;
00013 import java.util.Map;
00014 import java.util.Map.Entry;
00015
00016
00017 import edu.mit.csail.sdg.squander.spec.JType.Factory;
00018 import edu.mit.csail.sdg.squander.utils.ReflectionUtils;
00019 import forge.program.ForgeExpression;
00020 import forge.program.LocalVariable;
00021 import forge.util.ExpressionUtil;
00022
00023 @SuppressWarnings("unchecked")
00024 public class ClassSpec {
00025
00026 public static class Invariant {
00027 public final ForgeExpression expr;
00028 public final LocalVariable thisVar;
00029
00030 public Invariant(ForgeExpression expr, LocalVariable thisVar) {
00031 this.expr = expr;
00032 this.thisVar = thisVar;
00033 }
00034
00035 public ForgeExpression replaceThis(LocalVariable replacement) {
00036 return ExpressionUtil.replaceVariable(expr, thisVar, replacement);
00037 }
00038 }
00039
00040
00041
00042
00043
00044 private final JType.Unary jtype;
00045 private final JavaScene javaScene;
00046
00047 private Collection<ClassSpec> subs;
00048 private List<ClassSpec> supers = new LinkedList<ClassSpec>();
00049
00050 private Map<String, Source> specFieldSources = new HashMap<String, Source>();
00051 private List<Source> invariantSources = new ArrayList<Source>();
00052 private List<Invariant> invariants = new ArrayList<Invariant>();
00053
00054 private Map<String, JField> usedFields = new HashMap<String, JField>();
00055
00056 public ClassSpec(JType.Unary jtype, JavaScene javaScene) {
00057 this.jtype = jtype;
00058 this.javaScene = javaScene;
00059 }
00060
00061 public ClassSpec(Class clz, JType.Unary[] typeParams, JavaScene javaScene) {
00062 this(Factory.instance.newJType(clz, typeParams), javaScene);
00063 }
00064
00065 public boolean isEmpty() {
00066 return invariantSources.isEmpty() && specFieldSources.isEmpty();
00067 }
00068
00069 public JType.Unary jtype() { return jtype; }
00070 public Class clz() { return jtype.clazz(); }
00071 public JType.Unary[] typeParams() { return jtype.typeParams(); }
00072
00073 public Collection<ClassSpec> subs() { return subs; }
00074 public void setSubs(Collection<ClassSpec> subs) { this.subs = subs; }
00075
00076 public void addSuper(ClassSpec superClsSpec) { supers.add(superClsSpec); }
00077
00078 public JField findField(String name) {
00079 JField jf = usedFields.get(name);
00080 if (jf != null)
00081 return jf;
00082 for (ClassSpec scs : supers) {
00083 jf = scs.findField(name);
00084 if (jf != null) {
00085 return jf;
00086 }
00087 }
00088 return null;
00089 }
00090
00091 public JField ensureField(String name) {
00092 return ensureField(name, true);
00093 }
00094
00095
00096 public JField ensureField(String name, boolean recurse) {
00097 assert !javaScene.isFinished();
00098
00099 JField jf = usedFields.get(name);
00100 if (jf != null)
00101 return jf;
00102
00103
00104 Source specSource = specFieldSources.get(name);
00105 if (specSource != null) {
00106 TypeChecker checker = new TypeChecker(javaScene);
00107 checker.setClsSpecForSpecField(this);
00108 specSource.typecheck(checker);
00109 JField f = usedFields.get(name);
00110 assert f != null;
00111 if (specSource.isFuncField())
00112 f.setFuncFlag(true);
00113 return f;
00114 }
00115
00116
00117 Field f = ReflectionUtils.getField(jtype.clazz(), name);
00118 if (f != null) {
00119 jf = JField.newJavaField(f);
00120 addUsedField(jf);
00121
00122 ISpecProvider rsp = new ReflectiveSpecProvider();
00123 TypeChecker checker = new TypeChecker(javaScene);
00124 for (Source src : rsp.extractFieldSpec(f, jtype)) {
00125 addInvariant(src);
00126 src.typecheck(checker);
00127 }
00128 return jf;
00129 }
00130
00131
00132 if (recurse) {
00133 for (ClassSpec scs : supers) {
00134 jf = scs.ensureField(name);
00135 if (jf != null) {
00136 return jf;
00137 }
00138 }
00139 }
00140 return null;
00141 }
00142
00143 public Collection<Invariant> invariants() { return invariants; }
00144 public Collection<Source> specFields() { return specFieldSources.values(); }
00145 public boolean hasSpecField(String name) { return specFieldSources.containsKey(name); }
00146 public Collection<JField> usedFields() { return usedFields.values(); }
00147 public Collection<JField> usedFieldsAll() {
00148 Map<String, JField> result = new HashMap<String, JField>();
00149 result.putAll(usedFields);
00150 for (ClassSpec cs : supers) {
00151 for (JField f : cs.usedFieldsAll())
00152 if (!result.containsKey(f.name()))
00153 result.put(f.name(), f);
00154 }
00155 return result.values();
00156 }
00157
00158 public void addInvariant(Source src) {
00159 assert !javaScene.isFinished();
00160 invariantSources.add(src);
00161 }
00162
00163 public void addSpecFieldSource(Source src) {
00164 assert !javaScene.isFinished() : "can't add spec field after calling finish(): " + src;
00165 specFieldSources.put(extractSpecFieldName(src), src);
00166 }
00167
00168 public void addSpecField(JField field) {
00169 assert !javaScene.isFinished();
00170 assert field.isSpec();
00171 addUsedField(field);
00172 }
00173
00177 public void typecheck() {
00178 TypeChecker checker = new TypeChecker(javaScene);
00179
00180 ArrayList<Source> invSrcs = new ArrayList<Source>(invariantSources);
00181 for (Source s : invSrcs)
00182 s.typecheck(checker);
00183 }
00184
00185 public void translateSpecs(ForgeScene forgeScene) {
00186 LocalVariable thisVar = forgeScene.newThisVariable(jtype());
00187 ForgeEnv env = forgeScene.getEnv(thisVar);
00188 Tr tr = new Tr();
00189 Tr.SpecFieldTranslator funTr = new Tr.SpecFieldTranslator();
00190 for (Entry<String, JField> e : usedFields.entrySet()) {
00191 if (!e.getValue().isSpec())
00192 continue;
00193 Source s = specFieldSources.get(e.getKey());
00194 JField field = e.getValue();
00195 Tr.SpecFieldBoundTranslator boundTr = new Tr.SpecFieldBoundTranslator(field);
00196 field.setDomain(s.translate(tr, env));
00197 field.setAbsFun(new Invariant(s.translate(funTr, env), env.thisVar()));
00198 field.setBound(new Invariant(s.translate(boundTr, env), env.thisVar()));
00199 Frame frame = new Frame(forgeScene);
00200 Tr.FrameConstructor frameTr = new Tr.FrameConstructor(frame, forgeScene);
00201 s.translate(frameTr, env);
00202 if (frame.locations().size() > 0)
00203 field.setFrame(frame);
00204 }
00205 for (Source s : invariantSources) {
00206 ForgeExpression expr = s.translate(tr, env);
00207 Invariant inv = new Invariant(expr, env.thisVar());
00208 invariants.add(inv);
00209 }
00210 }
00211
00212 @Override
00213 public String toString() {
00214 StringBuilder sb = new StringBuilder();
00215 sb.append(jtype);
00216 for (JField jf : usedFields.values())
00217 sb.append("\n ").append(jf.name());
00218 return sb.toString();
00219 }
00220
00221 private void addUsedField(JField field) {
00222 usedFields.put(field.name(), field);
00223 }
00224
00225 private String extractSpecFieldName(Source src) {
00226
00227 return src.source.substring(0, src.source.indexOf(":")).trim();
00228 }
00229
00230 }