Update dependency: deps/haskell-backend_release (#557)

* Add the response from `:reason-unknown` when SMT response is unknown * Update kore-rpc error types --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Sam Balco <goodlyrottenapple@gmail.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Jost Berthold <jost.berthold@runtimeverification.com>
runtimeverification · Mar 25, 2024 · f18a030 · f18a030
1 parent 99a39cb
commit f18a030
Show file tree

Hide file tree

Showing 22 changed files with 327 additions and 248 deletions.
diff --git a/cabal.project b/cabal.project
@@ -5,7 +5,7 @@ packages:
 source-repository-package
     type: git
     location: https://github.com/runtimeverification/haskell-backend.git
-    tag: 093af3153a5e07626d9b2e628d7ad4fc77c5a723
+    tag: 8f97e95b77fe590a9fe5a9b0212f32fcad0be35b
     subdir: kore kore-rpc-types
 
 source-repository-package

diff --git a/deps/haskell-backend_release b/deps/haskell-backend_release
@@ -1 +1 @@
-093af3153a5e07626d9b2e628d7ad4fc77c5a723
+8f97e95b77fe590a9fe5a9b0212f32fcad0be35b
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -2,7 +2,7 @@
   description = "hs-backend-booster";
 
   inputs = {
-    haskell-backend.url = "github:runtimeverification/haskell-backend/093af3153a5e07626d9b2e628d7ad4fc77c5a723";
+    haskell-backend.url = "github:runtimeverification/haskell-backend/8f97e95b77fe590a9fe5a9b0212f32fcad0be35b";
     stacklock2nix.follows = "haskell-backend/stacklock2nix";
     nixpkgs.follows = "haskell-backend/nixpkgs";
   };

diff --git a/library/Booster/JsonRpc.hs b/library/Booster/JsonRpc.hs
@@ -24,7 +24,6 @@ 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
@@ -70,13 +69,14 @@ import Booster.Syntax.Json.Internalise (
     TermOrPredicates (..),
     internalisePattern,
     internaliseTermOrPredicate,
+    patternErrorToRpcError,
     pattern CheckSubsorts,
     pattern DisallowAlias,
  )
 import Booster.Syntax.ParsedKore (parseKoreModule)
 import Booster.Syntax.ParsedKore.Base hiding (ParsedModule)
 import Booster.Syntax.ParsedKore.Base qualified as ParsedModule (ParsedModule (..))
-import Booster.Syntax.ParsedKore.Internalise (addToDefinitions)
+import Booster.Syntax.ParsedKore.Internalise (addToDefinitions, definitionErrorToRpcError)
 import Booster.Util (Flag (..), constructorName)
 import Kore.JsonRpc.Error qualified as RpcError
 import Kore.JsonRpc.Server (ErrorObj (..), JsonRpcHandler (..), Respond)
@@ -105,7 +105,12 @@ respond stateVar =
             case internalised of
                 Left patternError -> do
                     Log.logDebug $ "Error internalising cterm" <> Text.pack (show patternError)
-                    pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternError
+                    pure $
+                        Left $
+                            RpcError.backendError $
+                                RpcError.CouldNotVerifyPattern
+                                    [ patternErrorToRpcError patternError
+                                    ]
                 Right (pat, substitution, unsupported) -> do
                     unless (null unsupported) $ do
                         Log.logWarnNS
@@ -153,46 +158,43 @@ respond stateVar =
             state <- liftIO $ takeMVar stateVar
             let nameAsId = fromMaybe False nameAsId'
                 moduleHash = Text.pack $ ('m' :) . show . hashWith SHA256 $ Text.encodeUtf8 _module
-                restoreStateAndRethrow (errTy, errMsg) = do
+                restoreStateAndRethrow err = do
                     liftIO (putMVar stateVar state)
-                    throwE $ RpcError.backendError errTy errMsg
+                    throwE $ RpcError.backendError err
                 listNames :: (HasField "name" a b, HasField "getId" b Text) => [a] -> Text
                 listNames = Text.intercalate ", " . map (.name.getId)
 
             flip catchE restoreStateAndRethrow $ do
                 newModule <-
-                    withExceptT ((RpcError.InvalidModule,) . toJSON) $
+                    withExceptT (RpcError.InvalidModule . RpcError.ErrorOnly . pack) $
                         except $
                             parseKoreModule "rpc-request" _module
 
                 unless (null newModule.sorts) $
-                    throwE
-                        ( RpcError.InvalidModule
-                        , toJSON $
+                    throwE $
+                        RpcError.InvalidModule . RpcError.ErrorOnly $
                             "Module introduces new sorts: " <> listNames newModule.sorts
-                        )
+
                 unless (null newModule.symbols) $
-                    throwE
-                        ( RpcError.InvalidModule
-                        , toJSON $
+                    throwE $
+                        RpcError.InvalidModule . RpcError.ErrorOnly $
                             "Module introduces new symbols: " <> listNames newModule.symbols
-                        )
 
                 -- check if we already received a module with this name
                 when nameAsId $
                     case Map.lookup (getId newModule.name) state.addedModules of
                         -- if a different module was already added, throw error
-                        Just m | _module /= m -> throwE (RpcError.DuplicateModuleName, toJSON $ getId newModule.name)
+                        Just m | _module /= m -> throwE $ RpcError.DuplicateModuleName $ getId newModule.name
                         _ -> pure ()
 
                 -- Check for a corner case when we send module M1 with the name "m<hash of M2>"" and name-as-id: true
                 -- followed by adding M2. Should not happen in practice...
                 case Map.lookup moduleHash state.addedModules of
-                    Just m | _module /= m -> throwE (RpcError.DuplicateModuleName, toJSON moduleHash)
+                    Just m | _module /= m -> throwE $ RpcError.DuplicateModuleName moduleHash
                     _ -> pure ()
 
                 newDefinitions <-
-                    withExceptT ((RpcError.InvalidModule,) . toJSON) $
+                    withExceptT (RpcError.InvalidModule . definitionErrorToRpcError) $
                         except $
                             runExcept $
                                 addToDefinitions newModule{ParsedModule.name = Id moduleHash} state.definitions
@@ -246,13 +248,18 @@ respond stateVar =
 
             result <- case internalised of
                 Left patternErrors -> do
-                    Log.logErrorNS "booster" $
-                        "Error internalising cterm: " <> Text.pack (show patternErrors)
+                    forM_ patternErrors $ \patternError ->
+                        Log.logErrorNS "booster" $
+                            "Error internalising cterm: " <> pack (show patternError)
                     Log.logOtherNS
                         "booster"
                         (Log.LevelOther "ErrorDetails")
                         (prettyPattern req.state.term)
-                    pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternErrors
+                    pure $
+                        Left $
+                            RpcError.backendError $
+                                RpcError.CouldNotVerifyPattern $
+                                    map patternErrorToRpcError patternErrors
                 -- term and predicate (pattern)
                 Right (TermAndPredicates pat substitution unsupported) -> do
                     Log.logInfoNS "booster" "Simplifying a pattern"
@@ -282,11 +289,11 @@ respond stateVar =
                         (Left ApplyEquations.SideConditionFalse{}, _) -> do
                             let tSort = externaliseSort $ sortOfPattern pat
                             pure $ Right (addHeader $ KoreJson.KJBottom tSort, [])
-                        (Left (ApplyEquations.EquationLoop terms), _) ->
-                            pure . Left . RpcError.backendError RpcError.Aborted $ map externaliseTerm terms -- FIXME
+                        (Left (ApplyEquations.EquationLoop _terms), _) ->
+                            pure . Left . RpcError.backendError $ RpcError.Aborted "equation loop detected"
                         (Left other, _) ->
-                            pure . Left . RpcError.backendError RpcError.Aborted $ (Text.pack . constructorName $ other) -- FIXME
-                            -- predicate only
+                            pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
+                -- predicate only
                 Right (Predicates ps)
                     | null ps.boolPredicates && null ps.ceilPredicates && null ps.substitution && null ps.unsupported ->
                         pure $
@@ -324,7 +331,7 @@ respond stateVar =
 
                                     pure $ Right (addHeader $ Syntax.KJAnd predicateSort result, [])
                                 (Left something, _) ->
-                                    pure . Left . RpcError.backendError RpcError.Aborted $ show something
+                                    pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty something
             whenJust solver SMT.closeSolver
             stop <- liftIO $ getTime Monotonic
 
@@ -344,13 +351,18 @@ respond stateVar =
                             internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term
                 case internalised of
                     Left patternErrors -> do
-                        Log.logErrorNS "booster" $
-                            "Error internalising cterm: " <> Text.pack (show patternErrors)
+                        forM_ patternErrors $ \patternError ->
+                            Log.logErrorNS "booster" $
+                                "Error internalising cterm: " <> pack (show patternError)
                         Log.logOtherNS
                             "booster"
                             (Log.LevelOther "ErrorDetails")
                             (prettyPattern req.state.term)
-                        pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternErrors
+                        pure $
+                            Left $
+                                RpcError.backendError $
+                                    RpcError.CouldNotVerifyPattern $
+                                        map patternErrorToRpcError patternErrors
                     -- various predicates obtained
                     Right things -> do
                         Log.logInfoNS "booster" "get-model request"
@@ -414,13 +426,18 @@ respond stateVar =
                                     { satisfiable = RpcTypes.Unsat
                                     , substitution = Nothing
                                     }
+                            Left SMT.ReasonUnknown{} ->
+                                RpcTypes.GetModelResult
+                                    { satisfiable = RpcTypes.Unknown
+                                    , substitution = Nothing
+                                    }
                             Left SMT.Unknown ->
                                 RpcTypes.GetModelResult
                                     { satisfiable = RpcTypes.Unknown
                                     , substitution = Nothing
                                     }
                             Left other ->
-                                error $ "Unexpected result " <> show other <> "from getModelFor"
+                                error $ "Unexpected result " <> show other <> " from getModelFor"
                             Right subst ->
                                 let sort = fromMaybe (error "Unknown sort in input") $ sortOfJson req.state.term
                                     substitution
@@ -463,20 +480,20 @@ respond stateVar =
         state <- liftIO $ readMVar stateVar
         let mainName = fromMaybe state.defaultMain mbMainModule
         case Map.lookup mainName state.definitions of
-            Nothing -> pure $ Left $ RpcError.backendError RpcError.CouldNotFindModule mainName
+            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
+    SMT.SMTSolverUnknown reason premises preds -> do
         Log.logErrorNS "booster" "SMT returned `Unknown'"
 
         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
+        pure $ RpcError.backendError $ RpcError.SmtSolverError $ RpcError.ErrorWithTerm reason allPreds
   where
     runtimeError prefix err = do
         let msg = "SMT " <> prefix <> ": " <> err

diff --git a/library/Booster/JsonRpc/Utils.hs b/library/Booster/JsonRpc/Utils.hs
@@ -21,6 +21,7 @@ import Data.Aeson as Json
 import Data.Aeson.Encode.Pretty (encodePretty')
 import Data.Aeson.Types (parseMaybe)
 import Data.ByteString.Lazy.Char8 qualified as BS
+
 import Data.Maybe (fromMaybe)
 import Network.JSONRPC
 import Prettyprinter
@@ -33,8 +34,12 @@ import System.Process (readProcessWithExitCode)
 import Booster.Definition.Base qualified as Internal
 import Booster.Prettyprinter
 import Booster.Syntax.Json.Internalise
+import Data.Binary.Builder (fromLazyByteString, toLazyByteString)
+import Data.List (intersperse)
 import Data.Map qualified as Map
 import Data.Set qualified as Set
+import Data.Text.Encoding qualified as Text
+import Kore.JsonRpc.Error qualified as RpcError
 import Kore.JsonRpc.Types
 import Kore.Syntax.Json.Types hiding (Left, Right)
 import Prettyprinter qualified as Pretty
@@ -256,7 +261,21 @@ diffBy def pat1 pat2 =
             <> if null u then "" else BS.unlines ("Unsupported parts: " : map Json.encode u)
     internalise =
         either
-            (("Pattern could not be internalised: " <>) . Json.encode)
+            ( ("Pattern could not be internalised: " <>)
+                . toLazyByteString
+                . prettyRpcErrors
+                . map patternErrorToRpcError
+            )
             renderBS
             . runExcept
             . internaliseTermOrPredicate DisallowAlias IgnoreSubsorts Nothing def
+    prettyRpcErrors = \case
+        [] -> "unknown error"
+        [e] -> prettyRpcError e
+        (e : es) -> prettyRpcError e <> "\n" <> prettyRpcErrors es
+
+    prettyRpcError RpcError.ErrorWithTermAndContext{error = err, term, context} =
+        Text.encodeUtf8Builder err
+            <> "\n"
+            <> maybe "" ((<> "\n") . fromLazyByteString . Json.encode) term
+            <> maybe "" (mconcat . intersperse ", " . map Text.encodeUtf8Builder) context
diff --git a/library/Booster/SMT/Base.hs b/library/Booster/SMT/Base.hs
@@ -14,6 +14,7 @@ import Data.ByteString.Char8 qualified as BS
 import Data.Data (Data)
 import Data.Hashable (Hashable)
 import Data.String
+import Data.Text (Text)
 import GHC.Generics (Generic)
 import Language.Haskell.TH.Syntax (Lift)
 
@@ -73,6 +74,7 @@ data ControlCommand
 data QueryCommand
     = CheckSat
     | GetValue [SExpr] -- for get-model
+    | GetReasonUnknown
     deriving stock (Eq, Ord, Show)
 
 data Response
@@ -81,6 +83,7 @@ data Response
     | Unsat
     | Unknown
     | Values [(SExpr, Value)]
+    | ReasonUnknown Text
     | Error BS.ByteString
     deriving stock (Eq, Ord, Show)
 

diff --git a/library/Booster/SMT/Interface.hs b/library/Booster/SMT/Interface.hs
@@ -55,7 +55,7 @@ data SMTOptions = SMTOptions
 data SMTError
     = GeneralSMTError Text
     | SMTTranslationError Text
-    | SMTSolverUnknown (Set Predicate) (Set Predicate)
+    | SMTSolverUnknown Text (Set Predicate) (Set Predicate)
     deriving (Eq, Show)
 
 instance Exception SMTError
@@ -66,8 +66,8 @@ throwSMT = throw . GeneralSMTError
 throwSMT' :: String -> a
 throwSMT' = throwSMT . pack
 
-throwUnknown :: Set Predicate -> Set Predicate -> a
-throwUnknown premises preds = throw $ SMTSolverUnknown premises preds
+throwUnknown :: Text -> Set Predicate -> Set Predicate -> a
+throwUnknown reason premises preds = throw $ SMTSolverUnknown reason premises preds
 
 smtTranslateError :: Text -> a
 smtTranslateError = throw . SMTTranslationError
@@ -179,9 +179,12 @@ getModelFor ctxt ps subst
             Unsat -> do
                 runCmd_ SMT.Pop
                 pure $ Left Unsat
-            Unknown -> do
+            Unknown{} -> do
+                res <- runCmd SMT.GetReasonUnknown
                 runCmd_ SMT.Pop
-                pure $ Left Unknown
+                pure $ Left res
+            r@ReasonUnknown{} ->
+                pure $ Left r
             Values{} -> do
                 runCmd_ SMT.Pop
                 throwSMT' $ "Unexpected SMT response to CheckSat: " <> show satResponse
@@ -306,8 +309,14 @@ checkPredicates ctxt givenPs givenSubst psToCheck
             (Sat, Sat) -> fail "Implication not determined"
             (Sat, Unsat) -> pure True
             (Unsat, Sat) -> pure False
-            (Unknown, _) -> throwUnknown givenPs psToCheck
-            (_, Unknown) -> throwUnknown givenPs psToCheck
+            (Unknown, _) -> do
+                smtRun GetReasonUnknown >>= \case
+                    ReasonUnknown reason -> throwUnknown reason givenPs psToCheck
+                    other -> throwSMT' $ "Unexpected result while calling ':reason-unknown': " <> show other
+            (_, Unknown) -> do
+                smtRun GetReasonUnknown >>= \case
+                    ReasonUnknown reason -> throwUnknown 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) ()
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		093af3153a5e07626d9b2e628d7ad4fc77c5a723
		8f97e95b77fe590a9fe5a9b0212f32fcad0be35b