Add Custom Error Messages

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,17 @@ 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;
 
-    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 +32,10 @@ public String getMessage() {
         return message;
     }
 
+    public String getCustomMessage() {
+        return customMessage;
+    }
+
     public String getDetails() {
         return ""; // to be overridden by subclasses
     }
@@ -98,25 +104,33 @@ public String getSnippet() {
 
             // calculate padding for line numbers
             int padding = String.valueOf(endLine).length();
+            String pipe = " | ";
 
             for (int i = startLine; i <= endLine; i++) {
                 String lineNumStr = String.format("%" + padding + "d", i);
                 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");
         }

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

@@ -89,6 +89,19 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
         return constr;
     }
 
+    public Optional<String> getMessageFromAnnotation(CtElement element) {
+        for (CtAnnotation<? extends Annotation> ann : element.getAnnotations()) {
+            String an = ann.getActualAnnotation().annotationType().getCanonicalName();
+            if (an.contentEquals("liquidjava.specification.Refinement")) {
+                String msg = getStringFromAnnotation(ann.getValue("msg"));
+                if (msg != null && !msg.isEmpty()) {
+                    return Optional.of(msg);
+                }
+            }
+        }
+        return Optional.empty();
+    }
+
     @SuppressWarnings("unchecked")
     public void handleStateSetsFromAnnotation(CtElement element) throws LJError {
         int set = 0;
@@ -277,13 +290,17 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
         for (CtTypeReference<?> t : mainRV.getSuperTypes())
             rv.addSuperType(t);
         context.addRefinementInstanceToVariable(simpleName, newName);
-        // smt check
-        checkSMT(cEt, usage); // TODO CHANGE
+        String customMessage = getMessageFromAnnotation(variable).orElse(mainRV != null ? mainRV.getMessage() : null);
+        checkSMT(cEt, usage, customMessage); // TODO CHANGE
         context.addRefinementToVariableInContext(simpleName, type, cet, usage);
     }
 
     public void checkSMT(Predicate expectedType, CtElement element) throws LJError {
-        vcChecker.processSubtyping(expectedType, context.getGhostState(), element, factory);
+        checkSMT(expectedType, element, null);
+    }
+
+    public void checkSMT(Predicate expectedType, CtElement element, String customMessage) throws LJError {
+        vcChecker.processSubtyping(expectedType, context.getGhostState(), element, factory, customMessage);
         element.putMetadata(Keys.REFINEMENT, expectedType);
     }
 
@@ -296,13 +313,14 @@ public boolean checksStateSMT(Predicate prevState, Predicate expectedState, Sour
         return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory);
     }
 
-    public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType)
-            throws LJError {
-        vcChecker.throwRefinementError(position, expectedType, foundType);
+    public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType,
+            String customMessage) throws LJError {
+        vcChecker.throwRefinementError(position, expectedType, foundType, customMessage);
     }
 
-    public void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected) throws LJError {
-        vcChecker.throwStateRefinementError(position, found, expected);
+    public void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected,
+            String customMessage) throws LJError {
+        vcChecker.throwStateRefinementError(position, found, expected, customMessage);
     }
 
     public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError {

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

@@ -31,6 +31,11 @@ public VCChecker() {
 
     public void processSubtyping(Predicate expectedType, List<GhostState> list, CtElement element, Factory f)
             throws LJError {
+        processSubtyping(expectedType, list, element, f, null);
+    }
+
+    public void processSubtyping(Predicate expectedType, List<GhostState> list, CtElement element, Factory f,
+            String customMessage) throws LJError {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
         gatherVariables(expectedType, lrv, mainVars);
         if (expectedType.isBooleanTrue())
@@ -53,7 +58,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         boolean isSubtype = smtChecks(expected, premises, element.getPosition());
         if (!isSubtype)
             throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(),
-                    map);
+                    map, customMessage);
     }
 
     /**
@@ -71,7 +76,7 @@ public void processSubtyping(Predicate type, Predicate expectedType, List<GhostS
             Factory f) throws LJError {
         boolean b = canProcessSubtyping(type, expectedType, list, element.getPosition(), f);
         if (!b)
-            throwRefinementError(element.getPosition(), expectedType, type);
+            throwRefinementError(element.getPosition(), expectedType, type, null);
     }
 
     /**
@@ -256,24 +261,24 @@ void removePathVariableThatIncludes(String otherVar) {
 
     // Errors---------------------------------------------------------------------------------------------------
 
-    protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found)
-            throws RefinementError {
+    protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found,
+            String customMessage) throws RefinementError {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
         gatherVariables(expected, lrv, mainVars);
         gatherVariables(found, lrv, mainVars);
         TranslationTable map = new TranslationTable();
         Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions();
-        throw new RefinementError(position, expected.simplify(), premises.simplify(), map);
+        throw new RefinementError(position, expected.simplify(), premises.simplify(), map, customMessage);
     }
 
-    protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected)
-            throws StateRefinementError {
+    protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected,
+            String customMessage) throws StateRefinementError {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
         gatherVariables(found, lrv, mainVars);
         TranslationTable map = new TranslationTable();
         VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
         throw new StateRefinementError(position, expected.getExpression(),
-                foundState.toConjunctions().simplify().getValue(), map);
+                foundState.toConjunctions().simplify().getValue(), map, customMessage);
     }
 
     protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -154,6 +154,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method,
                 c = oc.get().substituteVariable(Keys.WILDCARD, paramName);
             param.putMetadata(Keys.REFINEMENT, c);
             RefinedVariable v = rtc.getContext().addVarToContext(param.getSimpleName(), param.getType(), c, param);
+            rtc.getMessageFromAnnotation(param).ifPresent(v::setMessage);
             if (v instanceof Variable)
                 f.addArgRefinements((Variable) v);
             joint = Predicate.createConjunction(joint, c);
@@ -162,6 +163,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method,
         Predicate ret = oret.orElse(new Predicate());
         ret = ret.substituteVariable("return", Keys.WILDCARD);
         f.setRefReturn(ret);
+        rtc.getMessageFromAnnotation(method).ifPresent(f::setMessage);
         return Predicate.createConjunction(joint, ret);
     }
 
@@ -196,7 +198,7 @@ public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
                         .substituteVariable(Keys.THIS, returnVarName);
 
                 rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret);
-                rtc.checkSMT(cexpectedType, ret);
+                rtc.checkSMT(cexpectedType, ret, fi.getMessage());
                 rtc.getContext().newRefinementToVariableInContext(returnVarName, cexpectedType);
             }
         }
@@ -367,7 +369,7 @@ private void checkParameters(CtElement invocation, List<CtExpression<?>> argumen
                 VariableInstance vi = (VariableInstance) invocation.getMetadata(Keys.TARGET);
                 c = c.substituteVariable(Keys.THIS, vi.getName());
             }
-            rtc.checkSMT(c, invocation);
+            rtc.checkSMT(c, invocation, fArg.getMessage());
         }
     }
 

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java

@@ -83,7 +83,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF
             } else {
                 boolean ok = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition());
                 if (!ok) {
-                    tc.throwRefinementError(method.getPosition(), argRef, superArgRef);
+                    tc.throwRefinementError(method.getPosition(), argRef, superArgRef, function.getMessage());
                 }
             }
         }