From e8cf4029dd98dbd68e4a700df6e7fce32f25ea58 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Fri, 2 Oct 2026 17:30:41 +0100 Subject: [PATCH] Reject stale refinements after short-circuit RHS writes Port the short-circuit soundness fix and reproducer from closed PR #257 to current main. Add coverage for OR, nested assignments, increments, and an RHS without writes. Fixes #323 Co-authored-by: Guilherme Espada --- .../ErrorShortCircuitAssignUnsound.java | 46 ++++++++++++++++++ .../RefinementTypeChecker.java | 47 +++++++++++++++++++ 2 files changed, 93 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorShortCircuitAssignUnsound.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorShortCircuitAssignUnsound.java b/liquidjava-example/src/main/java/testSuite/ErrorShortCircuitAssignUnsound.java new file mode 100644 index 00000000..33a71a0c --- /dev/null +++ b/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; + } +} 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 bf6dcc99..7f17d174 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 @@ -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 void visitCtVariableRead(CtVariableRead variableRead) { public void visitCtBinaryOperator(CtBinaryOperator 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. + * + *

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