From 02cb5086a1995dbeb181f5fd567ed25bdf34ee85 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 12:44:01 +0000 Subject: [PATCH 1/2] Check each case of a switch from the state before it A switch is checked as the chain of ifs that tests its labels: each case knows the selector equals one of its labels (the default case, none of the others), starts from the state before the switch, falls through into the next case when it does not break, and the states of the cases that reach the end are joined after it. Switch expressions are checked the same way. Pattern and guarded cases keep the previous checking. A break or yield nested inside a case's statements is not followed: what those cases change is forgotten on that path. Fixes #494 Co-Authored-By: Claude Opus 5.5 --- .../main/java/testSuite/CorrectEnumUsage.java | 34 +++ .../main/java/testSuite/ErrorEnumUsage.java | 29 +++ .../RefinementTypeChecker.java | 211 +++++++++++++++++- .../java/liquidjava/utils/GeneratedNames.java | 2 + .../liquidjava/api/tests/TestStateHints.java | 10 +- 5 files changed, 275 insertions(+), 11 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java index 87c7cdce0..73fab8c03 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java @@ -42,4 +42,38 @@ public static void main(String[] args) { st.setMode(Mode.Video); // noMode -> videoMode st.takeVideo(); } + + // Each case starts from the state before the switch and knows the value of the selector + public static void capture(Mode mode) { + CorrectEnumUsage st = new CorrectEnumUsage(); + switch (mode) { + case Photo: + st.setMode(Mode.Photo); + st.takePhoto(); + break; + case Video: + st.setMode(mode); + st.takeVideo(); + break; + default: + break; + } + } + + public static boolean captureExpression(Mode mode) { + CorrectEnumUsage st = new CorrectEnumUsage(); + return switch (mode) { + case Photo -> { + st.setMode(Mode.Photo); + st.takePhoto(); + yield true; + } + case Video -> { + st.setMode(Mode.Video); + st.takeVideo(); + yield true; + } + default -> false; + }; + } } \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java index a35b5a4c6..953826728 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java @@ -30,4 +30,33 @@ public static void main(String[] args) { st.setMode(Mode.Video); st.takePhoto(); // Expect: State Refinement Error } + + // Video is not in photoMode: only Photo falls through to it + public static void capture(Mode mode) { + ErrorEnumUsage st = new ErrorEnumUsage(); + switch (mode) { + case Photo: + st.setMode(Mode.Photo); + case Video: + st.takePhoto(); // Expect: State Refinement Error + break; + default: + break; + } + } + + // The break inside the if leaves the switch before setMode + public static void captureUnlessSkipped(Mode mode, boolean skip) { + ErrorEnumUsage st = new ErrorEnumUsage(); + switch (mode) { + case Video: + if (skip) + break; + st.setMode(Mode.Photo); + break; + default: + st.setMode(Mode.Photo); + } + st.takePhoto(); // Expect: State Refinement Error + } } \ No newline at end of file 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 65f5bf19e..2bd6aeba9 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 @@ -5,6 +5,7 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.Deque; +import java.util.HashSet; import java.util.LinkedHashSet; import java.util.List; import java.util.Optional; @@ -29,13 +30,17 @@ import liquidjava.utils.constants.Types; import org.apache.commons.lang3.NotImplementedException; +import spoon.reflect.code.CaseKind; import spoon.reflect.code.CtArrayRead; import spoon.reflect.code.CtAbstractInvocation; +import spoon.reflect.code.CtAbstractSwitch; import spoon.reflect.code.CtArrayWrite; import spoon.reflect.code.CtAssignment; import spoon.reflect.code.CtBinaryOperator; import spoon.reflect.code.CtBlock; import spoon.reflect.code.CtBreak; +import spoon.reflect.code.CtCFlowBreak; +import spoon.reflect.code.CtCase; import spoon.reflect.code.CtCatchVariable; import spoon.reflect.code.CtConditional; import spoon.reflect.code.CtContinue; @@ -57,6 +62,7 @@ import spoon.reflect.code.CtNewArray; import spoon.reflect.code.CtNewClass; import spoon.reflect.code.CtOperatorAssignment; +import spoon.reflect.code.CtPattern; import spoon.reflect.code.CtReturn; import spoon.reflect.code.CtStatement; import spoon.reflect.code.CtSuperAccess; @@ -71,6 +77,7 @@ import spoon.reflect.code.CtVariableRead; import spoon.reflect.code.CtVariableWrite; import spoon.reflect.code.CtWhile; +import spoon.reflect.code.CtYieldStatement; import spoon.reflect.declaration.*; import spoon.reflect.factory.Factory; import spoon.reflect.reference.CtFieldReference; @@ -575,6 +582,189 @@ public void visitCtIf(CtIf ifElement) { context.variablesFinishIfCombination(); } + @Override + public void visitCtSwitch(CtSwitch switchStatement) { + if (!visitSwitch(switchStatement)) + super.visitCtSwitch(switchStatement); + } + + @Override + public void visitCtSwitchExpression(CtSwitchExpression switchExpression) { + if (!visitSwitch(switchExpression)) + super.visitCtSwitchExpression(switchExpression); + } + + /** + * Checks a switch as the chain of ifs that tests its labels in turn (see visitCtIf): each case is checked from the + * state before the switch, knowing that the selector equals one of its labels, and the default case knowing that it + * equals none of the others. A case that falls through goes on into the next one. The states of the cases that + * reach the end of the switch are joined after it. Pattern and guarded cases are not modelled. + * + * @return whether the switch was checked, false when it has pattern or guarded cases + */ + private boolean visitSwitch(CtAbstractSwitch switchElement) { + List> cases = new ArrayList<>(switchElement.getCases()); + if (cases.stream().anyMatch(c -> c.getGuard() != null + || c.getCaseExpressions().stream().anyMatch(label -> label instanceof CtPattern))) + return false; + CtExpression selector = switchElement.getSelector(); + scan(selector); + // the selector is evaluated once, so the cases compare its value then, not what its variables hold later + String selectorName = GeneratedNames.of(GeneratedNames.SWITCH_SELECTOR, context.getCounter()); + Predicate selectorRefs = getRefinement(selector).substituteVariable(Keys.WILDCARD, selectorName); + selectorRefs = snapshotMutableParameters(substituteAllVariablesForLastInstance(selectorRefs), selector); + context.addInstanceToContext(selectorName, selector.getType(), selectorRefs, selector); + + // the cases with no statements share the statements of the next case, the default one is tested last + List entries = new ArrayList<>(); + CaseEntry defaultEntry = null; + List labels = new ArrayList<>(); + boolean isDefault = false; + int start = 0; + for (int i = 0; i < cases.size(); i++) { + CtCase c = cases.get(i); + for (CtExpression label : c.getCaseExpressions()) { + scan(label); + labels.add(getRefinement(label)); + } + isDefault |= c.getCaseExpressions().isEmpty() || c.getIncludesDefault(); + if (c.getStatements().isEmpty() && i < cases.size() - 1) + continue; + CaseEntry entry = new CaseEntry(start, labels); + if (isDefault) + defaultEntry = entry; + else + entries.add(entry); + labels = new ArrayList<>(); + isDefault = false; + start = i + 1; + } + if (defaultEntry != null) + entries.add(defaultEntry); + visitCases(switchElement, cases, entries, 0, selectorName, defaultEntry != null, new HashSet<>()); + return true; + } + + /** A case to which the selector jumps when it equals one of {@code labels}, by their refinements */ + private record CaseEntry(int start, List labels) { + /** That the selector equals one of the labels, or null when a label has no known value */ + Predicate matches(String selectorName) { + Predicate matches = null; + for (Predicate label : labels) { + if (!label.getVariableNames().contains(Keys.WILDCARD)) + return null; + Predicate equals = label.substituteVariable(Keys.WILDCARD, selectorName); + matches = matches == null ? equals : Predicate.createDisjunction(matches, equals); + } + return matches; + } + } + + /** + * Checks the entries of a switch from {@code index} on, as an if that tests the one at {@code index} and checks the + * others in its else, the last one being the default case if there is one + * + * @return whether the end of the switch can be reached from here + */ + private boolean visitCases(CtAbstractSwitch switchElement, List> cases, List entries, + int index, String selectorName, boolean hasDefault, Set> checked) { + if (index == entries.size()) + return true; // no label matches and there is no default case + CaseEntry entry = entries.get(index); + if (hasDefault && index == entries.size() - 1) + return visitCasesFrom(switchElement, cases, entry.start(), checked); + + String pathVarName = GeneratedNames.of(GeneratedNames.CASE_CONDITION, context.getCounter()); + // a label with no known value gives no information about which way the test went + Predicate matches = entry.matches(selectorName); + Predicate branchGuard = matches != null ? matches : Predicate.createVar(pathVarName); + RefinedVariable pathVar = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, + branchGuard, cases.get(entry.start())); + keepFreshValues(branchGuard); + vcChecker.addPathVariable(pathVar); + + context.variablesNewIfCombination(); + context.variablesSetBeforeIf(); + context.enterContext(); + + context.enterContext(); + boolean thenReaches = visitCasesFrom(switchElement, cases, entry.start(), checked); + if (thenReaches) + context.variablesSetThenIf(); + context.exitContext(); + + context.newRefinementToVariableInContext(pathVarName, branchGuard.negate()); + context.enterContext(); + boolean elseReaches = visitCases(switchElement, cases, entries, index + 1, selectorName, hasDefault, checked); + if (elseReaches) + context.variablesSetElseIf(); + context.exitContext(); + + if (thenReaches == elseReaches) { + context.newRefinementToVariableInContext(pathVarName, matches != null ? matches : new Predicate()); + vcChecker.removePathVariable(pathVar); + } else { + // keep the guard of the only branch that reaches the end of the switch + context.newRefinementToVariableInContext(pathVarName, thenReaches ? branchGuard : branchGuard.negate()); + } + context.exitContext(); + context.variablesCombineFromIf(branchGuard); + context.variablesFinishIfCombination(); + return thenReaches || elseReaches; + } + + /** + * Checks the statements of the case at {@code start}, and of the next cases while they fall through. The path + * conditions they add are dropped after them. + * + * @return whether they reach the end of the switch + */ + private boolean visitCasesFrom(CtAbstractSwitch switchElement, List> cases, int start, + Set> checked) { + List pathVariables = vcChecker.getPathVariables(); + List exits = new ArrayList<>(); + int end = start; + boolean completes; + while (true) { + CtCase c = cases.get(end); + if (!checked.add(c)) + removeCheckMetadata(c, List.of()); // checked again after falling through from another case + for (CtStatement statement : c.getStatements()) + scan(statement); + exits.addAll(c.getElements(new TypeFilter<>(CtCFlowBreak.class)).stream() + .filter(jump -> leaves(jump, switchElement)).toList()); + List statements = c.getStatements(); + completes = statements.isEmpty() || canCompleteNormally(statements.get(statements.size() - 1)); + if (!completes || c.getCaseKind() == CaseKind.ARROW || end == cases.size() - 1) + break; + end++; + } + List last = cases.get(end).getStatements(); + CtStatement lastExit = last.isEmpty() ? null : endingJump(last.get(last.size() - 1)); + // the states where a break or yield inside a statement leaves the switch are not followed: forget what these + // cases change + if (exits.stream().anyMatch(jump -> jump != lastExit)) + for (CtCase c : cases.subList(start, end + 1)) + for (String name : changedIn(c, switchElement)) + forgetChanges(name, new Predicate(), c); + vcChecker.restorePathVariables(pathVariables); + return completes || !exits.isEmpty(); + } + + /** Whether {@code jump} is a break or yield that leaves {@code switchElement} */ + private static boolean leaves(CtCFlowBreak jump, CtAbstractSwitch switchElement) { + if (jump instanceof CtBreak breakStatement) + return jumpTarget(breakStatement) == switchElement; + return jump instanceof CtYieldStatement && jump.getParent(CtSwitchExpression.class) == switchElement; + } + + /** The jump that a statement ends with, as the last statement of its blocks */ + private static CtStatement endingJump(CtStatement statement) { + if (statement instanceof CtBlock block) + return block.getStatements().isEmpty() ? null : endingJump(block.getLastStatement()); + return statement instanceof CtCFlowBreak ? statement : null; + } + 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); @@ -651,7 +841,7 @@ boolean canCompleteNormally(CtStatement statement) { if (statement == null || isLeftByLabelledBreak(statement)) return true; if (statement instanceof CtReturn || statement instanceof CtThrow || statement instanceof CtBreak - || statement instanceof CtContinue) + || statement instanceof CtContinue || statement instanceof CtYieldStatement) return false; if (statement instanceof CtBlock block) { List statements = block.getStatements(); @@ -804,7 +994,11 @@ private static void removeCheckMetadata(CtLoop loop) { checkedBefore.addAll(forLoop.getForInit()); if (loop instanceof CtForEach forEach) checkedBefore.add(forEach.getExpression()); - for (CtElement element : loop.getElements((CtElement e) -> true)) { + removeCheckMetadata(loop, checkedBefore); + } + + private static void removeCheckMetadata(CtElement checked, List checkedBefore) { + for (CtElement element : checked.getElements((CtElement e) -> true)) { if (element instanceof CtTypeMember || (element instanceof CtParameter && element.getParent() instanceof CtTypeMember) || checkedBefore.stream().anyMatch(before -> element == before || element.hasParent(before))) @@ -906,9 +1100,14 @@ void forgetChanges(String name, Predicate known, CtElement element) { * if it calls any method or constructor (which may write them) */ private Set changedIn(CtLoop loop) { + return changedIn(loop, loop.getBody()); + } + + /** What {@code element} may change, but the variables declared in {@code scope}, which do not outlive it */ + private Set changedIn(CtElement element, CtElement scope) { List> changed = new ArrayList<>( - loop.getElements(new TypeFilter>(CtVariableWrite.class))); - List> calls = loop + element.getElements(new TypeFilter>(CtVariableWrite.class))); + List> calls = element .getElements(new TypeFilter>(CtAbstractInvocation.class)); Set names = new LinkedHashSet<>(); for (CtAbstractInvocation call : calls) { @@ -921,8 +1120,8 @@ else if (inv.getTarget() != null && AuxStateHandler.isCurrentReceiver(inv.getTar } for (CtVariableAccess access : changed) { CtVariable declaration = access.getVariable().getDeclaration(); - if (declaration != null && declaration.hasParent(loop.getBody())) - continue; // declared in the body: a new variable on each iteration + if (declaration != null && declaration.hasParent(scope)) + continue; // e.g. declared in a loop body: a new variable on each iteration String name = access.getVariable().getSimpleName(); names.add(access instanceof CtFieldAccess ? String.format(Formats.THIS, name) : name); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/GeneratedNames.java b/liquidjava-verifier/src/main/java/liquidjava/utils/GeneratedNames.java index e16337787..40185c211 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/GeneratedNames.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/GeneratedNames.java @@ -19,6 +19,8 @@ public final class GeneratedNames { public static final String IF_CONDITION = "if_condition"; public static final String LOOP_CONDITION = "loop_condition"; public static final String TERNARY_CONDITION = "ternary_condition"; + public static final String SWITCH_SELECTOR = "switch_selector"; + public static final String CASE_CONDITION = "case_condition"; public static final String TRY_BRANCH = "try_branch"; public static final String CATCH_BRANCH = "catch_branch"; public static final String ARRAY_LENGTH = "array_length"; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 3429e5ee5..4d853f4b5 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -325,11 +325,11 @@ void checksOfTheStudysUndoManagerAreSuggestedOneAfterTheOther() { "The state of undoManager is unknown here, and this call needs it to be redoable"), new Hint(Kind.GUARD, "Guard this call with if (undoManager.canRedo()): when it returns true, undoManager is redoable")); - assertHints(errors.get(1), new Hint(Kind.GUARD, - "Guard this call with if (undoManager.canUndo()): when it returns true, undoManager is undoable"), - new Hint(Kind.AVAILABLE_CALLS, - "In state undoable and notRedoable or notUndoable and notRedoable, undoManager can call: " - + "canUndo(), canRedo() (and possibly others)")); + assertHints(errors.get(1), + new Hint(Kind.NEEDED_STATE, + "The state of undoManager is unknown here, and this call needs it to be undoable"), + new Hint(Kind.GUARD, + "Guard this call with if (undoManager.canUndo()): when it returns true, undoManager is undoable")); } @Test From 432a508cd74c0b707fc276d96355eb7ba7e504b3 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 12:52:27 +0000 Subject: [PATCH 2/2] A switch expression that matches no label does not reach the code after it Co-Authored-By: Claude Opus 5.5 --- .../main/java/testSuite/CorrectEnumUsage.java | 16 ++++++++++++++++ .../RefinementTypeChecker.java | 3 ++- 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java index 73fab8c03..c7719f36f 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java @@ -76,4 +76,20 @@ public static boolean captureExpression(Mode mode) { default -> false; }; } + + // A switch expression that matches no label throws: it does not reach the code after it + public static void captureOnThread(Thread.State state) { + CorrectEnumUsage st = new CorrectEnumUsage(); + boolean running = switch (state) { + case NEW, RUNNABLE, BLOCKED -> { + st.setMode(Mode.Photo); + yield true; + } + case WAITING, TIMED_WAITING, TERMINATED -> { + st.setMode(Mode.Photo); + yield false; + } + }; + st.takePhoto(); + } } \ No newline at end of file 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 2bd6aeba9..f70c4eb79 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 @@ -668,8 +668,9 @@ Predicate matches(String selectorName) { */ private boolean visitCases(CtAbstractSwitch switchElement, List> cases, List entries, int index, String selectorName, boolean hasDefault, Set> checked) { + // no label matches and there is no default case: a switch expression then throws if (index == entries.size()) - return true; // no label matches and there is no default case + return !(switchElement instanceof CtSwitchExpression); CaseEntry entry = entries.get(index); if (hasDefault && index == entries.size() - 1) return visitCasesFrom(switchElement, cases, entry.start(), checked);