diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 5edca456..2461306e 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -11,7 +11,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.2 + 0.0.4 liquidjava-verifier LiquidJava Verifier https://github.com/liquid-java/liquidjava diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index bf7df8b0..88818dd8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -10,16 +10,14 @@ public class LJDiagnostic extends RuntimeException { private final String title; private final String message; - private final String details; private final String file; private final ErrorPosition position; private final String accentColor; - public LJDiagnostic(String title, String message, String details, SourcePosition pos, String accentColor) { + public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor) { this.title = title; this.message = message; - this.details = details; - this.file = pos != null ? pos.getFile().getPath() : null; + this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null; this.position = ErrorPosition.fromSpoonPosition(pos); this.accentColor = accentColor; } @@ -33,7 +31,7 @@ public String getMessage() { } public String getDetails() { - return details; + return ""; // to be overridden by subclasses } public ErrorPosition getPosition() { @@ -44,13 +42,17 @@ public String getFile() { return file; } + public String getAccentColor() { + return accentColor; + } + @Override public String toString() { StringBuilder sb = new StringBuilder(); // title - sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET) - .append(message.toLowerCase()).append("\n"); + sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message) + .append("\n"); // snippet String snippet = getSnippet(); @@ -59,7 +61,8 @@ public String toString() { } // details - if (details != null && !details.isEmpty()) { + String details = getDetails(); + if (!details.isEmpty()) { sb.append(" --> ").append(String.join("\n ", details.split("\n"))).append("\n"); } @@ -124,7 +127,6 @@ public boolean equals(Object obj) { return false; LJDiagnostic other = (LJDiagnostic) obj; return title.equals(other.title) && message.equals(other.message) - && ((details == null && other.details == null) || (details != null && details.equals(other.details))) && ((file == null && other.file == null) || (file != null && file.equals(other.file))) && ((position == null && other.position == null) || (position != null && position.equals(other.position))); @@ -134,7 +136,6 @@ public boolean equals(Object obj) { public int hashCode() { int result = title.hashCode(); result = 31 * result + message.hashCode(); - result = 31 * result + (details != null ? details.hashCode() : 0); result = 31 * result + (file != null ? file.hashCode() : 0); result = 31 * result + (position != null ? position.hashCode() : 0); return result; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java index b9a5baca..94e007f0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java @@ -1,7 +1,6 @@ package liquidjava.diagnostics.errors; import spoon.reflect.cu.SourcePosition; -import spoon.reflect.declaration.CtElement; /** * Custom error with an arbitrary message @@ -11,18 +10,10 @@ public class CustomError extends LJError { public CustomError(String message) { - super("Error", message, null, null, null); + super("Error", message, null, null); } - public CustomError(String message, SourcePosition pos) { - super("Error", message, null, pos, null); - } - - public CustomError(String message, String detail, CtElement element) { - super("Error", message, detail, element.getPosition(), null); - } - - public CustomError(String message, CtElement element) { - super("Error", message, null, element.getPosition(), null); + public CustomError(String message, SourcePosition position) { + super("Error", message, position, null); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java deleted file mode 100644 index 1c063fa0..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java +++ /dev/null @@ -1,25 +0,0 @@ -package liquidjava.diagnostics.errors; - -import liquidjava.diagnostics.TranslationTable; -import liquidjava.rj_language.ast.Expression; -import spoon.reflect.cu.SourcePosition; - -/** - * Error indicating that a ghost method invocation is invalid (e.g., has wrong arguments) - * - * @see LJError - */ -public class GhostInvocationError extends LJError { - - private final String expected; - - public GhostInvocationError(String message, SourcePosition pos, Expression expected, - TranslationTable translationTable) { - super("Ghost Invocation Error", message, "", pos, translationTable); - this.expected = expected.toSimplifiedString(); - } - - public String getExpected() { - return expected; - } -} 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 6ef5f6d7..ac04737d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java @@ -10,7 +10,8 @@ public class IllegalConstructorTransitionError extends LJError { public IllegalConstructorTransitionError(CtElement element) { - super("Illegal Constructor Transition Error", "Found constructor with 'from' state", - "Constructor methods should only have a 'to' state", element.getPosition(), null); + super("Illegal Constructor Transition Error", + "Found constructor with 'from' state: constructors should only have a 'to' state", + element.getPosition(), null); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java index c94ef1ff..cc14bacb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java @@ -1,6 +1,6 @@ package liquidjava.diagnostics.errors; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Error indicating that a refinement is invalid (e.g., not a boolean expression) @@ -11,8 +11,8 @@ public class InvalidRefinementError extends LJError { private final String refinement; - public InvalidRefinementError(CtElement element, String message, String refinement) { - super("Invalid Refinement", message, "", element.getPosition(), null); + public InvalidRefinementError(SourcePosition position, String message, String refinement) { + super("Invalid Refinement", message, position, 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 32a4e17d..e3fd5599 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -12,9 +12,8 @@ public abstract class LJError extends LJDiagnostic { private final TranslationTable translationTable; - public LJError(String title, String message, String details, SourcePosition pos, - TranslationTable translationTable) { - super(title, message, details, pos, Colors.BOLD_RED); + public LJError(String title, String message, SourcePosition pos, TranslationTable translationTable) { + super(title, message, pos, Colors.BOLD_RED); this.translationTable = translationTable != null ? translationTable : new TranslationTable(); } 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 9af41e49..e7973be2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -1,7 +1,8 @@ package liquidjava.diagnostics.errors; import liquidjava.diagnostics.TranslationTable; -import spoon.reflect.declaration.CtElement; +import liquidjava.utils.Utils; +import spoon.reflect.cu.SourcePosition; /** * Error indicating that an element referenced in a refinement was not found @@ -10,7 +11,21 @@ */ public class NotFoundError extends LJError { - public NotFoundError(CtElement element, String message, TranslationTable translationTable) { - super("Not Found Error", message, "", element.getPosition(), translationTable); + private final String name; + private final String kind; // "Variable" or "Ghost" + + public NotFoundError(SourcePosition position, String message, String name, String kind, + TranslationTable translationTable) { + super("Not Found Error", message, position, translationTable); + this.name = Utils.getSimpleName(name); + this.kind = kind; + } + + public String getName() { + return name; + } + + public String getKind() { + return kind; } } 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 87fd76e9..a2c13c91 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -3,7 +3,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Error indicating that a refinement constraint either was violated or cannot be proven @@ -15,11 +15,11 @@ public class RefinementError extends LJError { private final String expected; private final ValDerivationNode found; - public RefinementError(CtElement element, Expression expected, ValDerivationNode found, + public RefinementError(SourcePosition position, Expression expected, ValDerivationNode found, TranslationTable translationTable) { super("Refinement Error", - String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), "", - element.getPosition(), translationTable); + String.format("%s is not a subtype of %s", found.getValue(), expected.toSimplifiedString()), position, + translationTable); this.expected = expected.toSimplifiedString(); this.found = found; } 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 1fe85155..f1cd7c1c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -2,7 +2,7 @@ import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.ast.Expression; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Error indicating that two disjoint states were found in a state refinement @@ -11,22 +11,16 @@ */ public class StateConflictError extends LJError { - private final String state; - private final String className; + private final String state;; - public StateConflictError(CtElement element, Expression state, String className, - TranslationTable translationTable) { - super("State Conflict Error", "Found multiple disjoint states in state transition", - "State transition can only go to one state of each state set", element.getPosition(), translationTable); + public StateConflictError(SourcePosition position, Expression state, 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", + position, translationTable); this.state = state.toSimplifiedString(); - this.className = className; } public String getState() { return state; } - - public String getClassName() { - return className; - } } 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 013c64d2..508e6087 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java @@ -1,10 +1,8 @@ package liquidjava.diagnostics.errors; -import java.util.Arrays; - import liquidjava.diagnostics.TranslationTable; import liquidjava.rj_language.ast.Expression; -import spoon.reflect.declaration.CtElement; +import spoon.reflect.cu.SourcePosition; /** * Error indicating that a state refinement transition was violated @@ -13,28 +11,18 @@ */ public class StateRefinementError extends LJError { - private final String method; - private final String[] expected; + private final String expected; private final String found; - public StateRefinementError(CtElement element, String method, Expression[] expected, Expression found, + public StateRefinementError(SourcePosition position, Expression expected, Expression found, TranslationTable translationTable) { - super("State Refinement Error", "State refinement transition violation", - String.format("Expected: %s\nFound: %s", - String.join(", ", - Arrays.stream(expected).map(Expression::toSimplifiedString).toArray(String[]::new)), - found.toSimplifiedString()), - element.getPosition(), translationTable); - this.method = method; - this.expected = Arrays.stream(expected).map(Expression::toSimplifiedString).toArray(String[]::new); + super("State Refinement Error", String.format("Expected state %s but found %s", expected.toSimplifiedString(), + found.toSimplifiedString()), position, translationTable); + this.expected = expected.toSimplifiedString(); this.found = found.toSimplifiedString(); } - public String getMethod() { - return method; - } - - public String[] getExpected() { + public String getExpected() { return expected; } 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 226e6ed5..aac27123 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, SourcePosition pos, String refinement) { - super("Syntax Error", message, "", pos, null); + super("Syntax Error", message, pos, 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 e3d1c239..86438b6b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java @@ -12,7 +12,7 @@ public class ExternalClassNotFoundWarning extends LJWarning { private final String className; public ExternalClassNotFoundWarning(CtElement element, String message, String className) { - super(message, "", element.getPosition()); + super(message, element.getPosition()); 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 26ad6f51..60f20f17 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java @@ -11,12 +11,14 @@ public class ExternalMethodNotFoundWarning extends LJWarning { private final String methodName; private final String className; + private final String[] overloads; - public ExternalMethodNotFoundWarning(CtElement element, String message, String details, String methodName, - String className) { - super(message, details, element.getPosition()); + public ExternalMethodNotFoundWarning(CtElement element, String message, String methodName, String className, + String[] overloads) { + super(message, element.getPosition()); this.methodName = methodName; this.className = className; + this.overloads = overloads; } public String getMethodName() { @@ -26,4 +28,13 @@ public String getMethodName() { public String getClassName() { return className; } + + public String[] getOverloads() { + return overloads; + } + + @Override + public String getDetails() { + return overloads.length > 0 ? String.format("Available overloads:\n %s", String.join("\n ", overloads)) : ""; + } } 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 4ad3438a..29d65479 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/LJWarning.java @@ -9,7 +9,7 @@ */ public abstract class LJWarning extends LJDiagnostic { - public LJWarning(String message, String details, SourcePosition pos) { - super("Warning", message, details, pos, Colors.BOLD_YELLOW); + public LJWarning(String message, SourcePosition pos) { + super("Warning", message, pos, Colors.BOLD_YELLOW); } } 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 bfbb8de3..a52ac891 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 @@ -71,21 +71,16 @@ public void visitCtMethod(CtMethod method) { String message = String.format("Could not find constructor '%s' for '%s'", method.getSignature(), prefix); String[] overloads = getOverloads(targetType, method); - String details = overloads.length == 0 ? null - : "Available constructors:\n " + String.join("\n ", overloads); - diagnostics.add( - new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), prefix)); + new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix, overloads)); } } else { if (!methodExists(targetType, method)) { String message = String.format("Could not find method '%s %s' for '%s'", method.getType().getSimpleName(), method.getSignature(), prefix); String[] overloads = getOverloads(targetType, method); - String details = overloads.length == 0 ? null - : "Available overloads:\n " + String.join("\n ", overloads); diagnostics.add( - new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), prefix)); + new ExternalMethodNotFoundWarning(method, message, method.getSignature(), prefix, overloads)); return; } } 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 3b044848..da0c6b60 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 @@ -82,8 +82,8 @@ public Optional getRefinementFromAnnotation(CtElement element) throws // check if refinement is valid if (!p.getExpression().isBooleanExpression()) { - throw new InvalidRefinementError(element, "Refinement predicate must be a boolean expression", - ref.get()); + throw new InvalidRefinementError(element.getPosition(), + "Refinement predicate must be a boolean expression", ref.get()); } constr = Optional.of(p); } @@ -115,7 +115,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th CtLiteral s = (CtLiteral) ce; String f = s.getValue(); if (Character.isUpperCase(f.charAt(0))) { - throw new CustomError("State names must start with lowercase", s); + throw new CustomError("State names must start with lowercase", s.getPosition()); } } } @@ -152,7 +152,8 @@ private void createStateGhost(String string, CtAnnotation GhostDTO gd = RefinementsParser.getGhostDeclaration(string); if (!gd.paramTypes().isEmpty()) { throw new CustomError( - "Ghost States have the class as parameter " + "by default, no other parameters are allowed", ann); + "Ghost States have the class as parameter " + "by default, no other parameters are allowed", + ann.getPosition()); } // Set class as parameter of Ghost String qn = getQualifiedClassName(element); @@ -224,8 +225,8 @@ protected void handleAlias(String value, CtElement element) throws LJError { a.parse(path); // refinement alias must return a boolean expression if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) { - throw new InvalidRefinementError(element, "Refinement alias must return a boolean expression", - value); + throw new InvalidRefinementError(element.getPosition(), + "Refinement alias must return a boolean expression", value); } AliasWrapper aw = new AliasWrapper(a, factory, klass, path); context.addAlias(aw); @@ -295,16 +296,16 @@ public boolean checksStateSMT(Predicate prevState, Predicate expectedState, Sour return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); } - public void createError(CtElement element, Predicate expectedType, Predicate foundType) throws LJError { - vcChecker.raiseSubtypingError(element, expectedType, foundType); + public void createError(SourcePosition position, Predicate expectedType, Predicate foundType) throws LJError { + vcChecker.raiseSubtypingError(position, expectedType, foundType); } - public void createSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError { - vcChecker.raiseSameStateError(element, expectedType, klass); + public void createSameStateError(SourcePosition position, Predicate expectedType, String klass) throws LJError { + vcChecker.raiseSameStateError(position, expectedType, klass); } - public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate[] expected) + public void createStateMismatchError(SourcePosition position, String method, Predicate found, Predicate expected) throws LJError { - vcChecker.raiseStateMismatchError(element, method, found, expected); + vcChecker.raiseStateMismatchError(position, 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 3636ff93..4cad3a80 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,7 +1,6 @@ package liquidjava.processor.refinement_checker; import java.util.ArrayList; -import java.util.Arrays; import java.util.List; import java.util.Set; import java.util.Stack; @@ -9,7 +8,6 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.errors.CustomError; -import liquidjava.diagnostics.errors.GhostInvocationError; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.diagnostics.TranslationTable; @@ -19,7 +17,6 @@ import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.ast.Expression; import liquidjava.smt.SMTEvaluator; import liquidjava.smt.errors.TypeCheckError; import liquidjava.utils.constants.Keys; @@ -54,14 +51,14 @@ public void processSubtyping(Predicate expectedType, List list, CtEl premises = premisesBeforeChange.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); } catch (Exception e) { - throw new RefinementError(element, expectedType.getExpression(), premises.simplify(), map); + throw new RefinementError(element.getPosition(), expectedType.getExpression(), premises.simplify(), map); } try { smtChecking(premises, et); } catch (Exception e) { // To emit the message we use the constraints before the alias and state change - raiseError(e, premisesBeforeChange, expectedType, element, map); + raiseError(e, element.getPosition(), premisesBeforeChange, expectedType, map); } } @@ -69,11 +66,11 @@ public void processSubtyping(Predicate type, Predicate expectedType, List list, SourcePosition p, - Factory f) throws LJError { + public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List list, + SourcePosition position, Factory f) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(type, lrv, mainVars); @@ -94,7 +91,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List< } catch (Exception e) { return false; } - return smtChecks(premises, et, p); + return smtChecks(et, premises, position, map); } /** @@ -220,22 +217,14 @@ private void recAuxGetVars(RefinedVariable var, List newVars) { getVariablesFromContext(l, newVars, varName); } - public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition p) throws LJError { + public boolean smtChecks(Predicate expected, Predicate found, SourcePosition position, TranslationTable map) + throws LJError { try { - new SMTEvaluator().verifySubtype(found, expectedType, context); + new SMTEvaluator().verifySubtype(found, expected, context); } catch (TypeCheckError e) { return false; } catch (Exception e) { - String msg = e.getLocalizedMessage().toLowerCase(); - if (msg.contains("wrong number of arguments")) { - throw new GhostInvocationError("Wrong number of arguments in ghost invocation", p, - expectedType.getExpression(), null); - } else if (msg.contains("sort mismatch")) { - throw new GhostInvocationError("Type mismatch in arguments of ghost invocation", p, - expectedType.getExpression(), null); - } else { - throw new CustomError(e.getMessage(), p); - } + raiseError(e, position, found, expected, map); } return true; } @@ -275,39 +264,45 @@ private TranslationTable createMap(Predicate expectedType) { return map; } - protected void raiseSubtypingError(CtElement element, Predicate expectedType, Predicate foundType) throws LJError { - List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); - gatherVariables(expectedType, lrv, mainVars); - gatherVariables(foundType, lrv, mainVars); - TranslationTable map = new TranslationTable(); - Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); - throw new RefinementError(element, expectedType.getExpression(), premises.simplify(), map); - } - - public void raiseSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError { - TranslationTable map = createMap(expectedType); - throw new StateConflictError(element, expectedType.getExpression(), klass, map); - } - - private void raiseError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, + protected void raiseError(Exception e, SourcePosition position, Predicate found, Predicate expected, TranslationTable map) throws LJError { if (e instanceof TypeCheckError) { - throw new RefinementError(element, expectedType.getExpression(), premisesBeforeChange.simplify(), map); - } else if (e instanceof liquidjava.smt.errors.NotFoundError) { - throw new NotFoundError(element, e.getMessage(), map); + throw new RefinementError(position, expected.getExpression(), found.simplify(), map); + } else if (e instanceof liquidjava.smt.errors.NotFoundError nfe) { + throw new NotFoundError(position, e.getMessage(), nfe.getName(), nfe.getKind(), map); } else { - throw new CustomError(e.getMessage(), element); + String msg = e.getLocalizedMessage().toLowerCase(); + if (msg.contains("wrong number of arguments")) { + throw new CustomError("Wrong number of arguments in ghost invocation", position); + } else if (msg.contains("sort mismatch")) { + throw new CustomError("Type mismatch in arguments of ghost invocation", position); + } else { + throw new CustomError(e.getMessage(), position); + } } } - public void raiseStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states) + protected void raiseSubtypingError(SourcePosition position, Predicate expected, Predicate found) throws LJError { + List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); + gatherVariables(expected, lrv, mainVars); + gatherVariables(found, lrv, mainVars); + TranslationTable map = new TranslationTable(); + Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions(); + throw new RefinementError(position, expected.getExpression(), premises.simplify(), map); + } + + protected void raiseSameStateError(SourcePosition position, Predicate expected, String klass) throws LJError { + TranslationTable map = createMap(expected); + throw new StateConflictError(position, expected.getExpression(), map); + } + + protected void raiseStateMismatchError(SourcePosition position, String method, Predicate found, Predicate expected) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); VCImplication foundState = joinPredicates(found, mainVars, lrv, map); - throw new StateRefinementError(element, method, - Arrays.stream(states).map(Predicate::getExpression).toArray(Expression[]::new), + throw new StateRefinementError(position, expected.getExpression(), foundState.toConjunctions().simplify().getValue(), map); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java index 3fe01862..c4d27764 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java @@ -83,7 +83,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF } else { boolean ok = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition()); if (!ok) { - tc.createError(method, argRef, superArgRef); + tc.createError(method.getPosition(), argRef, superArgRef); } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 44164419..92bfd43d 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 @@ -65,7 +65,7 @@ private static void setConstructorStates(RefinedFunction f, List r = tc.getFactory().Type().createReference(targetClass); String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); @@ -214,7 +215,7 @@ private static Predicate createStatePredicate(String value, String targetClass, c = c.changeOldMentions(nameOld, name); boolean ok = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition()); if (ok) { - tc.createSameStateError(e, p, targetClass); + tc.createSameStateError(e.getPosition(), p, targetClass); } return c1; } @@ -406,8 +407,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L .changeOldMentions(vi.getName(), instanceName); if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition - Predicate[] states = { stateChange.getFrom() }; - tc.createStateMismatchError(fw, fw.toString(), prevState, states); + tc.createStateMismatchError(fw.getPosition(), fw.toString(), prevState, stateChange.getFrom()); return; } @@ -486,10 +486,12 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List makeBooleanLiteral(boolean value) { private Expr getVariableTranslation(String name) throws Exception { if (!varTranslation.containsKey(name)) - throw new NotFoundError("Variable '" + name + "' not found"); + throw new NotFoundError(Keys.VARIABLE, name); Expr e = varTranslation.get(name); if (e == null) e = varTranslation.get(String.format("this#%s", name)); @@ -133,7 +134,7 @@ private FuncDecl resolveFunctionDeclFallback(String name, Expr[] params) t if (candidate != null) { return candidate; } - throw new NotFoundError("Function '" + name + "' not found"); + throw new NotFoundError(Keys.GHOST, name); } @SuppressWarnings({ "unchecked", "rawtypes" }) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java index 5c163808..a6fb544a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java @@ -2,7 +2,20 @@ public class NotFoundError extends SMTError { - public NotFoundError(String message) { - super(message); + private final String name; + private final String kind; + + public NotFoundError(String kind, String name) { + super(String.format("%s '%s' not found", kind, name)); + this.name = name; + this.kind = kind; + } + + public String getName() { + return name; + } + + public String getKind() { + return kind; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java index 790845fa..cba8ee40 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java @@ -6,4 +6,6 @@ public final class Keys { public static final String THIS = "this"; public static final String WILDCARD = "_"; public static final String OLD = "old"; + public static final String VARIABLE = "Variable"; + public static final String GHOST = "Ghost"; } \ No newline at end of file