Hackeython/error reporting (#3432)

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());
         }
 

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

@@ -130,16 +130,20 @@ 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;
         try {
             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();

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) {

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) {

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());
         }
 

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<SLExpression> signature) {
         if (signature == null || signature.isEmpty()) {
             return "";
         }
-        StringBuilder sigString = new StringBuilder();
-
-        for (SLExpression expr : signature) {
-            final KeYJavaType t = expr.getType();
-            sigString.append(t == null ? "<unknown type>" : 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

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<Location> 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()) {

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<Arguments> 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());
+    }
+}