Merge remote-tracking branch 'origin/master' into 3813-map-update-hook-and-hook-refactoring

Author: jberthold

.github/workflows/test.yml

@@ -201,10 +201,6 @@ jobs:
             cabal-nix-${{ runner.os }}-ghc-${{ env.ghc_version }}-${{ hashFiles('cabal.project') }}
             cabal-nix-${{ runner.os }}-ghc-${{ env.ghc_version }}
 
-      - name: Run unit tests
-        if: ${{ steps.changes.outputs.booster == 'true' || steps.changes.outputs.kore == 'true' || steps.changes.outputs.project == 'true' }}
-        run: GC_DONT_GC=1 nix develop .#cabal --command bash -c "cabal update && cabal build all && cabal test --enable-tests --test-show-details=direct kore-test unit-tests"
-
       - name: Run booster integration tests
         if: ${{ (steps.changes.outputs.booster == 'true' || steps.changes.outputs.kore_rpc_types == 'true' || steps.changes.outputs.project == 'true') }}
         run: |

booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden

@@ -25,7 +25,7 @@ import Data.Bifunctor (second)
 import Data.Either (partitionEithers)
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Map qualified as Map
-import Data.Maybe (catMaybes, fromJust, fromMaybe, isJust, isNothing, mapMaybe)
+import Data.Maybe (catMaybes, fromMaybe, isJust, isNothing, mapMaybe)
 import Data.Text (Text)
 import Data.Text qualified as Text
 import Data.Text.Lazy (toStrict)
@@ -42,7 +42,6 @@ import Kore.Internal.TermLike (TermLike, VariableName)
 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 ImpliesRequest (ImpliesRequest (..))
 import Kore.JsonRpc.Types qualified as SimplifyRequest (SimplifyRequest (..))
 import Kore.JsonRpc.Types.Log qualified as RPCLog
 import Kore.Log qualified
@@ -69,6 +68,7 @@ data ProxyConfig = ProxyConfig
     , boosterState :: MVar.MVar Booster.ServerState
     , fallbackReasons :: [HaltReason]
     , simplifyAtEnd :: Bool
+    , simplifyBeforeFallback :: Bool
     , customLogLevels :: ![Log.LogLevel]
     }
 
@@ -105,26 +105,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                 Map.lookup m bState.definitions
                     handleExecute logSettings def start execReq
     Implies impliesReq -> do
-        koreResult <-
-            loggedKore
-                ImpliesM
-                ( Implies
-                    impliesReq
-                        { ImpliesRequest.logSuccessfulSimplifications =
-                            Just $ Log.LevelOther "SimplifyJson" `elem` cfg.customLogLevels
-                        }
-                )
-        case koreResult of
-            Right (Implies koreRes) -> do
-                -- Kore may have produced simplification logs during rewriting. If so,
-                -- output them Kore at "SimplifyJson" level. Erase terms from the traces.
-                when (isJust koreRes.logs) $ do
-                    outputLogsAtLevel (Log.LevelOther "SimplifyJson")
-                        . map RPCLog.logEntryEraseTerms
-                        . fromJust
-                        $ koreRes.logs
-            _ -> pure ()
-        pure koreResult
+        loggedKore ImpliesM (Implies impliesReq)
     Simplify simplifyReq ->
         liftIO (getTime Monotonic) >>= handleSimplify simplifyReq . Just
     AddModule _ -> do
@@ -175,8 +156,6 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                         Simplify
                             simplifyReq
                                 { SimplifyRequest.state = boosterRes.state
-                                , SimplifyRequest.logSuccessfulSimplifications =
-                                    Just $ Log.LevelOther "SimplifyJson" `elem` cfg.customLogLevels
                                 }
                 (koreResult, koreTime) <- Stats.timed $ kore koreReq
                 case koreResult of
@@ -194,13 +173,6 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                             diffBy def boosterRes.state.term koreRes.state.term
                                  in Text.pack ("Kore simplification: Diff (< before - > after)\n" <> diff)
                         stop <- liftIO $ getTime Monotonic
