diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStatePathFolding.java b/liquidjava-example/src/main/java/testSuite/ErrorStatePathFolding.java new file mode 100644 index 00000000..d31a1445 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorStatePathFolding.java @@ -0,0 +1,42 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +// Found folds the branches the path condition rules out: under next == BORDERLESS only the second if can have run +@StateSet(name = "display", value = {"hidden", "shown"}) +class FoldFrame { + @StateRefinement(to = "hidden(this)") + FoldFrame() {} + + @StateRefinement(from = "hidden(this)", to = "shown(this)") + void show() {} + + @StateRefinement(from = "shown(this)", to = "hidden(this)") + void hide() {} + + @StateRefinement(from = "hidden(this)") + void decorate() {} +} + +enum FoldMode { + WINDOWED, BORDERLESS +} + +public class ErrorStatePathFolding { + static void apply(FoldMode previous, FoldMode next) { + FoldFrame frame = new FoldFrame(); + frame.show(); + if (previous == FoldMode.BORDERLESS && next != FoldMode.BORDERLESS) + frame.hide(); + else if (previous != FoldMode.BORDERLESS && next == FoldMode.BORDERLESS) + frame.hide(); + switch (next) { + case BORDERLESS: + frame.decorate(); // Expect: State Refinement Error + break; + default: + break; + } + } +} 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 84d285e4..c8e0cc59 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 @@ -1,5 +1,8 @@ package liquidjava.processor.refinement_checker; +import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf; +import static liquidjava.rj_language.opt.VCSimplificationUtils.linkedToExpected; + import java.util.ArrayList; import java.util.HashSet; import java.util.List; @@ -22,6 +25,7 @@ import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.opt.NeededVariables; +import liquidjava.rj_language.opt.VCPathFolding; import liquidjava.rj_language.opt.VCRelevantFacts; import liquidjava.rj_language.opt.VCSimplification; import liquidjava.rj_language.opt.VCSimplificationResult; @@ -461,14 +465,33 @@ protected void throwStateRefinementError(SourcePosition position, SourcePosition TranslationTable map = new TranslationTable(); VCImplication foundState = buildPremiseChain(map, expected, found); VCSimplificationResult simplified = foundState.simplify(NeededVariables.forStateError(expected)); - VCSimplificationResult shown = VCSimplification.simplifyOnce(simplified, + VCSimplificationResult relevant = VCSimplification.simplifyOnce(simplified, new VCRelevantFacts(expected.getExpression(), this::ghostFunctionsOf)); + VCSimplificationResult folded = VCSimplification.simplifyOnce(relevant, new VCPathFolding(foundState)); + VCSimplificationResult shown = keepsShownFacts(relevant, folded, expected) ? folded : relevant; throw new StateRefinementError(position, declarationPosition, expected, shown, map, customMessage, hints, category, context, e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()), declarationNotes); } + /** + * Whether the error still shows, after folding, every fact it showed that is not conditional: the facts a fold uses + * must stay in sight, or the folded branch would read as if nothing chose it + */ + private static boolean keepsShownFacts(VCSimplificationResult before, VCSimplificationResult after, + Predicate expected) { + List shownAfter = factsOf( + linkedToExpected(after.getImplication().toPredicate().getExpression(), expected.getExpression())); + return factsOf( + linkedToExpected(before.getImplication().toPredicate().getExpression(), expected.getExpression())) + .stream().filter(fact -> !hasIte(fact)).allMatch(shownAfter::contains); + } + + private static boolean hasIte(Expression expression) { + return expression instanceof Ite || expression.getChildren().stream().anyMatch(VCChecker::hasIte); + } + /** The ghost functions an invocation name stands for: a state's state set function, or the ghost itself */ private Set ghostFunctionsOf(String name) { Set functions = new HashSet<>(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCPathFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCPathFolding.java new file mode 100644 index 00000000..5818d97d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCPathFolding.java @@ -0,0 +1,158 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf; + +import java.util.HashSet; +import java.util.LinkedHashMap; +import java.util.Map; +import java.util.Set; + +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.Ite; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.LiteralChar; +import liquidjava.rj_language.ast.LiteralInt; +import liquidjava.rj_language.ast.LiteralLong; +import liquidjava.rj_language.ast.LiteralReal; +import liquidjava.rj_language.ast.UnaryExpression; +import liquidjava.rj_language.ast.Var; +import liquidjava.utils.constants.Formats; +import spoon.reflect.declaration.CtEnum; +import spoon.reflect.reference.CtTypeReference; + +/** + * Folds the conditions of the conditional facts of a VC chain under the facts {@code x == c}, with {@code c} a literal + * or a constant of an enum the chain binds (written {@code Mode.ON}), that the chain states: each condition is written + * with {@code c} for {@code x} and folded, and a branch is dropped only when its condition folds to a constant that + * rules it out. Every fact of the chain holds wherever the others do, so the chain stays equivalent, and the facts + * {@code x == c} themselves stay as they are + */ +public class VCPathFolding implements VCSimplificationPass { + + private static final VCSimplificationPass FOLDING = new VCFolding(); + private static final VCSimplificationPass LOGIC = new VCLogicalSimplification(); + + private final Set enumConstants; + + /** + * @param bound + * a chain that binds the enum constants that may occur, such as the chain before its unused binders were + * dropped + */ + public VCPathFolding(VCImplication bound) { + this.enumConstants = enumConstants(bound); + } + + @Override + public VCImplication apply(VCImplication implication) { + Map constants = constants(implication, enumConstants); + if (constants.isEmpty()) + return implication; + VCImplication result = implication.clone(); + for (VCImplication node = result; node != null; node = node.getNext()) + if (node.getRefinement() != null) + node.setRefinement( + new Predicate(foldConditions(node.getRefinement().getExpression(), constants, enumConstants))); + return result; + } + + /** The enum constants the chain binds, each a distinct value of its enum */ + private static Set enumConstants(VCImplication implication) { + Set constants = new HashSet<>(); + for (VCImplication node = implication; node != null; node = node.getNext()) + if (node.hasBinder() && isEnumConstant(node.getName(), node.getType())) + constants.add(node.getName()); + return constants; + } + + private static boolean isEnumConstant(String name, CtTypeReference type) { + return type != null && type.getDeclaration()instanceof CtEnum declaration + && declaration.getEnumValues().stream().anyMatch(value -> name + .equals(String.format(Formats.ENUM, declaration.getSimpleName(), value.getSimpleName()))); + } + + /** The variables the chain states equal to a constant, with that constant */ + private static Map constants(VCImplication implication, Set enumConstants) { + Map constants = new LinkedHashMap<>(); + for (VCImplication node = implication; node != null; node = node.getNext()) { + if (node.getRefinement() == null) + continue; + for (Expression fact : factsOf(node.getRefinement().getExpression())) + if (fact instanceof BinaryExpression equality && "==".equals(equality.getOperator())) { + addConstant(equality.getFirstOperand(), equality.getSecondOperand(), constants, enumConstants); + addConstant(equality.getSecondOperand(), equality.getFirstOperand(), constants, enumConstants); + } + } + return constants; + } + + private static void addConstant(Expression variable, Expression value, Map constants, + Set enumConstants) { + if (variable instanceof Var var && !enumConstants.contains(var.getName()) && isConstant(value, enumConstants)) + constants.putIfAbsent(var, value); + } + + private static boolean isConstant(Expression expression, Set enumConstants) { + return expression instanceof Var var && enumConstants.contains(var.getName()) || expression instanceof Enum + || expression instanceof LiteralInt || expression instanceof LiteralLong + || expression instanceof LiteralReal || expression instanceof LiteralBoolean + || expression instanceof LiteralChar; + } + + private static Expression foldConditions(Expression expression, Map constants, + Set enumConstants) { + if (expression instanceof Ite ite) { + Expression condition = fold(compareEnumConstants(substitute(ite.getCondition(), constants), enumConstants)); + if (condition instanceof LiteralBoolean settled) + return foldConditions(settled.isBooleanTrue() ? ite.getThen() : ite.getElse(), constants, + enumConstants); + return new Ite(condition, foldConditions(ite.getThen(), constants, enumConstants), + foldConditions(ite.getElse(), constants, enumConstants)); + } + if (expression instanceof BinaryExpression binary) + return new BinaryExpression(foldConditions(binary.getFirstOperand(), constants, enumConstants), + binary.getOperator(), foldConditions(binary.getSecondOperand(), constants, enumConstants)); + if (expression instanceof UnaryExpression unary) + return new UnaryExpression(unary.getOp(), foldConditions(unary.getExpression(), constants, enumConstants)); + return expression.clone(); + } + + /** {@code A == B} and {@code A != B} of two enum constants, as the literal they are */ + private static Expression compareEnumConstants(Expression expression, Set enumConstants) { + if (expression instanceof BinaryExpression binary && binary.getFirstOperand()instanceof Var left + && binary.getSecondOperand()instanceof Var right && enumConstants.contains(left.getName()) + && enumConstants.contains(right.getName()) + && ("==".equals(binary.getOperator()) || "!=".equals(binary.getOperator()))) + return new LiteralBoolean(left.getName().equals(right.getName()) == "==".equals(binary.getOperator())); + for (int i = 0; i < expression.getChildren().size(); i++) + expression.setChild(i, compareEnumConstants(expression.getChildren().get(i), enumConstants)); + return expression; + } + + private static Expression substitute(Expression expression, Map constants) { + Expression substituted = expression.clone(); + for (Map.Entry constant : constants.entrySet()) + substituted = substituted.substitute(constant.getKey(), constant.getValue().clone()); + return substituted; + } + + /** The condition folded with the constant and logical identities, until neither applies */ + private static Expression fold(Expression condition) { + VCImplication current = new VCImplication(new Predicate(condition)); + while (true) { + VCImplication next = LOGIC.apply(FOLDING.apply(current)); + if (next.equals(current)) + return current.getRefinement().getExpression(); + current = next; + } + } + + @Override + public String getName() { + return "Path Folding"; + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java index ae883369..6c9946ef 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestFoundBinders.java @@ -115,6 +115,15 @@ void earlierValuesOfAVariableAreWrittenWithTheirLine() { } // the rows of Found as the IDE writes them, with the error's names: binder name, then its refinement + @Test + void stateFoundFoldsTheBranchesItsPathConditionRulesOut() { + CommandLineLauncher.launch("../liquidjava-example/src/main/java/testSuite/ErrorStatePathFolding.java"); + List errors = Diagnostics.getInstance().getErrors().stream().toList(); + assertEquals(1, errors.size()); + assertEquals("found next == BORDERLESS && (previous != BORDERLESS ? display(frame) == hidden : " + + "display(frame) == shown) but expected display(frame) == hidden", errors.get(0).getMessage()); + } + private static List rows(VCImplication found, DisplayNames names) { List rows = new ArrayList<>(); for (VCImplication current = found; current != null; current = current.getNext()) {