Booster interim simplification, refactor rewrite and logging parameters (#4010)

* adds option `--simplify-each DEPTH` which runs a booster-only
simplification every `DEPTH` steps
* refactors logging-related options into a dedicated `LogOptions` type
* refactors `performRewrite` and `runRewriteT` to use a pre-made
`RewriteConfig` (extended by parameters required only in
`performRewrite`

---------

Co-authored-by: github-actions <[email protected]>

Author: jberthold

booster/library/Booster/CLOptions.hs

@@ -7,6 +7,8 @@ module Booster.CLOptions (
     CLOptions (..),
     EquationOptions (..),
     LogFormat (..),
+    LogOptions (..),
+    RewriteOptions (..),
     TimestampFormat (..),
     clOptionsParser,
     adjustLogLevels,
@@ -25,6 +27,7 @@ import Data.Maybe (fromMaybe)
 import Data.Text (Text, pack)
 import Data.Text.Encoding (decodeASCII)
 import Data.Version (Version (..), showVersion)
+import Numeric.Natural (Natural)
 import Options.Applicative
 
 import Booster.GlobalState (EquationOptions (..))
@@ -41,18 +44,23 @@ data CLOptions = CLOptions
     , mainModuleName :: Text
     , llvmLibraryFile :: Maybe FilePath
     , port :: Int
-    , logLevels :: [LogLevel]
+    , logOptions :: LogOptions
+    , smtOptions :: Maybe SMTOptions
+    , equationOptions :: EquationOptions
+    , rewriteOptions :: RewriteOptions
+    }
+    deriving stock (Show)
+
+data LogOptions = LogOptions
+    { logLevels :: [LogLevel]
     , logTimeStamps :: Bool
     , timeStampsFormat :: TimestampFormat
     , logFormat :: LogFormat
     , logContexts :: [ContextFilter]
     , logFile :: Maybe FilePath
-    , smtOptions :: Maybe SMTOptions
-    , equationOptions :: EquationOptions
-    , indexCells :: [Text]
     , prettyPrintOptions :: [ModifierT]
     }
-    deriving (Show)
+    deriving stock (Show)
 
 data LogFormat
     = Standard
@@ -76,6 +84,12 @@ instance Show TimestampFormat where
         Pretty -> "pretty"
         Nanoseconds -> "nanoseconds"
 
+data RewriteOptions = RewriteOptions
+    { indexCells :: [Text]
+    , interimSimplification :: Maybe Natural
+    }
+    deriving stock (Show, Eq)
+
 clOptionsParser :: Parser CLOptions
 clOptionsParser =
     CLOptions
@@ -103,7 +117,15 @@ clOptionsParser =
                 <> help "Port for the RPC server to bind to"
                 <> showDefault
             )
-        <*> many
+        <*> parseLogOptions
+        <*> parseSMTOptions
+        <*> parseEquationOptions
+        <*> parseRewriteOptions
+
+parseLogOptions :: Parser LogOptions
+parseLogOptions =
+    LogOptions
+        <$> many
             ( option
                 (eitherReader readLogLevel)
                 ( metavar "LEVEL"
@@ -154,15 +176,6 @@ clOptionsParser =
                         "Log file to output the logs into"
                 )
             )
-        <*> parseSMTOptions
-        <*> parseEquationOptions
-        <*> option
-            (eitherReader $ mapM (readCellName . trim) . splitOn ",")
-            ( metavar "CELL-NAME[,CELL-NAME]"
-                <> long "index-cells"
-                <> help "Names of configuration cells to index rewrite rules with (default: 'k')"
-                <> value []
-            )
         <*> option
             (eitherReader $ mapM (readModifierT . trim) . splitOn ",")
             ( metavar "PRETTY_PRINT"
@@ -202,18 +215,6 @@ clOptionsParser =
         "nanoseconds" -> Right Nanoseconds
         other -> Left $ other <> ": Unsupported timestamp format"
 
-    readCellName :: String -> Either String Text
-    readCellName input
-        | null input =
-            Left "Empty cell name"
-        | all isAscii input
-        , all isPrint input =
-            Right $ "Lbl'-LT-'" <> enquote input <> "'-GT-'"
-        | otherwise =
-            Left $ "Illegal non-ascii characters in `" <> input <> "'"
-
-    enquote = decodeASCII . encodeLabel . BS.pack
-
 -- custom log levels that can be selected
 allowedLogLevels :: [(String, String)]
 allowedLogLevels =
@@ -364,13 +365,6 @@ parseSMTOptions =
   where
     smtDefaults = defaultSMTOptions
 
-    nonnegativeInt :: ReadM Int
-    nonnegativeInt =
-        auto >>= \case
-            i
-                | i < 0 -> readerError "must be a non-negative integer."
-                | otherwise -> pure i
-
     readTactic =
         either (readerError . ("Invalid s-expression. " <>)) pure . SMT.parseSExpr . BS.pack =<< str
 
@@ -397,12 +391,46 @@ parseEquationOptions =
     defaultMaxIterations = 100
     defaultMaxRecursion = 5
 
-    nonnegativeInt :: ReadM Int
-    nonnegativeInt =
-        auto >>= \case
-            i
-                | i < 0 -> readerError "must be a non-negative integer."
-                | otherwise -> pure i
+parseRewriteOptions :: Parser RewriteOptions
+parseRewriteOptions =
+    RewriteOptions
+        <$> option
+            (eitherReader $ mapM (readCellName . trim) . splitOn ",")
+            ( metavar "CELL-NAME[,CELL-NAME]"
+                <> long "index-cells"
+                <> help "Names of configuration cells to index rewrite rules with (default: 'k')"
+                <> value []
+            )
+        <*> optional
+            ( option
+                (intWith (> 0))
+                ( metavar "DEPTH"
+                    <> long "simplify-each"
+                    <> help "If given: Simplify the term each time the given rewrite depth is reached"
+                )
+            )
+  where
+    readCellName :: String -> Either String Text
+    readCellName input
+        | null input =
+            Left "Empty cell name"
+        | all isAscii input
+        , all isPrint input =
+            Right $ "Lbl'-LT-'" <> enquote input <> "'-GT-'"
+        | otherwise =
+            Left $ "Illegal non-ascii characters in `" <> input <> "'"
+
+    enquote = decodeASCII . encodeLabel . BS.pack
+
+intWith :: Integral i => (Integer -> Bool) -> ReadM i
+intWith p =
+    auto >>= \case
+        i
+            | not (p i) -> readerError $ show i <> ": Invalid integer value."
+            | otherwise -> pure (fromIntegral i)
+
+nonnegativeInt :: Integral i => ReadM i
+nonnegativeInt = intWith (>= 0)
 
 versionInfoParser :: Parser (a -> a)
 versionInfoParser =

booster/library/Booster/JsonRpc.hs

@@ -41,6 +41,7 @@ import Numeric.Natural
 import Prettyprinter (comma, hsep, punctuate, (<+>))
 import System.Clock (Clock (Monotonic), diffTimeSpec, getTime, toNanoSecs)
 
+import Booster.CLOptions (RewriteOptions (..))
 import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId)
 import Booster.Definition.Base (KoreDefinition (..))
 import Booster.Definition.Base qualified as Definition (RewriteRule (..))
@@ -53,6 +54,7 @@ import Booster.Pattern.Bool (pattern TrueBool)
 import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (..), matchTerms)
 import Booster.Pattern.Pretty
 import Booster.Pattern.Rewrite (
+    RewriteConfig (..),
     RewriteFailed (..),
     RewriteResult (..),
     RewriteTrace (..),
@@ -108,7 +110,7 @@ respond stateVar request =
                 | 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 CtxExecute $ do
+            RpcTypes.Execute req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions, rewriteOpts) -> Booster.Log.withContext CtxExecute $ do
                 start <- liftIO $ getTime Monotonic
                 -- internalise given constrained term
                 let internalised = runExcept $ internalisePattern DisallowAlias CheckSubsorts Nothing def req.state.term
