Further improvements on error message reporting

key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java

@@ -8,6 +8,8 @@
 import java.nio.file.Path;
 import java.util.*;
 import java.util.concurrent.atomic.AtomicInteger;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 import java.util.stream.Collectors;
 
 import de.uka.ilkd.key.java.ast.JPContext;
@@ -216,13 +218,63 @@ static String simplifyJavaParserMessage(@Nullable String message) {
             String head = result.substring(0, idx);
             String[] items =
                 result.substring(idx + "expected one of".length()).trim().split("\\s+");
-            final int limit = 6;
-            if (items.length > limit) {
-                result = head + "expected one of "
-                    + String.join(" ", Arrays.copyOf(items, limit)) + " ...";
+            // Drop JavaCard / schema-internal alternatives (e.g. "#abortJavaCardTransaction");
+            // they are noise for ordinary Java source and otherwise crowd out the relevant ones.
+            List<String> relevant = Arrays.stream(items)
+                    .filter(t -> !t.startsWith("\"#"))
+                    .collect(Collectors.toList());
+            if (relevant.isEmpty()) {
+                relevant = Arrays.asList(items);
             }
+            final int limit = 6;
+            String list = relevant.size() > limit
+                    ? String.join(" ", relevant.subList(0, limit)) + " ..."
+                    : String.join(" ", relevant);
+            result = head + "expected one of " + list;
         }
-        return result;
+        return humanizeJavaParserJargon(cleanFoundToken(result));
+    }
+
+    /**
+     * Rewrites JavaParser symbol-solver jargon into the user-facing wording KeY uses elsewhere:
+     * {@code "Unsolved symbol : Foobar"} becomes {@code "Cannot resolve 'Foobar'. No variable,
+     * field, or type with this name is in scope here (check for typos)."}. Text without that jargon
+     * is returned unchanged.
+     *
+     * @param message a message that may contain JavaParser symbol-solver jargon
+     * @return the message with that jargon humanized
+     */
+    public static String humanizeJavaParserJargon(@Nullable String message) {
+        if (message == null) {
+            return "";
+        }
+        return message.replaceAll("Unsolved symbol\\s*:\\s*([A-Za-z_$][\\w$.]*)",
+            "Cannot resolve '$1'. No variable, field, or type with this name is in scope here "
+                + "(check for typos)");
+    }
+
+    /**
+     * The offending token quoted in a JavaParser message can be a multi-line construct (e.g. a
+     * block comment); its raw text - with (escaped) line breaks - makes the message span many
+     * lines. Collapse the internal whitespace of that quoted {@code unexpected "..."} token to
+     * single spaces and shorten it if very long, so the message stays on one readable line.
+     *
+     * @param message a JavaParser message whose lead-in has already been rewritten
+     * @return the message with its offending token collapsed to a single line
+     */
+    private static String cleanFoundToken(String message) {
+        // JavaParser writes the offending token as {@code unexpected "..."} (note: it can use more
+        // than one space); match one-or-more spaces so the token is found and collapsed.
+        Matcher m = Pattern.compile("unexpected\\s+\"(.*?)\"", Pattern.DOTALL).matcher(message);
+        if (!m.find()) {
+            return message;
+        }
+        String token = m.group(1).replaceAll("\\\\[nrt]|\\s+", " ").trim();
+        final int max = 60;
+        if (token.length() > max) {
+            token = token.substring(0, max) + "…";
+        }
+        return message.substring(0, m.start(1)) + token + message.substring(m.end(1));
     }
 
     // region parsing of compilation units

key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java

