Return Null Origin for Unsimplified VCs

liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java

@@ -33,11 +33,14 @@ public VCImplication(VCImplication implication, Predicate ref) {
     }
 
     public VCImplication getOrigin() {
-        return new VCImplication(this, refinement.clone());
+        return null;
     }
 
     public Predicate getOriginRefinement() {
-        return getOrigin().getRefinement().clone();
+        VCImplication origin = getOrigin();
+        if (origin == null)
+            return refinement.clone();
+        return origin.getRefinement().clone();
     }
 
     public VCImplication copyWithRefinement(Predicate refinement) {

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

@@ -43,18 +43,18 @@ void simplifiesMultiplicativeIdentities() {
     @Test
     void simplifiesGuardedDivisionAndModuloIdentities() {
         assertSimplificationSteps(simplification::apply, vc("x != 0", "0 / x == 0"),
-                chain(expect("x != 0", "x != 0"), expect("0 == 0", "0 / x == 0")));
+                chain(expect("x != 0"), expect("0 == 0", "0 / x == 0")));
         assertSimplificationSteps(simplification::apply, vc("x != 0", "x / x == 1"),
-                chain(expect("x != 0", "x != 0"), expect("1 == 1", "x / x == 1")));
+                chain(expect("x != 0"), expect("1 == 1", "x / x == 1")));
         assertSimplificationSteps(simplification::apply, vc("0 != x", "x % x == 0"),
-                chain(expect("0 != x", "0 != x"), expect("0 == 0", "x % x == 0")));
+                chain(expect("0 != x"), expect("0 == 0", "x % x == 0")));
     }
 
     @Test
     void leavesUnguardedDivisionAndModuloIdentitiesUnchanged() {
-        assertSimplificationSteps(simplification::apply, vc("0 / x == 0"), chain(expect("0 / x == 0", "0 / x == 0")));
-        assertSimplificationSteps(simplification::apply, vc("x / x == 1"), chain(expect("x / x == 1", "x / x == 1")));
-        assertSimplificationSteps(simplification::apply, vc("x % x == 0"), chain(expect("x % x == 0", "x % x == 0")));
+        assertSimplificationSteps(simplification::apply, vc("0 / x == 0"), chain(expect("0 / x == 0")));
+        assertSimplificationSteps(simplification::apply, vc("x / x == 1"), chain(expect("x / x == 1")));
+        assertSimplificationSteps(simplification::apply, vc("x % x == 0"), chain(expect("x % x == 0")));
     }
 
     @Test
@@ -68,7 +68,7 @@ void recordsOriginWhenSimplifyingLaterImplication() {
         VCImplication implication = vc("x > 0", "y + 0 > x");
 
         VCImplication result = assertSimplificationSteps(simplification::apply, implication,
-                chain(expect("x > 0", "x > 0"), expect("y > x", "y + 0 > x")));
+                chain(expect("x > 0"), expect("y > x", "y + 0 > x")));
 
         SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
         assertEquals("y + 0 > x", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString());

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

@@ -21,8 +21,7 @@ void removesTrueBinderWhenVariableIsUnusedDownstream() {
     void keepsTrueBinderWhenVariableIsUsedDownstream() {
         VCImplication implication = vc("∀x:int. true", "x > 0");
 
-        assertSimplificationSteps(binderSimplification::apply, implication,
-                chain(expect("true", "∀x:int. true"), expect("x > 0", "x > 0")));
+        assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("true"), expect("x > 0")));
     }
 
     @Test
