Reject stale refinements after short-circuit RHS writes

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

@@ -0,0 +1,46 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: assignments on a not-taken control-flow path are applied to the abstract
+// state. In `false && ((x = 1) == 1)` the right operand never executes (short-circuit), so x stays
+// 0 at runtime, but the verifier records x = 1 and ACCEPTS "_ == 1". Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorShortCircuitAssignUnsound {
+    public static void main(String[] args) {
+        int x = 0;
+        boolean b = false && ((x = 1) == 1);
+        @Refinement("_ == 1")
+        int y = x; // Expect: Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because y == 0
+        assert y == 1 : "y=" + y;
+    }
+
+    public static void skippedOr() {
+        int x = 0;
+        boolean b = true || ((x = 1) == 1);
+        @Refinement("_ == 1")
+        int y = x; // Expect: Refinement Error
+    }
+
+    public static void nestedRightOperand() {
+        int x = 0;
+        boolean b = false && ((x = 1) == 1 && (x = 2) == 2);
+        @Refinement("_ == 2")
+        int y = x; // Expect: Refinement Error
+    }
+
+    public static void incrementInRightOperand() {
+        int x = 0;
+        boolean b = false && (++x > 0);
+        @Refinement("_ == 1")
+        int y = x; // Expect: Refinement Error
+    }
+
+    public static void noRightOperandWrite() {
+        int x = 0;
+        boolean b = false && (x == 1);
+        @Refinement("_ == 0")
+        int y = x;
+    }
+}

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

@@ -20,6 +20,7 @@
 import liquidjava.utils.constants.Types;
 
 import org.apache.commons.lang3.NotImplementedException;
+import spoon.reflect.code.BinaryOperatorKind;
 import spoon.reflect.code.CtArrayRead;
 import spoon.reflect.code.CtArrayWrite;
 import spoon.reflect.code.CtAssignment;
@@ -46,11 +47,13 @@
 import spoon.reflect.code.CtUnaryOperator;
 import spoon.reflect.code.CtVariableAccess;
 import spoon.reflect.code.CtVariableRead;
+import spoon.reflect.code.CtVariableWrite;
 import spoon.reflect.declaration.*;
 import spoon.reflect.factory.Factory;
 import spoon.reflect.reference.CtFieldReference;
 import spoon.reflect.reference.CtTypeReference;
 import spoon.reflect.reference.CtVariableReference;
+import spoon.reflect.visitor.filter.TypeFilter;
 import spoon.support.reflect.code.CtVariableWriteImpl;
 
 public class RefinementTypeChecker extends TypeChecker {
@@ -346,6 +349,50 @@ public <T> void visitCtVariableRead(CtVariableRead<T> variableRead) {
     public <T> void visitCtBinaryOperator(CtBinaryOperator<T> operator) {
         super.visitCtBinaryOperator(operator);
         otc.getBinaryOpRefinements(operator);
+        forgetShortCircuitedAssignments(operator);
+    }
+
+    /**
+     * The right operand of {@code &&}/{@code ||} runs only conditionally (it is short-circuited when the left operand
+     * is already {@code false} resp. {@code true}). Spoon visits children before this method, so any assignment in that
+     * operand (e.g. {@code false && ((x = 1) == 1)}) has already committed its value to the context as if it always
+     * executed. That is unsound: at runtime the assignment may never happen, so the post-operator value of every
+     * variable written there is uncertain. Havoc those variables (give them a fresh, unconstrained instance) so the
+     * verifier can no longer assume the assigned value survives the operator.
+     *
+     * <p>
+     * This is conservative: when the left operand is statically true (resp. false) the right operand does execute, yet
+     * we still forget the value. Forgetting only ever weakens what is known, so it cannot accept an unsound program; it
+     * costs precision only for the rare idiom of relying on a value assigned inside a short-circuited operand.
+     */
+    private void forgetShortCircuitedAssignments(CtBinaryOperator<?> operator) {
+        BinaryOperatorKind kind = operator.getKind();
+        if (kind != BinaryOperatorKind.AND && kind != BinaryOperatorKind.OR)
+            return;
+
+        CtExpression<?> conditionalOperand = operator.getRightHandOperand();
+        for (CtVariableWrite<?> write : conditionalOperand.getElements(new TypeFilter<>(CtVariableWrite.class))) {
+            CtVariableReference<?> ref = write.getVariable();
+            if (ref == null)
+                continue;
+            String name = (write instanceof CtFieldWrite<?>) ? String.format(Formats.THIS, ref.getSimpleName())
+                    : ref.getSimpleName();
+            havocVariable(name, write);
+        }
+    }
+
+    /**
+     * Drops everything currently known about {@code name} by installing a fresh, unconstrained instance as its latest
+     * value. Subsequent reads resolve to this instance and therefore carry no refinement.
+     */
+    private void havocVariable(String name, CtElement element) {
+        RefinedVariable rv = context.getVariableByName(name);
+        if (!(rv instanceof Variable))
+            return;
+        String freshName = String.format(Formats.INSTANCE, name, context.getCounter());
+        context.addInstanceToContext(freshName, rv.getType(), new Predicate(), element);
+        context.addRefinementInstanceToVariable(name, freshName);
+        context.addRefinementToVariableInContext(name, rv.getType(), new Predicate(), element);
     }
 
     @Override