Implement better booster logging

booster/library/Booster/CLOptions.hs

@@ -30,6 +30,9 @@ data CLOptions = CLOptions
     , llvmLibraryFile :: Maybe FilePath
     , port :: Int
     , logLevels :: [LogLevel]
+    , logTimeStamps :: Bool
+    , logContexts :: [String]
+    , notLogContexts :: [String]
     , simplificationLogFile :: Maybe FilePath
     , smtOptions :: Maybe SMTOptions
     , equationOptions :: EquationOptions
@@ -78,6 +81,26 @@ clOptionsParser =
                         )
                 )
             )
+        <*> switch (long "log-timestamps" <> help "Add timestamps to logs")
+        <*> many
+            ( option
+                str
+                ( metavar "CONTEXT"
+                    <> long "log-context"
+                    <> short 'c'
+                    <> help
+                        "Log context"
+                )
+            )
+        <*> many
+            ( option
+                str
+                ( metavar "CONTEXT"
+                    <> long "not-log-context"
+                    <> help
+                        "Not in log context"
+                )
+            )
         <*> optional
             ( strOption
                 ( metavar "JSON_LOG_FILE"

booster/library/Booster/Definition/Ceil.hs

@@ -14,6 +14,7 @@ import Booster.Pattern.ApplyEquations
 import Booster.Pattern.Base
 
 import Booster.LLVM as LLVM (API, simplifyBool)
+import Booster.Log
 import Booster.Pattern.Bool
 import Booster.Pattern.Util (isConcrete, sortOfTerm)
 import Booster.Util (Flag (..))
@@ -73,7 +74,7 @@ instance Pretty ComputeCeilSummary where
                         ]
 
 computeCeilsDefinition ::
-    MonadLoggerIO io => Maybe LLVM.API -> KoreDefinition -> io (KoreDefinition, [ComputeCeilSummary])
+    LoggerMIO io => Maybe LLVM.API -> KoreDefinition -> io (KoreDefinition, [ComputeCeilSummary])
 computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory} = do
     (rewriteTheory', ceilSummaries) <-
         runWriterT $
@@ -87,7 +88,7 @@ computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory} = do
     pure (def{rewriteTheory = rewriteTheory'}, toList ceilSummaries)
 
 computeCeilRule ::
-    MonadLoggerIO io =>
+    LoggerMIO io =>
     Maybe LLVM.API ->
     KoreDefinition ->
     RewriteRule.RewriteRule "Rewrite" ->

booster/library/Booster/JsonRpc.hs

@@ -20,7 +20,6 @@ import Control.Concurrent (MVar, putMVar, readMVar, takeMVar)
 import Control.Monad
 import Control.Monad.Extra (whenJust)
 import Control.Monad.IO.Class
-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)
@@ -45,12 +44,9 @@ import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId)
 import Booster.Definition.Base (KoreDefinition (..))
 import Booster.Definition.Base qualified as Definition (RewriteRule (..))
 import Booster.LLVM as LLVM (API)
+import Booster.Log
 import Booster.Pattern.ApplyEquations qualified as ApplyEquations
