00001
00005 package edu.mit.csail.sdg.squander.spec;
00006
00007 import java.lang.annotation.Annotation;
00008 import java.lang.reflect.Field;
00009 import java.lang.reflect.Method;
00010 import java.lang.reflect.Modifier;
00011 import java.util.ArrayList;
00012 import java.util.Collection;
00013 import java.util.LinkedHashSet;
00014 import java.util.List;
00015 import java.util.Set;
00016
00017 import edu.mit.csail.sdg.annotations.Case;
00018 import edu.mit.csail.sdg.annotations.Effects;
00019 import edu.mit.csail.sdg.annotations.Ensures;
00020 import edu.mit.csail.sdg.annotations.FuncField;
00021 import edu.mit.csail.sdg.annotations.Helper;
00022 import edu.mit.csail.sdg.annotations.Invariant;
00023 import edu.mit.csail.sdg.annotations.Modifies;
00024 import edu.mit.csail.sdg.annotations.NonNull;
00025 import edu.mit.csail.sdg.annotations.Pure;
00026 import edu.mit.csail.sdg.annotations.Requires;
00027 import edu.mit.csail.sdg.annotations.Returns;
00028 import edu.mit.csail.sdg.annotations.SpecField;
00029 import edu.mit.csail.sdg.annotations.Specification;
00030 import edu.mit.csail.sdg.annotations.Throws;
00031 import edu.mit.csail.sdg.squander.annotations.Fresh;
00032 import edu.mit.csail.sdg.squander.annotations.FreshObjects;
00033 import edu.mit.csail.sdg.squander.annotations.Options;
00034 import edu.mit.csail.sdg.squander.spec.Source.Rule;
00035 import edu.mit.csail.sdg.squander.utils.ReflectionUtils;
00036
00037
00038 public class ReflectiveSpecProvider implements ISpecProvider {
00039
00040 private final String TYPE_EXCEPTIONAL = "EXCEPTIONAL";
00041
00042
00043 private final String CLAUSE_DEFAULT = "true";
00044 private final String RETURNS_FORMAT = "return = (%s)";
00045 private final String NONNULL_FORMAT = "(%s) != null";
00046
00047 public MethodSpec extractMethodSpec(Method method, NameSpace ns) {
00048 MethodSpec result = new MethodSpec();
00049 extractMethodSpec(method, result, ns);
00050 return result;
00051 }
00052
00053 private void extractMethodSpec(Method method, MethodSpec result, NameSpace ns) {
00054 extractMethodSpecNonRecursive(method, result, ns);
00055
00056
00057 if (!Modifier.isStatic(method.getModifiers())) {
00058 Class<?> methodDeclCls = method.getDeclaringClass();
00059 for (Class<?> cls : ReflectionUtils.getImmParents(methodDeclCls)) {
00060 try {
00061 Method m = ReflectionUtils.getMethod(cls, method.getName(), method.getParameterTypes());
00062 extractMethodSpec(m, result, ns);
00063
00064
00065 } catch (NoSuchMethodException e) {
00066 }
00067 }
00068 }
00069 return;
00070 }
00071
00072 private void extractMethodSpecNonRecursive(Method method, MethodSpec result, NameSpace ns) {
00073
00074 Set<String> requires = new LinkedHashSet<String>();
00075 Set<String> ensures = new LinkedHashSet<String>();
00076 Set<String> modifies = new LinkedHashSet<String>();
00077
00078
00079 for (Annotation ann : method.getAnnotations()) {
00080 if (ann instanceof Requires) {
00081 requires.addAll(convertArray(((Requires) ann).value()));
00082 } else if (ann instanceof Ensures) {
00083 ensures.addAll(convertArray(((Ensures) ann).value()));
00084 } else if (ann instanceof Effects) {
00085 ensures.addAll(convertArray(((Effects) ann).value()));
00086 } else if (ann instanceof Modifies) {
00087 modifies.addAll(convertArray(((Modifies) ann).value()));
00088 } else if (ann instanceof Returns) {
00089 ensures.add(String.format(RETURNS_FORMAT, ((Returns) ann).value()));
00090 } else if (ann instanceof Pure) {
00091 result.makePure();
00092 } else if (ann instanceof Helper) {
00093 result.makePure();
00094 } else if (ann instanceof NonNull) {
00095 ensures.add(String.format(NONNULL_FORMAT, "return"));
00096 } else if (ann instanceof Throws) {
00097 throw new RuntimeException("Throws annotation not supported");
00098 } else if (ann instanceof Specification) {
00099
00100 for (Case cs : ((Specification) ann).value()) {
00101
00102 final List<String> caseRequires = new ArrayList<String>();
00103 final List<String> caseEnsures = new ArrayList<String>();
00104 final List<String> caseModifies = new ArrayList<String>();
00105 boolean caseExceptional = false;
00106
00107 caseRequires.addAll(convertArray(cs.requires()));
00108 caseEnsures.addAll(convertArray(cs.ensures()));
00109 caseModifies.addAll(convertArray(cs.modifies()));
00110 caseExceptional = TYPE_EXCEPTIONAL.equals(cs.type().name());
00111
00112 Source pres = new Source(clause(caseRequires), ns, Rule.CLAUSE);
00113 Source posts = new Source(clause(caseEnsures), ns, Rule.CLAUSE);
00114 Source frames = new Source(frame(caseModifies), ns, Rule.FRAME);
00115
00116 result.addCase(pres, posts, frames, caseExceptional);
00117 }
00118 } else if (ann instanceof Fresh) {
00119 Fresh fresh = (Fresh) ann;
00120 for (FreshObjects freshObj : fresh.value()) {
00121 result.addFreshObj(freshObj.cls(), freshObj.typeParams(), freshObj.num());
00122 }
00123 } else if (ann instanceof FreshObjects) {
00124 FreshObjects freshObj = (FreshObjects) ann;
00125 result.addFreshObj(freshObj.cls(), freshObj.typeParams(), freshObj.num());
00126 } else if (ann instanceof Options) {
00127 Options opt = (Options) ann;
00128 result.addOptions(opt);
00129 }
00130 }
00131
00132
00133 if (requires.size() > 0 || ensures.size() > 0 || modifies.size() > 0)
00134 result.addCase(new Source(clause(requires), ns, Rule.CLAUSE),
00135 new Source(clause(ensures), ns, Rule.CLAUSE),
00136 new Source(frame(modifies), ns, Rule.FRAME),
00137 false);
00138
00139 }
00140
00141
00142
00143
00144 public List<Source> extractClassSpec(JType.Unary jtype) {
00145 List<Source> result = new ArrayList<Source>();
00146 for (Annotation ann : jtype.clazz().getAnnotations()) {
00147 if (ann instanceof Invariant) {
00148 for (String inv : ((Invariant) ann).value())
00149 result.add(new Source(inv, NameSpace.forClass(jtype), Rule.CLAUSE));
00150 } else if (ann instanceof SpecField) {
00151 for (String sf : ((SpecField) ann).value())
00152 result.add(new Source(sf, NameSpace.forClass(jtype), Rule.DECLARATION, false));
00153 } else if (ann instanceof FuncField) {
00154 for (String sf : ((FuncField) ann).value())
00155 result.add(new Source(sf, NameSpace.forClass(jtype), Rule.DECLARATION, true));
00156 }
00157 }
00158 return result;
00159 }
00160
00161
00162
00163
00164 public List<Source> extractFieldSpec(Field field, JType.Unary declType) {
00165 List<Source> result = new ArrayList<Source>();
00166 for (Annotation ann : field.getAnnotations()) {
00167 if (ann instanceof NonNull) {
00168 result.add(new Source(String.format(NONNULL_FORMAT, "this." + field.getName()),
00169 NameSpace.forClass(declType), Rule.CLAUSE));
00170 } else if (ann instanceof Invariant) {
00171 for (String inv : ((Invariant) ann).value())
00172 result.add(new Source(inv, NameSpace.forClass(declType), Rule.CLAUSE));
00173 }
00174 }
00175 return result;
00176 }
00177
00178
00180 private List<String> convertArray(String[] strs) {
00181 List<String> result = new ArrayList<String>();
00182 for (String str : strs) {
00183 if ("@nothing".equals(str))
00184 continue;
00185 result.add(str);
00186 }
00187 return result;
00188 }
00189
00190 private String clause(Collection<String> clauses) {
00191 if (clauses.size() == 0)
00192 return CLAUSE_DEFAULT;
00193
00194 final StringBuilder sb = new StringBuilder();
00195 for (String s : clauses) {
00196 if (sb.length() > 0)
00197 sb.append(" && ");
00198 sb.append('(').append(s).append(')');
00199 }
00200 return sb.toString();
00201 }
00202
00203 private String frame(Collection<String> frames) {
00204 if (frames.size() == 0)
00205 return "";
00206
00207 final StringBuilder sb = new StringBuilder();
00208 for (String s : frames) {
00209 if (sb.length() > 0)
00210 sb.append(" , ");
00211 sb.append(s);
00212 }
00213
00214 return sb.toString();
00215 }
00216 }