00001
00005 package edu.mit.csail.sdg.squander.spec;
00006
00007 import java.util.ArrayList;
00008 import java.util.Collection;
00009 import java.util.HashMap;
00010 import java.util.HashSet;
00011 import java.util.IdentityHashMap;
00012 import java.util.LinkedList;
00013 import java.util.List;
00014 import java.util.Map;
00015 import java.util.Set;
00016 import java.util.Map.Entry;
00017
00018 import edu.mit.csail.sdg.squander.spec.JType.Factory;
00019 import edu.mit.csail.sdg.squander.spec.JType.Unary;
00020 import edu.mit.csail.sdg.squander.utils.ReflectionUtils;
00021
00022
00023
00024 @SuppressWarnings("unchecked")
00025 public class JavaScene {
00026
00027 private Map<JType.Unary, ClassSpec> classes = new HashMap<JType.Unary, ClassSpec>();
00028 private Map<Object, ClassSpec> obj2spec = new IdentityHashMap<Object, ClassSpec>();
00029
00030 private JMethod method;
00031 private Object caller;
00032 private Object[] methodArgs = new Object[0];
00033
00034 private boolean finished = false;
00035
00036 public boolean isFinished() { return finished; }
00037
00038 public void addObj2spec(Object object, ClassSpec cs) { obj2spec.put(object, cs); }
00039
00040 public ClassSpec ensureClass(Class<?> cls) {
00041 return ensureClass(Factory.instance.newJType(cls));
00042 }
00043
00044 public ClassSpec ensureClass(JType.Unary type) {
00045 ClassSpec clzSpec = classes.get(type);
00046 if (clzSpec == null) {
00047
00048 clzSpec = createClassSpec(type);
00049 classes.put(type, clzSpec);
00050
00051 clzSpec.typecheck();
00052
00053 Class<?> clz = type.clazz();
00054 for (Class<?> cls : ReflectionUtils.getImmParents(clz)) {
00055 JType.Unary superType = Factory.instance.newJType(cls, type.typeParams());
00056 ClassSpec superClzSpec = ensureClass(superType);
00057 clzSpec.addSuper(superClzSpec);
00058 }
00059 }
00060 return clzSpec;
00061 }
00062
00063 public void finish() {
00064 assert !finished : "don't call finish() more than once";
00065
00066 while (true) {
00067 Collection<ClassSpec> toVisit = new ArrayList<ClassSpec>(classSpecs());
00068 for (ClassSpec cs : toVisit) {
00069 for (JField jf : cs.usedFieldsAll()) {
00070 if (jf.declaringType().clazz() == cs.clz())
00071 continue;
00072 cs.ensureField(jf.name(), false);
00073 }
00074 }
00075 if (toVisit.size() == classSpecs().size())
00076 break;
00077 }
00078 finished = true;
00079 }
00080
00081
00082
00083
00084
00085
00086
00087
00088
00089
00090
00091
00092
00093
00094
00095
00096
00097
00098 public void setMethod(JMethod method) {
00099 this.method = method;
00100 method.spec().typecheck(this);
00101 }
00102
00103 public void setArgs(Object[] methodArgs) {
00104 if (methodArgs == null)
00105 this.methodArgs = new Object[0];
00106 else
00107 this.methodArgs = methodArgs;
00108 }
00109
00110 public JMethod method() { return method; }
00111 public MethodSpec methodSpec() { return method.spec(); }
00112 public Collection<ClassSpec> classSpecs() { return classes.values(); }
00113
00114
00115
00116
00117
00118
00119
00120
00121
00122 public Collection<Class<?>> classes() {
00123 Set<Class<?>> classes = new HashSet<Class<?>>();
00124 for (JType.Unary jtype : this.classes.keySet()) {
00125 classes.add(jtype.clazz());
00126 }
00127 return classes;
00128 }
00129 public List<JType.Unary> jtypes(Class<?> cls) {
00130 List<JType.Unary> result = new LinkedList<Unary>();
00131 for (JType.Unary t : classes.keySet()) {
00132 if (t.clazz() == cls)
00133 result.add(t);
00134 }
00135 return result;
00136 }
00137
00138 public ClassSpec classSpecForObj(Object o) { return obj2spec.get(o); }
00139 public JType.Unary jtypeForObj(Object o) { return obj2spec.get(o).jtype(); }
00140 public ClassSpec classSpec(Unary jtype) { return classes.get(jtype); }
00141 public ClassSpec findSpec(Class cls, boolean ensureSingle) {
00142 ClassSpec result = null;
00143 for (Entry<Unary, ClassSpec> e : classes.entrySet()) {
00144 if (e.getKey().clazz() == cls) {
00145 if (ensureSingle)
00146 if (result != null)
00147 throw new RuntimeException("Multiple specs found for class " + cls.getName());
00148 result = e.getValue();
00149 }
00150 }
00151 return result;
00152 }
00153 public void setCaller(Object caller) { this.caller = caller; }
00154 public Object caller() { return caller; }
00155 public Object[] methodArgs() { return methodArgs; }
00156
00157 public Collection<JField> specFields() {
00158 List<JField> specFields = new ArrayList<JField>();
00159 for (ClassSpec clsSpec : classSpecs()) {
00160 for (JField fld : clsSpec.usedFields())
00161 if (fld.isSpec())
00162 specFields.add(fld);
00163 }
00164 return specFields;
00165 }
00166
00167 public Collection<ClassSpec> subTypes(JType.Unary jtype) {
00168 return subTypes(classSpec(jtype));
00169 }
00170
00171 public Collection<ClassSpec> subTypes(Class<?> cls) {
00172 return subTypes(findSpec(cls, false));
00173 }
00174
00175 private Collection<ClassSpec> subTypes(ClassSpec clsSpec) {
00176 assert clsSpec != null : "clsSpec is null";
00177 if (((Class<?>) clsSpec.clz()).isArray())
00178 return new ArrayList<ClassSpec>(0);
00179 Collection<ClassSpec> subs = clsSpec.subs();
00180 if (subs == null) {
00181 subs = new LinkedList<ClassSpec>();
00182 for (ClassSpec cs : classes.values()) {
00183 if (cs == clsSpec)
00184 continue;
00185 if (clsSpec.jtype().isAssignableFrom(cs.jtype()))
00186 subs.add(cs);
00187 }
00188 clsSpec.setSubs(subs);
00189 }
00190 return subs;
00191 }
00192
00193 public void translateSpecs(ForgeScene forgeScene) {
00194 assert finished : "call finish() first";
00195 for (ClassSpec clsSpec : classSpecs()) {
00196 if (clsSpec.isEmpty())
00197 continue;
00198 clsSpec.translateSpecs(forgeScene);
00199 }
00200 if (method != null) {
00201 ForgeEnv env = forgeScene.getEnv(forgeScene.thisVar());
00202 method.spec().translateSpecs(env, forgeScene);
00203 }
00204 }
00205
00206 private ClassSpec createClassSpec(JType.Unary jtype) {
00207
00208
00209 ClassSpec clzSpec = new ClassSpec(jtype, this);
00210 ISpecProvider isp = new CompositeSpecProvider(
00211 new SpecFileSpecProvider(), new ReflectiveSpecProvider());
00212 List<Source> clsSpec = isp.extractClassSpec(jtype);
00213 for (Source src : clsSpec) {
00214 src.parse();
00215 if (src.isClause()) {
00216 clzSpec.addInvariant(src);
00217 } else if (src.isDecl()) {
00218 clzSpec.addSpecFieldSource(src);
00219 } else
00220 throw new RuntimeException("invalid class spec: " + src);
00221 }
00222 return clzSpec;
00223 }
00224
00225 }