diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 6e717e80f..ce98d2738 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -37,9 +37,8 @@ To run specific tests, run: ```bash mvn -pl liquidjava-verifier -Dtest=ExpressionFormatterTest test -mvn -pl liquidjava-verifier -Dtest=ExpressionSimplifierTest test mvn -pl liquidjava-verifier -Dtest=RefinementsParserTest test -mvn -pl liquidjava-verifier -Dtest=VariableResolverTest test +mvn -pl liquidjava-verifier -Dtest=VCSimplificationTest test ``` ## Release diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java index 0adcccd60..02c407939 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -56,7 +56,7 @@ public static void smtVerifying(SourcePosition position) { /** * Flat-predicate fallback: prints top-level conjuncts in order with no per-variable grouping. Used by SMT entry - * points that don't carry the structured per-variable {@link VCImplication} chain (e.g. ExpressionSimplifier). + * points that don't carry the structured per-variable {@link VCImplication} chain. */ public static void smtStart(Predicate premises, Predicate conclusion) { if (!enabled()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 3095bb91b..e56ce3c82 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -5,9 +5,10 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.TranslationTable; +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.formatter.VariableFormatter; -import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.smt.Counterexample; import spoon.reflect.cu.SourcePosition; @@ -18,14 +19,15 @@ */ public class RefinementError extends LJError { - private final ValDerivationNode expected; - private final ValDerivationNode found; + private final Predicate expected; + private final VCImplication found; private final Counterexample counterexample; - public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found, + public RefinementError(SourcePosition position, Predicate expected, VCImplication found, TranslationTable translationTable, Counterexample counterexample, String customMessage) { - super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue().toDisplayString(), - expected.getValue().toDisplayString()), position, translationTable, customMessage); + super("Refinement Error", String.format("%s is not a subtype of %s", + found.toPredicate().getExpression().toDisplayString(), expected.getExpression().toDisplayString()), + position, translationTable, customMessage); this.expected = expected; this.found = found; this.counterexample = counterexample; @@ -44,12 +46,14 @@ public String getCounterExampleString() { return null; List foundVarNames = new ArrayList<>(); - found.getValue().getVariableNames(foundVarNames); + Expression foundExpression = found.toPredicate().getExpression(); + Expression expectedExpression = expected.getExpression(); + foundExpression.getVariableNames(foundVarNames); // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the // subtyping check, so the counterexample maps the symbolic name back to its compile-time value - found.getValue().getResolvedConstantNames(foundVarNames); - expected.getValue().getResolvedConstantNames(foundVarNames); - List foundAssignments = found.getValue().getConjuncts().stream().map(Expression::toString).toList(); + foundExpression.getResolvedConstantNames(foundVarNames); + expectedExpression.getResolvedConstantNames(foundVarNames); + List foundAssignments = foundExpression.getConjuncts().stream().map(Expression::toString).toList(); String counterexampleString = counterexample.assignments().stream() // only include variables that appear in the found value and are not already fixed there .filter(a -> foundVarNames.contains(a.first()) @@ -69,11 +73,11 @@ public Counterexample getCounterexample() { return counterexample; } - public ValDerivationNode getExpected() { + public Predicate getExpected() { return expected; } - public ValDerivationNode getFound() { + public VCImplication getFound() { return found; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index c2055954a..874ccd921 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -1,7 +1,8 @@ package liquidjava.diagnostics.errors; import liquidjava.diagnostics.TranslationTable; -import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; import spoon.reflect.cu.SourcePosition; /** @@ -11,23 +12,24 @@ */ public class StateRefinementError extends LJError { - private final ValDerivationNode expected; - private final ValDerivationNode found; + private final Predicate expected; + private final VCImplication found; - public StateRefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found, + public StateRefinementError(SourcePosition position, Predicate expected, VCImplication found, TranslationTable translationTable, String customMessage) { - super("State Refinement Error", String.format("Expected state %s but found %s", - expected.getValue().toDisplayString(), found.getValue().toDisplayString()), position, translationTable, - customMessage); + super("State Refinement Error", + String.format("Expected state %s but found %s", expected.getExpression().toDisplayString(), + found.toPredicate().getExpression().toDisplayString()), + position, translationTable, customMessage); this.expected = expected; this.found = found; } - public ValDerivationNode getExpected() { + public Predicate getExpected() { return expected; } - public ValDerivationNode getFound() { + public VCImplication getFound() { return found; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index 4a5541f86..2130ee186 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -93,6 +93,10 @@ public VCImplication simplify() { return VCSimplification.simplifyToFixedPoint(this); } + public Predicate toPredicate() { + return hasBinder() || hasNext() ? toConjunctions() : refinement; + } + public Predicate toConjunctions() { Predicate c = new Predicate(); if (name == null && type == null && next == null) 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 228a318a6..d2ba3cc17 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 @@ -53,6 +53,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl TranslationTable map = new TranslationTable(); String[] s = { Keys.WILDCARD, Keys.THIS }; VCImplication impl = joinPredicates(expectedType, mainVars, lrv, map); + VCImplication implBeforeChange = impl.clone(); Predicate premisesBeforeChange = impl.toConjunctions(); Predicate premises; Predicate expected; @@ -81,8 +82,8 @@ public void processSubtyping(Predicate expectedType, List list, CtEl } DebugLog.smtResult(result); if (result.isError()) { - throw new RefinementError(element.getPosition(), expectedType.simplify(context), - premisesBeforeChange.simplify(context), map, result.getCounterexample(), customMessage); + throw new RefinementError(element.getPosition(), expectedType, implBeforeChange.simplify(), map, + result.getCounterexample(), customMessage); } } @@ -405,17 +406,15 @@ private VCImplication buildPremiseChain(TranslationTable map, Predicate... predi protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found, Counterexample counterexample, String customMessage) throws RefinementError { TranslationTable map = new TranslationTable(); - Predicate premises = buildPremiseChain(map, expected, found).toConjunctions(); - throw new RefinementError(position, expected.simplify(context), premises.simplify(context), map, counterexample, - customMessage); + VCImplication premises = buildPremiseChain(map, expected, found); + throw new RefinementError(position, expected, premises.simplify(), map, counterexample, customMessage); } protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected, String customMessage) throws StateRefinementError { TranslationTable map = new TranslationTable(); VCImplication foundState = buildPremiseChain(map, expected, found); - throw new StateRefinementError(position, expected.simplify(context), - foundState.toConjunctions().simplify(context), map, customMessage); + throw new StateRefinementError(position, expected, foundState.simplify(), map, customMessage); } protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError { 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 e6a4f04fb..303551cfa 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -9,6 +9,7 @@ import liquidjava.diagnostics.DebugLog; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.NotFoundError; +import liquidjava.processor.VCImplication; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; @@ -27,10 +28,8 @@ import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; -import liquidjava.utils.StaticConstants; -import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; -import liquidjava.rj_language.opt.ExpressionSimplifier; import liquidjava.rj_language.parsing.RefinementsParser; +import liquidjava.utils.StaticConstants; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; import liquidjava.utils.constants.Ops; @@ -260,15 +259,9 @@ public Predicate getOrigin() { return this; } - public ValDerivationNode simplify(Context context) { - // collect aliases from context - Map aliases = new HashMap<>(); - for (AliasWrapper aw : context.getAliases()) { - aliases.put(aw.getName(), aw.createAliasDTO()); - } - // simplify expression - ValDerivationNode result = ExpressionSimplifier.simplify(exp.clone(), aliases); - DebugLog.simplification(this.getExpression(), result.getValue()); + public VCImplication simplify() { + VCImplication result = new VCImplication(clone()).simplify(); + DebugLog.simplification(this.getExpression(), result.getRefinement().getExpression()); return result; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AliasExpansion.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AliasExpansion.java deleted file mode 100644 index b8ab6b3fa..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/AliasExpansion.java +++ /dev/null @@ -1,91 +0,0 @@ -package liquidjava.rj_language.opt; - -import java.util.Map; - -import liquidjava.processor.facade.AliasDTO; -import liquidjava.rj_language.ast.AliasInvocation; -import liquidjava.rj_language.ast.BinaryExpression; -import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.GroupExpression; -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; - -public class AliasExpansion { - - /** - * Expands alias invocations in a derivation node to their definitions, storing the expanded body as the origin of - * each alias invocation node. - */ - public static ValDerivationNode expand(ValDerivationNode node, Map aliases) { - return expandRecursive(node, aliases); - } - - private static ValDerivationNode expandRecursive(ValDerivationNode node, Map aliases) { - Expression exp = node.getValue(); - - // expand alias invocation - if (exp instanceof AliasInvocation ai) { - return expandAlias(ai, aliases); - } - - // recurse into binary expressions - if (exp instanceof BinaryExpression binary) { - ValDerivationNode leftNode; - ValDerivationNode rightNode; - if (node.getOrigin()instanceof BinaryDerivationNode binOrigin) { - leftNode = expandRecursive(binOrigin.getLeft(), aliases); - rightNode = expandRecursive(binOrigin.getRight(), aliases); - } else { - leftNode = expandRecursive(new ValDerivationNode(binary.getFirstOperand(), null), aliases); - rightNode = expandRecursive(new ValDerivationNode(binary.getSecondOperand(), null), aliases); - } - boolean hasExpansion = leftNode.getOrigin() != null || rightNode.getOrigin() != null; - DerivationNode origin = hasExpansion ? new BinaryDerivationNode(leftNode, rightNode, binary.getOperator()) - : node.getOrigin(); - return new ValDerivationNode(exp, origin); - } - - // recurse into unary expressions - if (exp instanceof UnaryExpression unary) { - ValDerivationNode operandNode; - if (node.getOrigin()instanceof UnaryDerivationNode unaryOrigin) { - operandNode = expandRecursive(unaryOrigin.getOperand(), aliases); - } else { - operandNode = expandRecursive(new ValDerivationNode(unary.getChildren().get(0), null), aliases); - } - DerivationNode origin = operandNode.getOrigin() != null - ? new UnaryDerivationNode(operandNode, unary.getOp()) : node.getOrigin(); - return new ValDerivationNode(exp, origin); - } - - // recurse into group expressions - if (exp instanceof GroupExpression group && group.getChildren().size() == 1) { - return expandRecursive(new ValDerivationNode(group.getChildren().get(0), node.getOrigin()), aliases); - } - - return node; - } - - private static ValDerivationNode expandAlias(AliasInvocation ai, Map aliases) { - AliasDTO dto = aliases.get(ai.getName()); - - // no alias found - if (dto == null || dto.getExpression() == null) { - return new ValDerivationNode(ai, null); - } - - // substitute parameters in the body with the invocation arguments - Expression body = dto.getExpression().clone(); - for (int i = 0; i < ai.getArgs().size() && i < dto.getVarNames().size(); i++) { - body = body.substitute(new Var(dto.getVarNames().get(i)), ai.getArgs().get(i)); - } - - // recursively expand the body - ValDerivationNode expandedBody = expandRecursive(new ValDerivationNode(body, null), aliases); - return new ValDerivationNode(ai, expandedBody); - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionFolding.java deleted file mode 100644 index 482a9948d..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionFolding.java +++ /dev/null @@ -1,301 +0,0 @@ -package liquidjava.rj_language.opt; - -import liquidjava.rj_language.ast.BinaryExpression; -import liquidjava.rj_language.ast.Enum; -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; -import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode; -import liquidjava.rj_language.opt.derivation_node.DerivationNode; -import liquidjava.rj_language.opt.derivation_node.IteDerivationNode; -import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode; -import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; - -public class ExpressionFolding { - - /** - * Performs expression folding on a derivation node by evaluating nodes when possible. Returns a new derivation node - * representing the folding steps taken - */ - public static ValDerivationNode fold(ValDerivationNode node) { - Expression exp = node.getValue(); - if (exp instanceof BinaryExpression) - return foldBinary(node); - - if (exp instanceof UnaryExpression) - return foldUnary(node); - - if (exp instanceof Ite) - return foldIte(node); - - if (exp instanceof GroupExpression group) { - if (group.getChildren().size() == 1) { - return fold(new ValDerivationNode(group.getChildren().get(0), node.getOrigin())); - } - } - return node; - } - - /** - * Folds a binary expression node (e.g. 1 + 2 => 3) - */ - 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 binaryOrigin) { - // has origin (from constant propagation) - 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(); - - if (left instanceof Enum en && en.getResolvedLiteral() != null) { - left = en.getResolvedLiteral().clone(); - leftNode = new ValDerivationNode(left, leftNode); - } - if (right instanceof Enum en && en.getResolvedLiteral() != null) { - right = en.getResolvedLiteral().clone(); - rightNode = new ValDerivationNode(right, rightNode); - } - - binExp.setChild(0, left); - binExp.setChild(1, right); - - // int and int - if (left instanceof LiteralInt && right instanceof LiteralInt) { - int l = ((LiteralInt) left).getValue(); - int r = ((LiteralInt) right).getValue(); - 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)); - } - // real and real - else if (left instanceof LiteralReal && right instanceof LiteralReal) { - double l = ((LiteralReal) left).getValue(); - double r = ((LiteralReal) right).getValue(); - 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 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(); - 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)); - } - // bool and bool - else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) { - boolean l = left.isBooleanTrue(); - boolean r = right.isBooleanTrue(); - 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)); - } - - else if (left instanceof Enum leftEnum && right instanceof Enum rightEnum - && leftEnum.getTypeName().equals(rightEnum.getTypeName())) { - boolean equal = leftEnum.getConstName().equals(rightEnum.getConstName()); - Expression res = switch (op) { - case "==" -> new LiteralBoolean(equal); - case "!=" -> new LiteralBoolean(!equal); - default -> null; - }; - if (res != null) - return new ValDerivationNode(res, new BinaryDerivationNode(leftNode, rightNode, op)); - } - - ValDerivationNode adjacentConstants = foldAdjacentIntegerConstants(leftNode, rightNode, op); - if (adjacentConstants != null) - return adjacentConstants; - - // no folding - DerivationNode origin = (leftNode.getOrigin() != null || rightNode.getOrigin() != null) - ? new BinaryDerivationNode(leftNode, rightNode, op) : null; - return new ValDerivationNode(binExp, origin); - } - - /** - * Folds a unary expression node (e.g. !true => false) - */ - private static ValDerivationNode foldUnary(ValDerivationNode node) { - UnaryExpression unaryExp = (UnaryExpression) node.getValue(); - DerivationNode parent = node.getOrigin(); - - // fold child node - ValDerivationNode operandNode; - if (parent instanceof UnaryDerivationNode unaryOrigin) { - // has origin (from constant propagation) - operandNode = fold(unaryOrigin.getOperand()); - } else { - // no origin - operandNode = fold(new ValDerivationNode(unaryExp.getChildren().get(0), null)); - } - Expression operand = operandNode.getValue(); - String operator = unaryExp.getOp(); - unaryExp.setChild(0, operand); - - // unary not - if ("!".equals(operator) && operand instanceof LiteralBoolean) { - // !true => false, !false => true - boolean value = operand.isBooleanTrue(); - Expression res = new LiteralBoolean(!value); - DerivationNode origin = operandNode.getOrigin() != null ? new UnaryDerivationNode(operandNode, operator) - : null; - return new ValDerivationNode(res, origin); - } - // unary minus - if ("-".equals(operator)) { - // -(x) => -x - if (operand instanceof LiteralInt) { - Expression res = new LiteralInt(-((LiteralInt) operand).getValue()); - DerivationNode origin = operandNode.getOrigin() != null ? new UnaryDerivationNode(operandNode, operator) - : null; - return new ValDerivationNode(res, origin); - } - if (operand instanceof LiteralReal) { - Expression res = new LiteralReal(-((LiteralReal) operand).getValue()); - DerivationNode origin = operandNode.getOrigin() != null ? new UnaryDerivationNode(operandNode, operator) - : null; - return new ValDerivationNode(res, origin); - } - } - - // no folding - DerivationNode origin = operandNode.getOrigin() != null ? new UnaryDerivationNode(operandNode, operator) : null; - return new ValDerivationNode(unaryExp, origin); - } - - /** - * Folds ternary expressions by checking if condition is a boolean literal or both branches are the same - */ - private static ValDerivationNode foldIte(ValDerivationNode node) { - Ite iteExp = (Ite) node.getValue(); - - ValDerivationNode condNode = fold(new ValDerivationNode(iteExp.getCondition(), null)); - ValDerivationNode thenNode = fold(new ValDerivationNode(iteExp.getThen(), null)); - ValDerivationNode elseNode = fold(new ValDerivationNode(iteExp.getElse(), null)); - - Expression condition = condNode.getValue(); - Expression thenExp = thenNode.getValue(); - Expression elseExp = elseNode.getValue(); - - iteExp.setChild(0, condition); - iteExp.setChild(1, thenExp); - iteExp.setChild(2, elseExp); - - // if condition is a boolean literal, select the corresponding branch: true ? a : b => a, false ? a : b => b - if (condition instanceof LiteralBoolean boolCond) { - Expression selected = boolCond.isBooleanTrue() ? thenExp : elseExp; - DerivationNode origin = new IteDerivationNode(condNode, thenNode, elseNode); - return new ValDerivationNode(selected, origin); - } - - // if both branches are the same, return one of them (e.g. cond ? b : b => b) - if (thenExp.equals(elseExp)) { - DerivationNode origin = new IteDerivationNode(condNode, thenNode, elseNode); - return new ValDerivationNode(thenExp, origin); - } - - // no folding, but keep track of the folding steps in the origin - DerivationNode origin = hasIteChildOrigin(condNode, thenNode, elseNode) - ? new IteDerivationNode(condNode, thenNode, elseNode) : node.getOrigin(); - return new ValDerivationNode(iteExp, origin); - } - - private static boolean hasIteChildOrigin(ValDerivationNode cond, ValDerivationNode then, ValDerivationNode els) { - return cond.getOrigin() != null || then.getOrigin() != null || els.getOrigin() != null; - } - - private static ValDerivationNode foldAdjacentIntegerConstants(ValDerivationNode leftNode, - ValDerivationNode rightNode, String op) { - if (!"+".equals(op) && !"-".equals(op)) - return null; - if (!(rightNode.getValue()instanceof LiteralInt rightLiteral)) - return null; - if (!(leftNode.getValue()instanceof BinaryExpression leftBinary)) - return null; - if (!"+".equals(leftBinary.getOperator()) && !"-".equals(leftBinary.getOperator())) - return null; - if (!(leftBinary.getSecondOperand()instanceof LiteralInt leftLiteral)) - return null; - - int signedLeft = "+".equals(leftBinary.getOperator()) ? leftLiteral.getValue() : -leftLiteral.getValue(); - int signedRight = "+".equals(op) ? rightLiteral.getValue() : -rightLiteral.getValue(); - Expression folded = expressionWithConstant(leftBinary.getFirstOperand(), signedLeft + signedRight); - - return new ValDerivationNode(folded, new BinaryDerivationNode(leftNode, rightNode, op)); - } - - private static Expression expressionWithConstant(Expression base, int constant) { - if (constant == 0) - return base.clone(); - if (constant > 0) - return new BinaryExpression(base.clone(), "+", new LiteralInt(constant)); - return new BinaryExpression(base.clone(), "-", new LiteralInt(-constant)); - } -} 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 deleted file mode 100644 index e94d2574c..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java +++ /dev/null @@ -1,237 +0,0 @@ -package liquidjava.rj_language.opt; - -import liquidjava.diagnostics.DebugLog; -import liquidjava.processor.context.Context; -import liquidjava.rj_language.Predicate; -import java.util.Map; - -import liquidjava.processor.facade.AliasDTO; -import liquidjava.rj_language.ast.BinaryExpression; -import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.LiteralBoolean; -import liquidjava.rj_language.ast.UnaryExpression; -import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode; -import liquidjava.rj_language.opt.derivation_node.DerivationNode; -import liquidjava.rj_language.opt.derivation_node.UnaryDerivationNode; -import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; -import liquidjava.smt.SMTEvaluator; -import liquidjava.smt.SMTResult; - -public class ExpressionSimplifier { - - /** - * Simplifies an expression by applying constant propagation, constant folding, removing redundant conjuncts and - * expanding aliases Returns a derivation node representing the tree of simplifications applied - */ - public static ValDerivationNode simplify(Expression exp, Map aliases) { - DebugLog.simplificationStart(exp); - ValDerivationNode fixedPoint = simplifyToFixedPoint(null, exp); - DebugLog.simplificationPass("fixed-point reached", fixedPoint.getValue()); - ValDerivationNode simplified = simplifyValDerivationNode(fixedPoint); - DebugLog.simplificationPass("remove redundant &&", simplified.getValue()); - ValDerivationNode unwrapped = unwrapBooleanLiterals(simplified); - DebugLog.simplificationPass("unwrap boolean literals", unwrapped.getValue()); - ValDerivationNode expanded = AliasExpansion.expand(unwrapped, aliases); - DebugLog.simplificationPass("expand aliases", expanded.getValue()); - return expanded; - } - - public static ValDerivationNode simplify(Expression exp) { - return simplify(exp, Map.of()); - } - - /** - * Recursively applies propagation and folding until the expression stops changing (fixed point) Stops early if the - * expression simplifies to a boolean literal, which means we've simplified too much. - */ - private static ValDerivationNode simplifyToFixedPoint(ValDerivationNode current, Expression prevExp) { - ValDerivationNode simplified = simplifyOnce(current, prevExp); - Expression currExp = simplified.getValue(); - - // fixed point reached — compare on toString() because propagate/fold/reduce mutate the AST in place, so a - // reference-level .equals() can trivially be true on shared (mutated) nodes - if (current != null && currExp.toString().equals(current.getValue().toString())) { - return current; - } - - // prevent oversimplification - if (current != null && currExp instanceof LiteralBoolean && !(current.getValue() instanceof LiteralBoolean)) { - return current; - } - - // continue simplifying - return simplifyToFixedPoint(simplified, simplified.getValue()); - } - - private static ValDerivationNode simplifyOnce(ValDerivationNode current, Expression prevExp) { - ValDerivationNode prop = VariablePropagation.propagate(prevExp, current); - DebugLog.simplificationPass("variable propagation", prop.getValue()); - ValDerivationNode fold = ExpressionFolding.fold(prop); - DebugLog.simplificationPass("expression folding", fold.getValue()); - ValDerivationNode simplified = simplifyValDerivationNode(fold); - DebugLog.simplificationPass("remove redundant && (loop)", simplified.getValue()); - return simplified; - } - - /** - * Recursively simplifies the derivation tree by removing redundant conjuncts - */ - private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode node) { - Expression value = node.getValue(); - DerivationNode origin = node.getOrigin(); - - // binary expression with && - if (value instanceof BinaryExpression binExp && "&&".equals(binExp.getOperator())) { - ValDerivationNode leftSimplified; - ValDerivationNode rightSimplified; - - if (origin instanceof BinaryDerivationNode binOrigin) { - leftSimplified = simplifyValDerivationNode(binOrigin.getLeft()); - rightSimplified = simplifyValDerivationNode(binOrigin.getRight()); - } else { - leftSimplified = simplifyValDerivationNode(new ValDerivationNode(binExp.getFirstOperand(), null)); - rightSimplified = simplifyValDerivationNode(new ValDerivationNode(binExp.getSecondOperand(), null)); - } - - // check if either side is redundant - if (isRedundant(leftSimplified.getValue())) - return rightSimplified; - if (isRedundant(rightSimplified.getValue())) - return leftSimplified; - - // collapse identical sides (x && x => x) — toString() avoids false positives when the two sides share a - // mutated AST node and false negatives are harmless (we just keep the conjunction) - if (leftSimplified.getValue().toString().equals(rightSimplified.getValue().toString())) { - return leftSimplified; - } - - // collapse symmetric equalities (e.g. x == y && y == x => x == y) - if (isSymmetricEquality(leftSimplified.getValue(), rightSimplified.getValue())) { - return leftSimplified; - } - - // remove weaker conjuncts (e.g. x > 0 && x > -1 => x > 0) - if (implies(leftSimplified.getValue(), rightSimplified.getValue())) { - return new ValDerivationNode(leftSimplified.getValue(), - new BinaryDerivationNode(leftSimplified, rightSimplified, "&&")); - } - if (implies(rightSimplified.getValue(), leftSimplified.getValue())) { - return new ValDerivationNode(rightSimplified.getValue(), - new BinaryDerivationNode(leftSimplified, rightSimplified, "&&")); - } - - // return the conjunction with simplified children - Expression newValue = new BinaryExpression(leftSimplified.getValue(), "&&", rightSimplified.getValue()); - // only create origin if at least one child has a meaningful origin - if (leftSimplified.getOrigin() != null || rightSimplified.getOrigin() != null) { - DerivationNode newOrigin = new BinaryDerivationNode(leftSimplified, rightSimplified, "&&"); - return new ValDerivationNode(newValue, newOrigin); - } - return new ValDerivationNode(newValue, null); - } - // no simplification - return node; - } - - private static boolean isSymmetricEquality(Expression left, Expression right) { - if (left instanceof BinaryExpression b1 && "==".equals(b1.getOperator()) && right instanceof BinaryExpression b2 - && "==".equals(b2.getOperator())) { - - Expression l1 = b1.getFirstOperand(); - Expression r1 = b1.getSecondOperand(); - Expression l2 = b2.getFirstOperand(); - Expression r2 = b2.getSecondOperand(); - return l1.equals(r2) && r1.equals(l2); - } - return false; - } - - /** - * Checks if an expression is redundant (e.g. true or x == x) - */ - private static boolean isRedundant(Expression exp) { - // true - if (exp instanceof LiteralBoolean && exp.isBooleanTrue()) { - return true; - } - // x == x - if (exp instanceof BinaryExpression binExp) { - if ("==".equals(binExp.getOperator())) { - Expression left = binExp.getFirstOperand(); - Expression right = binExp.getSecondOperand(); - return left.equals(right); - } - } - return false; - } - - /** - * Recursively traverses the derivation tree and replaces boolean literals with the expressions that produced them, - * but only when at least one operand in the derivation is non-boolean. e.g. "x == true" where true came from "1 > - * 0" becomes "x == 1 > 0" - */ - private static ValDerivationNode unwrapBooleanLiterals(ValDerivationNode node) { - Expression value = node.getValue(); - DerivationNode origin = node.getOrigin(); - - if (origin == null) - return node; - - // unwrap binary expressions - if (value instanceof BinaryExpression binExp && origin instanceof BinaryDerivationNode binOrigin) { - ValDerivationNode left = unwrapBooleanLiterals(binOrigin.getLeft()); - ValDerivationNode right = unwrapBooleanLiterals(binOrigin.getRight()); - if (left != binOrigin.getLeft() || right != binOrigin.getRight()) { - Expression newValue = new BinaryExpression(left.getValue(), binExp.getOperator(), right.getValue()); - return new ValDerivationNode(newValue, new BinaryDerivationNode(left, right, binOrigin.getOp())); - } - return node; - } - - // unwrap unary expressions - if (value instanceof UnaryExpression unaryExp && origin instanceof UnaryDerivationNode unaryOrigin) { - ValDerivationNode operand = unwrapBooleanLiterals(unaryOrigin.getOperand()); - if (operand != unaryOrigin.getOperand()) { - Expression newValue = new UnaryExpression(unaryExp.getOp(), operand.getValue()); - return new ValDerivationNode(newValue, new UnaryDerivationNode(operand, unaryOrigin.getOp())); - } - return node; - } - - // boolean literal with binary origin: unwrap if at least one child is non-boolean - if (value instanceof LiteralBoolean && origin instanceof BinaryDerivationNode binOrigin) { - ValDerivationNode left = unwrapBooleanLiterals(binOrigin.getLeft()); - ValDerivationNode right = unwrapBooleanLiterals(binOrigin.getRight()); - if (!(left.getValue() instanceof LiteralBoolean) || !(right.getValue() instanceof LiteralBoolean)) { - Expression newValue = new BinaryExpression(left.getValue(), binOrigin.getOp(), right.getValue()); - return new ValDerivationNode(newValue, new BinaryDerivationNode(left, right, binOrigin.getOp())); - } - return node; - } - - // boolean literal with unary origin: unwrap if operand is non-boolean - if (value instanceof LiteralBoolean && origin instanceof UnaryDerivationNode unaryOrigin) { - ValDerivationNode operand = unwrapBooleanLiterals(unaryOrigin.getOperand()); - if (!(operand.getValue() instanceof LiteralBoolean)) { - Expression newValue = new UnaryExpression(unaryOrigin.getOp(), operand.getValue()); - return new ValDerivationNode(newValue, new UnaryDerivationNode(operand, unaryOrigin.getOp())); - } - return node; - } - - return node; - } - - /** - * Checks whether one expression implies another by asking Z3, used to remove weaker conjuncts in the simplification - */ - private static boolean implies(Expression stronger, Expression weaker) { - try { - SMTResult result = new SMTEvaluator().verifySubtype(new Predicate(stronger), new Predicate(weaker), - Context.getInstance(), true); - return result.isOk(); - } catch (Exception e) { - return false; - } - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java deleted file mode 100644 index 48b37e030..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java +++ /dev/null @@ -1,166 +0,0 @@ -package liquidjava.rj_language.opt; - -import liquidjava.rj_language.ast.BinaryExpression; -import liquidjava.rj_language.ast.Enum; -import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.FunctionInvocation; -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.IteDerivationNode; -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.HashMap; -import java.util.Map; - -public class VariablePropagation { - - /** - * Performs constant and variable propagation on an expression, by substituting variables. 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, ValDerivationNode previousOrigin) { - Map substitutions = VariableResolver.resolve(exp); - Map directSubstitutions = new HashMap<>(); // var == literal or var == var - Map expressionSubstitutions = new HashMap<>(); // var == expression - for (Map.Entry entry : substitutions.entrySet()) { - Expression value = entry.getValue(); - if (value.isLiteral() || value instanceof Var || value instanceof Enum) { - directSubstitutions.put(entry.getKey(), value); - } else { - expressionSubstitutions.put(entry.getKey(), value); - } - } - - // map of variable origins from the previous derivation tree - Map varOrigins = new HashMap<>(); - if (previousOrigin != null) { - extractVarOrigins(previousOrigin, varOrigins); - } - Map activeSubstitutions = directSubstitutions.isEmpty() ? expressionSubstitutions - : directSubstitutions; - return propagateRecursive(exp, activeSubstitutions, varOrigins); - } - - /** - * Recursively performs propagation on an expression (e.g. x + y && x == 1 && y == 2 => 1 + 2) - */ - private static ValDerivationNode propagateRecursive(Expression exp, Map subs, - Map varOrigins) { - - // substitute variable - if (exp instanceof Var var) { - String name = var.getName(); - Expression value = subs.get(name); - // substitution - if (value != null) { - // check if this variable has an origin from a previous pass - DerivationNode previousOrigin = varOrigins.get(name); - - // preserve origin if value came from previous derivation - DerivationNode origin = previousOrigin != null ? new VarDerivationNode(name, previousOrigin) - : new VarDerivationNode(name); - return new ValDerivationNode(value.clone(), origin); - } - - // no substitution - return new ValDerivationNode(var, null); - } - - if (exp instanceof FunctionInvocation) { - Expression value = subs.get(exp.toString()); - if (value != null) - return new ValDerivationNode(value.clone(), new VarDerivationNode(exp.toString())); - } - - // lift unary origin - if (exp instanceof UnaryExpression unary) { - ValDerivationNode operand = propagateRecursive(unary.getChildren().get(0), subs, varOrigins); - UnaryExpression cloned = (UnaryExpression) unary.clone(); - cloned.setChild(0, operand.getValue()); - - return operand.getOrigin() != null - ? new ValDerivationNode(cloned, new UnaryDerivationNode(operand, cloned.getOp())) - : new ValDerivationNode(cloned, null); - } - - // lift binary origin - if (exp instanceof BinaryExpression binary) { - ValDerivationNode left = propagateRecursive(binary.getFirstOperand(), subs, varOrigins); - ValDerivationNode right = propagateRecursive(binary.getSecondOperand(), subs, varOrigins); - BinaryExpression cloned = (BinaryExpression) binary.clone(); - cloned.setChild(0, left.getValue()); - cloned.setChild(1, right.getValue()); - - return (left.getOrigin() != null || right.getOrigin() != null) - ? new ValDerivationNode(cloned, new BinaryDerivationNode(left, right, cloned.getOperator())) - : new ValDerivationNode(cloned, null); - } - - // recursively propagate children - if (exp.hasChildren()) { - Expression propagated = exp.clone(); - for (int i = 0; i < exp.getChildren().size(); i++) { - ValDerivationNode child = propagateRecursive(exp.getChildren().get(i), subs, varOrigins); - propagated.setChild(i, child.getValue()); - } - return new ValDerivationNode(propagated, null); - } - - // no propagation - return new ValDerivationNode(exp, null); - } - - /** - * Extracts the derivation nodes for variable values from the derivation tree This is so done so when we find "var - * == value" in the tree, we store the derivation of the value So it can be preserved when var is substituted in - * subsequent passes - */ - private static void extractVarOrigins(ValDerivationNode node, Map varOrigins) { - if (node == null) - return; - - Expression value = node.getValue(); - DerivationNode origin = node.getOrigin(); - - // check for equality expressions - if (value instanceof BinaryExpression binExp && "==".equals(binExp.getOperator()) - && origin instanceof BinaryDerivationNode binOrigin) { - Expression left = binExp.getFirstOperand(); - Expression right = binExp.getSecondOperand(); - - // extract variable name and value derivation from either side - String varName = null; - ValDerivationNode valueDerivation = null; - - if (left instanceof Var var && right.isLiteral()) { - varName = var.getName(); - valueDerivation = binOrigin.getRight(); - } else if (right instanceof Var var && left.isLiteral()) { - varName = var.getName(); - valueDerivation = binOrigin.getLeft(); - } - if (varName != null && valueDerivation != null && valueDerivation.getOrigin() != null) { - varOrigins.put(varName, valueDerivation.getOrigin()); - } - } - - // recursively process the origin tree - if (origin instanceof BinaryDerivationNode binOrigin) { - extractVarOrigins(binOrigin.getLeft(), varOrigins); - extractVarOrigins(binOrigin.getRight(), varOrigins); - } else if (origin instanceof UnaryDerivationNode unaryOrigin) { - extractVarOrigins(unaryOrigin.getOperand(), varOrigins); - } else if (origin instanceof IteDerivationNode iteOrigin) { - extractVarOrigins(iteOrigin.getCondition(), varOrigins); - extractVarOrigins(iteOrigin.getThenBranch(), varOrigins); - extractVarOrigins(iteOrigin.getElseBranch(), varOrigins); - } else if (origin instanceof ValDerivationNode valOrigin) { - extractVarOrigins(valOrigin, varOrigins); - } - } -} \ No newline at end of file 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 deleted file mode 100644 index 32170c796..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariableResolver.java +++ /dev/null @@ -1,225 +0,0 @@ -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.Enum; -import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.FunctionInvocation; -import liquidjava.rj_language.ast.Var; - -public class VariableResolver { - - /** - * Extracts variables with constant values from an expression - * - * @param exp - * - * @returns map from variable names to their values - */ - public static Map resolve(Expression exp) { - Map map = new HashMap<>(); - - // extract variable equalities recursively - resolveRecursive(exp, map); - - // remove variables that were not used in the expression - map.entrySet().removeIf(entry -> !hasUsage(exp, entry.getKey(), entry.getValue(), true)); - - // transitively resolve variables - return resolveTransitive(map); - } - - /** - * Recursively extracts variable equalities from an expression (e.g. ... && x == 1 && y == 2 => map: x -> 1, y -> 2) - * - * @param exp - * @param map - */ - private static void resolveRecursive(Expression exp, Map map) { - if (!(exp instanceof BinaryExpression be)) - return; - - String op = be.getOperator(); - if ("&&".equals(op)) { - resolveRecursive(be.getFirstOperand(), map); - resolveRecursive(be.getSecondOperand(), map); - return; - } - if (!"==".equals(op)) - return; - - Expression left = be.getFirstOperand(); - Expression right = be.getSecondOperand(); - String leftKey = substitutionKey(left); - String rightKey = substitutionKey(right); - - if (leftKey != null && isConstant(right)) { - map.put(leftKey, right.clone()); - } else if (rightKey != null && isConstant(left)) { - map.put(rightKey, left.clone()); - } else if (left instanceof Var leftVar && right instanceof Var rightVar) { - // to substitute internal variable with user-facing variable - if (isInternal(leftVar) && !isInternal(rightVar) && !isReturnVar(leftVar)) { - map.put(leftVar.getName(), right.clone()); - } else if (isInternal(rightVar) && !isInternal(leftVar) && !isReturnVar(rightVar)) { - map.put(rightVar.getName(), left.clone()); - } else if (isInternal(leftVar) && isInternal(rightVar)) { - // to substitute the lower-counter variable with the higher-counter one - boolean isLeftCounterLower = getCounter(leftVar) <= getCounter(rightVar); - Var lowerVar = isLeftCounterLower ? leftVar : rightVar; - Var higherVar = isLeftCounterLower ? rightVar : leftVar; - if (!isReturnVar(lowerVar) && !isFreshVar(higherVar)) - map.putIfAbsent(lowerVar.getName(), higherVar.clone()); - } - } else if (left instanceof Var var && canSubstitute(var, right)) { - map.put(var.getName(), right.clone()); - } else if (left instanceof FunctionInvocation && !containsExpression(right, left)) { - map.put(leftKey, right.clone()); - } - } - - private static String substitutionKey(Expression exp) { - if (exp instanceof Var var) - return var.getName(); - if (exp instanceof FunctionInvocation) - return exp.toString(); - return null; - } - - /** - * Handles transitive variable equalities in the map (e.g. map: x -> y, y -> 1 => map: x -> 1, y -> 1) - * - * @param map - * - * @return new map with resolved values - */ - private static Map resolveTransitive(Map map) { - Map result = new HashMap<>(); - for (Map.Entry entry : map.entrySet()) { - result.put(entry.getKey(), lookup(entry.getValue(), map, new HashSet<>())); - } - 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 - * - * @param exp - * @param map - * @param seen - * - * @return resolved expression - */ - private static Expression lookup(Expression exp, Map map, Set seen) { - String name = substitutionKey(exp); - if (name == null) - return exp; - - if (seen.contains(name)) - return exp; // circular reference - - Expression value = map.get(name); - if (value == null) - return exp; - - seen.add(name); - return lookup(value, map, seen); - } - - /** - * Checks if a variable is used in the expression (excluding its own definitions) - * - * @param exp - * @param name - * @param value - * @param topLevel - * - * @return true if used, false otherwise - */ - private static boolean hasUsage(Expression exp, String name, Expression value, boolean topLevel) { - if (topLevel && exp instanceof BinaryExpression binary && "&&".equals(binary.getOperator())) { - return hasUsage(binary.getFirstOperand(), name, value, true) - || hasUsage(binary.getSecondOperand(), name, value, true); - } - - if (topLevel && exp instanceof BinaryExpression binary && "==".equals(binary.getOperator())) { - Expression left = binary.getFirstOperand(); - Expression right = binary.getSecondOperand(); - boolean leftDefinition = name.equals(substitutionKey(left)) && right.equals(value) - && (isConstant(right) - || (left instanceof Var v && !(right instanceof Var) && canSubstitute(v, right)) - || (left instanceof FunctionInvocation && !(right instanceof Var) - && !containsExpression(right, left))); - boolean rightDefinition = name.equals(substitutionKey(right)) && left.equals(value) && isConstant(left); - if (leftDefinition || rightDefinition) - return false; - } - - if (name.equals(substitutionKey(exp))) - return true; - for (Expression child : exp.getChildren()) - if (hasUsage(child, name, value, false)) - return true; - return false; - } - - private static int getCounter(Var var) { - if (!isInternal(var)) - throw new IllegalStateException("Cannot get counter of non-internal variable"); - int lastUnderscore = var.getName().lastIndexOf('_'); - return Integer.parseInt(var.getName().substring(lastUnderscore + 1)); - } - - private static boolean isInternal(Var var) { - return var.getName().startsWith("#"); - } - - private static boolean isReturnVar(Var var) { - return var.getName().startsWith("#ret_"); - } - - private static boolean isFreshVar(Var var) { - return var.getName().startsWith("#fresh_"); - } - - private static boolean canSubstitute(Var var, Expression value) { - return !isReturnVar(var) && !isFreshVar(var) && !containsVariable(value, var.getName()); - } - - private static boolean isConstant(Expression exp) { - return exp.isLiteral() || exp instanceof Enum; - } - - private static boolean containsVariable(Expression exp, String name) { - if (exp instanceof Var var) - return var.getName().equals(name); - - if (!exp.hasChildren()) - return false; - - for (Expression child : exp.getChildren()) { - if (containsVariable(child, name)) - return true; - } - return false; - } - - private static boolean containsExpression(Expression exp, Expression target) { - if (exp.equals(target)) - return true; - - if (!exp.hasChildren()) - return false; - - for (Expression child : exp.getChildren()) { - if (containsExpression(child, target)) - return true; - } - return false; - } -} 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 8c30a802d..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/BinaryDerivationNode.java +++ /dev/null @@ -1,26 +0,0 @@ -package liquidjava.rj_language.opt.derivation_node; - -public class BinaryDerivationNode extends DerivationNode { - - private final String op; - private final ValDerivationNode left; - private final ValDerivationNode right; - - 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; - } -} 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 a6b08e542..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/DerivationNode.java +++ /dev/null @@ -1,15 +0,0 @@ -package liquidjava.rj_language.opt.derivation_node; - -import com.google.gson.Gson; -import com.google.gson.GsonBuilder; - -public abstract class DerivationNode { - - // disable html escaping to avoid escaping characters like &, >, <, =, etc. - private static final Gson gson = new GsonBuilder().setPrettyPrinting().disableHtmlEscaping().create(); - - @Override - public String toString() { - return gson.toJson(this); - } -} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/IteDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/IteDerivationNode.java deleted file mode 100644 index 8d0c7fc08..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/IteDerivationNode.java +++ /dev/null @@ -1,26 +0,0 @@ -package liquidjava.rj_language.opt.derivation_node; - -public class IteDerivationNode extends DerivationNode { - - private final ValDerivationNode condition; - private final ValDerivationNode thenBranch; - private final ValDerivationNode elseBranch; - - public IteDerivationNode(ValDerivationNode condition, ValDerivationNode thenBranch, ValDerivationNode elseBranch) { - this.condition = condition; - this.thenBranch = thenBranch; - this.elseBranch = elseBranch; - } - - public ValDerivationNode getCondition() { - return condition; - } - - public ValDerivationNode getThenBranch() { - return thenBranch; - } - - public ValDerivationNode getElseBranch() { - return elseBranch; - } -} \ 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 f0693dc3d..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/UnaryDerivationNode.java +++ /dev/null @@ -1,20 +0,0 @@ -package liquidjava.rj_language.opt.derivation_node; - -public class UnaryDerivationNode extends DerivationNode { - - private final String op; - private final ValDerivationNode operand; - - public UnaryDerivationNode(ValDerivationNode operand, String op) { - this.operand = operand; - this.op = op; - } - - public ValDerivationNode getOperand() { - return operand; - } - - 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 deleted file mode 100644 index 02367ee7f..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java +++ /dev/null @@ -1,54 +0,0 @@ -package liquidjava.rj_language.opt.derivation_node; - -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; -import liquidjava.rj_language.ast.LiteralInt; -import liquidjava.rj_language.ast.LiteralLong; -import liquidjava.rj_language.ast.LiteralReal; - -public class ValDerivationNode extends DerivationNode { - - @JsonAdapter(ExpressionSerializer.class) - 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; - } - - // Custom serializer to handle Expression subclasses properly - 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 v) - return new JsonPrimitive(v.getValue()); - if (exp instanceof LiteralLong v) - return new JsonPrimitive(v.getValue()); - if (exp instanceof LiteralReal v) - return new JsonPrimitive(v.getValue()); - if (exp instanceof LiteralBoolean v) - return new JsonPrimitive(v.isBooleanTrue()); - return new JsonPrimitive(exp.toDisplayString()); - } - } -} 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 a5aa6cc75..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/VarDerivationNode.java +++ /dev/null @@ -1,43 +0,0 @@ -package liquidjava.rj_language.opt.derivation_node; - -import java.lang.reflect.Type; - -import com.google.gson.JsonElement; -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.formatter.VariableFormatter; - -public class VarDerivationNode extends DerivationNode { - - @JsonAdapter(VariableSerializer.class) - private final String var; - private final DerivationNode origin; - - public VarDerivationNode(String var) { - this.var = var; - this.origin = null; - } - - public VarDerivationNode(String var, DerivationNode origin) { - this.var = var; - this.origin = origin; - } - - public String getVar() { - return var; - } - - public DerivationNode getOrigin() { - return origin; - } - - private static class VariableSerializer implements JsonSerializer { - @Override - public JsonElement serialize(String var, Type typeOfSrc, JsonSerializationContext context) { - return new JsonPrimitive(VariableFormatter.format(var)); - } - } -} 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 deleted file mode 100644 index 310515460..000000000 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/ExpressionSimplifierTest.java +++ /dev/null @@ -1,710 +0,0 @@ -package liquidjava.rj_language.opt; - -import static org.junit.jupiter.api.Assertions.*; -import static liquidjava.utils.TestUtils.*; - -import java.util.List; -import java.util.Map; - -import liquidjava.processor.facade.AliasDTO; -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.Var; -import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode; -import liquidjava.rj_language.opt.derivation_node.IteDerivationNode; -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 liquidjava.rj_language.parsing.RefinementsParser; -import org.junit.jupiter.api.Test; - -/** - * Test suite for expression simplification - */ -class ExpressionSimplifierTest { - - private static Expression parse(String sut) { - return RefinementsParser.createAST(sut, ""); - } - - @Test - void testNegation() { - Expression expression = parse("-a && a == 7"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - 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() { - Expression expression = parse("a + b && a == 3 && b == 5"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - 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() { - Expression expression = parse("((y || true) && !true) && y == false"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertInstanceOf(LiteralBoolean.class, result.getValue(), "Result should be a boolean"); - assertFalse((result.getValue()).isBooleanTrue(), "Expected result to be false"); - } - - @Test - void testArithmeticWithConstants() { - Expression expression = parse("((a / b + (-5)) + x) && (a == 6 && b == 2)"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - 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 is a literal with no origin - ValDerivationNode valNeg5 = new ValDerivationNode(new LiteralInt(-5), null); - - // 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() { - Expression expression = parse("a * 2 + b - 3 == c && a == 5 && b == 7 && c == 14"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - // boolean literals are unwrapped to show the verified conditions - assertNotNull(result, "Result should not be null"); - assertNotNull(result.getValue(), "Result value should not be null"); - assertEquals("14 == 14 && 5 == 5 && 7 == 7 && 14 == 14", result.getValue().toString(), - "All verified conditions should be visible instead of collapsed to true"); - } - - @Test - void testFixedPointSimplification() { - Expression expression = parse("x == -y && y == a / b && a == 6 && b == 3"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("x == -2", result.getValue().toString(), "Expected result to be x == -2"); - - // Compare derivation tree structure - - // Build the derivation chain for the right side: - // 6 came from a, 3 came from b - ValDerivationNode val6FromA = new ValDerivationNode(new LiteralInt(6), new VarDerivationNode("a")); - ValDerivationNode val3FromB = new ValDerivationNode(new LiteralInt(3), new VarDerivationNode("b")); - - // 6 / 3 -> 2 - BinaryDerivationNode divOrigin = new BinaryDerivationNode(val6FromA, val3FromB, "/"); - - // 2 came from y, and y's value came from 6 / 2 - VarDerivationNode yChainedOrigin = new VarDerivationNode("y", divOrigin); - ValDerivationNode val2FromY = new ValDerivationNode(new LiteralInt(2), yChainedOrigin); - - // -2 - UnaryDerivationNode negOrigin = new UnaryDerivationNode(val2FromY, "-"); - ValDerivationNode rightNode = new ValDerivationNode(new LiteralInt(-2), negOrigin); - - // Left node x has no origin - ValDerivationNode leftNode = new ValDerivationNode(new Var("x"), null); - - // Root equality - BinaryDerivationNode rootOrigin = new BinaryDerivationNode(leftNode, rightNode, "=="); - ValDerivationNode expected = new ValDerivationNode(result.getValue(), rootOrigin); - - assertDerivationEquals(expected, result, "Derivation tree structure"); - } - - @Test - void testSingleEqualityShouldNotSimplify() { - Expression xEquals1 = parse("x == 1"); - ValDerivationNode result = ExpressionSimplifier.simplify(xEquals1); - - assertNotNull(result, "Result should not be null"); - assertEquals("x == 1", result.getValue().toString(), - "Single equality should not be simplified to a boolean literal"); - - // The result should be the original expression unchanged - assertInstanceOf(BinaryExpression.class, result.getValue(), "Result should still be a binary expression"); - BinaryExpression resultExpr = (BinaryExpression) result.getValue(); - assertEquals("==", resultExpr.getOperator(), "Operator should still be =="); - assertEquals("x", resultExpr.getFirstOperand().toString(), "Left operand should be x"); - assertEquals("1", resultExpr.getSecondOperand().toString(), "Right operand should be 1"); - } - - @Test - void testTwoEqualitiesShouldNotSimplify() { - Expression expression = parse("x == 1 && y == 2"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("x == 1 && y == 2", result.getValue().toString(), - "Two equalities should not be simplified to a boolean literal"); - - // The result should be the original expression unchanged - assertInstanceOf(BinaryExpression.class, result.getValue(), "Result should still be a binary expression"); - BinaryExpression resultExpr = (BinaryExpression) result.getValue(); - assertEquals("&&", resultExpr.getOperator(), "Operator should still be &&"); - assertEquals("x == 1", resultExpr.getFirstOperand().toString(), "Left operand should be x == 1"); - assertEquals("y == 2", resultExpr.getSecondOperand().toString(), "Right operand should be y == 2"); - } - - @Test - void testSameVarTwiceShouldSimplifyToSingle() { - Expression expression = parse("x && x"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("x", result.getValue().toString(), - "Same variable twice should be simplified to a single variable"); - } - - @Test - void testSameEqualityTwiceShouldSimplifyToSingle() { - Expression expression = parse("x == 1 && x == 1"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("x == 1", result.getValue().toString(), - "Same equality twice should be simplified to a single equality"); - } - - @Test - void testSameExpressionTwiceShouldSimplifyToSingle() { - Expression expression = parse("a + b == 1 && a + b == 1"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("a + b == 1", result.getValue().toString(), - "Same expression twice should be simplified to a single equality"); - } - - @Test - void testSymmetricEqualityShouldSimplify() { - Expression expression = parse("x == y && y == x"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("x == y", result.getValue().toString(), - "Symmetric equality should be simplified to a single equality"); - } - - @Test - void testRealExpression() { - String input = "#a_5 == -#fresh_4 && #fresh_4 == #x_2 / #y_3 && #x_2 == #x_0 && #x_0 == 6 && #y_3 == #y_1 && #y_1 == 3"; - Expression expression = parse(input); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("#a_5 == -2", result.getValue().toString(), "Expected result to be #a_5 == -2"); - - } - - @Test - void testTransitive() { - Expression expression = parse("a == b && b == 1"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("a == 1", result.getValue().toString(), "Expected result to be a == 1"); - } - - @Test - void testShouldNotOversimplifyToTrue() { - Expression expression = parse("x > 5 && x == y && y == 10"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertFalse(result.getValue() instanceof LiteralBoolean, - "Should not oversimplify to a boolean literal, but got: " + result.getValue()); - assertEquals("x > 5 && x == 10", result.getValue().toString(), - "Should stop simplification before collapsing to true"); - } - - @Test - void testShouldUnwrapBooleanInEquality() { - Expression expression = parse("x == (1 > 0)"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("x == (1 > 0)", result.getValue().toDisplayString(), - "Boolean in equality should be unwrapped to show the original comparison"); - } - - @Test - void testShouldUnwrapBooleanInEqualityWithPropagation() { - Expression expression = parse("x == (a > b) && a == 3 && b == 1"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("x == (3 > 1)", result.getValue().toDisplayString(), - "Boolean in equality should be unwrapped after propagation"); - } - - @Test - void testShouldNotUnwrapBooleanWithBooleanChildren() { - Expression expression = parse("(y || true) && !true && y == false"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - // false stays as false since both sides in the derivation are booleans - assertNotNull(result, "Result should not be null"); - assertInstanceOf(LiteralBoolean.class, result.getValue(), "Result should remain a boolean"); - assertFalse(result.getValue().isBooleanTrue(), "Expected result to be false"); - } - - @Test - void testShouldUnwrapNestedBooleanInEquality() { - Expression expression = parse("x == (a + b > 10) && a == 3 && b == 5"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("x == (8 > 10)", result.getValue().toDisplayString(), - "Boolean in equality should be unwrapped to show the computed comparison"); - } - - @Test - void testVarToVarPropagationWithInternalVariable() { - Expression expression = parse("#x_0 == a && #x_0 > 5"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("a > 5", result.getValue().toString(), - "Internal variable #x_0 should be substituted with user-facing variable a"); - } - - @Test - void testVarToVarInternalToInternal() { - Expression expression = parse("#a_1 == #b_2 && #b_2 == 5 && x == #a_1 + 1"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("x == 6", result.getValue().toString(), - "#a should resolve through #b to 5 across passes, then x == 5 + 1 = x == 6"); - } - - @Test - void testVarToVarDoesNotAffectUserFacingVariables() { - Expression expression = parse("x == y && x > 5"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("x == y && x > 5", result.getValue().toString(), - "User-facing variable equalities should not trigger var-to-var propagation"); - } - - @Test - void testVarToVarRemovesRedundantEquality() { - Expression expression = parse("#ret_1 == #b_0 - 100 && #b_0 == b && b >= -128 && b <= 127"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("#ret_1 == b - 100 && b >= -128 && b <= 127", result.getValue().toString(), - "Internal variable #b_0 should be replaced with b and redundant equality removed"); - assertNotNull(result.getOrigin(), "Origin should be present showing the var-to-var derivation"); - } - - @Test - void testInternalToInternalReducesRedundantVariable() { - Expression expression = parse("#a_3 == #b_7 && #a_3 > 5"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result); - assertEquals("#b_7 > 5", result.getValue().toString(), - "#a_3 (lower counter) should be substituted with #b_7 (higher counter)"); - } - - @Test - void testInternalToInternalChainWithUserFacingVariableUserFacingFirst() { - Expression expression = parse("#b_7 == x && #a_3 == #b_7 && x > 0"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result); - assertEquals("x > 0", result.getValue().toString(), - "Both internal variables should be eliminated via chain resolution"); - } - - @Test - void testInternalToInternalChainWithUserFacingVariableInternalFirst() { - Expression expression = parse("#a_3 == #b_7 && #b_7 == x && x > 0"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result); - assertEquals("x > 0", result.getValue().toString(), - "Both internal variables should be eliminated via fixed-point iteration"); - } - - @Test - void testInternalToInternalBothResolvingToLiteral() { - Expression expression = parse("#a_3 == #b_7 && #b_7 == 5"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result); - assertEquals("5 == 5 && 5 == 5", result.getValue().toString(), - "#a_3 -> #b_7 -> 5 and #b_7 -> 5; both equalities collapse to 5 == 5"); - } - - @Test - void testInternalToInternalNoFurtherResolution() { - Expression expression = parse("#a_3 == #b_7 && #b_7 + 1 > 0"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result); - assertEquals("#b_7 + 1 > 0", result.getValue().toString(), - "#a_3 (lower counter) replaced by #b_7 (higher counter); equality collapses to trivial"); - } - - @Test - void testIteTrueConditionSimplifiesToThenBranch() { - Expression expr = parse("true ? a : b"); - ValDerivationNode result = ExpressionSimplifier.simplify(expr); - - assertNotNull(result, "Result should not be null"); - assertEquals("a", result.getValue().toString(), "Expected result to be a"); - - ValDerivationNode conditionNode = new ValDerivationNode(new LiteralBoolean(true), null); - ValDerivationNode thenNode = new ValDerivationNode(new Var("a"), null); - ValDerivationNode elseNode = new ValDerivationNode(new Var("b"), null); - IteDerivationNode iteOrigin = new IteDerivationNode(conditionNode, thenNode, elseNode); - ValDerivationNode expected = new ValDerivationNode(new Var("a"), iteOrigin); - - assertDerivationEquals(expected, result, ""); - } - - @Test - void testIteFalseConditionSimplifiesToElseBranch() { - Expression expr = parse("false ? a : b"); - ValDerivationNode result = ExpressionSimplifier.simplify(expr); - - assertNotNull(result, "Result should not be null"); - assertEquals("b", result.getValue().toString(), "Expected result to be b"); - - ValDerivationNode conditionNode = new ValDerivationNode(new LiteralBoolean(false), null); - ValDerivationNode thenNode = new ValDerivationNode(new Var("a"), null); - ValDerivationNode elseNode = new ValDerivationNode(new Var("b"), null); - IteDerivationNode iteOrigin = new IteDerivationNode(conditionNode, thenNode, elseNode); - ValDerivationNode expected = new ValDerivationNode(new Var("b"), iteOrigin); - - assertDerivationEquals(expected, result, ""); - } - - @Test - void testIteEqualBranchesSimplifiesToBranch() { - Expression expr = parse("cond ? b : b"); - ValDerivationNode result = ExpressionSimplifier.simplify(expr); - - assertNotNull(result, "Result should not be null"); - assertEquals("b", result.getValue().toString(), "Expected result to be b"); - - ValDerivationNode conditionNode = new ValDerivationNode(new Var("cond"), null); - ValDerivationNode thenNode = new ValDerivationNode(new Var("b"), null); - ValDerivationNode elseNode = new ValDerivationNode(new Var("b"), null); - IteDerivationNode iteOrigin = new IteDerivationNode(conditionNode, thenNode, elseNode); - ValDerivationNode expected = new ValDerivationNode(new Var("b"), iteOrigin); - - assertDerivationEquals(expected, result, ""); - } - - @Test - void testIteConditionUsesEqualityFromConjunction() { - Expression expr = parse("mode == 1 && (mode == 2 ? explicit(param) : start(param))"); - ValDerivationNode result = ExpressionSimplifier.simplify(expr); - - assertNotNull(result, "Result should not be null"); - assertEquals("start(param)", result.getValue().toString(), - "mode == 1 should make the mode == 2 ternary condition false"); - } - - @Test - void testByteAliasExpansion() { - String sut = "Byte(b)"; - AliasDTO byteAlias = new AliasDTO("Byte", List.of("int"), List.of("b"), "b >= -128 && b <= 127"); - byteAlias.parse(""); - Map aliases = Map.of("Byte", byteAlias); - Expression exp = parse(sut); - ValDerivationNode result = ExpressionSimplifier.simplify(exp, aliases); - - assertEquals("Byte(b)", result.getValue().toString()); - assertNotNull(result.getOrigin(), "Origin should contain the expanded body"); - ValDerivationNode origin = (ValDerivationNode) result.getOrigin(); - assertEquals("b >= -128 && b <= 127", origin.getValue().toString()); - } - - @Test - void testPositiveAliasExpansion() { - String sut = "Positive(x)"; - AliasDTO positiveAlias = new AliasDTO("Positive", List.of("int"), List.of("v"), "v > 0"); - positiveAlias.parse(""); - Map aliases = Map.of("Positive", positiveAlias); - Expression exp = parse(sut); - ValDerivationNode result = ExpressionSimplifier.simplify(exp, aliases); - - assertEquals("Positive(x)", result.getValue().toString()); - assertNotNull(result.getOrigin(), "Origin should contain the expanded body"); - ValDerivationNode origin = (ValDerivationNode) result.getOrigin(); - assertEquals("x > 0", origin.getValue().toString()); - } - - @Test - void testTwoArgAliasWithNormalExpression() { - String sut = "Bounded(v, 100) && v > 50"; - AliasDTO boundedAlias = new AliasDTO("Bounded", List.of("int", "int"), List.of("x", "n"), "x > 0 && x < n"); - boundedAlias.parse(""); - Map aliases = Map.of("Bounded", boundedAlias); - Expression expression = parse(sut); - ValDerivationNode result = ExpressionSimplifier.simplify(expression, aliases); - - assertEquals("Bounded(v, 100) && v > 50", result.getValue().toString()); - assertInstanceOf(BinaryDerivationNode.class, result.getOrigin()); - BinaryDerivationNode binOrigin = (BinaryDerivationNode) result.getOrigin(); - assertEquals("&&", binOrigin.getOp()); - ValDerivationNode leftNode = binOrigin.getLeft(); - assertEquals("Bounded(v, 100)", leftNode.getValue().toString()); - assertNotNull(leftNode.getOrigin(), "Alias invocation should have expanded body as origin"); - ValDerivationNode expandedBody = (ValDerivationNode) leftNode.getOrigin(); - assertEquals("v > 0 && v < 100", expandedBody.getValue().toString()); - ValDerivationNode rightNode = binOrigin.getRight(); - assertEquals("v > 50", rightNode.getValue().toString()); - assertNull(rightNode.getOrigin()); - } - - @Test - void testEntailedConjunctIsRemovedButOriginIsPreserved() { - String sut = "b >= 100 && b > 0"; - addIntVariableToContext("b"); - Expression expression = parse(sut); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result); - assertEquals("b >= 100", result.getValue().toString(), - "The weaker conjunct should be removed when implied by the stronger one"); - - BinaryExpression parsed = (BinaryExpression) expression; - Expression bGe100 = parsed.getFirstOperand(); - Expression bGt0 = parsed.getSecondOperand(); - ValDerivationNode expectedLeft = new ValDerivationNode(bGe100, null); - ValDerivationNode expectedRight = new ValDerivationNode(bGt0, null); - ValDerivationNode expected = new ValDerivationNode(bGe100, - new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); - - assertDerivationEquals(expected, result, "Entailment simplification should preserve conjunction origin"); - } - - @Test - void testStrictComparisonImpliesNonStrictComparison() { - String sut = "x > y && x >= y"; - addIntVariableToContext("x"); - addIntVariableToContext("y"); - Expression expression = parse(sut); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result); - assertEquals("x > y", result.getValue().toString(), - "The stricter comparison should be kept when it implies the weaker one"); - - BinaryExpression parsed = (BinaryExpression) expression; - Expression xGtY = parsed.getFirstOperand(); - Expression xGeY = parsed.getSecondOperand(); - ValDerivationNode expectedLeft = new ValDerivationNode(xGtY, null); - ValDerivationNode expectedRight = new ValDerivationNode(xGeY, null); - ValDerivationNode expected = new ValDerivationNode(xGtY, - new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); - - assertDerivationEquals(expected, result, "Strict comparison simplification should preserve conjunction origin"); - } - - @Test - void testEquivalentBoundsKeepOneSide() { - String sut = "0 <= i && i >= 0"; - addIntVariableToContext("i"); - Expression expression = parse(sut); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result); - assertEquals("0 <= i", result.getValue().toString(), "Equivalent bounds should collapse to a single conjunct"); - - BinaryExpression parsed = (BinaryExpression) expression; - Expression zeroLeI = parsed.getFirstOperand(); - Expression iGeZero = parsed.getSecondOperand(); - ValDerivationNode expectedLeft = new ValDerivationNode(zeroLeI, null); - ValDerivationNode expectedRight = new ValDerivationNode(iGeZero, null); - ValDerivationNode expected = new ValDerivationNode(zeroLeI, - new BinaryDerivationNode(expectedLeft, expectedRight, "&&")); - - assertDerivationEquals(expected, result, "Equivalent bounds simplification should preserve conjunction origin"); - } - - @Test - void testSubstitutesVariableDefinedByArithmeticExpression() { - Expression expression = parse("z == y - 2 && y == x + 1"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertNotNull(result, "Result should not be null"); - assertEquals("z == x - 1", result.getValue().toString(), "Expected variable definition to be substituted"); - } - - @Test - void testFoldsAdjacentIntegerConstantsInLeftAssociatedArithmetic() { - assertEquals("x - 1", ExpressionSimplifier.simplify(parse("x + 1 - 2")).getValue().toString()); - assertEquals("x + 1", ExpressionSimplifier.simplify(parse("x - 1 + 2")).getValue().toString()); - assertEquals("x + 3", ExpressionSimplifier.simplify(parse("x + 1 + 2")).getValue().toString()); - assertEquals("x", ExpressionSimplifier.simplify(parse("x + 1 - 1")).getValue().toString()); - } - - @Test - void testFunctionInvocationEqualitiesPropagateTransitively() { - Expression expression = parse("size(x3) == size(x2) - 1 && size(x2) == size(x1) + 1 && size(x1) == 0"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("size(x3) == 0", result.getValue().toString()); - } - - @Test - void testFunctionInvocationOnLeftBehavesLikeVariable() { - Expression expression = parse("func(a) == func(b) && func(b) == 1"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("func(a) == 1", result.getValue().toString()); - } - - @Test - void testFunctionInvocationEqualitiesMixWithVariables() { - Expression expression = parse("func(a) + x && func(a) == y && y == 1 && x == 2"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("3", result.getValue().toString()); - } - - @Test - void testEnumConstantsPropagateIntoVariableEquality() { - Expression expression = parse("current == mode && mode == Mode.Photo"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("current == Mode.Photo", result.getValue().toString()); - } - - @Test - void testEnumConstantsPropagateTransitively() { - Expression expression = parse("target == current && current == mode && mode == Mode.Photo"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("target == Mode.Photo", result.getValue().toString()); - } - - @Test - void testEnumConstantsPropagateThroughFunctionInvocations() { - Expression expression = parse("modeOf(x) == Mode.Photo && current == modeOf(x)"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("current == Mode.Photo", result.getValue().toString()); - } - - @Test - void testEnumConstantsPropagateIntoTernaryCondition() { - Expression expression = parse("mode == Mode.Photo && (mode == Mode.Video ? explicit(param) : start(param))"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("start(param)", result.getValue().toString()); - } - - @Test - void testRepeatedEqualDefinitionPropagatesIntoTernaryCondition() { - Expression expression = parse("mode == 2 && (mode == 2 ? explicit(param) : start(param))"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("explicit(param)", result.getValue().toString()); - } - - @Test - void testRepeatedEqualDefinitionsPropagateIntoCompoundTernaryCondition() { - Expression expression = parse( - "mode == 2 && other == 5 && ((mode == 2 && other == 5) ? explicit(param) : start(param))"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("explicit(param)", result.getValue().toString()); - } - - @Test - void testRepeatedEqualDefinitionPropagatesWhenUsageComesFirst() { - Expression expression = parse("(mode == 2 ? explicit(param) : start(param)) && mode == 2"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("explicit(param)", result.getValue().toString()); - } - - @Test - void testRepeatedFunctionInvocationDefinitionPropagatesIntoTernaryCondition() { - Expression expression = parse("modeOf(param) == 2 && (modeOf(param) == 2 ? explicit(param) : start(param))"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("explicit(param)", result.getValue().toString()); - } - - @Test - void testRepeatedEqualDefinitionsPropagateIntoNestedTernaryConditions() { - Expression expression = parse("mode == 2 && other == 3 && (mode == 2 ? (other == 3 ? a(p) : b(p)) : c(p))"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("a(p)", result.getValue().toString()); - } - - @Test - void testRepeatedEqualDefinitionsPropagateIntoNestedTernaryElseBranch() { - Expression expression = parse("mode == 2 && other == 4 && (mode == 2 ? (other == 3 ? a(p) : b(p)) : c(p))"); - ValDerivationNode result = ExpressionSimplifier.simplify(expression); - - assertEquals("b(p)", result.getValue().toString()); - } -} diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java deleted file mode 100644 index 136af9e27..000000000 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java +++ /dev/null @@ -1,217 +0,0 @@ -package liquidjava.rj_language.opt; - -import static org.junit.jupiter.api.Assertions.*; - -import java.util.Map; - -import org.junit.jupiter.api.Test; - -import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.parsing.RefinementsParser; - -class VariableResolverTest { - - private static Expression parse(String refinement) { - return RefinementsParser.createAST(refinement, ""); - } - - @Test - void testSingleEqualityNotExtracted() { - Expression expression = parse("x == 1"); - Map result = VariableResolver.resolve(expression); - - assertTrue(result.isEmpty(), "Single equality should not extract variable mapping"); - } - - @Test - void testConjunctionExtractsVariables() { - Expression expression = parse("x + y && x == 1 && y == 2"); - Map result = VariableResolver.resolve(expression); - - assertEquals(2, result.size(), "Should extract both variables"); - assertEquals("1", result.get("x").toString()); - assertEquals("2", result.get("y").toString()); - } - - @Test - void testSingleComparisonNotExtracted() { - Expression expression = parse("x > 0"); - Map result = VariableResolver.resolve(expression); - - assertTrue(result.isEmpty(), "Single comparison should not extract variable mapping"); - } - - @Test - void testSingleArithmeticExpression() { - Expression expression = parse("x + 1"); - Map result = VariableResolver.resolve(expression); - - assertTrue(result.isEmpty(), "Single arithmetic expression should not extract variable mapping"); - } - - @Test - void testDisjunctionWithEqualities() { - Expression expression = parse("x == 1 || y == 2"); - Map result = VariableResolver.resolve(expression); - - assertTrue(result.isEmpty(), "Disjunction should not extract variable mappings"); - } - - @Test - void testNegatedEquality() { - Expression expression = parse("!(x == 1)"); - Map result = VariableResolver.resolve(expression); - - assertTrue(result.isEmpty(), "Negated equality should not extract variable mapping"); - } - - @Test - void testGroupedEquality() { - Expression expression = parse("(x == 1)"); - Map result = VariableResolver.resolve(expression); - - assertTrue(result.isEmpty(), "Grouped single equality should not extract variable mapping"); - } - - @Test - void testCircularDependency() { - Expression expression = parse("x == y && y == x"); - Map result = VariableResolver.resolve(expression); - - assertTrue(result.isEmpty(), "Circular dependency should not extract variable mappings"); - } - - @Test - void testUnusedEqualitiesShouldBeIgnored() { - Expression expression = parse("z > 0 && x == 1 && y == 2 && z == 3"); - Map result = VariableResolver.resolve(expression); - - assertEquals(1, result.size(), "Should only extract used variable z"); - assertEquals("3", result.get("z").toString()); - } - - @Test - void testDifferentEqualityInIteConditionCountsAsUsage() { - Expression expression = parse("mode == 1 && (mode == 2 ? explicit(param) : start(param))"); - Map result = VariableResolver.resolve(expression); - - assertEquals(1, result.size(), "Ternary condition should count as a use of mode"); - assertEquals("1", result.get("mode").toString()); - } - - @Test - void testRepeatedEqualDefinitionCountsAsUsage() { - Expression expression = parse("mode == 2 && (mode == 2 ? explicit(param) : start(param))"); - Map result = VariableResolver.resolve(expression); - - assertEquals(1, result.size(), "Repeated equalities should keep one definition and treat the other as usage"); - assertEquals("2", result.get("mode").toString()); - } - - @Test - void testRepeatedEqualDefinitionsInCompoundIteConditionCountAsUsage() { - Expression expression = parse( - "mode == 2 && other == 5 && ((mode == 2 && other == 5) ? explicit(param) : start(param))"); - Map result = VariableResolver.resolve(expression); - - assertEquals(2, result.size(), "Compound ternary condition should count as a use of both variables"); - assertEquals("2", result.get("mode").toString()); - assertEquals("5", result.get("other").toString()); - } - - @Test - void testRepeatedEqualDefinitionCountsAsUsageBeforeDefinitionConjunct() { - Expression expression = parse("(mode == 2 ? explicit(param) : start(param)) && mode == 2"); - Map result = VariableResolver.resolve(expression); - - assertEquals(1, result.size(), "Conjunct order should not affect repeated equality usage detection"); - assertEquals("2", result.get("mode").toString()); - } - - @Test - void testRepeatedFunctionInvocationDefinitionCountsAsUsage() { - Expression expression = parse("modeOf(param) == 2 && (modeOf(param) == 2 ? explicit(param) : start(param))"); - Map result = VariableResolver.resolve(expression); - - assertEquals(1, result.size(), "Function invocation definition should count repeated nested equality as usage"); - assertEquals("2", result.get("modeOf(param)").toString()); - } - - @Test - void testRepeatedExpressionDefinitionCountsAsUsage() { - Expression expression = parse("limit == max - 1 && (limit == max - 1 ? a(p) : b(p))"); - Map result = VariableResolver.resolve(expression); - - assertEquals(1, result.size(), "Expression definition should count repeated nested equality as usage"); - assertEquals("max - 1", result.get("limit").toString()); - } - - @Test - void testRepeatedTopLevelDefinitionsOnlyDoNotCountAsUsage() { - Expression expression = parse("mode == 2 && mode == 2"); - Map result = VariableResolver.resolve(expression); - - assertTrue(result.isEmpty(), "Repeated top-level definitions alone should not count as usage"); - } - - @Test - void testReturnVariableIsNotSubstituted() { - Expression expression = parse("x > 0 && #ret_1 == x"); - Map result = VariableResolver.resolve(expression); - - assertTrue(result.isEmpty(), "Return variables should not be substituted with another variable"); - } - - @Test - void testFreshVariableIsNotUsedAsSubstitutionTarget() { - Expression expression = parse("#tmp_1 > 0 && #tmp_1 == #fresh_2"); - Map result = VariableResolver.resolve(expression); - - assertTrue(result.isEmpty(), "Fresh variables should not replace another variable"); - } - - @Test - void testFunctionInvocationEqualityExtractsFunctionKey() { - Expression expression = parse("size(stack) > 0 && size(stack) == 1"); - Map result = VariableResolver.resolve(expression); - - assertEquals(1, result.size(), "Should extract the function invocation as a substitution key"); - assertEquals("1", result.get("size(stack)").toString()); - } - - @Test - void testLiteralOnLeftExtractsFunctionInvocationKey() { - Expression expression = parse("size(stack) > 0 && 1 == size(stack)"); - Map result = VariableResolver.resolve(expression); - - assertEquals(1, result.size(), "Should extract function invocation equalities from either side"); - assertEquals("1", result.get("size(stack)").toString()); - } - - @Test - void testFunctionInvocationEqualitiesResolveTransitively() { - Expression expression = parse("func(a) > 0 && func(a) == func(b) && func(b) == 1"); - Map result = VariableResolver.resolve(expression); - - assertEquals(2, result.size(), "Should keep the function invocation chain that was used"); - assertEquals("1", result.get("func(a)").toString()); - assertEquals("1", result.get("func(b)").toString()); - } - - @Test - void testFunctionInvocationNamesAreMatchedStructurally() { - Expression expression = parse("f(a) > 0 && f(a) == ff(a) + b"); - Map result = VariableResolver.resolve(expression); - - assertEquals(1, result.size(), "Should not treat ff(a) as a use of f(a)"); - assertEquals("ff(a) + b", result.get("f(a)").toString()); - } - - @Test - void testUnusedFunctionInvocationEqualityIsIgnored() { - Expression expression = parse("x > 0 && size(stack) == 1"); - Map result = VariableResolver.resolve(expression); - - assertTrue(result.isEmpty(), "Function invocation definitions with no usage should be ignored"); - } -} diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index 35e1ead6d..f81f013fc 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -1,9 +1,6 @@ package liquidjava.utils; import java.io.BufferedReader; -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertNotNull; - import java.io.IOException; import java.nio.file.Files; import java.nio.file.Path; @@ -14,12 +11,6 @@ import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode; -import liquidjava.rj_language.opt.derivation_node.DerivationNode; -import liquidjava.rj_language.opt.derivation_node.IteDerivationNode; -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 spoon.Launcher; import spoon.reflect.factory.Factory; @@ -87,7 +78,7 @@ public static List> getExpectedErrorsFromDirectory(Path di try { List files = Files.list(dirPath).filter(Files::isRegularFile).toList(); for (Path file : files) { - getExpectedErrorsFromFile(file).forEach(expectedErrors::add); + expectedErrors.addAll(getExpectedErrorsFromFile(file)); } } catch (IOException e) { return List.of(); @@ -96,43 +87,7 @@ public static List> getExpectedErrorsFromDirectory(Path di } /** - * Helper method to compare two derivation nodes recursively - */ - public static void assertDerivationEquals(DerivationNode expected, DerivationNode actual, String message) { - if (expected == null && actual == null) - return; - - assertNotNull(expected); - assertEquals(expected.getClass(), actual.getClass(), message + ": node types should match"); - if (expected instanceof ValDerivationNode expectedVal) { - 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 expectedBin) { - 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 expectedVar) { - VarDerivationNode actualVar = (VarDerivationNode) actual; - assertEquals(expectedVar.getVar(), actualVar.getVar(), message + ": variables should match"); - } else if (expected instanceof UnaryDerivationNode expectedUnary) { - UnaryDerivationNode actualUnary = (UnaryDerivationNode) actual; - assertEquals(expectedUnary.getOp(), actualUnary.getOp(), message + ": operators should match"); - assertDerivationEquals(expectedUnary.getOperand(), actualUnary.getOperand(), message + " > operand"); - } else if (expected instanceof IteDerivationNode expectedIte) { - IteDerivationNode actualIte = (IteDerivationNode) actual; - assertDerivationEquals(expectedIte.getCondition(), actualIte.getCondition(), message + " > condition"); - assertDerivationEquals(expectedIte.getThenBranch(), actualIte.getThenBranch(), message + " > then"); - assertDerivationEquals(expectedIte.getElseBranch(), actualIte.getElseBranch(), message + " > else"); - } - } - - /** - * Helper method to add an integer variable to the context Needed for tests that rely on the SMT-based implication - * checks The simplifier asks Z3 whether one conjunct implies another, so every variable in those expressions must - * be in the context + * Helper method to add an integer variable to the context */ public static void addIntVariableToContext(String name) { context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, new Predicate(),