diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index b7471a36..dc6aa2b4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -3,7 +3,8 @@ import java.io.File; import java.util.Arrays; import java.util.List; -import liquidjava.errors.ErrorEmitter; + +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.RefinementProcessor; import spoon.Launcher; import spoon.processing.ProcessingManager; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorEmitter.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java similarity index 98% rename from liquidjava-verifier/src/main/java/liquidjava/errors/ErrorEmitter.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java index 0036d320..02610343 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorEmitter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorEmitter.java @@ -1,4 +1,4 @@ -package liquidjava.errors; +package liquidjava.diagnostics; import java.net.URI; import java.util.HashMap; diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java similarity index 99% rename from liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java index 91ab4987..af45af24 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java @@ -1,4 +1,4 @@ -package liquidjava.errors; +package liquidjava.diagnostics; import java.util.Formatter; import java.util.HashMap; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java new file mode 100644 index 00000000..1ee72e7d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java @@ -0,0 +1,40 @@ +package liquidjava.diagnostics; + +import spoon.reflect.cu.SourcePosition; + +public class ErrorPosition { + + private int lineStart; + private int colStart; + private int lineEnd; + private int colEnd; + + public ErrorPosition(int lineStart, int colStart, int lineEnd, int colEnd) { + this.lineStart = lineStart; + this.colStart = colStart; + this.lineEnd = lineEnd; + this.colEnd = colEnd; + } + + public int getLineStart() { + return lineStart; + } + + public int getColStart() { + return colStart; + } + + public int getLineEnd() { + return lineEnd; + } + + public int getColEnd() { + return colEnd; + } + + public static ErrorPosition fromSpoonPosition(SourcePosition pos) { + if (pos == null || !pos.isValidPosition()) + return null; + return new ErrorPosition(pos.getLine(), pos.getColumn(), pos.getEndLine(), pos.getEndColumn()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java new file mode 100644 index 00000000..624ffe65 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java @@ -0,0 +1,93 @@ +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; + +public class LJDiagnostics { + private static LJDiagnostics instance; + + 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 void addError(LJError error) { + this.errors.add(error); + } + + public void addWarning(LJWarning warning) { + this.warnings.add(warning); + } + + public void setTranslationMap(HashMap map) { + this.translationMap = map; + } + + public boolean foundError() { + return !this.errors.isEmpty(); + } + + public boolean foundWarning() { + return !this.warnings.isEmpty(); + } + + public ArrayList getErrors() { + return this.errors; + } + + public ArrayList getWarnings() { + return this.warnings; + } + + public HashMap getTranslationMap() { + return this.translationMap; + } + + public LJError getError() { + return foundError() ? this.errors.get(0) : null; + } + + public LJWarning getWarning() { + return foundWarning() ? this.warnings.get(0) : null; + } + + public void clear() { + this.errors.clear(); + this.warnings.clear(); + this.translationMap.clear(); + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + if (foundError()) { + for (LJError error : errors) { + sb.append(error.toString()).append("\n"); + } + } else { + if (foundWarning()) { + sb.append("Warnings:\n"); + for (LJWarning warning : warnings) { + sb.append(warning.getMessage()).append("\n"); + } + sb.append("Passed Verification!\n"); + } + } + return sb.toString(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java new file mode 100644 index 00000000..7f885e45 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -0,0 +1,18 @@ +package liquidjava.diagnostics.errors; + +/** + * Custom error with an arbitrary message + * + * @see LJError + */ +public class CustomError extends LJError { + + public CustomError(String message) { + super("Found Error", message, null); + } + + @Override + public String toString() { + return super.toString(null); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java new file mode 100644 index 00000000..7d04e28d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java @@ -0,0 +1,30 @@ +package liquidjava.diagnostics.errors; + +import liquidjava.rj_language.Predicate; +import spoon.reflect.declaration.CtElement; + +/** + * Error indicating that a ghost method invocation is invalid (e.g., has wrong arguments) + * + * @see LJError + */ +public class GhostInvocationError extends LJError { + + private Predicate expected; + + public GhostInvocationError(CtElement element, Predicate expected) { + super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element); + this.expected = expected; + } + + public Predicate getExpected() { + return expected; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Expected: ").append(expected.toString()).append("\n"); + return super.toString(sb.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 new file mode 100644 index 00000000..af5f05c6 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java @@ -0,0 +1,21 @@ +package liquidjava.diagnostics.errors; + +import spoon.reflect.declaration.CtElement; + +/** + * Error indicating that a constructor contains a state refinement with a 'from' state, which is not allowed + * + * @see LJError + */ +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); + } + + @Override + public String toString() { + return super.toString(null); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java new file mode 100644 index 00000000..02b41265 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java @@ -0,0 +1,29 @@ +package liquidjava.diagnostics.errors; + +import spoon.reflect.declaration.CtElement; + +/** + * Error indicating that a refinement is invalid (e.g., not a boolean expression) + * + * @see LJError + */ +public class InvalidRefinementError extends LJError { + + private String refinement; + + public InvalidRefinementError(String message, CtElement element, String refinement) { + super("Invalid Refinement", message, element); + this.refinement = refinement; + } + + public String getRefinement() { + return refinement; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Refinement: ").append(refinement).append("\n"); + return super.toString(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 new file mode 100644 index 00000000..6e92057f --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -0,0 +1,67 @@ +package liquidjava.diagnostics.errors; + +import liquidjava.diagnostics.ErrorPosition; +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 { + + private String title; + private String message; + private CtElement element; + private ErrorPosition position; + private SourcePosition location; + + public LJError(String title, String message, CtElement element) { + super(message); + this.title = title; + this.message = message; + this.element = element; + try { + this.location = element.getPosition(); + this.position = ErrorPosition.fromSpoonPosition(element.getPosition()); + } catch (Exception e) { + this.location = null; + this.position = null; + } + } + + public String getTitle() { + return title; + } + + public String getMessage() { + return message; + } + + public CtElement getElement() { + return element; + } + + public ErrorPosition getPosition() { + return position; + } + + public SourcePosition getLocation() { + return location; + } + + @Override + public abstract String toString(); + + 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(message).append("\n"); + if (extra != null) + sb.append(extra).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/diagnostics/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java new file mode 100644 index 00000000..77d1ab1f --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -0,0 +1,20 @@ +package liquidjava.diagnostics.errors; + +import spoon.reflect.declaration.CtElement; + +/** + * Error indicating that an element referenced in a refinement was not found + * + * @see LJError + */ +public class NotFoundError extends LJError { + + public NotFoundError(String message, CtElement element) { + super("Not Found Error", message, element); + } + + @Override + public String toString() { + return super.toString(null); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java new file mode 100644 index 00000000..051e5d95 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -0,0 +1,31 @@ +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; + +/** + * Error indicating that a refinement constraint either was violated or cannot be proven + * + * @see LJError + */ +public class RefinementError extends LJError { + + private Predicate expected; + private ValDerivationNode found; + + public RefinementError(CtElement element, Predicate expected, ValDerivationNode found) { + super("Refinement Error", "Predicate refinement violation", element); + this.expected = expected; + this.found = found; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Expected: ").append(Utils.stripParens(expected.toString())).append("\n"); + sb.append("Found: ").append(found.getValue()); + return super.toString(sb.toString()); + } +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java new file mode 100644 index 00000000..0a9ec435 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -0,0 +1,37 @@ +package liquidjava.diagnostics.errors; + +import liquidjava.rj_language.Predicate; +import spoon.reflect.declaration.CtElement; + +/** + * Error indicating that two disjoint states were found in a state refinement + * + * @see LJError + */ +public class StateConflictError extends LJError { + + private Predicate predicate; + private String className; + + public StateConflictError(CtElement element, Predicate predicate, String className) { + super("State Conflict Error", "Found multiple disjoint states from a StateSet in refinement", element); + this.predicate = predicate; + this.className = className; + } + + public Predicate getPredicate() { + return predicate; + } + + public String getClassName() { + return className; + } + + @Override + 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()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java new file mode 100644 index 00000000..5810946d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -0,0 +1,47 @@ +package liquidjava.diagnostics.errors; + +import java.util.Arrays; + +import spoon.reflect.declaration.CtElement; + +/** + * Error indicating that a state refinement transition was violated + * + * @see LJError + */ +public class StateRefinementError extends LJError { + + private final String method; + 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); + this.method = method; + this.expected = expected; + this.found = found; + } + + public String getMethod() { + return method; + } + + public String[] getExpected() { + return expected; + } + + public String getFound() { + return found; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Method: ").append(method).append("\n"); + sb.append("Expected: "); + Arrays.stream(expected).forEach(s -> sb.append(s).append(", ")); + sb.append("\n"); + sb.append("Found: ").append(found); + return super.toString(sb.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 new file mode 100644 index 00000000..ba679cc6 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java @@ -0,0 +1,33 @@ +package liquidjava.diagnostics.errors; + +import spoon.reflect.declaration.CtElement; + +/** + * Error indicating that the syntax of a refinement is invalid + * + * @see LJError + */ +public class SyntaxError extends LJError { + + private String refinement; + + public SyntaxError(String message, String refinement) { + this(message, null, refinement); + } + + public SyntaxError(String message, CtElement element, String refinement) { + super("Syntax Error", message, element); + this.refinement = refinement; + } + + public String getRefinement() { + return refinement; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Invalid syntax in refinement: ").append(refinement); + return super.toString(sb.toString()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java new file mode 100644 index 00000000..6a4eef29 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java @@ -0,0 +1,29 @@ +package liquidjava.diagnostics.warnings; + +import spoon.reflect.declaration.CtElement; + +/** + * Warning indicating that a class referenced in an external refinement was not found + * + * @see LJWarning + */ +public class ExternalClassNotFoundWarning extends LJWarning { + + private String className; + + public ExternalClassNotFoundWarning(CtElement element, String className) { + super("Class in external refinement not found", element); + this.className = className; + } + + public String getClassName() { + return className; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Class: ").append(className); + return super.toString(sb.toString()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java new file mode 100644 index 00000000..eee01505 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java @@ -0,0 +1,36 @@ +package liquidjava.diagnostics.warnings; + +import spoon.reflect.declaration.CtElement; + +/** + * Warning indicating that a method referenced in an external refinement was not found + * + * @see LJWarning + */ +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); + this.methodName = methodName; + this.className = className; + } + + public String getMethodName() { + return methodName; + } + + public String getClassName() { + return className; + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + sb.append("Class: ").append(className).append("\n"); + sb.append("Method: ").append(methodName); + return super.toString(sb.toString()); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java new file mode 100644 index 00000000..7cf59dd9 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java @@ -0,0 +1,60 @@ +package liquidjava.diagnostics.warnings; + +import liquidjava.diagnostics.ErrorPosition; +import liquidjava.utils.Utils; +import spoon.reflect.cu.SourcePosition; +import spoon.reflect.declaration.CtElement; + +/** + * Base class for all LiquidJava warnings + */ +public abstract class LJWarning { + + private String message; + private CtElement element; + private ErrorPosition position; + private SourcePosition location; + + public LJWarning(String message, CtElement element) { + this.message = message; + this.element = element; + try { + this.location = element.getPosition(); + this.position = ErrorPosition.fromSpoonPosition(element.getPosition()); + } catch (Exception e) { + // This warning is from a generated part of the source code, so no precise position is provided + this.location = null; + this.position = null; + } + } + + public String getMessage() { + return message; + } + + public CtElement getElement() { + return element; + } + + public ErrorPosition getPosition() { + return position; + } + + public SourcePosition getLocation() { + return location; + } + + @Override + public abstract String toString(); + + public String toString(String extra) { + StringBuilder sb = new StringBuilder(); + sb.append(message).append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@")) + .append("\n\n"); + if (extra != null) + sb.append(extra).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/errors/ErrorPosition.java b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorPosition.java deleted file mode 100644 index a7afd433..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorPosition.java +++ /dev/null @@ -1,33 +0,0 @@ -package liquidjava.errors; - -public class ErrorPosition { - - private int lineStart; - private int colStart; - - private int lineEnd; - private int colEnd; - - public ErrorPosition(int line1, int col1, int line2, int col2) { - lineStart = line1; - colStart = col1; - lineEnd = line2; - colEnd = col2; - } - - public int getLineStart() { - return lineStart; - } - - public int getColStart() { - return colStart; - } - - public int getLineEnd() { - return lineEnd; - } - - public int getColEnd() { - return colEnd; - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java index 2e168f76..46069f40 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java @@ -2,7 +2,8 @@ import java.util.ArrayList; import java.util.List; -import liquidjava.errors.ErrorEmitter; + +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.ann_generation.FieldGhostsGeneration; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.ExternalRefinementTypeChecker; 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 4e8b3987..dbe672f5 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,6 @@ package liquidjava.processor.ann_generation; -import liquidjava.errors.ErrorEmitter; +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.context.Context; import liquidjava.specification.Ghost; import spoon.reflect.declaration.*; 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 6b149ca9..cb218d7e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java @@ -4,7 +4,8 @@ import java.util.HashMap; import java.util.List; import java.util.Map; -import liquidjava.errors.ErrorEmitter; + +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.facade.AliasDTO; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; 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 111ee2de..8580135b 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 @@ -4,10 +4,9 @@ import java.util.List; import java.util.Optional; import java.util.stream.Collectors; -import java.util.stream.Stream; -import liquidjava.errors.ErrorEmitter; -import liquidjava.errors.ErrorHandler; +import liquidjava.diagnostics.ErrorEmitter; +import liquidjava.diagnostics.ErrorHandler; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.facade.GhostDTO; 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 b4224d3b..92cadcf5 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 @@ -2,7 +2,8 @@ import java.util.ArrayList; import java.util.List; -import liquidjava.errors.ErrorEmitter; + +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import liquidjava.rj_language.parsing.ParsingException; 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 6d46a535..ef6f2c55 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 @@ -4,7 +4,8 @@ import java.util.Arrays; import java.util.List; import java.util.Optional; -import liquidjava.errors.ErrorEmitter; + +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import liquidjava.processor.refinement_checker.general_checkers.OperationsChecker; 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 6be78523..8b714d29 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 @@ -4,8 +4,9 @@ import java.util.Arrays; import java.util.List; import java.util.Optional; -import liquidjava.errors.ErrorEmitter; -import liquidjava.errors.ErrorHandler; + +import liquidjava.diagnostics.ErrorEmitter; +import liquidjava.diagnostics.ErrorHandler; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; 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 458ae4da..fcded1ce 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 @@ -8,8 +8,9 @@ import java.util.function.Consumer; import java.util.regex.Pattern; import java.util.stream.Collectors; -import liquidjava.errors.ErrorEmitter; -import liquidjava.errors.ErrorHandler; + +import liquidjava.diagnostics.ErrorEmitter; +import liquidjava.diagnostics.ErrorHandler; import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; import liquidjava.rj_language.Predicate; 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 99f13890..0bd255f1 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 @@ -3,7 +3,8 @@ import java.lang.annotation.Annotation; import java.util.*; import java.util.stream.Collectors; -import liquidjava.errors.ErrorHandler; + +import liquidjava.diagnostics.ErrorHandler; import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.processor.refinement_checker.TypeCheckingUtils; 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 62284b25..0b57ac50 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java @@ -1,6 +1,6 @@ package liquidjava.rj_language; -import liquidjava.errors.ErrorEmitter; +import liquidjava.diagnostics.ErrorEmitter; import liquidjava.rj_language.parsing.ParsingException; import spoon.reflect.declaration.CtElement; 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 7fb7fa94..1f476f15 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -5,8 +5,9 @@ import java.util.List; import java.util.Map; import java.util.stream.Collectors; -import liquidjava.errors.ErrorEmitter; -import liquidjava.errors.ErrorHandler; + +import liquidjava.diagnostics.ErrorEmitter; +import liquidjava.diagnostics.ErrorHandler; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostState; diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 008879cb..6c204258 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -69,4 +69,8 @@ public static String qualifyName(String prefix, String name) { return name; // dont qualify return String.format("%s.%s", prefix, name); } + + public static String stripParens(String s) { + return s.startsWith("(") && s.endsWith(")") ? s.substring(1, s.length() - 1) : s; + } } 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 a1c627f9..7f216a32 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -8,7 +8,7 @@ import java.nio.file.Paths; import java.util.stream.Stream; import liquidjava.api.CommandLineLauncher; -import liquidjava.errors.ErrorEmitter; +import liquidjava.diagnostics.ErrorEmitter; import org.junit.Test; import org.junit.jupiter.params.ParameterizedTest;