Simplification Fixes (#125)

Author: rcosta358

liquidjava-verifier/pom.xml

@@ -11,7 +11,7 @@
 
 	<groupId>io.github.liquid-java</groupId>
 	<artifactId>liquidjava-verifier</artifactId>
-	<version>0.0.4</version>
+	<version>0.0.8</version>
 	<name>liquidjava-verifier</name>
 	<description>LiquidJava Verifier</description>
 	<url>https://github.com/liquid-java/liquidjava</url>

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

@@ -12,19 +12,18 @@
  */
 public class RefinementError extends LJError {
 
-    private final String expected;
+    private final ValDerivationNode expected;
     private final ValDerivationNode found;
 
-    public RefinementError(SourcePosition position, Expression expected, ValDerivationNode found,
+    public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
             TranslationTable translationTable) {
-        super("Refinement Error",
-                String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), position,
-                translationTable);
-        this.expected = expected.toSimplifiedString();
+        super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()),
+                position, translationTable);
+        this.expected = expected;
         this.found = found;
     }
 
-    public String getExpected() {
+    public ValDerivationNode getExpected() {
         return expected;
     }
 

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -52,8 +52,8 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         }
         boolean isSubtype = smtChecks(expected, premises, element.getPosition());
         if (!isSubtype)
-            throw new RefinementError(element.getPosition(), expectedType.getExpression(),
-                    premisesBeforeChange.simplify(), map);
+            throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(),
+                    map);
     }
 
     /**
@@ -263,7 +263,7 @@ protected void throwRefinementError(SourcePosition position, Predicate expected,
         gatherVariables(found, lrv, mainVars);
         TranslationTable map = new TranslationTable();
         Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions();
-        throw new RefinementError(position, expected.getExpression(), premises.simplify(), map);
+        throw new RefinementError(position, expected.simplify(), premises.simplify(), map);
     }
 
     protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected)

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

@@ -271,7 +271,7 @@ public void validateGhostInvocations(Context ctx, Factory f) throws LJError {
         if (this instanceof FunctionInvocation fi) {
             // get all ghosts with the matching name
             List<GhostFunction> candidates = ctx.getGhosts().stream().filter(g -> g.matches(fi.name)).toList();
-            if (candidates.isEmpty()) 
+            if (candidates.isEmpty())
                 return; // not found error is thrown elsewhere
 
             // find matching overload

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

@@ -10,6 +10,7 @@
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import liquidjava.rj_language.opt.derivation_node.VarDerivationNode;
 
+import java.util.HashMap;
 import java.util.Map;
 
 public class ConstantPropagation {
@@ -19,55 +20,71 @@ public class ConstantPropagation {
      * VariableResolver to extract variable equalities from the expression first. Returns a derivation node representing
      * the propagation steps taken.
      */
