Fix VC Function Substitution

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java

@@ -93,7 +93,7 @@ public int hashCode() {
         final int prime = 31;
         int result = 1;
         result = prime * result + ((getArgs() == null) ? 0 : getArgs().hashCode());
-        result = prime * result + ((name == null) ? 0 : name.hashCode());
+        result = prime * result + ((name == null) ? 0 : Utils.getSimpleName(name).hashCode()); // same here
         return result;
     }
 
@@ -114,7 +114,10 @@ public boolean equals(Object obj) {
         if (name == null) {
             return other.name == null;
         } else {
-            return name.equals(other.name);
+            // prefixes are inconsistent for refined class ghost calls: some use the
+            // original class prefix, others use the caller class prefix
+            // for now we compare simple names, but prefix handling should be fixed instead of having this workaround
+            return other.name != null && Utils.getSimpleName(name).equals(Utils.getSimpleName(other.name));
         }
     }
 }

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

@@ -1,7 +1,10 @@
 package liquidjava.rj_language.opt;
 
 import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.containsExpression;
 
+import java.util.ArrayList;
+import java.util.List;
 import java.util.Optional;
 
 import liquidjava.processor.VCImplication;
@@ -18,7 +21,8 @@ public class VCFunctionSubstitution implements VCSimplificationPass {
     /**
      * A substitution discovered from a function invocation equality
      */
-    private record Substitution(VCImplication node, FunctionInvocation invocation, Expression replacement) {
+    private record Substitution(VCImplication node, FunctionInvocation invocation, Expression replacement,
+            Expression sourceEquality) {
     }
 
     /**
@@ -31,32 +35,52 @@ public VCImplication apply(VCImplication implication) {
 
         if (substitutionOpt.isPresent()) {
             Substitution substitution = substitutionOpt.get();
-            result = substitute(result, substitution.node(), substitution.invocation(), substitution.replacement());
+            result = substitute(result, substitution.node(), substitution.invocation(), substitution.replacement(),
+                    substitution.sourceEquality());
         }
         return result;
     }
 
     /**
-     * Preserves nodes before the source equality and starts rewriting at the source suffix
+     * Rewrites one VC chain with a single substitution and removes its source equality
      */
     private VCImplication substitute(VCImplication implication, VCImplication node, FunctionInvocation invocation,
-            Expression replacement) {
+            Expression replacement, Expression sourceEquality) {
         if (implication == null)
             return null;
 
-        // skip the source node to remove it from the chain and start substitution from the next node
+        // consume the source equality and start substitution from the next node
         if (implication == node) {
-            VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
-            result.setNext(substituteSuffix(implication.getNext(), invocation, replacement));
-            return result;
+            VCImplication suffix = substituteSuffix(implication.getNext(), invocation, replacement);
+            VCImplication source = removeSourceEquality(implication, sourceEquality);
+            if (source == null)
+                return suffix;
+            source.setNext(suffix);
+            return source;
         }
 
         // preserve the current node and continue rewriting the suffix
         VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
-        result.setNext(substitute(implication.getNext(), node, invocation, replacement));
+        result.setNext(substitute(implication.getNext(), node, invocation, replacement, sourceEquality));
         return result;
     }
 
+    /**
+     * Removes the equality conjunct that supplied the substitution, preserving any sibling conjuncts
+     */
+    private VCImplication removeSourceEquality(VCImplication implication, Expression sourceEquality) {
+        List<Expression> remaining = new ArrayList<>(implication.getRefinement().getExpression().getConjuncts());
+        if (!remaining.remove(sourceEquality))
+            return copyWithRefinement(implication, implication.getRefinement().clone());
+        if (remaining.isEmpty())
+            return null;
+
+        Predicate refinement = new Predicate();
+        for (Expression conjunct : remaining)
+            refinement = Predicate.createConjunction(refinement, new Predicate(conjunct.clone()));
+        return copyWithRefinement(implication, refinement);
+    }
+
     /**
      * Rewrites every node after the source equality with one function substitution
      */
@@ -121,33 +145,13 @@ private Optional<Substitution> getSubstitution(VCImplication implication, Expres
         Expression left = binary.getFirstOperand();
         Expression right = binary.getSecondOperand();
         if (left instanceof FunctionInvocation invocation && !containsExpression(right, left))
-            return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), right.clone()));
+            return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), right.clone(),
+                    binary.clone()));
         if (right instanceof FunctionInvocation invocation && !containsExpression(left, right))
-            return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), left.clone()));
+            return Optional.of(new Substitution(implication, (FunctionInvocation) invocation.clone(), left.clone(),
+                    binary.clone()));
 
         return Optional.empty();
     }
 
-    /**
-     * Checks whether an expression contains another expression
-     */
-    private boolean containsExpression(Expression expression, Expression target) {
-        if (expression.equals(target))
-            return true;
-
-        for (Expression child : expression.getChildren())
-            if (containsExpression(child, target))
-                return true;
-        return false;
-    }
-
-    /**
-     * Checks whether a VC suffix contains an expression
-     */
-    private boolean containsExpression(VCImplication implication, Expression target) {
-        for (VCImplication current = implication; current != null; current = current.getNext())
-            if (containsExpression(current.getRefinement().getExpression(), target))
-                return true;
-        return false;
-    }
 }

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

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

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

