Add Custom Error Messages (#140)

Author: rcosta358

liquidjava-api/src/main/java/liquidjava/specification/Refinement.java

@@ -16,4 +16,6 @@
 public @interface Refinement {
 
     public String value();
+
+    public String msg() default "";
 }

liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java

@@ -7,9 +7,9 @@
 import java.lang.annotation.Target;
 
 /**
- * Annotation to create state transitions in a method. The annotation has two arguments: from : the
+ * Annotation to create state transitions in a method. The annotation has three arguments: from : the
  * state in which the object needs to be for the method to be invoked correctly to : the state in
- * which the object will be after the execution of the method
+ * which the object will be after the execution of the method msg : optional custom error message to display when refinement is violated
  * e.g. @StateRefinement(from="open(this)", to="closed(this)")
  *
  * @author catarina gamboa
@@ -21,4 +21,6 @@
     public String from() default "";
 
     public String to() default "";
+
+    public String msg() default "";
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -11,15 +11,18 @@ public class LJDiagnostic extends RuntimeException {
     private final String title;
     private final String message;
     private final String accentColor;
+    private final String customMessage;
     private String file;
     private ErrorPosition position;
+    private static final String PIPE = " | ";
 
-    public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor) {
+    public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) {
         this.title = title;
         this.message = message;
         this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null;
         this.position = ErrorPosition.fromSpoonPosition(pos);
         this.accentColor = accentColor;
+        this.customMessage = customMessage;
     }
 
     public String getTitle() {
@@ -30,6 +33,10 @@ public String getMessage() {
         return message;
     }
 
+    public String getCustomMessage() {
+        return customMessage;
+    }
+
     public String getDetails() {
         return ""; // to be overridden by subclasses
     }
@@ -104,19 +111,26 @@ public String getSnippet() {
                 String line = lines.get(i - 1);
 
                 // add line
-                sb.append(Colors.GREY).append(lineNumStr).append(" | ").append(line).append(Colors.RESET).append("\n");
+                sb.append(Colors.GREY).append(lineNumStr).append(PIPE).append(line).append(Colors.RESET).append("\n");
 
                 // add error markers on the line(s) with the error
                 if (i >= position.lineStart() && i <= position.lineEnd()) {
                     int colStart = (i == position.lineStart()) ? position.colStart() : 1;
                     int colEnd = (i == position.lineEnd()) ? position.colEnd() : line.length();
 
                     if (colStart > 0 && colEnd > 0) {
-                        // line number padding + " | " + column offset
-                        String indent = " ".repeat(padding) + Colors.GREY + " | " + Colors.RESET
+                        // line number padding + pipe + column offset
+                        String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET
                                 + " ".repeat(colStart - 1);
-                        String markers = accentColor + "^".repeat(Math.max(1, colEnd - colStart + 1)) + Colors.RESET;
-                        sb.append(indent).append(markers).append("\n");
+                        String markers = accentColor + "^".repeat(Math.max(1, colEnd - colStart + 1));
+                        sb.append(indent).append(markers);
+
+                        // custom message
+                        if (customMessage != null && !customMessage.isBlank()) {
+                            String offset = " ".repeat(padding + colEnd + PIPE.length() + 1);
+                            sb.append(" " + customMessage.replace("\n", "\n" + offset));
+                        }
+                        sb.append(Colors.RESET).append("\n");
                     }
                 }
             }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java

@@ -13,7 +13,12 @@ public abstract class LJError extends LJDiagnostic {
     private final TranslationTable translationTable;
 
     public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable) {
-        super(title, message, pos, Colors.BOLD_RED);
+        this(title, message, pos, translationTable, null);
+    }
+
+    public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable,
+            String customMessage) {
+        super(title, message, pos, Colors.BOLD_RED, customMessage);
         this.translationTable = translationTable != null ? translationTable : new TranslationTable();
     }
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -16,9 +16,9 @@ public class RefinementError extends LJError {
     private final ValDerivationNode found;
 
     public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
-            TranslationTable translationTable) {
+            TranslationTable translationTable, String customMessage) {
         super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()),
-                position, translationTable);
+                position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
     }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -15,9 +15,9 @@ public class StateRefinementError extends LJError {
     private final String found;
 
     public StateRefinementError(SourcePosition position, Expression expected, Expression found,
-            TranslationTable translationTable) {
+            TranslationTable translationTable, String customMessage) {
         super("State Refinement Error", String.format("Expected state %s but found %s", expected.toSimplifiedString(),
-                found.toSimplifiedString()), position, translationTable);
+                found.toSimplifiedString()), position, translationTable, customMessage);
         this.expected = expected.toSimplifiedString();
         this.found = found.toSimplifiedString();
     }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java

@@ -10,6 +10,6 @@
 public abstract class LJWarning extends LJDiagnostic {
 
     public LJWarning(String message, SourcePosition pos) {
-        super("Warning", message, pos, Colors.BOLD_YELLOW);
+        super("Warning", message, pos, Colors.BOLD_YELLOW, null);
     }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java

@@ -6,6 +6,7 @@ public class ObjectState {
 
     Predicate from;
     Predicate to;
+    String message;
 
     public ObjectState() {
     }
@@ -15,6 +16,12 @@ public ObjectState(Predicate from, Predicate to) {
         this.to = to;
     }
 
+    public ObjectState(Predicate from, Predicate to, String message) {
+        this.from = from;
+        this.to = to;
+        this.message = message;
+    }
+
     public void setFrom(Predicate from) {
         this.from = from;
     }
@@ -39,8 +46,16 @@ public Predicate getTo() {
         return to != null ? to : new Predicate();
     }
 
+    public String getMessage() {
+        return message;
+    }
+
+    public void setMessage(String message) {
+        this.message = message;
+    }
+
     public ObjectState clone() {
-        return new ObjectState(from.clone(), to.clone());
+        return new ObjectState(from.clone(), to.clone(), message);
     }
 
     @Override

liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java

@@ -8,6 +8,7 @@ public abstract class Refined {
     private String name; // y
     private CtTypeReference<?> type; // int
     private Predicate refinement; // 9 <= y && y <= 100
+    private String message;
 
     public Refined() {
     }
@@ -44,6 +45,14 @@ public Predicate getRefinement() {
         return new Predicate();
     }
 
+    public String getMessage() {
+        return message;
+    }
+
+    public void setMessage(String message) {
+        this.message = message;
+    }
+
     public Predicate getRenamedRefinements(String toReplace) {
         return refinement.substituteVariable(name, toReplace);
     }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -124,10 +124,10 @@ public <T> void visitCtLocalVariable(CtLocalVariable<T> localVariable) {
         super.visitCtLocalVariable(localVariable);
         // only declaration, no assignment
         if (localVariable.getAssignment() == null) {
-            Optional<Predicate> a;
-            a = getRefinementFromAnnotation(localVariable);
-            context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(), a.orElse(new Predicate()),
-                    localVariable);
+            Optional<Predicate> a = getRefinementFromAnnotation(localVariable);
+            RefinedVariable v = context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(),
+                    a.orElse(new Predicate()), localVariable);
+            getMessageFromAnnotation(localVariable).ifPresent(v::setMessage);
         } else {
             String varName = localVariable.getSimpleName();
             CtExpression<?> e = localVariable.getAssignment();
@@ -238,6 +238,7 @@ public <T> void visitCtField(CtField<T> f) {
             ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name);
         }
         RefinedVariable v = context.addVarToContext(name, f.getType(), ret, f);
+        getMessageFromAnnotation(f).ifPresent(v::setMessage);
         if (v instanceof Variable) {
             ((Variable) v).setLocation("this");
         }