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}