1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>2--3-- SPDX-License-Identifier: GPL-3.0-only45module Main (main) where67import Control.Exception (Exception, throwIO)8import Control.Monad (when)9import Data.List (find)10import Data.Maybe (isJust)11import Language.QBE (globalFuncs, parse)12import Language.QBE.Backend.Store qualified as ST13import Language.QBE.Backend.Tracer qualified as T14import Language.QBE.Simulator.Concolic.State (mkEnv)15import Language.QBE.Simulator.Explorer (defSolver, explore, logSolver, newEngine)16import Language.QBE.Simulator.Memory qualified as MEM17import Language.QBE.Simulator.Symbolic.Unwind (unwind)18import Language.QBE.Types qualified as QBE19import Options.Applicative qualified as OPT20import System.Directory (getTemporaryDirectory, removeFile)21import System.IO (IOMode (WriteMode), hClose, hPutStr, openFile, openTempFile, withFile)22import Text.Parsec (ParseError)2324data Opts = Opts25 { optMemStart :: MEM.Address,26 optMemSize :: MEM.Size,27 optLog :: Maybe FilePath,28 optLogIncr :: Maybe FilePath,29 optSeed :: Maybe Int,30 optQBEFile :: FilePath31 }3233optsParser :: OPT.Parser Opts34optsParser =35 Opts36 <$> OPT.option37 OPT.auto38 ( OPT.long "memory-start"39 <> OPT.short 'm'40 <> OPT.value 0x041 )42 <*> OPT.option43 OPT.auto44 ( OPT.long "memory-size"45 <> OPT.short 's'46 <> OPT.value (1024 * 1024) -- 1 MB RAM47 <> OPT.help "Size of the memory region"48 )49 <*> OPT.optional50 ( OPT.strOption51 ( OPT.long "dump-smt2"52 <> OPT.short 'd'53 <> OPT.metavar "FILE"54 <> OPT.help "Output queries as a non-incremental SMT-LIB file"55 )56 )57 <*> OPT.optional58 ( OPT.strOption59 ( OPT.long "dump-incr-smt2"60 <> OPT.short 'D'61 <> OPT.metavar "FILE"62 <> OPT.help "Output queries as an incremental SMT-LIB file"63 )64 )65 <*> OPT.optional66 ( OPT.option67 OPT.auto68 ( OPT.long "random-seed"69 <> OPT.short 'r'70 <> OPT.help "Initial seed to for the random number generator"71 )72 )73 <*> OPT.argument OPT.str (OPT.metavar "FILE")7475------------------------------------------------------------------------7677data ExecError78 = SyntaxError ParseError79 | UnknownFunction QBE.GlobalIdent80 deriving (Show)8182instance Exception ExecError8384exploreFile :: Opts -> IO [(ST.Assign, T.ExecTrace)]85exploreFile opts = do86 let filePath = optQBEFile opts87 content <- readFile filePath88 prog <- case parse filePath content of89 Right rt -> pure rt90 Left err -> throwIO $ SyntaxError err9192 let funcs = globalFuncs prog93 func <- case find (\f -> QBE.fName f == entryFunc) funcs of94 Just x -> pure x95 Nothing -> throwIO $ UnknownFunction entryFunc9697 env <- mkEnv prog (optMemStart opts) (optMemSize opts) (optSeed opts)98 if isJust (optLog opts) || isJust (optLogIncr opts)99 then do100 (logPath, logFile, isTemp) <- case optLogIncr opts of101 Just fn -> do102 f <- openFile fn WriteMode103 pure (fn, f, False)104 Nothing -> do105 tempDir <- getTemporaryDirectory106 (name, file) <- openTempFile tempDir "quebex-queries.smt2"107 pure (name, file, True)108109 ret <- exploreWithHandle env func logFile <* hClose logFile110 case optLog opts of111 Just fn -> withFile fn WriteMode (\h -> unwind logPath >>= hPutStr h)112 Nothing -> pure ()113114 when isTemp $115 removeFile logPath116 pure ret117 else do118 engine <- newEngine <$> defSolver119 explore engine env func params120 where121 params :: [(String, QBE.ExtType)]122 params = []123124 entryFunc :: QBE.GlobalIdent125 entryFunc = QBE.GlobalIdent "main"126127 exploreWithHandle env func handle = do128 engine <- newEngine <$> logSolver handle129 explore engine env func params130131main :: IO ()132main = do133 args <- OPT.execParser cmd134 paths <- exploreFile args135 putStrLn $ "Amount of paths: " ++ show (length paths)136 where137 cmd :: OPT.ParserInfo Opts138 cmd =139 OPT.info140 (optsParser OPT.<**> OPT.helper)141 ( OPT.fullDesc142 <> OPT.progDesc "Symbolic execution of programs in the QBE intermediate language"143 )