qute-symex 0.1.0 → 0.1.1

raw patch · 10 files changed

+57/−19 lines, 10 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• bench/SMT.hs +5/−2
• qute-symex.cabal +4/−3
• src/Language/QBE/Simulator/Explorer.hs +2/−0
• src/SimpleBV.hs +1/−1
• test/Backend.hs +5/−0
• test/Explorer.hs +5/−2
• test/Golden.hs +5/−2
• test/Main.hs +11/−2
• test/Symbolic.hs +14/−4
• test/Util.hs +5/−3

@@ -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

@@ -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 <https://github.com/yav/simple-smt/issues/28>.+    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

@@ -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

@@ -5,7 +5,7 @@  module SimpleBV   ( SExpr,-    SMT.Solver,+    SMT.Solver (..),     SMT.defaultConfig,     SMT.newLogger,     SMT.newLoggerWithHandle,

@@ -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     ] 

@@ -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 =

@@ -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 =

@@ -1,4 +1,4 @@--- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel <soeren+git@soeren-tempel.net> -- -- 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 =

@@ -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

@@ -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