001package daikon.split;
002
003import daikon.Daikon;
004import daikon.inv.DummyInvariant;
005import java.io.File;
006import java.io.FileNotFoundException;
007import java.io.IOException;
008import java.lang.reflect.InvocationTargetException;
009import org.checkerframework.checker.lock.qual.GuardSatisfied;
010import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
011import org.checkerframework.checker.nullness.qual.Nullable;
012import org.checkerframework.checker.signature.qual.BinaryName;
013import org.checkerframework.dataflow.qual.Pure;
014import org.checkerframework.dataflow.qual.SideEffectFree;
015import org.plumelib.reflection.ReflectionPlume;
016import typequals.prototype.qual.Prototype;
017
018/**
019 * A SplitterObject is the starting point for all the information we have about a splitting
020 * condition. It is created immediately when the condition is read from the {@code .spinfo} file,
021 * and later contains a reference to the compiled "Splitter" object.
022 */
023public class SplitterObject implements Comparable<SplitterObject> {
024
025  private @MonotonicNonNull Splitter splitter;
026  private String condition; // the condition
027  private @BinaryName String className = "Unassigned"; // the Java classname of this Splitter
028  private String directory; // the directory where it resides
029  private String pptName; // the program point with which it is associated
030  private boolean exists = false;
031  private String testString = "Unassigned";
032  // Not necessarily an error message -- really just a status message.
033  private String errorMessage = "Splitter not yet loaded";
034  private int guid = -999; // -999 indicates not yet set
035
036  /** class file containing compiled code for this splitter */
037  private @MonotonicNonNull File classFile;
038
039  public boolean dummyDesired = false;
040  public @Nullable String daikonFormat = null;
041  public @Nullable String javaFormat = null;
042  public @Nullable String escFormat = null;
043  public @Nullable String simplifyFormat = null;
044  public @Nullable String jmlFormat = null;
045  public @Nullable String dbcFormat = null;
046  public @Nullable String csharpFormat = null;
047
048  /**
049   * @param condition the splitting condition of this splitter
050   * @param directory the directory where the source of this splitter is located
051   */
052  public SplitterObject(String pptName, String condition, String directory) {
053    this.condition = condition;
054    this.pptName = pptName;
055    this.directory = directory;
056    this.javaFormat = condition;
057    this.daikonFormat = condition;
058    this.csharpFormat = condition;
059  }
060
061  /**
062   * @param fileName the pathname of a {@code .class} file
063   * @return a Java Class corresponding to the {@code .class} file, or null
064   */
065  static @Nullable Class<?> defineSplitterClass(@BinaryName String className, String fileName) {
066    try {
067      return ReflectionPlume.defineClassFromFile(className, fileName);
068    } catch (FileNotFoundException e) {
069      if (!PptSplitter.dkconfig_suppressSplitterErrors) {
070        System.out.println(
071            "File " + fileName.substring(0, fileName.length() - 6) + ".java did not compile");
072      }
073      return null;
074    } catch (IOException ioe) {
075      System.out.println("IO Error while reading class data " + fileName);
076      return null;
077    } catch (UnsupportedClassVersionError ucve) { // should be more general?
078      throw new Daikon.UserError(
079          String.join(
080              System.lineSeparator(),
081              "Wrong Java version while reading file " + fileName + ": " + ucve.getMessage(),
082              "This indicates a possible problem with configuration option",
083              "daikon.split.SplitterFactory.compiler whose value is: "
084                  + SplitterFactory.dkconfig_compiler));
085    }
086  }
087
088  /** Sets the "splitter" field of this object to a newly-instantiated object. */
089  public void load() {
090    Class<?> tempClass = defineSplitterClass(className, directory + className + ".class");
091    if (tempClass != null) {
092      try {
093        splitter = (Splitter) tempClass.getDeclaredConstructor().newInstance();
094      } catch (ClassFormatError
095          | IllegalAccessException
096          | InstantiationException
097          | InvocationTargetException
098          | NoSuchMethodException e) {
099        e.printStackTrace(System.out);
100        throw new Error("Trying to invoke " + tempClass + " constructor", e);
101      }
102      DummyInvariant dummy =
103          new @Prototype
104          DummyInvariant(
105              daikonFormat,
106              javaFormat,
107              escFormat,
108              simplifyFormat,
109              jmlFormat,
110              dbcFormat,
111              csharpFormat,
112              dummyDesired);
113      splitter.makeDummyInvariantFactory(dummy);
114      errorMessage = "Splitter exists " + this.toString();
115      exists = true;
116    } else {
117      errorMessage =
118          "No class data for "
119              + this.toString()
120              + ", to be loaded from "
121              + directory
122              + className
123              + ".class";
124      exists = false;
125    }
126  }
127
128  /**
129   * Returns true if the Splitter object exists for this SplitterObject, i.e. whether it
130   * successfully loaded.
131   *
132   * @return true if the Splitter object exists for this SplitterObject, i.e. whether it
133   *     successfully loaded
134   */
135  public boolean splitterExists() {
136    return exists;
137  }
138
139  /**
140   * Returns true if the {@code .class} file exists for the Splitter represented by this
141   * SplitterObject, false otherwise.
142   *
143   * @return true if the {@code .class} file exists for the Splitter represented by this
144   *     SplitterObject, false otherwise
145   */
146  public boolean compiled() {
147    if (classFile != null && classFile.exists()) {
148      errorMessage = "Splitter exists " + this.toString();
149      return true;
150    }
151    return false;
152  }
153
154  /**
155   * Returns the Splitter that this SplitterObject represents, or null if splitterExists() == false.
156   *
157   * @return the Splitter that this SplitterObject represents, or null if splitterExists() == false
158   */
159  public @Nullable Splitter getSplitter() {
160    return this.splitter;
161  }
162
163  /**
164   * Set the error message of this this SplitterObject. This indicates the status of the Splitter.
165   */
166  public void setError(String errorMessage) {
167    this.errorMessage = errorMessage;
168  }
169
170  /** Get the error message of this SplitterObject. */
171  public String getError() {
172    return this.errorMessage;
173  }
174
175  /** Set the unique ID of this splitterObject. */
176  public void setGUID(int ID) {
177    this.guid = ID;
178  }
179
180  /** Return the unique ID of this splitterObject. */
181  public int getGUID() {
182    return this.guid;
183  }
184
185  /**
186   * Returns the full source of the Splitter.
187   *
188   * @return the full source of the Splitter
189   */
190  public String getFullSourcePath() {
191    return (directory + className + ".java");
192  }
193
194  /**
195   * Returns the program point represented by this Splitter.
196   *
197   * @return the program point represented by this Splitter
198   */
199  public String getPptName() {
200    return this.pptName;
201  }
202
203  /** Set the className of this Splitter. */
204  public void setClassName(@BinaryName String className) {
205    this.className = className;
206    classFile = new File(directory + className + ".class");
207  }
208
209  /**
210   * Returns the className of the Splitter.
211   *
212   * @return the className of the Splitter
213   */
214  public @BinaryName String getClassName() {
215    return this.className;
216  }
217
218  public void setDirectory(String directory) {
219    this.directory = directory;
220  }
221
222  public String getDirectory() {
223    return this.directory;
224  }
225
226  /**
227   * Returns the condition represented by the Splitter.
228   *
229   * @return the condition represented by the Splitter
230   */
231  public String condition() {
232    return this.condition;
233  }
234
235  public void setTestString(String testString) {
236    this.testString = testString;
237  }
238
239  public String getTestString() {
240    return this.testString;
241  }
242
243  @SideEffectFree
244  @Override
245  public String toString(@GuardSatisfied SplitterObject this) {
246    return (className
247        + ": "
248        + "condition: "
249        + condition
250        + ", testString: "
251        + testString
252        + ", @ "
253        + pptName);
254  }
255
256  @Pure
257  @Override
258  public int compareTo(@GuardSatisfied SplitterObject this, SplitterObject o) {
259    return this.guid - o.getGUID();
260  }
261}