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 50356a94fd5..ab26c707cfa 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 @@ -130,7 +130,6 @@ public static KeyAst.File parseFile(CharStream stream) { KeYParser p = createParser(stream); p.getInterpreter().setPredictionMode(PredictionMode.SLL); - // we don't want error messages or recovery during first try p.removeErrorListeners(); p.setErrorHandler(new BailErrorStrategy()); KeYParser.FileContext ctx; @@ -138,7 +137,9 @@ public static KeyAst.File parseFile(CharStream stream) { ctx = p.file(); } catch (ParseCancellationException ex) { LOGGER.warn("SLL was not enough"); + stream.seek(0); p = createParser(stream); + p.setErrorHandler(new BailErrorStrategy()); ctx = p.file(); } 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 b32cbd03e75..6890c5118a9 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 @@ -3,7 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.util; +import java.io.File; import java.net.MalformedURLException; +import java.nio.file.Paths; import java.util.Optional; import java.util.regex.Matcher; import java.util.regex.Pattern; @@ -15,6 +17,11 @@ import de.uka.ilkd.key.parser.proofjava.TokenMgrError; import de.uka.ilkd.key.util.parsing.HasLocation; +import org.antlr.v4.runtime.InputMismatchException; +import org.antlr.v4.runtime.IntStream; +import org.antlr.v4.runtime.NoViableAltException; +import org.antlr.v4.runtime.Vocabulary; +import org.antlr.v4.runtime.misc.IntervalSet; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; @@ -38,6 +45,46 @@ public final class ExceptionTools { private ExceptionTools() { } + public static String getNiceMessage(InputMismatchException ime) { + return getNiceMessageInternal(ime.getInputStream(), ime.getOffendingToken(), + ime.getRecognizer().getVocabulary(), ime.getExpectedTokens()); + } + + public static String getNiceMessage(NoViableAltException ime) { + return getNiceMessageInternal(ime.getInputStream(), ime.getOffendingToken(), + ime.getRecognizer().getVocabulary(), ime.getExpectedTokens()); + } + + private static String getNiceMessageInternal(IntStream inputStream, + org.antlr.v4.runtime.Token offendingToken, Vocabulary vocabulary, + IntervalSet expectedTokens) { + StringBuilder sb = new StringBuilder(); + + sb.append("Syntax error in input file "); + var inFile = new File(inputStream.getSourceName()); + sb.append(inFile.getName()); + sb.append("\n"); + sb.append("Line: "); + sb.append(offendingToken.getLine()); + sb.append(" Character: "); + sb.append(offendingToken.getCharPositionInLine() + 1); + + sb.append("\n"); + sb.append("Found token which was not expected: "); + sb.append(vocabulary.getDisplayName(offendingToken.getType())); + sb.append("\n"); + sb.append("Expected token type(s): "); + for (var interval : expectedTokens.getIntervals()) { + for (int i = interval.a; i <= interval.b; i++) { + sb.append(vocabulary.getDisplayName(i)); + sb.append("\n"); + } + } + + return sb.toString(); + } + + /** * Tries to resolve the location (i.e., file name, line, and column) from a parsing exception. * Result may be null. @@ -56,6 +103,10 @@ public static Optional getLocation(@NonNull Throwable exc) return Optional.ofNullable(getLocation((ParseException) exc)); } else if (exc instanceof TokenMgrError) { return Optional.ofNullable(getLocation((TokenMgrError) exc)); + } else if (exc instanceof InputMismatchException ime) { + return Optional.ofNullable(getLocation(ime)); + } else if (exc instanceof NoViableAltException nvae) { + return Optional.ofNullable(getLocation(nvae)); } if (exc.getCause() != null) { @@ -73,6 +124,26 @@ private static Location getLocation(ParseException exc) { : new Location(null, Position.fromToken(token.next)); } + private static Location getLocation(NoViableAltException exc) { + var token = exc.getOffendingToken(); + + return token == null ? null + : new Location( + Paths.get(Paths.get("").toString(), exc.getInputStream().getSourceName()) + .normalize().toUri(), + Position.fromToken(token)); + } + + private static Location getLocation(InputMismatchException exc) { + var token = exc.getOffendingToken(); + + return token == null ? null + : new Location( + Paths.get(Paths.get("").toString(), exc.getInputStream().getSourceName()) + .normalize().toUri(), + Position.fromToken(token)); + } + private static Location getLocation(TokenMgrError exc) { Matcher m = TOKEN_MGR_ERR_PATTERN.matcher(exc.getMessage()); if (m.find()) { 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 new file mode 100644 index 00000000000..2e49f872f0f --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/util/ExceptionToolsTest.java @@ -0,0 +1,56 @@ +/* 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.util; + +import java.io.File; +import java.io.IOException; +import java.net.MalformedURLException; +import java.net.URISyntaxException; + +import de.uka.ilkd.key.nparser.ParsingFacade; +import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.util.parsing.SyntaxErrorReporter; + +import org.key_project.util.helper.FindResources; + +import org.antlr.v4.runtime.InputMismatchException; +import org.antlr.v4.runtime.misc.ParseCancellationException; +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +class ExceptionToolsTest { + public static final File testCaseDirectory = FindResources.getTestCasesDirectory(); + + @Test + void missingSemicolon() throws MalformedURLException, URISyntaxException { + var fileToRead = testCaseDirectory.toPath(); + fileToRead = fileToRead.resolve("parserErrorTest/missing_semicolon.key"); + try { + var result = ParsingFacade.parseFile(fileToRead); + fail("should fail to parse"); + } catch (IOException e) { + throw new RuntimeException(e); + } catch (ParseCancellationException exc) { + InputMismatchException ime = (InputMismatchException) exc.getCause(); + String message = """ + Syntax error in input file missing_semicolon.key + Line: 6 Character: 1 + Found token which was not expected: '}' + Expected token type(s): ';' + """; + String resultMessage = ExceptionTools.getNiceMessage(ime); + assertEquals(message, resultMessage); + + Location loc = ExceptionTools.getLocation(ime).get(); + assertEquals(6, loc.getPosition().line()); + assertEquals(1, loc.getPosition().column()); + assertEquals(fileToRead.toUri(), loc.fileUri()); + } catch (SyntaxErrorReporter.ParserException exception) { + Location loc = ExceptionTools.getLocation(exception).get(); + assertEquals(6, loc.getPosition().line()); + assertEquals(1, loc.getPosition().column()); + } + } +} diff --git a/key.core/src/test/resources/testcase/parserErrorTest/missing_semicolon.key b/key.core/src/test/resources/testcase/parserErrorTest/missing_semicolon.key new file mode 100644 index 00000000000..8fb326fb68f --- /dev/null +++ b/key.core/src/test/resources/testcase/parserErrorTest/missing_semicolon.key @@ -0,0 +1,10 @@ +\rules { + missingSemicolon { + \find(0=0) + \replacewith(1=1) + } +} +\problem { +0=0 +} + 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 2821d77057a..4b2143a514e 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 @@ -41,6 +41,9 @@ import org.key_project.util.java.StringUtil; import org.key_project.util.java.SwingUtil; +import org.antlr.v4.runtime.InputMismatchException; +import org.antlr.v4.runtime.NoViableAltException; +import org.antlr.v4.runtime.misc.ParseCancellationException; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -600,6 +603,17 @@ private static PositionedIssueString extractMessage(Throwable exception) { String message = exception.getMessage(); String info = sw.toString(); + if (exception instanceof ParseCancellationException) { + exception = exception.getCause(); + } + + if (exception instanceof InputMismatchException ime) { + message = ExceptionTools.getNiceMessage(ime); + } + if (exception instanceof NoViableAltException nvae) { + message = ExceptionTools.getNiceMessage(nvae); + } + // also add message of the cause to the string if available if (exception.getCause() != null) { String causeMessage = exception.getCause().getMessage();