Add VC Constraint Elimination Simplification

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCConstraintElimination.java

@@ -0,0 +1,94 @@
+package liquidjava.rj_language.opt;
+
+import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement;
+
+import liquidjava.processor.VCImplication;
+import liquidjava.processor.context.Context;
+import liquidjava.rj_language.Predicate;
+import liquidjava.smt.SMTEvaluator;
+import liquidjava.smt.SMTResult;
+
+/**
+ * Removes antecedent constraints that are implied by stronger constraints later in the VC chain
+ */
+public class VCConstraintElimination implements VCSimplificationPass {
+
+    /**
+     * Applies one constraint elimination in a VC chain
+     */
+    @Override
+    public VCImplication apply(VCImplication implication) {
+        VCImplication cloned = implication.clone();
+        VCImplication simplified = simplify(cloned);
+        return simplified == null ? cloned : simplified;
+    }
+
+    /**
+     * Removes the first antecedent implied by a later antecedent
+     */
+    private VCImplication simplify(VCImplication implication) {
+        if (implication == null || implication.getNext() == null)
+            return null;
+
+        VCImplication implying = findImplyingAntecedent(implication);
+        if (implying != null)
+            return eliminate(implication, implying);
+
+        VCImplication next = simplify(implication.getNext());
+        if (next == null)
+            return null;
+
+        VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
+        result.setNext(next);
+        return result;
+    }
+
+    /**
+     * Finds a later antecedent that implies the current constraint. The final node is the conclusion and is not a
+     * candidate
+     */
+    private VCImplication findImplyingAntecedent(VCImplication implication) {
+        for (VCImplication candidate = implication.getNext(); candidate != null
+                && candidate.getNext() != null; candidate = candidate.getNext()) {
+            if (implies(candidate.getRefinement(), implication.getRefinement()))
+                return candidate;
+        }
+        return null;
+    }
+
+    /**
+     * Eliminates one redundant constraint while preserving any binder attached to it
+     */
+    private VCImplication eliminate(VCImplication implication, VCImplication implying) {
+        if (!implication.hasBinder())
+            return implication.getNext().clone();
+
+        VCImplication result = copyWithRefinement(implication, implying.getRefinement().clone());
+        result.setNext(remove(implication.getNext(), implying));
+        return result;
+    }
+
+    /**
+     * Removes one node from a suffix
+     */
+    private VCImplication remove(VCImplication implication, VCImplication target) {
+        if (implication == target)
+            return implication.getNext() == null ? null : implication.getNext().clone();
+
+        VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
+        result.setNext(remove(implication.getNext(), target));
+        return result;
+    }
+
+    /**
+     * Checks logical implication using the verifier's existing SMT context
+     */
+    private boolean implies(Predicate stronger, Predicate weaker) {
+        try {
+            SMTResult result = new SMTEvaluator().verifySubtype(stronger, weaker, Context.getInstance(), true);
+            return result.isOk();
+        } catch (Exception e) {
+            return false;
+        }
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java

@@ -10,7 +10,8 @@
 public class VCSimplification {
 
     private static final List<VCSimplificationPass> PASSES = List.of(new VCSubstitution(), new VCBinderSimplification(),
-            new VCFolding(), new VCArithmeticSimplification(), new VCLogicalSimplification());
+            new VCFolding(), new VCArithmeticSimplification(), new VCLogicalSimplification(),
+            new VCConstraintElimination());
 
     /**
      * Applies all available simplification steps to a VC chain until a fixed point is reached

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCConstraintEliminationTest.java

@@ -0,0 +1,72 @@
+package liquidjava.rj_language.opt;
+
+import static liquidjava.utils.VCTestUtils.assertSimplificationSteps;
+import static liquidjava.utils.VCTestUtils.step;
+import static liquidjava.utils.VCTestUtils.vc;
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+import liquidjava.processor.VCImplication;
+import liquidjava.processor.context.Context;
+import liquidjava.utils.TestUtils;
+
+class VCConstraintEliminationTest {
+
+    private final VCConstraintElimination constraintElimination = new VCConstraintElimination();
+
+    @BeforeEach
+    void setUpContext() {
+        Context.getInstance().reinitializeAllContext();
+        TestUtils.addIntVariableToContext("x");
+        TestUtils.addIntVariableToContext("y");
+    }
+
+    @AfterEach
+    void resetContext() {
+        Context.getInstance().reinitializeAllContext();
+    }
+
+    @Test
+    void removesConstraintImpliedByLaterAntecedent() {
+        assertSimplificationSteps(constraintElimination,
+                vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"),
+                step("x > 1", "y == x + 1", "y < 0"));
+    }
+
+    @Test
+    void preservesBinderOnStrongerConstraint() {
+        VCImplication simplified = constraintElimination
+                .apply(vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"));
+
+        assertTrue(simplified.hasBinder());
+        assertEquals("x", simplified.getName());
+        assertEquals("int", simplified.getType().getQualifiedName());
+    }
+
+    @Test
+    void keepsConstraintThatIsNotImpliedByLaterAntecedent() {
+        assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 1", "x > 0", "y > 0"),
+                step("x > 1", "x > 0", "y > 0"));
+    }
+
+    @Test
+    void ignoresUnrelatedLaterAntecedent() {
+        assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 0", "y > 1", "x + y > 0"),
+                step("x > 0", "y > 1", "x + y > 0"));
+    }
+
+    @Test
+    void doesNotUseConclusionToEliminateConstraint() {
+        assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 0", "x > 1"), step("x > 0", "x > 1"));
+    }
+
+    @Test
+    void removesOnlyFirstImpliedConstraint() {
+        assertSimplificationSteps(constraintElimination, vc("∀x:int. x > 0", "x > 1", "x > 2", "y > 0"),
+                step("x > 1", "x > 2", "y > 0"), step("x > 2", "y > 0"));
+    }
+}

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java

@@ -3,10 +3,19 @@
 import static liquidjava.utils.VCTestUtils.*;
 import static org.junit.jupiter.api.Assertions.assertNull;
 
+import org.junit.jupiter.api.AfterEach;
 import org.junit.jupiter.api.Test;
 
+import liquidjava.processor.context.Context;
+import liquidjava.utils.TestUtils;
+
 class VCSimplificationTest {
 
+    @AfterEach
+    void resetContext() {
+        Context.getInstance().reinitializeAllContext();
+    }
+
     @Test
     void simplifyReturnsNullForNullImplication() {
         assertNull(VCSimplification.simplifyToFixedPoint(null));
@@ -163,4 +172,12 @@ void simplifyStopsAfterSubstitutionWhenOnlyNegativeLiteralShapeChanges() {
     void simplifyLeavesUnchangedVcAsPlainPredicates() {
         assertSimplificationSteps(vc("x > 0", "y > x"), step("x > 0", "y > x"));
     }
+
+    @Test
+    void simplifyEliminatesConstraintImpliedByLaterAntecedent() {
+        TestUtils.addIntVariableToContext("x");
+        TestUtils.addIntVariableToContext("y");
+        assertSimplificationSteps(vc("∀x:int. x > 0", "∀cond:boolean. x > 1", "∀y:int. y == x + 1", "y < 0"),
+                step("x > 0", "x > 1", "x + 1 < 0"), step("x > 1", "x + 1 < 0"));
+    }
 }

liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java

@@ -18,6 +18,7 @@
 public class VCTestUtils {
 
     private static final CtTypeReference<?> INT = new Launcher().getFactory().Type().INTEGER_PRIMITIVE;
+    private static final CtTypeReference<?> BOOLEAN = new Launcher().getFactory().Type().BOOLEAN_PRIMITIVE;
 
     public static VCImplication vc(String... implications) {
         VCImplication first = null;
@@ -98,6 +99,8 @@ private static VCImplication parseImplication(String implication) {
     private static CtTypeReference<?> type(String name) {
         if ("int".equals(name))
             return INT;
+        if ("boolean".equals(name))
+            return BOOLEAN;
         throw new IllegalArgumentException("Unsupported test type: " + name);
     }