Skip to content

Commit 2a9b40d

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
authored
Show in Found only the facts about the values Expected constrains (#485)
Closes #480. ## Problem The message's Found listed every path condition of the method, so a guard on another variable read as the reason for the error, and nothing was said about the variable Expected constrains. ## Change The message keeps only the facts of Found linked to the terms of Expected: the same `factsOf`/`linkedTerms` the counterexample already uses, exposed as one package-private `RefinementError.linkedToExpected` that `StateRefinementError` reuses. - When facts remain, the frames are unchanged: `X is not a subtype of Y` and `found X but expected Y`. When every fact is linked, Found is shown as written (e.g. `!(x < 0 || x > 5)`, not split). - When none remains (for a state error: none applies a ghost or state; an alias such as `box == getBox` says nothing about the state), the message reads `expected <refinement> but could not prove it`. Only the message text changes. The counterexample, hints, the Found the IDE shows and the verification query are unchanged. `TestGeneratedNames` now reads the whole Found of refinement errors, since the message no longer lists unrelated generated names. ## Before / after Reproducer 1 (refinement): ``` before: Refinement Error: !(port < 0 || port > 65535) is not a subtype of timeout >= 0 after: Refinement Error: expected timeout >= 0 but could not prove it Counterexample: timeout == -1 (unchanged) ``` Reproducer 2 (state): ``` before: State Refinement Error: found !(#isEmpty_result¹⁶ || #isEmpty_result¹⁷) && box¹⁵ == getBox¹³ but expected full(box¹⁵) after: State Refinement Error: expected full(box¹⁵) but could not prove it ``` Study exercise (JabRef `EditCommand`, fixture `state_hint_study_undo_manager_error`): ``` after: expected redoable(undoManager) but could not prove it ``` Facts that relate to Expected stay in the usual frame: - `!(port < 0 || retries > t)` with Expected `t >= 0` shows `!(retries > t) is not a subtype of t >= 0`; - a state reaching Expected through an alias: `found empty(b1) && box == b1 but expected full(box)`. ## Tests Each fails without the fix: - `RefinementErrorCounterexampleTest`: refinement reproducer, partial guard, Found kept as written when every fact is linked, state kept through an alias. - `TestStateHints`: the study's undo manager (state reproducer). Full suite passes locally (697 tests). Size: +99 / −18 over 5 files. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
1 parent 26506ff commit 2a9b40d

5 files changed

Lines changed: 99 additions & 18 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java‎

Lines changed: 28 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
import liquidjava.rj_language.ast.Enum;
1717
import liquidjava.rj_language.ast.Expression;
1818
import liquidjava.rj_language.ast.FunctionInvocation;
19+
import liquidjava.rj_language.ast.LiteralBoolean;
1920
import liquidjava.rj_language.ast.UnaryExpression;
2021
import liquidjava.rj_language.ast.Var;
2122
import liquidjava.rj_language.ast.formatter.VariableFormatter;
@@ -43,11 +44,7 @@ public class RefinementError extends LJError {
4344
public RefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
4445
VCSimplificationResult found, TranslationTable translationTable, Counterexample counterexample,
4546
String customMessage) {
46-
super("Refinement Error",
47-
String.format("%s is not a subtype of %s",
48-
found.getImplication().toPredicate().getExpression().toDisplayString(),
49-
expected.getExpression().toDisplayString()),
50-
position, translationTable, customMessage);
47+
super("Refinement Error", message(expected, found), position, translationTable, customMessage);
5148
this.expected = expected;
5249
this.found = found;
5350
this.counterexample = filterCounterexample(counterexample);
@@ -64,6 +61,32 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi
6461
"Not enough information to prove the expected refinement. Add a refinement or condition to constrain it."));
6562
}
6663

