diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java new file mode 100644 index 00000000..bdaadfec --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java @@ -0,0 +1,119 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement; +import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf; + +import java.util.HashMap; +import java.util.Map; + +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; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.Var; +import liquidjava.utils.constants.Formats; +import spoon.reflect.declaration.CtEnum; +import spoon.reflect.declaration.CtEnumValue; + +/** + * Decides the comparisons of a variable with an enum constant that a fact about the variable already decides: under + * {@code x == A}, {@code x == A} is true and {@code x == B} false, and under {@code x != A}, {@code x == A} is false, + * so the ternaries they test can fold. Only the constants of the enum types of the chain's binders are used, which the + * solver translates as distinct values, unlike {@code static final} constants that may share a value + */ +public class VCKnownEnumValues implements VCSimplificationPass { + + /** + * A comparison {@code variable == constant}, or {@code variable != constant} when not {@code equal} + */ + private record EnumComparison(Expression expression, String variable, String constant, boolean equal) { + } + + /** The enum type of each enum constant, by the name the solver translates the constant from */ + private final Map enumTypes = new HashMap<>(); + + public VCKnownEnumValues(VCImplication implication) { + for (VCImplication row = implication; row != null; row = row.getNext()) + if (row.getType() != null && row.getType().getDeclaration()instanceof CtEnum enumDecl) + for (CtEnumValue value : enumDecl.getEnumValues()) + enumTypes.put(String.format(Formats.ENUM, enumDecl.getSimpleName(), value.getSimpleName()), + enumDecl.getQualifiedName()); + } + + /** + * Uses the first fact that decides some comparison to replace those comparisons by their value + */ + @Override + public VCImplication apply(VCImplication implication) { + for (VCImplication row = implication; row != null; row = row.getNext()) + for (Expression fact : factsOf(row.getRefinement().getExpression())) { + EnumComparison known = enumComparison(fact); + if (known == null) + continue; + // the last row may be the conclusion, which the other rows cannot assume + boolean onlyLastRow = row.getNext() == null && row != implication; + VCImplication decided = decideRows(implication, known, onlyLastRow); + if (!decided.equals(implication)) + return decided; + } + return implication; + } + + private VCImplication decideRows(VCImplication implication, EnumComparison known, boolean onlyLastRow) { + if (implication == null) + return null; + Expression expression = implication.getRefinement().getExpression(); + boolean decides = !onlyLastRow || implication.getNext() == null; + VCImplication result = copyWithRefinement(implication, + new Predicate(decides ? decide(expression, known) : expression.clone())); + result.setNext(decideRows(implication.getNext(), known, onlyLastRow)); + return result; + } + + // The expression with the comparisons known decides replaced by their value, except for its own fact + private Expression decide(Expression expression, EnumComparison known) { + if (expression == known.expression()) + return expression.clone(); + EnumComparison compared = enumComparison(expression); + if (compared != null && compared.variable().equals(known.variable()) + && enumTypes.get(compared.constant()).equals(enumTypes.get(known.constant()))) { + boolean sameConstant = compared.constant().equals(known.constant()); + if (known.equal()) + return new LiteralBoolean(sameConstant == compared.equal()); + if (sameConstant) + return new LiteralBoolean(!compared.equal()); + } + Expression result = expression.clone(); + for (int i = 0; i < expression.getChildren().size(); i++) + result.setChild(i, decide(expression.getChildren().get(i), known)); + return result; + } + + // A comparison of a variable with an enum constant, either way round, or null + private EnumComparison enumComparison(Expression expression) { + if (!(expression instanceof BinaryExpression binary)) + return null; + boolean equal = "==".equals(binary.getOperator()); + if (!equal && !"!=".equals(binary.getOperator())) + return null; + Expression left = binary.getFirstOperand(), right = binary.getSecondOperand(); + String leftConstant = enumConstant(left), rightConstant = enumConstant(right); + if (left instanceof Var variable && leftConstant == null && rightConstant != null) + return new EnumComparison(expression, variable.getName(), rightConstant, equal); + if (right instanceof Var variable && rightConstant == null && leftConstant != null) + return new EnumComparison(expression, variable.getName(), leftConstant, equal); + return null; + } + + // The name of the enum constant an expression is, written in code or in a refinement, or null + private String enumConstant(Expression expression) { + String name = null; + if (expression instanceof Var var) + name = var.getName(); + else if (expression instanceof Enum en && en.getResolvedLiteral() == null) + name = en.toString(); + return enumTypes.containsKey(name) ? name : null; + } +} 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 d8fef471..7d7780bb 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 @@ -3,6 +3,8 @@ import static liquidjava.rj_language.opt.VCSimplificationUtils.isFalse; import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue; +import java.util.List; + import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.Ite; @@ -146,7 +148,30 @@ private Expression simplifyDisjunction(Expression left, Expression right) { // p || p -> p if (left.equals(right)) return left.clone(); - return null; + return factorCommonConjuncts(left, right); + } + + /** + * Factors the conjuncts both disjuncts share out of a disjunction + */ + private Expression factorCommonConjuncts(Expression left, Expression right) { + List leftConjuncts = left.getConjuncts(), rightConjuncts = right.getConjuncts(); + List common = leftConjuncts.stream().filter(rightConjuncts::contains).distinct().toList(); + if (common.isEmpty()) + return null; + List leftRest = leftConjuncts.stream().filter(c -> !common.contains(c)).toList(); + List rightRest = rightConjuncts.stream().filter(c -> !common.contains(c)).toList(); + // c || c && p -> c + if (leftRest.isEmpty() || rightRest.isEmpty()) + return conjunction(common); + // c && p || c && q -> c && (p || q) + return new BinaryExpression(conjunction(common), "&&", + new BinaryExpression(conjunction(leftRest), "||", conjunction(rightRest))); + } + + private Expression conjunction(List conjuncts) { + return conjuncts.stream().map(Expression::clone) + .reduce((first, second) -> new BinaryExpression(first, "&&", second)).get(); } /** 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 82705505..344bb8de 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 @@ -25,7 +25,7 @@ public static VCSimplificationResult simplifyToFixedPoint(VCImplication implicat if (implication == null) return null; - List passes = passes(needed); + List passes = passes(implication, needed); DebugLog.simplificationStart(implication); VCSimplificationResult current = new VCSimplificationResult(implication); while (true) { @@ -42,7 +42,9 @@ public static VCSimplificationResult simplifyToFixedPoint(VCImplication implicat * Applies one simplification step to a VC chain from all available simplification passes */ public static VCSimplificationResult simplifyOnce(VCSimplificationResult implication) { - return simplifyOnce(implication, passes(NeededVariables.NONE)); + if (implication == null) + return null; + return simplifyOnce(implication, passes(implication.getOriginal().getImplication(), NeededVariables.NONE)); } private static VCSimplificationResult simplifyOnce(VCSimplificationResult implication, @@ -55,10 +57,10 @@ private static VCSimplificationResult simplifyOnce(VCSimplificationResult implic return implication; } - private static List passes(NeededVariables needed) { + private static List passes(VCImplication implication, NeededVariables needed) { return List.of(new VCSubstitution(), new VCFunctionSubstitution(), new VCBinderSimplification(needed), - new VCFolding(), new VCArithmeticSimplification(), new VCLogicalSimplification(), - new VCConstraintSimplification()); + new VCKnownEnumValues(implication), new VCFolding(), new VCArithmeticSimplification(), + new VCLogicalSimplification(), new VCConstraintSimplification()); } /** diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCKnownEnumValuesTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCKnownEnumValuesTest.java new file mode 100644 index 00000000..f2c9a78e --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCKnownEnumValuesTest.java @@ -0,0 +1,47 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.utils.VCTestUtils.*; + +import liquidjava.processor.VCImplication; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Ite; +import liquidjava.rj_language.ast.Var; +import org.junit.jupiter.api.Test; + +class VCKnownEnumValuesTest { + + @Test + void decidesOnlyTheExcludedConstant() { + VCImplication implication = vc("∀mode:Mode. mode != Mode.Photo", + "mode == Mode.Photo ? a : (mode == Mode.Video ? b : c)"); + assertSimplificationSteps(new VCKnownEnumValues(implication), implication, + step("mode != Mode.Photo", "false ? a : (mode == Mode.Video ? b : c)")); + } + + @Test + void decidesConstantsReadInCode() { + // code reads an enum constant as a variable named after it + Var mode = new Var("mode"), photo = new Var("Mode.Photo"), video = new Var("Mode.Video"); + VCImplication implication = vc("∀mode:Mode. true", "true"); + implication.setRefinement(new Predicate(new BinaryExpression(mode, "==", photo))); + implication.getNext().setRefinement( + new Predicate(new Ite(new BinaryExpression(video, "==", mode), new Var("a"), new Var("b")))); + assertSimplificationSteps(new VCKnownEnumValues(implication), implication, + step("mode == Photo", "false ? a : b")); + } + + @Test + void keepsPremisesTheConclusionWouldDecide() { + VCImplication implication = vc("∀mode:Mode. mode == Mode.Video || p", "mode == Mode.Photo"); + assertSimplificationSteps(new VCKnownEnumValues(implication), implication, + step("mode == Mode.Video || p", "mode == Mode.Photo")); + } + + @Test + void foldsTheTernariesAFactDecides() { + assertSimplificationSteps(vc("∀mode:Mode. true", "mode == Mode.Video && (mode == Mode.Photo ? a : b)"), + step("mode == Mode.Video && (mode == Mode.Photo ? a : b)"), + step("mode == Mode.Video && (false ? a : b)"), step("mode == Mode.Video && b")); + } +} 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 141744d9..973d7add 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 @@ -23,6 +23,12 @@ void simplifiesDisjunctionWithBooleanLiterals() { assertSimplificationSteps(simplification, vc("false || x"), step("x")); } + @Test + void factorsConjunctsSharedByDisjuncts() { + assertSimplificationSteps(simplification, vc("a && c || b && c"), step("c && (a || b)")); + assertSimplificationSteps(simplification, vc("c || c && b"), step("c")); + } + @Test void simplifiesDoubleNegation() { assertSimplificationSteps(simplification, vc("!!x"), step("x")); diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index 2a039e25..afd8e58b 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java @@ -13,12 +13,17 @@ import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.rj_language.parsing.RefinementsParser; import spoon.Launcher; +import spoon.reflect.declaration.CtEnum; +import spoon.reflect.declaration.CtEnumValue; +import spoon.reflect.factory.Factory; import spoon.reflect.factory.TypeFactory; import spoon.reflect.reference.CtTypeReference; public class VCTestUtils { - private static final TypeFactory TYPE_FACTORY = new Launcher().getFactory().Type(); + private static final Factory FACTORY = new Launcher().getFactory(); + private static final TypeFactory TYPE_FACTORY = FACTORY.Type(); + private static final CtTypeReference MODE = enumType("Mode", "Photo", "Video"); public static VCImplication vc(String... implications) { VCImplication first = null; @@ -103,9 +108,21 @@ private static CtTypeReference type(String name) { return TYPE_FACTORY.BOOLEAN_PRIMITIVE; if ("Object".equals(name)) return TYPE_FACTORY.OBJECT; + if ("Mode".equals(name)) + return MODE; throw new IllegalArgumentException("Unsupported test type: " + name); } + private static CtTypeReference enumType(String name, String... values) { + CtEnum enumDecl = FACTORY.Enum().create(name); + for (String value : values) { + CtEnumValue enumValue = FACTORY.Core().createEnumValue(); + enumValue.setSimpleName(value); + enumDecl.addEnumValue(enumValue); + } + return enumDecl.getReference(); + } + private static String formatRefinement(VCImplication implication) { return implication.getRefinement().getExpression().toDisplayString(); }