-import Booster.Pattern.Base (
-    Pattern (..),
-    Term,
-    Variable,
- )
+import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable)
 import Booster.Pattern.Base qualified as Pattern
 import Booster.Pattern.Rewrite (
     RewriteFailed (..),
@@ -69,6 +65,7 @@ import Booster.Syntax.Json.Internalise (
     TermOrPredicates (..),
     internalisePattern,
     internaliseTermOrPredicate,
+    logPatternError,
     patternErrorToRpcError,
     pattern CheckSubsorts,
     pattern DisallowAlias,
@@ -88,7 +85,7 @@ import Kore.Syntax.Json.Types qualified as Syntax
 
 respond ::
     forall m.
-    MonadLoggerIO m =>
+    LoggerMIO m =>
     MVar ServerState ->
     Respond (RpcTypes.API 'RpcTypes.Req) m (RpcTypes.API 'RpcTypes.Res)
 respond stateVar =
@@ -97,14 +94,14 @@ respond stateVar =
             | isJust req.stepTimeout -> pure $ Left $ RpcError.unsupportedOption ("step-timeout" :: String)
             | isJust req.movingAverageStepTimeout ->
                 pure $ Left $ RpcError.unsupportedOption ("moving-average-step-timeout" :: String)
-        RpcTypes.Execute req -> withContext req._module $ \(def, mLlvmLibrary, mSMTOptions) -> do
+        RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "execute" $ do
             start <- liftIO $ getTime Monotonic
             -- internalise given constrained term
             let internalised = runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing def req.state.term
 
             case internalised of
                 Left patternError -> do
-                    Log.logDebug $ "Error internalising cterm" <> Text.pack (show patternError)
+                    void $ Booster.Log.withContext "internalise" $ logPatternError patternError
                     pure $
                         Left $
                             RpcError.backendError $
@@ -113,13 +110,12 @@ respond stateVar =
                                     ]
                 Right (pat, substitution, unsupported) -> do
                     unless (null unsupported) $ do
+                        withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $
+                            logMessage ("ignoring unsupported predicate parts" :: Text)
                         Log.logWarnNS
                             "booster"
                             "Execute: ignoring unsupported predicate parts"
-                        Log.logOtherNS
-                            "booster"
-                            (Log.LevelOther "ErrorDetails")
-                            (Text.unlines $ map prettyPattern unsupported)
+
                     let cutPoints = fromMaybe [] req.cutPointRules
                         terminals = fromMaybe [] req.terminalRules
                         mbDepth = fmap RpcTypes.getNat req.maxDepth
@@ -153,7 +149,7 @@ respond stateVar =
                                         fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
                                 else Nothing
                     pure $ execResponse duration req result substitution unsupported
-        RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> runExceptT $ do
+        RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext "add-module" $ runExceptT $ do
             -- block other request executions while modifying the server state
             state <- liftIO $ takeMVar stateVar
             let nameAsId = fromMaybe False nameAsId'
@@ -211,10 +207,10 @@ respond stateVar =
                                 (if nameAsId then Map.insert (getId newModule.name) _module else id) $
                                     Map.insert moduleHash _module state.addedModules
                             }
-                Log.logInfo $
+                Booster.Log.logMessage $
                     "Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions)
                 pure $ RpcTypes.AddModule $ RpcTypes.AddModuleResult moduleHash
-        RpcTypes.Simplify req -> withContext req._module $ \(def, mLlvmLibrary, mSMTOptions) -> do
+        RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "simplify" $ do
             start <- liftIO $ getTime Monotonic
             let internalised =
                     runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term
@@ -249,8 +245,7 @@ respond stateVar =
             result <- case internalised of
                 Left patternErrors -> do
                     forM_ patternErrors $ \patternError ->
-                        Log.logErrorNS "booster" $
-                            "Error internalising cterm: " <> pack (show patternError)
+                        void $ Booster.Log.withContext "internalise" $ logPatternError patternError
                     Log.logOtherNS
                         "booster"
                         (Log.LevelOther "ErrorDetails")
@@ -262,15 +257,12 @@ respond stateVar =
                                     map patternErrorToRpcError patternErrors
                 -- term and predicate (pattern)
                 Right (TermAndPredicates pat substitution unsupported) -> do
-                    Log.logInfoNS "booster" "Simplifying a pattern"
                     unless (null unsupported) $ do
+                        withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do
+                            logMessage ("ignoring unsupported predicate parts" :: Text)
                         Log.logWarnNS
                             "booster"
-                            "Simplify: ignoring unsupported predicates in input"
-                        Log.logOtherNS
-                            "booster"
-                            (Log.LevelOther "ErrorDetails")
-                            (Text.unlines $ map prettyPattern unsupported)
+                            "Simplify: ignoring unsupported predicate parts"
                     -- apply the given substitution before doing anything else
                     let substPat =
                             Pattern