@@ -152,8 +154,25 @@ respond stateVar request =
                                     ]
 
                         solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
+
+                        logger <- getLogger
+                        prettyModifiers <- getPrettyModifiers
+                        let rewriteConfig =
+                                RewriteConfig
+                                    { definition = def
+                                    , llvmApi = mLlvmLibrary
+                                    , smtSolver = solver
+                                    , varsToAvoid = substVars
+                                    , doTracing
+                                    , logger
+                                    , prettyModifiers
+                                    , mbMaxDepth = mbDepth
+                                    , mbSimplify = rewriteOpts.interimSimplification
+                                    , cutLabels = cutPoints
+                                    , terminalLabels = terminals
+                                    }
                         result <-
-                            performRewrite doTracing def mLlvmLibrary solver substVars mbDepth cutPoints terminals substPat
+                            performRewrite rewriteConfig substPat
                         SMT.finaliseSolver solver
                         stop <- liftIO $ getTime Monotonic
                         let duration =
@@ -224,7 +243,7 @@ respond stateVar request =
                     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 CtxSimplify $ 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
@@ -315,11 +334,11 @@ respond stateVar request =
                             RpcTypes.SimplifyResult{state, logs = mkTraces duration}
                 pure $ second mkSimplifyResponse result
             RpcTypes.GetModel req -> withModule req._module $ \case
