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. 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(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 81c681bd..b7471a36 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -1,7 +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; import spoon.Launcher; @@ -12,35 +13,36 @@ 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.")); } - 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("[\\[\\]]", "")); - 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; - } - 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 @@ -51,12 +53,10 @@ public static ErrorEmitter launch(String path) { // launcher.getEnvironment().setSourceClasspath( // "lib1.jar:lib2.jar".split(":")); launcher.getEnvironment().setComplianceLevel(8); - launcher.run(); final Factory factory = launcher.getFactory(); final ProcessingManager processingManager = new QueueProcessingManager(factory); - final RefinementProcessor processor = new RefinementProcessor(factory, ee); processingManager.addProcessor(processor); 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 46eb254f..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 @@ -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); @@ -634,4 +631,4 @@ private static List> getStateAnnotation(CtEle // } // return l; } -} +} \ No newline at end of file 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(); + } + } }