Merge branch 'main' into substitute-internal-vars

Author: rcosta358

liquidjava-example/src/main/java/testSuite/ErrorAssignmentBeforeReturn.java

@@ -0,0 +1,12 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorAssignmentBeforeReturn {
+    @Refinement("_ > 0")
+    static int example(int x) {
+        x = x + 1;
+        return x;
+    }
+}

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

@@ -1,7 +1,9 @@
 package liquidjava.processor.refinement_checker;
 
 import java.util.ArrayList;
+import java.util.HashSet;
 import java.util.List;
+import java.util.Optional;
 import java.util.Set;
 import java.util.Stack;
 import java.util.function.Consumer;
@@ -12,6 +14,9 @@
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.*;
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.Ite;
+import liquidjava.rj_language.ast.Var;
 import liquidjava.smt.Counterexample;
 import liquidjava.smt.SMTEvaluator;
 import liquidjava.smt.SMTResult;
@@ -191,7 +196,18 @@ private VCImplication joinPredicates(Predicate expectedType, List<RefinedVariabl
 
         for (RefinedVariable var : vars) { // join refinements of vars
             addMap(var, map);
-            VCImplication si = new VCImplication(var.getName(), var.getType(), var.getRefinement());
+
+            // if the last instance is already in vars, it is already in the premises
+            // adding "var == lastInstance" would create a contradictory cycle (e.g. x == x + 1 for x = x + 1)
+            // so we need to use main refinement to avoid this
+            Predicate refinement = var.getRefinement();
+            if (var instanceof Variable v) {
+                Optional<VariableInstance> lastInst = v.getLastInstance();
+                if (lastInst.isPresent() && vars.contains(lastInst.get())
+                        && hasDependencyCycle(lastInst.get(), var.getName(), vars, new HashSet<>()))
+                    refinement = v.getMainRefinement();
+            }
+            VCImplication si = new VCImplication(var.getName(), var.getType(), refinement);
             if (lastSi != null) {
                 lastSi.setNext(si);
                 lastSi = si;
@@ -268,6 +284,22 @@ void removePathVariableThatIncludes(String otherVar) {
                 .forEach(pathVariables::remove);
     }
 
+    private boolean hasDependencyCycle(RefinedVariable rv, String var, List<RefinedVariable> vars, Set<String> seen) {
+        if (!seen.add(rv.getName()))
+            return false;
+        Expression e = rv.getRefinement().getExpression();
+        return hasVariable(e, var) || vars.stream().filter(o -> hasVariable(e, o.getName()))
+                .anyMatch(o -> hasDependencyCycle(o, var, vars, seen));
+    }
+
+    private boolean hasVariable(Expression exp, String var) {
+        if (exp instanceof Var v)
+            return v.getName().equals(var);
+        if (exp instanceof Ite ite)
+            return hasVariable(ite.getThen(), var) || hasVariable(ite.getElse(), var);
+        return exp.getChildren().stream().anyMatch(c -> hasVariable(c, var));
+    }
+
     // Errors---------------------------------------------------------------------------------------------------
 
     protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found,

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

@@ -172,18 +172,24 @@ private static ValDerivationNode foldUnary(ValDerivationNode node) {
             // !true => false, !false => true
             boolean value = operand.isBooleanTrue();
             Expression res = new LiteralBoolean(!value);
-            return new ValDerivationNode(res, new UnaryDerivationNode(operandNode, operator));
+            DerivationNode origin = operandNode.getOrigin() != null ? new UnaryDerivationNode(operandNode, operator)
+                    : null;
+            return new ValDerivationNode(res, origin);
         }
         // unary minus
         if ("-".equals(operator)) {
             // -(x) => -x
             if (operand instanceof LiteralInt) {
                 Expression res = new LiteralInt(-((LiteralInt) operand).getValue());
-                return new ValDerivationNode(res, new UnaryDerivationNode(operandNode, operator));
+                DerivationNode origin = operandNode.getOrigin() != null ? new UnaryDerivationNode(operandNode, operator)
+                        : null;
+                return new ValDerivationNode(res, origin);
             }
             if (operand instanceof LiteralReal) {
                 Expression res = new LiteralReal(-((LiteralReal) operand).getValue());
-                return new ValDerivationNode(res, new UnaryDerivationNode(operandNode, operator));
+                DerivationNode origin = operandNode.getOrigin() != null ? new UnaryDerivationNode(operandNode, operator)
+                        : null;
+                return new ValDerivationNode(res, origin);
             }
         }
 

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

@@ -3,8 +3,10 @@
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode;
 import liquidjava.rj_language.opt.derivation_node.DerivationNode;
+import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 
 public class ExpressionSimplifier {
@@ -15,12 +17,13 @@ public class ExpressionSimplifier {
      */
     public static ValDerivationNode simplify(Expression exp) {
         ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp);
-        return simplifyValDerivationNode(fixedPoint);
+        ValDerivationNode simplified = simplifyValDerivationNode(fixedPoint);
+        return unwrapBooleanLiterals(simplified);
     }
 
     /**
      * 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
+     * expression simplifies to a boolean literal, which means we've simplified too much
      */
     private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, Expression prevExp) {
         // apply propagation and folding
@@ -34,6 +37,11 @@ private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current,
             return current;
         }
 
+        // prevent oversimplification
+        if (current != null && currExp instanceof LiteralBoolean && !(current.getValue() instanceof LiteralBoolean)) {
+            return current;
+        }
+
         // continue simplifying
         return simplifyToFixedPoint(simplified, simplified.getValue());
     }
@@ -76,8 +84,12 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod
 
             // 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);
+            // only create origin if at least one child has a meaningful origin
+            if (leftSimplified.getOrigin() != null || rightSimplified.getOrigin() != null) {
+                DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&");
+                return new ValDerivationNode(newValue, newOrigin);
+            }
+            return new ValDerivationNode(newValue, null);
         }
         // no simplification
         return node;
@@ -114,4 +126,61 @@ private static boolean isRedundant(Expression exp) {
         }
         return false;
     }
