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