64+
// Only the facts of found about the values expected constrains; path conditions about other values stay in the
65+
// derivation
66+
private static String message(Predicate expected, VCSimplificationResult found) {
67+
Expression shown = linkedToExpected(found.getImplication().toPredicate().getExpression(),
68+
expected.getExpression());
69+
if (isTrue(shown))
70+
return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString());
71+
return String.format("%s is not a subtype of %s", shown.toDisplayString(),
72+
expected.getExpression().toDisplayString());
73+
}
74+
75+
/**
76+
* The facts of found linked to the terms of expected, as a conjunction, or true when there are none; found as
77+
* written when every fact is linked
78+
*/
79+
static Expression linkedToExpected(Expression found, Expression expected) {
80+
List<Expression> facts = factsOf(found);
81+
Set<String> linked = linkedTerms(facts, termsOf(expected));
82+
List<Expression> linkedFacts = facts.stream().filter(fact -> termsOf(fact).stream().anyMatch(linked::contains))
83+
.toList();
84+
if (linkedFacts.size() == facts.size())
85+
return found;
86+
return linkedFacts.stream().reduce((first, second) -> new BinaryExpression(first, "&&", second))
87+
.orElse(new LiteralBoolean(true));
88+
}
89+
6790
/** Unknown when what was found says nothing about the values the expected refinement constrains */
6891
private static ErrorCategory categoryOf(Predicate expected, VCSimplificationResult found) {
6992
List<String> foundVariables = found.getImplication().toPredicate().getVariableNames();

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java‎

Lines changed: 19 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,8 @@
99
import liquidjava.diagnostics.hints.Hint;
1010
import liquidjava.processor.VCImplication;
1111
import liquidjava.rj_language.Predicate;
12+
import liquidjava.rj_language.ast.Expression;
13+
import liquidjava.rj_language.ast.FunctionInvocation;
1214
import liquidjava.rj_language.opt.VCSimplificationResult;
1315
import spoon.reflect.cu.SourcePosition;
1416

@@ -27,11 +29,7 @@ public class StateRefinementError extends LJError {
2729
public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
2830
VCSimplificationResult found, TranslationTable translationTable, String customMessage, List<Hint> hints,
2931
ErrorCategory category, StateErrorContext context) {
30-
super("State Refinement Error",
31-
String.format("found %s but expected %s",
32-
found.getImplication().toPredicate().getExpression().toDisplayString(),
33-
expected.getExpression().toDisplayString()),
34-
position, translationTable, customMessage);
32+
super("State Refinement Error", message(expected, found), position, translationTable, customMessage);
3533
this.declarationPosition = declarationPosition;
3634
this.expected = expected;
3735
this.found = found;
@@ -43,6 +41,22 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP
4341
"No state information is known for this object. Make sure its state is initialized and available at this point."));
4442
}
4543

