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