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 + } +} 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 9d435dff..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 @@ -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!! @@ -358,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()) { @@ -575,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)` @@ -616,4 +617,4 @@ private static List> getStateAnnotation(CtEle .getCanonicalName().contentEquals("liquidjava.specification.StateRefinement")) .collect(Collectors.toList()); } -} \ No newline at end of file +}