Add a Relevant to Expected step to state errors

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -21,6 +21,9 @@
 import liquidjava.rj_language.ast.Ite;
 import liquidjava.rj_language.ast.Var;
 import liquidjava.rj_language.opt.NeededVariables;
+import liquidjava.rj_language.opt.VCRelevantFacts;
+import liquidjava.rj_language.opt.VCSimplification;
+import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.smt.Counterexample;
 import liquidjava.smt.SMTEvaluator;
 import liquidjava.smt.SMTResult;
@@ -459,9 +462,23 @@ protected void throwStateRefinementError(SourcePosition position, SourcePosition
             StateErrorContext context) throws StateRefinementError {
         TranslationTable map = new TranslationTable();
         VCImplication foundState = buildPremiseChain(map, expected, found);
-        throw new StateRefinementError(position, declarationPosition, expected,
-                foundState.simplify(NeededVariables.forStateError(expected)), map, customMessage, hints, category,
-                context);
+        VCSimplificationResult simplified = foundState.simplify(NeededVariables.forStateError(expected));
+        VCSimplificationResult shown = VCSimplification.simplifyOnce(simplified,
+                new VCRelevantFacts(expected.getExpression(), this::ghostFunctionsOf));
+        throw new StateRefinementError(position, declarationPosition, expected, shown, map, customMessage, hints,
+                category, context);
+    }
+
+    /** 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<>();
+        for (GhostState state : context.getGhostStates())
+            if (state.matches(name))
+                functions.add(state.getParent() != null ? state.getParent().getName() : state.getName());
+        for (GhostFunction ghost : context.getGhosts())
+            if (ghost.matches(name))
+                functions.add(ghost.getName());
+        return functions;
     }
 
     protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCRelevantFacts.java

@@ -0,0 +1,130 @@
+package liquidjava.rj_language.opt;
+
+import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.variablesOf;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+import java.util.function.Function;
+
+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.FunctionInvocation;
+import liquidjava.rj_language.ast.Var;
+
+/**
+ * Keeps in a state error's Found only the facts the expected state depends on, for display: the solver's VC is not
+ * changed. Each fact is split into the symbols it constrains: a ghost function applied to an object, such as the state
+ * set {@code state1(x)} that both {@code open(x)} and {@code state1(x) == state1(y)} constrain, or a variable whose own
+ * value it constrains. Different ghost functions, or the same one over different objects, are different solver terms,
+ * so facts that share no symbol with expected, directly or through other facts, are independent of it and are left out.
+ * An object whose value a fact constrains, such as {@code x == y}, or that an alias or unknown function takes, is one
+ * symbol with all its ghost functions, so its facts are never split. Nothing changes when every fact or none is
+ * relevant
+ */
+public class VCRelevantFacts implements VCSimplificationPass {
+
+    private final Expression expected;
+    private final Function<String, Set<String>> ghostFunctionsOf;
+
+    /**
+     * @param ghostFunctionsOf
+     *            the ghost functions an invocation name stands for: a state's state set function, or the ghost itself;
+     *            none for any other name
+     */
+    public VCRelevantFacts(Expression expected, Function<String, Set<String>> ghostFunctionsOf) {
+        this.expected = expected;
+        this.ghostFunctionsOf = ghostFunctionsOf;
+    }
+
+    @Override
+    public String getName() {
+        return "Relevant to Expected";
+    }
+
+    @Override
+    public VCImplication apply(VCImplication implication) {
+        List<List<Expression>> rowFacts = new ArrayList<>();
+        for (VCImplication row = implication; row != null; row = row.getNext())
+            rowFacts.add(factsOf(row.getRefinement().getExpression()));
+        Set<String> values = new HashSet<>();
+        addSymbols(expected, new HashMap<>(), values);
+        rowFacts.forEach(facts -> facts.forEach(fact -> addSymbols(fact, new HashMap<>(), values)));
+
+        Set<String> linked = symbolsOf(expected, values);
+        List<Set<String>> unlinked = new ArrayList<>();
+        rowFacts.forEach(facts -> facts.forEach(fact -> unlinked.add(symbolsOf(fact, values))));
+        boolean changed = true;
+        while (changed) {
+            changed = false;
+            for (Iterator<Set<String>> it = unlinked.iterator(); it.hasNext();) {
+                Set<String> symbols = it.next();
+                if (symbols.stream().anyMatch(linked::contains)) {
+                    linked.addAll(symbols);
+                    it.remove();
+                    changed = true;
+                }
+            }
+        }
+
+        List<List<Expression>> kept = rowFacts.stream().map(facts -> facts.stream()
+                .filter(fact -> symbolsOf(fact, values).stream().anyMatch(linked::contains)).toList()).toList();
+        int relevant = kept.stream().mapToInt(List::size).sum();
+        if (relevant == 0 || relevant == rowFacts.stream().mapToInt(List::size).sum())
+            return implication;
+        return rebuild(implication, rowFacts.iterator(), kept.iterator());
+    }
+
+    // The rows with their relevant facts, leaving out those that keep none
+    private VCImplication rebuild(VCImplication row, Iterator<List<Expression>> all, Iterator<List<Expression>> kept) {
+        if (row == null)
+            return null;
+        List<Expression> rowAll = all.next(), rowKept = kept.next();
+        VCImplication next = rebuild(row.getNext(), all, kept);
+        if (rowKept.isEmpty())
+            return next;
+        Expression refinement = rowKept.size() == rowAll.size() ? row.getRefinement().getExpression().clone()
+                : rowKept.stream().map(Expression::clone)
+                        .reduce((first, second) -> new BinaryExpression(first, "&&", second)).get();
+        VCImplication result = copyWithRefinement(row, new Predicate(refinement));
+        result.setNext(next);
+        return result;
+    }
+
+    // The symbols an expression constrains: f(x) for a ghost function over an object, or the object itself when values
+    // has it, and the variables whose value it constrains
+    private Set<String> symbolsOf(Expression expression, Set<String> values) {
+        Map<String, String> applications = new HashMap<>();
+        Set<String> symbols = new HashSet<>();
+        addSymbols(expression, applications, symbols);
+        applications.forEach((application, object) -> symbols.add(values.contains(object) ? object : application));
+        return symbols;
+    }
+
+    // Adds each ghost function applied to a variable, as f(x) mapped to x, to applications, and the variables whose
+    // value the expression constrains, or that an unknown function takes, to values
+    private void addSymbols(Expression expression, Map<String, String> applications, Set<String> values) {
+        if (expression instanceof FunctionInvocation invocation) {
+            Set<String> functions = ghostFunctionsOf.apply(invocation.getName());
+            if (!functions.isEmpty() && invocation.getArgs().size() == 1
+                    && invocation.getArgs().get(0)instanceof Var object)
+                functions.forEach(
+                        function -> applications.put(function + "(" + object.getName() + ")", object.getName()));
+            else
+                values.addAll(variablesOf(invocation));
+            return;
+        }
+        if (expression instanceof Var var)
+            values.add(var.getName());
+        for (Expression child : expression.getChildren())
+            addSymbols(child, applications, values);
+    }
+}

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java

