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}