diff --git a/bench/SMT.hs b/bench/SMT.hs --- a/bench/SMT.hs +++ b/bench/SMT.hs @@ -11,6 +11,7 @@ import Language.QBE.Simulator.Explorer (PathResult, exploreFunc, logSolver, newEngine) import Language.QBE.Types qualified as QBE import SMTUnwind (unwind) +import SimpleBV qualified as SMT import System.Exit (ExitCode (ExitSuccess)) import System.FilePath (()) import System.IO (IOMode (WriteMode), hClose, hPutStrLn, openFile, withFile) @@ -39,8 +40,10 @@ where exploreFunc' prog func handle = do defEnv <- mkEnv prog 0 128 (Just 0) - engine <- newEngine defEnv <$> logSolver handle - exploreFunc engine func [] + solver <- logSolver handle + + let engine = newEngine defEnv solver + exploreFunc engine func [] <* SMT.stop solver getQueries :: String -> IO String getQueries name = do diff --git a/qute-symex.cabal b/qute-symex.cabal --- a/qute-symex.cabal +++ b/qute-symex.cabal @@ -1,6 +1,6 @@ cabal-version: 3.4 name: qute-symex -version: 0.1.0 +version: 0.1.1 synopsis: A symbolic execution engine for the QBE intermediate language. description: Based on the formal semantics of the [Qute](https://hackage.haskell.org/package/qute) package, @@ -29,7 +29,8 @@ ghc-options: -Wall common opts - ghc-options: -fspecialise-aggressively + -- -threaded required by simple-smt, see . + ghc-options: -fspecialise-aggressively -threaded library import: warnings, opts @@ -86,7 +87,7 @@ qute-symex test-suite qute-symex-test - import: warnings + import: warnings, opts default-language: GHC2021 type: exitcode-stdio-1.0 hs-source-dirs: test diff --git a/src/Language/QBE/Simulator/Explorer.hs b/src/Language/QBE/Simulator/Explorer.hs --- a/src/Language/QBE/Simulator/Explorer.hs +++ b/src/Language/QBE/Simulator/Explorer.hs @@ -92,6 +92,8 @@ expLastPath :: PathResult } +-- | Create a new t'Engine', the caller is responsible for calling +-- 'SimpleBV.stop' on the given 'SimpleBV.Solver'. newEngine :: Env -> SMT.Solver -> Engine newEngine env solver = Engine diff --git a/src/SimpleBV.hs b/src/SimpleBV.hs --- a/src/SimpleBV.hs +++ b/src/SimpleBV.hs @@ -5,7 +5,7 @@ module SimpleBV ( SExpr, - SMT.Solver, + SMT.Solver (..), SMT.defaultConfig, SMT.newLogger, SMT.newLoggerWithHandle, diff --git a/test/Backend.hs b/test/Backend.hs --- a/test/Backend.hs +++ b/test/Backend.hs @@ -14,6 +14,7 @@ import Language.QBE.Simulator.Explorer (defSolver) import Language.QBE.Simulator.Symbolic.Expression qualified as SE import Language.QBE.Types qualified as QBE +import SimpleBV qualified as SMT import System.Random (initStdGen) import Test.Tasty import Test.Tasty.HUnit @@ -39,6 +40,7 @@ let s5 = fst $ ST.getConcolic s4 "a" (QBE.Base QBE.Word) _ <- ST.finalize solver s5 + _ <- SMT.stop solver assertBool "finalize does not throw an exception" True ] @@ -95,6 +97,8 @@ assertBool "condition must be /= 0" (v /= 0) _ -> assertFailure "unexpected model" + _ <- SMT.stop s + -- There are only two branches: input == 0 and input /= 0 (nxt, _) <- findUnexplored s inputs nextPathSel nxt @?= Nothing, @@ -123,6 +127,7 @@ \ret\n\ \}" + _ <- SMT.stop s length t @?= 2 ] diff --git a/test/Explorer.hs b/test/Explorer.hs --- a/test/Explorer.hs +++ b/test/Explorer.hs @@ -19,6 +19,7 @@ newEngine, ) import Language.QBE.Types qualified as QBE +import SimpleBV qualified as SMT import System.FilePath (()) import Test.Tasty import Test.Tasty.HUnit @@ -35,9 +36,11 @@ explore' :: Program -> QBE.FuncDef -> [(String, QBE.BaseType)] -> IO [PathResult] explore' prog entry params = do defEnv <- mkEnv prog 0 128 Nothing - engine <- newEngine defEnv <$> defSolver + solver <- defSolver + let engine = newEngine defEnv solver - exploreFunc engine entry $ map (second QBE.Base) params + res <- exploreFunc engine entry $ map (second QBE.Base) params + SMT.stop solver >> pure res getFuncAndProg :: FilePath -> QBE.GlobalIdent -> IO (Program, QBE.FuncDef) getFuncAndProg fileName funcName = diff --git a/test/Golden.hs b/test/Golden.hs --- a/test/Golden.hs +++ b/test/Golden.hs @@ -9,6 +9,7 @@ import Language.QBE.Simulator.Concolic.State (mkEnv) import Language.QBE.Simulator.Explorer (defSolver, exploreFunc, newEngine) import Language.QBE.Types qualified as QBE +import SimpleBV qualified as SMT import System.FilePath import Test.Tasty import Test.Tasty.Golden.Advanced @@ -23,12 +24,14 @@ (prog, func) <- readFile filePath >>= parseAndFind entryFunc defEnv <- mkEnv prog 0 128 Nothing - engine <- newEngine defEnv <$> defSolver + solver <- defSolver + let engine = newEngine defEnv solver traces <- exploreFunc engine func $ map (second QBE.Base) params - pure $ length traces + + SMT.stop solver >> pure (length traces) simpleCmp :: Result -> Result -> IO (Maybe String) simpleCmp expt act = diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -1,4 +1,4 @@ --- SPDX-FileCopyrightText: 2025 Sören Tempel +-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel -- -- SPDX-License-Identifier: GPL-3.0-only @@ -7,13 +7,22 @@ import BV (bvTests) import Backend (backendTests) import Concolic qualified as CE +import Control.Exception (IOException, try) +import Data.Either (isLeft) import Explorer (exploreTests) import Golden (goldenTests) +import Language.QBE.Simulator.Explorer (defSolver) +import SimpleBV qualified as SMT import Symbolic qualified as SE +import System.IO (hPutStrLn, stderr) import Test.Tasty main :: IO () -main = defaultMain tests +main = do + solver <- try defSolver :: IO (Either IOException SMT.Solver) + if isLeft solver + then hPutStrLn stderr "WARNING: No solver found, skipping tests!" + else defaultMain tests tests :: TestTree tests = diff --git a/test/Symbolic.hs b/test/Symbolic.hs --- a/test/Symbolic.hs +++ b/test/Symbolic.hs @@ -35,10 +35,13 @@ eqConcrete (Just sym) (Just con) = do s <- getSolver symVal <- SMT.getValue s (SE.toSExpr sym) - case (symVal, con) of - (SMT.Bits 32 sv, DE.VWord cv) -> pure $ sv == fromIntegral cv - (SMT.Bits 64 sv, DE.VLong cv) -> pure $ sv == fromIntegral cv - _ -> pure False + + let res = + case (symVal, con) of + (SMT.Bits 32 sv, DE.VWord cv) -> sv == fromIntegral cv + (SMT.Bits 64 sv, DE.VLong cv) -> sv == fromIntegral cv + _ -> False + SMT.stop s >> pure res eqConcrete Nothing Nothing = pure True eqConcrete _ _ = pure False @@ -188,6 +191,7 @@ s <- getSolver let bytes = (MEM.toBytes (E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector) :: [SE.BitVector]) values <- mapM (SMT.getValue s . SE.toSExpr) bytes + _ <- SMT.stop s values @?= [SMT.Bits 8 0xef, SMT.Bits 8 0xbe, SMT.Bits 8 0xad, SMT.Bits 8 0xde], testCase "Convert bitvector to bytes and back" $ do @@ -199,6 +203,7 @@ value <- case MEM.fromBytes (QBE.LBase QBE.Word) bytes of Just x -> SMT.getValue s (SE.toSExpr x) <&> Just Nothing -> pure Nothing + _ <- SMT.stop s value @?= Just (SMT.Bits 32 0xdeadbeef) ] @@ -214,6 +219,7 @@ let v2 = E.fromLit (QBE.Base QBE.Word) 128 expr <- SMT.getValue s (SE.toSExpr $ fromJust $ v1 `E.add` v2) + _ <- SMT.stop s expr @?= SMT.Bits 32 0xff, testCase "add incompatible values" $ do @@ -236,6 +242,8 @@ ext2Val <- SMT.getValue s (SE.toSExpr ext2) ext2Val @?= SMT.Bits 32 0xffffffab + _ <- SMT.stop s + let v3 = E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector E.extend (QBE.Base QBE.Word) True v3 @?= Nothing E.extend QBE.Byte True v3 @?= Nothing, @@ -252,6 +260,8 @@ let ex2 = fromJust $ E.extract QBE.HalfWord value ex2Val <- SMT.getValue s (SE.toSExpr ex2) ex2Val @?= SMT.Bits 16 0xbeef + + _ <- SMT.stop s E.extract (QBE.Base QBE.Word) value @?= Just value E.extract (QBE.Base QBE.Long) value @?= Nothing diff --git a/test/Util.hs b/test/Util.hs --- a/test/Util.hs +++ b/test/Util.hs @@ -39,6 +39,8 @@ (prog, entry) <- parseAndFind (QBE.GlobalIdent funcName) input defEnv <- mkEnv prog 0 128 Nothing - engine <- newEngine defEnv <$> defSolver - exploreFunc engine entry $ - map (second QBE.Base) params + solver <- defSolver + + let engine = newEngine defEnv solver + exploreFunc engine entry (map (second QBE.Base) params) + <* SMT.stop solver