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..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 @@ -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 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 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/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); 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..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 @@ -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 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 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; } /** @@ -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(); 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..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); @@ -92,6 +101,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 +193,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 +247,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); + } } } 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..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 @@ -47,4 +47,40 @@ 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; 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); + 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/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/nparser/MultiSyntaxErrorTest.java b/key.core/src/test/java/de/uka/ilkd/key/nparser/MultiSyntaxErrorTest.java new file mode 100644 index 00000000000..c9da48ba1b9 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/nparser/MultiSyntaxErrorTest.java @@ -0,0 +1,53 @@ +/* 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 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 + 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); + } +} 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); + } } 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. 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..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 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 +548,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); @@ -564,7 +587,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(); } @@ -645,7 +668,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); @@ -688,21 +714,12 @@ private void updatePreview(PositionedIssueString issue) { // ensure that the currently selected problem is shown in view int offset = pos.isNegative() ? 0 : getOffsetFromLineColumn(txtSource.getDocument(), pos); + currentErrorOffset = offset; txtSource.setCaretPosition(offset); // setCaretPosition does not scroll the viewport while the dialog is not yet laid - // out; scroll to the error explicitly once the layout has settled, so the offending - // line is visible (and not left at the top of the file). - final int errorOffset = offset; - SwingUtilities.invokeLater(() -> { - 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); } @@ -710,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()); } 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()); } } } 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);