519 - use SmtSolverError for all Smt-related errors in booster (#525)

As in the legacy backend, the SMT errors are caught at the top level in a handler. An `SMTError` is thrown generally when there is a problem with solver operations. Undecided predicates during rewriting and simplifications are reported back to the client as `SMTSolverError` (code 5) and include the predicates in play in the `data` field. Other errors are reported as runtime errors. As in the legacy backend, we lose all rewriting/simplification work done prior to the SMT error. Fixes #519  ## Summary by CodeRabbit - **New Features** - Introduced enhanced error handling for SMT operations, including specific error messages and responses. - Added a new `SetTimeout` feature to control solver operation timeout settings. - **Bug Fixes** - Improved SMT error handling with the addition of `handleSmtError` function, ensuring more robust and informative error responses. - **Refactor** - Updated various modules to improve error handling logic and to support new timeout control feature. - **Tests** - Added a new test case to validate the handling of unknown states in SMT model generation.
runtimeverification · Mar 5, 2024 · 099d445 · 099d445
1 parent fd23076
commit 099d445
Show file tree

Hide file tree

Showing 10 changed files with 168 additions and 26 deletions.
diff --git a/.coderabbit.yaml b/.coderabbit.yaml
@@ -0,0 +1,21 @@
+# coderabbit configuration, see https://coderabbit.ai/integrations/coderabbit-overrides.v2.json
+
+language: en        # default
+early_access: false # default
+chat:
+  auto_reply: false # default true
+
+reviews:
+  request_changes_workflow: false # default
+  high_level_summary: true # default
+  poem: false # default true
+  review_status: false # default true
+  collapse_walkthrough: false # default
+  path_filters: [] # file patterns (glob patterns) to exclude in a review
+  path_instructions: [] # adds some phrases (like "make sure to document things" for file patterns. ???
+  auto_review: 
+    enabled: true # default
+    ignore_title_keywords: [] # ignore PRs that have any of those words in the title
+    labels: ["rabbit-review"] # restrict automated reviews to PRs with one of these labels 
+    drafts: false # default
+    base_branches: [] # target branches (other than default) for which to review PRs
diff --git a/dev-tools/booster-dev/Server.hs b/dev-tools/booster-dev/Server.hs
@@ -26,7 +26,7 @@ import Booster.CLOptions
 import Booster.Definition.Base (KoreDefinition (..))
 import Booster.Definition.Ceil (computeCeilsDefinition)
 import Booster.GlobalState
-import Booster.JsonRpc (ServerState (..), respond)
+import Booster.JsonRpc (ServerState (..), handleSmtError, respond)
 import Booster.LLVM as LLVM (API)
 import Booster.LLVM.Internal (mkAPI, withDLib)
 import Booster.SMT.Interface qualified as SMT
@@ -129,7 +129,7 @@ runServer port definitions defaultMain mLlvmLibrary mSMTOptions (logLevel, custo
             jsonRpcServer
                 srvSettings
                 (const $ respond stateVar)
-                [RpcError.handleErrorCall, RpcError.handleSomeException]
+                [handleSmtError, RpcError.handleErrorCall, RpcError.handleSomeException]
   where
     levelFilter _source lvl =
         lvl `elem` customLevels || lvl >= logLevel && lvl <= LevelError

diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs
@@ -9,6 +9,7 @@ License     : BSD-3-Clause
 module Booster.JsonRpc (
     ServerState (..),
     respond,
+    handleSmtError,
     RpcTypes.rpcJsonConfig,
     execStateToKoreJson,
     toExecState,
@@ -23,6 +24,7 @@ import Control.Monad.Logger.CallStack (MonadLoggerIO)
 import Control.Monad.Logger.CallStack qualified as Log
 import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
 import Crypto.Hash (SHA256 (..), hashWith)
+import Data.Aeson (ToJSON (toJSON))
 import Data.Bifunctor (second)
 import Data.Coerce (coerce)
 import Data.Foldable
@@ -31,6 +33,7 @@ import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
 import Data.Maybe (catMaybes, fromMaybe, isJust, mapMaybe)
 import Data.Sequence (Seq)
+import Data.Set qualified as Set
 import Data.Text (Text, pack)
 import Data.Text qualified as Text
 import Data.Text.Encoding qualified as Text
@@ -75,10 +78,8 @@ import Booster.Syntax.ParsedKore.Base hiding (ParsedModule)
 import Booster.Syntax.ParsedKore.Base qualified as ParsedModule (ParsedModule (..))
 import Booster.Syntax.ParsedKore.Internalise (addToDefinitions)
 import Booster.Util (Flag (..), constructorName)
-import Data.Aeson (ToJSON (toJSON))
-import Data.Set qualified as Set
 import Kore.JsonRpc.Error qualified as RpcError
-import Kore.JsonRpc.Server
+import Kore.JsonRpc.Server (ErrorObj (..), JsonRpcHandler (..), Respond)
 import Kore.JsonRpc.Types qualified as RpcTypes
 import Kore.JsonRpc.Types.Log
 import Kore.Syntax.Json.Types (Id (..))
@@ -465,6 +466,23 @@ respond stateVar =
             Nothing -> pure $ Left $ RpcError.backendError RpcError.CouldNotFindModule mainName
             Just d -> action (d, state.mLlvmLibrary, state.mSMTOptions)
 
+handleSmtError :: JsonRpcHandler
+handleSmtError = JsonRpcHandler $ \case
+    SMT.GeneralSMTError err -> runtimeError "problem" err
+    SMT.SMTTranslationError err -> runtimeError "translation" err
+    SMT.SMTSolverUnknown premises preds -> do
+        Log.logErrorNS "booster" $ "SMT returned unknown: " <> "FIXME"
+
+        let bool = externaliseSort Pattern.SortBool -- predicates are terms of sort Bool
+            externalise = Syntax.KJAnd bool . map (externalisePredicate bool) . Set.toList
+            allPreds = addHeader $ Syntax.KJAnd bool [externalise premises, externalise preds]
+        pure $ RpcError.backendError RpcError.SmtSolverError $ toJSON allPreds
+  where
+    runtimeError prefix err = do
+        let msg = "SMT " <> prefix <> ": " <> err
+        Log.logErrorNS "booster" msg
+        pure $ RpcError.runtimeError msg
+
 data ServerState = ServerState
     { definitions :: Map Text KoreDefinition
     -- ^ definitions for each loaded module as main module

diff --git a/library/Booster/SMT/Base.hs b/library/Booster/SMT/Base.hs
@@ -66,6 +66,7 @@ getComment (DeclareFunc c _ _ _) = c
 data ControlCommand
     = Push -- Int
     | Pop -- Int
+    | SetTimeout Int
     | Exit
     deriving stock (Eq, Ord, Show)
 

diff --git a/library/Booster/SMT/Interface.hs b/library/Booster/SMT/Interface.hs
@@ -4,6 +4,7 @@ License     : BSD-3-Clause
 -}
 module Booster.SMT.Interface (
     SMTContext, -- re-export
+    SMTError (..),
     SMTOptions (..),
     defaultSMTOptions,
     initSolver,
@@ -12,6 +13,7 @@ module Booster.SMT.Interface (
     checkPredicates,
 ) where
 
+import Control.Exception (Exception, throw)
 import Control.Monad
 import Control.Monad.Logger qualified as Log
 import Control.Monad.Trans.Class
@@ -24,7 +26,7 @@ import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Set (Set)
 import Data.Set qualified as Set
-import Data.Text as Text (Text, pack, unpack, unwords)
+import Data.Text as Text (Text, pack, unlines, unwords)
 import Prettyprinter (Pretty, pretty, vsep)
 
 import Booster.Definition.Base
@@ -50,6 +52,26 @@ data SMTOptions = SMTOptions
     }
     deriving (Eq, Show)
 
+data SMTError
+    = GeneralSMTError Text
+    | SMTTranslationError Text
+    | SMTSolverUnknown (Set Predicate) (Set Predicate)
+    deriving (Eq, Show)
+
+instance Exception SMTError
+
+throwSMT :: Text -> a
+throwSMT = throw . GeneralSMTError
+
+throwSMT' :: String -> a
+throwSMT' = throwSMT . pack
+
+throwUnknown :: Set Predicate -> Set Predicate -> a
+throwUnknown premises preds = throw $ SMTSolverUnknown premises preds
+
+smtTranslateError :: Text -> a
+smtTranslateError = throw . SMTTranslationError
+
 defaultSMTOptions :: SMTOptions
 defaultSMTOptions =
     SMTOptions
@@ -62,13 +84,14 @@ defaultSMTOptions =
 initSolver :: Log.MonadLoggerIO io => KoreDefinition -> SMTOptions -> io SMT.SMTContext
 initSolver def smtOptions = do
     ctxt <- mkContext smtOptions.transcript
+    -- set timeout value before doing anything with the solver
+    runSMT ctxt $ runCmd_ $ SetTimeout smtOptions.timeout
     logSMT "Checking definition prelude"
-    -- FIXME set timeout value before doing anything with the solver
     let prelude = smtDeclarations def
     case prelude of
         Left err -> do
             logSMT $ "Error translating definition to SMT: " <> err
-            error $ "Unable to translate elements of the definition to SMT: " <> Text.unpack err
+            throwSMT $ "Unable to translate elements of the definition to SMT: " <> err
         Right{} -> pure ()
     check <-
         runSMT ctxt $
@@ -78,7 +101,7 @@ initSolver def smtOptions = do
         other -> do
             logSMT $ "Initial SMT definition check returned " <> pack (show other)
             closeContext ctxt
-            error $
+            throwSMT' $
                 "Aborting due to potentially-inconsistent SMT setup: Initial check returned " <> show other
 
 closeSolver :: Log.MonadLoggerIO io => SMT.SMTContext -> io ()
@@ -124,13 +147,14 @@ getModelFor ctxt ps subst
                 Set.unions $
                     Map.keysSet subst : map ((.variables) . getAttributes . coerce) ps
         when (isLeft translated) $
-            error . Text.unpack $
-                fromLeft' translated
+            smtTranslateError (fromLeft' translated)
         let (smtAsserts, transState) = fromRight' translated
             freeVarsMap =
                 Map.filterWithKey
                     (const . (`Set.member` Set.map Var freeVars))
                     transState.mappings
+            getVar (Var v) = v
+            getVar other = smtTranslateError . pack $ "Solver returned non-var in translation state: " <> show other
             freeVarsToSExprs = Map.mapKeys getVar $ Map.map Atom freeVarsMap
 
         runCmd_ SMT.Push -- assuming the prelude has been run already,
@@ -151,7 +175,7 @@ getModelFor ctxt ps subst
         case satResponse of
             Error msg -> do
                 runCmd_ SMT.Pop
-                error $ "SMT Error: " <> BS.unpack msg
+                throwSMT' $ BS.unpack msg
             Unsat -> do
                 runCmd_ SMT.Pop
                 pure $ Left Unsat
@@ -160,10 +184,10 @@ getModelFor ctxt ps subst
                 pure $ Left Unknown
             Values{} -> do
                 runCmd_ SMT.Pop
-                error $ "Unexpected SMT response " <> show satResponse
+                throwSMT' $ "Unexpected SMT response to CheckSat: " <> show satResponse
             Success -> do
                 runCmd_ SMT.Pop
-                error $ "Unexpected SMT response " <> show satResponse
+                throwSMT' $ "Unexpected SMT response to CheckSat: " <> show satResponse
             Sat -> do
                 response <-
                     if Map.null freeVarsToSExprs
@@ -172,7 +196,7 @@ getModelFor ctxt ps subst
                 runCmd_ SMT.Pop
                 case response of
                     Error msg ->
-                        error $ "SMT Error: " <> BS.unpack msg
+                        throwSMT' $ BS.unpack msg
                     Values pairs ->
                         let (errors, values) =
                                 Map.partition isLeft
@@ -181,15 +205,12 @@ getModelFor ctxt ps subst
                          in if null errors
                                 then pure $ Right $ Map.map fromRight' values
                                 else
-                                    error . unlines $
+                                    throwSMT . Text.unlines $
                                         ( "SMT errors while converting results: "
-                                            : map (Text.unpack . fromLeft') (Map.elems errors)
+                                            : map fromLeft' (Map.elems errors)
                                         )
                     other ->
-                        error $ "Unexpected SMT response to GetValue: " <> show other
-  where
-    getVar (Var v) = v
-    getVar _ = error "not a var"
+                        throwSMT' $ "Unexpected SMT response to GetValue: " <> show other
 
 mkComment :: Pretty a => a -> BS.ByteString
 mkComment = BS.pack . Pretty.renderDefault . pretty
@@ -281,10 +302,13 @@ checkPredicates ctxt givenPs givenSubst psToCheck
                 <> pack (show (positive, negative))
 
         case (positive, negative) of
-            (Unsat, Unsat) -> fail "should have been caught above"
-            (_, Unsat) -> pure True
-            (Unsat, _) -> pure False
-            _anythingElse_ -> fail "Both Sat, Unknown results, or error"
+            (Unsat, Unsat) -> throwSMT "Inconsistent ground truth: should have been caught above"
+            (Sat, Sat) -> fail "Implication not determined"
+            (Sat, Unsat) -> pure True
+            (Unsat, Sat) -> pure False
+            (Unknown, _) -> throwUnknown givenPs psToCheck
+            (_, Unknown) -> throwUnknown givenPs psToCheck
+            other -> throwSMT' $ "Unexpected result while checking a condition: " <> show other
   where
     smtRun_ :: SMTEncode c => c -> MaybeT (SMT io) ()
     smtRun_ = lift . SMT.runCmd_

diff --git a/library/Booster/SMT/Runner.hs b/library/Booster/SMT/Runner.hs
@@ -162,6 +162,9 @@ instance SMTEncode QueryCommand where
 instance SMTEncode ControlCommand where
     encode Push = "(push)"
     encode Pop = "(pop)"
+    encode (SetTimeout n)
+        | n > 0 = "(set-option :timeout " <> BS.string7 (show n) <> ")"
+        | otherwise = error $ "Illegal SMT timeout value " <> show n
     encode Exit = "(exit)"
 
     comment _ = Just ";;;;;;;\n"

diff --git a/test/rpc-integration/test-get-model/README.md b/test/rpc-integration/test-get-model/README.md
@@ -17,3 +17,6 @@ For the time being, this is testing the pass-through of `get-model` requests to
 * a trivial satisfiable predicate without variables
   - Input kore term: ` 0 <= 0`
   - Result: `sat`, no substitution
+* a predicate that causes the SMT solver to return `Unknown`
+  - Input kore term: `X == X ^ 256`
+  - Result: `unknown`, no substitution
diff --git a/test/rpc-integration/test-get-model/response-smt-unknown.json b/test/rpc-integration/test-get-model/response-smt-unknown.json
@@ -0,0 +1 @@
+{"jsonrpc":"2.0","id":1,"result":{"satisfiable":"Unknown"}}
diff --git a/test/rpc-integration/test-get-model/state-smt-unknown.get-model b/test/rpc-integration/test-get-model/state-smt-unknown.get-model
@@ -0,0 +1,67 @@
+{
+  "format": "KORE",
+  "version": 1,
+  "term": {
+    "tag": "Equals",
+    "argSort": {
+      "tag": "SortApp",
+      "name": "SortBool",
+      "args": []
+    },
+    "sort": {
+      "tag": "SortApp",
+      "name": "SortBool",
+      "args": []
+    },
+    "first": {
+      "tag": "DV",
+      "sort": {
+        "tag": "SortApp",
+        "name": "SortBool",
+        "args": []
+      },
+      "value": "true"
+    },
+    "second": {
+      "tag": "App",
+      "name": "Lbl'UndsEqlsEqls'Int'Unds'",
+      "sorts": [],
+      "args": [
+        {
+          "tag": "EVar",
+          "name": "X",
+          "sort": {
+            "tag": "SortApp",
+            "name": "SortInt",
+            "args": []
+          }
+        },
+        {
+          "tag": "App",
+          "name": "Lbl'UndsXor-'Int'Unds'",
+          "sorts": [],
+          "args": [
+            {
+              "tag": "EVar",
+              "name": "X",
+              "sort": {
+                "tag": "SortApp",
+                "name": "SortInt",
+                "args": []
+              }
+            },
+            {
+              "tag": "DV",
+              "sort": {
+                "tag": "SortApp",
+                "name": "SortInt",
+                "args": []
+              },
+              "value": "256"
+            }
+          ]
+        }
+      ]
+    }
+  }
+}
diff --git a/tools/booster/Server.hs b/tools/booster/Server.hs
@@ -197,7 +197,11 @@ main = do
                         jsonRpcServer
                             srvSettings
                             (const $ Proxy.respondEither proxyConfig boosterRespond koreRespond)
-                            [Kore.handleDecidePredicateUnknown, handleErrorCall, handleSomeException]
+                            [ Kore.handleDecidePredicateUnknown
+                            , Booster.handleSmtError
+                            , handleErrorCall
+                            , handleSomeException
+                            ]
                     interruptHandler _ = do
                         when (logLevel >= LevelInfo) $
                             IO.hPutStrLn IO.stderr "[Info#proxy] Server shutting down"
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		{"jsonrpc":"2.0","id":1,"result":{"satisfiable":"Unknown"}}