Report location on error in constant evaluation

key.core/src/main/java/de/uka/ilkd/key/java/PosConvertException.java

@@ -19,6 +19,11 @@ public class PosConvertException extends ConvertException implements HasLocation
 
     private static final long serialVersionUID = 758453353495075586L;
 
+    /**
+     * The file this error references. May be null.
+     */
+    private String file;
+
     /**
      * The line
      */
@@ -40,6 +45,22 @@ public PosConvertException(String message, int line, int column) {
         super(message);
         this.line = line;
         this.column = column;
+        this.file = null;
+    }
+
+    /**
+     * Instantiates a new exception with position and file information.
+     *
+     * @param message the message, not null
+     * @param line the line to point to
+     * @param column the column to point to
+     * @param file the file that contains the error
+     */
+    public PosConvertException(String message, int line, int column, String file) {
+        super(message);
+        this.line = line;
+        this.column = column;
+        this.file = file;
     }
 
     /**
@@ -53,6 +74,7 @@ public PosConvertException(Throwable cause, int line, int column) {
         super(cause);
         this.line = line;
         this.column = column;
+        this.file = null;
     }
 
 
@@ -78,12 +100,15 @@ public int getColumn() {
     @Override
     public Location getLocation() throws MalformedURLException {
         Throwable cause = getCause();
-        String file = "";
-        if (cause instanceof UnresolvedReferenceException) {
-            UnresolvedReferenceException ure = (UnresolvedReferenceException) cause;
-            CompilationUnit cu = UnitKit.getCompilationUnit(ure.getUnresolvedReference());
-            String dataloc = cu.getDataLocation().toString();
-            file = dataloc.substring(dataloc.indexOf(':') + 1);
+        if (this.file == null) {
+            if (cause instanceof UnresolvedReferenceException) {
+                UnresolvedReferenceException ure = (UnresolvedReferenceException) cause;
+                CompilationUnit cu = UnitKit.getCompilationUnit(ure.getUnresolvedReference());
+                String dataloc = cu.getDataLocation().toString();
+                this.file = dataloc.substring(dataloc.indexOf(':') + 1);
+            } else {
+                this.file = "";
+            }
         }
         return new Location(file, getLine(), getColumn());
     }

key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java

@@ -41,7 +41,6 @@
 import java.io.*;
 import java.nio.charset.StandardCharsets;
 import java.nio.file.Paths;
-import java.text.MessageFormat;
 import java.util.*;
 
 /**
@@ -1234,9 +1233,14 @@ public static void reportError(String message, Throwable t) {
         }
 
         int[] pos = extractPositionInfo(cause.toString());
+        reportErrorWithPositionInFile(message, cause, pos, null);
+    }
+
+    public static void reportErrorWithPositionInFile(String message, Throwable cause, int[] pos,
+            String file) {
         final RuntimeException rte;
         if (pos.length > 0) {
-            rte = new PosConvertException(message, pos[0], pos[1]);
+            rte = new PosConvertException(message, pos[0], pos[1], file);
             rte.initCause(cause);
         } else {
             rte = new ConvertException(message, cause);

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstantStringExpressionEvaluator.java

@@ -1,10 +1,12 @@
 package de.uka.ilkd.key.java.recoderext;
 
+import de.uka.ilkd.key.java.Recoder2KeY;
 import recoder.CrossReferenceServiceConfiguration;
 import recoder.abstraction.Type;
 import recoder.java.Expression;
 import recoder.java.NonTerminalProgramElement;
 import recoder.java.ProgramElement;
+import recoder.java.SourceElement;
 import recoder.java.declaration.TypeDeclaration;
 import recoder.java.expression.literal.NullLiteral;
 import recoder.java.expression.literal.StringLiteral;
@@ -26,7 +28,18 @@ private void evaluateConstantStringExpressions(NonTerminalProgramElement td) {
 
                 ConstantEvaluator.EvaluationResult res = new ConstantEvaluator.EvaluationResult();
 
-                Type expType = services.getSourceInfo().getType((Expression) pe);
+                Type expType = null;
+                try {
+                    expType = services.getSourceInfo().getType((Expression) pe);
+                } catch (Exception e) {
+                    // on failure: report with position information
+                    SourceElement.Position pos = pe.getStartPosition();
+                    int[] posArr = new int[] { pos.getLine(), pos.getColumn() };
+                    String file = td.compilationUnit().getDataLocation().toString();
+                    Recoder2KeY.reportErrorWithPositionInFile(
+                        "failed to perform constant evaluation", e,
+                        posArr, file);
+                }
 
                 if (!(pe instanceof NullLiteral) && expType != null
                         && expType.getFullName().equals("java.lang.String")) {

key.core/src/test/java/de/uka/ilkd/key/parser/TestParser.java

@@ -2,6 +2,7 @@
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.java.PosConvertException;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.nparser.KeyIO;
@@ -16,6 +17,7 @@
 
 import java.io.File;
 import java.io.IOException;
+import java.net.MalformedURLException;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
 import static org.junit.jupiter.api.Assertions.assertThrows;
@@ -79,4 +81,19 @@ public void testIssue39() {
         });
 
     }
+
+    @Test
+    void testConstantEvaluationError() throws MalformedURLException {
+        var file =
+            new File(HelperClassForTests.TESTCASE_DIRECTORY, "parserErrorTest/AssignToArray.java");
+        var problemLoaderException = assertThrows(ProblemLoaderException.class, () -> {
+            KeYEnvironment<DefaultUserInterfaceControl> env =
+                KeYEnvironment.load(file, null, null, null);
+        });
+        var error = (PosConvertException) problemLoaderException.getCause();
+        assertEquals(6, error.getLine());
+        assertEquals(23, error.getColumn());
+        assertEquals(file.toURI().toURL(), error.getLocation().getFileURL());
+
+    }
 }

key.core/src/test/resources/testcase/parserErrorTest/AssignToArray.java

@@ -0,0 +1,6 @@
+class AssignToArray {
+    public static void main(String[] args) {
+        boolean notAnArray = new boolean[5];
+        notAnArray[1] = true;
+    }
+}

recoder/src/main/java/recoder/java/CompilationUnit.java

@@ -490,4 +490,9 @@ public void removeTypeFromScope(String name) {
     public void accept(SourceVisitor v) {
         v.visitCompilationUnit(this);
     }
+
+    @Override
+    public CompilationUnit compilationUnit() {
+        return this;
+    }
 }

recoder/src/main/java/recoder/java/NonTerminalProgramElement.java

@@ -108,9 +108,23 @@ public interface NonTerminalProgramElement extends ProgramElement {
      * parent link of the replaced child is left untouched.
      *
      * @param p the old child.
-     * @param p the new child.
+     * @param q the new child.
      * @return true if a replacement has occured, false otherwise.
      * @throws ClassCastException if the new child cannot take over the role of the old one.
      */
     boolean replaceChild(ProgramElement p, ProgramElement q);
+
+    /**
+     * Get the compilation unit that contains this program element.
+     *
+     * @return the compilation unit
+     */
+    default CompilationUnit compilationUnit() {
+        NonTerminalProgramElement parent = getASTParent();
+        if (parent != null) {
+            return parent.compilationUnit();
+        } else {
+            return null;
+        }
+    }
 }