Add Diagnostics Classes

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;

liquidjava-verifier/src/main/java/liquidjava/errors/ErrorEmitter.java → 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;

liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java → 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;

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());
+    }
+}

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<LJError> errors;
+    private ArrayList<LJWarning> warnings;
+    private HashMap<String, PlacementInCode> 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<String, PlacementInCode> map) {
+        this.translationMap = map;
+    }
+
+    public boolean foundError() {
+        return !this.errors.isEmpty();
+    }
+
+    public boolean foundWarning() {
+        return !this.warnings.isEmpty();
+    }
+
+    public ArrayList<LJError> getErrors() {
+        return this.errors;
+    }
+
+    public ArrayList<LJWarning> getWarnings() {
+        return this.warnings;
+    }
+
+    public HashMap<String, PlacementInCode> 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();
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java

@@ -0,0 +1,13 @@
+package liquidjava.diagnostics.errors;
+
+public class CustomError extends LJError {
+
+    public CustomError(String message) {
+        super("Found Error", message, null);
+    }
+
+    @Override
+    public String toString() {
+        return super.toString(null);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java

@@ -0,0 +1,26 @@
+package liquidjava.diagnostics.errors;
+
+import liquidjava.rj_language.Predicate;
+import spoon.reflect.declaration.CtElement;
+
+// when a ghost call has wrong types or number of arguments
+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());
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java

@@ -0,0 +1,17 @@
+package liquidjava.diagnostics.errors;
+
+import spoon.reflect.declaration.CtElement;
+
+// when a constructor contains a @StateRefinement with a from state
+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);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java

@@ -0,0 +1,25 @@
+package liquidjava.diagnostics.errors;
+
+import spoon.reflect.declaration.CtElement;
+
+// when a refinement is invalid, e.g. is not a boolean expression
+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());
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java

@@ -0,0 +1,65 @@
+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()) : "<unknown>")
+                .append("\n");
+        return sb.toString();
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java

@@ -0,0 +1,16 @@
+package liquidjava.diagnostics.errors;
+
+import spoon.reflect.declaration.CtElement;
+
+// e.g. when a variable used in a refinement is not found
+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);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -0,0 +1,27 @@
+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;
+
+// when a @Refinement is violated
+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());
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java

@@ -0,0 +1,33 @@
+package liquidjava.diagnostics.errors;
+
+import liquidjava.rj_language.Predicate;
+import spoon.reflect.declaration.CtElement;
+
+// when two incompatible states are found in a state set
+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());
+    }
+}