From 19b20491ca453cbb76b6eb0c0fd4bae3df4ef199 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 19 Nov 2025 15:15:28 +0000 Subject: [PATCH 1/6] Error Updates --- liquidjava-verifier/pom.xml | 2 +- .../liquidjava/diagnostics/LJDiagnostic.java | 6 ++++- .../errors/GhostInvocationError.java | 25 ------------------- .../diagnostics/errors/NotFoundError.java | 10 +++++++- .../errors/StateConflictError.java | 10 ++------ .../errors/StateRefinementError.java | 22 ++++------------ .../refinement_checker/TypeChecker.java | 2 +- .../refinement_checker/VCChecker.java | 23 ++++++++--------- .../object_checkers/AuxStateHandler.java | 9 +++---- .../liquidjava/rj_language/Predicate.java | 9 +++++++ .../java/liquidjava/smt/TranslatorToZ3.java | 4 +-- .../liquidjava/smt/errors/NotFoundError.java | 9 ++++++- 12 files changed, 57 insertions(+), 74 deletions(-) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 5edca456..5ed5521f 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -11,7 +11,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.2 + 0.0.3 liquidjava-verifier LiquidJava Verifier https://github.com/liquid-java/liquidjava diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index bf7df8b0..40510e43 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -19,7 +19,7 @@ public LJDiagnostic(String title, String message, String details, SourcePosition this.title = title; this.message = message; this.details = details; - this.file = pos != null ? pos.getFile().getPath() : null; + this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null; this.position = ErrorPosition.fromSpoonPosition(pos); this.accentColor = accentColor; } @@ -44,6 +44,10 @@ public String getFile() { return file; } + public String getAccentColor() { + return accentColor; + } + @Override public String toString() { StringBuilder sb = new StringBuilder(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java deleted file mode 100644 index 1c063fa0..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java +++ /dev/null @@ -1,25 +0,0 @@ -package liquidjava.diagnostics.errors; - -import liquidjava.diagnostics.TranslationTable; -import liquidjava.rj_language.ast.Expression; -import spoon.reflect.cu.SourcePosition; - -/** - * Error indicating that a ghost method invocation is invalid (e.g., has wrong arguments) - * - * @see LJError - */ -public class GhostInvocationError extends LJError { - - private final String expected; - - public GhostInvocationError(String message, SourcePosition pos, Expression expected, - TranslationTable translationTable) { - super("Ghost Invocation Error", message, "", pos, translationTable); - this.expected = expected.toSimplifiedString(); - } - - public String getExpected() { - return expected; - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java index 9af41e49..cc056441 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -1,6 +1,7 @@ package liquidjava.diagnostics.errors; import liquidjava.diagnostics.TranslationTable; +import liquidjava.utils.Utils; import spoon.reflect.declaration.CtElement; /** @@ -9,8 +10,15 @@ * @see LJError */ public class NotFoundError extends LJError { + + private final String name; - public NotFoundError(CtElement element, String message, TranslationTable translationTable) { + public NotFoundError(CtElement element, String message, String name, TranslationTable translationTable) { super("Not Found Error", message, "", element.getPosition(), translationTable); + this.name = Utils.getSimpleName(name); + } + + public String getName() { + return name; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java index 1fe85155..34d8c430 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -11,22 +11,16 @@ */ public class StateConflictError extends LJError { - private final String state; - private final String className; + private final String state;; - public StateConflictError(CtElement element, Expression state, String className, + public StateConflictError(CtElement element, Expression state, TranslationTable translationTable) { super("State Conflict Error", "Found multiple disjoint states in state transition", "State transition can only go to one state of each state set", element.getPosition(), translationTable); this.state = state.toSimplifiedString(); - this.className = className; } public String getState() { return state; } - - public String getClassName() { - return className; - } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index 013c64d2..09ae6ec8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -1,7 +1,5 @@ package liquidjava.diagnostics.errors; -import java.util.Arrays; - import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.ast.Expression; import spoon.reflect.declaration.CtElement; @@ -13,28 +11,18 @@ */ public class StateRefinementError extends LJError { - private final String method; - private final String[] expected; + private final String expected; private final String found; - public StateRefinementError(CtElement element, String method, Expression[] expected, Expression found, + public StateRefinementError(CtElement element, Expression expected, Expression found, TranslationTable translationTable) { - super("State Refinement Error", "State refinement transition violation", - String.format("Expected: %s\nFound: %s", - String.join(", ", - Arrays.stream(expected).map(Expression::toSimplifiedString).toArray(String[]::new)), - found.toSimplifiedString()), + super("State Refinement Error", String.format("Expected state '%s' but found '%s'", expected.toSimplifiedString(), found.toSimplifiedString()), null, element.getPosition(), translationTable); - this.method = method; - this.expected = Arrays.stream(expected).map(Expression::toSimplifiedString).toArray(String[]::new); + this.expected = expected.toSimplifiedString(); this.found = found.toSimplifiedString(); } - public String getMethod() { - return method; - } - - public String[] getExpected() { + public String getExpected() { return expected; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 3b044848..504f43fb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -303,7 +303,7 @@ public void createSameStateError(CtElement element, Predicate expectedType, Stri vcChecker.raiseSameStateError(element, expectedType, klass); } - public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate[] expected) + public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate expected) throws LJError { vcChecker.raiseStateMismatchError(element, method, found, expected); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 3636ff93..7085e20c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -9,7 +9,6 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.errors.CustomError; -import liquidjava.diagnostics.errors.GhostInvocationError; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.diagnostics.TranslationTable; @@ -225,14 +224,14 @@ public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition new SMTEvaluator().verifySubtype(found, expectedType, context); } catch (TypeCheckError e) { return false; - } catch (Exception e) { + } + //TODO: handle NotFoundError properly + catch (Exception e) { String msg = e.getLocalizedMessage().toLowerCase(); if (msg.contains("wrong number of arguments")) { - throw new GhostInvocationError("Wrong number of arguments in ghost invocation", p, - expectedType.getExpression(), null); + throw new CustomError("Wrong number of arguments in ghost invocation", p); } else if (msg.contains("sort mismatch")) { - throw new GhostInvocationError("Type mismatch in arguments of ghost invocation", p, - expectedType.getExpression(), null); + throw new CustomError("Type mismatch in arguments of ghost invocation", p); } else { throw new CustomError(e.getMessage(), p); } @@ -286,28 +285,28 @@ protected void raiseSubtypingError(CtElement element, Predicate expectedType, Pr public void raiseSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError { TranslationTable map = createMap(expectedType); - throw new StateConflictError(element, expectedType.getExpression(), klass, map); + throw new StateConflictError(element, expectedType.getExpression(), map); } private void raiseError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, TranslationTable map) throws LJError { if (e instanceof TypeCheckError) { throw new RefinementError(element, expectedType.getExpression(), premisesBeforeChange.simplify(), map); - } else if (e instanceof liquidjava.smt.errors.NotFoundError) { - throw new NotFoundError(element, e.getMessage(), map); + } else if (e instanceof liquidjava.smt.errors.NotFoundError nfe) { + throw new NotFoundError(element, e.getMessage(), nfe.getName(), map); } else { throw new CustomError(e.getMessage(), element); } } - public void raiseStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states) + public void raiseStateMismatchError(CtElement element, String method, Predicate found, Predicate expected) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); VCImplication foundState = joinPredicates(found, mainVars, lrv, map); - throw new StateRefinementError(element, method, - Arrays.stream(states).map(Predicate::getExpression).toArray(Expression[]::new), + throw new StateRefinementError(element, + expected.getExpression(), foundState.toConjunctions().simplify().getValue(), map); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 44164419..744aa097 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -406,8 +406,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L .changeOldMentions(vi.getName(), instanceName); if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition - Predicate[] states = { stateChange.getFrom() }; - tc.createStateMismatchError(fw, fw.toString(), prevState, states); + tc.createStateMismatchError(fw, fw.toString(), prevState, stateChange.getFrom()); return; } @@ -486,10 +485,10 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List makeBooleanLiteral(boolean value) { private Expr getVariableTranslation(String name) throws Exception { if (!varTranslation.containsKey(name)) - throw new NotFoundError("Variable '" + name + "' not found"); + throw new NotFoundError("Variable '" + name + "' not found", name); Expr e = varTranslation.get(name); if (e == null) e = varTranslation.get(String.format("this#%s", name)); @@ -133,7 +133,7 @@ private FuncDecl resolveFunctionDeclFallback(String name, Expr[] params) t if (candidate != null) { return candidate; } - throw new NotFoundError("Function '" + name + "' not found"); + throw new NotFoundError("Ghost '" + name + "' not found", name); } @SuppressWarnings({ "unchecked", "rawtypes" }) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java index 5c163808..fcbfe96b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java @@ -2,7 +2,14 @@ public class NotFoundError extends SMTError { - public NotFoundError(String message) { + private final String name; + + public NotFoundError(String message, String name) { super(message); + this.name = name; + } + + public String getName() { + return name; } } From c9c22e9a5756d3f238f8fd601ba3c6b6713a054c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Wed, 19 Nov 2025 16:18:54 +0000 Subject: [PATCH 2/6] Refactor Errors --- .../liquidjava/diagnostics/LJDiagnostic.java | 4 +- .../diagnostics/errors/CustomError.java | 13 +-- .../errors/InvalidRefinementError.java | 6 +- .../diagnostics/errors/NotFoundError.java | 15 +++- .../diagnostics/errors/RefinementError.java | 6 +- .../errors/StateConflictError.java | 7 +- .../errors/StateRefinementError.java | 8 +- .../refinement_checker/TypeChecker.java | 25 +++--- .../refinement_checker/VCChecker.java | 80 +++++++++---------- .../AuxHierarchyRefinementsPassage.java | 2 +- .../object_checkers/AuxStateHandler.java | 15 ++-- .../liquidjava/rj_language/Predicate.java | 12 ++- .../java/liquidjava/smt/TranslatorToZ3.java | 5 +- .../liquidjava/smt/errors/NotFoundError.java | 10 ++- .../java/liquidjava/utils/constants/Keys.java | 2 + 15 files changed, 112 insertions(+), 98 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 40510e43..25f392ac 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -53,8 +53,8 @@ public String toString() { StringBuilder sb = new StringBuilder(); // title - sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET) - .append(message.toLowerCase()).append("\n"); + sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message) + .append("\n"); // snippet String snippet = getSnippet(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java index b9a5baca..c8d20316 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -1,7 +1,6 @@ package liquidjava.diagnostics.errors; import spoon.reflect.cu.SourcePosition; -import spoon.reflect.declaration.CtElement; /** * Custom error with an arbitrary message @@ -14,15 +13,11 @@ public CustomError(String message) { super("Error", message, null, null, null); } - public CustomError(String message, SourcePosition pos) { - super("Error", message, null, pos, null); + public CustomError(String message, SourcePosition position) { + super("Error", message, null, position, null); } - public CustomError(String message, String detail, CtElement element) { - super("Error", message, detail, element.getPosition(), null); - } - - public CustomError(String message, CtElement element) { - super("Error", message, null, element.getPosition(), null); + public CustomError(String message, SourcePosition position, String detail) { + super("Error", message, detail, position, null); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java index c94ef1ff..a0b274f0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java @@ -1,6 +1,6 @@ package liquidjava.diagnostics.errors; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Error indicating that a refinement is invalid (e.g., not a boolean expression) @@ -11,8 +11,8 @@ public class InvalidRefinementError extends LJError { private final String refinement; - public InvalidRefinementError(CtElement element, String message, String refinement) { - super("Invalid Refinement", message, "", element.getPosition(), null); + public InvalidRefinementError(SourcePosition position, String message, String refinement) { + super("Invalid Refinement", message, "", position, null); this.refinement = refinement; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java index cc056441..2be789c6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -2,7 +2,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.utils.Utils; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Error indicating that an element referenced in a refinement was not found @@ -10,15 +10,22 @@ * @see LJError */ public class NotFoundError extends LJError { - + private final String name; + private final String kind; // "Variable" or "Ghost" - public NotFoundError(CtElement element, String message, String name, TranslationTable translationTable) { - super("Not Found Error", message, "", element.getPosition(), translationTable); + public NotFoundError(SourcePosition position, String message, String name, String kind, + TranslationTable translationTable) { + super("Not Found Error", message, "", position, translationTable); this.name = Utils.getSimpleName(name); + this.kind = kind; } public String getName() { return name; } + + public String getKind() { + return kind; + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 87fd76e9..0e85d20c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -3,7 +3,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Error indicating that a refinement constraint either was violated or cannot be proven @@ -15,11 +15,11 @@ public class RefinementError extends LJError { private final String expected; private final ValDerivationNode found; - public RefinementError(CtElement element, Expression expected, ValDerivationNode found, + public RefinementError(SourcePosition position, Expression expected, ValDerivationNode found, TranslationTable translationTable) { super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), "", - element.getPosition(), translationTable); + position, translationTable); this.expected = expected.toSimplifiedString(); this.found = found; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java index 34d8c430..443dd5bf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -2,7 +2,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.ast.Expression; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Error indicating that two disjoint states were found in a state refinement @@ -13,10 +13,9 @@ public class StateConflictError extends LJError { private final String state;; - public StateConflictError(CtElement element, Expression state, - TranslationTable translationTable) { + public StateConflictError(SourcePosition position, Expression state, TranslationTable translationTable) { super("State Conflict Error", "Found multiple disjoint states in state transition", - "State transition can only go to one state of each state set", element.getPosition(), translationTable); + "State transition can only go to one state of each state set", position, translationTable); this.state = state.toSimplifiedString(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index 09ae6ec8..bc3ad21d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -2,7 +2,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.ast.Expression; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Error indicating that a state refinement transition was violated @@ -14,10 +14,10 @@ public class StateRefinementError extends LJError { private final String expected; private final String found; - public StateRefinementError(CtElement element, Expression expected, Expression found, + public StateRefinementError(SourcePosition position, Expression expected, Expression found, TranslationTable translationTable) { - super("State Refinement Error", String.format("Expected state '%s' but found '%s'", expected.toSimplifiedString(), found.toSimplifiedString()), null, - element.getPosition(), translationTable); + super("State Refinement Error", String.format("Expected state %s but found %s", expected.toSimplifiedString(), + found.toSimplifiedString()), null, position, translationTable); this.expected = expected.toSimplifiedString(); this.found = found.toSimplifiedString(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 504f43fb..da0c6b60 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -82,8 +82,8 @@ public Optional getRefinementFromAnnotation(CtElement element) throws // check if refinement is valid if (!p.getExpression().isBooleanExpression()) { - throw new InvalidRefinementError(element, "Refinement predicate must be a boolean expression", - ref.get()); + throw new InvalidRefinementError(element.getPosition(), + "Refinement predicate must be a boolean expression", ref.get()); } constr = Optional.of(p); } @@ -115,7 +115,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th CtLiteral s = (CtLiteral) ce; String f = s.getValue(); if (Character.isUpperCase(f.charAt(0))) { - throw new CustomError("State names must start with lowercase", s); + throw new CustomError("State names must start with lowercase", s.getPosition()); } } } @@ -152,7 +152,8 @@ private void createStateGhost(String string, CtAnnotation GhostDTO gd = RefinementsParser.getGhostDeclaration(string); if (!gd.paramTypes().isEmpty()) { throw new CustomError( - "Ghost States have the class as parameter " + "by default, no other parameters are allowed", ann); + "Ghost States have the class as parameter " + "by default, no other parameters are allowed", + ann.getPosition()); } // Set class as parameter of Ghost String qn = getQualifiedClassName(element); @@ -224,8 +225,8 @@ protected void handleAlias(String value, CtElement element) throws LJError { a.parse(path); // refinement alias must return a boolean expression if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) { - throw new InvalidRefinementError(element, "Refinement alias must return a boolean expression", - value); + throw new InvalidRefinementError(element.getPosition(), + "Refinement alias must return a boolean expression", value); } AliasWrapper aw = new AliasWrapper(a, factory, klass, path); context.addAlias(aw); @@ -295,16 +296,16 @@ public boolean checksStateSMT(Predicate prevState, Predicate expectedState, Sour return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); } - public void createError(CtElement element, Predicate expectedType, Predicate foundType) throws LJError { - vcChecker.raiseSubtypingError(element, expectedType, foundType); + public void createError(SourcePosition position, Predicate expectedType, Predicate foundType) throws LJError { + vcChecker.raiseSubtypingError(position, expectedType, foundType); } - public void createSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError { - vcChecker.raiseSameStateError(element, expectedType, klass); + public void createSameStateError(SourcePosition position, Predicate expectedType, String klass) throws LJError { + vcChecker.raiseSameStateError(position, expectedType, klass); } - public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate expected) + public void createStateMismatchError(SourcePosition position, String method, Predicate found, Predicate expected) throws LJError { - vcChecker.raiseStateMismatchError(element, method, found, expected); + vcChecker.raiseStateMismatchError(position, method, found, expected); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 7085e20c..4cad3a80 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -1,7 +1,6 @@ package liquidjava.processor.refinement_checker; import java.util.ArrayList; -import java.util.Arrays; import java.util.List; import java.util.Set; import java.util.Stack; @@ -18,7 +17,6 @@ import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.ast.Expression; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.errors.TypeCheckError; import liquidjava.utils.constants.Keys; @@ -53,14 +51,14 @@ public void processSubtyping(Predicate expectedType, List list, CtEl premises = premisesBeforeChange.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); } catch (Exception e) { - throw new RefinementError(element, expectedType.getExpression(), premises.simplify(), map); + throw new RefinementError(element.getPosition(), expectedType.getExpression(), premises.simplify(), map); } try { smtChecking(premises, et); } catch (Exception e) { // To emit the message we use the constraints before the alias and state change - raiseError(e, premisesBeforeChange, expectedType, element, map); + raiseError(e, element.getPosition(), premisesBeforeChange, expectedType, map); } } @@ -68,11 +66,11 @@ public void processSubtyping(Predicate type, Predicate expectedType, List list, SourcePosition p, - Factory f) throws LJError { + public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List list, + SourcePosition position, Factory f) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(type, lrv, mainVars); @@ -93,7 +91,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List< } catch (Exception e) { return false; } - return smtChecks(premises, et, p); + return smtChecks(et, premises, position, map); } /** @@ -219,22 +217,14 @@ private void recAuxGetVars(RefinedVariable var, List newVars) { getVariablesFromContext(l, newVars, varName); } - public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition p) throws LJError { + public boolean smtChecks(Predicate expected, Predicate found, SourcePosition position, TranslationTable map) + throws LJError { try { - new SMTEvaluator().verifySubtype(found, expectedType, context); + new SMTEvaluator().verifySubtype(found, expected, context); } catch (TypeCheckError e) { return false; - } - //TODO: handle NotFoundError properly - catch (Exception e) { - String msg = e.getLocalizedMessage().toLowerCase(); - if (msg.contains("wrong number of arguments")) { - throw new CustomError("Wrong number of arguments in ghost invocation", p); - } else if (msg.contains("sort mismatch")) { - throw new CustomError("Type mismatch in arguments of ghost invocation", p); - } else { - throw new CustomError(e.getMessage(), p); - } + } catch (Exception e) { + raiseError(e, position, found, expected, map); } return true; } @@ -274,39 +264,45 @@ private TranslationTable createMap(Predicate expectedType) { return map; } - protected void raiseSubtypingError(CtElement element, Predicate expectedType, Predicate foundType) throws LJError { - List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); - gatherVariables(expectedType, lrv, mainVars); - gatherVariables(foundType, lrv, mainVars); - TranslationTable map = new TranslationTable(); - Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); - throw new RefinementError(element, expectedType.getExpression(), premises.simplify(), map); - } - - public void raiseSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError { - TranslationTable map = createMap(expectedType); - throw new StateConflictError(element, expectedType.getExpression(), map); - } - - private void raiseError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, + protected void raiseError(Exception e, SourcePosition position, Predicate found, Predicate expected, TranslationTable map) throws LJError { if (e instanceof TypeCheckError) { - throw new RefinementError(element, expectedType.getExpression(), premisesBeforeChange.simplify(), map); + throw new RefinementError(position, expected.getExpression(), found.simplify(), map); } else if (e instanceof liquidjava.smt.errors.NotFoundError nfe) { - throw new NotFoundError(element, e.getMessage(), nfe.getName(), map); + throw new NotFoundError(position, e.getMessage(), nfe.getName(), nfe.getKind(), map); } else { - throw new CustomError(e.getMessage(), element); + String msg = e.getLocalizedMessage().toLowerCase(); + if (msg.contains("wrong number of arguments")) { + throw new CustomError("Wrong number of arguments in ghost invocation", position); + } else if (msg.contains("sort mismatch")) { + throw new CustomError("Type mismatch in arguments of ghost invocation", position); + } else { + throw new CustomError(e.getMessage(), position); + } } } - public void raiseStateMismatchError(CtElement element, String method, Predicate found, Predicate expected) + protected void raiseSubtypingError(SourcePosition position, Predicate expected, Predicate found) throws LJError { + List 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.getExpression(), premises.simplify(), map); + } + + protected void raiseSameStateError(SourcePosition position, Predicate expected, String klass) throws LJError { + TranslationTable map = createMap(expected); + throw new StateConflictError(position, expected.getExpression(), map); + } + + protected void raiseStateMismatchError(SourcePosition position, String method, Predicate found, Predicate expected) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); VCImplication foundState = joinPredicates(found, mainVars, lrv, map); - throw new StateRefinementError(element, - expected.getExpression(), + throw new StateRefinementError(position, expected.getExpression(), foundState.toConjunctions().simplify().getValue(), map); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java index 3fe01862..c4d27764 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java +++ b/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.createError(method, argRef, superArgRef); + tc.createError(method.getPosition(), argRef, superArgRef); } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 744aa097..92bfd43d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -65,7 +65,7 @@ private static void setConstructorStates(RefinedFunction f, List r = tc.getFactory().Type().createReference(targetClass); String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); @@ -214,7 +215,7 @@ private static Predicate createStatePredicate(String value, String targetClass, c = c.changeOldMentions(nameOld, name); boolean ok = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition()); if (ok) { - tc.createSameStateError(e, p, targetClass); + tc.createSameStateError(e.getPosition(), p, targetClass); } return c1; } @@ -406,7 +407,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L .changeOldMentions(vi.getName(), instanceName); if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition - tc.createStateMismatchError(fw, fw.toString(), prevState, stateChange.getFrom()); + tc.createStateMismatchError(fw.getPosition(), fw.toString(), prevState, stateChange.getFrom()); return; } @@ -485,10 +486,12 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List makeBooleanLiteral(boolean value) { private Expr getVariableTranslation(String name) throws Exception { if (!varTranslation.containsKey(name)) - throw new NotFoundError("Variable '" + name + "' not found", name); + throw new NotFoundError(Keys.VARIABLE, name); Expr e = varTranslation.get(name); if (e == null) e = varTranslation.get(String.format("this#%s", name)); @@ -133,7 +134,7 @@ private FuncDecl resolveFunctionDeclFallback(String name, Expr[] params) t if (candidate != null) { return candidate; } - throw new NotFoundError("Ghost '" + name + "' not found", name); + throw new NotFoundError(Keys.GHOST, name); } @SuppressWarnings({ "unchecked", "rawtypes" }) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java index fcbfe96b..a6fb544a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java @@ -3,13 +3,19 @@ public class NotFoundError extends SMTError { private final String name; + private final String kind; - public NotFoundError(String message, String name) { - super(message); + public NotFoundError(String kind, String name) { + super(String.format("%s '%s' not found", kind, name)); this.name = name; + this.kind = kind; } public String getName() { return name; } + + public String getKind() { + return kind; + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java index 790845fa..cba8ee40 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java @@ -6,4 +6,6 @@ public final class Keys { public static final String THIS = "this"; public static final String WILDCARD = "_"; public static final String OLD = "old"; + public static final String VARIABLE = "Variable"; + public static final String GHOST = "Ghost"; } \ No newline at end of file From ead256930fc0cdc15155401f474783fdef80ad42 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 20 Nov 2025 11:34:56 +0000 Subject: [PATCH 3/6] Minor Changes --- .../java/liquidjava/diagnostics/errors/CustomError.java | 4 ++-- .../warnings/ExternalClassNotFoundWarning.java | 2 +- .../warnings/ExternalMethodNotFoundWarning.java | 8 +++++++- .../refinement_checker/ExternalRefinementTypeChecker.java | 8 ++++---- 4 files changed, 14 insertions(+), 8 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java index c8d20316..cb7538a2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -17,7 +17,7 @@ public CustomError(String message, SourcePosition position) { super("Error", message, null, position, null); } - public CustomError(String message, SourcePosition position, String detail) { - super("Error", message, detail, position, null); + public CustomError(String message, SourcePosition position, String details) { + super("Error", message, details, position, null); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java index e3d1c239..a4a75ca2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java @@ -12,7 +12,7 @@ public class ExternalClassNotFoundWarning extends LJWarning { private final String className; public ExternalClassNotFoundWarning(CtElement element, String message, String className) { - super(message, "", element.getPosition()); + super(message, null, element.getPosition()); this.className = className; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java index 26ad6f51..22ae9cc4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java @@ -11,12 +11,14 @@ public class ExternalMethodNotFoundWarning extends LJWarning { private final String methodName; private final String className; + private final String[] overloads; public ExternalMethodNotFoundWarning(CtElement element, String message, String details, String methodName, - String className) { + String className, String[] overloads) { super(message, details, element.getPosition()); this.methodName = methodName; this.className = className; + this.overloads = overloads; } public String getMethodName() { @@ -26,4 +28,8 @@ public String getMethodName() { public String getClassName() { return className; } + + public String[] getOverloads() { + return overloads; + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index bfbb8de3..dd775f85 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -74,8 +74,8 @@ public void visitCtMethod(CtMethod method) { String details = overloads.length == 0 ? null : "Available constructors:\n " + String.join("\n ", overloads); - diagnostics.add( - new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), prefix)); + diagnostics.add(new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), + prefix, overloads)); } } else { if (!methodExists(targetType, method)) { @@ -84,8 +84,8 @@ public void visitCtMethod(CtMethod method) { String[] overloads = getOverloads(targetType, method); String details = overloads.length == 0 ? null : "Available overloads:\n " + String.join("\n ", overloads); - diagnostics.add( - new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), prefix)); + diagnostics.add(new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), + prefix, overloads)); return; } } From d243c73f2e8ee0b96d31734d3e789a899c4eb9df Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 20 Nov 2025 11:51:29 +0000 Subject: [PATCH 4/6] Replace Details Field with Method --- .../java/liquidjava/diagnostics/LJDiagnostic.java | 11 ++++------- .../liquidjava/diagnostics/errors/CustomError.java | 8 ++------ .../errors/IllegalConstructorTransitionError.java | 3 +-- .../diagnostics/errors/InvalidRefinementError.java | 2 +- .../java/liquidjava/diagnostics/errors/LJError.java | 4 ++-- .../liquidjava/diagnostics/errors/NotFoundError.java | 2 +- .../diagnostics/errors/RefinementError.java | 2 +- .../diagnostics/errors/StateConflictError.java | 3 +-- .../diagnostics/errors/StateRefinementError.java | 2 +- .../liquidjava/diagnostics/errors/SyntaxError.java | 2 +- .../warnings/ExternalClassNotFoundWarning.java | 2 +- .../warnings/ExternalMethodNotFoundWarning.java | 9 +++++++-- .../liquidjava/diagnostics/warnings/LJWarning.java | 4 ++-- .../ExternalRefinementTypeChecker.java | 9 ++------- 14 files changed, 27 insertions(+), 36 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 25f392ac..7970ca24 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -10,15 +10,13 @@ public class LJDiagnostic extends RuntimeException { private final String title; private final String message; - private final String details; private final String file; private final ErrorPosition position; private final String accentColor; - public LJDiagnostic(String title, String message, String details, SourcePosition pos, String accentColor) { + public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor) { this.title = title; this.message = message; - this.details = details; this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null; this.position = ErrorPosition.fromSpoonPosition(pos); this.accentColor = accentColor; @@ -33,7 +31,7 @@ public String getMessage() { } public String getDetails() { - return details; + return ""; } public ErrorPosition getPosition() { @@ -63,7 +61,8 @@ public String toString() { } // details - if (details != null && !details.isEmpty()) { + String details = getDetails(); + if (!details.isEmpty()) { sb.append(" --> ").append(String.join("\n ", details.split("\n"))).append("\n"); } @@ -128,7 +127,6 @@ public boolean equals(Object obj) { return false; LJDiagnostic other = (LJDiagnostic) obj; return title.equals(other.title) && message.equals(other.message) - && ((details == null && other.details == null) || (details != null && details.equals(other.details))) && ((file == null && other.file == null) || (file != null && file.equals(other.file))) && ((position == null && other.position == null) || (position != null && position.equals(other.position))); @@ -138,7 +136,6 @@ public boolean equals(Object obj) { public int hashCode() { int result = title.hashCode(); result = 31 * result + message.hashCode(); - result = 31 * result + (details != null ? details.hashCode() : 0); result = 31 * result + (file != null ? file.hashCode() : 0); result = 31 * result + (position != null ? position.hashCode() : 0); return result; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java index cb7538a2..94e007f0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -10,14 +10,10 @@ public class CustomError extends LJError { public CustomError(String message) { - super("Error", message, null, null, null); + super("Error", message, null, null); } public CustomError(String message, SourcePosition position) { - super("Error", message, null, position, null); - } - - public CustomError(String message, SourcePosition position, String details) { - super("Error", message, details, position, null); + super("Error", message, position, null); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java index 6ef5f6d7..d0b2b59a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java @@ -10,7 +10,6 @@ public class IllegalConstructorTransitionError extends LJError { public IllegalConstructorTransitionError(CtElement element) { - super("Illegal Constructor Transition Error", "Found constructor with 'from' state", - "Constructor methods should only have a 'to' state", element.getPosition(), null); + super("Illegal Constructor Transition Error", "Found constructor with 'from' state: constructors should only have a 'to' state", element.getPosition(), null); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java index a0b274f0..cc14bacb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java @@ -12,7 +12,7 @@ public class InvalidRefinementError extends LJError { private final String refinement; public InvalidRefinementError(SourcePosition position, String message, String refinement) { - super("Invalid Refinement", message, "", position, null); + super("Invalid Refinement", message, position, null); this.refinement = refinement; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java index 32a4e17d..693911d8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -12,9 +12,9 @@ public abstract class LJError extends LJDiagnostic { private final TranslationTable translationTable; - public LJError(String title, String message, String details, SourcePosition pos, + public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable) { - super(title, message, details, pos, Colors.BOLD_RED); + super(title, message, pos, Colors.BOLD_RED); this.translationTable = translationTable != null ? translationTable : new TranslationTable(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java index 2be789c6..e7973be2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -16,7 +16,7 @@ public class NotFoundError extends LJError { public NotFoundError(SourcePosition position, String message, String name, String kind, TranslationTable translationTable) { - super("Not Found Error", message, "", position, translationTable); + super("Not Found Error", message, position, translationTable); this.name = Utils.getSimpleName(name); this.kind = kind; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 0e85d20c..91da89ea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -18,7 +18,7 @@ public class RefinementError extends LJError { public RefinementError(SourcePosition position, Expression expected, ValDerivationNode found, TranslationTable translationTable) { super("Refinement Error", - String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), "", + String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), position, translationTable); this.expected = expected.toSimplifiedString(); this.found = found; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java index 443dd5bf..3e830f07 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -14,8 +14,7 @@ public class StateConflictError extends LJError { private final String state;; public StateConflictError(SourcePosition position, Expression state, TranslationTable translationTable) { - super("State Conflict Error", "Found multiple disjoint states in state transition", - "State transition can only go to one state of each state set", position, translationTable); + super("State Conflict Error", "Found multiple disjoint states in state transition: state transition can only go to one state of each state set", position, translationTable); this.state = state.toSimplifiedString(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java index bc3ad21d..508e6087 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -17,7 +17,7 @@ public class StateRefinementError extends LJError { public StateRefinementError(SourcePosition position, Expression expected, Expression found, TranslationTable translationTable) { super("State Refinement Error", String.format("Expected state %s but found %s", expected.toSimplifiedString(), - found.toSimplifiedString()), null, position, translationTable); + found.toSimplifiedString()), position, translationTable); this.expected = expected.toSimplifiedString(); this.found = found.toSimplifiedString(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java index 226e6ed5..aac27123 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java @@ -16,7 +16,7 @@ public SyntaxError(String message, String refinement) { } public SyntaxError(String message, SourcePosition pos, String refinement) { - super("Syntax Error", message, "", pos, null); + super("Syntax Error", message, pos, null); this.refinement = refinement; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java index a4a75ca2..86438b6b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java @@ -12,7 +12,7 @@ public class ExternalClassNotFoundWarning extends LJWarning { private final String className; public ExternalClassNotFoundWarning(CtElement element, String message, String className) { - super(message, null, element.getPosition()); + super(message, element.getPosition()); this.className = className; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java index 22ae9cc4..799e8e97 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java @@ -13,9 +13,9 @@ public class ExternalMethodNotFoundWarning extends LJWarning { private final String className; private final String[] overloads; - public ExternalMethodNotFoundWarning(CtElement element, String message, String details, String methodName, + public ExternalMethodNotFoundWarning(CtElement element, String message, String methodName, String className, String[] overloads) { - super(message, details, element.getPosition()); + super(message, element.getPosition()); this.methodName = methodName; this.className = className; this.overloads = overloads; @@ -32,4 +32,9 @@ public String getClassName() { public String[] getOverloads() { return overloads; } + + @Override + public String getDetails() { + return overloads.length > 0 ? String.format("Available overloads:\n %s", String.join("\n ", overloads)) : ""; + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java index 4ad3438a..29d65479 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java @@ -9,7 +9,7 @@ */ public abstract class LJWarning extends LJDiagnostic { - public LJWarning(String message, String details, SourcePosition pos) { - super("Warning", message, details, pos, Colors.BOLD_YELLOW); + public LJWarning(String message, SourcePosition pos) { + super("Warning", message, pos, Colors.BOLD_YELLOW); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index dd775f85..56e57770 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -71,10 +71,7 @@ public void visitCtMethod(CtMethod method) { String message = String.format("Could not find constructor '%s' for '%s'", method.getSignature(), prefix); String[] overloads = getOverloads(targetType, method); - String details = overloads.length == 0 ? null - : "Available constructors:\n " + String.join("\n ", overloads); - - diagnostics.add(new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), + diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix, overloads)); } } else { @@ -82,9 +79,7 @@ public void visitCtMethod(CtMethod method) { String message = String.format("Could not find method '%s %s' for '%s'", method.getType().getSimpleName(), method.getSignature(), prefix); String[] overloads = getOverloads(targetType, method); - String details = overloads.length == 0 ? null - : "Available overloads:\n " + String.join("\n ", overloads); - diagnostics.add(new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), + diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix, overloads)); return; } From d1210a84ac01c8eac62f53ad60b25a1c7f93d56f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 20 Nov 2025 14:42:36 +0000 Subject: [PATCH 5/6] Update Version --- liquidjava-verifier/pom.xml | 2 +- .../errors/IllegalConstructorTransitionError.java | 4 +++- .../main/java/liquidjava/diagnostics/errors/LJError.java | 3 +-- .../liquidjava/diagnostics/errors/RefinementError.java | 4 ++-- .../liquidjava/diagnostics/errors/StateConflictError.java | 4 +++- .../warnings/ExternalMethodNotFoundWarning.java | 4 ++-- .../refinement_checker/ExternalRefinementTypeChecker.java | 8 ++++---- 7 files changed, 16 insertions(+), 13 deletions(-) diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 5ed5521f..2461306e 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -11,7 +11,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.3 + 0.0.4 liquidjava-verifier LiquidJava Verifier https://github.com/liquid-java/liquidjava diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java index d0b2b59a..ac04737d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java @@ -10,6 +10,8 @@ public class IllegalConstructorTransitionError extends LJError { public IllegalConstructorTransitionError(CtElement element) { - super("Illegal Constructor Transition Error", "Found constructor with 'from' state: constructors should only have a 'to' state", element.getPosition(), null); + super("Illegal Constructor Transition Error", + "Found constructor with 'from' state: constructors should only have a 'to' state", + element.getPosition(), null); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java index 693911d8..e3fd5599 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -12,8 +12,7 @@ public abstract class LJError extends LJDiagnostic { private final TranslationTable translationTable; - public LJError(String title, String message, SourcePosition pos, - TranslationTable translationTable) { + public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable) { super(title, message, pos, Colors.BOLD_RED); this.translationTable = translationTable != null ? translationTable : new TranslationTable(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 91da89ea..a2c13c91 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -18,8 +18,8 @@ public class RefinementError extends LJError { public RefinementError(SourcePosition position, Expression expected, ValDerivationNode found, TranslationTable translationTable) { super("Refinement Error", - String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), - position, translationTable); + String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), position, + translationTable); this.expected = expected.toSimplifiedString(); this.found = found; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java index 3e830f07..f1cd7c1c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -14,7 +14,9 @@ public class StateConflictError extends LJError { private final String state;; public StateConflictError(SourcePosition position, Expression state, TranslationTable translationTable) { - super("State Conflict Error", "Found multiple disjoint states in state transition: state transition can only go to one state of each state set", position, translationTable); + super("State Conflict Error", + "Found multiple disjoint states in state transition: state transition can only go to one state of each state set", + position, translationTable); this.state = state.toSimplifiedString(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java index 799e8e97..60f20f17 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java @@ -13,8 +13,8 @@ public class ExternalMethodNotFoundWarning extends LJWarning { private final String className; private final String[] overloads; - public ExternalMethodNotFoundWarning(CtElement element, String message, String methodName, - String className, String[] overloads) { + public ExternalMethodNotFoundWarning(CtElement element, String message, String methodName, String className, + String[] overloads) { super(message, element.getPosition()); this.methodName = methodName; this.className = className; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 56e57770..a52ac891 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -71,16 +71,16 @@ public void visitCtMethod(CtMethod method) { String message = String.format("Could not find constructor '%s' for '%s'", method.getSignature(), prefix); String[] overloads = getOverloads(targetType, method); - diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(), - prefix, overloads)); + diagnostics.add( + new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix, overloads)); } } else { if (!methodExists(targetType, method)) { String message = String.format("Could not find method '%s %s' for '%s'", method.getType().getSimpleName(), method.getSignature(), prefix); String[] overloads = getOverloads(targetType, method); - diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(), - prefix, overloads)); + diagnostics.add( + new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix, overloads)); return; } } From f2b8c219b0c637e0ab42dca92e6c63d90402dd23 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 20 Nov 2025 16:51:40 +0000 Subject: [PATCH 6/6] Add Comment --- .../src/main/java/liquidjava/diagnostics/LJDiagnostic.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 7970ca24..88818dd8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -31,7 +31,7 @@ public String getMessage() { } public String getDetails() { - return ""; + return ""; // to be overridden by subclasses } public ErrorPosition getPosition() {