001package daikon.tools.runtimechecker; 002 003import static java.nio.charset.StandardCharsets.UTF_8; 004import static java.util.logging.Level.FINE; 005import static java.util.logging.Level.INFO; 006 007import daikon.Daikon; 008import daikon.FileIO; 009import daikon.Global; 010import daikon.PptMap; 011import daikon.tools.jtb.ParseResults; 012import gnu.getopt.Getopt; 013import gnu.getopt.LongOpt; 014import java.io.File; 015import java.io.IOException; 016import java.io.Writer; 017import java.nio.file.Files; 018import java.util.ArrayList; 019import java.util.List; 020import java.util.logging.Logger; 021import jtb.syntaxtree.*; 022import jtb.visitor.TreeDumper; 023import jtb.visitor.TreeFormatter; 024import org.checkerframework.checker.interning.qual.UsesObjectEquals; 025 026/** 027 * Instruments a file to check invariant violations at run time. Violated invariants are stored in a 028 * list in daikon.tools.runtimechecker.Runtime. The control flow of the class remains unchanged from 029 * the original. 030 * 031 * @author Carlos Pacheco 032 */ 033public class InstrumentHandler extends CommandHandler { 034 035 @Override 036 public boolean handles(String command) { 037 if (command.equals("instrument")) { 038 return true; 039 } 040 return false; 041 } 042 043 // If true, the instrumenter also outputs checker classes (classes that define 044 // invariant-checking methods outside the instrumented class). 045 private static boolean createCheckerClasses = false; 046 047 public static final Logger debug = 048 Logger.getLogger("daikon.tools.runtimechecker.InstrumentHandler"); 049 050 // If the --max_invariants_pp option is given, this variable is set 051 // to the maximum number of invariants out annotate per program point. 052 protected static int maxInvariantsPP = -1; 053 054 // User documentation for these fields appears in file InstrumentHandler.doc 055 private static final String make_all_fields_public_SWITCH = "make_all_fields_public"; 056 private static final String output_only_high_conf_invariants_SWITCH = 057 "output_only_high_conf_invariants"; 058 private static final String create_checker_classes_SWITCH = "create_checker_classes"; 059 private static final String directory_SWITCH = "directory"; 060 private static final String checkers_directory_SWITCH = "checker_classes_directory"; 061 062 // Default values; can be overridden by the command-line switches above. 063 /** Default directory for instrumented classes. */ 064 private String instrumented_directory = "instrumented-classes"; 065 066 /** Default directory for checker classes. */ 067 private String checkersOutputDirName = "checker-classes"; 068 069 @SuppressWarnings( 070 "enhancedfor" // Checker Framework bug exposed on line "for (TypeDeclaration decl : 071 // oneFile.roots) {" 072 ) 073 @Override 074 public boolean handle(String[] args) { 075 076 Daikon.output_format = daikon.inv.OutputFormat.JAVA; 077 daikon.PrintInvariants.wrap_xml = true; 078 079 if (!args[0].equals("instrument")) { 080 System.err.println("Command (first argument) to instrumenter was not recognized."); 081 return false; 082 } 083 084 String[] realArgs = new String[args.length - 1]; 085 for (int i = 0; i < realArgs.length; i++) { 086 realArgs[i] = args[i + 1]; 087 } 088 Arguments arguments = readArguments(realArgs); 089 if (arguments == errorWhileReadingArguments) { 090 return false; 091 } 092 093 // Set up debug traces; note this comes after reading command line options. 094 daikon.LogHelper.setupLogs(Global.debugAll ? FINE : INFO); 095 096 // Create instrumented-classes dir. 097 File outputDir = new File(instrumented_directory); 098 099 System.out.println("Reading invariant file: " + arguments.invFile); 100 PptMap ppts; 101 try { 102 ppts = 103 FileIO.read_serialized_pptmap(new File(arguments.invFile), true /* use saved config */); 104 } catch (IOException e) { 105 System.err.println("Exception while reading invariant file " + arguments.invFile); 106 System.err.println(e.getMessage()); 107 e.printStackTrace(); 108 return false; 109 } 110 111 // Compile original sources (because daikon.tools.jtb.Ast accesses 112 // them via reflection). 113 // compile(arguments.javaFileNames, ""); 114 115 // Create filenames including temp directory and package directories. 116 List<ParseResults> parseResults = 117 ParseResults.parse(arguments.javaFileNames, true /* discard comments */); 118 119 for (ParseResults oneFile : parseResults) { 120 121 System.out.println("Instrumenting " + oneFile.fileName); 122 123 List<CheckerClass> checkerClasses = new ArrayList<>(); 124 125 for (TypeDeclaration decl : oneFile.roots) { 126 127 InstrumentVisitor v = new InstrumentVisitor(ppts, decl); 128 129 decl.accept(v); 130 131 if (createCheckerClasses) { 132 v.add_checkers_for_nondeclared_members(); 133 checkerClasses.addAll(v.checkerClasses.getCheckerClasses()); 134 } 135 } 136 137 try { 138 139 File instrumentedFileDir = 140 new File(outputDir.getPath(), oneFile.packageName.replace(".", File.separator)); 141 142 if (!instrumentedFileDir.exists()) { 143 instrumentedFileDir.mkdirs(); 144 } 145 146 File checkerClassesDir = 147 new File(checkersOutputDirName, oneFile.packageName.replace(".", File.separator)); 148 149 if (!checkerClassesDir.exists()) { 150 checkerClassesDir.mkdirs(); 151 } 152 153 // Output instrumented class 154 String instrumentedFileName = oneFile.fileName; 155 File instrumentedFile = new File(instrumentedFileDir, instrumentedFileName); 156 debug.fine("instrumented file name: " + instrumentedFile.getPath()); 157 System.out.println("Writing " + instrumentedFile); 158 try (Writer output = Files.newBufferedWriter(instrumentedFile.toPath(), UTF_8)) { 159 // Bug: JTB seems to order the modifiers in a non-standard way, 160 // such as "static final public" instead of "public static final". 161 oneFile.compilationUnit.accept(new TreeFormatter()); 162 TreeDumper dumper = new TreeDumper(output); 163 dumper.printSpecials(false); 164 oneFile.compilationUnit.accept(dumper); 165 } 166 167 // Output checker classes 168 for (CheckerClass cls : checkerClasses) { 169 String checkerClassFileName = cls.getCheckerClassName() + ".java"; 170 File checkerClassFile = new File(checkerClassesDir, checkerClassFileName); 171 System.out.println("Writing " + checkerClassFile); 172 try (Writer output = Files.newBufferedWriter(checkerClassFile.toPath(), UTF_8)) { 173 CompilationUnit cu = cls.getCompilationUnit(); 174 cu.accept(new TreeFormatter()); 175 cu.accept(new TreeDumper(output)); 176 } 177 } 178 179 } catch (IOException e) { 180 System.err.println("Exception while instrumenting " + oneFile.fileName); 181 System.err.println(e.getMessage()); 182 e.printStackTrace(); 183 return false; 184 } 185 } 186 187 return true; 188 } 189 190 @UsesObjectEquals 191 private static class Arguments { 192 public String invFile; 193 public List<String> javaFileNames; 194 195 public Arguments(String invFile, List<String> javaFileNames) { 196 this.invFile = invFile; 197 this.javaFileNames = javaFileNames; 198 } 199 } 200 201 private static Arguments errorWhileReadingArguments = 202 new Arguments("error while reading arguments", new ArrayList<String>()); 203 204 private Arguments readArguments(String[] args) { 205 206 LongOpt[] longopts = 207 new LongOpt[] { 208 new LongOpt(Daikon.debugAll_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 209 new LongOpt(Daikon.debug_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 210 new LongOpt(output_only_high_conf_invariants_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 211 new LongOpt(make_all_fields_public_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 212 new LongOpt(create_checker_classes_SWITCH, LongOpt.NO_ARGUMENT, null, 0), 213 new LongOpt(directory_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0), 214 new LongOpt(checkers_directory_SWITCH, LongOpt.REQUIRED_ARGUMENT, null, 0) 215 }; 216 Getopt g = new Getopt("daikon.tools.runtimechecker.InstrumentHandler", args, "hs", longopts); 217 int c; 218 while ((c = g.getopt()) != -1) { 219 switch (c) { 220 case 0: 221 // got a long option 222 String option_name = longopts[g.getLongind()].getName(); 223 224 if (create_checker_classes_SWITCH.equals(option_name)) { 225 createCheckerClasses = true; 226 } else if (output_only_high_conf_invariants_SWITCH.equals(option_name)) { 227 InstrumentVisitor.outputOnlyHighConfInvariants = true; 228 } else if (make_all_fields_public_SWITCH.equals(option_name)) { 229 InstrumentVisitor.makeAllFieldsPublic = true; 230 } else if (directory_SWITCH.equals(option_name)) { 231 instrumented_directory = Daikon.getOptarg(g); 232 } else if (checkers_directory_SWITCH.equals(option_name)) { 233 checkersOutputDirName = Daikon.getOptarg(g); 234 } else if (Daikon.debugAll_SWITCH.equals(option_name)) { 235 Global.debugAll = true; 236 } else if (Daikon.debug_SWITCH.equals(option_name)) { 237 daikon.LogHelper.setLevel(Daikon.getOptarg(g), FINE); 238 } else { 239 System.err.println("Unknown long option received: " + option_name); 240 } 241 break; 242 default: 243 System.out.println("unrecognized option" + c); 244 return errorWhileReadingArguments; 245 } 246 } 247 // The index of the first non-option argument -- the name of the 248 // invariant file. 249 int argindex = g.getOptind(); 250 if (argindex >= args.length) { 251 System.out.println("Error: No .inv file or .java file arguments supplied."); 252 return errorWhileReadingArguments; 253 } 254 String invfile = args[argindex]; 255 argindex++; 256 if (!(invfile.endsWith(".inv") || invfile.endsWith(".inv.gz"))) { 257 System.out.println("Error: first argument must be a file ending in .inv or .inv.gz."); 258 return errorWhileReadingArguments; 259 } 260 if (argindex >= args.length) { 261 System.out.println("Error: No .java file arguments supplied."); 262 return errorWhileReadingArguments; 263 } 264 List<String> javaFileNames = new ArrayList<>(); 265 for (; argindex < args.length; argindex++) { 266 String javafile = args[argindex]; 267 if (!javafile.endsWith(".java")) { 268 System.out.println("File does not end in .java: " + javafile); 269 return errorWhileReadingArguments; 270 } 271 javaFileNames.add(javafile); 272 } 273 274 return new Arguments(invfile, javaFileNames); 275 } 276}