From fb59a84935266c0d899cf0b95c07f29290a9f319 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 20 Jun 2024 22:02:44 +1000 Subject: [PATCH] 3888 typed context and parser (#3950) * Introduces a JSON-enabled type for the log context * Uses the new type in all booster logging * Modifies `count-aborts` to parse the json data using the new type. Performance is on par after switching to TH-derived `FromJSON` instances. Conversion of `kore-rpc` logging is left for future work. Part of #3888 --------- Co-authored-by: github-actions --- booster/library/Booster/JsonRpc.hs | 44 ++--- booster/library/Booster/Log.hs | 180 +++++++++++------- .../library/Booster/Pattern/ApplyEquations.hs | 76 ++++---- booster/library/Booster/Pattern/Rewrite.hs | 46 ++--- booster/library/Booster/SMT/Interface.hs | 18 +- booster/tools/booster/Proxy.hs | 71 +++---- booster/tools/booster/Server.hs | 24 +-- dev-tools/booster-dev/Server.hs | 4 +- dev-tools/count-aborts/Main.hs | 37 +++- dev-tools/kore-rpc-dev/Server.hs | 8 +- dev-tools/package.yaml | 1 + kore-rpc-types/kore-rpc-types.cabal | 3 + .../src/Kore/JsonRpc/Types/ContextLog.hs | 178 +++++++++++++++++ 13 files changed, 469 insertions(+), 221 deletions(-) create mode 100644 kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index af5d228ecd..11ecf9fbdc 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -103,14 +103,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 -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "execute" $ do + RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxExecute $ 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 - void $ Booster.Log.withContext "internalise" $ logPatternError patternError + void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError pure $ Left $ RpcError.backendError $ @@ -152,7 +152,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'} -> Booster.Log.withContext "add-module" $ runExceptT $ do + RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do -- block other request executions while modifying the server state state <- liftIO $ takeMVar stateVar let nameAsId = fromMaybe False nameAsId' @@ -213,7 +213,7 @@ respond stateVar = Booster.Log.logMessage $ "Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions) pure $ RpcTypes.AddModule $ RpcTypes.AddModuleResult moduleHash - RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "simplify" $ do + RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxSimplify $ do start <- liftIO $ getTime Monotonic let internalised = runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term @@ -228,7 +228,7 @@ respond stateVar = result <- case internalised of Left patternErrors -> do forM_ patternErrors $ \patternError -> - void $ Booster.Log.withContext "internalise" $ logPatternError patternError + void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError pure $ Left $ RpcError.backendError $ @@ -273,7 +273,7 @@ respond stateVar = logMessage ("ignoring unsupported predicate parts" :: Text) -- apply the given substitution before doing anything else let predicates = map (substituteInPredicate ps.substitution) $ Set.toList ps.boolPredicates - withContext "constraint" $ + withContext CtxConstraint $ ApplyEquations.simplifyConstraints def mLlvmLibrary @@ -305,7 +305,7 @@ respond stateVar = pure $ second mkSimplifyResponse result RpcTypes.GetModel req -> withModule req._module $ \case (_, _, Nothing) -> do - withContext "get-model" $ + withContext CtxGetModel $ logMessage' ("get-model request, not supported without SMT solver" :: Text) pure $ Left RpcError.notImplemented (def, _, Just smtOptions) -> do @@ -315,7 +315,7 @@ respond stateVar = case internalised of Left patternErrors -> do forM_ patternErrors $ \patternError -> - void $ Booster.Log.withContext "internalise" $ logPatternError patternError + void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError pure $ Left $ RpcError.backendError $ @@ -327,20 +327,20 @@ respond stateVar = (boolPs, suppliedSubst) <- case things of TermAndPredicates pat substitution unsupported -> do - withContext "get-model" $ + withContext CtxGetModel $ logMessage' ("ignoring supplied terms and only checking predicates" :: Text) unless (null unsupported) $ do - withContext "get-model" $ do + withContext CtxGetModel $ do logMessage' ("ignoring unsupported predicates" :: Text) - withContext "detail" $ + withContext CtxDetail $ logMessage (Text.unwords $ map prettyPattern unsupported) pure (Set.toList pat.constraints, substitution) Predicates ps -> do unless (null ps.ceilPredicates && null ps.unsupported) $ do - withContext "get-model" $ do + withContext CtxGetModel $ do logMessage' ("ignoring supplied ceils and unsupported predicates" :: Text) - withContext "detail" $ + withContext CtxDetail $ logMessage ( Text.unlines $ map @@ -354,8 +354,8 @@ respond stateVar = if null boolPs && Map.null suppliedSubst then do -- as per spec, no predicate, no answer - withContext "get-model" $ - withContext "smt" $ + withContext CtxGetModel $ + withContext CtxSMT $ logMessage ("No predicates or substitutions given, returning Unknown" :: Text) pure $ Left SMT.Unknown else do @@ -365,8 +365,8 @@ respond stateVar = case result of Left err -> liftIO $ Exception.throw err -- fail hard on SMT errors Right response -> pure response - withContext "get-model" $ - withContext "smt" $ + withContext CtxGetModel $ + withContext CtxSMT $ logMessage $ "SMT result: " <> pack (either show (("Subst: " <>) . show . Map.size) smtResult) pure . Right . RpcTypes.GetModel $ case smtResult of @@ -413,14 +413,14 @@ respond stateVar = { satisfiable = RpcTypes.Sat , substitution } - RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "implies" $ do + RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxImplies $ do -- internalise given constrained term let internalised = runExcept . internalisePattern DisallowAlias CheckSubsorts Nothing def . fst . extractExistentials case (internalised req.antecedent.term, internalised req.consequent.term) of (Left patternError, _) -> do - void $ Booster.Log.withContext "internalise" $ logPatternError patternError + void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError pure $ Left $ RpcError.backendError $ @@ -428,7 +428,7 @@ respond stateVar = [ patternErrorToRpcError patternError ] (_, Left patternError) -> do - void $ Booster.Log.withContext "internalise" $ logPatternError patternError + void $ Booster.Log.withContext CtxInternalise $ logPatternError patternError pure $ Left $ RpcError.backendError $ @@ -440,11 +440,11 @@ respond stateVar = logMessage' ("aborting due to unsupported predicate parts" :: Text) unless (null unsupportedL) $ - withContext "detail" $ + withContext CtxDetail $ logMessage (Text.unwords $ map prettyPattern unsupportedL) unless (null unsupportedR) $ - withContext "detail" $ + withContext CtxDetail $ logMessage (Text.unwords $ map prettyPattern unsupportedR) let diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs index b6b96d6d02..82204a97e6 100644 --- a/booster/library/Booster/Log.hs +++ b/booster/library/Booster/Log.hs @@ -1,9 +1,31 @@ +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -module Booster.Log (module Booster.Log) where +module Booster.Log ( + ContextFor (..), + LogMessage (..), + Logger (..), + LoggerT (..), + LoggerMIO (..), + ToLogFormat (..), + WithJsonMessage (..), + logMessage, + logMessage', + logPretty, + filterLogger, + jsonLogger, + textLogger, + withContext, + withKorePatternContext, + withPatternContext, + withRuleContext, + withTermContext, + -- re-export SimpleContext for withContext + SimpleContext (..), +) where import Control.Monad (when) import Control.Monad.IO.Class @@ -16,26 +38,25 @@ import Control.Monad.Trans.State (StateT (..)) import Control.Monad.Trans.State.Strict qualified as Strict import Data.Aeson (ToJSON (..), Value (..), (.=)) import Data.Aeson.Encode.Pretty (Config (confIndent), Indent (Spaces), encodePretty') -import Data.Aeson.Key qualified as Key import Data.Aeson.Types (object) import Data.Coerce (coerce) -import Data.Data (Proxy (..)) import Data.Hashable qualified import Data.List (foldl', intercalate, intersperse) import Data.List.Extra (splitOn, takeEnd) +import Data.Maybe (fromMaybe) import Data.Set qualified as Set -import Data.String (IsString) import Data.Text (Text, pack) -import Data.Text.Lazy qualified as LazyText -import GHC.Exts (IsString (..)) -import GHC.TypeLits (KnownSymbol, symbolVal) +import Data.Text.Encoding (decodeUtf8) import Prettyprinter (Pretty, pretty) +import System.Log.FastLogger (FormattedTime) +import UnliftIO (MonadUnliftIO) import Booster.Definition.Attributes.Base import Booster.Definition.Base (RewriteRule (..), SourceRef (..), sourceRef) import Booster.Pattern.Base ( Pattern (..), Predicate (..), + Symbol (..), Term (..), TermAttributes (hash), pattern AndTerm, @@ -44,11 +65,9 @@ import Booster.Prettyprinter (renderOneLineText) import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern) import Booster.Syntax.Json.Externalise (externaliseTerm) import Booster.Util (Flag (..)) -import Data.Text.Encoding (decodeUtf8) import Kore.JsonRpc.Types (rpcJsonConfig) -import Kore.Util (showHashHex) -import System.Log.FastLogger (FormattedTime) -import UnliftIO (MonadUnliftIO) +import Kore.JsonRpc.Types.ContextLog as CL +import Kore.Util newtype Logger a = Logger (a -> IO ()) @@ -56,13 +75,32 @@ class ToLogFormat a where toTextualLog :: a -> Text toJSONLog :: a -> Value -data LogContext = forall a. ToLogFormat a => LogContext a +instance ToLogFormat CLContext where + toTextualLog = pack . show + toJSONLog = toJSON + +instance ToLogFormat Text where + toTextualLog t = t + toJSONLog t = String t + +instance ToLogFormat Term where + toTextualLog t = renderOneLineText $ pretty t + toJSONLog t = toJSON $ addHeader $ externaliseTerm t -instance IsString LogContext where - fromString = LogContext . pack +instance ToLogFormat (RewriteRule tag) where + toTextualLog = shortRuleLocation + toJSONLog = String . shortRuleLocation + +shortRuleLocation :: RewriteRule tag -> Text +shortRuleLocation rule = renderOneLineText $ + pretty $ + case sourceRef rule of + Located l@Location{file = FileSource f} -> + Located l{file = FileSource $ "..." <> (intercalate "/" $ takeEnd 3 $ splitOn "/" f)} + loc -> loc data LogMessage where - LogMessage :: ToLogFormat a => Flag "alwaysShown" -> [LogContext] -> a -> LogMessage + LogMessage :: ToLogFormat a => Flag "alwaysShown" -> [CLContext] -> a -> LogMessage class MonadIO m => LoggerMIO m where getLogger :: m (Logger LogMessage) @@ -100,78 +138,84 @@ logMessage' a = logPretty :: (LoggerMIO m, Pretty a) => a -> m () logPretty = logMessage . renderOneLineText . pretty -withContext :: LoggerMIO m => LogContext -> m a -> m a -withContext c = +withContext :: LoggerMIO m => SimpleContext -> m a -> m a +withContext c = withContext_ (CLNullary c) + +withContext_ :: LoggerMIO m => CLContext -> m a -> m a +withContext_ c = withLogger ( \(Logger l) -> Logger $ l . (\(LogMessage alwaysShown ctxt m) -> LogMessage alwaysShown (c : ctxt) m) ) -newtype TermCtxt = TermCtxt Int - -instance ToLogFormat TermCtxt where - toTextualLog (TermCtxt hsh) = "term " <> (showHashHex hsh) - toJSONLog (TermCtxt hsh) = object ["term" .= showHashHex hsh] - -newtype HookCtxt = HookCtxt Text - -instance ToLogFormat HookCtxt where - toTextualLog (HookCtxt h) = "hook " <> h - toJSONLog (HookCtxt h) = object ["hook" .= h] - -instance ToLogFormat Term where - toTextualLog t = renderOneLineText $ pretty t - toJSONLog t = toJSON $ addHeader $ externaliseTerm t - -instance ToLogFormat Text where - toTextualLog t = t - toJSONLog t = String t - withTermContext :: LoggerMIO m => Term -> m a -> m a -withTermContext t@(Term attrs _) m = withContext (LogContext $ TermCtxt attrs.hash) $ do - withContext "kore-term" $ logMessage t - m +withTermContext t@(Term attrs _) m = + withContext_ (CLWithId . CtxTerm . ShortId $ showHashHex attrs.hash) $ do + withContext CtxKoreTerm $ logMessage t + m withPatternContext :: LoggerMIO m => Pattern -> m a -> m a withPatternContext Pattern{term, constraints} m = - let t' = foldl' AndTerm term $ Set.toList $ Set.map coerce constraints + let t' = foldl' AndTerm term $ Set.toList $ Set.map coerce constraints -- FIXME in withTermContext t' m instance ToLogFormat KorePattern where toTextualLog = prettyPattern toJSONLog p = toJSON p -newtype KorePatternCtxt = KorePatternCtxt KorePattern - -instance ToLogFormat KorePatternCtxt where - toTextualLog (KorePatternCtxt t) = "term " <> (showHashHex $ Data.Hashable.hash $ prettyPattern t) - toJSONLog (KorePatternCtxt t) = object ["term" .= (showHashHex $ Data.Hashable.hash $ prettyPattern t)] - -instance KnownSymbol k => ToLogFormat (RewriteRule k) where - toTextualLog RewriteRule{attributes} = - LazyText.toStrict $ - (LazyText.toLower $ LazyText.pack $ symbolVal (Proxy :: Proxy k)) - <> " " - <> (LazyText.take 7 . LazyText.fromStrict . coerce $ attributes.uniqueId) - toJSONLog RewriteRule{attributes} = - object - [ (Key.fromText $ LazyText.toStrict $ LazyText.toLower $ LazyText.pack $ symbolVal (Proxy :: Proxy k)) - .= (coerce attributes.uniqueId :: Text) - ] - withKorePatternContext :: LoggerMIO m => KorePattern -> m a -> m a -withKorePatternContext t m = withContext (LogContext $ KorePatternCtxt t) $ do - withContext "kore-term" $ logMessage t - m - -withRuleContext :: KnownSymbol tag => LoggerMIO m => RewriteRule tag -> m a -> m a -withRuleContext rule m = withContext (LogContext rule) $ do - withContext "detail" $ logPretty $ case sourceRef rule of +withKorePatternContext p m = + withContextFor p $ do + withContext CtxKoreTerm $ logMessage p + m + +withRuleContext :: + ContextFor (RewriteRule tag) => + LoggerMIO m => + RewriteRule tag -> + m a -> + m a +withRuleContext rule m = withContextFor rule $ do + withContext CtxDetail $ logPretty $ case sourceRef rule of Located Location{file = FileSource f, position} -> Located Location{file = FileSource $ "..." <> (intercalate "/" $ takeEnd 3 $ splitOn "/" f), position} loc -> loc m +class ContextFor a where + withContextFor :: LoggerMIO m => a -> m b -> m b + +instance ContextFor Term where + withContextFor (Term attrs _) = + withContext_ (CLWithId . CtxTerm . ShortId $ showHashHex attrs.hash) + +instance ContextFor KorePattern where + withContextFor p = + withContext_ (CLWithId . CtxTerm . ShortId . showHashHex . Data.Hashable.hash $ show p) -- FIXME + +instance ContextFor (RewriteRule "Rewrite") where + withContextFor r = + withContext_ (CLWithId . CtxRewrite $ parseRuleId r) + +instance ContextFor (RewriteRule "Function") where + withContextFor r = + withContext_ (CLWithId . CtxFunction $ parseRuleId r) + +instance ContextFor (RewriteRule "Simplification") where + withContextFor r = + withContext_ (CLWithId . CtxSimplification $ parseRuleId r) + +instance ContextFor (RewriteRule "Ceil") where + withContextFor r = + withContext_ (CLWithId . CtxCeil $ parseRuleId r) + +instance ContextFor Symbol where + withContextFor s = + withContext_ (CLWithId . CtxHook $ maybe "not-hooked" decodeUtf8 s.attributes.hook) + +parseRuleId :: RewriteRule tag -> CL.UniqueId +parseRuleId = fromMaybe CL.UNKNOWN . CL.parseUId . coerce . (.attributes.uniqueId) + data WithJsonMessage where WithJsonMessage :: ToLogFormat a => Value -> a -> WithJsonMessage @@ -196,7 +240,7 @@ instance MonadIO m => LoggerMIO (LoggerT m) where textLogger :: ((Maybe FormattedTime -> Control.Monad.Logger.LogStr) -> IO ()) -> Logger LogMessage textLogger l = Logger $ \(LogMessage _ ctxts msg) -> - let logLevel = mconcat $ intersperse "][" $ map (\(LogContext lc) -> toTextualLog lc) ctxts + let logLevel = mconcat $ intersperse "][" $ map toTextualLog ctxts in l $ \mTime -> ( case mTime of Nothing -> mempty @@ -210,7 +254,7 @@ textLogger l = Logger $ \(LogMessage _ ctxts msg) -> jsonLogger :: ((Maybe FormattedTime -> Control.Monad.Logger.LogStr) -> IO ()) -> Logger LogMessage jsonLogger l = Logger $ \(LogMessage _ ctxts msg) -> - let ctxt = toJSON $ map (\(LogContext lc) -> toJSONLog lc) ctxts + let ctxt = toJSON $ map toJSONLog ctxts in liftIO $ l $ \mTime -> ( Control.Monad.Logger.toLogStr $ diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 8c110f003b..367bf8e26f 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE PatternSynonyms #-} {- | @@ -48,7 +49,6 @@ import Data.Set qualified as Set import Data.Text (Text) import Data.Text qualified as Text import Data.Text.Encoding qualified as Text -import GHC.TypeLits (KnownSymbol) import Prettyprinter import Booster.Builtin as Builtin @@ -218,7 +218,7 @@ popRecursion = do s <- getState if null s.recursionStack then do - withContext "abort" $ + withContext CtxAbort $ logMessage ("Trying to pop an empty recursion stack" :: Text) throw $ InternalError "Trying to pop an empty recursion stack" else eqState $ put s{recursionStack = tail s.recursionStack} @@ -239,16 +239,16 @@ fromCache tag t = eqState $ Map.lookup t <$> gets (select tag . (.cache)) logWarn :: LoggerMIO m => Text -> m () logWarn msg = - withContext "warning" $ + withContext CtxWarn $ logMessage msg checkForLoop :: LoggerMIO io => Term -> EquationT io () checkForLoop t = do EquationState{termStack} <- getState whenJust (Seq.elemIndexL t termStack) $ \i -> do - withContext "abort" $ do + withContext CtxAbort $ do logWarn "Equation loop detected." - withContext "detail" $ + withContext CtxDetail $ logMessage $ renderOneLineText $ hsep @@ -304,7 +304,7 @@ iterateEquations direction preference startTerm = do checkCounter counter = do config <- getConfig when (counter > config.maxRecursion) $ do - withContext "abort" $ do + withContext CtxAbort $ do logWarn "Recursion limit exceeded. The limit can be increased by \ \ restarting the server with '--equation-max-recursion N'." @@ -317,11 +317,11 @@ iterateEquations direction preference startTerm = do config <- getConfig currentCount <- countSteps when (coerce currentCount > config.maxIterations) $ do - withContext "abort" $ do + withContext CtxAbort $ do logWarn $ renderOneLineText $ "Unable to finish evaluation in" <+> pretty currentCount <+> "iterations." - withContext "detail" . logMessage . renderOneLineText $ + withContext CtxDetail . logMessage . renderOneLineText $ "Final term:" <+> pretty currentTerm throw $ TooManyIterations currentCount startTerm currentTerm @@ -351,18 +351,18 @@ llvmSimplify term = do where evalLlvm definition api cb t@(Term attributes _) | attributes.isEvaluated = pure t - | isConcrete t && attributes.canBeEvaluated = withContext "llvm" $ do + | isConcrete t && attributes.canBeEvaluated = withContext CtxLlvm $ do LLVM.simplifyTerm api definition t (sortOfTerm t) >>= \case Left (LlvmError e) -> do - withContext "abort" $ + withContext CtxAbort $ logWarn $ "LLVM backend error detected: " <> Text.decodeUtf8 e throw $ UndefinedTerm t $ LlvmError e Right result -> do when (result /= t) $ do setChanged - withContext "success" $ + withContext CtxSuccess $ withTermContext result $ pure () pure result @@ -531,8 +531,8 @@ cached cacheTag cb t@(Term attributes _) Just cachedTerm -> do when (t /= cachedTerm) $ do setChanged - withContext "success" $ - withContext "cached" $ + withContext CtxSuccess $ + withContext CtxCached $ withTermContext cachedTerm $ pure () pure cachedTerm @@ -563,12 +563,11 @@ applyHooksAndEquations pref term = do case term of SymbolApplication sym _sorts args | Just hook <- flip Map.lookup Builtin.hooks =<< sym.attributes.hook -> do - let hookName = maybe "UNKNOWN" Text.decodeUtf8 sym.attributes.hook - onError e = do - withContext "abort" $ + let onError e = do + withContext CtxAbort $ logWarn e throw (InternalError e) - withContext (LogContext $ HookCtxt hookName) $ + withContextFor sym $ either onError checkChanged $ runExcept (hook args) _other -> pure Nothing @@ -577,9 +576,9 @@ applyHooksAndEquations pref term = do -- cannot blindly set the changed flag when we have applied a hook checkChanged :: Maybe Term -> EquationT io (Maybe Term) checkChanged Nothing = - withContext "failure" (logMessage ("Hook returned no result" :: Text)) >> pure Nothing + withContext CtxFailure (logMessage ("Hook returned no result" :: Text)) >> pure Nothing checkChanged (Just t) = - withContext "success" $ withTermContext t $ do + withContext CtxSuccess $ withTermContext t $ do unless (t == term) setChanged pure (Just t) @@ -621,7 +620,7 @@ handleFunctionEquation continue abort = \case IndeterminateCondition{} -> abort ConditionFalse _ -> continue EnsuresFalse p -> do - withContext "abort" $ + withContext CtxAbort $ logMessage ("A side condition was found to be false during evaluation (pruning)" :: Text) throw $ SideConditionFalse p RuleNotPreservingDefinedness -> abort @@ -634,7 +633,7 @@ handleSimplificationEquation continue _abort = \case IndeterminateCondition{} -> continue ConditionFalse _ -> continue EnsuresFalse p -> do - withContext "abort" $ + withContext CtxAbort $ logMessage ("A side condition was found to be false during evaluation (pruning)" :: Text) throw $ SideConditionFalse p RuleNotPreservingDefinedness -> continue @@ -642,7 +641,7 @@ handleSimplificationEquation continue _abort = \case applyEquations :: forall io tag. - KnownSymbol tag => + ContextFor (RewriteRule tag) => LoggerMIO io => Theory (RewriteRule tag) -> ResultHandler io -> @@ -651,7 +650,7 @@ applyEquations :: applyEquations theory handler term = do let index = Idx.termTopIndex term when (Idx.hasNone index) $ do - withContext "abort" $ logMessage ("Index 'None'" :: Text) + withContext CtxAbort $ logMessage ("Index 'None'" :: Text) throw (IndexIsNone term) let indexes = Set.toList $ Idx.coveringIndexes index @@ -679,18 +678,18 @@ applyEquations theory handler term = do pure term -- nothing to do, term stays the same processEquations (eq : rest) = do withRuleContext eq (applyEquation term eq) >>= \case - Right t -> setChanged >> (withContext (LogContext eq) $ withContext "success" $ withTermContext t $ pure t) + Right t -> setChanged >> (withContextFor eq $ withContext CtxSuccess $ withTermContext t $ pure t) Left (m, err) -> handler - ( ( withContext (LogContext eq) $ + ( ( withContextFor eq $ m $ - withContext "failure" . withContext "continue" + withContext CtxFailure . withContext CtxContinue ) >> processEquations rest ) - ( ( withContext (LogContext eq) $ + ( ( withContextFor eq $ m $ - withContext "failure" . withContext "break" + withContext CtxFailure . withContext CtxBreak ) >> pure term ) @@ -698,7 +697,6 @@ applyEquations theory handler term = do applyEquation :: forall io tag. - KnownSymbol tag => LoggerMIO io => Term -> RewriteRule tag -> @@ -708,7 +706,7 @@ applyEquation :: applyEquation term rule = runExceptT $ do -- ensured by internalisation: no existentials in equations unless (null rule.existentials) $ do - withContext "abort" $ + withContext CtxAbort $ logMessage ("Equation with existentials" :: Text) lift . throw . InternalError $ "Equation with existentials: " <> Text.pack (show rule) @@ -735,7 +733,7 @@ applyEquation term rule = runExceptT $ do MatchFailed failReason -> throwE ( \ctxt -> - withContext "match" $ + withContext CtxMatch $ ctxt $ logPretty failReason , FailedMatch failReason @@ -743,7 +741,7 @@ applyEquation term rule = runExceptT $ do MatchIndeterminate remainder -> throwE ( \ctxt -> - withContext "match" $ + withContext CtxMatch $ ctxt $ logMessage $ WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $ @@ -756,11 +754,11 @@ applyEquation term rule = runExceptT $ do -- forall (v, t) : subst. concrete(v) -> isConstructorLike(t) /\ -- symbolic(v) -> not $ t isConstructorLike(t) -- is violated - withContext "match" $ checkConcreteness rule.attributes.concreteness subst + withContext CtxMatch $ checkConcreteness rule.attributes.concreteness subst - withContext "match" $ withContext "success" $ do + withContext CtxMatch $ withContext CtxSuccess $ do logMessage rule - withContext "substitution" + withContext CtxSubstitution $ logMessage $ WithJsonMessage (object ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList subst)]) @@ -829,7 +827,7 @@ applyEquation term rule = runExceptT $ do -- Simplify given predicate in a nested EquationT execution. -- Call 'whenBottom' if it is Bottom, return Nothing if it is Top, -- otherwise return the simplified remaining predicate. - checkConstraint whenBottom (Predicate p) = withContext "constraint" $ do + checkConstraint whenBottom (Predicate p) = withContext CtxConstraint $ do let fallBackToUnsimplifiedOrBottom :: EquationFailure -> EquationT io Term fallBackToUnsimplifiedOrBottom = \case UndefinedTerm{} -> pure FalseBool @@ -947,10 +945,10 @@ simplifyConstraint' recurseIntoEvalBool = \case mbApi <- (.llvmApi) <$> getConfig case mbApi of Just api -> - withContext "llvm" $ + withContext CtxLlvm $ LLVM.simplifyBool api t >>= \case Left (LlvmError e) -> do - withContext "abort" $ + withContext CtxAbort $ logWarn $ "LLVM backend error detected: " <> Text.decodeUtf8 e throw $ UndefinedTerm t $ LlvmError e @@ -959,7 +957,7 @@ simplifyConstraint' recurseIntoEvalBool = \case if res then TrueBool else FalseBool - withContext "success" $ + withContext CtxSuccess $ withTermContext result $ pure result Nothing -> if recurseIntoEvalBool then evalBool t else pure t diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 7b2349849b..ba37452c53 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -44,17 +44,7 @@ import Prettyprinter import Booster.Definition.Attributes.Base import Booster.Definition.Base import Booster.LLVM as LLVM (API) -import Booster.Log ( - LogMessage, - Logger, - LoggerMIO (..), - WithJsonMessage (..), - logMessage, - logPretty, - withContext, - withPatternContext, - withRuleContext, - ) +import Booster.Log import Booster.Pattern.ApplyEquations ( EquationFailure (..), SimplifierCache, @@ -282,27 +272,27 @@ applyRule :: applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRuleAppT $ do def <- lift getDefinition -- unify terms - subst <- withContext "match" $ case matchTerms Rewrite def rule.lhs pat.term of + subst <- withContext CtxMatch $ case matchTerms Rewrite def rule.lhs pat.term of MatchFailed (SubsortingError sortError) -> do - withContext "error" $ logPretty sortError + withContext CtxError $ logPretty sortError failRewrite $ RewriteSortError rule pat.term sortError MatchFailed err@ArgLengthsDiffer{} -> do - withContext "error" $ logPretty err + withContext CtxError $ logPretty err failRewrite $ InternalMatchError $ renderText $ pretty err MatchFailed reason -> do - withContext "failure" $ logPretty reason + withContext CtxFailure $ logPretty reason fail "Rule matching failed" MatchIndeterminate remainder -> do - withContext "indeterminate" $ + withContext CtxIndeterminate $ logMessage $ WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $ renderOneLineText $ "Uncertain about match with rule. Remainder:" <+> pretty remainder failRewrite $ RuleApplicationUnclear rule pat.term remainder MatchSuccess substitution -> do - withContext "success" $ do + withContext CtxSuccess $ do logMessage rule - withContext "substitution" + withContext CtxSubstitution $ logMessage $ WithJsonMessage ( object @@ -316,7 +306,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu -- Also fail the whole rewrite if a rule applies but may introduce -- an undefined term. unless (null rule.computedAttributes.notPreservesDefinednessReasons) $ do - withContext "definedness" . withContext "abort" $ + withContext CtxDefinedness . withContext CtxAbort $ logMessage $ renderOneLineText $ "Uncertain about definedness of rule due to:" @@ -347,7 +337,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu mbSolver <- lift $ RewriteT $ (.smtSolver) <$> ask let smtUnclear = do - withContext "constraint" . withContext "abort" . logMessage . renderOneLineText $ + withContext CtxConstraint . withContext CtxAbort . logMessage . renderOneLineText $ "Uncertain about condition(s) in a rule:" <+> pretty unclearRequires failRewrite $ RuleConditionUnclear rule . coerce . foldl1 AndTerm $ @@ -364,7 +354,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu liftIO $ Exception.throw other -- fail hard on other SMT errors Right (Just False) -> do -- requires is actually false given the prior - withContext "failure" $ logMessage ("Required clauses evaluated to #Bottom." :: Text) + withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text) RewriteRuleAppT $ pure NotApplied Right (Just True) -> pure () -- can proceed @@ -372,7 +362,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu smtUnclear -- no implication could be determined Nothing -> unless (null unclearRequires) $ do - withContext "constraint" . withContext "abort" $ + withContext CtxConstraint . withContext CtxAbort $ logMessage $ renderOneLineText $ "Uncertain about a condition(s) in rule, no SMT solver:" <+> pretty unclearRequires @@ -392,7 +382,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu whenJust mbSolver $ \solver -> (lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case Right (Just False) -> do - withContext "success" $ logMessage ("New constraints evaluated to #Bottom." :: Text) + withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) RewriteRuleAppT $ pure Trivial Right _other -> pure () @@ -423,7 +413,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu <> (Set.fromList $ map (coerce . substituteInTerm existentialSubst . coerce) newConstraints) ) ceilConditions - withContext "success" $ + withContext CtxSuccess $ withPatternContext rewritten $ return (rule, rewritten) where @@ -438,7 +428,7 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu RewriteConfig{definition, llvmApi, smtSolver} <- lift $ RewriteT ask oldCache <- lift . RewriteT . lift $ get (simplified, cache) <- - withContext "constraint" $ + withContext CtxConstraint $ simplifyConstraint definition llvmApi smtSolver oldCache p -- update cache lift . RewriteT . lift . modify $ const cache @@ -694,7 +684,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL flip runStateT rewriteStart $ doSteps False pat pure (counter, traces, rr) where - logDepth = withContext "depth" . logMessage + logDepth = withContext CtxDepth . logMessage depthReached n = maybe False (n >=) mbMaxDepth @@ -711,7 +701,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL updateCache simplifierCache = modify $ \rss -> rss{simplifierCache} simplifyP :: Pattern -> StateT RewriteStepsState io (Maybe Pattern) - simplifyP p = withContext "simplify" $ do + simplifyP p = withContext CtxSimplify $ do st <- get let cache = st.simplifierCache smt = st.smtSolver @@ -853,7 +843,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL withSimplified pat' "Retrying with simplified pattern" (doSteps True) | otherwise -> do -- was already simplified, emit an abort log entry - withRuleContext rule . withContext "match" . withContext "abort" . logMessage $ + withRuleContext rule . withContext CtxMatch . withContext CtxAbort . logMessage $ WithJsonMessage (object ["remainder" .= (bimap externaliseTerm externaliseTerm <$> remainder)]) $ renderOneLineText $ "Uncertain about match with rule. Remainder:" <+> pretty remainder diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index b9b9b61140..5d0fd5b0c1 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -82,7 +82,7 @@ declareVariables transState = do - set user-specified timeout for queries -} initSolver :: Log.LoggerMIO io => KoreDefinition -> SMTOptions -> io SMT.SMTContext -initSolver def smtOptions = Log.withContext "smt" $ do +initSolver def smtOptions = Log.withContext Log.CtxSMT $ do prelude <- translatePrelude def Log.logMessage ("Starting new SMT solver" :: Text) @@ -168,13 +168,13 @@ getModelFor :: Map Variable Term -> -- supplied substitution io (Either SMTError (Either SMT.Response (Map Variable Term))) getModelFor ctxt ps subst - | null ps && Map.null subst = Log.withContext "smt" $ do + | null ps && Map.null subst = Log.withContext Log.CtxSMT $ do Log.logMessage ("No constraints or substitutions to check, returning Sat" :: Text) pure . Right . Right $ Map.empty - | Left errMsg <- translated = Log.withContext "smt" $ do + | Left errMsg <- translated = Log.withContext Log.CtxSMT $ do Log.logMessage $ "SMT translation error: " <> errMsg smtTranslateError errMsg - | Right (smtAsserts, transState) <- translated = Log.withContext "smt" $ do + | Right (smtAsserts, transState) <- translated = Log.withContext Log.CtxSMT $ do evalSMT ctxt . runExceptT $ do lift $ hardResetSolver ctxt.options solve smtAsserts transState @@ -330,10 +330,10 @@ checkPredicates :: io (Either SMTError (Maybe Bool)) checkPredicates ctxt givenPs givenSubst psToCheck | null psToCheck = pure . Right $ Just True - | Left errMsg <- translated = Log.withContext "smt" $ do - Log.withContext "abort" $ Log.logMessage $ "SMT translation error: " <> errMsg + | Left errMsg <- translated = Log.withContext Log.CtxSMT $ do + Log.withContext Log.CtxAbort $ Log.logMessage $ "SMT translation error: " <> errMsg pure . Left . SMTTranslationError $ errMsg - | Right ((smtGiven, sexprsToCheck), transState) <- translated = Log.withContext "smt" $ do + | Right ((smtGiven, sexprsToCheck), transState) <- translated = Log.withContext Log.CtxSMT $ do evalSMT ctxt . runExceptT $ do lift $ hardResetSolver ctxt.options solve smtGiven sexprsToCheck transState @@ -400,13 +400,13 @@ checkPredicates ctxt givenPs givenSubst psToCheck failBecauseUnknown = smtRun GetReasonUnknown >>= \case ReasonUnknown reason -> do - Log.withContext "abort" $ + Log.withContext Log.CtxAbort $ Log.logMessage $ "Returned Unknown. Reason: " <> reason throwE $ SMTSolverUnknown reason givenPs psToCheck other -> do let msg = "Unexpected result while calling ':reason-unknown': " <> show other - Log.withContext "abort" $ Log.logMessage $ Text.pack msg + Log.withContext Log.CtxAbort $ Log.logMessage $ Text.pack msg throwSMT' msg -- Given the known truth and the expressions to check, diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs index c64cce9969..b490df12d2 100644 --- a/booster/tools/booster/Proxy.hs +++ b/booster/tools/booster/Proxy.hs @@ -35,7 +35,7 @@ import System.Clock (Clock (Monotonic), TimeSpec, diffTimeSpec, getTime, toNanoS import Booster.Definition.Base (KoreDefinition) import Booster.JsonRpc as Booster (ServerState (..), execStateToKoreJson, toExecState) import Booster.JsonRpc.Utils -import Booster.Log qualified +import Booster.Log import Booster.Syntax.Json.Internalise import Kore.Attribute.Symbol (StepperAttributes) import Kore.IndexedModule.MetadataTools (SmtMetadataTools) @@ -111,7 +111,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re logStats ImpliesM (boosterTime, 0) pure res Left err -> do - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage' $ Text.pack $ "implies error in booster: " <> fromError err @@ -140,7 +140,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re (result, kTime) <- case bResult of Left err -> do - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage' $ Text.pack $ "get-model error in booster: " <> fromError err @@ -148,13 +148,13 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re Right (GetModel res@GetModelResult{}) -- re-check with legacy-kore if result is unknown | Unknown <- res.satisfiable -> do - Booster.Log.withContext "proxy" $ - Booster.Log.withContext "abort" $ + Booster.Log.withContext CtxProxy $ + Booster.Log.withContext CtxAbort $ Booster.Log.logMessage $ Text.pack "Re-checking a get-model result Unknown" r@(kResult, _) <- Stats.timed $ kore req - Booster.Log.withContext "proxy" $ - Booster.Log.withContext "abort" $ + Booster.Log.withContext CtxProxy $ + Booster.Log.withContext CtxAbort $ Booster.Log.logMessage $ "Double-check returned " <> toStrict (encodeToLazyText kResult) pure r @@ -187,9 +187,9 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re when (koreRes.state /= boosterRes.state) $ do bState <- liftIO (MVar.readMVar boosterState) - Booster.Log.withContext "proxy" $ - Booster.Log.withContext "abort" $ - Booster.Log.withContext "detail" $ + Booster.Log.withContext CtxProxy $ + Booster.Log.withContext CtxAbort $ + Booster.Log.withContext CtxDetail $ Booster.Log.logMessage $ let m = fromMaybe bState.defaultMain simplifyReq._module def = @@ -234,7 +234,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re fromString (String s) = s fromString other = Text.pack (show other) - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage' $ Text.unwords ["Problem with simplify request: ", Text.pack getErrMsg, "-", boosterError] @@ -244,7 +244,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re pure . Left $ ErrorObj "Wrong result type" (-32002) $ toJSON _wrong loggedKore method r = do - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage' $ Text.pack $ show method <> " (using kore)" @@ -255,7 +255,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re logStats method (time, koreTime) | Just v <- statsVar = do addStats v method time koreTime - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage' $ Text.pack $ unwords @@ -305,7 +305,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re ExecuteRequest -> m (Either ErrorObj (API 'Res)) executionLoop logSettings def (currentDepth@(Depth cDepth), !time, !koreTime, !rpcLogs) r = do - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage $ Text.pack $ if currentDepth == 0 @@ -328,7 +328,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re | DepthBound <- boosterResult.reason , Just forceDepth <- cfg.forceFallback , forceDepth == boosterResult.depth -> do - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage $ Text.pack $ "Forced simplification at " <> show (currentDepth + boosterResult.depth) @@ -336,7 +336,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re case simplifyResult of Left logsOnly -> do -- state was simplified to \bottom, return vacuous - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage $ Text.pack "Vacuous state after simplification" pure . Right . Execute $ @@ -365,12 +365,12 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re -- if we stop for a reason in fallbackReasons (default [Aborted, Stuck, Branching], -- revert to the old backend to re-confirm and possibly proceed | boosterResult.reason `elem` cfg.fallbackReasons -> do - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage $ Text.pack $ "Booster " <> show boosterResult.reason <> " at " <> show boosterResult.depth -- simplify Booster's state with Kore's simplifier - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage ("Simplifying booster state and falling back to Kore" :: Text) simplifyResult <- if cfg.simplifyBeforeFallback @@ -379,13 +379,13 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re case simplifyResult of Left logsOnly -> do -- state was simplified to \bottom, return vacuous - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage $ Text.pack "Vacuous state after simplification" pure . Right . Execute $ makeVacuous (postProcessLogs <$> logsOnly) boosterResult Right (simplifiedBoosterState, boosterStateSimplificationLogs) -> do -- attempt to do one step in the old backend - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage ("Executing fall-back request" :: Text) (kResult, kTime) <- Stats.timed $ @@ -398,7 +398,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re } ) when (isJust statsVar) $ do - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage $ Text.pack $ "Kore fall-back in " <> microsWithUnit kTime @@ -432,19 +432,19 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re r{ExecuteRequest.state = nextState} case (boosterResult.reason, koreResult.reason) of (Aborted, res) -> - Booster.Log.withContext "proxy" $ - Booster.Log.withContext "abort" $ + Booster.Log.withContext CtxProxy $ + Booster.Log.withContext CtxAbort $ Booster.Log.logMessage $ "Booster aborted, kore yields " <> Text.pack (show res) (bRes, kRes) | bRes /= kRes -> - Booster.Log.withContext "proxy" $ - Booster.Log.withContext "abort" $ + Booster.Log.withContext CtxProxy $ + Booster.Log.withContext CtxAbort $ Booster.Log.logMessage $ "Booster and kore disagree: " <> Text.pack (show (bRes, kRes)) | otherwise -> - Booster.Log.withContext "proxy" $ - Booster.Log.withContext "abort" $ + Booster.Log.withContext CtxProxy $ + Booster.Log.withContext CtxAbort $ Booster.Log.logMessage $ "kore confirms result " <> Text.pack (show bRes) @@ -454,7 +454,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re -- steps we have taken to the counter and -- attempt with booster again when (koreResult.depth == 0) $ error "Expected kore-rpc to take at least one step" - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage $ Text.pack $ "kore depth-bound, continuing... (currently at " @@ -465,7 +465,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re -- otherwise we have hit a different -- HaltReason, at which point we should -- return, setting the correct depth - Booster.Log.withContext "proxy" . Booster.Log.logMessage . Text.pack $ + Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $ "Kore " <> show koreResult.reason <> " at " <> show koreResult.depth -- perform post-exec simplification. -- NB This has been found to make a difference, @@ -499,7 +499,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re -- we were successful with the booster, thus we -- return the booster result with the updated -- depth, in case we previously looped - Booster.Log.withContext "proxy" . Booster.Log.logMessage . Text.pack $ + Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $ "Booster " <> show boosterResult.reason <> " at " <> show boosterResult.depth -- perform post-exec simplification postExecResult <- @@ -543,7 +543,8 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re mbModule def s = do - Booster.Log.withContext "proxy" . Booster.Log.logMessage . Text.pack $ "Simplifying execution state" + Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $ + "Simplifying execution state" simplResult <- handleSimplify (toSimplifyRequest s) Nothing case simplResult of @@ -576,13 +577,13 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re , simplified.logs ) Left err -> do - Booster.Log.withContext "proxy" . Booster.Log.logMessage $ + Booster.Log.withContext CtxProxy . Booster.Log.logMessage $ "Error processing execute state simplification result: " <> Text.pack (show err) pure $ Right (s, Nothing) _other -> do -- if we hit an error here, return the original - Booster.Log.withContext "proxy" . Booster.Log.logMessage . Text.pack $ + Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $ "Unexpected failure when calling Kore simplifier, returning original term" pure $ Right (s, Nothing) where @@ -606,13 +607,13 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re simplifyExecResult logSettings mbModule def res@ExecuteResult{reason, state, nextStates} | not cfg.simplifyAtEnd = pure $ Right res | otherwise = do - Booster.Log.withContext "proxy" . Booster.Log.logMessage . Text.pack $ + Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $ "Simplifying state in " <> show reason <> " result" simplified <- simplifyExecuteState logSettings mbModule def state case simplified of Left logsOnly -> do -- state simplified to \bottom, return vacuous - Booster.Log.withContext "proxy" . Booster.Log.logMessage . Text.pack $ + Booster.Log.withContext CtxProxy . Booster.Log.logMessage . Text.pack $ "Vacuous after simplifying result state" pure . Right $ makeVacuous logsOnly res Right (simplifiedState, simplifiedStateLogs) -> do diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs index f61487cf4d..a25e690179 100644 --- a/booster/tools/booster/Server.hs +++ b/booster/tools/booster/Server.hs @@ -57,7 +57,7 @@ import Booster.Definition.Ceil (ComputeCeilSummary (..), computeCeilsDefinition) import Booster.GlobalState import Booster.JsonRpc qualified as Booster import Booster.LLVM.Internal (mkAPI, withDLib) -import Booster.Log qualified +import Booster.Log hiding (withLogger) import Booster.Log.Context qualified import Booster.Pattern.Base (Predicate (..)) import Booster.Prettyprinter (renderOneLineText) @@ -193,7 +193,7 @@ main = do filteredBoosterContextLogger = flip Booster.Log.filterLogger boosterContextLogger $ \(Booster.Log.LogMessage (Booster.Flag alwaysDisplay) ctxts _) -> alwaysDisplay - || let ctxt = map (\(Booster.Log.LogContext lc) -> Text.encodeUtf8 $ Booster.Log.toTextualLog lc) ctxts + || let ctxt = map (Text.encodeUtf8 . Booster.Log.toTextualLog) ctxts in any (flip Booster.Log.Context.mustMatch ctxt) logContextsWithcustomLevelContexts runBoosterLogger :: Booster.Log.LoggerT IO a -> IO a @@ -209,7 +209,7 @@ main = do (fromMaybe stderrLogger mFileLogger) runBoosterLogger $ - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage' $ Text.pack $ "Loading definition from " @@ -239,18 +239,18 @@ main = do >>= evaluate . force . either (error . show) id unless (isJust $ Map.lookup mainModuleName definitionsWithCeilSummaries) $ do runBoosterLogger $ - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage' $ "Main module " <> mainModuleName <> " not found in " <> Text.pack definitionFile liftIO exitFailure liftIO $ runBoosterLogger $ - Booster.Log.withContext "ceil" $ + Booster.Log.withContext CtxInfo $ -- FIXME "ceil" $ forM_ (Map.elems definitionsWithCeilSummaries) $ \(KoreDefinition{simplifications}, summaries) -> do forM_ summaries $ \ComputeCeilSummary{rule, ceils} -> Booster.Log.withRuleContext rule $ do - Booster.Log.withContext "partial-symbols" + Booster.Log.withContext CtxInfo -- FIXME "partial-symbols" $ Booster.Log.logMessage $ Booster.Log.WithJsonMessage (JSON.toJSON rule.computedAttributes.notPreservesDefinednessReasons) @@ -261,7 +261,7 @@ main = do (\(UndefinedSymbol sym) -> Pretty.pretty $ Text.decodeUtf8 $ Booster.decodeLabel' sym) rule.computedAttributes.notPreservesDefinednessReasons unless (null ceils) - $ Booster.Log.withContext "computed-ceils" + $ Booster.Log.withContext CtxInfo -- FIXME"computed-ceils" $ Booster.Log.logMessage $ Booster.Log.WithJsonMessage ( JSON.object @@ -277,7 +277,7 @@ main = do forM_ (concat $ concatMap Map.elems simplifications) $ \s -> unless (null s.computedAttributes.notPreservesDefinednessReasons) $ Booster.Log.withRuleContext s - $ Booster.Log.withContext "partial-symbols" + $ Booster.Log.withContext CtxInfo -- FIXME"partial-symbols" $ Booster.Log.logMessage $ Booster.Log.WithJsonMessage (JSON.toJSON s.computedAttributes.notPreservesDefinednessReasons) @@ -308,13 +308,13 @@ main = do writeGlobalEquationOptions equationOptions runBoosterLogger $ - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage' ("Starting RPC server" :: Text) let koreRespond, boosterRespond :: Respond (API 'Req) (Booster.Log.LoggerT IO) (API 'Res) koreRespond = Kore.respond kore.serverState (ModuleName kore.mainModule) runSMT boosterRespond = - Booster.Log.withContext "booster" + Booster.Log.withContext CtxBooster . Booster.respond boosterState proxyConfig = @@ -341,7 +341,7 @@ main = do , handleSomeException ] interruptHandler _ = - runBoosterLogger . Booster.Log.withContext "proxy" $ do + runBoosterLogger . Booster.Log.withContext CtxProxy $ do Booster.Log.logMessage' @_ @Text "Server shutting down" whenJust statsVar $ \var -> liftIO (Stats.finaliseStats var) >>= Booster.Log.logMessage' @@ -357,7 +357,7 @@ main = do withMDLib (Just fp) f = withDLib fp $ \dl -> f (Just dl) logRequestId rid = - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxProxy $ Booster.Log.logMessage' $ Text.pack $ "Processing request " <> rid diff --git a/dev-tools/booster-dev/Server.hs b/dev-tools/booster-dev/Server.hs index 638d0a76e2..abb3855b7c 100644 --- a/dev-tools/booster-dev/Server.hs +++ b/dev-tools/booster-dev/Server.hs @@ -143,7 +143,7 @@ runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (_logLev filteredBoosterContextLogger = flip Booster.Log.filterLogger boosterContextLogger $ \(Booster.Log.LogMessage (Booster.Flag alwaysDisplay) ctxts _) -> alwaysDisplay - || let ctxt = map (\(Booster.Log.LogContext lc) -> Text.encodeUtf8 $ Booster.Log.toTextualLog lc) ctxts + || let ctxt = map (Text.encodeUtf8 . Booster.Log.toTextualLog) ctxts in any (flip Booster.Log.mustMatch ctxt) $ logContexts <> concatMap (\case Log.LevelOther o -> fromMaybe [] $ levelToContext Map.!? o; _ -> []) customLevels @@ -161,7 +161,7 @@ runServer port definitions defaultMain mLlvmLibrary logFile mSMTOptions (_logLev ( const $ flip runReaderT filteredBoosterContextLogger . Booster.Log.unLoggerT - . Booster.Log.withContext "booster" + . Booster.Log.withContext Booster.Log.CtxBooster . respond stateVar ) [handleSmtError, RpcError.handleErrorCall, RpcError.handleSomeException] diff --git a/dev-tools/count-aborts/Main.hs b/dev-tools/count-aborts/Main.hs index 4b955a3fe9..411f6804a1 100644 --- a/dev-tools/count-aborts/Main.hs +++ b/dev-tools/count-aborts/Main.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE PatternSynonyms #-} + {- | Stand-alone parser executable for testing and profiling Copyright : (c) Runtime Verification, 2022 @@ -11,13 +13,17 @@ import Control.Monad (foldM, forM_) import Data.Aeson (decode) import Data.ByteString.Lazy.Char8 qualified as BS import Data.List (foldl', sortOn) +import Data.Map (Map) import Data.Map qualified as Map import Data.Maybe (fromMaybe) import Data.Ord (Down (..)) +import Data.Sequence (Seq (..)) +import Data.Text (Text) import Data.Text qualified as T import Data.Text.IO qualified as T import System.Environment (getArgs) -import Types + +import Kore.JsonRpc.Types.ContextLog {- | Utility for parsing and extracting information from context logs, produced by running the booster binary with `--log-format json --log-file `. @@ -40,4 +46,31 @@ main = forM_ (sortOn (Down . snd) $ Map.toList counts) $ \((rule, reason), count) -> do let (rType, rLoc) = fromMaybe ("-", "-") $ Map.lookup rule rIdTorLoc T.putStrLn . T.unwords $ - map ("| " <>) [rType <> " " <> rule, rLoc, reason, T.pack (show count)] + map ("| " <>) [rType <> " " <> T.pack (show rule), rLoc, T.pack (show reason), T.pack (show count)] + +type AbortKey = (UniqueId, SimpleContext) + +pattern CRewrite, CFunction, CSimpl :: UniqueId -> CLContext +pattern CRewrite r = CLWithId (CtxRewrite r) +pattern CFunction r = CLWithId (CtxFunction r) +pattern CSimpl r = CLWithId (CtxSimplification r) + +pattern C :: SimpleContext -> CLContext +pattern C ctx = CLNullary ctx + +countAborts :: + (Map AbortKey Int, Map UniqueId (Text, Text)) -> + LogLine -> + (Map AbortKey Int, Map UniqueId (Text, Text)) +countAborts maps@(countMap, ruleMap) LogLine{context, message} = case context of + (_ :|> CRewrite ruleId :|> C reason :|> C CtxAbort) -> increment reason ruleId + (_ :|> CFunction ruleId :|> C CtxFailure :|> C CtxBreak) -> increment CtxFailure ruleId + (_ :|> CSimpl ruleId :|> C CtxFailure :|> C CtxBreak) -> increment CtxFailure ruleId + (_ :|> CFunction ruleId :|> C CtxMatch :|> C CtxFailure :|> C CtxBreak) -> increment CtxFailure ruleId + (_ :|> CSimpl ruleId :|> C CtxMatch :|> C CtxFailure :|> C CtxBreak) -> increment CtxFailure ruleId + (_ :|> CRewrite ruleId :|> C CtxDetail) | CLText ruleLoc <- message -> (countMap, Map.insert ruleId ("rewrite", ruleLoc) ruleMap) + (_ :|> CFunction ruleId :|> C CtxDetail) | CLText ruleLoc <- message -> (countMap, Map.insert ruleId ("function", ruleLoc) ruleMap) + (_ :|> CSimpl ruleId :|> C CtxDetail) | CLText ruleLoc <- message -> (countMap, Map.insert ruleId ("simplification", ruleLoc) ruleMap) + _ -> maps + where + increment rsn rid = (Map.alter (maybe (Just 1) (Just . (+ 1))) (rid, rsn) countMap, ruleMap) diff --git a/dev-tools/kore-rpc-dev/Server.hs b/dev-tools/kore-rpc-dev/Server.hs index f6914b620b..6e4ca8b5d5 100644 --- a/dev-tools/kore-rpc-dev/Server.hs +++ b/dev-tools/kore-rpc-dev/Server.hs @@ -97,7 +97,7 @@ respond kore req = case req of Execute _ -> loggedKore ExecuteM req >>= \case Right (Execute koreResult) -> do - withContext "proxy" $ + withContext CtxKore $ logMessage $ Text.pack $ "Kore " <> show koreResult.reason <> " at " <> show koreResult.depth @@ -126,7 +126,7 @@ respond kore req = case req of pure koreError loggedKore method r = do - withContext "proxy" $ + withContext CtxKore $ logMessage' $ Text.pack $ show method <> " (using kore)" @@ -217,7 +217,7 @@ main = do filteredBoosterContextLogger = flip filterLogger boosterContextLogger $ \(LogMessage (Booster.Flag alwaysDisplay) ctxts _) -> alwaysDisplay - || let ctxt = map (\(LogContext lc) -> Text.encodeUtf8 $ toTextualLog lc) ctxts + || let ctxt = map (Text.encodeUtf8 . toTextualLog) ctxts in any (flip Booster.Log.Context.mustMatch ctxt) logContextsWithcustomLevelContexts runBoosterLogger :: Booster.Log.LoggerT IO a -> IO a @@ -230,7 +230,7 @@ main = do kore@KoreServer{runSMT} <- mkKoreServer Log.LoggerEnv{logAction} clOPts koreSolverOptions runBoosterLogger $ - Booster.Log.withContext "proxy" $ + Booster.Log.withContext CtxKore $ Booster.Log.logMessage' ("Starting RPC server" :: Text.Text) let koreRespond :: Respond (API 'Req) (LoggerT IO) (API 'Res) diff --git a/dev-tools/package.yaml b/dev-tools/package.yaml index aea7fcccc1..749a928d8b 100644 --- a/dev-tools/package.yaml +++ b/dev-tools/package.yaml @@ -99,6 +99,7 @@ executables: - containers - directory - filepath + - kore-rpc-types - text ghc-options: - -rtsopts diff --git a/kore-rpc-types/kore-rpc-types.cabal b/kore-rpc-types/kore-rpc-types.cabal index 107f12e1bc..61519e6237 100644 --- a/kore-rpc-types/kore-rpc-types.cabal +++ b/kore-rpc-types/kore-rpc-types.cabal @@ -67,6 +67,7 @@ common library build-depends: casing >= 0.1.4 build-depends: conduit >= 1.3 build-depends: conduit-extra >=1.3 + build-depends: containers >= 0.6 build-depends: deepseq >=1.4 build-depends: extra >=1.7 build-depends: deriving-aeson >=0.2 @@ -77,6 +78,7 @@ common library build-depends: stm >=2.5 build-depends: stm-conduit >= 4.0 build-depends: text >=1.2 + build-depends: time build-depends: unliftio >= 0.2 build-depends: vector >= 0.12.3.1 @@ -88,6 +90,7 @@ library Kore.JsonRpc.Error Kore.JsonRpc.Types Kore.JsonRpc.Types.Log + Kore.JsonRpc.Types.ContextLog Kore.JsonRpc.Types.Depth Kore.JsonRpc.Server Kore.Syntax.Json.Types diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs new file mode 100644 index 0000000000..dc87190377 --- /dev/null +++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs @@ -0,0 +1,178 @@ +{-# LANGUAGE TemplateHaskell #-} + +{- | +Copyright : (c) Runtime Verification, 2023 +License : BSD-3-Clause +-} +module Kore.JsonRpc.Types.ContextLog ( + module Kore.JsonRpc.Types.ContextLog, +) where + +import Data.Aeson.TH (deriveJSON) +import Data.Aeson.Types (FromJSON (..), ToJSON (..), defaultOptions) +import Data.Aeson.Types qualified as JSON +import Data.Data (Data, toConstr) +import Data.Sequence (Seq) +import Data.Text (Text, unpack) +import Data.Text qualified as Text + +data SimpleContext + = -- component + CtxBooster + | CtxKore + | CtxProxy + | -- method + CtxExecute + | CtxSimplify + | CtxImplies + | CtxGetModel + | CtxAddModule + | -- mode/phase + CtxInternalise + | CtxMatch + | CtxDefinedness + | CtxConstraint + | CtxSMT + | CtxLlvm + | CtxCached + | -- results + CtxFailure + | CtxIndeterminate + | CtxAbort + | CtxSuccess + | CtxBreak + | CtxContinue + | -- information + CtxKoreTerm + | CtxDetail + | CtxSubstitution + | CtxDepth + | -- standard log levels + CtxError + | CtxWarn + | CtxInfo + deriving stock (Eq, Ord, Enum, Data) + +instance Show SimpleContext where + show = JSON.camelTo2 '-' . drop 3 . show . toConstr + +$( deriveJSON + defaultOptions + { JSON.constructorTagModifier = JSON.camelTo2 '-' . drop 3 + , JSON.sumEncoding = JSON.ObjectWithSingleField + } + ''SimpleContext + ) + +---------------------------------------- +data IdContext + = -- entities with hex identifier + CtxRewrite UniqueId + | CtxSimplification UniqueId + | CtxFunction UniqueId + | CtxCeil UniqueId + | CtxTerm UniqueId + | -- entities with name + CtxHook Text + deriving stock (Eq) + +instance Show IdContext where + show (CtxRewrite uid) = "rewrite " <> show uid + show (CtxSimplification uid) = "simplification " <> show uid + show (CtxFunction uid) = "function " <> show uid + show (CtxCeil uid) = "ceil " <> show uid + show (CtxTerm uid) = "term " <> show uid + show (CtxHook name) = "hook " <> unpack name + +---------------------------------------- +data UniqueId + = ShortId Text -- short hashes (7 char) + | LongId Text -- long hashes (64 char) + | UNKNOWN + deriving stock (Eq, Ord) + +instance Show UniqueId where + show (ShortId x) = unpack x + show (LongId x) = unpack $ Text.take 7 x -- for parity with legacy log + show UNKNOWN = "UNKNOWN" + +parseUId :: Text -> Maybe UniqueId +parseUId "UNKNOWN" = pure UNKNOWN +parseUId hex + | Text.length hex == 7 = Just $ ShortId hex + | Text.length hex == 64 = Just $ LongId hex + | otherwise = Nothing + +instance FromJSON UniqueId where + parseJSON = JSON.withText "Hash ID" parseHex + where + parseHex :: Text -> JSON.Parser UniqueId + parseHex hex = + maybe (JSON.parseFail $ "Bad hash ID: " <> show hex) pure $ parseUId hex + +instance ToJSON UniqueId where + toJSON = \case + ShortId x -> JSON.String x + LongId x -> JSON.String x + UNKNOWN -> JSON.String "UNKNOWN" + +$( deriveJSON + defaultOptions + { JSON.constructorTagModifier = JSON.camelTo2 '-' . drop 3 + , JSON.sumEncoding = JSON.ObjectWithSingleField + } + ''IdContext + ) + +---------------------------------------- +data CLContext + = CLNullary SimpleContext + | CLWithId IdContext + deriving stock (Eq) + +instance Show CLContext where + show (CLNullary c) = show c + show (CLWithId withId) = show withId + +instance ToJSON CLContext where + toJSON (CLNullary c) = toJSON c + toJSON (CLWithId withId) = toJSON withId + +instance FromJSON CLContext where + parseJSON = \case + simple@JSON.String{} -> + CLNullary <$> parseJSON simple + obj@JSON.Object{} -> + CLWithId <$> parseJSON obj + other -> + JSON.typeMismatch "Object or string" other + +---------------------------------------- +data CLMessage + = CLText Text -- generic log message + | CLValue JSON.Value -- other stuff + deriving stock (Eq) + +instance Show CLMessage where + show (CLText t) = unpack t + show (CLValue value) = show value + +-- a message is a term if it is an object with format: KORE +instance FromJSON CLMessage where + parseJSON (JSON.String msg) = pure $ CLText msg + parseJSON obj@JSON.Object{} = pure $ CLValue obj + parseJSON arr@JSON.Array{} = pure $ CLValue arr + parseJSON other = + JSON.typeMismatch "Object, array, or string" other + +instance ToJSON CLMessage where + toJSON (CLText text) = toJSON text + toJSON (CLValue value) = value + +data LogLine = LogLine + { context :: Seq CLContext + , message :: CLMessage + } + deriving stock (Show, Eq) + +$(deriveJSON defaultOptions ''LogLine)