Skip to content

Add Custom Messages to Errors #140

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
rcosta358 wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Add Custom Messages to Errors #140

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
618c5b5
Add Custom Messages
rcosta358 Feb 5, 2026
15c99da
Separate Multiple Messages by Line
rcosta358 Feb 5, 2026
520ef85
Minor Changes
rcosta358 Feb 5, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions liquidjava-api/src/main/java/liquidjava/specification/Refinement.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,4 +16,6 @@
public @interface Refinement {

public String value();

public String msg() default "";
}
6 changes: 4 additions & 2 deletions liquidjava-api/src/main/java/liquidjava/specification/StateRefinement.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -21,4 +21,6 @@
public String from() default "";

public String to() default "";

public String msg() default "";
}
26 changes: 20 additions & 6 deletions liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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() {
Expand All @@ -30,6 +32,10 @@ public String getMessage() {
return message;
}

public String getCustomMessage() {
return customMessage;
}

public String getDetails() {
return ""; // to be overridden by subclasses
}
Expand Down Expand Up @@ -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");
}
}
}
Expand Down
7 changes: 6 additions & 1 deletion liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}

Expand Down
4 changes: 2 additions & 2 deletions liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
4 changes: 2 additions & 2 deletions liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}
Expand Down
2 changes: 1 addition & 1 deletion liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
17 changes: 16 additions & 1 deletion liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ public class ObjectState {

Predicate from;
Predicate to;
String message;

public ObjectState() {
}
Expand All @@ -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;
}
Expand All @@ -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
Expand Down
9 changes: 9 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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() {
}
Expand Down Expand Up @@ -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);
}
Expand Down
9 changes: 5 additions & 4 deletions ...verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -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");
}
Expand Down
34 changes: 26 additions & 8 deletions liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
}

Expand All @@ -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 {
Expand Down
21 changes: 13 additions & 8 deletions liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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())
Expand All @@ -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);
}

/**
Expand All @@ -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);
}

/**
Expand Down Expand Up @@ -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 {
Expand Down
6 changes: 4 additions & 2 deletions ...ava/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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);
}

Expand Down Expand Up @@ -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);
}
}
Expand Down Expand Up @@ -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());
}
}

Expand Down
2 changes: 1 addition & 1 deletion ...quidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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());
}
}
}
Expand Down
Loading