quebex

 1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
 2--
 3-- SPDX-License-Identifier: MIT AND GPL-3.0-only
 4
 5module SMT (smtBench) where
 6
 7import Control.Monad (when)
 8import Criterion.Main
 9import Language.QBE (parseAndFind)
10import Language.QBE.Simulator.Concolic.State (mkEnv)
11import Language.QBE.Simulator.Explorer (PathResult, exploreFunc, logSolver, newEngine)
12import Language.QBE.Types qualified as QBE
13import SMTUnwind (unwind)
14import System.Exit (ExitCode (ExitSuccess))
15import System.FilePath ((</>))
16import System.IO (IOMode (WriteMode), hClose, hPutStrLn, openFile, withFile)
17import System.Process
18  ( StdStream (CreatePipe, UseHandle),
19    createProcess,
20    proc,
21    std_in,
22    std_out,
23    waitForProcess,
24  )
25
26logPath :: FilePath
27logPath = "/tmp/quebex-symex-bench.smt2"
28
29entryFunc :: QBE.GlobalIdent
30entryFunc = QBE.GlobalIdent "main"
31
32------------------------------------------------------------------------
33
34exploreQBE :: FilePath -> IO [PathResult]
35exploreQBE filePath = do
36  (prog, func) <- readFile filePath >>= parseAndFind entryFunc
37
38  withFile logPath WriteMode (exploreFunc' prog func)
39  where
40    exploreFunc' prog func handle = do
41      defEnv <- mkEnv prog 0 128 (Just 0)
42      engine <- newEngine defEnv <$> logSolver handle
43      exploreFunc engine func []
44
45getQueries :: String -> IO String
46getQueries name = do
47  _ <- exploreQBE ("bench" </> "data" </> "SMT" </> name)
48  -- XXX: Uncomment this to benchmark incremental solving instead.
49  unwind logPath
50
51solveQueries :: String -> IO ()
52solveQueries queries = do
53  devNull <- openFile "/dev/null" WriteMode
54  (Just hin, _, _, p) <-
55    createProcess
56      (proc "bitwuzla" [])
57        { std_in = CreatePipe,
58          std_out = UseHandle devNull
59        }
60
61  hPutStrLn hin queries <* hClose hin
62  ret <- waitForProcess p <* hClose devNull
63  when (ret /= ExitSuccess) $
64    error "SMT solver failed"
65
66smtBench :: Benchmark
67smtBench = do
68  bgroup
69    "SMT Complexity"
70    [ benchWithEnv "prime-numbers.qbe",
71      benchWithEnv "bubble-sort.qbe",
72      benchWithEnv "insertion-sort-uchar.qbe"
73    ]
74  where
75    benchSolver :: String -> String -> Benchmark
76    benchSolver name queries = bench name $ nfIO (solveQueries queries)
77
78    benchWithEnv :: String -> Benchmark
79    benchWithEnv name = env (getQueries name) (benchSolver name)