diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/CustomError.java b/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/CustomError.java new file mode 100644 index 00000000..953c56ef --- /dev/null +++ b/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 { + +} diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/GhostInvocationError.java b/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/GhostInvocationError.java new file mode 100644 index 00000000..db4bcd57 --- /dev/null +++ b/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() {} +} diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/IllegalConstructorTransitionError.java b/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/IllegalConstructorTransitionError.java new file mode 100644 index 00000000..dcfacf93 --- /dev/null +++ b/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() {} +} diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/InvalidRefinementError.java b/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/InvalidRefinementError.java new file mode 100644 index 00000000..92ed8dbd --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/NotFoundError.java b/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/NotFoundError.java new file mode 100644 index 00000000..ff22cc9b --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/RefinementError.java b/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/RefinementError.java new file mode 100644 index 00000000..25dac068 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateConflictError.java b/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateConflictError.java new file mode 100644 index 00000000..9701ff05 --- /dev/null +++ b/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() {} +} diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateRefinementError.java b/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateRefinementError.java new file mode 100644 index 00000000..6e4aa8fb --- /dev/null +++ b/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(); + } +} diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/SyntaxError.java b/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/SyntaxError.java new file mode 100644 index 00000000..87953608 --- /dev/null +++ b/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; + } +} diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentClass.java b/liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentClass.java new file mode 100644 index 00000000..f4eb3ebe --- /dev/null +++ b/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(); +} diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentConstructor.java b/liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentConstructor.java new file mode 100644 index 00000000..c4a5f4d5 --- /dev/null +++ b/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 { + + @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); +} diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentMethod.java b/liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentMethod.java new file mode 100644 index 00000000..af7237f1 --- /dev/null +++ b/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 { + + @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); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 8b925819..b1187271 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/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; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java new file mode 100644 index 00000000..ff669fec --- /dev/null +++ b/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"; +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java similarity index 87% rename from liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java rename to liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java index 211115be..dd69be2e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java +++ b/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 errors; private ArrayList 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() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java index 1ee72e7d..354e8680 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java +++ b/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; + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java new file mode 100644 index 00000000..db48c8a9 --- /dev/null +++ b/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 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; + } +} 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 e02b8c9f..b9a5baca 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -11,19 +11,18 @@ public class CustomError extends LJError { public CustomError(String message) { - super("Found Error", message, null, null, null); + super("Error", message, null, null, null); } public CustomError(String message, SourcePosition pos) { - super("Found Error", message, pos, null, null); + super("Error", message, null, pos, null); } - public CustomError(CtElement element, String message) { - super("Found Error", message, element.getPosition(), element.toString(), null); + public CustomError(String message, String detail, CtElement element) { + super("Error", message, detail, element.getPosition(), null); } - @Override - public String toString() { - return super.toString(null); + public CustomError(String message, CtElement element) { + super("Error", message, null, element.getPosition(), 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 index 2b539c9b..73a933aa 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java @@ -1,7 +1,7 @@ package liquidjava.diagnostics.errors; import liquidjava.diagnostics.TranslationTable; -import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; import spoon.reflect.cu.SourcePosition; /** @@ -13,20 +13,13 @@ public class GhostInvocationError extends LJError { private String expected; - public GhostInvocationError(String message, SourcePosition pos, Predicate expected, + public GhostInvocationError(String message, SourcePosition pos, Expression expected, TranslationTable translationTable) { - super("Ghost Invocation Error", message, pos, null, translationTable); - this.expected = expected.toString(); + super("Ghost Invocation Error", message, "", pos, translationTable); + this.expected = expected.toSimplifiedString(); } public String getExpected() { return expected; } - - @Override - public String toString() { - StringBuilder sb = new StringBuilder(); - sb.append("Expected: ").append(expected).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 index 11908a6b..6ef5f6d7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java @@ -10,13 +10,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.getPosition(), - element.toString(), null); - } - - @Override - public String toString() { - return super.toString(null); + super("Illegal Constructor Transition Error", "Found constructor with 'from' state", + "Constructor methods should only have a 'to' state", element.getPosition(), null); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java index 03c55813..96cc272d 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; /** @@ -12,18 +13,11 @@ public class InvalidRefinementError extends LJError { private String refinement; public InvalidRefinementError(CtElement element, String message, String refinement) { - super("Invalid Refinement", message, element.getPosition(), element.toString(), null); + super("Invalid Refinement", message, "", element.getPosition(), null); 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 index 12b4c79f..446dea22 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -1,72 +1,24 @@ package liquidjava.diagnostics.errors; -import liquidjava.diagnostics.ErrorPosition; +import liquidjava.diagnostics.LJDiagnostic; import liquidjava.diagnostics.TranslationTable; -import liquidjava.utils.Utils; +import liquidjava.diagnostics.Colors; import spoon.reflect.cu.SourcePosition; /** * Base class for all LiquidJava errors */ -public abstract class LJError { +public abstract class LJError extends LJDiagnostic { - private String title; - private String message; - private String snippet; - private ErrorPosition position; - private SourcePosition location; private TranslationTable translationTable; - public LJError(String title, String message, SourcePosition pos, String snippet, + public LJError(String title, String message, String details, SourcePosition pos, TranslationTable translationTable) { - this.title = title; - this.message = message; - this.snippet = snippet; + super(title, message, details, pos, Colors.BOLD_RED); this.translationTable = translationTable != null ? translationTable : new TranslationTable(); - this.location = pos; - this.position = ErrorPosition.fromSpoonPosition(pos); - } - - public String getTitle() { - return title; - } - - public String getMessage() { - return message; - } - - public String getSnippet() { - return snippet; - } - - public ErrorPosition getPosition() { - return position; - } - - public SourcePosition getLocation() { - return location; } public TranslationTable getTranslationTable() { return translationTable; } - - @Override - public abstract String toString(); - - public String toString(String extra) { - StringBuilder sb = new StringBuilder(); - sb.append(title); - - if (snippet != null) - sb.append(" at: \n").append(snippet.replace("@liquidjava.specification.", "@")); - - sb.append("\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 index fda0ddd9..9af41e49 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -11,11 +11,6 @@ public class NotFoundError extends LJError { public NotFoundError(CtElement element, String message, TranslationTable translationTable) { - super("Not Found Error", message, element.getPosition(), element.toString(), translationTable); - } - - @Override - public String toString() { - return super.toString(null); + super("Not Found Error", message, "", element.getPosition(), translationTable); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 6451ed3c..72172934 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,9 +1,8 @@ package liquidjava.diagnostics.errors; import liquidjava.diagnostics.TranslationTable; -import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; -import liquidjava.utils.Utils; import spoon.reflect.declaration.CtElement; /** @@ -16,11 +15,12 @@ public class RefinementError extends LJError { private String expected; private ValDerivationNode found; - public RefinementError(CtElement element, Predicate expected, ValDerivationNode found, + public RefinementError(CtElement element, Expression expected, ValDerivationNode found, TranslationTable 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(); + super("Refinement Error", + String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), "", + element.getPosition(), translationTable); + this.expected = expected.toSimplifiedString(); this.found = found; } @@ -31,12 +31,4 @@ public String getExpected() { public ValDerivationNode getFound() { return found; } - - @Override - public String toString() { - StringBuilder sb = new StringBuilder(); - sb.append("Expected: ").append(Utils.stripParens(expected)).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 index e464349e..fd250e49 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -1,7 +1,7 @@ package liquidjava.diagnostics.errors; import liquidjava.diagnostics.TranslationTable; -import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; import spoon.reflect.declaration.CtElement; /** @@ -14,10 +14,11 @@ public class StateConflictError extends LJError { private String state; 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.getPosition(), - element.toString(), translationTable); - this.state = state.toString(); + public StateConflictError(CtElement element, Expression 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.getPosition(), translationTable); + this.state = state.toSimplifiedString(); this.className = className; } @@ -28,12 +29,4 @@ public String getState() { public String getClassName() { return className; } - - @Override - 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 e5f95d69..013c64d2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -3,7 +3,7 @@ import java.util.Arrays; import liquidjava.diagnostics.TranslationTable; -import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.Expression; import spoon.reflect.declaration.CtElement; /** @@ -17,13 +17,17 @@ public class StateRefinementError extends LJError { private final String[] expected; private final String found; - public StateRefinementError(CtElement element, String method, Predicate[] expected, Predicate found, + public StateRefinementError(CtElement element, String method, Expression[] expected, Expression found, TranslationTable translationTable) { - super("State Refinement Error", "State refinement transition violation", element.getPosition(), - element.toString(), translationTable); + super("State Refinement Error", "State refinement transition violation", + String.format("Expected: %s\nFound: %s", + String.join(", ", + Arrays.stream(expected).map(Expression::toSimplifiedString).toArray(String[]::new)), + found.toSimplifiedString()), + element.getPosition(), translationTable); this.method = method; - this.expected = Arrays.stream(expected).map(Predicate::toString).toArray(String[]::new); - this.found = found.toString(); + this.expected = Arrays.stream(expected).map(Expression::toSimplifiedString).toArray(String[]::new); + this.found = found.toSimplifiedString(); } public String getMethod() { @@ -37,15 +41,4 @@ public String[] getExpected() { 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 index 80a7670c..1cf7101a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java @@ -1,6 +1,6 @@ package liquidjava.diagnostics.errors; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Error indicating that the syntax of a refinement is invalid @@ -15,19 +15,12 @@ public SyntaxError(String message, String refinement) { this(message, null, refinement); } - public SyntaxError(String message, CtElement element, String refinement) { - super("Syntax Error", message, element.getPosition(), element.toString(), null); + public SyntaxError(String message, SourcePosition pos, String refinement) { + super("Syntax Error", message, "", pos, null); 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 index 95f0d121..7fcbc468 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java @@ -12,18 +12,11 @@ public class ExternalClassNotFoundWarning extends LJWarning { private String className; public ExternalClassNotFoundWarning(CtElement element, String message, String className) { - super(message, element); + super(message, "", element.getPosition()); 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 index 6ea00388..4f90e994 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,9 @@ public class ExternalMethodNotFoundWarning extends LJWarning { private String methodName; private String className; - public ExternalMethodNotFoundWarning(CtElement element, String message, String methodName, String className) { - super(message, element); + public ExternalMethodNotFoundWarning(CtElement element, String message, String details, String methodName, + String className) { + super(message, details, element.getPosition()); this.methodName = methodName; this.className = className; } @@ -25,12 +26,4 @@ public String getMethodName() { 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 index 8cecc0c7..4ad3438a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java @@ -1,65 +1,15 @@ package liquidjava.diagnostics.warnings; -import liquidjava.diagnostics.ErrorPosition; -import liquidjava.utils.Utils; +import liquidjava.diagnostics.Colors; +import liquidjava.diagnostics.LJDiagnostic; import spoon.reflect.cu.SourcePosition; -import spoon.reflect.declaration.CtElement; /** * Base class for all LiquidJava warnings */ -public abstract class LJWarning { +public abstract class LJWarning extends LJDiagnostic { - 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); - - if (element != null) - sb.append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@")); - - if (extra != null) - sb.append("\n").append(extra); - - sb.append("\n"); - sb.append("Location: ").append(location != null ? Utils.stripParens(location.toString()) : "") - .append("\n"); - return sb.toString(); + public LJWarning(String message, String details, SourcePosition pos) { + super("Warning", message, details, pos, Colors.BOLD_YELLOW); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java index 75b8edc5..5254f494 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java @@ -1,7 +1,5 @@ package liquidjava.processor; -import static liquidjava.diagnostics.LJDiagnostics.diagnostics; - import java.util.ArrayList; import java.util.List; @@ -32,14 +30,9 @@ public void process(CtPackage pkg) { c.reinitializeAllContext(); 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)); pkg.accept(new MethodsFirstChecker(c, factory)); // double passing idea (instead of headers) - 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 719e6d40..12b6b49f 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 static liquidjava.diagnostics.LJDiagnostics.diagnostics; +import static liquidjava.diagnostics.Diagnostics.diagnostics; import liquidjava.processor.context.Context; import liquidjava.specification.Ghost; 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 bd825c8f..ce05d7db 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,6 +1,6 @@ package liquidjava.processor.refinement_checker; -import static liquidjava.diagnostics.LJDiagnostics.diagnostics; +import static liquidjava.diagnostics.Diagnostics.diagnostics; import java.util.Arrays; import java.util.List; @@ -48,7 +48,7 @@ public void visitCtInterface(CtInterface intrface) { if (externalRefinements.isPresent()) { this.prefix = externalRefinements.get(); if (!classExists(prefix)) { - String message = String.format("Could not find external class '%s'", prefix); + String message = String.format("Could not find class '%s'", prefix); diagnostics.add(new ExternalClassNotFoundWarning(intrface, message, prefix)); return; } @@ -89,21 +89,24 @@ public void visitCtMethod(CtMethod method) { boolean isConstructor = method.getSimpleName().equals(targetType.getSimpleName()); if (isConstructor) { if (!constructorExists(targetType, method)) { - String title = String.format("Could not find constructor '%s' for '%s'", method.getSignature(), prefix); + String message = 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); + String details = overloads.length == 0 ? null + : "Available constructors:\n " + String.join("\n ", overloads); - diagnostics.add(new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix)); + diagnostics.add( + new ExternalMethodNotFoundWarning(method, message, details, 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 message = 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)); + String details = overloads.length == 0 ? null + : "Available overloads:\n " + String.join("\n ", overloads); + diagnostics.add( + new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), prefix)); return; } } @@ -127,7 +130,7 @@ protected void getGhostFunction(String value, CtElement element) { } } catch (ParsingException e) { - diagnostics.add(new CustomError(element, "Could not parse the ghost function" + e.getMessage())); + diagnostics.add(new CustomError("Could not parse the ghost function", e.getMessage(), element)); } } 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 6e84985d..c4d97695 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,6 +1,6 @@ package liquidjava.processor.refinement_checker; -import static liquidjava.diagnostics.LJDiagnostics.diagnostics; +import static liquidjava.diagnostics.Diagnostics.diagnostics; import java.util.ArrayList; import java.util.List; 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 2365d9b9..6c20c816 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,6 +1,6 @@ package liquidjava.processor.refinement_checker; -import static liquidjava.diagnostics.LJDiagnostics.diagnostics; +import static liquidjava.diagnostics.Diagnostics.diagnostics; import java.lang.annotation.Annotation; import java.util.Arrays; 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 ebce5070..7b06b3c3 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,6 +1,6 @@ package liquidjava.processor.refinement_checker; -import static liquidjava.diagnostics.LJDiagnostics.diagnostics; +import static liquidjava.diagnostics.Diagnostics.diagnostics; import java.lang.annotation.Annotation; import java.util.Arrays; @@ -20,6 +20,7 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.ParsingException; import liquidjava.rj_language.parsing.RefinementsParser; +import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import liquidjava.utils.constants.Types; @@ -86,7 +87,6 @@ public Optional getRefinementFromAnnotation(CtElement element) throws if (!p.getExpression().isBooleanExpression()) { diagnostics.add(new InvalidRefinementError(element, "Refinement predicate must be a boolean expression", ref.get())); - return Optional.empty(); } if (diagnostics.foundError()) return Optional.empty(); @@ -121,8 +121,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) { CtLiteral s = (CtLiteral) ce; String f = s.getValue(); if (Character.isUpperCase(f.charAt(0))) { - diagnostics - .add(new CustomError(s, String.format("State name must start with lowercase in '%s'", f))); + diagnostics.add(new CustomError("State names must start with lowercase", s)); } } } @@ -163,12 +162,12 @@ private void createStateGhost(String string, CtAnnotation try { gd = RefinementsParser.getGhostDeclaration(string); } catch (ParsingException e) { - diagnostics.add(new CustomError(ann, "Could not parse the ghost function " + e.getMessage())); + diagnostics.add(new CustomError("Could not parse the ghost function", e.getMessage(), ann)); return; } if (gd.getParam_types().size() > 0) { - diagnostics.add(new CustomError(ann, "Ghost States have the class as parameter " - + "by default, no other parameters are allowed in '" + string + "'")); + diagnostics.add(new CustomError( + "Ghost States have the class as parameter " + "by default, no other parameters are allowed", ann)); return; } // Set class as parameter of Ghost @@ -226,7 +225,7 @@ protected void getGhostFunction(String value, CtElement element) { context.addGhostFunction(gh); } } catch (ParsingException e) { - diagnostics.add(new CustomError(element, "Could not parse the ghost function " + e.getMessage())); + diagnostics.add(new CustomError("Could not parse the ghost function", e.getMessage(), element)); // e.printStackTrace(); return; } @@ -256,7 +255,8 @@ protected void handleAlias(String value, CtElement element) { context.addAlias(aw); } } catch (ParsingException e) { - diagnostics.add(new SyntaxError(e.getMessage(), element, value)); + SourcePosition pos = Utils.getRefinementAnnotationPosition(element, value); + diagnostics.add(new SyntaxError(e.getMessage(), pos, value)); } } @@ -318,8 +318,8 @@ public boolean checksStateSMT(Predicate prevState, Predicate expectedState, Sour return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); } - public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customeMessage) { - vcChecker.printSubtypingError(element, expectedType, foundType, customeMessage); + public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customMessage) { + vcChecker.printSubtypingError(element, expectedType, foundType, customMessage); } public void createSameStateError(CtElement element, Predicate expectedType, String klass) { 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 2a4c17ae..b467a757 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,8 +1,9 @@ package liquidjava.processor.refinement_checker; -import static liquidjava.diagnostics.LJDiagnostics.diagnostics; +import static liquidjava.diagnostics.Diagnostics.diagnostics; import java.util.ArrayList; +import java.util.Arrays; import java.util.List; import java.util.Set; import java.util.Stack; @@ -20,10 +21,9 @@ import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; import liquidjava.rj_language.Predicate; -import liquidjava.smt.GhostFunctionError; -import liquidjava.smt.NotFoundSMTError; +import liquidjava.rj_language.ast.Expression; import liquidjava.smt.SMTEvaluator; -import liquidjava.smt.TypeCheckError; +import liquidjava.smt.errors.TypeCheckError; import liquidjava.utils.constants.Keys; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; @@ -56,7 +56,7 @@ public void processSubtyping(Predicate expectedType, List list, CtEl et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); } catch (Exception e) { - diagnostics.add(new RefinementError(element, expectedType, premises.simplify(), map)); + diagnostics.add(new RefinementError(element, expectedType.getExpression(), premises.simplify(), map)); return; } @@ -234,13 +234,24 @@ private void recAuxGetVars(RefinedVariable var, List newVars) { getVariablesFromContext(l, newVars, varName); } - public boolean smtChecks(Predicate cSMT, Predicate expectedType, SourcePosition p) { + public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition p) { try { - new SMTEvaluator().verifySubtype(cSMT, expectedType, context, p); + new SMTEvaluator().verifySubtype(found, expectedType, context, p); } catch (TypeCheckError e) { return false; } catch (Exception e) { - diagnostics.add(new CustomError(e.getMessage(), p)); + String msg = e.getLocalizedMessage().toLowerCase(); + LJError error; + if (msg.contains("wrong number of arguments")) { + error = new GhostInvocationError("Wrong number of arguments in ghost invocation", p, + expectedType.getExpression(), null); + } else if (msg.contains("sort mismatch")) { + error = new GhostInvocationError("Type mismatch in arguments of ghost invocation", p, + expectedType.getExpression(), null); + } else { + error = new CustomError(e.getMessage(), p); + } + diagnostics.add(error); } return true; } @@ -252,12 +263,12 @@ public boolean smtChecks(Predicate cSMT, Predicate expectedType, SourcePosition * @param cSMT * @param expectedType * - * @throws Exception - * @throws GhostFunctionError * @throws TypeCheckError + * @throws Exception + * */ private void smtChecking(Predicate cSMT, Predicate expectedType, SourcePosition p) - throws TypeCheckError, GhostFunctionError, Exception { + throws TypeCheckError, Exception { new SMTEvaluator().verifySubtype(cSMT, expectedType, context, p); } @@ -298,18 +309,18 @@ private TranslationTable createMap(CtElement element, Predicate expectedType) { } protected void printSubtypingError(CtElement element, Predicate expectedType, Predicate foundType, - String customeMsg) { + String customMsg) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(foundType, lrv, mainVars); TranslationTable map = new TranslationTable(); Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); - diagnostics.add(new RefinementError(element, expectedType, premises.simplify(), map)); + diagnostics.add(new RefinementError(element, expectedType.getExpression(), premises.simplify(), map)); } public void printSameStateError(CtElement element, Predicate expectedType, String klass) { TranslationTable map = createMap(element, expectedType); - diagnostics.add(new StateConflictError(element, expectedType, klass, map)); + diagnostics.add(new StateConflictError(element, expectedType.getExpression(), klass, map)); } private void printError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, @@ -321,14 +332,11 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e private LJError mapError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, TranslationTable map) { if (e instanceof TypeCheckError) { - return new RefinementError(element, expectedType, premisesBeforeChange.simplify(), map); - } else if (e instanceof GhostFunctionError) { - return new GhostInvocationError("Invalid types or number of arguments in ghost invocation", - element.getPosition(), expectedType, map); - } else if (e instanceof NotFoundSMTError) { + return new RefinementError(element, expectedType.getExpression(), premisesBeforeChange.simplify(), map); + } else if (e instanceof liquidjava.smt.errors.NotFoundError) { return new NotFoundError(element, e.getMessage(), map); } else { - return new CustomError(element, e.getMessage()); + return new CustomError(e.getMessage(), element); } } @@ -337,6 +345,8 @@ public void printStateMismatchError(CtElement element, String method, Predicate gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); VCImplication foundState = joinPredicates(found, mainVars, lrv, map); - diagnostics.add(new StateRefinementError(element, method, states, foundState.toConjunctions(), map)); + diagnostics.add(new StateRefinementError(element, method, + Arrays.stream(states).map(Predicate::getExpression).toArray(Expression[]::new), + foundState.toConjunctions().simplify().getValue(), map)); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index c729b2ce..52fe40dc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -15,7 +15,7 @@ import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; -import liquidjava.processor.refinement_checker.object_checkers.AuxHierarchyRefinememtsPassage; +import liquidjava.processor.refinement_checker.object_checkers.AuxHierarchyRefinementsPassage; import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.ParsingException; @@ -107,7 +107,7 @@ public void getMethodRefinements(CtMethod method) throws ParsingException AuxStateHandler.handleMethodState(method, f, rtc, prefix); if (klass != null) - AuxHierarchyRefinememtsPassage.checkFunctionInSupertypes(klass, method, f, rtc); + AuxHierarchyRefinementsPassage.checkFunctionInSupertypes(klass, method, f, rtc); } public void getMethodRefinements(CtMethod method, String prefix) throws ParsingException { 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/AuxHierarchyRefinementsPassage.java similarity index 96% rename from liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java rename to liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java index 63e5ad18..fc92e29a 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/AuxHierarchyRefinementsPassage.java @@ -1,7 +1,5 @@ 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; @@ -20,7 +18,7 @@ import spoon.reflect.declaration.CtParameter; import spoon.reflect.reference.CtTypeReference; -public class AuxHierarchyRefinememtsPassage { +public class AuxHierarchyRefinementsPassage { public static void checkFunctionInSupertypes(CtClass klass, CtMethod method, RefinedFunction f, TypeChecker tc) { @@ -83,10 +81,9 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF if (argRef.isBooleanTrue()) { arg.setRefinement(superArgRef.substituteVariable(newName, arg.getName())); } else { - boolean f = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition()); - if (!f) { - if (!diagnostics.foundError()) - tc.createError(method, argRef, superArgRef, ""); + boolean ok = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition()); + if (!ok) { + 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 4cc11384..9ec34087 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,6 +1,6 @@ package liquidjava.processor.refinement_checker.object_checkers; -import static liquidjava.diagnostics.LJDiagnostics.diagnostics; +import static liquidjava.diagnostics.Diagnostics.diagnostics; import java.lang.annotation.Annotation; import java.util.*; @@ -197,23 +197,20 @@ private static Predicate createStatePredicate(String value, /* RefinedFunction f new InvalidRefinementError(e, "State refinement transition must be a boolean expression", value)); return new Predicate(); } - String t = targetClass; // f.getTargetClass(); - CtTypeReference r = tc.getFactory().Type().createReference(t); - + CtTypeReference r = tc.getFactory().Type().createReference(targetClass); String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); String name = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); tc.getContext().addVarToContext(name, r, new Predicate(), e); tc.getContext().addVarToContext(nameOld, r, new Predicate(), e); // TODO REVIEW!! // what is it for? - Predicate c1 = isTo ? getMissingStates(t, tc, p) : p; + Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p; Predicate c = c1.substituteVariable(Keys.THIS, name); c = c.changeOldMentions(nameOld, name); - boolean b = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition()); - if (b && !diagnostics.foundError()) { - tc.createSameStateError(e, p, t); + boolean ok = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition()); + if (ok) { + tc.createSameStateError(e, p, targetClass); } - return c1; } @@ -390,9 +387,8 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { stateChange.setFrom(fromPredicate); stateChange.setTo(toPredicate); } catch (ParsingException e) { - 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()))); + String message = String.format("Parsing error while constructing assignment update for `%s`", fw); + diagnostics.add(new CustomError(message, e.getMessage(), field)); return; } @@ -401,10 +397,8 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { .changeOldMentions(vi.getName(), instanceName); if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition - if (!diagnostics.foundError()) { // No errors so far - Predicate[] states = { stateChange.getFrom() }; - tc.createStateMismatchError(fw, fw.toString(), prevState, states); - } + Predicate[] states = { stateChange.getFrom() }; + tc.createStateMismatchError(fw, fw.toString(), prevState, states); return; } @@ -489,13 +483,11 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi, return transitionedState; } } - if (!found && !diagnostics.foundError()) { // Reaches the end of stateChange no matching states + if (!found) { // 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(); + String simpleInvocation = invocation.toString(); tc.createStateMismatchError(invocation, simpleInvocation, prevState, states); - // ErrorPrinter.printStateMismatch(invocation, simpleInvocation, prevState, - // states); } return new Predicate(); } 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 41de354b..7410b7bb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -1,6 +1,6 @@ package liquidjava.rj_language; -import static liquidjava.diagnostics.LJDiagnostics.diagnostics; +import static liquidjava.diagnostics.Diagnostics.diagnostics; import java.util.ArrayList; import java.util.HashMap; @@ -31,6 +31,7 @@ import liquidjava.utils.constants.Keys; import liquidjava.utils.constants.Ops; import liquidjava.utils.constants.Types; +import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtType; import spoon.reflect.factory.Factory; @@ -76,9 +77,6 @@ public Predicate(String ref, CtElement element) throws ParsingException { public Predicate(String ref, CtElement element, String prefix) throws ParsingException { this.prefix = prefix; exp = parse(ref, element); - if (diagnostics.foundError()) { - return; - } if (!(exp instanceof GroupExpression)) { exp = new GroupExpression(exp); } @@ -93,7 +91,8 @@ protected Expression parse(String ref, CtElement element) throws ParsingExceptio try { return RefinementsParser.createAST(ref, prefix); } catch (ParsingException e) { - diagnostics.add(new SyntaxError(e.getMessage(), element, ref)); + SourcePosition pos = Utils.getRefinementAnnotationPosition(element, ref); + diagnostics.add(new SyntaxError(e.getMessage(), pos, ref)); throw e; } } @@ -223,11 +222,33 @@ public ValDerivationNode simplify() { return ExpressionSimplifier.simplify(exp.clone()); } + private static boolean isBooleanLiteral(Expression expr, boolean value) { + return expr instanceof LiteralBoolean && ((LiteralBoolean) expr).isBooleanTrue() == value; + } + public static Predicate createConjunction(Predicate c1, Predicate c2) { + // simplification: (true && x) = x, (false && x) = false + if (isBooleanLiteral(c1.getExpression(), true)) + return c2; + if (isBooleanLiteral(c2.getExpression(), true)) + return c1; + if (isBooleanLiteral(c1.getExpression(), false)) + return c1; + if (isBooleanLiteral(c2.getExpression(), false)) + return c2; return new Predicate(new BinaryExpression(c1.getExpression(), Ops.AND, c2.getExpression())); } public static Predicate createDisjunction(Predicate c1, Predicate c2) { + // simplification: (false || x) = x, (true || x) = true + if (isBooleanLiteral(c1.getExpression(), false)) + return c2; + if (isBooleanLiteral(c2.getExpression(), false)) + return c1; + if (isBooleanLiteral(c1.getExpression(), true)) + return c1; + if (isBooleanLiteral(c2.getExpression(), true)) + return c2; return new Predicate(new BinaryExpression(c1.getExpression(), Ops.OR, c2.getExpression())); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java index afe7b518..74e54cce 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java @@ -33,6 +33,12 @@ public String toString() { return name + "(" + getArgs().stream().map(p -> p.toString()).collect(Collectors.joining(", ")) + ")"; } + @Override + public String toSimplifiedString() { + return name + "(" + getArgs().stream().map(Expression::toSimplifiedString).collect(Collectors.joining(", ")) + + ")"; + } + @Override public void getVariableNames(List toAdd) { for (Expression e : getArgs()) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java index 5e07cd03..2cc30c6b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java @@ -49,6 +49,11 @@ public String toString() { return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString(); } + @Override + public String toSimplifiedString() { + return getFirstOperand().toSimplifiedString() + " " + op + " " + getSecondOperand().toSimplifiedString(); + } + @Override public void getVariableNames(List toAdd) { getFirstOperand().getVariableNames(toAdd); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java index 37e3343e..7a7bf0ab 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -29,6 +29,17 @@ public abstract class Expression { public abstract String toString(); + /** + * Returns a simplified string representation of this expression with unqualified names (e.g., + * com.example.State.open => open Default implementation delegates to toString() Subclasses that contain qualified + * names should override this method + * + * @return simplified string representation + */ + public String toSimplifiedString() { + return toString(); + } + List children = new ArrayList<>(); public void addChild(Expression e) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java index f2c4984f..44d91a75 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java @@ -39,6 +39,13 @@ public String toString() { return name + "(" + getArgs().stream().map(p -> p.toString()).collect(Collectors.joining(",")) + ")"; } + @Override + public String toSimplifiedString() { + String simpleName = Utils.getSimpleName(name); + return simpleName + "(" + + getArgs().stream().map(Expression::toSimplifiedString).collect(Collectors.joining(",")) + ")"; + } + @Override public void getVariableNames(List toAdd) { for (Expression e : getArgs()) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java index a2be4ea2..f2517fb2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java @@ -23,6 +23,11 @@ public String toString() { return "(" + getExpression().toString() + ")"; } + @Override + public String toSimplifiedString() { + return getExpression().toSimplifiedString(); + } + @Override public void getVariableNames(List toAdd) { getExpression().getVariableNames(toAdd); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java index 44f90965..6090c894 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java @@ -34,6 +34,12 @@ public String toString() { return getCondition().toString() + "?" + getThen().toString() + ":" + getElse().toString(); } + @Override + public String toSimplifiedString() { + return getCondition().toSimplifiedString() + "?" + getThen().toSimplifiedString() + ":" + + getElse().toSimplifiedString(); + } + @Override public void getVariableNames(List toAdd) { getCondition().getVariableNames(toAdd); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java index 9bfdfec5..82218ec3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java @@ -31,6 +31,11 @@ public String toString() { return op + getExpression().toString(); } + @Override + public String toSimplifiedString() { + return op + getExpression().toSimplifiedString(); + } + @Override public void getVariableNames(List toAdd) { getExpression().getVariableNames(toAdd); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/ParsingException.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/ParsingException.java index d4d43439..7eae1e71 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/ParsingException.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/ParsingException.java @@ -2,9 +2,6 @@ public class ParsingException extends Exception { - /** */ - private static final long serialVersionUID = 1L; - public ParsingException(String errorMessage) { super(errorMessage); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/GhostFunctionError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/GhostFunctionError.java deleted file mode 100644 index 9f6259ae..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/GhostFunctionError.java +++ /dev/null @@ -1,23 +0,0 @@ -package liquidjava.smt; - -import spoon.reflect.declaration.CtElement; - -public class GhostFunctionError extends Exception { - - /** */ - private static final long serialVersionUID = 1L; - - private CtElement location; - - public GhostFunctionError(String message) { - super(message); - } - - public CtElement getLocation() { - return location; - } - - public void setLocation(CtElement location) { - this.location = location; - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/NotFoundSMTError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/NotFoundSMTError.java deleted file mode 100644 index 0a23d2af..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/NotFoundSMTError.java +++ /dev/null @@ -1,22 +0,0 @@ -package liquidjava.smt; - -import spoon.reflect.declaration.CtElement; - -public class NotFoundSMTError extends Exception { - private CtElement location; - - public NotFoundSMTError(String message) { - super(message); - } - - public CtElement getLocation() { - return location; - } - - public void setLocation(CtElement location) { - this.location = location; - } - - /** */ - private static final long serialVersionUID = 1L; -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 9eb23e6f..6276a872 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -1,22 +1,20 @@ 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 liquidjava.smt.errors.TypeCheckError; import spoon.reflect.cu.SourcePosition; public class SMTEvaluator { public void verifySubtype(Predicate subRef, Predicate supRef, Context c, SourcePosition pos) - throws TypeCheckError, GhostFunctionError, Exception { + throws TypeCheckError, Exception { // Creates a parser for our SMT-ready refinement language // Discharges the verification to z3 @@ -42,10 +40,6 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c, SourceP System.out.println("Could not parse: " + toVerify); e1.printStackTrace(); } catch (Z3Exception e) { - 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()); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index b508592d..79eb58cd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -17,6 +17,7 @@ import java.util.List; import java.util.Map; import liquidjava.processor.context.AliasWrapper; +import liquidjava.smt.errors.NotFoundError; import liquidjava.utils.Utils; import org.apache.commons.lang3.NotImplementedException; @@ -75,7 +76,7 @@ public Expr makeBooleanLiteral(boolean value) { private Expr getVariableTranslation(String name) throws Exception { if (!varTranslation.containsKey(name)) - throw new NotFoundSMTError("Variable '" + name.toString() + "' not found"); + throw new NotFoundError("Variable '" + name.toString() + "' not found"); Expr e = varTranslation.get(name); if (e == null) e = varTranslation.get(String.format("this#%s", name)); @@ -144,7 +145,7 @@ private FuncDecl resolveFunctionDeclFallback(String name, Expr[] params) t if (candidate != null) { return candidate; } - throw new NotFoundSMTError("Function '" + name + "' not found"); + throw new NotFoundError("Function '" + name + "' not found"); } @SuppressWarnings({ "unchecked", "rawtypes" }) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java new file mode 100644 index 00000000..5c163808 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java @@ -0,0 +1,8 @@ +package liquidjava.smt.errors; + +public class NotFoundError extends SMTError { + + public NotFoundError(String message) { + super(message); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/SMTError.java similarity index 59% rename from liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java rename to liquidjava-verifier/src/main/java/liquidjava/smt/errors/SMTError.java index d2f59fff..04d9890c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/SMTError.java @@ -1,12 +1,11 @@ -package liquidjava.smt; +package liquidjava.smt.errors; import spoon.reflect.declaration.CtElement; -public class TypeCheckError extends Exception { - +public class SMTError extends Exception { private CtElement location; - public TypeCheckError(String message) { + public SMTError(String message) { super(message); } @@ -17,7 +16,4 @@ public CtElement getLocation() { public void setLocation(CtElement location) { this.location = location; } - - /** */ - private static final long serialVersionUID = 1L; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/TypeCheckError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/TypeCheckError.java new file mode 100644 index 00000000..2419b740 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/TypeCheckError.java @@ -0,0 +1,8 @@ +package liquidjava.smt.errors; + +public class TypeCheckError extends Exception { + + public TypeCheckError(String message) { + super(message); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 089c28d7..b56a8cfd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -3,6 +3,8 @@ import java.util.Set; import liquidjava.utils.constants.Types; +import spoon.reflect.cu.SourcePosition; +import spoon.reflect.declaration.CtElement; import spoon.reflect.factory.Factory; import spoon.reflect.reference.CtTypeReference; @@ -36,4 +38,12 @@ public static String qualifyName(String prefix, String name) { public static String stripParens(String s) { return s.startsWith("(") && s.endsWith(")") ? s.substring(1, s.length() - 1) : s; } + + public static SourcePosition getRefinementAnnotationPosition(CtElement element, String refinement) { + return element.getAnnotations().stream().filter(a -> { + String value = a.getValue("value").toString(); + String unquoted = value.substring(1, value.length() - 1); + return unquoted.equals(refinement); + }).findFirst().map(a -> a.getPosition()).orElse(element.getPosition()); + } } 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 5ffa1dcb..b7f6d218 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -1,6 +1,6 @@ package liquidjava.api.tests; -import static liquidjava.diagnostics.LJDiagnostics.diagnostics; +import static liquidjava.diagnostics.Diagnostics.diagnostics; import static org.junit.Assert.fail; import java.io.IOException;