qute-symex-0.1.1: bench/SMT.hs

-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
--
-- SPDX-License-Identifier: MIT AND GPL-3.0-only

module SMT (smtBench) where

import Control.Monad (when)
import Criterion.Main
import Language.QBE (parseAndFind)
import Language.QBE.Simulator.Concolic.State (mkEnv)
import Language.QBE.Simulator.Explorer (PathResult, exploreFunc, logSolver, newEngine)
import Language.QBE.Types qualified as QBE
import SMTUnwind (unwind)
import SimpleBV qualified as SMT
import System.Exit (ExitCode (ExitSuccess))
import System.FilePath ((</>))
import System.IO (IOMode (WriteMode), hClose, hPutStrLn, openFile, withFile)
import System.Process
  ( StdStream (CreatePipe, UseHandle),
    createProcess,
    proc,
    std_in,
    std_out,
    waitForProcess,
  )

logPath :: FilePath
logPath = "/tmp/qute-symex-bench.smt2"

entryFunc :: QBE.GlobalIdent
entryFunc = QBE.GlobalIdent "main"

------------------------------------------------------------------------

exploreQBE :: FilePath -> IO [PathResult]
exploreQBE filePath = do
  (prog, func) <- readFile filePath >>= parseAndFind entryFunc

  withFile logPath WriteMode (exploreFunc' prog func)
  where
    exploreFunc' prog func handle = do
      defEnv <- mkEnv prog 0 128 (Just 0)
      solver <- logSolver handle

      let engine = newEngine defEnv solver
      exploreFunc engine func [] <* SMT.stop solver

getQueries :: String -> IO String
getQueries name = do
  _ <- exploreQBE ("bench" </> "data" </> "SMT" </> name)
  -- XXX: Uncomment this to benchmark incremental solving instead.
  unwind logPath

solveQueries :: String -> IO ()
solveQueries queries = do
  devNull <- openFile "/dev/null" WriteMode
  (Just hin, _, _, p) <-
    createProcess
      (proc "bitwuzla" [])
        { std_in = CreatePipe,
          std_out = UseHandle devNull
        }

  hPutStrLn hin queries <* hClose hin
  ret <- waitForProcess p <* hClose devNull
  when (ret /= ExitSuccess) $
    error "SMT solver failed"

smtBench :: Benchmark
smtBench = do
  bgroup
    "SMT Complexity"
    [ benchWithEnv "prime-numbers.qbe",
      benchWithEnv "bubble-sort.qbe",
      benchWithEnv "insertion-sort-uchar.qbe"
    ]
  where
    benchSolver :: String -> String -> Benchmark
    benchSolver name queries = bench name $ nfIO (solveQueries queries)

    benchWithEnv :: String -> Benchmark
    benchWithEnv name = env (getQueries name) (benchSolver name)