@@ -162,12 +162,17 @@ public static KeyAst.File parseFile(CharStream stream) {
         try {
             ctx = p.file();
         } catch (ParseCancellationException ex) {
-            LOGGER.warn("SLL was not enough");
+            LOGGER.warn("SLL was not enough; retrying with LL and error recovery");
+            // Re-parse with LL prediction and ANTLR's default error recovery so that ALL syntax
+            // errors are collected (the bail strategy above stops at the first). To avoid
+            // regressing the polished single-error message and position, keep the bail-path
+            // exception when recovery finds exactly one error; report the whole list only when
+            // there are several. Zero errors means SLL was merely insufficient and the LL parse
+            // actually succeeded - fall through and return the tree.
             stream.seek(0);
             p = createParser(stream);
-            p.setErrorHandler(new BailErrorStrategy());
             ctx = p.file();
-            if (p.getErrorReporter().hasErrors()) {
+            if (p.getErrorReporter().errorCount() == 1) {
                 throw ex;
             }
         }

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java

@@ -670,6 +670,7 @@ private PairOfStringAndJavaBlock getJavaBlock(Token t) {
                 String reason = ExceptionTools.getMessages(e).stream()
                         .map(de.uka.ilkd.key.speclang.PositionedString::getText)
                         .collect(Collectors.joining("\n"));
+                reason = JavaService.humanizeJavaParserJargon(reason);
                 throw new BuildingException(t, pos,
                     "Could not parse Java block '" + cleanJava + "':\n" + reason,
                     e);

key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java

@@ -208,7 +208,8 @@ public void beginExpr(ProofElementID eid, String str) {
                     ((BuiltinRuleInformation) ruleInfo).currPredAbstraLatticeType =
                         (Class<? extends AbstractPredicateAbstractionLattice>) Class.forName(str);
                 } catch (ClassNotFoundException e) {
-                    errors.add(e);
+                    errors.add(new IllegalArgumentException(
+                        "Unknown predicate abstraction lattice type \"" + str + "\".", e));
                 }
             }
             case MERGE_ABSTRACTION_PREDICATES ->

key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java

@@ -381,7 +381,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener,
                 // Default exception catcher -- proof should not stop loading
                 // if anything goes wrong, but instead continue with the next
                 // node in the queue.
-                reportError(ERROR_LOADING_PROOF_LINE, throwable);
+                reportError(ERROR_LOADING_PROOF_LINE + "Node " + currNode.serialNr(), throwable);
             }
         }
         if (listener != null) {
@@ -502,7 +502,10 @@ private TacletApp constructTacletApp(TacletAppIntermediate currInterm, Goal curr
             } catch (TacletAppConstructionException e) {
                 throw e;
             } catch (Exception e) {
-                throw new TacletAppConstructionException("Wrong position information: " + pos, e);
+                throw new TacletAppConstructionException(
+                    "Could not reconstruct the rule application: the stored position does not fit "
+                        + "the current sequent (" + pos + ").",
+                    e);
             }
         }
 
@@ -671,7 +674,11 @@ private IBuiltInRuleApp constructBuiltinApp(BuiltInAppIntermediate currInterm, G
                 pos = PosInOccurrence
                         .findInSequent(currGoal.sequent(), currFormula, currPosInTerm);
             } catch (RuntimeException e) {
-                throw new BuiltInConstructionException("Wrong position information.", e);
+                throw new BuiltInConstructionException(
+                    "Could not reconstruct the rule application: the stored position (formula "
+                        + currFormula + ", term " + currPosInTerm
+                        + ") could not be located in the current sequent.",
+                    e);
             }
         }
 
