Merge branch 'main' into krypto-bytes

dev-tools/kore-rpc-dev/Server.hs

@@ -28,9 +28,11 @@ import Data.Conduit.Network (serverSettings)
 import Data.IORef (writeIORef)
 import Data.InternedText (globalInternedTextCache)
 import Data.Map qualified as Map
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, mapMaybe)
+import Data.Set qualified as Set
 import Data.Text (Text)
 import Data.Text qualified as Text
+import Data.Text.Encoding qualified as Text (decodeUtf8)
 import Network.JSONRPC
 import Options.Applicative
 import System.Clock (
@@ -41,7 +43,10 @@ import System.Exit
 import System.IO (hPutStrLn, stderr)
 
 import Booster.CLOptions
+import Booster.SMT.Base qualified as SMT (SExpr (..), SMTId (..))
+import Booster.SMT.Interface (SMTOptions (..))
 import Booster.Trace
+import Data.Limit (Limit (..))
 import GlobalMain qualified
 import Kore.Attribute.Symbol (StepperAttributes)
 import Kore.BugReport (BugReportOption (..), withBugReport)
@@ -64,10 +69,11 @@ import Kore.Log (
 import Kore.Log qualified
 import Kore.Log qualified as Log
 import Kore.Log.DebugSolver qualified as Log
+import Kore.Log.Registry qualified as Log
 import Kore.Rewrite.SMT.Lemma (declareSMTLemmas)
 import Kore.Syntax.Definition (ModuleName (ModuleName), SentenceAxiom)
-import Options.SMT (KoreSolverOptions (..), parseKoreSolverOptions)
-import SMT qualified
+import Options.SMT as KoreSMT (KoreSolverOptions (..), Solver (..))
+import SMT qualified as KoreSMT
 
 data KoreServer = KoreServer
     { serverState :: MVar.MVar Kore.ServerState
@@ -76,7 +82,7 @@ data KoreServer = KoreServer
         forall a.
         SmtMetadataTools StepperAttributes ->
         [SentenceAxiom (TermLike VariableName)] ->
-        SMT.SMT a ->
+        KoreSMT.SMT a ->
         IO a
     , loggerEnv :: Kore.Log.LoggerEnv IO
     }
@@ -129,15 +135,17 @@ main = do
                 clOPts@CLOptions
                     { port
                     , logLevels
+                    , smtOptions
                     , eventlogEnabledUserEvents
                     }
-            , koreSolverOptions
-            , debugSolverOptions
             } = options
         (logLevel, customLevels) = adjustLogLevels logLevels
         levelFilter :: Logger.LogSource -> LogLevel -> Bool
         levelFilter _source lvl =
             lvl `elem` customLevels || lvl >= logLevel && lvl <= LevelError
+        koreLogExtraLevels =
+            Set.unions $ mapMaybe (`Map.lookup` koreExtraLogs) customLevels
+        koreSolverOptions = translateSMTOpts smtOptions
 
     Logger.runStderrLoggingT $ Logger.filterLogger levelFilter $ do
         liftIO $ forM_ eventlogEnabledUserEvents $ \t -> do
@@ -150,8 +158,10 @@ main = do
             koreLogOptions =
                 (defaultKoreLogOptions (ExeName "") startTime)
                     { Log.logLevel = coLogLevel
+                    , Log.logEntries = koreLogExtraLevels
                     , Log.timestampsSwitch = TimestampsDisable
-                    , Log.debugSolverOptions = debugSolverOptions
+                    , Log.debugSolverOptions =
+                        Log.DebugSolverOptions . fmap (<> ".kore") $ smtOptions >>= (.transcript)
                     , Log.logType = LogSomeAction $ LogAction $ \txt -> liftIO $ monadLogger defaultLoc "kore" logLevel $ toLogStr txt
                     }
             srvSettings = serverSettings port "*"
@@ -193,10 +203,18 @@ toSeverity LevelWarn = Just Log.Warning
 toSeverity LevelError = Just Log.Error
 toSeverity LevelOther{} = Nothing
 
-data CLProxyOptions = CLProxyOptions
+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", "DebugAppliedRewriteRules"])
+            , (LevelOther "SimplifySuccess", ["DebugApplyEquation"])
+            , (LevelOther "RewriteSuccess", ["DebugAppliedRewriteRules"])
+            ]
+
+newtype CLProxyOptions = CLProxyOptions
     { clOptions :: CLOptions
-    , koreSolverOptions :: !KoreSolverOptions
-    , debugSolverOptions :: !Log.DebugSolverOptions
     }
 
 parserInfoModifiers :: InfoMod options
@@ -208,10 +226,34 @@ clProxyOptionsParser :: Parser CLProxyOptions
 clProxyOptionsParser =
     CLProxyOptions
         <$> clOptionsParser
-        <*> parseKoreSolverOptions
-        <*> Log.parseDebugSolverOptions
 
