Source code

001package daikon.test;
002
003import static java.nio.charset.StandardCharsets.UTF_8;
004import static java.util.logging.Level.INFO;
005import static org.junit.Assert.fail;
006
007import daikon.Daikon;
008import java.io.BufferedReader;
009import java.io.ByteArrayOutputStream;
010import java.io.File;
011import java.io.IOException;
012import java.io.InputStream;
013import java.io.InputStreamReader;
014import java.io.LineNumberReader;
015import java.io.OutputStream;
016import java.io.PrintStream;
017import java.util.ArrayList;
018import java.util.List;
019import junit.framework.TestSuite;
020import org.checkerframework.checker.nullness.qual.Nullable;
021import org.checkerframework.dataflow.qual.Pure;
022import org.junit.Test;
023import org.plumelib.options.Option;
024import org.plumelib.options.Options;
025
026/**
027 * This is a tester for the formatting of invariants in different modes that is configurable by file
028 * input. It can test practically any invariant in the Daikon system given the appropriate commands.
029 * The test are configured from the {@code InvariantFormatTest.commands} file and errors that occur
030 * are written to the InvariantFormatTest.diffs file. More detail on the expected formats of these
031 * files is in Daikon developer manual.
032 */
033public class InvariantFormatTester {
034
035  /**
036   * Maximum file size that can currently be examined by the program. It is arbitrary, but a length
037   * must be supplied to LineNumberReader.mark().
038   */
039  private static final int MAX_FILE_SIZE = 262144;
040
041  /** Indicates a string that when it starts a line signifies that the line is a comment. */
042  public static final String COMMENT_STARTER_STRING = ";";
043
044  /** A list containing all of the test formats. */
045  public static final List<String> TEST_FORMAT_LIST = getTestFormatList();
046
047  /** File that contains the format test commands. Must be found as a resource. */
048  private static String command_file = "InvariantFormatTest.commands";
049
050  @Option("-d File to write any differences to.  Will be deleted on success")
051  public static File diff_file = new File("InvariantFormatTest.diffs");
052
053  /** Determines whether the object will generate goal statements. */
054  @Option("-g Filename to write goals to")
055  public static @Nullable File generate_goals = null;
056
057  /**
058   * This function allows this test to be run from the command line instead of its usual method,
059   * which is through the Daikon MasterTester.
060   *
061   * @param args arguments to the main function, which control options to the program. As of now
062   *     there is only one option, "--generate_goals", which will generate goal information for the
063   *     selected tests assuming the output that the tests provide is the correct output.
064   */
065  public static void main(String[] args) {
066    daikon.LogHelper.setupLogs(INFO);
067
068    String usage = "java daikon.test.InvariantFormatTester";
069    Options options = new Options(usage, InvariantFormatTester.class);
070    String[] other_args = options.parse(true, args);
071    if (other_args.length > 0) {
072      System.out.println("unexpected arguments");
073      options.printUsage();
074      return;
075    }
076
077    junit.textui.TestRunner.run(new TestSuite(InvariantFormatTester.class));
078  }
079
080  /**
081   * This function produces the format list for intialization of the static format list variable.
082   */
083  static List<String> getTestFormatList() {
084    List<String> result = new ArrayList<>();
085
086    // Add test formats - hard coded in
087    result.add("daikon");
088    result.add("java");
089    result.add("esc");
090    result.add("jml");
091    result.add("dbc");
092    result.add("simplify");
093    result.add("csharpcontract");
094
095    return result;
096  }
097
098  /** This function is the actual function performed when this class is run through JUnit. */
099  @Test
100  public void testFormats() {
101
102    // Don't care about comparability info because we are only
103    // creating variables for the purpose of being compared (thus they
104    // should all be comparable)
105    Daikon.ignore_comparability = true;
106
107    // run the actual test
108
109    if (!execute()) {
110      fail("At least one test failed. Inspect " + diff_file + " for error report.");
111    }
112  }
113
114  /**
115   * Returns the next non-comment, non-whitespace line of the input buffer.
116   *
117   * @param input the input buffer
118   * @return the next non-comment, non-whitespace line of the input buffer or null if the end of the
119   *     buffer is reached before such a line can be found
120   */
121  static @Nullable String getNextRealLine(BufferedReader input) {
122    String currentLine = "";
123
124    try {
125      while (currentLine != null) {
126        currentLine = input.readLine();
127        if (currentLine != null && !isComment(currentLine) && !isWhitespace(currentLine)) {
128          return currentLine;
129        }
130      }
131    } catch (IOException e) {
132      throw new RuntimeException(e.toString());
133    }
134    return null;
135  }
136
137  /**
138   * This function performs the testing for a particular format indicated by the format string. It
139   * subsequently sets up appropriate input and output streams for the format test, performs the
140   * test, and the compares the test results to the goals. If the goals differ from the actual
141   * results the test fails.
142   */
143  private boolean execute() {
144
145    // Open the input stream.
146    InputStream inputStream = InvariantFormatTester.class.getResourceAsStream(command_file);
147    if (inputStream == null) {
148      fail(
149          "Input file for invariant format tests missing."
150              + " (Should be in "
151              + command_file
152              + " and it must be within the classpath)");
153      throw new Error("This can't happen"); // to quiet Findbugs
154    }
155    LineNumberReader commandReader =
156        new LineNumberReader(new InputStreamReader(inputStream, UTF_8));
157
158    // Create a stream for the output
159    OutputStream out = new ByteArrayOutputStream();
160    boolean result;
161
162    // Run the test
163    try {
164      result = performTest(commandReader, new PrintStream(out));
165    } catch (Throwable e) {
166      throw new RuntimeException(
167          "Error detected on line "
168              + commandReader.getLineNumber()
169              + " of "
170              + InvariantFormatTester.class.getResource(command_file),
171          e);
172    }
173
174    // Close the command file
175    try {
176      inputStream.close();
177    } catch (IOException e) {
178      // Can't write the goals into the commands file if it can't be cleared,
179      // otherwise not important.  Only matters if output file is the same
180      // as the input file
181      if (generate_goals != null) {
182        throw new RuntimeException(
183            "Can't close commands file " + InvariantFormatTester.class.getResource(command_file));
184      }
185    }
186
187    // Get all of the output as a string
188    String output = out.toString();
189
190    // If we are generating a new goal file
191    if (generate_goals != null) {
192
193      // Create the goal file and write the output to it
194      try {
195        PrintStream out_fp = new PrintStream(generate_goals);
196        out_fp.printf("%s", output);
197        out_fp.close();
198        System.out.println("Goals generated");
199      } catch (Exception e) {
200        throw new RuntimeException("Can't write goal file " + generate_goals, e);
201      }
202    } else { // handle any differences
203
204      // Delete any previous diffs
205      diff_file.delete();
206
207      // If the test failed, write the differences to the diff file
208      if (!result) {
209        try {
210          PrintStream diff_fp = new PrintStream(diff_file);
211          diff_fp.printf("%s", output);
212          diff_fp.close();
213        } catch (Exception e) {
214          throw new RuntimeException("Can't write diff file " + diff_file, e);
215        }
216        return false;
217      }
218    }
219    return true;
220  }
221
222  /**
223   * This function performs an individual formatting test after the input and output streams have
224   * been created.
225   *
226   * @param commands the input that decides which tests to perform
227   * @param output the place to where the test output is written
228   */
229  private boolean performTest(LineNumberReader commands, PrintStream output) {
230    List<FormatTestCase> invariantTestCases = new ArrayList<>();
231    boolean noTestFailed = true;
232
233    // Need to be able to go to beginning of buffer for combining goals with the input
234    if (generate_goals != null) {
235      try {
236        commands.mark(MAX_FILE_SIZE);
237      } catch (IOException e) {
238        throw new RuntimeException("Cannot mark file in order to generate goals");
239      }
240    }
241
242    while (true) {
243      // Create a new test case
244      FormatTestCase currentCase = FormatTestCase.readFromFile(commands, (generate_goals != null));
245      if (currentCase == null) {
246        break;
247      } else {
248        invariantTestCases.add(currentCase);
249        if ((generate_goals == null) && !currentCase.passes()) {
250          output.print(currentCase.getDiffString());
251          noTestFailed = false;
252        }
253      }
254    }
255
256    if (generate_goals != null) {
257
258      // Go to beginning of the commands buffer
259      try {
260        commands.reset();
261      } catch (IOException e) {
262        throw new RuntimeException("Cannot reset to mark, thus cannot write goals");
263      }
264
265      String debugTemp;
266
267      try {
268        for (FormatTestCase currentCase : invariantTestCases) {
269          // System.out.println("Goal output #" + i);
270          debugTemp = currentCase.generateGoalOutput(commands);
271          // System.out.println(debugTemp);
272
273          output.println(debugTemp);
274        }
275
276        String currentLineOfText = commands.readLine();
277
278        while (currentLineOfText != null) {
279          if (FormatTestCase.parseGoal(currentLineOfText) == null) {
280            output.println(currentLineOfText);
281          }
282          currentLineOfText = commands.readLine();
283        }
284      } catch (IOException e) {
285        throw new RuntimeException("Writing goal output failed");
286      }
287    }
288    return noTestFailed;
289  }
290
291  /**
292   * Determines whether a line is a comment or not.
293   *
294   * @param line the line in question
295   * @return true if the line is a comment (that is, not to be interpretted as a command); false
296   *     otherwise
297   */
298  @Pure
299  static boolean isComment(String line) {
300    return line.startsWith(COMMENT_STARTER_STRING);
301  }
302
303  /**
304   * Determines whether a given line is made only of whitespace.
305   *
306   * @param line the line in question
307   * @return true if the line is made up only of whitespace, false otherwise
308   */
309  @Pure
310  static boolean isWhitespace(String line) {
311    for (int x = 0; x < line.length(); x++) {
312      if (!Character.isWhitespace(line.charAt(x))) {
313        return false;
314      }
315    }
316    return true;
317  }
318}