diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java index b79eaa87..6d0fd1fd 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java @@ -2,7 +2,7 @@ import liquidjava.specification.ExternalRefinementsFor; -@ExternalRefinementsFor("non.existent.Class") +@ExternalRefinementsFor("non.existent.Class") // Warning public interface WarningExtRefNonExistentClass { public void NonExistentClass(); } diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java index 08d81de9..e1794c58 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java @@ -12,5 +12,5 @@ public interface WarningExtRefNonExistentMethod { public void ArrayList(); @StateRefinement(to = "size(this) == (size(old(this)) + 1)") - public boolean adddd(E e); + public boolean adddd(E e); // Warning } diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java index 576a70e9..76b0a4c4 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java @@ -9,7 +9,7 @@ public interface WarningExtRefWrongConstructor { @StateRefinement(to = "size(this) == 0") - public void ArrayList(String wrongParameter); + public void ArrayList(String wrongParameter); // Warning @StateRefinement(to = "size(this) == (size(old(this)) + 1)") public boolean add(E e); diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java index 988c465f..5b31471b 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java @@ -12,5 +12,5 @@ public interface WarningExtRefWrongParameterType { public void ArrayList(); @StateRefinement(to = "size(this) == (size(old(this)) + 1)") - public boolean add(int wrongParameter); + public boolean add(int wrongParameter); // Warning } diff --git a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java index 97477b2a..61994d53 100644 --- a/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java @@ -12,5 +12,5 @@ public interface WarningExtRefWrongRetType { public void ArrayList(); @StateRefinement(to = "size(this) == (size(old(this)) + 1)") - public int add(E e); // wrong return type + public int add(E e); // Warning } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java index e739915f..f088afbe 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -8,11 +8,13 @@ import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; +import java.util.Collection; import java.util.List; import java.util.stream.Stream; import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.LJDiagnostic; import liquidjava.diagnostics.errors.LJError; import liquidjava.utils.Pair; @@ -25,11 +27,7 @@ public class TestExamples { Diagnostics diagnostics = Diagnostics.getInstance(); /** - * Test the file at the given path by launching the verifier and checking for errors. The file/directory is expected - * to be either correct or contain an error based on its name. - * - * @param path - * path to the file to test + * Runs the verifier and checks the expected diagnostics */ @ParameterizedTest @MethodSource("sourcePaths") @@ -40,6 +38,14 @@ public void testPath(final Path path) { // run verification CommandLineLauncher.launch(path.toFile().toString()); + List> expectedWarnings = isDirectory ? getExpectedWarningsFromDirectory(path) + : getExpectedWarningsFromFile(path); + + if (shouldWarn(pathName)) { + checkExpectedDiagnostics(pathName, diagnostics.getWarnings(), expectedWarnings, + diagnostics.getWarningOutput()); + } + // verification should pass, check if any errors were found if (shouldPass(pathName) && diagnostics.foundError()) { System.out.println("Error in: " + pathName + " --- should pass but an error was found. \n" @@ -56,55 +62,58 @@ else if (shouldFail(pathName)) { // check if expected error was found List> expectedErrors = isDirectory ? getExpectedErrorsFromDirectory(path) : getExpectedErrorsFromFile(path); - if (diagnostics.getErrors().size() != expectedErrors.size()) { - System.out.println("Multiple errors found in: " + pathName + " --- expected exactly " - + expectedErrors.size() + " errors. \n" + diagnostics.getErrorOutput()); - fail(); - } - if (!expectedErrors.isEmpty()) { - for (LJError e : diagnostics.getErrors()) { - String foundError = e.getTitle(); - int errorPosition = e.getPosition().getLine(); - boolean match = expectedErrors.stream().anyMatch( - expected -> expected.first().equals(foundError) && expected.second() == errorPosition); - - if (!match) { - System.out.println("Error in: " + pathName + " --- expected errors: " + expectedErrors - + ", but found: " + foundError + " at " + errorPosition + ". \n" - + diagnostics.getErrorOutput()); - fail(); - } - } - } else { - System.out.println("No expected error messages found for: " + pathName); - System.out.println( - "Please specify each expected error in the test file as a comment on the line where the error should be reported."); - fail(); - } + checkExpectedDiagnostics(pathName, diagnostics.getErrors(), expectedErrors, + diagnostics.getErrorOutput()); + } + } + } + + /** + * Checks that the found diagnostics match the expected diagnostics + */ + private static void checkExpectedDiagnostics(String pathName, Collection found, + List> expected, String output) { + if (found.size() != expected.size()) { + System.out.println("Unexpected number of diagnostics found in: " + pathName + " --- expected exactly " + + expected.size() + ". \n" + output); + fail(); + } + if (expected.isEmpty()) { + System.out.println("No expected diagnostic messages found for: " + pathName); + System.out.println( + "Please specify each expected diagnostic in the test file as a comment on the line where it should be reported."); + fail(); + } + for (LJDiagnostic diagnostic : found) { + boolean match = expected.stream().anyMatch(expectedDiagnostic -> matches(diagnostic, expectedDiagnostic)); + if (!match) { + System.out.println( + "Unexpected diagnostic in: " + pathName + " --- expected: " + expected + ". \n" + output); + fail(); } } } + private static boolean matches(LJDiagnostic diagnostic, Pair expected) { + if (diagnostic.getPosition().getLine() != expected.second()) + return false; + return !(diagnostic instanceof LJError) || diagnostic.getTitle().equals(expected.first()); + } + /** - * Returns a Stream of paths to test files in the testSuite directory. These include files with names starting with - * "Correct" or "Error", and directories containing "correct" or "error". ยง - * - * @return Stream of paths to test files - * - * @throws IOException - * if an I/O error occurs or the path does not exist + * Returns the test suite paths to verify */ private static Stream sourcePaths() throws IOException { return Files.find(Paths.get("../liquidjava-example/src/main/java/testSuite/"), Integer.MAX_VALUE, (filePath, fileAttr) -> { String name = filePath.getFileName().toString(); - // Files that start with "Correct" or "Error" + // Files that start with "Correct", "Error" or "Warning" boolean isFileStartingWithCorrectOrError = fileAttr.isRegularFile() - && (shouldPass(name) || shouldFail(name)); + && (shouldPass(name) || shouldFail(name) || shouldWarn(name)); - // Directories that contain "correct" or "error" + // Directories that contain "correct", "error" or "warning" boolean isDirectoryWithCorrectOrError = fileAttr.isDirectory() - && (shouldPass(name) || shouldFail(name)); + && (shouldPass(name) || shouldFail(name) || shouldWarn(name)); // Return true if either condition matches return isFileStartingWithCorrectOrError || isDirectoryWithCorrectOrError; @@ -112,8 +121,7 @@ private static Stream sourcePaths() throws IOException { } /** - * Test multiple paths at once, including both files and directories. This test ensures that the verifier can handle - * multiple inputs correctly and that no errors are found in files/directories that are expected to be correct. + * Verifies that multiple correct inputs can be processed together */ @Test public void testMultiplePaths() { diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index f81f013f..33ee09b2 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -16,81 +16,70 @@ public class TestUtils { + private static final Pattern EXPECTED_DIAGNOSTIC = Pattern.compile("//\\s*(.*?\\b(Error|Warning)\\b)", Pattern.CASE_INSENSITIVE); private final static Factory factory = new Launcher().getFactory(); private final static Context context = Context.getInstance(); - /** - * Determines if the given path indicates that the test should pass - * - * @param path - */ public static boolean shouldPass(String path) { return path.toLowerCase().contains("correct"); } - /** - * Determines if the given path indicates that the test should fail - * - * @param path - */ public static boolean shouldFail(String path) { return path.toLowerCase().contains("error"); } - /** - * Reads the expected error messages from the given file by looking for a comment containing the expected error - * message. - * - * @param filePath - * - * @return list of expected error messages found in the file, or empty list if there was an error reading the file - * or if there are no expected error messages in the file - */ + public static boolean shouldWarn(String path) { + return path.toLowerCase().contains("warning"); + } + public static List> getExpectedErrorsFromFile(Path filePath) { - List> expectedErrors = new ArrayList<>(); + return getExpectedDiagnosticsFromFile(filePath, "error"); + } + + private static List> getExpectedDiagnosticsFromFile(Path filePath, String type) { + List> expectedDiagnostics = new ArrayList<>(); try (BufferedReader reader = Files.newBufferedReader(filePath)) { String line; int lineNumber = 0; while ((line = reader.readLine()) != null) { lineNumber++; - Pattern p = Pattern.compile("//\\s*(.*?\\bError\\b)", Pattern.CASE_INSENSITIVE); - Matcher m = p.matcher(line); - if (m.find()) { - expectedErrors.add(new Pair<>(m.group(1).trim(), lineNumber)); + Matcher matcher = EXPECTED_DIAGNOSTIC.matcher(line); + if (matcher.find() && matcher.group(2).equalsIgnoreCase(type)) { + expectedDiagnostics.add(new Pair<>(matcher.group(1).trim(), lineNumber)); } } } catch (IOException e) { return List.of(); } - return expectedErrors; + return expectedDiagnostics; + } + + public static List> getExpectedWarningsFromFile(Path filePath) { + return getExpectedDiagnosticsFromFile(filePath, "warning"); } - /** - * Reads the expected error messages from all files in the given directory and combines them into a single list - * - * @param dirPath - * - * @return list of expected error messages from all files in the directory, or empty list if there was an error - * reading the directory or if there are no files in the directory - */ public static List> getExpectedErrorsFromDirectory(Path dirPath) { - List> expectedErrors = new ArrayList<>(); + return getExpectedDiagnosticsFromDirectory(dirPath, "error"); + } + + public static List> getExpectedWarningsFromDirectory(Path dirPath) { + return getExpectedDiagnosticsFromDirectory(dirPath, "warning"); + } + + private static List> getExpectedDiagnosticsFromDirectory(Path dirPath, String type) { + List> expectedDiagnostics = new ArrayList<>(); try { List files = Files.list(dirPath).filter(Files::isRegularFile).toList(); for (Path file : files) { - expectedErrors.addAll(getExpectedErrorsFromFile(file)); + expectedDiagnostics.addAll(getExpectedDiagnosticsFromFile(file, type)); } } catch (IOException e) { return List.of(); } - return expectedErrors; + return expectedDiagnostics; } - /** - * Helper method to add an integer variable to the context - */ public static void addIntVariableToContext(String name) { - context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(), - factory.Code().createCodeSnippetStatement("")); + context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(), factory.Code().createCodeSnippetStatement("")); } }