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 1/2] 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 From dd8ba716cf8fdc685dc1287c966977dc1a8341e7 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sat, 24 Oct 2026 01:21:06 +0100 Subject: [PATCH 2/2] Preserve mutable condition values and nested fresh dependencies --- .../CorrectRepeatedParameterCondition.java | 44 +++++++++++++++++ .../testSuite/ErrorIfReferenceComparison.java | 18 +++++++ .../ErrorNestedIfCallComparison.java | 17 +++++++ .../processor/context/Variable.java | 3 ++ .../RefinementTypeChecker.java | 47 ++++++++++++++++--- .../MethodsFunctionsChecker.java | 4 ++ 6 files changed, 127 insertions(+), 6 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectRepeatedParameterCondition.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectRepeatedParameterCondition.java b/liquidjava-example/src/main/java/testSuite/CorrectRepeatedParameterCondition.java new file mode 100644 index 00000000..6818adb2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectRepeatedParameterCondition.java @@ -0,0 +1,44 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +class RepeatedConditionDoor { + @StateRefinement(to = "open(this)") + public RepeatedConditionDoor() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} + +public class CorrectRepeatedParameterCondition { + @Refinement("_ == b") + static boolean identity(boolean b) { + if (b == true) { + return b; + } + return b; + } + + @Refinement("_ == b") + static boolean returnAfterReassignment(boolean b) { + if (b) { + // Exercise the condition snapshot before the reassignment. + } + b = false; + return b; + } + + static void closeOnce(boolean b) { + RepeatedConditionDoor d = new RepeatedConditionDoor(); + if (b == true) { + d.close(); + } + if (b == false) { + d.close(); + } + b = false; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java b/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java index 248db689..d287d941 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java @@ -20,4 +20,22 @@ static void closeTwice(ErrorIfReferenceDoor other) { } d.close(); // Expect: State Refinement Error } + + static void closeTwiceAfterChangingCondition(boolean b) { + ErrorIfReferenceDoor d = new ErrorIfReferenceDoor(); + if (b == true) { + d.close(); + } + b = false; + d.close(); // Expect: State Refinement Error + } + + static void closeTwiceAfterBareCondition(boolean b) { + ErrorIfReferenceDoor d = new ErrorIfReferenceDoor(); + if (b) { + d.close(); + } + b = false; + 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 index dbcb14e6..568522ae 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java @@ -1,5 +1,6 @@ package testSuite; +import liquidjava.specification.Refinement; import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; @@ -17,6 +18,12 @@ static ErrorNestedIfDoor current() { return new ErrorNestedIfDoor(); } + @Refinement("_ == 1") + static int one() { return 1; } + + @Refinement("_ == (n > 0)") + static boolean positive(int n) { return n > 0; } + static void closeTwice(boolean b) { ErrorNestedIfDoor d = new ErrorNestedIfDoor(); if (b) { @@ -26,4 +33,14 @@ static void closeTwice(boolean b) { } d.close(); // Expect: State Refinement Error } + + static void closeTwiceWithCallArgument(boolean b) { + ErrorNestedIfDoor d = new ErrorNestedIfDoor(); + if (b) { + if (positive(one() + 1)) { + d.close(); + } + } + d.close(); // Expect: State Refinement Error + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java index d8e1f838..3234df49 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java @@ -156,6 +156,9 @@ Optional getIfInstanceCombination(int counter, Predicate cond) return Optional.empty(); if (has(ifbeforeIndex) && !has(ifthenIndex) && !has(ifelseIndex)) return Optional.empty(); + if (has(ifbeforeIndex) && has(ifthenIndex) && get(ifbeforeIndex) == get(ifthenIndex) + && (!has(ifelseIndex) || get(ifbeforeIndex) == get(ifelseIndex))) + return Optional.empty(); String nName = String.format("#%s_%d", super.getName(), counter); Predicate ref = new Predicate(); 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 c4dfa63b..7c58c315 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 @@ -491,11 +491,15 @@ public void visitCtIf(CtIf ifElement) { || isUninformativeCondition(expRefs, exp); expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName); Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs); + if (canCompleteNormally(ifElement.getThenStatement()) || ifElement.getElseStatement() == null + || canCompleteNormally(ifElement.getElseStatement())) + lastExpRefs = snapshotMutableParameters(lastExpRefs, exp); expRefs = Predicate.createConjunction(expRefs, lastExpRefs); // TODO Change in future if (expRefs.getVariableNames().contains("null")) { expRefs = new Predicate(); + lastExpRefs = new Predicate(); valueIsCondition = true; } @@ -503,12 +507,12 @@ public void visitCtIf(CtIf ifElement) { // 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(); RefinedVariable freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp); + keepFreshValues(joinGuard); vcChecker.addPathVariable(freshRV); context.variablesNewIfCombination(); @@ -544,7 +548,7 @@ public void visitCtIf(CtIf ifElement) { if (thenCompletes == elseCompletes) { // Reset the path variable's refinement to the original condition after the if, // so branch-local truth assertions (and any typestate they imply) don't leak past the join. - context.newRefinementToVariableInContext(pathVarName, expRefs); + context.newRefinementToVariableInContext(pathVarName, lastExpRefs); vcChecker.removePathVariable(freshRV); } else { // Keep the refinement of the only branch that reaches the code after the if. @@ -555,21 +559,52 @@ public void visitCtIf(CtIf ifElement) { context.variablesFinishIfCombination(); } + private Predicate snapshotMutableParameters(Predicate predicate, CtExpression condition) { + // An unchanged parameter can keep its name; a later write must not change this guard's meaning. + CtExecutable executable = condition.getParent(CtExecutable.class); + Set> written = new LinkedHashSet<>(); + if (executable != null) + for (CtVariableWrite write : executable + .getElements(new TypeFilter>(CtVariableWrite.class))) + if (write.getVariable().getDeclaration() != null) + written.add(write.getVariable().getDeclaration()); + Set parameters = new LinkedHashSet<>(); + for (CtVariableRead read : condition.getElements(new TypeFilter>(CtVariableRead.class))) + if (read.getVariable().getDeclaration()instanceof CtParameter parameter && written.contains(parameter)) + parameters.add(read.getVariable().getSimpleName()); + for (String name : predicate.getVariableNames()) { + if (!parameters.contains(name) || !(context.getVariableByName(name)instanceof Variable variable) + || variable.getLastInstance().isPresent()) + continue; + String snapshot = String.format(Formats.INSTANCE, name, context.getCounter()); + context.addInstanceToContext(snapshot, variable.getType(), + variable.getMainRefinement().substituteVariable(name, snapshot), condition); + context.addRefinementInstanceToVariable(name, snapshot); + predicate = predicate.substituteVariable(name, snapshot); + } + return predicate; + } + /** * 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) { + keepFreshValues(predicate, new LinkedHashSet<>()); + } + + private void keepFreshValues(Predicate predicate, Set visited) { String freshPrefix = Formats.FRESH.substring(0, Formats.FRESH.indexOf('%')); for (String name : predicate.getVariableNames()) { - if (!name.startsWith(freshPrefix)) + if (!visited.add(name)) continue; RefinedVariable value = context.getVariableByName(name); - if (value != null && !context.getCtxInstanceVars().contains(value)) { + if (value == null) + continue; + if (name.startsWith(freshPrefix)) context.addInstanceVariable(value); - keepFreshValues(value.getRefinement()); - } + keepFreshValues(value.getMainRefinement(), visited); } } 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 6002a408..cd686f24 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 @@ -232,6 +232,10 @@ public void getReturnRefinements(CtReturn ret) throws LJError { .substituteVariable(Keys.WILDCARD, returnVarName).substituteVariable(Keys.THIS, returnVarName); Predicate cexpectedType = fi.getRefReturn().substituteVariable(Keys.WILDCARD, returnVarName) .substituteVariable(Keys.THIS, returnVarName); + for (Variable parameter : lv) + if (parameter.getLastInstance().isPresent()) + cexpectedType = cexpectedType.substituteVariable(parameter.getName(), + parameter.getLastInstance().get().getName()); rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret); rtc.checkSMT(cexpectedType, ret, fi.getPlacementInCode().getAnnotationPosition(), fi.getMessage());