Improvements

rcosta358 · rcosta358 · commit dc1742585171 · 2025-11-10T15:52:39.000Z
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java
@@ -1,5 +1,6 @@
 package liquidjava.diagnostics.errors;
 
+import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
 
 /**
@@ -10,11 +11,15 @@
 public class CustomError extends LJError {
 
     public CustomError(String message) {
-        super("Found Error", message, null, null);
+        super("Found Error", message, null, null, null);
+    }
+
+    public CustomError(String message, SourcePosition pos) {
+        super("Found Error", message, pos, null, null);
     }
 
     public CustomError(CtElement element, String message) {
-        super("Found Error", message, element, null);
+        super("Found Error", message, element.getPosition(), element.toString(), null);
     }
 
     @Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java
@@ -2,7 +2,7 @@
 
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.Predicate;
-import spoon.reflect.declaration.CtElement;
+import spoon.reflect.cu.SourcePosition;
 
 /**
  * Error indicating that a ghost method invocation is invalid (e.g., has wrong arguments)
@@ -13,9 +13,9 @@ public class GhostInvocationError extends LJError {
 
     private String expected;
 
-    public GhostInvocationError(CtElement element, Predicate expected, TranslationTable translationTable) {
-        super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element,
-                translationTable);
+    public GhostInvocationError(String message, SourcePosition pos, Predicate expected,
+            TranslationTable translationTable) {
+        super("Ghost Invocation Error", message, pos, null, translationTable);
         this.expected = expected.toString();
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java
@@ -11,7 +11,8 @@ public class IllegalConstructorTransitionError extends LJError {
 
     public IllegalConstructorTransitionError(CtElement element) {
         super("Illegal Constructor Transition Error",
-                "Found constructor with 'from' state (should only have a 'to' state)", element, null);
+                "Found constructor with 'from' state (should only have a 'to' state)", element.getPosition(),
+                element.toString(), null);
     }
 
     @Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java
@@ -12,7 +12,7 @@ public class InvalidRefinementError extends LJError {
     private String refinement;
 
     public InvalidRefinementError(CtElement element, String message, String refinement) {
-        super("Invalid Refinement", message, element, null);
+        super("Invalid Refinement", message, element.getPosition(), element.toString(), null);
         this.refinement = refinement;
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java
@@ -4,33 +4,27 @@
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
-import spoon.reflect.declaration.CtElement;
 
 /**
  * Base class for all LiquidJava errors
  */
