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.Strict (evalStateT, gets, liftIO)
  9import Data.Binary (encodeFile)
 10import Data.KTest (KTest (KTest), KTestObj, fromAssign)
 11import Data.String (fromString)
 12import Language.QBE.Backend.Store (Assign)
 13import Language.QBE.CmdLine qualified as CMD
 14import Language.QBE.Simulator (execFunc)
 15import Language.QBE.Simulator.Concolic.State (mkEnv)
 16import Language.QBE.Simulator.Error (EvalError)
 17import Language.QBE.Simulator.Explorer
 18  ( Engine (expLastPath),
 19    PathResult (pathErr, pathVars),
 20    defSolver,
 21    explorePath,
 22    logSolver,
 23    newEngine,
 24  )
 25import Language.QBE.Types qualified as QBE
 26import Options.Applicative qualified as OPT
 27import System.Directory (createDirectoryIfMissing)
 28import System.Exit (die)
 29import System.FilePath (addExtension, (</>))
 30import System.IO (IOMode (WriteMode), hPutStrLn, stderr, withFile)
 31import Text.Printf (printf)
 32
 33data Opts = Opts
 34  { optLog :: Maybe FilePath,
 35    optSeed :: Maybe Int,
 36    optTestDir :: Maybe FilePath,
 37    optErrExit :: Bool,
 38    optWriteAll :: Bool,
 39    optVerbose :: Bool,
 40    optBase :: CMD.BasicArgs
 41  }
 42
 43optTestCases :: String
 44optTestCases = "test-cases"
 45
 46optsParser :: OPT.Parser Opts
 47optsParser =
 48  Opts
 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 an SMT-LIB file"
 55          )
 56      )
 57    <*> OPT.optional
 58      ( OPT.option
 59          OPT.auto
 60          ( OPT.long "random-seed"
 61              <> OPT.short 'r'
 62              <> OPT.help "Initial seed to for the random number generator"
 63          )
 64      )
 65    <*> OPT.optional
 66      ( OPT.strOption
 67          ( OPT.long optTestCases
 68              <> OPT.short 't'
 69              <> OPT.metavar "FILE"
 70              <> OPT.help "Directory to write generate test inputs to"
 71          )
 72      )
 73    <*> OPT.switch
 74      ( OPT.long "exit-on-error"
 75          <> OPT.short 'e'
 76          <> OPT.help "Stop exploration after encountering the first error"
 77      )
 78    <*> OPT.switch
 79      ( OPT.long "write-all"
 80          <> OPT.short 'a'
 81          <> OPT.help "Write tests for all paths, not just those with errors"
 82      )
 83    <*> OPT.switch
 84      ( OPT.long "verbose"
 85          <> OPT.short 'v'
 86          <> OPT.help "Enable more verbose output"
 87      )
 88    <*> CMD.basicArgs
 89
 90------------------------------------------------------------------------
 91
 92data LogLevel = LogAll | LogErr
 93  deriving (Show, Eq, Ord)
 94
 95data KTestConf
 96  = KTestConf
 97  { confLevel :: LogLevel,
 98    confPath :: FilePath,
 99    confName :: String
100  }
101  deriving (Show)
102
103mkKTestConf :: LogLevel -> FilePath -> String -> IO KTestConf
104mkKTestConf level directory name = do
105  createDirectoryIfMissing True directory
106  pure $ KTestConf level directory name
107
108writeAssign :: Maybe KTestConf -> LogLevel -> Int -> Assign -> IO ()
109writeAssign Nothing _ _ _ = pure ()
110writeAssign (Just conf) level pathID assign
111  | level >= confLevel conf = writeKTest conf pathID (fromAssign assign)
112  | otherwise = pure ()
113
114testCasePath :: KTestConf -> Int -> FilePath
115testCasePath (KTestConf {confPath = directory}) n =
116  addExtension
117    (directory </> ("test" ++ printf "%06d" n))
118    ".ktest"
119
120writeKTest :: KTestConf -> Int -> [KTestObj] -> IO ()
121writeKTest conf@(KTestConf {confName = name}) pathID =
122  writeKTest' pathID . KTest [fromString name]
123  where
124    writeKTest' :: Int -> KTest -> IO ()
125    writeKTest' n ktest = do
126      flip encodeFile ktest $
127        testCasePath conf n
128
129------------------------------------------------------------------------
130
131handleError :: Opts -> Maybe KTestConf -> Int -> EvalError -> IO ()
132handleError opts ktest n err = do
133  printErr
134  when (optErrExit opts) $
135    die "Exiting due to encountered error"
136  where
137    printErr = do
138      hPutStrLn stderr $
139        "Encoundered error on path #"
140          ++ show n
141          ++ ": "
142          ++ show err
143          ++ "\n"
144          ++ "↳ "
145          ++ printPath ktest
146
147    printPath :: Maybe KTestConf -> String
148    printPath Nothing = "Pass --" ++ optTestCases ++ " to generate test case"
149    printPath (Just kt) =
150      "Refer to the KTest file in " ++ show (testCasePath kt n)
151
152exploreEntry :: Opts -> Maybe KTestConf -> Engine -> QBE.FuncDef -> IO Int
153exploreEntry opts ktest engine entry =
154  evalStateT (go 1 $ execFunc entry []) engine
155  where
156    go n st = do
157      when (optVerbose opts) $
158        liftIO (putStrLn $ "Exploring path " ++ show n ++ "...")
159      morePaths <- explorePath st
160
161      lastPath <- gets expLastPath
162      logLevel <- case pathErr lastPath of
163        Just err -> liftIO $ do
164          handleError opts ktest n err
165          pure LogErr
166        Nothing -> pure LogAll
167
168      liftIO $ writeAssign ktest logLevel n (pathVars lastPath)
169      if morePaths
170        then go (n + 1) st
171        else pure n
172
173exploreFile :: Opts -> IO Int
174exploreFile opts@Opts {optBase = base} = do
175  (prog, func) <- CMD.parseEntryFile $ CMD.optQBEFile base
176
177  let binName = CMD.optQBEFile $ optBase opts
178      logLevel = if optWriteAll opts then LogAll else LogErr
179  ktest <-
180    case optTestDir opts of
181      Just dir -> do
182        Just <$> mkKTestConf logLevel dir binName
183      Nothing -> pure Nothing
184
185  env <- mkEnv prog (CMD.optMemStart base) (CMD.optMemSize base) (optSeed opts)
186  case optLog opts of
187    Just fn -> withFile fn WriteMode (exploreWithHandle ktest env func)
188    Nothing -> do
189      engine <- newEngine env <$> defSolver
190      exploreEntry opts ktest engine func
191  where
192    exploreWithHandle ktest env func handle = do
193      engine <- newEngine env <$> logSolver handle
194      exploreEntry opts ktest engine func
195
196------------------------------------------------------------------------
197
198cmd :: OPT.ParserInfo Opts
199cmd =
200  OPT.info
201    (optsParser OPT.<**> OPT.helper)
202    ( OPT.fullDesc
203        <> OPT.progDesc "Symbolic execution of programs in the QBE intermediate language"
204    )
205
206main :: IO ()
207main = do
208  numPaths <- OPT.execParser cmd >>= exploreFile
209  putStrLn $ "\n---\nAmount of paths: " ++ show numPaths