@@ -28,6 +28,23 @@ public static boolean containsVar(VCImplication implication, String name) {
         return false;
     }
 
+    public static boolean containsExpression(Expression expression, Expression target) {
+        if (expression.equals(target))
+            return true;
+
+        for (Expression child : expression.getChildren())
+            if (containsExpression(child, target))
+                return true;
+        return false;
+    }
+
+    public static boolean containsExpression(VCImplication implication, Expression target) {
+        for (VCImplication current = implication; current != null; current = current.getNext())
+            if (containsExpression(current.getRefinement().getExpression(), target))
+                return true;
+        return false;
+    }
+
     public static boolean isTrue(Expression expression) {
         return expression instanceof LiteralBoolean literal && literal.isBooleanTrue();
     }

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

@@ -13,21 +13,21 @@ class VCFunctionSubstitutionTest {
     void substitutesExactFunctionInvocationIntoSuffix() {
         VCImplication implication = vc("f(x) == 0", "f(y) == f(x) + 1");
 
-        assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "f(y) == 0 + 1"));
+        assertSimplificationSteps(substitution::apply, implication, step("f(y) == 0 + 1"));
     }
 
     @Test
     void substitutesReverseFunctionEquality() {
         VCImplication implication = vc("0 == f(x)", "f(y) == f(x) + 1");
 
-        assertSimplificationSteps(substitution::apply, implication, step("0 == f(x)", "f(y) == 0 + 1"));
+        assertSimplificationSteps(substitution::apply, implication, step("f(y) == 0 + 1"));
     }
 
     @Test
-    void preservesSourceNode() {
+    void consumesSourceNodeWhenSubstitutedInvocationIsGoneFromSuffix() {
         VCImplication implication = vc("f(x) == 0", "f(x) > -1");
 
-        assertSimplificationSteps(substitution::apply, implication, step("f(x) == 0", "0 > -1"));
+        assertSimplificationSteps(substitution::apply, implication, step("0 > -1"));
     }
 
     @Test
@@ -41,8 +41,8 @@ void doesNotRewriteEarlierNodesFromLaterEquality() {
     void skipsUsedUpEqualityAndUsesNextAvailableEquality() {
         VCImplication implication = vc("f(x) == 0", "f(y) == f(x) + 1", "f(y) == 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"));
+        assertSimplificationSteps(substitution::apply, implication, step("f(y) == 0 + 1", "f(y) == 1"),
+                step("0 + 1 == 1"));
     }
 
     @Test
@@ -63,6 +63,13 @@ void ignoresRecursiveFunctionEquality() {
     void extractsEqualityFromTopLevelConjunction() {
         VCImplication implication = vc("ok && f(x) == 0", "f(y) == f(x) + 1");
 
-        assertSimplificationSteps(substitution::apply, implication, step("ok && f(x) == 0", "f(y) == 0 + 1"));
+        assertSimplificationSteps(substitution::apply, implication, step("ok", "f(y) == 0 + 1"));
+    }
+
+    @Test
+    void removesOnlySourceEqualityConjunct() {
+        VCImplication implication = vc("ok && f(x) == 0 && ready", "f(y) == f(x) + 1");
+
+        assertSimplificationSteps(substitution::apply, implication, step("ok && ready", "f(y) == 0 + 1"));
     }
 }

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

@@ -2,6 +2,7 @@
 
 import static org.junit.jupiter.api.Assertions.assertTrue;
 import static org.junit.jupiter.api.Assertions.fail;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.containsExpression;
 
 import java.util.ArrayList;
 import java.util.List;
@@ -15,6 +16,7 @@
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.FunctionInvocation;
 import liquidjava.rj_language.ast.Var;
 import liquidjava.smt.SMTEvaluator;
 import liquidjava.smt.SMTResult;
@@ -81,10 +83,28 @@ private static Predicate substitutionPremises(VCImplication implication) {
         for (VCImplication current = implication; current != null; current = current.getNext()) {
             if (isSubstitution(current))
                 premises = Predicate.createConjunction(premises, current.getRefinement());
+            for (Expression conjunct : current.getRefinement().getExpression().getConjuncts()) {
+                if (!isFunctionSubstitution(conjunct, current.getNext()))
+                    continue;
+                premises = Predicate.createConjunction(premises, new Predicate(conjunct.clone()));
+            }
         }
         return premises;
     }
 
+    private static boolean isFunctionSubstitution(Expression expression, VCImplication suffix) {
+        if (!(expression instanceof BinaryExpression binary) || !"==".equals(binary.getOperator()))
+            return false;
+
+        Expression left = binary.getFirstOperand();
+        Expression right = binary.getSecondOperand();
+        if (left instanceof FunctionInvocation && !containsExpression(right, left))
+            return containsExpression(suffix, left);
+        if (right instanceof FunctionInvocation && !containsExpression(left, right))
+            return containsExpression(suffix, right);
+        return false;
+    }
+
     private static boolean isSubstitution(VCImplication implication) {
         if (!implication.hasBinder())
             return false;