From 59a999a92babd83e0f856cbd7feef907cbfd3b8c Mon Sep 17 00:00:00 2001
From: Georgy Lukyanov <mail@geo2a.info>
Date: Tue, 25 Jun 2024 10:14:17 +0200
Subject: [PATCH] More precise `[llvm]`/`[cached *]` log context (#3957)

We emit a log message upon getting the result of an LLVM backend call,
but we do not have a message that would give us the precise term we
send. This PR fixes that.

---------

Co-authored-by: Samuel Balco <goodlyrottenapple@gmail.com>
---
 booster/library/Booster/Log.hs                   |  1 +
 .../library/Booster/Pattern/ApplyEquations.hs    | 16 +++++++++++-----
 .../src/Kore/JsonRpc/Types/ContextLog.hs         |  3 ++-
 3 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs
index 93f03c8758..45443af0e4 100644
--- a/booster/library/Booster/Log.hs
+++ b/booster/library/Booster/Log.hs
@@ -19,6 +19,7 @@ module Booster.Log (
     jsonLogger,
     textLogger,
     withContext,
+    withContext_,
     withContexts,
     withKorePatternContext,
     withPatternContext,
diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
index 367bf8e26f..9a001d2196 100644
--- a/booster/library/Booster/Pattern/ApplyEquations.hs
+++ b/booster/library/Booster/Pattern/ApplyEquations.hs
@@ -67,6 +67,7 @@ import Booster.Prettyprinter (renderOneLineText)
 import Booster.SMT.Interface qualified as SMT
 import Booster.Syntax.Json.Externalise (externaliseTerm)
 import Booster.Util (Bound (..))
+import Kore.JsonRpc.Types.ContextLog (CLContext (CLWithId), IdContext (CtxCached))
 import Kore.Util (showHashHex)
 
 newtype EquationT io a
@@ -165,6 +166,10 @@ instance Monoid SimplifierCache where
 data CacheTag = LLVM | Equations
     deriving stock (Show)
 
+instance ContextFor CacheTag where
+    withContextFor t =
+        withContext_ (CLWithId . CtxCached $ Text.toLower $ Text.pack $ show t)
+
 data EquationMetadata = EquationMetadata
     { location :: Maybe Location
     , label :: Maybe Label
@@ -351,7 +356,7 @@ llvmSimplify term = do
   where
     evalLlvm definition api cb t@(Term attributes _)
         | attributes.isEvaluated = pure t
-        | isConcrete t && attributes.canBeEvaluated = withContext CtxLlvm $ do
+        | isConcrete t && attributes.canBeEvaluated = withContext CtxLlvm . withTermContext t $ do
             LLVM.simplifyTerm api definition t (sortOfTerm t)
                 >>= \case
                     Left (LlvmError e) -> do
@@ -531,10 +536,11 @@ cached cacheTag cb t@(Term attributes _)
             Just cachedTerm -> do
                 when (t /= cachedTerm) $ do
                     setChanged
-                    withContext CtxSuccess $
-                        withContext CtxCached $
-                            withTermContext cachedTerm $
-                                pure ()
+                    withTermContext t $
+                        withContext CtxSuccess $
+                            withContextFor cacheTag $
+                                withTermContext cachedTerm $
+                                    pure ()
                 pure cachedTerm
 
 elseApply :: (Monad m, Eq b) => (b -> m b) -> (b -> m b) -> b -> m b
diff --git a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
index 663479e276..86a76839f5 100644
--- a/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
+++ b/kore-rpc-types/src/Kore/JsonRpc/Types/ContextLog.hs
@@ -34,7 +34,6 @@ data SimpleContext
     | CtxConstraint
     | CtxSMT
     | CtxLlvm
-    | CtxCached
     | -- results
       CtxFailure
     | CtxIndeterminate
@@ -76,6 +75,7 @@ data IdContext
     | -- entities with name
       CtxHook Text
     | CtxRequest Text
+    | CtxCached Text
     deriving stock (Eq, Ord)
 
 instance Show IdContext where
@@ -86,6 +86,7 @@ instance Show IdContext where
     show (CtxTerm uid) = "term " <> show uid
     show (CtxHook name) = "hook " <> unpack name
     show (CtxRequest name) = "request " <> unpack name
+    show (CtxCached name) = "cached " <> unpack name
 
 getUniqueId :: IdContext -> Maybe UniqueId
 getUniqueId = \case