-    public static ValDerivationNode propagate(Expression exp) {
+    public static ValDerivationNode propagate(Expression exp, ValDerivationNode previousOrigin) {
         Map<String, Expression> substitutions = VariableResolver.resolve(exp);
-        return propagateRecursive(exp, substitutions);
+
+        // map of variable origins from the previous derivation tree
+        Map<String, DerivationNode> varOrigins = new HashMap<>();
+        if (previousOrigin != null) {
+            extractVarOrigins(previousOrigin, varOrigins);
+        }
+        return propagateRecursive(exp, substitutions, varOrigins);
     }
 
     /**
      * Recursively performs constant propagation on an expression (e.g. x + y && x == 1 && y == 2 => 1 + 2)
      */
-    private static ValDerivationNode propagateRecursive(Expression exp, Map<String, Expression> subs) {
+    private static ValDerivationNode propagateRecursive(Expression exp, Map<String, Expression> subs,
+            Map<String, DerivationNode> varOrigins) {
 
         // substitute variable
         if (exp instanceof Var var) {
             String name = var.getName();
             Expression value = subs.get(name);
             // substitution
-            if (value != null)
-                return new ValDerivationNode(value.clone(), new VarDerivationNode(name));
+            if (value != null) {
+                // check if this variable has an origin from a previous pass
+                DerivationNode previousOrigin = varOrigins.get(name);
+
+                // preserve origin if value came from previous derivation
+                DerivationNode origin = previousOrigin != null ? new VarDerivationNode(name, previousOrigin)
+                        : new VarDerivationNode(name);
+                return new ValDerivationNode(value.clone(), origin);
+            }
 
             // no substitution
             return new ValDerivationNode(var, null);
         }
 
         // lift unary origin
         if (exp instanceof UnaryExpression unary) {
-            ValDerivationNode operand = propagateRecursive(unary.getChildren().get(0), subs);
-            unary.setChild(0, operand.getValue());
+            ValDerivationNode operand = propagateRecursive(unary.getChildren().get(0), subs, varOrigins);
+            UnaryExpression cloned = (UnaryExpression) unary.clone();
+            cloned.setChild(0, operand.getValue());
 
-            DerivationNode origin = operand.getOrigin() != null ? new UnaryDerivationNode(operand, unary.getOp())
-                    : null;
-            return new ValDerivationNode(unary, origin);
+            return operand.getOrigin() != null
+                    ? new ValDerivationNode(cloned, new UnaryDerivationNode(operand, cloned.getOp()))
+                    : new ValDerivationNode(cloned, null);
         }
 
         // lift binary origin
         if (exp instanceof BinaryExpression binary) {
-            ValDerivationNode left = propagateRecursive(binary.getFirstOperand(), subs);
-            ValDerivationNode right = propagateRecursive(binary.getSecondOperand(), subs);
-            binary.setChild(0, left.getValue());
-            binary.setChild(1, right.getValue());
-
-            DerivationNode origin = (left.getOrigin() != null || right.getOrigin() != null)
-                    ? new BinaryDerivationNode(left, right, binary.getOperator()) : null;
-            return new ValDerivationNode(binary, origin);
+            ValDerivationNode left = propagateRecursive(binary.getFirstOperand(), subs, varOrigins);
+            ValDerivationNode right = propagateRecursive(binary.getSecondOperand(), subs, varOrigins);
+            BinaryExpression cloned = (BinaryExpression) binary.clone();
+            cloned.setChild(0, left.getValue());
+            cloned.setChild(1, right.getValue());
+
+            return (left.getOrigin() != null || right.getOrigin() != null)
+                    ? new ValDerivationNode(cloned, new BinaryDerivationNode(left, right, cloned.getOperator()))
+                    : new ValDerivationNode(cloned, null);
         }
 
         // recursively propagate children
         if (exp.hasChildren()) {
             Expression propagated = exp.clone();
             for (int i = 0; i < exp.getChildren().size(); i++) {
-                ValDerivationNode child = propagateRecursive(exp.getChildren().get(i), subs);
+                ValDerivationNode child = propagateRecursive(exp.getChildren().get(i), subs, varOrigins);
                 propagated.setChild(i, child.getValue());
             }
             return new ValDerivationNode(propagated, null);
@@ -76,4 +93,49 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map<String,
         // no propagation
         return new ValDerivationNode(exp, null);
     }
+
+    /**
+     * Extracts the derivation nodes for variable values from the derivation tree This is so done so when we find "var
+     * == value" in the tree, we store the derivation of the value So it can be preserved when var is substituted in
+     * subsequent passes
+     */
+    private static void extractVarOrigins(ValDerivationNode node, Map<String, DerivationNode> varOrigins) {
+        if (node == null)
+            return;
+
+        Expression value = node.getValue();
+        DerivationNode origin = node.getOrigin();
+
+        // check for equality expressions
+        if (value instanceof BinaryExpression binExp && "==".equals(binExp.getOperator())
+                && origin instanceof BinaryDerivationNode binOrigin) {
+            Expression left = binExp.getFirstOperand();
+            Expression right = binExp.getSecondOperand();
+
+            // extract variable name and value derivation from either side
+            String varName = null;
+            ValDerivationNode valueDerivation = null;
+
+            if (left instanceof Var var && right.isLiteral()) {
+                varName = var.getName();
+                valueDerivation = binOrigin.getRight();
+            } else if (right instanceof Var var && left.isLiteral()) {
+                varName = var.getName();
+                valueDerivation = binOrigin.getLeft();
+            }
+            if (varName != null && valueDerivation != null && valueDerivation.getOrigin() != null) {
+                varOrigins.put(varName, valueDerivation.getOrigin());
+            }
+        }
+
+        // recursively process the origin tree
+        if (origin instanceof BinaryDerivationNode binOrigin) {
+            extractVarOrigins(binOrigin.getLeft(), varOrigins);
+            extractVarOrigins(binOrigin.getRight(), varOrigins);
+        } else if (origin instanceof UnaryDerivationNode unaryOrigin) {
+            extractVarOrigins(unaryOrigin.getOperand(), varOrigins);
+        } else if (origin instanceof ValDerivationNode valOrigin) {
+            extractVarOrigins(valOrigin, varOrigins);
+        }
+    }
 }

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

@@ -14,41 +14,88 @@ public class ExpressionSimplifier {
      * Returns a derivation node representing the tree of simplifications applied
      */
     public static ValDerivationNode simplify(Expression exp) {
-        ValDerivationNode prop = ConstantPropagation.propagate(exp);
+        ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp);
+        return simplifyValDerivationNode(fixedPoint);
+    }
+
+    /**
+     * Recursively applies propagation and folding until the expression stops changing (fixed point) Stops early if the
+     * expression simplifies to 'true', which means we've simplified too much
+     */
+    private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, Expression prevExp) {
+        // apply propagation and folding
+        ValDerivationNode prop = ConstantPropagation.propagate(prevExp, current);
         ValDerivationNode fold = ConstantFolding.fold(prop);
-        return simplifyDerivationTree(fold);
+        ValDerivationNode simplified = simplifyValDerivationNode(fold);
+        Expression currExp = simplified.getValue();
+
+        // fixed point reached
+        if (current != null && currExp.equals(current.getValue())) {
+            return current;
+        }
+
+        // continue simplifying
+        return simplifyToFixedPoint(simplified, simplified.getValue());
     }
 
     /**
      * Recursively simplifies the derivation tree by removing redundant conjuncts
      */
-    private static ValDerivationNode simplifyDerivationTree(ValDerivationNode node) {
+    private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode node) {
         Expression value = node.getValue();
         DerivationNode origin = node.getOrigin();
 
         // binary expression with &&
-        if (value instanceof BinaryExpression binExp) {
-            if ("&&".equals(binExp.getOperator()) && origin instanceof BinaryDerivationNode binOrigin) {
-                // recursively simplify children
-                ValDerivationNode leftSimplified = simplifyDerivationTree(binOrigin.getLeft());
-                ValDerivationNode rightSimplified = simplifyDerivationTree(binOrigin.getRight());
-
-                // check if either side is redundant
-                if (isRedundant(leftSimplified.getValue()))
-                    return rightSimplified;
-                if (isRedundant(rightSimplified.getValue()))
-                    return leftSimplified;
-
-                // return the conjunction with simplified children
-                Expression newValue = new BinaryExpression(leftSimplified.getValue(), "&&", rightSimplified.getValue());
-                DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&");
-                return new ValDerivationNode(newValue, newOrigin);
+        if (value instanceof BinaryExpression binExp && "&&".equals(binExp.getOperator())) {
+            ValDerivationNode leftSimplified;
+            ValDerivationNode rightSimplified;
+
+            if (origin instanceof BinaryDerivationNode binOrigin) {
+                leftSimplified = simplifyValDerivationNode(binOrigin.getLeft());
+                rightSimplified = simplifyValDerivationNode(binOrigin.getRight());
+            } else {
+                leftSimplified = simplifyValDerivationNode(new ValDerivationNode(binExp.getFirstOperand(), null));
+                rightSimplified = simplifyValDerivationNode(new ValDerivationNode(binExp.getSecondOperand(), null));
             }
+
+            // check if either side is redundant
+            if (isRedundant(leftSimplified.getValue()))
+                return rightSimplified;
+            if (isRedundant(rightSimplified.getValue()))
+                return leftSimplified;
+
+            // collapse identical sides (x && x => x)
+            if (leftSimplified.getValue().equals(rightSimplified.getValue())) {
+                return leftSimplified;
+            }
+
+            // collapse symmetric equalities (e.g. x == y && y == x => x == y)
+            if (isSymmetricEquality(leftSimplified.getValue(), rightSimplified.getValue())) {
+                return leftSimplified;
+            }
+
+            // return the conjunction with simplified children
+            Expression newValue = new BinaryExpression(leftSimplified.getValue(), "&&", rightSimplified.getValue());
+            DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&");
+            return new ValDerivationNode(newValue, newOrigin);
         }
         // no simplification
         return node;
     }
 
+    private static boolean isSymmetricEquality(Expression left, Expression right) {
+        if (left instanceof BinaryExpression b1 && "==".equals(b1.getOperator()) && right instanceof BinaryExpression b2
+                && "==".equals(b2.getOperator())) {
+
+            Expression l1 = b1.getFirstOperand();
+            Expression r1 = b1.getSecondOperand();
+            Expression l2 = b2.getFirstOperand();
+            Expression r2 = b2.getSecondOperand();
+            return l1.equals(r2) && r1.equals(l2);
+        }
+        return false;
+    }
+
     /**
      * Checks if an expression is redundant (e.g. true or x == x)
      */