Track Simplification Origins by Full VC Implication

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -9,6 +9,7 @@
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
+import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.smt.Counterexample;
 import spoon.reflect.cu.SourcePosition;
 
@@ -20,13 +21,15 @@
 public class RefinementError extends LJError {
 
     private final Predicate expected;
-    private final VCImplication found;
+    private final VCSimplificationResult found;
     private final Counterexample counterexample;
 
-    public RefinementError(SourcePosition position, Predicate expected, VCImplication found,
+    public RefinementError(SourcePosition position, Predicate expected, VCSimplificationResult found,
             TranslationTable translationTable, Counterexample counterexample, String customMessage) {
-        super("Refinement Error", String.format("%s is not a subtype of %s",
-                found.toPredicate().getExpression().toDisplayString(), expected.getExpression().toDisplayString()),
+        super("Refinement Error",
+                String.format("%s is not a subtype of %s",
+                        found.getImplication().toPredicate().getExpression().toDisplayString(),
+                        expected.getExpression().toDisplayString()),
                 position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
@@ -46,7 +49,7 @@ public String getCounterExampleString() {
             return null;
 
         List<String> foundVarNames = new ArrayList<>();
-        Expression foundExpression = found.toPredicate().getExpression();
+        Expression foundExpression = getFound().getImplication().toPredicate().getExpression();
         Expression expectedExpression = expected.getExpression();
         foundExpression.getVariableNames(foundVarNames);
         // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the
@@ -77,7 +80,7 @@ public Predicate getExpected() {
         return expected;
     }
 
-    public VCImplication getFound() {
+    public VCSimplificationResult getFound() {
         return found;
     }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -3,6 +3,7 @@
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.opt.VCSimplificationResult;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -13,13 +14,13 @@
 public class StateRefinementError extends LJError {
 
     private final Predicate expected;
-    private final VCImplication found;
+    private final VCSimplificationResult found;
 
-    public StateRefinementError(SourcePosition position, Predicate expected, VCImplication found,
+    public StateRefinementError(SourcePosition position, Predicate expected, VCSimplificationResult found,
             TranslationTable translationTable, String customMessage) {
         super("State Refinement Error",
                 String.format("Expected state %s but found %s", expected.getExpression().toDisplayString(),
-                        found.toPredicate().getExpression().toDisplayString()),
+                        found.getImplication().toPredicate().getExpression().toDisplayString()),
                 position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
@@ -30,6 +31,10 @@ public Predicate getExpected() {
     }
 
     public VCImplication getFound() {
+        return found.getImplication();
+    }
+
+    public VCSimplificationResult getFoundSimplification() {
         return found;
     }
 }

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

@@ -4,6 +4,7 @@
 
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.opt.VCSimplification;
+import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.utils.Utils;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -32,21 +33,6 @@ public VCImplication(VCImplication implication, Predicate ref) {
         this.refinement = ref;
     }
 
-    public VCImplication getOrigin() {
-        return null;
-    }
-
-    public Predicate getOriginRefinement() {
-        VCImplication origin = getOrigin();
-        if (origin == null)
-            return refinement.clone();
-        return origin.getRefinement().clone();
-    }
-
-    public VCImplication copyWithRefinement(Predicate refinement) {
-        return new VCImplication(this, refinement);
-    }
-
     public void setNext(VCImplication c) {
         next = c;
     }
@@ -89,7 +75,7 @@ public String toString() {
             return String.format("%-20s %s", "", refinement.toString());
     }
 
-    public VCImplication simplify() {
+    public VCSimplificationResult simplify() {
         return VCSimplification.simplifyToFixedPoint(this);
     }
 

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -10,6 +10,7 @@
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.NotFoundError;
 import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.GhostFunction;
@@ -259,12 +260,6 @@ public Predicate getOrigin() {
         return this;
     }
 
-    public VCImplication simplify() {
-        VCImplication result = new VCImplication(clone()).simplify();
-        DebugLog.simplification(this.getExpression(), result.getRefinement().getExpression());
-        return result;
-    }
-
     private static boolean isBooleanLiteral(Expression expr, boolean value) {
         return expr instanceof LiteralBoolean && expr.isBooleanTrue() == value;
     }

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

@@ -1,10 +1,10 @@
 package liquidjava.rj_language.opt;
 
 import static liquidjava.rj_language.opt.VCSimplificationUtils.containsVar;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isFalse;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
 
-import liquidjava.processor.SimplifiedVCImplication;
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.LiteralBoolean;
@@ -41,7 +41,7 @@ private VCImplication simplify(VCImplication implication) {
         if (next == null)
             return null;
 
-        VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone());
+        VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
         result.setNext(next);
         return result;
     }
@@ -53,17 +53,12 @@ private VCImplication removeTrueBinder(VCImplication implication) {
         VCImplication next = implication.getNext();
 
         // ∀x. true => P -> P
-        if (next != null) {
-            VCImplication origin = new VCImplication(implication.getName(), implication.getType(),
-                    next.getOriginRefinement());
-            VCImplication result = new SimplifiedVCImplication(next, next.getRefinement().clone(), origin);
-            result.setNext(next.getNext() == null ? null : next.getNext().clone());
-            return result;
-        }
+        if (next != null)
+            return next.clone();
 
         // ∀x. true -> true
         Predicate truePredicate = new Predicate(new LiteralBoolean(true));
-        return new SimplifiedVCImplication(new VCImplication(truePredicate), truePredicate, implication);
+        return new VCImplication(truePredicate);
     }
 
     /**
@@ -72,7 +67,7 @@ private VCImplication removeTrueBinder(VCImplication implication) {
     private VCImplication collapseFalseBinder(VCImplication implication) {
         // ∀x. false => P -> true
         Predicate truePredicate = new Predicate(new LiteralBoolean(true));
-        return new SimplifiedVCImplication(new VCImplication(truePredicate), truePredicate, implication);
+        return new VCImplication(truePredicate);
     }
 
     /**

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

@@ -1,6 +1,7 @@
 package liquidjava.rj_language.opt;
 
-import liquidjava.processor.SimplifiedVCImplication;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement;
+
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
@@ -32,7 +33,7 @@ private VCImplication apply(VCImplication implication, C context) {
         Expression expression = implication.getRefinement().getExpression();
         Expression simplified = simplify(expression, context);
         if (!expression.equals(simplified)) {
-            VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), implication);
+            VCImplication result = copyWithRefinement(implication, new Predicate(simplified));
             result.setNext(implication.getNext() == null ? null : implication.getNext().clone());
             return result;
         }
@@ -41,7 +42,7 @@ private VCImplication apply(VCImplication implication, C context) {
         if (implication.getNext() == null || implication.getNext().equals(next))
             return implication;
 
-        VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone());
+        VCImplication result = copyWithRefinement(implication, implication.getRefinement().clone());
         result.setNext(next);
         return result;
     }

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

@@ -15,32 +15,41 @@ public class VCSimplification {
     /**
      * Applies all available simplification steps to a VC chain until a fixed point is reached
      */
-    public static VCImplication simplifyToFixedPoint(VCImplication implication) {
+    public static VCSimplificationResult simplifyToFixedPoint(VCImplication implication) {
         if (implication == null)
             return null;
 
-        // keep applying simplification steps until a fixed point is reached
-        VCImplication current = implication.clone();
+        VCSimplificationResult current = new VCSimplificationResult(implication);
         while (true) {
-            VCImplication simplified = simplifyOnce(current);
-            if (current.equals(simplified))
-                return simplified; // fixed point reached
+            VCSimplificationResult simplified = simplifyOnce(current);
+            if (simplified == current)
+                return current; // fixed point reached
             current = simplified;
         }
     }
 
     /**
-     * Applies one simplification step to a VC chain
+     * Applies one simplification step to a VC chain from all available simplification passes
      */
-    public static VCImplication simplifyOnce(VCImplication implication) {
-        if (implication == null)
-            return null;
-
+    public static VCSimplificationResult simplifyOnce(VCSimplificationResult implication) {
         for (VCSimplificationPass pass : PASSES) {
-            VCImplication simplified = pass.apply(implication);
-            if (!implication.equals(simplified))
+            VCSimplificationResult simplified = simplifyOnce(implication, pass);
+            if (simplified != implication)
                 return simplified;
         }
         return implication;
     }
+
+    /**
+     * Applies one selected simplification pass to a VC chain
+     */
+    public static VCSimplificationResult simplifyOnce(VCSimplificationResult implication, VCSimplificationPass pass) {
+        if (implication == null)
+            return null;
+
+        VCImplication simplified = pass.apply(implication.getImplication());
+        if (implication.getImplication().equals(simplified))
+            return implication;
+        return new VCSimplificationResult(simplified, implication);
+    }
 }

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

@@ -0,0 +1,44 @@
+package liquidjava.rj_language.opt;
+
+import java.util.Objects;
+
+import liquidjava.processor.VCImplication;
+
+/**
+ * Result of simplifying VC implication chain
+ */
+public final class VCSimplificationResult {
+
+    private final VCImplication implication;
+    private final VCSimplificationResult origin;
+
+    public VCSimplificationResult(VCImplication implication) {
+        this(implication, null);
+    }
+
+    public VCSimplificationResult(VCImplication implication, VCSimplificationResult origin) {
+        this.implication = Objects.requireNonNull(implication).clone();
+        this.origin = origin;
+    }
+
+    /**
+     * Returns the simplified VC chain represented by this result
+     */
+    public VCImplication getImplication() {
+        return implication;
+    }
+
+    /**
+     * Returns the origin of this simplification result or null if this result is the original VC chain
+     */
+    public VCSimplificationResult getOrigin() {
+        return origin;
+    }
+
+    @Override
+    public String toString() {
+        if (origin == null)
+            return "\n" + implication;
+        return "\n" + implication + "\n" + origin.toString().indent(2).stripTrailing();
+    }
+}

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

@@ -4,11 +4,16 @@
 import java.util.List;
 
 import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.LiteralBoolean;
 
 public final class VCSimplificationUtils {
 
+    public static VCImplication copyWithRefinement(VCImplication implication, Predicate refinement) {
+        return new VCImplication(implication, refinement);
+    }
+
     public static boolean containsVar(Expression expression, String name) {
         List<String> names = new ArrayList<>();
         expression.getVariableNames(names);