-                        -- output simplification traces returned by Kore at "SimplifyJson" level, effectively
-                        -- appending them to Booster's traces. Erase terms from the traces.
-                        when (isJust koreRes.logs) $ do
-                            outputLogsAtLevel (Log.LevelOther "SimplifyJson")
-                                . map RPCLog.logEntryEraseTerms
-                                . fromJust
-                                $ koreRes.logs
                         let timing
                                 | Just start <- mbStart
                                 , fromMaybe False simplifyReq.logTiming =
@@ -289,7 +261,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
             other -> other
 
     postProcessLogs :: [RPCLog.LogEntry] -> [RPCLog.LogEntry]
-    postProcessLogs !logs = map RPCLog.logEntryEraseTerms . filter (not . isSimplificationLogEntry) $ logs
+    postProcessLogs !logs = map RPCLog.logEntryEraseTerms logs
 
     executionLoop ::
         LogSettings ->
@@ -353,7 +325,10 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                         "Booster " <> show boosterResult.reason <> " at " <> show boosterResult.depth
                     -- simplify Booster's state with Kore's simplifier
                     Log.logInfoNS "proxy" . Text.pack $ "Simplifying booster state and falling back to Kore "
-                    simplifyResult <- simplifyExecuteState logSettings r._module def boosterResult.state
+                    simplifyResult <-
+                        if cfg.simplifyBeforeFallback
+                            then simplifyExecuteState logSettings r._module def boosterResult.state
+                            else pure $ Right (boosterResult.state, Nothing)
                     case simplifyResult of
                         Left logsOnly -> do
                             -- state was simplified to \bottom, return vacuous
@@ -369,8 +344,6 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                                 { state = execStateToKoreJson simplifiedBoosterState
                                                 , maxDepth = Just $ Depth 1
                                                 , assumeStateDefined = Just True
-                                                , ExecuteRequest.logSuccessfulSimplifications =
-                                                    Just $ Log.LevelOther "SimplifyJson" `elem` cfg.customLogLevels
                                                 }
                                         )
                             when (isJust statsVar) $ do
@@ -416,16 +389,6 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                                                 Log.logOtherNS "proxy" (Log.LevelOther "Aborts") $
                                                     "kore confirms result " <> Text.pack (show bRes)
 
-                                    -- Kore may have produced simplification logs during rewriting. If so,
-                                    -- output them Kore at "SimplifyJson" level, effectively
-                                    -- appending them to Booster's traces. Erase terms from the traces.
-                                    when (isJust koreResult.logs) $ do
-                                        outputLogsAtLevel (Log.LevelOther "SimplifyJson")
-                                            . map RPCLog.logEntryEraseTerms
-                                            . filter isSimplificationLogEntry
-                                            . fromJust
-                                            $ koreResult.logs
-
                                     case koreResult.reason of
                                         DepthBound -> do
                                             -- if we made one step, add the number of
@@ -644,15 +607,6 @@ combineLogs logSources
     | all isNothing logSources = Nothing
     | otherwise = Just $ concat $ catMaybes logSources
 
--- | Log a list of RPCLog items at a certain level
-outputLogsAtLevel :: Log.MonadLogger m => Log.LogLevel -> [RPCLog.LogEntry] -> m ()
-outputLogsAtLevel level = mapM_ (Log.logOtherNS "proxy" level . RPCLog.encodeLogEntryText)
-
-isSimplificationLogEntry :: RPCLog.LogEntry -> Bool
-isSimplificationLogEntry = \case
-    RPCLog.Simplification{} -> True
-    _ -> False
-
 makeVacuous :: Maybe [RPCLog.LogEntry] -> ExecuteResult -> ExecuteResult
 makeVacuous newLogs execState =
     execState

booster/tools/booster/Proxy.hs

@@ -24,6 +24,7 @@ import Control.Monad.Logger (
     runNoLoggingT,
  )
 import Control.Monad.Logger qualified as Logger
+import Data.ByteString qualified as BS
 import Data.Conduit.Network (serverSettings)
 import Data.IORef (writeIORef)
 import Data.InternedText (globalInternedTextCache)
