Refactor Errors to Use Expression Instead of Predicate

liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java

@@ -45,10 +45,8 @@ public boolean equals(Object obj) {
         if (obj == null || getClass() != obj.getClass())
             return false;
         ErrorPosition other = (ErrorPosition) obj;
-        return lineStart == other.lineStart 
-            && colStart == other.colStart 
-            && lineEnd == other.lineEnd 
-            && colEnd == other.colEnd;
+        return lineStart == other.lineStart && colStart == other.colStart && lineEnd == other.lineEnd
+                && colEnd == other.colEnd;
     }
 
     @Override

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -7,7 +7,7 @@
 import spoon.reflect.cu.SourcePosition;
 
 public class LJDiagnostic {
-    
+
     private String title;
     private String message;
     private String details;
@@ -27,11 +27,11 @@ public LJDiagnostic(String title, String message, String details, SourcePosition
     public String getTitle() {
         return title;
     }
-    
+
     public String getMessage() {
         return message;
     }
-    
+
     public String getDetails() {
         return details;
     }
@@ -74,7 +74,7 @@ public String toString() {
     public String getSnippet() {
         if (file == null || position == null)
             return null;
-        
+
         Path path = Path.of(file);
         try {
             List<String> lines = Files.readAllLines(path);

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java

@@ -1,7 +1,7 @@
 package liquidjava.diagnostics.errors;
 
 import liquidjava.diagnostics.TranslationTable;
-import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.Expression;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -13,7 +13,7 @@ public class GhostInvocationError extends LJError {
 
     private String expected;
 
-    public GhostInvocationError(String message, SourcePosition pos, Predicate expected,
+    public GhostInvocationError(String message, SourcePosition pos, Expression expected,
             TranslationTable translationTable) {
         super("Ghost Invocation Error", message, "", pos, translationTable);
         this.expected = expected.toString();

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/IllegalConstructorTransitionError.java

@@ -10,7 +10,7 @@
 public class IllegalConstructorTransitionError extends LJError {
 
     public IllegalConstructorTransitionError(CtElement element) {
-        super("Illegal Constructor Transition Error",
-                "Found constructor with 'from' state", "Constructor methods should only have a 'to' state", element.getPosition(), null);
+        super("Illegal Constructor Transition Error", "Found constructor with 'from' state",
+                "Constructor methods should only have a 'to' state", element.getPosition(), null);
     }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java

@@ -12,7 +12,8 @@ public abstract class LJError extends LJDiagnostic {
 
     private TranslationTable translationTable;
 
-    public LJError(String title, String message, String details, SourcePosition pos, TranslationTable translationTable) {
+    public LJError(String title, String message, String details, SourcePosition pos,
+            TranslationTable translationTable) {
         super(title, message, details, pos, Colors.BOLD_RED);
         this.translationTable = translationTable != null ? translationTable : new TranslationTable();
     }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -1,7 +1,7 @@
 package liquidjava.diagnostics.errors;
 
 import liquidjava.diagnostics.TranslationTable;
-import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import spoon.reflect.declaration.CtElement;
 
@@ -15,7 +15,7 @@ public class RefinementError extends LJError {
     private String expected;
     private ValDerivationNode found;
 
-    public RefinementError(CtElement element, Predicate expected, ValDerivationNode found,
+    public RefinementError(CtElement element, Expression expected, ValDerivationNode found,
             TranslationTable translationTable) {
         super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), "",
                 element.getPosition(), translationTable);

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java

@@ -1,7 +1,7 @@
 package liquidjava.diagnostics.errors;
 
 import liquidjava.diagnostics.TranslationTable;
-import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.Expression;
 import spoon.reflect.declaration.CtElement;
 
 /**
@@ -14,10 +14,10 @@ public class StateConflictError extends LJError {
     private String state;
     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.getPosition(), translationTable);
+    public StateConflictError(CtElement element, Expression 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.getPosition(), translationTable);
         this.state = state.toString();
         this.className = className;
     }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -4,6 +4,7 @@
 
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.Expression;
 import spoon.reflect.declaration.CtElement;
 
 /**
@@ -17,13 +18,15 @@ public class StateRefinementError extends LJError {
     private final String[] expected;
     private final String found;
 
-    public StateRefinementError(CtElement element, String method, Predicate[] expected, Predicate found,
+    public StateRefinementError(CtElement element, String method, Expression[] expected, Expression found,
             TranslationTable translationTable) {
-        super("State Refinement Error", "State refinement transition violation", String.format("Expected: %s\nFound: %s",
-                String.join(", ", Arrays.stream(expected).map(Predicate::toString).toArray(String[]::new)), found.toString()), element.getPosition(),
-                translationTable);
+        super("State Refinement Error", "State refinement transition violation",
+                String.format("Expected: %s\nFound: %s",
+                        String.join(", ", Arrays.stream(expected).map(Expression::toString).toArray(String[]::new)),
+                        found.toString()),
+                element.getPosition(), translationTable);
         this.method = method;
-        this.expected = Arrays.stream(expected).map(Predicate::toString).toArray(String[]::new);
+        this.expected = Arrays.stream(expected).map(Expression::toString).toArray(String[]::new);
         this.found = found.toString();
     }
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java

@@ -12,7 +12,8 @@ public class ExternalMethodNotFoundWarning extends LJWarning {
     private String methodName;
     private String className;
 
-    public ExternalMethodNotFoundWarning(CtElement element, String message, String details, String methodName, String className) {
+    public ExternalMethodNotFoundWarning(CtElement element, String message, String details, String methodName,
+            String className) {
         super(message, details, element.getPosition());
         this.methodName = methodName;
         this.className = className;

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java

@@ -89,19 +89,24 @@ public <R> void visitCtMethod(CtMethod<R> method) {
         boolean isConstructor = method.getSimpleName().equals(targetType.getSimpleName());
         if (isConstructor) {
             if (!constructorExists(targetType, method)) {
-                String message = String.format("Could not find constructor '%s' for '%s'", method.getSignature(), prefix);
+                String message = String.format("Could not find constructor '%s' for '%s'", method.getSignature(),
+                        prefix);
                 String[] overloads = getOverloads(targetType, method);
-                String details = overloads.length == 0 ? null : "Available constructors:\n  " + String.join("\n  ", overloads);
+                String details = overloads.length == 0 ? null
+                        : "Available constructors:\n  " + String.join("\n  ", overloads);
 
-                diagnostics.add(new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), prefix));
+                diagnostics.add(
+                        new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), prefix));
             }
         } else {
             if (!methodExists(targetType, method)) {
-                String message = String.format("Could not find method '%s %s' for '%s'", method.getType().getSimpleName(),
-                        method.getSignature(), prefix);
+                String message = String.format("Could not find method '%s %s' for '%s'",
+                        method.getType().getSimpleName(), method.getSignature(), prefix);
                 String[] overloads = getOverloads(targetType, method);
-                String details = overloads.length == 0 ? null : "Available overloads:\n  " + String.join("\n  ", overloads);
-                diagnostics.add(new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), prefix));
+                String details = overloads.length == 0 ? null
+                        : "Available overloads:\n  " + String.join("\n  ", overloads);
+                diagnostics.add(
+                        new ExternalMethodNotFoundWarning(method, message, details, method.getSignature(), prefix));
                 return;
             }
         }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -3,6 +3,7 @@
 import static liquidjava.diagnostics.LJDiagnostics.diagnostics;
 
 import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.List;
 import java.util.Set;
 import java.util.Stack;
@@ -20,6 +21,7 @@
 import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.*;
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.Expression;
 import liquidjava.smt.GhostFunctionError;
 import liquidjava.smt.NotFoundSMTError;
 import liquidjava.smt.SMTEvaluator;
@@ -56,7 +58,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
 
             et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
         } catch (Exception e) {
-            diagnostics.add(new RefinementError(element, expectedType, premises.simplify(), map));
+            diagnostics.add(new RefinementError(element, expectedType.getExpression(), premises.simplify(), map));
             return;
         }
 
@@ -304,12 +306,12 @@ protected void printSubtypingError(CtElement element, Predicate expectedType, Pr
         gatherVariables(foundType, lrv, mainVars);
         TranslationTable map = new TranslationTable();
         Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
-        diagnostics.add(new RefinementError(element, expectedType, premises.simplify(), map));
+        diagnostics.add(new RefinementError(element, expectedType.getExpression(), premises.simplify(), map));
     }
 
     public void printSameStateError(CtElement element, Predicate expectedType, String klass) {
         TranslationTable map = createMap(element, expectedType);
-        diagnostics.add(new StateConflictError(element, expectedType, klass, map));
+        diagnostics.add(new StateConflictError(element, expectedType.getExpression(), klass, map));
     }
 
     private void printError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element,
@@ -321,10 +323,10 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e
     private LJError mapError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element,
             TranslationTable map) {
         if (e instanceof TypeCheckError) {
-            return new RefinementError(element, expectedType, premisesBeforeChange.simplify(), map);
+            return new RefinementError(element, expectedType.getExpression(), premisesBeforeChange.simplify(), map);
         } else if (e instanceof GhostFunctionError) {
             return new GhostInvocationError("Invalid types or number of arguments in ghost invocation",
-                    element.getPosition(), expectedType, map);
+                    element.getPosition(), expectedType.getExpression(), map);
         } else if (e instanceof NotFoundSMTError) {
             return new NotFoundError(element, e.getMessage(), map);
         } else {
@@ -337,6 +339,8 @@ public void printStateMismatchError(CtElement element, String method, Predicate
         gatherVariables(found, lrv, mainVars);
         TranslationTable map = new TranslationTable();
         VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
-        diagnostics.add(new StateRefinementError(element, method, states, foundState.toConjunctions(), map));
+        diagnostics.add(new StateRefinementError(element, method,
+                Arrays.stream(states).map(Predicate::getExpression).toArray(Expression[]::new),
+                foundState.toConjunctions().simplify().getValue(), map));
     }
 }

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -229,19 +229,27 @@ private static boolean isBooleanLiteral(Expression expr, boolean value) {
 
     public static Predicate createConjunction(Predicate c1, Predicate c2) {
         // simplification: (true && x) = x, (false && x) = false
-        if (isBooleanLiteral(c1.getExpression(), true)) return c2;
-        if (isBooleanLiteral(c2.getExpression(), true)) return c1;
-        if (isBooleanLiteral(c1.getExpression(), false)) return c1;
-        if (isBooleanLiteral(c2.getExpression(), false)) return c2;
+        if (isBooleanLiteral(c1.getExpression(), true))
+            return c2;
+        if (isBooleanLiteral(c2.getExpression(), true))
+            return c1;
+        if (isBooleanLiteral(c1.getExpression(), false))
+            return c1;
+        if (isBooleanLiteral(c2.getExpression(), false))
+            return c2;
         return new Predicate(new BinaryExpression(c1.getExpression(), Ops.AND, c2.getExpression()));
     }
 
     public static Predicate createDisjunction(Predicate c1, Predicate c2) {
         // simplification: (false || x) = x, (true || x) = true
-        if (isBooleanLiteral(c1.getExpression(), false)) return c2;
-        if (isBooleanLiteral(c2.getExpression(), false)) return c1;
-        if (isBooleanLiteral(c1.getExpression(), true)) return c1;
-        if (isBooleanLiteral(c2.getExpression(), true)) return c2;
+        if (isBooleanLiteral(c1.getExpression(), false))
+            return c2;
+        if (isBooleanLiteral(c2.getExpression(), false))
+            return c1;
+        if (isBooleanLiteral(c1.getExpression(), true))
+            return c1;
+        if (isBooleanLiteral(c2.getExpression(), true))
+            return c2;
         return new Predicate(new BinaryExpression(c1.getExpression(), Ops.OR, c2.getExpression()));
     }
 

liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java

@@ -44,7 +44,7 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c, SourceP
         } catch (Z3Exception e) {
             String msg = e.getLocalizedMessage().toLowerCase();
             if (msg.contains("wrong number of arguments") || msg.contains("sort mismatch"))
-                diagnostics.add(new GhostInvocationError(msg, pos, supRef, null));
+                diagnostics.add(new GhostInvocationError(msg, pos, supRef.getExpression(), null));
 
             throw new Z3Exception(e.getLocalizedMessage());
         }