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 Data.List (find)
10import Language.QBE (globalFuncs, parse)
11import Language.QBE.Backend.Store qualified as ST
12import Language.QBE.Backend.Tracer qualified as T
13import Language.QBE.Simulator.Concolic.State (mkEnv)
14import Language.QBE.Simulator.Explorer (explore, logSolver, newEngine)
15import Language.QBE.Simulator.Symbolic.Unwind (unwind)
16import Language.QBE.Types qualified as QBE
17import System.Exit (ExitCode (ExitSuccess))
18import System.FilePath ((</>))
19import System.IO (IOMode (WriteMode), hClose, hPutStrLn, openFile, withFile)
20import System.Process
21  ( StdStream (CreatePipe, UseHandle),
22    createProcess,
23    proc,
24    std_in,
25    std_out,
26    waitForProcess,
27  )
28
29logPath :: FilePath
30logPath = "/tmp/quebex-symex-bench.smt2"
31
32entryFunc :: QBE.GlobalIdent
33entryFunc = QBE.GlobalIdent "main"
34
35------------------------------------------------------------------------
36
37exploreQBE :: FilePath -> IO [(ST.Assign, T.ExecTrace)]
38exploreQBE filePath = do
39  content <- readFile filePath
40  prog <- case parse filePath content of
41    Right rt -> pure rt
42    Left err -> fail $ "Parsing error: " ++ show err
43
44  let funcs = globalFuncs prog
45  func <- case find (\f -> QBE.fName f == entryFunc) funcs of
46    Just x -> pure x
47    Nothing -> fail $ "Unable to find entry function: " ++ show entryFunc
48
49  withFile logPath WriteMode (explore' prog func)
50  where
51    explore' prog func handle = do
52      engine <- newEngine <$> logSolver handle
53      defEnv <- mkEnv prog 0 128 (Just 0)
54      explore engine defEnv func []
55
56getQueries :: String -> IO String
57getQueries name = do
58  _ <- exploreQBE ("bench" </> "data" </> "SMT" </> name)
59  -- XXX: Uncomment this to benchmark incremental solving instead.
60  unwind logPath
61
62solveQueries :: String -> IO ()
63solveQueries queries = do
64  devNull <- openFile "/dev/null" WriteMode
65  (Just hin, _, _, p) <-
66    createProcess
67      (proc "bitwuzla" [])
68        { std_in = CreatePipe,
69          std_out = UseHandle devNull
70        }
71
72  hPutStrLn hin queries <* hClose hin
73  ret <- waitForProcess p <* hClose devNull
74  when (ret /= ExitSuccess) $
75    error "SMT solver failed"
76
77smtBench :: Benchmark
78smtBench = do
79  bgroup
80    "SMT Complexity"
81    [ benchWithEnv "prime-numbers.qbe",
82      benchWithEnv "bubble-sort.qbe",
83      benchWithEnv "insertion-sort-uchar.qbe"
84    ]
85  where
86    benchSolver :: String -> String -> Benchmark
87    benchSolver name queries = bench name $ nfIO (solveQueries queries)
88
89    benchWithEnv :: String -> Benchmark
90    benchWithEnv name = env (getQueries name) (benchSolver name)