diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 1b82977d..22e275b8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -16,6 +16,7 @@ import liquidjava.rj_language.ast.Enum; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.ast.FunctionInvocation; +import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.ast.formatter.VariableFormatter; @@ -43,11 +44,7 @@ public class RefinementError extends LJError { public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected, VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample, String customMessage) { - super("Refinement Error", - String.format("%s is not a subtype of %s", - found.getImplication().toPredicate().getExpression().toDisplayString(), - expected.getExpression().toDisplayString()), - position, translationTable, customMessage); + super("Refinement Error", message(expected, found), position, translationTable, customMessage); this.expected = expected; this.found = found; this.counterexample = filterCounterexample(counterexample); @@ -64,6 +61,32 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi "Not enough information to prove the expected refinement. Add a refinement or condition to constrain it.")); } + // Only the facts of found about the values expected constrains; path conditions about other values stay in the + // derivation + private static String message(Predicate expected, VCSimplificationResult found) { + Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(), + expected.getExpression()); + if (isTrue(shown)) + return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString()); + return String.format("%s is not a subtype of %s", shown.toDisplayString(), + expected.getExpression().toDisplayString()); + } + + /** + * The facts of found linked to the terms of expected, as a conjunction, or true when there are none; found as + * written when every fact is linked + */ + static Expression linkedToExpected(Expression found, Expression expected) { + List facts = factsOf(found); + Set linked = linkedTerms(facts, termsOf(expected)); + List linkedFacts = facts.stream().filter(fact -> termsOf(fact).stream().anyMatch(linked::contains)) + .toList(); + if (linkedFacts.size() == facts.size()) + return found; + return linkedFacts.stream().reduce((first, second) -> new BinaryExpression(first, "&&", second)) + .orElse(new LiteralBoolean(true)); + } + /** Unknown when what was found says nothing about the values the expected refinement constrains */ private static ErrorCategory categoryOf(Predicate expected, VCSimplificationResult found) { List foundVariables = found.getImplication().toPredicate().getVariableNames(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index 4bc2994e..c0ff6bcb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -9,6 +9,8 @@ import liquidjava.diagnostics.hints.Hint; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.FunctionInvocation; import liquidjava.rj_language.opt.VCSimplificationResult; import spoon.reflect.cu.SourcePosition; @@ -27,11 +29,7 @@ public class StateRefinementError extends LJError { public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected, VCSimplificationResult found, TranslationTable translationTable, String customMessage, List hints, ErrorCategory category, StateErrorContext context) { - super("State Refinement Error", - String.format("found %s but expected %s", - found.getImplication().toPredicate().getExpression().toDisplayString(), - expected.getExpression().toDisplayString()), - position, translationTable, customMessage); + super("State Refinement Error", message(expected, found), position, translationTable, customMessage); this.declarationPosition = declarationPosition; this.expected = expected; this.found = found; @@ -43,6 +41,22 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP "No state information is known for this object. Make sure its state is initialized and available at this point.")); } + // Only the facts of found about the objects of expected, and only when one of them tells a state: an alias or a + // guard on another value says nothing about the state expected needs + private static String message(Predicate expected, VCSimplificationResult found) { + Expression shown = RefinementError.linkedToExpected(found.getImplication().toPredicate().getExpression(), + expected.getExpression()); + if (!appliesGhost(shown)) + return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString()); + return String.format("found %s but expected %s", shown.toDisplayString(), + expected.getExpression().toDisplayString()); + } + + private static boolean appliesGhost(Expression expression) { + return expression instanceof FunctionInvocation + || expression.getChildren().stream().anyMatch(StateRefinementError::appliesGhost); + } + @Override public SourcePosition getDeclarationPosition() { return declarationPosition; diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java index c0d16143..ade19e64 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java @@ -9,6 +9,7 @@ import liquidjava.api.CommandLineLauncher; import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.RefinementError; /** * Checks that the messages for {@code classes/generated_names_error} name each value the verifier introduces after what @@ -19,15 +20,18 @@ class TestGeneratedNames { @Test void namesEachGeneratedValueAfterWhatItIs() { CommandLineLauncher.launch("../liquidjava-example/src/main/java/testSuite/classes/generated_names_error"); - Map messages = Diagnostics.getInstance().getErrors().stream().collect(Collectors.toMap( - error -> error.getPosition().getLine(), error -> error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""))); + // the whole Found of a refinement error, as the message keeps only the facts about the expected values + Map messages = Diagnostics.getInstance().getErrors().stream() + .collect(Collectors.toMap(error -> error.getPosition().getLine(), + error -> (error instanceof RefinementError refinement + ? refinement.getFound().getImplication().toPredicate().getExpression().toDisplayString() + : error.getMessage()).replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""))); - assertEquals(Map.of(25, "#if_condition == #ready_result && #if_condition is not a subtype of a > 0", 30, - "#loop_condition == #ready_result && #loop_condition == true is not a subtype of a > 0", 34, - "#ternary_condition == #ready_result && #ternary_condition == true is not a subtype of a < 0", 43, - "!#try_branch && !#catch_branch is not a subtype of a > 0", 48, - "x == #read_result - 1 is not a subtype of x > 0", 54, - "#if_condition == #operation_result && #if_condition && x == 0 is not a subtype of x > 0", 58, + assertEquals(Map.of(25, "#if_condition == #ready_result && #if_condition", 30, + "#loop_condition == #ready_result && #loop_condition == true", 34, + "#ternary_condition == #ready_result && #ternary_condition == true", 43, + "!#try_branch && !#catch_branch", 48, "x == #read_result - 1", 54, + "#if_condition == #operation_result && #if_condition && x == 0", 58, "found closed(#new_Door) but expected opened(#new_Door)"), messages); } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 42f7d494..3429e5ee 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java @@ -332,6 +332,13 @@ void checksOfTheStudysUndoManagerAreSuggestedOneAfterTheOther() { + "canUndo(), canRedo() (and possibly others)")); } + @Test + void foundOfTheStudysUndoManagerOmitsTheResultsOfOtherCalls() { + StateRefinementError error = errors("classes/state_hint_study_undo_manager_error", 2).get(0); + assertEquals("expected redoable(undoManager) but could not prove it", + error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")); + } + @Test void classWithoutStateSetKeepsTheGeneralHint() { assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general( diff --git a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java index d9930d5d..863f761b 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java @@ -13,6 +13,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.opt.VCSimplificationResult; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.smt.Counterexample; import liquidjava.utils.Pair; @@ -114,6 +115,38 @@ void keepsAGuardThatRelatesExpectedToAnotherVariable() { assertEquals(List.of(pair("t", "-1"), pair("retries", "-2")), error.getCounterexample().assignments()); } + @Test + void messageSaysExpectedCouldNotBeProvedWhenFoundOnlyGuardsOtherVariables() { + RefinementError error = error("timeout >= 0", vc("∀port:int. true", "∀timeout:int. true", + "∀##if_condition_1:boolean. !(port < 0 || port > 65535)", "true"), "port=0", "timeout=-1"); + assertEquals("expected timeout >= 0 but could not prove it", error.getMessage()); + } + + @Test + void messageKeepsOnlyTheGuardsLinkedToExpected() { + RefinementError error = error("t >= 0", + vc("∀port:int. true", "∀retries:int. true", "∀t:int. true", + "∀##if_condition_1:boolean. !(port < 0 || retries > t)", "true"), + "port=0", "retries=-2", "t=-1"); + assertEquals("!(retries > t) is not a subtype of t >= 0", error.getMessage()); + } + + @Test + void messageKeepsFoundAsWrittenWhenEveryFactIsLinked() { + RefinementError error = error("x >= 0", vc("∀x:int. !(x < 0 || x > 5)", "true"), "x=-1"); + assertEquals("!(x < 0 || x > 5) is not a subtype of x >= 0", error.getMessage()); + } + + @Test + void stateMessageKeepsAStateReachingExpectedThroughAnAlias() { + StateRefinementError error = new StateRefinementError(null, null, + new Predicate(RefinementsParser.createAST("full(box)", "")), + new VCSimplificationResult( + vc("∀b1:Object. empty(b1)", "∀x:int. x > 0", "∀box:Object. box == b1", "true")), + new TranslationTable(), null, List.of(), null, null); + assertEquals("found empty(b1) && box == b1 but expected full(box)", error.getMessage()); + } + @Test void omitsEnumValuesFoundAlreadyStates() { RefinementError error = error("f == Format.PNG && n > 0", vc("∀f:int. f == Format.JPG", "∀n:int. true", "true"),