diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java index 87c7cdce..c7719f36 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java @@ -42,4 +42,54 @@ 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; + }; + } + + // 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-example/src/main/java/testSuite/ErrorEnumUsage.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumUsage.java index a35b5a4c..95382672 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 65f5bf19..f70c4eb7 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,190 @@ 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) { + // no label matches and there is no default case: a switch expression then throws + if (index == entries.size()) + return !(switchElement instanceof CtSwitchExpression); + 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 +842,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 +995,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 +1101,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 +1121,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 e1633778..40185c21 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 3429e5ee..4d853f4b 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