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.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 "entry"
33
34------------------------------------------------------------------------
35
36exploreQBE :: FilePath -> [(String, QBE.BaseType)] -> IO [(ST.Assign, T.ExecTrace)]
37exploreQBE filePath params = do
38  content <- readFile filePath
39  prog <- case parse filePath content of
40    Right rt -> pure rt
41    Left err -> fail $ "Parsing error: " ++ show err
42
43  let funcs = globalFuncs prog
44  func <- case find (\f -> QBE.fName f == entryFunc) funcs of
45    Just x -> pure x
46    Nothing -> fail $ "Unable to find entry function: " ++ show entryFunc
47
48  withFile logPath WriteMode (explore' prog func)
49  where
50    explore' prog func handle = do
51      engine <- logSolver handle >>= newEngine
52      explore engine prog func params
53
54getQueries :: String -> [(String, QBE.BaseType)] -> IO String
55getQueries name params = do
56  _ <- exploreQBE ("bench" </> "data" </> "SMT" </> name) params
57  -- XXX: Uncomment this to benchmark incremental solving instead.
58  unwind logPath
59
60solveQueries :: String -> IO ()
61solveQueries queries = do
62  devNull <- openFile "/dev/null" WriteMode
63  (Just hin, _, _, p) <-
64    createProcess
65      (proc "bitwuzla" [])
66        { std_in = CreatePipe,
67          std_out = UseHandle devNull
68        }
69
70  hPutStrLn hin queries <* hClose hin
71  ret <- waitForProcess p <* hClose devNull
72  when (ret /= ExitSuccess) $
73    error "SMT solver failed"
74
75smtBench :: Benchmark
76smtBench = do
77  bgroup
78    "SMT Complexity"
79    [ benchWithEnv "prime-numbers.qbe" [("a", QBE.Word)],
80      benchWithEnv "bubble-sort.qbe" [("a", QBE.Word), ("b", QBE.Word), ("c", QBE.Word), ("d", QBE.Word)]
81    ]
82  where
83    benchSolver :: String -> String -> Benchmark
84    benchSolver name queries = bench name $ nfIO (solveQueries queries)
85
86    benchWithEnv :: String -> [(String, QBE.BaseType)] -> Benchmark
87    benchWithEnv name params = env (getQueries name params) (benchSolver name)