Fix VCFunctionSubstitution

Author: rcosta358

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

@@ -1,8 +1,9 @@
 package liquidjava.rj_language.opt;
 
+import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement;
+
 import java.util.Optional;
 
-import liquidjava.processor.SimplifiedVCImplication;
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.BinaryExpression;
@@ -46,41 +47,41 @@ private VCImplication substitute(VCImplication implication, VCImplication node,
 
         // skip the source node to remove it from the chain and start substitution from the next node
         if (implication == node) {
-            VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone());
-            result.setNext(substituteSuffix(implication.getNext(), node, invocation, replacement));
+            VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
+            result.setNext(substituteSuffix(implication.getNext(), invocation, replacement));
             return result;
         }
 
         // preserve the current node and continue rewriting the suffix
-        VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone());
+        VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
         result.setNext(substitute(implication.getNext(), node, invocation, replacement));
         return result;
     }
 
     /**
      * Rewrites every node after the source equality with one function substitution
      */
-    private VCImplication substituteSuffix(VCImplication implication, VCImplication source,
-            FunctionInvocation invocation, Expression replacement) {
+    private VCImplication substituteSuffix(VCImplication implication, FunctionInvocation invocation,
+            Expression replacement) {
         if (implication == null)
             return null;
 
-        VCImplication result = substituteNode(implication, source, invocation, replacement);
-        result.setNext(substituteSuffix(implication.getNext(), source, invocation, replacement));
+        VCImplication result = substituteNode(implication, invocation, replacement);
+        result.setNext(substituteSuffix(implication.getNext(), invocation, replacement));
         return result;
     }
 
     /**
-     * Substitutes one exact function invocation inside one VC node while preserving simplification metadata
+     * Substitutes one exact function invocation inside one VC node
      */
-    private VCImplication substituteNode(VCImplication implication, VCImplication source, FunctionInvocation invocation,
+    private VCImplication substituteNode(VCImplication implication, FunctionInvocation invocation,
             Expression replacement) {
         Expression expression = implication.getRefinement().getExpression().clone();
         if (!containsExpression(expression, invocation))
-            return implication.copyWithRefinement(new Predicate(expression));
+            return copyWithRefinement(implication, new Predicate(expression));
 
         Expression substituted = expression.substitute(invocation, replacement.clone());
-        return new SimplifiedVCImplication(implication, new Predicate(substituted), source);
+        return copyWithRefinement(implication, new Predicate(substituted));
     }
 
     /**

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

@@ -13,63 +13,56 @@ class VCFunctionSubstitutionTest {
     void substitutesExactFunctionInvocationIntoSuffix() {
         VCImplication implication = vc("f(x) == 0", "f(y) == f(x) + 1");
 
-        assertSimplificationSteps(substitution::apply, implication,
-                chain(expect("f(x) == 0"), expect("f(y) == 0 + 1", "f(x) == 0")));
+        assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "f(y) == 0 + 1"));
     }
 
     @Test
     void substitutesReverseFunctionEquality() {
         VCImplication implication = vc("0 == f(x)", "f(y) == f(x) + 1");
 
-        assertSimplificationSteps(substitution::apply, implication,
-                chain(expect("0 == f(x)"), expect("f(y) == 0 + 1", "0 == f(x)")));
+        assertSimplificationSteps(substitution::apply, implication, step("0 == f(x)", "f(y) == 0 + 1"));
     }
 
     @Test
     void preservesSourceNode() {
         VCImplication implication = vc("f(x) == 0", "f(x) > -1");
 
-        assertSimplificationSteps(substitution::apply, implication,
-                chain(expect("f(x) == 0"), expect("0 > -1", "f(x) == 0")));
+        assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "0 > -1"));
     }
 
     @Test
     void doesNotRewriteEarlierNodesFromLaterEquality() {
         VCImplication implication = vc("f(x) > 0", "f(x) == 1");
 
-        assertSimplificationSteps(substitution::apply, implication, chain(expect("f(x) > 0"), expect("f(x) == 1")));
+        assertSimplificationSteps(substitution::apply, implication, step("f(x) > 0", "f(x) == 1"));
     }
 
     @Test
     void skipsUsedUpEqualityAndUsesNextAvailableEquality() {
         VCImplication implication = vc("f(x) == 0", "f(y) == f(x) + 1", "f(y) == 1");
 
-        assertSimplificationSteps(substitution::apply, implication,
-                chain(expect("f(x) == 0"), expect("f(y) == 0 + 1", "f(x) == 0"), expect("f(y) == 1")),
-                chain(expect("f(x) == 0"), expect("f(y) == 0 + 1", "f(x) == 0"),
-                        expect("0 + 1 == 1", "f(y) == 0 + 1")));
+        assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "f(y) == 0 + 1", "f(y) == 1"),
+                step("f(x) == 0", "f(y) == 0 + 1", "0 + 1 == 1"));
     }
 
     @Test
     void doesNotGeneralizeAcrossDifferentArguments() {
         VCImplication implication = vc("f(x) == 0", "f(y) == 0");
 
-        assertSimplificationSteps(substitution::apply, implication, chain(expect("f(x) == 0"), expect("f(y) == 0")));
+        assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "f(y) == 0"));
     }
 
     @Test
     void ignoresRecursiveFunctionEquality() {
         VCImplication implication = vc("f(x) == f(x) + 1", "f(x) > 0");
 
-        assertSimplificationSteps(substitution::apply, implication,
-                chain(expect("f(x) == f(x) + 1"), expect("f(x) > 0")));
+        assertSimplificationSteps(substitution::apply, implication, step("f(x) == f(x) + 1", "f(x) > 0"));
     }
 
     @Test
     void extractsEqualityFromTopLevelConjunction() {
         VCImplication implication = vc("ok && f(x) == 0", "f(y) == f(x) + 1");
 
-        assertSimplificationSteps(substitution::apply, implication,
-                chain(expect("ok && f(x) == 0"), expect("f(y) == 0 + 1", "ok && f(x) == 0")));
+        assertSimplificationSteps(substitution::apply, implication, step("ok && f(x) == 0", "f(y) == 0 + 1"));
     }
 }

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

@@ -11,6 +11,7 @@
 import com.pholser.junit.quickcheck.runner.JUnitQuickcheck;
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.Context;
+import liquidjava.processor.context.GhostFunction;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
@@ -19,12 +20,15 @@
 import liquidjava.smt.SMTResult;
 import liquidjava.utils.TestUtils;
 import org.junit.runner.RunWith;
+import spoon.Launcher;
+import spoon.reflect.factory.Factory;
 
 @RunWith(JUnitQuickcheck.class)
 public class VCSimplificationPropertyBasedTest {
 
     private static final int TRIALS = 50; // number of random VCs to test
     private static final int MAX_STEPS = 20; // to prevent infinite loops in case of non-termination
+    private static final Factory FACTORY = new Launcher().getFactory();
 
     @Property(trials = TRIALS)
     public void eachSimplificationStepPreservesVcSemantics(@From(VCImplicationGenerator.class) VCImplication vc) {
@@ -50,6 +54,9 @@ private static void setUpContext() {
             TestUtils.addIntVariableToContext(variable);
         for (String variable : VCImplicationGenerator.FREE_VARS)
             TestUtils.addIntVariableToContext(variable);
+        for (String function : VCImplicationGenerator.FUNCTIONS)
+            Context.getInstance().addGhostFunction(
+                    new GhostFunction(function, List.of("int"), FACTORY.Type().INTEGER_PRIMITIVE, FACTORY, ""));
     }
 
     private static void assertEquivalent(VCImplication unsimplified, VCImplication simplified, int step) {