Refactor Diagnostics

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/CustomError.java

@@ -0,0 +1,8 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.StateSet;
+
+@StateSet({"Open", "Closed"})
+public class CustomError {
+
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/GhostInvocationError.java

@@ -0,0 +1,11 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("int size")
+public class GhostInvocationError {
+
+    @StateRefinement(to="size(this, this) == 0")
+    public void test() {}
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/IllegalConstructorTransitionError.java

@@ -0,0 +1,11 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class IllegalConstructorTransitionError {
+
+    @StateRefinement(from="open(this)", to="closed(this)")
+    public IllegalConstructorTransitionError() {}
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/InvalidRefinementError.java

@@ -0,0 +1,10 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.Refinement;
+
+public class InvalidRefinementError {
+    public static void main(String[] args) {
+        @Refinement("_ + 1")
+        int x = 5;
+    }
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/NotFoundError.java

@@ -0,0 +1,11 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.Refinement;
+
+public class NotFoundError {
+
+    public static void main(String[] args) {
+        @Refinement("x > 0")
+        int y = 1;
+    }
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/RefinementError.java

@@ -0,0 +1,11 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.Refinement;
+
+public class RefinementError {
+
+    public static void main(String[] args) {
+        @Refinement("x > 0")
+        int x = -1;
+    }
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateConflictError.java

@@ -0,0 +1,14 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class StateConflictError {
+
+    @StateRefinement(to="open(this)")
+    public StateConflictError() {}
+
+    @StateRefinement(from="open(this) && closed(this)")
+    public void close() {}
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateRefinementError.java

@@ -0,0 +1,20 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class StateRefinementError {
+
+    @StateRefinement(to="open(this)")
+    public StateRefinementError() {}
+
+    @StateRefinement(from="!closed(this)", to="closed(this)")
+    public void close() {}
+
+    public static void main(String[] args) {
+        StateRefinementError s = new StateRefinementError();
+        s.close();
+        s.close();
+    }
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/SyntaxError.java

@@ -0,0 +1,11 @@
+package testingInProgress.diagnostics.errors;
+
+import liquidjava.specification.Refinement;
+
+public class SyntaxError {
+
+    public static void main(String[] args) {
+        @Refinement("x $ 0")
+        int x = -1;
+    }
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentClass.java

@@ -0,0 +1,8 @@
+package testingInProgress.diagnostics.warnings;
+
+import liquidjava.specification.ExternalRefinementsFor;
+
+@ExternalRefinementsFor("non.existent.Class")
+public interface NonExistentClass {
+    public void NonExistentClass(); 
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentConstructor.java

@@ -0,0 +1,16 @@
+package testingInProgress.diagnostics.warnings;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.RefinementPredicate;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+public interface NonExistentConstructor<E> {
+
+    @RefinementPredicate("int size(ArrayList l)")
+    @StateRefinement(to = "size(this) == 0")
+    public void ArrayList(String wrongParameter);
+
+    @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
+    public boolean add(E e);
+}

liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentMethod.java

@@ -0,0 +1,16 @@
+package testingInProgress.diagnostics.warnings;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.RefinementPredicate;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+public interface NonExistentMethod<E> {
+
+    @RefinementPredicate("int size(ArrayList l)")
+    @StateRefinement(to = "size(this) == 0")
+    public void ArrayList();
+
+    @StateRefinement(to = "size(this) == (size(old(this)) + 1)")
+    public boolean add(String e);
+}

liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java

@@ -1,6 +1,6 @@
 package liquidjava.api;
 
-import static liquidjava.diagnostics.LJDiagnostics.diagnostics;
+import static liquidjava.diagnostics.Diagnostics.diagnostics;
 
 import java.io.File;
 import java.util.Arrays;

liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java

@@ -0,0 +1,12 @@
+package liquidjava.diagnostics;
+
+// ANSI color codes
+public class Colors {
+    public static final String RESET = "\u001B[0m";
+    public static final String BOLD = "\u001B[1m";
+    public static final String GREY = "\u001B[90m";
+    public static final String RED = "\u001B[31m";
+    public static final String BOLD_RED = "\u001B[1;31m";
+    public static final String YELLOW = "\u001B[33m";
+    public static final String BOLD_YELLOW = "\u001B[1;33m";
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java → liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java

@@ -10,23 +10,25 @@
  * @see LJError
  * @see LJWarning
  */
-public class LJDiagnostics {
-    public static final LJDiagnostics diagnostics = new LJDiagnostics();
+public class Diagnostics {
+    public static final Diagnostics diagnostics = new Diagnostics();
 
     private ArrayList<LJError> errors;
     private ArrayList<LJWarning> warnings;
 
-    private LJDiagnostics() {
+    private Diagnostics() {
         this.errors = new ArrayList<>();
         this.warnings = new ArrayList<>();
     }
 
     public void add(LJError error) {
-        this.errors.add(error);
+        if (!this.errors.contains(error))
+            this.errors.add(error);
     }
 
     public void add(LJWarning warning) {
-        this.warnings.add(warning);
+        if (!this.warnings.contains(warning))
+            this.warnings.add(warning);
     }
 
     public boolean foundError() {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java

@@ -37,4 +37,24 @@ public static ErrorPosition fromSpoonPosition(SourcePosition pos) {
             return null;
         return new ErrorPosition(pos.getLine(), pos.getColumn(), pos.getEndLine(), pos.getEndColumn());
     }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        if (obj == null || getClass() != obj.getClass())
+            return false;
+        ErrorPosition other = (ErrorPosition) obj;
+        return lineStart == other.lineStart && colStart == other.colStart && lineEnd == other.lineEnd
+                && colEnd == other.colEnd;
+    }
+
+    @Override
+    public int hashCode() {
+        int result = lineStart;
+        result = 31 * result + colStart;
+        result = 31 * result + lineEnd;
+        result = 31 * result + colEnd;
+        return result;
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -0,0 +1,144 @@
+package liquidjava.diagnostics;
+
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.List;
+
+import spoon.reflect.cu.SourcePosition;
+
+public class LJDiagnostic {
+
+    private String title;
+    private String message;
+    private String details;
+    private String file;
+    private ErrorPosition position;
+    private String accentColor;
+
+    public LJDiagnostic(String title, String message, String details, SourcePosition pos, String accentColor) {
+        this.title = title;
+        this.message = message;
+        this.details = details;
+        this.file = pos != null ? pos.getFile().getPath() : null;
+        this.position = ErrorPosition.fromSpoonPosition(pos);
+        this.accentColor = accentColor;
+    }
+
+    public String getTitle() {
+        return title;
+    }
+
+    public String getMessage() {
+        return message;
+    }
+
+    public String getDetails() {
+        return details;
+    }
+
+    public ErrorPosition getPosition() {
+        return position;
+    }
+
+    public String getFile() {
+        return file;
+    }
+
+    @Override
+    public String toString() {
+        StringBuilder sb = new StringBuilder();
+
+        // title
+        sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message)
+                .append("\n");
+
+        // snippet
+        String snippet = getSnippet();
+        if (snippet != null) {
+            sb.append(snippet);
+        }
+
+        // details
+        if (details != null && !details.isEmpty()) {
+            sb.append(" --> ").append(String.join("\n     ", details.split("\n"))).append("\n");
+        }
+
+        // location
+        if (file != null && position != null) {
+            sb.append("\n").append(file).append(":").append(position.getLineStart()).append(Colors.RESET).append("\n");
+        }
+
+        return sb.toString();
+    }
+
+    public String getSnippet() {
+        if (file == null || position == null)
+            return null;
+
+        Path path = Path.of(file);
+        try {
+            List<String> lines = Files.readAllLines(path);
+            StringBuilder sb = new StringBuilder();
+
+            // before and after lines for context
+            int contextBefore = 2;
+            int contextAfter = 2;
+            int startLine = Math.max(1, position.getLineStart() - contextBefore);
+            int endLine = Math.min(lines.size(), position.getLineEnd() + contextAfter);
+
+            // calculate padding for line numbers
+            int maxLineNum = endLine;
+            int padding = String.valueOf(maxLineNum).length();
+
+            for (int i = startLine; i <= endLine; i++) {
+                String lineNumStr = String.format("%" + padding + "d", i);
+                String line = lines.get(i - 1);
+
+                // add line
+                sb.append(Colors.GREY).append(lineNumStr).append(" | ").append(line).append(Colors.RESET).append("\n");
+
+                // add error markers on the line(s) with the error
+                if (i >= position.getLineStart() && i <= position.getLineEnd()) {
+                    int colStart = (i == position.getLineStart()) ? position.getColStart() : 1;
+                    int colEnd = (i == position.getLineEnd()) ? position.getColEnd() : line.length();
+
+                    if (colStart > 0 && colEnd > 0) {
+                        // line number padding + " | " + column offset
+                        String indent = " ".repeat(padding) + Colors.GREY + " | " + Colors.RESET
+                                + " ".repeat(colStart - 1);
+                        String markers = accentColor + "^".repeat(Math.max(1, colEnd - colStart + 1)) + Colors.RESET;
+                        sb.append(indent).append(markers).append("\n");
+                    }
+                }
+            }
+            return sb.toString();
+        } catch (Exception e) {
+            e.printStackTrace();
+            return null;
+        }
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        if (obj == null || getClass() != obj.getClass())
+            return false;
+        LJDiagnostic other = (LJDiagnostic) obj;
+        return title.equals(other.title) && message.equals(other.message)
+                && ((details == null && other.details == null) || (details != null && details.equals(other.details)))
+                && ((file == null && other.file == null) || (file != null && file.equals(other.file)))
+                && ((position == null && other.position == null)
+                        || (position != null && position.equals(other.position)));
+    }
+
+    @Override
+    public int hashCode() {
+        int result = title.hashCode();
+        result = 31 * result + message.hashCode();
+        result = 31 * result + (details != null ? details.hashCode() : 0);
+        result = 31 * result + (file != null ? file.hashCode() : 0);
+        result = 31 * result + (position != null ? position.hashCode() : 0);
+        return result;
+    }
+}