Fold a state error's Found under the constants its path conditions state

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;
+        }
+    }
+}

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<Expression> 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<String> ghostFunctionsOf(String name) {
         Set<String> functions = new HashSet<>();

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<String> 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<Var, Expression> 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<String> enumConstants(VCImplication implication) {
+        Set<String> 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<Var, Expression> constants(VCImplication implication, Set<String> enumConstants) {
+        Map<Var, Expression> 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<Var, Expression> constants,
+            Set<String> enumConstants) {
+        if (variable instanceof Var var && !enumConstants.contains(var.getName()) && isConstant(value, enumConstants))
+            constants.putIfAbsent(var, value);
+    }
+
+    private static boolean isConstant(Expression expression, Set<String> 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<Var, Expression> constants,
+            Set<String> 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<String> 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<Var, Expression> constants) {
+        Expression substituted = expression.clone();
+        for (Map.Entry<Var, Expression> 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";
+    }
+}

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<LJError> 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<String> rows(VCImplication found, DisplayNames names) {
         List<String> rows = new ArrayList<>();
         for (VCImplication current = found; current != null; current = current.getNext()) {