diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java index c6878e3aa4f..a44be55c0b6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java @@ -92,13 +92,32 @@ private String concatenate(Comment[] comments) { StringBuilder sb = new StringBuilder(comments[0].getText()); for (int i = 1; i < comments.length; i++) { - Position relativePos = comments[i].getRelativePosition(); - for (int j = 0; j < relativePos.getLine(); j++) { - sb.append("\n"); - } - for (int j = 0; j < relativePos.getColumn(); j++) { - sb.append(" "); - } + Position previousStart = comments[i - 1].getStartPosition(); + + // this also includes // or /* ... */ + String previousText = comments[i - 1].getText(); + + int previousEndLine = previousStart.getLine() + + (int) previousText.chars().filter(x -> x == '\n').count(); + + // /*ab*/ => length: 6, lastIndex: -1, so we get 6 + // /*\nb*/ => length: 6, lastIndex: 2, so we get 3 + int previousEndColumn = previousStart.getColumn() - 1 + + previousText.length() - (previousText.lastIndexOf('\n') + 1); + + Position currentStart = comments[i].getStartPosition(); + + int insertRows = currentStart.getLine() - previousEndLine; + + // the columns are starting at 1 and not at 0 + int insertColumns = insertRows > 0 ? // line break between the comments + currentStart.getColumn() - 1 + : (currentStart.getColumn() - 1) - previousEndColumn; + + assert insertRows >= 0 && insertColumns >= 0; + + sb.append("\n".repeat(insertRows)); + sb.append(" ".repeat(insertColumns)); sb.append(comments[i].getText()); } 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 e130885505f..e995affe6a5 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,8 +137,13 @@ 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(); + if (p.getErrorReporter().hasErrors()) { + throw ex; + } } p.getErrorReporter().throwException(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java index 7afd8a868e0..01d1b37b512 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java @@ -81,6 +81,10 @@ public Object visitProg_var_decls(KeYParser.Prog_var_declsContext ctx) { KeYJavaType kjt = accept(ctx.keyjavatype(i)); assert varNames != null; for (String varName : varNames) { + if (varName.equals("null")) { + semanticError(ctx.simple_ident_comma_list(i), + "Function '" + varName + "' is already defined!"); + } ProgramElementName pvName = new ProgramElementName(varName); Named name = lookup(pvName); if (name != null) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java index e4bafa128c1..2225ca78ddb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java @@ -173,6 +173,8 @@ protected Operator lookupVarfuncId(ParserRuleContext ctx, String varfuncName, St SortDependingFunction firstInstance = SortDependingFunction.getFirstInstance(new Name(varfuncName), getServices()); + if (sort == null) + semanticError(ctx, "Could not find sort: %s", sortName); if (firstInstance != null) { SortDependingFunction v = firstInstance.getInstanceFor(sort, getServices()); if (v != null) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java index 7ea6299b0c0..7dc422f318f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java @@ -90,13 +90,40 @@ private String concatenate(Comment[] comments) { StringBuilder sb = new StringBuilder(comments[0].getText()); for (int i = 1; i < comments.length; i++) { - var relativePos = comments[i].getRelativePosition(); - for (int j = 0; j < relativePos.getLine(); j++) { - sb.append("\n"); - } - for (int j = 0; j < relativePos.getColumn(); j++) { - sb.append(" "); + Position previousStart = comments[i - 1].getStartPosition(); + + // this also includes // or /* ... */ + String previousText = comments[i - 1].getText(); + + int previousEndLine = previousStart.line() + + (int) previousText.chars().filter(x -> x == '\n').count(); + + // /*ab*/ => length: 6, lastIndex: -1, so we get 6 + // /*\nb*/ => length: 6, lastIndex: 2, so we get 3 + int previousEndColumn = previousStart.column() - 1 + + previousText.length() - (previousText.lastIndexOf('\n') + 1); + + Position currentStart = comments[i].getStartPosition(); + if (currentStart.isNegative()) { + // The comment is an artificial one; we cannot reproduce positions anyway, so just + // paste them. ... + while (i < comments.length) { + sb.append(comments[i].getText()); + i++; + } + break; } + + int insertRows = currentStart.line() - previousEndLine; + + // the columns are starting at 1 and not at 0 + int insertColumns = insertRows > 0 ? // line break between the comments + currentStart.column() - 1 : (currentStart.column() - 1) - previousEndColumn; + + assert insertRows >= 0 && insertColumns >= 0; + + sb.append("\n".repeat(insertRows)); + sb.append(" ".repeat(insertColumns)); sb.append(comments[i].getText()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java index e99d70e08d3..0c99ce64fc8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java @@ -3,10 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.speclang.njml; -import java.util.LinkedHashMap; -import java.util.List; -import java.util.Map; -import java.util.Optional; +import java.util.*; import java.util.stream.Collectors; import de.uka.ilkd.key.java.JavaInfo; @@ -233,14 +230,10 @@ private String createSignatureString(ImmutableList signature) { if (signature == null || signature.isEmpty()) { return ""; } - StringBuilder sigString = new StringBuilder(); - - for (SLExpression expr : signature) { - final KeYJavaType t = expr.getType(); - sigString.append(t == null ? "" : t.getFullName()).append(", "); - } - - return sigString.substring(0, sigString.length() - 2); + return String.join(", ", signature + .map(SLExpression::getType) + .filter(Objects::nonNull) + .map(KeYJavaType::getFullName)); } // region expression 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..6a53bbc1c0a 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; @@ -13,8 +15,15 @@ import de.uka.ilkd.key.parser.proofjava.ParseException; import de.uka.ilkd.key.parser.proofjava.Token; import de.uka.ilkd.key.parser.proofjava.TokenMgrError; +import de.uka.ilkd.key.proof.io.ProblemLoaderException; 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.antlr.v4.runtime.misc.ParseCancellationException; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; @@ -38,6 +47,68 @@ public final class ExceptionTools { private ExceptionTools() { } + /** + * Get the throwable's message. This will return a nicer error message for + * certain ANTLR exceptions. + * + * @param throwable a throwable + * @return message for the exception + */ + public static String getMessage(Throwable throwable) { + if (throwable == null) { + return ""; + } else if (throwable instanceof ParseCancellationException + || throwable instanceof ProblemLoaderException) { + return getMessage(throwable.getCause()); + } else if (throwable instanceof InputMismatchException ime) { + return getNiceMessage(ime); + } else if (throwable instanceof NoViableAltException nvae) { + return getNiceMessage(nvae); + } else { + return throwable.getMessage(); + } + } + + 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(" Column: "); + 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 +127,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 +148,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/nparser/KeYParserExceptionTest.java b/key.core/src/test/java/de/uka/ilkd/key/nparser/KeYParserExceptionTest.java new file mode 100644 index 00000000000..eca08f2e558 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/nparser/KeYParserExceptionTest.java @@ -0,0 +1,59 @@ +/* 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.io.IOException; +import java.net.URISyntaxException; +import java.net.URL; +import java.nio.file.Path; +import java.util.stream.Stream; + +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.util.ParserExceptionTest; + +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.Arguments; +import org.junit.jupiter.params.provider.MethodSource; + +/** + * This test case is used to ensure that errors in KeY files are reported + * with a reasonable error message and the right position pointing + * into the file. + * + * To add a test case, locate the "exceptional" directory in the resources + * (below the directory for this package here) and add a .key file + * that contains an error that should be presented to the user (like syntax + * error, unresolved names, ...) + * + * See README.md in said directory for information on the meta-data inside + * the files. + * + * @author Mattias Ulbrich + */ +public class KeYParserExceptionTest extends ParserExceptionTest { + + /* + * Usually a directory is scanned for files to operate on. + * If this here is not null, this file name (referring to the resources + * directory) will be loaded. + */ + private static final String FIX_FILE = null; // "conflict.java"; + + public static Stream getFiles() throws URISyntaxException, IOException { + URL fileURL = KeYParserExceptionTest.class.getResource("exceptional"); + return ParserExceptionTest.getFiles(FIX_FILE, fileURL, ".key"); + } + + + @ParameterizedTest(name = "case {1}") + @MethodSource("getFiles") + public void testParseAndInterpret(Path file, Path localFilename) throws Exception { + parseAndInterpret(file); + } + + @Override + protected void tryLoadFile(Path file) throws Exception { + KeYEnvironment.load(file.toFile()); + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/JMLParserExceptionTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/JMLParserExceptionTest.java index c8d469cb9b4..ba1b699835a 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/JMLParserExceptionTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/JMLParserExceptionTest.java @@ -6,32 +6,20 @@ import java.io.IOException; import java.net.URISyntaxException; import java.net.URL; -import java.nio.file.Files; import java.nio.file.Path; -import java.nio.file.Paths; -import java.util.List; import java.util.Properties; -import java.util.regex.Matcher; -import java.util.regex.Pattern; import java.util.stream.Stream; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; -import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.init.AbstractProfile; import de.uka.ilkd.key.proof.io.AbstractProblemLoader; import de.uka.ilkd.key.proof.io.ProblemLoaderControl; import de.uka.ilkd.key.proof.io.SingleThreadProblemLoader; -import de.uka.ilkd.key.util.ExceptionTools; +import de.uka.ilkd.key.util.ParserExceptionTest; -import org.junit.jupiter.api.Assumptions; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.Arguments; import org.junit.jupiter.params.provider.MethodSource; -import org.opentest4j.AssertionFailedError; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -import static org.junit.jupiter.api.Assertions.*; /** * This test case is used to ensure that errors in JML (and perhaps also in Java) @@ -48,30 +36,18 @@ * * @author Mattias Ulbrich */ -public class JMLParserExceptionTest { - - // The following can be changed temporarily to control run tests - private static final boolean IGNORE_BROKEN = true; - - // File name local to the res directoy with the test cases - private static final String FIX_FILE = null; // "SetInClass.java"; - - private static final Logger LOGGER = LoggerFactory.getLogger(JMLParserExceptionTest.class); +public class JMLParserExceptionTest extends ParserExceptionTest { - private final static Pattern PROP_LINE = - Pattern.compile("//\\s*(\\p{Alnum}+)\\s*[:=]\\s*(.*?)\\s*"); + /* + * Usually a directory is scanned for files to operate on. + * If this here is not null, this file name (referring to the resources + * directory) will be loaded. + */ + private static final String FIX_FILE = null; // "SomeSpecificFile.java"; public static Stream getFiles() throws URISyntaxException, IOException { URL fileURL = JMLParserExceptionTest.class.getResource("exceptional"); - assert fileURL != null : "Directory 'exceptional' not found"; - assert fileURL.getProtocol().equals("file") : "Test resources must be in file system"; - Path dir = Paths.get(fileURL.toURI()); - if (FIX_FILE != null) { - List list = List.of(Arguments.of(dir.resolve(FIX_FILE), FIX_FILE)); - return list.stream(); - } - return Files.walk(dir).filter(it -> it.getFileName().toString().endsWith(".java")) - .map(it -> Arguments.of(it, it.getFileName())); + return ParserExceptionTest.getFiles(FIX_FILE, fileURL, ".java"); } @@ -81,87 +57,13 @@ public void testParseAndInterpret(Path file, Path localFilename) throws Exceptio parseAndInterpret(file); } - // This method does not depend on anything can also be called from other test cases. - public static void parseAndInterpret(Path file) throws Exception { - List lines = Files.readAllLines(file); - Properties props = new Properties(); - for (String line : lines) { - Matcher m = PROP_LINE.matcher(line); - if (m.matches()) { - props.put(m.group(1), m.group(2)); - } else { - break; - } - } - - if ("true".equals(props.get("ignore")) - || IGNORE_BROKEN && "true".equals(props.get("broken"))) { - Assumptions.abort("This test case has been marked to be ignored"); - } - - try { - ProblemLoaderControl control = new DefaultUserInterfaceControl(null); - AbstractProblemLoader pl = new SingleThreadProblemLoader(file.toFile(), null, null, - null, AbstractProfile.getDefaultProfile(), false, - control, false, new Properties()); - pl.setLoadSingleJavaFile(true); - pl.load(); - // No exception encountered - assertEquals("true", props.getProperty("noException"), - "Unless 'noException: true' has been set, an exception is expected"); - - } catch (AssertionFailedError ae) { - throw ae; - } catch (Throwable e) { - if ("true".equals(props.getProperty("verbose"))) { - LOGGER.info("Exception raised while parsing {}", file.getFileName(), e); - } - - try { - assertNotEquals("true", props.getProperty("noException"), - "'noException: true' has been set: no exception expected"); - - // We must use throwable here since there are some Errors around ... - String exc = props.getProperty("exceptionClass"); - if (exc != null) { - if (exc.contains(".")) { - assertEquals(exc, e.getClass().getName(), "Exception type expected"); - } else { - assertEquals(exc, e.getClass().getSimpleName(), "Exception type expected"); - } - } - - String msg = props.getProperty("msgContains"); - if (msg != null) { - assertTrue(e.getMessage().contains(msg), "Message must contain " + msg); - } - - msg = props.getProperty("msgMatches"); - if (msg != null) { - assertTrue(e.getMessage().matches(msg), - "Message must match regular exp " + msg); - } - - msg = props.getProperty("msgIs"); - if (msg != null) { - assertEquals(msg, e.getMessage(), "Message must be " + msg); - } - - String loc = props.getProperty("position"); - if (loc != null) { - Location actLoc = ExceptionTools.getLocation(e).orElseThrow( - () -> new Exception("there is no location in the exception")); - assertEquals(file.toUri(), actLoc.getFileURI().orElse(null), - "Exception location must point to file under test"); - assertEquals(loc, actLoc.getPosition().toString()); - } - } catch (AssertionFailedError assertionFailedError) { - // in case of a failed assertion log the stacktrace - LOGGER.info("Original stacktrace leading to failed junit assertion in {}", - file.getFileName(), e); - // e.printStackTrace(); - throw assertionFailedError; - } - } + @Override + protected void tryLoadFile(Path file) throws Exception { + ProblemLoaderControl control = new DefaultUserInterfaceControl(null); + AbstractProblemLoader pl = new SingleThreadProblemLoader(file.toFile(), null, null, + null, AbstractProfile.getDefaultProfile(), false, + control, false, new Properties()); + pl.setLoadSingleJavaFile(true); + pl.load(); } } 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..a467bffdff0 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/util/ExceptionToolsTest.java @@ -0,0 +1,55 @@ +/* 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 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 { + 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 Column: 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/java/de/uka/ilkd/key/util/ParserExceptionTest.java b/key.core/src/test/java/de/uka/ilkd/key/util/ParserExceptionTest.java new file mode 100644 index 00000000000..e45196338f2 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/util/ParserExceptionTest.java @@ -0,0 +1,187 @@ +/* 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.IOException; +import java.net.URISyntaxException; +import java.net.URL; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.List; +import java.util.Properties; +import java.util.Set; +import java.util.regex.Matcher; +import java.util.regex.Pattern; +import java.util.stream.Stream; + +import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.proof.io.ProblemLoaderException; + +import org.junit.jupiter.api.Assumptions; +import org.junit.jupiter.params.provider.Arguments; +import org.opentest4j.AssertionFailedError; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * This test case is used to ensure that parser errors are reported with a + * reasonable error message and the right position pointing into the file. + *

+ * This framework class is versatile and can be used for different parsers, + * in particular the JML and the JavaDL parsers will be targeted. + *

+ * To add a test case, locate the "exceptional" directory in the resources + * (below the directory for the package of the refining class) and add single + * test files (file extension depending on the implementation as returned by + * ...) that contains an error that should be presented to the user (like + * syntax errors, unresolved names, ...) + *

+ * See README.md in said directories for information on the meta-data inside + * the files. + * + * @author Mattias Ulbrich + */ +public abstract class ParserExceptionTest { + + /* + * There are rest cases which are known to be broken. + * In order to remain productive, these known broken instances + * are usually deactivated. + * + * This can be changed to reactivate the broken test cases + * (to go bughunting). + */ + private static final boolean IGNORE_BROKEN = true; + + /** + * The keys supported in the headers of the files + */ + private static final Set SUPPORTED_KEYS = + Set.of("noException", "exceptionClass", "msgContains", + "msgMatches", "msgIs", "position", "ignore", "broken", "verbose"); + + private static final Logger LOGGER = LoggerFactory.getLogger(ParserExceptionTest.class); + + private final static Pattern PROP_LINE = + Pattern.compile("//\\s*(\\p{Alnum}+)\\s*[:=]\\s*(.*?)\\s*"); + + protected static Stream getFiles(String fixedFile, URL fileURL, String extension) + throws URISyntaxException, IOException { + assert fileURL != null : "Directory 'exceptional' not found"; + assert fileURL.getProtocol().equals("file") : "Test resources must be in file system"; + Path dir = Paths.get(fileURL.toURI()); + if (fixedFile != null) { + List list = List.of(Arguments.of(dir.resolve(fixedFile), fixedFile)); + return list.stream(); + } + return Files.walk(dir).filter(it -> it.getFileName().toString().endsWith(extension)) + .map(it -> Arguments.of(it, it.getFileName())); + } + + protected abstract void tryLoadFile(Path file) throws Exception; + + // This method does not depend on anything can also be called from other test cases. + public void parseAndInterpret(Path file) throws Exception { + List lines = Files.readAllLines(file); + Properties props = new Properties(); + for (String line : lines) { + Matcher m = PROP_LINE.matcher(line); + if (m.matches()) { + props.put(m.group(1), m.group(2)); + } else { + break; + } + } + + if ("true".equals(props.get("ignore")) + || IGNORE_BROKEN && "true".equals(props.get("broken"))) { + Assumptions.abort("This test case has been marked to be ignored"); + } + + props.keySet().stream().filter(k -> !SUPPORTED_KEYS.contains(k)).forEach( + k -> fail("Unsupported test spec key: " + k)); + + try { + tryLoadFile(file); + // No exception encountered + assertEquals("true", props.getProperty("noException"), + "Unless 'noException: true' has been set, an exception is expected"); + + } catch (Error ae) { + throw ae; + } catch (Throwable e) { + Throwable error = e; + if (error instanceof ProblemLoaderException) { + error = error.getCause(); + } + if ("true".equals(props.getProperty("verbose"))) { + LOGGER.info("Exception raised while parsing {}", file.getFileName(), error); + } + + try { + assertNotEquals("true", props.getProperty("noException"), + "'noException: true' has been set: no exception expected"); + + // We must use throwable here since there are some Errors around ... + String exc = props.getProperty("exceptionClass"); + if (exc != null) { + if (exc.contains(".")) { + assertEquals(exc, error.getClass().getName(), "Exception type expected"); + } else { + assertEquals(exc, error.getClass().getSimpleName(), + "Exception type expected"); + } + } + + String actualMessage = ExceptionTools.getMessage(error); + String msg = props.getProperty("msgContains"); + String errMsg = e.getMessage(); + if (msg != null) { + assertTrue(actualMessage.contains(msg), + "Message must contain '" + msg + "', but message is: '" + actualMessage + + "'"); + } + + msg = props.getProperty("msgMatches"); + if (msg != null) { + assertTrue(actualMessage.matches(msg), + "Message must match regular expression '" + msg + "', but is '" + + actualMessage + "'"); + } + + msg = props.getProperty("msgIs"); + if (msg != null) { + assertEquals(msg, actualMessage, + "Message must be " + msg + ", but is " + actualMessage + "'"); + } + + String loc = props.getProperty("position"); + if (loc != null) { + Location actLoc = ExceptionTools.getLocation(error).orElseThrow( + () -> new Exception("there is no location in the exception")); + assertEquals(file.toUri(), actLoc.getFileURI().orElse(null), + "Exception location must point to file under test"); + assertEquals(loc, actLoc.getPosition().toString()); + } + + if ("true".equals(props.getProperty("broken"))) { + LOGGER.warn( + "This test case is marked as broken, but it would actually succeed!"); + } + + } catch (AssertionFailedError assertionFailedError) { + // in case of a failed assertion log the stacktrace + LOGGER.info("Original stacktrace leading to failed junit assertion in {}", + file.getFileName(), error); + // e.printStackTrace(); + throw assertionFailedError; + } + } + } + + +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/README.md b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/README.md new file mode 100644 index 00000000000..8470792ff19 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/README.md @@ -0,0 +1,29 @@ + +This directory contains test cases for the class +`de.uka.ilkd.key.nparser.KeYParserExceptionTest`. + +To add a test case add your single .key file that contains an error +that should be presented to the user (like syntax error, unresolved +names, ...) + +The first lines of the file may contain meta data on what to +expect from the exception. Meta data are key-value pairs like + + // : + +The following keys are supported + +| Key | Description | +| --- | --- | +| `noException` | This particular file must **not** throw an exception. Default: false | +| `exceptionClass` | Either a fully qualified class name or a short classname (w/o package prefix) of the actual type of the exception. Optional. | +| `msgContains` | A string which occur somewhere in the exception message (obtained via {@link Exception#getMessage()}). Optional | +| `msgMatches` | A regular expression that must match the exception message (obtained via {@link Exception#getMessage()}). Optional | +| `msgIs` | A string to which the exception message (obtained via {@link Exception#getMessage()}) must be equal. Optional | +| `position` | A tuple in form `line`/`column` describing the position within this file. Both line and column are 1-based. It is also checked that the URL of the location points to the file under test. Optional | +| `ignore` | Ignore this test case if set to true. Default is false. | +| `broken` | If broken tests are disabled, ignore this test case if set to true. Indicates that this needs to be fixed! Default is false. | +| `verbose` | Logs the stacktrace if set to true. Default is false. | +| `checkScript` | Experimental: Provide a piece of java (script) code that must return true to make the test succeed. You may use the variable 'env' containing the parsed KeYEnvironment. | +\@author Mattias Ulbrich + diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/delayed_error.key b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/delayed_error.key new file mode 100644 index 00000000000..5cc044f6093 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/delayed_error.key @@ -0,0 +1,22 @@ +// verbose: true +// position: 13/7 +// msgContains: Expected token type(s): ';' +// exceptionClass: ParseCancellationException + +\sorts { + S; +} + +\rules { + missingSemicolon { + \schemaVar \term int t + \find(t=t) + \replacewith(0=0) + }; +} + +\problem { true } + +// The exception originally was +// line 1:0 mismatched input '(' expecting {, '\sorts', '\schemaVariables', '\programVariables', '\include', '\includeLDTs', '\classpath', '\bootclasspath', '\javaSource', '\withOptions', '\optionsDecl', '\settings', '\profile', '\heuristicsDecl', '\predicates', '\functions', '\datatypes', '\transformers', '\rules', '\axioms', '\problem', '\chooseContract', '\proofObligation', '\proof', '\contracts', '\invariants', '/*!'} +// but the problem is the missing semicolon in line 12 \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/doubleDecl.key b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/doubleDecl.key new file mode 100644 index 00000000000..7bc8ddf8eda --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/doubleDecl.key @@ -0,0 +1,12 @@ +// verbose: true +// msgContains: Function 'null' is already defined! +// position: 9/5 + + + + +\functions { + int null; +} + +\problem {true} \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/doubleDecl2.key b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/doubleDecl2.key new file mode 100644 index 00000000000..6826d03327b --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/doubleDecl2.key @@ -0,0 +1,15 @@ +// verbose: true +// msgContains: Function 'null' is already defined! +// position: 9/9 + + + + +\programVariables { + int null; +} + +\problem {true} + + +// Originally, the problem was: This crashes everything :( \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/missing_semicolon.key b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/missing_semicolon.key new file mode 100644 index 00000000000..e5feefcccfb --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/missing_semicolon.key @@ -0,0 +1,16 @@ +// noException: false +// position: 10/1 +// msgContains: Found token which was not expected: '}' + +\rules { + missingSemicolon { + \find(0=0) + \replacewith(1=1) + } +} + +\problem { true } + + +// There should be an exception; +// at least the rule missingSemicolon must be present in the end. \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/unknownsort.key b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/unknownsort.key new file mode 100644 index 00000000000..9a044c08966 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/unknownsort.key @@ -0,0 +1,9 @@ +// verbose: true +// msgContains: Could not find sort: seq +// exceptionClass: BuildingException +// position: 8/4 + + +\problem { + seq::seqGet(seqEmpty, 0) +} \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/unknownsort2.key b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/unknownsort2.key new file mode 100644 index 00000000000..62c0e48c388 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/exceptional/unknownsort2.key @@ -0,0 +1,14 @@ +// verbose: true +// msgContains: Could not find sort: seq +// exceptionClass: BuildingException +// position: 9/11 + + +\rules { + R { + \find(seq::seqGet(seqEmpty, 0)) + \replacewith(seq::seqGet(seqEmpty, 0)) + }; +} + +// There is a twin of this case where the error message is reasonable \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/AccessingSequences.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/AccessingSequences.java new file mode 100644 index 00000000000..a61ee001927 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/AccessingSequences.java @@ -0,0 +1,21 @@ +// verbose: true +// broken: true +// msgContains: expecting an integer value, not null + +class AccessingSequences { + + //@ ghost \seq seq; + + //@ ensures \result == seq[null]; + int m() { } +} + +// Is there positioning information? + +/* Not so helpful error message: + +Building a term failed. Normally there is an arity mismatch or one of the subterms' sorts is not compatible (e.g. like the '2' in "true & 2") +The top level operator was any::seqGet(Sort: any); its expected arg sorts were: +1.) sort: Seq, sort hash: 1884170567 +2.) sort: int, sort hash: 1928174253 + */ \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/Bevhavioural.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/Bevhavioural.java index 04cba1a61c9..12b1b683d7f 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/Bevhavioural.java +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/Bevhavioural.java @@ -1,9 +1,9 @@ // exceptionClass: PosConvertException // msgContains: no viable alternative at input 'normal_bevhaviour // verbose: true -// broken: true +// broken: false -// This is broken since it currently reports the wrong location +// Originally, the problem was: This is broken since it currently reports the wrong location class Bevhavioural { diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/BigInt.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/BigInt.java new file mode 100644 index 00000000000..28fa3370580 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/BigInt.java @@ -0,0 +1,11 @@ +// verbose: true +// broken: false +// msgContains: Method f(\bigint) not found +// position: 10/20 + +class BigInt { + + static int f(int x) { return 42; } + + //@ invariant f(3+4) == 42; +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/IllegalInv.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/IllegalInv.java index 4d04e33832e..c9930e9d63e 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/IllegalInv.java +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/IllegalInv.java @@ -1,8 +1,8 @@ -// exceptionClass: ConvertException +// exceptionClass: PosConvertException // msgContains: mismatched input ';' // position: 17/19 // verbose: true -// broken: true +// broken: false // currently reports the wrong position diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/KeyTest.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/KeyTest.java index adefbdf7382..5799e97f0f8 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/KeyTest.java +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/KeyTest.java @@ -1,6 +1,5 @@ -// exceptionClass: PosConvertException // msgContains: no viable alternative at input 'asignable -// position: xx/10 +// position: 8/23 // broken: true // This reports "extraneous input '*' expecting RBRACKET" which is not helpful at all. diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingClosingBrace.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingClosingBrace.java new file mode 100644 index 00000000000..77a1a60e507 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingClosingBrace.java @@ -0,0 +1,12 @@ +// verbose: true +// broken: true +// msgContains: missing '}' +// position: 8/7 + +class MissingClosingBrace { + /*@ model int modelMethodWithoutClose() { + @ return 0; + @*/ +} + +// Since RBRACE is defined twice in the grammar, this can be reported only like this?! diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingClosingParens.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingClosingParens.java new file mode 100644 index 00000000000..71163058555 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingClosingParens.java @@ -0,0 +1,11 @@ +// verbose: true +// msgContains: missing closing parenthesis +// position: 7/40 +// broken: true + +class MissingClosingParens { + //@ ensures (\forall int x; x > 5; x > 0 ; + void m() { } +} + +// Gives strange: no viable alternative at input '(\forall int x; x > 5; x > 0 ;' diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingOpeningParen.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingOpeningParen.java new file mode 100644 index 00000000000..fe453d0a860 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingOpeningParen.java @@ -0,0 +1,10 @@ +// msgContains mismatched input ')' +// position 7/32 + +class MissingOpeningParen { + + /*@ public normal_behaviour + @ requires a.length > 0); + @*/ + public int m(int a[]) { return 42; } +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingReturnType.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingReturnType.java index 806a728197e..c9f2a7f06e0 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingReturnType.java +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/MissingReturnType.java @@ -1,8 +1,8 @@ // exceptionClass: PosConvertException // msgContains: no viable alternative at input 'modelFct(' -// position: 11/14 +// position: 11/23 // verbose: true -// broken: true + class MissingReturnType { diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/NamedAccessInContract.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/NamedAccessInContract.java index 527cd20a8fc..d367e1557ed 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/NamedAccessInContract.java +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/NamedAccessInContract.java @@ -1,10 +1,9 @@ // position: 12/20 // verbose: true // broken: true -// exceptionClass: XXXX -// msgContains: XXXX +// noException: false -// currently does not report an exception +// Originally, the problem was: currently does not report an exception class NamedAccessInContract { diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/NoState.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/NoState.java index 0bfccfa9a0b..f22adf6cdc9 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/NoState.java +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/NoState.java @@ -1,5 +1,5 @@ // noException: true - +// broken: true class NoState { /*@ public model_behaviour @@ -7,3 +7,5 @@ class NoState { @ model no_state int modelFct() { return 1; } @*/ } + +// Strange error message: 'Lexical error at line 11, column 38. Encountered: after : ""' \ No newline at end of file diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/Outside.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/Outside.java new file mode 100644 index 00000000000..42591f53869 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/Outside.java @@ -0,0 +1,18 @@ +// verbose: true +// broken: true +// noException: false +// msgContains: outside +// exceptionClass: NotAnAssertion + +// currently does not raise an exception ... but it should! + +//@ invariant true; + +class Outside { + int x; + + //@ ensures true; + void m() {} +} + +//@ invariant x==2; diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/SpuriousContract.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/SpuriousContract.java new file mode 100644 index 00000000000..704afe3ad92 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/SpuriousContract.java @@ -0,0 +1,14 @@ +// position: 12/20 +// verbose: true +// broken: true +// noException: false + +// currently does not report an exception + +class SpuriousContract { + + /*@ public normal_behaviour + @ requires true; + @ ensures true; + @*/ +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/ThisStarStar.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/ThisStarStar.java new file mode 100644 index 00000000000..d69b1acf513 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/ThisStarStar.java @@ -0,0 +1,25 @@ +// NOTE: This is currently not giving a good error message +// broken: true +// msgContains: this.*.* is not a valid location set expression +// position: 9/28 + +class ThisStarStar { + + int max; + + /*@ public normal_behaviour + @ assignable this.*.*; + @*/ + public int m(int a[]) { return 0; } + +} + + +/* +TermCreationException: Building a term failed. Normally there is an arity mismatch or one of the subterms' sorts is not compatible (e.g. like the '2' in "true & 2") +The top level operator was allFields(Sort: LocSet); its expected arg sorts were: +1.) sort: java.lang.Object, sort hash: 1108066952 + +The subterms were: +1.) allFields(self)(sort: LocSet, sort hash: 1253633245) +*/ diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/TypeError.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/TypeError.java index 1be9fbf4568..d955e564ef4 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/TypeError.java +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/TypeError.java @@ -1,8 +1,9 @@ // exceptionClass: RuntimeException // msgContains: Error in equality-expression -// position: 11/19 +// position: 12/19 // verbose: true + // It's not the best of error messages ... // and there is no file location information class TypeError { diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/UnnamedAccessibleInClass.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/UnnamedAccessibleInClass.java index 537dddc077b..928fa971f0a 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/UnnamedAccessibleInClass.java +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/UnnamedAccessibleInClass.java @@ -1,7 +1,6 @@ // position: 12/20 // verbose: true // broken: true -// exceptionClass: XXXX // msgContains: XXXX // currently does not report an exception diff --git a/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/WrongEquals.java b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/WrongEquals.java new file mode 100644 index 00000000000..0ab7786f505 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/speclang/njml/exceptional/WrongEquals.java @@ -0,0 +1,25 @@ +// msgContains: mismatched input '=' +// position: 12/27 +// verbose: true + +// Author Kai Wallisch + +class WrongEquals { + + int max; + + /*@ public normal_behaviour + @ ensures \result = max; + @*/ + public int m() { return 42; } +} + +/* + * In this test "=" is used instead of "==" (line 11). + * Currently the parser message says something like: "result cannot be transformed into a formula". + * It tries to convert the term "\result" (which is of type int) into a formula. + * It would be better to inform the user that the assignment operator "=" is not allowed in a specification expression. + * (see http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_12.html#SEC127) + * The reason why this happens is because the semantic analysis of the JML code starts before the syntactic + * analysis is finished. + */ 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 8e3e602703c..6e36b867321 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(); 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 fb2115dbe09..f9066745de7 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 @@ -52,6 +52,7 @@ import org.key_project.util.collection.Pair; import org.key_project.util.java.SwingUtil; +import org.antlr.v4.runtime.misc.ParseCancellationException; import org.slf4j.Logger; import org.slf4j.LoggerFactory; import sun.misc.Signal; @@ -226,6 +227,9 @@ private void taskFinishedInternal(TaskFinishedInfo info) { Throwable result = (Throwable) info.getResult(); if (info.getResult() != null) { LOGGER.error("", result); + if (result instanceof ParseCancellationException) { + result = result.getCause(); + } IssueDialog.showExceptionDialog(mainWindow, result); } else if (getMediator().getUI().isSaveOnly()) { mainWindow.displayResults("Finished Saving!");