From b76c9a86afd8e2342975e70365bdc8669fe9ae4e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 9 Nov 2025 15:56:27 +0000 Subject: [PATCH 01/12] Code Refactoring --- .../liquidjava/diagnostics/errors/StateConflictError.java | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) 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 1f714cb2..23ac0812 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -14,9 +14,7 @@ public class StateConflictError extends LJError { private String className; public StateConflictError(CtElement element, Predicate predicate, String className) { - super("State Conflict Error", - "Found multiple disjoint states in state transition — State transition can only go to one state of each state set", - element); + super("State Conflict Error", "Found multiple disjoint states in state transition", element); this.predicate = predicate; this.className = className; } From 647d873b64f697deb1ad7bf1d27e594d56f8c7e9 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 10 Nov 2025 15:27:32 +0000 Subject: [PATCH 02/12] Requested Changes --- .../liquidjava/diagnostics/errors/StateConflictError.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 23ac0812..1f714cb2 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 String className; public StateConflictError(CtElement element, Predicate predicate, String className) { - super("State Conflict Error", "Found multiple disjoint states in state transition", element); + super("State Conflict Error", + "Found multiple disjoint states in state transition — State transition can only go to one state of each state set", + element); this.predicate = predicate; this.className = className; } From aa102bc14de6ece6ea495dde39ba78ac3399b622 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 9 Nov 2025 20:42:25 +0000 Subject: [PATCH 03/12] Refactor LJDiagnostics --- .../liquidjava/diagnostics/LJDiagnostics.java | 46 ++----------------- .../diagnostics/errors/LJError.java | 13 ++++++ 2 files changed, 17 insertions(+), 42 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java index 02a6d315..b5473a53 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java @@ -1,67 +1,34 @@ package liquidjava.diagnostics; import java.util.ArrayList; -import java.util.HashMap; - import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.warnings.LJWarning; -import liquidjava.processor.context.PlacementInCode; /** - * Singleton class to store diagnostics information (errors, warnings, translation map) during the verification process + * Singleton class to store diagnostics (errors and warnings) during the verification process * * @see LJError * @see LJWarning */ public class LJDiagnostics { - private static LJDiagnostics instance; + public static final LJDiagnostics diagnostics = new LJDiagnostics(); private ArrayList errors; private ArrayList warnings; - private HashMap translationMap; private LJDiagnostics() { this.errors = new ArrayList<>(); this.warnings = new ArrayList<>(); - this.translationMap = new HashMap<>(); - } - - public static LJDiagnostics getInstance() { - if (instance == null) - instance = new LJDiagnostics(); - return instance; - } - - public static LJDiagnostics add(LJError error) { - LJDiagnostics instance = getInstance(); - instance.addError(error); - return instance; - } - - public static LJDiagnostics add(LJWarning warning) { - LJDiagnostics instance = getInstance(); - instance.addWarning(warning); - return instance; } - public static LJDiagnostics add(HashMap map) { - LJDiagnostics instance = getInstance(); - instance.setTranslationMap(map); - return instance; - } - - public void addError(LJError error) { + public void add(LJError error) { this.errors.add(error); } - public void addWarning(LJWarning warning) { + public void add(LJWarning warning) { this.warnings.add(warning); } - public void setTranslationMap(HashMap map) { - this.translationMap = map; - } - public boolean foundError() { return !this.errors.isEmpty(); } @@ -78,10 +45,6 @@ public ArrayList getWarnings() { return this.warnings; } - public HashMap getTranslationMap() { - return this.translationMap; - } - public LJError getError() { return foundError() ? this.errors.get(0) : null; } @@ -93,7 +56,6 @@ public LJWarning getWarning() { public void clear() { this.errors.clear(); this.warnings.clear(); - this.translationMap.clear(); } @Override 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 6e92057f..986cd878 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -1,6 +1,9 @@ package liquidjava.diagnostics.errors; +import java.util.HashMap; + import liquidjava.diagnostics.ErrorPosition; +import liquidjava.processor.context.PlacementInCode; import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; @@ -15,12 +18,14 @@ public abstract class LJError extends Exception { private CtElement element; private ErrorPosition position; private SourcePosition location; + private HashMap translationTable; public LJError(String title, String message, CtElement element) { super(message); this.title = title; this.message = message; this.element = element; + this.translationTable = new HashMap<>(); try { this.location = element.getPosition(); this.position = ErrorPosition.fromSpoonPosition(element.getPosition()); @@ -50,6 +55,14 @@ public SourcePosition getLocation() { return location; } + public HashMap getTranslationTable() { + return translationTable; + } + + public void setTranslationTable(HashMap translationTable) { + this.translationTable = translationTable; + } + @Override public abstract String toString(); From 35c0addde2ef6c1ca1d07e8f1d3b1f7f775b5326 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 9 Nov 2025 20:53:56 +0000 Subject: [PATCH 04/12] Use Strings in Error Classes `CtElement` will also need to be replaced at some point --- .../diagnostics/errors/GhostInvocationError.java | 9 ++++----- .../diagnostics/errors/RefinementError.java | 15 +++++++++++---- .../diagnostics/errors/StateConflictError.java | 12 +++++------- 3 files changed, 20 insertions(+), 16 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java index 7d04e28d..bcd1c32e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java @@ -1,6 +1,5 @@ package liquidjava.diagnostics.errors; -import liquidjava.rj_language.Predicate; import spoon.reflect.declaration.CtElement; /** @@ -10,21 +9,21 @@ */ public class GhostInvocationError extends LJError { - private Predicate expected; + private String expected; - public GhostInvocationError(CtElement element, Predicate expected) { + public GhostInvocationError(CtElement element, String expected) { super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element); this.expected = expected; } - public Predicate getExpected() { + public String getExpected() { return expected; } @Override public String toString() { StringBuilder sb = new StringBuilder(); - sb.append("Expected: ").append(expected.toString()).append("\n"); + sb.append("Expected: ").append(expected).append("\n"); return super.toString(sb.toString()); } } 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 fc4b31f1..838f6c8e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,6 +1,5 @@ package liquidjava.diagnostics.errors; -import liquidjava.rj_language.Predicate; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.utils.Utils; import spoon.reflect.declaration.CtElement; @@ -12,19 +11,27 @@ */ public class RefinementError extends LJError { - private Predicate expected; + private String expected; private ValDerivationNode found; - public RefinementError(CtElement element, Predicate expected, ValDerivationNode found) { + public RefinementError(CtElement element, String expected, ValDerivationNode found) { super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element); this.expected = expected; this.found = found; } + public String getExpected() { + return expected; + } + + public ValDerivationNode getFound() { + return found; + } + @Override public String toString() { StringBuilder sb = new StringBuilder(); - sb.append("Expected: ").append(Utils.stripParens(expected.toString())).append("\n"); + sb.append("Expected: ").append(Utils.stripParens(expected)).append("\n"); sb.append("Found: ").append(found.getValue()); return super.toString(sb.toString()); } 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 1f714cb2..984d8593 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -1,6 +1,5 @@ package liquidjava.diagnostics.errors; -import liquidjava.rj_language.Predicate; import spoon.reflect.declaration.CtElement; /** @@ -10,19 +9,19 @@ */ public class StateConflictError extends LJError { - private Predicate predicate; + private String state; private String className; - public StateConflictError(CtElement element, Predicate predicate, String className) { + public StateConflictError(CtElement element, String state, String className) { super("State Conflict Error", "Found multiple disjoint states in state transition — State transition can only go to one state of each state set", element); - this.predicate = predicate; + this.state = state; this.className = className; } - public Predicate getPredicate() { - return predicate; + public String getState() { + return state; } public String getClassName() { @@ -33,7 +32,6 @@ public String getClassName() { public String toString() { StringBuilder sb = new StringBuilder(); sb.append("Class: ").append(className).append("\n"); - sb.append("Predicate: ").append(predicate.toString()); return super.toString(sb.toString()); } } From a0153c7d1d7cf71f27aff02cab4cf131a989fbea Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 9 Nov 2025 21:21:40 +0000 Subject: [PATCH 05/12] Modify Errors to Use TranslationTable --- .../liquidjava/diagnostics/ErrorHandler.java | 46 +++++++++---------- .../diagnostics/TranslationTable.java | 17 +++++++ .../diagnostics/errors/CustomError.java | 2 +- .../errors/GhostInvocationError.java | 6 ++- .../IllegalConstructorTransitionError.java | 2 +- .../errors/InvalidRefinementError.java | 6 ++- .../diagnostics/errors/LJError.java | 16 ++----- .../diagnostics/errors/NotFoundError.java | 5 +- .../diagnostics/errors/RefinementError.java | 7 ++- .../errors/StateConflictError.java | 6 ++- .../errors/StateRefinementError.java | 6 ++- .../diagnostics/errors/SyntaxError.java | 2 +- .../refinement_checker/TypeChecker.java | 4 +- .../refinement_checker/VCChecker.java | 39 ++++++++++------ .../object_checkers/AuxStateHandler.java | 7 ++- 15 files changed, 103 insertions(+), 68 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/TranslationTable.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java index 39452f90..4c219274 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java @@ -12,29 +12,29 @@ public class ErrorHandler { - public static void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT, - HashMap map, ErrorEmitter ee) { - String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" + - // cSMT.toString(); - - StringBuilder sb = new StringBuilder(); - sb.append("______________________________________________________\n"); - // title - StringBuilder sbtitle = new StringBuilder(); - sbtitle.append("Failed to check refinement at: \n\n"); - if (moreInfo != null) - sbtitle.append(moreInfo + "\n"); - sbtitle.append(var.toString()); - // all message - sb.append(sbtitle.toString() + "\n\n"); - sb.append("Type expected:" + expectedType.toString() + "\n"); - sb.append("Refinement found: " + cSMT.simplify().getValue() + "\n"); - sb.append(printMap(map)); - sb.append("Location: " + var.getPosition() + "\n"); - sb.append("______________________________________________________\n"); - - ee.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map); - } + // public static void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT, + // HashMap map, ErrorEmitter ee) { + // String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" + + // // cSMT.toString(); + + // StringBuilder sb = new StringBuilder(); + // sb.append("______________________________________________________\n"); + // // title + // StringBuilder sbtitle = new StringBuilder(); + // sbtitle.append("Failed to check refinement at: \n\n"); + // if (moreInfo != null) + // sbtitle.append(moreInfo + "\n"); + // sbtitle.append(var.toString()); + // // all message + // sb.append(sbtitle.toString() + "\n\n"); + // sb.append("Type expected:" + expectedType.toString() + "\n"); + // sb.append("Refinement found: " + cSMT.simplify().getValue() + "\n"); + // sb.append(printMap(map)); + // sb.append("Location: " + var.getPosition() + "\n"); + // sb.append("______________________________________________________\n"); + + // ee.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map); + // } public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg, String states, HashMap map, ErrorEmitter ee) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/TranslationTable.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/TranslationTable.java new file mode 100644 index 00000000..01f96c77 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/TranslationTable.java @@ -0,0 +1,17 @@ +package liquidjava.diagnostics; + +import java.util.HashMap; + +import liquidjava.processor.context.PlacementInCode; + +/** + * Translation table mapping variable names to their placement in code + * + * @see HashMap + * @see PlacementInCode + */ +public class TranslationTable extends HashMap { + public TranslationTable() { + super(); + } +} 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 7f885e45..09b497ef 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -8,7 +8,7 @@ public class CustomError extends LJError { public CustomError(String message) { - super("Found Error", message, null); + super("Found Error", message, null, null); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java index bcd1c32e..1aadc528 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java @@ -1,5 +1,6 @@ package liquidjava.diagnostics.errors; +import liquidjava.diagnostics.TranslationTable; import spoon.reflect.declaration.CtElement; /** @@ -11,8 +12,9 @@ public class GhostInvocationError extends LJError { private String expected; - public GhostInvocationError(CtElement element, String expected) { - super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element); + public GhostInvocationError(CtElement element, String expected, TranslationTable translationTable) { + super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element, + translationTable); this.expected = expected; } 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 af5f05c6..8146ccf8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java @@ -11,7 +11,7 @@ public class IllegalConstructorTransitionError extends LJError { public IllegalConstructorTransitionError(CtElement element) { super("Illegal Constructor Transition Error", - "Found constructor with 'from' state (should only have a 'to' state)", element); + "Found constructor with 'from' state (should only have a 'to' state)", element, null); } @Override 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 02b41265..2eb39d68 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java @@ -1,5 +1,6 @@ package liquidjava.diagnostics.errors; +import liquidjava.diagnostics.TranslationTable; import spoon.reflect.declaration.CtElement; /** @@ -11,8 +12,9 @@ public class InvalidRefinementError extends LJError { private String refinement; - public InvalidRefinementError(String message, CtElement element, String refinement) { - super("Invalid Refinement", message, element); + public InvalidRefinementError(String message, CtElement element, String refinement, + TranslationTable translationTable) { + super("Invalid Refinement", message, element, translationTable); 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 986cd878..ea7fe942 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -1,9 +1,7 @@ package liquidjava.diagnostics.errors; -import java.util.HashMap; - import liquidjava.diagnostics.ErrorPosition; -import liquidjava.processor.context.PlacementInCode; +import liquidjava.diagnostics.TranslationTable; import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; @@ -18,14 +16,14 @@ public abstract class LJError extends Exception { private CtElement element; private ErrorPosition position; private SourcePosition location; - private HashMap translationTable; + private TranslationTable translationTable; - public LJError(String title, String message, CtElement element) { + public LJError(String title, String message, CtElement element, TranslationTable translationTable) { super(message); this.title = title; this.message = message; this.element = element; - this.translationTable = new HashMap<>(); + this.translationTable = translationTable != null ? translationTable : new TranslationTable(); try { this.location = element.getPosition(); this.position = ErrorPosition.fromSpoonPosition(element.getPosition()); @@ -55,14 +53,10 @@ public SourcePosition getLocation() { return location; } - public HashMap getTranslationTable() { + public TranslationTable getTranslationTable() { return translationTable; } - public void setTranslationTable(HashMap translationTable) { - this.translationTable = translationTable; - } - @Override public abstract String toString(); 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 77d1ab1f..5a0f94d0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -1,5 +1,6 @@ package liquidjava.diagnostics.errors; +import liquidjava.diagnostics.TranslationTable; import spoon.reflect.declaration.CtElement; /** @@ -9,8 +10,8 @@ */ public class NotFoundError extends LJError { - public NotFoundError(String message, CtElement element) { - super("Not Found Error", message, element); + public NotFoundError(String message, CtElement element, TranslationTable translationTable) { + super("Not Found Error", message, element, translationTable); } @Override 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 838f6c8e..2ec812a6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,5 +1,6 @@ package liquidjava.diagnostics.errors; +import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.utils.Utils; import spoon.reflect.declaration.CtElement; @@ -14,8 +15,10 @@ public class RefinementError extends LJError { private String expected; private ValDerivationNode found; - public RefinementError(CtElement element, String expected, ValDerivationNode found) { - super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element); + public RefinementError(CtElement element, String expected, ValDerivationNode found, + TranslationTable translationTable) { + super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element, + translationTable); this.expected = expected; 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 984d8593..437f457c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -1,5 +1,6 @@ package liquidjava.diagnostics.errors; +import liquidjava.diagnostics.TranslationTable; import spoon.reflect.declaration.CtElement; /** @@ -12,10 +13,10 @@ public class StateConflictError extends LJError { private String state; private String className; - public StateConflictError(CtElement element, String state, String className) { + public StateConflictError(CtElement element, String state, String className, 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); + element, translationTable); this.state = state; this.className = className; } @@ -32,6 +33,7 @@ public String getClassName() { public String toString() { StringBuilder sb = new StringBuilder(); sb.append("Class: ").append(className).append("\n"); + sb.append("State: ").append(state); return super.toString(sb.toString()); } } 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 5810946d..35ddb1c3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -2,6 +2,7 @@ import java.util.Arrays; +import liquidjava.diagnostics.TranslationTable; import spoon.reflect.declaration.CtElement; /** @@ -15,8 +16,9 @@ public class StateRefinementError extends LJError { private final String[] expected; private final String found; - public StateRefinementError(CtElement element, String method, String[] expected, String found) { - super("State Refinement Error", "State refinement transition violation", element); + public StateRefinementError(CtElement element, String method, String[] expected, String found, + TranslationTable translationTable) { + super("State Refinement Error", "State refinement transition violation", element, translationTable); this.method = method; this.expected = expected; this.found = found; 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 ba679cc6..3c2c424f 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, CtElement element, String refinement) { - super("Syntax Error", message, element); + super("Syntax Error", message, element, null); this.refinement = refinement; } 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 375bff40..c4885d60 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 @@ -326,8 +326,8 @@ public void createSameStateError(CtElement element, Predicate expectedType, Stri vcChecker.printSameStateError(element, expectedType, klass); } - public void createStateMismatchError(CtElement element, String method, Predicate c, String states) { - vcChecker.printStateMismatchError(element, method, c, states); + public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate[] expected) { + vcChecker.printStateMismatchError(element, method, found, expected); } public ErrorEmitter getErrorEmitter() { 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 cba055bc..684a1b67 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,6 +1,9 @@ package liquidjava.processor.refinement_checker; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; + import java.util.ArrayList; +import java.util.Arrays; import java.util.HashMap; import java.util.List; import java.util.Set; @@ -10,6 +13,9 @@ import liquidjava.diagnostics.ErrorEmitter; import liquidjava.diagnostics.ErrorHandler; +import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.errors.RefinementError; +import liquidjava.diagnostics.errors.StateRefinementError; import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; import liquidjava.rj_language.Predicate; @@ -54,7 +60,8 @@ public void processSubtyping(Predicate expectedType, List list, CtEl et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f); } catch (Exception e) { - ErrorHandler.printError(element, e.getMessage(), expectedType, premises, map, errorEmitter); + diagnostics.add(new RefinementError(element, expectedType, premises.simplify())); + // ErrorHandler.printError(element, e.getMessage(), expectedType, premises, map, errorEmitter); return; } @@ -322,7 +329,8 @@ protected void printSubtypingError(CtElement element, Predicate expectedType, Pr HashMap map = new HashMap<>(); Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); - ErrorHandler.printError(element, customeMsg, expectedType, premises, map, errorEmitter); + diagnostics.add(new RefinementError(element, expectedType, premises.simplify())); + // ErrorHandler.printError(element, customeMsg, expectedType, premises, map, errorEmitter); } public void printSameStateError(CtElement element, Predicate expectedType, String klass) { @@ -343,16 +351,17 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e s = "Method invocation " + totalS + " in:"; } - Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map); - Predicate cSMTMessageReady = premisesBeforeChange; // substituteByMap(premisesBeforeChange, map); + // Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map); + // Predicate cSMTMessageReady = premisesBeforeChange; // substituteByMap(premisesBeforeChange, map); if (e instanceof TypeCheckError) { - ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter); + diagnostics.add(new RefinementError(element, expectedType, premisesBeforeChange.simplify())); + // ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter); } else if (e instanceof GhostFunctionError) { - ErrorHandler.printErrorArgs(element, etMessageReady, e.getMessage(), map, errorEmitter); + ErrorHandler.printErrorArgs(element, expectedType, e.getMessage(), map, errorEmitter); } else if (e instanceof TypeMismatchError) { - ErrorHandler.printErrorTypeMismatch(element, etMessageReady, e.getMessage(), map, errorEmitter); + ErrorHandler.printErrorTypeMismatch(element, expectedType, e.getMessage(), map, errorEmitter); } else if (e instanceof NotFoundError) { - ErrorHandler.printNotFound(element, cSMTMessageReady, etMessageReady, e.getMessage(), map, errorEmitter); + ErrorHandler.printNotFound(element, premisesBeforeChange, expectedType, e.getMessage(), map, errorEmitter); } else { ErrorHandler.printCustomError(element, e.getMessage(), errorEmitter); // System.err.println("Unknown error:"+e.getMessage()); @@ -361,12 +370,16 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e } } - public void printStateMismatchError(CtElement element, String method, Predicate c, String states) { + public void printStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); - gatherVariables(c, lrv, mainVars); + gatherVariables(found, lrv, mainVars); HashMap map = new HashMap<>(); - VCImplication constraintForErrorMsg = joinPredicates(c, mainVars, lrv, map); - // HashMap map = createMap(element, c); - ErrorHandler.printStateMismatch(element, method, constraintForErrorMsg, states, map, errorEmitter); + VCImplication foundState = joinPredicates(found, mainVars, lrv, map); + String[] expectedStates = Arrays.stream(states).toArray(String[]::new); + + LJError error = new StateRefinementError(element, method, expectedStates, foundState.toString()); + error.setTranslationTable(map); + diagnostics.add(error); + // ErrorHandler.printStateMismatch(element, method, constraintForErrorMsg, states, map, errorEmitter); } } 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 1d52caa9..a1eafa6a 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 @@ -399,7 +399,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition if (!tc.getErrorEmitter().foundError()) { // No errors in errorEmitter - String states = stateChange.getFrom().toString(); + Predicate[] states = { stateChange.getFrom() }; tc.createStateMismatchError(fw, fw.toString(), prevState, states); } return; @@ -487,9 +487,8 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi, } } if (!found && !tc.getErrorEmitter().foundError()) { // Reaches the end of stateChange no matching states - String states = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom) - .map(Predicate::toString).collect(Collectors.joining(",")); - + Predicate[] states = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom) + .toArray(Predicate[]::new); String simpleInvocation = invocation.toString(); // .getExecutable().toString(); tc.createStateMismatchError(invocation, simpleInvocation, prevState, states); // ErrorPrinter.printStateMismatch(invocation, simpleInvocation, prevState, From fb6d3d5c0d3cb087dd968d75782bbf2e31531a3c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 9 Nov 2025 21:46:23 +0000 Subject: [PATCH 06/12] Update Error Constructors --- .../liquidjava/diagnostics/ErrorEmitter.java | 7 ++-- .../liquidjava/diagnostics/ErrorHandler.java | 18 +++++----- .../errors/GhostInvocationError.java | 5 +-- .../diagnostics/errors/RefinementError.java | 5 +-- .../errors/StateConflictError.java | 9 +++-- .../errors/StateRefinementError.java | 7 ++-- .../refinement_checker/VCChecker.java | 33 +++++++++---------- 7 files changed, 41 insertions(+), 43 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java index 02610343..85bff112 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java @@ -12,13 +12,12 @@ public class ErrorEmitter { private URI filePath; private ErrorPosition position; private int errorStatus; - private HashMap map; + private TranslationTable map; public ErrorEmitter() { } - public void addError(String titleMessage, String msg, SourcePosition p, int errorStatus, - HashMap map) { + public void addError(String titleMessage, String msg, SourcePosition p, int errorStatus, TranslationTable map) { this.titleMessage = titleMessage; fullMessage = msg; try { @@ -86,7 +85,7 @@ public int getErrorStatus() { return errorStatus; } - public HashMap getVCMap() { + public TranslationTable getVCMap() { return map; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java index 4c219274..2d131826 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java @@ -37,7 +37,7 @@ public class ErrorHandler { // } public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg, - String states, HashMap map, ErrorEmitter ee) { + String states, TranslationTable map, ErrorEmitter ee) { String resumeMessage = "Failed to check state transitions. " + "Expected possible states:" + states; // + "; // Found @@ -66,7 +66,7 @@ public static void printStateMismatch(CtElement element, String method, VCImplic } public static void printErrorUnknownVariable(CtElement var, String et, String correctRefinement, - HashMap map, ErrorEmitter ee) { + TranslationTable map, ErrorEmitter ee) { String resumeMessage = "Encountered unknown variable"; @@ -85,7 +85,7 @@ public static void printErrorUnknownVariable(CtElement var, String et, Strin } public static void printNotFound(CtElement var, Predicate constraint, Predicate constraint2, String msg, - HashMap map, ErrorEmitter ee) { + TranslationTable map, ErrorEmitter ee) { StringBuilder sb = new StringBuilder(); sb.append("______________________________________________________\n"); @@ -101,8 +101,8 @@ public static void printNotFound(CtElement var, Predicate constraint, Predic ee.addError(msg, sb.toString(), var.getPosition(), 2, map); } - public static void printErrorArgs(CtElement var, Predicate expectedType, String msg, - HashMap map, ErrorEmitter ee) { + public static void printErrorArgs(CtElement var, Predicate expectedType, String msg, TranslationTable map, + ErrorEmitter ee) { StringBuilder sb = new StringBuilder(); sb.append("______________________________________________________\n"); String title = "Error in ghost invocation: " + msg + "\n"; @@ -116,7 +116,7 @@ public static void printErrorArgs(CtElement var, Predicate expectedType, Str } public static void printErrorTypeMismatch(CtElement element, Predicate expectedType, String message, - HashMap map, ErrorEmitter ee) { + TranslationTable map, ErrorEmitter ee) { StringBuilder sb = new StringBuilder(); sb.append("______________________________________________________\n"); sb.append(message + "\n\n"); @@ -128,8 +128,8 @@ public static void printErrorTypeMismatch(CtElement element, Predicate expectedT ee.addError(message, sb.toString(), element.getPosition(), 2, map); } - public static void printSameStateSetError(CtElement element, Predicate p, String name, - HashMap map, ErrorEmitter ee) { + public static void printSameStateSetError(CtElement element, Predicate p, String name, TranslationTable map, + ErrorEmitter ee) { String resume = "Error found multiple disjoint states from a State Set in a refinement"; StringBuilder sb = new StringBuilder(); @@ -210,7 +210,7 @@ private static String printLine() { return sb.toString(); } - private static String printMap(HashMap map) { + private static String printMap(TranslationTable map) { StringBuilder sb = new StringBuilder(); Formatter formatter = new Formatter(sb, Locale.US); if (map.isEmpty()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java index 1aadc528..3fd4b7a2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java @@ -1,6 +1,7 @@ package liquidjava.diagnostics.errors; import liquidjava.diagnostics.TranslationTable; +import liquidjava.rj_language.Predicate; import spoon.reflect.declaration.CtElement; /** @@ -12,10 +13,10 @@ public class GhostInvocationError extends LJError { private String expected; - public GhostInvocationError(CtElement element, String expected, TranslationTable translationTable) { + public GhostInvocationError(CtElement element, Predicate expected, TranslationTable translationTable) { super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element, translationTable); - this.expected = expected; + this.expected = expected.toString(); } public String getExpected() { 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 2ec812a6..345dac55 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,6 +1,7 @@ package liquidjava.diagnostics.errors; import liquidjava.diagnostics.TranslationTable; +import liquidjava.rj_language.Predicate; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.utils.Utils; import spoon.reflect.declaration.CtElement; @@ -15,11 +16,11 @@ public class RefinementError extends LJError { private String expected; private ValDerivationNode found; - public RefinementError(CtElement element, String expected, ValDerivationNode found, + public RefinementError(CtElement element, Predicate expected, ValDerivationNode found, TranslationTable translationTable) { super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element, translationTable); - this.expected = expected; + this.expected = expected.toString(); 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 437f457c..57c5c05f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -1,6 +1,7 @@ package liquidjava.diagnostics.errors; import liquidjava.diagnostics.TranslationTable; +import liquidjava.rj_language.Predicate; import spoon.reflect.declaration.CtElement; /** @@ -13,11 +14,9 @@ public class StateConflictError extends LJError { private String state; private String className; - public StateConflictError(CtElement element, String state, String className, 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, translationTable); - this.state = state; + public StateConflictError(CtElement element, Predicate state, String className, 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, translationTable); + this.state = state.toString(); this.className = 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 35ddb1c3..aa1f15c3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -3,6 +3,7 @@ import java.util.Arrays; import liquidjava.diagnostics.TranslationTable; +import liquidjava.rj_language.Predicate; import spoon.reflect.declaration.CtElement; /** @@ -16,12 +17,12 @@ public class StateRefinementError extends LJError { private final String[] expected; private final String found; - public StateRefinementError(CtElement element, String method, String[] expected, String found, + public StateRefinementError(CtElement element, String method, Predicate[] expected, Predicate found, TranslationTable translationTable) { super("State Refinement Error", "State refinement transition violation", element, translationTable); this.method = method; - this.expected = expected; - this.found = found; + this.expected = Arrays.stream(expected).map(Predicate::toString).toArray(String[]::new); + this.found = found.toString(); } public String getMethod() { 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 684a1b67..92700903 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 @@ -14,6 +14,7 @@ import liquidjava.diagnostics.ErrorEmitter; import liquidjava.diagnostics.ErrorHandler; import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.errors.RefinementError; import liquidjava.diagnostics.errors.StateRefinementError; import liquidjava.processor.VCImplication; @@ -48,7 +49,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl if (expectedType.isBooleanTrue()) return; - HashMap map = new HashMap<>(); + TranslationTable map = new TranslationTable(); String[] s = { Keys.WILDCARD, Keys.THIS }; Predicate premisesBeforeChange = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); Predicate premises = new Predicate(); @@ -60,7 +61,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f); } catch (Exception e) { - diagnostics.add(new RefinementError(element, expectedType, premises.simplify())); + diagnostics.add(new RefinementError(element, expectedType, premises.simplify(), map)); // ErrorHandler.printError(element, e.getMessage(), expectedType, premises, map, errorEmitter); return; } @@ -89,7 +90,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List< return true; // Predicate premises = joinPredicates(type, element, mainVars, lrv); - HashMap map = new HashMap<>(); + TranslationTable map = new TranslationTable(); String[] s = { Keys.WILDCARD, Keys.THIS }; Predicate premises = new Predicate(); @@ -152,7 +153,7 @@ private List filterGhostStatesForVariables(List list, Li } private VCImplication joinPredicates(Predicate expectedType, List mainVars, - List vars, HashMap map) { + List vars, TranslationTable map) { VCImplication firstSi = null; VCImplication lastSi = null; @@ -192,7 +193,7 @@ private VCImplication joinPredicates(Predicate expectedType, List map) { + private void addMap(RefinedVariable var, TranslationTable map) { map.put(var.getName(), var.getPlacementInCode()); // if(var instanceof VariableInstance) { // VariableInstance vi = (VariableInstance) var; @@ -313,10 +314,10 @@ void removePathVariableThatIncludes(String otherVar) { // Errors--------------------------------------------------------------------------------------------------- - private HashMap createMap(CtElement element, Predicate expectedType) { + private TranslationTable createMap(CtElement element, Predicate expectedType) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); - HashMap map = new HashMap<>(); + TranslationTable map = new TranslationTable(); joinPredicates(expectedType, mainVars, lrv, map); return map; } @@ -326,20 +327,20 @@ protected void printSubtypingError(CtElement element, Predicate expectedType, Pr List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(foundType, lrv, mainVars); - HashMap map = new HashMap<>(); + TranslationTable map = new TranslationTable(); Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); - diagnostics.add(new RefinementError(element, expectedType, premises.simplify())); + diagnostics.add(new RefinementError(element, expectedType, premises.simplify(), map)); // ErrorHandler.printError(element, customeMsg, expectedType, premises, map, errorEmitter); } public void printSameStateError(CtElement element, Predicate expectedType, String klass) { - HashMap map = createMap(element, expectedType); + TranslationTable map = createMap(element, expectedType); ErrorHandler.printSameStateSetError(element, expectedType, klass, map, errorEmitter); } private void printError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, - HashMap map) { + TranslationTable map) { String s = null; if (element instanceof CtInvocation) { CtInvocation ci = (CtInvocation) element; @@ -354,7 +355,7 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e // Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map); // Predicate cSMTMessageReady = premisesBeforeChange; // substituteByMap(premisesBeforeChange, map); if (e instanceof TypeCheckError) { - diagnostics.add(new RefinementError(element, expectedType, premisesBeforeChange.simplify())); + diagnostics.add(new RefinementError(element, expectedType, premisesBeforeChange.simplify(), map)); // ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter); } else if (e instanceof GhostFunctionError) { ErrorHandler.printErrorArgs(element, expectedType, e.getMessage(), map, errorEmitter); @@ -373,13 +374,9 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e public void printStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(found, lrv, mainVars); - HashMap map = new HashMap<>(); + TranslationTable map = new TranslationTable(); VCImplication foundState = joinPredicates(found, mainVars, lrv, map); - String[] expectedStates = Arrays.stream(states).toArray(String[]::new); - - LJError error = new StateRefinementError(element, method, expectedStates, foundState.toString()); - error.setTranslationTable(map); - diagnostics.add(error); + diagnostics.add(new StateRefinementError(element, method, states, foundState.toConjunctions(), map)); // ErrorHandler.printStateMismatch(element, method, constraintForErrorMsg, states, map, errorEmitter); } } From becab3ef77d5c573c87d8e7cd28b6f7fecc5366e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 9 Nov 2025 22:48:40 +0000 Subject: [PATCH 07/12] Remove `ErrorHandler` --- .../liquidjava/diagnostics/ErrorEmitter.java | 2 - .../liquidjava/diagnostics/ErrorHandler.java | 234 ------------------ .../diagnostics/errors/CustomError.java | 6 +- .../errors/InvalidRefinementError.java | 6 +- .../diagnostics/errors/NotFoundError.java | 2 +- .../ExternalClassNotFoundWarning.java | 4 +- .../ExternalMethodNotFoundWarning.java | 4 +- .../ExternalRefinementTypeChecker.java | 62 ++--- .../refinement_checker/TypeChecker.java | 30 +-- .../refinement_checker/VCChecker.java | 65 ++--- .../AuxHierarchyRefinememtsPassage.java | 17 +- .../object_checkers/AuxStateHandler.java | 47 ++-- .../liquidjava/rj_language/Predicate.java | 16 +- ...tFoundError.java => NotFoundSMTError.java} | 4 +- .../java/liquidjava/smt/TranslatorToZ3.java | 4 +- .../liquidjava/smt/TypeMismatchError.java | 23 -- 16 files changed, 112 insertions(+), 414 deletions(-) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java rename liquidjava-verifier/src/main/java/liquidjava/smt/{NotFoundError.java => NotFoundSMTError.java} (78%) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/smt/TypeMismatchError.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java index 85bff112..b938f070 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java @@ -1,8 +1,6 @@ package liquidjava.diagnostics; import java.net.URI; -import java.util.HashMap; -import liquidjava.processor.context.PlacementInCode; import spoon.reflect.cu.SourcePosition; public class ErrorEmitter { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java deleted file mode 100644 index 2d131826..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java +++ /dev/null @@ -1,234 +0,0 @@ -package liquidjava.diagnostics; - -import java.util.Formatter; -import java.util.HashMap; -import java.util.Locale; - -import liquidjava.processor.VCImplication; -import liquidjava.processor.context.PlacementInCode; -import liquidjava.rj_language.Predicate; -import spoon.reflect.code.CtLiteral; -import spoon.reflect.declaration.CtElement; - -public class ErrorHandler { - - // public static void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT, - // HashMap map, ErrorEmitter ee) { - // String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" + - // // cSMT.toString(); - - // StringBuilder sb = new StringBuilder(); - // sb.append("______________________________________________________\n"); - // // title - // StringBuilder sbtitle = new StringBuilder(); - // sbtitle.append("Failed to check refinement at: \n\n"); - // if (moreInfo != null) - // sbtitle.append(moreInfo + "\n"); - // sbtitle.append(var.toString()); - // // all message - // sb.append(sbtitle.toString() + "\n\n"); - // sb.append("Type expected:" + expectedType.toString() + "\n"); - // sb.append("Refinement found: " + cSMT.simplify().getValue() + "\n"); - // sb.append(printMap(map)); - // sb.append("Location: " + var.getPosition() + "\n"); - // sb.append("______________________________________________________\n"); - - // ee.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map); - // } - - public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg, - String states, TranslationTable map, ErrorEmitter ee) { - - String resumeMessage = "Failed to check state transitions. " + "Expected possible states:" + states; // + "; - // Found - // state:"+constraintForErrorMsg.toString() - // ; - - StringBuilder sb = new StringBuilder(); - sb.append("______________________________________________________\n"); - - StringBuilder sbtitle = new StringBuilder(); - sbtitle.append("Failed to check state transitions when calling " + method + " in:\n\n"); - sbtitle.append(element + "\n\n"); - - sb.append(sbtitle.toString()); - sb.append("Expected possible states:" + states + "\n"); - sb.append("\nState found:\n"); - sb.append(printLine()); - sb.append("\n" + constraintForErrorMsg /* .toConjunctions() */.toString() + "\n"); - sb.append(printLine()); - sb.append("\n"); - sb.append(printMap(map)); - sb.append("Location: " + element.getPosition() + "\n"); - sb.append("______________________________________________________\n"); - - ee.addError(resumeMessage, sb.toString(), element.getPosition(), 1, map); - } - - public static void printErrorUnknownVariable(CtElement var, String et, String correctRefinement, - TranslationTable map, ErrorEmitter ee) { - - String resumeMessage = "Encountered unknown variable"; - - StringBuilder sb = new StringBuilder(); - sb.append("______________________________________________________\n"); - StringBuilder sbtitle = new StringBuilder(); - sbtitle.append("Encountered unknown variable\n\n"); - sbtitle.append(var + "\n\n"); - - sb.append(sbtitle.toString()); - sb.append(printMap(map)); - sb.append("Location: " + var.getPosition() + "\n"); - sb.append("______________________________________________________\n"); - - ee.addError(resumeMessage, sb.toString(), var.getPosition(), 2, map); - } - - public static void printNotFound(CtElement var, Predicate constraint, Predicate constraint2, String msg, - TranslationTable map, ErrorEmitter ee) { - - StringBuilder sb = new StringBuilder(); - sb.append("______________________________________________________\n"); - sb.append(msg); - sb.append(constraint + "\n"); - sb.append(constraint2 + "\n\n"); - sb.append("Error found while checking conditions in:\n"); - sb.append(var + "\n\n"); - sb.append(printMap(map)); - sb.append("Location: " + var.getPosition() + "\n"); - sb.append("______________________________________________________\n"); - - ee.addError(msg, sb.toString(), var.getPosition(), 2, map); - } - - public static void printErrorArgs(CtElement var, Predicate expectedType, String msg, TranslationTable map, - ErrorEmitter ee) { - StringBuilder sb = new StringBuilder(); - sb.append("______________________________________________________\n"); - String title = "Error in ghost invocation: " + msg + "\n"; - sb.append(title); - sb.append(var + "\nError in refinement:" + expectedType.toString() + "\n"); - sb.append(printMap(map)); - sb.append("Location: " + var.getPosition() + "\n"); - sb.append("______________________________________________________\n"); - - ee.addError(title, sb.toString(), var.getPosition(), 2, map); - } - - public static void printErrorTypeMismatch(CtElement element, Predicate expectedType, String message, - TranslationTable map, ErrorEmitter ee) { - StringBuilder sb = new StringBuilder(); - sb.append("______________________________________________________\n"); - sb.append(message + "\n\n"); - sb.append(element + "\n"); - sb.append(printMap(map)); - sb.append("Location: " + element.getPosition() + "\n"); - sb.append("______________________________________________________\n"); - - ee.addError(message, sb.toString(), element.getPosition(), 2, map); - } - - public static void printSameStateSetError(CtElement element, Predicate p, String name, TranslationTable map, - ErrorEmitter ee) { - String resume = "Error found multiple disjoint states from a State Set in a refinement"; - - StringBuilder sb = new StringBuilder(); - sb.append("______________________________________________________\n"); - StringBuilder sbtitle = new StringBuilder(); - sbtitle.append("Error found multiple disjoint states from a State Set in a refinement\n\n"); - sbtitle.append(element + "\n\n"); - sb.append(sbtitle.toString()); - sb.append("In predicate:" + p.toString() + "\n"); - sb.append("In class:" + name + "\n"); - sb.append(printMap(map)); - sb.append("Location: " + element.getPosition() + "\n"); - sb.append("______________________________________________________\n"); - - ee.addError(resume, sb.toString(), element.getPosition(), 1, map); - } - - public static void printErrorConstructorFromState(CtElement element, CtLiteral from, ErrorEmitter ee) { - StringBuilder sb = new StringBuilder(); - sb.append("______________________________________________________\n"); - String s = " Error found constructor with FROM state (Constructor's should only have a TO state)\n\n"; - sb.append(s); - sb.append(element + "\n\n"); - sb.append("State found:" + from + "\n"); - sb.append("Location: " + element.getPosition() + "\n"); - sb.append("______________________________________________________\n"); - - ee.addError(s, sb.toString(), element.getPosition(), 1); - } - - public static void printCustomError(CtElement element, String msg, ErrorEmitter ee) { - StringBuilder sb = new StringBuilder(); - sb.append("______________________________________________________\n"); - String s = "Found Error: " + msg; - sb.append(s + "\n\n"); - sb.append(element + "\n\n"); - sb.append("Location: " + element.getPosition() + "\n"); - sb.append("______________________________________________________\n"); - - ee.addError(s, sb.toString(), element.getPosition(), 1); - } - - public static void printSyntaxError(String msg, String ref, CtElement element, ErrorEmitter ee) { - StringBuilder sb = new StringBuilder(); - sb.append("______________________________________________________\n"); - StringBuilder sbtitle = new StringBuilder(); - sbtitle.append("Syntax error with message\n"); - sbtitle.append(msg + "\n"); - sb.append(sbtitle.toString()); - sb.append("Found in refinement:\n"); - sb.append(ref + "\n"); - sb.append("In:\n"); - sb.append(element + "\n"); - sb.append("Location: " + element.getPosition() + "\n"); - sb.append("______________________________________________________\n"); - - ee.addError(sbtitle.toString(), sb.toString(), element.getPosition(), 2); - } - - public static void printSyntaxError(String msg, String ref, ErrorEmitter ee) { - StringBuilder sb = new StringBuilder(); - sb.append("______________________________________________________\n"); - StringBuilder sbtitle = new StringBuilder(); - sbtitle.append("Syntax error with message\n"); - sbtitle.append(msg + "\n"); - sb.append(sbtitle.toString()); - sb.append("Found in refinement:\n"); - sb.append(ref + "\n"); - sb.append("______________________________________________________\n"); - - ee.addError(sbtitle.toString(), sb.toString(), 2); - } - - private static String printLine() { - StringBuilder sb = new StringBuilder(); - for (int i = 0; i < 130; i++) - sb.append("-"); // ----------- - return sb.toString(); - } - - private static String printMap(TranslationTable map) { - StringBuilder sb = new StringBuilder(); - Formatter formatter = new Formatter(sb, Locale.US); - if (map.isEmpty()) { - formatter.close(); - return ""; - } - formatter.format("\nInstance translation table:\n"); - formatter.format(printLine()); - // title - formatter.format("\n| %-32s | %-60s | %-1s \n", "Variable Name", "Created in", "File"); - formatter.format(printLine() + "\n"); - // data - for (String s : map.keySet()) - formatter.format("| %-32s | %-60s | %-1s \n", s, map.get(s).getText(), map.get(s).getSimplePosition()); - // end - formatter.format(printLine() + "\n\n"); - String s = formatter.toString(); - formatter.close(); - return s; - } -} 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 09b497ef..d0c6b971 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -1,5 +1,7 @@ package liquidjava.diagnostics.errors; +import spoon.reflect.declaration.CtElement; + /** * Custom error with an arbitrary message * @@ -7,8 +9,8 @@ */ public class CustomError extends LJError { - public CustomError(String message) { - super("Found Error", message, null, null); + public CustomError(CtElement element, String message) { + super("Found Error", message, element, null); } @Override 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 2eb39d68..bbf95081 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,5 @@ package liquidjava.diagnostics.errors; -import liquidjava.diagnostics.TranslationTable; import spoon.reflect.declaration.CtElement; /** @@ -12,9 +11,8 @@ public class InvalidRefinementError extends LJError { private String refinement; - public InvalidRefinementError(String message, CtElement element, String refinement, - TranslationTable translationTable) { - super("Invalid Refinement", message, element, translationTable); + public InvalidRefinementError(CtElement element, String message, String refinement) { + super("Invalid Refinement", message, element, 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 5a0f94d0..a6ccb1f9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -10,7 +10,7 @@ */ public class NotFoundError extends LJError { - public NotFoundError(String message, CtElement element, TranslationTable translationTable) { + public NotFoundError(CtElement element, String message, TranslationTable translationTable) { super("Not Found Error", message, element, translationTable); } 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 6a4eef29..95f0d121 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java @@ -11,8 +11,8 @@ public class ExternalClassNotFoundWarning extends LJWarning { private String className; - public ExternalClassNotFoundWarning(CtElement element, String className) { - super("Class in external refinement not found", element); + public ExternalClassNotFoundWarning(CtElement element, String message, String className) { + super(message, element); 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 eee01505..6ea00388 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java @@ -12,8 +12,8 @@ public class ExternalMethodNotFoundWarning extends LJWarning { private String methodName; private String className; - public ExternalMethodNotFoundWarning(CtElement element, String methodName, String className) { - super("Method in external refinement not found", element); + public ExternalMethodNotFoundWarning(CtElement element, String message, String methodName, String className) { + super(message, element); 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 8580135b..8d128015 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 @@ -1,12 +1,14 @@ package liquidjava.processor.refinement_checker; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; + import java.util.Arrays; import java.util.List; import java.util.Optional; -import java.util.stream.Collectors; - import liquidjava.diagnostics.ErrorEmitter; -import liquidjava.diagnostics.ErrorHandler; +import liquidjava.diagnostics.errors.CustomError; +import liquidjava.diagnostics.warnings.ExternalClassNotFoundWarning; +import liquidjava.diagnostics.warnings.ExternalMethodNotFoundWarning; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.facade.GhostDTO; @@ -47,7 +49,8 @@ public void visitCtInterface(CtInterface intrface) { if (externalRefinements.isPresent()) { this.prefix = externalRefinements.get(); if (!classExists(prefix)) { - ErrorHandler.printCustomError(intrface, "Could not find class '" + prefix + "'", errorEmitter); + String message = String.format("Could not find external class '%s'", prefix); + diagnostics.add(new ExternalClassNotFoundWarning(intrface, message, prefix)); return; } try { @@ -85,33 +88,21 @@ public void visitCtMethod(CtMethod method) { return; boolean isConstructor = method.getSimpleName().equals(targetType.getSimpleName()); - if (isConstructor) { - if (!constructorExists(targetType, method)) { - ErrorHandler.printCustomError(method, - String.format("Could not find constructor '%s' for '%s'", method.getSignature(), prefix), - errorEmitter); - return; - } - } else { - if (!methodExists(targetType, method)) { - String matchingNames = targetType.getMethods().stream() - .filter(m -> m.getSimpleName().equals(method.getSimpleName())) - .map(m -> String.format("%s %s", m.getType().getSimpleName(), m.getSignature())) - .collect(Collectors.joining("\n ")); - - StringBuilder sb = new StringBuilder(); - sb.append(String.format("Could not find method '%s %s' for '%s'", method.getType().getSimpleName(), - method.getSignature(), prefix)); - - if (!matchingNames.isEmpty()) { - sb.append("\nAvailable overloads:\n "); - sb.append(matchingNames); - } - ErrorHandler.printCustomError(method, sb.toString(), errorEmitter); - return; - } + if (isConstructor && !constructorExists(targetType, method)) { + String title = String.format("Could not find constructor '%s' for '%s'", method.getSignature(), prefix); + String[] overloads = getOverloads(targetType, method); + String message = overloads.length == 0 ? title + : title + "\nAvailable constructors:\n " + String.join("\n ", overloads); + diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix)); + } else if (!methodExists(targetType, method)) { + String title = String.format("Could not find method '%s %s' for '%s'", method.getType().getSimpleName(), + method.getSignature(), prefix); + String[] overloads = getOverloads(targetType, method); + String message = overloads.length == 0 ? title + : title + "\nAvailable overloads:\n " + String.join("\n ", overloads); + diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix)); + return; } - MethodsFunctionsChecker mfc = new MethodsFunctionsChecker(this); try { mfc.getMethodRefinements(method, prefix); @@ -119,9 +110,6 @@ public void visitCtMethod(CtMethod method) { return; } super.visitCtMethod(method); - - // - // System.out.println("visited method external"); } protected void getGhostFunction(String value, CtElement element) { @@ -135,8 +123,7 @@ protected void getGhostFunction(String value, CtElement element) { } } catch (ParsingException e) { - ErrorHandler.printCustomError(element, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter); - // e.printStackTrace(); + diagnostics.add(new CustomError(element, "Could not parse the ghost function" + e.getMessage())); } } @@ -206,4 +193,9 @@ private boolean parametersMatch(List targetParams, List refinementParams) } return true; } + + private String[] getOverloads(CtType targetType, CtMethod method) { + return targetType.getMethods().stream().filter(m -> m.getSimpleName().equals(method.getSimpleName())) + .map(m -> String.format("%s %s", m.getType().getSimpleName(), m.getSignature())).toArray(String[]::new); + } } 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 c4885d60..bc1a008e 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 @@ -1,12 +1,16 @@ package liquidjava.processor.refinement_checker; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; + import java.lang.annotation.Annotation; import java.util.Arrays; import java.util.List; import java.util.Optional; import liquidjava.diagnostics.ErrorEmitter; -import liquidjava.diagnostics.ErrorHandler; +import liquidjava.diagnostics.errors.CustomError; +import liquidjava.diagnostics.errors.InvalidRefinementError; +import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; @@ -83,8 +87,9 @@ public Optional getRefinementFromAnnotation(CtElement element) throws // check if refinement is valid if (!p.getExpression().isBooleanExpression()) { - ErrorHandler.printCustomError(element, "Refinement predicate must be a boolean expression", - errorEmitter); + diagnostics.add(new InvalidRefinementError(element, "Refinement predicate must be a boolean expression", + ref.get())); + return Optional.empty(); } if (errorEmitter.foundError()) return Optional.empty(); @@ -119,8 +124,8 @@ private void createStateSet(CtNewArray e, int set, CtElement element) { CtLiteral s = (CtLiteral) ce; String f = s.getValue(); if (Character.isUpperCase(f.charAt(0))) { - ErrorHandler.printCustomError(s, "State name must start with lowercase in '" + f + "'", - errorEmitter); + diagnostics + .add(new CustomError(s, String.format("State name must start with lowercase in '%s'", f))); } } } @@ -161,12 +166,12 @@ private void createStateGhost(String string, CtAnnotation try { gd = RefinementsParser.getGhostDeclaration(string); } catch (ParsingException e) { - ErrorHandler.printCustomError(ann, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter); + diagnostics.add(new CustomError(ann, "Could not parse the ghost function " + e.getMessage())); return; } if (gd.getParam_types().size() > 0) { - ErrorHandler.printCustomError(ann, "Ghost States have the class as parameter " - + "by default, no other parameters are allowed in '" + string + "'", errorEmitter); + diagnostics.add(new CustomError(ann, "Ghost States have the class as parameter " + + "by default, no other parameters are allowed in '" + string + "'")); return; } // Set class as parameter of Ghost @@ -224,7 +229,7 @@ protected void getGhostFunction(String value, CtElement element) { context.addGhostFunction(gh); } } catch (ParsingException e) { - ErrorHandler.printCustomError(element, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter); + diagnostics.add(new CustomError(element, "Could not parse the ghost function " + e.getMessage())); // e.printStackTrace(); return; } @@ -246,17 +251,14 @@ protected void handleAlias(String value, CtElement element) { a.parse(path); // refinement alias must return a boolean expression if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) { - ErrorHandler.printCustomError(element, "Refinement alias must return a boolean expression", - errorEmitter); + diagnostics.add(new CustomError(element, "Refinement alias must return a boolean expression")); return; } AliasWrapper aw = new AliasWrapper(a, factory, Keys.WILDCARD, context, klass, path); context.addAlias(aw); } } catch (ParsingException e) { - ErrorHandler.printSyntaxError(e.getMessage(), value, element, errorEmitter); - return; - // e.printStackTrace(); + diagnostics.add(new SyntaxError(e.getMessage(), element, value)); } } 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 92700903..e8a54e26 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 @@ -3,8 +3,6 @@ import static liquidjava.diagnostics.LJDiagnostics.diagnostics; import java.util.ArrayList; -import java.util.Arrays; -import java.util.HashMap; import java.util.List; import java.util.Set; import java.util.Stack; @@ -12,21 +10,22 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.ErrorEmitter; -import liquidjava.diagnostics.ErrorHandler; +import liquidjava.diagnostics.errors.CustomError; +import liquidjava.diagnostics.errors.GhostInvocationError; import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.diagnostics.TranslationTable; import liquidjava.diagnostics.errors.RefinementError; +import liquidjava.diagnostics.errors.StateConflictError; import liquidjava.diagnostics.errors.StateRefinementError; import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; import liquidjava.rj_language.Predicate; import liquidjava.smt.GhostFunctionError; -import liquidjava.smt.NotFoundError; +import liquidjava.smt.NotFoundSMTError; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.TypeCheckError; -import liquidjava.smt.TypeMismatchError; import liquidjava.utils.constants.Keys; -import spoon.reflect.code.CtInvocation; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.factory.Factory; @@ -62,7 +61,6 @@ public void processSubtyping(Predicate expectedType, List list, CtEl et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f); } catch (Exception e) { diagnostics.add(new RefinementError(element, expectedType, premises.simplify(), map)); - // ErrorHandler.printError(element, e.getMessage(), expectedType, premises, map, errorEmitter); return; } @@ -103,11 +101,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List< et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f); } catch (Exception e) { return false; - // printError(premises, expectedType, element, map, e.getMessage()); } - - // System.out.println("premise: " + premises.toString() + "\nexpectation: " + - // et.toString()); return smtChecks(premises, et, p); } @@ -195,17 +189,6 @@ private VCImplication joinPredicates(Predicate expectedType, List lrv, List mainVars) { @@ -329,45 +312,30 @@ protected void printSubtypingError(CtElement element, Predicate expectedType, Pr gatherVariables(foundType, lrv, mainVars); TranslationTable map = new TranslationTable(); Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); - diagnostics.add(new RefinementError(element, expectedType, premises.simplify(), map)); - // ErrorHandler.printError(element, customeMsg, expectedType, premises, map, errorEmitter); } public void printSameStateError(CtElement element, Predicate expectedType, String klass) { TranslationTable map = createMap(element, expectedType); - ErrorHandler.printSameStateSetError(element, expectedType, klass, map, errorEmitter); + diagnostics.add(new StateConflictError(element, expectedType, klass, map)); } private void printError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, TranslationTable map) { - String s = null; - if (element instanceof CtInvocation) { - CtInvocation ci = (CtInvocation) element; - String totalS = ci.getExecutable().toString(); - if (ci.getTarget() != null) { - int targetL = ci.getTarget().toString().length(); - totalS = ci.toString().substring(targetL + 1); - } - s = "Method invocation " + totalS + " in:"; - } + LJError error = mapError(e, premisesBeforeChange, expectedType, element, map); + diagnostics.add(error); + } - // Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map); - // Predicate cSMTMessageReady = premisesBeforeChange; // substituteByMap(premisesBeforeChange, map); + private LJError mapError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, + TranslationTable map) { if (e instanceof TypeCheckError) { - diagnostics.add(new RefinementError(element, expectedType, premisesBeforeChange.simplify(), map)); - // ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter); + return new RefinementError(element, expectedType, premisesBeforeChange.simplify(), map); } else if (e instanceof GhostFunctionError) { - ErrorHandler.printErrorArgs(element, expectedType, e.getMessage(), map, errorEmitter); - } else if (e instanceof TypeMismatchError) { - ErrorHandler.printErrorTypeMismatch(element, expectedType, e.getMessage(), map, errorEmitter); - } else if (e instanceof NotFoundError) { - ErrorHandler.printNotFound(element, premisesBeforeChange, expectedType, e.getMessage(), map, errorEmitter); + return new GhostInvocationError(element, expectedType, map); + } else if (e instanceof NotFoundSMTError) { + return new NotFoundError(element, e.getMessage(), map); } else { - ErrorHandler.printCustomError(element, e.getMessage(), errorEmitter); - // System.err.println("Unknown error:"+e.getMessage()); - // e.printStackTrace(); - // System.exit(7); + return new CustomError(element, e.getMessage()); } } @@ -377,6 +345,5 @@ public void printStateMismatchError(CtElement element, String method, Predicate TranslationTable map = new TranslationTable(); VCImplication foundState = joinPredicates(found, mainVars, lrv, map); diagnostics.add(new StateRefinementError(element, method, states, foundState.toConjunctions(), map)); - // ErrorHandler.printStateMismatch(element, method, constraintForErrorMsg, states, map, errorEmitter); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java index 04c0c14f..0d2499e5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java @@ -83,7 +83,6 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF } else { boolean f = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition()); if (!f) { - // ErrorPrinter.printError(method, argRef, superArgRef); if (!tc.getErrorEmitter().foundError()) tc.createError(method, argRef, superArgRef, ""); } @@ -100,8 +99,8 @@ static void transferReturnRefinement(RefinedFunction superFunction, RefinedFunct else { String name = String.format(Formats.FRESH, tc.getContext().getCounter()); tc.getContext().addVarToContext(name, superFunction.getType(), new Predicate(), method); - // functionRef might be stronger than superRef -> check (superRef <: - // functionRef) + // functionRef might be stronger than superRef + // check (superRef <: functionRef) functionRef = functionRef.substituteVariable(Keys.WILDCARD, name); superRef = superRef.substituteVariable(Keys.WILDCARD, name); for (String m : super2function.keySet()) @@ -110,10 +109,7 @@ static void transferReturnRefinement(RefinedFunction superFunction, RefinedFunct functionRef = functionRef.substituteVariable(m, super2function.get(m)); tc.checkStateSMT(functionRef, superRef, method, - "Return Refinement of Subclass must be subtype of the Return Refinement of the" + " Superclass"); - // boolean f = tc.checkStateSMT(functionRef, superRef, method); - // if(!f) - // ErrorPrinter.printError(method, superRef, functionRef); + "Return of subclass must be subtype of the return of the superclass"); } } @@ -152,18 +148,13 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi // fromSup <: fromSub <==> fromSup is sub type and fromSub is expectedType tc.checkStateSMT(superConst, subConst, method, "FROM State from Superclass must be subtype of FROM State from Subclass"); - // boolean correct = tc.checkStateSMT(superConst, subConst, method); - // if(!correct) ErrorPrinter.printError(method, subState.getFrom(), - // superState.getFrom()); superConst = matchVariableNames(Keys.THIS, thisName, superState.getTo()); subConst = matchVariableNames(Keys.THIS, thisName, superFunction, subFunction, subState.getTo()); // toSub <: toSup <==> ToSub is sub type and toSup is expectedType tc.checkStateSMT(subConst, superConst, method, "TO State from Subclass must be subtype of TO State from Superclass"); - // boolean correct = tc.checkStateSMT(subConst, superConst, method); - // if(!correct) ErrorPrinter.printError(method, subState.getTo(), - // superState.getTo()); + } } } 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 a1eafa6a..0ea5d336 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 @@ -1,10 +1,14 @@ package liquidjava.processor.refinement_checker.object_checkers; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; + import java.lang.annotation.Annotation; import java.util.*; import java.util.stream.Collectors; -import liquidjava.diagnostics.ErrorHandler; +import liquidjava.diagnostics.errors.CustomError; +import liquidjava.diagnostics.errors.IllegalConstructorTransitionError; +import liquidjava.diagnostics.errors.InvalidRefinementError; import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.processor.refinement_checker.TypeCheckingUtils; @@ -40,7 +44,7 @@ public static void handleConstructorState(CtConstructor c, RefinedFunction f, Map m = a.getAllValues(); CtLiteral from = (CtLiteral) m.get("from"); if (from != null) { - ErrorHandler.printErrorConstructorFromState(c, from, tc.getErrorEmitter()); + diagnostics.add(new IllegalConstructorTransitionError(from)); return; } } @@ -71,8 +75,8 @@ private static void setConstructorStates(RefinedFunction f, List ctAnnota String from = TypeCheckingUtils.getStringFromAnnotation(m.get("from")); String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to")); ObjectState state = new ObjectState(); - if (from != null) { // has From + + // has from + if (from != null) state.setFrom(createStatePredicate(from, f.getTargetClass(), tc, e, false, prefix)); - } - if (to != null) { // has To + + // has to + if (to != null) state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true, prefix)); - } - if (from != null && to == null) // has From but not To -> the state remains the same - { + // has from but not to, state remains the same + if (from != null && to == null) state.setTo(createStatePredicate(from, f.getTargetClass(), tc, e, true, prefix)); - } - if (from == null && to != null) // has To but not From -> enters with true and exists with a specific state - { + + // has to but not from, state enters with true + if (from == null && to != null) state.setFrom(new Predicate()); - } + return state; } @@ -187,8 +193,8 @@ private static Predicate createStatePredicate(String value, /* RefinedFunction f TypeChecker tc, CtElement e, boolean isTo, String prefix) throws ParsingException { Predicate p = new Predicate(value, e, tc.getErrorEmitter(), prefix); if (!p.getExpression().isBooleanExpression()) { - ErrorHandler.printCustomError(e, "State refinement transition must be a boolean expression", - tc.getErrorEmitter()); + diagnostics.add( + new InvalidRefinementError(e, "State refinement transition must be a boolean expression", value)); return new Predicate(); } String t = targetClass; // f.getTargetClass(); @@ -384,12 +390,9 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { stateChange.setFrom(fromPredicate); stateChange.setTo(toPredicate); } catch (ParsingException e) { - ErrorHandler - .printCustomError(fw, - "ParsingException while constructing assignment update for `" + fw + "` in class `" - + fw.getVariable().getDeclaringType() + "` : " + e.getMessage(), - tc.getErrorEmitter()); - + diagnostics.add(new CustomError(field, + String.format("Parsing error while constructing assignment update for `%s` in class `%s` : %s", fw, + field.getDeclaringType().getQualifiedName(), e.getMessage()))); return; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index cb17f5ea..4eb77218 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -1,5 +1,7 @@ package liquidjava.rj_language; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; + import java.util.ArrayList; import java.util.HashMap; import java.util.List; @@ -7,7 +9,7 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.ErrorEmitter; -import liquidjava.diagnostics.ErrorHandler; +import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostState; @@ -88,12 +90,12 @@ public Predicate(Expression e) { exp = e; } - protected Expression parse(String ref, CtElement element, ErrorEmitter e) throws ParsingException { + protected Expression parse(String ref, CtElement element, ErrorEmitter ee) throws ParsingException { try { return RefinementsParser.createAST(ref, prefix); - } catch (ParsingException e1) { - ErrorHandler.printSyntaxError(e1.getMessage(), ref, element, e); - throw e1; + } catch (ParsingException e) { + diagnostics.add(new SyntaxError(e.getMessage(), element, ref)); + throw e; } } @@ -101,9 +103,9 @@ protected Expression innerParse(String ref, ErrorEmitter e, String prefix) { try { return RefinementsParser.createAST(ref, prefix); } catch (ParsingException e1) { - ErrorHandler.printSyntaxError(e1.getMessage(), ref, e); + diagnostics.add(new SyntaxError(e1.getMessage(), ref)); + return null; } - return null; } public Predicate changeAliasToRefinement(Context context, Factory f) throws Exception { diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/NotFoundSMTError.java similarity index 78% rename from liquidjava-verifier/src/main/java/liquidjava/smt/NotFoundError.java rename to liquidjava-verifier/src/main/java/liquidjava/smt/NotFoundSMTError.java index 70a80827..0a23d2af 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/NotFoundSMTError.java @@ -2,10 +2,10 @@ import spoon.reflect.declaration.CtElement; -public class NotFoundError extends Exception { +public class NotFoundSMTError extends Exception { private CtElement location; - public NotFoundError(String message) { + public NotFoundSMTError(String message) { super(message); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index ed0db04e..b508592d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -75,7 +75,7 @@ public Expr makeBooleanLiteral(boolean value) { private Expr getVariableTranslation(String name) throws Exception { if (!varTranslation.containsKey(name)) - throw new NotFoundError("Variable '" + name.toString() + "' not found"); + throw new NotFoundSMTError("Variable '" + name.toString() + "' not found"); Expr e = varTranslation.get(name); if (e == null) e = varTranslation.get(String.format("this#%s", name)); @@ -144,7 +144,7 @@ private FuncDecl resolveFunctionDeclFallback(String name, Expr[] params) t if (candidate != null) { return candidate; } - throw new NotFoundError("Function '" + name + "' not found"); + throw new NotFoundSMTError("Function '" + name + "' not found"); } @SuppressWarnings({ "unchecked", "rawtypes" }) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TypeMismatchError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TypeMismatchError.java deleted file mode 100644 index 4f368874..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TypeMismatchError.java +++ /dev/null @@ -1,23 +0,0 @@ -package liquidjava.smt; - -import spoon.reflect.declaration.CtElement; - -public class TypeMismatchError extends Exception { - - private CtElement location; - - public TypeMismatchError(String message) { - super(message); - } - - public CtElement getLocation() { - return location; - } - - public void setLocation(CtElement location) { - this.location = location; - } - - /** */ - private static final long serialVersionUID = 1L; -} From 298ad2982bb559191f7c48b0b3b1d56aea1930e0 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 10 Nov 2025 11:24:45 +0000 Subject: [PATCH 08/12] Minor Changes --- .../src/main/java/liquidjava/api/CommandLineLauncher.java | 5 ++++- .../java/liquidjava/diagnostics/errors/CustomError.java | 4 ++++ .../liquidjava/processor/refinement_checker/VCChecker.java | 6 +----- 3 files changed, 9 insertions(+), 6 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index dc6aa2b4..4657b71b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -1,10 +1,13 @@ package liquidjava.api; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; + import java.io.File; import java.util.Arrays; import java.util.List; import liquidjava.diagnostics.ErrorEmitter; +import liquidjava.diagnostics.errors.CustomError; import liquidjava.processor.RefinementProcessor; import spoon.Launcher; import spoon.processing.ProcessingManager; @@ -39,7 +42,7 @@ public static ErrorEmitter launch(String... paths) { Launcher launcher = new Launcher(); for (String path : paths) { if (!new File(path).exists()) { - ee.addError("Path not found", "The path " + path + " does not exist", 1); + diagnostics.add(new CustomError("The path " + path + " was not found")); return ee; } launcher.addInputResource(path); 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 d0c6b971..b0fb13d7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -9,6 +9,10 @@ */ public class CustomError extends LJError { + public CustomError(String message) { + super("Found Error", message, null, null); + } + public CustomError(CtElement element, String message) { super("Found Error", message, element, null); } 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 e8a54e26..241c107e 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 @@ -244,11 +244,7 @@ public boolean smtChecks(Predicate cSMT, Predicate expectedType, SourcePosition } catch (TypeCheckError e) { return false; } catch (Exception e) { - // System.err.println("Unknown error:"+e.getMessage()); - // e.printStackTrace(); - // System.exit(7); - // fail(); - errorEmitter.addError("Unknown Error", e.getMessage(), p, 7); + diagnostics.add(new CustomError(e.getMessage())); } return true; } From f762e6f2089a3cdc8e0ee96527472283100d3e59 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 10 Nov 2025 11:29:37 +0000 Subject: [PATCH 09/12] Remove `ErrorEmitter` from `CommandLineLauncher` --- .../liquidjava/api/CommandLineLauncher.java | 33 +++----- .../liquidjava/diagnostics/ErrorEmitter.java | 83 +------------------ 2 files changed, 11 insertions(+), 105 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 4657b71b..0aa4112b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -17,51 +17,38 @@ public class CommandLineLauncher { public static void main(String[] args) { - // String allPath = "C://Regen/test-projects/src/Main.java"; - // In eclipse only needed this:"../liquidjava-example/src/main/java/" - // In VSCode needs: - // "../liquidjava/liquidjava-umbrella/liquidjava-example/src/main/java/liquidjava/test/project"; - if (args.length == 0) { - System.out.println("No input files or directories provided"); + System.out.println("No input paths provided"); System.out.println("\nUsage: ./liquidjava <...paths>"); - System.out.println(" <...paths>: Paths to files or directories to be verified by LiquidJava"); + System.out.println(" <...paths>: Paths to be verified by LiquidJava"); System.out.println( - "\nExample: ./liquidjava liquidjava-example/src/main/java/test/currentlyTesting liquidjava-example/src/main/java/testingInProgress/Account.java"); + "\nExample: ./liquidjava liquidjava-example/src/main/java/test liquidjava-example/src/main/java/testingInProgress/Account.java"); return; } List paths = Arrays.asList(args); - ErrorEmitter ee = launch(paths.toArray(new String[0])); - System.out.println(ee.foundError() ? (ee.getFullMessage()) : ("Correct! Passed Verification.")); + launch(paths.toArray(new String[0])); + System.out.println(diagnostics.foundError() ? diagnostics.toString() : "Correct! Passed Verification."); } - public static ErrorEmitter launch(String... paths) { + public static void launch(String... paths) { System.out.println("Running LiquidJava on: " + Arrays.toString(paths).replaceAll("[\\[\\]]", "")); - ErrorEmitter ee = new ErrorEmitter(); Launcher launcher = new Launcher(); for (String path : paths) { if (!new File(path).exists()) { diagnostics.add(new CustomError("The path " + path + " was not found")); - return ee; + return; } launcher.addInputResource(path); } - launcher.getEnvironment().setNoClasspath(true); - // Get the current classpath from the system - // String classpath = System.getProperty("java.class.path"); - // launcher.getEnvironment().setSourceClasspath(classpath.split(File.pathSeparator)); - - // optional - // launcher.getEnvironment().setSourceClasspath( - // "lib1.jar:lib2.jar".split(":")); + launcher.getEnvironment().setNoClasspath(true); launcher.getEnvironment().setComplianceLevel(8); launcher.run(); final Factory factory = launcher.getFactory(); final ProcessingManager processingManager = new QueueProcessingManager(factory); - final RefinementProcessor processor = new RefinementProcessor(factory, ee); + final RefinementProcessor processor = new RefinementProcessor(factory); processingManager.addProcessor(processor); try { @@ -74,6 +61,6 @@ public static ErrorEmitter launch(String... paths) { throw e; } - return ee; + return; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java index b938f070..21e6028e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java @@ -1,89 +1,8 @@ package liquidjava.diagnostics; -import java.net.URI; -import spoon.reflect.cu.SourcePosition; - public class ErrorEmitter { - private String titleMessage; - private String fullMessage; - private URI filePath; - private ErrorPosition position; - private int errorStatus; - private TranslationTable map; - - public ErrorEmitter() { - } - - public void addError(String titleMessage, String msg, SourcePosition p, int errorStatus, TranslationTable map) { - this.titleMessage = titleMessage; - fullMessage = msg; - try { - position = new ErrorPosition(p.getLine(), p.getColumn(), p.getEndLine(), p.getEndColumn()); - filePath = p.getFile().toURI(); - } catch (Exception ignored) { - fullMessage = "Seems like this error is created in generated part of source code, so no precise" - + " position is provided. " + fullMessage; - position = null; - filePath = null; - } - this.errorStatus = errorStatus; - this.map = map; - } - - public void addError(String titleMessage, String msg, SourcePosition p, int errorStatus) { - this.titleMessage = titleMessage; - fullMessage = msg; - try { - position = new ErrorPosition(p.getLine(), p.getColumn(), p.getEndLine(), p.getEndColumn()); - filePath = p.getFile().toURI(); - } catch (Exception ignored) { - fullMessage = "Seems like this error is created in generated part of source code, so no precise" - + " position is provided. " + fullMessage; - position = null; - filePath = null; - } - this.errorStatus = errorStatus; - } - - public void addError(String titleMessage, String msg, int errorStatus) { - this.titleMessage = titleMessage; - fullMessage = msg; - this.errorStatus = errorStatus; - } - public boolean foundError() { - return fullMessage != null; - } - - public String getTitleMessage() { - return titleMessage; - } - - public String getFullMessage() { - return fullMessage; - } - - public URI getFilePath() { - return filePath; - } - - public void reset() { - fullMessage = null; - position = null; - errorStatus = 0; - map = null; - } - - public ErrorPosition getPosition() { - return position; - } - - public int getErrorStatus() { - return errorStatus; - } - - public TranslationTable getVCMap() { - return map; + return false; } } From d73b53b20247b636b53b92549551de284af3062f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 10 Nov 2025 14:06:30 +0000 Subject: [PATCH 10/12] Replace `ErrorEmitter` with `LJDiagnostics` --- .../{SimpleTest.java => CorrectSimple.java} | 2 +- ...ava => WarningExtRefNonExistentClass.java} | 2 +- ...va => WarningExtRefNonExistentMethod.java} | 2 +- ...ava => WarningExtRefWrongConstructor.java} | 2 +- ...a => WarningExtRefWrongParameterType.java} | 2 +- ...pe.java => WarningExtRefWrongRetType.java} | 2 +- .../liquidjava/api/CommandLineLauncher.java | 9 +- .../liquidjava/diagnostics/ErrorEmitter.java | 8 -- .../liquidjava/diagnostics/LJDiagnostics.java | 13 ++- .../diagnostics/errors/LJError.java | 8 +- .../diagnostics/warnings/LJWarning.java | 11 ++- .../processor/RefinementProcessor.java | 18 ++-- .../ann_generation/FieldGhostsGeneration.java | 13 ++- .../processor/context/AliasWrapper.java | 11 +-- .../ExternalRefinementTypeChecker.java | 48 ++++++----- .../MethodsFirstChecker.java | 19 ++-- .../RefinementTypeChecker.java | 86 +++++++++---------- .../refinement_checker/TypeChecker.java | 19 ++-- .../refinement_checker/VCChecker.java | 14 ++- .../general_checkers/OperationsChecker.java | 10 +-- .../AuxHierarchyRefinememtsPassage.java | 4 +- .../object_checkers/AuxStateHandler.java | 18 ++-- .../rj_language/BuiltinFunctionPredicate.java | 17 ++-- .../liquidjava/rj_language/Predicate.java | 21 +++-- .../liquidjava/api/tests/TestExamples.java | 38 ++++---- 25 files changed, 203 insertions(+), 194 deletions(-) rename liquidjava-example/src/main/java/testSuite/{SimpleTest.java => CorrectSimple.java} (87%) rename liquidjava-example/src/main/java/testSuite/{ErrorExtRefNonExistentClass.java => WarningExtRefNonExistentClass.java} (76%) rename liquidjava-example/src/main/java/testSuite/{ErrorExtRefNonExistentMethod.java => WarningExtRefNonExistentMethod.java} (89%) rename liquidjava-example/src/main/java/testSuite/{ErrorExtRefWrongConstructor.java => WarningExtRefWrongConstructor.java} (90%) rename liquidjava-example/src/main/java/testSuite/{ErrorExtRefWrongParameterType.java => WarningExtRefWrongParameterType.java} (89%) rename liquidjava-example/src/main/java/testSuite/{ErrorExtRefWrongRetType.java => WarningExtRefWrongRetType.java} (90%) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java diff --git a/liquidjava-example/src/main/java/testSuite/SimpleTest.java b/liquidjava-example/src/main/java/testSuite/CorrectSimple.java similarity index 87% rename from liquidjava-example/src/main/java/testSuite/SimpleTest.java rename to liquidjava-example/src/main/java/testSuite/CorrectSimple.java index 8821c0c9..c9096799 100644 --- a/liquidjava-example/src/main/java/testSuite/SimpleTest.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectSimple.java @@ -3,7 +3,7 @@ import liquidjava.specification.Refinement; @SuppressWarnings("unused") -public class SimpleTest { +public class CorrectSimple { public static void main(String[] args) { // Arithmetic Binary Operations @Refinement("a >= 10") diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentClass.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java similarity index 76% rename from liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentClass.java rename to liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java index 800ee7c0..b79eaa87 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentClass.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentClass.java @@ -3,6 +3,6 @@ import liquidjava.specification.ExternalRefinementsFor; @ExternalRefinementsFor("non.existent.Class") -public interface ErrorExtRefNonExistentClass { +public interface WarningExtRefNonExistentClass { public void NonExistentClass(); } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java similarity index 89% rename from liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java rename to liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java index 78b1c8c9..b98e48db 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorExtRefNonExistentMethod.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefNonExistentMethod.java @@ -5,7 +5,7 @@ import liquidjava.specification.StateRefinement; @ExternalRefinementsFor("java.util.ArrayList") -public interface ErrorExtRefNonExistentMethod { +public interface WarningExtRefNonExistentMethod { @RefinementPredicate("int size(ArrayList l)") @StateRefinement(to = "size(this) == 0") diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongConstructor.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java similarity index 90% rename from liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongConstructor.java rename to liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java index 636d3adb..a81ee0ed 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongConstructor.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongConstructor.java @@ -5,7 +5,7 @@ import liquidjava.specification.StateRefinement; @ExternalRefinementsFor("java.util.ArrayList") -public interface ErrorExtRefWrongConstructor { +public interface WarningExtRefWrongConstructor { @RefinementPredicate("int size(ArrayList l)") @StateRefinement(to = "size(this) == 0") diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongParameterType.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java similarity index 89% rename from liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongParameterType.java rename to liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java index da2135c5..c847d9e7 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongParameterType.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongParameterType.java @@ -5,7 +5,7 @@ import liquidjava.specification.StateRefinement; @ExternalRefinementsFor("java.util.ArrayList") -public interface ErrorExtRefWrongParameterType { +public interface WarningExtRefWrongParameterType { @RefinementPredicate("int size(ArrayList l)") @StateRefinement(to = "size(this) == 0") diff --git a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongRetType.java b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java similarity index 90% rename from liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongRetType.java rename to liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java index 48509080..bbba0b9a 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorExtRefWrongRetType.java +++ b/liquidjava-example/src/main/java/testSuite/WarningExtRefWrongRetType.java @@ -5,7 +5,7 @@ import liquidjava.specification.StateRefinement; @ExternalRefinementsFor("java.util.ArrayList") -public interface ErrorExtRefWrongRetType { +public interface WarningExtRefWrongRetType { @RefinementPredicate("int size(ArrayList l)") @StateRefinement(to = "size(this) == 0") diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 0aa4112b..8b925819 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -6,7 +6,6 @@ import java.util.Arrays; import java.util.List; -import liquidjava.diagnostics.ErrorEmitter; import liquidjava.diagnostics.errors.CustomError; import liquidjava.processor.RefinementProcessor; import spoon.Launcher; @@ -27,7 +26,12 @@ public static void main(String[] args) { } List paths = Arrays.asList(args); launch(paths.toArray(new String[0])); - System.out.println(diagnostics.foundError() ? diagnostics.toString() : "Correct! Passed Verification."); + if (diagnostics.foundError()) { + System.out.println(diagnostics.getErrorOutput()); + } else { + System.out.println(diagnostics.getWarningOutput()); + System.out.println("Correct! Passed Verification."); + } } public static void launch(String... paths) { @@ -45,6 +49,7 @@ public static void launch(String... paths) { launcher.getEnvironment().setNoClasspath(true); launcher.getEnvironment().setComplianceLevel(8); launcher.run(); + diagnostics.clear(); final Factory factory = launcher.getFactory(); final ProcessingManager processingManager = new QueueProcessingManager(factory); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java deleted file mode 100644 index 21e6028e..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java +++ /dev/null @@ -1,8 +0,0 @@ -package liquidjava.diagnostics; - -public class ErrorEmitter { - - public boolean foundError() { - return false; - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java index b5473a53..211115be 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java @@ -58,8 +58,7 @@ public void clear() { this.warnings.clear(); } - @Override - public String toString() { + public String getErrorOutput() { StringBuilder sb = new StringBuilder(); if (foundError()) { for (LJError error : errors) { @@ -76,4 +75,14 @@ public String toString() { } return sb.toString(); } + + public String getWarningOutput() { + StringBuilder sb = new StringBuilder(); + if (foundWarning()) { + for (LJWarning warning : warnings) { + sb.append(warning.toString()).append("\n"); + } + } + return sb.toString(); + } } 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 ea7fe942..806a86b9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -62,8 +62,12 @@ public TranslationTable getTranslationTable() { public String toString(String extra) { StringBuilder sb = new StringBuilder(); - sb.append(title).append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@")) - .append("\n\n"); + sb.append(title); + + if (element != null) + sb.append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@")); + + sb.append("\n"); sb.append(message).append("\n"); if (extra != null) sb.append(extra).append("\n"); 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 7cf59dd9..8cecc0c7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java @@ -49,10 +49,15 @@ public SourcePosition getLocation() { public String toString(String extra) { StringBuilder sb = new StringBuilder(); - sb.append(message).append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@")) - .append("\n\n"); + sb.append(message); + + if (element != null) + sb.append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@")); + if (extra != null) - sb.append(extra).append("\n"); + sb.append("\n").append(extra); + + sb.append("\n"); sb.append("Location: ").append(location != null ? Utils.stripParens(location.toString()) : "") .append("\n"); return sb.toString(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java index 46069f40..75b8edc5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java @@ -1,9 +1,10 @@ package liquidjava.processor; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; + import java.util.ArrayList; import java.util.List; -import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.ann_generation.FieldGhostsGeneration; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.ExternalRefinementTypeChecker; @@ -18,11 +19,9 @@ public class RefinementProcessor extends AbstractProcessor { List visitedPackages = new ArrayList<>(); Factory factory; - ErrorEmitter errorEmitter; - public RefinementProcessor(Factory factory, ErrorEmitter ee) { + public RefinementProcessor(Factory factory) { this.factory = factory; - errorEmitter = ee; } @Override @@ -32,15 +31,14 @@ public void process(CtPackage pkg) { Context c = Context.getInstance(); c.reinitializeAllContext(); - pkg.accept(new FieldGhostsGeneration(c, factory, errorEmitter)); // generate annotations for field ghosts + pkg.accept(new FieldGhostsGeneration(c, factory)); // generate annotations for field ghosts // void spoon.reflect.visitor.CtVisitable.accept(CtVisitor arg0) - pkg.accept(new ExternalRefinementTypeChecker(c, factory, errorEmitter)); - - pkg.accept(new MethodsFirstChecker(c, factory, errorEmitter)); // double passing idea (instead of headers) + pkg.accept(new ExternalRefinementTypeChecker(c, factory)); + pkg.accept(new MethodsFirstChecker(c, factory)); // double passing idea (instead of headers) - pkg.accept(new RefinementTypeChecker(c, factory, errorEmitter)); - if (errorEmitter.foundError()) + pkg.accept(new RefinementTypeChecker(c, factory)); + if (diagnostics.foundError()) return; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java b/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java index dbe672f5..719e6d40 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java @@ -1,6 +1,7 @@ package liquidjava.processor.ann_generation; -import liquidjava.diagnostics.ErrorEmitter; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; + import liquidjava.processor.context.Context; import liquidjava.specification.Ghost; import spoon.reflect.declaration.*; @@ -11,12 +12,10 @@ public class FieldGhostsGeneration extends CtScanner { Context context; Factory factory; - ErrorEmitter errorEmitter; - public FieldGhostsGeneration(Context c, Factory fac, ErrorEmitter errorEmitter) { - this.context = c; - this.factory = fac; - this.errorEmitter = errorEmitter; + public FieldGhostsGeneration(Context context, Factory factory) { + this.context = context; + this.factory = factory; } public Context getContext() { @@ -29,7 +28,7 @@ public Factory getFactory() { @Override public void visitCtClass(CtClass ctClass) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java index cb218d7e..fc8283d5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java @@ -5,7 +5,6 @@ import java.util.List; import java.util.Map; -import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.facade.AliasDTO; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; @@ -60,9 +59,8 @@ public Expression getNewExpression(List newNames) { return expr.getExpression().clone(); } - public Predicate getPremises(List list, List newNames, CtElement elem, ErrorEmitter ee) - throws ParsingException { - List invocationPredicates = getPredicatesFromExpression(list, elem, ee); + public Predicate getPremises(List list, List newNames, CtElement elem) throws ParsingException { + List invocationPredicates = getPredicatesFromExpression(list, elem); Predicate prem = new Predicate(); for (int i = 0; i < invocationPredicates.size(); i++) { prem = Predicate.createConjunction(prem, @@ -71,11 +69,10 @@ public Predicate getPremises(List list, List newNames, CtElement return prem.clone(); } - private List getPredicatesFromExpression(List list, CtElement elem, ErrorEmitter ee) - throws ParsingException { + private List getPredicatesFromExpression(List list, CtElement elem) throws ParsingException { List lp = new ArrayList<>(); for (String e : list) - lp.add(new Predicate(e, elem, ee)); + lp.add(new Predicate(e, elem)); return lp; } 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 8d128015..bd825c8f 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 @@ -5,7 +5,6 @@ import java.util.Arrays; import java.util.List; import java.util.Optional; -import liquidjava.diagnostics.ErrorEmitter; import liquidjava.diagnostics.errors.CustomError; import liquidjava.diagnostics.warnings.ExternalClassNotFoundWarning; import liquidjava.diagnostics.warnings.ExternalMethodNotFoundWarning; @@ -31,8 +30,8 @@ public class ExternalRefinementTypeChecker extends TypeChecker { String prefix; MethodsFunctionsChecker m; - public ExternalRefinementTypeChecker(Context context, Factory fac, ErrorEmitter errorEmitter) { - super(context, fac, errorEmitter); + public ExternalRefinementTypeChecker(Context context, Factory factory) { + super(context, factory); } @Override @@ -42,7 +41,7 @@ public void visitCtClass(CtClass ctClass) { @Override public void visitCtInterface(CtInterface intrface) { - if (errorEmitter.foundError()) + if (diagnostics.foundError()) return; Optional externalRefinements = getExternalRefinement(intrface); @@ -56,7 +55,7 @@ public void visitCtInterface(CtInterface intrface) { try { getRefinementFromAnnotation(intrface); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } handleStateSetsFromAnnotation(intrface); super.visitCtInterface(intrface); @@ -65,14 +64,14 @@ public void visitCtInterface(CtInterface intrface) { @Override public void visitCtField(CtField f) { - if (errorEmitter.foundError()) + if (diagnostics.foundError()) return; Optional oc; try { oc = getRefinementFromAnnotation(f); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } Predicate c = oc.orElse(new Predicate()); context.addGlobalVariableToContext(f.getSimpleName(), prefix, f.getType(), c); @@ -80,7 +79,7 @@ public void visitCtField(CtField f) { } public void visitCtMethod(CtMethod method) { - if (errorEmitter.foundError()) + if (diagnostics.foundError()) return; CtType targetType = factory.Type().createReference(prefix).getTypeDeclaration(); @@ -88,20 +87,25 @@ public void visitCtMethod(CtMethod method) { return; boolean isConstructor = method.getSimpleName().equals(targetType.getSimpleName()); - if (isConstructor && !constructorExists(targetType, method)) { - String title = String.format("Could not find constructor '%s' for '%s'", method.getSignature(), prefix); - String[] overloads = getOverloads(targetType, method); - String message = overloads.length == 0 ? title - : title + "\nAvailable constructors:\n " + String.join("\n ", overloads); - diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix)); - } else if (!methodExists(targetType, method)) { - String title = String.format("Could not find method '%s %s' for '%s'", method.getType().getSimpleName(), - method.getSignature(), prefix); - String[] overloads = getOverloads(targetType, method); - String message = overloads.length == 0 ? title - : title + "\nAvailable overloads:\n " + String.join("\n ", overloads); - diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix)); - return; + if (isConstructor) { + if (!constructorExists(targetType, method)) { + String title = String.format("Could not find constructor '%s' for '%s'", method.getSignature(), prefix); + String[] overloads = getOverloads(targetType, method); + String message = overloads.length == 0 ? title + : title + "\nAvailable constructors:\n " + String.join("\n ", overloads); + + diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix)); + } + } else { + if (!methodExists(targetType, method)) { + String title = String.format("Could not find method '%s %s' for '%s'", method.getType().getSimpleName(), + method.getSignature(), prefix); + String[] overloads = getOverloads(targetType, method); + String message = overloads.length == 0 ? title + : title + "\nAvailable overloads:\n " + String.join("\n ", overloads); + diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix)); + return; + } } MethodsFunctionsChecker mfc = new MethodsFunctionsChecker(this); try { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index 92cadcf5..6e84985d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -1,9 +1,10 @@ package liquidjava.processor.refinement_checker; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; + import java.util.ArrayList; import java.util.List; -import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import liquidjava.rj_language.parsing.ParsingException; @@ -20,15 +21,15 @@ public class MethodsFirstChecker extends TypeChecker { MethodsFunctionsChecker mfc; List visitedClasses; - public MethodsFirstChecker(Context c, Factory fac, ErrorEmitter errorEmitter) { - super(c, fac, errorEmitter); + public MethodsFirstChecker(Context context, Factory factory) { + super(context, factory); mfc = new MethodsFunctionsChecker(this); visitedClasses = new ArrayList<>(); } @Override public void visitCtClass(CtClass ctClass) { - if (errorEmitter.foundError()) + if (diagnostics.foundError()) return; context.reinitializeContext(); @@ -55,7 +56,7 @@ public void visitCtClass(CtClass ctClass) { try { getRefinementFromAnnotation(ctClass); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } handleStateSetsFromAnnotation(ctClass); super.visitCtClass(ctClass); @@ -63,7 +64,7 @@ public void visitCtClass(CtClass ctClass) { @Override public void visitCtInterface(CtInterface intrface) { - if (errorEmitter.foundError()) + if (diagnostics.foundError()) return; if (visitedClasses.contains(intrface.getQualifiedName())) @@ -76,7 +77,7 @@ public void visitCtInterface(CtInterface intrface) { try { getRefinementFromAnnotation(intrface); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } handleStateSetsFromAnnotation(intrface); super.visitCtInterface(intrface); @@ -84,7 +85,7 @@ public void visitCtInterface(CtInterface intrface) { @Override public void visitCtConstructor(CtConstructor c) { - if (errorEmitter.foundError()) + if (diagnostics.foundError()) return; context.enterContext(); @@ -99,7 +100,7 @@ public void visitCtConstructor(CtConstructor c) { } public void visitCtMethod(CtMethod method) { - if (errorEmitter.foundError()) + if (diagnostics.foundError()) return; context.enterContext(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 53b65116..2365d9b9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -1,11 +1,12 @@ package liquidjava.processor.refinement_checker; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; + import java.lang.annotation.Annotation; import java.util.Arrays; import java.util.List; import java.util.Optional; -import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import liquidjava.processor.refinement_checker.general_checkers.OperationsChecker; @@ -55,8 +56,8 @@ public class RefinementTypeChecker extends TypeChecker { OperationsChecker otc; MethodsFunctionsChecker mfc; - public RefinementTypeChecker(Context context, Factory factory, ErrorEmitter errorEmitter) { - super(context, factory, errorEmitter); + public RefinementTypeChecker(Context context, Factory factory) { + super(context, factory); otc = new OperationsChecker(this); mfc = new MethodsFunctionsChecker(this); } @@ -65,7 +66,7 @@ public RefinementTypeChecker(Context context, Factory factory, ErrorEmitter erro @Override public void visitCtClass(CtClass ctClass) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -76,7 +77,7 @@ public void visitCtClass(CtClass ctClass) { @Override public void visitCtInterface(CtInterface intrface) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -89,7 +90,7 @@ public void visitCtInterface(CtInterface intrface) { @Override public void visitCtAnnotationType(CtAnnotationType annotationType) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } super.visitCtAnnotationType(annotationType); @@ -97,7 +98,7 @@ public void visitCtAnnotationType(CtAnnotationType ann @Override public void visitCtConstructor(CtConstructor c) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -108,7 +109,7 @@ public void visitCtConstructor(CtConstructor c) { } public void visitCtMethod(CtMethod method) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -122,7 +123,7 @@ public void visitCtMethod(CtMethod method) { @Override public void visitCtLocalVariable(CtLocalVariable localVariable) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -133,7 +134,7 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { try { a = getRefinementFromAnnotation(localVariable); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(), a.orElse(new Predicate()), localVariable); @@ -151,7 +152,7 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, localVariable); } catch (ParsingException e1) { - return; // error already in ErrorEmitter + return; // error already reported } AuxStateHandler.addStateRefinements(this, varName, e); @@ -160,7 +161,7 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { @Override public void visitCtNewArray(CtNewArray newArray) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -172,7 +173,7 @@ public void visitCtNewArray(CtNewArray newArray) { try { c = getExpressionRefinements(exp); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } String name = String.format(Formats.FRESH, context.getCounter()); if (c.getVariableNames().contains(Keys.WILDCARD)) { @@ -183,11 +184,10 @@ public void visitCtNewArray(CtNewArray newArray) { context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, c, exp); Predicate ep; try { - ep = Predicate.createEquals( - BuiltinFunctionPredicate.builtin_length(Keys.WILDCARD, newArray, getErrorEmitter()), + ep = Predicate.createEquals(BuiltinFunctionPredicate.length(Keys.WILDCARD, newArray), Predicate.createVar(name)); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } newArray.putMetadata(Keys.REFINEMENT, ep); } @@ -195,7 +195,7 @@ public void visitCtNewArray(CtNewArray newArray) { @Override public void visitCtThisAccess(CtThisAccess thisAccess) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -212,7 +212,7 @@ public void visitCtThisAccess(CtThisAccess thisAccess) { @SuppressWarnings("unchecked") @Override public void visitCtAssignment(CtAssignment assignment) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -246,7 +246,7 @@ public void visitCtAssignment(CtAssignment assignment) { @Override public void visitCtArrayRead(CtArrayRead arrayRead) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -259,7 +259,7 @@ public void visitCtArrayRead(CtArrayRead arrayRead) { @Override public void visitCtLiteral(CtLiteral lit) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -281,7 +281,7 @@ public void visitCtLiteral(CtLiteral lit) { @Override public void visitCtField(CtField f) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -290,7 +290,7 @@ public void visitCtField(CtField f) { try { c = getRefinementFromAnnotation(f); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } // context.addVarToContext(f.getSimpleName(), f.getType(), // c.map( i -> i.substituteVariable(WILD_VAR, f.getSimpleName()).orElse(new @@ -308,7 +308,7 @@ public void visitCtField(CtField f) { @Override public void visitCtFieldRead(CtFieldRead fieldRead) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -332,9 +332,9 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { String targetName = fieldRead.getTarget().toString(); try { fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), - BuiltinFunctionPredicate.builtin_length(targetName, fieldRead, getErrorEmitter()))); + BuiltinFunctionPredicate.length(targetName, fieldRead))); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } } else { fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); @@ -346,7 +346,7 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { @Override public void visitCtVariableRead(CtVariableRead variableRead) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -360,7 +360,7 @@ public void visitCtVariableRead(CtVariableRead variableRead) { */ @Override public void visitCtBinaryOperator(CtBinaryOperator operator) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -368,13 +368,13 @@ public void visitCtBinaryOperator(CtBinaryOperator operator) { try { otc.getBinaryOpRefinements(operator); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } } @Override public void visitCtUnaryOperator(CtUnaryOperator operator) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -382,12 +382,12 @@ public void visitCtUnaryOperator(CtUnaryOperator operator) { try { otc.getUnaryOpRefinements(operator); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } } public void visitCtInvocation(CtInvocation invocation) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -397,7 +397,7 @@ public void visitCtInvocation(CtInvocation invocation) { @Override public void visitCtReturn(CtReturn ret) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -407,7 +407,7 @@ public void visitCtReturn(CtReturn ret) { @Override public void visitCtIf(CtIf ifElement) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -417,7 +417,7 @@ public void visitCtIf(CtIf ifElement) { try { expRefs = getExpressionRefinements(exp); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } String freshVarName = String.format(Formats.FRESH, context.getCounter()); expRefs = expRefs.substituteVariable(Keys.WILDCARD, freshVarName); @@ -463,7 +463,7 @@ public void visitCtIf(CtIf ifElement) { @Override public void visitCtArrayWrite(CtArrayWrite arrayWrite) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -471,17 +471,17 @@ public void visitCtArrayWrite(CtArrayWrite arrayWrite) { CtExpression index = arrayWrite.getIndexExpression(); BuiltinFunctionPredicate fp; try { - fp = BuiltinFunctionPredicate.builtin_addToIndex(arrayWrite.getTarget().toString(), index.toString(), - Keys.WILDCARD, arrayWrite, getErrorEmitter()); + fp = BuiltinFunctionPredicate.addToIndex(arrayWrite.getTarget().toString(), index.toString(), Keys.WILDCARD, + arrayWrite); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } arrayWrite.putMetadata(Keys.REFINEMENT, fp); } @Override public void visitCtConditional(CtConditional conditional) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -494,7 +494,7 @@ public void visitCtConditional(CtConditional conditional) { @Override public void visitCtConstructorCall(CtConstructorCall ctConstructorCall) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -504,7 +504,7 @@ public void visitCtConstructorCall(CtConstructorCall ctConstructorCall) { @Override public void visitCtNewClass(CtNewClass newClass) { - if (errorEmitter.foundError()) { + if (diagnostics.foundError()) { return; } @@ -534,7 +534,7 @@ private void checkAssignment(String name, CtTypeReference type, CtExpression< try { checkVariableRefinements(refinementFound, name, type, parentElem, varDecl); } catch (ParsingException e) { - return; // error already in ErrorEmitter + return; // error already reported } } @@ -552,7 +552,7 @@ private Predicate getExpressionRefinements(CtExpression element) throws Parsi return getRefinement(op); } else if (element instanceof CtLiteral) { CtLiteral l = (CtLiteral) element; - return new Predicate(l.getValue().toString(), l, errorEmitter); + return new Predicate(l.getValue().toString(), l); } else if (element instanceof CtInvocation) { CtInvocation inv = (CtInvocation) element; visitCtInvocation(inv); 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 bc1a008e..8986dfb0 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 @@ -7,7 +7,6 @@ import java.util.List; import java.util.Optional; -import liquidjava.diagnostics.ErrorEmitter; import liquidjava.diagnostics.errors.CustomError; import liquidjava.diagnostics.errors.InvalidRefinementError; import liquidjava.diagnostics.errors.SyntaxError; @@ -41,13 +40,11 @@ public abstract class TypeChecker extends CtScanner { Context context; Factory factory; VCChecker vcChecker; - ErrorEmitter errorEmitter; - public TypeChecker(Context c, Factory fac, ErrorEmitter errorEmitter) { - this.context = c; - this.factory = fac; - this.errorEmitter = errorEmitter; - vcChecker = new VCChecker(errorEmitter); + public TypeChecker(Context context, Factory factory) { + this.context = context; + this.factory = factory; + vcChecker = new VCChecker(); } public Context getContext() { @@ -83,7 +80,7 @@ public Optional getRefinementFromAnnotation(CtElement element) throws } } if (ref.isPresent()) { - Predicate p = new Predicate(ref.get(), element, errorEmitter); + Predicate p = new Predicate(ref.get(), element); // check if refinement is valid if (!p.getExpression().isBooleanExpression()) { @@ -91,7 +88,7 @@ public Optional getRefinementFromAnnotation(CtElement element) throws ref.get())); return Optional.empty(); } - if (errorEmitter.foundError()) + if (diagnostics.foundError()) return Optional.empty(); constr = Optional.of(p); @@ -331,8 +328,4 @@ public void createSameStateError(CtElement element, Predicate expectedType, Stri public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate[] expected) { vcChecker.printStateMismatchError(element, method, found, expected); } - - public ErrorEmitter getErrorEmitter() { - return errorEmitter; - } } 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 241c107e..0f0839ae 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.function.Consumer; import java.util.stream.Collectors; -import liquidjava.diagnostics.ErrorEmitter; import liquidjava.diagnostics.errors.CustomError; import liquidjava.diagnostics.errors.GhostInvocationError; import liquidjava.diagnostics.errors.LJError; @@ -34,12 +33,10 @@ public class VCChecker { private final Context context; private final List pathVariables; - private final ErrorEmitter errorEmitter; - public VCChecker(ErrorEmitter errorEmitter) { + public VCChecker() { context = Context.getInstance(); pathVariables = new Stack<>(); - this.errorEmitter = errorEmitter; } public void processSubtyping(Predicate expectedType, List list, CtElement element, Factory f) { @@ -55,10 +52,9 @@ public void processSubtyping(Predicate expectedType, List list, CtEl Predicate et = new Predicate(); try { List filtered = filterGhostStatesForVariables(list, mainVars, lrv); - premises = premisesBeforeChange.changeStatesToRefinements(filtered, s, errorEmitter) - .changeAliasToRefinement(context, f); + premises = premisesBeforeChange.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); - et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f); + et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); } catch (Exception e) { diagnostics.add(new RefinementError(element, expectedType, premises.simplify(), map)); return; @@ -96,9 +92,9 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List< try { premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); List filtered = filterGhostStatesForVariables(list, mainVars, lrv); - premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s, errorEmitter) + premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s) .changeAliasToRefinement(context, f); - et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f); + et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); } catch (Exception e) { return false; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index a4adf7c7..0a93f1ac 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -237,7 +237,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab a = a.substituteVariable(Keys.WILDCARD, ""); String s = a.toString().replace("(", "").replace(")", "").replace("==", "").replace(" ", ""); // TODO // IMPROVE - return new Predicate(String.format("(%s)", s), element, rtc.getErrorEmitter()); + return new Predicate(String.format("(%s)", s), element); } else if (element instanceof CtLiteral) { CtLiteral l = (CtLiteral) element; @@ -248,7 +248,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab if (l.getValue() == null) throw new ParsingException("Null literals are not supported"); - return new Predicate(l.getValue().toString(), element, rtc.getErrorEmitter()); + return new Predicate(l.getValue().toString(), element); } else if (element instanceof CtInvocation) { CtInvocation inv = (CtInvocation) element; @@ -266,7 +266,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab innerRefs = innerRefs.substituteVariable(Keys.WILDCARD, newName); rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv); - return new Predicate(newName, inv, rtc.getErrorEmitter()); // Return variable that represents the invocation + return new Predicate(newName, inv); // Return variable that represents the invocation } return rtc.getRefinement(element); // TODO Maybe add cases @@ -301,7 +301,7 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv, CtB } rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv); - return new Predicate(newName, inv, rtc.getErrorEmitter()); // Return variable that represents the invocation + return new Predicate(newName, inv); // Return variable that represents the invocation } return new Predicate(); } @@ -375,6 +375,6 @@ private Predicate getOperatorFromKind(UnaryOperatorKind kind, CtElement elem) th case NEG -> "-" + Keys.WILDCARD; default -> throw new ParsingException(kind + "operation not supported"); }; - return new Predicate(ret, elem, rtc.getErrorEmitter()); + return new Predicate(ret, elem); }; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java index 0d2499e5..63e5ad18 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java @@ -1,5 +1,7 @@ package liquidjava.processor.refinement_checker.object_checkers; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; + import java.util.HashMap; import java.util.List; import java.util.Optional; @@ -83,7 +85,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF } else { boolean f = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition()); if (!f) { - if (!tc.getErrorEmitter().foundError()) + if (!diagnostics.foundError()) tc.createError(method, 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 0ea5d336..4cc11384 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 @@ -73,7 +73,7 @@ private static void setConstructorStates(RefinedFunction f, List ctAnnota private static Predicate createStatePredicate(String value, /* RefinedFunction f */ String targetClass, TypeChecker tc, CtElement e, boolean isTo, String prefix) throws ParsingException { - Predicate p = new Predicate(value, e, tc.getErrorEmitter(), prefix); + Predicate p = new Predicate(value, e, prefix); if (!p.getExpression().isBooleanExpression()) { diagnostics.add( new InvalidRefinementError(e, "State refinement transition must be a boolean expression", value)); @@ -208,9 +208,9 @@ private static Predicate createStatePredicate(String value, /* RefinedFunction f // what is it for? Predicate c1 = isTo ? getMissingStates(t, tc, p) : p; Predicate c = c1.substituteVariable(Keys.THIS, name); - c = c.changeOldMentions(nameOld, name, tc.getErrorEmitter()); + c = c.changeOldMentions(nameOld, name); boolean b = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition()); - if (b && !tc.getErrorEmitter().foundError()) { + if (b && !diagnostics.foundError()) { tc.createSameStateError(e, p, t); } @@ -398,10 +398,10 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { // replace "state(this)" to "state(whatever method is called from) and so on" Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName) - .changeOldMentions(vi.getName(), instanceName, tc.getErrorEmitter()); + .changeOldMentions(vi.getName(), instanceName); if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition - if (!tc.getErrorEmitter().foundError()) { // No errors in errorEmitter + if (!diagnostics.foundError()) { // No errors so far Predicate[] states = { stateChange.getFrom() }; tc.createStateMismatchError(fw, fw.toString(), prevState, states); } @@ -473,7 +473,7 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi, prevCheck = prevCheck.substituteVariable(s, map.get(s)); expectState = expectState.substituteVariable(s, map.get(s)); } - expectState = expectState.changeOldMentions(vi.getName(), instanceName, tc.getErrorEmitter()); + expectState = expectState.changeOldMentions(vi.getName(), instanceName); found = tc.checksStateSMT(prevCheck, expectState, invocation.getPosition()); if (found && stateChange.hasTo()) { @@ -489,7 +489,7 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi, return transitionedState; } } - if (!found && !tc.getErrorEmitter().foundError()) { // Reaches the end of stateChange no matching states + if (!found && !diagnostics.foundError()) { // Reaches the end of stateChange no matching states Predicate[] states = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom) .toArray(Predicate[]::new); String simpleInvocation = invocation.toString(); // .getExecutable().toString(); @@ -502,7 +502,7 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi, private static Predicate checkOldMentions(Predicate transitionedState, String instanceName, String newInstanceName, TypeChecker tc) { - return transitionedState.changeOldMentions(instanceName, newInstanceName, tc.getErrorEmitter()); + return transitionedState.changeOldMentions(instanceName, newInstanceName); } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java index 0b57ac50..61fe26e8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java @@ -1,24 +1,21 @@ package liquidjava.rj_language; -import liquidjava.diagnostics.ErrorEmitter; import liquidjava.rj_language.parsing.ParsingException; import spoon.reflect.declaration.CtElement; public class BuiltinFunctionPredicate extends Predicate { - public BuiltinFunctionPredicate(ErrorEmitter ee, CtElement elem, String functionName, String... params) - throws ParsingException { - super(functionName + "(" + getFormattedParams(params) + ")", elem, ee); + public BuiltinFunctionPredicate(CtElement elem, String functionName, String... params) throws ParsingException { + super(functionName + "(" + getFormattedParams(params) + ")", elem); } - public static BuiltinFunctionPredicate builtin_length(String param, CtElement elem, ErrorEmitter ee) - throws ParsingException { - return new BuiltinFunctionPredicate(ee, elem, "length", param); + public static BuiltinFunctionPredicate length(String param, CtElement elem) throws ParsingException { + return new BuiltinFunctionPredicate(elem, "length", param); } - public static BuiltinFunctionPredicate builtin_addToIndex(String array, String index, String value, CtElement elem, - ErrorEmitter ee) throws ParsingException { - return new BuiltinFunctionPredicate(ee, elem, "addToIndex", index, value); + public static BuiltinFunctionPredicate addToIndex(String array, String index, String value, CtElement elem) + throws ParsingException { + return new BuiltinFunctionPredicate(elem, "addToIndex", index, value); } private static String getFormattedParams(String... params) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 4eb77218..41de354b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -8,7 +8,6 @@ import java.util.Map; import java.util.stream.Collectors; -import liquidjava.diagnostics.ErrorEmitter; import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; @@ -60,8 +59,8 @@ public Predicate() { * * @throws ParsingException */ - public Predicate(String ref, CtElement element, ErrorEmitter e) throws ParsingException { - this(ref, element, e, element.getParent(CtType.class).getQualifiedName()); + public Predicate(String ref, CtElement element) throws ParsingException { + this(ref, element, element.getParent(CtType.class).getQualifiedName()); } /** @@ -74,10 +73,10 @@ public Predicate(String ref, CtElement element, ErrorEmitter e) throws ParsingEx * * @throws ParsingException */ - public Predicate(String ref, CtElement element, ErrorEmitter e, String prefix) throws ParsingException { + public Predicate(String ref, CtElement element, String prefix) throws ParsingException { this.prefix = prefix; - exp = parse(ref, element, e); - if (e.foundError()) { + exp = parse(ref, element); + if (diagnostics.foundError()) { return; } if (!(exp instanceof GroupExpression)) { @@ -90,7 +89,7 @@ public Predicate(Expression e) { exp = e; } - protected Expression parse(String ref, CtElement element, ErrorEmitter ee) throws ParsingException { + protected Expression parse(String ref, CtElement element) throws ParsingException { try { return RefinementsParser.createAST(ref, prefix); } catch (ParsingException e) { @@ -99,7 +98,7 @@ protected Expression parse(String ref, CtElement element, ErrorEmitter ee) throw } } - protected Expression innerParse(String ref, ErrorEmitter e, String prefix) { + protected Expression innerParse(String ref, String prefix) { try { return RefinementsParser.createAST(ref, prefix); } catch (ParsingException e1) { @@ -154,7 +153,7 @@ public List getStateInvocations(List lgs) { } /** Change old mentions of previous name to the new name e.g., old(previousName) -> newName */ - public Predicate changeOldMentions(String previousName, String newName, ErrorEmitter ee) { + public Predicate changeOldMentions(String previousName, String newName) { Expression e = exp.clone(); Expression prev = createVar(previousName).getExpression(); List le = new ArrayList<>(); @@ -186,12 +185,12 @@ private void expressionGetOldVariableNames(Expression exp, List ls) { } } - public Predicate changeStatesToRefinements(List ghostState, String[] toChange, ErrorEmitter ee) { + public Predicate changeStatesToRefinements(List ghostState, String[] toChange) { Map nameRefinementMap = new HashMap<>(); for (GhostState gs : ghostState) { if (gs.getRefinement() != null) { // is a state and not a ghost state String name = gs.getQualifiedName(); - Expression exp = innerParse(gs.getRefinement().toString(), ee, gs.getPrefix()); + Expression exp = innerParse(gs.getRefinement().toString(), gs.getPrefix()); nameRefinementMap.put(name, exp); // Also allow simple name lookup to enable hierarchy matching String simple = Utils.getSimpleName(name); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java index 7f216a32..5ffa1dcb 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -1,5 +1,6 @@ package liquidjava.api.tests; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; import static org.junit.Assert.fail; import java.io.IOException; @@ -8,7 +9,6 @@ import java.nio.file.Paths; import java.util.stream.Stream; import liquidjava.api.CommandLineLauncher; -import liquidjava.diagnostics.ErrorEmitter; import org.junit.Test; import org.junit.jupiter.params.ParameterizedTest; @@ -29,17 +29,18 @@ public void testFile(final Path filePath) { String fileName = filePath.getFileName().toString(); // 1. Run the verifier on the file or package - ErrorEmitter errorEmitter = CommandLineLauncher.launch(filePath.toAbsolutePath().toString()); + CommandLineLauncher.launch(filePath.toAbsolutePath().toString()); // 2. Check if the file is correct or contains an error - if ((fileName.startsWith("Correct") && errorEmitter.foundError()) - || (fileName.contains("correct") && errorEmitter.foundError())) { + if (isCorrect(fileName) && diagnostics.foundError()) { + if (fileName.toLowerCase().startsWith("warning")) { + System.out.println("Warning in directory: " + fileName + " --- should be correct with warnings"); + } System.out.println("Error in directory: " + fileName + " --- should be correct but an error was found"); fail(); } // 3. Check if the file has an error but passed verification - if ((fileName.startsWith("Error") && !errorEmitter.foundError()) - || (fileName.contains("error") && !errorEmitter.foundError())) { + if (isError(fileName) && !diagnostics.foundError()) { System.out.println("Error in directory: " + fileName + " --- should be an error but passed verification"); fail(); } @@ -47,8 +48,8 @@ public void testFile(final Path filePath) { /** * Returns a Stream of paths to test files in the testSuite directory. These include files with names starting with - * "Correct" or "Error", and directories containing "correct" or "error". - * + * "Correct" or "Error", and directories containing "correct" or "error". § + * * @return Stream of paths to test files * * @throws IOException @@ -60,11 +61,11 @@ private static Stream fileNameSource() throws IOException { String name = filePath.getFileName().toString(); // 1. Files that start with "Correct" or "Error" boolean isFileStartingWithCorrectOrError = fileAttr.isRegularFile() - && (name.startsWith("Correct") || name.startsWith("Error")); + && (isCorrect(name) || isError(name)); // 2. Folders (directories) that contain "correct" or "error" boolean isDirectoryWithCorrectOrError = fileAttr.isDirectory() - && (name.contains("correct") || name.contains("error")); + && (isCorrect(name) || isError(name)); // Return true if either condition matches return isFileStartingWithCorrectOrError || isDirectoryWithCorrectOrError; @@ -77,14 +78,21 @@ private static Stream fileNameSource() throws IOException { */ @Test public void testMultiplePaths() { - String[] paths = { "../liquidjava-example/src/main/java/testSuite/SimpleTest.java", + String[] paths = { "../liquidjava-example/src/main/java/testSuite/CorrectSimple.java", "../liquidjava-example/src/main/java/testSuite/classes/arraylist_correct", }; - ErrorEmitter errorEmitter = CommandLineLauncher.launch(paths); - + CommandLineLauncher.launch(paths); // Check if any of the paths that should be correct found an error - if (errorEmitter.foundError()) { - System.out.println("Error found in files that should be correct."); + if (diagnostics.foundError()) { + System.out.println("Error found in files that should be correct"); fail(); } } + + private static boolean isCorrect(String path) { + return path.toLowerCase().contains("correct") || path.toLowerCase().contains("warning"); + } + + private static boolean isError(String path) { + return path.toLowerCase().contains("error"); + } } From a0239cee41053249e26bb3269f5acc5519c19f35 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 10 Nov 2025 14:33:16 +0000 Subject: [PATCH 11/12] Minor Change --- .../liquidjava/processor/refinement_checker/TypeChecker.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 8986dfb0..ebce5070 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 @@ -248,7 +248,8 @@ protected void handleAlias(String value, CtElement element) { a.parse(path); // refinement alias must return a boolean expression if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) { - diagnostics.add(new CustomError(element, "Refinement alias must return a boolean expression")); + diagnostics.add(new InvalidRefinementError(element, + "Refinement alias must return a boolean expression", value)); return; } AliasWrapper aw = new AliasWrapper(a, factory, Keys.WILDCARD, context, klass, path); From dc1742585171722ca05eb2929b9b97eb9e35df84 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 10 Nov 2025 15:17:58 +0000 Subject: [PATCH 12/12] Improvements --- .../diagnostics/errors/CustomError.java | 9 ++++-- .../errors/GhostInvocationError.java | 8 +++--- .../IllegalConstructorTransitionError.java | 3 +- .../errors/InvalidRefinementError.java | 2 +- .../diagnostics/errors/LJError.java | 28 ++++++++----------- .../diagnostics/errors/NotFoundError.java | 2 +- .../diagnostics/errors/RefinementError.java | 4 +-- .../errors/StateConflictError.java | 3 +- .../errors/StateRefinementError.java | 3 +- .../diagnostics/errors/SyntaxError.java | 2 +- .../refinement_checker/VCChecker.java | 13 +++++---- .../java/liquidjava/smt/SMTEvaluator.java | 17 +++++++---- 12 files changed, 51 insertions(+), 43 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 b0fb13d7..e02b8c9f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -1,5 +1,6 @@ package liquidjava.diagnostics.errors; +import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; /** @@ -10,11 +11,15 @@ public class CustomError extends LJError { public CustomError(String message) { - super("Found Error", message, null, null); + super("Found Error", message, null, null, null); + } + + public CustomError(String message, SourcePosition pos) { + super("Found Error", message, pos, null, null); } public CustomError(CtElement element, String message) { - super("Found Error", message, element, null); + super("Found Error", message, element.getPosition(), element.toString(), null); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java index 3fd4b7a2..2b539c9b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java @@ -2,7 +2,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.Predicate; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Error indicating that a ghost method invocation is invalid (e.g., has wrong arguments) @@ -13,9 +13,9 @@ public class GhostInvocationError extends LJError { private String expected; - public GhostInvocationError(CtElement element, Predicate expected, TranslationTable translationTable) { - super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element, - translationTable); + public GhostInvocationError(String message, SourcePosition pos, Predicate expected, + TranslationTable translationTable) { + super("Ghost Invocation Error", message, pos, null, translationTable); this.expected = expected.toString(); } 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 8146ccf8..11908a6b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java @@ -11,7 +11,8 @@ public class IllegalConstructorTransitionError extends LJError { public IllegalConstructorTransitionError(CtElement element) { super("Illegal Constructor Transition Error", - "Found constructor with 'from' state (should only have a 'to' state)", element, null); + "Found constructor with 'from' state (should only have a 'to' state)", element.getPosition(), + element.toString(), null); } @Override 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 bbf95081..03c55813 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 String refinement; public InvalidRefinementError(CtElement element, String message, String refinement) { - super("Invalid Refinement", message, element, null); + super("Invalid Refinement", message, element.getPosition(), element.toString(), 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 806a86b9..12b4c79f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -4,33 +4,27 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; -import spoon.reflect.declaration.CtElement; /** * Base class for all LiquidJava errors */ -public abstract class LJError extends Exception { +public abstract class LJError { private String title; private String message; - private CtElement element; + private String snippet; private ErrorPosition position; private SourcePosition location; private TranslationTable translationTable; - public LJError(String title, String message, CtElement element, TranslationTable translationTable) { - super(message); + public LJError(String title, String message, SourcePosition pos, String snippet, + TranslationTable translationTable) { this.title = title; this.message = message; - this.element = element; + this.snippet = snippet; this.translationTable = translationTable != null ? translationTable : new TranslationTable(); - try { - this.location = element.getPosition(); - this.position = ErrorPosition.fromSpoonPosition(element.getPosition()); - } catch (Exception e) { - this.location = null; - this.position = null; - } + this.location = pos; + this.position = ErrorPosition.fromSpoonPosition(pos); } public String getTitle() { @@ -41,8 +35,8 @@ public String getMessage() { return message; } - public CtElement getElement() { - return element; + public String getSnippet() { + return snippet; } public ErrorPosition getPosition() { @@ -64,8 +58,8 @@ public String toString(String extra) { StringBuilder sb = new StringBuilder(); sb.append(title); - if (element != null) - sb.append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@")); + if (snippet != null) + sb.append(" at: \n").append(snippet.replace("@liquidjava.specification.", "@")); sb.append("\n"); sb.append(message).append("\n"); 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 a6ccb1f9..fda0ddd9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -11,7 +11,7 @@ public class NotFoundError extends LJError { public NotFoundError(CtElement element, String message, TranslationTable translationTable) { - super("Not Found Error", message, element, translationTable); + super("Not Found Error", message, element.getPosition(), element.toString(), translationTable); } @Override 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 345dac55..6451ed3c 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(CtElement element, Predicate expected, ValDerivationNode found, TranslationTable translationTable) { - super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element, - translationTable); + super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), + element.getPosition(), element.toString(), translationTable); this.expected = expected.toString(); 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 57c5c05f..e464349e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -15,7 +15,8 @@ public class StateConflictError extends LJError { private String className; public StateConflictError(CtElement element, Predicate state, String className, 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, 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(), + element.toString(), translationTable); this.state = state.toString(); this.className = 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 aa1f15c3..e5f95d69 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -19,7 +19,8 @@ public class StateRefinementError extends LJError { public StateRefinementError(CtElement element, String method, Predicate[] expected, Predicate found, TranslationTable translationTable) { - super("State Refinement Error", "State refinement transition violation", element, translationTable); + super("State Refinement Error", "State refinement transition violation", element.getPosition(), + element.toString(), translationTable); this.method = method; this.expected = Arrays.stream(expected).map(Predicate::toString).toArray(String[]::new); this.found = found.toString(); 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 3c2c424f..80a7670c 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, CtElement element, String refinement) { - super("Syntax Error", message, element, null); + super("Syntax Error", message, element.getPosition(), element.toString(), null); this.refinement = refinement; } 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 0f0839ae..2a4c17ae 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 @@ -61,7 +61,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl } try { - smtChecking(premises, et); + smtChecking(premises, et, element.getPosition()); } catch (Exception e) { // To emit the message we use the constraints before the alias and state change printError(e, premisesBeforeChange, expectedType, element, map); @@ -236,11 +236,11 @@ private void recAuxGetVars(RefinedVariable var, List newVars) { public boolean smtChecks(Predicate cSMT, Predicate expectedType, SourcePosition p) { try { - new SMTEvaluator().verifySubtype(cSMT, expectedType, context); + new SMTEvaluator().verifySubtype(cSMT, expectedType, context, p); } catch (TypeCheckError e) { return false; } catch (Exception e) { - diagnostics.add(new CustomError(e.getMessage())); + diagnostics.add(new CustomError(e.getMessage(), p)); } return true; } @@ -256,9 +256,9 @@ public boolean smtChecks(Predicate cSMT, Predicate expectedType, SourcePosition * @throws GhostFunctionError * @throws TypeCheckError */ - private void smtChecking(Predicate cSMT, Predicate expectedType) + private void smtChecking(Predicate cSMT, Predicate expectedType, SourcePosition p) throws TypeCheckError, GhostFunctionError, Exception { - new SMTEvaluator().verifySubtype(cSMT, expectedType, context); + new SMTEvaluator().verifySubtype(cSMT, expectedType, context, p); } /** @@ -323,7 +323,8 @@ private LJError mapError(Exception e, Predicate premisesBeforeChange, Predicate if (e instanceof TypeCheckError) { return new RefinementError(element, expectedType, premisesBeforeChange.simplify(), map); } else if (e instanceof GhostFunctionError) { - return new GhostInvocationError(element, expectedType, map); + return new GhostInvocationError("Invalid types or number of arguments in ghost invocation", + element.getPosition(), expectedType, map); } else if (e instanceof NotFoundSMTError) { return new NotFoundError(element, e.getMessage(), map); } else { diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 68dc4862..9eb23e6f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -1,16 +1,21 @@ package liquidjava.smt; +import static liquidjava.diagnostics.LJDiagnostics.diagnostics; + import com.martiansoftware.jsap.SyntaxException; import com.microsoft.z3.Expr; import com.microsoft.z3.Status; import com.microsoft.z3.Z3Exception; + +import liquidjava.diagnostics.errors.GhostInvocationError; import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; +import spoon.reflect.cu.SourcePosition; public class SMTEvaluator { - public void verifySubtype(Predicate subRef, Predicate supRef, Context c) + public void verifySubtype(Predicate subRef, Predicate supRef, Context c, SourcePosition pos) throws TypeCheckError, GhostFunctionError, Exception { // Creates a parser for our SMT-ready refinement language // Discharges the verification to z3 @@ -37,11 +42,11 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c) System.out.println("Could not parse: " + toVerify); e1.printStackTrace(); } catch (Z3Exception e) { - if (e.getLocalizedMessage().substring(0, 24).equals("Wrong number of argument") - || e.getLocalizedMessage().substring(0, 13).equals("Sort mismatch")) - throw new GhostFunctionError(e.getLocalizedMessage()); - else - throw new Z3Exception(e.getLocalizedMessage()); + String msg = e.getLocalizedMessage().toLowerCase(); + if (msg.contains("wrong number of arguments") || msg.contains("sort mismatch")) + diagnostics.add(new GhostInvocationError(msg, pos, supRef, null)); + + throw new Z3Exception(e.getLocalizedMessage()); } } }