Modify Errors to Use TranslationTable

rcosta358 · rcosta358 · commit 57f5ae4802b6 · 2025-11-10T15:39:35.000Z
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java
@@ -12,29 +12,29 @@
 
 public class ErrorHandler {
 
-    public static <T> void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
-            HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
-        String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" +
-        // cSMT.toString();
-
-        StringBuilder sb = new StringBuilder();
-        sb.append("______________________________________________________\n");
-        // title
-        StringBuilder sbtitle = new StringBuilder();
-        sbtitle.append("Failed to check refinement at: \n\n");
-        if (moreInfo != null)
-            sbtitle.append(moreInfo + "\n");
-        sbtitle.append(var.toString());
-        // all message
-        sb.append(sbtitle.toString() + "\n\n");
-        sb.append("Type expected:" + expectedType.toString() + "\n");
-        sb.append("Refinement found: " + cSMT.simplify().getValue() + "\n");
-        sb.append(printMap(map));
-        sb.append("Location: " + var.getPosition() + "\n");
-        sb.append("______________________________________________________\n");
-
-        ee.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map);
-    }
+    // public static <T> void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
+    // HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
+    // String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" +
+    // // cSMT.toString();
+
+    // StringBuilder sb = new StringBuilder();
+    // sb.append("______________________________________________________\n");
+    // // title
+    // StringBuilder sbtitle = new StringBuilder();
+    // sbtitle.append("Failed to check refinement at: \n\n");
+    // if (moreInfo != null)
+    // sbtitle.append(moreInfo + "\n");
+    // sbtitle.append(var.toString());
+    // // all message
+    // sb.append(sbtitle.toString() + "\n\n");
+    // sb.append("Type expected:" + expectedType.toString() + "\n");
+    // sb.append("Refinement found: " + cSMT.simplify().getValue() + "\n");
+    // sb.append(printMap(map));
+    // sb.append("Location: " + var.getPosition() + "\n");
+    // sb.append("______________________________________________________\n");
+
+    // ee.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map);
+    // }
 
     public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg,
             String states, HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/TranslationTable.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/TranslationTable.java
