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.option
 66      OPT.auto
 67      ( OPT.long "random-seed"
 68          <> OPT.short 'r'
 69          <> OPT.help "Initial seed to for the random number generator"
 70      )
 71    <*> OPT.argument OPT.str (OPT.metavar "FILE")
 72
 73------------------------------------------------------------------------
 74
 75data ExecError
 76  = SyntaxError ParseError
 77  | UnknownFunction QBE.GlobalIdent
 78  deriving (Show)
 79
 80instance Exception ExecError
 81
 82exploreFile :: Opts -> IO [(ST.Assign, T.ExecTrace)]
 83exploreFile opts = do
 84  let filePath = optQBEFile opts
 85  content <- readFile filePath
 86  prog <- case parse filePath content of
 87    Right rt -> pure rt
 88    Left err -> throwIO $ SyntaxError err
 89
 90  let funcs = globalFuncs prog
 91  func <- case find (\f -> QBE.fName f == entryFunc) funcs of
 92    Just x -> pure x
 93    Nothing -> throwIO $ UnknownFunction entryFunc
 94
 95  env <- mkEnv prog (optMemStart opts) (optMemSize opts) (optSeed opts)
 96  if isJust (optLog opts) || isJust (optLogIncr opts)
 97    then do
 98      (logPath, logFile, isTemp) <- case optLogIncr opts of
 99        Just fn -> do
100          f <- openFile fn WriteMode
101          pure (fn, f, False)
102        Nothing -> do
103          tempDir <- getTemporaryDirectory
104          (name, file) <- openTempFile tempDir "quebex-queries.smt2"
105          pure (name, file, True)
106
107      ret <- exploreWithHandle env func logFile <* hClose logFile
108      case optLog opts of
109        Just fn -> withFile fn WriteMode (\h -> unwind logPath >>= hPutStr h)
110        Nothing -> pure ()
111
112      when isTemp $
113        removeFile logPath
114      pure ret
115    else do
116      engine <- newEngine <$> defSolver
117      explore engine env func params
118  where
119    params :: [(String, QBE.ExtType)]
120    params = []
121
122    entryFunc :: QBE.GlobalIdent
123    entryFunc = QBE.GlobalIdent "main"
124
125    exploreWithHandle env func handle = do
126      engine <- newEngine <$> logSolver handle
127      explore engine env func params
128
129main :: IO ()
130main = do
131  args <- OPT.execParser cmd
132  paths <- exploreFile args
133  putStrLn $ "Amount of paths: " ++ show (length paths)
134  where
135    cmd :: OPT.ParserInfo Opts
136    cmd =
137      OPT.info
138        (optsParser OPT.<**> OPT.helper)
139        ( OPT.fullDesc
140            <> OPT.progDesc "Symbolic execution of programs in the QBE intermediate language"
141        )