Skip to content

Commit 9addae1

Browse files
CatarinaGamboaCatarinaGamboa
authored
Isolate deferred callback state from lambda creation (#386)
Creating a lambda currently applies its body's state transitions to captured objects. For example, `Runnable later = () -> manager.addEdit(null); manager.undo();` passes even though the callback may never run. Check lambda bodies in an isolated context so their assignments, branch facts, and try transitions do not change the surrounding execution. Forget invocation-time assumptions about mutable captures while preserving guards on effectively final primitive captures. Restore variable instances, shared refinements, paths, and enclosing try recorders even after a body diagnostic. The regressions cover local and field callbacks, nested lambdas, try/catch/finally, invalid bodies, primitive guards, and the anonymous-class reproducer already fixed by #326. Callback invocation summaries remain unsupported: `listener.run()` does not apply effects to its captures. Receiver-call checking and lambda return boundaries are handled separately by #384 and #385. Validation: `mvn test -pl liquidjava-verifier -am` (389 tests, no failures) before the final blank-local capture precision adjustment. Both focused fixtures were rerun on the final code: the passing fixture verifies, including blank locals assigned before capture, and all seven expected failing-fixture diagnostic titles and positions match. Fixes #341.
1 parent 26ea1c8 commit 9addae1

7 files changed

Lines changed: 349 additions & 2 deletions

File tree

‎README.md‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,12 @@ socket.sendUrgentData(1); // State Refinement Error
6161
socket.close();
6262
```
6363

64+
Lambda bodies are checked separately from the code that creates them. Creating a lambda does not apply its state
65+
transitions to captured objects. While checking the body, LiquidJava keeps declared refinements but forgets the current
66+
state of mutable captures, since that state may change before invocation. Callback execution summaries are not supported:
67+
a call such as `listener.run()` does not apply the lambda body's effects to its captures. Explicit return statements in
68+
lambdas and state checks on captured `this`/`super` receivers also have incomplete contract handling.
69+
6470
### Ghosts
6571

6672
Finally, LiquidJava also provides ghost variables that are used to track additional information about the program state with the `@Ghost` annotation. These are also updated through the `@StateRefinement` annotation.
@@ -211,4 +217,4 @@ You can find out more about LiquidJava in the following resources:
211217
* [LiquidJava Examples](https://github.com/liquid-java/liquidjava-examples)
212218
* [LiquidJava External Libraries Examples](https://github.com/liquid-java/liquid-java-external-libs)
213219
* [LiquidJava MCP](https://github.com/liquid-java/liquidjava-mcp)
214-
<!-- * [Formalization of LiquidJava](https://github.com/liquid-java/liquidjava-formalization) - not opensource yet -->
220+
<!-- * [Formalization of LiquidJava](https://github.com/liquid-java/liquidjava-formalization) - not opensource yet -->

‎liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java‎

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
package testSuite;
2+
3+
import javax.swing.undo.UndoManager;
4+
import javax.swing.undo.UndoableEdit;
5+
import liquidjava.specification.Refinement;
6+
import liquidjava.specification.ExternalRefinementsFor;
7+
import liquidjava.specification.StateRefinement;
8+
import liquidjava.specification.StateSet;
9+
10+
@ExternalRefinementsFor("javax.swing.undo.UndoManager")
11+
@StateSet({"empty", "full"})
12+
interface CorrectDeferredUndoManagerSpec {
13+
@StateRefinement(to = "empty(this)") void UndoManager();
14+
@StateRefinement(to = "full(this)") boolean addEdit(UndoableEdit edit);
15+
@StateRefinement(from = "full(this)") void undo();
16+
@StateRefinement(from = "empty(this)") void discardAllEdits();
17+
}
18+
19+
class CorrectDeferredCallbackState {
20+
UndoManager manager = new UndoManager();
21+
Runnable listener = () -> { manager.addEdit(null); };
22+
23+
void fieldCallbackMayNeverRun() {
24+
manager.discardAllEdits();
25+
}
26+
27+
void localCallbackMayNeverRun() {
28+
UndoManager local = new UndoManager();
29+
Runnable later = () -> { local.addEdit(null); };
30+
local.discardAllEdits();
31+
}
32+
33+
void directTransitionStillWorks() {
34+
UndoManager local = new UndoManager();
35+
local.addEdit(null);
36+
local.undo();
37+
}
38+
39+
void nestedCallbackMayNeverRun() {
40+
Runnable outer = () -> {
41+
UndoManager local = new UndoManager();
42+
Runnable inner = () -> { local.addEdit(null); };
43+
local.discardAllEdits();
44+
};
45+
}
46+
47+
void callbackInTry() {
48+
UndoManager local = new UndoManager();
49+
try {
50+
Runnable later = () -> { local.addEdit(null); };
51+
local.discardAllEdits();
52+
} catch (RuntimeException e) {
53+
local.discardAllEdits();
54+
} finally {
55+
local.discardAllEdits();
56+
}
57+
}
58+
59+
void tryInsideCallback() {
60+
Runnable later = () -> {
61+
UndoManager local = new UndoManager();
62+
try {
63+
local.addEdit(null);
64+
} finally {
65+
local.addEdit(null);
66+
}
67+
local.undo();
68+
};
69+
}
70+
71+
void capturedPrimitive(int n) {
72+
if (n > 0) {
73+
Runnable later = () -> { manager.addEdit(null); };
74+
@Refinement("_ > 0") int positive = n;
75+
}
76+
}
77+
78+
void immutableCaptureGuard(int n, boolean choose) {
79+
if (n > 0) {
80+
Runnable later = () -> {
81+
@Refinement("_ > 0") int positive = n;
82+
if (choose) {
83+
@Refinement("_ > 0") int thenPositive = n;
84+
} else {
85+
@Refinement("_ > 0") int elsePositive = n;
86+
}
87+
};
88+
@Refinement("_ > 0") int stillPositive = n;
89+
}
90+
}
91+
92+
void blankPrimitiveCaptureGuard(int input) {
93+
int n;
94+
n = input;
95+
if (n > 0) {
96+
Runnable later = () -> {
97+
@Refinement("_ > 0") int positive = n;
98+
};
99+
@Refinement("_ > 0") int stillPositive = n;
100+
}
101+
}
102+
103+
}

‎liquidjava-example/src/main/java/testSuite/ErrorDeferredCallbackState.java‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
package testSuite;
2+
3+
import javax.swing.undo.UndoManager;
4+
import javax.swing.undo.UndoableEdit;
5+
import liquidjava.specification.ExternalRefinementsFor;
6+
import liquidjava.specification.StateRefinement;
7+
import liquidjava.specification.StateSet;
8+
import liquidjava.specification.Refinement;
9+
10+
@ExternalRefinementsFor("javax.swing.undo.UndoManager")
11+
@StateSet({"empty", "full"})
12+
interface ErrorDeferredUndoManagerSpec {
13+
@StateRefinement(to = "empty(this)") void UndoManager();
14+
@StateRefinement(to = "full(this)") boolean addEdit(UndoableEdit edit);
15+
@StateRefinement(from = "full(this)") void undo();
16+
@StateRefinement(from = "empty(this)") void discardAllEdits();
17+
}
18+
19+
class ErrorAnonymousCallbackState {
20+
UndoManager manager = new UndoManager();
21+
22+
ErrorAnonymousCallbackState() {
23+
Runnable listener = new Runnable() {
24+
public void run() { manager.addEdit(null); }
25+
};
26+
}
27+
28+
void undo() {
29+
manager.undo(); // Expect: State Refinement Error
30+
}
31+
}
32+
33+
class ErrorLocalLambdaCallbackState {
34+
void callbackMayNeverRun() {
35+
UndoManager manager = new UndoManager();
36+
Runnable listener = () -> { manager.addEdit(null); };
37+
manager.undo(); // Expect: State Refinement Error
38+
}
39+
}
40+
41+
class ErrorFieldLambdaCallbackState {
42+
UndoManager manager = new UndoManager();
43+
Runnable listener = () -> { manager.addEdit(null); };
44+
45+
void undo() {
46+
manager.undo(); // Expect: State Refinement Error
47+
}
48+
}
49+
50+
class ErrorInvalidLambdaBody {
51+
void invalidBodyStillChecked() {
52+
UndoManager manager = new UndoManager();
53+
Runnable listener = () -> {
54+
if (true) {
55+
manager.undo(); // Expect: State Refinement Error
56+
}
57+
};
58+
// The invalid callback must not stop checking its surrounding method.
59+
manager.undo(); // Expect: State Refinement Error
60+
}
61+
62+
void creationStateDoesNotDescribeInvocation() {
63+
UndoManager manager = new UndoManager();
64+
manager.addEdit(null);
65+
Runnable listener = () -> {
66+
manager.undo(); // Expect: State Refinement Error
67+
};
68+
}
69+
}
70+
71+
class ErrorMutableCallbackGuard {
72+
int value = 1;
73+
74+
void mutableGuardDoesNotDescribeInvocation() {
75+
if (value > 0) {
76+
Runnable later = () -> {
77+
@Refinement("_ > 0") int positive = value; // Expect: Refinement Error
78+
};
79+
@Refinement("_ > 0") int stillPositive = value;
80+
}
81+
}
82+
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java‎

Lines changed: 45 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ public class Context {
1717

1818
private int counter;
1919
// instances given to each variable while visiting the try statements being visited, innermost last
20-
private final Deque<Map<Variable, List<VariableInstance>>> instanceRecorders = new ArrayDeque<>();
20+
private Deque<Map<Variable, List<VariableInstance>>> instanceRecorders = new ArrayDeque<>();
2121
private static Context instance;
2222

2323
private Context() {
@@ -60,6 +60,50 @@ public void exitClassScope(ClassScope scope) {
6060
ctxInstanceVars = scope.instances;
6161
}
6262

63+
/** Keeps captures visible without applying a deferred body's assignments to its enclosing execution. */
64+
public DeferredScope enterDeferredScope() {
65+
DeferredScope scope = new DeferredScope(ctxVars, ctxInstanceVars, instanceRecorders);
66+
ctxVars = new Stack<>();
67+
for (List<RefinedVariable> variables : scope.variables) {
68+
ctxVars.add(new ArrayList<>(variables));
69+
for (RefinedVariable variable : variables) {
70+
scope.refinements.putIfAbsent(variable, variable.getMainRefinement());
71+
if (variable instanceof Variable v)
72+
scope.variableScopes.computeIfAbsent(v, Variable::enterDeferredScope);
73+
}
74+
}
75+
for (RefinedVariable instance : scope.instances)
76+
scope.refinements.putIfAbsent(instance, instance.getMainRefinement());
77+
ctxInstanceVars = new ArrayList<>(scope.instances);
78+
// Try statements inside the body still record locally; enclosing tries must not see deferred transitions.
79+
instanceRecorders = new ArrayDeque<>();
80+
enterContext();
81+
return scope;
82+
}
83+
84+
public void exitDeferredScope(DeferredScope scope) {
85+
scope.variableScopes.forEach(Variable::exitDeferredScope);
86+
scope.refinements.forEach(RefinedVariable::setRefinement);
87+
ctxVars = scope.variables;
88+
ctxInstanceVars = scope.instances;
89+
instanceRecorders = scope.recorders;
90+
}
91+
92+
public static class DeferredScope {
93+
private final Stack<List<RefinedVariable>> variables;
94+
private final List<RefinedVariable> instances;
95+
private final Deque<Map<Variable, List<VariableInstance>>> recorders;
96+
private final Map<Variable, Variable.DeferredScope> variableScopes = new IdentityHashMap<>();
97+
private final Map<RefinedVariable, Predicate> refinements = new IdentityHashMap<>();
98+
99+
private DeferredScope(Stack<List<RefinedVariable>> variables, List<RefinedVariable> instances,
100+
Deque<Map<Variable, List<VariableInstance>>> recorders) {
101+
this.variables = variables;
102+
this.instances = instances;
103+
this.recorders = recorders;
104+
}
105+
}
106+
63107
public static class ClassScope {
64108
private final Stack<List<RefinedVariable>> variables;
65109
private final List<RefinedVariable> instances;

‎liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,30 @@ public void exitContext() {
6969
instances.pop();
7070
}
7171

72+
/** Isolates assignments and branch joins while a deferred body is checked. */
73+
DeferredScope enterDeferredScope() {
74+
DeferredScope scope = new DeferredScope(instances, ifCombiner);
75+
instances = new Stack<>();
76+
instances.addAll(scope.instances);
77+
ifCombiner = new Stack<>();
78+
return scope;
79+
}
80+
81+
void exitDeferredScope(DeferredScope scope) {
82+
instances = scope.instances;
83+
ifCombiner = scope.ifCombiner;
84+
}
85+
86+
static class DeferredScope {
87+
private final Stack<List<VariableInstance>> instances;
88+
private final Stack<Object[]> ifCombiner;
89+
90+
private DeferredScope(Stack<List<VariableInstance>> instances, Stack<Object[]> ifCombiner) {
91+
this.instances = instances;
92+
this.ifCombiner = ifCombiner;
93+
}
94+
}
95+
7296
public void addInstance(VariableInstance vi) {
7397
instances.peek().add(vi);
7498
}

0 commit comments

Comments
 (0)