diff --git a/liquidjava-example/src/main/java/testSuite/CorrectNestedIfCallComparison.java b/liquidjava-example/src/main/java/testSuite/CorrectNestedIfCallComparison.java new file mode 100644 index 00000000..c1a3163c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectNestedIfCallComparison.java @@ -0,0 +1,29 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +class CorrectNestedIfDoor { + @StateRefinement(to = "open(this)") + public CorrectNestedIfDoor() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} + +public class CorrectNestedIfCallComparison { + static CorrectNestedIfDoor current() { + return new CorrectNestedIfDoor(); + } + + static void compareInNestedIf(boolean b) { + CorrectNestedIfDoor d = new CorrectNestedIfDoor(); + if (b) { + if (current() == d) { + System.out.println("same"); + } + } + d.close(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectRepeatedParameterCondition.java b/liquidjava-example/src/main/java/testSuite/CorrectRepeatedParameterCondition.java new file mode 100644 index 00000000..6818adb2 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectRepeatedParameterCondition.java @@ -0,0 +1,44 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +class RepeatedConditionDoor { + @StateRefinement(to = "open(this)") + public RepeatedConditionDoor() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} + +public class CorrectRepeatedParameterCondition { + @Refinement("_ == b") + static boolean identity(boolean b) { + if (b == true) { + return b; + } + return b; + } + + @Refinement("_ == b") + static boolean returnAfterReassignment(boolean b) { + if (b) { + // Exercise the condition snapshot before the reassignment. + } + b = false; + return b; + } + + static void closeOnce(boolean b) { + RepeatedConditionDoor d = new RepeatedConditionDoor(); + if (b == true) { + d.close(); + } + if (b == false) { + d.close(); + } + b = false; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java b/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java new file mode 100644 index 00000000..d287d941 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorIfReferenceComparison.java @@ -0,0 +1,41 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +class ErrorIfReferenceDoor { + @StateRefinement(to = "open(this)") + public ErrorIfReferenceDoor() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} + +public class ErrorIfReferenceComparison { + static void closeTwice(ErrorIfReferenceDoor other) { + ErrorIfReferenceDoor d = new ErrorIfReferenceDoor(); + if (other == d) { + d.close(); + } + d.close(); // Expect: State Refinement Error + } + + static void closeTwiceAfterChangingCondition(boolean b) { + ErrorIfReferenceDoor d = new ErrorIfReferenceDoor(); + if (b == true) { + d.close(); + } + b = false; + d.close(); // Expect: State Refinement Error + } + + static void closeTwiceAfterBareCondition(boolean b) { + ErrorIfReferenceDoor d = new ErrorIfReferenceDoor(); + if (b) { + d.close(); + } + b = false; + d.close(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java b/liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java new file mode 100644 index 00000000..568522ae --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorNestedIfCallComparison.java @@ -0,0 +1,46 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +class ErrorNestedIfDoor { + @StateRefinement(to = "open(this)") + public ErrorNestedIfDoor() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} + +public class ErrorNestedIfCallComparison { + static ErrorNestedIfDoor current() { + return new ErrorNestedIfDoor(); + } + + @Refinement("_ == 1") + static int one() { return 1; } + + @Refinement("_ == (n > 0)") + static boolean positive(int n) { return n > 0; } + + static void closeTwice(boolean b) { + ErrorNestedIfDoor d = new ErrorNestedIfDoor(); + if (b) { + if (current() == d) { + d.close(); + } + } + d.close(); // Expect: State Refinement Error + } + + static void closeTwiceWithCallArgument(boolean b) { + ErrorNestedIfDoor d = new ErrorNestedIfDoor(); + if (b) { + if (positive(one() + 1)) { + d.close(); + } + } + d.close(); // Expect: State Refinement Error + } +} 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 d8e1f838..3234df49 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java @@ -156,6 +156,9 @@ Optional getIfInstanceCombination(int counter, Predicate cond) return Optional.empty(); if (has(ifbeforeIndex) && !has(ifthenIndex) && !has(ifelseIndex)) return Optional.empty(); + if (has(ifbeforeIndex) && has(ifthenIndex) && get(ifbeforeIndex) == get(ifthenIndex) + && (!has(ifelseIndex) || get(ifbeforeIndex) == get(ifelseIndex))) + return Optional.empty(); String nName = String.format("#%s_%d", super.getName(), counter); Predicate ref = new Predicate(); 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 7fcbc31d..7c58c315 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 @@ -491,20 +491,28 @@ public void visitCtIf(CtIf ifElement) { || isUninformativeCondition(expRefs, exp); expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName); Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs); + if (canCompleteNormally(ifElement.getThenStatement()) || ifElement.getElseStatement() == null + || canCompleteNormally(ifElement.getElseStatement())) + lastExpRefs = snapshotMutableParameters(lastExpRefs, exp); expRefs = Predicate.createConjunction(expRefs, lastExpRefs); // TODO Change in future if (expRefs.getVariableNames().contains("null")) { expRefs = new Predicate(); + lastExpRefs = new Predicate(); valueIsCondition = true; } Predicate branchGuard = valueIsCondition ? Predicate.createVar(pathVarName) : expRefs; + // The joined instances are read after the if, where a variable's name stands for its latest instance; the + // guard must name the instances the condition read (`other == d` would otherwise compare the joined d) + Predicate joinGuard = valueIsCondition ? branchGuard : lastExpRefs; Predicate thenRefs = valueIsCondition ? Predicate.createConjunction(expRefs, branchGuard) : branchGuard; Predicate elseRefs = valueIsCondition ? Predicate.createConjunction(expRefs, branchGuard.negate()) : branchGuard.negate(); RefinedVariable freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp); + keepFreshValues(joinGuard); vcChecker.addPathVariable(freshRV); context.variablesNewIfCombination(); @@ -540,17 +548,66 @@ public void visitCtIf(CtIf ifElement) { if (thenCompletes == elseCompletes) { // 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); + context.newRefinementToVariableInContext(pathVarName, lastExpRefs); vcChecker.removePathVariable(freshRV); } else { // Keep the refinement of the only branch that reaches the code after the if. context.newRefinementToVariableInContext(pathVarName, thenCompletes ? thenRefs : elseRefs); } context.exitContext(); - context.variablesCombineFromIf(branchGuard); + context.variablesCombineFromIf(joinGuard); context.variablesFinishIfCombination(); } + 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); + Set> written = new LinkedHashSet<>(); + if (executable != null) + for (CtVariableWrite write : executable + .getElements(new TypeFilter>(CtVariableWrite.class))) + if (write.getVariable().getDeclaration() != null) + written.add(write.getVariable().getDeclaration()); + Set parameters = new LinkedHashSet<>(); + for (CtVariableRead read : condition.getElements(new TypeFilter>(CtVariableRead.class))) + if (read.getVariable().getDeclaration()instanceof CtParameter parameter && written.contains(parameter)) + parameters.add(read.getVariable().getSimpleName()); + for (String name : predicate.getVariableNames()) { + if (!parameters.contains(name) || !(context.getVariableByName(name)instanceof Variable variable) + || variable.getLastInstance().isPresent()) + continue; + String snapshot = String.format(Formats.INSTANCE, name, context.getCounter()); + context.addInstanceToContext(snapshot, variable.getType(), + variable.getMainRefinement().substituteVariable(name, snapshot), condition); + context.addRefinementInstanceToVariable(name, snapshot); + predicate = predicate.substituteVariable(name, snapshot); + } + return predicate; + } + + /** + * The fresh values a condition creates (such as a call's result) belong to the enclosing block, but the branch + * guard ends up in the joined instances of the variables changed in the if, which can outlive that block (an if + * nested in another if's branch). Keeps those values, and the fresh values their refinements use, in the context. + */ + private void keepFreshValues(Predicate predicate) { + keepFreshValues(predicate, new LinkedHashSet<>()); + } + + private void keepFreshValues(Predicate predicate, Set visited) { + String freshPrefix = Formats.FRESH.substring(0, Formats.FRESH.indexOf('%')); + for (String name : predicate.getVariableNames()) { + if (!visited.add(name)) + continue; + RefinedVariable value = context.getVariableByName(name); + if (value == null) + continue; + if (name.startsWith(freshPrefix)) + context.addInstanceVariable(value); + keepFreshValues(value.getMainRefinement(), visited); + } + } + /** * A condition is uninformative when its refinement is the trivial {@code true} predicate yet the expression itself * is not a boolean literal — i.e. the verifier has no symbolic information to relate the branch to. Treating such a 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 6002a408..cd686f24 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 @@ -232,6 +232,10 @@ public void getReturnRefinements(CtReturn ret) throws LJError { .substituteVariable(Keys.WILDCARD, returnVarName).substituteVariable(Keys.THIS, returnVarName); Predicate cexpectedType = fi.getRefReturn().substituteVariable(Keys.WILDCARD, returnVarName) .substituteVariable(Keys.THIS, returnVarName); + for (Variable parameter : lv) + if (parameter.getLastInstance().isPresent()) + cexpectedType = cexpectedType.substituteVariable(parameter.getName(), + parameter.getLastInstance().get().getName()); rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret); rtc.checkSMT(cexpectedType, ret, fi.getPlacementInCode().getAnnotationPosition(), fi.getMessage());