@@ -858,7 +865,7 @@ private MergeRuleBuiltInRuleApp instantiateJoinApp(final MergeAppIntermediate jo
      * @param e Error encountered.
      */
     private void reportError(String string, Throwable e) {
-        status = "Errors while reading the proof. Not all branches could be load successfully.";
+        status = "Errors while reading the proof. Not all branches could be loaded successfully.";
         errors.add(new ProblemLoaderException(loader, string, e));
     }
 
@@ -908,9 +915,16 @@ public static TacletApp constructInsts(@NonNull TacletApp app, Goal currGoal,
 
             SchemaVariable sv = lookupName(uninsts, varname);
             if (sv == null) {
-                // throw new IllegalStateException(
-                // varname+" from \n"+loadedInsts+"\n is not in\n"+uninsts);
-                LOGGER.error("{} from {} is not in uninsts", varname, app.rule().name());
+                // Tolerated inconsistency: the stored instantiation names a schema variable that is
+                // not among the rule's uninstantiated variables (e.g. a proof saved with a slightly
+                // different version of the rule). We skip this single instantiation and continue
+                // the
+                // replay instead of aborting (this was once a hard IllegalStateException); the skip
+                // is logged so it can be diagnosed if the replay result looks wrong.
+                LOGGER.warn(
+                    "Skipping instantiation \"{}\": schema variable \"{}\" is not among the "
+                        + "uninstantiated variables of rule \"{}\".",
+                    s, varname, app.rule().name());
                 continue;
             }
             final String value = s.substring(eq + 1);
@@ -975,8 +989,7 @@ public static JTerm parseTerm(String value, Proof proof, Namespace<QuantifiableV
                 proof.getNamespaces().parametricFunctions(),
                 progVarNS, new AbbrevMap());
         } catch (ParserException e) {
-            throw new RuntimeException(
-                "Error while parsing value " + value + "\nVar namespace is: " + varNS + "\n", e);
+            throw new RuntimeException("Error while parsing the value \"" + value + "\".", e);
         }
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoaderException.java

@@ -3,26 +3,63 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof.io;
 
+import java.util.List;
+
 
 public final class ProblemLoaderException extends Exception {
 
     private static final long serialVersionUID = 5683051720482052601L;
     private final AbstractProblemLoader origin;
 
+    /**
+     * Several sub-problems bundled into this single exception (e.g. all rule applications that
+     * could
+     * not be replayed). Empty for an ordinary single-cause exception. Lets the message extraction
+     * ({@link de.uka.ilkd.key.util.ExceptionTools#getMessages}) surface every problem instead of
+     * only the first.
+     */
+    private final List<Throwable> subExceptions;
+
     public ProblemLoaderException(AbstractProblemLoader origin, String msg, Throwable cause) {
         super(msg, cause);
         this.origin = origin;
+        this.subExceptions = List.of();
     }
 
     public ProblemLoaderException(AbstractProblemLoader origin, String msg) {
         super(msg);
         this.origin = origin;
+        this.subExceptions = List.of();
+    }
+
+    /**
+     * Bundles several problems into one exception. The summary {@code msg} describes them; the
+     * first
+     * sub-exception is kept as the {@link #getCause() cause}, and the full list is available via
+     * {@link #getSubExceptions()}.
+     *
+     * @param origin the loader that produced the problems
+     * @param msg a summary message
+     * @param subExceptions the individual problems (must not be empty)
+     */
+    public ProblemLoaderException(AbstractProblemLoader origin, String msg,
+            List<Throwable> subExceptions) {
+        super(msg, subExceptions.isEmpty() ? null : subExceptions.get(0));
+        this.origin = origin;
+        this.subExceptions = List.copyOf(subExceptions);
     }
 
     public AbstractProblemLoader getOrigin() {
         return origin;
     }
 
+    /**
+     * @return the bundled sub-problems, or an empty list for an ordinary single-cause exception
+     */
+    public List<Throwable> getSubExceptions() {
+        return subExceptions;
+    }
+
     @Override
     public String toString() {
         StringBuffer sb = new StringBuffer();

key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java

@@ -22,6 +22,7 @@
 import de.uka.ilkd.key.util.parsing.BuildingExceptions;
 import de.uka.ilkd.key.util.parsing.BuildingIssue;
 import de.uka.ilkd.key.util.parsing.HasLocation;
+import de.uka.ilkd.key.util.parsing.SyntaxErrorReporter;
 
 import org.antlr.v4.runtime.InputMismatchException;
 import org.antlr.v4.runtime.IntStream;
@@ -115,6 +116,22 @@ public static String getMessage(Throwable throwable) {
         List<PositionedString> result = new ArrayList<>();
         // Search the cause chain for an exception that bundles several located issues.
         for (Throwable e = throwable; e != null; e = e.getCause()) {
+            if (e instanceof ProblemLoaderException ple && !ple.getSubExceptions().isEmpty()) {
+                // e.g. a partial proof replay: report every rule application that failed, led by
+                // the summary, instead of only the first.
+                result.add(new PositionedString(ple.getMessage(), safeLocation(ple)));
+                for (Throwable sub : ple.getSubExceptions()) {
+                    result.add(new PositionedString(subErrorText(sub), safeLocation(sub)));
+                }
+                break;
+            }
+            if (e instanceof SyntaxErrorReporter.ParserException pe && pe.getErrors().size() > 1) {
+                // several syntax errors collected from one file: report each with its own location
+                for (SyntaxErrorReporter.SyntaxError se : pe.getErrors()) {
+                    result.add(new PositionedString(se.getMessage(), se.getLocation()));
+                }
+                break;
+            }
             if (e instanceof BuildingExceptions be) {
                 for (BuildingIssue issue : be.getErrors()) {
                     result.add(issue.asPositionedString());
@@ -153,6 +170,17 @@ private static Location safeLocation(Throwable t) {
         }
     }
 
+    /**
+     * Message for a bundled sub-problem. Prefers the exception's own message (which, for the
+     * replay errors, carries the contextual "Line .., goal .., rule .." text); only when it has
+     * none do we fall back to {@link #getMessage} (which would otherwise unwrap a
+     * {@link ProblemLoaderException} to its cause and drop that context).
+     */
+    private static String subErrorText(Throwable sub) {
+        String own = sub.getMessage();
+        return (own != null && !own.isBlank()) ? own : getMessage(sub);
+    }
+
     public static String getNiceMessage(InputMismatchException ime) {
         return getNiceMessageInternal(ime.getInputStream(), ime.getOffendingToken(),
             ime.getRecognizer().getVocabulary(), ime.getExpectedTokens());
@@ -313,27 +341,51 @@ private static String friendlyTokenName(Vocabulary vocabulary, int tokenType) {
      */
     private static @Nullable Location reportLocationFor(InputMismatchException ime) {
         Token offending = ime.getOffendingToken();
-        if (!expectsOnlyClosingToken(ime) || offending == null
-                || !(ime.getInputStream() instanceof TokenStream ts)) {
+        // Single-error path: only redirect to the insertion point when the closing token is the
+        // ONLY expected one (the precise SLL prediction yields such tight expected sets).
+        Position ip = insertionPointFor(ime, true);
+        if (ip == null) {
             return Location.fromToken(offending);
         }
+        return new Location(MiscTools.getURIFromTokenSource(offending.getTokenSource()), ip);
+    }
+
+    /**
+     * The insertion-point position for a missing closing/terminating token: one past the preceding
+     * token, i.e. the spot where the missing {@code ';'}/{@code ')'}/... belongs (rather than the
+     * next, unexpected token). Returns {@code null} when the heuristic does not apply.
+     *
+     * @param ime the input mismatch
+     * @param onlyClosing if {@code true}, fire only when a closing token is the <em>only</em>
+     *        expected token (precise single-error path); if {@code false}, fire when a closing
+     *        token
+     *        is <em>among</em> the expected ones (multi-error recovery, where LL prediction yields
+     *        a
+     *        broader expected set so the strict check would never match)
+     * @return the 1-based insertion-point position, or {@code null}
+     */
+    public static @Nullable Position insertionPointFor(InputMismatchException ime,
+            boolean onlyClosing) {
+        Token offending = ime.getOffendingToken();
+        boolean applies =
+            onlyClosing ? expectsOnlyClosingToken(ime) : expectedContainsClosingToken(ime);
+        if (!applies || offending == null
+                || !(ime.getInputStream() instanceof TokenStream ts)) {
+            return null;
+        }
         // Search backwards for the previous token on the default channel (skip
         // whitespace/comments).
         for (int i = offending.getTokenIndex() - 1; i >= 0; i--) {
             Token prev = ts.get(i);
-            if (prev.getChannel() == Token.DEFAULT_CHANNEL
-                    && prev.getType() != Token.EOF) {
-                URI uri = MiscTools.getURIFromTokenSource(prev.getTokenSource());
+            if (prev.getChannel() == Token.DEFAULT_CHANNEL && prev.getType() != Token.EOF) {
                 String text = prev.getText();
                 int len = text == null ? 1 : Math.max(1, text.length());
                 // 1-based column of the insertion point: one past the last character of the
                 // preceding token (where the missing closing token belongs)
-                int col = prev.getCharPositionInLine() + len + 1;
-                return new Location(uri,
-                    Position.newOneBased(prev.getLine(), col));
+                return Position.newOneBased(prev.getLine(), prev.getCharPositionInLine() + len + 1);
             }
         }
-        return Location.fromToken(offending);
+        return null;
     }
 
     /**
@@ -349,6 +401,24 @@ private static boolean expectsOnlyClosingToken(InputMismatchException ime) {
         return CLOSING_TOKENS.contains(vocabulary.getDisplayName(expected.getMinElement()));
     }
 
+    /**
+     * @return true iff a closing/terminating token (see {@link #CLOSING_TOKENS}) is among the
+     *         expected tokens at the error position.
+     */
+    private static boolean expectedContainsClosingToken(InputMismatchException ime) {
+        IntervalSet expected = ime.getExpectedTokens();
+        if (expected == null || expected.isNil()) {
+            return false;
+        }
+        Vocabulary vocabulary = ime.getRecognizer().getVocabulary();
+        for (int type : expected.toList()) {
+            if (CLOSING_TOKENS.contains(vocabulary.getDisplayName(type))) {
+                return true;
+            }
+        }
+        return false;
+    }
+
     private static URI parseFileName(String filename) throws MalformedURLException {
         try {
             return filename == null ? null : MiscTools.parseURL(filename).toURI();