Fix Alias & Ghost Argument Mismatch

liquidjava-example/src/main/java/testSuite/ErrorAliasArgumentSize.java

@@ -1,4 +1,4 @@
-// Not Found Error
+// Argument Mismatch Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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;
+    }
+}

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;
+    }
+}

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
     }
 }

liquidjava-example/src/main/java/testSuite/ErrorGhostArgsTypes.java

@@ -1,4 +1,4 @@
-// Error
+// Argument Mismatch Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorGhostNumberArgs.java

@@ -1,4 +1,4 @@
-// Error
+// Argument Mismatch Error
 package testSuite;
 
 import liquidjava.specification.Refinement;

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());
     }
 }

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;
     }

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);
+    }
+}

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;
     }

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<Predicate> getRefinementFromAnnotation(CtElement element) throws
         for (CtAnnotation<? extends Annotation> 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);
     }
 }