Skip to content

Join an if on the instances its condition read #408

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
CatarinaGamboa wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Join an if on the instances its condition read #408

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 29 additions & 0 deletions liquidjava-example/src/main/java/testSuite/CorrectNestedIfCallComparison.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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();
}
}
23 changes: 23 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
}
}
29 changes: 29 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
}
}
24 changes: 23 additions & 1 deletion ...verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

@CatarinaGamboa CatarinaGamboa Oct 20, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This still leaves a soundness gap when a condition reads a variable that has no last instance (for example, a method parameter). substituteAllVariablesForLastInstance leaves b as a name, so a later assignment changes the meaning of the already-joined guard:

// Door() establishes open(this); close() requires open(this) and establishes closed(this).
void closeTwice(boolean b) {
    Door d = new Door();
    if (b == true) d.close();
    b = false;
    d.close(); // should be a State Refinement Error
}

I ran this on the PR head; LiquidJava says Correct! Passed Verification. The join uses the current b == true (false), discarding the path where d was closed. Could we snapshot condition operands even when they have no existing instance, and add a regression for mutation after the if? This appears to be an existing weakness that the new joinGuard does not cover.

keepFreshValues(joinGuard);
Predicate thenRefs = valueIsCondition ? Predicate.createConjunction(expRefs, branchGuard) : branchGuard;
Predicate elseRefs = valueIsCondition ? Predicate.createConjunction(expRefs, branchGuard.negate())
: branchGuard.negate();
Expand Down Expand Up @@ -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)) {

@CatarinaGamboa CatarinaGamboa Oct 20, 2026

Copy link
Copy Markdown
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The retention walk stops at a value already in ctxInstanceVars, even though that value's refinement can refer to a block-local #fresh value. This leaves the nested-if scope failure unresolved for a refined boolean call whose argument is an expression:

@Refinement("_ == 1") static int one() { return 1; }
@Refinement("_ == (n > 0)") static boolean positive(int n) { return n > 0; }
void check(boolean b) {
    Door d = new Door(); // initially open
    if (b) {
        if (positive(one() + 1)) d.close();
    }
    d.close(); // should be a State Refinement Error
}

On this head the second close() instead reports Not Found Error: Variable '#fresh_12' could not be found. Here the joined guard names the synthetic condition value, which is already an instance; the chain through the call's argument refinement to #fresh_12 is never traversed. Please test transitive dependencies of nested conditions, including values already retained as instances.

More broadly, this fix promotes block-local values into the method-wide instance list. Could we document the intended lifetime/scope invariant for values captured by a join and check that this approach fits it? Issue #406 describes the same kind of out-of-scope refinement dependency across try/finally; a general treatment may be safer than handling only names with the #fresh prefix here.

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
Expand Down
Loading