Use found … but expected … for refinement errors, drop the general hint, declare every from

liquidjava-example/src/main/java/testSuite/ErrorStateRefinementEveryFrom.java

@@ -0,0 +1,20 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+// the call needs either entry state: the error declares both, each where its annotation writes it
+@StateSet(name = "door", value = {"shut", "ajar", "wide"})
+public class ErrorStateRefinementEveryFrom {
+
+    @StateRefinement(to = "wide(this)")
+    public ErrorStateRefinementEveryFrom() {}
+
+    @StateRefinement(from = "shut(this)", to = "ajar(this)")
+    @StateRefinement(from = "ajar(this)", to = "ajar(this)")
+    public void push() {}
+
+    public static void main(String[] args) {
+        new ErrorStateRefinementEveryFrom().push(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -70,6 +70,12 @@ public SourcePosition getDeclarationPosition() {
         return null;
     }
 
+    /** Where each part of the refinement is declared, the first being {@link #getDeclarationPosition()} */
+    public List<SourcePosition> getDeclarationPositions() {
+        SourcePosition declarationPosition = getDeclarationPosition();
+        return declarationPosition == null ? List.of() : List.of(declarationPosition);
+    }
+
     /** Lines printed under the message that explain it, such as what the names it uses mean */
     public List<String> getMessageNotes() {
         return List.of();
@@ -149,7 +155,7 @@ public String toString() {
         SourcePosition declPos = getDeclarationPosition();
         if (declPos != null && declPos.getFile() != null && !declPos.equals(position)) {
             sb.append(Colors.CYAN).append("\n--> Refinement declared here:\n").append(Colors.RESET);
-            String declarationSnippet = getSnippet(declPos, 1, 1, Colors.CYAN, null, true);
+            String declarationSnippet = getSnippet(getDeclarationPositions(), 1, 1, Colors.CYAN, null, true);
             if (declarationSnippet != null) {
                 sb.append(declarationSnippet);
                 for (String note : getDeclarationNotes())
@@ -164,22 +170,27 @@ public String toString() {
     }
 
     public String getSnippet() {
-        return getSnippet(position, 2, 2, accentColor, customMessage, false);
+        return position == null ? null : getSnippet(List.of(position), 2, 2, accentColor, customMessage, false);
     }
 
-    private String getSnippet(SourcePosition snippetPosition, int contextBefore, int contextAfter, String markerColor,
+    // One excerpt of the file of the first position, marking each position in that file
+    private String getSnippet(List<SourcePosition> positions, int contextBefore, int contextAfter, String markerColor,
             String markerMessage, boolean firstLineOnly) {
-        if (snippetPosition == null || snippetPosition.getFile() == null)
+        if (positions.isEmpty() || positions.get(0).getFile() == null)
             return null;
 
-        Path path = snippetPosition.getFile().toPath();
+        Path path = positions.get(0).getFile().toPath();
+        List<SourcePosition> marked = positions.stream()
+                .filter(p -> p.getFile() != null && p.getFile().toPath().equals(path)).toList();
         try {
             List<String> lines = Files.readAllLines(path);
             StringBuilder sb = new StringBuilder();
 
-            int startLine = Math.max(1, snippetPosition.getLine() - contextBefore);
-            int highlightedEndLine = firstLineOnly ? snippetPosition.getLine() : snippetPosition.getEndLine();
-            int endLine = Math.min(lines.size(), highlightedEndLine + contextAfter);
+            int startLine = Math.max(1,
+                    marked.stream().mapToInt(SourcePosition::getLine).min().getAsInt() - contextBefore);
+            int endLine = Math.min(lines.size(),
+                    marked.stream().mapToInt(p -> highlightedEndLine(p, firstLineOnly)).max().getAsInt()
+                            + contextAfter);
 
             // calculate padding for line numbers
             int padding = String.valueOf(endLine).length();
@@ -193,31 +204,34 @@ private String getSnippet(SourcePosition snippetPosition, int contextBefore, int
                 sb.append(Colors.GREY).append(lineNumStr).append(PIPE).append(line).append(Colors.RESET).append("\n");
 
                 // add error markers on the line(s) with the error
-                if (i >= snippetPosition.getLine() && i <= highlightedEndLine) {
-                    int colStart = (i == snippetPosition.getLine()) ? snippetPosition.getColumn() : 1;
-                    int colEnd = (i == snippetPosition.getEndLine()) ? snippetPosition.getEndColumn()
-                            : rawLine.length();
-
-                    if (colStart > 0 && colEnd > 0) {
-                        int tabsBeforeStart = (int) rawLine.substring(0, Math.max(0, colStart - 1)).chars()
-                                .filter(ch -> ch == '\t').count();
-                        int tabsBeforeEnd = (int) rawLine.substring(0, Math.max(0, colEnd)).chars()
-                                .filter(ch -> ch == '\t').count();
-                        int visualColStart = colStart + tabsBeforeStart * 3;
-                        int visualColEnd = colEnd + tabsBeforeEnd * 3;
-
-                        // line number padding + pipe + column offset
-                        String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET
-                                + " ".repeat(visualColStart - 1);
-                        String markers = markerColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1));
-                        sb.append(indent).append(markers);
-
-                        // custom message
-                        if (markerMessage != null && !markerMessage.isBlank()) {
-                            String offset = " ".repeat(padding + visualColEnd + PIPE.length() + 1);
-                            sb.append(" " + markerMessage.replace("\n", "\n" + offset));
+                for (SourcePosition snippetPosition : marked) {
+                    int highlightedEndLine = highlightedEndLine(snippetPosition, firstLineOnly);
+                    if (i >= snippetPosition.getLine() && i <= highlightedEndLine) {
+                        int colStart = (i == snippetPosition.getLine()) ? snippetPosition.getColumn() : 1;
+                        int colEnd = (i == snippetPosition.getEndLine()) ? snippetPosition.getEndColumn()
+                                : rawLine.length();
+
+                        if (colStart > 0 && colEnd > 0) {
+                            int tabsBeforeStart = (int) rawLine.substring(0, Math.max(0, colStart - 1)).chars()
+                                    .filter(ch -> ch == '\t').count();
+                            int tabsBeforeEnd = (int) rawLine.substring(0, Math.max(0, colEnd)).chars()
+                                    .filter(ch -> ch == '\t').count();
+                            int visualColStart = colStart + tabsBeforeStart * 3;
+                            int visualColEnd = colEnd + tabsBeforeEnd * 3;
+
+                            // line number padding + pipe + column offset
+                            String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET
+                                    + " ".repeat(visualColStart - 1);
+                            String markers = markerColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1));
+                            sb.append(indent).append(markers);
+
+                            // custom message
+                            if (markerMessage != null && !markerMessage.isBlank()) {
+                                String offset = " ".repeat(padding + visualColEnd + PIPE.length() + 1);
+                                sb.append(" " + markerMessage.replace("\n", "\n" + offset));
+                            }
+                            sb.append(Colors.RESET).append("\n");
                         }
-                        sb.append(Colors.RESET).append("\n");
                     }
                 }
             }
@@ -227,6 +241,10 @@ private String getSnippet(SourcePosition snippetPosition, int contextBefore, int
         }
     }
 
+    private static int highlightedEndLine(SourcePosition position, boolean firstLineOnly) {
+        return firstLineOnly ? position.getLine() : position.getEndLine();
+    }
+
     @Override
     public boolean equals(Object obj) {
         if (this == obj)

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

@@ -13,7 +13,6 @@
 import liquidjava.diagnostics.AliasExpansion;
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.diagnostics.categories.ErrorCategory;
-import liquidjava.diagnostics.hints.Hint;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.BinaryExpression;
@@ -54,7 +53,7 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi
             String customMessage, List<AliasWrapper> aliases) {
         super("Refinement Error",
                 ErrorMessage.of(expected.getExpression(), found, translationTable, shown -> !isTrue(shown),
-                        "%s is not a subtype of %s", UnaryOperator.identity()),
+                        "found %s but expected %s", UnaryOperator.identity()),
                 position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
@@ -72,9 +71,6 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi
             setCounterexampleStr("Counterexample: " + counterexampleString);
         }
         setCategory(categoryOf(expected, found));
-        if (isTrue(found.getImplication().toPredicate().getExpression()))
-            addHint(Hint.general(
-                    "Not enough information to prove the expected refinement. Add a refinement or condition to constrain it."));
     }
 
     // Each alias the message uses once, with those their definitions use, as declared

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

@@ -24,25 +24,27 @@ public class StateRefinementError extends LJError {
 
     private final Predicate expected;
     private final VCSimplificationResult found;
-    private final SourcePosition declarationPosition;
+    private final List<SourcePosition> declarationPositions;
     private final StateErrorContext context;
     private final List<String> declarationNotes;
 
     /**
+     * @param declarationPositions
+     *            where each entry state that makes up expected is declared
      * @param display
      *            rewrites expected and found as the error shows them, here and to the IDE, after the facts to show are
      *            chosen on them as given
      * @param declarationNotes
      *            lines that explain the declaration, printed under its excerpt
      */
-    public StateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate expected,
+    public StateRefinementError(SourcePosition position, List<SourcePosition> declarationPositions, Predicate expected,
             VCSimplificationResult found, TranslationTable translationTable, String customMessage, List<Hint> hints,
             ErrorCategory category, StateErrorContext context, UnaryOperator<Expression> display,
             List<String> declarationNotes) {
         super("State Refinement Error", ErrorMessage.of(expected.getExpression(), found, translationTable,
                 StateRefinementError::appliesGhost, "found %s but expected %s", display), position, translationTable,
                 customMessage);
-        this.declarationPosition = declarationPosition;
+        this.declarationPositions = declarationPositions;
         this.expected = new Predicate(display.apply(expected.getExpression()));
         this.found = found.map(display);
         this.context = context;
@@ -68,7 +70,12 @@ public List<String> getDeclarationNotes() {
 
     @Override
     public SourcePosition getDeclarationPosition() {
-        return declarationPosition;
+        return declarationPositions.isEmpty() ? null : declarationPositions.get(0);
+    }
+
+    @Override
+    public List<SourcePosition> getDeclarationPositions() {
+        return declarationPositions;
     }
 
     public Predicate getExpected() {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -613,14 +613,14 @@ public void throwRefinementError(SourcePosition position, SourcePosition declara
 
     public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found,
             Predicate expected, String customMessage) throws LJError {
-        throwStateRefinementError(position, declarationPosition, found, expected, customMessage, List.of(), null, null,
-                List.of());
+        throwStateRefinementError(position, List.of(declarationPosition), found, expected, customMessage, List.of(),
+                null, null, List.of());
     }
 
-    public void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition, Predicate found,
-            Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category,
+    public void throwStateRefinementError(SourcePosition position, List<SourcePosition> declarationPositions,
+            Predicate found, Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category,
             StateErrorContext context, List<String> declarationNotes) throws LJError {
-        vcChecker.throwStateRefinementError(position, declarationPosition, found, expected, customMessage, hints,
+        vcChecker.throwStateRefinementError(position, declarationPositions, found, expected, customMessage, hints,
                 category, context, declarationNotes);
     }
 

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -455,15 +455,15 @@ protected Predicate shownFound(Predicate found, Predicate expected) {
         return buildPremiseChain(new TranslationTable(), expected, found).simplify().getImplication().toPredicate();
     }
 
-    protected void throwStateRefinementError(SourcePosition position, SourcePosition declarationPosition,
+    protected void throwStateRefinementError(SourcePosition position, List<SourcePosition> declarationPositions,
             Predicate found, Predicate expected, String customMessage, List<Hint> hints, ErrorCategory category,
             StateErrorContext context, List<String> declarationNotes) throws StateRefinementError {
         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));
-        throw new StateRefinementError(position, declarationPosition, expected, shown, map, customMessage, hints,
+        throw new StateRefinementError(position, declarationPositions, expected, shown, map, customMessage, hints,
                 category, context,
                 e -> StateValues.toSetForm(e, this.context.getGhostStates(), this.context.getGhosts()),
                 declarationNotes);

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -417,13 +417,13 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
             Predicate written = new Predicate(from, e, prefix);
             state.setWrittenFrom(written);
             state.setFrom(createStatePredicate(written, from, f.getTargetClass(), tc, e, false));
-            state.setFromPosition(Utils.getLJAnnotationPosition(e, from));
+            state.setFromPosition(valuePosition(m.get("from"), e, from));
         }
 
         // has to
         if (to != null) {
             state.setTo(createStatePredicate(new Predicate(to, e, prefix), to, f.getTargetClass(), tc, e, true));
-            state.setToPosition(Utils.getLJAnnotationPosition(e, to));
+            state.setToPosition(valuePosition(m.get("to"), e, to));
         }
 
         // has to but not from, state enters with true
@@ -433,6 +433,12 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
         return state;
     }
 
+    // Where this annotation writes a literal value, since another annotation of the element may write the same text
+    private static SourcePosition valuePosition(CtExpression<?> value, CtElement element, String written) {
+        SourcePosition position = value instanceof CtLiteral<?> ? Utils.getAnnotationValuePosition(value) : null;
+        return position != null ? position : Utils.getLJAnnotationPosition(element, written);
+    }
+
     /**
      * Creates the predicate for state transition
      * 
@@ -796,12 +802,16 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc
             // combine messages of all state changes
             String message = stateChanges.stream().map(ObjectState::getMessage)
                     .filter(msg -> msg != null && !msg.isBlank()).distinct().collect(Collectors.joining("\n"));
-            Optional<ObjectState> declaration = stateChanges.stream().filter(ObjectState::hasFrom)
-                    .filter(s -> s.getFromPosition() != null).findFirst();
-            SourcePosition declarationPosition = declaration.map(ObjectState::getFromPosition)
-                    .orElse(function.getPlacementInCode().getPosition());
-            List<String> declarationNotes = declaration.map(ObjectState::getWrittenFrom).filter(Objects::nonNull)
-                    .map(written -> declarationNotes(written.getExpression(), tc.getContext())).orElse(List.of());
+            // every entry state that makes up expected, each with what its states mean
+            List<ObjectState> declarations = stateChanges.stream().filter(ObjectState::hasFrom)
+                    .filter(s -> s.getFromPosition() != null).toList();
+            List<SourcePosition> declarationPositions = declarations.isEmpty()
+                    ? List.of(function.getPlacementInCode().getPosition())
+                    : declarations.stream().map(ObjectState::getFromPosition).toList();
+            List<String> declarationNotes = declarations.stream().map(ObjectState::getWrittenFrom)
+                    .filter(Objects::nonNull)
+                    .flatMap(written -> declarationNotes(written.getExpression(), tc.getContext()).stream()).distinct()
+                    .toList();
             List<GhostState> ghostStates = getGhostStatesFor(function.getTargetClass(), tc);
             Optional<DecidingArgument> deciding = decidingArgument(tc, vi, function, ghostStates, invocation);
             Optional<ReceiverStates> states = receiverStates(tc, function, vi, prevState, invocation);
@@ -817,7 +827,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc
             StateErrorContext context = states
                     .map(r -> StateErrorContext.of(r.machine(), function, r.current(), writtenReceiver(invocation)))
                     .orElse(null);
-            tc.throwStateRefinementError(invocation.getPosition(), declarationPosition, prevState,
+            tc.throwStateRefinementError(invocation.getPosition(), declarationPositions, prevState,
                     expectedStatesDisjunction, message, hints, category, context, declarationNotes);
         }
     }