-public abstract class LJError extends Exception {
+public abstract class LJError {
 
     private String title;
     private String message;
-    private CtElement element;
+    private String snippet;
     private ErrorPosition position;
     private SourcePosition location;
     private TranslationTable translationTable;
 
-    public LJError(String title, String message, CtElement element, TranslationTable translationTable) {
-        super(message);
+    public LJError(String title, String message, SourcePosition pos, String snippet,
+            TranslationTable translationTable) {
         this.title = title;
         this.message = message;
-        this.element = element;
+        this.snippet = snippet;
         this.translationTable = translationTable != null ? translationTable : new TranslationTable();
-        try {
-            this.location = element.getPosition();
-            this.position = ErrorPosition.fromSpoonPosition(element.getPosition());
-        } catch (Exception e) {
-            this.location = null;
-            this.position = null;
-        }
+        this.location = pos;
+        this.position = ErrorPosition.fromSpoonPosition(pos);
     }
 
     public String getTitle() {
@@ -41,8 +35,8 @@ public String getMessage() {
         return message;
     }
 
-    public CtElement getElement() {
-        return element;
+    public String getSnippet() {
+        return snippet;
     }
 
     public ErrorPosition getPosition() {
@@ -64,8 +58,8 @@ public String toString(String extra) {
         StringBuilder sb = new StringBuilder();
         sb.append(title);
 
-        if (element != null)
-            sb.append(" at: \n").append(element.toString().replace("@liquidjava.specification.", "@"));
+        if (snippet != null)
+            sb.append(" at: \n").append(snippet.replace("@liquidjava.specification.", "@"));
 
         sb.append("\n");
         sb.append(message).append("\n");
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java
@@ -11,7 +11,7 @@
 public class NotFoundError extends LJError {
 
     public NotFoundError(CtElement element, String message, TranslationTable translationTable) {
-        super("Not Found Error", message, element, translationTable);
+        super("Not Found Error", message, element.getPosition(), element.toString(), translationTable);
     }
 
     @Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
@@ -18,8 +18,8 @@ public class RefinementError extends LJError {
 
     public RefinementError(CtElement element, Predicate expected, ValDerivationNode found,
             TranslationTable translationTable) {
-        super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element,
-                translationTable);
+        super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected),
+                element.getPosition(), element.toString(), translationTable);
         this.expected = expected.toString();
         this.found = found;
     }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java
@@ -15,7 +15,8 @@ public class StateConflictError extends LJError {
     private String className;
 
     public StateConflictError(CtElement element, Predicate state, String className, TranslationTable translationTable) {
-        super("State Conflict Error", "Found multiple disjoint states in state transition — State transition can only go to one state of each state set", element, translationTable);
+        super("State Conflict Error", "Found multiple disjoint states in state transition — State transition can only go to one state of each state set", element.getPosition(),
+                element.toString(), translationTable);
         this.state = state.toString();
         this.className = className;
     }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
@@ -19,7 +19,8 @@ public class StateRefinementError extends LJError {
 
     public StateRefinementError(CtElement element, String method, Predicate[] expected, Predicate found,
             TranslationTable translationTable) {
-        super("State Refinement Error", "State refinement transition violation", element, translationTable);
+        super("State Refinement Error", "State refinement transition violation", element.getPosition(),
+                element.toString(), translationTable);
         this.method = method;
         this.expected = Arrays.stream(expected).map(Predicate::toString).toArray(String[]::new);
         this.found = found.toString();
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java
@@ -16,7 +16,7 @@ public SyntaxError(String message, String refinement) {
     }
 
     public SyntaxError(String message, CtElement element, String refinement) {
-        super("Syntax Error", message, element, null);
+        super("Syntax Error", message, element.getPosition(), element.toString(), null);
         this.refinement = refinement;
     }
 
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
@@ -61,7 +61,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         }
 
         try {
-            smtChecking(premises, et);
+            smtChecking(premises, et, element.getPosition());
         } catch (Exception e) {
             // To emit the message we use the constraints before the alias and state change
             printError(e, premisesBeforeChange, expectedType, element, map);
@@ -236,11 +236,11 @@ private void recAuxGetVars(RefinedVariable var, List<RefinedVariable> newVars) {
 
     public boolean smtChecks(Predicate cSMT, Predicate expectedType, SourcePosition p) {
         try {
-            new SMTEvaluator().verifySubtype(cSMT, expectedType, context);
+            new SMTEvaluator().verifySubtype(cSMT, expectedType, context, p);
         } catch (TypeCheckError e) {
             return false;
         } catch (Exception e) {
-            diagnostics.add(new CustomError(e.getMessage()));
+            diagnostics.add(new CustomError(e.getMessage(), p));
         }
         return true;
     }
@@ -256,9 +256,9 @@ public boolean smtChecks(Predicate cSMT, Predicate expectedType, SourcePosition
      * @throws GhostFunctionError
      * @throws TypeCheckError
      */
-    private void smtChecking(Predicate cSMT, Predicate expectedType)
+    private void smtChecking(Predicate cSMT, Predicate expectedType, SourcePosition p)
             throws TypeCheckError, GhostFunctionError, Exception {
-        new SMTEvaluator().verifySubtype(cSMT, expectedType, context);
+        new SMTEvaluator().verifySubtype(cSMT, expectedType, context, p);
     }
 
     /**
@@ -323,7 +323,8 @@ private LJError mapError(Exception e, Predicate premisesBeforeChange, Predicate
         if (e instanceof TypeCheckError) {
             return new RefinementError(element, expectedType, premisesBeforeChange.simplify(), map);
         } else if (e instanceof GhostFunctionError) {
-            return new GhostInvocationError(element, expectedType, map);
+            return new GhostInvocationError("Invalid types or number of arguments in ghost invocation",
+                    element.getPosition(), expectedType, map);
         } else if (e instanceof NotFoundSMTError) {
             return new NotFoundError(element, e.getMessage(), map);
         } else {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java
@@ -1,16 +1,21 @@
 package liquidjava.smt;
 
+import static liquidjava.diagnostics.LJDiagnostics.diagnostics;
+
 import com.martiansoftware.jsap.SyntaxException;
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.Status;
 import com.microsoft.z3.Z3Exception;
+
+import liquidjava.diagnostics.errors.GhostInvocationError;
 import liquidjava.processor.context.Context;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
+import spoon.reflect.cu.SourcePosition;
 
 public class SMTEvaluator {
 
-    public void verifySubtype(Predicate subRef, Predicate supRef, Context c)
+    public void verifySubtype(Predicate subRef, Predicate supRef, Context c, SourcePosition pos)
             throws TypeCheckError, GhostFunctionError, Exception {
         // Creates a parser for our SMT-ready refinement language
         // Discharges the verification to z3
@@ -37,11 +42,11 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c)
             System.out.println("Could not parse: " + toVerify);
             e1.printStackTrace();
         } catch (Z3Exception e) {
-            if (e.getLocalizedMessage().substring(0, 24).equals("Wrong number of argument")
-                    || e.getLocalizedMessage().substring(0, 13).equals("Sort mismatch"))
-                throw new GhostFunctionError(e.getLocalizedMessage());
-            else
-                throw new Z3Exception(e.getLocalizedMessage());
+            String msg = e.getLocalizedMessage().toLowerCase();
+            if (msg.contains("wrong number of arguments") || msg.contains("sort mismatch"))
+                diagnostics.add(new GhostInvocationError(msg, pos, supRef, null));
+
+            throw new Z3Exception(e.getLocalizedMessage());
         }
     }
 }

Original file line number	Diff line number	Diff line change
`@@ -11,7 +11,8 @@ public class IllegalConstructorTransitionError extends LJError {`
`11`	`11`
`12`	`12`	`public IllegalConstructorTransitionError(CtElement element) {`
`13`	`13`	`super("Illegal Constructor Transition Error",`
`14`		`- "Found constructor with 'from' state (should only have a 'to' state)", element, null);`
	`14`	`+ "Found constructor with 'from' state (should only have a 'to' state)", element.getPosition(),`
	`15`	`+ element.toString(), null);`
`15`	`16`	`}`
`16`	`17`
`17`	`18`	`@Override`
Original file line number	Diff line number	Diff line change
`@@ -12,7 +12,7 @@ public class InvalidRefinementError extends LJError {`
`12`	`12`	`private String refinement;`
`13`	`13`
`14`	`14`	`public InvalidRefinementError(CtElement element, String message, String refinement) {`
`15`		`- super("Invalid Refinement", message, element, null);`
	`15`	`+ super("Invalid Refinement", message, element.getPosition(), element.toString(), null);`
`16`	`16`	`this.refinement = refinement;`
`17`	`17`	`}`
`18`	`18`
Original file line number	Diff line number	Diff line change
`@@ -11,7 +11,7 @@`
`11`	`11`	`public class NotFoundError extends LJError {`
`12`	`12`
`13`	`13`	`public NotFoundError(CtElement element, String message, TranslationTable translationTable) {`
`14`		`- super("Not Found Error", message, element, translationTable);`
	`14`	`+ super("Not Found Error", message, element.getPosition(), element.toString(), translationTable);`
`15`	`15`	`}`
`16`	`16`
`17`	`17`	`@Override`
Original file line number	Diff line number	Diff line change
`@@ -15,7 +15,8 @@ public class StateConflictError extends LJError {`
`15`	`15`	`private String className;`
`16`	`16`
`17`	`17`	`public StateConflictError(CtElement element, Predicate state, String className, TranslationTable translationTable) {`
`18`		`- super("State Conflict Error", "Found multiple disjoint states in state transition — State transition can only go to one state of each state set", element, translationTable);`
	`18`	`+ 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(),`
	`19`	`+ element.toString(), translationTable);`
`19`	`20`	`this.state = state.toString();`
`20`	`21`	`this.className = className;`
`21`	`22`	`}`
Original file line number	Diff line number	Diff line change
`@@ -16,7 +16,7 @@ public SyntaxError(String message, String refinement) {`
`16`	`16`	`}`
`17`	`17`
`18`	`18`	`public SyntaxError(String message, CtElement element, String refinement) {`
`19`		`- super("Syntax Error", message, element, null);`
	`19`	`+ super("Syntax Error", message, element.getPosition(), element.toString(), null);`
`20`	`20`	`this.refinement = refinement;`
`21`	`21`	`}`
`22`	`22`