Remove Unused Fresh Path Binders In Simplification

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

@@ -8,12 +8,15 @@
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.Var;
 
 /**
  * Simplifies VCImplication chains by removing vacuous binder implications
  */
 public class VCBinderSimplification implements VCSimplificationPass {
 
+    private static final String FRESH_PREFIX = "#fresh_";
+
     /**
      * Applies one binder simplification in a VC chain
      */
@@ -34,8 +37,8 @@ private VCImplication simplify(VCImplication implication) {
         if (isFalseBinder(implication))
             return collapseFalseBinder(implication);
 
-        if (isTrueBinder(implication) && !containsVar(implication.getNext(), implication.getName()))
-            return removeTrueBinder(implication);
+        if (isRemovableUnusedBinder(implication))
+            return removeBinder(implication);
 
         VCImplication next = simplify(implication.getNext());
         if (next == null)
@@ -47,12 +50,12 @@ private VCImplication simplify(VCImplication implication) {
     }
 
     /**
-     * Removes a true binder whose name is not used in the suffix
+     * Removes a binder that can be omitted from the suffix
      */
-    private VCImplication removeTrueBinder(VCImplication implication) {
+    private VCImplication removeBinder(VCImplication implication) {
         VCImplication next = implication.getNext();
 
-        // ∀x. true => P -> P
+        // ∀x. true => P -> P, and unused generated path conditions can be omitted from diagnostics
         if (next != null)
             return next.clone();
 
@@ -61,6 +64,28 @@ private VCImplication removeTrueBinder(VCImplication implication) {
         return new VCImplication(truePredicate);
     }
 
+    /**
+     * Checks whether a binder is unused and can be removed without changing the VC conclusion
+     */
+    private boolean isRemovableUnusedBinder(VCImplication implication) {
+        if (!implication.hasBinder() || containsVar(implication.getNext(), implication.getName()))
+            return false;
+
+        return isTrueBinder(implication) || isUnusedFreshPathBinder(implication);
+    }
+
+    /**
+     * Checks for a generated boolean path binder refined exactly by itself
+     */
+    private boolean isUnusedFreshPathBinder(VCImplication implication) {
+        if (!implication.hasNext() || !implication.getName().startsWith(FRESH_PREFIX)
+                || !"boolean".equals(implication.getType().getQualifiedName()))
+            return false;
+
+        return implication.getRefinement().getExpression()instanceof Var var
+                && implication.getName().equals(var.getName());
+    }
+
     /**
      * Replaces a false binder implication with true
      */

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

@@ -1,7 +1,5 @@
 package liquidjava.rj_language.opt;
 
-import java.util.Objects;
-
 import liquidjava.processor.VCImplication;
 
 /**

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

@@ -12,6 +12,21 @@ void removesTrueBinderWhenVariableIsUnusedDownstream() {
         assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "y > 0"), step("y > 0"));
     }
 
+    @Test
+    void removesFreshPathBinderWhenVariableIsUnusedDownstream() {
+        assertSimplificationSteps(binderSimplification, vc("∀#fresh_1:boolean. #fresh_1", "y > 0"), step("y > 0"));
+    }
+
+    @Test
+    void keepsNonTrueBinderWhenVariableIsUnusedDownstream() {
+        assertSimplificationSteps(binderSimplification, vc("∀x:int. x > 0", "y > 0"), step("x > 0", "y > 0"));
+    }
+
+    @Test
+    void keepsNonTrueTerminalBinderAsConclusion() {
+        assertSimplificationSteps(binderSimplification, vc("∀x:int. x > 0"), step("x > 0"));
+    }
+
     @Test
     void keepsTrueBinderWhenVariableIsUsedDownstream() {
         assertSimplificationSteps(binderSimplification, vc("∀x:int. true", "x > 0"), step("true", "x > 0"));

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

@@ -13,11 +13,12 @@
 import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.rj_language.parsing.RefinementsParser;
 import spoon.Launcher;
+import spoon.reflect.factory.TypeFactory;
 import spoon.reflect.reference.CtTypeReference;
 
 public class VCTestUtils {
 
-    private static final CtTypeReference<?> INT = new Launcher().getFactory().Type().INTEGER_PRIMITIVE;
+    private static final TypeFactory TYPE_FACTORY = new Launcher().getFactory().Type();
 
     public static VCImplication vc(String... implications) {
         VCImplication first = null;
@@ -97,7 +98,9 @@ private static VCImplication parseImplication(String implication) {
 
     private static CtTypeReference<?> type(String name) {
         if ("int".equals(name))
-            return INT;
+            return TYPE_FACTORY.INTEGER_PRIMITIVE;
+        if ("boolean".equals(name))
+            return TYPE_FACTORY.BOOLEAN_PRIMITIVE;
         throw new IllegalArgumentException("Unsupported test type: " + name);
     }