From 067cf9563f6cc7e11b6a62ef1ea92e7f6cdadbe9 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 9 Oct 2026 00:04:43 +0100 Subject: [PATCH 1/2] Isolate deferred lambda state changes from callback creation --- README.md | 8 +- .../CorrectDeferredCallbackState.java | 92 +++++++++++++++++++ .../testSuite/ErrorDeferredCallbackState.java | 82 +++++++++++++++++ .../liquidjava/processor/context/Context.java | 46 +++++++++- .../processor/context/Variable.java | 24 +++++ .../RefinementTypeChecker.java | 83 +++++++++++++++++ .../refinement_checker/VCChecker.java | 6 ++ 7 files changed, 339 insertions(+), 2 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorDeferredCallbackState.java diff --git a/README.md b/README.md index 72c98443f..2a3cb8798 100644 --- a/README.md +++ b/README.md @@ -61,6 +61,12 @@ socket.sendUrgentData(1); // State Refinement Error socket.close(); ``` +Lambda bodies are checked separately from the code that creates them. Creating a lambda does not apply its state +transitions to captured objects. While checking the body, LiquidJava keeps declared refinements but forgets the current +state of mutable captures, since that state may change before invocation. Callback execution summaries are not supported: +a call such as `listener.run()` does not apply the lambda body's effects to its captures. Explicit return statements in +lambdas and state checks on captured `this`/`super` receivers also have incomplete contract handling. + ### Ghosts 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: * [LiquidJava Examples](https://github.com/liquid-java/liquidjava-examples) * [LiquidJava External Libraries Examples](https://github.com/liquid-java/liquid-java-external-libs) * [LiquidJava MCP](https://github.com/liquid-java/liquidjava-mcp) - \ No newline at end of file + diff --git a/liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java b/liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java new file mode 100644 index 000000000..8f762f04e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java @@ -0,0 +1,92 @@ +package testSuite; + +import javax.swing.undo.UndoManager; +import javax.swing.undo.UndoableEdit; +import liquidjava.specification.Refinement; +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("javax.swing.undo.UndoManager") +@StateSet({"empty", "full"}) +interface CorrectDeferredUndoManagerSpec { + @StateRefinement(to = "empty(this)") void UndoManager(); + @StateRefinement(to = "full(this)") boolean addEdit(UndoableEdit edit); + @StateRefinement(from = "full(this)") void undo(); + @StateRefinement(from = "empty(this)") void discardAllEdits(); +} + +class CorrectDeferredCallbackState { + UndoManager manager = new UndoManager(); + Runnable listener = () -> { manager.addEdit(null); }; + + void fieldCallbackMayNeverRun() { + manager.discardAllEdits(); + } + + void localCallbackMayNeverRun() { + UndoManager local = new UndoManager(); + Runnable later = () -> { local.addEdit(null); }; + local.discardAllEdits(); + } + + void directTransitionStillWorks() { + UndoManager local = new UndoManager(); + local.addEdit(null); + local.undo(); + } + + void nestedCallbackMayNeverRun() { + Runnable outer = () -> { + UndoManager local = new UndoManager(); + Runnable inner = () -> { local.addEdit(null); }; + local.discardAllEdits(); + }; + } + + void callbackInTry() { + UndoManager local = new UndoManager(); + try { + Runnable later = () -> { local.addEdit(null); }; + local.discardAllEdits(); + } catch (RuntimeException e) { + local.discardAllEdits(); + } finally { + local.discardAllEdits(); + } + } + + void tryInsideCallback() { + Runnable later = () -> { + UndoManager local = new UndoManager(); + try { + local.addEdit(null); + } finally { + local.addEdit(null); + } + local.undo(); + }; + } + + void capturedPrimitive(int n) { + if (n > 0) { + Runnable later = () -> { manager.addEdit(null); }; + @Refinement("_ > 0") int positive = n; + } + } + + void immutableCaptureGuard(int n, boolean choose) { + if (n > 0) { + Runnable later = () -> { + @Refinement("_ > 0") int positive = n; + if (choose) { + @Refinement("_ > 0") int thenPositive = n; + } else { + @Refinement("_ > 0") int elsePositive = n; + } + }; + @Refinement("_ > 0") int stillPositive = n; + } + } + +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorDeferredCallbackState.java b/liquidjava-example/src/main/java/testSuite/ErrorDeferredCallbackState.java new file mode 100644 index 000000000..c49e2471f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorDeferredCallbackState.java @@ -0,0 +1,82 @@ +package testSuite; + +import javax.swing.undo.UndoManager; +import javax.swing.undo.UndoableEdit; +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; +import liquidjava.specification.Refinement; + +@ExternalRefinementsFor("javax.swing.undo.UndoManager") +@StateSet({"empty", "full"}) +interface ErrorDeferredUndoManagerSpec { + @StateRefinement(to = "empty(this)") void UndoManager(); + @StateRefinement(to = "full(this)") boolean addEdit(UndoableEdit edit); + @StateRefinement(from = "full(this)") void undo(); + @StateRefinement(from = "empty(this)") void discardAllEdits(); +} + +class ErrorAnonymousCallbackState { + UndoManager manager = new UndoManager(); + + ErrorAnonymousCallbackState() { + Runnable listener = new Runnable() { + public void run() { manager.addEdit(null); } + }; + } + + void undo() { + manager.undo(); // Expect: State Refinement Error + } +} + +class ErrorLocalLambdaCallbackState { + void callbackMayNeverRun() { + UndoManager manager = new UndoManager(); + Runnable listener = () -> { manager.addEdit(null); }; + manager.undo(); // Expect: State Refinement Error + } +} + +class ErrorFieldLambdaCallbackState { + UndoManager manager = new UndoManager(); + Runnable listener = () -> { manager.addEdit(null); }; + + void undo() { + manager.undo(); // Expect: State Refinement Error + } +} + +class ErrorInvalidLambdaBody { + void invalidBodyStillChecked() { + UndoManager manager = new UndoManager(); + Runnable listener = () -> { + if (true) { + manager.undo(); // Expect: State Refinement Error + } + }; + // The invalid callback must not stop checking its surrounding method. + manager.undo(); // Expect: State Refinement Error + } + + void creationStateDoesNotDescribeInvocation() { + UndoManager manager = new UndoManager(); + manager.addEdit(null); + Runnable listener = () -> { + manager.undo(); // Expect: State Refinement Error + }; + } +} + +class ErrorMutableCallbackGuard { + int value = 1; + + void mutableGuardDoesNotDescribeInvocation() { + if (value > 0) { + Runnable later = () -> { + @Refinement("_ > 0") int positive = value; // Expect: Refinement Error + }; + @Refinement("_ > 0") int stillPositive = value; + } + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index e8731991b..87cdd552b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -17,7 +17,7 @@ public class Context { private int counter; // instances given to each variable while visiting the try statements being visited, innermost last - private final Deque>> instanceRecorders = new ArrayDeque<>(); + private Deque>> instanceRecorders = new ArrayDeque<>(); private static Context instance; private Context() { @@ -60,6 +60,50 @@ public void exitClassScope(ClassScope scope) { ctxInstanceVars = scope.instances; } + /** Keeps captures visible without applying a deferred body's assignments to its enclosing execution. */ + public DeferredScope enterDeferredScope() { + DeferredScope scope = new DeferredScope(ctxVars, ctxInstanceVars, instanceRecorders); + ctxVars = new Stack<>(); + for (List variables : scope.variables) { + ctxVars.add(new ArrayList<>(variables)); + for (RefinedVariable variable : variables) { + scope.refinements.putIfAbsent(variable, variable.getMainRefinement()); + if (variable instanceof Variable v) + scope.variableScopes.computeIfAbsent(v, Variable::enterDeferredScope); + } + } + for (RefinedVariable instance : scope.instances) + scope.refinements.putIfAbsent(instance, instance.getMainRefinement()); + ctxInstanceVars = new ArrayList<>(scope.instances); + // Try statements inside the body still record locally; enclosing tries must not see deferred transitions. + instanceRecorders = new ArrayDeque<>(); + enterContext(); + return scope; + } + + public void exitDeferredScope(DeferredScope scope) { + scope.variableScopes.forEach(Variable::exitDeferredScope); + scope.refinements.forEach(RefinedVariable::setRefinement); + ctxVars = scope.variables; + ctxInstanceVars = scope.instances; + instanceRecorders = scope.recorders; + } + + public static class DeferredScope { + private final Stack> variables; + private final List instances; + private final Deque>> recorders; + private final Map variableScopes = new IdentityHashMap<>(); + private final Map refinements = new IdentityHashMap<>(); + + private DeferredScope(Stack> variables, List instances, + Deque>> recorders) { + this.variables = variables; + this.instances = instances; + this.recorders = recorders; + } + } + public static class ClassScope { private final Stack> variables; private final List instances; 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 cfed765dc..d8e1f8384 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java @@ -69,6 +69,30 @@ public void exitContext() { instances.pop(); } + /** Isolates assignments and branch joins while a deferred body is checked. */ + DeferredScope enterDeferredScope() { + DeferredScope scope = new DeferredScope(instances, ifCombiner); + instances = new Stack<>(); + instances.addAll(scope.instances); + ifCombiner = new Stack<>(); + return scope; + } + + void exitDeferredScope(DeferredScope scope) { + instances = scope.instances; + ifCombiner = scope.ifCombiner; + } + + static class DeferredScope { + private final Stack> instances; + private final Stack ifCombiner; + + private DeferredScope(Stack> instances, Stack ifCombiner) { + this.instances = instances; + this.ifCombiner = ifCombiner; + } + } + public void addInstance(VariableInstance vi) { instances.peek().add(vi); } 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 0810c24d5..cc19c70d7 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 @@ -44,6 +44,7 @@ import spoon.reflect.code.CtForEach; import spoon.reflect.code.CtIf; import spoon.reflect.code.CtInvocation; +import spoon.reflect.code.CtLambda; import spoon.reflect.code.CtLiteral; import spoon.reflect.code.CtLocalVariable; import spoon.reflect.code.CtLoop; @@ -52,6 +53,7 @@ import spoon.reflect.code.CtOperatorAssignment; import spoon.reflect.code.CtReturn; import spoon.reflect.code.CtStatement; +import spoon.reflect.code.CtSuperAccess; import spoon.reflect.code.CtThisAccess; import spoon.reflect.code.CtThrow; import spoon.reflect.code.CtTry; @@ -400,6 +402,87 @@ public void visitCtReturn(CtReturn ret) { mfc.getReturnRefinements(ret); } + @Override + public void visitCtLambda(CtLambda lambda) { + Context.DeferredScope scope = context.enterDeferredScope(); + List pathVariables = vcChecker.getPathVariables(); + try { + // Only facts about immutable primitive captures survive until an unknown later invocation. + Set immutableNames = immutableLambdaCaptureNames(lambda); + vcChecker + .replacePathVariables(pathVariables.stream() + .filter(path -> path.getRefinement().getVariableNames().stream() + .allMatch(name -> name.equals(path.getName()) || immutableNames.contains(name))) + .toList()); + havocLambdaCaptures(lambda); + for (CtParameter parameter : lambda.getParameters()) { + Predicate declared = getRefinementFromAnnotation(parameter).orElseGet(Predicate::new) + .substituteVariable(Keys.WILDCARD, parameter.getSimpleName()); + context.addVarToContext(parameter.getSimpleName(), parameter.getType(), declared, parameter); + } + super.visitCtLambda(lambda); + } catch (LJError e) { + diagnostics.add(e); + } finally { + context.exitDeferredScope(scope); + vcChecker.replacePathVariables(pathVariables); + } + } + + private Set immutableLambdaCaptureNames(CtLambda lambda) { + Set names = new LinkedHashSet<>(); + for (CtVariableAccess access : lambda + .getElements(new TypeFilter>(CtVariableAccess.class))) { + CtVariable declaration = access.getVariable().getDeclaration(); + if (access instanceof CtFieldAccess || access.getType() == null || !access.getType().isPrimitive() + || declaration == null || declaration.hasParent(lambda)) + continue; + CtExecutable executable = declaration instanceof CtParameter parameter + ? parameter.getParent(CtExecutable.class) : declaration.getParent(CtExecutable.class); + if (executable == null || executable.getElements(new TypeFilter<>(CtVariableWrite.class)).stream() + .anyMatch(write -> write.getVariable().getDeclaration() == declaration)) + continue; + names.add(access.getVariable().getSimpleName()); + } + for (RefinedVariable rv : context.getCtxInstanceVars()) + if (rv instanceof VariableInstance instance + && instance.getParent().map(parent -> names.contains(parent.getName())).orElse(false)) + names.add(instance.getName()); + return names; + } + + private void havocLambdaCaptures(CtLambda lambda) { + Set names = new LinkedHashSet<>(); + for (CtVariableAccess access : lambda + .getElements(new TypeFilter>(CtVariableAccess.class))) { + CtVariable declaration = access.getVariable().getDeclaration(); + if (declaration != null && declaration.hasParent(lambda)) + continue; + if (access instanceof CtFieldAccess field) { + names.add(Utils.qualifyFieldName(field.getVariable())); + } else if (access instanceof CtSuperAccess parent) { + if (parent.getTarget() == null || parent.getTarget().isImplicit()) + names.add(Keys.THIS); + } else if (access.getType() != null && !access.getType().isPrimitive()) { + names.add(access.getVariable().getSimpleName()); + } + } + for (CtThisAccess self : lambda.getElements(new TypeFilter>(CtThisAccess.class))) { + CtType owner = self.getParent(CtType.class); + if (owner != null && self.getType() != null + && self.getType().getQualifiedName().equals(owner.getQualifiedName())) + names.add(Keys.THIS); + } + for (String name : names) { + if (!(context.getVariableByName(name)instanceof Variable variable)) + continue; + String instanceName = String.format(Formats.INSTANCE, name, context.getCounter()); + Predicate declared = variable.getMainRefinement().substituteVariable(name, instanceName); + context.addInstanceToContext(instanceName, variable.getType(), declared, lambda); + context.addRefinementInstanceToVariable(name, instanceName); + } + } + @Override public void visitCtIf(CtIf ifElement) { CtExpression exp = ifElement.getCondition(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 011bd95bd..ddca35069 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -371,6 +371,12 @@ void restorePathVariables(List saved) { pathVariables.retainAll(saved); } + /** Restores an enclosing execution after checking a deferred body, including facts removed by that body. */ + void replacePathVariables(List saved) { + pathVariables.clear(); + pathVariables.addAll(saved); + } + void removePathVariableThatIncludes(String otherVar) { pathVariables.stream().filter(rv -> rv.getRefinement().getVariableNames().contains(otherVar)).toList() .forEach(pathVariables::remove); From b8f81200d02ead0cfc0f5b9556ea4631ca26aded Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 9 Oct 2026 00:07:04 +0100 Subject: [PATCH 2/2] Preserve guards for blank primitive captures --- .../java/testSuite/CorrectDeferredCallbackState.java | 11 +++++++++++ .../refinement_checker/RefinementTypeChecker.java | 7 +++---- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java b/liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java index 8f762f04e..dc51fa32a 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java @@ -89,4 +89,15 @@ void immutableCaptureGuard(int n, boolean choose) { } } + void blankPrimitiveCaptureGuard(int input) { + int n; + n = input; + if (n > 0) { + Runnable later = () -> { + @Refinement("_ > 0") int positive = n; + }; + @Refinement("_ > 0") int stillPositive = n; + } + } + } 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 cc19c70d7..a3740c9d5 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 @@ -437,10 +437,9 @@ private Set immutableLambdaCaptureNames(CtLambda lambda) { if (access instanceof CtFieldAccess || access.getType() == null || !access.getType().isPrimitive() || declaration == null || declaration.hasParent(lambda)) continue; - CtExecutable executable = declaration instanceof CtParameter parameter - ? parameter.getParent(CtExecutable.class) : declaration.getParent(CtExecutable.class); - if (executable == null || executable.getElements(new TypeFilter<>(CtVariableWrite.class)).stream() - .anyMatch(write -> write.getVariable().getDeclaration() == declaration)) + // Java requires captured locals and parameters to be final or effectively final, including blank + // locals assigned before capture. Their primitive values cannot change before invocation. + if (!(declaration instanceof CtLocalVariable || declaration instanceof CtParameter)) continue; names.add(access.getVariable().getSimpleName()); }