From 52b922535b1e484fbc79239dff70a0def7fa200a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 2 Oct 2025 09:03:14 +0100 Subject: [PATCH 01/12] Simplify Expressions --- .../java/liquidjava/errors/ErrorHandler.java | 4 +- .../refinement_checker/TypeChecker.java | 3 +- .../liquidjava/rj_language/Predicate.java | 8 + .../rj_language/ast/LiteralInt.java | 4 + .../rj_language/ast/LiteralReal.java | 4 + .../rj_language/opt/AssertionExtractor.java | 76 ++++++ .../rj_language/opt/ConstantFolding.java | 170 +++++++++++++ .../rj_language/opt/ConstantPropagation.java | 35 +++ .../rj_language/opt/ExpressionSimplifier.java | 44 ++++ .../rj_language/opt/LogicSimplifier.java | 230 ++++++++++++++++++ .../derivation_node/BinaryDerivationNode.java | 43 ++++ .../opt/derivation_node/DerivationNode.java | 49 ++++ .../derivation_node/UnaryDerivationNode.java | 33 +++ .../derivation_node/ValDerivationNode.java | 17 ++ .../derivation_node/VarDerivationNode.java | 26 ++ 15 files changed, 743 insertions(+), 3 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AssertionExtractor.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/LogicSimplifier.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java index f7a242d0..557f2ada 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java @@ -41,7 +41,7 @@ public static void printError(CtElement var, String moreInfo, Predicate expe // all message sb.append(sbtitle.toString() + "\n\n"); sb.append("Type expected:" + expectedType.toString() + "\n"); - sb.append("Refinement found:" + cSMT.toString() + "\n"); + sb.append("Refinement found:\n" + cSMT.simplify() + "\n"); sb.append(printMap(map)); sb.append("Location: " + var.getPosition() + "\n"); sb.append("______________________________________________________\n"); @@ -181,7 +181,7 @@ public static void printCostumeError(CtElement element, String msg, ErrorEmitter sb.append(element + "\n\n"); sb.append("Location: " + element.getPosition() + "\n"); sb.append("______________________________________________________\n"); - + errorl.addError(s, sb.toString(), element.getPosition(), 1); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index a535137d..56cf6248 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -119,7 +119,8 @@ private void createStateSet(CtNewArray e, int set, CtElement element) { CtLiteral s = (CtLiteral) ce; String f = s.getValue(); if (Character.isUpperCase(f.charAt(0))) { - ErrorHandler.printCostumeError(s, "State name must start with lowercase in '" + f + "'", errorEmitter); + ErrorHandler.printCostumeError(s, "State name must start with lowercase in '" + f + "'", + errorEmitter); } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index eca80729..a3b5c38e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -21,6 +21,8 @@ import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; +import liquidjava.rj_language.opt.ExpressionSimplifier; +import liquidjava.rj_language.opt.derivation_node.DerivationNode; import liquidjava.rj_language.parsing.ParsingException; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.utils.Utils; @@ -212,6 +214,12 @@ public Expression getExpression() { return exp; } + public Expression simplify() { + List steps = ExpressionSimplifier.simplify(exp.clone()); + steps.forEach(System.out::println); + return steps.isEmpty() ? exp : steps.get(steps.size() - 1); + } + public static Predicate createConjunction(Predicate c1, Predicate c2) { return new Predicate(new BinaryExpression(c1.getExpression(), Utils.AND, c2.getExpression())); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java index 6a4e97f1..4e98fa57 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java @@ -25,6 +25,10 @@ public String toString() { return Integer.toString(value); } + public int getValue() { + return value; + } + @Override public void getVariableNames(List toAdd) { // end leaf diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java index 2ddc8430..e6c4a810 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java @@ -25,6 +25,10 @@ public String toString() { return Double.toString(value); } + public double getValue() { + return value; + } + @Override public void getVariableNames(List toAdd) { // end leaf diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AssertionExtractor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AssertionExtractor.java new file mode 100644 index 00000000..ec84c58b --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AssertionExtractor.java @@ -0,0 +1,76 @@ +package liquidjava.rj_language.opt; + +import java.util.HashMap; +import java.util.Map; + +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralReal; +import liquidjava.rj_language.ast.Var; + +public class AssertionExtractor { + + public static Map extract(Expression exp) { + Map assertions = new HashMap<>(); + + // only extract assertions if the expression contains conjunctions (&&) + if (containsConjunction(exp)) { + extractRecursive(exp, assertions); + } + return assertions; + } + + private static boolean containsConjunction(Expression exp) { + if (exp instanceof BinaryExpression) { + BinaryExpression binExp = (BinaryExpression) exp; + if (binExp.getOperator().equals("&&")) { + return true; + } + // recursively check children + return containsConjunction(binExp.getFirstOperand()) || containsConjunction(binExp.getSecondOperand()); + } + if (exp.hasChildren()) { + for (Expression child : exp.getChildren()) { + if (containsConjunction(child)) { + return true; + } + } + } + return false; + } + + private static void extractRecursive(Expression exp, Map assertions) { + if (exp instanceof BinaryExpression) { + BinaryExpression binExp = (BinaryExpression) exp; + String operator = binExp.getOperator(); + + if (operator.equals("&&")) { + // for conjunctions recursively extract from both sides + extractRecursive(binExp.getFirstOperand(), assertions); + extractRecursive(binExp.getSecondOperand(), assertions); + } else if (operator.equals("==")) { + // for assertions check if one side is a variable and the other is a literal + Expression left = binExp.getFirstOperand(); + Expression right = binExp.getSecondOperand(); + + if (left instanceof Var && isLiteral(right)) { + assertions.put(((Var) left).getName(), right); + } else if (right instanceof Var && isLiteral(left)) { + assertions.put(((Var) right).getName(), left); + } + } + } + // for other expressions, recurse into children + else if (exp.hasChildren()) { + for (Expression child : exp.getChildren()) { + extractRecursive(child, assertions); + } + } + } + + private static boolean isLiteral(Expression exp) { + return exp instanceof LiteralInt || exp instanceof LiteralReal || exp instanceof LiteralBoolean; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java new file mode 100644 index 00000000..69f88e86 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java @@ -0,0 +1,170 @@ +package liquidjava.rj_language.opt; + +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralReal; +import liquidjava.rj_language.ast.UnaryExpression; + +public class ConstantFolding { + + public static Expression fold(Expression exp) { + // recursively simplify in all children + if (exp.hasChildren()) { + for (int i = 0; i < exp.getChildren().size(); i++) { + Expression child = exp.getChildren().get(i); + Expression propagatedChild = fold(child); + exp.setChild(i, propagatedChild); + } + } + + // try to fold the current expression + if (exp instanceof BinaryExpression) { + return foldBinaryExpression((BinaryExpression) exp); + } else if (exp instanceof UnaryExpression) { + return foldUnaryExpression((UnaryExpression) exp); + } + return exp; + } + + private static Expression foldBinaryExpression(BinaryExpression binExp) { + Expression left = binExp.getFirstOperand(); + Expression right = binExp.getSecondOperand(); + String op = binExp.getOperator(); + + // arithmetic operations with integer literals + if (left instanceof LiteralInt && right instanceof LiteralInt) { + int l = ((LiteralInt) left).getValue(); + int r = ((LiteralInt) right).getValue(); + + switch (op) { + case "+": + return new LiteralInt(l + r); + case "-": + return new LiteralInt(l - r); + case "*": + return new LiteralInt(l * r); + case "/": + if (r != 0) + return new LiteralInt(l / r); + break; + case "%": + if (r != 0) + return new LiteralInt(l % r); + break; + case "<": + return new LiteralBoolean(l < r); + case "<=": + return new LiteralBoolean(l <= r); + case ">": + return new LiteralBoolean(l > r); + case ">=": + return new LiteralBoolean(l >= r); + case "==": + return new LiteralBoolean(l == r); + case "!=": + return new LiteralBoolean(l != r); + } + } + + // arithmetic operations with real literals + else if (left instanceof LiteralReal && right instanceof LiteralReal) { + double l = ((LiteralReal) left).getValue(); + double r = ((LiteralReal) right).getValue(); + switch (op) { + case "+": + return new LiteralReal(l + r); + case "-": + return new LiteralReal(l - r); + case "*": + return new LiteralReal(l * r); + case "/": + if (r != 0.0) + return new LiteralReal(l / r); + break; + case "%": + if (r != 0.0) + return new LiteralReal(l % r); + break; + case "<": + return new LiteralBoolean(l < r); + case "<=": + return new LiteralBoolean(l <= r); + case ">": + return new LiteralBoolean(l > r); + case ">=": + return new LiteralBoolean(l >= r); + case "==": + return new LiteralBoolean(l == r); + case "!=": + return new LiteralBoolean(l != r); + } + } + + // mixed integer and real operations + else if ((left instanceof LiteralInt && right instanceof LiteralReal) || (left instanceof LiteralReal && right instanceof LiteralInt)) { + double l = left instanceof LiteralInt ? ((LiteralInt) left).getValue() : ((LiteralReal) left).getValue(); + double r = right instanceof LiteralInt ? ((LiteralInt) right).getValue() : ((LiteralReal) right).getValue(); + switch (op) { + case "+": + return new LiteralReal(l + r); + case "-": + return new LiteralReal(l - r); + case "*": + return new LiteralReal(l * r); + case "/": + if (r != 0.0) + return new LiteralReal(l / r); + break; + case "%": + if (r != 0.0) + return new LiteralReal(l % r); + break; + case "<": + return new LiteralBoolean(l < r); + case "<=": + return new LiteralBoolean(l <= r); + case ">": + return new LiteralBoolean(l > r); + case ">=": + return new LiteralBoolean(l >= r); + case "==": + return new LiteralBoolean(l == r); + case "!=": + return new LiteralBoolean(l != r); + } + } + + // boolean operations with boolean literals + else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) { + boolean l = ((LiteralBoolean) left).isBooleanTrue(); + boolean r = ((LiteralBoolean) right).isBooleanTrue(); + switch (op) { + case "&&": + return new LiteralBoolean(l && r); + case "||": + return new LiteralBoolean(l || r); + case "-->": // implication: !a || b + return new LiteralBoolean(!l || r); + case "==": + return new LiteralBoolean(l == r); + case "!=": + return new LiteralBoolean(l != r); + } + } + // no folding, return original + return binExp; + } + + private static Expression foldUnaryExpression(UnaryExpression unaryExp) { + Expression operand = unaryExp.getChildren().get(0); + String operator = unaryExp.getOp(); + if (operator.equals("!") && operand instanceof LiteralBoolean) { + // !true -> false, !false -> true + boolean value = ((LiteralBoolean) operand).isBooleanTrue(); + return new LiteralBoolean(!value); + } + return unaryExp; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java new file mode 100644 index 00000000..dbeebcfd --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java @@ -0,0 +1,35 @@ +package liquidjava.rj_language.opt; + +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.Var; +import java.util.Map; + +public class ConstantPropagation { + + public static Expression propagate(Expression exp) { + Map substitutions = AssertionExtractor.extract(exp); + return propagateRecursive(exp, substitutions); + } + + private static Expression propagateRecursive(Expression exp, Map substitutions) { + // apply substitutions to children for other expression types + if (exp.hasChildren()) { + Expression result = exp.clone(); + for (int i = 0; i < result.getChildren().size(); i++) { + Expression child = result.getChildren().get(i); + Expression substitutedChild = propagateRecursive(child, substitutions); + result.setChild(i, substitutedChild); + } + return result; + } + // if the expression is a variable, substitute if in map + if (exp instanceof Var) { + Var var = (Var) exp; + String varName = var.getName(); + if (substitutions.containsKey(varName)) { + return substitutions.get(varName).clone(); + } + } + return exp; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java new file mode 100644 index 00000000..4d275e77 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java @@ -0,0 +1,44 @@ +package liquidjava.rj_language.opt; + +import java.util.ArrayList; +import java.util.List; +import liquidjava.rj_language.ast.Expression; + +public class ExpressionSimplifier { + + public static List simplify(Expression exp) { + ArrayList derivationSteps = new ArrayList<>(); + Expression current = exp.clone(); + boolean changed = true; + + derivationSteps.add(current); + while (changed) { + changed = false; + + Expression simplified = LogicSimplifier.simplify(current.clone()); + if (!simplified.equals(current)) { + // derivationSteps.add(simplified); + current = simplified; + changed = true; + continue; + } + + Expression propagated = ConstantPropagation.propagate(current.clone()); + if (!propagated.equals(current)) { + // derivationSteps.add(propagated); + current = propagated; + changed = true; + continue; + } + + Expression folded = ConstantFolding.fold(current.clone()); + if (!folded.equals(current)) { + derivationSteps.add(folded); + current = folded; + changed = true; + continue; + } + } + return derivationSteps; + } +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/LogicSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/LogicSimplifier.java new file mode 100644 index 00000000..11f0f310 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/LogicSimplifier.java @@ -0,0 +1,230 @@ +package liquidjava.rj_language.opt; + +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.GroupExpression; +import liquidjava.rj_language.ast.Ite; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralReal; +import liquidjava.rj_language.ast.UnaryExpression; + +public class LogicSimplifier { + + public static Expression simplify(Expression exp) { + // recursively simplify in all children + if (exp.hasChildren()) { + for (int i = 0; i < exp.getChildren().size(); i++) { + Expression child = exp.getChildren().get(i); + Expression propagatedChild = simplify(child); + exp.setChild(i, propagatedChild); + } + } + + // apply simplification rules to the current expression + if (exp instanceof BinaryExpression) { + return simplifyBinaryExpression((BinaryExpression) exp); + } else if (exp instanceof UnaryExpression) { + return simplifyUnaryExpression((UnaryExpression) exp); + } else if (exp instanceof Ite) { + return simplifyIte((Ite) exp); + } else if (exp instanceof GroupExpression) { + return simplifyGroupExpression((GroupExpression) exp); + } + + // literals, variables and function invocations cant be simplified + return exp; + } + + private static Expression simplifyBinaryExpression(BinaryExpression binExp) { + Expression left = binExp.getFirstOperand(); + Expression right = binExp.getSecondOperand(); + String operator = binExp.getOperator(); + + // boolean logic simplifications + if (operator.equals("&&")) { + // true && x => x + if (left instanceof LiteralBoolean && ((LiteralBoolean) left).isBooleanTrue()) { + return right; + } + // x && true => x + if (right instanceof LiteralBoolean && ((LiteralBoolean) right).isBooleanTrue()) { + return left; + } + // false && x => false + if (left instanceof LiteralBoolean && !((LiteralBoolean) left).isBooleanTrue()) { + return new LiteralBoolean(false); + } + // x && false => false + if (right instanceof LiteralBoolean && !((LiteralBoolean) right).isBooleanTrue()) { + return new LiteralBoolean(false); + } + } else if (operator.equals("||")) { + // true || x => true + if (left instanceof LiteralBoolean && ((LiteralBoolean) left).isBooleanTrue()) { + return new LiteralBoolean(true); + } + // x || true => true + if (right instanceof LiteralBoolean && ((LiteralBoolean) right).isBooleanTrue()) { + return new LiteralBoolean(true); + } + // false || x => x + if (left instanceof LiteralBoolean && !((LiteralBoolean) left).isBooleanTrue()) { + return right; + } + // x || false => x + if (right instanceof LiteralBoolean && !((LiteralBoolean) right).isBooleanTrue()) { + return left; + } + } else if (operator.equals("-->")) { + // false --> x => true + if (left instanceof LiteralBoolean && !((LiteralBoolean) left).isBooleanTrue()) { + return new LiteralBoolean(true); + } + // x --> true => true + if (right instanceof LiteralBoolean && ((LiteralBoolean) right).isBooleanTrue()) { + return new LiteralBoolean(true); + } + // true --> x => x + if (left instanceof LiteralBoolean && ((LiteralBoolean) left).isBooleanTrue()) { + return right; + } + } + + // arithmetic identity simplifications + else if (operator.equals("+")) { + // 0 + x => x + if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 0) { + return right; + } + // x + 0 => x + if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 0) { + return left; + } + // 0.0 + x => x + if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 0.0) { + return right; + } + // x + 0.0 => x + if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 0.0) { + return left; + } + } else if (operator.equals("-")) { + // x - 0 => x + if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 0) { + return left; + } + // x - 0.0 => x + if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 0.0) { + return left; + } + } else if (operator.equals("*")) { + // 1 * x => x + if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 1) { + return right; + } + // x * 1 => x + if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 1) { + return left; + } + // 0 * x => 0 + if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 0) { + return new LiteralInt(0); + } + // x * 0 => 0 + if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 0) { + return new LiteralInt(0); + } + // 1.0 * x => x + if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 1.0) { + return right; + } + // x * 1.0 => x + if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 1.0) { + return left; + } + // 0.0 * x => 0.0 + if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 0.0) { + return new LiteralReal(0.0); + } + // x * 0.0 => 0.0 + if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 0.0) { + return new LiteralReal(0.0); + } + } else if (operator.equals("/")) { + // x / 1 => x + if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 1) { + return left; + } + // x / 1.0 => x + if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 1.0) { + return left; + } + // 0 / x => 0 (assuming x != 0) + if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 0) { + return new LiteralInt(0); + } + // 0.0 / x => 0.0 (assuming x != 0) + if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 0.0) { + return new LiteralReal(0.0); + } + } + + // comparison simplifications + else if (operator.equals("==")) { + // x == x => true + if (left.equals(right)) { + return new LiteralBoolean(true); + } + } else if (operator.equals("!=")) { + // x != x => false + if (left.equals(right)) { + return new LiteralBoolean(false); + } + } + // no simplification applied + return binExp; + } + + private static Expression simplifyUnaryExpression(UnaryExpression unaryExpr) { + Expression operand = unaryExpr.getChildren().get(0); + String operator = unaryExpr.getOp(); + if (operator.equals("!")) { + // !!x => x (double negation) + if (operand instanceof UnaryExpression) { + UnaryExpression innerUnary = (UnaryExpression) operand; + if (innerUnary.getOp().equals("!")) { + return innerUnary.getChildren().get(0); + } + } + } else if (operator.equals("-")) { + // -(-x) => x (double negation) + if (operand instanceof UnaryExpression) { + UnaryExpression innerUnary = (UnaryExpression) operand; + if (innerUnary.getOp().equals("-")) { + return innerUnary.getChildren().get(0); + } + } + } + return unaryExpr; + } + + private static Expression simplifyIte(Ite iteExp) { + Expression condExp = iteExp.getChildren().get(0); + Expression thenExp = iteExp.getChildren().get(1); + Expression elseExp = iteExp.getChildren().get(2); + if (condExp instanceof LiteralBoolean) { + boolean cond = ((LiteralBoolean) condExp).isBooleanTrue(); + return cond ? thenExp : elseExp; + } + return iteExp; + } + + private static Expression simplifyGroupExpression(GroupExpression groupExp) { + // (expression) => expression + if (groupExp.getChildren().size() == 1) { + return groupExp.getChildren().get(0); + } + return groupExp; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java new file mode 100644 index 00000000..174e5043 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java @@ -0,0 +1,43 @@ +package liquidjava.rj_language.opt.derivation_node; + +import java.util.Map; + +import liquidjava.rj_language.ast.Expression; + +public class BinaryDerivationNode extends DerivationNode { + private DerivationNode left; + private DerivationNode right; + private String op; + + public BinaryDerivationNode(Expression exp, DerivationNode left, DerivationNode right, String operator) { + super(exp); + this.left = left; + this.right = right; + this.op = operator; + } + + public DerivationNode getLeft() { + return left; + } + + public DerivationNode getRight() { + return right; + } + + public String getOp() { + return op; + } + + @Override + public Map toJson() { + Map json = baseJson(); + json.put("op", op); + if (left != null) { + json.put("left", left.toJson()); + } + if (right != null) { + json.put("right", right.toJson()); + } + return json; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java new file mode 100644 index 00000000..f2b479e1 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java @@ -0,0 +1,49 @@ +package liquidjava.rj_language.opt.derivation_node; + +import java.util.LinkedHashMap; +import java.util.Map; + +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralReal; +import liquidjava.rj_language.ast.Var; + +public abstract class DerivationNode { + private Expression exp; + + public DerivationNode(Expression exp) { + this.exp = exp; + } + + public Expression getExp() { + return exp; + } + + @Override + public String toString() { + return toJson().toString(); + } + + public abstract Map toJson(); + + protected Map baseJson() { + Map json = new LinkedHashMap<>(); + json.put("exp", expressionToValue(exp)); + return json; + } + + protected Object expressionToValue(Expression expression) { + if (expression == null) + return null; + if (expression instanceof LiteralInt) + return ((LiteralInt) expression).getValue(); + if (expression instanceof LiteralReal) + return ((LiteralReal) expression).getValue(); + if (expression instanceof LiteralBoolean) + return ((LiteralBoolean) expression).isBooleanTrue(); + if (expression instanceof Var) + return ((Var) expression).getName(); + return expression.toString(); + } +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java new file mode 100644 index 00000000..b95a22c5 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java @@ -0,0 +1,33 @@ +package liquidjava.rj_language.opt.derivation_node; + +import java.util.Map; + +import liquidjava.rj_language.ast.Expression; + +public class UnaryDerivationNode extends DerivationNode { + private DerivationNode operand; + private String operator; + + public UnaryDerivationNode(Expression exp, DerivationNode operand, String operator) { + super(exp); + this.operator = operator; + } + + public DerivationNode getOperand() { + return operand; + } + + public String getOperator() { + return operator; + } + + @Override + public Map toJson() { + Map json = baseJson(); + json.put("op", operator); + if (operand != null) { + json.put("operand", operand.toJson()); + } + return json; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java new file mode 100644 index 00000000..b736fde8 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java @@ -0,0 +1,17 @@ +package liquidjava.rj_language.opt.derivation_node; + +import java.util.Map; + +import liquidjava.rj_language.ast.Expression; + +public class ValDerivationNode extends DerivationNode { + + public ValDerivationNode(Expression exp) { + super(exp); + } + + @Override + public Map toJson() { + return baseJson(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java new file mode 100644 index 00000000..c717fd6f --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java @@ -0,0 +1,26 @@ +package liquidjava.rj_language.opt.derivation_node; + +import java.util.Map; + +import liquidjava.rj_language.ast.Expression; + +public class VarDerivationNode extends DerivationNode { + + private String var; + + public VarDerivationNode(Expression exp, String var) { + super(exp); + this.var = var; + } + + public String getVar() { + return var; + } + + @Override + public Map toJson() { + Map json = baseJson(); + json.put("var", var); + return json; + } +} From cd52d4142c2aecd637090f50b2b7a3060e9ccb8a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 2 Oct 2025 12:05:43 +0100 Subject: [PATCH 02/12] Simple Approach --- .../liquidjava/rj_language/Predicate.java | 5 +- .../rj_language/opt/ConstantPropagation.java | 2 +- .../rj_language/opt/ExpressionSimplifier.java | 40 ++++++++------- ...nExtractor.java => VariableExtractor.java} | 2 +- .../derivation_node/BinaryDerivationNode.java | 43 ---------------- .../opt/derivation_node/DerivationNode.java | 49 ------------------- .../derivation_node/UnaryDerivationNode.java | 33 ------------- .../derivation_node/ValDerivationNode.java | 17 ------- .../derivation_node/VarDerivationNode.java | 26 ---------- 9 files changed, 24 insertions(+), 193 deletions(-) rename liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/{AssertionExtractor.java => VariableExtractor.java} (98%) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index a3b5c38e..a4d3263c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -22,7 +22,6 @@ import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.opt.ExpressionSimplifier; -import liquidjava.rj_language.opt.derivation_node.DerivationNode; import liquidjava.rj_language.parsing.ParsingException; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.utils.Utils; @@ -215,9 +214,7 @@ public Expression getExpression() { } public Expression simplify() { - List steps = ExpressionSimplifier.simplify(exp.clone()); - steps.forEach(System.out::println); - return steps.isEmpty() ? exp : steps.get(steps.size() - 1); + return ExpressionSimplifier.simplify(exp.clone()); } public static Predicate createConjunction(Predicate c1, Predicate c2) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java index dbeebcfd..e4390d26 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java @@ -7,7 +7,7 @@ public class ConstantPropagation { public static Expression propagate(Expression exp) { - Map substitutions = AssertionExtractor.extract(exp); + Map substitutions = VariableExtractor.extract(exp); return propagateRecursive(exp, substitutions); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java index 4d275e77..dcf2e32d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java @@ -1,44 +1,46 @@ package liquidjava.rj_language.opt; -import java.util.ArrayList; -import java.util.List; import liquidjava.rj_language.ast.Expression; public class ExpressionSimplifier { - public static List simplify(Expression exp) { - ArrayList derivationSteps = new ArrayList<>(); - Expression current = exp.clone(); + public static Expression simplify(Expression exp) { + System.out.println(exp); + Expression current = simplifyExp(exp.clone()); + System.out.println(current); boolean changed = true; - derivationSteps.add(current); while (changed) { changed = false; - Expression simplified = LogicSimplifier.simplify(current.clone()); - if (!simplified.equals(current)) { - // derivationSteps.add(simplified); - current = simplified; - changed = true; - continue; - } - Expression propagated = ConstantPropagation.propagate(current.clone()); if (!propagated.equals(current)) { - // derivationSteps.add(propagated); - current = propagated; + current = simplifyExp(propagated); + System.out.println(current); changed = true; continue; } Expression folded = ConstantFolding.fold(current.clone()); if (!folded.equals(current)) { - derivationSteps.add(folded); - current = folded; + current = simplifyExp(folded); + System.out.println(current); changed = true; continue; } } - return derivationSteps; + return current; + } + + private static Expression simplifyExp(Expression exp) { + Expression current = exp.clone(); + while (true) { + Expression simplified = LogicSimplifier.simplify(current.clone()); + if (simplified.equals(current)) { + break; + } + current = simplified; + } + return current; } } \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AssertionExtractor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableExtractor.java similarity index 98% rename from liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AssertionExtractor.java rename to liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableExtractor.java index ec84c58b..a02a3724 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AssertionExtractor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableExtractor.java @@ -10,7 +10,7 @@ import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.Var; -public class AssertionExtractor { +public class VariableExtractor { public static Map extract(Expression exp) { Map assertions = new HashMap<>(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java deleted file mode 100644 index 174e5043..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java +++ /dev/null @@ -1,43 +0,0 @@ -package liquidjava.rj_language.opt.derivation_node; - -import java.util.Map; - -import liquidjava.rj_language.ast.Expression; - -public class BinaryDerivationNode extends DerivationNode { - private DerivationNode left; - private DerivationNode right; - private String op; - - public BinaryDerivationNode(Expression exp, DerivationNode left, DerivationNode right, String operator) { - super(exp); - this.left = left; - this.right = right; - this.op = operator; - } - - public DerivationNode getLeft() { - return left; - } - - public DerivationNode getRight() { - return right; - } - - public String getOp() { - return op; - } - - @Override - public Map toJson() { - Map json = baseJson(); - json.put("op", op); - if (left != null) { - json.put("left", left.toJson()); - } - if (right != null) { - json.put("right", right.toJson()); - } - return json; - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java deleted file mode 100644 index f2b479e1..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java +++ /dev/null @@ -1,49 +0,0 @@ -package liquidjava.rj_language.opt.derivation_node; - -import java.util.LinkedHashMap; -import java.util.Map; - -import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.LiteralBoolean; -import liquidjava.rj_language.ast.LiteralInt; -import liquidjava.rj_language.ast.LiteralReal; -import liquidjava.rj_language.ast.Var; - -public abstract class DerivationNode { - private Expression exp; - - public DerivationNode(Expression exp) { - this.exp = exp; - } - - public Expression getExp() { - return exp; - } - - @Override - public String toString() { - return toJson().toString(); - } - - public abstract Map toJson(); - - protected Map baseJson() { - Map json = new LinkedHashMap<>(); - json.put("exp", expressionToValue(exp)); - return json; - } - - protected Object expressionToValue(Expression expression) { - if (expression == null) - return null; - if (expression instanceof LiteralInt) - return ((LiteralInt) expression).getValue(); - if (expression instanceof LiteralReal) - return ((LiteralReal) expression).getValue(); - if (expression instanceof LiteralBoolean) - return ((LiteralBoolean) expression).isBooleanTrue(); - if (expression instanceof Var) - return ((Var) expression).getName(); - return expression.toString(); - } -} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java deleted file mode 100644 index b95a22c5..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java +++ /dev/null @@ -1,33 +0,0 @@ -package liquidjava.rj_language.opt.derivation_node; - -import java.util.Map; - -import liquidjava.rj_language.ast.Expression; - -public class UnaryDerivationNode extends DerivationNode { - private DerivationNode operand; - private String operator; - - public UnaryDerivationNode(Expression exp, DerivationNode operand, String operator) { - super(exp); - this.operator = operator; - } - - public DerivationNode getOperand() { - return operand; - } - - public String getOperator() { - return operator; - } - - @Override - public Map toJson() { - Map json = baseJson(); - json.put("op", operator); - if (operand != null) { - json.put("operand", operand.toJson()); - } - return json; - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java deleted file mode 100644 index b736fde8..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java +++ /dev/null @@ -1,17 +0,0 @@ -package liquidjava.rj_language.opt.derivation_node; - -import java.util.Map; - -import liquidjava.rj_language.ast.Expression; - -public class ValDerivationNode extends DerivationNode { - - public ValDerivationNode(Expression exp) { - super(exp); - } - - @Override - public Map toJson() { - return baseJson(); - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java deleted file mode 100644 index c717fd6f..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java +++ /dev/null @@ -1,26 +0,0 @@ -package liquidjava.rj_language.opt.derivation_node; - -import java.util.Map; - -import liquidjava.rj_language.ast.Expression; - -public class VarDerivationNode extends DerivationNode { - - private String var; - - public VarDerivationNode(Expression exp, String var) { - super(exp); - this.var = var; - } - - public String getVar() { - return var; - } - - @Override - public Map toJson() { - Map json = baseJson(); - json.put("var", var); - return json; - } -} From c3d05d143d5166a0876e1c617c9fedcc881da009 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 2 Oct 2025 14:53:47 +0100 Subject: [PATCH 03/12] Build Derivation with Linked List --- .../liquidjava/rj_language/Predicate.java | 3 +- .../rj_language/opt/DerivationNode.java | 32 +++++++++++++++++++ .../rj_language/opt/ExpressionSimplifier.java | 27 ++++++++-------- 3 files changed, 48 insertions(+), 14 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/DerivationNode.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index a4d3263c..bf24eec5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -21,6 +21,7 @@ import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; +import liquidjava.rj_language.opt.DerivationNode; import liquidjava.rj_language.opt.ExpressionSimplifier; import liquidjava.rj_language.parsing.ParsingException; import liquidjava.rj_language.parsing.RefinementsParser; @@ -213,7 +214,7 @@ public Expression getExpression() { return exp; } - public Expression simplify() { + public DerivationNode simplify() { return ExpressionSimplifier.simplify(exp.clone()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/DerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/DerivationNode.java new file mode 100644 index 00000000..d6a31ab4 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/DerivationNode.java @@ -0,0 +1,32 @@ +package liquidjava.rj_language.opt; + +import liquidjava.rj_language.ast.Expression; + +public class DerivationNode { + + private DerivationNode from; + private Expression exp; + + public DerivationNode(Expression exp) { + this.exp = exp; + } + + public DerivationNode getFrom() { + return from; + } + + public void setFrom(DerivationNode from) { + this.from = from; + } + + public DerivationNode addNode(Expression exp) { + DerivationNode newNode = new DerivationNode(exp); + newNode.setFrom(this); + return newNode; + } + + @Override + public String toString() { + return String.format("%s <=\n%s", exp, from); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java index dcf2e32d..20e9c65c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java @@ -4,32 +4,33 @@ public class ExpressionSimplifier { - public static Expression simplify(Expression exp) { - System.out.println(exp); - Expression current = simplifyExp(exp.clone()); - System.out.println(current); + public static DerivationNode simplify(Expression exp) { + DerivationNode currentNode = new DerivationNode(exp); + Expression currentExp = simplifyExp(exp.clone()); + currentNode = currentNode.addNode(currentExp); boolean changed = true; while (changed) { changed = false; - Expression propagated = ConstantPropagation.propagate(current.clone()); - if (!propagated.equals(current)) { - current = simplifyExp(propagated); - System.out.println(current); + Expression propagated = ConstantPropagation.propagate(currentExp.clone()); + if (!propagated.equals(currentExp)) { + currentExp = simplifyExp(propagated); + currentNode = currentNode.addNode(currentExp); changed = true; continue; } - Expression folded = ConstantFolding.fold(current.clone()); - if (!folded.equals(current)) { - current = simplifyExp(folded); - System.out.println(current); + Expression folded = ConstantFolding.fold(currentExp.clone()); + if (!folded.equals(currentExp)) { + currentExp = simplifyExp(folded); + currentNode = currentNode.addNode(currentExp); + System.out.println(currentExp); changed = true; continue; } } - return current; + return currentNode; } private static Expression simplifyExp(Expression exp) { From 9ef9595b6e72442673ecab4a4464c501425e6099 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 2 Oct 2025 20:33:18 +0100 Subject: [PATCH 04/12] Improve Switch Cases --- .../rj_language/opt/ConstantFolding.java | 146 +++------ .../rj_language/opt/LogicSimplifier.java | 297 +++++++++--------- 2 files changed, 203 insertions(+), 240 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java index 69f88e86..03535970 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java @@ -38,120 +38,74 @@ private static Expression foldBinaryExpression(BinaryExpression binExp) { int l = ((LiteralInt) left).getValue(); int r = ((LiteralInt) right).getValue(); - switch (op) { - case "+": - return new LiteralInt(l + r); - case "-": - return new LiteralInt(l - r); - case "*": - return new LiteralInt(l * r); - case "/": - if (r != 0) - return new LiteralInt(l / r); - break; - case "%": - if (r != 0) - return new LiteralInt(l % r); - break; - case "<": - return new LiteralBoolean(l < r); - case "<=": - return new LiteralBoolean(l <= r); - case ">": - return new LiteralBoolean(l > r); - case ">=": - return new LiteralBoolean(l >= r); - case "==": - return new LiteralBoolean(l == r); - case "!=": - return new LiteralBoolean(l != r); - } + return switch (op) { + case "+" -> new LiteralInt(l + r); + case "-" -> new LiteralInt(l - r); + case "*" -> new LiteralInt(l * r); + case "/" -> r != 0 ? new LiteralInt(l / r) : binExp; + case "%" -> r != 0 ? new LiteralInt(l % r) : binExp; + case "<" -> new LiteralBoolean(l < r); + case "<=" -> new LiteralBoolean(l <= r); + case ">" -> new LiteralBoolean(l > r); + case ">=" -> new LiteralBoolean(l >= r); + case "==" -> new LiteralBoolean(l == r); + case "!=" -> new LiteralBoolean(l != r); + default -> binExp; + }; } // arithmetic operations with real literals else if (left instanceof LiteralReal && right instanceof LiteralReal) { double l = ((LiteralReal) left).getValue(); double r = ((LiteralReal) right).getValue(); - switch (op) { - case "+": - return new LiteralReal(l + r); - case "-": - return new LiteralReal(l - r); - case "*": - return new LiteralReal(l * r); - case "/": - if (r != 0.0) - return new LiteralReal(l / r); - break; - case "%": - if (r != 0.0) - return new LiteralReal(l % r); - break; - case "<": - return new LiteralBoolean(l < r); - case "<=": - return new LiteralBoolean(l <= r); - case ">": - return new LiteralBoolean(l > r); - case ">=": - return new LiteralBoolean(l >= r); - case "==": - return new LiteralBoolean(l == r); - case "!=": - return new LiteralBoolean(l != r); - } + return switch (op) { + case "+" -> new LiteralReal(l + r); + case "-" -> new LiteralReal(l - r); + case "*" -> new LiteralReal(l * r); + case "/" -> r != 0.0 ? new LiteralReal(l / r) : binExp; + case "%" -> r != 0.0 ? new LiteralReal(l % r) : binExp; + case "<" -> new LiteralBoolean(l < r); + case "<=" -> new LiteralBoolean(l <= r); + case ">" -> new LiteralBoolean(l > r); + case ">=" -> new LiteralBoolean(l >= r); + case "==" -> new LiteralBoolean(l == r); + case "!=" -> new LiteralBoolean(l != r); + default -> binExp; + }; } // mixed integer and real operations else if ((left instanceof LiteralInt && right instanceof LiteralReal) || (left instanceof LiteralReal && right instanceof LiteralInt)) { double l = left instanceof LiteralInt ? ((LiteralInt) left).getValue() : ((LiteralReal) left).getValue(); double r = right instanceof LiteralInt ? ((LiteralInt) right).getValue() : ((LiteralReal) right).getValue(); - switch (op) { - case "+": - return new LiteralReal(l + r); - case "-": - return new LiteralReal(l - r); - case "*": - return new LiteralReal(l * r); - case "/": - if (r != 0.0) - return new LiteralReal(l / r); - break; - case "%": - if (r != 0.0) - return new LiteralReal(l % r); - break; - case "<": - return new LiteralBoolean(l < r); - case "<=": - return new LiteralBoolean(l <= r); - case ">": - return new LiteralBoolean(l > r); - case ">=": - return new LiteralBoolean(l >= r); - case "==": - return new LiteralBoolean(l == r); - case "!=": - return new LiteralBoolean(l != r); - } + return switch (op) { + case "+" -> new LiteralReal(l + r); + case "-" -> new LiteralReal(l - r); + case "*" -> new LiteralReal(l * r); + case "/" -> r != 0.0 ? new LiteralReal(l / r) : binExp; + case "%" -> r != 0.0 ? new LiteralReal(l % r) : binExp; + case "<" -> new LiteralBoolean(l < r); + case "<=" -> new LiteralBoolean(l <= r); + case ">" -> new LiteralBoolean(l > r); + case ">=" -> new LiteralBoolean(l >= r); + case "==" -> new LiteralBoolean(l == r); + case "!=" -> new LiteralBoolean(l != r); + default -> binExp; + }; } // boolean operations with boolean literals else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) { boolean l = ((LiteralBoolean) left).isBooleanTrue(); boolean r = ((LiteralBoolean) right).isBooleanTrue(); - switch (op) { - case "&&": - return new LiteralBoolean(l && r); - case "||": - return new LiteralBoolean(l || r); - case "-->": // implication: !a || b - return new LiteralBoolean(!l || r); - case "==": - return new LiteralBoolean(l == r); - case "!=": - return new LiteralBoolean(l != r); - } + return switch (op) { + case "&&" -> new LiteralBoolean(l && r); + case "||" -> new LiteralBoolean(l || r); + case "-->" -> new LiteralBoolean(!l || r); + case "==" -> new LiteralBoolean(l == r); + case "!=" -> new LiteralBoolean(l != r); + default -> binExp; + }; } // no folding, return original return binExp; diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/LogicSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/LogicSimplifier.java index 11f0f310..a0b971ea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/LogicSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/LogicSimplifier.java @@ -41,168 +41,177 @@ private static Expression simplifyBinaryExpression(BinaryExpression binExp) { Expression right = binExp.getSecondOperand(); String operator = binExp.getOperator(); - // boolean logic simplifications - if (operator.equals("&&")) { - // true && x => x - if (left instanceof LiteralBoolean && ((LiteralBoolean) left).isBooleanTrue()) { - return right; - } - // x && true => x - if (right instanceof LiteralBoolean && ((LiteralBoolean) right).isBooleanTrue()) { - return left; - } - // false && x => false - if (left instanceof LiteralBoolean && !((LiteralBoolean) left).isBooleanTrue()) { - return new LiteralBoolean(false); - } - // x && false => false - if (right instanceof LiteralBoolean && !((LiteralBoolean) right).isBooleanTrue()) { - return new LiteralBoolean(false); - } - } else if (operator.equals("||")) { - // true || x => true - if (left instanceof LiteralBoolean && ((LiteralBoolean) left).isBooleanTrue()) { - return new LiteralBoolean(true); - } - // x || true => true - if (right instanceof LiteralBoolean && ((LiteralBoolean) right).isBooleanTrue()) { - return new LiteralBoolean(true); - } - // false || x => x - if (left instanceof LiteralBoolean && !((LiteralBoolean) left).isBooleanTrue()) { - return right; - } - // x || false => x - if (right instanceof LiteralBoolean && !((LiteralBoolean) right).isBooleanTrue()) { - return left; - } - } else if (operator.equals("-->")) { - // false --> x => true - if (left instanceof LiteralBoolean && !((LiteralBoolean) left).isBooleanTrue()) { - return new LiteralBoolean(true); - } - // x --> true => true - if (right instanceof LiteralBoolean && ((LiteralBoolean) right).isBooleanTrue()) { - return new LiteralBoolean(true); - } - // true --> x => x - if (left instanceof LiteralBoolean && ((LiteralBoolean) left).isBooleanTrue()) { - return right; - } - } - - // arithmetic identity simplifications - else if (operator.equals("+")) { - // 0 + x => x - if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 0) { - return right; - } - // x + 0 => x - if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 0) { - return left; - } - // 0.0 + x => x - if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 0.0) { - return right; - } - // x + 0.0 => x - if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 0.0) { - return left; - } - } else if (operator.equals("-")) { - // x - 0 => x - if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 0) { - return left; - } - // x - 0.0 => x - if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 0.0) { - return left; - } - } else if (operator.equals("*")) { - // 1 * x => x - if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 1) { - return right; - } - // x * 1 => x - if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 1) { - return left; - } - // 0 * x => 0 - if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 0) { - return new LiteralInt(0); - } - // x * 0 => 0 - if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 0) { - return new LiteralInt(0); - } - // 1.0 * x => x - if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 1.0) { - return right; - } - // x * 1.0 => x - if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 1.0) { - return left; + switch (operator) { + // logical simplifications + case "&&" -> { + // true && x => x + if (left instanceof LiteralBoolean && ((LiteralBoolean) left).isBooleanTrue()) { + return right; + } + // x && true => x + if (right instanceof LiteralBoolean && ((LiteralBoolean) right).isBooleanTrue()) { + return left; + } + // false && x => false + if (left instanceof LiteralBoolean && !((LiteralBoolean) left).isBooleanTrue()) { + return new LiteralBoolean(false); + } + // x && false => false + if (right instanceof LiteralBoolean && !((LiteralBoolean) right).isBooleanTrue()) { + return new LiteralBoolean(false); + } } - // 0.0 * x => 0.0 - if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 0.0) { - return new LiteralReal(0.0); + case "||" -> { + // true || x => true + if (left instanceof LiteralBoolean && ((LiteralBoolean) left).isBooleanTrue()) { + return new LiteralBoolean(true); + } + // x || true => true + if (right instanceof LiteralBoolean && ((LiteralBoolean) right).isBooleanTrue()) { + return new LiteralBoolean(true); + } + // false || x => x + if (left instanceof LiteralBoolean && !((LiteralBoolean) left).isBooleanTrue()) { + return right; + } + // x || false => x + if (right instanceof LiteralBoolean && !((LiteralBoolean) right).isBooleanTrue()) { + return left; + } } - // x * 0.0 => 0.0 - if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 0.0) { - return new LiteralReal(0.0); + case "-->" -> { + // false --> x => true + if (left instanceof LiteralBoolean && !((LiteralBoolean) left).isBooleanTrue()) { + return new LiteralBoolean(true); + } + // x --> true => true + if (right instanceof LiteralBoolean && ((LiteralBoolean) right).isBooleanTrue()) { + return new LiteralBoolean(true); + } + // true --> x => x + if (left instanceof LiteralBoolean && ((LiteralBoolean) left).isBooleanTrue()) { + return right; + } } - } else if (operator.equals("/")) { - // x / 1 => x - if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 1) { - return left; + // arithmetic simplifications + case "+" -> { + // 0 + x => x + if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 0) { + return right; + } + // x + 0 => x + if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 0) { + return left; + } + // 0.0 + x => x + if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 0.0) { + return right; + } + // x + 0.0 => x + if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 0.0) { + return left; + } } - // x / 1.0 => x - if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 1.0) { - return left; + case "-" -> { + // x - 0 => x + if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 0) { + return left; + } + // x - 0.0 => x + if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 0.0) { + return left; + } } - // 0 / x => 0 (assuming x != 0) - if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 0) { - return new LiteralInt(0); + case "*" -> { + // 1 * x => x + if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 1) { + return right; + } + // x * 1 => x + if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 1) { + return left; + } + // 0 * x => 0 + if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 0) { + return new LiteralInt(0); + } + // x * 0 => 0 + if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 0) { + return new LiteralInt(0); + } + // 1.0 * x => x + if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 1.0) { + return right; + } + // x * 1.0 => x + if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 1.0) { + return left; + } + // 0.0 * x => 0.0 + if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 0.0) { + return new LiteralReal(0.0); + } + // x * 0.0 => 0.0 + if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 0.0) { + return new LiteralReal(0.0); + } } - // 0.0 / x => 0.0 (assuming x != 0) - if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 0.0) { - return new LiteralReal(0.0); + case "/" -> { + // x / 1 => x + if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 1) { + return left; + } + // x / 1.0 => x + if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 1.0) { + return left; + } + // 0 / x => 0 (assuming x != 0) + if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 0) { + return new LiteralInt(0); + } + // 0.0 / x => 0.0 (assuming x != 0) + if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 0.0) { + return new LiteralReal(0.0); + } } - } - - // comparison simplifications - else if (operator.equals("==")) { - // x == x => true - if (left.equals(right)) { - return new LiteralBoolean(true); + // comparison simplifications + case "==" -> { + // x == x => true + if (left.equals(right)) { + return new LiteralBoolean(true); + } } - } else if (operator.equals("!=")) { - // x != x => false - if (left.equals(right)) { - return new LiteralBoolean(false); + case "!=" -> { + // x != x => false + if (left.equals(right)) { + return new LiteralBoolean(false); + } } } - // no simplification applied + // no simplification return binExp; } private static Expression simplifyUnaryExpression(UnaryExpression unaryExpr) { Expression operand = unaryExpr.getChildren().get(0); String operator = unaryExpr.getOp(); - if (operator.equals("!")) { - // !!x => x (double negation) - if (operand instanceof UnaryExpression) { - UnaryExpression innerUnary = (UnaryExpression) operand; - if (innerUnary.getOp().equals("!")) { - return innerUnary.getChildren().get(0); + switch (operator) { + case "!" -> { + // !!x => x (double negation) + if (operand instanceof UnaryExpression) { + UnaryExpression innerUnary = (UnaryExpression) operand; + if (innerUnary.getOp().equals("!")) { + return innerUnary.getChildren().get(0); + } } } - } else if (operator.equals("-")) { - // -(-x) => x (double negation) - if (operand instanceof UnaryExpression) { - UnaryExpression innerUnary = (UnaryExpression) operand; - if (innerUnary.getOp().equals("-")) { - return innerUnary.getChildren().get(0); + case "-" -> { + // -(-x) => x (double negation) + if (operand instanceof UnaryExpression) { + UnaryExpression innerUnary = (UnaryExpression) operand; + if (innerUnary.getOp().equals("-")) { + return innerUnary.getChildren().get(0); + } } } } From 0a69e86362b0959d2e063ac2db35e820cc77d46a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 2 Oct 2025 21:00:40 +0100 Subject: [PATCH 05/12] Fix Unary Minus Constant Folding --- .../liquidjava/rj_language/opt/ConstantFolding.java | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java index 03535970..a24e26f8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java @@ -119,6 +119,17 @@ private static Expression foldUnaryExpression(UnaryExpression unaryExp) { boolean value = ((LiteralBoolean) operand).isBooleanTrue(); return new LiteralBoolean(!value); } + if (operator.equals("-")) { + // -(x) = -x + if (operand instanceof LiteralInt) { + int value = ((LiteralInt) operand).getValue(); + return new LiteralInt(-value); + } + if (operand instanceof LiteralReal) { + double value = ((LiteralReal) operand).getValue(); + return new LiteralReal(-value); + } + } return unaryExp; } } From 0350e9a8c515a1abbcf55f74b06fec445cf7bd9c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 3 Oct 2025 11:04:40 +0100 Subject: [PATCH 06/12] Refactoring --- .../rj_language/opt/ConstantFolding.java | 9 +++++---- .../rj_language/opt/ConstantPropagation.java | 2 +- ...iableExtractor.java => VariableCollector.java} | 15 +++++++-------- 3 files changed, 13 insertions(+), 13 deletions(-) rename liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/{VariableExtractor.java => VariableCollector.java} (86%) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java index a24e26f8..c0dfc580 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java @@ -22,7 +22,8 @@ public static Expression fold(Expression exp) { // try to fold the current expression if (exp instanceof BinaryExpression) { return foldBinaryExpression((BinaryExpression) exp); - } else if (exp instanceof UnaryExpression) { + } + if (exp instanceof UnaryExpression) { return foldUnaryExpression((UnaryExpression) exp); } return exp; @@ -55,7 +56,7 @@ private static Expression foldBinaryExpression(BinaryExpression binExp) { } // arithmetic operations with real literals - else if (left instanceof LiteralReal && right instanceof LiteralReal) { + if (left instanceof LiteralReal && right instanceof LiteralReal) { double l = ((LiteralReal) left).getValue(); double r = ((LiteralReal) right).getValue(); return switch (op) { @@ -75,7 +76,7 @@ else if (left instanceof LiteralReal && right instanceof LiteralReal) { } // mixed integer and real operations - else if ((left instanceof LiteralInt && right instanceof LiteralReal) || (left instanceof LiteralReal && right instanceof LiteralInt)) { + if ((left instanceof LiteralInt && right instanceof LiteralReal) || (left instanceof LiteralReal && right instanceof LiteralInt)) { double l = left instanceof LiteralInt ? ((LiteralInt) left).getValue() : ((LiteralReal) left).getValue(); double r = right instanceof LiteralInt ? ((LiteralInt) right).getValue() : ((LiteralReal) right).getValue(); return switch (op) { @@ -95,7 +96,7 @@ else if ((left instanceof LiteralInt && right instanceof LiteralReal) || (left i } // boolean operations with boolean literals - else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) { + if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) { boolean l = ((LiteralBoolean) left).isBooleanTrue(); boolean r = ((LiteralBoolean) right).isBooleanTrue(); return switch (op) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java index e4390d26..6f06a3e9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java @@ -7,7 +7,7 @@ public class ConstantPropagation { public static Expression propagate(Expression exp) { - Map substitutions = VariableExtractor.extract(exp); + Map substitutions = VariableCollector.collect(exp); return propagateRecursive(exp, substitutions); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableExtractor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableCollector.java similarity index 86% rename from liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableExtractor.java rename to liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableCollector.java index a02a3724..6e3f3209 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableExtractor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableCollector.java @@ -10,14 +10,14 @@ import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.Var; -public class VariableExtractor { +public class VariableCollector { - public static Map extract(Expression exp) { + public static Map collect(Expression exp) { Map assertions = new HashMap<>(); // only extract assertions if the expression contains conjunctions (&&) if (containsConjunction(exp)) { - extractRecursive(exp, assertions); + collectRecursive(exp, assertions); } return assertions; } @@ -41,20 +41,19 @@ private static boolean containsConjunction(Expression exp) { return false; } - private static void extractRecursive(Expression exp, Map assertions) { + private static void collectRecursive(Expression exp, Map assertions) { if (exp instanceof BinaryExpression) { BinaryExpression binExp = (BinaryExpression) exp; String operator = binExp.getOperator(); if (operator.equals("&&")) { // for conjunctions recursively extract from both sides - extractRecursive(binExp.getFirstOperand(), assertions); - extractRecursive(binExp.getSecondOperand(), assertions); + collectRecursive(binExp.getFirstOperand(), assertions); + collectRecursive(binExp.getSecondOperand(), assertions); } else if (operator.equals("==")) { // for assertions check if one side is a variable and the other is a literal Expression left = binExp.getFirstOperand(); Expression right = binExp.getSecondOperand(); - if (left instanceof Var && isLiteral(right)) { assertions.put(((Var) left).getName(), right); } else if (right instanceof Var && isLiteral(left)) { @@ -65,7 +64,7 @@ private static void extractRecursive(Expression exp, Map ass // for other expressions, recurse into children else if (exp.hasChildren()) { for (Expression child : exp.getChildren()) { - extractRecursive(child, assertions); + collectRecursive(child, assertions); } } } From b3d15183c8435931156f26b1e5c00fa59dc2ef54 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 5 Oct 2025 22:34:28 +0100 Subject: [PATCH 07/12] Simplify Expressions Using Derivation Nodes This allows simplification steps to be expanded by keeping track of their origin nodes, for both constant propagation and constant folding --- .../java/liquidjava/errors/ErrorHandler.java | 2 +- .../liquidjava/rj_language/Predicate.java | 5 +- .../rj_language/ast/Expression.java | 8 +- .../rj_language/opt/ConstantFolding.java | 227 ++++++++++------- .../rj_language/opt/ConstantPropagation.java | 77 ++++-- .../rj_language/opt/DerivationNode.java | 32 --- .../rj_language/opt/ExpressionSimplifier.java | 89 ++++--- .../rj_language/opt/LogicSimplifier.java | 239 ------------------ .../rj_language/opt/VariableCollector.java | 75 ------ .../rj_language/opt/VariableResolver.java | 56 ++++ .../derivation_node/BinaryDerivationNode.java | 39 +++ .../opt/derivation_node/DerivationNode.java | 42 +++ .../derivation_node/UnaryDerivationNode.java | 31 +++ .../derivation_node/ValDerivationNode.java | 51 ++++ .../derivation_node/VarDerivationNode.java | 24 ++ 15 files changed, 507 insertions(+), 490 deletions(-) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/DerivationNode.java delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/LogicSimplifier.java delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableCollector.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java index 557f2ada..7e45622a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java @@ -41,7 +41,7 @@ public static void printError(CtElement var, String moreInfo, Predicate expe // all message sb.append(sbtitle.toString() + "\n\n"); sb.append("Type expected:" + expectedType.toString() + "\n"); - sb.append("Refinement found:\n" + cSMT.simplify() + "\n"); + sb.append("Refinement found:\n" + cSMT.simplify().getValue() + "\n"); sb.append(printMap(map)); sb.append("Location: " + var.getPosition() + "\n"); sb.append("______________________________________________________\n"); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index bf24eec5..7fb7fa94 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -21,7 +21,8 @@ import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; -import liquidjava.rj_language.opt.DerivationNode; +import liquidjava.rj_language.opt.derivation_node.DerivationNode; +import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.rj_language.opt.ExpressionSimplifier; import liquidjava.rj_language.parsing.ParsingException; import liquidjava.rj_language.parsing.RefinementsParser; @@ -214,7 +215,7 @@ public Expression getExpression() { return exp; } - public DerivationNode simplify() { + public ValDerivationNode simplify() { return ExpressionSimplifier.simplify(exp.clone()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java index da75ec71..008b651c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -1,9 +1,11 @@ package liquidjava.rj_language.ast; -import com.microsoft.z3.Expr; import java.util.ArrayList; import java.util.List; import java.util.Map; + +import com.microsoft.z3.Expr; + import liquidjava.processor.context.Context; import liquidjava.processor.facade.AliasDTO; import liquidjava.rj_language.ast.typing.TypeInfer; @@ -47,6 +49,10 @@ public void setChild(int index, Expression element) { children.set(index, element); } + public boolean isLiteral() { + return this instanceof LiteralInt || this instanceof LiteralReal || this instanceof LiteralBoolean; + } + /** * Substitutes the expression first given expression by the second * diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java index c0dfc580..e29f3bb3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java @@ -2,135 +2,186 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; import liquidjava.rj_language.ast.LiteralReal; 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 ConstantFolding { - public static Expression fold(Expression exp) { - // recursively simplify in all children - if (exp.hasChildren()) { - for (int i = 0; i < exp.getChildren().size(); i++) { - Expression child = exp.getChildren().get(i); - Expression propagatedChild = fold(child); - exp.setChild(i, propagatedChild); - } - } - - // try to fold the current expression + public static ValDerivationNode fold(ValDerivationNode node) { + Expression exp = node.getValue(); if (exp instanceof BinaryExpression) { - return foldBinaryExpression((BinaryExpression) exp); + return foldBinary(node); } if (exp instanceof UnaryExpression) { - return foldUnaryExpression((UnaryExpression) exp); + return foldUnary(node); + } + if (exp instanceof GroupExpression) { + GroupExpression group = (GroupExpression) exp; + if (group.getChildren().size() == 1) { + return fold(new ValDerivationNode(group.getChildren().get(0), node.getOrigin())); + } } - return exp; + return node; } - private static Expression foldBinaryExpression(BinaryExpression binExp) { - Expression left = binExp.getFirstOperand(); - Expression right = binExp.getSecondOperand(); + private static ValDerivationNode foldBinary(ValDerivationNode node) { + BinaryExpression binExp = (BinaryExpression) node.getValue(); + DerivationNode parent = node.getOrigin(); + + // fold child nodes + ValDerivationNode leftNode; + ValDerivationNode rightNode; + if (parent instanceof BinaryDerivationNode) { + // has origin (from constant propagation) + BinaryDerivationNode binaryOrigin = (BinaryDerivationNode) parent; + leftNode = fold(binaryOrigin.getLeft()); + rightNode = fold(binaryOrigin.getRight()); + } else { + // no origin + leftNode = fold(new ValDerivationNode(binExp.getFirstOperand(), null)); + rightNode = fold(new ValDerivationNode(binExp.getSecondOperand(), null)); + } + + Expression left = leftNode.getValue(); + Expression right = rightNode.getValue(); String op = binExp.getOperator(); + binExp.setChild(0, left); + binExp.setChild(1, right); - // arithmetic operations with integer literals + // int and int if (left instanceof LiteralInt && right instanceof LiteralInt) { int l = ((LiteralInt) left).getValue(); int r = ((LiteralInt) right).getValue(); - - return switch (op) { - case "+" -> new LiteralInt(l + r); - case "-" -> new LiteralInt(l - r); - case "*" -> new LiteralInt(l * r); - case "/" -> r != 0 ? new LiteralInt(l / r) : binExp; - case "%" -> r != 0 ? new LiteralInt(l % r) : binExp; - case "<" -> new LiteralBoolean(l < r); - case "<=" -> new LiteralBoolean(l <= r); - case ">" -> new LiteralBoolean(l > r); - case ">=" -> new LiteralBoolean(l >= r); - case "==" -> new LiteralBoolean(l == r); - case "!=" -> new LiteralBoolean(l != r); - default -> binExp; + Expression res = switch (op) { + case "+" -> new LiteralInt(l + r); + case "-" -> new LiteralInt(l - r); + case "*" -> new LiteralInt(l * r); + case "/" -> r != 0 ? new LiteralInt(l / r) : null; + case "%" -> r != 0 ? new LiteralInt(l % r) : null; + case "<" -> new LiteralBoolean(l < r); + case "<=" -> new LiteralBoolean(l <= r); + case ">" -> new LiteralBoolean(l > r); + case ">=" -> new LiteralBoolean(l >= r); + case "==" -> new LiteralBoolean(l == r); + case "!=" -> new LiteralBoolean(l != r); + default -> null; }; + if (res != null) + return new ValDerivationNode(res, new BinaryDerivationNode(leftNode, rightNode, op)); } - - // arithmetic operations with real literals - if (left instanceof LiteralReal && right instanceof LiteralReal) { + // real and real + else if (left instanceof LiteralReal && right instanceof LiteralReal) { double l = ((LiteralReal) left).getValue(); double r = ((LiteralReal) right).getValue(); - return switch (op) { - case "+" -> new LiteralReal(l + r); - case "-" -> new LiteralReal(l - r); - case "*" -> new LiteralReal(l * r); - case "/" -> r != 0.0 ? new LiteralReal(l / r) : binExp; - case "%" -> r != 0.0 ? new LiteralReal(l % r) : binExp; - case "<" -> new LiteralBoolean(l < r); - case "<=" -> new LiteralBoolean(l <= r); - case ">" -> new LiteralBoolean(l > r); - case ">=" -> new LiteralBoolean(l >= r); - case "==" -> new LiteralBoolean(l == r); - case "!=" -> new LiteralBoolean(l != r); - default -> binExp; + Expression res = switch (op) { + case "+" -> new LiteralReal(l + r); + case "-" -> new LiteralReal(l - r); + case "*" -> new LiteralReal(l * r); + case "/" -> r != 0.0 ? new LiteralReal(l / r) : null; + case "%" -> r != 0.0 ? new LiteralReal(l % r) : null; + case "<" -> new LiteralBoolean(l < r); + case "<=" -> new LiteralBoolean(l <= r); + case ">" -> new LiteralBoolean(l > r); + case ">=" -> new LiteralBoolean(l >= r); + case "==" -> new LiteralBoolean(l == r); + case "!=" -> new LiteralBoolean(l != r); + default -> null; }; + if (res != null) + return new ValDerivationNode(res, new BinaryDerivationNode(leftNode, rightNode, op)); } - // mixed integer and real operations - if ((left instanceof LiteralInt && right instanceof LiteralReal) || (left instanceof LiteralReal && right instanceof LiteralInt)) { + // mixed int and real + else if ((left instanceof LiteralInt && right instanceof LiteralReal) + || (left instanceof LiteralReal && right instanceof LiteralInt)) { double l = left instanceof LiteralInt ? ((LiteralInt) left).getValue() : ((LiteralReal) left).getValue(); double r = right instanceof LiteralInt ? ((LiteralInt) right).getValue() : ((LiteralReal) right).getValue(); - return switch (op) { - case "+" -> new LiteralReal(l + r); - case "-" -> new LiteralReal(l - r); - case "*" -> new LiteralReal(l * r); - case "/" -> r != 0.0 ? new LiteralReal(l / r) : binExp; - case "%" -> r != 0.0 ? new LiteralReal(l % r) : binExp; - case "<" -> new LiteralBoolean(l < r); - case "<=" -> new LiteralBoolean(l <= r); - case ">" -> new LiteralBoolean(l > r); - case ">=" -> new LiteralBoolean(l >= r); - case "==" -> new LiteralBoolean(l == r); - case "!=" -> new LiteralBoolean(l != r); - default -> binExp; + Expression res = switch (op) { + case "+" -> new LiteralReal(l + r); + case "-" -> new LiteralReal(l - r); + case "*" -> new LiteralReal(l * r); + case "/" -> r != 0.0 ? new LiteralReal(l / r) : null; + case "%" -> r != 0.0 ? new LiteralReal(l % r) : null; + case "<" -> new LiteralBoolean(l < r); + case "<=" -> new LiteralBoolean(l <= r); + case ">" -> new LiteralBoolean(l > r); + case ">=" -> new LiteralBoolean(l >= r); + case "==" -> new LiteralBoolean(l == r); + case "!=" -> new LiteralBoolean(l != r); + default -> null; }; + if (res != null) + return new ValDerivationNode(res, new BinaryDerivationNode(leftNode, rightNode, op)); } - - // boolean operations with boolean literals - if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) { + // bool and bool + else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) { boolean l = ((LiteralBoolean) left).isBooleanTrue(); boolean r = ((LiteralBoolean) right).isBooleanTrue(); - return switch (op) { - case "&&" -> new LiteralBoolean(l && r); - case "||" -> new LiteralBoolean(l || r); - case "-->" -> new LiteralBoolean(!l || r); - case "==" -> new LiteralBoolean(l == r); - case "!=" -> new LiteralBoolean(l != r); - default -> binExp; + Expression res = switch (op) { + case "&&" -> new LiteralBoolean(l && r); + case "||" -> new LiteralBoolean(l || r); + case "-->" -> new LiteralBoolean(!l || r); + case "==" -> new LiteralBoolean(l == r); + case "!=" -> new LiteralBoolean(l != r); + default -> null; }; + if (res != null) + return new ValDerivationNode(res, new BinaryDerivationNode(leftNode, rightNode, op)); } - // no folding, return original - return binExp; + + // no folding + DerivationNode origin = (leftNode.getOrigin() != null || rightNode.getOrigin() != null) + ? new BinaryDerivationNode(leftNode, rightNode, op) : null; + return new ValDerivationNode(binExp, origin); } - private static Expression foldUnaryExpression(UnaryExpression unaryExp) { - Expression operand = unaryExp.getChildren().get(0); + private static ValDerivationNode foldUnary(ValDerivationNode node) { + UnaryExpression unaryExp = (UnaryExpression) node.getValue(); + DerivationNode parent = node.getOrigin(); + + // fold child node + ValDerivationNode operandNode; + if (parent instanceof UnaryDerivationNode) { + // has origin (from constant propagation) + UnaryDerivationNode unaryOrigin = (UnaryDerivationNode) parent; + operandNode = fold(unaryOrigin.getOperand()); + } else { + // no origin + operandNode = fold(new ValDerivationNode(unaryExp.getChildren().get(0), null)); + } + Expression operand = operandNode.getValue(); String operator = unaryExp.getOp(); - if (operator.equals("!") && operand instanceof LiteralBoolean) { - // !true -> false, !false -> true + unaryExp.setChild(0, operand); + + // unary not + if ("!".equals(operator) && operand instanceof LiteralBoolean) { + // !true => false, !false => true boolean value = ((LiteralBoolean) operand).isBooleanTrue(); - return new LiteralBoolean(!value); + Expression res = new LiteralBoolean(!value); + return new ValDerivationNode(res, new UnaryDerivationNode(operandNode, operator)); } - if (operator.equals("-")) { - // -(x) = -x + // unary minus + if ("-".equals(operator)) { + // -(x) => -x if (operand instanceof LiteralInt) { - int value = ((LiteralInt) operand).getValue(); - return new LiteralInt(-value); + Expression res = new LiteralInt(-((LiteralInt) operand).getValue()); + return new ValDerivationNode(res, new UnaryDerivationNode(operandNode, operator)); } if (operand instanceof LiteralReal) { - double value = ((LiteralReal) operand).getValue(); - return new LiteralReal(-value); + Expression res = new LiteralReal(-((LiteralReal) operand).getValue()); + return new ValDerivationNode(res, new UnaryDerivationNode(operandNode, operator)); } } - return unaryExp; + + // no folding + DerivationNode origin = operandNode.getOrigin() != null ? new UnaryDerivationNode(operandNode, operator) : null; + return new ValDerivationNode(unaryExp, origin); } -} +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java index 6f06a3e9..934a6570 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java @@ -1,35 +1,74 @@ package liquidjava.rj_language.opt; +import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; +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; +import liquidjava.rj_language.opt.derivation_node.VarDerivationNode; + import java.util.Map; public class ConstantPropagation { - public static Expression propagate(Expression exp) { - Map substitutions = VariableCollector.collect(exp); + public static ValDerivationNode propagate(Expression exp) { + Map substitutions = VariableResolver.resolve(exp); return propagateRecursive(exp, substitutions); } - private static Expression propagateRecursive(Expression exp, Map substitutions) { - // apply substitutions to children for other expression types - if (exp.hasChildren()) { - Expression result = exp.clone(); - for (int i = 0; i < result.getChildren().size(); i++) { - Expression child = result.getChildren().get(i); - Expression substitutedChild = propagateRecursive(child, substitutions); - result.setChild(i, substitutedChild); - } - return result; - } - // if the expression is a variable, substitute if in map + private static ValDerivationNode propagateRecursive(Expression exp, Map subs) { + + // substitute variable if (exp instanceof Var) { Var var = (Var) exp; - String varName = var.getName(); - if (substitutions.containsKey(varName)) { - return substitutions.get(varName).clone(); + String name = var.getName(); + Expression value = subs.get(name); + // substitution + if (value != null) + return new ValDerivationNode(value.clone(), new VarDerivationNode(name)); + + // no substitution + return new ValDerivationNode(var, null); + } + + // lift unary origin + if (exp instanceof UnaryExpression) { + UnaryExpression unary = (UnaryExpression) exp; + ValDerivationNode operand = propagateRecursive(unary.getChildren().get(0), subs); + unary.setChild(0, operand.getValue()); + + DerivationNode origin = operand.getOrigin() != null ? new UnaryDerivationNode(operand, unary.getOp()) + : null; + return new ValDerivationNode(unary, origin); + } + + // lift binary origin + if (exp instanceof BinaryExpression) { + BinaryExpression binary = (BinaryExpression) exp; + 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); + } + + // 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); + propagated.setChild(i, child.getValue()); } + return new ValDerivationNode(propagated, null); } - return exp; + + // no propagation + return new ValDerivationNode(exp, null); } -} +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/DerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/DerivationNode.java deleted file mode 100644 index d6a31ab4..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/DerivationNode.java +++ /dev/null @@ -1,32 +0,0 @@ -package liquidjava.rj_language.opt; - -import liquidjava.rj_language.ast.Expression; - -public class DerivationNode { - - private DerivationNode from; - private Expression exp; - - public DerivationNode(Expression exp) { - this.exp = exp; - } - - public DerivationNode getFrom() { - return from; - } - - public void setFrom(DerivationNode from) { - this.from = from; - } - - public DerivationNode addNode(Expression exp) { - DerivationNode newNode = new DerivationNode(exp); - newNode.setFrom(this); - return newNode; - } - - @Override - public String toString() { - return String.format("%s <=\n%s", exp, from); - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java index 20e9c65c..1400e5ad 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java @@ -1,47 +1,70 @@ package liquidjava.rj_language.opt; +import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode; +import liquidjava.rj_language.opt.derivation_node.DerivationNode; +import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; public class ExpressionSimplifier { - public static DerivationNode simplify(Expression exp) { - DerivationNode currentNode = new DerivationNode(exp); - Expression currentExp = simplifyExp(exp.clone()); - currentNode = currentNode.addNode(currentExp); - boolean changed = true; - - while (changed) { - changed = false; - - Expression propagated = ConstantPropagation.propagate(currentExp.clone()); - if (!propagated.equals(currentExp)) { - currentExp = simplifyExp(propagated); - currentNode = currentNode.addNode(currentExp); - changed = true; - continue; - } + public static ValDerivationNode simplify(Expression exp) { + ValDerivationNode prop = ConstantPropagation.propagate(exp); + ValDerivationNode fold = ConstantFolding.fold(prop); + return simplifyDerivationTree(fold); + } + + /** + * Recursively simplify the derivation tree by removing redundant conjuncts + */ + private static ValDerivationNode simplifyDerivationTree(ValDerivationNode node) { + Expression value = node.getValue(); + DerivationNode origin = node.getOrigin(); + + // binary expression with && + if (value instanceof BinaryExpression) { + BinaryExpression binExp = (BinaryExpression) value; + if ("&&".equals(binExp.getOperator()) && origin instanceof BinaryDerivationNode) { + BinaryDerivationNode binOrigin = (BinaryDerivationNode) origin; - Expression folded = ConstantFolding.fold(currentExp.clone()); - if (!folded.equals(currentExp)) { - currentExp = simplifyExp(folded); - currentNode = currentNode.addNode(currentExp); - System.out.println(currentExp); - changed = true; - continue; + // 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); } } - return currentNode; + // no simplification + return node; } - private static Expression simplifyExp(Expression exp) { - Expression current = exp.clone(); - while (true) { - Expression simplified = LogicSimplifier.simplify(current.clone()); - if (simplified.equals(current)) { - break; + /** + * Check if an expression is redundant + */ + private static boolean isRedundant(Expression exp) { + // true + if (exp instanceof LiteralBoolean && ((LiteralBoolean) exp).isBooleanTrue()) { + return true; + } + // x == x + if (exp instanceof BinaryExpression) { + BinaryExpression binExp = (BinaryExpression) exp; + if ("==".equals(binExp.getOperator())) { + Expression left = binExp.getFirstOperand(); + Expression right = binExp.getSecondOperand(); + return left.equals(right); } - current = simplified; } - return current; + return false; } -} \ No newline at end of file +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/LogicSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/LogicSimplifier.java deleted file mode 100644 index a0b971ea..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/LogicSimplifier.java +++ /dev/null @@ -1,239 +0,0 @@ -package liquidjava.rj_language.opt; - -import liquidjava.rj_language.ast.BinaryExpression; -import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.GroupExpression; -import liquidjava.rj_language.ast.Ite; -import liquidjava.rj_language.ast.LiteralBoolean; -import liquidjava.rj_language.ast.LiteralInt; -import liquidjava.rj_language.ast.LiteralReal; -import liquidjava.rj_language.ast.UnaryExpression; - -public class LogicSimplifier { - - public static Expression simplify(Expression exp) { - // recursively simplify in all children - if (exp.hasChildren()) { - for (int i = 0; i < exp.getChildren().size(); i++) { - Expression child = exp.getChildren().get(i); - Expression propagatedChild = simplify(child); - exp.setChild(i, propagatedChild); - } - } - - // apply simplification rules to the current expression - if (exp instanceof BinaryExpression) { - return simplifyBinaryExpression((BinaryExpression) exp); - } else if (exp instanceof UnaryExpression) { - return simplifyUnaryExpression((UnaryExpression) exp); - } else if (exp instanceof Ite) { - return simplifyIte((Ite) exp); - } else if (exp instanceof GroupExpression) { - return simplifyGroupExpression((GroupExpression) exp); - } - - // literals, variables and function invocations cant be simplified - return exp; - } - - private static Expression simplifyBinaryExpression(BinaryExpression binExp) { - Expression left = binExp.getFirstOperand(); - Expression right = binExp.getSecondOperand(); - String operator = binExp.getOperator(); - - switch (operator) { - // logical simplifications - case "&&" -> { - // true && x => x - if (left instanceof LiteralBoolean && ((LiteralBoolean) left).isBooleanTrue()) { - return right; - } - // x && true => x - if (right instanceof LiteralBoolean && ((LiteralBoolean) right).isBooleanTrue()) { - return left; - } - // false && x => false - if (left instanceof LiteralBoolean && !((LiteralBoolean) left).isBooleanTrue()) { - return new LiteralBoolean(false); - } - // x && false => false - if (right instanceof LiteralBoolean && !((LiteralBoolean) right).isBooleanTrue()) { - return new LiteralBoolean(false); - } - } - case "||" -> { - // true || x => true - if (left instanceof LiteralBoolean && ((LiteralBoolean) left).isBooleanTrue()) { - return new LiteralBoolean(true); - } - // x || true => true - if (right instanceof LiteralBoolean && ((LiteralBoolean) right).isBooleanTrue()) { - return new LiteralBoolean(true); - } - // false || x => x - if (left instanceof LiteralBoolean && !((LiteralBoolean) left).isBooleanTrue()) { - return right; - } - // x || false => x - if (right instanceof LiteralBoolean && !((LiteralBoolean) right).isBooleanTrue()) { - return left; - } - } - case "-->" -> { - // false --> x => true - if (left instanceof LiteralBoolean && !((LiteralBoolean) left).isBooleanTrue()) { - return new LiteralBoolean(true); - } - // x --> true => true - if (right instanceof LiteralBoolean && ((LiteralBoolean) right).isBooleanTrue()) { - return new LiteralBoolean(true); - } - // true --> x => x - if (left instanceof LiteralBoolean && ((LiteralBoolean) left).isBooleanTrue()) { - return right; - } - } - // arithmetic simplifications - case "+" -> { - // 0 + x => x - if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 0) { - return right; - } - // x + 0 => x - if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 0) { - return left; - } - // 0.0 + x => x - if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 0.0) { - return right; - } - // x + 0.0 => x - if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 0.0) { - return left; - } - } - case "-" -> { - // x - 0 => x - if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 0) { - return left; - } - // x - 0.0 => x - if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 0.0) { - return left; - } - } - case "*" -> { - // 1 * x => x - if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 1) { - return right; - } - // x * 1 => x - if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 1) { - return left; - } - // 0 * x => 0 - if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 0) { - return new LiteralInt(0); - } - // x * 0 => 0 - if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 0) { - return new LiteralInt(0); - } - // 1.0 * x => x - if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 1.0) { - return right; - } - // x * 1.0 => x - if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 1.0) { - return left; - } - // 0.0 * x => 0.0 - if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 0.0) { - return new LiteralReal(0.0); - } - // x * 0.0 => 0.0 - if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 0.0) { - return new LiteralReal(0.0); - } - } - case "/" -> { - // x / 1 => x - if (right instanceof LiteralInt && ((LiteralInt) right).getValue() == 1) { - return left; - } - // x / 1.0 => x - if (right instanceof LiteralReal && ((LiteralReal) right).getValue() == 1.0) { - return left; - } - // 0 / x => 0 (assuming x != 0) - if (left instanceof LiteralInt && ((LiteralInt) left).getValue() == 0) { - return new LiteralInt(0); - } - // 0.0 / x => 0.0 (assuming x != 0) - if (left instanceof LiteralReal && ((LiteralReal) left).getValue() == 0.0) { - return new LiteralReal(0.0); - } - } - // comparison simplifications - case "==" -> { - // x == x => true - if (left.equals(right)) { - return new LiteralBoolean(true); - } - } - case "!=" -> { - // x != x => false - if (left.equals(right)) { - return new LiteralBoolean(false); - } - } - } - // no simplification - return binExp; - } - - private static Expression simplifyUnaryExpression(UnaryExpression unaryExpr) { - Expression operand = unaryExpr.getChildren().get(0); - String operator = unaryExpr.getOp(); - switch (operator) { - case "!" -> { - // !!x => x (double negation) - if (operand instanceof UnaryExpression) { - UnaryExpression innerUnary = (UnaryExpression) operand; - if (innerUnary.getOp().equals("!")) { - return innerUnary.getChildren().get(0); - } - } - } - case "-" -> { - // -(-x) => x (double negation) - if (operand instanceof UnaryExpression) { - UnaryExpression innerUnary = (UnaryExpression) operand; - if (innerUnary.getOp().equals("-")) { - return innerUnary.getChildren().get(0); - } - } - } - } - return unaryExpr; - } - - private static Expression simplifyIte(Ite iteExp) { - Expression condExp = iteExp.getChildren().get(0); - Expression thenExp = iteExp.getChildren().get(1); - Expression elseExp = iteExp.getChildren().get(2); - if (condExp instanceof LiteralBoolean) { - boolean cond = ((LiteralBoolean) condExp).isBooleanTrue(); - return cond ? thenExp : elseExp; - } - return iteExp; - } - - private static Expression simplifyGroupExpression(GroupExpression groupExp) { - // (expression) => expression - if (groupExp.getChildren().size() == 1) { - return groupExp.getChildren().get(0); - } - return groupExp; - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableCollector.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableCollector.java deleted file mode 100644 index 6e3f3209..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableCollector.java +++ /dev/null @@ -1,75 +0,0 @@ -package liquidjava.rj_language.opt; - -import java.util.HashMap; -import java.util.Map; - -import liquidjava.rj_language.ast.BinaryExpression; -import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.LiteralBoolean; -import liquidjava.rj_language.ast.LiteralInt; -import liquidjava.rj_language.ast.LiteralReal; -import liquidjava.rj_language.ast.Var; - -public class VariableCollector { - - public static Map collect(Expression exp) { - Map assertions = new HashMap<>(); - - // only extract assertions if the expression contains conjunctions (&&) - if (containsConjunction(exp)) { - collectRecursive(exp, assertions); - } - return assertions; - } - - private static boolean containsConjunction(Expression exp) { - if (exp instanceof BinaryExpression) { - BinaryExpression binExp = (BinaryExpression) exp; - if (binExp.getOperator().equals("&&")) { - return true; - } - // recursively check children - return containsConjunction(binExp.getFirstOperand()) || containsConjunction(binExp.getSecondOperand()); - } - if (exp.hasChildren()) { - for (Expression child : exp.getChildren()) { - if (containsConjunction(child)) { - return true; - } - } - } - return false; - } - - private static void collectRecursive(Expression exp, Map assertions) { - if (exp instanceof BinaryExpression) { - BinaryExpression binExp = (BinaryExpression) exp; - String operator = binExp.getOperator(); - - if (operator.equals("&&")) { - // for conjunctions recursively extract from both sides - collectRecursive(binExp.getFirstOperand(), assertions); - collectRecursive(binExp.getSecondOperand(), assertions); - } else if (operator.equals("==")) { - // for assertions check if one side is a variable and the other is a literal - Expression left = binExp.getFirstOperand(); - Expression right = binExp.getSecondOperand(); - if (left instanceof Var && isLiteral(right)) { - assertions.put(((Var) left).getName(), right); - } else if (right instanceof Var && isLiteral(left)) { - assertions.put(((Var) right).getName(), left); - } - } - } - // for other expressions, recurse into children - else if (exp.hasChildren()) { - for (Expression child : exp.getChildren()) { - collectRecursive(child, assertions); - } - } - } - - private static boolean isLiteral(Expression exp) { - return exp instanceof LiteralInt || exp instanceof LiteralReal || exp instanceof LiteralBoolean; - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java new file mode 100644 index 00000000..6f74ed46 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java @@ -0,0 +1,56 @@ +package liquidjava.rj_language.opt; + +import java.util.HashMap; +import java.util.Map; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.Var; + +public class VariableResolver { + + public static Map resolve(Expression exp) { + Map map = new HashMap<>(); + resolveRecursive(exp, map); + return resolveTransitive(map); + } + + private static void resolveRecursive(Expression exp, Map map) { + if (!(exp instanceof BinaryExpression)) { + return; + } + BinaryExpression be = (BinaryExpression) exp; + String op = be.getOperator(); + if ("&&".equals(op)) { + resolveRecursive(be.getFirstOperand(), map); + resolveRecursive(be.getSecondOperand(), map); + } else if ("==".equals(op)) { + Expression left = be.getFirstOperand(); + Expression right = be.getSecondOperand(); + if (left instanceof Var && (right.isLiteral() || right instanceof Var)) { + map.put(left.toString(), right.clone()); + } else if (right instanceof Var && left.isLiteral()) { + map.put(right.toString(), left.clone()); + } + } + } + + // e.g. x == y && y == 1 => x == 1 + private static Map resolveTransitive(Map map) { + Map result = new HashMap<>(); + for (Map.Entry entry : map.entrySet()) { + result.put(entry.getKey(), lookup(entry.getValue(), map)); + } + return result; + } + + private static Expression lookup(Expression exp, Map map) { + if (!(exp instanceof Var)) { + return exp; + } + Expression value = map.get(exp.toString()); + if (value == null) { + return exp; + } + return lookup(value, map); + } +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java new file mode 100644 index 00000000..dbe24e8d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java @@ -0,0 +1,39 @@ +package liquidjava.rj_language.opt.derivation_node; + +import java.util.Map; + +public class BinaryDerivationNode extends DerivationNode { + + private final ValDerivationNode left; + private final ValDerivationNode right; + private final String op; + + public BinaryDerivationNode(ValDerivationNode left, ValDerivationNode right, String op) { + this.left = left; + this.right = right; + this.op = op; + } + + public ValDerivationNode getLeft() { + return left; + } + + public ValDerivationNode getRight() { + return right; + } + + public String getOp() { + return op; + } + + @Override + public Map toJson() { + Map json = baseJson(); + json.put("op", op); + if (left != null) + json.put("left", left.toJson()); + if (right != null) + json.put("right", right.toJson()); + return json; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java new file mode 100644 index 00000000..9b6cb0da --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java @@ -0,0 +1,42 @@ +package liquidjava.rj_language.opt.derivation_node; + +import java.util.LinkedHashMap; +import java.util.Map; + +public abstract class DerivationNode { + + @Override + public String toString() { + return prettyPrint(toJson(), ""); + } + + private String prettyPrint(Map json, String indent) { + StringBuilder sb = new StringBuilder(); + String nextIndent = indent + " "; + sb.append("{\n"); + for (String key : json.keySet()) { + sb.append(nextIndent + "\"" + key + "\": "); + Object value = json.get(key); + if (value instanceof Map) { + sb.append(prettyPrint((Map) value, nextIndent)); + } else if (value instanceof String) { + sb.append("\"" + value + "\""); + } else { + sb.append(value); + } + sb.append(",\n"); + } + if (json.size() > 0) { + sb.setLength(sb.length() - 2); // remove last comma + sb.append("\n"); + } + sb.append(indent + "}"); + return sb.toString(); + } + + public abstract Map toJson(); + + protected Map baseJson() { + return new LinkedHashMap<>(); + } +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java new file mode 100644 index 00000000..e1286369 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java @@ -0,0 +1,31 @@ +package liquidjava.rj_language.opt.derivation_node; + +import java.util.Map; + +public class UnaryDerivationNode extends DerivationNode { + + private final ValDerivationNode operand; + private final String operator; + + public UnaryDerivationNode(ValDerivationNode operand, String operator) { + this.operand = operand; + this.operator = operator; + } + + public ValDerivationNode getOperand() { + return operand; + } + + public String getOperator() { + return operator; + } + + @Override + public Map toJson() { + Map json = baseJson(); + json.put("op", operator); + if (operand != null) + json.put("operand", operand.toJson()); + return json; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java new file mode 100644 index 00000000..b96f2e95 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java @@ -0,0 +1,51 @@ +package liquidjava.rj_language.opt.derivation_node; + +import java.util.Map; + +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralReal; +import liquidjava.rj_language.ast.Var; + +public class ValDerivationNode extends DerivationNode { + + private final Expression value; + private final DerivationNode origin; + + public ValDerivationNode(Expression exp, DerivationNode origin) { + this.value = exp; + this.origin = origin; + } + + public Expression getValue() { + return value; + } + + public DerivationNode getOrigin() { + return origin; + } + + @Override + public Map toJson() { + Map json = baseJson(); + json.put("value", expToValue(value)); + if (origin != null) + json.put("origin", origin.toJson()); + return json; + } + + private Object expToValue(Expression exp) { + if (exp == null) + return null; + if (exp instanceof LiteralInt) + return ((LiteralInt) exp).getValue(); + if (exp instanceof LiteralReal) + return ((LiteralReal) exp).getValue(); + if (exp instanceof LiteralBoolean) + return ((LiteralBoolean) exp).isBooleanTrue(); + if (exp instanceof Var) + return ((Var) exp).getName(); + return exp.toString(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java new file mode 100644 index 00000000..619abb54 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java @@ -0,0 +1,24 @@ +package liquidjava.rj_language.opt.derivation_node; + +import java.util.Map; + +public class VarDerivationNode extends DerivationNode { + + private final String var; + + public VarDerivationNode(String var) { + this.var = var; + } + + public String getVar() { + return var; + } + + @Override + public Map toJson() { + Map json = baseJson(); + if (var != null) + json.put("var", var); + return json; + } +} From 0374a6796d821f8ef344d40332979bf6fd1521c2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 6 Oct 2025 14:05:50 +0100 Subject: [PATCH 08/12] Fix Circular References in Variable Resolver --- .../rj_language/opt/VariableResolver.java | 28 ++++++++++++------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java index 6f74ed46..bb978a3b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java @@ -1,7 +1,10 @@ package liquidjava.rj_language.opt; import java.util.HashMap; +import java.util.HashSet; import java.util.Map; +import java.util.Set; + import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.Var; @@ -15,9 +18,9 @@ public static Map resolve(Expression exp) { } private static void resolveRecursive(Expression exp, Map map) { - if (!(exp instanceof BinaryExpression)) { + if (!(exp instanceof BinaryExpression)) return; - } + BinaryExpression be = (BinaryExpression) exp; String op = be.getOperator(); if ("&&".equals(op)) { @@ -38,19 +41,24 @@ private static void resolveRecursive(Expression exp, Map map private static Map resolveTransitive(Map map) { Map result = new HashMap<>(); for (Map.Entry entry : map.entrySet()) { - result.put(entry.getKey(), lookup(entry.getValue(), map)); + result.put(entry.getKey(), lookup(entry.getValue(), map, new HashSet<>())); } return result; } - private static Expression lookup(Expression exp, Map map) { - if (!(exp instanceof Var)) { + private static Expression lookup(Expression exp, Map map, Set seen) { + if (!(exp instanceof Var)) return exp; - } - Expression value = map.get(exp.toString()); - if (value == null) { + + String name = exp.toString(); + if (seen.contains(name)) + return exp; // circular reference + + Expression value = map.get(name); + if (value == null) return exp; - } - return lookup(value, map); + + seen.add(name); + return lookup(value, map, seen); } } \ No newline at end of file From 328a839c646d26cc88f9a96d11924ad4a499617c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 6 Oct 2025 15:09:03 +0100 Subject: [PATCH 09/12] Add Tests for ExpressionSimplifier (Sonnet 4.5) --- .../opt/ExpressionSimplifierTest.java | 338 ++++++++++++++++++ 1 file changed, 338 insertions(+) create mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java new file mode 100644 index 00000000..dbf89b8b --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java @@ -0,0 +1,338 @@ +package liquidjava.rj_language.opt; + +import static org.junit.jupiter.api.Assertions.*; + +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.UnaryExpression; +import liquidjava.rj_language.ast.Var; +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; +import liquidjava.rj_language.opt.derivation_node.VarDerivationNode; +import org.junit.jupiter.api.Test; + +/** + * Test suite for expression simplification using constant propagation and folding + */ +class ExpressionSimplifierTest { + + @Test + void testNegation() { + // Given: -a && a == 7 + // Expected: -7 + + Expression varA = new Var("a"); + Expression negA = new UnaryExpression("-", varA); + Expression seven = new LiteralInt(7); + Expression aEquals7 = new BinaryExpression(varA, "==", seven); + Expression fullExpression = new BinaryExpression(negA, "&&", aEquals7); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("-7", result.getValue().toString(), "Expected result to be -7"); + + // 7 from variable a + ValDerivationNode val7 = new ValDerivationNode(new LiteralInt(7), new VarDerivationNode("a")); + + // -7 + UnaryDerivationNode negation = new UnaryDerivationNode(val7, "-"); + ValDerivationNode expected = new ValDerivationNode(new LiteralInt(-7), negation); + + // Compare the derivation trees + assertDerivationEquals(expected, result, ""); + } + + @Test + void testSimpleAddition() { + // Given: a + b && a == 3 && b == 5 + // Expected: 8 (3 + 5) + + Expression varA = new Var("a"); + Expression varB = new Var("b"); + Expression addition = new BinaryExpression(varA, "+", varB); + + Expression three = new LiteralInt(3); + Expression aEquals3 = new BinaryExpression(varA, "==", three); + + Expression five = new LiteralInt(5); + Expression bEquals5 = new BinaryExpression(varB, "==", five); + + Expression conditions = new BinaryExpression(aEquals3, "&&", bEquals5); + Expression fullExpression = new BinaryExpression(addition, "&&", conditions); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertEquals("8", result.getValue().toString(), "Expected result to be 8"); + + // 3 from variable a + ValDerivationNode val3 = new ValDerivationNode(new LiteralInt(3), new VarDerivationNode("a")); + + // 5 from variable b + ValDerivationNode val5 = new ValDerivationNode(new LiteralInt(5), new VarDerivationNode("b")); + + // 3 + 5 + BinaryDerivationNode add3Plus5 = new BinaryDerivationNode(val3, val5, "+"); + ValDerivationNode expected = new ValDerivationNode(new LiteralInt(8), add3Plus5); + + // Compare the derivation trees + assertDerivationEquals(expected, result, ""); + } + + @Test + void testSimpleComparison() { + // Given: (y || true) && !true && y == false + // Expected: false (true && false) + + Expression varY = new Var("y"); + Expression trueExp = new LiteralBoolean(true); + Expression yOrTrue = new BinaryExpression(varY, "||", trueExp); + + Expression notTrue = new UnaryExpression("!", trueExp); + + Expression falseExp = new LiteralBoolean(false); + Expression yEqualsFalse = new BinaryExpression(varY, "==", falseExp); + + Expression firstAnd = new BinaryExpression(yOrTrue, "&&", notTrue); + Expression fullExpression = new BinaryExpression(firstAnd, "&&", yEqualsFalse); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertTrue(result.getValue() instanceof LiteralBoolean, "Result should be a boolean"); + assertFalse(((LiteralBoolean) result.getValue()).isBooleanTrue(), "Expected result to befalse"); + + // (y || true) && y == false => false || true = true + ValDerivationNode valFalseForY = new ValDerivationNode(new LiteralBoolean(false), new VarDerivationNode("y")); + ValDerivationNode valTrue1 = new ValDerivationNode(new LiteralBoolean(true), null); + BinaryDerivationNode orFalseTrue = new BinaryDerivationNode(valFalseForY, valTrue1, "||"); + ValDerivationNode trueFromOr = new ValDerivationNode(new LiteralBoolean(true), orFalseTrue); + + // !true = false + ValDerivationNode valTrue2 = new ValDerivationNode(new LiteralBoolean(true), null); + UnaryDerivationNode notOp = new UnaryDerivationNode(valTrue2, "!"); + ValDerivationNode falseFromNot = new ValDerivationNode(new LiteralBoolean(false), notOp); + + // true && false = false + BinaryDerivationNode andTrueFalse = new BinaryDerivationNode(trueFromOr, falseFromNot, "&&"); + ValDerivationNode falseFromFirstAnd = new ValDerivationNode(new LiteralBoolean(false), andTrueFalse); + + // y == false + ValDerivationNode valFalseForY2 = new ValDerivationNode(new LiteralBoolean(false), new VarDerivationNode("y")); + ValDerivationNode valFalse2 = new ValDerivationNode(new LiteralBoolean(false), null); + BinaryDerivationNode compareFalseFalse = new BinaryDerivationNode(valFalseForY2, valFalse2, "=="); + ValDerivationNode trueFromCompare = new ValDerivationNode(new LiteralBoolean(true), compareFalseFalse); + + // false && true = false + BinaryDerivationNode finalAnd = new BinaryDerivationNode(falseFromFirstAnd, trueFromCompare, "&&"); + ValDerivationNode expected = new ValDerivationNode(new LiteralBoolean(false), finalAnd); + + // Compare the derivation trees + assertDerivationEquals(expected, result, ""); + } + + @Test + void testArithmeticWithConstants() { + // Given: (a / b + (-5)) + x && a == 6 && b == 2 + // Expected: -2 + x (6 / 2 = 3, 3 + (-5) = -2) + + Expression varA = new Var("a"); + Expression varB = new Var("b"); + Expression division = new BinaryExpression(varA, "/", varB); + + Expression five = new LiteralInt(5); + Expression negFive = new UnaryExpression("-", five); + + Expression firstSum = new BinaryExpression(division, "+", negFive); + Expression varX = new Var("x"); + Expression fullArithmetic = new BinaryExpression(firstSum, "+", varX); + + Expression six = new LiteralInt(6); + Expression aEquals6 = new BinaryExpression(varA, "==", six); + + Expression two = new LiteralInt(2); + Expression bEquals2 = new BinaryExpression(varB, "==", two); + + Expression allConditions = new BinaryExpression(aEquals6, "&&", bEquals2); + Expression fullExpression = new BinaryExpression(fullArithmetic, "&&", allConditions); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertNotNull(result.getValue(), "Result value should not be null"); + + String resultStr = result.getValue().toString(); + assertEquals("-2 + x", resultStr, "Expected result to be -2 + x"); + + // 6 from variable a + ValDerivationNode val6 = new ValDerivationNode(new LiteralInt(6), new VarDerivationNode("a")); + + // 2 from variable b + ValDerivationNode val2 = new ValDerivationNode(new LiteralInt(2), new VarDerivationNode("b")); + + // 6 / 2 = 3 + BinaryDerivationNode div6By2 = new BinaryDerivationNode(val6, val2, "/"); + ValDerivationNode val3 = new ValDerivationNode(new LiteralInt(3), div6By2); + + // -5 from unary negation of 5 + ValDerivationNode val5 = new ValDerivationNode(new LiteralInt(5), null); + UnaryDerivationNode unaryNeg5 = new UnaryDerivationNode(val5, "-"); + ValDerivationNode valNeg5 = new ValDerivationNode(new LiteralInt(-5), unaryNeg5); + + // 3 + (-5) = -2 + BinaryDerivationNode add3AndNeg5 = new BinaryDerivationNode(val3, valNeg5, "+"); + ValDerivationNode valNeg2 = new ValDerivationNode(new LiteralInt(-2), add3AndNeg5); + + // x (variable with null origin) + ValDerivationNode valX = new ValDerivationNode(new Var("x"), null); + + // -2 + x + BinaryDerivationNode addNeg2AndX = new BinaryDerivationNode(valNeg2, valX, "+"); + Expression expectedResultExpr = new BinaryExpression(new LiteralInt(-2), "+", new Var("x")); + ValDerivationNode expected = new ValDerivationNode(expectedResultExpr, addNeg2AndX); + + // Compare the derivation trees + assertDerivationEquals(expected, result, ""); + } + + @Test + void testComplexArithmeticWithMultipleOperations() { + // Given: (a * 2 + b - 3) == c && a == 5 && b == 7 && c == 14 + // Expected: (5 * 2 + 7 - 3) == 14 => 14 == 14 => true + + Expression varA = new Var("a"); + Expression varB = new Var("b"); + Expression varC = new Var("c"); + + Expression two = new LiteralInt(2); + Expression aTimes2 = new BinaryExpression(varA, "*", two); + + Expression sum = new BinaryExpression(aTimes2, "+", varB); + + Expression three = new LiteralInt(3); + Expression arithmetic = new BinaryExpression(sum, "-", three); + + Expression comparison = new BinaryExpression(arithmetic, "==", varC); + + Expression five = new LiteralInt(5); + Expression aEquals5 = new BinaryExpression(varA, "==", five); + + Expression seven = new LiteralInt(7); + Expression bEquals7 = new BinaryExpression(varB, "==", seven); + + Expression fourteen = new LiteralInt(14); + Expression cEquals14 = new BinaryExpression(varC, "==", fourteen); + + Expression conj1 = new BinaryExpression(aEquals5, "&&", bEquals7); + Expression allConditions = new BinaryExpression(conj1, "&&", cEquals14); + Expression fullExpression = new BinaryExpression(comparison, "&&", allConditions); + + // When + ValDerivationNode result = ExpressionSimplifier.simplify(fullExpression); + + // Then + assertNotNull(result, "Result should not be null"); + assertNotNull(result.getValue(), "Result value should not be null"); + assertTrue(result.getValue() instanceof LiteralBoolean, "Result should be a boolean literal"); + assertTrue(((LiteralBoolean) result.getValue()).isBooleanTrue(), "Expected result to be true"); + + // 5 * 2 + 7 - 3 + ValDerivationNode val5 = new ValDerivationNode(new LiteralInt(5), new VarDerivationNode("a")); + ValDerivationNode val2 = new ValDerivationNode(new LiteralInt(2), null); + BinaryDerivationNode mult5Times2 = new BinaryDerivationNode(val5, val2, "*"); + ValDerivationNode val10 = new ValDerivationNode(new LiteralInt(10), mult5Times2); + + ValDerivationNode val7 = new ValDerivationNode(new LiteralInt(7), new VarDerivationNode("b")); + BinaryDerivationNode add10Plus7 = new BinaryDerivationNode(val10, val7, "+"); + ValDerivationNode val17 = new ValDerivationNode(new LiteralInt(17), add10Plus7); + + ValDerivationNode val3 = new ValDerivationNode(new LiteralInt(3), null); + BinaryDerivationNode sub17Minus3 = new BinaryDerivationNode(val17, val3, "-"); + ValDerivationNode val14Left = new ValDerivationNode(new LiteralInt(14), sub17Minus3); + + // 14 from variable c + ValDerivationNode val14Right = new ValDerivationNode(new LiteralInt(14), new VarDerivationNode("c")); + + // 14 == 14 + BinaryDerivationNode compare14 = new BinaryDerivationNode(val14Left, val14Right, "=="); + ValDerivationNode trueFromComparison = new ValDerivationNode(new LiteralBoolean(true), compare14); + + // a == 5 => true + ValDerivationNode val5ForCompA = new ValDerivationNode(new LiteralInt(5), new VarDerivationNode("a")); + ValDerivationNode val5Literal = new ValDerivationNode(new LiteralInt(5), null); + BinaryDerivationNode compareA5 = new BinaryDerivationNode(val5ForCompA, val5Literal, "=="); + ValDerivationNode trueFromA = new ValDerivationNode(new LiteralBoolean(true), compareA5); + + // b == 7 => true + ValDerivationNode val7ForCompB = new ValDerivationNode(new LiteralInt(7), new VarDerivationNode("b")); + ValDerivationNode val7Literal = new ValDerivationNode(new LiteralInt(7), null); + BinaryDerivationNode compareB7 = new BinaryDerivationNode(val7ForCompB, val7Literal, "=="); + ValDerivationNode trueFromB = new ValDerivationNode(new LiteralBoolean(true), compareB7); + + // (a == 5) && (b == 7) => true + BinaryDerivationNode andAB = new BinaryDerivationNode(trueFromA, trueFromB, "&&"); + ValDerivationNode trueFromAB = new ValDerivationNode(new LiteralBoolean(true), andAB); + + // c == 14 => true + ValDerivationNode val14ForCompC = new ValDerivationNode(new LiteralInt(14), new VarDerivationNode("c")); + ValDerivationNode val14Literal = new ValDerivationNode(new LiteralInt(14), null); + BinaryDerivationNode compareC14 = new BinaryDerivationNode(val14ForCompC, val14Literal, "=="); + ValDerivationNode trueFromC = new ValDerivationNode(new LiteralBoolean(true), compareC14); + + // ((a == 5) && (b == 7)) && (c == 14) => true + BinaryDerivationNode andABC = new BinaryDerivationNode(trueFromAB, trueFromC, "&&"); + ValDerivationNode trueFromAllConditions = new ValDerivationNode(new LiteralBoolean(true), andABC); + + // 14 == 14 => true + BinaryDerivationNode finalAnd = new BinaryDerivationNode(trueFromComparison, trueFromAllConditions, "&&"); + ValDerivationNode expected = new ValDerivationNode(new LiteralBoolean(true), finalAnd); + + // Compare the derivation trees + assertDerivationEquals(expected, result, ""); + } + + /** + * Helper method to compare two derivation nodes recursively + */ + private void assertDerivationEquals(DerivationNode expected, DerivationNode actual, String message) { + if (expected == null && actual == null) + return; + + assertEquals(expected.getClass(), actual.getClass(), message + ": node types should match"); + if (expected instanceof ValDerivationNode) { + ValDerivationNode expectedVal = (ValDerivationNode) expected; + ValDerivationNode actualVal = (ValDerivationNode) actual; + assertEquals(expectedVal.getValue().toString(), actualVal.getValue().toString(), + message + ": values should match"); + assertDerivationEquals(expectedVal.getOrigin(), actualVal.getOrigin(), message + " > origin"); + } else if (expected instanceof BinaryDerivationNode) { + BinaryDerivationNode expectedBin = (BinaryDerivationNode) expected; + BinaryDerivationNode actualBin = (BinaryDerivationNode) actual; + assertEquals(expectedBin.getOp(), actualBin.getOp(), message + ": operators should match"); + assertDerivationEquals(expectedBin.getLeft(), actualBin.getLeft(), message + " > left"); + assertDerivationEquals(expectedBin.getRight(), actualBin.getRight(), message + " > right"); + } else if (expected instanceof VarDerivationNode) { + VarDerivationNode expectedVar = (VarDerivationNode) expected; + VarDerivationNode actualVar = (VarDerivationNode) actual; + assertEquals(expectedVar.getVar(), actualVar.getVar(), message + ": variables should match"); + } else if (expected instanceof UnaryDerivationNode) { + UnaryDerivationNode expectedUnary = (UnaryDerivationNode) expected; + UnaryDerivationNode actualUnary = (UnaryDerivationNode) actual; + assertEquals(expectedUnary.getOperator(), actualUnary.getOperator(), message + ": operators should match"); + assertDerivationEquals(expectedUnary.getOperand(), actualUnary.getOperand(), message + " > operand"); + } + } +} From 88e063c53aaf531dc750f47a408508e146c46e14 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 7 Oct 2025 10:46:07 +0100 Subject: [PATCH 10/12] Renamed printCostumeError to printCustomError --- .../java/liquidjava/errors/ErrorHandler.java | 46 +++++++++---------- .../ExternalRefinementTypeChecker.java | 3 +- .../refinement_checker/TypeChecker.java | 11 ++--- .../refinement_checker/VCChecker.java | 2 +- .../object_checkers/AuxStateHandler.java | 2 +- 5 files changed, 31 insertions(+), 33 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java index 7e45622a..91ab4987 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java @@ -26,7 +26,7 @@ public static void printError(CtElement var, Predicate expectedType, Predica } public static void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT, - HashMap map, ErrorEmitter errorl) { + HashMap map, ErrorEmitter ee) { String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" + // cSMT.toString(); @@ -41,16 +41,16 @@ public static void printError(CtElement var, String moreInfo, Predicate expe // all message sb.append(sbtitle.toString() + "\n\n"); sb.append("Type expected:" + expectedType.toString() + "\n"); - sb.append("Refinement found:\n" + cSMT.simplify().getValue() + "\n"); + sb.append("Refinement found: " + cSMT.simplify().getValue() + "\n"); sb.append(printMap(map)); sb.append("Location: " + var.getPosition() + "\n"); sb.append("______________________________________________________\n"); - errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map); + ee.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map); } public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg, - String states, HashMap map, ErrorEmitter errorl) { + String states, HashMap map, ErrorEmitter ee) { String resumeMessage = "Failed to check state transitions. " + "Expected possible states:" + states; // + "; // Found @@ -75,11 +75,11 @@ public static void printStateMismatch(CtElement element, String method, VCImplic sb.append("Location: " + element.getPosition() + "\n"); sb.append("______________________________________________________\n"); - errorl.addError(resumeMessage, sb.toString(), element.getPosition(), 1, map); + ee.addError(resumeMessage, sb.toString(), element.getPosition(), 1, map); } public static void printErrorUnknownVariable(CtElement var, String et, String correctRefinement, - HashMap map, ErrorEmitter errorl) { + HashMap map, ErrorEmitter ee) { String resumeMessage = "Encountered unknown variable"; @@ -94,11 +94,11 @@ public static void printErrorUnknownVariable(CtElement var, String et, Strin sb.append("Location: " + var.getPosition() + "\n"); sb.append("______________________________________________________\n"); - errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 2, map); + ee.addError(resumeMessage, sb.toString(), var.getPosition(), 2, map); } public static void printNotFound(CtElement var, Predicate constraint, Predicate constraint2, String msg, - HashMap map, ErrorEmitter errorl) { + HashMap map, ErrorEmitter ee) { StringBuilder sb = new StringBuilder(); sb.append("______________________________________________________\n"); @@ -111,11 +111,11 @@ public static void printNotFound(CtElement var, Predicate constraint, Predic sb.append("Location: " + var.getPosition() + "\n"); sb.append("______________________________________________________\n"); - errorl.addError(msg, sb.toString(), var.getPosition(), 2, map); + ee.addError(msg, sb.toString(), var.getPosition(), 2, map); } public static void printErrorArgs(CtElement var, Predicate expectedType, String msg, - HashMap map, ErrorEmitter errorl) { + HashMap map, ErrorEmitter ee) { StringBuilder sb = new StringBuilder(); sb.append("______________________________________________________\n"); String title = "Error in ghost invocation: " + msg + "\n"; @@ -125,11 +125,11 @@ public static void printErrorArgs(CtElement var, Predicate expectedType, Str sb.append("Location: " + var.getPosition() + "\n"); sb.append("______________________________________________________\n"); - errorl.addError(title, sb.toString(), var.getPosition(), 2, map); + ee.addError(title, sb.toString(), var.getPosition(), 2, map); } public static void printErrorTypeMismatch(CtElement element, Predicate expectedType, String message, - HashMap map, ErrorEmitter errorl) { + HashMap map, ErrorEmitter ee) { StringBuilder sb = new StringBuilder(); sb.append("______________________________________________________\n"); sb.append(message + "\n\n"); @@ -138,11 +138,11 @@ public static void printErrorTypeMismatch(CtElement element, Predicate expectedT sb.append("Location: " + element.getPosition() + "\n"); sb.append("______________________________________________________\n"); - errorl.addError(message, sb.toString(), element.getPosition(), 2, map); + ee.addError(message, sb.toString(), element.getPosition(), 2, map); } public static void printSameStateSetError(CtElement element, Predicate p, String name, - HashMap map, ErrorEmitter errorl) { + HashMap map, ErrorEmitter ee) { String resume = "Error found multiple disjoint states from a State Set in a refinement"; StringBuilder sb = new StringBuilder(); @@ -157,10 +157,10 @@ public static void printSameStateSetError(CtElement element, Predicate p, String sb.append("Location: " + element.getPosition() + "\n"); sb.append("______________________________________________________\n"); - errorl.addError(resume, sb.toString(), element.getPosition(), 1, map); + ee.addError(resume, sb.toString(), element.getPosition(), 1, map); } - public static void printErrorConstructorFromState(CtElement element, CtLiteral from, ErrorEmitter errorl) { + public static void printErrorConstructorFromState(CtElement element, CtLiteral from, ErrorEmitter ee) { StringBuilder sb = new StringBuilder(); sb.append("______________________________________________________\n"); String s = " Error found constructor with FROM state (Constructor's should only have a TO state)\n\n"; @@ -170,10 +170,10 @@ public static void printErrorConstructorFromState(CtElement element, CtLiteral e, int set, CtElement element) { CtLiteral s = (CtLiteral) ce; String f = s.getValue(); if (Character.isUpperCase(f.charAt(0))) { - ErrorHandler.printCostumeError(s, "State name must start with lowercase in '" + f + "'", + ErrorHandler.printCustomError(s, "State name must start with lowercase in '" + f + "'", errorEmitter); } } @@ -161,11 +161,11 @@ private void createStateGhost(String string, CtAnnotation try { gd = RefinementsParser.getGhostDeclaration(string); } catch (ParsingException e) { - ErrorHandler.printCostumeError(ann, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter); + ErrorHandler.printCustomError(ann, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter); return; } if (gd.getParam_types().size() > 0) { - ErrorHandler.printCostumeError(ann, "Ghost States have the class as parameter " + ErrorHandler.printCustomError(ann, "Ghost States have the class as parameter " + "by default, no other parameters are allowed in '" + string + "'", errorEmitter); return; } @@ -224,8 +224,7 @@ protected void getGhostFunction(String value, CtElement element) { context.addGhostFunction(gh); } } catch (ParsingException e) { - ErrorHandler.printCostumeError(element, "Could not parse the Ghost Function" + e.getMessage(), - errorEmitter); + ErrorHandler.printCustomError(element, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter); // e.printStackTrace(); return; } @@ -252,7 +251,7 @@ protected void handleAlias(String value, CtElement element) { } } } catch (ParsingException e) { - ErrorHandler.printCostumeError(element, e.getMessage(), errorEmitter); + ErrorHandler.printCustomError(element, e.getMessage(), errorEmitter); return; // e.printStackTrace(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 82cbf15d..458ae4da 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -364,7 +364,7 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e } else if (e instanceof NotFoundError) { ErrorHandler.printNotFound(element, cSMTMessageReady, etMessageReady, e.getMessage(), map, errorEmitter); } else { - ErrorHandler.printCostumeError(element, e.getMessage(), errorEmitter); + ErrorHandler.printCustomError(element, e.getMessage(), errorEmitter); // System.err.println("Unknown error:"+e.getMessage()); // e.printStackTrace(); // System.exit(7); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 46eb254f..182285d9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -369,7 +369,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { stateChange.setTo(toPredicate); } catch (ParsingException e) { ErrorHandler - .printCostumeError(fw, + .printCustomError(fw, "ParsingException while constructing assignment update for `" + fw + "` in class `" + fw.getVariable().getDeclaringType() + "` : " + e.getMessage(), tc.getErrorEmitter()); From 893b1e0b728a6640b4dc100a3d61d092d20883aa Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 7 Oct 2025 11:07:21 +0100 Subject: [PATCH 11/12] DerivationNode JSON Serialization Using Gson --- liquidjava-verifier/pom.xml | 5 ++ .../derivation_node/BinaryDerivationNode.java | 15 +----- .../opt/derivation_node/DerivationNode.java | 41 ++++------------- .../derivation_node/UnaryDerivationNode.java | 21 ++------- .../derivation_node/ValDerivationNode.java | 46 ++++++++++--------- .../derivation_node/VarDerivationNode.java | 10 ---- .../opt/ExpressionSimplifierTest.java | 2 +- 7 files changed, 44 insertions(+), 96 deletions(-) diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 21464fa3..46a4972d 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -188,6 +188,11 @@ antlr4-runtime 4.7.1 + + com.google.code.gson + gson + 2.10.1 + diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java index dbe24e8d..8c30a802 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java @@ -1,12 +1,10 @@ package liquidjava.rj_language.opt.derivation_node; -import java.util.Map; - public class BinaryDerivationNode extends DerivationNode { + private final String op; private final ValDerivationNode left; private final ValDerivationNode right; - private final String op; public BinaryDerivationNode(ValDerivationNode left, ValDerivationNode right, String op) { this.left = left; @@ -25,15 +23,4 @@ public ValDerivationNode getRight() { public String getOp() { return op; } - - @Override - public Map toJson() { - Map json = baseJson(); - json.put("op", op); - if (left != null) - json.put("left", left.toJson()); - if (right != null) - json.put("right", right.toJson()); - return json; - } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java index 9b6cb0da..7acc8e72 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java @@ -1,42 +1,17 @@ package liquidjava.rj_language.opt.derivation_node; -import java.util.LinkedHashMap; -import java.util.Map; +import com.google.gson.Gson; +import com.google.gson.GsonBuilder; public abstract class DerivationNode { + private static final Gson gson = new GsonBuilder() + .setPrettyPrinting() // remove later + .disableHtmlEscaping() // to not escape characters like &, >, <, =, etc. + .create(); + @Override public String toString() { - return prettyPrint(toJson(), ""); - } - - private String prettyPrint(Map json, String indent) { - StringBuilder sb = new StringBuilder(); - String nextIndent = indent + " "; - sb.append("{\n"); - for (String key : json.keySet()) { - sb.append(nextIndent + "\"" + key + "\": "); - Object value = json.get(key); - if (value instanceof Map) { - sb.append(prettyPrint((Map) value, nextIndent)); - } else if (value instanceof String) { - sb.append("\"" + value + "\""); - } else { - sb.append(value); - } - sb.append(",\n"); - } - if (json.size() > 0) { - sb.setLength(sb.length() - 2); // remove last comma - sb.append("\n"); - } - sb.append(indent + "}"); - return sb.toString(); - } - - public abstract Map toJson(); - - protected Map baseJson() { - return new LinkedHashMap<>(); + return gson.toJson(this); } } \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java index e1286369..f0693dc3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java @@ -1,31 +1,20 @@ package liquidjava.rj_language.opt.derivation_node; -import java.util.Map; - public class UnaryDerivationNode extends DerivationNode { + private final String op; private final ValDerivationNode operand; - private final String operator; - public UnaryDerivationNode(ValDerivationNode operand, String operator) { + public UnaryDerivationNode(ValDerivationNode operand, String op) { this.operand = operand; - this.operator = operator; + this.op = op; } public ValDerivationNode getOperand() { return operand; } - public String getOperator() { - return operator; - } - - @Override - public Map toJson() { - Map json = baseJson(); - json.put("op", operator); - if (operand != null) - json.put("operand", operand.toJson()); - return json; + public String getOp() { + return op; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java index b96f2e95..07ac9b0f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java @@ -1,6 +1,13 @@ package liquidjava.rj_language.opt.derivation_node; -import java.util.Map; +import java.lang.reflect.Type; + +import com.google.gson.JsonElement; +import com.google.gson.JsonNull; +import com.google.gson.JsonPrimitive; +import com.google.gson.JsonSerializationContext; +import com.google.gson.JsonSerializer; +import com.google.gson.annotations.JsonAdapter; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.LiteralBoolean; @@ -10,6 +17,7 @@ public class ValDerivationNode extends DerivationNode { + @JsonAdapter(ExpressionSerializer.class) private final Expression value; private final DerivationNode origin; @@ -26,26 +34,20 @@ public DerivationNode getOrigin() { return origin; } - @Override - public Map toJson() { - Map json = baseJson(); - json.put("value", expToValue(value)); - if (origin != null) - json.put("origin", origin.toJson()); - return json; - } - - private Object expToValue(Expression exp) { - if (exp == null) - return null; - if (exp instanceof LiteralInt) - return ((LiteralInt) exp).getValue(); - if (exp instanceof LiteralReal) - return ((LiteralReal) exp).getValue(); - if (exp instanceof LiteralBoolean) - return ((LiteralBoolean) exp).isBooleanTrue(); - if (exp instanceof Var) - return ((Var) exp).getName(); - return exp.toString(); + private static class ExpressionSerializer implements JsonSerializer { + @Override + public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationContext context) { + if (exp == null) + return JsonNull.INSTANCE; + if (exp instanceof LiteralInt) + return new JsonPrimitive(((LiteralInt) exp).getValue()); + if (exp instanceof LiteralReal) + return new JsonPrimitive(((LiteralReal) exp).getValue()); + if (exp instanceof LiteralBoolean) + return new JsonPrimitive(((LiteralBoolean) exp).isBooleanTrue()); + if (exp instanceof Var) + return new JsonPrimitive(((Var) exp).getName()); + return new JsonPrimitive(exp.toString()); + } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java index 619abb54..1c044f52 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java @@ -1,7 +1,5 @@ package liquidjava.rj_language.opt.derivation_node; -import java.util.Map; - public class VarDerivationNode extends DerivationNode { private final String var; @@ -13,12 +11,4 @@ public VarDerivationNode(String var) { public String getVar() { return var; } - - @Override - public Map toJson() { - Map json = baseJson(); - if (var != null) - json.put("var", var); - return json; - } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java index dbf89b8b..d1629682 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java @@ -331,7 +331,7 @@ private void assertDerivationEquals(DerivationNode expected, DerivationNode actu } else if (expected instanceof UnaryDerivationNode) { UnaryDerivationNode expectedUnary = (UnaryDerivationNode) expected; UnaryDerivationNode actualUnary = (UnaryDerivationNode) actual; - assertEquals(expectedUnary.getOperator(), actualUnary.getOperator(), message + ": operators should match"); + assertEquals(expectedUnary.getOp(), actualUnary.getOp(), message + ": operators should match"); assertDerivationEquals(expectedUnary.getOperand(), actualUnary.getOperand(), message + " > operand"); } } From 15089853b997b87833b224064d4a09e241a67db7 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 7 Oct 2025 11:28:19 +0100 Subject: [PATCH 12/12] Add Documentation to Methods --- .../rj_language/opt/ConstantFolding.java | 18 ++++++++++++++---- .../rj_language/opt/ConstantPropagation.java | 8 ++++++++ .../rj_language/opt/ExpressionSimplifier.java | 8 ++++++-- .../rj_language/opt/VariableResolver.java | 19 ++++++++++++++++--- .../opt/derivation_node/DerivationNode.java | 6 ++---- .../derivation_node/ValDerivationNode.java | 1 + 6 files changed, 47 insertions(+), 13 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java index e29f3bb3..0d5fe242 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java @@ -14,14 +14,18 @@ public class ConstantFolding { + /** + * Performs constant folding on a derivation node by evaluating nodes with constant values. Returns a new derivation + * node representing the folding steps taken + */ public static ValDerivationNode fold(ValDerivationNode node) { Expression exp = node.getValue(); - if (exp instanceof BinaryExpression) { + if (exp instanceof BinaryExpression) return foldBinary(node); - } - if (exp instanceof UnaryExpression) { + + if (exp instanceof UnaryExpression) return foldUnary(node); - } + if (exp instanceof GroupExpression) { GroupExpression group = (GroupExpression) exp; if (group.getChildren().size() == 1) { @@ -31,6 +35,9 @@ public static ValDerivationNode fold(ValDerivationNode node) { return node; } + /** + * Folds a binary expression node if both children are constant values (e.g. 1 + 2 => 3) + */ private static ValDerivationNode foldBinary(ValDerivationNode node) { BinaryExpression binExp = (BinaryExpression) node.getValue(); DerivationNode parent = node.getOrigin(); @@ -142,6 +149,9 @@ else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) { return new ValDerivationNode(binExp, origin); } + /** + * Folds a unary expression node if the child (operand) is a constant value (e.g. !true => false) + */ private static ValDerivationNode foldUnary(ValDerivationNode node) { UnaryExpression unaryExp = (UnaryExpression) node.getValue(); DerivationNode parent = node.getOrigin(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java index 934a6570..a72a9b33 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java @@ -14,11 +14,19 @@ public class ConstantPropagation { + /** + * Performs constant propagation on an expression, by substituting variables with their constant values. Uses the + * VariableResolver to extract variable equalities from the expression first. Returns a derivation node representing + * the propagation steps taken. + */ public static ValDerivationNode propagate(Expression exp) { Map substitutions = VariableResolver.resolve(exp); return propagateRecursive(exp, substitutions); } + /** + * Recursively performs constant propagation on an expression (e.g. x + y && x == 1 && y == 2 => 1 + 2) + */ private static ValDerivationNode propagateRecursive(Expression exp, Map subs) { // substitute variable diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java index 1400e5ad..2a022b81 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java @@ -9,6 +9,10 @@ public class ExpressionSimplifier { + /** + * Simplifies an expression by applying constant propagation, constant folding and removing redundant conjuncts + * Returns a derivation node representing the tree of simplifications applied + */ public static ValDerivationNode simplify(Expression exp) { ValDerivationNode prop = ConstantPropagation.propagate(exp); ValDerivationNode fold = ConstantFolding.fold(prop); @@ -16,7 +20,7 @@ public static ValDerivationNode simplify(Expression exp) { } /** - * Recursively simplify the derivation tree by removing redundant conjuncts + * Recursively simplifies the derivation tree by removing redundant conjuncts */ private static ValDerivationNode simplifyDerivationTree(ValDerivationNode node) { Expression value = node.getValue(); @@ -49,7 +53,7 @@ private static ValDerivationNode simplifyDerivationTree(ValDerivationNode node) } /** - * Check if an expression is redundant + * Checks if an expression is redundant (e.g. true or x == x) */ private static boolean isRedundant(Expression exp) { // true diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java index bb978a3b..2ac6d210 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java @@ -11,12 +11,19 @@ public class VariableResolver { + /** + * Extracts variables with constant values from an expression Returns a map from variable names to their values + */ public static Map resolve(Expression exp) { Map map = new HashMap<>(); resolveRecursive(exp, map); return resolveTransitive(map); } + /** + * Recursively extracts variable equalities from an expression (e.g. ... && x == 1 && y == 2 => map: x -> 1, y -> 2) + * Modifies the given map in place + */ private static void resolveRecursive(Expression exp, Map map) { if (!(exp instanceof BinaryExpression)) return; @@ -30,14 +37,16 @@ private static void resolveRecursive(Expression exp, Map map Expression left = be.getFirstOperand(); Expression right = be.getSecondOperand(); if (left instanceof Var && (right.isLiteral() || right instanceof Var)) { - map.put(left.toString(), right.clone()); + map.put(((Var) left).getName(), right.clone()); } else if (right instanceof Var && left.isLiteral()) { - map.put(right.toString(), left.clone()); + map.put(((Var) right).getName(), left.clone()); } } } - // e.g. x == y && y == 1 => x == 1 + /** + * Handles transitive variable equalities in the map (e.g. map: x -> y, y -> 1 => map: x -> 1, y -> 1) + */ private static Map resolveTransitive(Map map) { Map result = new HashMap<>(); for (Map.Entry entry : map.entrySet()) { @@ -46,6 +55,10 @@ private static Map resolveTransitive(Map return result; } + /** + * Returns the value of a variable by looking up in the map recursively Uses the seen set to avoid circular + * references (e.g. x -> y, y -> x) which would cause infinite recursion + */ private static Expression lookup(Expression exp, Map map, Set seen) { if (!(exp instanceof Var)) return exp; diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java index 7acc8e72..a6b08e54 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java @@ -5,10 +5,8 @@ public abstract class DerivationNode { - private static final Gson gson = new GsonBuilder() - .setPrettyPrinting() // remove later - .disableHtmlEscaping() // to not escape characters like &, >, <, =, etc. - .create(); + // disable html escaping to avoid escaping characters like &, >, <, =, etc. + private static final Gson gson = new GsonBuilder().setPrettyPrinting().disableHtmlEscaping().create(); @Override public String toString() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java index 07ac9b0f..eeb6f21d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java @@ -34,6 +34,7 @@ public DerivationNode getOrigin() { return origin; } + // Custom serializer to handle Expression subclasses properly private static class ExpressionSerializer implements JsonSerializer { @Override public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationContext context) {