@@ -39,23 +38,22 @@ void simplifiesOnlyFirstApplicableBinder() {
         VCImplication implication = vc("∀x:int. true", "∀y:int. true", "z > 0");
 
         assertSimplificationSteps(binderSimplification::apply, implication,
-                chain(expect("true", "∀x:int. true"), expect("z > 0", "z > 0")));
+                chain(expect("true", "∀x:int. true"), expect("z > 0")));
     }
 
     @Test
     void skipsInapplicableTrueBinderAndSimplifiesLaterBinder() {
         VCImplication implication = vc("∀x:int. true", "x > 0", "∀y:int. true", "z > 0");
 
         assertSimplificationSteps(binderSimplification::apply, implication,
-                chain(expect("true", "∀x:int. true"), expect("x > 0", "x > 0"), expect("z > 0", "∀y:int. z > 0")));
+                chain(expect("true"), expect("x > 0"), expect("z > 0", "∀y:int. z > 0")));
     }
 
     @Test
     void ignoresNonBinderBooleanLiterals() {
         VCImplication implication = vc("true", "false");
 
-        assertSimplificationSteps(binderSimplification::apply, implication,
-                chain(expect("true", "true"), expect("false", "false")));
+        assertSimplificationSteps(binderSimplification::apply, implication, chain(expect("true"), expect("false")));
     }
 
     @Test

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

@@ -39,16 +39,14 @@ void foldsRealAndMixedNumericExpressions() {
 
     @Test
     void leavesDivisionAndModuloByZeroUnchanged() {
-        assertSimplificationSteps(folding::apply, vc("4 / 0 == 0"), chain(expect("4 / 0 == 0", "4 / 0 == 0")));
-        assertSimplificationSteps(folding::apply, vc("4 % 0 == 0"), chain(expect("4 % 0 == 0", "4 % 0 == 0")));
+        assertSimplificationSteps(folding::apply, vc("4 / 0 == 0"), chain(expect("4 / 0 == 0")));
+        assertSimplificationSteps(folding::apply, vc("4 % 0 == 0"), chain(expect("4 % 0 == 0")));
     }
 
     @Test
     void leavesRealDivisionAndModuloByZeroUnchanged() {
-        assertSimplificationSteps(folding::apply, vc("4.0 / 0.0 == 0.0"),
-                chain(expect("4.0 / 0.0 == 0.0", "4.0 / 0.0 == 0.0")));
-        assertSimplificationSteps(folding::apply, vc("4.0 % 0.0 == 0.0"),
-                chain(expect("4.0 % 0.0 == 0.0", "4.0 % 0.0 == 0.0")));
+        assertSimplificationSteps(folding::apply, vc("4.0 / 0.0 == 0.0"), chain(expect("4.0 / 0.0 == 0.0")));
+        assertSimplificationSteps(folding::apply, vc("4.0 % 0.0 == 0.0"), chain(expect("4.0 % 0.0 == 0.0")));
     }
 
     @Test
@@ -173,13 +171,12 @@ void recordsOriginWhenFoldingLaterImplication() {
         VCImplication implication = vc("x > 0", "1 + 2 > 0");
 
         VCImplication result = assertSimplificationSteps(folding::apply, implication,
-                chain(expect("x > 0", "x > 0"), expect("3 > 0", "1 + 2 > 0")));
+                chain(expect("x > 0"), expect("3 > 0", "1 + 2 > 0")));
 
         SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
         assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString());
 
-        result = assertSimplificationSteps(folding::apply, result,
-                chain(expect("x > 0", "x > 0"), expect("true", "3 > 0")));
+        result = assertSimplificationSteps(folding::apply, result, chain(expect("x > 0"), expect("true", "3 > 0")));
 
         simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
         assertEquals("3 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString());

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

@@ -76,7 +76,7 @@ void recordsOriginWhenSimplifyingLaterImplication() {
         VCImplication implication = vc("x > 0", "y || false");
 
         VCImplication result = assertSimplificationSteps(simplification::apply, implication,
-                chain(expect("x > 0", "x > 0"), expect("y", "y || false")));
+                chain(expect("x > 0"), expect("y", "y || false")));
 
         SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext());
         assertEquals("y || false", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString());

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

