diff --git a/liquidjava-example/src/main/java/testSuite/CorrectLoopPostState.java b/liquidjava-example/src/main/java/testSuite/CorrectLoopPostState.java new file mode 100644 index 00000000..119a62b8 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectLoopPostState.java @@ -0,0 +1,79 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "marked"}) +public class CorrectLoopPostState { + @StateRefinement(to = "open(this)") + CorrectLoopPostState() {} + + @StateRefinement(to = "marked(this)") + void mark() {} + + @StateRefinement(from = "marked(this)", to = "open(this)") + void reset() {} + + @StateRefinement(from = "open(this)") + void use() {} + + // A state-preserving call leaves the entry state available after the loop. + static void unchangedState(int n) { + CorrectLoopPostState b = new CorrectLoopPostState(); + while (n > 0) { + b.use(); + n--; + } + b.use(); + } + + // An unconditional transition after the loop establishes the required state. + static void establishStateAfterLoop(int n) { + CorrectLoopPostState b = new CorrectLoopPostState(); + while (n > 0) { + b.mark(); + n--; + } + b.mark(); + b.reset(); + } + + @StateRefinement(from = "open(this)") + void unchangedThisState(int n) { + while (n > 0) { + this.use(); + n--; + } + use(); + } + + @StateRefinement(from = "open(this)") + void establishThisStateAfterLoop(int n) { + while (n > 0) { + mark(); + n--; + } + this.mark(); + reset(); + } + + @StateRefinement(from = "open(this)") + void directValidTransitions() { + this.use(); + mark(); + this.reset(); + use(); + } + + @StateRefinement(from = "open(this)") + @StateRefinement(from = "marked(this)") + void acceptEitherState() {} + + // Neither alternative is known individually; the call accepts their union and preserves it. + @StateRefinement(from = "open(this)") + @StateRefinement(from = "marked(this)") + void wrapEitherState() { + acceptEitherState(); + this.acceptEitherState(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorLoopPostState.java b/liquidjava-example/src/main/java/testSuite/ErrorLoopPostState.java new file mode 100644 index 00000000..45710a74 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorLoopPostState.java @@ -0,0 +1,90 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "marked"}) +public class ErrorLoopPostState { + @StateRefinement(to = "open(this)") + ErrorLoopPostState() {} + + @StateRefinement(to = "marked(this)") + void mark() {} + + @StateRefinement(from = "marked(this)", to = "open(this)") + void reset() {} + + @StateRefinement(from = "open(this)") + void use() {} + + // Issue #338: the loop may run zero times, leaving b open. + static void whileMayBeEmpty(int n) { + ErrorLoopPostState b = new ErrorLoopPostState(); + int k = 0; + while (k < n) { + b.mark(); + k++; + } + b.reset(); // Expect: State Refinement Error + } + + static void forMayBeEmpty(int n) { + ErrorLoopPostState b = new ErrorLoopPostState(); + for (int k = 0; k < n; k++) { + b.mark(); + } + b.reset(); // Expect: State Refinement Error + } + + static void forEachMayBeEmpty(int[] values) { + ErrorLoopPostState b = new ErrorLoopPostState(); + for (int value : values) { + b.mark(); + } + b.reset(); // Expect: State Refinement Error + } + + @StateRefinement(from = "open(this)") + void explicitThisMayBeEmpty(int n) { + while (n > 0) { + this.mark(); + n--; + } + this.reset(); // Expect: State Refinement Error + } + + @StateRefinement(from = "open(this)") + void implicitThisMayBeEmpty(int n) { + while (n > 0) { + mark(); + n--; + } + reset(); // Expect: State Refinement Error + } + + @StateRefinement(from = "open(this)") + void laterIteration(int n) { + while (n > 0) { + use(); // Expect: State Refinement Error + mark(); + n--; + } + } + + @StateRefinement(from = "open(this)") + void directInvalidCall() { + this.reset(); // Expect: State Refinement Error + } + + @StateRefinement(from = "open(this)") + void directInvalidSequence() { + mark(); + use(); // Expect: State Refinement Error + } + + @StateRefinement(from = "open(this)") + @StateRefinement(from = "marked(this)") + void unionDoesNotImplyOneState() { + use(); // Expect: 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 0810c24d..97c1d482 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 @@ -604,13 +604,17 @@ private void havocChangedIn(CtLoop loop) { loop.getElements(new TypeFilter>(CtVariableWrite.class))); List> calls = loop .getElements(new TypeFilter>(CtAbstractInvocation.class)); + Set names = new LinkedHashSet<>(); for (CtAbstractInvocation call : calls) { - if (call instanceof CtInvocation inv && inv.getTarget()instanceof CtVariableAccess target + if (call instanceof CtInvocation inv && context.getAllMethodsWithNameSize(inv.getExecutable().getSimpleName(), inv.getArguments().size()) - .stream().anyMatch(f -> f.getAllStates().stream().anyMatch(ObjectState::hasTo))) - changed.add(target); + .stream().anyMatch(f -> f.getAllStates().stream().anyMatch(ObjectState::hasTo))) { + if (inv.getTarget()instanceof CtVariableAccess target) + changed.add(target); + else if (inv.getTarget() != null && AuxStateHandler.isCurrentReceiver(inv.getTarget())) + names.add(Keys.THIS); + } } - Set names = new LinkedHashSet<>(); for (CtVariableAccess access : changed) { CtVariable declaration = access.getVariable().getDeclaration(); if (declaration != null && declaration.hasParent(loop.getBody())) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 88a37936..8db12788 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -19,6 +19,7 @@ import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; +import liquidjava.utils.constants.Types; import spoon.reflect.code.CtConstructorCall; import spoon.reflect.code.CtExpression; import spoon.reflect.code.CtFieldRead; @@ -446,6 +447,19 @@ public void loadFunctionInfo(CtExecutable method) { for (Variable v : lv) rtc.getContext().addVarToContext(v); } + if (method instanceof CtMethod instanceMethod && !instanceMethod.isStatic()) { + // The contract describes the entry state, not an invariant of every intermediate receiver state. + Predicate entry = fi == null || fi.getAllStates().isEmpty() ? new Predicate() : fi.getFromStates() + .stream().reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction); + CtTypeReference receiverType = rtc.getFactory().Type().createReference(className); + RefinedVariable receiver = rtc.getContext().addVarToContext(Keys.THIS, receiverType, new Predicate(), + method); + receiver.addSuperTypes(receiverType.getSuperclass(), receiverType.getSuperInterfaces()); + String instanceName = String.format(Formats.INSTANCE, Keys.THIS, rtc.getContext().getCounter()); + rtc.getContext().addInstanceToContext(instanceName, receiverType, + entry.substituteVariable(Keys.THIS, instanceName), method); + rtc.getContext().addRefinementInstanceToVariable(Keys.THIS, instanceName); + } } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 74955db3..4ad7852f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -564,8 +564,28 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc .substituteVariable(name, instanceName); boolean found = false; + boolean preservesState = stateChanges.stream().noneMatch(ObjectState::hasTo); + if (preservesState) { + // A state-preserving call accepts any of its entry states, including a disjunction of them. + Predicate expected = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom) + .reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction) + .substituteVariable(Keys.THIS, instanceName); + Predicate previous = prevState; + for (String parameter : map.keySet()) { + previous = previous.substituteVariable(parameter, map.get(parameter)); + expected = expected.substituteVariable(parameter, map.get(parameter)); + } + expected = expected.changeOldMentions(vi.getName(), instanceName); + try { + found = tc.checkStateSMT(previous, expected, invocation.getPosition()); + } catch (SMTUnknownError error) { + error.setDeclarationPosition(stateChanges.stream().map(ObjectState::getFromPosition) + .filter(Objects::nonNull).findFirst().orElse(function.getPlacementInCode().getPosition())); + throw error; + } + } for (ObjectState stateChange : stateChanges) { // TODO: only working for 1 state annotation - if (found) + if (found || preservesState) break; if (!stateChange.hasFrom()) continue; @@ -679,6 +699,18 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin invocation.putMetadata(Keys.TARGET, vi2); } + /** Whether the access denotes the receiver of the enclosing type, including unqualified super. */ + public static boolean isCurrentReceiver(CtElement target) { + CtType owner = target.getParent(CtType.class); + if (owner == null) + return false; + if (target instanceof CtThisAccess self) + return self.getType() != null && self.getType().getQualifiedName().equals(owner.getQualifiedName()); + if (target instanceof CtSuperAccess parent) + return parent.getTarget() == null || parent.getTarget().isImplicit(); + return false; + } + /** * Gets the name of the parent target and adds the closest target to the elem TARGET metadata * @@ -687,10 +719,10 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin * @return the name of the parent target */ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, CtElement invocation) { - if (target2 instanceof CtVariableRead v) { + if (target2 instanceof CtVariableRead || isCurrentReceiver(target2)) { // v--------- field read // means invocation is in a form of `t.method(args)` - String name = v.getVariable().getSimpleName(); + String name = target2 instanceof CtVariableRead v ? v.getVariable().getSimpleName() : Keys.THIS; if (target2 instanceof CtFieldRead fieldRead && fieldRead.getTarget() instanceof CtThisAccess) { String fieldName = Utils.qualifyFieldName(fieldRead.getVariable()); if (tc.getContext().hasVariable(fieldName))