-                (_, _, Nothing) -> do
+                (_, _, Nothing, _) -> do
                     withContext CtxGetModel $
                         logMessage' ("get-model request, not supported without SMT solver" :: Text)
                     pure $ Left RpcError.notImplemented
-                (def, _, Just smtOptions) -> do
+                (def, _, Just smtOptions, _) -> do
                     let internalised =
                             runExcept $
                                 internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term
@@ -419,7 +438,7 @@ respond stateVar request =
                                             { satisfiable = RpcTypes.Sat
                                             , substitution
                                             }
-            RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext CtxImplies $ 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
@@ -504,7 +523,7 @@ respond stateVar request =
   where
     withModule ::
         Maybe Text ->
-        ( (KoreDefinition, Maybe LLVM.API, Maybe SMT.SMTOptions) ->
+        ( (KoreDefinition, Maybe LLVM.API, Maybe SMT.SMTOptions, RewriteOptions) ->
           m (Either ErrorObj (RpcTypes.API 'RpcTypes.Res))
         ) ->
         m (Either ErrorObj (RpcTypes.API 'RpcTypes.Res))
@@ -513,7 +532,7 @@ respond stateVar request =
         let mainName = fromMaybe state.defaultMain mbMainModule
         case Map.lookup mainName state.definitions of
             Nothing -> pure $ Left $ RpcError.backendError $ RpcError.CouldNotFindModule mainName
-            Just d -> action (d, state.mLlvmLibrary, state.mSMTOptions)
+            Just d -> action (d, state.mLlvmLibrary, state.mSMTOptions, state.rewriteOptions)
 
     doesNotImply s l r =
         pure $
@@ -571,9 +590,11 @@ data ServerState = ServerState
     , defaultMain :: Text
     -- ^ default main module (initially from command line, could be changed later)
     , mLlvmLibrary :: Maybe LLVM.API
-    -- ^ optional LLVM simplification library
+    -- ^ Read-only: optional LLVM simplification library
     , mSMTOptions :: Maybe SMT.SMTOptions
-    -- ^ (optional) SMT solver options
+    -- ^ Read-only: (optional) SMT solver options
+    , rewriteOptions :: RewriteOptions
+    -- ^ Read-only: configuration related to booster rewriting
     , addedModules :: Map Text Text
     -- ^ map of raw modules added via add-module
     }