From 7575e5ad2d04b80854f4f65261af9fa5d7364a78 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?M=C3=A1rcio=20Caetano?= Date: Tue, 22 Jul 2025 21:29:49 +0100 Subject: [PATCH 1/9] added support to analyze multiple folders --- .../liquidjava/api/CommandLineLauncher.java | 38 +++++++++++-------- 1 file changed, 23 insertions(+), 15 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 81c681bd..93149918 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -1,6 +1,8 @@ package liquidjava.api; import java.io.File; +import java.util.Arrays; +import java.util.List; import liquidjava.errors.ErrorEmitter; import liquidjava.processor.RefinementProcessor; @@ -12,14 +14,21 @@ public class CommandLineLauncher { public static void main(String[] args) { - String allPath = "./liquidjava-example/src/main/java/test/currentlyTesting"; - // String allPath = "C://Regen/test-projects/src/Main.java"; // In eclipse only needed this:"../liquidjava-example/src/main/java/" // In VSCode needs: // "../liquidjava/liquidjava-umbrella/liquidjava-example/src/main/java/liquidjava/test/project"; - String path = args.length == 0 ? allPath : args[0]; - ErrorEmitter ee = launch(path); + + if (args.length == 0) { + System.out.println("No input files or directories provided"); + System.out.println("\nUsage: ./liquidjava <...paths>"); + System.out.println(" <...paths>: Paths to files or directories to be verified by LiquidJava"); + System.out.println( + "\nExample: ./liquidjava liquidjava-example/src/main/java/test/currentlyTesting liquidjava-example/src/main/java/testingInProgress/Account.java"); + return; + } + List paths = Arrays.asList(args); + ErrorEmitter ee = launch(paths.toArray(new String[0])); System.out.println(ee.foundError() ? (ee.getFullMessage()) : ("Correct! Passed Verification.")); } @@ -28,19 +37,18 @@ public static ErrorEmitter launchTest(String path) { return ee; } - public static ErrorEmitter launch(String path) { - System.out.println("Running LiquidJava on: " + path); - ErrorEmitter ee = new ErrorEmitter(); - - // check if the path exists - File f = new File(path); - if (!f.exists()) { - ee.addError("Path not found", "The path " + path + " does not exist", 1); - return ee; - } + public static ErrorEmitter launch(String... paths) { + System.out.println("Running LiquidJava on: " + Arrays.toString(paths).replaceAll("[\\[\\]]", "")); + ErrorEmitter ee = new ErrorEmitter(); Launcher launcher = new Launcher(); - launcher.addInputResource(path); + for (String path : paths) { + if (!new File(path).exists()) { + ee.addError("Path not found", "The path " + path + " does not exist", 1); + return ee; + } + launcher.addInputResource(path); + } launcher.getEnvironment().setNoClasspath(true); // Get the current classpath from the system From b9a8f5d42ecd272f3675248d2e3642bf3de53640 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?M=C3=A1rcio=20Caetano?= Date: Wed, 23 Jul 2025 01:30:39 +0100 Subject: [PATCH 2/9] allowed support for verifying refinements declared in a separate package --- .../liquidjava/api/CommandLineLauncher.java | 2 +- .../object_checkers/AuxStateHandler.java | 29 +++++++++---------- 2 files changed, 14 insertions(+), 17 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 93149918..764dce2a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -18,7 +18,7 @@ public static void main(String[] args) { // In eclipse only needed this:"../liquidjava-example/src/main/java/" // In VSCode needs: // "../liquidjava/liquidjava-umbrella/liquidjava-example/src/main/java/liquidjava/test/project"; - + if (args.length == 0) { System.out.println("No input files or directories provided"); System.out.println("\nUsage: ./liquidjava <...paths>"); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 46eb254f..9c4974d9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -551,24 +551,21 @@ private static String addInstanceWithState(TypeChecker tc, String superName, Str prevInstance.getRefinement(), invocation); // vi2.setState(transitionedState); vi2.setRefinement(transitionedState); - RefinedVariable rv = superName != null ? tc.getContext().getVariableByName(superName) : null; - if (rv != null) { - // propagate supertypes from the refined variable - for (CtTypeReference t : rv.getSuperTypes()) + Context ctx = tc.getContext(); + if (ctx.hasVariable(superName)) { + RefinedVariable rv = ctx.getVariableByName(superName); + for (CtTypeReference t : rv.getSuperTypes()) { vi2.addSuperType(t); - } else { - // propagate supertypes from the previous instance - for (CtTypeReference t : prevInstance.getSuperTypes()) - vi2.addSuperType(t); - } + } - // if the variable is a parent (not a VariableInstance) we need to check that - // this refinement - // is a subtype of the variable's main refinement - if (rv instanceof Variable) { - Predicate superC = rv.getMainRefinement().substituteVariable(rv.getName(), vi2.getName()); - tc.checkSMT(superC, invocation); - tc.getContext().addRefinementInstanceToVariable(superName, name2); + // if the variable is a parent (not a VariableInstance) we need to check that + // this refinement + // is a subtype of the variable's main refinement + if (rv instanceof Variable) { + Predicate superC = rv.getMainRefinement().substituteVariable(rv.getName(), vi2.getName()); + tc.checkSMT(superC, invocation); + tc.getContext().addRefinementInstanceToVariable(superName, name2); + } } invocation.putMetadata(tc.TARGET_KEY, vi2); From ae73f92753b6e34392584a34178f4b1aabcd18d0 Mon Sep 17 00:00:00 2001 From: rodrigomilisse Date: Thu, 10 Jul 2025 11:51:52 +0100 Subject: [PATCH 3/9] added basic support for boolean ghost variables --- .../refinement_checker/object_checkers/AuxStateHandler.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 9c4974d9..aee9fd78 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -81,9 +81,13 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) { Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), s), Predicate.createLit("0", Utils.INT)); c = Predicate.createConjunction(c, p); + } else if (sg.getReturnType().toString().equals("boolean")) { + Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s), + Predicate.createLit("false", Utils.BOOLEAN)); + c = Predicate.createConjunction(c, p); } else { // TODO: Implement other stuff - throw new RuntimeException("Ghost Functions not implemented for other types than int -> implement in" + throw new RuntimeException("Ghost Functions not implemented for other types than int/boolean -> implement in" + " AuxStateHandler defaultState"); } } From fafb05068e6cb63d135377a55d102acea6204ccc Mon Sep 17 00:00:00 2001 From: rodrigomilisse Date: Fri, 11 Jul 2025 15:56:43 +0100 Subject: [PATCH 4/9] added elementary testing for boolean ghost variables --- .../testBooleanGhost/BooleanGhostClass.java | 39 +++++++++++++++++++ .../testBooleanGhost/BooleanGhostTest.java | 12 ++++++ 2 files changed, 51 insertions(+) create mode 100644 liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java create mode 100644 liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java diff --git a/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java b/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java new file mode 100644 index 00000000..1c08c349 --- /dev/null +++ b/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostClass.java @@ -0,0 +1,39 @@ +package testBooleanGhost; + +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@Ghost("boolean opened") +@Ghost("boolean closed") +public class BooleanGhostClass { + + boolean opened; + boolean closed; + + @StateRefinement(from = "!opened(this) && !closed(this)", to = "opened(this) && !closed(this)") + void open() { + opened = true; + } + + @StateRefinement(from = "opened(this) && !closed(this)") + void execute() { + // System.out.println("opened:" + open + "\nclosed::" + closed); // lança + // exceção + + System.out.println("opened: "); + System.out.println(opened); + System.out.println("\nclosed: "); + System.out.println(closed); + + } + + @StateRefinement(from = "opened(this) && !closed(this)", to = "opened(this) && closed(this)") + void close() { + closed = true; + } + + @StateRefinement(from = "opened(this) && closed(this)") + void terminate() { + System.out.println("Terminating\n"); + } +} diff --git a/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java b/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java new file mode 100644 index 00000000..e8a07d82 --- /dev/null +++ b/liquidjava-example/src/main/java/testBooleanGhost/BooleanGhostTest.java @@ -0,0 +1,12 @@ +package testBooleanGhost; + +public class BooleanGhostTest { + public static void main(String[] args) { + BooleanGhostClass bgc = new BooleanGhostClass(); + + bgc.open(); // ccomment out for error + bgc.execute(); + bgc.close(); // comment out for error + bgc.terminate(); + } +} From 542073dbe81812dbbcaa4389a6a0e6f420ae1c3d Mon Sep 17 00:00:00 2001 From: Paulo Santos Date: Sun, 6 Jul 2025 20:17:53 +0100 Subject: [PATCH 5/9] Fixed typo --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index cf2aa782..17d44069 100644 --- a/README.md +++ b/README.md @@ -55,6 +55,8 @@ To run LiquidJava, use the Maven command below, replacing `/path/to/your/project ```bash mvn exec:java -pl liquidjava-verifier -Dexec.mainClass="liquidjava.api.CommandLineLauncher" -Dexec.args="/path/to/your/project" ``` +*Warning: Any change to LiquidJava requires rebuilding the jar.* + If you're on Linux/macOS, you can use the `liquidjava` script (from the repository root) to simplify the process. From c22c8dbd6e9cffbb4d6915e1b366c1cd4ea679bc Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 9 Oct 2025 11:53:34 +0100 Subject: [PATCH 6/9] Minor Improvements to CommandLineLauncher --- .../src/main/java/liquidjava/api/CommandLineLauncher.java | 1 - 1 file changed, 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 764dce2a..404cad1c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -8,7 +8,6 @@ import liquidjava.processor.RefinementProcessor; import spoon.Launcher; import spoon.processing.ProcessingManager; -import spoon.reflect.declaration.CtPackage; import spoon.reflect.factory.Factory; import spoon.support.QueueProcessingManager; From 63358cf8687474de7f388d5bba88640ee9244bc6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 9 Oct 2025 13:44:29 +0100 Subject: [PATCH 7/9] Merge with #54 and #55 --- .../liquidjava/api/CommandLineLauncher.java | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 404cad1c..22e59c51 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -3,11 +3,11 @@ import java.io.File; import java.util.Arrays; import java.util.List; - import liquidjava.errors.ErrorEmitter; import liquidjava.processor.RefinementProcessor; import spoon.Launcher; import spoon.processing.ProcessingManager; +import spoon.reflect.declaration.CtPackage; import spoon.reflect.factory.Factory; import spoon.support.QueueProcessingManager; @@ -31,11 +31,6 @@ public static void main(String[] args) { System.out.println(ee.foundError() ? (ee.getFullMessage()) : ("Correct! Passed Verification.")); } - public static ErrorEmitter launchTest(String path) { - ErrorEmitter ee = launch(path); - return ee; - } - public static ErrorEmitter launch(String... paths) { System.out.println("Running LiquidJava on: " + Arrays.toString(paths).replaceAll("[\\[\\]]", "")); @@ -63,7 +58,6 @@ public static ErrorEmitter launch(String... paths) { final Factory factory = launcher.getFactory(); final ProcessingManager processingManager = new QueueProcessingManager(factory); - final RefinementProcessor processor = new RefinementProcessor(factory, ee); processingManager.addProcessor(processor); @@ -79,4 +73,13 @@ public static ErrorEmitter launch(String... paths) { return ee; } + + /** + * Launch the LiquidJava verifier on the given file or directory path (for testing purposes) + * @param path Path to to be verified + * @return ErrorEmitter containing any errors found during verification + */ + public static ErrorEmitter launchTest(String path) { + return launch(path); + } } From da868c7e5098a22b1523191d9517aa429afc2328 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 9 Oct 2025 14:01:25 +0100 Subject: [PATCH 8/9] Add Test for Multiple Paths --- .../liquidjava/api/CommandLineLauncher.java | 10 --------- .../liquidjava/api/tests/TestExamples.java | 21 ++++++++++++++++++- 2 files changed, 20 insertions(+), 11 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 22e59c51..b7471a36 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -53,7 +53,6 @@ public static ErrorEmitter launch(String... paths) { // launcher.getEnvironment().setSourceClasspath( // "lib1.jar:lib2.jar".split(":")); launcher.getEnvironment().setComplianceLevel(8); - launcher.run(); final Factory factory = launcher.getFactory(); @@ -73,13 +72,4 @@ public static ErrorEmitter launch(String... paths) { return ee; } - - /** - * Launch the LiquidJava verifier on the given file or directory path (for testing purposes) - * @param path Path to to be verified - * @return ErrorEmitter containing any errors found during verification - */ - public static ErrorEmitter launchTest(String path) { - return launch(path); - } } 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 223907e3..a1c627f9 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -9,6 +9,8 @@ import java.util.stream.Stream; import liquidjava.api.CommandLineLauncher; import liquidjava.errors.ErrorEmitter; + +import org.junit.Test; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; @@ -27,7 +29,7 @@ public void testFile(final Path filePath) { String fileName = filePath.getFileName().toString(); // 1. Run the verifier on the file or package - ErrorEmitter errorEmitter = CommandLineLauncher.launchTest(filePath.toAbsolutePath().toString()); + ErrorEmitter errorEmitter = CommandLineLauncher.launch(filePath.toAbsolutePath().toString()); // 2. Check if the file is correct or contains an error if ((fileName.startsWith("Correct") && errorEmitter.foundError()) @@ -68,4 +70,21 @@ private static Stream fileNameSource() throws IOException { return isFileStartingWithCorrectOrError || isDirectoryWithCorrectOrError; }); } + + /** + * 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. + */ + @Test + public void testMultiplePaths() { + String[] paths = { "../liquidjava-example/src/main/java/testSuite/SimpleTest.java", + "../liquidjava-example/src/main/java/testSuite/classes/arraylist_correct", }; + ErrorEmitter errorEmitter = CommandLineLauncher.launch(paths); + + // Check if any of the paths that should be correct found an error + if (errorEmitter.foundError()) { + System.out.println("Error found in files that should be correct."); + fail(); + } + } } From 9d3344e46e52c430aade53ef648b1f387d968683 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 9 Oct 2025 14:07:46 +0100 Subject: [PATCH 9/9] Fix AuxStateHandler --- .../src/main/java/liquidjava/errors/ErrorHandler.java | 2 +- .../processor/refinement_checker/TypeChecker.java | 3 ++- .../object_checkers/AuxStateHandler.java | 8 ++------ 3 files changed, 5 insertions(+), 8 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java index f7a242d0..b17f51b4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java @@ -181,7 +181,7 @@ public static void printCostumeError(CtElement element, String msg, ErrorEmitter sb.append(element + "\n\n"); sb.append("Location: " + element.getPosition() + "\n"); sb.append("______________________________________________________\n"); - + errorl.addError(s, sb.toString(), element.getPosition(), 1); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index a535137d..56cf6248 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -119,7 +119,8 @@ private void createStateSet(CtNewArray e, int set, CtElement element) { CtLiteral s = (CtLiteral) ce; String f = s.getValue(); if (Character.isUpperCase(f.charAt(0))) { - ErrorHandler.printCostumeError(s, "State name must start with lowercase in '" + f + "'", errorEmitter); + ErrorHandler.printCostumeError(s, "State name must start with lowercase in '" + f + "'", + errorEmitter); } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index aee9fd78..fa0f00da 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -81,13 +81,9 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) { Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), s), Predicate.createLit("0", Utils.INT)); c = Predicate.createConjunction(c, p); - } else if (sg.getReturnType().toString().equals("boolean")) { - Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s), - Predicate.createLit("false", Utils.BOOLEAN)); - c = Predicate.createConjunction(c, p); } else { // TODO: Implement other stuff - throw new RuntimeException("Ghost Functions not implemented for other types than int/boolean -> implement in" + throw new RuntimeException("Ghost Functions not implemented for other types than int -> implement in" + " AuxStateHandler defaultState"); } } @@ -635,4 +631,4 @@ private static List> getStateAnnotation(CtEle // } // return l; } -} +} \ No newline at end of file