diff --git a/CLAUDE.md b/CLAUDE.md index 9963394ecf..a6ecda6464 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -57,7 +57,7 @@ Run `hpack` inside `booster/` if you edit `package.yaml` before cabal sees chang ## Linting and Formatting The CI enforces both — fix them before pushing. -Fourmolu must pass on **every commit**, not just the final one. +Both Fourmolu **and** HLint must pass on **every commit**, not just the final one. ```sh # Format all Haskell files (fourmolu) diff --git a/booster/hs-backend-booster.cabal b/booster/hs-backend-booster.cabal index e3722ab1fb..34970ecf96 100644 --- a/booster/hs-backend-booster.cabal +++ b/booster/hs-backend-booster.cabal @@ -246,6 +246,7 @@ library Booster.LLVM.TH Booster.Log Booster.Log.Context + Booster.Log.LogCapture Booster.Pattern.ApplyEquations Booster.Pattern.Base Booster.Pattern.Binary @@ -368,6 +369,7 @@ executable kore-rpc-booster , stm , text , transformers + , unliftio default-language: Haskell2010 executable kore-rpc-client diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 44f9180a60..a1eeb3bb77 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/booster/library/Booster/JsonRpc.hs @@ -235,7 +235,9 @@ respond stateVar request = } Booster.Log.logMessage $ "Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions) - pure $ RpcTypes.AddModule $ RpcTypes.AddModuleResult moduleHash + pure $ + RpcTypes.AddModule $ + RpcTypes.AddModuleResult{_module = moduleHash, haskellLogEntries = Nothing} RpcTypes.Simplify req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, _) -> Booster.Log.withContext CtxSimplify $ do let internalised = runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term @@ -317,7 +319,11 @@ respond stateVar request = let mkSimplifyResponse state = RpcTypes.Simplify - RpcTypes.SimplifyResult{state, logs = Nothing} + RpcTypes.SimplifyResult + { state + , logs = Nothing + , haskellLogEntries = Nothing + } pure $ second mkSimplifyResponse result RpcTypes.GetModel req -> withModule req._module $ \case (_, _, Nothing, _) -> do @@ -408,6 +414,7 @@ respond stateVar request = RpcTypes.GetModelResult { satisfiable = RpcTypes.Sat , substitution + , haskellLogEntries = Nothing } SMT.IsUnsat -> do logMessage ("SMT result: Unsat" :: Text) @@ -415,6 +422,7 @@ respond stateVar request = RpcTypes.GetModelResult { satisfiable = RpcTypes.Unsat , substitution = Nothing + , haskellLogEntries = Nothing } SMT.IsUnknown reason -> do logMessage $ "SMT result: Unknown - " <> show reason @@ -422,6 +430,7 @@ respond stateVar request = RpcTypes.GetModelResult { satisfiable = RpcTypes.Unknown , substitution = Nothing + , haskellLogEntries = Nothing } RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, _) -> runImplies def mLlvmLibrary mSMTOptions req.antecedent req.consequent -- this case is only reachable if the cancel appeared as part of a batch request @@ -503,6 +512,7 @@ execResponse req (d, traces, rr) unsupported = case rr of $ toList nexts , rule = Nothing , unknownPredicate = Nothing + , haskellLogEntries = Nothing } RewriteStuck p -> Right $ @@ -515,6 +525,7 @@ execResponse req (d, traces, rr) unsupported = case rr of , nextStates = Nothing , rule = Nothing , unknownPredicate = Nothing + , haskellLogEntries = Nothing } RewriteTrivial p -> Right $ @@ -527,6 +538,7 @@ execResponse req (d, traces, rr) unsupported = case rr of , nextStates = Nothing , rule = Nothing , unknownPredicate = Nothing + , haskellLogEntries = Nothing } RewriteCutPoint lbl _ p next -> Right $ @@ -539,6 +551,7 @@ execResponse req (d, traces, rr) unsupported = case rr of , nextStates = Just [toExecState next Nothing unsupported] , rule = Just lbl , unknownPredicate = Nothing + , haskellLogEntries = Nothing } RewriteTerminal lbl _ p -> Right $ @@ -551,6 +564,7 @@ execResponse req (d, traces, rr) unsupported = case rr of , nextStates = Nothing , rule = Just lbl , unknownPredicate = Nothing + , haskellLogEntries = Nothing } RewriteFinished _ _ p -> Right $ @@ -563,6 +577,7 @@ execResponse req (d, traces, rr) unsupported = case rr of , nextStates = Nothing , rule = Nothing , unknownPredicate = Nothing + , haskellLogEntries = Nothing } RewriteAborted failure p -> do Right $ @@ -580,6 +595,7 @@ execResponse req (d, traces, rr) unsupported = case rr of , nextStates = Nothing , rule = Nothing , unknownPredicate = Nothing + , haskellLogEntries = Nothing } where logSuccessfulRewrites = fromMaybe False req.logSuccessfulRewrites diff --git a/booster/library/Booster/Log/LogCapture.hs b/booster/library/Booster/Log/LogCapture.hs new file mode 100644 index 0000000000..a553943e71 --- /dev/null +++ b/booster/library/Booster/Log/LogCapture.hs @@ -0,0 +1,78 @@ +{- | +Copyright : (c) Runtime Verification, 2026 +License : BSD-3-Clause + +Booster-side per-request log capture for the @haskell-logging@ +JSON-RPC flag. + +Provides a tee combinator and a capture 'Logger' so a request handler +can fan its logs into a per-request 'Collector' on top of the regular +stderr/file logger. Capture is purely additive; the existing logger +keeps writing exactly what it would have anyway. + +Which messages are captured is decided per request by the set of +context names carried on the request (see 'Booster.JsonRpc' / +@Proxy.withHaskellLoggingCapture@); a message matches if any context in +its stack has a requested name (via 'clContextName', so id-carrying +contexts like @CtxRewrite@ match by tag). Names this engine does not +recognise (e.g. kore entry-type names) simply never match here. +-} +module Booster.Log.LogCapture ( + withBoosterCapture, +) where + +import Control.Monad (when) +import Data.Aeson (Value (String)) +import Data.Sequence qualified as Seq +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Text (Text) + +import Booster.Log (LogMessage (..), Logger (..), LoggerMIO (..), toJSONLog) +import Kore.JsonRpc.Types.ContextLog (CLMessage (..), LogLine (..), clContextName) +import Kore.JsonRpc.Types.LogCapture (Collector, appendCollector) + +{- | A 'Logger' that writes matching 'LogMessage's as structured +'LogLine's into the given 'Collector'. A message matches when any +context in its stack has one of the requested names. Compose with the +existing logger via 'teeLogger' to enable capture without losing +stderr/file output. +-} +boosterCaptureLogger :: Set Text -> Collector -> Logger LogMessage +boosterCaptureLogger names collector = + Logger $ \msg@(LogMessage _ ctxts _) -> + when (any ((`Set.member` names) . clContextName) ctxts) $ + appendCollector collector (renderLogMessage msg) + +{- | Build a 'LogLine' from a booster 'LogMessage'. The context stack is +already a list of 'CLContext', so it carries over directly; the message +is wrapped as 'CLText' when it renders to a JSON string and 'CLValue' +otherwise. This is the same content the JSON file logger emits. +-} +renderLogMessage :: LogMessage -> LogLine +renderLogMessage (LogMessage _ ctxts msg) = + LogLine + { timestamp = Nothing + , context = Seq.fromList ctxts + , message = case toJSONLog msg of + String t -> CLText t + other -> CLValue other + } + +{- | Run two loggers on every message. Order is left-then-right; both +run unconditionally. +-} +teeLogger :: Logger LogMessage -> Logger LogMessage -> Logger LogMessage +teeLogger (Logger l1) (Logger l2) = + Logger $ \m -> l1 m >> l2 m + +{- | Run a 'LoggerMIO' action with the booster-side capture installed +as a tee onto the existing logger. When 'Nothing' this is the +identity. Otherwise the carried context-name set selects which +messages are captured. The original logger continues to receive every +message; capture is purely additive. +-} +withBoosterCapture :: LoggerMIO m => Maybe (Collector, Set Text) -> m a -> m a +withBoosterCapture Nothing = id +withBoosterCapture (Just (collector, names)) = + withLogger (`teeLogger` boosterCaptureLogger names collector) diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index dcc9c0e1f2..e1d115f328 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -213,6 +213,7 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = , valid = False , condition , logs = Nothing + , haskellLogEntries = Nothing } doesNotImply s' = let s = externaliseSort s' in doesNotImply' s Nothing @@ -239,5 +240,6 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = $ subst } , logs = Nothing + , haskellLogEntries = Nothing } implies s' = let s = externaliseSort s' in implies' (Kore.Syntax.KJTop s) s diff --git a/booster/package.yaml b/booster/package.yaml index 1e39cbec2b..f465fca43b 100644 --- a/booster/package.yaml +++ b/booster/package.yaml @@ -163,6 +163,7 @@ executables: - stm - text - transformers + - unliftio ghc-options: - -rtsopts - -threaded diff --git a/booster/test/rpc-integration/resources/haskell-log-capture.kore b/booster/test/rpc-integration/resources/haskell-log-capture.kore new file mode 120000 index 0000000000..11bc018fec --- /dev/null +++ b/booster/test/rpc-integration/resources/haskell-log-capture.kore @@ -0,0 +1 @@ +a-to-f.kore \ No newline at end of file diff --git a/booster/test/rpc-integration/test-haskell-log-capture/README.md b/booster/test/rpc-integration/test-haskell-log-capture/README.md new file mode 100644 index 0000000000..ea60fa35d8 --- /dev/null +++ b/booster/test/rpc-integration/test-haskell-log-capture/README.md @@ -0,0 +1,23 @@ +# Per-request log capture (`haskell-logging`) + +Exercises the `haskell-logging` JSON-RPC request flag and the corresponding +`haskell-log-entries` response field. The request carries a **list of +entry/context names** to capture; the matching log entries are returned in-band. + +`test.sh` sends `execute` requests against the small `a-to-f` definition +(reused via the `resources/haskell-log-capture.kore` symlink) and asserts: + +1. a list of booster context names (`params-contexts.json`) yields a non-empty + `haskell-log-entries` array; +2. narrowing the list to just `["Proxy"]` (`params-proxy-only.json`) still + captures entries, and *every* captured entry carries a proxy context — i.e. + the list selects per request; +3. omitting the flag (`params-control.json`) omits `haskell-log-entries`. + +Names route across both engines: kore entry-type names (e.g. +`DebugAttemptEquation`) are resolved against the kore log registry, booster +context names (e.g. `Proxy`, `Rewrite`) against the message context stack +(tag-only for id-carrying contexts like `CtxRewrite`); a name unknown to both is +skipped. The capture happens in the proxy, so the test runs only under +`kore-rpc-booster`. Entries are not diffed against a golden file because their +content is timing-sensitive; the test asserts on presence/selection. diff --git a/booster/test/rpc-integration/test-haskell-log-capture/params-contexts.json b/booster/test/rpc-integration/test-haskell-log-capture/params-contexts.json new file mode 100644 index 0000000000..03798091fd --- /dev/null +++ b/booster/test/rpc-integration/test-haskell-log-capture/params-contexts.json @@ -0,0 +1,4 @@ +{ + "max-depth": 6, + "haskell-logging": ["Proxy", "Detail", "Abort", "Simplify", "Rewrite"] +} diff --git a/booster/test/rpc-integration/test-haskell-log-capture/params-control.json b/booster/test/rpc-integration/test-haskell-log-capture/params-control.json new file mode 100644 index 0000000000..252c66b408 --- /dev/null +++ b/booster/test/rpc-integration/test-haskell-log-capture/params-control.json @@ -0,0 +1,3 @@ +{ + "max-depth": 6 +} diff --git a/booster/test/rpc-integration/test-haskell-log-capture/params-proxy-only.json b/booster/test/rpc-integration/test-haskell-log-capture/params-proxy-only.json new file mode 100644 index 0000000000..7695674bdd --- /dev/null +++ b/booster/test/rpc-integration/test-haskell-log-capture/params-proxy-only.json @@ -0,0 +1,4 @@ +{ + "max-depth": 6, + "haskell-logging": ["Proxy"] +} diff --git a/booster/test/rpc-integration/test-haskell-log-capture/state.execute b/booster/test/rpc-integration/test-haskell-log-capture/state.execute new file mode 120000 index 0000000000..130378a8bb --- /dev/null +++ b/booster/test/rpc-integration/test-haskell-log-capture/state.execute @@ -0,0 +1 @@ +../resources/a-to-f/state-d.json \ No newline at end of file diff --git a/booster/test/rpc-integration/test-haskell-log-capture/test.sh b/booster/test/rpc-integration/test-haskell-log-capture/test.sh new file mode 100755 index 0000000000..634dbb0b4d --- /dev/null +++ b/booster/test/rpc-integration/test-haskell-log-capture/test.sh @@ -0,0 +1,62 @@ +#!/usr/bin/env bash + +# Round-trip test for the per-request `haskell-logging` JSON-RPC flag. +# +# The request carries a list of entry/context names to capture; the matching +# log entries come back in-band on `haskell-log-entries`. Uses variables +# provided by runDirectoryTest.sh: ${client} (with port), ${dir}, and "$@". +# +# The capture-and-attach happens in the proxy (booster/tools/booster/Proxy.hs), +# so this test is only meaningful under kore-rpc-booster — see the entry in +# scripts/booster-integration-tests.sh. +# +# Assertions (against the small `a-to-f` definition, whose execute exercises the +# booster-side contexts): +# 1. a name list of booster contexts comes back with a non-empty +# `haskell-log-entries` array; +# 2. narrowing the list to just ["Proxy"] still captures entries, and *every* +# captured entry carries a proxy context — i.e. the list selects per +# request (subset correctness); +# 3. omitting the flag omits `haskell-log-entries` entirely. +# +# We assert on shape/selection rather than diffing a golden file: the captured +# entries contain timing- and scheduling-sensitive content that is not stable. + +set -exuo pipefail + +# runDirectoryTest.sh forwards extra args (e.g. --regenerate). There are no +# golden files here, so drop --regenerate and pass the rest to the client. +client_args="" +for arg in $*; do + case "$arg" in + --regenerate) ;; + *) client_args+=" $arg" ;; + esac +done + +workdir=$(mktemp -d) +contexts="$workdir/contexts.json" +proxy_only="$workdir/proxy-only.json" +control="$workdir/control.json" + +echo "1. execute with a booster-context name list -> non-empty capture" +${client} execute "$dir/state.execute" \ + --param-file "$dir/params-contexts.json" \ + --output "$contexts" ${client_args} +jq -e '.result["haskell-log-entries"] | type == "array" and length > 0' "$contexts" > /dev/null + +echo "2. execute selecting only [\"Proxy\"] -> non-empty, and every entry carries a proxy context" +${client} execute "$dir/state.execute" \ + --param-file "$dir/params-proxy-only.json" \ + --output "$proxy_only" ${client_args} +jq -e '.result["haskell-log-entries"] | type == "array" and length > 0' "$proxy_only" > /dev/null +jq -e '.result["haskell-log-entries"] | all((.context | tostring) | test("proxy"))' "$proxy_only" > /dev/null + +echo "3. execute WITHOUT the flag (control) -> haskell-log-entries omitted" +${client} execute "$dir/state.execute" \ + --param-file "$dir/params-control.json" \ + --output "$control" ${client_args} +jq -e '.result | has("haskell-log-entries") | not' "$control" > /dev/null + +rm -rf "$workdir" +echo "haskell-logging capture round-trip OK" diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs index e65d5ced6c..2be6308e72 100644 --- a/booster/tools/booster/Proxy.hs +++ b/booster/tools/booster/Proxy.hs @@ -1,4 +1,5 @@ {-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} {- | Module : Proxy @@ -44,12 +45,18 @@ import Kore.JsonRpc qualified as Kore (ServerState) import Kore.JsonRpc.Types import Kore.JsonRpc.Types qualified as ExecuteRequest (ExecuteRequest (..)) import Kore.JsonRpc.Types qualified as SimplifyRequest (SimplifyRequest (..)) +import Kore.JsonRpc.Types.ContextLog (LogLine) import Kore.JsonRpc.Types.Log qualified as RPCLog +import Kore.JsonRpc.Types.LogCapture (drainCollector, newCollector) import Kore.Log qualified +import Kore.Log.LogCapture (KoreCaptureRegistry, koreTypesFromNames, withKoreCapture) import Kore.Syntax.Definition (SentenceAxiom) import Kore.Syntax.Json.Types qualified as KoreJson import SMT qualified import Stats (MethodTiming (..), StatsVar, addStats, secWithUnit, timed) +import UnliftIO (MonadUnliftIO, withRunInIO) + +import Booster.Log.LogCapture (withBoosterCapture) data KoreServer = KoreServer { serverState :: MVar.MVar Kore.ServerState @@ -61,6 +68,11 @@ data KoreServer = KoreServer SMT.SMT a -> IO a , loggerEnv :: Kore.Log.LoggerEnv IO + , captureRegistry :: KoreCaptureRegistry + -- ^ per-request kore log capture registry; the kore log action + -- is wired at server startup to consult this registry for the + -- calling thread so requests that opt in via @haskell-logging@ + -- can drain captured entries into their response. } data ProxyConfig = ProxyConfig @@ -71,134 +83,199 @@ data ProxyConfig = ProxyConfig , simplifyAtEnd :: Bool , simplifyBeforeFallback :: Bool , customLogLevels :: ![Log.LogLevel] + , koreCaptureRegistry :: KoreCaptureRegistry + -- ^ shared with 'KoreServer.captureRegistry'; the proxy uses it + -- to register a per-request kore-side capture collector for the + -- duration of any kore invocation triggered while serving a + -- @haskell-logging: true@ request. } serverError :: String -> Value -> ErrorObj serverError detail = ErrorObj ("Server error: " <> detail) (-32032) +{- | Extract the @haskell-logging@ entry-name list from any request type +that carries it. 'Nothing' (and 'Cancel', which has no payload) yields +the empty list, i.e. capture nothing. +-} +haskellLoggingEntries :: API 'Req -> [Text] +haskellLoggingEntries = \case + Execute r -> fromMaybe [] r.haskellLogging + Implies r -> fromMaybe [] r.haskellLogging + Simplify r -> fromMaybe [] r.haskellLogging + AddModule r -> fromMaybe [] r.haskellLogging + GetModel r -> fromMaybe [] r.haskellLogging + Cancel -> [] + +{- | Reconstruct the result variant with its 'haskellLogEntries' field +set to the captured entries. Written as full record construction +(via 'RecordWildCards') rather than record-update so that the +@DuplicateRecordFields@-flagged 'haskellLogEntries' name is +unambiguously resolved to each concrete constructor. The 'API' GADT +hides each result type behind a type family, which interacts poorly +with record-update sugar. +-} +injectHaskellLogEntries :: Maybe [LogLine] -> API 'Res -> API 'Res +injectHaskellLogEntries entries = \case + Execute ExecuteResult{..} -> Execute ExecuteResult{haskellLogEntries = entries, ..} + Implies ImpliesResult{..} -> Implies ImpliesResult{haskellLogEntries = entries, ..} + Simplify SimplifyResult{..} -> Simplify SimplifyResult{haskellLogEntries = entries, ..} + AddModule AddModuleResult{..} -> AddModule AddModuleResult{haskellLogEntries = entries, ..} + GetModel GetModelResult{..} -> GetModel GetModelResult{haskellLogEntries = entries, ..} + +{- | Run a request handler with the haskell-logging capture installed +when the request asked for any entries, then attach the captured +entries to the response. The requested name list is a single flat set +spanning both engines: it is passed verbatim to the booster capture +('withBoosterCapture', a ReaderT-overlaid logger tee, which matches by +context name) and resolved to kore entry types ('koreTypesFromNames') +for the kore capture ('withKoreCapture', which registers the collector +and type set against the calling thread in the shared +'KoreCaptureRegistry'). Each engine ignores names it does not +recognise, so a name unknown to both is simply never captured. When +the list is empty this is the identity. +-} +withHaskellLoggingCapture :: + (Booster.Log.LoggerMIO m, MonadUnliftIO m) => + KoreCaptureRegistry -> + [Text] -> + m (Either ErrorObj (API 'Res)) -> + m (Either ErrorObj (API 'Res)) +withHaskellLoggingCapture registry names action + | null names = action + | otherwise = do + collector <- liftIO newCollector + let boosterNames = Set.fromList names + koreTypes = koreTypesFromNames names + result <- + withBoosterCapture (Just (collector, boosterNames)) $ + withRunInIO $ \run -> + withKoreCapture registry (Just (collector, koreTypes)) (run action) + entries <- liftIO (drainCollector collector) + pure $ second (injectHaskellLogEntries (Just entries)) result + respondEither :: forall m. - Booster.Log.LoggerMIO m => + (Booster.Log.LoggerMIO m, MonadUnliftIO m) => ProxyConfig -> Respond (API 'Req) m (API 'Res) -> Respond (API 'Req) m (API 'Res) -> Respond (API 'Req) m (API 'Res) -respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of - Execute execReq - | isJust execReq.stepTimeout || isJust execReq.movingAverageStepTimeout -> - loggedKore ExecuteM req - | otherwise -> - let logSettings = - LogSettings - { logSuccessfulRewrites = execReq.logSuccessfulRewrites - , logFailedRewrites = execReq.logFailedRewrites - } - in do - bState <- liftIO $ MVar.readMVar boosterState - let m = fromMaybe bState.defaultMain execReq._module - def = - fromMaybe (error $ "Module " <> show m <> " not found") $ - Map.lookup m bState.definitions - handleExecute logSettings def execReq - Implies impliesReq - | fromMaybe False impliesReq.assumeDefined || fromMaybe False impliesReq.boosterOnly -> do - -- try the booster end-point first - (boosterResult, boosterTime) <- Stats.timed $ booster req - case boosterResult of - res@Right{} -> do - logStats ImpliesM (boosterTime, 0) - pure res - Left err - | fromMaybe False impliesReq.boosterOnly -> do - Booster.Log.withContext CtxProxy $ - Booster.Log.logMessage . Text.pack $ - "Implies abort in booster (booster-only mode): " - <> fromError err - -- Emit a structured proxy-level closing event so that - -- pyk's group_kore_calls() can finalise the KoreCall for - -- this request. Without this, the accumulated - -- BoosterEquationFailed data stays orphaned in the - -- pending dict because no result event ever closes it. - Booster.Log.withContexts [CtxProxy, CtxAbort, CtxDetail] $ - Booster.Log.logMessage $ - WithJsonMessage - ( object - [ "tag" .= ("booster-implies-invalid" :: Text) - , "antecedent" .= impliesReq.antecedent - , "consequent" .= impliesReq.consequent - , "valid" .= False - ] - ) - ("booster-implies-invalid" :: Text) +respondEither cfg@ProxyConfig{boosterState, koreCaptureRegistry} booster kore req = + withHaskellLoggingCapture koreCaptureRegistry (haskellLoggingEntries req) $ case req of + Execute execReq + | isJust execReq.stepTimeout || isJust execReq.movingAverageStepTimeout -> + loggedKore ExecuteM req + | otherwise -> + let logSettings = + LogSettings + { logSuccessfulRewrites = execReq.logSuccessfulRewrites + , logFailedRewrites = execReq.logFailedRewrites + } + in do + bState <- liftIO $ MVar.readMVar boosterState + let m = fromMaybe bState.defaultMain execReq._module + def = + fromMaybe (error $ "Module " <> show m <> " not found") $ + Map.lookup m bState.definitions + handleExecute logSettings def execReq + Implies impliesReq + | fromMaybe False impliesReq.assumeDefined || fromMaybe False impliesReq.boosterOnly -> do + -- try the booster end-point first + (boosterResult, boosterTime) <- Stats.timed $ booster req + case boosterResult of + res@Right{} -> do logStats ImpliesM (boosterTime, 0) - pure $ Left err - | otherwise -> do - Booster.Log.withContext CtxProxy $ - Booster.Log.logMessage . Text.pack $ - "Implies abort in booster: " - <> fromError err - <> ". Falling back to kore." - (koreRes, koreTime) <- Stats.timed $ kore req - logStats ImpliesM (boosterTime + koreTime, koreTime) - Booster.Log.withContexts [CtxProxy, CtxAbort, CtxDetail] $ - Booster.Log.logMessage $ - WithJsonMessage - ( object $ - [ "tag" .= ("kore-implies-fallback" :: Text) - , "antecedent" .= impliesReq.antecedent - , "consequent" .= impliesReq.consequent - ] - <> case koreRes of - Right (Implies r) -> ["valid" .= r.valid] - _ -> [] - ) - ("kore-implies-fallback" :: Text) - pure koreRes - | otherwise -> do - (koreRes, koreTime) <- Stats.timed $ kore req - logStats ImpliesM (koreTime, koreTime) - Booster.Log.withContext CtxProxy $ - Booster.Log.withContext CtxDetail $ - Booster.Log.logMessage $ - WithJsonMessage - ( object $ - [ "tag" .= ("kore-implies" :: Text) - , "antecedent" .= impliesReq.antecedent - , "consequent" .= impliesReq.consequent - ] - <> case koreRes of - Right (Implies r) -> ["valid" .= r.valid] - _ -> [] - ) - ("kore-implies" :: Text) - pure koreRes - Simplify simplifyReq -> - handleSimplify simplifyReq - AddModule _ -> do - -- execute in booster first, assuming that kore won't throw an - -- error if booster did not. The response is empty anyway. - (boosterResult, boosterTime) <- Stats.timed $ booster req - case boosterResult of - Left _err -> pure boosterResult - Right _ -> do + pure res + Left err + | fromMaybe False impliesReq.boosterOnly -> do + Booster.Log.withContext CtxProxy $ + Booster.Log.logMessage . Text.pack $ + "Implies abort in booster (booster-only mode): " + <> fromError err + -- Emit a structured proxy-level closing event so that + -- pyk's group_kore_calls() can finalise the KoreCall for + -- this request. Without this, the accumulated + -- BoosterEquationFailed data stays orphaned in the + -- pending dict because no result event ever closes it. + Booster.Log.withContexts [CtxProxy, CtxAbort, CtxDetail] $ + Booster.Log.logMessage $ + WithJsonMessage + ( object + [ "tag" .= ("booster-implies-invalid" :: Text) + , "antecedent" .= impliesReq.antecedent + , "consequent" .= impliesReq.consequent + , "valid" .= False + ] + ) + ("booster-implies-invalid" :: Text) + logStats ImpliesM (boosterTime, 0) + pure $ Left err + | otherwise -> do + Booster.Log.withContext CtxProxy $ + Booster.Log.logMessage . Text.pack $ + "Implies abort in booster: " + <> fromError err + <> ". Falling back to kore." + (koreRes, koreTime) <- Stats.timed $ kore req + logStats ImpliesM (boosterTime + koreTime, koreTime) + Booster.Log.withContexts [CtxProxy, CtxAbort, CtxDetail] $ + Booster.Log.logMessage $ + WithJsonMessage + ( object $ + [ "tag" .= ("kore-implies-fallback" :: Text) + , "antecedent" .= impliesReq.antecedent + , "consequent" .= impliesReq.consequent + ] + <> case koreRes of + Right (Implies r) -> ["valid" .= r.valid] + _ -> [] + ) + ("kore-implies-fallback" :: Text) + pure koreRes + | otherwise -> do (koreRes, koreTime) <- Stats.timed $ kore req - logStats AddModuleM (boosterTime + koreTime, koreTime) + logStats ImpliesM (koreTime, koreTime) + Booster.Log.withContext CtxProxy $ + Booster.Log.withContext CtxDetail $ + Booster.Log.logMessage $ + WithJsonMessage + ( object $ + [ "tag" .= ("kore-implies" :: Text) + , "antecedent" .= impliesReq.antecedent + , "consequent" .= impliesReq.consequent + ] + <> case koreRes of + Right (Implies r) -> ["valid" .= r.valid] + _ -> [] + ) + ("kore-implies" :: Text) pure koreRes - GetModel getModelReq -> do - -- try the booster end-point first - (bResult, bTime) <- Stats.timed $ booster req - let boosterOnly = fromMaybe False getModelReq.boosterOnly - (result, kTime) <- - case bResult of - Left err + Simplify simplifyReq -> + handleSimplify simplifyReq + AddModule _ -> do + -- execute in booster first, assuming that kore won't throw an + -- error if booster did not. The response is empty anyway. + (boosterResult, boosterTime) <- Stats.timed $ booster req + case boosterResult of + Left _err -> pure boosterResult + Right _ -> do + (koreRes, koreTime) <- Stats.timed $ kore req + logStats AddModuleM (boosterTime + koreTime, koreTime) + pure koreRes + GetModel getModelReq -> do + -- try the booster end-point first + (bResult, bTime) <- Stats.timed $ booster req + let boosterOnly = fromMaybe False getModelReq.boosterOnly + (result, kTime) <- + case bResult of -- under booster-only, booster errors are returned as-is — no kore fallback - | boosterOnly -> do + Left err | boosterOnly -> do Booster.Log.withContext CtxProxy $ Booster.Log.logMessage $ Text.pack $ "get-model error in booster (booster-only mode, not falling back): " <> fromError err pure (Left err, 0) - | otherwise -> do + Left err -> do Booster.Log.withContext CtxProxy $ Booster.Log.logMessage $ Text.pack $ @@ -217,42 +294,42 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of ) ("kore-get-model-fallback" :: Text) pure (kRes, kTime) - Right (GetModel res@GetModelResult{}) - -- re-check with legacy-kore if result is unknown, - -- unless the request asked us to stay booster-only - | Unknown <- res.satisfiable - , not boosterOnly -> do - Booster.Log.withContext CtxProxy $ - Booster.Log.withContext CtxAbort $ - Booster.Log.logMessage $ - Text.pack "Re-checking a get-model result Unknown" - (kResult, kTime) <- Stats.timed $ kore req - Booster.Log.withContext CtxProxy $ - Booster.Log.withContext CtxAbort $ + Right (GetModel res@GetModelResult{}) + -- re-check with legacy-kore if result is unknown, + -- unless the request asked us to stay booster-only + | Unknown <- res.satisfiable + , not boosterOnly -> do + Booster.Log.withContext CtxProxy $ + Booster.Log.withContext CtxAbort $ + Booster.Log.logMessage $ + Text.pack "Re-checking a get-model result Unknown" + (kResult, kTime) <- Stats.timed $ kore req + Booster.Log.withContext CtxProxy $ + Booster.Log.withContext CtxAbort $ + Booster.Log.logMessage $ + "Double-check returned " <> toStrict (encodeToLazyText kResult) + Booster.Log.withContexts [CtxProxy, CtxAbort, CtxDetail] $ Booster.Log.logMessage $ - "Double-check returned " <> toStrict (encodeToLazyText kResult) - Booster.Log.withContexts [CtxProxy, CtxAbort, CtxDetail] $ - Booster.Log.logMessage $ - WithJsonMessage - ( object $ - [ "tag" .= ("kore-get-model-recheck" :: Text) - , "state" .= getModelReq.state - ] - <> case kResult of - Right (GetModel r) -> ["satisfiable" .= r.satisfiable] - _ -> [] - ) - ("kore-get-model-recheck" :: Text) - pure (kResult, kTime) - -- keep other results (including Unknown under booster-only) - | otherwise -> - pure (bResult, 0) - other -> - error $ "Unexpected get-model result " <> show other - logStats GetModelM (bTime + kTime, kTime) - pure result - Cancel -> - pure $ Left $ ErrorObj "Cancel not supported" (-32601) Null + WithJsonMessage + ( object $ + [ "tag" .= ("kore-get-model-recheck" :: Text) + , "state" .= getModelReq.state + ] + <> case kResult of + Right (GetModel r) -> ["satisfiable" .= r.satisfiable] + _ -> [] + ) + ("kore-get-model-recheck" :: Text) + pure (kResult, kTime) + -- keep other results (including Unknown under booster-only) + | otherwise -> + pure (bResult, 0) + other -> + error $ "Unexpected get-model result " <> show other + logStats GetModelM (bTime + kTime, kTime) + pure result + Cancel -> + pure $ Left $ ErrorObj "Cancel not supported" (-32601) Null where handleSimplify :: SimplifyRequest -> m (Either ErrorObj (API 'Res)) handleSimplify simplifyReq = do @@ -268,6 +345,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of SimplifyResult { state = boosterRes.state , logs = postProcessLogs <$> boosterRes.logs + , haskellLogEntries = Nothing } | otherwise -> do let koreReq = @@ -315,6 +393,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of [ boosterRes.logs , koreRes.logs ] + , haskellLogEntries = Nothing } koreError -> -- can only be an error @@ -679,6 +758,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of { state = execStateToKoreJson state , _module = mbModule , boosterOnly = mbBoosterOnly + , haskellLogging = Nothing } -- used for post-exec simplification returns either a state to diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs index 8ab92bc50d..4da266e8d8 100644 --- a/booster/tools/booster/Server.hs +++ b/booster/tools/booster/Server.hs @@ -95,6 +95,7 @@ import Kore.Log.BoosterAdaptor ( import Kore.Log.BoosterAdaptor qualified as Log import Kore.Log.DebugContext qualified as Log import Kore.Log.DebugSolver qualified as Log +import Kore.Log.LogCapture (KoreCaptureRegistry, newKoreCaptureRegistry, registryLogAction) import Kore.Log.Registry qualified as Log import Kore.Rewrite.SMT.Lemma (declareSMTLemmas) import Kore.Syntax.Definition (ModuleName (ModuleName), SentenceAxiom) @@ -162,6 +163,8 @@ main = do mTimeCache <- if logTimeStamps then Just <$> Booster.newTimeCache timestampFlag else pure Nothing + koreCaptureRegistry <- newKoreCaptureRegistry + Booster.withFastLogger mTimeCache logFile $ \stderrLogger mFileLogger -> do let koreLogRenderer = case logFormat of Standard -> renderStandardPretty @@ -201,14 +204,16 @@ main = do flip runReaderT (filteredBoosterContextLogger, toModifiersRep prettyPrintOptions) . Booster.Log.unLoggerT - koreLogActions :: forall m. MonadIO m => [Log.LogAction m Log.SomeEntry] - koreLogActions = [koreLogAction] - where - koreLogAction = - koreSomeEntryLogAction - koreLogRenderer - koreLogFilter - (fromMaybe stderrLogger mFileLogger) + -- The configured (CLI -l/--log-entries) kore log action that renders + -- to stderr/file. Per-request capture is NOT included here: it is + -- composed outside koreLogFilters below (see mvarLogAction) so that + -- haskell-logging capture is independent of the server's -l set. + koreLogAction :: forall m. MonadIO m => Log.LogAction m Log.SomeEntry + koreLogAction = + koreSomeEntryLogAction + koreLogRenderer + koreLogFilter + (fromMaybe stderrLogger mFileLogger) runBoosterLogger $ Booster.Log.withContext CtxProxy $ @@ -228,7 +233,7 @@ main = do , Log.timestampsSwitch = TimestampsDisable , Log.debugSolverOptions = Log.DebugSolverOptions . fmap (<> ".kore") $ smtOptions >>= (.transcript) - , Log.logType = LogProxy (mconcat koreLogActions) + , Log.logType = LogProxy koreLogAction , Log.logFormat = Log.Standard } srvSettings = serverSettings port "*" @@ -290,11 +295,18 @@ main = do $ map (pretty' @mods) s.computedAttributes.notPreservesDefinednessReasons - mvarLogAction <- newMVar actualLogAction + -- Compose the kore-side per-request capture action *outside* the + -- koreLogFilters wrapper that withLogger applied to actualLogAction. + -- Kore emits its entries unconditionally (Log.logEntry is not gated + -- by logEntries), so capturing here — filtered only by each request's + -- own requested entry-type set — makes `haskell-logging` self-sufficient: + -- the requested kore entries are captured regardless of the server's + -- -l/--log-entries configuration. + mvarLogAction <- newMVar (actualLogAction <> registryLogAction koreCaptureRegistry) let logAction = swappableLogger mvarLogAction kore@KoreServer{runSMT} <- - mkKoreServer Log.LoggerEnv{logAction} clOPts koreSolverOptions + mkKoreServer Log.LoggerEnv{logAction} koreCaptureRegistry clOPts koreSolverOptions boosterState <- liftIO $ @@ -330,6 +342,7 @@ main = do , simplifyAtEnd , simplifyBeforeFallback , customLogLevels = customLevels + , koreCaptureRegistry } server = jsonRpcServer @@ -512,8 +525,8 @@ translateSMTOpts = \case translateSExpr (SMT.List ss) = KoreSMT.List $ map translateSExpr ss mkKoreServer :: - Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer -mkKoreServer loggerEnv@Log.LoggerEnv{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions = + Log.LoggerEnv IO -> KoreCaptureRegistry -> CLOptions -> KoreSolverOptions -> IO KoreServer +mkKoreServer loggerEnv@Log.LoggerEnv{logAction} captureRegistry CLOptions{definitionFile, mainModuleName} koreSolverOptions = flip Log.runLoggerT logAction $ Log.logWhile (Log.DebugContext $ Log.CLNullary CtxKore) $ do sd@GlobalMain.SerializedDefinition{internedTextCache} <- GlobalMain.deserializeDefinition @@ -538,6 +551,7 @@ mkKoreServer loggerEnv@Log.LoggerEnv{logAction} CLOptions{definitionFile, mainMo , mainModule = mainModuleName , runSMT , loggerEnv + , captureRegistry } where KoreSMT.KoreSolverOptions{timeOut, retryLimit, tactic, args} = koreSolverOptions diff --git a/dev-tools/kore-rpc-dev/Server.hs b/dev-tools/kore-rpc-dev/Server.hs index a8a1daad7a..012398d49a 100644 --- a/dev-tools/kore-rpc-dev/Server.hs +++ b/dev-tools/kore-rpc-dev/Server.hs @@ -122,6 +122,7 @@ respond kore req = case req of SimplifyResult { state = koreRes.state , logs = koreRes.logs + , haskellLogEntries = Nothing } koreError -> pure koreError diff --git a/kore-rpc-types/kore-rpc-types.cabal b/kore-rpc-types/kore-rpc-types.cabal index 61519e6237..883a4673ff 100644 --- a/kore-rpc-types/kore-rpc-types.cabal +++ b/kore-rpc-types/kore-rpc-types.cabal @@ -92,6 +92,7 @@ library Kore.JsonRpc.Types.Log Kore.JsonRpc.Types.ContextLog Kore.JsonRpc.Types.Depth + Kore.JsonRpc.Types.LogCapture Kore.JsonRpc.Server Kore.Syntax.Json.Types hs-source-dirs: diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types.hs b/kore-rpc-types/src/Kore/JsonRpc/Types.hs index 8e6b319794..0716971038 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types.hs @@ -27,6 +27,7 @@ import Deriving.Aeson ( ) import GHC.Generics (Generic) import GHC.TypeLits +import Kore.JsonRpc.Types.ContextLog (LogLine) import Kore.JsonRpc.Types.Depth (Depth (..)) import Kore.JsonRpc.Types.Log (LogEntry) import Kore.Syntax.Json.Types (KoreJson) @@ -47,6 +48,7 @@ data ExecuteRequest = ExecuteRequest , logSuccessfulRewrites :: !(Maybe Bool) , logFailedRewrites :: !(Maybe Bool) , boosterOnly :: !(Maybe Bool) + , haskellLogging :: !(Maybe [Text]) } deriving stock (Generic, Show, Eq) deriving @@ -59,6 +61,7 @@ data ImpliesRequest = ImpliesRequest , _module :: !(Maybe Text) , assumeDefined :: !(Maybe Bool) , boosterOnly :: !(Maybe Bool) + , haskellLogging :: !(Maybe [Text]) } deriving stock (Generic, Show, Eq) deriving @@ -69,6 +72,7 @@ data SimplifyRequest = SimplifyRequest { state :: KoreJson , _module :: !(Maybe Text) , boosterOnly :: !(Maybe Bool) + , haskellLogging :: !(Maybe [Text]) } deriving stock (Generic, Show, Eq) deriving @@ -78,6 +82,7 @@ data SimplifyRequest = SimplifyRequest data AddModuleRequest = AddModuleRequest { _module :: Text , nameAsId :: !(Maybe Bool) + , haskellLogging :: !(Maybe [Text]) } deriving stock (Generic, Show, Eq) deriving @@ -88,6 +93,7 @@ data GetModelRequest = GetModelRequest { state :: KoreJson , _module :: !(Maybe Text) , boosterOnly :: !(Maybe Bool) + , haskellLogging :: !(Maybe [Text]) } deriving stock (Generic, Show, Eq) deriving @@ -142,6 +148,7 @@ data ExecuteResult = ExecuteResult , rule :: Maybe Text , logs :: Maybe [LogEntry] , unknownPredicate :: Maybe KoreJson + , haskellLogEntries :: Maybe [LogLine] } deriving stock (Generic, Show, Eq) deriving @@ -162,6 +169,7 @@ data ImpliesResult = ImpliesResult , valid :: Bool , condition :: Maybe Condition , logs :: Maybe [LogEntry] + , haskellLogEntries :: Maybe [LogLine] } deriving stock (Generic, Show, Eq) deriving @@ -171,21 +179,26 @@ data ImpliesResult = ImpliesResult data SimplifyResult = SimplifyResult { state :: KoreJson , logs :: Maybe [LogEntry] + , haskellLogEntries :: Maybe [LogLine] } deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab]] SimplifyResult -data AddModuleResult = AddModuleResult {_module :: !Text} +data AddModuleResult = AddModuleResult + { _module :: !Text + , haskellLogEntries :: Maybe [LogLine] + } deriving stock (Generic, Show, Eq) deriving (FromJSON, ToJSON) - via CustomJSON '[FieldLabelModifier '[StripPrefix "_"]] AddModuleResult + via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab, StripPrefix "_"]] AddModuleResult data GetModelResult = GetModelResult { satisfiable :: SatResult , substitution :: Maybe KoreJson + , haskellLogEntries :: Maybe [LogLine] } deriving stock (Generic, Show, Eq) deriving diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs index 7d382a5261..777de7789f 100644 --- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs +++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs @@ -167,6 +167,34 @@ instance FromJSON CLContext where other -> JSON.typeMismatch "Object or string" other +{- | The capture-selector name of a context: the constructor name with the +@Ctx@ prefix dropped, ignoring any 'UniqueId' / name payload. Per-request +@haskell-logging@ matches requested context names (e.g. @"Proxy"@, +@"Rewrite"@) against the names of the contexts in a message's stack; for the +id-carrying contexts ('CtxRewrite', 'CtxFunction', etc.) this is a tag-only match +(the requested @"Rewrite"@ matches any @CtxRewrite _@). These are the CamelCase +constructor names (not the kebab-case JSON tags), which is the form downstream +sends. +-} +clContextName :: CLContext -> Text +clContextName (CLNullary c) = Text.pack . drop 3 . show $ toConstr c +clContextName (CLWithId c) = idContextName c + +{- | Tag name (constructor minus @Ctx@) of an 'IdContext', discarding its +'UniqueId' / 'Text' payload. 'IdContext' does not derive 'Data', so this is +written out explicitly; the wildcard matches keep it total. +-} +idContextName :: IdContext -> Text +idContextName = \case + CtxRewrite{} -> "Rewrite" + CtxSimplification{} -> "Simplification" + CtxFunction{} -> "Function" + CtxCeil{} -> "Ceil" + CtxTerm{} -> "Term" + CtxHook{} -> "Hook" + CtxRequest{} -> "Request" + CtxCached{} -> "Cached" + ---------------------------------------- data CLMessage = CLText Text -- generic log message diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/LogCapture.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/LogCapture.hs new file mode 100644 index 0000000000..33adfc32e0 --- /dev/null +++ b/kore-rpc-types/src/Kore/JsonRpc/Types/LogCapture.hs @@ -0,0 +1,54 @@ +{- | +Copyright : (c) Runtime Verification, 2026 +License : BSD-3-Clause + +Per-request log capture for the `haskell-logging` JSON-RPC flag. + +A 'Collector' is a thread-safe buffer of 'LogLine's, one per matching +log entry. The booster-side and kore-side log paths each carry their +own predicate and build a 'LogLine' (defined in 'ContextLog', the same +structured type the context log uses); both write into the same +'Collector', so the proxy can drain a single buffer at response time +and attach the entries to the response's @haskell-log-entries@ field. + +The buffer is unbounded: the design requires lossless capture for any +request that opts in. Memory growth is proportional to the volume of +matched entries during a single request and is released when the +'Collector' is dropped at response time. +-} +module Kore.JsonRpc.Types.LogCapture ( + Collector, + newCollector, + appendCollector, + drainCollector, +) where + +import Control.Concurrent.STM (TVar, atomically, modifyTVar', newTVarIO, readTVar, writeTVar) +import Data.Foldable (toList) +import Data.Sequence (Seq, (|>)) +import Data.Sequence qualified as Seq + +import Kore.JsonRpc.Types.ContextLog (LogLine) + +{- | A per-request buffer for captured log entries, each built as a +structured 'LogLine' by the engine-specific capture path. +-} +newtype Collector = Collector (TVar (Seq LogLine)) + +newCollector :: IO Collector +newCollector = Collector <$> newTVarIO Seq.empty + +{- | Append a single captured entry to the buffer. Non-blocking; safe to +call concurrently from any thread. +-} +appendCollector :: Collector -> LogLine -> IO () +appendCollector (Collector tv) l = atomically $ modifyTVar' tv (|> l) + +{- | Drain the buffer and reset it to empty. Returns entries in +insertion order. +-} +drainCollector :: Collector -> IO [LogLine] +drainCollector (Collector tv) = atomically $ do + s <- readTVar tv + writeTVar tv Seq.empty + pure (toList s) diff --git a/kore/kore.cabal b/kore/kore.cabal index 45d3f06813..51e2194029 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -366,6 +366,7 @@ library Kore.Log.ErrorRewriteLoop Kore.Log.ErrorRewritesInstantiation Kore.Log.ErrorVerify + Kore.Log.LogCapture Kore.Log.DebugAttemptUnification Kore.Log.DebugContext Kore.Log.JsonRpc diff --git a/kore/src/Kore/JsonRpc.hs b/kore/src/Kore/JsonRpc.hs index 18845b9a06..a568cd8e52 100644 --- a/kore/src/Kore/JsonRpc.hs +++ b/kore/src/Kore/JsonRpc.hs @@ -231,6 +231,7 @@ respond reqId serverState moduleName runSMT = , nextStates = Nothing , logs = mkLogs rules , unknownPredicate = Nothing + , haskellLogEntries = Nothing } GraphTraversal.GotStuck _n @@ -247,6 +248,7 @@ respond reqId serverState moduleName runSMT = , nextStates = Nothing , logs = mkLogs rules , unknownPredicate = Nothing + , haskellLogEntries = Nothing } GraphTraversal.GotStuck _n @@ -263,6 +265,7 @@ respond reqId serverState moduleName runSMT = , nextStates = Nothing , logs = mkLogs rules , unknownPredicate = Nothing + , haskellLogEntries = Nothing } GraphTraversal.Stopped [Exec.RpcExecState{rpcDepth = ExecDepth depth, rpcProgState, rpcRules = rules}] @@ -279,6 +282,7 @@ respond reqId serverState moduleName runSMT = Just $ map (patternToExecState False sort . Exec.rpcProgState) nexts , logs = mkLogs rules , unknownPredicate = Nothing + , haskellLogEntries = Nothing } | Just rule <- containsLabelOrRuleId rules terminalRules -> Right $ @@ -291,6 +295,7 @@ respond reqId serverState moduleName runSMT = , nextStates = Nothing , logs = mkLogs rules , unknownPredicate = Nothing + , haskellLogEntries = Nothing } | otherwise -> Right $ @@ -304,6 +309,7 @@ respond reqId serverState moduleName runSMT = Just $ map (patternToExecState True sort . Exec.rpcProgState) nexts , logs = mkLogs rules , unknownPredicate = Nothing + , haskellLogEntries = Nothing } GraphTraversal.TimedOut Exec.RpcExecState{rpcDepth = ExecDepth depth, rpcProgState, rpcRules = rules} @@ -318,6 +324,7 @@ respond reqId serverState moduleName runSMT = , nextStates = Nothing , logs = mkLogs rules , unknownPredicate = Nothing + , haskellLogEntries = Nothing } -- these are programmer errors result@GraphTraversal.Aborted{} -> @@ -463,16 +470,16 @@ respond reqId serverState moduleName runSMT = in Right . Implies $ case r of Claim.Implied Nothing -> - ImpliesResult jsonTerm True (Just . renderCond sort $ Condition.bottom) logs + ImpliesResult jsonTerm True (Just . renderCond sort $ Condition.bottom) logs Nothing Claim.Implied (Just cond) -> - ImpliesResult jsonTerm True (Just . renderCond sort $ cond) logs + ImpliesResult jsonTerm True (Just . renderCond sort $ cond) logs Nothing Claim.NotImplied _ -> - ImpliesResult jsonTerm False Nothing logs + ImpliesResult jsonTerm False Nothing logs Nothing Claim.NotImpliedStuck (Just cond) -> let jsonCond = renderCond sort cond - in ImpliesResult jsonTerm False (Just jsonCond) logs + in ImpliesResult jsonTerm False (Just jsonCond) logs Nothing Claim.NotImpliedStuck Nothing -> - ImpliesResult jsonTerm False (Just . renderCond sort $ Condition.bottom) logs + ImpliesResult jsonTerm False (Just . renderCond sort $ Condition.bottom) logs Nothing Simplify SimplifyRequest{state, _module} -> withMainModule (coerce _module) $ \serializedModule lemmas -> do case verifyIn serializedModule state of Left Error{errorError, errorContext} -> @@ -505,6 +512,7 @@ respond reqId serverState moduleName runSMT = TermLike.mapVariables getRewritingVariable $ OrPattern.toTermLike sort result , logs = allLogs + , haskellLogEntries = Nothing } AddModule AddModuleRequest{_module, nameAsId = nameAsId'} -> runExceptT $ do let nameAsId = fromMaybe False nameAsId' @@ -557,7 +565,8 @@ respond reqId serverState moduleName runSMT = } else -- the module already exists so we don't need to add it again st - pure . AddModule $ AddModuleResult (getModuleName moduleHash) + pure . AddModule $ + AddModuleResult{_module = getModuleName moduleHash, haskellLogEntries = Nothing} _ -> do (newIndexedModules, newDefinedNames) <- withExceptT @@ -612,7 +621,8 @@ respond reqId serverState moduleName runSMT = Map.insert (coerce moduleHash) _module receivedModules } - pure . AddModule $ AddModuleResult (getModuleName moduleHash) + pure . AddModule $ + AddModuleResult{_module = getModuleName moduleHash, haskellLogEntries = Nothing} GetModel GetModelRequest{state, _module} -> withMainModule (coerce _module) $ \serializedModule lemmas -> case verifyIn serializedModule state of @@ -648,11 +658,13 @@ respond reqId serverState moduleName runSMT = GetModelResult { satisfiable = Unknown , substitution = Nothing + , haskellLogEntries = Nothing } Left True -> GetModelResult { satisfiable = Unsat , substitution = Nothing + , haskellLogEntries = Nothing } Right subst -> GetModelResult @@ -660,6 +672,7 @@ respond reqId serverState moduleName runSMT = , substitution = PatternJson.fromSubstitution sort $ Substitution.mapVariables getRewritingVariable subst + , haskellLogEntries = Nothing } -- this case is only reachable if the cancel appeared as part of a batch request diff --git a/kore/src/Kore/Log/BoosterAdaptor.hs b/kore/src/Kore/Log/BoosterAdaptor.hs index 0c6019a730..cfcdd34a31 100644 --- a/kore/src/Kore/Log/BoosterAdaptor.hs +++ b/kore/src/Kore/Log/BoosterAdaptor.hs @@ -6,6 +6,7 @@ module Kore.Log.BoosterAdaptor ( renderStandardPretty, renderOnelinePretty, renderJson, + entryToJsonValue, koreSomeEntryLogAction, withLogger, WithTimestamp (..), @@ -77,15 +78,21 @@ koreSomeEntryLogAction renderer earlyFilter logger = \mTime -> renderer mTime se <> "\n" renderJson :: Maybe ByteString -> SomeEntry -> LogStr -renderJson mTime e@(SomeEntry context actualEntry) = - toLogStr . Text.decodeUtf8 . BSL.toStrict . JSON.encodePretty' rpcJsonConfig{confIndent = Spaces 0} $ - json - where - jsonContext = - Vec.fromList $ - concatMap (\(SomeEntry _ c) -> map JSON.toJSON (oneLineContextDoc c)) (context <> [e]) +renderJson mTime = + toLogStr + . Text.decodeUtf8 + . BSL.toStrict + . JSON.encodePretty' rpcJsonConfig{confIndent = Spaces 0} + . entryToJsonValue mTime - json = case oneLineJson actualEntry of +{- | Build the JSON 'Value' for a 'SomeEntry' in the same shape that +'renderJson' would serialize to stderr/file (modulo whitespace). +Shared so per-request log capture writes byte-for-byte equivalent +entries. +-} +entryToJsonValue :: Maybe ByteString -> SomeEntry -> JSON.Value +entryToJsonValue mTime e@(SomeEntry context actualEntry) = + case oneLineJson actualEntry of JSON.Object o | Just (JSON.Array ctxt) <- JSON.lookup "context" o -> JSON.Object @@ -102,6 +109,10 @@ renderJson mTime e@(SomeEntry context actualEntry) = <> case mTime of Nothing -> [] Just time -> ["timestamp" JSON..= Text.decodeUtf8 time] + where + jsonContext = + Vec.fromList $ + concatMap (\(SomeEntry _ c) -> map JSON.toJSON (oneLineContextDoc c)) (context <> [e]) renderOnelinePretty :: Maybe ByteString -> SomeEntry -> LogStr renderOnelinePretty mTime entry@(SomeEntry entryContext _actualEntry) = diff --git a/kore/src/Kore/Log/LogCapture.hs b/kore/src/Kore/Log/LogCapture.hs new file mode 100644 index 0000000000..d6dc48dea7 --- /dev/null +++ b/kore/src/Kore/Log/LogCapture.hs @@ -0,0 +1,115 @@ +{- | +Copyright : (c) Runtime Verification, 2026 +License : BSD-3-Clause + +Kore-side per-request log capture for the @haskell-logging@ JSON-RPC +flag. + +A request carries the list of entry-type names to capture. The proxy +turns the names this engine recognises into a 'Set' 'SomeTypeRep' (via +'koreTypesFromNames') and registers it, together with a 'Collector', +against the request's thread for the duration of the request. +'registryLogAction' — installed once at server startup, outside the +@-l@/@--log-entries@ filter — then fans every matching entry into that +collector. Because it sits outside the CLI filter, capture is +independent of server-startup verbosity: the requested entries are +captured whether or not the server was started with @-l@ for them. +-} +module Kore.Log.LogCapture ( + KoreCaptureRegistry, + newKoreCaptureRegistry, + koreTypesFromNames, + registryLogAction, + withKoreCapture, +) where + +import Control.Concurrent (ThreadId, myThreadId) +import Control.Concurrent.STM (TVar, atomically, modifyTVar', newTVarIO, readTVarIO) +import Control.Exception (bracket_) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Text (Text) +import Prelude.Kore +import Type.Reflection (SomeTypeRep) + +import Data.Aeson (Result (..), fromJSON) + +import Kore.JsonRpc.Types.ContextLog (CLMessage (..), LogLine (..)) +import Kore.JsonRpc.Types.LogCapture (Collector, appendCollector) +import Kore.Log.BoosterAdaptor (entryToJsonValue) +import Kore.Log.Registry (registry, textToType, typeOfSomeEntry) +import Log (LogAction (..), SomeEntry) + +{- | Resolve requested entry-type names to the kore 'SomeTypeRep's the +capture should match. Names not in the log registry — booster context +tags, or entries this backend version does not know — are skipped, so a +client can request a superset spanning both engines (and across backend +versions) without failing the request. +-} +koreTypesFromNames :: [Text] -> Set SomeTypeRep +koreTypesFromNames names = + Set.fromList $ mapMaybe (`Map.lookup` textToType registry) names + +---------------------------------------------------------------------- +-- Per-request capture registry, keyed by the OS thread that owns the +-- request. The proxy's main log action is augmented once at server +-- startup with 'registryLogAction'; each request that opts in +-- registers its own 'Collector' (and the set of entry types it wants) +-- against its 'ThreadId' so concurrent requests do not see each +-- other's logs. +---------------------------------------------------------------------- + +newtype KoreCaptureRegistry = KoreCaptureRegistry (TVar (Map ThreadId (Collector, Set SomeTypeRep))) + +newKoreCaptureRegistry :: IO KoreCaptureRegistry +newKoreCaptureRegistry = KoreCaptureRegistry <$> newTVarIO Map.empty + +{- | A 'LogAction' that dispatches matching kore entries to whichever +'Collector' is registered for the calling thread, if any, filtered by +that request's requested entry-type set. Combined with the static kore +log action via 'mconcat' so capture is purely additive. +-} +registryLogAction :: MonadIO m => KoreCaptureRegistry -> LogAction m SomeEntry +registryLogAction (KoreCaptureRegistry tv) = + LogAction $ \entry -> liftIO $ do + -- Runs for every kore entry (it is composed outside the -l filter). + -- Most requests register nothing, so the thread lookup short-circuits. + tid <- myThreadId + m <- readTVarIO tv + case Map.lookup tid m of + Nothing -> pure () + Just (c, types) + | typeOfSomeEntry entry `Set.member` types -> + appendCollector c (entryToLogLine entry) + | otherwise -> pure () + +{- | Convert a kore 'SomeEntry' to a structured 'LogLine'. We reuse +'entryToJsonValue' — the very renderer the JSON file logger uses, so a +captured entry is identical to its on-disk form — and parse its output +back into 'LogLine' (kore's context vocabulary is the same 'CLContext' +the context log models). Should that parse ever fail, fall back to a +context-less line carrying the raw value, so capture is total. +-} +entryToLogLine :: SomeEntry -> LogLine +entryToLogLine entry = + let value = entryToJsonValue Nothing entry + in case fromJSON value of + Success logLine -> logLine + Error _ -> LogLine{timestamp = Nothing, context = mempty, message = CLValue value} + +{- | Register a collector and its requested entry-type set against the +current thread for the duration of the inner action. Existing +registrations on the same thread (rare but possible if a request is +re-entered) are restored on exit. When the argument is 'Nothing' the +inner action runs unchanged. +-} +withKoreCapture :: KoreCaptureRegistry -> Maybe (Collector, Set SomeTypeRep) -> IO a -> IO a +withKoreCapture _ Nothing action = action +withKoreCapture (KoreCaptureRegistry tv) (Just entry) action = do + tid <- myThreadId + bracket_ + (atomically $ modifyTVar' tv (Map.insert tid entry)) + (atomically $ modifyTVar' tv (Map.delete tid)) + action diff --git a/scripts/booster-integration-tests.sh b/scripts/booster-integration-tests.sh index 331d478703..7cae5fe783 100755 --- a/scripts/booster-integration-tests.sh +++ b/scripts/booster-integration-tests.sh @@ -62,6 +62,10 @@ for dir in $(ls -d test-*); do "imp") SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name --time $@ ;; + "haskell-log-capture") + # per-request log capture is a proxy feature, so only kore-rpc-booster + SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@ + ;; *) SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@ ;;