diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java index d2dbccbe..959c799d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java @@ -3,9 +3,7 @@ import java.util.ArrayList; import java.util.List; -import liquidjava.processor.SimplifiedVCImplication; import liquidjava.processor.VCImplication; -import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.GroupExpression; @@ -17,46 +15,29 @@ /** * Simplifies VCImplication chains by applying arithmetic identities inside refinements */ -public class VCArithmeticSimplification { +public class VCArithmeticSimplification extends VCExpressionSimplificationPass> { - /** - * Applies the first arithmetic simplification available in a VC chain - */ - public static VCImplication apply(VCImplication implication) { - if (implication == null) - return null; - - return apply(implication, List.of()); + @Override + protected List initialContext() { + return List.of(); } - private static VCImplication apply(VCImplication implication, List nonZeroExpressions) { - if (implication == null) - return null; - - Expression expression = implication.getRefinement().getExpression(); - Expression simplified = simplify(expression, nonZeroExpressions); - if (!expression.equals(simplified)) { - VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), implication); - result.setNext(implication.getNext() == null ? null : implication.getNext().clone()); - return result; - } - - List nextNoneZeroExpressions = new ArrayList<>(nonZeroExpressions); - addNonZeroExpression(implication.getRefinement().getExpression(), nextNoneZeroExpressions); - - VCImplication next = apply(implication.getNext(), nextNoneZeroExpressions); - if (implication.getNext() == null || implication.getNext().equals(next)) - return implication; + @Override + protected List nextContext(List nonZeroExpressions, VCImplication implication) { + List nextNonZeroExpressions = new ArrayList<>(nonZeroExpressions); + addNonZeroExpression(implication.getRefinement().getExpression(), nextNonZeroExpressions); + return nextNonZeroExpressions; + } - VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone()); - result.setNext(next); - return result; + @Override + protected Expression simplify(Expression expression, List nonZeroExpressions) { + return simplifyExpression(expression, nonZeroExpressions); } /** * Simplifies the first arithmetic identity found inside an expression */ - private static Expression simplify(Expression expression, List nonZeroExpressions) { + private Expression simplifyExpression(Expression expression, List nonZeroExpressions) { if (expression instanceof BinaryExpression binary) return simplifyBinary(binary, nonZeroExpressions); if (expression instanceof UnaryExpression unary) @@ -71,14 +52,14 @@ private static Expression simplify(Expression expression, List nonZe /** * Simplifies a binary expression by visiting operands before the current node */ - private static Expression simplifyBinary(BinaryExpression binary, List nonZeroExpressions) { + private Expression simplifyBinary(BinaryExpression binary, List nonZeroExpressions) { Expression left = binary.getFirstOperand(); - Expression simplifiedLeft = simplify(left, nonZeroExpressions); + Expression simplifiedLeft = simplifyExpression(left, nonZeroExpressions); if (!left.equals(simplifiedLeft)) return new BinaryExpression(simplifiedLeft, binary.getOperator(), binary.getSecondOperand().clone()); Expression right = binary.getSecondOperand(); - Expression simplifiedRight = simplify(right, nonZeroExpressions); + Expression simplifiedRight = simplifyExpression(right, nonZeroExpressions); if (!right.equals(simplifiedRight)) return new BinaryExpression(left.clone(), binary.getOperator(), simplifiedRight); @@ -92,9 +73,9 @@ private static Expression simplifyBinary(BinaryExpression binary, List nonZeroExpressions) { + private Expression simplifyUnary(UnaryExpression unary, List nonZeroExpressions) { Expression operand = unary.getExpression(); - Expression simplifiedOperand = simplify(operand, nonZeroExpressions); + Expression simplifiedOperand = simplifyExpression(operand, nonZeroExpressions); if (!operand.equals(simplifiedOperand)) return new UnaryExpression(unary.getOp(), simplifiedOperand); @@ -108,19 +89,19 @@ private static Expression simplifyUnary(UnaryExpression unary, List /** * Simplifies a ternary expression by visiting condition, then branch, and else branch */ - private static Expression simplifyIte(Ite ite, List nonZeroExpressions) { + private Expression simplifyIte(Ite ite, List nonZeroExpressions) { Expression condition = ite.getCondition(); - Expression simplifiedCondition = simplify(condition, nonZeroExpressions); + Expression simplifiedCondition = simplifyExpression(condition, nonZeroExpressions); if (!condition.equals(simplifiedCondition)) return new Ite(simplifiedCondition, ite.getThen().clone(), ite.getElse().clone()); Expression thenExpression = ite.getThen(); - Expression simplifiedThen = simplify(thenExpression, nonZeroExpressions); + Expression simplifiedThen = simplifyExpression(thenExpression, nonZeroExpressions); if (!thenExpression.equals(simplifiedThen)) return new Ite(condition.clone(), simplifiedThen, ite.getElse().clone()); Expression elseExpression = ite.getElse(); - Expression simplifiedElse = simplify(elseExpression, nonZeroExpressions); + Expression simplifiedElse = simplifyExpression(elseExpression, nonZeroExpressions); if (!elseExpression.equals(simplifiedElse)) return new Ite(condition.clone(), thenExpression.clone(), simplifiedElse); @@ -130,9 +111,9 @@ private static Expression simplifyIte(Ite ite, List nonZeroExpressio /** * Simplifies an expression wrapped in parentheses while preserving the group node */ - private static Expression simplifyGroup(GroupExpression group, List nonZeroExpressions) { + private Expression simplifyGroup(GroupExpression group, List nonZeroExpressions) { Expression expression = group.getExpression(); - Expression simplified = simplify(expression, nonZeroExpressions); + Expression simplified = simplifyExpression(expression, nonZeroExpressions); if (!expression.equals(simplified)) return new GroupExpression(simplified); return group.clone(); @@ -141,7 +122,7 @@ private static Expression simplifyGroup(GroupExpression group, List /** * Dispatches a local binary arithmetic identity by operator */ - private static Expression simplifyLocalBinary(Expression left, Expression right, String op, + private Expression simplifyLocalBinary(Expression left, Expression right, String op, List nonZeroExpressions) { return switch (op) { case "+" -> simplifyAddition(left, right); @@ -156,7 +137,7 @@ private static Expression simplifyLocalBinary(Expression left, Expression right, /** * Applies addition identities involving zero and unary negation */ - private static Expression simplifyAddition(Expression left, Expression right) { + private Expression simplifyAddition(Expression left, Expression right) { // x + 0 -> x if (isZero(right)) return left.clone(); @@ -178,7 +159,7 @@ private static Expression simplifyAddition(Expression left, Expression right) { /** * Applies subtraction identities involving zero, same operands, and unary negation */ - private static Expression simplifySubtraction(Expression left, Expression right) { + private Expression simplifySubtraction(Expression left, Expression right) { // x - 0 -> x if (isZero(right)) return left.clone(); @@ -197,7 +178,7 @@ private static Expression simplifySubtraction(Expression left, Expression right) /** * Applies multiplication identities involving one and zero */ - private static Expression simplifyMultiplication(Expression left, Expression right) { + private Expression simplifyMultiplication(Expression left, Expression right) { // x * 1 -> x if (isOne(right)) return left.clone(); @@ -216,7 +197,7 @@ private static Expression simplifyMultiplication(Expression left, Expression rig /** * Applies division identities, using prior non-zero premises when needed */ - private static Expression simplifyDivision(Expression left, Expression right, List nonZeroExpressions) { + private Expression simplifyDivision(Expression left, Expression right, List nonZeroExpressions) { // x / 1 -> x if (isOne(right)) return left.clone(); @@ -232,7 +213,7 @@ private static Expression simplifyDivision(Expression left, Expression right, Li /** * Applies modulo identities, using prior non-zero premises when needed */ - private static Expression simplifyModulo(Expression left, Expression right, List nonZeroExpressions) { + private Expression simplifyModulo(Expression left, Expression right, List nonZeroExpressions) { // x % 1 -> 0 if (isOne(right)) return new LiteralInt(0); @@ -245,7 +226,7 @@ private static Expression simplifyModulo(Expression left, Expression right, List /** * Records direct non-zero premises shaped as x != 0 or 0 != x */ - private static void addNonZeroExpression(Expression expression, List nonZeroExpressions) { + private void addNonZeroExpression(Expression expression, List nonZeroExpressions) { if (!(expression instanceof BinaryExpression binary) || !"!=".equals(binary.getOperator())) return; @@ -260,14 +241,14 @@ private static void addNonZeroExpression(Expression expression, List /** * Checks whether a previous premise recorded an expression as non-zero */ - private static boolean isNonZero(Expression expression, List nonZeroExpressions) { + private boolean isNonZero(Expression expression, List nonZeroExpressions) { return nonZeroExpressions.stream().anyMatch(e -> e.equals(expression)); } /** * Checks whether an expression is a numeric zero literal */ - private static boolean isZero(Expression expression) { + private boolean isZero(Expression expression) { if (expression instanceof LiteralInt literal) return literal.getValue() == 0; if (expression instanceof LiteralReal literal) @@ -278,7 +259,7 @@ private static boolean isZero(Expression expression) { /** * Checks whether an expression is a numeric one literal */ - private static boolean isOne(Expression expression) { + private boolean isOne(Expression expression) { if (expression instanceof LiteralInt literal) return literal.getValue() == 1; if (expression instanceof LiteralReal literal) @@ -289,14 +270,14 @@ private static boolean isOne(Expression expression) { /** * Checks whether an expression is unary negation */ - private static boolean isNegation(Expression expression) { + private boolean isNegation(Expression expression) { return expression instanceof UnaryExpression unary && "-".equals(unary.getOp()); } /** * Returns the operand of a unary negation expression */ - private static Expression negatedExpression(Expression expression) { + private Expression negatedExpression(Expression expression) { return ((UnaryExpression) expression).getExpression(); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCExpressionSimplificationPass.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCExpressionSimplificationPass.java new file mode 100644 index 00000000..c4baf16a --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCExpressionSimplificationPass.java @@ -0,0 +1,48 @@ +package liquidjava.rj_language.opt; + +import liquidjava.processor.SimplifiedVCImplication; +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; + +/** + * Base implementation for passes that simplify one refinement expression at a time. + */ +abstract class VCExpressionSimplificationPass implements VCSimplificationPass { + + @Override + public final VCImplication apply(VCImplication implication) { + return apply(implication, initialContext()); + } + + protected C initialContext() { + return null; + } + + protected C nextContext(C context, VCImplication implication) { + return context; + } + + protected abstract Expression simplify(Expression expression, C context); + + private VCImplication apply(VCImplication implication, C context) { + if (implication == null) + return null; + + Expression expression = implication.getRefinement().getExpression(); + Expression simplified = simplify(expression, context); + if (!expression.equals(simplified)) { + VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), implication); + result.setNext(implication.getNext() == null ? null : implication.getNext().clone()); + return result; + } + + VCImplication next = apply(implication.getNext(), nextContext(context, implication)); + if (implication.getNext() == null || implication.getNext().equals(next)) + return implication; + + VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone()); + result.setNext(next); + return result; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java index a8927f2b..eaa4760d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java @@ -1,8 +1,5 @@ package liquidjava.rj_language.opt; -import liquidjava.processor.SimplifiedVCImplication; -import liquidjava.processor.VCImplication; -import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Enum; import liquidjava.rj_language.ast.Expression; @@ -16,36 +13,17 @@ /** * Simplifies VCImplication chains by folding constant expressions and other foldable patterns inside refinements */ -public class VCFolding { +public class VCFolding extends VCExpressionSimplificationPass { - /** - * Applies folding to the first foldable predicate in a VC chain - */ - public static VCImplication apply(VCImplication implication) { - if (implication == null) - return null; - - Expression expression = implication.getRefinement().getExpression(); - Expression folded = fold(expression); - if (!expression.equals(folded)) { - VCImplication result = new SimplifiedVCImplication(implication, new Predicate(folded), implication); - result.setNext(implication.getNext() == null ? null : implication.getNext().clone()); - return result; - } - - VCImplication next = apply(implication.getNext()); - if (implication.getNext() == null || implication.getNext().equals(next)) - return implication; - - VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone()); - result.setNext(next); - return result; + @Override + protected Expression simplify(Expression expression, Void context) { + return fold(expression); } /** * Folds the first foldable expression found */ - private static Expression fold(Expression expression) { + private Expression fold(Expression expression) { // enum constant -> literal if (expression instanceof Enum en && en.getResolvedLiteral() != null) return en.getResolvedLiteral().clone(); @@ -64,7 +42,7 @@ private static Expression fold(Expression expression) { /** * Folds a binary expression and its operands */ - private static Expression foldBinary(BinaryExpression binary) { + private Expression foldBinary(BinaryExpression binary) { Expression left = binary.getFirstOperand(); Expression foldedLeft = fold(left); if (!left.equals(foldedLeft)) @@ -91,7 +69,7 @@ private static Expression foldBinary(BinaryExpression binary) { /** * Folds a unary expression and its operand */ - private static Expression foldUnary(UnaryExpression unary) { + private Expression foldUnary(UnaryExpression unary) { Expression operand = unary.getExpression(); Expression foldedOperand = fold(operand); if (!operand.equals(foldedOperand)) @@ -118,7 +96,7 @@ private static Expression foldUnary(UnaryExpression unary) { /** * Folds a conditional expression and its branches */ - private static Expression foldIte(Ite ite) { + private Expression foldIte(Ite ite) { Expression condition = ite.getCondition(); Expression foldedCondition = fold(condition); if (!condition.equals(foldedCondition)) @@ -149,7 +127,7 @@ private static Expression foldIte(Ite ite) { /** * Folds a binary expression whose operands are both literals */ - private static Expression foldLiteralBinary(Expression left, Expression right, String op) { + private Expression foldLiteralBinary(Expression left, Expression right, String op) { if (left instanceof LiteralInt leftInt && right instanceof LiteralInt rightInt) return foldInts(leftInt.getValue(), rightInt.getValue(), op); @@ -183,7 +161,7 @@ private static Expression foldLiteralBinary(Expression left, Expression right, S /** * Combines adjacent integer constants in additions and subtractions */ - private static Expression foldAdjacentInts(Expression left, Expression right, String op) { + private Expression foldAdjacentInts(Expression left, Expression right, String op) { if (!"+".equals(op) && !"-".equals(op)) return null; if (!(right instanceof LiteralInt rightLiteral)) @@ -213,7 +191,7 @@ private static Expression foldAdjacentInts(Expression left, Expression right, St /** * Folds integer operations */ - private static Expression foldInts(int left, int right, String op) { + private Expression foldInts(int left, int right, String op) { return switch (op) { case "+" -> new LiteralInt(left + right); case "-" -> new LiteralInt(left - right); @@ -233,7 +211,7 @@ private static Expression foldInts(int left, int right, String op) { /** * Folds real number operations */ - private static Expression foldReals(double left, double right, String op) { + private Expression foldReals(double left, double right, String op) { return switch (op) { case "+" -> new LiteralReal(left + right); case "-" -> new LiteralReal(left - right); @@ -253,7 +231,7 @@ private static Expression foldReals(double left, double right, String op) { /** * Folds boolean operations */ - private static Expression foldBooleans(boolean left, boolean right, String op) { + private Expression foldBooleans(boolean left, boolean right, String op) { return switch (op) { case "&&" -> new LiteralBoolean(left && right); case "||" -> new LiteralBoolean(left || right); @@ -267,7 +245,7 @@ private static Expression foldBooleans(boolean left, boolean right, String op) { /** * Checks whether two expressions mix integer and real literals */ - private static boolean isMixedNumeric(Expression left, Expression right) { + private boolean isMixedNumeric(Expression left, Expression right) { return left instanceof LiteralInt && right instanceof LiteralReal || left instanceof LiteralReal && right instanceof LiteralInt; } @@ -275,7 +253,7 @@ private static boolean isMixedNumeric(Expression left, Expression right) { /** * Reads a numeric literal as a double */ - private static double numericValue(Expression expression) { + private double numericValue(Expression expression) { if (expression instanceof LiteralInt literal) return literal.getValue(); return ((LiteralReal) expression).getValue(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java index 743ad9a4..84c3b3ca 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java @@ -1,8 +1,5 @@ package liquidjava.rj_language.opt; -import liquidjava.processor.SimplifiedVCImplication; -import liquidjava.processor.VCImplication; -import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.GroupExpression; @@ -13,36 +10,17 @@ /** * Simplifies VCImplication chains by applying logical identities inside refinements */ -public class VCLogicalSimplification { +public class VCLogicalSimplification extends VCExpressionSimplificationPass { - /** - * Applies the first logical simplification available in a VC chain - */ - public static VCImplication apply(VCImplication implication) { - if (implication == null) - return null; - - Expression expression = implication.getRefinement().getExpression(); - Expression simplified = simplify(expression); - if (!expression.equals(simplified)) { - VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), implication); - result.setNext(implication.getNext() == null ? null : implication.getNext().clone()); - return result; - } - - VCImplication next = apply(implication.getNext()); - if (implication.getNext() == null || implication.getNext().equals(next)) - return implication; - - VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone()); - result.setNext(next); - return result; + @Override + protected Expression simplify(Expression expression, Void context) { + return simplify(expression); } /** * Simplifies the first logical identity found inside an expression */ - private static Expression simplify(Expression expression) { + private Expression simplify(Expression expression) { if (expression instanceof BinaryExpression binary) return simplifyBinary(binary); if (expression instanceof UnaryExpression unary) @@ -57,7 +35,7 @@ private static Expression simplify(Expression expression) { /** * Simplifies a binary expression by visiting operands before the current node */ - private static Expression simplifyBinary(BinaryExpression binary) { + private Expression simplifyBinary(BinaryExpression binary) { Expression left = binary.getFirstOperand(); Expression simplifiedLeft = simplify(left); if (!left.equals(simplifiedLeft)) @@ -78,7 +56,7 @@ private static Expression simplifyBinary(BinaryExpression binary) { /** * Simplifies a unary expression by visiting its operand before the current node */ - private static Expression simplifyUnary(UnaryExpression unary) { + private Expression simplifyUnary(UnaryExpression unary) { Expression operand = unary.getExpression(); Expression simplifiedOperand = simplify(operand); if (!operand.equals(simplifiedOperand)) @@ -94,7 +72,7 @@ private static Expression simplifyUnary(UnaryExpression unary) { /** * Simplifies a ternary expression by visiting condition, then branch, and else branch */ - private static Expression simplifyIte(Ite ite) { + private Expression simplifyIte(Ite ite) { Expression condition = ite.getCondition(); Expression simplifiedCondition = simplify(condition); if (!condition.equals(simplifiedCondition)) @@ -116,7 +94,7 @@ private static Expression simplifyIte(Ite ite) { /** * Simplifies an expression wrapped in parentheses while preserving the group node */ - private static Expression simplifyGroup(GroupExpression group) { + private Expression simplifyGroup(GroupExpression group) { Expression expression = group.getExpression(); Expression simplified = simplify(expression); if (!expression.equals(simplified)) @@ -127,7 +105,7 @@ private static Expression simplifyGroup(GroupExpression group) { /** * Dispatches a local binary logical identity by operator */ - private static Expression simplifyLocalBinary(Expression left, Expression right, String op) { + private Expression simplifyLocalBinary(Expression left, Expression right, String op) { return switch (op) { case "&&" -> simplifyConjunction(left, right); case "||" -> simplifyDisjunction(left, right); @@ -141,7 +119,7 @@ private static Expression simplifyLocalBinary(Expression left, Expression right, /** * Applies conjunction identities involving boolean literals and same operands */ - private static Expression simplifyConjunction(Expression left, Expression right) { + private Expression simplifyConjunction(Expression left, Expression right) { // x && true -> x if (isTrue(right)) return left.clone(); @@ -163,7 +141,7 @@ private static Expression simplifyConjunction(Expression left, Expression right) /** * Applies disjunction identities involving boolean literals and same operands */ - private static Expression simplifyDisjunction(Expression left, Expression right) { + private Expression simplifyDisjunction(Expression left, Expression right) { // x || true -> true if (isTrue(right)) return right.clone(); @@ -185,7 +163,7 @@ private static Expression simplifyDisjunction(Expression left, Expression right) /** * Applies equality identity for same operands */ - private static Expression simplifyEquality(Expression left, Expression right) { + private Expression simplifyEquality(Expression left, Expression right) { // x == x -> true if (left.equals(right)) return new LiteralBoolean(true); @@ -195,7 +173,7 @@ private static Expression simplifyEquality(Expression left, Expression right) { /** * Applies inequality identity for same operands */ - private static Expression simplifyInequality(Expression left, Expression right) { + private Expression simplifyInequality(Expression left, Expression right) { // x != x -> false if (left.equals(right)) return new LiteralBoolean(false); @@ -205,7 +183,7 @@ private static Expression simplifyInequality(Expression left, Expression right) /** * Applies implication identities involving boolean literals and same operands */ - private static Expression simplifyImplication(Expression left, Expression right) { + private Expression simplifyImplication(Expression left, Expression right) { // x --> true -> true if (isTrue(right)) return right.clone(); @@ -224,28 +202,28 @@ private static Expression simplifyImplication(Expression left, Expression right) /** * Checks whether an expression is true */ - private static boolean isTrue(Expression expression) { + private boolean isTrue(Expression expression) { return expression instanceof LiteralBoolean literal && literal.isBooleanTrue(); } /** * Checks whether an expression is false */ - private static boolean isFalse(Expression expression) { + private boolean isFalse(Expression expression) { return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue(); } /** * Checks whether an expression is unary logical negation */ - private static boolean isNot(Expression expression) { + private boolean isNot(Expression expression) { return expression instanceof UnaryExpression unary && "!".equals(unary.getOp()); } /** * Returns the operand of a unary logical negation expression */ - private static Expression negatedExpression(Expression expression) { + private Expression negatedExpression(Expression expression) { return ((UnaryExpression) expression).getExpression(); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java index 4c0dbec4..38eb7f3b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java @@ -1,7 +1,6 @@ package liquidjava.rj_language.opt; import java.util.List; -import java.util.function.UnaryOperator; import liquidjava.processor.VCImplication; @@ -10,8 +9,8 @@ */ public class VCSimplification { - private static final List> PASSES = List.of(VCSubstitution::apply, VCFolding::apply, - VCArithmeticSimplification::apply, VCLogicalSimplification::apply); + private static final List PASSES = List.of(new VCSubstitution(), new VCFolding(), + new VCArithmeticSimplification(), new VCLogicalSimplification()); /** * Applies all available simplification steps to a VC chain until a fixed point is reached @@ -37,7 +36,7 @@ public static VCImplication simplifyOnce(VCImplication implication) { if (implication == null) return null; - for (UnaryOperator pass : PASSES) { + for (VCSimplificationPass pass : PASSES) { VCImplication simplified = pass.apply(implication); if (!implication.equals(simplified)) return simplified; diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationPass.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationPass.java new file mode 100644 index 00000000..0d58cf68 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationPass.java @@ -0,0 +1,10 @@ +package liquidjava.rj_language.opt; + +import liquidjava.processor.VCImplication; + +/** + * Applies one simplification step to a VC implication chain. + */ +public interface VCSimplificationPass { + VCImplication apply(VCImplication implication); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java index 21133bc1..c5be0134 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSubstitution.java @@ -14,7 +14,7 @@ /** * Simplifies VCImplication chains by replacing binder equalities with their known values */ -public class VCSubstitution { +public class VCSubstitution implements VCSimplificationPass { /** * A substitution discovered from an implication node @@ -25,17 +25,15 @@ private record Substitution(VCImplication node, Expression replacement) { /** * Applies one substitution in a VC chain */ - public static VCImplication apply(VCImplication implication) { - if (implication == null) - return null; - + @Override + public VCImplication apply(VCImplication implication) { VCImplication result = implication.clone(); - Optional substitutionOpt = VCSubstitution.findSubstitution(result); + Optional substitutionOpt = findSubstitution(result); // apply only the first available substitution if (substitutionOpt.isPresent()) { - VCSubstitution.Substitution substitution = substitutionOpt.get(); - result = VCSubstitution.substitute(result, substitution.node(), substitution.replacement()); + Substitution substitution = substitutionOpt.get(); + result = substitute(result, substitution.node(), substitution.replacement()); } return result; } @@ -43,7 +41,7 @@ public static VCImplication apply(VCImplication implication) { /** * Rewrites one VC chain with a single substitution and removes its source node */ - private static VCImplication substitute(VCImplication implication, VCImplication node, Expression replacement) { + private VCImplication substitute(VCImplication implication, VCImplication node, Expression replacement) { if (implication == null) return null; @@ -60,7 +58,7 @@ private static VCImplication substitute(VCImplication implication, VCImplication /** * Substitutes a source binder inside one VC node while preserving simplification metadata */ - private static VCImplication substituteNode(VCImplication implication, VCImplication node, Expression replacement) { + private VCImplication substituteNode(VCImplication implication, VCImplication node, Expression replacement) { Expression exp = implication.getRefinement().getExpression().clone(); if (!containsVar(exp, node.getName())) return implication.copyWithRefinement(new Predicate(exp)); @@ -73,7 +71,7 @@ private static VCImplication substituteNode(VCImplication implication, VCImplica /** * Finds the first substitution candidate in the VC chain */ - private static Optional findSubstitution(VCImplication implication) { + private Optional findSubstitution(VCImplication implication) { if (implication == null) return Optional.empty(); @@ -87,7 +85,7 @@ private static Optional findSubstitution(VCImplication implication /** * Extracts a substitution from one binder equality */ - private static Optional getSubstitution(VCImplication implication) { + private Optional getSubstitution(VCImplication implication) { if (!implication.hasBinder()) return Optional.empty(); @@ -110,14 +108,14 @@ private static Optional getSubstitution(VCImplication implication) /** * Checks whether an expression is a variable with a given name */ - public static boolean isVar(Expression expression, String name) { + private boolean isVar(Expression expression, String name) { return expression instanceof Var var && name.equals(var.getName()); } /** * Checks whether an expression contains a variable name */ - public static boolean containsVar(Expression expression, String name) { + private boolean containsVar(Expression expression, String name) { List names = new ArrayList<>(); expression.getVariableNames(names); return names.contains(name); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java index 88440c49..1a9c09ac 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java @@ -3,7 +3,6 @@ import static liquidjava.utils.VCTestUtils.*; import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertInstanceOf; -import static org.junit.jupiter.api.Assertions.assertNull; import liquidjava.processor.SimplifiedVCImplication; import liquidjava.processor.VCImplication; @@ -11,78 +10,56 @@ class VCArithmeticSimplificationTest { - @Test - void applyReturnsNullForNullImplication() { - assertNull(VCArithmeticSimplification.apply(null)); - } + private final VCArithmeticSimplification simplification = new VCArithmeticSimplification(); @Test void simplifiesAdditiveIdentities() { - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x + 0 > 0"), - chain(expect("x > 0", "x + 0 > 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("0 + x > 0"), - chain(expect("x > 0", "0 + x > 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x - 0 > 0"), - chain(expect("x > 0", "x - 0 > 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("0 - x > 0"), - chain(expect("-x > 0", "0 - x > 0"))); + assertSimplificationSteps(simplification::apply, vc("x + 0 > 0"), chain(expect("x > 0", "x + 0 > 0"))); + assertSimplificationSteps(simplification::apply, vc("0 + x > 0"), chain(expect("x > 0", "0 + x > 0"))); + assertSimplificationSteps(simplification::apply, vc("x - 0 > 0"), chain(expect("x > 0", "x - 0 > 0"))); + assertSimplificationSteps(simplification::apply, vc("0 - x > 0"), chain(expect("-x > 0", "0 - x > 0"))); } @Test void simplifiesNegatedAdditionAndSubtraction() { - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x + -x == 0"), - chain(expect("0 == 0", "x + -x == 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("-x + x == 0"), - chain(expect("0 == 0", "-x + x == 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x - x == 0"), - chain(expect("0 == 0", "x - x == 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("--x == x"), - chain(expect("x == x", "-(-x) == x"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x + -y == 0"), - chain(expect("x - y == 0", "x + -y == 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x - -y == 0"), - chain(expect("x + y == 0", "x - -y == 0"))); + assertSimplificationSteps(simplification::apply, vc("x + -x == 0"), chain(expect("0 == 0", "x + -x == 0"))); + assertSimplificationSteps(simplification::apply, vc("-x + x == 0"), chain(expect("0 == 0", "-x + x == 0"))); + assertSimplificationSteps(simplification::apply, vc("x - x == 0"), chain(expect("0 == 0", "x - x == 0"))); + assertSimplificationSteps(simplification::apply, vc("--x == x"), chain(expect("x == x", "-(-x) == x"))); + assertSimplificationSteps(simplification::apply, vc("x + -y == 0"), chain(expect("x - y == 0", "x + -y == 0"))); + assertSimplificationSteps(simplification::apply, vc("x - -y == 0"), chain(expect("x + y == 0", "x - -y == 0"))); } @Test void simplifiesMultiplicativeIdentities() { - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x * 1 > 0"), - chain(expect("x > 0", "x * 1 > 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("1 * x > 0"), - chain(expect("x > 0", "1 * x > 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x * 0 == 0"), - chain(expect("0 == 0", "x * 0 == 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("0 * x == 0"), - chain(expect("0 == 0", "0 * x == 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x / 1 > 0"), - chain(expect("x > 0", "x / 1 > 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x % 1 == 0"), - chain(expect("0 == 0", "x % 1 == 0"))); + assertSimplificationSteps(simplification::apply, vc("x * 1 > 0"), chain(expect("x > 0", "x * 1 > 0"))); + assertSimplificationSteps(simplification::apply, vc("1 * x > 0"), chain(expect("x > 0", "1 * x > 0"))); + assertSimplificationSteps(simplification::apply, vc("x * 0 == 0"), chain(expect("0 == 0", "x * 0 == 0"))); + assertSimplificationSteps(simplification::apply, vc("0 * x == 0"), chain(expect("0 == 0", "0 * x == 0"))); + assertSimplificationSteps(simplification::apply, vc("x / 1 > 0"), chain(expect("x > 0", "x / 1 > 0"))); + assertSimplificationSteps(simplification::apply, vc("x % 1 == 0"), chain(expect("0 == 0", "x % 1 == 0"))); } @Test void simplifiesGuardedDivisionAndModuloIdentities() { - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x != 0", "0 / x == 0"), + assertSimplificationSteps(simplification::apply, vc("x != 0", "0 / x == 0"), chain(expect("x != 0", "x != 0"), expect("0 == 0", "0 / x == 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x != 0", "x / x == 1"), + assertSimplificationSteps(simplification::apply, vc("x != 0", "x / x == 1"), chain(expect("x != 0", "x != 0"), expect("1 == 1", "x / x == 1"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("0 != x", "x % x == 0"), + assertSimplificationSteps(simplification::apply, vc("0 != x", "x % x == 0"), chain(expect("0 != x", "0 != x"), expect("0 == 0", "x % x == 0"))); } @Test void leavesUnguardedDivisionAndModuloIdentitiesUnchanged() { - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("0 / x == 0"), - chain(expect("0 / x == 0", "0 / x == 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x / x == 1"), - chain(expect("x / x == 1", "x / x == 1"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x % x == 0"), - chain(expect("x % x == 0", "x % x == 0"))); + assertSimplificationSteps(simplification::apply, vc("0 / x == 0"), chain(expect("0 / x == 0", "0 / x == 0"))); + assertSimplificationSteps(simplification::apply, vc("x / x == 1"), chain(expect("x / x == 1", "x / x == 1"))); + assertSimplificationSteps(simplification::apply, vc("x % x == 0"), chain(expect("x % x == 0", "x % x == 0"))); } @Test void simplifiesOnlyFirstArithmeticIdentity() { - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x + 0 + 1 > 0"), + assertSimplificationSteps(simplification::apply, vc("x + 0 + 1 > 0"), chain(expect("x + 1 > 0", "x + 0 + 1 > 0"))); } @@ -90,17 +67,10 @@ void simplifiesOnlyFirstArithmeticIdentity() { void recordsOriginWhenSimplifyingLaterImplication() { VCImplication implication = vc("x > 0", "y + 0 > x"); - VCImplication result = assertSimplificationSteps(VCArithmeticSimplification::apply, implication, + VCImplication result = assertSimplificationSteps(simplification::apply, implication, chain(expect("x > 0", "x > 0"), expect("y > x", "y + 0 > x"))); SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); assertEquals("y + 0 > x", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); } - - @Test - void recordsCurrentImplicationAsOriginWhenSimplifyingExistingSimplifiedImplication() { - VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == y + 0", "x > 0")); - - assertSimplificationSteps(VCArithmeticSimplification::apply, substituted, chain(expect("y > 0", "y + 0 > 0"))); - } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java index b73bd8ec..9d6f3e0c 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java @@ -3,7 +3,6 @@ import static liquidjava.utils.VCTestUtils.*; import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertInstanceOf; -import static org.junit.jupiter.api.Assertions.assertNull; import liquidjava.processor.SimplifiedVCImplication; import liquidjava.processor.VCImplication; @@ -16,18 +15,15 @@ class VCFoldingTest { - @Test - void applyReturnsNullForNullImplication() { - assertNull(VCFolding.apply(null)); - } + private final VCFolding folding = new VCFolding(); @Test void foldsIntegerArithmeticAndComparisons() { VCImplication implication = vc("1 + 2 == 3"); - assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 == 3", "1 + 2 == 3")), + assertSimplificationSteps(folding::apply, implication, chain(expect("3 == 3", "1 + 2 == 3")), chain(expect("true", "3 == 3"))); - assertSimplificationSteps(VCFolding::apply, vc("4 > 7"), chain(expect("false", "4 > 7"))); + assertSimplificationSteps(folding::apply, vc("4 > 7"), chain(expect("false", "4 > 7"))); } @Test @@ -35,23 +31,23 @@ void foldsRealAndMixedNumericExpressions() { VCImplication realArithmetic = vc("1.5 + 2.0 == 3.5"); VCImplication mixedArithmetic = vc("2 + 0.5 > 2"); - assertSimplificationSteps(VCFolding::apply, realArithmetic, chain(expect("3.5 == 3.5", "1.5 + 2.0 == 3.5")), + assertSimplificationSteps(folding::apply, realArithmetic, chain(expect("3.5 == 3.5", "1.5 + 2.0 == 3.5")), chain(expect("true", "3.5 == 3.5"))); - assertSimplificationSteps(VCFolding::apply, mixedArithmetic, chain(expect("2.5 > 2", "2 + 0.5 > 2")), + assertSimplificationSteps(folding::apply, mixedArithmetic, chain(expect("2.5 > 2", "2 + 0.5 > 2")), chain(expect("true", "2.5 > 2"))); } @Test void leavesDivisionAndModuloByZeroUnchanged() { - assertSimplificationSteps(VCFolding::apply, vc("4 / 0 == 0"), chain(expect("4 / 0 == 0", "4 / 0 == 0"))); - assertSimplificationSteps(VCFolding::apply, vc("4 % 0 == 0"), chain(expect("4 % 0 == 0", "4 % 0 == 0"))); + assertSimplificationSteps(folding::apply, vc("4 / 0 == 0"), chain(expect("4 / 0 == 0", "4 / 0 == 0"))); + assertSimplificationSteps(folding::apply, vc("4 % 0 == 0"), chain(expect("4 % 0 == 0", "4 % 0 == 0"))); } @Test void leavesRealDivisionAndModuloByZeroUnchanged() { - assertSimplificationSteps(VCFolding::apply, vc("4.0 / 0.0 == 0.0"), + assertSimplificationSteps(folding::apply, vc("4.0 / 0.0 == 0.0"), chain(expect("4.0 / 0.0 == 0.0", "4.0 / 0.0 == 0.0"))); - assertSimplificationSteps(VCFolding::apply, vc("4.0 % 0.0 == 0.0"), + assertSimplificationSteps(folding::apply, vc("4.0 % 0.0 == 0.0"), chain(expect("4.0 % 0.0 == 0.0", "4.0 % 0.0 == 0.0"))); } @@ -59,8 +55,7 @@ void leavesRealDivisionAndModuloByZeroUnchanged() { void foldsIntegerDivisionTowardZeroForNegativeResults() { VCImplication implication = vc("(2 - 7) / 2 == -2"); - assertSimplificationSteps(VCFolding::apply, implication, - chain(expect("(2 - 7) / 2 == -2", "(2 - 7) / 2 == -2")), + assertSimplificationSteps(folding::apply, implication, chain(expect("(2 - 7) / 2 == -2", "(2 - 7) / 2 == -2")), chain(expect("-5 / 2 == -2", "(2 - 7) / 2 == -2")), chain(expect("-2 == -2", "-5 / 2 == -2")), chain(expect("-2 == -2", "-2 == -2")), chain(expect("true", "-2 == -2"))); } @@ -70,73 +65,73 @@ void foldsIntegerModuloWithJavaSignedRemainder() { VCImplication negativeDividend = vc("-5 % 2 < 0"); VCImplication negativeDivisor = vc("5 % -2 > 0"); - assertSimplificationSteps(VCFolding::apply, negativeDividend, chain(expect("-5 % 2 < 0", "-5 % 2 < 0")), + assertSimplificationSteps(folding::apply, negativeDividend, chain(expect("-5 % 2 < 0", "-5 % 2 < 0")), chain(expect("-1 < 0", "-5 % 2 < 0")), chain(expect("true", "-1 < 0"))); - assertSimplificationSteps(VCFolding::apply, negativeDivisor, chain(expect("5 % -2 > 0", "5 % -2 > 0")), + assertSimplificationSteps(folding::apply, negativeDivisor, chain(expect("5 % -2 > 0", "5 % -2 > 0")), chain(expect("1 > 0", "5 % -2 > 0")), chain(expect("true", "1 > 0"))); } @Test void foldsBooleanBinaryExpressions() { - assertSimplificationSteps(VCFolding::apply, vc("true && false"), chain(expect("false", "true && false"))); - assertSimplificationSteps(VCFolding::apply, vc("false --> true"), chain(expect("true", "false --> true"))); - assertSimplificationSteps(VCFolding::apply, vc("true != false"), chain(expect("true", "true != false"))); + assertSimplificationSteps(folding::apply, vc("true && false"), chain(expect("false", "true && false"))); + assertSimplificationSteps(folding::apply, vc("false --> true"), chain(expect("true", "false --> true"))); + assertSimplificationSteps(folding::apply, vc("true != false"), chain(expect("true", "true != false"))); } @Test void foldsBooleanSubexpressionsInsideLargerExpression() { - assertSimplificationSteps(VCFolding::apply, vc("true && false || ok"), + assertSimplificationSteps(folding::apply, vc("true && false || ok"), chain(expect("false || ok", "true && false || ok"))); } @Test void foldsNestedConstantsInsideLargerExpression() { - assertSimplificationSteps(VCFolding::apply, vc("x > 1 + 2"), chain(expect("x > 3", "x > 1 + 2"))); - assertSimplificationSteps(VCFolding::apply, vc("x + 1 + 2 > 4"), chain(expect("x + 3 > 4", "x + 1 + 2 > 4"))); + assertSimplificationSteps(folding::apply, vc("x > 1 + 2"), chain(expect("x > 3", "x > 1 + 2"))); + assertSimplificationSteps(folding::apply, vc("x + 1 + 2 > 4"), chain(expect("x + 3 > 4", "x + 1 + 2 > 4"))); } @Test void foldsPartialComparisonsWithoutDroppingSymbolicTerms() { - assertSimplificationSteps(VCFolding::apply, vc("1 + 2 < x + 4"), chain(expect("3 < x + 4", "1 + 2 < x + 4"))); + assertSimplificationSteps(folding::apply, vc("1 + 2 < x + 4"), chain(expect("3 < x + 4", "1 + 2 < x + 4"))); } @Test void foldsUnaryExpressions() { - assertSimplificationSteps(VCFolding::apply, vc("!true"), chain(expect("false", "!true"))); + assertSimplificationSteps(folding::apply, vc("!true"), chain(expect("false", "!true"))); VCImplication implication = vc("-3 < 0"); - assertSimplificationSteps(VCFolding::apply, implication, chain(expect("-3 < 0", "-3 < 0")), + assertSimplificationSteps(folding::apply, implication, chain(expect("-3 < 0", "-3 < 0")), chain(expect("true", "-3 < 0"))); } @Test void foldsIteExpressions() { - assertSimplificationSteps(VCFolding::apply, vc("true ? a : b"), chain(expect("a", "true ? a : b"))); - assertSimplificationSteps(VCFolding::apply, vc("false ? a : b"), chain(expect("b", "false ? a : b"))); - assertSimplificationSteps(VCFolding::apply, vc("cond ? b : b"), chain(expect("b", "cond ? b : b"))); + assertSimplificationSteps(folding::apply, vc("true ? a : b"), chain(expect("a", "true ? a : b"))); + assertSimplificationSteps(folding::apply, vc("false ? a : b"), chain(expect("b", "false ? a : b"))); + assertSimplificationSteps(folding::apply, vc("cond ? b : b"), chain(expect("b", "cond ? b : b"))); } @Test void foldsIteBranchesBeforeComparingThem() { VCImplication implication = vc("cond ? 1 + 2 : 3"); - assertSimplificationSteps(VCFolding::apply, implication, chain(expect("cond ? 3 : 3", "cond ? 1 + 2 : 3")), + assertSimplificationSteps(folding::apply, implication, chain(expect("cond ? 3 : 3", "cond ? 1 + 2 : 3")), chain(expect("3", "cond ? 3 : 3"))); } @Test void foldsAdjacentIntegerConstants() { - assertSimplificationSteps(VCFolding::apply, vc("x + 1 - 2"), chain(expect("x - 1", "x + 1 - 2"))); - assertSimplificationSteps(VCFolding::apply, vc("x - 1 + 2"), chain(expect("x + 1", "x - 1 + 2"))); - assertSimplificationSteps(VCFolding::apply, vc("x + 1 + 2"), chain(expect("x + 3", "x + 1 + 2"))); - assertSimplificationSteps(VCFolding::apply, vc("x + 1 - 1"), chain(expect("x", "x + 1 - 1"))); + assertSimplificationSteps(folding::apply, vc("x + 1 - 2"), chain(expect("x - 1", "x + 1 - 2"))); + assertSimplificationSteps(folding::apply, vc("x - 1 + 2"), chain(expect("x + 1", "x - 1 + 2"))); + assertSimplificationSteps(folding::apply, vc("x + 1 + 2"), chain(expect("x + 3", "x + 1 + 2"))); + assertSimplificationSteps(folding::apply, vc("x + 1 - 1"), chain(expect("x", "x + 1 - 1"))); } @Test void foldsEnumEqualityAndInequality() { - assertSimplificationSteps(VCFolding::apply, vc("Mode.Photo == Mode.Photo"), + assertSimplificationSteps(folding::apply, vc("Mode.Photo == Mode.Photo"), chain(expect("true", "Mode.Photo == Mode.Photo"))); - assertSimplificationSteps(VCFolding::apply, vc("Mode.Photo != Mode.Video"), + assertSimplificationSteps(folding::apply, vc("Mode.Photo != Mode.Video"), chain(expect("true", "Mode.Photo != Mode.Video"))); } @@ -147,7 +142,7 @@ void foldsResolvedEnumLiterals() { VCImplication implication = new VCImplication( new Predicate(new BinaryExpression(limit, "==", new LiteralInt(3)))); - assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 == 3", "Config.LIMIT == 3")), + assertSimplificationSteps(folding::apply, implication, chain(expect("3 == 3", "Config.LIMIT == 3")), chain(expect("true", "3 == 3"))); } @@ -159,23 +154,14 @@ void foldsResolvedEnumLiteralsInsideLargerExpression() { VCImplication implication = new VCImplication( new Predicate(new BinaryExpression(arithmetic, "==", new LiteralInt(5)))); - assertSimplificationSteps(VCFolding::apply, implication, chain(expect("3 + 2 == 5", "Config.LIMIT + 2 == 5")), + assertSimplificationSteps(folding::apply, implication, chain(expect("3 + 2 == 5", "Config.LIMIT + 2 == 5")), chain(expect("5 == 5", "3 + 2 == 5")), chain(expect("true", "5 == 5"))); } - @Test - void recordsCurrentImplicationAsOriginWhenFoldingExistingSimplifiedImplication() { - VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == 1", "x + 1 + 2 > 0")); - - assertSimplificationSteps(VCFolding::apply, substituted, chain(expect("2 + 2 > 0", "1 + 1 + 2 > 0")), - chain(expect("4 > 0", "2 + 2 > 0")), chain(expect("true", "4 > 0"))); - } - @Test void recordsOriginWhenOnlyGroupIsUnwrapped() { VCImplication implication = vc("(x > 0)"); - VCImplication result = assertSimplificationSteps(VCFolding::apply, implication, - chain(expect("x > 0", "x > 0"))); + VCImplication result = assertSimplificationSteps(folding::apply, implication, chain(expect("x > 0", "x > 0"))); SimplifiedVCImplication simplified = assertInstanceOf(SimplifiedVCImplication.class, result); assertEquals("x > 0", simplified.getRefinement().toString()); @@ -186,13 +172,13 @@ void recordsOriginWhenOnlyGroupIsUnwrapped() { void recordsOriginWhenFoldingLaterImplication() { VCImplication implication = vc("x > 0", "1 + 2 > 0"); - VCImplication result = assertSimplificationSteps(VCFolding::apply, implication, + VCImplication result = assertSimplificationSteps(folding::apply, implication, chain(expect("x > 0", "x > 0"), expect("3 > 0", "1 + 2 > 0"))); SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); assertEquals("1 + 2 > 0", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); - result = assertSimplificationSteps(VCFolding::apply, result, + result = assertSimplificationSteps(folding::apply, result, chain(expect("x > 0", "x > 0"), expect("true", "3 > 0"))); simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java index 47b51438..7712e630 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java @@ -3,7 +3,6 @@ import static liquidjava.utils.VCTestUtils.*; import static org.junit.jupiter.api.Assertions.assertEquals; import static org.junit.jupiter.api.Assertions.assertInstanceOf; -import static org.junit.jupiter.api.Assertions.assertNull; import liquidjava.processor.SimplifiedVCImplication; import liquidjava.processor.VCImplication; @@ -11,71 +10,64 @@ class VCLogicalSimplificationTest { - @Test - void applyReturnsNullForNullImplication() { - assertNull(VCLogicalSimplification.apply(null)); - } + private final VCLogicalSimplification simplification = new VCLogicalSimplification(); @Test void simplifiesConjunctionWithBooleanLiterals() { - assertSimplificationSteps(VCLogicalSimplification::apply, vc("x && true"), chain(expect("x", "x && true"))); - assertSimplificationSteps(VCLogicalSimplification::apply, vc("true && x"), chain(expect("x", "true && x"))); - assertSimplificationSteps(VCLogicalSimplification::apply, vc("x && false"), - chain(expect("false", "x && false"))); - assertSimplificationSteps(VCLogicalSimplification::apply, vc("false && x"), - chain(expect("false", "false && x"))); + assertSimplificationSteps(simplification::apply, vc("x && true"), chain(expect("x", "x && true"))); + assertSimplificationSteps(simplification::apply, vc("true && x"), chain(expect("x", "true && x"))); + assertSimplificationSteps(simplification::apply, vc("x && false"), chain(expect("false", "x && false"))); + assertSimplificationSteps(simplification::apply, vc("false && x"), chain(expect("false", "false && x"))); } @Test void simplifiesDisjunctionWithBooleanLiterals() { - assertSimplificationSteps(VCLogicalSimplification::apply, vc("x || true"), chain(expect("true", "x || true"))); - assertSimplificationSteps(VCLogicalSimplification::apply, vc("true || x"), chain(expect("true", "true || x"))); - assertSimplificationSteps(VCLogicalSimplification::apply, vc("x || false"), chain(expect("x", "x || false"))); - assertSimplificationSteps(VCLogicalSimplification::apply, vc("false || x"), chain(expect("x", "false || x"))); + assertSimplificationSteps(simplification::apply, vc("x || true"), chain(expect("true", "x || true"))); + assertSimplificationSteps(simplification::apply, vc("true || x"), chain(expect("true", "true || x"))); + assertSimplificationSteps(simplification::apply, vc("x || false"), chain(expect("x", "x || false"))); + assertSimplificationSteps(simplification::apply, vc("false || x"), chain(expect("x", "false || x"))); } @Test void simplifiesDoubleNegation() { - assertSimplificationSteps(VCLogicalSimplification::apply, vc("!!x"), chain(expect("x", "!!x"))); + assertSimplificationSteps(simplification::apply, vc("!!x"), chain(expect("x", "!!x"))); } @Test void simplifiesDuplicateLogicalOperands() { - assertSimplificationSteps(VCLogicalSimplification::apply, vc("p && p"), chain(expect("p", "p && p"))); - assertSimplificationSteps(VCLogicalSimplification::apply, vc("p || p"), chain(expect("p", "p || p"))); + assertSimplificationSteps(simplification::apply, vc("p && p"), chain(expect("p", "p && p"))); + assertSimplificationSteps(simplification::apply, vc("p || p"), chain(expect("p", "p || p"))); } @Test void simplifiesSelfEqualityAndInequality() { - assertSimplificationSteps(VCLogicalSimplification::apply, vc("x == x"), chain(expect("true", "x == x"))); - assertSimplificationSteps(VCLogicalSimplification::apply, vc("x != x"), chain(expect("false", "x != x"))); + assertSimplificationSteps(simplification::apply, vc("x == x"), chain(expect("true", "x == x"))); + assertSimplificationSteps(simplification::apply, vc("x != x"), chain(expect("false", "x != x"))); } @Test void simplifiesImplicationIdentities() { - assertSimplificationSteps(VCLogicalSimplification::apply, vc("x --> true"), - chain(expect("true", "x --> true"))); - assertSimplificationSteps(VCLogicalSimplification::apply, vc("false --> x"), - chain(expect("true", "false --> x"))); - assertSimplificationSteps(VCLogicalSimplification::apply, vc("true --> x"), chain(expect("x", "true --> x"))); - assertSimplificationSteps(VCLogicalSimplification::apply, vc("x --> x"), chain(expect("true", "x --> x"))); + assertSimplificationSteps(simplification::apply, vc("x --> true"), chain(expect("true", "x --> true"))); + assertSimplificationSteps(simplification::apply, vc("false --> x"), chain(expect("true", "false --> x"))); + assertSimplificationSteps(simplification::apply, vc("true --> x"), chain(expect("x", "true --> x"))); + assertSimplificationSteps(simplification::apply, vc("x --> x"), chain(expect("true", "x --> x"))); } @Test void simplifiesOnlyFirstLogicalIdentity() { - assertSimplificationSteps(VCLogicalSimplification::apply, vc("x && true && false"), + assertSimplificationSteps(simplification::apply, vc("x && true && false"), chain(expect("x && false", "x && true && false"))); } @Test void simplifiesNestedExpressionsBeforeParent() { - assertSimplificationSteps(VCLogicalSimplification::apply, vc("(x && true) || false"), + assertSimplificationSteps(simplification::apply, vc("(x && true) || false"), chain(expect("x || false", "x && true || false"))); } @Test void simplifiesIteChildren() { - assertSimplificationSteps(VCLogicalSimplification::apply, vc("cond ? x && true : y || false"), + assertSimplificationSteps(simplification::apply, vc("cond ? x && true : y || false"), chain(expect("cond ? x : y || false", "cond ? x && true : y || false"))); } @@ -83,17 +75,10 @@ void simplifiesIteChildren() { void recordsOriginWhenSimplifyingLaterImplication() { VCImplication implication = vc("x > 0", "y || false"); - VCImplication result = assertSimplificationSteps(VCLogicalSimplification::apply, implication, + VCImplication result = assertSimplificationSteps(simplification::apply, implication, chain(expect("x > 0", "x > 0"), expect("y", "y || false"))); SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); assertEquals("y || false", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); } - - @Test - void recordsCurrentImplicationAsOriginWhenSimplifyingExistingSimplifiedImplication() { - VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == y", "x == x")); - - assertSimplificationSteps(VCLogicalSimplification::apply, substituted, chain(expect("true", "y == y"))); - } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java index c20fc106..8a638ddc 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationPropertyBasedTest.java @@ -1,10 +1,11 @@ package liquidjava.rj_language.opt; -import static liquidjava.rj_language.opt.VCSubstitution.containsVar; -import static liquidjava.rj_language.opt.VCSubstitution.isVar; import static org.junit.jupiter.api.Assertions.assertTrue; import static org.junit.jupiter.api.Assertions.fail; +import java.util.ArrayList; +import java.util.List; + import com.pholser.junit.quickcheck.From; import com.pholser.junit.quickcheck.Property; import com.pholser.junit.quickcheck.runner.JUnitQuickcheck; @@ -13,6 +14,7 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.Var; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.SMTResult; import liquidjava.utils.TestUtils; @@ -87,6 +89,16 @@ private static boolean isSubstitution(VCImplication implication) { return isVar(left, name) && !containsVar(right, name) || isVar(right, name) && !containsVar(left, name); } + private static boolean isVar(Expression expression, String name) { + return expression instanceof Var var && name.equals(var.getName()); + } + + private static boolean containsVar(Expression expression, String name) { + List names = new ArrayList<>(); + expression.getVariableNames(names); + return names.contains(name); + } + private static void assertImplies(Predicate antecedent, Predicate consequent, VCImplication unsimplified, VCImplication simplified, int step, String direction) { try { diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java index afe8b60f..d5669358 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSubstitutionTest.java @@ -1,58 +1,54 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; -import static org.junit.jupiter.api.Assertions.assertNull; import liquidjava.processor.VCImplication; import org.junit.jupiter.api.Test; class VCSubstitutionTest { - @Test - void applyReturnsNullForNullImplication() { - assertNull(VCSubstitution.apply(null)); - } + private final VCSubstitution substitution = new VCSubstitution(); @Test void substitutesBinderEqualityIntoWholeChain() { VCImplication implication = vc("∀x:int. x == 3", "x > 0"); - assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("3 > 0", "∀x:int. x > 0"))); + assertSimplificationSteps(substitution::apply, implication, chain(expect("3 > 0", "∀x:int. x > 0"))); } @Test void substitutesReverseBinderEquality() { VCImplication implication = vc("∀x:int. 3 == x", "x > 0"); - assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("3 > 0", "∀x:int. x > 0"))); + assertSimplificationSteps(substitution::apply, implication, chain(expect("3 > 0", "∀x:int. x > 0"))); } @Test void substitutesCompoundKnownValue() { VCImplication implication = vc("∀x:int. x == y + 1", "x > y"); - assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("y + 1 > y", "∀x:int. x > y"))); + assertSimplificationSteps(substitution::apply, implication, chain(expect("y + 1 > y", "∀x:int. x > y"))); } @Test void substitutesOnlyWholeVariableReferences() { VCImplication implication = vc("∀x:int. x == 3", "xx > x"); - assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("xx > 3", "∀x:int. xx > x"))); + assertSimplificationSteps(substitution::apply, implication, chain(expect("xx > 3", "∀x:int. xx > x"))); } @Test void substitutesEveryOccurrenceInPredicate() { VCImplication implication = vc("∀x:int. x == 2", "x + x > 0"); - assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("2 + 2 > 0", "∀x:int. x + x > 0"))); + assertSimplificationSteps(substitution::apply, implication, chain(expect("2 + 2 > 0", "∀x:int. x + x > 0"))); } @Test void preservesRemainingBinderAfterSubstitution() { VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y > x", "y > 0"); - assertSimplificationSteps(VCSubstitution::apply, implication, + assertSimplificationSteps(substitution::apply, implication, chain(expect("y > 3", "∀x:int. y > x"), expect("y > 0", "y > 0"))); } @@ -60,14 +56,14 @@ void preservesRemainingBinderAfterSubstitution() { void removesSourceNodeWhenItIsLastInChain() { VCImplication implication = vc("x > 0", "∀y:int. y == 1"); - assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("x > 0", "x > 0"))); + assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 0", "x > 0"))); } @Test void usesFirstSubstitutionFoundInChain() { VCImplication implication = vc("∀x:int. x > 0", "∀y:int. y == 4", "x + y > 0"); - assertSimplificationSteps(VCSubstitution::apply, implication, + assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 0", "∀x:int. x > 0"), expect("x + 4 > 0", "∀y:int. x + y > 0"))); } @@ -75,7 +71,7 @@ void usesFirstSubstitutionFoundInChain() { void substitutesInnerKnownValueAcrossNestedImplications() { VCImplication implication = vc("∀x:int. true", "∀y:int. y == 1", "∀z:int. z > y", "y + z > 0"); - assertSimplificationSteps(VCSubstitution::apply, implication, chain(expect("true", "∀x:int. true"), + assertSimplificationSteps(substitution::apply, implication, chain(expect("true", "∀x:int. true"), expect("z > 1", "∀y:int. z > y"), expect("1 + z > 0", "∀y:int. y + z > 0"))); } @@ -83,7 +79,7 @@ void substitutesInnerKnownValueAcrossNestedImplications() { void substitutesOuterKnownValueIntoNestedBinderRefinements() { VCImplication implication = vc("∀x:int. x == 3", "∀y:int. y == x + 1", "y > x"); - assertSimplificationSteps(VCSubstitution::apply, implication, + assertSimplificationSteps(substitution::apply, implication, chain(expect("y == 3 + 1", "∀x:int. y == x + 1"), expect("y > 3", "∀x:int. y > x")), chain(expect("3 + 1 > 3", "∀y:int. y > x"))); } @@ -92,7 +88,7 @@ void substitutesOuterKnownValueIntoNestedBinderRefinements() { void ignoresRecursiveBinderEquality() { VCImplication implication = vc("∀x:int. x == x + 1", "x > 0"); - assertSimplificationSteps(VCSubstitution::apply, implication, + assertSimplificationSteps(substitution::apply, implication, chain(expect("x == x + 1", "∀x:int. x == x + 1"), expect("x > 0", "x > 0"))); } @@ -100,7 +96,7 @@ void ignoresRecursiveBinderEquality() { void ignoresNonEqualityBinderRefinement() { VCImplication implication = vc("∀x:int. x > 3", "x > 0"); - assertSimplificationSteps(VCSubstitution::apply, implication, + assertSimplificationSteps(substitution::apply, implication, chain(expect("x > 3", "∀x:int. x > 3"), expect("x > 0", "x > 0"))); } @@ -108,7 +104,7 @@ void ignoresNonEqualityBinderRefinement() { void ignoresDerivedBinderEquality() { VCImplication implication = vc("∀x:int. x + 1 == 3", "x > 0"); - assertSimplificationSteps(VCSubstitution::apply, implication, + assertSimplificationSteps(substitution::apply, implication, chain(expect("x + 1 == 3", "∀x:int. x + 1 == 3"), expect("x > 0", "x > 0"))); } @@ -116,7 +112,7 @@ void ignoresDerivedBinderEquality() { void ignoresEqualityWithoutBinder() { VCImplication implication = vc("x == 3", "x > 0"); - assertSimplificationSteps(VCSubstitution::apply, implication, + assertSimplificationSteps(substitution::apply, implication, chain(expect("x == 3", "x == 3"), expect("x > 0", "x > 0"))); } }