Show details of the error message in test failures (#7513)

Author: mernst

docs/CHANGELOG.md

@@ -25,6 +25,11 @@ In `AnnotationClassLoader`:
   The method now returns `true` for annotations bearing `@InvisibleQualifier`
   or `@SubtypeOf`, in addition to the existing `@Target(TYPE_USE)` check.
 
+In `TestDiagnostic`:
+
+* Renamed field `message` to `key`.
+* Added new nullable field `message` for the full message without the key.
+
 Removed classes and methods that have been deprecated for more than two years.
 
 ### Closed issues

framework-test/src/main/java/org/checkerframework/framework/test/TypecheckExecutor.java

@@ -86,11 +86,7 @@ public CompilationResult compile(TestConfiguration configuration) {
       nonJvmOptions.add("-ApermitMissingJdk");
       nonJvmOptions.add("-Anocheckjdk"); // temporary, for backward compatibility
 
-      // -Anomsgtext is needed to ensure expected errors can be matched.
-      // Note: Since "-Anomsgtext" is always added to the non-JVM options,
-      //  we are passing `true` as the `noMsgText` argument to all invocations
-      //  of `TestDiagnosticUtils.fromJavaxDiagnosticList`.
-      nonJvmOptions.add("-Anomsgtext");
+      nonJvmOptions.add("-Aonelinemsg");
 
       options.addAll(nonJvmOptions);
 

framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java

@@ -12,36 +12,51 @@
  */
 public class TestDiagnostic {
 
+  /** The file to which the diagnostic applies. */
   private final String filename;
+
+  /** The line number to which the diagnostic applies. */
   private final long lineNumber;
+
+  /** The kind of diagnostic. */
   private final DiagnosticKind kind;
 
   /**
-   * An error key or full error message that usually appears between parentheses in diagnostic
+   * An error key or full error message that usually appears between square brackets in diagnostic
    * messages.
    */
-  private final String message;
+  private final String key;
 
-  /** Returns true if this diagnostic should no longer be reported after whole program inference. */
-  private final boolean isFixable;
+  /** The full error message, without the key. Null if the key is the whole message. */
+  private final @Nullable String message;
 
-  /** True if the toString representation should omit the parentheses around the message. */
-  private final boolean omitParentheses;
+  /** True if this diagnostic should no longer be reported after whole-program inference. */
+  private final boolean isFixable;
 
-  /** Basic constructor that sets the immutable fields of this diagnostic. */
+  /**
+   * Basic constructor that sets the immutable fields of this diagnostic.
+   *
+   * @param filename the file to which the diagnostic applies
+   * @param lineNumber the line number to which the diagnostic applies
+   * @param kind kind of diagnostic
+   * @param key an error key or full error message
+   * @param message the full error message, without the key; null if the key is the whole message
+   * @param isFixable true if this diagnostic should no longer be reported after whole-program
+   *     inference
+   */
   public TestDiagnostic(
       String filename,
       long lineNumber,
       DiagnosticKind kind,
-      String message,
-      boolean isFixable,
-      boolean omitParentheses) {
+      String key,
+      @Nullable String message,
+      boolean isFixable) {
     this.filename = filename;
     this.lineNumber = lineNumber;
     this.kind = kind;
+    this.key = key;
     this.message = message;
     this.isFixable = isFixable;
-    this.omitParentheses = omitParentheses;
   }
 
   public String getFilename() {
@@ -56,28 +71,38 @@ public DiagnosticKind getKind() {
     return kind;
   }
 
-  public String getMessage() {
-    return message;
+  /**
+   * Returns the error message key.
+   *
+   * @return the error message key
+   */
+  public String getKey() {
+    return key;
   }
 
-  public boolean isFixable() {
-    return isFixable;
+  /**
+   * Returns the full error message, without the key.
+   *
+   * @return the full error message, without the key
+   */
+  public @Nullable String getMessage() {
+    return message;
   }
 
   /**
-   * Returns true if the printed representation should omit parentheses around the message.
+   * Returns true if this diagnostic should no longer be reported after whole-program inference.
    *
-   * @return true if the printed representation should omit parentheses around the message
+   * @return true if this diagnostic should no longer be reported after whole-program inference
    */
-  public boolean shouldOmitParentheses() {
-    return omitParentheses;
+  public boolean isFixable() {
+    return isFixable;
   }
 
   /**
-   * Equality is compared without isFixable/omitParentheses.
+   * Equality is compared without fields {@code message} and {@code isFixable}.
    *
    * @return true if this and otherObj are equal according to filename, lineNumber, kind, and
-   *     message
+   *     message key
    */
   @Override
   public boolean equals(@Nullable Object otherObj) {
@@ -89,12 +114,12 @@ public boolean equals(@Nullable Object otherObj) {
     return other.filename.equals(this.filename)
         && other.lineNumber == lineNumber
         && other.kind == this.kind
-        && other.message.equals(this.message);
+        && other.key.equals(this.key);
   }
 
   @Override
   public int hashCode() {
-    return Objects.hash(filename, lineNumber, kind, message);
+    return Objects.hash(filename, lineNumber, kind, key);
   }
 
   /**
@@ -104,13 +129,14 @@ public int hashCode() {
    */
   @Override
   public String toString() {
+    String loc = filename + ":" + lineNumber + ": ";
+    String key = "(" + this.key + ")";
+    String msg = message == null ? "" : " " + message;
     if (kind == DiagnosticKind.JSpecify) {
-      return filename + ":" + lineNumber + ": " + message;
-    }
-    if (omitParentheses) {
-      return filename + ":" + lineNumber + ": " + kind.parseString + ": " + message;
+      return loc + key;
+    } else {
+      return loc + kind.parseString + ": " + key + msg;
     }
-    return filename + ":" + lineNumber + ": " + kind.parseString + ": (" + message + ")";
   }
 
   /**
@@ -120,7 +146,7 @@ public String toString() {
    */
   public String repr() {
     return String.format(
-        "[TestDiagnostic: filename=%s, lineNumber=%d, kind=%s, message=%s]",
-        filename, lineNumber, kind, message);
+        "[TestDiagnostic: filename=%s, lineNumber=%d, kind=%s, key=%s]",
+        filename, lineNumber, kind, key);
   }
 }

framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticUtils.java

@@ -12,6 +12,7 @@
 import javax.tools.JavaFileObject;
 import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.javacutil.BugInCF;
 import org.plumelib.util.CollectionsPlume;
 import org.plumelib.util.IPair;
 
@@ -64,8 +65,8 @@ public static TestDiagnostic fromDiagnosticFileString(String stringFromDiagnosti
   }
 
   /**
-   * Instantiate the diagnostic from a string that would appear in a Java file, e.g.: "error:
-   * (message)"
+   * Instantiate the diagnostic from a string that would appear in a Java test file, e.g.: "error:
+   * (error-message-key)"
    *
    * @param filename the file containing the diagnostic (and the error)
    * @param lineNumber the line number of the line immediately below the diagnostic comment in the
@@ -117,17 +118,18 @@ public static TestDiagnostic fromJSpecifyFileComment(
         lineNumber,
         DiagnosticKind.JSpecify,
         stringFromJavaFile,
-        /* isFixable= */ false,
-        /* omitParentheses= */ true);
+        null,
+        /* isFixable= */ false);
   }
 
   /**
-   * Instantiate the diagnostic via pattern-matching against patterns.
+   * Instantiate the diagnostic via pattern-matching against the given patterns.
    *
    * @param diagnosticPattern a pattern that matches any diagnostic
    * @param warningPattern a pattern that matches a warning diagnostic
    * @param filename the file name
-   * @param lineNumber the line number
+   * @param lineNumber the line number. Either this is non-null, or the pattern's first matching
+   *     group is the line number.
    * @param diagnosticString the string to parse
    * @return a diagnostic parsed from the given string
    */
@@ -139,9 +141,9 @@ protected static TestDiagnostic fromPatternMatching(
       @Nullable Long lineNumber,
       String diagnosticString) {
     final DiagnosticKind kind;
+    final String key;
     final String message;
     final boolean isFixable;
-    final boolean noParentheses;
     long lineNo = -1;
     int capturingGroupOffset = 1;
 
@@ -152,13 +154,33 @@ protected static TestDiagnostic fromPatternMatching(
 
     Matcher diagnosticMatcher = diagnosticPattern.matcher(diagnosticString);
     if (diagnosticMatcher.matches()) {
-      IPair<DiagnosticKind, Boolean> categoryToFixable =
+
+      IPair<DiagnosticKind, Boolean> categoryAndFixable =
           categoryAndFixable(diagnosticMatcher.group(1 + capturingGroupOffset));
-      kind = categoryToFixable.first;
-      isFixable = categoryToFixable.second;
+      kind = categoryAndFixable.first;
+      isFixable = categoryAndFixable.second;
       String msg = diagnosticMatcher.group(2 + capturingGroupOffset).trim();
-      noParentheses = msg.equals("") || msg.charAt(0) != '(' || msg.charAt(msg.length() - 1) != ')';
-      message = noParentheses ? msg : msg.substring(1, msg.length() - 1);
+
+      char firstChar = msg.isEmpty() ? ' ' : msg.charAt(0);
+      if (firstChar == '(' || firstChar == '[') {
+        char closeDelimiter = firstChar == '(' ? ')' : ']';
+        int closeDelimiterPos = msg.indexOf(closeDelimiter);
+        int msgLength = msg.length();
+        if (closeDelimiterPos == msgLength - 1) {
+          key = msg.substring(1, msgLength - 1);
+          message = null;
+        } else if (closeDelimiterPos != -1) {
+          key = msg.substring(1, closeDelimiterPos);
+          message = msg.substring(closeDelimiterPos + 1).trim();
+        } else {
+          throw new BugInCF(
+              "No closing delimiter '%s' found in %s", closeDelimiter, diagnosticString);
+        }
+      } else {
+        // The message does not start with "(" or "[".
+        key = msg;
+        message = null;
+      }
 
       if (lineNumber == null) {
         try {
@@ -173,8 +195,8 @@ protected static TestDiagnostic fromPatternMatching(
       if (warningMatcher.matches()) {
         kind = DiagnosticKind.Warning;
         isFixable = false;
-        message = warningMatcher.group(1 + capturingGroupOffset);
-        noParentheses = true;
+        key = warningMatcher.group(1 + capturingGroupOffset);
+        message = null;
 
         if (lineNumber == null) {
           try {
@@ -187,8 +209,8 @@ protected static TestDiagnostic fromPatternMatching(
       } else if (diagnosticString.startsWith("warning:")) {
         kind = DiagnosticKind.Warning;
         isFixable = false;
-        message = diagnosticString.substring("warning:".length()).trim();
-        noParentheses = true;
+        key = diagnosticString.substring("warning:".length()).trim();
+        message = null;
         if (lineNumber != null) {
           lineNo = lineNumber;
         } else {
@@ -198,19 +220,23 @@ protected static TestDiagnostic fromPatternMatching(
       } else {
         kind = DiagnosticKind.Other;
         isFixable = false;
-        message = diagnosticString;
-        noParentheses = true;
+        key = diagnosticString;
+        message = null;
 
-        // this should only happen if we are parsing a Java Diagnostic from the compiler
-        // that we did do not handle
+        // This should only happen if we are parsing a Java Diagnostic from the compiler
+        // that we did do not handle.
         if (lineNumber == null) {
           lineNo = -1;
         }
       }
     }
-    return new TestDiagnostic(filename, lineNo, kind, message, isFixable, noParentheses);
+    return new TestDiagnostic(filename, lineNo, kind, key, message, isFixable);
   }
 
+  /** Matches an absolute filename (with delimiters). */
+  // TODO: This only handles Unix paths, not Windows paths.
+  static final Pattern filenamePattern = Pattern.compile(" (?:/[^: ]*/)([^/: ]+\\.[a-z]+):");
+
   /**
    * Given a javax diagnostic, return a pair of (trimmed, filename), where "trimmed" is the first
    * line of the message, without the leading filename.
@@ -224,17 +250,26 @@ public static IPair<String, String> messageAndFilename(String original, boolean
     String filename = "";
     if (noMsgText) {
       if (!retainAllLines(trimmed)) {
+
+        // Retain only the first line.
         int lineSepPos = trimmed.indexOf(System.lineSeparator());
         if (lineSepPos != -1) {
           trimmed = trimmed.substring(0, lineSepPos);
         }
 
         int extensionPos = trimmed.indexOf(".java:");
         if (extensionPos != -1) {
-          int basenameStart = trimmed.lastIndexOf(File.separator);
+          int basenameStart = trimmed.lastIndexOf(File.separator, extensionPos);
           filename = trimmed.substring(basenameStart + 1, extensionPos + 5).trim();
           trimmed = trimmed.substring(extensionPos + 5).trim();
         }
+
+        // Retain only the file basename, without directories, when embedded in message.
+        Matcher m = filenamePattern.matcher(trimmed);
+        if (m.find()) {
+          trimmed =
+              trimmed.substring(0, m.start()) + " " + m.group(1) + ":" + trimmed.substring(m.end());
+        }
       }
     }
 
@@ -363,8 +398,8 @@ public static TestDiagnosticLine fromJavaSourceLine(
               lineNumber,
               DiagnosticKind.Error,
               "Use \"// ::\", not \"//::\"",
-              false,
-              true);
+              null,
+              false);
       return new TestDiagnosticLine(
           filename, lineNumber, line, Collections.singletonList(diagnostic));
     } else if (trimmedLine.startsWith("// jspecify_")) {