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