Skip to content

Commit 067cf95

Browse files
CatarinaGamboaCatarinaGamboa
committed
Isolate deferred lambda state changes from callback creation
1 parent dcfc4eb commit 067cf95

7 files changed

Lines changed: 339 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: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
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+
}

‎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
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@
4444
import spoon.reflect.code.CtForEach;
4545
import spoon.reflect.code.CtIf;
4646
import spoon.reflect.code.CtInvocation;
47+
import spoon.reflect.code.CtLambda;
4748
import spoon.reflect.code.CtLiteral;
4849
import spoon.reflect.code.CtLocalVariable;
4950
import spoon.reflect.code.CtLoop;
@@ -52,6 +53,7 @@
5253
import spoon.reflect.code.CtOperatorAssignment;
5354
import spoon.reflect.code.CtReturn;
5455
import spoon.reflect.code.CtStatement;
56+
import spoon.reflect.code.CtSuperAccess;
5557
import spoon.reflect.code.CtThisAccess;
5658
import spoon.reflect.code.CtThrow;
5759
import spoon.reflect.code.CtTry;
@@ -400,6 +402,87 @@ public <R> void visitCtReturn(CtReturn<R> ret) {
400402
mfc.getReturnRefinements(ret);
401403
}
402404

405+
@Override
406+
public <T> void visitCtLambda(CtLambda<T> lambda) {
407+
Context.DeferredScope scope = context.enterDeferredScope();
408+
List<RefinedVariable> pathVariables = vcChecker.getPathVariables();
409+
try {
410+
// Only facts about immutable primitive captures survive until an unknown later invocation.
411+
Set<String> immutableNames = immutableLambdaCaptureNames(lambda);
412+
vcChecker
413+
.replacePathVariables(pathVariables.stream()
414+
.filter(path -> path.getRefinement().getVariableNames().stream()
415+
.allMatch(name -> name.equals(path.getName()) || immutableNames.contains(name)))
416+
.toList());
417+
havocLambdaCaptures(lambda);
418+
for (CtParameter<?> parameter : lambda.getParameters()) {
419+
Predicate declared = getRefinementFromAnnotation(parameter).orElseGet(Predicate::new)
420+
.substituteVariable(Keys.WILDCARD, parameter.getSimpleName());
421+
context.addVarToContext(parameter.getSimpleName(), parameter.getType(), declared, parameter);
422+
}
423+
super.visitCtLambda(lambda);
424+
} catch (LJError e) {
425+
diagnostics.add(e);
426+
} finally {
427+
context.exitDeferredScope(scope);
428+
vcChecker.replacePathVariables(pathVariables);
429+
}
430+
}
431+
432+
private Set<String> immutableLambdaCaptureNames(CtLambda<?> lambda) {
433+
Set<String> names = new LinkedHashSet<>();
434+
for (CtVariableAccess<?> access : lambda
435+
.getElements(new TypeFilter<CtVariableAccess<?>>(CtVariableAccess.class))) {
436+
CtVariable<?> declaration = access.getVariable().getDeclaration();
437+
if (access instanceof CtFieldAccess<?> || access.getType() == null || !access.getType().isPrimitive()
438+
|| declaration == null || declaration.hasParent(lambda))
439+
continue;
440+
CtExecutable<?> executable = declaration instanceof CtParameter<?> parameter
441+
? parameter.getParent(CtExecutable.class) : declaration.getParent(CtExecutable.class);
442+
if (executable == null || executable.getElements(new TypeFilter<>(CtVariableWrite.class)).stream()
443+
.anyMatch(write -> write.getVariable().getDeclaration() == declaration))
444+
continue;
445+
names.add(access.getVariable().getSimpleName());
446+
}
447+
for (RefinedVariable rv : context.getCtxInstanceVars())
448+
if (rv instanceof VariableInstance instance
449+
&& instance.getParent().map(parent -> names.contains(parent.getName())).orElse(false))
450+
names.add(instance.getName());
451+
return names;
452+
}
453+
454+
private void havocLambdaCaptures(CtLambda<?> lambda) {
455+
Set<String> names = new LinkedHashSet<>();
456+
for (CtVariableAccess<?> access : lambda
457+
.getElements(new TypeFilter<CtVariableAccess<?>>(CtVariableAccess.class))) {
458+
CtVariable<?> declaration = access.getVariable().getDeclaration();
459+
if (declaration != null && declaration.hasParent(lambda))
460+
continue;
461+
if (access instanceof CtFieldAccess<?> field) {
462+
names.add(Utils.qualifyFieldName(field.getVariable()));
463+
} else if (access instanceof CtSuperAccess<?> parent) {
464+
if (parent.getTarget() == null || parent.getTarget().isImplicit())
465+
names.add(Keys.THIS);
466+
} else if (access.getType() != null && !access.getType().isPrimitive()) {
467+
names.add(access.getVariable().getSimpleName());
468+
}
469+
}
470+
for (CtThisAccess<?> self : lambda.getElements(new TypeFilter<CtThisAccess<?>>(CtThisAccess.class))) {
471+
CtType<?> owner = self.getParent(CtType.class);
472+
if (owner != null && self.getType() != null
473+
&& self.getType().getQualifiedName().equals(owner.getQualifiedName()))
474+
names.add(Keys.THIS);
475+
}
476+
for (String name : names) {
477+
if (!(context.getVariableByName(name)instanceof Variable variable))
478+
continue;
479+
String instanceName = String.format(Formats.INSTANCE, name, context.getCounter());
480+
Predicate declared = variable.getMainRefinement().substituteVariable(name, instanceName);
481+
context.addInstanceToContext(instanceName, variable.getType(), declared, lambda);
482+
context.addRefinementInstanceToVariable(name, instanceName);
483+
}
484+
}
485+
403486
@Override
404487
public void visitCtIf(CtIf ifElement) {
405488
CtExpression<Boolean> exp = ifElement.getCondition();

0 commit comments

Comments
 (0)