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 31c1ca55..34ae996b 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 00000000..063b760b --- /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 Expected"; + } + + @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 880c233e..a0f448bc 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 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 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 b2a0508e..5d8ab0af 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)")); + } }