+
+    /**
+     * Recursively traverses the derivation tree and replaces boolean literals with the expressions that produced them,
+     * but only when at least one operand in the derivation is non-boolean. e.g. "x == true" where true came from "1 >
+     * 0" becomes "x == 1 > 0"
+     */
+    private static ValDerivationNode unwrapBooleanLiterals(ValDerivationNode node) {
+        Expression value = node.getValue();
+        DerivationNode origin = node.getOrigin();
+
+        if (origin == null)
+            return node;
+
+        // unwrap binary expressions
+        if (value instanceof BinaryExpression binExp && origin instanceof BinaryDerivationNode binOrigin) {
+            ValDerivationNode left = unwrapBooleanLiterals(binOrigin.getLeft());
+            ValDerivationNode right = unwrapBooleanLiterals(binOrigin.getRight());
+            if (left != binOrigin.getLeft() || right != binOrigin.getRight()) {
+                Expression newValue = new BinaryExpression(left.getValue(), binExp.getOperator(), right.getValue());
+                return new ValDerivationNode(newValue, new BinaryDerivationNode(left, right, binOrigin.getOp()));
+            }
+            return node;
+        }
+
+        // unwrap unary expressions
+        if (value instanceof UnaryExpression unaryExp && origin instanceof UnaryDerivationNode unaryOrigin) {
+            ValDerivationNode operand = unwrapBooleanLiterals(unaryOrigin.getOperand());
+            if (operand != unaryOrigin.getOperand()) {
+                Expression newValue = new UnaryExpression(unaryExp.getOp(), operand.getValue());
+                return new ValDerivationNode(newValue, new UnaryDerivationNode(operand, unaryOrigin.getOp()));
+            }
+            return node;
+        }
+
+        // boolean literal with binary origin: unwrap if at least one child is non-boolean
+        if (value instanceof LiteralBoolean && origin instanceof BinaryDerivationNode binOrigin) {
+            ValDerivationNode left = unwrapBooleanLiterals(binOrigin.getLeft());
+            ValDerivationNode right = unwrapBooleanLiterals(binOrigin.getRight());
+            if (!(left.getValue() instanceof LiteralBoolean) || !(right.getValue() instanceof LiteralBoolean)) {
+                Expression newValue = new BinaryExpression(left.getValue(), binOrigin.getOp(), right.getValue());
+                return new ValDerivationNode(newValue, new BinaryDerivationNode(left, right, binOrigin.getOp()));
+            }
+            return node;
+        }
+
+        // boolean literal with unary origin: unwrap if operand is non-boolean
+        if (value instanceof LiteralBoolean && origin instanceof UnaryDerivationNode unaryOrigin) {
+            ValDerivationNode operand = unwrapBooleanLiterals(unaryOrigin.getOperand());
+            if (!(operand.getValue() instanceof LiteralBoolean)) {
+                Expression newValue = new UnaryExpression(unaryOrigin.getOp(), operand.getValue());
+                return new ValDerivationNode(newValue, new UnaryDerivationNode(operand, unaryOrigin.getOp()));
+            }
+            return node;
+        }
+
+        return node;
+    }
 }