Fix Alias Argument Mismatch & Not Found

rcosta358 · rcosta358 · commit 9fb6fa4ff2f8 · 2025-11-22T14:31:22.000Z
- Add ArgumentMismatchError
- Check argument count and types of aliases
- Add not found error for aliases as well
- Add locations to LJErrors after catching them in the places they don't include positions
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -1,4 +1,4 @@
-// Error
+// Argument Mismatch Error
 package testSuite;
 
 import liquidjava.specification.Refinement;
diff --git 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/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
@@ -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
@@ -14,7 +14,11 @@ public class NotFoundError extends LJError {
     private final String name;
     private final String kind; // "Variable" or "Ghost"
 
-    public NotFoundError(SourcePosition position, String message, String name, String kind,
+    public NotFoundError(String message, String name, String kind) {
+        this(message, null, name, kind, null);
+    }
+
+    public NotFoundError(String message, SourcePosition position, String name, String kind,
             TranslationTable translationTable) {
         super("Not Found Error", message, position, translationTable);
         this.name = Utils.getSimpleName(name);
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
@@ -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,6 +31,8 @@
 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;
@@ -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;
         }
     }
 
@@ -301,11 +301,11 @@ public void createError(SourcePosition position, Predicate expectedType, Predica
     }
 
     public void createSameStateError(SourcePosition position, Predicate expectedType, String klass) throws LJError {
-        vcChecker.raiseSameStateError(position, expectedType, klass);
+        vcChecker.raiseSameStateError(position, expectedType);
     }
 
     public void createStateMismatchError(SourcePosition position, String method, Predicate found, Predicate expected)
             throws LJError {
-        vcChecker.raiseStateMismatchError(position, method, found, expected);
+        vcChecker.raiseStateMismatchError(position, 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
@@ -7,13 +7,8 @@
 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;
@@ -45,15 +40,16 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         String[] s = { Keys.WILDCARD, Keys.THIS };
         Predicate premisesBeforeChange = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
         Predicate premises = new Predicate();
-        Predicate et = new Predicate();
+        Predicate et;
         try {
             List<GhostState> 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);
+        } catch (LJError e) {
+            // add location info to error
+            e.setPosition(element.getPosition());
+            throw e;
         }
-
         try {
             smtChecking(premises, et);
         } catch (Exception e) {
@@ -80,14 +76,18 @@ 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();
+        Predicate premises;
+        Predicate et;
         try {
             premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
             List<GhostState> 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 (LJError e) {
+            // add location info to error
+            e.setPosition(position);
+            throw e;
         } catch (Exception e) {
             return false;
         }
@@ -269,13 +269,13 @@ protected void raiseError(Exception e, SourcePosition position, Predicate found,
         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);
+            throw new NotFoundError(e.getMessage(), position, 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);
+                throw new ArgumentMismatchError("Wrong number of arguments in ghost invocation", position, map);
             } else if (msg.contains("sort mismatch")) {
-                throw new CustomError("Type mismatch in arguments of ghost invocation", position);
+                throw new ArgumentMismatchError("Type mismatch in arguments of ghost invocation", position, map);
             } else {
                 throw new CustomError(e.getMessage(), position);
             }
@@ -291,12 +291,12 @@ protected void raiseSubtypingError(SourcePosition position, Predicate expected,
         throw new RefinementError(position, expected.getExpression(), premises.simplify(), map);
     }
 
-    protected void raiseSameStateError(SourcePosition position, Predicate expected, String klass) throws LJError {
+    protected void raiseSameStateError(SourcePosition position, Predicate expected) throws LJError {
         TranslationTable map = createMap(expected);
         throw new StateConflictError(position, expected.getExpression(), map);
     }
 
-    protected void raiseStateMismatchError(SourcePosition position, String method, Predicate found, Predicate expected)
+    protected void raiseStateMismatchError(SourcePosition position, Predicate found, Predicate expected)
             throws LJError {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
         gatherVariables(found, lrv, mainVars);
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
@@ -6,6 +6,7 @@
 import java.util.Map;
 import java.util.stream.Collectors;
 
+import liquidjava.diagnostics.errors.ArgumentMismatchError;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.SyntaxError;
 import liquidjava.processor.context.AliasWrapper;
@@ -83,18 +84,19 @@ public Predicate(Expression e) {
     protected Expression parse(String ref, CtElement element) throws LJError {
         try {
             return RefinementsParser.createAST(ref, prefix);
-        } catch (SyntaxError e) {
+        } catch (LJError e) {
             // add location info to error
             SourcePosition pos = Utils.getRefinementAnnotationPosition(element, ref);
-            throw new SyntaxError(e.getMessage(), pos, ref);
+            e.setPosition(pos);
+            throw e;
         }
     }
 
     protected Expression innerParse(String ref, String prefix) throws LJError {
         return RefinementsParser.createAST(ref, prefix);
     }
 
-    public Predicate changeAliasToRefinement(Context context, Factory f) throws Exception {
+    public Predicate changeAliasToRefinement(Context context, Factory f) throws LJError {
         Expression ref = getExpression();
 
         Map<String, AliasDTO> alias = new HashMap<>();
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
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
diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java
diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/TestUtils.java

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// Not Found Error`
	`1`	`+// Argument Mismatch Error`
`2`	`2`	`package testSuite;`
`3`	`3`
`4`	`4`	`import liquidjava.specification.Refinement;`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// Refinement Error`
	`1`	`+// Argument Mismatch Error`
`2`	`2`	`package testSuite;`
`3`	`3`
`4`	`4`	`import liquidjava.specification.Refinement;`
`@@ -15,6 +15,5 @@ public static void main(String[] args) {`
`15`	`15`
`16`	`16`	`@Refinement("Positive(_)")`
`17`	`17`	`double positive = positiveGrade2;`
`18`		`- // Positive(_) fica positive > 0`
`19`	`18`	`}`
`20`	`19`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-// Error`
	`1`	`+// Argument Mismatch Error`
`2`	`2`	`package testSuite;`
`3`	`3`
`4`	`4`	`import liquidjava.specification.Refinement;`