From e5ab2ad51558f83e7c3272fa042acc1ea6e4e451 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 23 Jun 2026 08:38:39 +0200 Subject: [PATCH 01/10] Error reporting: clearer loading & proof-replay errors Improve the messages produced by the proof loading/replay framework so they state the actual problem instead of leaking internal objects or surfacing only the first of several failures. - PosInOccurrence: add a human-readable toString ("term at of formula in the antecedent/succedent"). Previously the default Object form (PosInOccurrence@) leaked into replay error dialogs. - IntermediateProofReplayer: actionable text for the two "Wrong position information" cases; include the node serial in the otherwise context-free catch-all; drop a whole-namespace dump from a parse-value error; downgrade the tolerated "not in uninsts" inconsistency to a clear warn (with a comment on why it is tolerated); grammar fix. - ProblemLoaderException can now bundle several sub-problems, and ExceptionTools.getMessages expands them so every failed rule application is reported (summary + one entry each) instead of only the first; WindowUserInterfaceControl throws the bundle on a partial replay. - IntermediatePresentationProofFileParser: wrap a ClassNotFoundException with the offending type name. - IssueDialog.showExceptionDialog: neutral "Error" title instead of the misleading "Parser Error" (the method has ~27 mostly non-parser callers). --- ...termediatePresentationProofFileParser.java | 3 +- .../proof/io/IntermediateProofReplayer.java | 31 +++++++++++----- .../key/proof/io/ProblemLoaderException.java | 37 +++++++++++++++++++ .../de/uka/ilkd/key/util/ExceptionTools.java | 20 ++++++++++ .../prover/sequent/PosInOccurrence.java | 6 +++ .../java/de/uka/ilkd/key/gui/IssueDialog.java | 2 +- .../key/gui/WindowUserInterfaceControl.java | 8 ++-- 7 files changed, 91 insertions(+), 16 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java index a5cec77b332..faf618fc918 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java +++ b/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) Class.forName(str); } catch (ClassNotFoundException e) { - errors.add(e); + errors.add(new IllegalArgumentException( + "Unknown predicate abstraction lattice type \"" + str + "\".", e)); } } case MERGE_ABSTRACTION_PREDICATES -> diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java index dc42cc8ec19..33e98d751a8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java +++ b/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 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 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 getSubExceptions() { + return subExceptions; + } + @Override public String toString() { StringBuffer sb = new StringBuffer(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java b/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java index ab53c3db217..80caf07d9a1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java @@ -115,6 +115,15 @@ public static String getMessage(Throwable throwable) { List 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 BuildingExceptions be) { for (BuildingIssue issue : be.getErrors()) { result.add(issue.asPositionedString()); @@ -153,6 +162,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()); diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/sequent/PosInOccurrence.java b/key.ncore.calculus/src/main/java/org/key_project/prover/sequent/PosInOccurrence.java index f9375d91eb0..44fadc9a2c0 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/sequent/PosInOccurrence.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/sequent/PosInOccurrence.java @@ -217,6 +217,12 @@ public int hashCode() { return h; } + @Override + public String toString() { + return "term at " + posInTerm() + " of formula \"" + sequentFormula() + "\" in the " + + (inAntec ? "antecedent" : "succedent"); + } + /// Replaces the formula associated with this occurrence and returns a new object pointing /// to the same position within the new formula. /// diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java index 6289bf2497c..02a0dd2411a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java @@ -564,7 +564,7 @@ public static void showExceptionDialog(Window parent, Throwable exception) { ((BuildingExceptions) exception).getErrors().forEach( it -> LOGGER.info("Error", it)); } - IssueDialog dlg = new IssueDialog(parent, "Parser Error", msg, true, exception); + IssueDialog dlg = new IssueDialog(parent, "Error", msg, true, exception); dlg.setVisible(true); dlg.dispose(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index 609bdf7b755..c6e2af46895 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -543,11 +543,9 @@ public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poCo } if (result.hasErrors()) { throw new ProblemLoaderException(loader, - "Proof could only be loaded partially.\n" + "In summary " - + result.getErrorList().size() - + " not loadable rule application(s) have been detected.\n" - + "The first one:\n" + result.getErrorList().getFirst().getMessage(), - result.getErrorList().getFirst()); + "The proof could only be loaded partially: " + result.getErrorList().size() + + " rule application(s) could not be replayed (see the list below).", + result.getErrorList()); } } } From 02223c8a7d4a26649d1f46fe9ecd9bf72ad03d28 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 23 Jun 2026 08:38:39 +0200 Subject: [PATCH 02/10] Error reporting: tests for PosInOccurrence.toString and bundled replay errors - TestPosInOcc#testToStringIsReadable guards against the default Object representation (PosInOccurrence@) leaking into user-facing messages. - ExceptionToolsTest#getMessagesExpandsBundledProblemLoaderException: every bundled sub-problem (e.g. all failed rule applications) is reported, not just the first. --- .../de/uka/ilkd/key/logic/TestPosInOcc.java | 28 +++++++++++++++++++ .../uka/ilkd/key/util/ExceptionToolsTest.java | 24 ++++++++++++++++ 2 files changed, 52 insertions(+) diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestPosInOcc.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestPosInOcc.java index 4209065f56a..7fad7403f5c 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestPosInOcc.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestPosInOcc.java @@ -110,4 +110,32 @@ public void testReplaceConstrainedFormula() { pio = pio.replaceSequentFormula(cfma2); assertSame(pio.subTerm(), terms2[2]); } + + /** + * A {@link PosInOccurrence} must render itself in a human-readable way, naming the position and + * the formula it points at. Regression guard against the default {@code Object} representation + * ({@code PosInOccurrence@}) leaking into user-facing messages (e.g. proof-replay + * errors). + */ + @Test + public void testToStringIsReadable() { + Sort sort1 = new SortImpl(new Name("S1")); + LogicVariable x = new LogicVariable(new Name("x"), sort1); + Function f = new JFunction(new Name("f"), sort1, sort1); + Function p = new JFunction(new Name("p"), JavaDLTheory.FORMULA, sort1); + + JTerm fml = TB.func(p, new JTerm[] { TB.func(f, new JTerm[] { TB.var(x) }) }); + + String antec = + new PosInOccurrence(new SequentFormula(fml), PosInTerm.getTopLevel(), true).toString(); + assertFalse(antec.contains("PosInOccurrence@"), + "toString must not fall back to the default Object representation, but was: " + antec); + assertTrue(antec.contains(fml.toString()), + "toString should mention the formula, but was: " + antec); + assertTrue(antec.contains("antecedent"), antec); + + String succ = + new PosInOccurrence(new SequentFormula(fml), PosInTerm.getTopLevel(), false).toString(); + assertTrue(succ.contains("succedent"), succ); + } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/ExceptionToolsTest.java b/key.core/src/test/java/de/uka/ilkd/key/util/ExceptionToolsTest.java index 4d77cafb9c9..16ab0f35ac9 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/ExceptionToolsTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/util/ExceptionToolsTest.java @@ -8,6 +8,7 @@ import java.util.Objects; import de.uka.ilkd.key.java.Position; +import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.speclang.PositionedString; import de.uka.ilkd.key.util.parsing.BuildingExceptions; import de.uka.ilkd.key.util.parsing.BuildingIssue; @@ -86,4 +87,27 @@ void getMessagesFallsBackToSingleMessage() { assertEquals(1, messages.size()); assertEquals("boom", messages.get(0).getText()); } + + @Test + void getMessagesExpandsBundledProblemLoaderException() { + // e.g. a partial proof replay where several rule applications could not be replayed: every + // failure must be reported, not just the first. + var sub1 = new ProblemLoaderException(null, + "Error loading proof.\nLine 3, goal 5, rule andLeft not applicable"); + var sub2 = new ProblemLoaderException(null, + "Error loading proof.\nLine 7, goal 9, rule impRight not applicable"); + var bundle = new ProblemLoaderException(null, + "The proof could only be loaded partially: 2 rule application(s) could not be replayed.", + List.of(sub1, sub2)); + + List messages = ExceptionTools.getMessages(bundle); + // the summary plus one entry per failed rule application + assertEquals(3, messages.size(), "expected summary + 2 failures, got: " + messages); + assertTrue(messages.stream().anyMatch(m -> m.getText().contains("partially")), + "summary should be present: " + messages); + assertTrue(messages.stream().anyMatch(m -> m.getText().contains("andLeft")), + "first failure should be present: " + messages); + assertTrue(messages.stream().anyMatch(m -> m.getText().contains("impRight")), + "second failure should be present (not dropped): " + messages); + } } From f60c45030262233de0902bb714dce85ffeb0078d Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 23 Jun 2026 08:55:49 +0200 Subject: [PATCH 03/10] Error reporting: tidy JavaParser messages and humanize symbol-solver jargon - JavaService.simplifyJavaParserMessage: collapse the (possibly multi-line) offending token to a single line and shorten it if very long; drop JavaCard / schema-internal alternatives ("#abortJavaCardTransaction", ...) from the "expected one of" list so the relevant alternatives are shown. - New JavaService.humanizeJavaParserJargon: rewrite "Unsolved symbol : X" into the user-facing wording KeY already uses ("Cannot resolve 'X'. No variable, field, or type with this name is in scope here (check for typos)."). Applied in simplifyJavaParserMessage and to the reason of a failed Java block in ExpressionBuilder, where the type-resolution path previously leaked the raw jargon. --- .../de/uka/ilkd/key/java/JavaService.java | 60 +++++++++++++++++-- .../nparser/builder/ExpressionBuilder.java | 1 + 2 files changed, 56 insertions(+), 5 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java index a1af19e047f..a197a0b95b9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java +++ b/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,61 @@ 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 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) { + Matcher m = Pattern.compile("unexpected \"(.*?)\"", 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 diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java index 7c0cf2543a8..24e507a879a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java +++ b/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); From e41ec7baa93b72d67307e8182fc447198e391264 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 23 Jun 2026 08:55:49 +0200 Subject: [PATCH 04/10] Error reporting: tests for JavaParser message tidy-up and jargon humanizing - JavaServiceMessageTest: dropping JavaCard/schema alternatives, collapsing a multi-line offending token, and humanizing "Unsolved symbol". - TestJavaDLASTExtensions: assert the user-facing "Cannot resolve" wording for an unresolved type in a Java block (cause chain unchanged). --- .../ilkd/key/java/JavaServiceMessageTest.java | 35 +++++++++++++++++++ .../key/java/TestJavaDLASTExtensions.java | 4 +-- .../exceptional/javaBlockUnknownType.key | 6 ++-- 3 files changed, 41 insertions(+), 4 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/java/JavaServiceMessageTest.java b/key.core/src/test/java/de/uka/ilkd/key/java/JavaServiceMessageTest.java index 72c441b4b83..4706b499c50 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/java/JavaServiceMessageTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/java/JavaServiceMessageTest.java @@ -47,4 +47,39 @@ void leavesSemanticMessagesUnchanged() { String in = "Cannot resolve type Foo"; assertEquals(in, JavaService.simplifyJavaParserMessage(in)); } + + @Test + void dropsJavaCardSchemaAlternatives() { + String in = "Parse error. Found \";\", expected one of " + + "\"#abortJavaCardTransaction\" \"#beginJavaCardTransaction\" \"!\" \"(\""; + String out = JavaService.simplifyJavaParserMessage(in); + assertFalse(out.contains("#abortJavaCardTransaction"), + "JavaCard/schema tokens should be dropped: " + out); + assertTrue(out.contains("\"!\"") && out.contains("\"(\""), + "relevant alternatives should remain: " + out); + } + + @Test + void collapsesMultiLineOffendingToken() { + // the offending token is an (escaped) multi-line comment + String in = "Parse error. Found \"/*@ loop_invariant 0 <= i\\n @ && x\\n @*/\", " + + "expected one of \"!\" \"(\""; + String out = JavaService.simplifyJavaParserMessage(in); + assertFalse(out.contains("\\n"), "escaped newlines should be collapsed: " + out); + assertFalse(out.contains("\n"), "real newlines should be collapsed: " + out); + assertTrue(out.startsWith("Java syntax error: unexpected"), out); + } + + @Test + void humanizesUnsolvedSymbolJargon() { + String out = JavaService.humanizeJavaParserJargon("Unsolved symbol : Foobar"); + assertFalse(out.contains("Unsolved symbol"), "jargon should be removed: " + out); + assertTrue(out.contains("Cannot resolve 'Foobar'"), out); + assertTrue(out.contains("check for typos"), out); + } + + @Test + void humanizeLeavesOtherTextUnchanged() { + assertEquals("all good", JavaService.humanizeJavaParserJargon("all good")); + } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/java/TestJavaDLASTExtensions.java b/key.core/src/test/java/de/uka/ilkd/key/java/TestJavaDLASTExtensions.java index 50f050ba305..e2d581edff6 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/java/TestJavaDLASTExtensions.java +++ b/key.core/src/test/java/de/uka/ilkd/key/java/TestJavaDLASTExtensions.java @@ -42,8 +42,8 @@ public void testTypeNotInScopeShouldNotBeFound() { * its (now no longer hidden) message mentions the unresolvable type. */ private static void assertUnsolvedType(BuildingException ex) { - Assertions.assertTrue(ExceptionTools.getMessage(ex).contains("Unsolved symbol"), - "the message should expose the unresolved symbol, but was: " + Assertions.assertTrue(ExceptionTools.getMessage(ex).contains("Cannot resolve"), + "the message should expose the unresolved symbol in user-facing wording, but was: " + ExceptionTools.getMessage(ex)); boolean hasUnsolvedCause = false; for (Throwable c = ex; c != null; c = c.getCause()) { diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/javaBlockUnknownType.key b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/javaBlockUnknownType.key index 77d4e2ee20a..6f4bd656e98 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/javaBlockUnknownType.key +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/javaBlockUnknownType.key @@ -1,6 +1,6 @@ // verbose: true // exceptionClass: BuildingException -// msgContains: Unsolved symbol : Foobar +// msgContains: Cannot resolve 'Foobar' // position: 7/8 \problem { @@ -10,4 +10,6 @@ // The Java block refers to an unknown type. Previously the resulting // UnsolvedSymbolException escaped without any location pointing into the // .key file (ExceptionTools.getLocation returned null). Now the error is -// wrapped with the modality's location and a descriptive message. +// wrapped with the modality's location and the JavaParser jargon +// ("Unsolved symbol : Foobar") is humanized to the same "Cannot resolve ..." +// wording KeY uses elsewhere. From b9c25f083e549a79c05338eeb301692c3c71b1d8 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 23 Jun 2026 09:11:21 +0200 Subject: [PATCH 05/10] Error reporting: report all syntax errors in a .key file, not just the first ParsingFacade.parseFile keeps the fast SLL+bail pass for the common case; when it fails it now re-parses with LL and ANTLR's default error recovery, which collects all syntax errors. To avoid regressing the polished single-error message and position, the bail-path exception is kept when recovery finds exactly one error; the full list is reported only when there are several (zero errors means SLL was merely insufficient and the LL parse actually succeeded). - SyntaxErrorReporter: expose errorCount(), ParserException.getErrors(), and per-error SyntaxError.getMessage()/getLocation(). - ExceptionTools.getMessages: expand a multi-error ParserException into one located message per error, so the dialog lists them separately and the console prints each (via the unified extraction, both get this for free). --- .../uka/ilkd/key/nparser/ParsingFacade.java | 11 +++++-- .../de/uka/ilkd/key/util/ExceptionTools.java | 8 +++++ .../key/util/parsing/SyntaxErrorReporter.java | 29 +++++++++++++++++++ 3 files changed, 45 insertions(+), 3 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java index b86472b9215..8c1ae4e2e36 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java +++ b/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; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java b/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java index 80caf07d9a1..b959efd1b24 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java +++ b/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; @@ -124,6 +125,13 @@ public static String getMessage(Throwable throwable) { } 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()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java index afdb0da069f..2d5a8efde8f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java @@ -92,6 +92,13 @@ public boolean hasErrors() { return !errors.isEmpty(); } + /** + * @return the number of syntax errors discovered by this listener + */ + public int errorCount() { + return errors.size(); + } + /** * Throws an exception if an error has occured. * @@ -177,6 +184,21 @@ public String showInInput(String[] lines) { public String positionAsUrl() { return String.format("file://source:%d", line); } + + /** + * @return the (already humanized, for an InputMismatch) error message of this single error + */ + public String getMessage() { + return msg; + } + + /** + * @return the source location of this error (1-based line and column) + */ + public Location getLocation() { + // charPositionInLine is 0-based + return new Location(source, Position.fromOneZeroBased(line, charPositionInLine)); + } } public static class ParserException extends RuntimeException implements HasLocation { @@ -216,5 +238,12 @@ public String getMessage() { public @NonNull Location getLocation() { return location; } + + /** + * @return the individual syntax errors, in the order they were encountered + */ + public List getErrors() { + return Collections.unmodifiableList(errors); + } } } From fcd9c2c83e801047c2f85429aac473e853ae8660 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 23 Jun 2026 09:11:21 +0200 Subject: [PATCH 06/10] Error reporting: test multi syntax-error reporting for .key files MultiSyntaxErrorTest: two independent errors are both reported (each with its own line); a single error keeps the one-message bail path (regression guard). --- .../key/nparser/MultiSyntaxErrorTest.java | 51 +++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/nparser/MultiSyntaxErrorTest.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/nparser/MultiSyntaxErrorTest.java b/key.core/src/test/java/de/uka/ilkd/key/nparser/MultiSyntaxErrorTest.java new file mode 100644 index 00000000000..92cfa6a631c --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/nparser/MultiSyntaxErrorTest.java @@ -0,0 +1,51 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.nparser; + +import java.util.List; + +import de.uka.ilkd.key.speclang.PositionedString; +import de.uka.ilkd.key.util.ExceptionTools; + +import org.antlr.v4.runtime.CharStreams; +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * When a {@code .key} file contains several independent syntax errors, all of them should be + * reported (not just the first). A single error keeps the polished bail-path message (covered by + * {@link KeYParserExceptionTest}); this test covers the multi-error path of + * {@link ParsingFacade#parseFile}. + * + * @author Claude (improveErrorMessages) + */ +public class MultiSyntaxErrorTest { + + @Test + public void reportsEveryIndependentSyntaxError() { + // two function declarations each missing their terminating ';' + String src = "\\functions {\n int f\n int g;\n int h\n}\n\\problem { true }\n"; + var ex = assertThrows(RuntimeException.class, + () -> ParsingFacade.parseFile(CharStreams.fromString(src))); + + List msgs = ExceptionTools.getMessages(ex); + assertTrue(msgs.size() >= 2, + "both missing semicolons should be reported, but got: " + msgs); + // each error carries its own location (different lines) + assertTrue( + msgs.stream().map(m -> m.getLocation().getPosition().line()).distinct().count() >= 2, + "the reported errors should point at different lines: " + msgs); + } + + @Test + public void singleSyntaxErrorStaysAtOneMessage() { + // regression guard: one error keeps the single-error (bail) path -> exactly one message + String src = "\\problem {\n (true & true\n}\n"; + var ex = assertThrows(RuntimeException.class, + () -> ParsingFacade.parseFile(CharStreams.fromString(src))); + List msgs = ExceptionTools.getMessages(ex); + assertEquals(1, msgs.size(), "a single error should produce a single message: " + msgs); + } +} From fbe7c270c6fe2c5127275b38a0d17a4e91b3752c Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 23 Jun 2026 09:23:37 +0200 Subject: [PATCH 07/10] Error reporting: make the issue location clickable and per-issue - IssueDialog: the location field ("URL: ...") is now a clickable link (hand cursor, link colour) that opens the source file at the selected issue; the "Edit File" action is rebound to the selected issue in updatePreview so it jumps to that issue's location rather than always the first one reported (relevant now that several issues can be listed). - EditSourceFileAction: add a constructor taking an explicit (Location, message) so the editor can open at a specific issue; the existing Throwable constructor is unchanged. The "no positional information" guard now also covers a location without a file URI. --- .../java/de/uka/ilkd/key/gui/IssueDialog.java | 22 ++++-- .../key/gui/actions/EditSourceFileAction.java | 71 ++++++++++++++----- 2 files changed, 70 insertions(+), 23 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java index 02a0dd2411a..49ad673231d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java @@ -329,9 +329,8 @@ private JScrollPane createWarningsPane(Font font) { listWarnings.addListSelectionListener(e -> updatePreview(listWarnings.getSelectedValue())); listWarnings .addListSelectionListener(e -> updateStackTrace(listWarnings.getSelectedValue())); - // enable/disable "open file" and "show details" - listWarnings.addListSelectionListener( - e -> btnEditFile.setEnabled(listWarnings.getSelectedValue().hasFilename())); + // "Edit File" is (re)bound to the selected issue in updatePreview (so it opens at that + // issue's location); here we only manage "show details" listWarnings.addListSelectionListener(e -> { if (listWarnings.getSelectedValue().getAdditionalInfo().isEmpty()) { chkDetails.setSelected(false); @@ -537,6 +536,18 @@ private JPanel createSourcePanel(Font font) { fTextField.setEditable(false); lTextField.setEditable(false); cTextField.setEditable(false); + // make the location a clickable link that opens the source at the selected issue + fTextField.setForeground(new Color(0x0b, 0x57, 0xd0)); + fTextField.setCursor(Cursor.getPredefinedCursor(Cursor.HAND_CURSOR)); + fTextField.setToolTipText("Click to open the source file at this location"); + fTextField.addMouseListener(new MouseAdapter() { + @Override + public void mouseClicked(MouseEvent e) { + if (btnEditFile.isEnabled()) { + btnEditFile.doClick(); + } + } + }); locPanel.add(fTextField); locPanel.add(lTextField); locPanel.add(cTextField); @@ -645,7 +656,10 @@ private void updatePreview(PositionedIssueString issue) { cTextField.setText("Column: " + pos.column()); lTextField.setText("Line: " + pos.line()); - btnEditFile.setEnabled(pos != Position.UNDEFINED); + // Bind "Edit File" (and the clickable location field) to THIS issue, so jumping to the + // source opens at the selected issue rather than the first one reported. The action enables + // itself only when the issue carries a usable file location. + btnEditFile.setAction(new EditSourceFileAction(this, location, issue.getText())); if (location.getFileURI().isEmpty()) { fTextField.setVisible(false); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java index a4b2eb83422..4fad38d8124 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java @@ -66,9 +66,13 @@ public class EditSourceFileAction extends KeyAction { */ private final Window parent; /** - * The exception. + * The exception (when constructed from one); {@code null} when an explicit location was given. */ private final Throwable exception; + /** explicit location to open at; overrides the one derived from {@link #exception} */ + private final Location overrideLocation; + /** message to show next to the source when {@link #overrideLocation} is used */ + private final String overrideMessage; /** * Instantiates a new edits the source file action. @@ -81,9 +85,31 @@ public EditSourceFileAction(final Window parent, final Throwable exception) { setIcon(IconFactory.editFile(16)); this.parent = parent; this.exception = exception; + this.overrideLocation = null; + this.overrideMessage = null; setEnabled(exception != null); } + /** + * Opens the editor directly at the given location. Used to jump to a specific issue + * when several are reported, so the editor opens at the selected issue rather than the first. + * + * @param parent the parent window + * @param location the location to open and place the caret at + * @param message the message to show next to the source + */ + public EditSourceFileAction(final Window parent, final Location location, + final String message) { + setName("Edit File"); + setIcon(IconFactory.editFile(16)); + this.parent = parent; + this.exception = null; + this.overrideLocation = location; + this.overrideMessage = message == null ? "" : message; + setEnabled(location != null && location.getFileUri() != null + && !location.getPosition().isNegative()); + } + /** * Moves the caret in a {@link JTextArea} to the specified position. Assumes the first position * in the textarea is in line 1 column 1. @@ -106,16 +132,15 @@ private static void textAreaGoto(JTextComponent textArea, Position position) { textArea.setCaretPosition(i); } - private static JScrollPane createParserMessageScrollPane(final Throwable exception, + private static JScrollPane createParserMessageScrollPane(final String message, final int columnNumber) { JTextArea parserMessage = new JTextArea(); - String message = exception.getMessage(); - message = message == null ? "" : message; - parserMessage.setText(message); + String msg = message == null ? "" : message; + parserMessage.setText(msg); parserMessage.setEditable(false); parserMessage.setColumns(columnNumber); // approximate # rows - parserMessage.setRows(message.length() / (columnNumber - 10)); + parserMessage.setRows(Math.max(1, msg.length() / (columnNumber - 10))); parserMessage.setLineWrap(true); parserMessage.setWrapStyleWord(true); parserMessage.setBorder(new TitledBorder("Parser Message")); @@ -235,19 +260,27 @@ private JPanel createButtonPanel(final URI sourceURI, final JTextPane textPane, @Override public void actionPerformed(ActionEvent arg0) { - if (exception == null) { - JOptionPane.showMessageDialog( - SwingUtilities.windowForComponent((Component) arg0.getSource()), - "The given exception does not carry any positional information.", - "Position not available", JOptionPane.ERROR_MESSAGE); - return; - } - try { - final Location location = ExceptionTools.getLocation(exception); - if (location == null) - throw new IOException("Cannot recover file location from exception."); - final URI uri = location.fileUri(); + final Location location; + final String message; + if (overrideLocation != null) { + location = overrideLocation; + message = overrideMessage; + } else if (exception != null) { + location = ExceptionTools.getLocation(exception); + message = exception.getMessage() == null ? "" : exception.getMessage(); + } else { + location = null; + message = ""; + } + if (location == null || location.getFileUri() == null) { + JOptionPane.showMessageDialog( + SwingUtilities.windowForComponent((Component) arg0.getSource()), + "The given problem does not carry any positional information.", + "Position not available", JOptionPane.ERROR_MESSAGE); + return; + } + final URI uri = location.getFileUri(); // indicate edit/readonly in dialog title String prefix; @@ -263,7 +296,7 @@ public void actionPerformed(ActionEvent arg0) { final int columnNumber = 75; final JScrollPane parserMessageScrollPane = - createParserMessageScrollPane(exception, columnNumber); + createParserMessageScrollPane(message, columnNumber); final JTextPane txtSource = createSrcTextPane(location); From f016c2c01d4c29d008fc0ff6654d72558ea5afaa Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 23 Jun 2026 09:47:33 +0200 Subject: [PATCH 08/10] Error reporting: collapse the multi-line JavaParser token in real messages cleanFoundToken matched "unexpected \"" with a single space, but JavaParser emits "Found \"...\"" (two spaces) - so the offending multi-line token in real messages (e.g. the top-level entry for a broken \javaSource file) was not collapsed; only the hand-built single-space test input was. Match one-or-more spaces, and use the realistic two-space form in the test. --- key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java | 4 +++- .../java/de/uka/ilkd/key/java/JavaServiceMessageTest.java | 5 +++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java index a197a0b95b9..03deadf3737 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/JavaService.java @@ -263,7 +263,9 @@ public static String humanizeJavaParserJargon(@Nullable String message) { * @return the message with its offending token collapsed to a single line */ private static String cleanFoundToken(String message) { - Matcher m = Pattern.compile("unexpected \"(.*?)\"", Pattern.DOTALL).matcher(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; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/java/JavaServiceMessageTest.java b/key.core/src/test/java/de/uka/ilkd/key/java/JavaServiceMessageTest.java index 4706b499c50..de1d3aa97ca 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/java/JavaServiceMessageTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/java/JavaServiceMessageTest.java @@ -61,8 +61,9 @@ void dropsJavaCardSchemaAlternatives() { @Test void collapsesMultiLineOffendingToken() { - // the offending token is an (escaped) multi-line comment - String in = "Parse error. Found \"/*@ loop_invariant 0 <= i\\n @ && x\\n @*/\", " + // the offending token is an (escaped) multi-line comment; JavaParser writes "Found \"...\"" + // with two spaces, so the message reads "unexpected \"...\"" - the cleanup must still match + String in = "Parse error. Found \"/*@ loop_invariant 0 <= i\\n @ && x\\n @*/\", " + "expected one of \"!\" \"(\""; String out = JavaService.simplifyJavaParserMessage(in); assertFalse(out.contains("\\n"), "escaped newlines should be collapsed: " + out); From d1522cde64263aa64e26dcd87998145a9edf814f Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 23 Jun 2026 10:25:23 +0200 Subject: [PATCH 09/10] Error reporting: scroll the issue preview to the selected issue on first open updatePreview's scroll-to-error ran via invokeLater during construction, before the source preview was laid out, so modelToView2D returned null and the scroll was skipped on the initial show - the selected issue's line became visible only after clicking another issue and back. Remember the offset and re-run the scroll from componentShown (when the pane is finally laid out). --- .../java/de/uka/ilkd/key/gui/IssueDialog.java | 45 +++++++++++++------ 1 file changed, 32 insertions(+), 13 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java index 49ad673231d..bbb7327bf8c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java @@ -104,6 +104,9 @@ public final class IssueDialog extends JDialog { private final JTextPane txtSource = new JTextPane(); private final JTextArea txtStacktrace = new JTextArea(); + /** offset (in the source preview) of the currently selected issue, used for scroll-to-error */ + private int currentErrorOffset = 0; + private final JList listWarnings; private final JButton btnEditFile = new JButton(); @@ -310,6 +313,15 @@ private static List decorateHTML(Set { - try { - var rect = txtSource.modelToView2D(errorOffset); - if (rect != null) { - txtSource.scrollRectToVisible(rect.getBounds()); - } - } catch (BadLocationException ignore) { - // best effort: leave the view where it is - } - }); + // out; scroll to the error explicitly. On the initial show this still runs before + // layout (modelToView2D == null), so the scroll is also re-run from componentShown. + SwingUtilities.invokeLater(this::scrollToError); } catch (Exception e) { LOGGER.warn("Failed to update preview", e); } @@ -724,6 +727,22 @@ private void updatePreview(PositionedIssueString issue) { validate(); } + /** + * Scrolls the source preview so the currently selected issue ({@link #currentErrorOffset}) is + * visible. A no-op while the text pane is not yet laid out ({@code modelToView2D == null}), + * which is why it is invoked both from {@link #updatePreview} and on {@code componentShown}. + */ + private void scrollToError() { + try { + var rect = txtSource.modelToView2D(currentErrorOffset); + if (rect != null) { + txtSource.scrollRectToVisible(rect.getBounds()); + } + } catch (BadLocationException ignore) { + // best effort: leave the view where it is + } + } + private void updateStackTrace(PositionedIssueString issue) { txtStacktrace.setText(issue.getAdditionalInfo()); } From e553154d4ba76118e745e0011a4146ad03e66c75 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 23 Jun 2026 10:45:02 +0200 Subject: [PATCH 10/10] Error reporting: point multi-error syntax errors at the missing-token insertion point In the multi-error path the recovered syntax errors were located at the next, unexpected token instead of the insertion point of the missing ';'/')'/... (the single-error/bail path already does this). LL recovery yields a broader expected set than SLL, so the strict "only a closing token is expected" check never fired. - ExceptionTools: extract insertionPointFor(ime, onlyClosing); the single-error path keeps the strict (only-closing) check (unchanged positions), while the multi-error path accepts a closing token being among the expected ones. - SyntaxErrorReporter: for an InputMismatch, redirect the reported position to that insertion point. - MultiSyntaxErrorTest now asserts the two errors mark lines 2 and 4 (the missing ';'), not 3 and 5. --- .../de/uka/ilkd/key/util/ExceptionTools.java | 60 ++++++++++++++++--- .../key/util/parsing/SyntaxErrorReporter.java | 11 +++- .../key/nparser/MultiSyntaxErrorTest.java | 10 ++-- 3 files changed, 67 insertions(+), 14 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java b/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java index b959efd1b24..5cf07e6527c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java @@ -341,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 only + * expected token (precise single-error path); if {@code false}, fire when a closing + * token + * is among 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; } /** @@ -377,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(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java index 2d5a8efde8f..0d3bbcce27d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java @@ -67,9 +67,18 @@ public void syntaxError(Recognizer recognizer, @Nullable Object offendingS } // Replace ANTLR's terse default messages (e.g. "mismatched input ';' expecting ...") with a // concise, human-readable description that names the expected token(s) and what was found. - if (e instanceof InputMismatchException) { + if (e instanceof InputMismatchException ime) { msg = ExceptionTools.describeSyntaxError(parser.getVocabulary(), tok, e.getExpectedTokens()); + // For a missing closing/terminating token, point at the insertion point just after the + // preceding token (where the missing token belongs) rather than the next, unexpected + // token - matching the single-error path. The recovery parser's LL prediction yields a + // broad expected set, so accept a closing token being among the expected ones. + Position ip = ExceptionTools.insertionPointFor(ime, false); + if (ip != null) { + line = ip.line(); + charPositionInLine = ip.column() - 1; // SyntaxError stores a 0-based column + } } SyntaxError se = new SyntaxError(recognizer, line, tok, charPositionInLine, msg, MiscTools.getURIFromTokenSource(tok.getTokenSource()), stack); diff --git a/key.core/src/test/java/de/uka/ilkd/key/nparser/MultiSyntaxErrorTest.java b/key.core/src/test/java/de/uka/ilkd/key/nparser/MultiSyntaxErrorTest.java index 92cfa6a631c..c9da48ba1b9 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/nparser/MultiSyntaxErrorTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/nparser/MultiSyntaxErrorTest.java @@ -33,10 +33,12 @@ public void reportsEveryIndependentSyntaxError() { List msgs = ExceptionTools.getMessages(ex); assertTrue(msgs.size() >= 2, "both missing semicolons should be reported, but got: " + msgs); - // each error carries its own location (different lines) - assertTrue( - msgs.stream().map(m -> m.getLocation().getPosition().line()).distinct().count() >= 2, - "the reported errors should point at different lines: " + msgs); + // Each error points at the insertion point of the missing ';' (the end of the declaration + // on lines 2 and 4), not at the next, unexpected token (lines 3 and 5). + var lines = msgs.stream().map(m -> m.getLocation().getPosition().line()) + .collect(java.util.stream.Collectors.toSet()); + assertTrue(lines.contains(2) && lines.contains(4), + "errors should mark the missing ';' on lines 2 and 4, but got lines: " + lines); } @Test