{@code java.util.Iterator} itself is an interface, and external refinements only attach to + * classes — Scanner gives us the same API in a class form. + */ +@StateSet({"hasMore", "noMore"}) +@ExternalRefinementsFor("java.util.Scanner") +public interface IteratorRefinements { + + @Refinement("_ == true --> hasMore(this)") + boolean hasNext(); + + @StateRefinement(from = "hasMore(this)", to = "noMore(this)") + String next(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorUse.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorUse.java new file mode 100644 index 00000000..9a3be805 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorUse.java @@ -0,0 +1,36 @@ +package testSuite.classes.iterator_observer_correct; + +import java.util.Scanner; + +public class IteratorUse { + + public static void readOne(Scanner it) { + if (it.hasNext()) { + it.next(); + } + } + + public static void readTwo(Scanner it) { + if (it.hasNext()) { + it.next(); + if (it.hasNext()) { + it.next(); + } + } + } + + public static void readInElse(Scanner it) { + if (!it.hasNext()) { + } else { + it.next(); + } + } + + public static void recursive(Scanner it) { + if (it.hasNext()) { + String s = it.next(); + System.out.println(s); + recursive(it); + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorMisuse.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorMisuse.java new file mode 100644 index 00000000..4aa1f52b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorMisuse.java @@ -0,0 +1,62 @@ +package testSuite.classes.iterator_observer_error; + +import java.util.Scanner; + +public class IteratorMisuse { + + // No check at all: state of the parameter is unknown. + public static void nextWithoutCheck(Scanner it) { + it.next(); // State Refinement Error + } + + // Else branch of hasNext(): condition was false, so we know !hasMore. + public static void nextInElseBranch(Scanner it) { + if (it.hasNext()) { + } else { + it.next(); // State Refinement Error + } + } + + // Negated check: !hasNext() true means hasNext returned false, so !hasMore. + public static void nextNotInElse(Scanner it) { + if (!it.hasNext()) { + it.next(); // State Refinement Error + } + } + + // After consuming with next(), state becomes noMore — a second next() in the same + // then-branch must fail. + public static void doubleNextInThen(Scanner it) { + if (it.hasNext()) { + it.next(); + it.next(); // State Refinement Error + } + } + + // Empty if-then: the bug we fixed in visitCtIf would have masked this join, leaking the + // path-variable's truthiness past the if and silently asserting hasMore. + public static void nextAfterEmptyIf(Scanner it) { + if (it.hasNext()) { + } + it.next(); // State Refinement Error + } + + // Sequential ifs: state is consumed by the first then-branch's next(), and the second if's + // path-variable assertion must not leak past its join. + public static void sequentialIfsLoseState(Scanner it) { + if (it.hasNext()) { + it.next(); + } + if (it.hasNext()) { + } + it.next(); // State Refinement Error + } + + // Empty if + empty else: neither branch establishes hasMore. + public static void nextAfterEmptyIfElse(Scanner it) { + if (it.hasNext()) { + } else { + } + it.next(); // State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorRefinements.java new file mode 100644 index 00000000..7574607a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorRefinements.java @@ -0,0 +1,25 @@ +package testSuite.classes.iterator_observer_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +/** + * Observer-style iteration over {@link java.util.Scanner} (an iterator-shaped JDK class): + * {@code hasNext} is an informative check (no state change), and {@code next} consumes one + * element, resetting state so a fresh check is required before the next consumption. + * + *
{@code java.util.Iterator} itself is an interface, and external refinements only attach to + * classes — Scanner gives us the same API in a class form. + */ +@StateSet({"hasMore", "noMore"}) +@ExternalRefinementsFor("java.util.Scanner") +public interface IteratorRefinements { + + @Refinement("_ == true --> hasMore(this)") + boolean hasNext(); + + @StateRefinement(from = "hasMore(this)", to = "noMore(this)") + String next(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/AbstractUndoableEditRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/AbstractUndoableEditRefinements.java new file mode 100644 index 00000000..35b81156 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/AbstractUndoableEditRefinements.java @@ -0,0 +1,29 @@ +package testSuite.classes.state_test_method_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"aliveDone", "aliveNotDone", "notAlive"}) +@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit") +public interface AbstractUndoableEditRefinements { + + @StateRefinement(to = "aliveDone(this)") + void AbstractUndoableEdit(); + + @StateRefinement(from = "aliveNotDone(this)", to = "aliveDone(this)") + void redo(); + + @StateRefinement(from = "aliveDone(this)", to = "aliveNotDone(this)") + void undo(); + + @StateRefinement(from = "!notAlive(this)", to = "notAlive(this)") + void die(); + + @Refinement("_ == true --> aliveDone(this)") + boolean canUndo(); + + @Refinement("_ == true --> aliveNotDone(this)") + boolean canRedo(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java new file mode 100644 index 00000000..63383cc2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java @@ -0,0 +1,23 @@ +package testSuite.classes.state_test_method_correct; + +import javax.swing.undo.AbstractUndoableEdit; + +public class EditCycler { + public static void undoIfPossible(AbstractUndoableEdit edit) { + if (edit.canUndo()) { + edit.undo(); + } + } + + public static void redoIfPossible(AbstractUndoableEdit edit) { + if (edit.canRedo()) { + edit.redo(); + } + } + + public static void redoIfPossible() { + AbstractUndoableEdit edit = new AbstractUndoableEdit(); + edit.canRedo(); + edit.undo(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/AbstractUndoableEditRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/AbstractUndoableEditRefinements.java new file mode 100644 index 00000000..a29ba8ac --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/AbstractUndoableEditRefinements.java @@ -0,0 +1,26 @@ +package testSuite.classes.state_test_method_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"aliveDone", "aliveNotDone", "notAlive"}) +@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit") +public interface AbstractUndoableEditRefinements { + + @StateRefinement(to = "aliveDone(this)") + void AbstractUndoableEdit(); + + @StateRefinement(from = "aliveNotDone(this)", to = "aliveDone(this)") + void redo(); + + @StateRefinement(from = "aliveDone(this)", to = "aliveNotDone(this)") + void undo(); + + @Refinement("_ == true --> aliveDone(this)") + boolean canUndo(); + + @Refinement("_ == true --> aliveNotDone(this)") + boolean canRedo(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java new file mode 100644 index 00000000..236437bf --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java @@ -0,0 +1,95 @@ +package testSuite.classes.state_test_method_error; + +import javax.swing.undo.AbstractUndoableEdit; + +public class EditMisuse { + + public static void undoInElseBranch(AbstractUndoableEdit edit) { + if (edit.canUndo()) { + } else { + edit.undo(); // State Refinement Error + } + } + + public static void undoNotInElse(AbstractUndoableEdit edit) { + if (!edit.canUndo()) { + edit.undo(); // State Refinement Error + } + } + + public static void wrongTesterForRedo(AbstractUndoableEdit edit) { + if (edit.canUndo()) { + edit.redo(); // State Refinement Error + } + } + + public static void wrongTester2() { + AbstractUndoableEdit edit = new AbstractUndoableEdit(); + edit.undo(); + if (edit.canUndo()) { + edit.undo(); + } + edit.undo(); // State Refinement Error + } + + // Two undos in the same then-branch: condition forces aliveDone for the first, but the second + // is in aliveNotDone. + public static void doubleUndoInThen(AbstractUndoableEdit edit) { + if (edit.canUndo()) { + edit.undo(); + edit.undo(); // State Refinement Error + } + } + + // Nested ifs: outer canUndo => aliveDone, inner canUndo => aliveDone (still), so calling + // redo() in the inner then is illegal (redo needs aliveNotDone). + public static void nestedIfRedoFromAliveDone(AbstractUndoableEdit edit) { + if (edit.canUndo()) { + if (edit.canUndo()) { + edit.redo(); // State Refinement Error + } + } + } + + // Sequential guarded undos with no else: after the first if, state is aliveNotDone in BOTH + // paths (then took canUndo=>aliveDone then undo=>aliveNotDone; else had canUndo=false meaning + // !aliveDone, which can only be aliveNotDone given the state set). The second undo therefore + // cannot succeed — but the verifier must not let the first if's truth assertion leak. + public static void sequentialIfsLoseState() { + AbstractUndoableEdit edit = new AbstractUndoableEdit(); + if (edit.canUndo()) { + edit.undo(); + } + if (edit.canUndo()) { + } + edit.undo(); // State Refinement Error + } + + // Wrong direction: canRedo() implies aliveNotDone, so calling undo() in that branch is illegal. + public static void undoGuardedByCanRedo(AbstractUndoableEdit edit) { + if (edit.canRedo()) { + edit.undo(); // State Refinement Error + } + } + + // Redo after undo inside the then: the inner state is aliveDone -> aliveNotDone -> aliveDone + // after redo, so a second redo from aliveDone is illegal. + public static void doubleRedoAfterUndo(AbstractUndoableEdit edit) { + if (edit.canUndo()) { + edit.undo(); + edit.redo(); + edit.redo(); // State Refinement Error + } + } + + // Empty if / empty else: the bug we fixed would have let `pathVar == true` (or false) leak past + // the join, masking violations. Here the constructor leaves edit in aliveDone, neither branch + // changes it, so after the if the state is still aliveDone — calling redo() is illegal. + public static void redoAfterEmptyIfElse() { + AbstractUndoableEdit edit = new AbstractUndoableEdit(); + if (edit.canUndo()) { + } else { + } + edit.redo(); // State Refinement Error + } +} 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 50ba05f5..09095f35 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 @@ -343,24 +343,45 @@ public void visitCtIf(CtIf ifElement) { String pathVarName = String.format(Formats.FRESH, context.getCounter()); RefinedVariable freshRV; + + // When the condition's predicate uses Keys.WILDCARD as a stand-in for its boolean value (e.g. _ == true --> + // state(this) or _ == k), the fresh path variable IS that value — assert it true in the then branch and false + // in the else, since negating the whole predicate is unsound for implications and equality forms. + boolean valueIsCondition = false; + Predicate thenRefs; + Predicate elseRefs; if (isUninformativeCondition(expRefs, exp)) { // No refinement means the condition is unknown, not true: model it as a fresh // boolean so the SMT solver may pick either truth value for each branch. expRefs = Predicate.createVar(pathVarName); + thenRefs = expRefs; + elseRefs = expRefs.negate(); freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, new Predicate(), exp); } else { + valueIsCondition = expRefs.getVariableNames().contains(Keys.WILDCARD); expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName); Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs); expRefs = Predicate.createConjunction(expRefs, lastExpRefs); - freshRV = context.addInstanceToContext(pathVarName, factory.Type().INTEGER_PRIMITIVE, expRefs, exp); - } + // TODO Change in future + if (expRefs.getVariableNames().contains("null")) { + expRefs = new Predicate(); + valueIsCondition = false; + } - // TODO Change in future - if (expRefs.getVariableNames().contains("null")) { - expRefs = new Predicate(); + thenRefs = expRefs; + elseRefs = expRefs.negate(); + if (valueIsCondition) { + Predicate freshIsTrue = Predicate.createEquals(Predicate.createVar(pathVarName), + Predicate.createLit("true", Types.BOOLEAN)); + Predicate freshIsFalse = Predicate.createEquals(Predicate.createVar(pathVarName), + Predicate.createLit("false", Types.BOOLEAN)); + thenRefs = Predicate.createConjunction(expRefs, freshIsTrue); + elseRefs = Predicate.createConjunction(expRefs, freshIsFalse); + } + + freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp); } - vcChecker.addPathVariable(freshRV); context.variablesNewIfCombination(); @@ -378,7 +399,8 @@ public void visitCtIf(CtIf ifElement) { // VISIT ELSE if (ifElement.getElseStatement() != null) { - context.newRefinementToVariableInContext(pathVarName, expRefs.negate()); + context.getVariableByName(pathVarName); + context.newRefinementToVariableInContext(pathVarName, elseRefs); context.enterContext(); visitCtBlock(ifElement.getElseStatement()); @@ -389,6 +411,9 @@ public void visitCtIf(CtIf ifElement) { context.exitContext(); } // end + // Reset the path variable's refinement to the original condition after the if, + // so branch-local truth assertions (and any typestate they imply) don't leak past the join. + context.newRefinementToVariableInContext(pathVarName, expRefs); vcChecker.removePathVariable(freshRV); context.exitContext(); context.variablesCombineFromIf(expRefs);