Show in Found only the facts about the values Expected constrains

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<Expression> facts = factsOf(found);
+        Set<String> linked = linkedTerms(facts, termsOf(expected));
+        List<Expression> 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<String> foundVariables = found.getImplication().toPredicate().getVariableNames();

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<Hint> 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;

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<Integer, String> 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<Integer, String> 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);
     }
 }

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(

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"),