Source code

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}