qute

  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
131showError :: Maybe KTestConf -> Int -> EvalError -> IO ()
132showError ktest n err = printErr
133  where
134    printErr = do
135      hPutStrLn stderr $
136        "Encountered error on path #"
137          ++ show n
138          ++ ": "
139          ++ show err
140          ++ "\n"
141          ++ "-> "
142          ++ printPath ktest
143
144    printPath :: Maybe KTestConf -> String
145    printPath Nothing = "Pass --" ++ optTestCases ++ " to generate test case"
146    printPath (Just kt) =
147      "Refer to the KTest file in " ++ show (testCasePath kt n)
148
149exploreEntry :: Opts -> Maybe KTestConf -> Engine -> QBE.FuncDef -> IO Int
150exploreEntry opts ktest engine entry =
151  evalStateT (go 1 $ execFunc entry []) engine
152  where
153    go n st = do
154      when (optVerbose opts) $
155        liftIO (hPutStrLn stderr $ "Exploring path " ++ show n ++ "...")
156      morePaths <- explorePath st
157
158      lastPath <- gets expLastPath
159      logLevel <- case pathErr lastPath of
160        Just err -> liftIO $ do
161          showError ktest n err
162          pure LogErr
163        Nothing -> pure LogAll
164
165      liftIO $ do
166        writeAssign ktest logLevel n (pathVars lastPath)
167        when (optErrExit opts && logLevel == LogErr) $
168          die "Exiting due to encountered error"
169
170      if morePaths
171        then go (n + 1) st
172        else pure n
173
174exploreFile :: Opts -> IO Int
175exploreFile opts@Opts {optBase = base} = do
176  (prog, func) <- CMD.parseEntryFile $ CMD.optQBEFile base
177
178  let binName = CMD.optQBEFile $ optBase opts
179      logLevel = if optWriteAll opts then LogAll else LogErr
180  ktest <-
181    case optTestDir opts of
182      Just dir -> do
183        Just <$> mkKTestConf logLevel dir binName
184      Nothing -> pure Nothing
185
186  env <- mkEnv prog (CMD.optMemStart base) (CMD.optMemSize base) (optSeed opts)
187  case optLog opts of
188    Just fn -> withFile fn WriteMode (exploreWithHandle ktest env func)
189    Nothing -> do
190      engine <- newEngine env <$> defSolver
191      exploreEntry opts ktest engine func
192  where
193    exploreWithHandle ktest env func handle = do
194      engine <- newEngine env <$> logSolver handle
195      exploreEntry opts ktest engine func
196
197------------------------------------------------------------------------
198
199cmd :: OPT.ParserInfo Opts
200cmd =
201  OPT.info
202    (optsParser OPT.<**> OPT.helper)
203    ( OPT.fullDesc
204        <> OPT.progDesc "Symbolic execution of programs in the QBE intermediate language"
205    )
206
207main :: IO ()
208main = do
209  numPaths <- OPT.execParser cmd >>= exploreFile
210  putStrLn $ "\n---\nAmount of paths: " ++ show numPaths