Check each branch of a conditional expression under its condition

liquidjava-example/src/main/java/testSuite/CorrectTernaryConditionInBranch.java

@@ -0,0 +1,30 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"empty", "full"})
+class CorrectTernaryBox {
+    @StateRefinement(to = "empty(this)")
+    public CorrectTernaryBox() {}
+
+    @StateRefinement(from = "empty(this)", to = "full(this)")
+    public void fill() {}
+
+    @StateRefinement(to = "return ? full(this) : empty(this)")
+    public boolean isFull() {
+        return false;
+    }
+
+    @StateRefinement(from = "full(this)")
+    public int peek() {
+        return 1;
+    }
+}
+
+public class CorrectTernaryConditionInBranch {
+    static int peekIfFull(CorrectTernaryBox box) {
+        boolean full = box.isFull();
+        return full ? box.peek() : 0;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorTernaryConditionInBranch.java

@@ -0,0 +1,30 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"empty", "full"})
+class ErrorTernaryBox {
+    @StateRefinement(to = "empty(this)")
+    public ErrorTernaryBox() {}
+
+    @StateRefinement(from = "empty(this)", to = "full(this)")
+    public void fill() {}
+
+    @StateRefinement(to = "return ? full(this) : empty(this)")
+    public boolean isFull() {
+        return false;
+    }
+
+    @StateRefinement(from = "full(this)")
+    public int peek() {
+        return 1;
+    }
+}
+
+public class ErrorTernaryConditionInBranch {
+    static int peekIfFull(ErrorTernaryBox box) {
+        boolean full = box.isFull();
+        return full ? 0 : box.peek(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -700,22 +700,35 @@ else if (inv.getTarget() != null && AuxStateHandler.isCurrentReceiver(inv.getTar
      * the condition of an if, see visitCtIf). Re-assigning a variable in the body drops the conditions on it.
      */
     private void assumeLoopCondition(CtExpression<Boolean> condition) {
+        assumeCondition(condition, true);
+    }
+
+    /**
+     * Adds a path condition saying that {@code condition} evaluated to {@code holds}, on the values it was evaluated
+     * on. Returns the path variable, so the caller can remove it where the condition no longer applies, or null when
+     * nothing is assumed.
+     */
+    private RefinedVariable assumeCondition(CtExpression<Boolean> condition, boolean holds) {
         // conditions with side effects (e.g. (n = read()) > 0) are not encoded, so they assume nothing
         if (condition == null || !condition.getElements(new TypeFilter<>(CtVariableWrite.class)).isEmpty())
-            return;
+            return null;
         Predicate refs = getRefinement(condition);
         if (isUninformativeCondition(refs, condition))
-            return;
+            return null;
         String pathVarName = String.format(Formats.FRESH, context.getCounter());
         boolean valueIsCondition = refs.getVariableNames().contains(Keys.WILDCARD);
         refs = refs.substituteVariable(Keys.WILDCARD, pathVarName);
         refs = Predicate.createConjunction(refs, substituteAllVariablesForLastInstance(refs));
         if (valueIsCondition) {
             refs = Predicate.createConjunction(refs, Predicate.createEquals(Predicate.createVar(pathVarName),
-                    Predicate.createLit("true", Types.BOOLEAN)));
+                    Predicate.createLit(String.valueOf(holds), Types.BOOLEAN)));
+        } else if (!holds) {
+            refs = refs.negate();
         }
-        vcChecker.addPathVariable(
-                context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, refs, condition));
+        RefinedVariable pathVar = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, refs,
+                condition);
+        vcChecker.addPathVariable(pathVar);
+        return pathVar;
     }
 
     @Override
@@ -728,13 +741,24 @@ public <T> void visitCtArrayWrite(CtArrayWrite<T> arrayWrite) {
 
     @Override
     public <T> void visitCtConditional(CtConditional<T> conditional) {
-        super.visitCtConditional(conditional);
+        // each branch is checked knowing which way the condition went, as the branches of an if
+        CtExpression<Boolean> condition = conditional.getCondition();
+        scan(condition);
+        scanAssuming(conditional.getThenExpression(), condition, true);
+        scanAssuming(conditional.getElseExpression(), condition, false);
         Predicate cond = getRefinement(conditional.getCondition());
         Predicate c = Predicate.createITE(cond, getRefinement(conditional.getThenExpression()),
                 getRefinement(conditional.getElseExpression()));
         conditional.putMetadata(Keys.REFINEMENT, c);
     }
 
+    private void scanAssuming(CtExpression<?> branch, CtExpression<Boolean> condition, boolean holds) {
+        RefinedVariable pathVar = assumeCondition(condition, holds);
+        scan(branch);
+        if (pathVar != null)
+            vcChecker.removePathVariable(pathVar);
+    }
+
     @Override
     public <T> void visitCtConstructorCall(CtConstructorCall<T> ctConstructorCall) {
         super.visitCtConstructorCall(ctConstructorCall);