Add Missing this Binding + Method Checking Ordering (#190)

Author: rcosta358

liquidjava-example/src/main/java/testSuite/classes/downloader_correct/Downloader.java

@@ -0,0 +1,23 @@
+package testSuite.classes.downloader_correct;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@Ghost("int progress")
+@StateSet({"created", "downloading", "completed"})
+public class Downloader {
+
+    @StateRefinement(to="created(this) && progress(this) == 0")
+    public Downloader() {}
+
+    @StateRefinement(from="created(this) && progress(this) == 0", to="downloading(this) && progress(this) == 0")
+    public void start() {}
+
+    @StateRefinement(from="downloading(this)", to="downloading(this) && progress(this) == percentage")
+    public void update(@Refinement("percentage > progress(this)") int percentage) {}
+
+    @StateRefinement(from="downloading(this) && progress(this) == 100", to="completed(this)")
+    public void finish() {}
+}

liquidjava-example/src/main/java/testSuite/classes/downloader_correct/SimpleTest.java

@@ -0,0 +1,11 @@
+package testSuite.classes.downloader_correct;
+
+public class SimpleTest {
+    public static void main(String[] args) {
+        Downloader d = new Downloader();
+        d.start();
+        d.update(50);
+        d.update(100);
+        d.finish();
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/Downloader.java

@@ -0,0 +1,23 @@
+package testSuite.classes.downloader_refinement_error;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@Ghost("int progress")
+@StateSet({"created", "downloading", "completed"})
+public class Downloader {
+
+    @StateRefinement(to="created(this) && progress(this) == 0")
+    public Downloader() {}
+
+    @StateRefinement(from="created(this) && progress(this) == 0", to="downloading(this) && progress(this) == 0")
+    public void start() {}
+
+    @StateRefinement(from="downloading(this)", to="downloading(this) && progress(this) == percentage")
+    public void update(@Refinement("percentage > progress(this)") int percentage) {}
+
+    @StateRefinement(from="downloading(this) && progress(this) == 100", to="completed(this)")
+    public void finish() {}
+}

liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/SimpleTest.java

@@ -0,0 +1,10 @@
+package testSuite.classes.downloader_refinement_error;
+
+public class SimpleTest {
+    public static void main(String[] args) {
+        Downloader d = new Downloader();
+        d.start();
+        d.update(50);
+        d.update(40); // Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/Downloader.java

@@ -0,0 +1,23 @@
+package testSuite.classes.downloader_state_refinement_error;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.Refinement;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@Ghost("int progress")
+@StateSet({"created", "downloading", "completed"})
+public class Downloader {
+
+    @StateRefinement(to="created(this) && progress(this) == 0")
+    public Downloader() {}
+
+    @StateRefinement(from="created(this) && progress(this) == 0", to="downloading(this) && progress(this) == 0")
+    public void start() {}
+
+    @StateRefinement(from="downloading(this)", to="downloading(this) && progress(this) == percentage")
+    public void update(@Refinement("percentage > progress(this)") int percentage) {}
+
+    @StateRefinement(from="downloading(this) && progress(this) == 100", to="completed(this)")
+    public void finish() {}
+}

liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/SimpleTest.java

@@ -0,0 +1,10 @@
+package testSuite.classes.downloader_state_refinement_error;
+
+public class SimpleTest {
+    public static void main(String[] args) {
+        Downloader d = new Downloader();
+        d.start();
+        d.update(50);
+        d.finish(); // State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -286,16 +286,22 @@ private Map<String, String> checkInvocationRefinements(CtElement invocation, Lis
             return new HashMap<>();
         Map<String, String> map = mapInvocation(arguments, f);
 
-        if (target != null) {
-            AuxStateHandler.checkTargetChanges(rtc, f, target, map, invocation);
-        }
+        if (target != null)
+            AuxStateHandler.prepareInvocationTarget(rtc, target, invocation);
+
         if (f.allRefinementsTrue()) {
+            if (target != null)
+                AuxStateHandler.checkTargetChanges(rtc, f, target, map, invocation);
+
             invocation.putMetadata(Keys.REFINEMENT, new Predicate());
             return map;
         }
 
         checkParameters(invocation, arguments, f, map);
 
+        if (target != null)
+            AuxStateHandler.checkTargetChanges(rtc, f, target, map, invocation);
+
         // -- Part 2: Apply changes
         // applyRefinementsToArguments(element, arguments, f, map);
         Predicate methodRef = f.getRefReturn();

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -212,6 +212,7 @@ private static Predicate createStatePredicate(String value, String targetClass,
         CtTypeReference<?> r = tc.getFactory().Type().createReference(targetClass);
         String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
         String name = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
+        tc.getContext().addVarToContext(Keys.THIS, r, new Predicate(), e);
         tc.getContext().addVarToContext(name, r, new Predicate(), e);
         tc.getContext().addVarToContext(nameOld, r, new Predicate(), e);
         // TODO REVIEW!!
@@ -355,7 +356,7 @@ public static void addStateRefinements(TypeChecker tc, String varName, CtExpress
      */
     public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpression<?> target2,
             Map<String, String> map, CtElement invocation) throws LJError {
-        String parentTargetName = searchFistVariableTarget(tc, target2, invocation);
+        String parentTargetName = prepareInvocationTarget(tc, target2, invocation);
         VariableInstance target = getTarget(invocation);
         if (target != null) {
             if (f.hasStateChange() && !f.getFromStates().isEmpty()) {
@@ -572,7 +573,7 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin
      *
      * @return the name of the parent target
      */
-    static String searchFistVariableTarget(TypeChecker tc, CtElement target2, CtElement invocation) {
+    public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, CtElement invocation) {
         if (target2 instanceof CtVariableRead<?> v) {
             // v--------- field read
             // means invocation is in a form of `t.method(args)`