@@ -0,0 +1,17 @@
+package liquidjava.diagnostics;
+
+import java.util.HashMap;
+
+import liquidjava.processor.context.PlacementInCode;
+
+/**
+ * Translation table mapping variable names to their placement in code
+ * 
+ * @see HashMap
+ * @see PlacementInCode
+ */
+public class TranslationTable extends HashMap<String, PlacementInCode> {
+    public TranslationTable() {
+        super();
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/CustomError.java
@@ -8,7 +8,7 @@
 public class CustomError extends LJError {
 
     public CustomError(String message) {
-        super("Found Error", message, null);
+        super("Found Error", message, null, 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
@@ -1,5 +1,6 @@
 package liquidjava.diagnostics.errors;
 
+import liquidjava.diagnostics.TranslationTable;
 import spoon.reflect.declaration.CtElement;
 
 /**
@@ -11,8 +12,9 @@ public class GhostInvocationError extends LJError {
 
     private String expected;
 
-    public GhostInvocationError(CtElement element, String expected) {
-        super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element);
+    public GhostInvocationError(CtElement element, String expected, TranslationTable translationTable) {
+        super("Ghost Invocation Error", "Invalid types or number of arguments in ghost invocation", element,
+                translationTable);
         this.expected = expected;
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java
@@ -11,7 +11,7 @@ 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);
+                "Found constructor with 'from' state (should only have a 'to' state)", element, 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
@@ -1,5 +1,6 @@
 package liquidjava.diagnostics.errors;
 
+import liquidjava.diagnostics.TranslationTable;
 import spoon.reflect.declaration.CtElement;
 
 /**
@@ -11,8 +12,9 @@ public class InvalidRefinementError extends LJError {
 
     private String refinement;
 
-    public InvalidRefinementError(String message, CtElement element, String refinement) {
-        super("Invalid Refinement", message, element);
+    public InvalidRefinementError(String message, CtElement element, String refinement,
+            TranslationTable translationTable) {
+        super("Invalid Refinement", message, element, translationTable);
         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
@@ -1,9 +1,7 @@
 package liquidjava.diagnostics.errors;
 
-import java.util.HashMap;
-
 import liquidjava.diagnostics.ErrorPosition;
-import liquidjava.processor.context.PlacementInCode;
+import liquidjava.diagnostics.TranslationTable;
 import liquidjava.utils.Utils;
 import spoon.reflect.cu.SourcePosition;
 import spoon.reflect.declaration.CtElement;
@@ -18,14 +16,14 @@ public abstract class LJError extends Exception {
     private CtElement element;
     private ErrorPosition position;
     private SourcePosition location;
-    private HashMap<String, PlacementInCode> translationTable;
+    private TranslationTable translationTable;
 
-    public LJError(String title, String message, CtElement element) {
+    public LJError(String title, String message, CtElement element, TranslationTable translationTable) {
         super(message);
         this.title = title;
         this.message = message;
         this.element = element;
-        this.translationTable = new HashMap<>();
+        this.translationTable = translationTable != null ? translationTable : new TranslationTable();
         try {
             this.location = element.getPosition();
             this.position = ErrorPosition.fromSpoonPosition(element.getPosition());
@@ -55,14 +53,10 @@ public SourcePosition getLocation() {
         return location;
     }
 
-    public HashMap<String, PlacementInCode> getTranslationTable() {
+    public TranslationTable getTranslationTable() {
         return translationTable;
     }
 
-    public void setTranslationTable(HashMap<String, PlacementInCode> translationTable) {
-        this.translationTable = translationTable;
-    }
-
     @Override
     public abstract String toString();
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java
@@ -1,5 +1,6 @@
 package liquidjava.diagnostics.errors;
 
+import liquidjava.diagnostics.TranslationTable;
 import spoon.reflect.declaration.CtElement;
 
 /**
@@ -9,8 +10,8 @@
  */
 public class NotFoundError extends LJError {
 
-    public NotFoundError(String message, CtElement element) {
-        super("Not Found Error", message, element);
+    public NotFoundError(String message, CtElement element, TranslationTable translationTable) {
+        super("Not Found Error", message, element, 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
@@ -1,5 +1,6 @@
 package liquidjava.diagnostics.errors;
 
+import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import liquidjava.utils.Utils;
 import spoon.reflect.declaration.CtElement;
@@ -14,8 +15,10 @@ public class RefinementError extends LJError {
     private String expected;
     private ValDerivationNode found;
 
-    public RefinementError(CtElement element, String expected, ValDerivationNode found) {
-        super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element);
+    public RefinementError(CtElement element, String expected, ValDerivationNode found,
+            TranslationTable translationTable) {
+        super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element,
+                translationTable);
         this.expected = expected;
         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
@@ -1,5 +1,6 @@
 package liquidjava.diagnostics.errors;
 
+import liquidjava.diagnostics.TranslationTable;
 import spoon.reflect.declaration.CtElement;
 
 /**
@@ -12,10 +13,10 @@ public class StateConflictError extends LJError {
     private String state;
     private String className;
 
-    public StateConflictError(CtElement element, String state, String className) {
+    public StateConflictError(CtElement element, String 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);
+                element, translationTable);
         this.state = state;
         this.className = className;
     }
@@ -32,6 +33,7 @@ public String getClassName() {
     public String toString() {
         StringBuilder sb = new StringBuilder();
         sb.append("Class: ").append(className).append("\n");
+        sb.append("State: ").append(state);
         return super.toString(sb.toString());
     }
 }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
@@ -2,6 +2,7 @@
 
 import java.util.Arrays;
 
+import liquidjava.diagnostics.TranslationTable;
 import spoon.reflect.declaration.CtElement;
 
 /**
@@ -15,8 +16,9 @@ public class StateRefinementError extends LJError {
     private final String[] expected;
     private final String found;
 
-    public StateRefinementError(CtElement element, String method, String[] expected, String found) {
-        super("State Refinement Error", "State refinement transition violation", element);
+    public StateRefinementError(CtElement element, String method, String[] expected, String found,
+            TranslationTable translationTable) {
+        super("State Refinement Error", "State refinement transition violation", element, translationTable);
         this.method = method;
         this.expected = expected;
         this.found = found;
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);
+        super("Syntax Error", message, element, null);
         this.refinement = refinement;
     }
 
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
@@ -326,8 +326,8 @@ public void createSameStateError(CtElement element, Predicate expectedType, Stri
         vcChecker.printSameStateError(element, expectedType, klass);
     }
 
-    public void createStateMismatchError(CtElement element, String method, Predicate c, String states) {
-        vcChecker.printStateMismatchError(element, method, c, states);
+    public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate[] expected) {
+        vcChecker.printStateMismatchError(element, method, found, expected);
     }
 
     public ErrorEmitter getErrorEmitter() {
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
@@ -1,6 +1,9 @@
 package liquidjava.processor.refinement_checker;
 
+import static liquidjava.diagnostics.LJDiagnostics.diagnostics;
+
 import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Set;
@@ -10,6 +13,9 @@
 
 import liquidjava.diagnostics.ErrorEmitter;
 import liquidjava.diagnostics.ErrorHandler;
+import liquidjava.diagnostics.errors.LJError;
+import liquidjava.diagnostics.errors.RefinementError;
+import liquidjava.diagnostics.errors.StateRefinementError;
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.*;
 import liquidjava.rj_language.Predicate;
@@ -54,7 +60,8 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
 
             et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f);
         } catch (Exception e) {
-            ErrorHandler.printError(element, e.getMessage(), expectedType, premises, map, errorEmitter);
+            diagnostics.add(new RefinementError(element, expectedType, premises.simplify()));
+            // ErrorHandler.printError(element, e.getMessage(), expectedType, premises, map, errorEmitter);
             return;
         }
 
@@ -322,7 +329,8 @@ protected void printSubtypingError(CtElement element, Predicate expectedType, Pr
         HashMap<String, PlacementInCode> map = new HashMap<>();
         Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
 
-        ErrorHandler.printError(element, customeMsg, expectedType, premises, map, errorEmitter);
+        diagnostics.add(new RefinementError(element, expectedType, premises.simplify()));
+        // ErrorHandler.printError(element, customeMsg, expectedType, premises, map, errorEmitter);
     }
 
     public void printSameStateError(CtElement element, Predicate expectedType, String klass) {
@@ -343,16 +351,17 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e
             s = "Method invocation " + totalS + " in:";
         }
 
-        Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map);
-        Predicate cSMTMessageReady = premisesBeforeChange; // substituteByMap(premisesBeforeChange, map);
+        // Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map);
+        // Predicate cSMTMessageReady = premisesBeforeChange; // substituteByMap(premisesBeforeChange, map);
         if (e instanceof TypeCheckError) {
-            ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter);
+            diagnostics.add(new RefinementError(element, expectedType, premisesBeforeChange.simplify()));
+            // ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter);
         } else if (e instanceof GhostFunctionError) {
-            ErrorHandler.printErrorArgs(element, etMessageReady, e.getMessage(), map, errorEmitter);
+            ErrorHandler.printErrorArgs(element, expectedType, e.getMessage(), map, errorEmitter);
         } else if (e instanceof TypeMismatchError) {
-            ErrorHandler.printErrorTypeMismatch(element, etMessageReady, e.getMessage(), map, errorEmitter);
+            ErrorHandler.printErrorTypeMismatch(element, expectedType, e.getMessage(), map, errorEmitter);
         } else if (e instanceof NotFoundError) {
-            ErrorHandler.printNotFound(element, cSMTMessageReady, etMessageReady, e.getMessage(), map, errorEmitter);
+            ErrorHandler.printNotFound(element, premisesBeforeChange, expectedType, e.getMessage(), map, errorEmitter);
         } else {
             ErrorHandler.printCustomError(element, e.getMessage(), errorEmitter);
             // System.err.println("Unknown error:"+e.getMessage());
@@ -361,12 +370,16 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e
         }
     }
 
-    public void printStateMismatchError(CtElement element, String method, Predicate c, String states) {
+    public void printStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states) {
         List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
-        gatherVariables(c, lrv, mainVars);
+        gatherVariables(found, lrv, mainVars);
         HashMap<String, PlacementInCode> map = new HashMap<>();
-        VCImplication constraintForErrorMsg = joinPredicates(c, mainVars, lrv, map);
-        // HashMap<String, PlacementInCode> map = createMap(element, c);
-        ErrorHandler.printStateMismatch(element, method, constraintForErrorMsg, states, map, errorEmitter);
+        VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
+        String[] expectedStates = Arrays.stream(states).toArray(String[]::new);
+
+        LJError error = new StateRefinementError(element, method, expectedStates, foundState.toString());
+        error.setTranslationTable(map);
+        diagnostics.add(error);
+        // ErrorHandler.printStateMismatch(element, method, constraintForErrorMsg, states, map, errorEmitter);
     }
 }
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
@@ -399,7 +399,7 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) {
 
         if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition
             if (!tc.getErrorEmitter().foundError()) { // No errors in errorEmitter
-                String states = stateChange.getFrom().toString();
+                Predicate[] states = { stateChange.getFrom() };
                 tc.createStateMismatchError(fw, fw.toString(), prevState, states);
             }
             return;
@@ -487,9 +487,8 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi,
             }
         }
         if (!found && !tc.getErrorEmitter().foundError()) { // Reaches the end of stateChange no matching states
-            String states = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom)
-                    .map(Predicate::toString).collect(Collectors.joining(","));
-
+            Predicate[] states = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom)
+                    .toArray(Predicate[]::new);
             String simpleInvocation = invocation.toString(); // .getExecutable().toString();
             tc.createStateMismatchError(invocation, simpleInvocation, prevState, states);
             // ErrorPrinter.printStateMismatch(invocation, simpleInvocation, prevState,

Original file line number	Diff line number	Diff line change
`@@ -8,7 +8,7 @@`
`8`	`8`	`public class CustomError extends LJError {`
`9`	`9`
`10`	`10`	`public CustomError(String message) {`
`11`		`- super("Found Error", message, null);`
	`11`	`+ super("Found Error", message, null, null);`
`12`	`12`	`}`
`13`	`13`
`14`	`14`	`@Override`
Original file line number	Diff line number	Diff line change
`@@ -11,7 +11,7 @@ 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);`
	`14`	`+ "Found constructor with 'from' state (should only have a 'to' state)", element, null);`
`15`	`15`	`}`
`16`	`16`
`17`	`17`	`@Override`