@@ -11,6 +11,7 @@
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.StateErrorContext;
 import liquidjava.diagnostics.errors.StateRefinementError;
+import liquidjava.rj_language.opt.VCSimplificationResult;
 
 class TestStateErrorContext {
 
@@ -50,10 +51,25 @@ void classWithoutStateSetHasNoContext() {
         assertNull(contextOf("ErrorUnconstrainedStateRefinement.java"));
     }
 
+    @Test
+    void foundEndsWithTheFactsRelevantToTheExpectedStateSet() {
+        StateRefinementError error = errorOf("ErrorArgumentPicksTheStateEarlier.java");
+        assertEquals("found tilingOff(param@25) && state1(param) == state1(param@25) but expected tilingOn(param)",
+                error.getMessage());
+        VCSimplificationResult found = error.getFoundSimplification();
+        assertEquals("Relevant to Expected", found.getSimplification());
+        // stepping back shows the compression state set again
+        assertTrue(found.getOrigin().getImplication().toString().contains("compressed"));
+    }
+
     private static StateErrorContext contextOf(String test) {
+        return errorOf(test).getContext();
+    }
+
+    private static StateRefinementError errorOf(String test) {
         CommandLineLauncher.launch(TEST_SUITE + test);
         List<LJError> errors = Diagnostics.getInstance().getErrors().stream().toList();
         assertEquals(1, errors.size(), "Expected exactly one error from " + test);
-        return assertInstanceOf(StateRefinementError.class, errors.get(0)).getContext();
+        return assertInstanceOf(StateRefinementError.class, errors.get(0));
     }
 }

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java

@@ -3,10 +3,14 @@
 import static liquidjava.utils.VCTestUtils.*;
 import static org.junit.jupiter.api.Assertions.assertNull;
 
+import java.util.Map;
+import java.util.Set;
+
 import org.junit.jupiter.api.AfterEach;
 import org.junit.jupiter.api.Test;
 
 import liquidjava.processor.context.Context;
+import liquidjava.rj_language.parsing.RefinementsParser;
 import liquidjava.utils.TestUtils;
 
 class VCSimplificationTest {
@@ -180,4 +184,25 @@ void simplifyEliminatesRemovableConstraintImpliedByEarlierAntecedent() {
         assertSimplificationSteps(vc("∀x:int. x > 1", "∀cond:boolean. x > 0", "∀y:int. y == x + 1", "y < 0"),
                 step("x > 1", "x > 0", "x + 1 < 0"), step("x > 1", "x + 1 < 0"));
     }
+
+    // tiling states and state1 are one state set, compression states and state2 another
+    private static VCRelevantFacts relevantTo(String expected) {
+        Map<String, String> stateSets = Map.of("startTiling", "state1", "tilingSet", "state1", "state1", "state1",
+                "compressionSet", "state2", "state2", "state2");
+        return new VCRelevantFacts(RefinementsParser.createAST(expected, ""),
+                name -> stateSets.containsKey(name) ? Set.of(stateSets.get(name)) : Set.of());
+    }
+
+    @Test
+    void relevantStepKeepsEveryStateSetOfAnObjectComparedAsAValue() {
+        assertSimplificationSteps(relevantTo("tilingSet(p)"),
+                vc("∀q:Object. compressionSet(q) && startTiling(p)", "p == q"),
+                step("compressionSet(q) && startTiling(p)", "p == q"));
+    }
+
+    @Test
+    void relevantStepKeepsFactsAnUnknownFunctionTakesTheObjectOf() {
+        assertSimplificationSteps(relevantTo("tilingSet(p)"), vc("compressionSet(p) && ready(p)", "startTiling(p)"),
+                step("compressionSet(p) && ready(p)", "startTiling(p)"));
+    }
 }