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 Control.Exception (Exception, throwIO)
  8import Data.List (find)
  9import Language.QBE (globalFuncs, parse)
 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 (defSolver, explore, logSolver, newEngine)
 14import Language.QBE.Simulator.Memory qualified as MEM
 15import Language.QBE.Types qualified as QBE
 16import Options.Applicative qualified as OPT
 17import System.IO (IOMode (WriteMode), withFile)
 18import Text.Parsec (ParseError)
 19
 20data Opts = Opts
 21  { optMemStart :: MEM.Address,
 22    optMemSize :: MEM.Size,
 23    optLog :: Maybe FilePath,
 24    optSeed :: Maybe Int,
 25    optQBEFile :: FilePath
 26  }
 27
 28optsParser :: OPT.Parser Opts
 29optsParser =
 30  Opts
 31    <$> OPT.option
 32      OPT.auto
 33      ( OPT.long "memory-start"
 34          <> OPT.short 'm'
 35          <> OPT.value 0x0
 36      )
 37    <*> OPT.option
 38      OPT.auto
 39      ( OPT.long "memory-size"
 40          <> OPT.short 's'
 41          <> OPT.value (1024 * 1024) -- 1 MB RAM
 42          <> OPT.help "Size of the memory region"
 43      )
 44    <*> OPT.optional
 45      ( OPT.strOption
 46          ( OPT.long "dump-smt2"
 47              <> OPT.short 'd'
 48              <> OPT.metavar "FILE"
 49              <> OPT.help "Output queries as an SMT-LIB file"
 50          )
 51      )
 52    <*> OPT.optional
 53      ( OPT.option
 54          OPT.auto
 55          ( OPT.long "random-seed"
 56              <> OPT.short 'r'
 57              <> OPT.help "Initial seed to for the random number generator"
 58          )
 59      )
 60    <*> OPT.argument OPT.str (OPT.metavar "FILE")
 61
 62------------------------------------------------------------------------
 63
 64data ExecError
 65  = SyntaxError ParseError
 66  | UnknownFunction QBE.GlobalIdent
 67  deriving (Show)
 68
 69instance Exception ExecError
 70
 71exploreFile :: Opts -> IO [(ST.Assign, T.ExecTrace)]
 72exploreFile opts = do
 73  let filePath = optQBEFile opts
 74  content <- readFile filePath
 75  prog <- case parse filePath content of
 76    Right rt -> pure rt
 77    Left err -> throwIO $ SyntaxError err
 78
 79  let funcs = globalFuncs prog
 80  func <- case find (\f -> QBE.fName f == entryFunc) funcs of
 81    Just x -> pure x
 82    Nothing -> throwIO $ UnknownFunction entryFunc
 83
 84  env <- mkEnv prog (optMemStart opts) (optMemSize opts) (optSeed opts)
 85  case optLog opts of
 86    Just fn -> withFile fn WriteMode (exploreWithHandle env func)
 87    Nothing -> do
 88      engine <- newEngine <$> defSolver
 89      explore engine env func params
 90  where
 91    params :: [(String, QBE.ExtType)]
 92    params = []
 93
 94    entryFunc :: QBE.GlobalIdent
 95    entryFunc = QBE.GlobalIdent "main"
 96
 97    exploreWithHandle env func handle = do
 98      engine <- newEngine <$> logSolver handle
 99      explore engine env func params
100
101main :: IO ()
102main = do
103  args <- OPT.execParser cmd
104  paths <- exploreFile args
105  putStrLn $ "Amount of paths: " ++ show (length paths)
106  where
107    cmd :: OPT.ParserInfo Opts
108    cmd =
109      OPT.info
110        (optsParser OPT.<**> OPT.helper)
111        ( OPT.fullDesc
112            <> OPT.progDesc "Symbolic execution of programs in the QBE intermediate language"
113        )