@@ -41,8 +41,8 @@ void simplifyOnceAppliesSubstitutionBeforeBinderSimplification() {
         VCImplication implication = vc("∀x:int. x == 3", "∀y:int. true", "x > 0");
 
         assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
-                chain(expect("true", "∀y:int. true"), expect("3 > 0", "∀x:int. x > 0")),
-                chain(expect("3 > 0", "∀y:int. x > 0")), chain(expect("true", "3 > 0")));
+                chain(expect("true"), expect("3 > 0", "∀x:int. x > 0")), chain(expect("3 > 0", "∀y:int. x > 0")),
+                chain(expect("true", "3 > 0")));
     }
 
     @Test
@@ -138,9 +138,8 @@ void simplifyAppliesLongSubstitutionChainBeforeReachingFixedPoint() {
         VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 1", "∀z:int. z == y + 1", "z == 3");
 
         assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
-                chain(expect("y == 1 + 1", "∀x:int. y == x + 1"), expect("z == y + 1", "∀z:int. z == y + 1"),
-                        expect("z == 3", "z == 3")),
-                chain(expect("z == 1 + 1 + 1", "∀y:int. z == y + 1"), expect("z == 3", "z == 3")),
+                chain(expect("y == 1 + 1", "∀x:int. y == x + 1"), expect("z == y + 1"), expect("z == 3")),
+                chain(expect("z == 1 + 1 + 1", "∀y:int. z == y + 1"), expect("z == 3")),
                 chain(expect("1 + 1 + 1 == 3", "∀z:int. z == 3")), chain(expect("2 + 1 == 3", "1 + 1 + 1 == 3")),
                 chain(expect("3 == 3", "2 + 1 == 3")), chain(expect("true", "3 == 3")));
     }
@@ -150,7 +149,7 @@ void simplifyCombinesSubstitutionAndNestedFoldingAcrossFixedPoint() {
         VCImplication implication = vc("∀x:int. x == 1", "∀y:int. y == x + 2", "y - 1 == 2");
 
         assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
-                chain(expect("y == 1 + 2", "∀x:int. y == x + 2"), expect("y - 1 == 2", "y - 1 == 2")),
+                chain(expect("y == 1 + 2", "∀x:int. y == x + 2"), expect("y - 1 == 2")),
                 chain(expect("1 + 2 - 1 == 2", "∀y:int. y - 1 == 2")), chain(expect("3 - 1 == 2", "1 + 2 - 1 == 2")),
                 chain(expect("2 == 2", "3 - 1 == 2")), chain(expect("true", "2 == 2")));
     }
@@ -167,7 +166,6 @@ void simplifyStopsAfterSubstitutionWhenOnlyNegativeLiteralShapeChanges() {
     void simplifyLeavesUnchangedVcAsPlainPredicates() {
         VCImplication implication = vc("x > 0", "y > x");
 
-        assertSimplificationSteps(VCSimplification::simplifyOnce, implication,
-                chain(expect("x > 0", "x > 0"), expect("y > x", "y > x")));
+        assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x > 0"), expect("y > x")));
     }
 }

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

@@ -49,30 +49,30 @@ void preservesRemainingBinderAfterSubstitution() {
         VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y > x", "y > 0");
 
         assertSimplificationSteps(substitution::apply, implication,
-                chain(expect("y > 3", "∀x:int. y > x"), expect("y > 0", "y > 0")));
+                chain(expect("y > 3", "∀x:int. y > x"), expect("y > 0")));
     }
 
     @Test
     void removesSourceNodeWhenItIsLastInChain() {
         VCImplication implication = vc("x > 0", "∀y:int. y == 1");
 
-        assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 0", "x > 0")));
+        assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 0")));
     }
 
     @Test
     void usesFirstSubstitutionFoundInChain() {
         VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0");
 
         assertSimplificationSteps(substitution::apply, implication,
-                chain(expect("x > 0", "∀x:int. x > 0"), expect("x + 4 > 0", "∀y:int. x + y > 0")));
+                chain(expect("x > 0"), expect("x + 4 > 0", "∀y:int. x + y > 0")));
     }
 
     @Test
     void substitutesInnerKnownValueAcrossNestedImplications() {
         VCImplication implication = vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0");
 
-        assertSimplificationSteps(substitution::apply, implication, chain(expect("true", "∀x:int. true"),
-                expect("z > 1", "∀y:int. z > y"), expect("1 + z > 0", "∀y:int. y + z > 0")));
+        assertSimplificationSteps(substitution::apply, implication,
+                chain(expect("true"), expect("z > 1", "∀y:int. z > y"), expect("1 + z > 0", "∀y:int. y + z > 0")));
     }
 
     @Test
