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 Control.Monad (when)
  9import Data.List (find)
 10import Data.Maybe (isJust)
 11import Language.QBE (globalFuncs, parse)
 12import Language.QBE.Backend.Store qualified as ST
 13import Language.QBE.Backend.Tracer qualified as T
 14import Language.QBE.Simulator.Concolic.State (mkEnv)
 15import Language.QBE.Simulator.Explorer (defSolver, explore, logSolver, newEngine)
 16import Language.QBE.Simulator.Memory qualified as MEM
 17import Language.QBE.Simulator.Symbolic.Unwind (unwind)
 18import Language.QBE.Types qualified as QBE
 19import Options.Applicative qualified as OPT
 20import System.Directory (getTemporaryDirectory, removeFile)
 21import System.IO (IOMode (WriteMode), hClose, hPutStr, openFile, openTempFile, withFile)
 22import Text.Parsec (ParseError)
 23
 24data Opts = Opts
 25  { optMemStart :: MEM.Address,
 26    optMemSize :: MEM.Size,
 27    optLog :: Maybe FilePath,
 28    optLogIncr :: Maybe FilePath,
 29    optSeed :: Maybe Int,
 30    optQBEFile :: FilePath
 31  }
 32
 33optsParser :: OPT.Parser Opts
 34optsParser =
 35  Opts
 36    <$> OPT.option
 37      OPT.auto
 38      ( OPT.long "memory-start"
 39          <> OPT.short 'm'
 40          <> OPT.value 0x0
 41      )
 42    <*> OPT.option
 43      OPT.auto
 44      ( OPT.long "memory-size"
 45          <> OPT.short 's'
 46          <> OPT.value (1024 * 1024) -- 1 MB RAM
 47          <> OPT.help "Size of the memory region"
 48      )
 49    <*> OPT.optional
 50      ( OPT.strOption
 51          ( 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.optional
 58      ( OPT.strOption
 59          ( 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.optional
 66      ( OPT.option
 67          OPT.auto
 68          ( 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")
 74
 75------------------------------------------------------------------------
 76
 77data ExecError
 78  = SyntaxError ParseError
 79  | UnknownFunction QBE.GlobalIdent
 80  deriving (Show)
 81
 82instance Exception ExecError
 83
 84exploreFile :: Opts -> IO [(ST.Assign, T.ExecTrace)]
 85exploreFile opts = do
 86  let filePath = optQBEFile opts
 87  content <- readFile filePath
 88  prog <- case parse filePath content of
 89    Right rt -> pure rt
 90    Left err -> throwIO $ SyntaxError err
 91
 92  let funcs = globalFuncs prog
 93  func <- case find (\f -> QBE.fName f == entryFunc) funcs of
 94    Just x -> pure x
 95    Nothing -> throwIO $ UnknownFunction entryFunc
 96
 97  env <- mkEnv prog (optMemStart opts) (optMemSize opts) (optSeed opts)
 98  if isJust (optLog opts) || isJust (optLogIncr opts)
 99    then do
100      (logPath, logFile, isTemp) <- case optLogIncr opts of
101        Just fn -> do
102          f <- openFile fn WriteMode
103          pure (fn, f, False)
104        Nothing -> do
105          tempDir <- getTemporaryDirectory
106          (name, file) <- openTempFile tempDir "quebex-queries.smt2"
107          pure (name, file, True)
108
109      ret <- exploreWithHandle env func logFile <* hClose logFile
110      case optLog opts of
111        Just fn -> withFile fn WriteMode (\h -> unwind logPath >>= hPutStr h)
112        Nothing -> pure ()
113
114      when isTemp $
115        removeFile logPath
116      pure ret
117    else do
118      engine <- newEngine <$> defSolver
119      explore engine env func params
120  where
121    params :: [(String, QBE.ExtType)]
122    params = []
123
124    entryFunc :: QBE.GlobalIdent
125    entryFunc = QBE.GlobalIdent "main"
126
127    exploreWithHandle env func handle = do
128      engine <- newEngine <$> logSolver handle
129      explore engine env func params
130
131main :: IO ()
132main = do
133  args <- OPT.execParser cmd
134  paths <- exploreFile args
135  putStrLn $ "Amount of paths: " ++ show (length paths)
136  where
137    cmd :: OPT.ParserInfo Opts
138    cmd =
139      OPT.info
140        (optsParser OPT.<**> OPT.helper)
141        ( OPT.fullDesc
142            <> OPT.progDesc "Symbolic execution of programs in the QBE intermediate language"
143        )