Remove Unused Fresh Path Binders In Simplification

Author: rcosta358

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
      */
@@ -47,12 +50,12 @@ private VCImplication simplify(VCImplication implication) {
     }
 
     /**
-     * Removes a binder whose name is not used in the suffix
+     * Removes a binder that can be omitted from the suffix
      */
     private VCImplication removeBinder(VCImplication implication) {
         VCImplication next = implication.getNext();
 
-        // ∀x. R => P -> P when x is not used in P
+        // ∀x. true => P -> P, and unused generated path conditions can be omitted from diagnostics
         if (next != null)
             return next.clone();
 
@@ -62,13 +65,25 @@ private VCImplication removeBinder(VCImplication implication) {
     }
 
     /**
-     * Checks whether a binder is unused and can be removed
+     * 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 implication.hasNext() || isTrueBinder(implication);
+        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());
     }
 
     /**

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

@@ -13,8 +13,13 @@ void removesTrueBinderWhenVariableIsUnusedDownstream() {
     }
 
     @Test
-    void removesNonTrueBinderWhenVariableIsUnusedDownstream() {
-        assertSimplificationSteps(binderSimplification, vc("∀x:int. x > 0", "y > 0"), step("y > 0"));
+    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

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

@@ -108,13 +108,14 @@ void simplifyUsesLogicalSimplificationToEnableSubstitutionOnNextStep() {
     }
 
     @Test
-    void simplifyRemovesUnusedBinderBeforeFolding() {
-        assertSimplificationSteps(vc("∀x:int. 1 > 2", "y > 0"), step("y > 0"));
+    void simplifyUsesFoldingToEnableBinderSimplificationOnNextStep() {
+        assertSimplificationSteps(vc("∀x:int. 1 > 2", "y > 0"), step("false", "y > 0"), step("true"));
     }
 
     @Test
-    void simplifyRemovesUnusedBinderBeforeArithmeticAndLogicalSimplification() {
-        assertSimplificationSteps(vc("∀x:int. x + 0 == x", "y > 0"), step("y > 0"));
+    void simplifyUsesArithmeticAndLogicalSimplificationToEnableBinderRemoval() {
+        assertSimplificationSteps(vc("∀x:int. x + 0 == x", "y > 0"), step("x == x", "y > 0"), step("true", "y > 0"),
+                step("y > 0"));
     }
 
     @Test

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);
     }