Save Failing Refinements

Author: rcosta358

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);
             }
         }