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   * Return a Java Class corresponding to the {@code .class} file, or null.
063   *
064   * @param fileName the pathname of a {@code .class} file
065   * @return a Java Class corresponding to the {@code .class} file, or null
066   */
067  static @Nullable Class<?> defineSplitterClass(@BinaryName String className, String fileName) {
068    try {
069      return ReflectionPlume.defineClassFromFile(className, fileName);
070    } catch (FileNotFoundException e) {
071      if (!PptSplitter.dkconfig_suppressSplitterErrors) {
072        System.out.println(
073            "File " + fileName.substring(0, fileName.length() - 6) + ".java did not compile");
074      }
075      return null;
076    } catch (IOException ioe) {
077      System.out.println("IO Error while reading class data " + fileName);
078      return null;
079    } catch (UnsupportedClassVersionError ucve) { // should be more general?
080      throw new Daikon.UserError(
081          String.join(
082              System.lineSeparator(),
083              "Wrong Java version while reading file " + fileName + ": " + ucve.getMessage(),
084              "This indicates a possible problem with configuration option",
085              "daikon.split.SplitterFactory.compiler whose value is: "
086                  + SplitterFactory.dkconfig_compiler));
087    }
088  }
089
090  /** Sets the "splitter" field of this object to a newly-instantiated object. */
091  public void load() {
092    Class<?> tempClass = defineSplitterClass(className, directory + className + ".class");
093    if (tempClass != null) {
094      try {
095        splitter = (Splitter) tempClass.getDeclaredConstructor().newInstance();
096      } catch (ClassFormatError
097          | IllegalAccessException
098          | InstantiationException
099          | InvocationTargetException
100          | NoSuchMethodException e) {
101        e.printStackTrace(System.out);
102        throw new Error("Trying to invoke " + tempClass + " constructor", e);
103      }
104      DummyInvariant dummy =
105          new @Prototype
106          DummyInvariant(
107              daikonFormat,
108              javaFormat,
109              escFormat,
110              simplifyFormat,
111              jmlFormat,
112              dbcFormat,
113              csharpFormat,
114              dummyDesired);
115      splitter.makeDummyInvariantFactory(dummy);
116      errorMessage = "Splitter exists " + this.toString();
117      exists = true;
118    } else {
119      errorMessage =
120          "No class data for "
121              + this.toString()
122              + ", to be loaded from "
123              + directory
124              + className
125              + ".class";
126      exists = false;
127    }
128  }
129
130  /**
131   * Returns true if the Splitter object exists for this SplitterObject, i.e. whether it
132   * successfully loaded.
133   *
134   * @return true if the Splitter object exists for this SplitterObject, i.e. whether it
135   *     successfully loaded
136   */
137  public boolean splitterExists() {
138    return exists;
139  }
140
141  /**
142   * Returns true if the {@code .class} file exists for the Splitter represented by this
143   * SplitterObject, false otherwise.
144   *
145   * @return true if the {@code .class} file exists for the Splitter represented by this
146   *     SplitterObject, false otherwise
147   */
148  public boolean compiled() {
149    if (classFile != null && classFile.exists()) {
150      errorMessage = "Splitter exists " + this.toString();
151      return true;
152    }
153    return false;
154  }
155
156  /**
157   * Returns the Splitter that this SplitterObject represents, or null if splitterExists() == false.
158   *
159   * @return the Splitter that this SplitterObject represents, or null if splitterExists() == false
160   */
161  public @Nullable Splitter getSplitter() {
162    return this.splitter;
163  }
164
165  /**
166   * Set the error message of this this SplitterObject. This indicates the status of the Splitter.
167   */
168  public void setError(String errorMessage) {
169    this.errorMessage = errorMessage;
170  }
171
172  /** Get the error message of this SplitterObject. */
173  public String getError() {
174    return this.errorMessage;
175  }
176
177  /** Set the unique ID of this splitterObject. */
178  public void setGUID(int ID) {
179    this.guid = ID;
180  }
181
182  /** Return the unique ID of this splitterObject. */
183  public int getGUID() {
184    return this.guid;
185  }
186
187  /**
188   * Returns the full source of the Splitter.
189   *
190   * @return the full source of the Splitter
191   */
192  public String getFullSourcePath() {
193    return (directory + className + ".java");
194  }
195
196  /**
197   * Returns the program point represented by this Splitter.
198   *
199   * @return the program point represented by this Splitter
200   */
201  public String getPptName() {
202    return this.pptName;
203  }
204
205  /** Set the className of this Splitter. */
206  public void setClassName(@BinaryName String className) {
207    this.className = className;
208    classFile = new File(directory + className + ".class");
209  }
210
211  /**
212   * Returns the className of the Splitter.
213   *
214   * @return the className of the Splitter
215   */
216  public @BinaryName String getClassName() {
217    return this.className;
218  }
219
220  public void setDirectory(String directory) {
221    this.directory = directory;
222  }
223
224  public String getDirectory() {
225    return this.directory;
226  }
227
228  /**
229   * Returns the condition represented by the Splitter.
230   *
231   * @return the condition represented by the Splitter
232   */
233  public String condition() {
234    return this.condition;
235  }
236
237  public void setTestString(String testString) {
238    this.testString = testString;
239  }
240
241  public String getTestString() {
242    return this.testString;
243  }
244
245  @SideEffectFree
246  @Override
247  public String toString(@GuardSatisfied SplitterObject this) {
248    return (className
249        + ": "
250        + "condition: "
251        + condition
252        + ", testString: "
253        + testString
254        + ", @ "
255        + pptName);
256  }
257
258  @Pure
259  @Override
260  public int compareTo(@GuardSatisfied SplitterObject this, SplitterObject o) {
261    return this.guid - o.getGUID();
262  }
263}