From 19d25affe45e27092d8efc1d67b53cee506c2ff2 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Tue, 20 Oct 2026 18:45:42 +0100 Subject: [PATCH] Join an if on the instances its condition read The join's guard used the condition both with variable names and with their instances. After the if, a name stands for its latest instance, so `if (other == d) d.close(); d.close();` compared the joined d with the old one, which made the closed branch impossible and the error was missed. The guard now names only the instances the condition read. Fresh values the condition creates (a call's result) are kept in the context: inside another if's branch they left scope at the outer join while the joined instances still used them ('Variable #fresh_N could not be found'). Co-Authored-By: Claude Opus 5.5 --- .../CorrectNestedIfCallComparison.java | 29 +++++++++++++++++++ .../testSuite/ErrorIfReferenceComparison.java | 23 +++++++++++++++ .../ErrorNestedIfCallComparison.java | 29 +++++++++++++++++++ .../RefinementTypeChecker.java | 24 ++++++++++++++- 4 files changed, 104 insertions(+), 1 deletion(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectNestedIfCallComparison.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectNestedIfCallComparison.java b/liquidjava-example/src/main/java/testSuite/CorrectNestedIfCallComparison.java new file mode 100644 index 00000000..c1a3163c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectNestedIfCallComparison.java @@ -0,0 +1,29 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +class CorrectNestedIfDoor { + @StateRefinement(to = "open(this)") + public CorrectNestedIfDoor() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} + +public class CorrectNestedIfCallComparison { + static CorrectNestedIfDoor current() { + return new CorrectNestedIfDoor(); + } + + static void compareInNestedIf(boolean b) { + CorrectNestedIfDoor d = new CorrectNestedIfDoor(); + if (b) { + if (current() == d) { + System.out.println("same"); + } + } + d.close(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java b/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java new file mode 100644 index 00000000..248db689 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java @@ -0,0 +1,23 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +class ErrorIfReferenceDoor { + @StateRefinement(to = "open(this)") + public ErrorIfReferenceDoor() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} + +public class ErrorIfReferenceComparison { + static void closeTwice(ErrorIfReferenceDoor other) { + ErrorIfReferenceDoor d = new ErrorIfReferenceDoor(); + if (other == d) { + d.close(); + } + d.close(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java b/liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java new file mode 100644 index 00000000..dbcb14e6 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java @@ -0,0 +1,29 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +class ErrorNestedIfDoor { + @StateRefinement(to = "open(this)") + public ErrorNestedIfDoor() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} + +public class ErrorNestedIfCallComparison { + static ErrorNestedIfDoor current() { + return new ErrorNestedIfDoor(); + } + + static void closeTwice(boolean b) { + ErrorNestedIfDoor d = new ErrorNestedIfDoor(); + if (b) { + if (current() == d) { + d.close(); + } + } + d.close(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 7fcbc31d..c4dfa63b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -500,6 +500,10 @@ public void visitCtIf(CtIf ifElement) { } Predicate branchGuard = valueIsCondition ? Predicate.createVar(pathVarName) : expRefs; + // The joined instances are read after the if, where a variable's name stands for its latest instance; the + // guard must name the instances the condition read (`other == d` would otherwise compare the joined d) + Predicate joinGuard = valueIsCondition ? branchGuard : lastExpRefs; + keepFreshValues(joinGuard); Predicate thenRefs = valueIsCondition ? Predicate.createConjunction(expRefs, branchGuard) : branchGuard; Predicate elseRefs = valueIsCondition ? Predicate.createConjunction(expRefs, branchGuard.negate()) : branchGuard.negate(); @@ -547,10 +551,28 @@ public void visitCtIf(CtIf ifElement) { context.newRefinementToVariableInContext(pathVarName, thenCompletes ? thenRefs : elseRefs); } context.exitContext(); - context.variablesCombineFromIf(branchGuard); + context.variablesCombineFromIf(joinGuard); context.variablesFinishIfCombination(); } + /** + * The fresh values a condition creates (such as a call's result) belong to the enclosing block, but the branch + * guard ends up in the joined instances of the variables changed in the if, which can outlive that block (an if + * nested in another if's branch). Keeps those values, and the fresh values their refinements use, in the context. + */ + private void keepFreshValues(Predicate predicate) { + String freshPrefix = Formats.FRESH.substring(0, Formats.FRESH.indexOf('%')); + for (String name : predicate.getVariableNames()) { + if (!name.startsWith(freshPrefix)) + continue; + RefinedVariable value = context.getVariableByName(name); + if (value != null && !context.getCtxInstanceVars().contains(value)) { + context.addInstanceVariable(value); + keepFreshValues(value.getRefinement()); + } + } + } + /** * A condition is uninformative when its refinement is the trivial {@code true} predicate yet the expression itself * is not a boolean literal — i.e. the verifier has no symbolic information to relate the branch to. Treating such a