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 Data.Binary (encodeFile)
  8import Data.KTest (KTest (KTest), KTestObj, fromAssign)
  9import Data.String (fromString)
 10import Language.QBE.Backend.Store qualified as ST
 11import Language.QBE.Backend.Tracer qualified as T
 12import Language.QBE.CmdLine qualified as CMD
 13import Language.QBE.Simulator.Concolic.State (mkEnv)
 14import Language.QBE.Simulator.Explorer (defSolver, explore, logSolver, newEngine)
 15import Language.QBE.Types qualified as QBE
 16import Options.Applicative qualified as OPT
 17import System.Directory (createDirectoryIfMissing)
 18import System.FilePath (addExtension, (</>))
 19import System.IO (IOMode (WriteMode), withFile)
 20import Text.Printf (printf)
 21
 22data Opts = Opts
 23  { optLog :: Maybe FilePath,
 24    optSeed :: Maybe Int,
 25    optTests :: Maybe FilePath,
 26    optBase :: CMD.BasicArgs
 27  }
 28
 29optsParser :: OPT.Parser Opts
 30optsParser =
 31  Opts
 32    <$> OPT.optional
 33      ( OPT.strOption
 34          ( OPT.long "dump-smt2"
 35              <> OPT.short 'd'
 36              <> OPT.metavar "FILE"
 37              <> OPT.help "Output queries as an SMT-LIB file"
 38          )
 39      )
 40    <*> OPT.optional
 41      ( OPT.option
 42          OPT.auto
 43          ( OPT.long "random-seed"
 44              <> OPT.short 'r'
 45              <> OPT.help "Initial seed to for the random number generator"
 46          )
 47      )
 48    <*> OPT.optional
 49      ( OPT.strOption
 50          ( OPT.long "write-tests"
 51              <> OPT.short 't'
 52              <> OPT.metavar "DIR"
 53              <> OPT.help "Write .ktest files to the given directory"
 54          )
 55      )
 56    <*> CMD.basicArgs
 57
 58------------------------------------------------------------------------
 59
 60exploreFile :: Opts -> IO [(ST.Assign, T.ExecTrace)]
 61exploreFile opts@Opts {optBase = base} = do
 62  (prog, func) <- CMD.parseEntryFile $ CMD.optQBEFile base
 63
 64  env <- mkEnv prog (CMD.optMemStart base) (CMD.optMemSize base) (optSeed opts)
 65  case optLog opts of
 66    Just fn -> withFile fn WriteMode (exploreWithHandle env func)
 67    Nothing -> do
 68      engine <- newEngine <$> defSolver
 69      explore engine env func params
 70  where
 71    params :: [(String, QBE.ExtType)]
 72    params = []
 73
 74    exploreWithHandle env func handle = do
 75      engine <- newEngine <$> logSolver handle
 76      explore engine env func params
 77
 78writeKTests :: FilePath -> FilePath -> [[KTestObj]] -> IO ()
 79writeKTests directory fileArg objs = do
 80  createDirectoryIfMissing True directory
 81  mapM_ (uncurry writeKTest) $ zip [1 ..] (map mkTestCase objs)
 82  where
 83    mkTestCase :: [KTestObj] -> KTest
 84    mkTestCase = KTest [fromString fileArg]
 85
 86    writeKTest :: Int -> KTest -> IO ()
 87    writeKTest n ktest = do
 88      flip encodeFile ktest $
 89        addExtension
 90          (directory </> ("test" ++ printf "%06d" n))
 91          ".ktest"
 92
 93main :: IO ()
 94main = do
 95  args <- OPT.execParser cmd
 96  paths <- exploreFile args
 97
 98  putStrLn $ "\n---\nAmount of paths: " ++ show (length paths)
 99  case optTests args of
100    Just dir ->
101      writeKTests dir (CMD.optQBEFile $ optBase args) $
102        map (fromAssign . fst) paths
103    Nothing -> pure ()
104  where
105    cmd :: OPT.ParserInfo Opts
106    cmd =
107      OPT.info
108        (optsParser OPT.<**> OPT.helper)
109        ( OPT.fullDesc
110            <> OPT.progDesc "Symbolic execution of programs in the QBE intermediate language"
111        )