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 <[email protected]>
runtimeverification · Jun 25, 2024 · 59a999a · 59a999a
1 parent 47f2ac8
commit 59a999a
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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