From b8f2b5692ff6da1850dbdc14f481321bff2b406d Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 5 Nov 2026 11:57:59 +0000 Subject: [PATCH] Show in Found only the facts about what Expected constrains The message's Found listed every path condition of the method, so a guard on another variable read as the reason for the error. It now keeps only the facts linked to the terms of Expected, the ones the counterexample already keeps, and reads 'expected but could not prove it' when none is left (for a state error, when none applies a state). The Found the IDE shows and the verification query are unchanged. Co-Authored-By: Claude Opus 5.5 --- .../diagnostics/errors/RefinementError.java | 33 ++++++++++++++++--- .../errors/StateRefinementError.java | 24 +++++++++++--- .../api/tests/TestGeneratedNames.java | 20 ++++++----- .../liquidjava/api/tests/TestStateHints.java | 7 ++++ .../RefinementErrorCounterexampleTest.java | 33 +++++++++++++++++++ 5 files changed, 99 insertions(+), 18 deletions(-) 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"),