@@ -33,7 +34,7 @@ import Data.Map qualified as Map
 import Data.Maybe (fromMaybe, isJust, mapMaybe)
 import Data.Set qualified as Set
 import Data.Text qualified as Text
-import Data.Text.Encoding qualified as Text (decodeUtf8)
+import Data.Text.Encoding qualified as Text (decodeUtf8, encodeUtf8)
 import Options.Applicative
 import System.Clock (
     Clock (..),
@@ -69,8 +70,9 @@ import Kore.JsonRpc.Types (API, HaltReason (..), ReqOrRes (Req, Res))
 import Kore.JsonRpc.Types.Depth (Depth (..))
 import Kore.Log (
     ExeName (..),
-    KoreLogType (LogSomeAction),
+    KoreLogType (..),
     LogAction (LogAction),
+    LogSomeActionData (..),
     TimestampsSwitch (TimestampsDisable),
     defaultKoreLogOptions,
     swappableLogger,
@@ -112,6 +114,7 @@ main = do
                     , boosterSMT
                     , fallbackReasons
                     , simplifyAtEnd
+                    , simplifyBeforeFallback
                     }
             } = options
         (logLevel, customLevels) = adjustLogLevels logLevels
@@ -123,8 +126,9 @@ main = do
         koreSolverOptions = translateSMTOpts smtOptions
 
     Booster.withLogFile simplificationLogFile $ \mLogFileHandle -> do
-        let logLevelToHandle = \case
-                Logger.LevelOther "SimplifyJson" -> fromMaybe IO.stderr mLogFileHandle
+        let simplificationLogHandle = fromMaybe IO.stderr mLogFileHandle
+            logLevelToHandle = \case
+                Logger.LevelOther "SimplifyJson" -> simplificationLogHandle
                 _ -> IO.stderr
 
         Booster.runHandleLoggingT logLevelToHandle . Logger.filterLogger levelFilter $ do
@@ -140,7 +144,16 @@ main = do
 
             monadLogger <- askLoggerIO
 
-            liftIO $ void $ withBugReport (ExeName "kore-rpc-booster") BugReportOnError $ \reportDirectory -> withMDLib llvmLibraryFile $ \mdl -> do
+            koreLogEntriesAsJsonSelector <-
+                case Map.lookup (Logger.LevelOther "SimplifyJson") logLevelToKoreLogEntryMap of
+                    Nothing -> do
+                        Logger.logWarnNS
+                            "proxy"
+                            "Could not find out which Kore log entries correspond to the SimplifyJson level"
+                        pure (const False)
+                    Just es -> pure (`elem` es)
+
+            liftIO $ void $ withBugReport (ExeName "kore-rpc-booster") BugReportOnError $ \_reportDirectory -> withMDLib llvmLibraryFile $ \mdl -> do
                 let coLogLevel = fromMaybe Log.Info $ toSeverity logLevel
                     koreLogOptions =
                         (defaultKoreLogOptions (ExeName "") startTime)
@@ -149,11 +162,29 @@ main = do
                             , Log.timestampsSwitch = TimestampsDisable
                             , Log.debugSolverOptions =
                                 Log.DebugSolverOptions . fmap (<> ".kore") $ smtOptions >>= (.transcript)
-                            , Log.logType = LogSomeAction $ LogAction $ \txt -> liftIO $ monadLogger defaultLoc "kore" logLevel $ toLogStr txt
+                            , Log.logType =
+                                LogSomeAction $
+                                    LogSomeActionData
+                                        { entrySelector = koreLogEntriesAsJsonSelector
+                                        , standardLogAction =
+                                            (LogAction $ \txt -> liftIO $ monadLogger defaultLoc "kore" logLevel $ toLogStr txt)
+                                        , jsonLogAction =
+                                            ( LogAction $ \txt ->
+                                                let bytes =
+                                                        Text.encodeUtf8 $
+                                                            if simplificationLogHandle == IO.stderr
+                                                                then "[SimplifyJson] " <> txt <> "\n"
+                                                                else txt <> "\n"
+                                                 in liftIO $ do
+                                                        BS.hPutStr simplificationLogHandle bytes
+                                                        IO.hFlush simplificationLogHandle
+                                            )
+                                        }
+                            , Log.logFormat = Log.Standard
                             }
                     srvSettings = serverSettings port "*"
 
