Remove Error Position

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

@@ -13,14 +13,14 @@ public class LJDiagnostic extends RuntimeException {
     private final String accentColor;
     private final String customMessage;
     private String file;
-    private ErrorPosition position;
+    private SourcePosition position;
     private static final String PIPE = " | ";
 
     public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) {
         this.title = title;
         this.message = message;
         this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null;
-        this.position = ErrorPosition.fromSpoonPosition(pos);
+        this.position = pos;
         this.accentColor = accentColor;
         this.customMessage = customMessage;
     }
@@ -41,14 +41,14 @@ public String getDetails() {
         return ""; // to be overridden by subclasses
     }
 
-    public ErrorPosition getPosition() {
+    public SourcePosition getPosition() {
         return position;
     }
 
     public void setPosition(SourcePosition pos) {
         if (pos == null)
             return;
-        this.position = ErrorPosition.fromSpoonPosition(pos);
+        this.position = pos;
         this.file = pos.getFile().getPath();
     }
 
@@ -82,7 +82,7 @@ public String toString() {
 
         // location
         if (file != null && position != null) {
-            sb.append("\n").append(file).append(":").append(position.lineStart()).append(Colors.RESET).append("\n");
+            sb.append("\n").append(file).append(":").append(position.getLine()).append(Colors.RESET).append("\n");
         }
 
         return sb.toString();
@@ -100,8 +100,8 @@ public String getSnippet() {
             // before and after lines for context
             int contextBefore = 2;
             int contextAfter = 2;
-            int startLine = Math.max(1, position.lineStart() - contextBefore);
-            int endLine = Math.min(lines.size(), position.lineEnd() + contextAfter);
+            int startLine = Math.max(1, position.getLine() - contextBefore);
+            int endLine = Math.min(lines.size(), position.getEndLine() + contextAfter);
 
             // calculate padding for line numbers
             int padding = String.valueOf(endLine).length();
@@ -115,9 +115,9 @@ public String getSnippet() {
                 sb.append(Colors.GREY).append(lineNumStr).append(PIPE).append(line).append(Colors.RESET).append("\n");
 
                 // add error markers on the line(s) with the error
-                if (i >= position.lineStart() && i <= position.lineEnd()) {
-                    int colStart = (i == position.lineStart()) ? position.colStart() : 1;
-                    int colEnd = (i == position.lineEnd()) ? position.colEnd() : rawLine.length();
+                if (i >= position.getLine() && i <= position.getEndLine()) {
+                    int colStart = (i == position.getLine()) ? position.getColumn() : 1;
+                    int colEnd = (i == position.getEndLine()) ? position.getEndColumn() : rawLine.length();
 
                     if (colStart > 0 && colEnd > 0) {
                         int tabsBeforeStart = (int) rawLine.substring(0, Math.max(0, colStart - 1)).chars()

liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java

@@ -14,6 +14,7 @@ public abstract class RefinedVariable extends Refined {
     private PlacementInCode placementInCode;
     private boolean isParameter;
     private SourcePosition annPosition;
+    private Predicate failingRefinement;
 
     public RefinedVariable(String name, CtTypeReference<?> type, Predicate c) {
         super(name, type, c);
@@ -88,4 +89,12 @@ public void setIsParameter(boolean b) {
     public boolean isParameter() {
         return isParameter;
     }
+
+    public void setFailingRefinement(Predicate failingRefinement) {
+        this.failingRefinement = failingRefinement;
+    }
+
+    public Predicate getFailingRefinement() {
+        return failingRefinement;
+    }
 }

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

@@ -305,17 +305,23 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam
             rv.addSuperType(t);
         context.addRefinementInstanceToVariable(simpleName, newName);
         String customMessage = getMessageFromAnnotation(variable).orElse(mainRV != null ? mainRV.getMessage() : null);
-        checkSMT(cEt, usage, customMessage); // TODO CHANGE
+        checkSMT(cEt, usage, customMessage, mainRV); // TODO CHANGE
         context.addRefinementToVariableInContext(simpleName, type, cet, usage);
     }
 
-    public void checkSMT(Predicate expectedType, CtElement element) throws LJError {
-        checkSMT(expectedType, element, null);
+    public void checkSMT(Predicate expectedType, CtElement element, RefinedVariable rv) throws LJError {
+        checkSMT(expectedType, element, null, rv);
     }
 
-    public void checkSMT(Predicate expectedType, CtElement element, String customMessage) throws LJError {
-        vcChecker.processSubtyping(expectedType, context.getGhostStates(), element, factory, customMessage);
-        element.putMetadata(Keys.REFINEMENT, expectedType);
+    public void checkSMT(Predicate expectedType, CtElement element, String customMessage, RefinedVariable rv)
+            throws LJError {
+        try {
+            vcChecker.processSubtyping(expectedType, context.getGhostStates(), element, factory, customMessage);
+            element.putMetadata(Keys.REFINEMENT, expectedType);
+        } catch (RefinementError e) {
+            rv.setFailingRefinement(expectedType);
+            throw e;
+        }
     }
 
     public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo)

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

@@ -200,8 +200,8 @@ public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
                 Predicate cexpectedType = fi.getRefReturn().substituteVariable(Keys.WILDCARD, returnVarName)
                         .substituteVariable(Keys.THIS, returnVarName);
 
-                rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret);
-                rtc.checkSMT(cexpectedType, ret, fi.getMessage());
+                RefinedVariable rv = rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret);
+                rtc.checkSMT(cexpectedType, ret, fi.getMessage(), rv);
                 rtc.getContext().newRefinementToVariableInContext(returnVarName, cexpectedType);
             }
         }
@@ -372,7 +372,7 @@ private void checkParameters(CtElement invocation, List<CtExpression<?>> argumen
                 VariableInstance vi = (VariableInstance) invocation.getMetadata(Keys.TARGET);
                 c = c.substituteVariable(Keys.THIS, vi.getName());
             }
-            rtc.checkSMT(c, invocation, fArg.getMessage());
+            rtc.checkSMT(c, invocation, fArg.getMessage(), fArg);
         }
     }
 

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -440,7 +440,7 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
         // is a subtype of the variable's main refinement
         if (rv instanceof Variable) {
             Predicate superC = rv.getMainRefinement().substituteVariable(rv.getName(), vi2.getName());
-            tc.checkSMT(superC, fw);
+            tc.checkSMT(superC, fw, rv);
             tc.getContext().addRefinementInstanceToVariable(parentTargetName, newInstanceName);
         }
     }
@@ -558,7 +558,7 @@ private static void addInstanceWithState(TypeChecker tc, String superName, Strin
             // is a subtype of the variable's main refinement
             if (rv instanceof Variable) {
                 Predicate superC = rv.getMainRefinement().substituteVariable(rv.getName(), vi2.getName());
-                tc.checkSMT(superC, invocation);
+                tc.checkSMT(superC, invocation, rv);
                 tc.getContext().addRefinementInstanceToVariable(superName, name2);
             }
         }