-mkKoreServer :: Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer
+translateSMTOpts :: Maybe SMTOptions -> KoreSMT.KoreSolverOptions
+translateSMTOpts = \case
+    Just smtOpts ->
+        defaultKoreSolverOptions
+            { timeOut = KoreSMT.TimeOut . Limit . fromIntegral $ smtOpts.timeout
+            , retryLimit =
+                KoreSMT.RetryLimit . maybe Unlimited (Limit . fromIntegral) $ smtOpts.retryLimit
+            , tactic = fmap translateSExpr smtOpts.tactic
+            }
+    Nothing ->
+        defaultKoreSolverOptions{solver = KoreSMT.None}
+  where
+    defaultKoreSolverOptions =
+        KoreSMT.KoreSolverOptions
+            { timeOut = KoreSMT.TimeOut Unlimited
+            , retryLimit = KoreSMT.RetryLimit Unlimited
+            , rLimit = KoreSMT.RLimit Unlimited
+            , resetInterval = KoreSMT.ResetInterval 100
+            , prelude = KoreSMT.Prelude Nothing
+            , solver = KoreSMT.Z3
+            , tactic = Nothing
+            }
+    translateSExpr :: SMT.SExpr -> KoreSMT.SExpr
+    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 -> KoreSMT.KoreSolverOptions -> IO KoreServer
 mkKoreServer loggerEnv@Log.LoggerEnv{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =
     flip Log.runLoggerT logAction $ do
         sd@GlobalMain.SerializedDefinition{internedTextCache} <-
@@ -238,31 +280,32 @@ mkKoreServer [email protected]{logAction} CLOptions{definitionFile, mainMo
                 , loggerEnv
                 }
   where
-    KoreSolverOptions{timeOut, rLimit, resetInterval, prelude} = koreSolverOptions
+    KoreSMT.KoreSolverOptions{timeOut, retryLimit, tactic} = koreSolverOptions
+    smtConfig :: KoreSMT.Config
     smtConfig =
-        SMT.defaultConfig
-            { SMT.timeOut = timeOut
-            , SMT.rLimit = rLimit
-            , SMT.resetInterval = resetInterval
-            , SMT.prelude = prelude
+        KoreSMT.defaultConfig
+            { KoreSMT.executable = KoreSMT.defaultConfig.executable -- hack to shut up GHC field warning
+            , KoreSMT.timeOut = timeOut
+            , KoreSMT.retryLimit = retryLimit
+            , KoreSMT.tactic = tactic
             }
 
     -- SMT solver with user declared lemmas
     runSMT ::
         forall a.
         SmtMetadataTools StepperAttributes ->
         [SentenceAxiom (TermLike VariableName)] ->
-        SMT.SMT a ->
+        KoreSMT.SMT a ->
         IO a
     runSMT metadataTools lemmas m =
         flip Log.runLoggerT logAction $
-            bracket (SMT.newSolver smtConfig) SMT.stopSolver $ \refSolverHandle -> do
-                let userInit = SMT.runWithSolver $ declareSMTLemmas metadataTools lemmas
+            bracket (KoreSMT.newSolver smtConfig) KoreSMT.stopSolver $ \refSolverHandle -> do
+                let userInit = KoreSMT.runWithSolver $ declareSMTLemmas metadataTools lemmas
                     solverSetup =
-                        SMT.SolverSetup
+                        KoreSMT.SolverSetup
                             { userInit
                             , refSolverHandle
                             , config = smtConfig
                             }
-                SMT.initSolver solverSetup
-                SMT.runWithSolver m solverSetup
+                KoreSMT.initSolver solverSetup
+                KoreSMT.runWithSolver m solverSetup

library/Booster/CLOptions.hs

@@ -10,14 +10,16 @@ module Booster.CLOptions (
 import Booster.Trace (CustomUserEventType)
 import Booster.VersionInfo (VersionInfo (..), versionInfo)
 import Control.Monad.Logger (LogLevel (..))
+import Data.ByteString.Char8 qualified as BS (pack)
 import Data.List (intercalate, partition)
 import Data.Maybe (fromMaybe)
 import Data.Text (Text, pack)
 import Options.Applicative
 import Text.Casing (fromHumps, fromKebab, toKebab, toPascal)
 import Text.Read (readMaybe)
 
-import Booster.SMT.Interface (SMTOptions (..))
+import Booster.SMT.Interface (SMTOptions (..), defaultSMTOptions)
+import Booster.SMT.LowLevelCodec qualified as SMT (parseSExpr)
 
 data CLOptions = CLOptions
     { definitionFile :: FilePath
@@ -135,25 +137,67 @@ adjustLogLevels ls = (standardLevel, customLevels)
     (stds, customLevels) = partition (<= LevelError) ls
     standardLevel = if null stds then LevelInfo else minimum stds
 
--- FIXME SMTOptions should later replace Options.SMT from kore-rpc,
--- with fully-compatible option names
+-- SMTOptions aligned with Options.SMT from kore-rpc, with
+-- fully-compatible option names in the parser
 parseSMTOptions :: Parser (Maybe SMTOptions)
 parseSMTOptions =
     flag
-        (Just $ SMTOptions Nothing)
+        (Just defaultSMTOptions)
         Nothing
         ( long "no-smt"
             <> help "Disable SMT solver sub-process"
         )
-        <|> ( Just . SMTOptions
+        <|> fmap
+            Just
+            ( SMTOptions
                 <$> optional
                     ( strOption
-                        ( metavar "SMT_TRANSCRIPT_FILE"
-                            <> long "smt-transcript"
+                        ( metavar "PATH"
+                            <> long "solver-transcript"
                             <> help "Destination file for SMT transcript (should not exist prior)"
                         )
                     )
+                <*> option
+                    nonnegativeInt
+                    ( metavar "TIMEOUT"
+                        <> long "smt-timeout"
+                        <> help "Timeout for SMT requests, in milliseconds (0 for Nothing)."
+                        <> value smtDefaults.timeout
+                        <> showDefault
+                    )
+                <*> optional
+                    ( option
+                        nonnegativeInt
+                        ( metavar "COUNT"
+                            <> long "smt-retry-limit"
+                            <> help "Optional Retry-limit for SMT requests - with scaling timeout."
+                            <> value (fromMaybe 0 smtDefaults.retryLimit)
+                            <> showDefault
+                        )
+                    )
+                <*> optional
+                    ( option
+                        readTactic
+                        ( metavar "TACTIC"
+                            <> long "smt-tactic"
+                            <> help
+                                "Optional Z3 tactic to use when checking satisfiability. \
+                                \Example: '(check-sat-using smt)' (i.e., plain 'check-sat')"
+                        )
+                    )
             )
+  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
 
 versionInfoParser :: Parser (a -> a)
 versionInfoParser =

library/Booster/JsonRpc.hs

@@ -152,7 +152,7 @@ respond stateVar =
                                 Log.logInfo $
                                     "Added a new module. Now in scope: " <> Text.intercalate ", " (Map.keys newDefinitions)
                                 pure $ Right $ RpcTypes.AddModule $ RpcTypes.AddModuleResult $ getId newModule.name
-        RpcTypes.Simplify req -> withContext req._module $ \(def, mLlvmLibrary, _mSMTOptions) -> do
+        RpcTypes.Simplify req -> withContext req._module $ \(def, mLlvmLibrary, mSMTOptions) -> do
             start <- liftIO $ getTime Monotonic
             let internalised =
                     runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term
@@ -180,14 +180,17 @@ respond stateVar =
                         [ req.logSuccessfulSimplifications
                         , req.logFailedSimplifications
                         ]
+
+            solver <- traverse (SMT.initSolver def) mSMTOptions
+
             result <- case internalised of
                 Left patternErrors -> do
                     Log.logError $ "Error internalising cterm: " <> Text.pack (show patternErrors)
                     pure $ Left $ RpcError.backendError RpcError.CouldNotVerifyPattern patternErrors
                 -- term and predicate (pattern)
                 Right (TermAndPredicateAndSubstitution pat substitution) -> do
                     Log.logInfoNS "booster" "Simplifying a pattern"
-                    ApplyEquations.evaluatePattern doTracing def mLlvmLibrary mempty pat >>= \case
+                    ApplyEquations.evaluatePattern doTracing def mLlvmLibrary solver mempty pat >>= \case
                         (Right newPattern, patternTraces, _) -> do
                             let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution
                                 tSort = externaliseSort (sortOfPattern newPattern)
@@ -210,7 +213,7 @@ respond stateVar =
                                 (addHeader $ Syntax.KJTop (fromMaybe (error "not a predicate") $ sortOfJson req.state.term), [])
                     | otherwise -> do
                         Log.logInfoNS "booster" "Simplifying all predicates"
-                        ApplyEquations.simplifyConstraints doTracing def mLlvmLibrary mempty (Set.toList predicates) >>= \case
+                        ApplyEquations.simplifyConstraints doTracing def mLlvmLibrary solver mempty (Set.toList predicates) >>= \case
                             (Right newPreds, traces, _) -> do
                                 let predicateSort =
                                         fromMaybe (error "not a predicate") $
@@ -223,6 +226,7 @@ respond stateVar =
                                 pure $ Right (addHeader $ Syntax.KJAnd predicateSort result, traces)
                             (Left something, _traces, _) ->
                                 pure . Left . RpcError.backendError RpcError.Aborted $ show something -- FIXME
+            whenJust solver SMT.closeSolver
             stop <- liftIO $ getTime Monotonic
 
             let duration =