-                withLogger reportDirectory koreLogOptions $ \actualLogAction -> do
+                withLogger koreLogOptions $ \actualLogAction -> do
                     mLlvmLibrary <- maybe (pure Nothing) (fmap Just . mkAPI) mdl
                     definitionsWithCeilSummaries <-
                         liftIO $
@@ -220,6 +251,7 @@ main = do
                                 , boosterState
                                 , fallbackReasons
                                 , simplifyAtEnd
+                                , simplifyBeforeFallback
                                 , customLogLevels = customLevels
                                 }
                         server =
@@ -259,16 +291,22 @@ toSeverity LevelOther{} = Nothing
 
 koreExtraLogs :: Map.Map LogLevel Log.EntryTypes
 koreExtraLogs =
-    Map.map (Set.fromList . mapMaybe (`Map.lookup` Log.textToType Log.registry)) $
-        Map.fromList
-            [ (LevelOther "SimplifyKore", ["DebugAttemptEquation", "DebugApplyEquation"])
-            ,
-                ( LevelOther "RewriteKore"
-                , ["DebugAttemptedRewriteRules", "DebugAppliedLabeledRewriteRule", "DebugAppliedRewriteRules"]
-                )
-            , (LevelOther "SimplifySuccess", ["DebugApplyEquation"])
-            , (LevelOther "RewriteSuccess", ["DebugAppliedRewriteRules"])
-            ]
+    Map.map
+        (Set.fromList . mapMaybe (`Map.lookup` Log.textToType Log.registry))
+        logLevelToKoreLogEntryMap
+
+logLevelToKoreLogEntryMap :: Map.Map LogLevel [Text.Text]
+logLevelToKoreLogEntryMap =
+    Map.fromList
+        [ (LevelOther "SimplifyKore", ["DebugAttemptEquation", "DebugApplyEquation"])
+        , (LevelOther "SimplifyJson", ["DebugAttemptEquation"])
+        ,
+            ( LevelOther "RewriteKore"
+            , ["DebugAttemptedRewriteRules", "DebugAppliedLabeledRewriteRule", "DebugAppliedRewriteRules"]
+            )
+        , (LevelOther "SimplifySuccess", ["DebugApplyEquation"])
+        , (LevelOther "RewriteSuccess", ["DebugAppliedRewriteRules"])
+        ]
 
 data CLProxyOptions = CLProxyOptions
     { clOptions :: CLOptions
@@ -286,6 +324,8 @@ data ProxyOptions = ProxyOptions
     -- ^ halt reasons to re-execute (fallback) to double-check the result
     , simplifyAtEnd :: Bool
     -- ^ whether to run a post-exec simplification
+    , simplifyBeforeFallback :: Bool
+    -- ^ whether to run a simplification before fall-back execute requests
     }
 
 parserInfoModifiers :: InfoMod options
@@ -334,6 +374,12 @@ clProxyOptionsParser =
                 ( long "no-post-exec-simplify"
                     <> help "disable post-exec simplification"
                 )
+            <*> flag
+                True
+                False
+                ( long "no-fallback-simplify"
+                    <> help "disable simplification before fallback requests"
+                )
 
     reasonReader :: String -> Either String HaltReason
     reasonReader = \case
@@ -368,7 +414,8 @@ translateSMTOpts = \case
     translateSExpr (SMT.Atom (SMT.SMTId x)) = KoreSMT.Atom (Text.decodeUtf8 x)
     translateSExpr (SMT.List ss) = KoreSMT.List $ map translateSExpr ss
 
-mkKoreServer :: Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer
+mkKoreServer ::
+    Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer
 mkKoreServer loggerEnv@Log.LoggerEnv{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =
     flip Log.runLoggerT logAction $ do
         sd@GlobalMain.SerializedDefinition{internedTextCache} <-