44+
// Only the facts of found about the objects of expected, and only when one of them tells a state: an alias or a
45+
// guard on another value says nothing about the state expected needs
46+
private static String message(Predicate expected, VCSimplificationResult found) {
47+
Expression shown = RefinementError.linkedToExpected(found.getImplication().toPredicate().getExpression(),
48+
expected.getExpression());
49+
if (!appliesGhost(shown))
50+
return String.format("expected %s but could not prove it", expected.getExpression().toDisplayString());
51+
return String.format("found %s but expected %s", shown.toDisplayString(),
52+
expected.getExpression().toDisplayString());
53+
}
54+
55+
private static boolean appliesGhost(Expression expression) {
56+
return expression instanceof FunctionInvocation
57+
|| expression.getChildren().stream().anyMatch(StateRefinementError::appliesGhost);
58+
}
59+
4660
@Override
4761
public SourcePosition getDeclarationPosition() {
4862
return declarationPosition;

‎liquidjava-verifier/src/test/java/liquidjava/api/tests/TestGeneratedNames.java‎

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99

1010
import liquidjava.api.CommandLineLauncher;
1111
import liquidjava.diagnostics.Diagnostics;
12+
import liquidjava.diagnostics.errors.RefinementError;
1213

1314
/**
1415
* Checks that the messages for {@code classes/generated_names_error} name each value the verifier introduces after what
@@ -19,15 +20,18 @@ class TestGeneratedNames {
1920
@Test
2021
void namesEachGeneratedValueAfterWhatItIs() {
2122
CommandLineLauncher.launch("../liquidjava-example/src/main/java/testSuite/classes/generated_names_error");
22-
Map<Integer, String> messages = Diagnostics.getInstance().getErrors().stream().collect(Collectors.toMap(
23-
error -> error.getPosition().getLine(), error -> error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")));
23+
// the whole Found of a refinement error, as the message keeps only the facts about the expected values
24+
Map<Integer, String> messages = Diagnostics.getInstance().getErrors().stream()
25+
.collect(Collectors.toMap(error -> error.getPosition().getLine(),
26+
error -> (error instanceof RefinementError refinement
27+
? refinement.getFound().getImplication().toPredicate().getExpression().toDisplayString()
28+
: error.getMessage()).replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", "")));
2429

25-
assertEquals(Map.of(25, "#if_condition == #ready_result && #if_condition is not a subtype of a > 0", 30,
26-
"#loop_condition == #ready_result && #loop_condition == true is not a subtype of a > 0", 34,
27-
"#ternary_condition == #ready_result && #ternary_condition == true is not a subtype of a < 0", 43,
28-
"!#try_branch && !#catch_branch is not a subtype of a > 0", 48,
29-
"x == #read_result - 1 is not a subtype of x > 0", 54,
30-
"#if_condition == #operation_result && #if_condition && x == 0 is not a subtype of x > 0", 58,
30+
assertEquals(Map.of(25, "#if_condition == #ready_result && #if_condition", 30,
31+
"#loop_condition == #ready_result && #loop_condition == true", 34,
32+
"#ternary_condition == #ready_result && #ternary_condition == true", 43,
33+
"!#try_branch && !#catch_branch", 48, "x == #read_result - 1", 54,
34+
"#if_condition == #operation_result && #if_condition && x == 0", 58,
3135
"found closed(#new_Door) but expected opened(#new_Door)"), messages);
3236
}
3337
}

‎liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -332,6 +332,13 @@ void checksOfTheStudysUndoManagerAreSuggestedOneAfterTheOther() {
332332
+ "canUndo(), canRedo() (and possibly others)"));
333333
}
334334

335+
@Test
336+
void foundOfTheStudysUndoManagerOmitsTheResultsOfOtherCalls() {
337+
StateRefinementError error = errors("classes/state_hint_study_undo_manager_error", 2).get(0);
338+
assertEquals("expected redoable(undoManager) but could not prove it",
339+
error.getMessage().replaceAll("[⁰¹²³⁴⁵⁶⁷⁸⁹]", ""));
340+
}
341+
335342
@Test
336343
void classWithoutStateSetKeepsTheGeneralHint() {
337344
assertHints("ErrorUnconstrainedStateRefinement.java", Hint.general(

‎liquidjava-verifier/src/test/java/liquidjava/diagnostics/errors/RefinementErrorCounterexampleTest.java‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
import liquidjava.diagnostics.TranslationTable;
1414
import liquidjava.processor.VCImplication;
1515
import liquidjava.rj_language.Predicate;
16+
import liquidjava.rj_language.opt.VCSimplificationResult;
1617
import liquidjava.rj_language.parsing.RefinementsParser;
1718
import liquidjava.smt.Counterexample;
1819
import liquidjava.utils.Pair;
@@ -114,6 +115,38 @@ void keepsAGuardThatRelatesExpectedToAnotherVariable() {
114115
assertEquals(List.of(pair("t", "-1"), pair("retries", "-2")), error.getCounterexample().assignments());
115116
}
116117

118+
@Test
119+
void messageSaysExpectedCouldNotBeProvedWhenFoundOnlyGuardsOtherVariables() {
120+
RefinementError error = error("timeout >= 0", vc("∀port:int. true", "∀timeout:int. true",
121+
"∀##if_condition_1:boolean. !(port < 0 || port > 65535)", "true"), "port=0", "timeout=-1");
122+
assertEquals("expected timeout >= 0 but could not prove it", error.getMessage());
123+
}
124+
125+
@Test
126+
void messageKeepsOnlyTheGuardsLinkedToExpected() {
127+
RefinementError error = error("t >= 0",
128+
vc("∀port:int. true", "∀retries:int. true", "∀t:int. true",
129+
"∀##if_condition_1:boolean. !(port < 0 || retries > t)", "true"),
130+
"port=0", "retries=-2", "t=-1");
131+
assertEquals("!(retries > t) is not a subtype of t >= 0", error.getMessage());
132+
}
133+
134+
@Test
135+
void messageKeepsFoundAsWrittenWhenEveryFactIsLinked() {
136+
RefinementError error = error("x >= 0", vc("∀x:int. !(x < 0 || x > 5)", "true"), "x=-1");
137+
assertEquals("!(x < 0 || x > 5) is not a subtype of x >= 0", error.getMessage());
138+
}
139+
140+
@Test
141+
void stateMessageKeepsAStateReachingExpectedThroughAnAlias() {
142+
StateRefinementError error = new StateRefinementError(null, null,
143+
new Predicate(RefinementsParser.createAST("full(box)", "")),
144+
new VCSimplificationResult(
145+
vc("∀b1:Object. empty(b1)", "∀x:int. x > 0", "∀box:Object. box == b1", "true")),
146+
new TranslationTable(), null, List.of(), null, null);
147+
assertEquals("found empty(b1) && box == b1 but expected full(box)", error.getMessage());
148+
}
149+
117150
@Test
118151
void omitsEnumValuesFoundAlreadyStates() {
119152
RefinementError error = error("f == Format.PNG && n > 0", vc("∀f:int. f == Format.JPG", "∀n:int. true", "true"),

0 commit comments

Comments
 (0)