diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java index bdf527c5..a5dd6c75 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java @@ -1,4 +1,4 @@ -// Not Found Error +// Argument Mismatch Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java new file mode 100644 index 00000000..99231431 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasEmptyArguments.java @@ -0,0 +1,15 @@ +// Argument Mismatch Error +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; + +@SuppressWarnings("unused") +@RefinementAlias("InRange(int val, int low, int up) {low < val && val < up}") +public class ErrorAliasEmptyArguments { + + public static void main(String[] args) { + @Refinement("InRange()") + int j = 15; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java new file mode 100644 index 00000000..ca21871a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasNotFound.java @@ -0,0 +1,12 @@ +// Not Found Error +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorAliasNotFound { + + public static void main(String[] args) { + @Refinement("UndefinedAlias(x)") + int x = 5; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java index 1131b73f..263a0f9b 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorAliasTypeMismatch.java @@ -1,4 +1,4 @@ -// Refinement Error +// Argument Mismatch Error package testSuite; import liquidjava.specification.Refinement; @@ -15,6 +15,5 @@ public static void main(String[] args) { @Refinement("Positive(_)") double positive = positiveGrade2; - // Positive(_) fica positive > 0 } } diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java index 207e3edd..6ff3be00 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java @@ -1,4 +1,4 @@ -// Error +// Argument Mismatch Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java new file mode 100644 index 00000000..be2af75c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNotFound.java @@ -0,0 +1,12 @@ +// Not Found Error +package testSuite; + +import liquidjava.specification.Refinement; + +public class ErrorGhostNotFound { + + public void test() { + @Refinement("notFound(x)") + int x = 5; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java index b46a1a70..f9b8ef35 100644 --- a/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java +++ b/liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java @@ -1,4 +1,4 @@ -// Error +// Argument Mismatch Error package testSuite; import liquidjava.specification.Refinement; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java index 846f3dc6..f125f5fc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java @@ -55,11 +55,10 @@ public void clear() { } public String getErrorOutput() { - return String.join("\n", errors.stream().map(LJError::toString).toList()) + (errors.isEmpty() ? "" : "\n"); + return String.join("\n", errors.stream().map(LJError::toString).toList()); } public String getWarningOutput() { - return String.join("\n", warnings.stream().map(LJWarning::toString).toList()) - + (warnings.isEmpty() ? "" : "\n"); + return String.join("\n", warnings.stream().map(LJWarning::toString).toList()); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 88818dd8..245c53d8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -10,9 +10,9 @@ public class LJDiagnostic extends RuntimeException { private final String title; private final String message; - private final String file; - private final ErrorPosition position; private final String accentColor; + private String file; + private ErrorPosition position; public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor) { this.title = title; @@ -38,6 +38,13 @@ public ErrorPosition getPosition() { return position; } + public void setPosition(SourcePosition pos) { + if (pos == null) + return; + this.position = ErrorPosition.fromSpoonPosition(pos); + this.file = pos.getFile().getPath(); + } + public String getFile() { return file; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ArgumentMismatchError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ArgumentMismatchError.java new file mode 100644 index 00000000..d8516f91 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/ArgumentMismatchError.java @@ -0,0 +1,21 @@ +package liquidjava.diagnostics.errors; + +import liquidjava.diagnostics.TranslationTable; +import spoon.reflect.cu.SourcePosition; + +/** + * Error indicating that the arguments provided to a function or method do not match the expected parameters either in + * number or type of arguments + * + * @see LJError + */ +public class ArgumentMismatchError extends LJError { + + public ArgumentMismatchError(String message) { + super("Argument Mismatch Error", message, null, null); + } + + public ArgumentMismatchError(String message, SourcePosition position, TranslationTable translationTable) { + super("Argument Mismatch Error", message, position, 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 e7973be2..1a2c260a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -12,11 +12,14 @@ public class NotFoundError extends LJError { private final String name; - private final String kind; // "Variable" or "Ghost" + private final String kind; // "Variable" | "Ghost" | "Alias" - public NotFoundError(SourcePosition position, String message, String name, String kind, - TranslationTable translationTable) { - super("Not Found Error", message, position, translationTable); + public NotFoundError(String name, String kind) { + this(null, name, kind, null); + } + + public NotFoundError(SourcePosition position, String name, String kind, TranslationTable translationTable) { + super("Not Found Error", String.format("%s '%s' not found", kind, name), position, translationTable); this.name = Utils.getSimpleName(name); this.kind = kind; } 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 da0c6b60..0078f89f 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 @@ -5,10 +5,7 @@ import java.util.List; import java.util.Optional; -import liquidjava.diagnostics.errors.CustomError; -import liquidjava.diagnostics.errors.InvalidRefinementError; -import liquidjava.diagnostics.errors.LJError; -import liquidjava.diagnostics.errors.SyntaxError; +import liquidjava.diagnostics.errors.*; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; @@ -34,16 +31,18 @@ import spoon.reflect.reference.CtTypeReference; import spoon.reflect.visitor.CtScanner; +import static liquidjava.processor.refinement_checker.TypeCheckingUtils.*; + public abstract class TypeChecker extends CtScanner { - Context context; - Factory factory; - VCChecker vcChecker; + protected final Context context; + protected final Factory factory; + protected final VCChecker vcChecker; public TypeChecker(Context context, Factory factory) { this.context = context; this.factory = factory; - vcChecker = new VCChecker(); + this.vcChecker = new VCChecker(); } public Context getContext() { @@ -65,15 +64,15 @@ public Optional getRefinementFromAnnotation(CtElement element) throws for (CtAnnotation ann : element.getAnnotations()) { String an = ann.getActualAnnotation().annotationType().getCanonicalName(); if (an.contentEquals("liquidjava.specification.Refinement")) { - String st = TypeCheckingUtils.getStringFromAnnotation(ann.getValue("value")); + String st = getStringFromAnnotation(ann.getValue("value")); ref = Optional.of(st); } else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) { - String st = TypeCheckingUtils.getStringFromAnnotation(ann.getValue("value")); + String st = getStringFromAnnotation(ann.getValue("value")); getGhostFunction(st, element); } else if (an.contentEquals("liquidjava.specification.RefinementAlias")) { - String st = TypeCheckingUtils.getStringFromAnnotation(ann.getValue("value")); + String st = getStringFromAnnotation(ann.getValue("value")); handleAlias(st, element); } } @@ -209,9 +208,9 @@ protected void getGhostFunction(String value, CtElement element) throws LJError } } - protected void handleAlias(String value, CtElement element) throws LJError { + protected void handleAlias(String ref, CtElement element) throws LJError { try { - AliasDTO a = RefinementsParser.getAliasDeclaration(value); + AliasDTO a = RefinementsParser.getAliasDeclaration(ref); String klass = null; String path = null; if (element instanceof CtClass) { @@ -226,15 +225,16 @@ protected void handleAlias(String value, CtElement element) throws LJError { // refinement alias must return a boolean expression if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) { throw new InvalidRefinementError(element.getPosition(), - "Refinement alias must return a boolean expression", value); + "Refinement alias must return a boolean expression", ref); } AliasWrapper aw = new AliasWrapper(a, factory, klass, path); context.addAlias(aw); } - } catch (SyntaxError e) { + } catch (LJError e) { // add location info to error - SourcePosition pos = Utils.getRefinementAnnotationPosition(element, value); - throw new SyntaxError(e.getMessage(), pos, value); + SourcePosition pos = Utils.getRefinementAnnotationPosition(element, ref); + e.setPosition(pos); + throw e; } } @@ -296,16 +296,16 @@ public boolean checksStateSMT(Predicate prevState, Predicate expectedState, Sour return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); } - public void createError(SourcePosition position, Predicate expectedType, Predicate foundType) throws LJError { - vcChecker.raiseSubtypingError(position, expectedType, foundType); + public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType) + throws LJError { + vcChecker.throwRefinementError(position, expectedType, foundType); } - public void createSameStateError(SourcePosition position, Predicate expectedType, String klass) throws LJError { - vcChecker.raiseSameStateError(position, expectedType, klass); + public void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected) throws LJError { + vcChecker.throwStateRefinementError(position, found, expected); } - public void createStateMismatchError(SourcePosition position, String method, Predicate found, Predicate expected) - throws LJError { - vcChecker.raiseStateMismatchError(position, method, found, expected); + public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError { + vcChecker.throwStateConflictError(position, expectedType); } } 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 4cad3a80..3df794ac 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 @@ -7,18 +7,13 @@ import java.util.function.Consumer; import java.util.stream.Collectors; -import liquidjava.diagnostics.errors.CustomError; -import liquidjava.diagnostics.errors.LJError; -import liquidjava.diagnostics.errors.NotFoundError; +import liquidjava.diagnostics.errors.*; 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.SMTEvaluator; -import liquidjava.smt.errors.TypeCheckError; +import liquidjava.smt.TypeCheckError; import liquidjava.utils.constants.Keys; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; @@ -44,29 +39,64 @@ public void processSubtyping(Predicate expectedType, List list, CtEl 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(); + Predicate premises; + Predicate expected; try { List filtered = filterGhostStatesForVariables(list, mainVars, lrv); premises = premisesBeforeChange.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); - et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); - } catch (Exception e) { - 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, element.getPosition(), premisesBeforeChange, expectedType, map); + expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); + } catch (LJError e) { + // add location info to error + e.setPosition(element.getPosition()); + throw e; } + boolean isSubtype = smtChecks(expected, premises, element.getPosition()); + if (!isSubtype) + throw new RefinementError(element.getPosition(), expectedType.getExpression(), + premisesBeforeChange.simplify(), map); } + /** + * Check that type is a subtype of expectedType Throws RefinementError otherwise + * + * @param type + * @param expectedType + * @param list + * @param element + * @param f + * + * @throws LJError + */ public void processSubtyping(Predicate type, Predicate expectedType, List list, CtElement element, Factory f) throws LJError { boolean b = canProcessSubtyping(type, expectedType, list, element.getPosition(), f); if (!b) - raiseSubtypingError(element.getPosition(), expectedType, type); + throwRefinementError(element.getPosition(), expectedType, type); + } + + /** + * Checks the expected against the found constraint + * + * @param expected + * @param found + * @param position + * + * @return true if expected type is subtype of found type, false otherwise + * + * @throws LJError + */ + public boolean smtChecks(Predicate expected, Predicate found, SourcePosition position) throws LJError { + try { + new SMTEvaluator().verifySubtype(found, expected, context); + return true; + } catch (TypeCheckError e) { + return false; + } catch (LJError e) { + e.setPosition(position); + throw e; + } catch (Exception e) { + throw new CustomError(e.getMessage(), position); + } } public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List list, @@ -79,19 +109,14 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List< TranslationTable map = new TranslationTable(); String[] s = { Keys.WILDCARD, Keys.THIS }; - - Predicate premises = new Predicate(); - Predicate et = new Predicate(); - try { - premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); - List filtered = filterGhostStatesForVariables(list, mainVars, lrv); - premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s) - .changeAliasToRefinement(context, f); - et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); - } catch (Exception e) { - return false; - } - return smtChecks(et, premises, position, map); + Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); + List filtered = filterGhostStatesForVariables(list, mainVars, lrv); + premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s) + .changeAliasToRefinement(context, f); + Predicate expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); + + // check subtyping + return smtChecks(expected, premises, position); } /** @@ -196,7 +221,6 @@ private List getVariables(Predicate c, String varName) { getVariablesFromContext(c.getVariableNames(), allVars, varName); List pathNames = pathVariables.stream().map(Refined::getName).collect(Collectors.toList()); getVariablesFromContext(pathNames, allVars, ""); - return allVars; } @@ -217,30 +241,6 @@ private void recAuxGetVars(RefinedVariable var, List newVars) { getVariablesFromContext(l, newVars, varName); } - public boolean smtChecks(Predicate expected, Predicate found, SourcePosition position, TranslationTable map) - throws LJError { - try { - new SMTEvaluator().verifySubtype(found, expected, context); - } catch (TypeCheckError e) { - return false; - } catch (Exception e) { - raiseError(e, position, found, expected, map); - } - return true; - } - - /** - * Checks the expectedType against the cSMT constraint. If the types do not check and error is sent and the program - * ends - * - * @param cSMT - * @param expectedType - * - */ - private void smtChecking(Predicate cSMT, Predicate expectedType) throws Exception { - new SMTEvaluator().verifySubtype(cSMT, expectedType, context); - } - public void addPathVariable(RefinedVariable rv) { pathVariables.add(rv); } @@ -256,53 +256,36 @@ void removePathVariableThatIncludes(String otherVar) { // Errors--------------------------------------------------------------------------------------------------- - private TranslationTable createMap(Predicate expectedType) { + protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found) + throws RefinementError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); - gatherVariables(expectedType, lrv, mainVars); + gatherVariables(expected, lrv, mainVars); + gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); - joinPredicates(expectedType, mainVars, lrv, map); - return map; - } - - protected void raiseError(Exception e, SourcePosition position, Predicate found, Predicate expected, - TranslationTable map) throws LJError { - if (e instanceof TypeCheckError) { - 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 { - 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); - } - } + Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions(); + throw new RefinementError(position, expected.getExpression(), premises.simplify(), map); } - protected void raiseSubtypingError(SourcePosition position, Predicate expected, Predicate found) throws LJError { + protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected) + throws StateRefinementError { 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); + VCImplication foundState = joinPredicates(found, mainVars, lrv, map); + throw new StateRefinementError(position, expected.getExpression(), + foundState.toConjunctions().simplify().getValue(), map); } - protected void raiseSameStateError(SourcePosition position, Predicate expected, String klass) throws LJError { + protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError { TranslationTable map = createMap(expected); throw new StateConflictError(position, expected.getExpression(), map); } - protected void raiseStateMismatchError(SourcePosition position, String method, Predicate found, Predicate expected) - throws LJError { + private TranslationTable createMap(Predicate expectedType) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); - gatherVariables(found, lrv, mainVars); + gatherVariables(expectedType, lrv, mainVars); TranslationTable map = new TranslationTable(); - VCImplication foundState = joinPredicates(found, mainVars, lrv, map); - throw new StateRefinementError(position, expected.getExpression(), - foundState.toConjunctions().simplify().getValue(), map); + joinPredicates(expectedType, mainVars, lrv, map); + return 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 c4d27764..88dcf683 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.getPosition(), argRef, superArgRef); + tc.throwRefinementError(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 92bfd43d..bd76950b 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 @@ -215,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.getPosition(), p, targetClass); + tc.throwStateConflictError(e.getPosition(), p); } return c1; } @@ -407,7 +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 - tc.createStateMismatchError(fw.getPosition(), fw.toString(), prevState, stateChange.getFrom()); + tc.throwStateRefinementError(fw.getPosition(), prevState, stateChange.getFrom()); return; } @@ -490,8 +490,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List alias = new HashMap<>(); @@ -103,6 +105,8 @@ public Predicate changeAliasToRefinement(Context context, Factory f) throws Exce } ref = ref.changeAlias(alias, context, f); + ref.validateGhostInvocations(context, f); + return new Predicate(ref); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java index 13b68ba1..c9e2f58b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java @@ -4,6 +4,7 @@ import java.util.List; import java.util.stream.Collectors; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; public class AliasInvocation extends Expression { @@ -24,7 +25,7 @@ public List getArgs() { } @Override - public T accept(ExpressionVisitor visitor) throws Exception { + public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitAliasInvocation(this); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java index 9e25e644..b60ef2ec 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java @@ -2,6 +2,7 @@ import java.util.List; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; public class BinaryExpression extends Expression { @@ -40,7 +41,7 @@ public boolean isArithmeticOperation() { } @Override - public T accept(ExpressionVisitor visitor) throws Exception { + public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitBinaryExpression(this); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java index 48441251..fac053e6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -3,17 +3,24 @@ import java.util.ArrayList; import java.util.List; import java.util.Map; +import java.util.Optional; +import liquidjava.diagnostics.errors.ArgumentMismatchError; +import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.processor.context.Context; +import liquidjava.processor.context.GhostFunction; import liquidjava.processor.facade.AliasDTO; import liquidjava.rj_language.ast.typing.TypeInfer; import liquidjava.rj_language.visitors.ExpressionVisitor; import liquidjava.utils.Utils; +import liquidjava.utils.constants.Keys; import spoon.reflect.factory.Factory; +import spoon.reflect.reference.CtTypeReference; public abstract class Expression { - public abstract T accept(ExpressionVisitor visitor) throws Exception; + public abstract T accept(ExpressionVisitor visitor) throws LJError; public abstract void getVariableNames(List toAdd); @@ -33,7 +40,7 @@ public abstract class Expression { * Returns a simplified string representation of this expression with unqualified names (e.g., * com.example.State.open => open Default implementation delegates to toString() Subclasses that contain qualified * names should override this method - * + * * @return simplified string representation */ public String toSimplifiedString() { @@ -64,7 +71,7 @@ public boolean isLiteral() { /** * Checks if this expression produces a boolean type based on its structure - * + * * @return true if it is a boolean expression, false otherwise */ public boolean isBooleanExpression() { @@ -175,23 +182,33 @@ private void auxSubstituteState(Map subMap, String[] toChang } } - public Expression changeAlias(Map alias, Context ctx, Factory f) throws Exception { + public Expression changeAlias(Map alias, Context ctx, Factory f) throws LJError { Expression e = clone(); if (this instanceof AliasInvocation ai) { if (alias.containsKey(ai.name)) { // object state AliasDTO dto = alias.get(ai.name); + // check argument count + if (children.size() != dto.getVarNames().size()) { + String msg = String.format( + "Wrong number of arguments in alias invocation '%s': expected %d, got %d", ai.name, + dto.getVarNames().size(), children.size()); + throw new ArgumentMismatchError(msg); + } Expression sub = dto.getExpression().clone(); for (int i = 0; i < children.size(); i++) { Expression varExp = new Var(dto.getVarNames().get(i)); String varType = dto.getVarTypes().get(i); Expression aliasExp = children.get(i); + // check argument types boolean compatible = TypeInfer.checkCompatibleType(varType, aliasExp, ctx, f); - if (!compatible) - throw new Exception("Type Mismatch: Cannot substitute " + aliasExp + " : " - + TypeInfer.getType(ctx, f, aliasExp).get().getQualifiedName() + " by " + varExp + " : " - + TypeInfer.getType(ctx, f, varExp).get().getQualifiedName()); - + if (!compatible) { + String msg = String.format( + "Argument '%s' and parameter '%s' of alias '%s' types are incompatible: expected %s, got %s", + aliasExp, dto.getVarNames().get(i), ai.name, varType, + TypeInfer.getType(ctx, f, aliasExp).get().getQualifiedName()); + throw new ArgumentMismatchError(msg); + } sub = sub.substitute(varExp, aliasExp); } e = new GroupExpression(sub); @@ -201,13 +218,20 @@ public Expression changeAlias(Map alias, Context ctx, Factory return e; } - private void auxChangeAlias(Map alias, Context ctx, Factory f) throws Exception { + private void auxChangeAlias(Map alias, Context ctx, Factory f) throws LJError { if (hasChildren()) for (int i = 0; i < children.size(); i++) { if (children.get(i)instanceof AliasInvocation ai) { if (!alias.containsKey(ai.name)) - throw new Exception("Alias '" + ai.getName() + "' not found"); + throw new NotFoundError(ai.getName(), Keys.ALIAS); AliasDTO dto = alias.get(ai.name); + // check argument count + if (ai.children.size() != dto.getVarNames().size()) { + String msg = String.format( + "Wrong number of arguments in alias invocation '%s': expected %d, got %d", ai.name, + dto.getVarNames().size(), ai.children.size()); + throw new ArgumentMismatchError(msg); + } Expression sub = dto.getExpression().clone(); if (ai.hasChildren()) for (int j = 0; j < ai.children.size(); j++) { @@ -215,13 +239,15 @@ private void auxChangeAlias(Map alias, Context ctx, Factory f) String varType = dto.getVarTypes().get(j); Expression aliasExp = ai.children.get(j); - boolean checks = TypeInfer.checkCompatibleType(varType, aliasExp, ctx, f); - if (!checks) - throw new Exception( - "Type Mismatch: Cannot substitute " + varExp + ":" + varType + " by " + aliasExp - + ":" + TypeInfer.getType(ctx, f, aliasExp).get().getQualifiedName() - + " in alias '" + ai.name + "'"); - + // check argument types + boolean compatible = TypeInfer.checkCompatibleType(varType, aliasExp, ctx, f); + if (!compatible) { + String msg = String.format( + "Argument '%s' and parameter '%s' of alias '%s' types are incompatible: expected %s, got %s", + aliasExp, dto.getVarNames().get(i), ai.name, varType, + TypeInfer.getType(ctx, f, aliasExp).get().getQualifiedName()); + throw new ArgumentMismatchError(msg); + } sub = sub.substitute(varExp, aliasExp); } setChild(i, sub); @@ -229,4 +255,99 @@ private void auxChangeAlias(Map alias, Context ctx, Factory f) children.get(i).auxChangeAlias(alias, ctx, f); } } + + /** + * Validates all ghost function invocations within this expression against the provided context This method supports + * overloading by iterating through all ghost functions with the matching name If a valid signature is found, no + * error is thrown If the invocation name exists but no overload matches the argument types, an + * {@link ArgumentMismatchError} is thrown. + * + * @param ctx + * @param f + * + * @throws LJError + */ + public void validateGhostInvocations(Context ctx, Factory f) throws LJError { + if (this instanceof FunctionInvocation fi) { + // get all ghosts with the matching name + List candidates = ctx.getGhosts().stream().filter(g -> g.matches(fi.name)).toList(); + if (candidates.isEmpty()) + return; // not found error is thrown elsewhere + + // find matching overload + Optional found = candidates.stream().filter(g -> argumentsMatch(fi, g, ctx, f)).findFirst(); + if (found.isEmpty()) { + // no overload found, use the first candidate to throw the error + throwArgumentMismatchError(fi, candidates.get(0), ctx, f); + } + } + // recurse children + if (hasChildren()) { + for (Expression child : children) { + child.validateGhostInvocations(ctx, f); + } + } + } + + /** + * Checks if the arguments of the given function invocation match the parameters of the given ghost function + * + * @param fi + * @param g + * @param ctx + * @param f + */ + private boolean argumentsMatch(FunctionInvocation fi, GhostFunction g, Context ctx, Factory f) { + // check argument count + if (fi.children.size() != g.getParametersTypes().size()) + return false; + + // check argument types + for (int i = 0; i < fi.children.size(); i++) { + Expression arg = fi.children.get(i); + CtTypeReference expected = g.getParametersTypes().get(i); + Optional> actualOpt = TypeInfer.getType(ctx, f, arg); + + if (actualOpt.isPresent()) { + CtTypeReference actual = actualOpt.get(); + if (!actual.equals(expected) && !actual.isSubtypeOf(expected)) { + return false; + } + } + } + return true; + } + + /** + * Throws an ArgumentMismatchError for the given function invocation and ghost function + * + * @param fi + * @param g + * @param ctx + * @param f + * + * @throws ArgumentMismatchError + */ + private void throwArgumentMismatchError(FunctionInvocation fi, GhostFunction g, Context ctx, Factory f) + throws ArgumentMismatchError { + if (fi.children.size() != g.getParametersTypes().size()) { + throw new ArgumentMismatchError( + String.format("Wrong number of arguments in ghost invocation '%s': expected %d, got %d", fi.name, + g.getParametersTypes().size(), fi.children.size())); + } + + for (int i = 0; i < fi.children.size(); i++) { + CtTypeReference expected = g.getParametersTypes().get(i); + Optional> actualOpt = TypeInfer.getType(ctx, f, fi.children.get(i)); + if (actualOpt.isPresent()) { + CtTypeReference actual = actualOpt.get(); + if (!actual.equals(expected) && !actual.isSubtypeOf(expected)) { + Expression arg = fi.children.get(i); + throw new ArgumentMismatchError(String.format( + "Argument '%s' and its respective parameter of ghost '%s' types are incompatible: expected %s, got %s", + arg, fi.name, expected.getSimpleName(), actual.getSimpleName())); + } + } + } + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java index f4dc3b9a..71f3febd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java @@ -4,6 +4,7 @@ import java.util.List; import java.util.stream.Collectors; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; import liquidjava.utils.Utils; @@ -30,7 +31,7 @@ public void setChild(int index, Expression element) { } @Override - public T accept(ExpressionVisitor visitor) throws Exception { + public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitFunctionInvocation(this); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java index 24e45fb4..c68edaa9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java @@ -2,6 +2,7 @@ import java.util.List; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; public class GroupExpression extends Expression { @@ -15,7 +16,7 @@ public Expression getExpression() { } @Override - public T accept(ExpressionVisitor visitor) throws Exception { + public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitGroupExpression(this); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java index 5b72ce6a..a779aad4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java @@ -2,6 +2,7 @@ import java.util.List; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; public class Ite extends Expression { @@ -25,7 +26,7 @@ public Expression getElse() { } @Override - public T accept(ExpressionVisitor visitor) throws Exception { + public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitIte(this); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java index 8da1091c..81ab62d0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java @@ -2,6 +2,7 @@ import java.util.List; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; public class LiteralBoolean extends Expression { @@ -17,7 +18,7 @@ public LiteralBoolean(String value) { } @Override - public T accept(ExpressionVisitor visitor) throws Exception { + public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitLiteralBoolean(this); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java index 993c177b..7d68a738 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java @@ -2,6 +2,7 @@ import java.util.List; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; public class LiteralInt extends Expression { @@ -17,7 +18,7 @@ public LiteralInt(String v) { } @Override - public T accept(ExpressionVisitor visitor) throws Exception { + public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitLiteralInt(this); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java index 7913438d..b21f1cf2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java @@ -2,6 +2,7 @@ import java.util.List; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; public class LiteralReal extends Expression { @@ -17,7 +18,7 @@ public LiteralReal(String v) { } @Override - public T accept(ExpressionVisitor visitor) throws Exception { + public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitLiteralReal(this); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java index 1382535c..1d8d2842 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java @@ -2,6 +2,7 @@ import java.util.List; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; public class LiteralString extends Expression { @@ -13,7 +14,7 @@ public LiteralString(String v) { } @Override - public T accept(ExpressionVisitor visitor) throws Exception { + public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitLiteralString(this); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java index b805df84..4913e04c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java @@ -2,6 +2,7 @@ import java.util.List; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; public class UnaryExpression extends Expression { @@ -22,7 +23,7 @@ public String getOp() { } @Override - public T accept(ExpressionVisitor visitor) throws Exception { + public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitUnaryExpression(this); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java index e89365c6..495a873b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java @@ -2,6 +2,7 @@ import java.util.List; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.visitors.ExpressionVisitor; public class Var extends Expression { @@ -17,7 +18,7 @@ public String getName() { } @Override - public T accept(ExpressionVisitor visitor) throws Exception { + public T accept(ExpressionVisitor visitor) throws LJError { return visitor.visitVar(this); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index 96530499..82e6ea52 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -52,6 +52,8 @@ import rj.grammar.RJParser.StartPredContext; import rj.grammar.RJParser.TargetInvocationContext; import rj.grammar.RJParser.VarContext; +import spoon.reflect.cu.SourcePosition; +import liquidjava.diagnostics.errors.ArgumentMismatchError; /** * Create refinements language AST using antlr @@ -168,14 +170,14 @@ private Expression functionCallCreate(FunctionCallContext rc) throws LJError { String name = Utils.qualifyName(prefix, ref); List args = getArgs(gc.args()); if (args.isEmpty()) - throw new SyntaxError("Ghost call cannot have empty arguments", ref); + throw new ArgumentMismatchError("Ghost call cannot have empty arguments"); return new FunctionInvocation(name, args); } else { AliasCallContext gc = rc.aliasCall(); String ref = gc.ID_UPPER().getText(); List args = getArgs(gc.args()); if (args.isEmpty()) - throw new SyntaxError("Alias call cannot have empty arguments", ref); + throw new ArgumentMismatchError("Alias call cannot have empty arguments"); return new AliasInvocation(ref, args); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java index 51ab5357..dc8d9089 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java @@ -1,5 +1,6 @@ package liquidjava.rj_language.visitors; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.FunctionInvocation; @@ -13,25 +14,25 @@ import liquidjava.rj_language.ast.Var; public interface ExpressionVisitor { - T visitAliasInvocation(AliasInvocation alias) throws Exception; + T visitAliasInvocation(AliasInvocation alias) throws LJError; - T visitBinaryExpression(BinaryExpression exp) throws Exception; + T visitBinaryExpression(BinaryExpression exp) throws LJError; - T visitFunctionInvocation(FunctionInvocation fun) throws Exception; + T visitFunctionInvocation(FunctionInvocation fun) throws LJError; - T visitGroupExpression(GroupExpression exp) throws Exception; + T visitGroupExpression(GroupExpression exp) throws LJError; - T visitIte(Ite ite) throws Exception; + T visitIte(Ite ite) throws LJError; - T visitLiteralInt(LiteralInt lit) throws Exception; + T visitLiteralInt(LiteralInt lit) throws LJError; - T visitLiteralBoolean(LiteralBoolean lit) throws Exception; + T visitLiteralBoolean(LiteralBoolean lit) throws LJError; - T visitLiteralReal(LiteralReal lit) throws Exception; + T visitLiteralReal(LiteralReal lit) throws LJError; - T visitLiteralString(LiteralString lit) throws Exception; + T visitLiteralString(LiteralString lit) throws LJError; - T visitUnaryExpression(UnaryExpression exp) throws Exception; + T visitUnaryExpression(UnaryExpression exp) throws LJError; - T visitVar(Var var) throws Exception; + T visitVar(Var var) throws LJError; } \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java index a11f0639..1425b438 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -2,6 +2,7 @@ import com.microsoft.z3.Expr; +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.FunctionInvocation; @@ -24,7 +25,7 @@ public ExpressionToZ3Visitor(TranslatorToZ3 ctx) { } @Override - public Expr visitAliasInvocation(AliasInvocation alias) throws Exception { + public Expr visitAliasInvocation(AliasInvocation alias) throws LJError { Expr[] argsExpr = new Expr[alias.getArgs().size()]; for (int i = 0; i < argsExpr.length; i++) { argsExpr[i] = alias.getArgs().get(i).accept(this); @@ -33,7 +34,7 @@ public Expr visitAliasInvocation(AliasInvocation alias) throws Exception { } @Override - public Expr visitBinaryExpression(BinaryExpression exp) throws Exception { + public Expr visitBinaryExpression(BinaryExpression exp) throws LJError { Expr e1 = exp.getFirstOperand().accept(this); Expr e2 = exp.getSecondOperand().accept(this); return switch (exp.getOperator()) { @@ -56,7 +57,7 @@ public Expr visitBinaryExpression(BinaryExpression exp) throws Exception { } @Override - public Expr visitFunctionInvocation(FunctionInvocation fun) throws Exception { + public Expr visitFunctionInvocation(FunctionInvocation fun) throws LJError { Expr[] argsExpr = new Expr[fun.getArgs().size()]; for (int i = 0; i < argsExpr.length; i++) { argsExpr[i] = fun.getArgs().get(i).accept(this); @@ -65,17 +66,17 @@ public Expr visitFunctionInvocation(FunctionInvocation fun) throws Exception } @Override - public Expr visitGroupExpression(GroupExpression exp) throws Exception { + public Expr visitGroupExpression(GroupExpression exp) throws LJError { return exp.getExpression().accept(this); } @Override - public Expr visitIte(Ite ite) throws Exception { + public Expr visitIte(Ite ite) throws LJError { return ctx.makeIte(ite.getCondition().accept(this), ite.getThen().accept(this), ite.getElse().accept(this)); } @Override - public Expr visitVar(Var var) throws Exception { + public Expr visitVar(Var var) throws LJError { return ctx.makeVariable(var.getName()); } @@ -100,7 +101,7 @@ public Expr visitLiteralString(LiteralString lit) { } @Override - public Expr visitUnaryExpression(UnaryExpression exp) throws Exception { + public Expr visitUnaryExpression(UnaryExpression exp) throws LJError { return switch (exp.getOp()) { case "-" -> ctx.makeMinus(exp.getExpression().accept(this)); case "!" -> ctx.mkNot(exp.getExpression().accept(this)); diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 4bec8f9e..bf00f999 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -8,7 +8,6 @@ import liquidjava.processor.context.Context; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; -import liquidjava.smt.errors.TypeCheckError; public class SMTEvaluator { diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 6d08a32d..e844ad12 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -16,8 +16,10 @@ import java.util.HashMap; import java.util.List; import java.util.Map; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.processor.context.AliasWrapper; -import liquidjava.smt.errors.NotFoundError; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; @@ -67,22 +69,22 @@ public Expr makeBooleanLiteral(boolean value) { return z3.mkBool(value); } - private Expr getVariableTranslation(String name) throws Exception { + private Expr getVariableTranslation(String name) throws LJError { if (!varTranslation.containsKey(name)) - throw new NotFoundError(Keys.VARIABLE, name); + throw new NotFoundError(name, Keys.VARIABLE); Expr e = varTranslation.get(name); if (e == null) e = varTranslation.get(String.format("this#%s", name)); if (e == null) - throw new SyntaxException("Unknown variable:" + name); + throw new NotFoundError(name, Keys.VARIABLE); return e; } - public Expr makeVariable(String name) throws Exception { + public Expr makeVariable(String name) throws LJError { return getVariableTranslation(name); // int[] not in varTranslation } - public Expr makeFunctionInvocation(String name, Expr[] params) throws Exception { + public Expr makeFunctionInvocation(String name, Expr[] params) throws LJError { if (name.equals("addToIndex")) return makeStore(params); if (name.equals("getFromIndex")) @@ -111,7 +113,7 @@ public Expr makeFunctionInvocation(String name, Expr[] params) throws Exce * name and number of parameters, preferring an exact qualified-name match if found among candidates; otherwise * returns the first compatible candidate and relies on later coercion via var supertypes. */ - private FuncDecl resolveFunctionDeclFallback(String name, Expr[] params) throws Exception { + private FuncDecl resolveFunctionDeclFallback(String name, Expr[] params) throws LJError { String simple = Utils.getSimpleName(name); FuncDecl candidate = null; for (Map.Entry> entry : funcTranslation.entrySet()) { @@ -134,7 +136,7 @@ private FuncDecl resolveFunctionDeclFallback(String name, Expr[] params) t if (candidate != null) { return candidate; } - throw new NotFoundError(Keys.GHOST, name); + throw new NotFoundError(name, Keys.GHOST); } @SuppressWarnings({ "unchecked", "rawtypes" }) diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/TypeCheckError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java similarity index 80% rename from liquidjava-verifier/src/main/java/liquidjava/smt/errors/TypeCheckError.java rename to liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java index 2419b740..04c6c07d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/TypeCheckError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java @@ -1,4 +1,4 @@ -package liquidjava.smt.errors; +package liquidjava.smt; public class TypeCheckError extends Exception { diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java deleted file mode 100644 index a6fb544a..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/NotFoundError.java +++ /dev/null @@ -1,21 +0,0 @@ -package liquidjava.smt.errors; - -public class NotFoundError extends SMTError { - - 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/smt/errors/SMTError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/errors/SMTError.java deleted file mode 100644 index 04d9890c..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/errors/SMTError.java +++ /dev/null @@ -1,19 +0,0 @@ -package liquidjava.smt.errors; - -import spoon.reflect.declaration.CtElement; - -public class SMTError extends Exception { - private CtElement location; - - public SMTError(String message) { - super(message); - } - - public CtElement getLocation() { - return location; - } - - public void setLocation(CtElement location) { - this.location = location; - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java index cba8ee40..93311c01 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java @@ -8,4 +8,5 @@ public final class Keys { public static final String OLD = "old"; public static final String VARIABLE = "Variable"; public static final String GHOST = "Ghost"; + public static final String ALIAS = "Alias"; } \ No newline at end of file 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 be0f1ca0..0f3552e8 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -56,6 +56,10 @@ else if (shouldFail(pathName)) { fail(); } LJError error = diagnostics.getErrors().iterator().next(); + if (error.getPosition() == null) { + System.out.println("Error in: " + pathName + " --- error has no position information"); + fail(); + } if (expected.isPresent()) { String expectedError = expected.get(); String foundError = error.getTitle(); diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java index 9b05725e..cd15f869 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java +++ b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java @@ -10,6 +10,7 @@ public class TestUtils { /** * Determines if the given path indicates that the test should pass + * * @param path */ public static boolean shouldPass(String path) { @@ -18,6 +19,7 @@ public static boolean shouldPass(String path) { /** * Determines if the given path indicates that the test should fail + * * @param path */ public static boolean shouldFail(String path) {