001package daikon.tools.runtimechecker; 002 003import java.io.ObjectStreamException; 004import java.io.Serializable; 005import java.util.ArrayList; 006import java.util.Arrays; 007import java.util.HashMap; 008import java.util.HashSet; 009import java.util.List; 010import java.util.Set; 011import org.checkerframework.checker.interning.qual.UsesObjectEquals; 012import org.checkerframework.checker.lock.qual.GuardSatisfied; 013import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; 014import org.checkerframework.checker.nullness.qual.Nullable; 015import org.checkerframework.checker.signedness.qual.UnknownSignedness; 016import org.checkerframework.dataflow.qual.Pure; 017import org.checkerframework.dataflow.qual.SideEffectFree; 018 019/** 020 * Represents a violation of a {@code Property}. 021 * 022 * @see Property 023 */ 024public class Violation implements Serializable { 025 026 private static final long serialVersionUID = 1L; 027 028 // The violated property. 029 private final Property property; 030 031 // The time at which the violation happened (entry or exit 032 // from method). 033 private final Time time; 034 035 /** The violated property. */ 036 public Property property() { 037 return property; 038 } 039 040 /** The time at which the violation happened (entry or exit from method). */ 041 public Time time() { 042 return time; 043 } 044 045 /** 046 * Indicates at which program point the violation occurred: at method entry or method exit. 047 * 048 * <p>This class contains only two (static) objects: {@code onEntry} and {@code onExit}. 049 */ 050 // This should be an enum 051 @UsesObjectEquals 052 public static class Time implements Serializable { 053 054 private static final long serialVersionUID = 1L; 055 056 public final String name; 057 058 public final String xmlname; 059 060 private Time(String name, String xmlname) { 061 this.name = name; 062 this.xmlname = xmlname; 063 } 064 065 @Pure 066 @Override 067 public int hashCode(@GuardSatisfied @UnknownSignedness Time this) { 068 return name.hashCode(); 069 } 070 071 @SideEffectFree 072 @Override 073 public String toString(@GuardSatisfied Time this) { 074 return name; 075 } 076 077 public String xmlString() { 078 return xmlname; 079 } 080 081 public static final Time onEntry = new Time("violated on entry ", "<ON_ENTRY>"); 082 083 public static final Time onExit = new Time("violated on exit ", "<ON_EXIT>"); 084 085 // See documentation for Serializable. 086 private Object readResolve() throws ObjectStreamException { 087 if (name.equals("violated on entry")) { 088 return onEntry; 089 } else { 090 assert name.equals("violated on exit ") : name; 091 return onExit; 092 } 093 } 094 } 095 096 /** 097 * Creates the violation represented by {@code vioString}. 098 * 099 * @param vioString: a the string is of the form: {@code <INVINFO> property time</INVINFO>} where 100 * {@code property} is valid XML representation of a {@code Property}, and time is {@code 101 * <ON_ENTRY>} or {@code <ON_EXIT>}. 102 * @return the violation represented by {@code vioString} 103 */ 104 public static Violation get(String vioString) { 105 106 if (!vioString.matches(".*(<INVINFO>.*</INVINFO>).*")) { 107 throw new IllegalArgumentException(vioString); 108 } 109 110 String annoString = vioString.replaceFirst(".*(<INVINFO>.*</INVINFO>).*", "$1"); 111 112 Property anno; 113 try { 114 anno = Property.get(annoString); 115 } catch (MalformedPropertyException e) { 116 throw new IllegalArgumentException(e.getMessage(), e); 117 } 118 119 Time t; 120 if (vioString.matches(".*<ON_ENTRY>.*")) { 121 t = Time.onEntry; 122 } else if (vioString.matches(".*<ON_EXIT>.*")) { 123 t = Time.onExit; 124 } else { 125 throw new Error("Bad time"); 126 } 127 128 return get(anno, t); 129 } 130 131 // Collection of all the Violation objects created. 132 // The key is the hashCode of the Violation that is the value. 133 private static HashMap<Integer, Violation> violationsMap = new HashMap<>(); 134 135 // [[[ TODO: ensure args are not null (otherwise hashCode, 136 // equals can break). Do the same thing for Property. ]]] 137 private Violation(Property anno, Time t) { 138 this.property = anno; 139 this.time = t; 140 } 141 142 /** Returns a violation with the given attributes. */ 143 public static Violation get(Property anno, Time t) { 144 Violation vio = new Violation(anno, t); 145 Integer key = vio.hashCode(); 146 if (violationsMap.containsKey(key)) { 147 return violationsMap.get(key); 148 } else { 149 violationsMap.put(key, vio); 150 return vio; 151 } 152 } 153 154 /** 155 * if {@code property} is an entry or exit property, returns the violation corresponding to this 156 * property. If it's an object invariant property, throws an exception. 157 */ 158 public static Violation get(Property property) { 159 Time t; 160 if (property.kind() == Property.Kind.enter) { 161 t = Time.onEntry; 162 } else if (property.kind() == Property.Kind.exit) { 163 t = Time.onExit; 164 } else { 165 throw new IllegalArgumentException( 166 "property must be ENTER or EXIT kind: " + property.toString()); 167 } 168 return get(property, t); 169 } 170 171 /** The XML String representing this property. */ 172 public String xmlString() { 173 return "<VIOLATION>" + property.xmlString() + time.xmlString() + "</VIOLATION>"; 174 } 175 176 /** String representation. */ 177 @SideEffectFree 178 @Override 179 public String toString(@GuardSatisfied Violation this) { 180 return time.toString() + " : " + property.toString(); 181 } 182 183 /** String representation. */ 184 @SideEffectFree 185 public String toStringWithMethod(@GuardSatisfied Violation this) { 186 return time.toString() + "of " + property.method() + " : " + property.toString(); 187 } 188 189 /** Two violations are equal if their properties and times are equal. */ 190 @EnsuresNonNullIf(result = true, expression = "#1") 191 @Pure 192 @Override 193 public boolean equals(@GuardSatisfied Violation this, @GuardSatisfied @Nullable Object o) { 194 if (o == null) { 195 return false; 196 } 197 if (!(o instanceof Violation)) { 198 return false; 199 } 200 Violation other = (Violation) o; 201 return this.property.equals(other.property) && this.time.equals(other.time); 202 } 203 204 @Pure 205 @Override 206 public int hashCode(@GuardSatisfied @UnknownSignedness Violation this) { 207 return property.hashCode() + time.hashCode(); 208 } 209 210 /** 211 * Returns all violations in {@code vios} that violate properties with confidence greater than or 212 * equal to {@code thresh}. 213 */ 214 public static Violation[] viosWithConfGEQ(Violation[] vios, double thresh) { 215 List<Violation> ret = new ArrayList<>(); 216 for (int i = 0; i < vios.length; i++) { 217 Violation v = vios[i]; 218 Property a = v.property; 219 if (a.confidence >= thresh) { 220 ret.add(v); 221 } 222 } 223 return ret.toArray(new Violation[] {}); 224 } 225 226 /** 227 * Returns all violations in {@code vios} that violate properties with confidence less than {@code 228 * thresh}. 229 */ 230 public static Violation[] viosWithConfLT(Violation[] vios, double thresh) { 231 List<Violation> ret = new ArrayList<>(); 232 for (int i = 0; i < vios.length; i++) { 233 Violation v = vios[i]; 234 Property a = v.property; 235 if (a.confidence < thresh) { 236 ret.add(v); 237 } 238 } 239 return ret.toArray(new Violation[] {}); 240 } 241 242 /** Returns all violations in {@code vios} with the given time. */ 243 public static Violation[] withTime(Violation[] vios, Time time) { 244 List<Violation> ret = new ArrayList<>(); 245 for (int i = 0; i < vios.length; i++) { 246 Violation v = vios[i]; 247 if (v.time == time) { 248 ret.add(v); 249 } 250 } 251 return ret.toArray(new Violation[] {}); 252 } 253 254 /** Returns all violations in {@code vios} with the given king. */ 255 public static Violation[] withKind(Violation[] vios, Property.Kind kind) { 256 List<Violation> ret = new ArrayList<>(); 257 for (int i = 0; i < vios.length; i++) { 258 if (kind == vios[i].property().kind()) { 259 ret.add(vios[i]); 260 } 261 } 262 return ret.toArray(new Violation[] {}); 263 } 264 265 /** 266 * Looks for legal XML representation of violations in the given string, and returns all 267 * violations that are successfully parsed. 268 */ 269 // [[[ TODO: There's something unsatisfying about this method 270 // swallowing up erroneous input silently. Fix this. ]]] 271 public static Violation[] findViolations(String vioString) { 272 273 if (vioString == null || vioString.equals("")) { 274 return new Violation[] {}; 275 } 276 Set<Violation> vios = new HashSet<>(); 277 String[] cutUp = vioString.split("<VIOLATION>"); 278 for (int splits = 0; splits < cutUp.length; splits++) { 279 try { 280 String s = cutUp[splits]; 281 Violation v = Violation.get("<VIOLATION>" + s); // [[[ explain 282 // this! ]]] 283 vios.add(v); 284 } catch (Exception e) { 285 // go on to next split 286 } 287 } 288 return vios.toArray(new Violation[] {}); 289 } 290 291 public String toNiceString(String prefix, double confidenceThreshold) { 292 return prefix 293 + ((property.confidence > confidenceThreshold) ? "H" : " ") 294 + " " 295 + prefix 296 + " " 297 + toString() 298 + daikon.Global.lineSep; 299 } 300 301 /** 302 * A human-readable String representation of a list of violations. The violations are sorted by 303 * "time" (which is not the same as sorting them by time!) and violations of high-confidence 304 * properties are prepended with "H". 305 */ 306 public static String toNiceString( 307 String prefix, Set<Violation> vios, double confidenceThreshold) { 308 309 // TODO; It is bizarre that withTime requires conversion to an array. 310 Violation[] vios_array = vios.toArray(new Violation[] {}); 311 Violation[] onEntry = Violation.withTime(vios_array, Violation.Time.onEntry); 312 Violation[] onExit = Violation.withTime(vios_array, Violation.Time.onExit); 313 314 assert onEntry.length + onExit.length == vios.size() 315 : "onEntry: " 316 + Arrays.asList(onEntry).toString() 317 + "onExit: " 318 + Arrays.asList(onExit).toString() 319 + "vios: " 320 + vios; 321 322 StringBuilder retval = new StringBuilder(); 323 for (int i = 0; i < onEntry.length; i++) { 324 retval.append(onEntry[i].toNiceString(prefix, confidenceThreshold)); 325 } 326 for (int i = 0; i < onExit.length; i++) { 327 retval.append(onExit[i].toNiceString(prefix, confidenceThreshold)); 328 } 329 return retval.toString(); 330 } 331 332 // See documentation for Serializable. 333 private Object readResolve() throws ObjectStreamException { 334 return get(property, time); 335 } 336}