qute-cli (empty) → 0.1.0
raw patch · 7 files changed
+604/−0 lines, 7 filesdep +basedep +binarydep +bytestring
Dependencies added: base, binary, bytestring, containers, directory, filepath, mtl, optparse-applicative, qute, qute-cli, qute-symex, qute-syntax, tasty, tasty-hunit
Files
- app/qute-symex/Main.hs +210/−0
- app/qute/Main.hs +49/−0
- qute-cli.cabal +98/−0
- src/Data/KTest.hs +120/−0
- src/Language/QBE/CmdLine.hs +58/−0
- test/KTest.hs +55/−0
- test/Main.hs +14/−0
+ app/qute-symex/Main.hs view
@@ -0,0 +1,210 @@+-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Main (main) where++import Control.Monad (when)+import Control.Monad.State.Strict (evalStateT, gets, liftIO)+import Data.Binary (encodeFile)+import Data.KTest (KTest (KTest), KTestObj, fromAssign)+import Data.String (fromString)+import Language.QBE.Backend.Store (Assign)+import Language.QBE.CmdLine qualified as CMD+import Language.QBE.Simulator (execFunc)+import Language.QBE.Simulator.Concolic.State (mkEnv)+import Language.QBE.Simulator.Error (EvalError)+import Language.QBE.Simulator.Explorer+ ( Engine (expLastPath),+ PathResult (pathErr, pathVars),+ defSolver,+ explorePath,+ logSolver,+ newEngine,+ )+import Language.QBE.Types qualified as QBE+import Options.Applicative qualified as OPT+import System.Directory (createDirectoryIfMissing)+import System.Exit (die)+import System.FilePath (addExtension, (</>))+import System.IO (IOMode (WriteMode), hPutStrLn, stderr, withFile)+import Text.Printf (printf)++data Opts = Opts+ { optLog :: Maybe FilePath,+ optSeed :: Maybe Int,+ optTestDir :: Maybe FilePath,+ optErrExit :: Bool,+ optWriteAll :: Bool,+ optVerbose :: Bool,+ optBase :: CMD.BasicArgs+ }++optTestCases :: String+optTestCases = "test-cases"++optsParser :: OPT.Parser Opts+optsParser =+ Opts+ <$> OPT.optional+ ( OPT.strOption+ ( OPT.long "dump-smt2"+ <> OPT.short 'd'+ <> OPT.metavar "FILE"+ <> OPT.help "Output queries as an SMT-LIB file"+ )+ )+ <*> OPT.optional+ ( OPT.option+ OPT.auto+ ( OPT.long "random-seed"+ <> OPT.short 'r'+ <> OPT.help "Initial seed to for the random number generator"+ )+ )+ <*> OPT.optional+ ( OPT.strOption+ ( OPT.long optTestCases+ <> OPT.short 't'+ <> OPT.metavar "FILE"+ <> OPT.help "Directory to write generate test inputs to"+ )+ )+ <*> OPT.switch+ ( OPT.long "exit-on-error"+ <> OPT.short 'e'+ <> OPT.help "Stop exploration after encountering the first error"+ )+ <*> OPT.switch+ ( OPT.long "write-all"+ <> OPT.short 'a'+ <> OPT.help "Write tests for all paths, not just those with errors"+ )+ <*> OPT.switch+ ( OPT.long "verbose"+ <> OPT.short 'v'+ <> OPT.help "Enable more verbose output"+ )+ <*> CMD.basicArgs++------------------------------------------------------------------------++data LogLevel = LogAll | LogErr+ deriving (Show, Eq, Ord)++data KTestConf+ = KTestConf+ { confLevel :: LogLevel,+ confPath :: FilePath,+ confName :: String+ }+ deriving (Show)++mkKTestConf :: LogLevel -> FilePath -> String -> IO KTestConf+mkKTestConf level directory name = do+ createDirectoryIfMissing True directory+ pure $ KTestConf level directory name++writeAssign :: Maybe KTestConf -> LogLevel -> Int -> Assign -> IO ()+writeAssign Nothing _ _ _ = pure ()+writeAssign (Just conf) level pathID assign+ | level >= confLevel conf = writeKTest conf pathID (fromAssign assign)+ | otherwise = pure ()++testCasePath :: KTestConf -> Int -> FilePath+testCasePath (KTestConf {confPath = directory}) n =+ addExtension+ (directory </> ("test" ++ printf "%06d" n))+ ".ktest"++writeKTest :: KTestConf -> Int -> [KTestObj] -> IO ()+writeKTest conf@(KTestConf {confName = name}) pathID =+ writeKTest' pathID . KTest [fromString name]+ where+ writeKTest' :: Int -> KTest -> IO ()+ writeKTest' n ktest = do+ flip encodeFile ktest $+ testCasePath conf n++------------------------------------------------------------------------++showError :: Maybe KTestConf -> Int -> EvalError -> IO ()+showError ktest n err = printErr+ where+ printErr = do+ hPutStrLn stderr $+ "Encountered error on path #"+ ++ show n+ ++ ": "+ ++ show err+ ++ "\n"+ ++ "-> "+ ++ printPath ktest++ printPath :: Maybe KTestConf -> String+ printPath Nothing = "Pass --" ++ optTestCases ++ " to generate test case"+ printPath (Just kt) =+ "Refer to the KTest file in " ++ show (testCasePath kt n)++exploreEntry :: Opts -> Maybe KTestConf -> Engine -> QBE.FuncDef -> IO Int+exploreEntry opts ktest engine entry =+ evalStateT (go 1 $ execFunc entry []) engine+ where+ go n st = do+ when (optVerbose opts) $+ liftIO (hPutStrLn stderr $ "Exploring path " ++ show n ++ "...")+ morePaths <- explorePath st++ lastPath <- gets expLastPath+ logLevel <- case pathErr lastPath of+ Just err -> liftIO $ do+ showError ktest n err+ pure LogErr+ Nothing -> pure LogAll++ liftIO $ do+ writeAssign ktest logLevel n (pathVars lastPath)+ when (optErrExit opts && logLevel == LogErr) $+ die "Exiting due to encountered error"++ if morePaths+ then go (n + 1) st+ else pure n++exploreFile :: Opts -> IO Int+exploreFile opts@Opts {optBase = base} = do+ (prog, func) <- CMD.parseEntryFile $ CMD.optQBEFile base++ let binName = CMD.optQBEFile $ optBase opts+ logLevel = if optWriteAll opts then LogAll else LogErr+ ktest <-+ case optTestDir opts of+ Just dir -> do+ Just <$> mkKTestConf logLevel dir binName+ Nothing -> pure Nothing++ env <- mkEnv prog (CMD.optMemStart base) (CMD.optMemSize base) (optSeed opts)+ case optLog opts of+ Just fn -> withFile fn WriteMode (exploreWithHandle ktest env func)+ Nothing -> do+ engine <- newEngine env <$> defSolver+ exploreEntry opts ktest engine func+ where+ exploreWithHandle ktest env func handle = do+ engine <- newEngine env <$> logSolver handle+ exploreEntry opts ktest engine func++------------------------------------------------------------------------++cmd :: OPT.ParserInfo Opts+cmd =+ OPT.info+ (optsParser OPT.<**> OPT.helper)+ ( OPT.fullDesc+ <> OPT.progDesc "Symbolic execution of programs in the QBE intermediate language"+ )++main :: IO ()+main = do+ numPaths <- OPT.execParser cmd >>= exploreFile+ putStrLn $ "\n---\nAmount of paths: " ++ show numPaths
+ app/qute/Main.hs view
@@ -0,0 +1,49 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Main (main) where++import Data.Word (Word64, Word8)+import Language.QBE.CmdLine qualified as CMD+import Language.QBE.Simulator (execFunc)+import Language.QBE.Simulator.Default.Expression qualified as DE+import Language.QBE.Simulator.Default.State (Env, mkEnv, run)+import Language.QBE.Simulator.Expression qualified as E+import Language.QBE.Types qualified as QBE+import Options.Applicative qualified as OPT+import System.Exit (ExitCode (ExitFailure, ExitSuccess), exitWith)++fromWord :: DE.RegVal -> Maybe Word64+fromWord v+ | E.getType v == QBE.Base QBE.Word = Just $ E.toWord64 v+ | otherwise = Nothing++execFile :: CMD.BasicArgs -> IO Int+execFile opts = do+ (prog, func) <- CMD.parseEntryFile $ CMD.optQBEFile opts++ env <- mkEnv prog (CMD.optMemStart opts) (CMD.optMemSize opts)+ res <- run (env :: Env DE.RegVal Word8) (execFunc func [])+ case res >>= fromWord of+ Just x -> pure $ fromIntegral x+ Nothing ->+ -- The main function emitted by the Hare compiler does not+ -- return an int. Therefore, we do not emit an error here.+ pure 0++main :: IO ()+main = do+ retVal <- OPT.execParser cmd >>= execFile+ exitWith $+ if retVal == 0+ then ExitSuccess+ else ExitFailure retVal+ where+ cmd :: OPT.ParserInfo CMD.BasicArgs+ cmd =+ OPT.info+ (CMD.basicArgs OPT.<**> OPT.helper)+ ( OPT.fullDesc+ <> OPT.progDesc "Concrete execution of programs in the QBE intermediate language"+ )
+ qute-cli.cabal view
@@ -0,0 +1,98 @@+cabal-version: 3.4+name: qute-cli+version: 0.1.0+synopsis: Command-line interface for the Qute software analysis framework.+description:+ This package provides a command-line interface for the software analysis framework+ [Qute](https://hackage.haskell.org/package/qute). Specifically, it includes a concrete+ simulator for the [QBE intermediate language](https://c9x.me/compile/) targeted by Qute+ and a [symbolic executor](https://en.wikipedia.org/wiki/Symbolic_execution) based on+ Qute's [symbolic semantics](https://hackage.haskell.org/package/qute-symex). Further,+ it provides a library with utility modules needed for this purpose. This, for example,+ includes an implementation of the [KTest format](https://notes.8pit.net/notes/c8o8.html).+license: GPL-3.0-only AND MIT+-- license-file:+author: Sören Tempel+maintainer: soeren+hackage@soeren-tempel.net+-- copyright:+category: Language+build-type: Simple+homepage: https://git.8pit.net/qute+bug-reports: https://github.com/nmeum/qute/issues++source-repository head+ type: git+ location: https://git.8pit.net/qute.git++common warnings+ -- -Wall-missed-specializations can be useful too+ ghc-options: -Wall++common opts+ ghc-options: -fspecialise-aggressively++library+ import: warnings, opts+ hs-source-dirs: src+ default-language: GHC2021++ build-depends:+ base >= 4.16.4.0 && < 4.23,+ binary >= 0.8.9.0 && < 0.9,+ bytestring >= 0.11.4.0 && < 0.13,+ containers >= 0.6.5.1 && < 0.9,+ qute == 0.1.*,+ qute-symex == 0.1.*,+ qute-syntax == 0.1.*,+ optparse-applicative >=0.17.0.0 && < 0.20++ exposed-modules:+ Data.KTest,+ Language.QBE.CmdLine++executable qute+ import: warnings, opts+ main-is: Main.hs+ hs-source-dirs: app/qute+ default-language: GHC2021+ build-depends:+ base,+ qute,+ qute-cli,+ qute-syntax,+ optparse-applicative++executable qute-symex+ import: warnings, opts+ main-is: Main.hs+ hs-source-dirs: app/qute-symex+ default-language: GHC2021+ build-depends:+ base,+ qute,+ qute-cli,+ qute-symex,+ qute-syntax,+ mtl >= 2.2.2 && < 2.4,+ filepath >= 1.4.2.2 && < 1.6,+ binary,+ directory >= 1.3.6.2 && < 1.4,+ optparse-applicative++test-suite qute-cli-test+ import: warnings+ default-language: GHC2021+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ main-is: Main.hs++ other-modules:+ KTest++ build-depends:+ base,+ binary,+ bytestring,+ qute-cli,+ tasty >=1.4.3,+ tasty-hunit >=0.10
+ src/Data/KTest.hs view
@@ -0,0 +1,120 @@+-- SPDX-FileCopyrightText: 2026 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Data.KTest+ ( KTest (..),+ KTestObj (..),+ fromAssign,+ )+where++import Control.Monad (forM_, void, when)+import Data.Binary (Binary (get, put))+import Data.Binary.Get (getLazyByteString, getWord32be)+import Data.Binary.Put (putLazyByteString, putWord32be)+import Data.ByteString.Lazy qualified as BL+import Data.Map qualified as Map+import Data.String (fromString)+import Data.Word (Word32)+import Language.QBE.Backend.Store (Assign)+import Language.QBE.Simulator.Default.Expression qualified as DE+import Language.QBE.Simulator.Memory (toBytes)++newtype KTestString+ = KTestString BL.ByteString+ deriving (Show, Eq)++instance Binary KTestString where+ put (KTestString bs) =+ putWord32be (fromIntegral $ BL.length bs) >> putLazyByteString bs++ get = do+ len <- getWord32be+ str <- getLazyByteString (fromIntegral len)+ pure $ KTestString str++------------------------------------------------------------------------++data KTestObj+ = KTestObj+ { objName :: BL.ByteString,+ objBytes :: BL.ByteString+ }+ deriving (Show, Eq)++instance Binary KTestObj where+ put (KTestObj name bytes) = do+ put (KTestString name)+ put (KTestString bytes)++ get = do+ (KTestString name) <- get+ (KTestString bytes) <- get+ pure $ KTestObj name bytes++fromAssign :: Assign -> [KTestObj]+fromAssign assign = map go $ Map.toList assign+ where+ go :: (String, DE.RegVal) -> KTestObj+ go (name, value) =+ KTestObj (fromString name) (BL.pack $ toBytes value)++------------------------------------------------------------------------++data KTest+ = KTest+ { ktArgs :: [BL.ByteString],+ ktObjs :: [KTestObj]+ }+ deriving (Show, Eq)++header :: BL.ByteString+header = fromString "KTEST"++legacyHeader :: BL.ByteString+legacyHeader = fromString "BOUT\n"++version :: Word32+version = 3++instance Binary KTest where+ get = do+ hdr <- getLazyByteString (BL.length header)+ when (hdr /= header && hdr /= legacyHeader) $+ fail "invalid ktest header"+ ver <- getWord32be+ when (ver > version) $+ fail "unsupported ktest version"++ numArgs <- getWord32be+ strs <-+ mapM+ ( \_ -> do+ (KTestString s) <- get+ pure s+ )+ [1 .. numArgs]++ when (ver >= 2) $+ -- XXX: Skip symArgvs and symArgvLen for now.+ void (getWord32be >> getWord32be)++ numObjs <- getWord32be+ objs <- mapM (const get) [1 .. numObjs]++ pure $ KTest strs objs++ put (KTest args objs) = do+ putLazyByteString header+ putWord32be version++ putWord32be (fromIntegral $ length args)+ forM_ args (put . KTestString)++ -- XXX: Skip symArgvs and symArgvLen for now.+ putWord32be 0+ putWord32be 0++ putWord32be (fromIntegral $ length objs)+ forM_ objs put
+ src/Language/QBE/CmdLine.hs view
@@ -0,0 +1,58 @@+-- SPDX-FileCopyrightText: 2024 University of Bremen+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: MIT AND GPL-3.0-only++module Language.QBE.CmdLine+ ( BasicArgs (..),+ basicArgs,+ entryFunc,+ parseEntryFile,+ )+where++import Language.QBE (Program, parseAndFind)+import Language.QBE.Simulator.Memory qualified as MEM+import Language.QBE.Types qualified as QBE+import Options.Applicative qualified as OPT++-- | t'BasicArgs' can be combined/extended with additional parsers using+-- the '<*>' applicative operator provided by "Options.Applicative".+data BasicArgs = BasicArgs+ { -- | Start address of the general-purpose memory.+ optMemStart :: MEM.Address,+ -- | Size of the memory in bytes.+ optMemSize :: MEM.Size,+ -- | Path to the QBE input file.+ optQBEFile :: FilePath+ }++-- | "Options.Applicative" parser for t'BasicArgs'.+basicArgs :: OPT.Parser BasicArgs+basicArgs =+ BasicArgs+ <$> OPT.option+ OPT.auto+ ( OPT.long "memory-start"+ <> OPT.short 'm'+ <> OPT.value 0x10000+ )+ <*> OPT.option+ OPT.auto+ ( OPT.long "memory-size"+ <> OPT.short 's'+ <> OPT.value (1024 * 1024) -- 1 MB RAM+ <> OPT.help "Size of the memory region"+ )+ <*> OPT.argument OPT.str (OPT.metavar "FILE")++------------------------------------------------------------------------++-- | Name of the entry function.+entryFunc :: QBE.GlobalIdent+entryFunc = QBE.GlobalIdent "main"++-- | Parse a file and find the 'entryFunc'.+parseEntryFile :: FilePath -> IO (Program, QBE.FuncDef)+parseEntryFile filePath =+ readFile filePath >>= parseAndFind entryFunc
+ test/KTest.hs view
@@ -0,0 +1,55 @@+-- SPDX-FileCopyrightText: 2026 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only+{-# LANGUAGE OverloadedStrings #-}++module KTest (ktestTests) where++import Data.Binary (decode, encode)+import Data.ByteString.Lazy qualified as BL+import Data.KTest+import Test.Tasty+import Test.Tasty.HUnit++rawDecode :: FilePath -> IO (KTest, BL.ByteString)+rawDecode fp = do+ content <- BL.readFile fp+ pure (decode content, content)++------------------------------------------------------------------------++ktestTests :: TestTree+ktestTests =+ testGroup+ "KTest"+ [ testCase "single-variable.ktest" $ do+ (ktest, content) <- rawDecode "test/testdata/single-variable.ktest"++ let expected =+ KTest+ { ktArgs = ["shift-test.bc"],+ ktObjs =+ [ KTestObj+ { objName = "x",+ objBytes = "\NUL\NUL\NUL\NUL"+ }+ ]+ }++ ktest @?= expected+ encode expected @?= content,+ testCase "multiple-variables.ktest" $ do+ (ktest, content) <- rawDecode "test/testdata/multiple-variables.ktest"++ let expected =+ KTest+ { ktArgs = ["main.bc"],+ ktObjs =+ [ KTestObj "first" "\NUL\NUL\NUL@",+ KTestObj "second" "\SOH\NUL\NUL@"+ ]+ }++ ktest @?= expected+ encode expected @?= content+ ]
+ test/Main.hs view
@@ -0,0 +1,14 @@+-- SPDX-FileCopyrightText: 2026 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Main (main) where++import KTest (ktestTests)+import Test.Tasty++main :: IO ()+main = defaultMain tests++tests :: TestTree+tests = testGroup "Tests" [ktestTests]