Join an if on the instances its condition read

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();
+    }
+}

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;
+    }
+}

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
+    }
+}

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
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java

@@ -156,6 +156,9 @@ Optional<VariableInstance> 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();

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<CtVariable<?>> written = new LinkedHashSet<>();
+        if (executable != null)
+            for (CtVariableWrite<?> write : executable
+                    .getElements(new TypeFilter<CtVariableWrite<?>>(CtVariableWrite.class)))
+                if (write.getVariable().getDeclaration() != null)
+                    written.add(write.getVariable().getDeclaration());
+        Set<String> parameters = new LinkedHashSet<>();
+        for (CtVariableRead<?> read : condition.getElements(new TypeFilter<CtVariableRead<?>>(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<String> 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

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -232,6 +232,10 @@ public <R> void getReturnRefinements(CtReturn<R> 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());