diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/PosConvertException.java b/key.core/src/main/java/de/uka/ilkd/key/java/PosConvertException.java index 80309c529f0..3c39e428f9f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/PosConvertException.java +++ b/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()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java index eecbd0427fd..4c0223f22fd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java +++ b/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); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstantStringExpressionEvaluator.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstantStringExpressionEvaluator.java index 0bb9b100691..bccb1b7e379 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstantStringExpressionEvaluator.java +++ b/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")) { diff --git a/key.core/src/test/java/de/uka/ilkd/key/parser/TestParser.java b/key.core/src/test/java/de/uka/ilkd/key/parser/TestParser.java index 30cc502a37a..3b6036e95c4 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/parser/TestParser.java +++ b/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 env = + KeYEnvironment.load(file, null, null, null); + }); + var error = (PosConvertException) problemLoaderException.getCause(); + assertEquals(4, error.getLine()); + assertEquals(23, error.getColumn()); + assertEquals(file.toURI().toURL(), error.getLocation().getFileURL()); + + } } diff --git a/key.core/src/test/resources/testcase/parserErrorTest/AssignToArray.java b/key.core/src/test/resources/testcase/parserErrorTest/AssignToArray.java new file mode 100644 index 00000000000..2c4d2a66549 --- /dev/null +++ b/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; + } +} diff --git a/recoder/src/main/java/recoder/java/CompilationUnit.java b/recoder/src/main/java/recoder/java/CompilationUnit.java index f990334c282..66b6ca849c8 100644 --- a/recoder/src/main/java/recoder/java/CompilationUnit.java +++ b/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; + } } diff --git a/recoder/src/main/java/recoder/java/NonTerminalProgramElement.java b/recoder/src/main/java/recoder/java/NonTerminalProgramElement.java index 3b497a57f38..9063dd6e83f 100644 --- a/recoder/src/main/java/recoder/java/NonTerminalProgramElement.java +++ b/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; + } + } }