@@ -88,31 +88,27 @@ void substitutesOuterKnownValueIntoNestedBinderRefinements() {
     void ignoresRecursiveBinderEquality() {
         VCImplication implication = vc("∀x:int. x == x + 1", "x > 0");
 
-        assertSimplificationSteps(substitution::apply, implication,
-                chain(expect("x == x + 1", "∀x:int. x == x + 1"), expect("x > 0", "x > 0")));
+        assertSimplificationSteps(substitution::apply, implication, chain(expect("x == x + 1"), expect("x > 0")));
     }
 
     @Test
     void ignoresNonEqualityBinderRefinement() {
         VCImplication implication = vc("∀x:int. x > 3", "x > 0");
 
-        assertSimplificationSteps(substitution::apply, implication,
-                chain(expect("x > 3", "∀x:int. x > 3"), expect("x > 0", "x > 0")));
+        assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 3"), expect("x > 0")));
     }
 
     @Test
     void ignoresDerivedBinderEquality() {
         VCImplication implication = vc("∀x:int. x + 1 == 3", "x > 0");
 
-        assertSimplificationSteps(substitution::apply, implication,
-                chain(expect("x + 1 == 3", "∀x:int. x + 1 == 3"), expect("x > 0", "x > 0")));
+        assertSimplificationSteps(substitution::apply, implication, chain(expect("x + 1 == 3"), expect("x > 0")));
     }
 
     @Test
     void ignoresEqualityWithoutBinder() {
         VCImplication implication = vc("x == 3", "x > 0");
 
-        assertSimplificationSteps(substitution::apply, implication,
-                chain(expect("x == 3", "x == 3"), expect("x > 0", "x > 0")));
+        assertSimplificationSteps(substitution::apply, implication, chain(expect("x == 3"), expect("x > 0")));
     }
 }

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

@@ -1,6 +1,7 @@
 package liquidjava.utils;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertNotNull;
 import static org.junit.jupiter.api.Assertions.assertNull;
 
 import java.util.function.UnaryOperator;
@@ -55,9 +56,14 @@ public static void assertSimplifiedVC(VCImplication implication, ExpectedSimplif
                     "Expected simplified refinement at implication " + i + " to be a plain Predicate");
             assertEquals(expectedPredicate.simplified(), formatRefinement(current),
                     "Unexpected simplified expression at implication " + i);
-            if (expectedPredicate.origin() != null)
-                assertEquals(expectedPredicate.origin(), formatOrigin(current.getOrigin()),
+            if (expectedPredicate.origin() == null)
+                assertNull(current.getOrigin(), "Unexpected origin VC at implication " + i);
+            else {
+                VCImplication origin = current.getOrigin();
+                assertNotNull(origin, "Expected origin VC at implication " + i);
+                assertEquals(expectedPredicate.origin(), formatOrigin(origin),
                         "Unexpected origin VC at implication " + i);
+            }
             current = current.getNext();
         }
         assertNull(current, "Expected VC chain to end after " + expected.length + " implications");
@@ -81,6 +87,10 @@ public static ExpectedSimplifiedVCImplication expect(String simplified, String o
         return new ExpectedSimplifiedVCImplication(simplified, origin);
     }
 
+    public static ExpectedSimplifiedVCImplication expect(String simplified) {
+        return new ExpectedSimplifiedVCImplication(simplified, null);
+    }
+
     private static String formatOrigin(VCImplication origin) {
         if (!origin.hasBinder())
             return formatRefinement(origin);