Multiple args (#49)

Author: rodrigomilisse

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.
 

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");
+	}
+}

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();
+	}
+}

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<String> 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);
 

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);
     }
 

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -119,7 +119,8 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) {
                 CtLiteral<String> s = (CtLiteral<String>) 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);
                 }
             }
         }

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<CtAnnotation<? extends Annotation>> getStateAnnotation(CtEle
         // }
         // return l;
     }
-}
+}

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<Path> 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();
+        }
+    }
 }