Merge remote-tracking branch 'origin/master' into georgy/booster-rema…

…inders
runtimeverification · Aug 6, 2024 · a580cfc · a580cfc
2 parents 70817d4 + def3190
commit a580cfc
Show file tree

Hide file tree

Showing 92 changed files with 98,968 additions and 1,951 deletions.
diff --git a/booster/library/Booster/CLOptions.hs b/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 =

diff --git a/booster/library/Booster/Definition/Ceil.hs b/booster/library/Booster/Definition/Ceil.hs
@@ -18,6 +18,7 @@ import Booster.Log
 import Booster.Pattern.Bool
 import Booster.Pattern.Pretty
 import Booster.Pattern.Util (isConcrete, sortOfTerm)
+import Booster.SMT.Interface
 import Booster.Util (Flag (..))
 import Control.DeepSeq (NFData)
 import Control.Monad (foldM)
@@ -101,7 +102,8 @@ computeCeilRule ::
 computeCeilRule mllvm def r@RewriteRule.RewriteRule{lhs, requires, rhs, attributes, computedAttributes}
     | null computedAttributes.notPreservesDefinednessReasons = pure Nothing
     | otherwise = do
-        (res, _) <- runEquationT def mllvm Nothing mempty mempty $ do
+        ns <- noSolver
+        (res, _) <- runEquationT def mllvm ns mempty mempty $ do
             lhsCeils <- Set.fromList <$> computeCeil lhs
             requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) (Set.toList requires)
             let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList