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..c8f316e0 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 @@ -22,6 +22,7 @@ import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.opt.NeededVariables; +import liquidjava.rj_language.opt.VCKnownEnumValues; import liquidjava.rj_language.opt.VCRelevantFacts; import liquidjava.rj_language.opt.VCSimplification; import liquidjava.rj_language.opt.VCSimplificationResult; @@ -461,8 +462,8 @@ 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, - new VCRelevantFacts(expected.getExpression(), this::ghostFunctionsOf)); + VCSimplificationResult shown = VCSimplification.simplifyOnce(simplified, new VCRelevantFacts( + expected.getExpression(), this::ghostFunctionsOf, VCKnownEnumValues.enumConstants(foundState))); throw new StateRefinementError(position, declarationPosition, expected, shown, map, customMessage, hints, category, context, e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()), diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java index bdaadfec..ddf13abc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java @@ -5,6 +5,7 @@ import java.util.HashMap; import java.util.Map; +import java.util.Set; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; @@ -32,14 +33,25 @@ private record EnumComparison(Expression expression, String variable, String con } /** The enum type of each enum constant, by the name the solver translates the constant from */ - private final Map enumTypes = new HashMap<>(); + private final Map enumTypes; public VCKnownEnumValues(VCImplication implication) { + this.enumTypes = enumTypesOf(implication); + } + + /** The names the constants of the enum types of the chain's binders are translated from, which denote values */ + public static Set enumConstants(VCImplication implication) { + return enumTypesOf(implication).keySet(); + } + + private static Map enumTypesOf(VCImplication implication) { + Map enumTypes = new HashMap<>(); for (VCImplication row = implication; row != null; row = row.getNext()) if (row.getType() != null && row.getType().getDeclaration()instanceof CtEnum enumDecl) for (CtEnumValue value : enumDecl.getEnumValues()) enumTypes.put(String.format(Formats.ENUM, enumDecl.getSimpleName(), value.getSimpleName()), enumDecl.getQualifiedName()); + return enumTypes; } /** 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 2e8272f8..7eac5a82 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 @@ -15,6 +15,7 @@ import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.FunctionInvocation; @@ -27,22 +28,28 @@ * 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 + * symbol with all its ghost functions, so its facts are never split. A constant, such as an enum constant read in code, + * is a fixed value, so facts that only compare values with it share no symbol through it; it stays one when a function + * or alias takes it or a value one takes is compared with it, as equal objects have equal ghost values. Nothing changes + * when every fact or none is relevant */ public class VCRelevantFacts implements VCSimplificationPass { private final Expression expected; private final Function> ghostFunctionsOf; + private final Set constants; /** * @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 + * @param constants + * the variable names that denote constants, such as enum constants */ - public VCRelevantFacts(Expression expected, Function> ghostFunctionsOf) { + public VCRelevantFacts(Expression expected, Function> ghostFunctionsOf, Set constants) { this.expected = expected; this.ghostFunctionsOf = ghostFunctionsOf; + this.constants = constants; } @Override @@ -60,8 +67,10 @@ public VCImplication apply(VCImplication implication) { addSymbols(expected, new HashMap<>(), values); allFacts.forEach(fact -> addSymbols(fact, new HashMap<>(), values)); - Set linked = symbolsOf(expected, values); - List> unlinked = new ArrayList<>(allFacts.stream().map(fact -> symbolsOf(fact, values)).toList()); + Set valueConstants = valueConstants(expected, allFacts); + Set linked = symbolsOf(expected, values, valueConstants); + List> unlinked = new ArrayList<>( + allFacts.stream().map(fact -> symbolsOf(fact, values, valueConstants)).toList()); boolean changed = true; while (changed) { changed = false; @@ -75,8 +84,11 @@ public VCImplication apply(VCImplication implication) { } } - List> kept = rowFacts.stream().map(facts -> facts.stream() - .filter(fact -> symbolsOf(fact, values).stream().anyMatch(linked::contains)).toList()).toList(); + List> kept = rowFacts.stream() + .map(facts -> facts.stream() + .filter(fact -> symbolsOf(fact, values, valueConstants).stream().anyMatch(linked::contains)) + .toList()) + .toList(); int relevant = kept.stream().mapToInt(List::size).sum(); if (relevant == 0 || relevant == allFacts.size()) return implication; @@ -99,13 +111,45 @@ private VCImplication rebuild(VCImplication row, Iterator> all, return result; } + // The constants no function or alias takes and that are compared with no value one takes + private Set valueConstants(Expression expected, List facts) { + Set objects = new HashSet<>(); + addArguments(expected, objects); + facts.forEach(fact -> addArguments(fact, objects)); + Set valueConstants = new HashSet<>(constants); + valueConstants.removeAll(objects); + removeComparedWithObjects(expected, objects, valueConstants); + facts.forEach(fact -> removeComparedWithObjects(fact, objects, valueConstants)); + return valueConstants; + } + + private static void addArguments(Expression expression, Set objects) { + if (expression instanceof FunctionInvocation invocation) + invocation.getArgs().forEach(argument -> objects.addAll(variablesOf(argument))); + else if (expression instanceof AliasInvocation alias) + alias.getArgs().forEach(argument -> objects.addAll(variablesOf(argument))); + expression.getChildren().forEach(child -> addArguments(child, objects)); + } + + private static void removeComparedWithObjects(Expression expression, Set objects, + Set valueConstants) { + if (expression instanceof BinaryExpression binary + && ("==".equals(binary.getOperator()) || "!=".equals(binary.getOperator()))) { + List compared = variablesOf(binary); + if (compared.stream().anyMatch(objects::contains)) + valueConstants.removeAll(compared); + } + expression.getChildren().forEach(child -> removeComparedWithObjects(child, objects, valueConstants)); + } + // 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) { + // has it, and the variables whose value it constrains, except the value constants + private Set symbolsOf(Expression expression, Set values, Set valueConstants) { Map applications = new HashMap<>(); Set symbols = new HashSet<>(); addSymbols(expression, applications, symbols); applications.forEach((application, object) -> symbols.add(values.contains(object) ? object : application)); + symbols.removeAll(valueConstants); return symbols; } 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 5d8ab0af..351deca7 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 @@ -9,7 +9,12 @@ import org.junit.jupiter.api.AfterEach; import org.junit.jupiter.api.Test; +import liquidjava.processor.VCImplication; import liquidjava.processor.context.Context; +import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Ite; +import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.utils.TestUtils; @@ -190,7 +195,7 @@ 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()); + name -> stateSets.containsKey(name) ? Set.of(stateSets.get(name)) : Set.of(), Set.of("Mode.Photo")); } @Test @@ -200,6 +205,31 @@ void relevantStepKeepsEveryStateSetOfAnObjectComparedAsAValue() { step("compressionSet(q) && startTiling(p)", "p == q")); } + @Test + void relevantStepDoesNotLinkFactsThroughAConstant() { + // code reads an enum constant as a variable named after it + Var photo = new Var("Mode.Photo"); + VCImplication implication = vc("∀n:Mode. true", "true"); + implication.setRefinement(new Predicate(new BinaryExpression(new Var("n"), "==", photo))); + implication.getNext() + .setRefinement(new Predicate(new Ite(new BinaryExpression(new Var("m"), "==", photo), + RefinementsParser.createAST("startTiling(p)", ""), + RefinementsParser.createAST("compressionSet(p)", "")))); + assertSimplificationSteps(relevantTo("tilingSet(p)"), implication, + step("m == Photo ? startTiling(p) : compressionSet(p)")); + } + + @Test + void relevantStepLinksFactsThroughAConstantAnObjectEquals() { + Var photo = new Var("Mode.Photo"); + VCImplication implication = vc("∀p:Mode. true", "true"); + implication.setRefinement(new Predicate(new BinaryExpression(new Var("p"), "==", photo))); + implication.getNext().setRefinement(new Predicate( + new BinaryExpression(RefinementsParser.createAST("startTiling(q)", ""), "&&", new Var("ready")))); + implication.getNext().getRefinement().getExpression().getChildren().get(0).setChild(0, photo); + assertSimplificationSteps(relevantTo("tilingSet(p)"), implication, step("p == Photo", "startTiling(Photo)")); + } + @Test void relevantStepKeepsFactsAnUnknownFunctionTakesTheObjectOf() { assertSimplificationSteps(relevantTo("tilingSet(p)"), vc("compressionSet(p) && ready(p)", "startTiling(p)"),