@@ -302,36 +294,35 @@ respond stateVar =
                     | otherwise -> do
                         Log.logInfoNS "booster" "Simplifying predicates"
                         unless (null ps.unsupported) $ do
-                            Log.logWarnNS
-                                "booster"
-                                "Simplify: ignoring unsupported predicates in input"
-                            Log.logOtherNS
-                                "booster"
-                                (Log.LevelOther "ErrorDetails")
-                                (Text.unlines $ map prettyPattern ps.unsupported)
-                        Log.logOtherNS "booster" (Log.LevelOther "Simplify") $ renderText (pretty ps)
+                            withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
+                                logMessage ("ignoring unsupported predicate parts" :: Text)
+                                Log.logWarnNS
+                                    "booster"
+                                    "Simplify: ignoring unsupported predicate parts"
+                        -- apply the given substitution before doing anything else
                         let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates
-                        ApplyEquations.simplifyConstraints
-                            doTracing
-                            def
-                            mLlvmLibrary
-                            solver
-                            mempty
-                            predicates
-                            >>= \case
-                                (Right newPreds, _) -> do
-                                    let predicateSort =
-                                            fromMaybe (error "not a predicate") $
-                                                sortOfJson req.state.term
-                                        result =
-                                            map (externalisePredicate predicateSort) newPreds
-                                                <> map (externaliseCeil predicateSort) (Set.toList ps.ceilPredicates)
-                                                <> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
-                                                <> ps.unsupported
+                        withContext "constraint" $
+                            ApplyEquations.simplifyConstraints
+                                doTracing
+                                def
+                                mLlvmLibrary
+                                solver
+                                mempty
+                                predicates
+                                >>= \case
+                                    (Right newPreds, _) -> do
+                                        let predicateSort =
+                                                fromMaybe (error "not a predicate") $
+                                                    sortOfJson req.state.term
+                                            result =
+                                                map (externalisePredicate predicateSort) newPreds
+                                                    <> map (externaliseCeil predicateSort) (Set.toList ps.ceilPredicates)
+                                                    <> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
+                                                    <> ps.unsupported
 
-                                    pure $ Right (addHeader $ Syntax.KJAnd predicateSort result, [])
-                                (Left something, _) ->
-                                    pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty something
+                                        pure $ Right (addHeader $ Syntax.KJAnd predicateSort result, [])
+                                    (Left something, _) ->
+                                        pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty something
             whenJust solver SMT.closeSolver
             stop <- liftIO $ getTime Monotonic
 
@@ -341,7 +332,7 @@ respond stateVar =
                     RpcTypes.Simplify
                         RpcTypes.SimplifyResult{state, logs = mkTraces duration traceData}
             pure $ second (uncurry mkSimplifyResponse) (fmap (second (map ApplyEquations.eraseStates)) result)
-        RpcTypes.GetModel req -> withContext req._module $ \case
+        RpcTypes.GetModel req -> withModule req._module $ \case
             (_, _, Nothing) -> do
                 Log.logErrorNS "booster" "get-model request, not supported without SMT solver"
                 pure $ Left RpcError.notImplemented
@@ -470,13 +461,13 @@ respond stateVar =
         -- using "Method does not exist" error code
         _ -> pure $ Left RpcError.notImplemented
   where
-    withContext ::
+    withModule ::
         Maybe Text ->
         ( (KoreDefinition, Maybe LLVM.API, Maybe SMT.SMTOptions) ->
           m (Either ErrorObj (RpcTypes.API 'RpcTypes.Res))
         ) ->
         m (Either ErrorObj (RpcTypes.API 'RpcTypes.Res))
-    withContext mbMainModule action = do
+    withModule mbMainModule action = do
         state <- liftIO $ readMVar stateVar
         let mainName = fromMaybe state.defaultMain mbMainModule
         case Map.lookup mainName state.definitions of