quebex

 1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
 2--
 3-- SPDX-License-Identifier: GPL-3.0-only
 4
 5module Main (main) where
 6
 7import Language.QBE.Backend.Store qualified as ST
 8import Language.QBE.Backend.Tracer qualified as T
 9import Language.QBE.CmdLine qualified as CMD
10import Language.QBE.Simulator.Concolic.State (mkEnv)
11import Language.QBE.Simulator.Explorer (defSolver, explore, logSolver, newEngine)
12import Language.QBE.Types qualified as QBE
13import Options.Applicative qualified as OPT
14import System.IO (IOMode (WriteMode), withFile)
15
16data Opts = Opts
17  { optLog :: Maybe FilePath,
18    optSeed :: Maybe Int,
19    optBase :: CMD.BasicArgs
20  }
21
22optsParser :: OPT.Parser Opts
23optsParser =
24  Opts
25    <$> OPT.optional
26      ( OPT.strOption
27          ( OPT.long "dump-smt2"
28              <> OPT.short 'd'
29              <> OPT.metavar "FILE"
30              <> OPT.help "Output queries as an SMT-LIB file"
31          )
32      )
33    <*> OPT.optional
34      ( OPT.option
35          OPT.auto
36          ( OPT.long "random-seed"
37              <> OPT.short 'r'
38              <> OPT.help "Initial seed to for the random number generator"
39          )
40      )
41    <*> CMD.basicArgs
42
43------------------------------------------------------------------------
44
45exploreFile :: Opts -> IO [(ST.Assign, T.ExecTrace)]
46exploreFile opts@Opts {optBase = base} = do
47  (prog, func) <- CMD.parseEntryFile $ CMD.optQBEFile base
48
49  env <- mkEnv prog (CMD.optMemStart base) (CMD.optMemSize base) (optSeed opts)
50  case optLog opts of
51    Just fn -> withFile fn WriteMode (exploreWithHandle env func)
52    Nothing -> do
53      engine <- newEngine <$> defSolver
54      explore engine env func params
55  where
56    params :: [(String, QBE.ExtType)]
57    params = []
58
59    exploreWithHandle env func handle = do
60      engine <- newEngine <$> logSolver handle
61      explore engine env func params
62
63main :: IO ()
64main = do
65  args <- OPT.execParser cmd
66  paths <- exploreFile args
67  putStrLn $ "Amount of paths: " ++ show (length paths)
68  where
69    cmd :: OPT.ParserInfo Opts
70    cmd =
71      OPT.info
72        (optsParser OPT.<**> OPT.helper)
73        ( OPT.fullDesc
74            <> OPT.progDesc "Symbolic execution of programs in the QBE intermediate language"
75        )