Abort when Kore's simplifier throws DecidePredicateUnknown (#392)

Fixes
runtimeverification/hs-backend-booster#373

This PR makes `kore-rpc-booster` return `"execute"` responses with
`"reason": "aborted"` in cases when Kore's simplifier fails due to
`DecidePredicateUnknown` in the post-exec simplification in `Proxy.hs`.

**Scenario before**
```
"execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> JsonRpcError`
``` 
returning `JsonRpcError` resulted in loosing information gained by
executing in booster for X steps + in kore for up to 1 step.
**Scenario now**
```
"execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> ExecuteResult {reason=Aborted, unknownPredicate = <predicate>}`
``` 
this this change, we return the reached state (may be branching) and do
not lose information anymore. Additionaly, we return the unknown
predicate, so that `pyk` can decide what to do with these.

PR to `pyk` that takes advantage of this feature by intrroducing
`Undecided` nodes to KCFG:
runtimeverification/pyk#744

---------

Co-authored-by: Samuel Balco <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: 4 people

booster/dev-tools/kore-rpc-dev/Server.hs

@@ -180,7 +180,7 @@ main = do
                         jsonRpcServer
                             srvSettings
                             (const $ respond koreRespond)
-                            [handleErrorCall, handleSomeException]
+                            [Kore.handleDecidePredicateUnknown, handleErrorCall, handleSomeException]
                     interruptHandler _ = do
                         when (logLevel >= LevelInfo) $
                             hPutStrLn stderr "[Info#proxy] Server shutting down"

booster/tools/booster/Proxy.hs

@@ -14,6 +14,7 @@ module Proxy (
 
 import Control.Concurrent.MVar qualified as MVar
 import Control.Monad (when)
+import Control.Monad.Catch (MonadCatch (..), catch)
 import Control.Monad.IO.Class (MonadIO, liftIO)
 import Control.Monad.Logger qualified as Log
 import Control.Monad.Trans.Except (runExcept)
@@ -43,6 +44,7 @@ import Kore.JsonRpc.Types qualified as ExecuteRequest (ExecuteRequest (..))
 import Kore.JsonRpc.Types qualified as SimplifyRequest (SimplifyRequest (..))
 import Kore.JsonRpc.Types.Log qualified as RPCLog
 import Kore.Log qualified
+import Kore.Log.DecidePredicateUnknown (DecidePredicateUnknown, externaliseDecidePredicateUnknown)
 import Kore.Syntax.Definition (SentenceAxiom)
 import Kore.Syntax.Json.Types qualified as KoreJson
 import SMT qualified
@@ -72,7 +74,7 @@ serverError detail = ErrorObj ("Server error: " <> detail) (-32032)
 respondEither ::
     forall m.
     Log.MonadLogger m =>
-    MonadIO m =>
+    (MonadIO m, MonadCatch m) =>
     ProxyConfig ->
     Respond (API 'Req) m (API 'Res) ->
     Respond (API 'Req) m (API 'Res) ->
@@ -418,7 +420,13 @@ respondEither ProxyConfig{statsVar, forceFallback, boosterState} booster kore re
     postExecSimplify ::
         LogSettings -> TimeSpec -> Maybe Text -> KoreDefinition -> API 'Res -> m (API 'Res)
     postExecSimplify logSettings start mbModule def = \case
-        Execute res -> Execute <$> simplifyResult res
+        Execute res ->
+            Execute
+                <$> ( simplifyResult res
+                        `catch` ( \(err :: DecidePredicateUnknown) ->
+                                    pure res{reason = Aborted, unknownPredicate = Just . externaliseDecidePredicateUnknown $ err}
+                                )
+                    )
         other -> pure other
       where
         -- timeLog :: TimeDiff -> Maybe [LogEntry]

booster/tools/booster/Server.hs

@@ -168,7 +168,7 @@ main = do
                             jsonRpcServer
                                 srvSettings
                                 (const $ Proxy.respondEither proxyConfig boosterRespond koreRespond)
-                                [handleErrorCall, handleSomeException]
+                                [Kore.handleDecidePredicateUnknown, handleErrorCall, handleSomeException]
                         interruptHandler _ = do
                             when (logLevel >= LevelInfo) $
                                 hPutStrLn stderr "[Info#proxy] Server shutting down"