Improve Error Message

Author: rcosta358

liquidjava-example/src/main/java/testSuite/ErrorSMTUnknownState.java

@@ -0,0 +1,19 @@
+package testSuite;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("int amount")
+public class ErrorSMTUnknownState {
+    @StateRefinement(to = "amount(this) > 0")
+    public ErrorSMTUnknownState() {}
+
+    @StateRefinement(from = "amount(this) < limit")
+    public void consume(int limit) {}
+
+    public static void test(double limit) {
+        ErrorSMTUnknownState value = new ErrorSMTUnknownState();
+        int boundary = (int) limit;
+        value.consume(boundary); // Expect: SMT Unknown Error
+    }
+}

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

@@ -1,12 +1,28 @@
 package liquidjava.diagnostics.errors;
 
+import spoon.reflect.cu.SourcePosition;
+
 /**
  * Error indicating that the SMT solver could not decide a verification condition
  */
 public class SMTUnknownError extends LJError {
+    private SourcePosition declarationPosition;
 
     public SMTUnknownError(String reason) {
-        super("SMT Unknown Error",
-                "The SMT solver returned UNKNOWN and could not verify the refinement. Reason: " + reason, null, null);
+        super("SMT Unknown Error", "The SMT solver could not prove refinement", null, null);
+        String tacticFailure = "smt tactic failed to show goal to be sat/unsat ";
+        if (reason.startsWith(tacticFailure)) {
+            reason = reason.substring(tacticFailure.length()).replace("(", "").replace(")", "");
+        }
+        setHint("Reason: " + reason);
+    }
+
+    public void setDeclarationPosition(SourcePosition declarationPosition) {
+        this.declarationPosition = declarationPosition;
+    }
+
+    @Override
+    public SourcePosition getDeclarationPosition() {
+        return declarationPosition;
     }
 }

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

@@ -70,6 +70,10 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         SMTResult result;
         try {
             result = dischargeToSMT(expected, premises, annotationValuePos, true);
+        } catch (SMTUnknownError error) {
+            error.setDeclarationPosition(declarationPosition);
+            DebugLog.smtError(error.getMessage());
+            throw error;
         } catch (RuntimeException ex) {
             DebugLog.smtError(ex.getMessage());
             throw ex;
@@ -94,7 +98,13 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
      */
     public void processSubtyping(Predicate type, Predicate expectedType, List<GhostState> list, CtElement element,
             SourcePosition declarationPosition, Factory f) throws LJError {
-        SMTResult result = verifySMTSubtypeStates(type, expectedType, list, element.getPosition(), f);
+        SMTResult result;
+        try {
+            result = verifySMTSubtypeStates(type, expectedType, list, element.getPosition(), f);
+        } catch (SMTUnknownError error) {
+            error.setDeclarationPosition(declarationPosition);
+            throw error;
+        }
         if (result.isError())
             throwRefinementError(element.getPosition(), declarationPosition, expectedType, type,
                     result.getCounterexample(), null);

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

@@ -7,6 +7,7 @@
 import liquidjava.diagnostics.errors.IllegalConstructorTransitionError;
 import liquidjava.diagnostics.errors.InvalidRefinementError;
 import liquidjava.diagnostics.errors.LJError;
+import liquidjava.diagnostics.errors.SMTUnknownError;
 import liquidjava.processor.context.*;
 import liquidjava.processor.refinement_checker.TypeChecker;
 import liquidjava.processor.refinement_checker.TypeCheckingUtils;
@@ -430,7 +431,14 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
         Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName)
                 .changeOldMentions(vi.getName(), instanceName);
 
-        if (!tc.checkStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition
+        boolean validTransition;
+        try {
+            validTransition = tc.checkStateSMT(prevState, expectState, fw.getPosition());
+        } catch (SMTUnknownError error) {
+            error.setDeclarationPosition(field.getDeclaringType().getPosition());
+            throw error;
+        }
+        if (!validTransition) { // Invalid field transition
             tc.throwStateRefinementError(fw.getPosition(), field.getDeclaringType().getPosition(), prevState,
                     expectState, stateChange.getMessage());
             return;
@@ -496,7 +504,12 @@ private static void changeState(TypeChecker tc, VariableInstance vi, RefinedFunc
             }
             expectState = expectState.changeOldMentions(vi.getName(), instanceName);
 
-            found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition());
+            try {
+                found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition());
+            } catch (SMTUnknownError error) {
+                error.setDeclarationPosition(stateChange.getFromPosition());
+                throw error;
+            }
             if (found && stateChange.hasTo()) {
                 String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter());
                 // Non-void: `_` is the return value; void: legacy alias for the new instance.