From 707afb19d35fe1ef8ca9dc05b72ddbd65d6a3123 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 24 Mar 2026 15:03:29 +0000 Subject: [PATCH 1/3] Add Missing Binding --- .../CorrectStateAndParameterRefinementThis.java | 15 +++++++++++++++ .../object_checkers/AuxStateHandler.java | 3 ++- 2 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectStateAndParameterRefinementThis.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStateAndParameterRefinementThis.java b/liquidjava-example/src/main/java/testSuite/CorrectStateAndParameterRefinementThis.java new file mode 100644 index 00000000..2cebb43d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectStateAndParameterRefinementThis.java @@ -0,0 +1,15 @@ +package testSuite; + +import liquidjava.specification.Ghost; +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementPredicate; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@Ghost("int progress") +@StateSet({"downloading", "completed"}) +public class CorrectStateAndParameterRefinementThis { + + @StateRefinement(from = "downloading(this)", to = "progress(this) == percentage") + public void updateProgress(@Refinement("percentage > progress(this)") int percentage) {} +} 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 9d435dff..c1a9320e 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 @@ -216,6 +216,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!! @@ -616,4 +617,4 @@ private static List> getStateAnnotation(CtEle .getCanonicalName().contentEquals("liquidjava.specification.StateRefinement")) .collect(Collectors.toList()); } -} \ No newline at end of file +} From b56ac2119cc0551b65d8f58c392c2b95e280135c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 28 Mar 2026 16:15:29 +0000 Subject: [PATCH 2/3] Fix Method Check Ordering --- .../general_checkers/MethodsFunctionsChecker.java | 12 +++++++++--- .../object_checkers/AuxStateHandler.java | 4 ++-- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 12628ab9..cbdca4a5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -286,16 +286,22 @@ private Map checkInvocationRefinements(CtElement invocation, Lis return new HashMap<>(); Map 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(); 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 c1a9320e..13a035f0 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 @@ -359,7 +359,7 @@ public static void addStateRefinements(TypeChecker tc, String varName, CtExpress */ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpression target2, Map 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()) { @@ -576,7 +576,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)` From a60da241bfda76269f0f9ea460ff09806dd63077 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 28 Mar 2026 16:15:48 +0000 Subject: [PATCH 3/3] Add Tests --- ...orrectStateAndParameterRefinementThis.java | 15 ------------ .../downloader_correct/Downloader.java | 23 +++++++++++++++++++ .../downloader_correct/SimpleTest.java | 11 +++++++++ .../downloader_refinement_error/.expected | 1 + .../Downloader.java | 23 +++++++++++++++++++ .../SimpleTest.java | 10 ++++++++ .../.expected | 1 + .../Downloader.java | 23 +++++++++++++++++++ .../SimpleTest.java | 10 ++++++++ 9 files changed, 102 insertions(+), 15 deletions(-) delete mode 100644 liquidjava-example/src/main/java/testSuite/CorrectStateAndParameterRefinementThis.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/downloader_correct/Downloader.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/downloader_correct/SimpleTest.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/Downloader.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/SimpleTest.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/.expected create mode 100644 liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/Downloader.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/SimpleTest.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStateAndParameterRefinementThis.java b/liquidjava-example/src/main/java/testSuite/CorrectStateAndParameterRefinementThis.java deleted file mode 100644 index 2cebb43d..00000000 --- a/liquidjava-example/src/main/java/testSuite/CorrectStateAndParameterRefinementThis.java +++ /dev/null @@ -1,15 +0,0 @@ -package testSuite; - -import liquidjava.specification.Ghost; -import liquidjava.specification.Refinement; -import liquidjava.specification.RefinementPredicate; -import liquidjava.specification.StateRefinement; -import liquidjava.specification.StateSet; - -@Ghost("int progress") -@StateSet({"downloading", "completed"}) -public class CorrectStateAndParameterRefinementThis { - - @StateRefinement(from = "downloading(this)", to = "progress(this) == percentage") - public void updateProgress(@Refinement("percentage > progress(this)") int percentage) {} -} diff --git a/liquidjava-example/src/main/java/testSuite/classes/downloader_correct/Downloader.java b/liquidjava-example/src/main/java/testSuite/classes/downloader_correct/Downloader.java new file mode 100644 index 00000000..87aa0780 --- /dev/null +++ b/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() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/downloader_correct/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/downloader_correct/SimpleTest.java new file mode 100644 index 00000000..4ac60e09 --- /dev/null +++ b/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(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/.expected new file mode 100644 index 00000000..4cdf9573 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/.expected @@ -0,0 +1 @@ +Refinement Error \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/Downloader.java b/liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/Downloader.java new file mode 100644 index 00000000..0ccbb738 --- /dev/null +++ b/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() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/downloader_refinement_error/SimpleTest.java new file mode 100644 index 00000000..7dbb574a --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/.expected b/liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/.expected new file mode 100644 index 00000000..47ef7162 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/.expected @@ -0,0 +1 @@ +State Refinement Error \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/Downloader.java b/liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/Downloader.java new file mode 100644 index 00000000..83b0b526 --- /dev/null +++ b/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() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/classes/downloader_state_refinement_error/SimpleTest.java new file mode 100644 index 00000000..f38e4668 --- /dev/null +++ b/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 + } +}