001package daikon.tools.jtb; 002 003import java.util.Collections; 004import java.util.HashMap; 005import java.util.HashSet; 006import java.util.List; 007import java.util.Set; 008import org.checkerframework.checker.interning.qual.UsesObjectEquals; 009import org.checkerframework.checker.lock.qual.GuardSatisfied; 010import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; 011import org.checkerframework.checker.nullness.qual.Nullable; 012import org.checkerframework.dataflow.qual.Pure; 013import org.checkerframework.dataflow.qual.SideEffectFree; 014 015/** 016 * Utility class to parse annotations generated with the Annotate program using the {@code 017 * --wrap_xml} flag. 018 * 019 * <p>An example of the String representation of an annotation, as output with the {@code 020 * --wrap_xml} flag, is: 021 * 022 * <pre>{@code 023 * <INVINFO> 024 * <INV> this.topOfStack <= this.theArray.length-1 </INV> 025 * <ENTER> 026 * <DAIKON> this.topOfStack <= size(this.theArray[])-1 </DAIKON> 027 * <DAIKONCLASS>class daikon.inv.binary.twoScalar.IntLessEqual</DAIKONCLASS> 028 * <METHOD> isEmpty() </METHOD> 029 * </INVINFO> 030 * }</pre> 031 * 032 * The above string should actually span only one line. 033 * 034 * <p>To be well-formed, an annotation should be enclosed in {@code <INVINFO>} tags, contain 035 * 036 * <pre>{@code 037 * <DAIKON> and 038 * <METHOD> 039 * }</pre> 040 * 041 * tags, and exactly one of 042 * 043 * <pre>{@code 044 * <ENTER>, 045 * <EXIT>, 046 * <OBJECT>, or 047 * <CLASS>. 048 * }</pre> 049 * 050 * Obviously, the tool Annotate outputs well-formed annotations, so the user shouldn't have to worry 051 * too much about well-formedness. 052 * 053 * <p>Two annotations are equal iff their fields "daikonRep", "method" and "kind" are equal. 054 * 055 * <p>The factory method get(String annoString) returns an annotation that equals to the annotation 056 * represented by annoString. In particular, if the same String is given twice to get(String 057 * annoString), the method will return the same Annotation object. 058 */ 059public class Annotation { 060 061 // Maps into all the Annotation objects created. 062 private static HashMap<Integer, Annotation> annotationsMap = new HashMap<>(); 063 064 /** Daikon representation (as output by Daikon's default output format). */ 065 private final String daikonRep; 066 067 /** The way this annotation would be printed by Daikon. */ 068 public String daikonRep(@GuardSatisfied Annotation this) { 069 return daikonRep; 070 } 071 072 private final String method; 073 074 /** The method that this annotation refers to. */ 075 public String method(@GuardSatisfied Annotation this) { 076 return method; 077 } 078 079 private final Kind kind; 080 081 /** The kind of this annotation. */ 082 public Kind kind(@GuardSatisfied Annotation this) { 083 return kind; 084 } 085 086 private String invRep; 087 088 /** 089 * Representation of this annotation (the format depends on which output format was used to create 090 * the annotation in Daikon; it's one of JAVA, JML, ESC or DBC). 091 */ 092 public String invRep() { 093 return invRep; 094 } 095 096 public String daikonClass; 097 098 /** The Daikon class name that this invariant represents an instance of. */ 099 public String daikonClass() { 100 return daikonClass; 101 } 102 103 private Annotation( 104 Kind kind, String daikonRep, String method, String invRep, String daikonClass) { 105 this.kind = kind; 106 this.daikonRep = daikonRep; 107 this.method = method; 108 this.invRep = invRep; 109 this.daikonClass = daikonClass; 110 } 111 112 /** Parse a String and return the annotation that it represents. */ 113 // [[ Note: Using an XML parser seems like too strong a hammer here, 114 // and the performance of string matching is not an obvious 115 // bottleneck. ]] 116 public static Annotation get(String annoString) throws Annotation.MalformedAnnotationException { 117 118 // check well-formedness 119 if (!(annoString.matches(".*<INVINFO>.*</INVINFO>.*") 120 && annoString.matches(".*<DAIKON>(.*)</DAIKON>.*") 121 && annoString.matches(".*<METHOD>(.*)</METHOD>.*"))) { 122 throw new Annotation.MalformedAnnotationException(annoString); 123 } 124 125 // figure out what kind of annotation it is 126 Kind k; 127 if (annoString.matches(".*<ENTER>.*")) { 128 k = Kind.enter; 129 } else if (annoString.matches(".*<EXIT>.*")) { 130 k = Kind.exit; 131 } else if (annoString.matches(".*<OBJECT>.*") || annoString.matches(".*<CLASS>.*")) { 132 k = Kind.objectInvariant; 133 } else { 134 throw new Annotation.MalformedAnnotationException(annoString); 135 } 136 137 String theDaikonRep = annoString.replaceFirst(".*<DAIKON>(.*)</DAIKON>.*", "$1").trim(); 138 String theMethod = annoString.replaceFirst(".*<METHOD>(.*)</METHOD>.*", "$1").trim(); 139 String theInvRep = annoString.replaceFirst(".*<INV>(.*)</INV>.*", "$1").trim(); 140 String theDaikonClass = 141 annoString.replaceFirst(".*<DAIKONCLASS>(.*)</DAIKONCLASS>.*", "$1").trim(); 142 143 Annotation anno = Annotation.get(k, theDaikonRep, theMethod, theInvRep, theDaikonClass); 144 145 return anno; 146 } 147 148 /** 149 * Thrown by method get(String annoString) if annoString doesn't represent a well-formed 150 * annotation. 151 */ 152 public static class MalformedAnnotationException extends Exception { 153 static final long serialVersionUID = 20050923L; 154 155 public MalformedAnnotationException(String s) { 156 super(s); 157 } 158 } 159 160 /** 161 * XML representation. May be different from the String used to generate the input; only those 162 * tags that were parsed by the get() method will be output here. 163 */ 164 public String xmlString() { 165 return "<INVINFO> " 166 + kind.xmlString() 167 + "<DAIKON>" 168 + daikonRep 169 + " </DAIKON> " 170 + "<METHOD> " 171 + method 172 + " </METHOD>" 173 + "<INV>" 174 + invRep 175 + "</INV>" 176 + " <DAIKONCLASS>" 177 + daikonClass 178 + " </DAIKONCLASS>" 179 + "</INVINFO>"; 180 } 181 182 /** 183 * Find, parse and return all distinct annotations found in a String. The string {@code 184 * annoString} may contain none, one, or several annotations. Malformed annotations are ignored. 185 */ 186 public static Annotation[] findAnnotations(String annoString) { 187 List<String> l = Collections.singletonList(annoString); 188 return findAnnotations(l); 189 } 190 191 /** 192 * Find, parse and return all distinct annotations found in a list of strings. Each string in 193 * {@code annoStrings} may contain none, one, or several annotations. Malformed annotations are 194 * ignored. 195 */ 196 public static Annotation[] findAnnotations(List<String> annoStrings) { 197 198 if (annoStrings == null) { 199 return new Annotation[] {}; 200 } 201 // Pattern p = Pattern.compile("(<INVINFO>.*</INVINFO>)"); 202 Set<Annotation> annos = new HashSet<>(); 203 for (String location : annoStrings) { 204 if (location == null || location.equals("")) { 205 continue; 206 } 207 String[] cutUp = location.split("<INVINFO>"); 208 // Matcher m = p.matcher(location); 209 for (int splits = 0; splits < cutUp.length; splits++) { 210 // while (m.find()) { 211 try { 212 // String s = m.group(1); 213 String s = cutUp[splits]; 214 Annotation anno = Annotation.get("<INVINFO>" + s); 215 // [[[ explain this! ]]] 216 annos.add(anno); 217 } catch (Exception e) { 218 // malformed annotation; just go to next iteration 219 } 220 } 221 } 222 return annos.toArray(new Annotation[] {}); 223 } 224 225 // This class should really be an enum. 226 /** 227 * A class representing the kind of an annotation. An invariant is either {@code Kind.enter}, 228 * {@code Kind.exit}, or {@code Kind.objectInvariant} For well-formed Annotations, the following 229 * holds: 230 * 231 * <pre> 232 * a.kind == Kind.enter 233 * || a.kind == Kind.exit 234 * || a.kind == Kind.objectInvariant 235 * </pre> 236 */ 237 @UsesObjectEquals 238 public static class Kind { 239 public final String name; 240 public final String xmlname; 241 242 private Kind(String name, String xmlname) { 243 this.name = name; 244 this.xmlname = xmlname; 245 } 246 247 @Pure 248 @Override 249 public int hashCode(@GuardSatisfied Kind this) { 250 return name.hashCode(); 251 } 252 253 @SideEffectFree 254 @Override 255 public String toString(@GuardSatisfied Kind this) { 256 return name; 257 } 258 259 public String xmlString() { 260 return xmlname; 261 } 262 263 public static final Kind enter = new Kind("precondition ", "<ENTER>"); 264 public static final Kind exit = new Kind("postcondition", "<EXIT>"); 265 public static final Kind objectInvariant = new Kind("obj invariant", "<OBJECT>"); 266 } 267 268 /** Easy-on-the-eye format. */ 269 @SideEffectFree 270 @Override 271 public String toString(@GuardSatisfied Annotation this) { 272 return kind.toString() + " : " + daikonRep(); 273 } 274 275 /** Two annotations are equal iff their fields "daikonRep", "method" and "kind" are equal. */ 276 @EnsuresNonNullIf(result = true, expression = "#1") 277 @Pure 278 @Override 279 public boolean equals(@GuardSatisfied Annotation this, @GuardSatisfied @Nullable Object o) { 280 if (o == null) { 281 return false; 282 } 283 if (!(o instanceof Annotation)) { 284 return false; 285 } 286 Annotation anno = (Annotation) o; 287 return (this.daikonRep().equals(anno.daikonRep()) 288 && this.method().equals(anno.method()) 289 && this.kind().equals(anno.kind())); 290 } 291 292 @Pure 293 @Override 294 public int hashCode(@GuardSatisfied Annotation this) { 295 return daikonRep.hashCode() + kind.hashCode() + method.hashCode(); 296 } 297 298 /** Get the annotation with corresponding properties. */ 299 public static Annotation get( 300 Kind kind, String daikonRep, String method, String invRep, String daikonClass) 301 throws Annotation.MalformedAnnotationException { 302 303 Annotation anno = new Annotation(kind, daikonRep, method, invRep, daikonClass); 304 Integer key = anno.hashCode(); 305 if (annotationsMap.containsKey(key)) { 306 return annotationsMap.get(key); 307 } else { 308 annotationsMap.put(key, anno); 309 return anno; 310 } 311 } 312 313 // This is never used, and the "break" clause seems to be buggy, so 314 // that this returns at most one property. 315 // /** 316 // * The annotations in {@code annas} of kind {@code kind}. 317 // */ 318 // public static Annotation[] getKind(Annotation[] annas, Kind kind) { 319 // List<Annotation> retval = new ArrayList<>(); 320 // for (int i = 0; i < annas.length; i++) { 321 // if (kind == annas[i].kind) { 322 // retval.add(annas[i]); 323 // } 324 // break; 325 // } 326 // return retval.toArray(new Annotation[] { 327 // }); 328 // } 329 330}