quebex

  1-- SPDX-FileCopyrightText: 2025-2026 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.Monad (when)
  8import Control.Monad.State (evalStateT, gets, liftIO)
  9import Data.Binary (encodeFile)
 10import Data.KTest (KTest (KTest), KTestObj, fromAssign)
 11import Data.String (fromString)
 12import Language.QBE.CmdLine qualified as CMD
 13import Language.QBE.Simulator (execFunc)
 14import Language.QBE.Simulator.Concolic.State (mkEnv)
 15import Language.QBE.Simulator.Explorer
 16  ( Engine (expPathVars),
 17    defSolver,
 18    explorePath,
 19    logSolver,
 20    newEngine,
 21  )
 22import Language.QBE.Types qualified as QBE
 23import Options.Applicative qualified as OPT
 24import System.Directory (createDirectoryIfMissing)
 25import System.FilePath (addExtension, (</>))
 26import System.IO (IOMode (WriteMode), withFile)
 27import Text.Printf (printf)
 28
 29data Opts = Opts
 30  { optLog :: Maybe FilePath,
 31    optSeed :: Maybe Int,
 32    optTests :: Maybe FilePath,
 33    optVerbose :: Bool,
 34    optBase :: CMD.BasicArgs
 35  }
 36
 37optsParser :: OPT.Parser Opts
 38optsParser =
 39  Opts
 40    <$> OPT.optional
 41      ( OPT.strOption
 42          ( OPT.long "dump-smt2"
 43              <> OPT.short 'd'
 44              <> OPT.metavar "FILE"
 45              <> OPT.help "Output queries as an SMT-LIB file"
 46          )
 47      )
 48    <*> OPT.optional
 49      ( OPT.option
 50          OPT.auto
 51          ( OPT.long "random-seed"
 52              <> OPT.short 'r'
 53              <> OPT.help "Initial seed to for the random number generator"
 54          )
 55      )
 56    <*> OPT.optional
 57      ( OPT.strOption
 58          ( OPT.long "write-tests"
 59              <> OPT.short 't'
 60              <> OPT.metavar "DIR"
 61              <> OPT.help "Write .ktest files to the given directory"
 62          )
 63      )
 64    <*> OPT.switch
 65      ( OPT.long "verbose"
 66          <> OPT.short 'v'
 67          <> OPT.help "Enable more verbose output"
 68      )
 69    <*> CMD.basicArgs
 70
 71------------------------------------------------------------------------
 72
 73data KTestConf = KTestConf FilePath String
 74  deriving (Show)
 75
 76mkKTestConf :: FilePath -> String -> IO KTestConf
 77mkKTestConf directory name = do
 78  createDirectoryIfMissing True directory
 79  pure $ KTestConf directory name
 80
 81writeKTest :: KTestConf -> Int -> [KTestObj] -> IO ()
 82writeKTest (KTestConf directory name) pathID =
 83  writeKTest' pathID . KTest [fromString name]
 84  where
 85    writeKTest' :: Int -> KTest -> IO ()
 86    writeKTest' n ktest = do
 87      flip encodeFile ktest $
 88        addExtension
 89          (directory </> ("test" ++ printf "%06d" n))
 90          ".ktest"
 91
 92------------------------------------------------------------------------
 93
 94exploreEntry :: Opts -> Maybe KTestConf -> Engine -> QBE.FuncDef -> IO Int
 95exploreEntry opts ktest engine entry =
 96  evalStateT (go 1 $ execFunc entry []) engine
 97  where
 98    go n st = do
 99      when (optVerbose opts) $
100        liftIO (putStrLn $ "Exploring path " ++ show n ++ "...")
101
102      morePaths <- explorePath st
103      case ktest of
104        Just conf -> do
105          assign <- gets (fromAssign . expPathVars)
106          liftIO $ writeKTest conf n assign
107        Nothing -> pure ()
108
109      if morePaths
110        then go (n + 1) st
111        else pure n
112
113exploreFile :: Opts -> IO Int
114exploreFile opts@Opts {optBase = base} = do
115  (prog, func) <- CMD.parseEntryFile $ CMD.optQBEFile base
116
117  ktest <-
118    case optTests opts of
119      Just dir -> do
120        Just <$> mkKTestConf dir (CMD.optQBEFile $ optBase opts)
121      Nothing -> pure Nothing
122
123  env <- mkEnv prog (CMD.optMemStart base) (CMD.optMemSize base) (optSeed opts)
124  case optLog opts of
125    Just fn -> withFile fn WriteMode (exploreWithHandle ktest env func)
126    Nothing -> do
127      engine <- newEngine env <$> defSolver
128      exploreEntry opts ktest engine func
129  where
130    exploreWithHandle ktest env func handle = do
131      engine <- newEngine env <$> logSolver handle
132      exploreEntry opts ktest engine func
133
134------------------------------------------------------------------------
135
136cmd :: OPT.ParserInfo Opts
137cmd =
138  OPT.info
139    (optsParser OPT.<**> OPT.helper)
140    ( OPT.fullDesc
141        <> OPT.progDesc "Symbolic execution of programs in the QBE intermediate language"
142    )
143
144main :: IO ()
145main = do
146  numPaths <- OPT.execParser cmd >>= exploreFile
147  putStrLn $ "\n---\nAmount of paths: " ++ show numPaths