Abort on "Unknown" side conditions, don't crash (#3907)

This PR makes sure we do not immediately hard-stop with an RPC error
when receiving `Unknown` from Z3 in Booster.

- use pure exceptions in SMT functions, check results at call sites to
`checkPredicates`
- threat Z3-`Unknown` predicates as any other unclear conditions: abort
rewriting

Author: geo2a

booster/library/Booster/Pattern/Rewrite.hs

@@ -359,7 +359,8 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
             checkAllRequires <- SMT.checkPredicates solver prior mempty (Set.fromList unclearRequires)
 
             case checkAllRequires of
-                Nothing -> do
+                Left _ -> do
+                    -- TODO: we could process SMTError here
                     -- unclear even with the prior
                     withContext "abort" $
                         logMessage $
@@ -369,11 +370,11 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
                         RuleConditionUnclear rule . coerce $
                             foldl1 AndTerm $
                                 map coerce unclearRequires
-                Just False -> do
+                Right False -> do
                     -- requires is actually false given the prior
                     withContext "failure" $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
                     RewriteRuleAppT $ pure NotApplied
-                Just True ->
+                Right True ->
                     -- can proceed
                     pure ()
         Nothing ->
@@ -397,7 +398,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
     -- check all new constraints together with the known side constraints
     whenJust mbSolver $ \solver ->
         (lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case
-            Just False -> do
+            Right False -> do
                 withContext "success" $ logMessage ("New constraints evaluated to #Bottom." :: Text)
                 RewriteRuleAppT $ pure Trivial
             _other -> pure ()

booster/library/Booster/SMT/Interface.hs

@@ -16,7 +16,7 @@ module Booster.SMT.Interface (
 import Control.Exception (Exception, throw)
 import Control.Monad
 import Control.Monad.Trans.Class
-import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Except
 import Data.ByteString.Char8 qualified as BS
 import Data.Coerce
 import Data.Either (isLeft)
@@ -68,9 +68,6 @@ throwSMT = throw . GeneralSMTError
 throwSMT' :: String -> a
 throwSMT' = throwSMT . pack
 
-throwUnknown :: Text -> Set Predicate -> Set Predicate -> a
-throwUnknown reason premises preds = throw $ SMTSolverUnknown reason premises preds
-
 smtTranslateError :: Text -> a
 smtTranslateError = throw . SMTTranslationError
 
@@ -266,14 +263,14 @@ checkPredicates ::
     Set Predicate ->
     Map Variable Term ->
     Set Predicate ->
-    io (Maybe Bool)
+    io (Either SMTError Bool)
 checkPredicates ctxt givenPs givenSubst psToCheck
-    | null psToCheck = pure $ Just True -- or Nothing?
+    | null psToCheck = pure $ Right True
     | Left errMsg <- translated = Log.withContext "smt" $ do
         Log.logErrorNS "booster" $ "SMT translation error: " <> errMsg
         Log.logMessage $ "SMT translation error: " <> errMsg
-        pure Nothing
-    | Right ((smtGiven, sexprsToCheck), transState) <- translated = Log.withContext "smt" $ runSMT ctxt . runMaybeT $ do
+        pure . Left . SMTTranslationError $ errMsg
+    | Right ((smtGiven, sexprsToCheck), transState) <- translated = Log.withContext "smt" $ runSMT ctxt . runExceptT $ do
         Log.logMessage $
             Text.unwords
                 [ "Checking"
@@ -302,8 +299,9 @@ checkPredicates ctxt givenPs givenSubst psToCheck
         consistent <- smtRun CheckSat
         when (consistent /= Sat) $ do
             void $ smtRun Pop
-            Log.logMessage ("Inconsistent ground truth, check returns Nothing" :: Text)
-            fail "returns nothing"
+            let errMsg = ("Inconsistent ground truth, check returns Nothing" :: Text)
+            Log.logMessage errMsg
+            throwE $ GeneralSMTError errMsg
 
         -- save ground truth for 2nd check
         smtRun_ Push
@@ -324,22 +322,22 @@ checkPredicates ctxt givenPs givenSubst psToCheck
 
         case (positive, negative) of
             (Unsat, Unsat) -> throwSMT "Inconsistent ground truth: should have been caught above"
-            (Sat, Sat) -> fail "Implication not determined"
+            (Sat, Sat) -> throwE $ GeneralSMTError "Implication not determined"
             (Sat, Unsat) -> pure True
             (Unsat, Sat) -> pure False
             (Unknown, _) -> do
                 smtRun GetReasonUnknown >>= \case
-                    ReasonUnknown reason -> throwUnknown reason givenPs psToCheck
+                    ReasonUnknown reason -> throwE $ SMTSolverUnknown reason givenPs psToCheck
                     other -> throwSMT' $ "Unexpected result while calling ':reason-unknown': " <> show other
             (_, Unknown) -> do
                 smtRun GetReasonUnknown >>= \case
-                    ReasonUnknown reason -> throwUnknown reason givenPs psToCheck
+                    ReasonUnknown reason -> throwE $ SMTSolverUnknown reason givenPs psToCheck
                     other -> throwSMT' $ "Unexpected result while calling ':reason-unknown': " <> show other
             other -> throwSMT' $ "Unexpected result while checking a condition: " <> show other
   where
-    smtRun_ :: SMTEncode c => c -> MaybeT (SMT io) ()
+    smtRun_ :: SMTEncode c => c -> ExceptT SMTError (SMT io) ()
     smtRun_ = lift . SMT.runCmd_
-    smtRun :: SMTEncode c => c -> MaybeT (SMT io) Response
+    smtRun :: SMTEncode c => c -> ExceptT SMTError (SMT io) Response
     smtRun = lift . SMT.runCmd
 
     translated = SMT.runTranslator $ do