From a3d0f5aa7ade06dab1606f1019f15b72a0c1ed17 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 12:25:55 +0000 Subject: [PATCH 1/2] Add a step to state errors that keeps the facts relevant to Expected The last step of a state error's Found keeps only the facts that share a ghost function application or a value with Expected, directly or through other facts. Facts about other state sets, or earlier versions not linked to the expected one, are left out. Objects compared as values, or passed to an alias or unknown function, are never split. No step is added when every fact or none is relevant. The VC and the verdict do not change. Co-Authored-By: Claude Opus 5.5 --- .../refinement_checker/VCChecker.java | 23 +++- .../rj_language/opt/VCRelevantFacts.java | 130 ++++++++++++++++++ .../api/tests/TestStateErrorContext.java | 18 ++- .../rj_language/opt/VCSimplificationTest.java | 25 ++++ 4 files changed, 192 insertions(+), 4 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCRelevantFacts.java 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 31c1ca553..34ae996be 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 @@ -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 ghostFunctionsOf(String name) { + Set 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 { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCRelevantFacts.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCRelevantFacts.java new file mode 100644 index 000000000..817d94ec8 --- /dev/null +++ b/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> 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> ghostFunctionsOf) { + this.expected = expected; + this.ghostFunctionsOf = ghostFunctionsOf; + } + + @Override + public String getName() { + return "Relevant to this requirement"; + } + + @Override + public VCImplication apply(VCImplication implication) { + List> rowFacts = new ArrayList<>(); + for (VCImplication row = implication; row != null; row = row.getNext()) + rowFacts.add(factsOf(row.getRefinement().getExpression())); + Set values = new HashSet<>(); + addSymbols(expected, new HashMap<>(), values); + rowFacts.forEach(facts -> facts.forEach(fact -> addSymbols(fact, new HashMap<>(), values))); + + Set linked = symbolsOf(expected, values); + List> unlinked = new ArrayList<>(); + rowFacts.forEach(facts -> facts.forEach(fact -> unlinked.add(symbolsOf(fact, values)))); + boolean changed = true; + while (changed) { + changed = false; + for (Iterator> it = unlinked.iterator(); it.hasNext();) { + Set symbols = it.next(); + if (symbols.stream().anyMatch(linked::contains)) { + linked.addAll(symbols); + it.remove(); + changed = true; + } + } + } + + List> 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> all, Iterator> kept) { + if (row == null) + return null; + List 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 symbolsOf(Expression expression, Set values) { + Map applications = new HashMap<>(); + Set 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 applications, Set values) { + if (expression instanceof FunctionInvocation invocation) { + Set 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); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java index 880c233e2..9a7e6c0f3 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java +++ b/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 this requirement", 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 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)); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java index b2a0508e0..5d8ab0af7 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java +++ b/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 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)")); + } } From 70b1b4631e04d8ed7463bc4ce675918ac8485d53 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 6 Nov 2026 12:42:37 +0000 Subject: [PATCH 2/2] Name the relevant step Relevant to Expected Co-Authored-By: Claude Opus 5.5 --- .../main/java/liquidjava/rj_language/opt/VCRelevantFacts.java | 2 +- .../test/java/liquidjava/api/tests/TestStateErrorContext.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCRelevantFacts.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCRelevantFacts.java index 817d94ec8..063b760bd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCRelevantFacts.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCRelevantFacts.java @@ -47,7 +47,7 @@ public VCRelevantFacts(Expression expected, Function> ghostF @Override public String getName() { - return "Relevant to this requirement"; + return "Relevant to Expected"; } @Override diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java index 9a7e6c0f3..a0f448bc3 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateErrorContext.java @@ -57,7 +57,7 @@ void foundEndsWithTheFactsRelevantToTheExpectedStateSet() { assertEquals("found tilingOff(param@25) && state1(param) == state1(param@25) but expected tilingOn(param)", error.getMessage()); VCSimplificationResult found = error.getFoundSimplification(); - assertEquals("Relevant to this requirement", found.getSimplification()); + assertEquals("Relevant to Expected", found.getSimplification()); // stepping back shows the compression state set again assertTrue(found.getOrigin().getImplication().toString().contains("compressed")); }