packages feed

qute-symex (empty) → 0.1.0

raw patch · 24 files changed

+2896/−0 lines, 24 filesdep +basedep +containersdep +criterion

Dependencies added: base, containers, criterion, deepseq, directory, exceptions, filepath, mtl, process, qute, qute-symex, qute-syntax, random, simple-smt, tasty, tasty-golden, tasty-hunit, tasty-quickcheck

Files

+ bench/Exec.hs view
@@ -0,0 +1,41 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: MIT AND GPL-3.0-only++module Exec (execBench) where++import Control.Monad (void)+import Criterion.Main (Benchmark, Benchmarkable, bench, bgroup, nfIO)+import Data.Word (Word64, Word8)+import Language.QBE (parseAndFind)+import Language.QBE.Simulator (execFunc)+import Language.QBE.Simulator.Concolic.Expression qualified as CE+import Language.QBE.Simulator.Default.Expression qualified as DE+import Language.QBE.Simulator.Default.State (SimState, mkEnv, run)+import Language.QBE.Simulator.Expression qualified as E+import Language.QBE.Types qualified as QBE++exec :: [CE.Concolic DE.RegVal] -> String -> IO ()+exec params input = do+  (prog, func) <- parseAndFind entryFunc input++  env <- mkEnv prog 0 1024+  void $ run env (execFunc func params :: SimState (CE.Concolic DE.RegVal) (CE.Concolic Word8) (Maybe (CE.Concolic DE.RegVal)))+  where+    entryFunc :: QBE.GlobalIdent+    entryFunc = QBE.GlobalIdent "entry"++------------------------------------------------------------------------++bubbleSort :: Word64 -> Benchmarkable+bubbleSort inputSize =+  nfIO (readFile "bench/data/Exec/bubble-sort.qbe" >>= exec [E.fromLit (QBE.Base QBE.Word) inputSize])++execBench :: Benchmark+execBench =+  bgroup+    "Concrete Execution"+    [ bench "10" $ bubbleSort 25,+      bench "50" $ bubbleSort 50,+      bench "100" $ bubbleSort 100+    ]
+ bench/Main.hs view
@@ -0,0 +1,12 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: MIT AND GPL-3.0-only++module Main (main) where++import Criterion.Main (defaultMain)+import Exec (execBench)+import SMT (smtBench)++main :: IO ()+main = defaultMain [execBench, smtBench]
+ bench/SMT.hs view
@@ -0,0 +1,79 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: MIT AND GPL-3.0-only++module SMT (smtBench) where++import Control.Monad (when)+import Criterion.Main+import Language.QBE (parseAndFind)+import Language.QBE.Simulator.Concolic.State (mkEnv)+import Language.QBE.Simulator.Explorer (PathResult, exploreFunc, logSolver, newEngine)+import Language.QBE.Types qualified as QBE+import SMTUnwind (unwind)+import System.Exit (ExitCode (ExitSuccess))+import System.FilePath ((</>))+import System.IO (IOMode (WriteMode), hClose, hPutStrLn, openFile, withFile)+import System.Process+  ( StdStream (CreatePipe, UseHandle),+    createProcess,+    proc,+    std_in,+    std_out,+    waitForProcess,+  )++logPath :: FilePath+logPath = "/tmp/qute-symex-bench.smt2"++entryFunc :: QBE.GlobalIdent+entryFunc = QBE.GlobalIdent "main"++------------------------------------------------------------------------++exploreQBE :: FilePath -> IO [PathResult]+exploreQBE filePath = do+  (prog, func) <- readFile filePath >>= parseAndFind entryFunc++  withFile logPath WriteMode (exploreFunc' prog func)+  where+    exploreFunc' prog func handle = do+      defEnv <- mkEnv prog 0 128 (Just 0)+      engine <- newEngine defEnv <$> logSolver handle+      exploreFunc engine func []++getQueries :: String -> IO String+getQueries name = do+  _ <- exploreQBE ("bench" </> "data" </> "SMT" </> name)+  -- XXX: Uncomment this to benchmark incremental solving instead.+  unwind logPath++solveQueries :: String -> IO ()+solveQueries queries = do+  devNull <- openFile "/dev/null" WriteMode+  (Just hin, _, _, p) <-+    createProcess+      (proc "bitwuzla" [])+        { std_in = CreatePipe,+          std_out = UseHandle devNull+        }++  hPutStrLn hin queries <* hClose hin+  ret <- waitForProcess p <* hClose devNull+  when (ret /= ExitSuccess) $+    error "SMT solver failed"++smtBench :: Benchmark+smtBench = do+  bgroup+    "SMT Complexity"+    [ benchWithEnv "prime-numbers.qbe",+      benchWithEnv "bubble-sort.qbe",+      benchWithEnv "insertion-sort-uchar.qbe"+    ]+  where+    benchSolver :: String -> String -> Benchmark+    benchSolver name queries = bench name $ nfIO (solveQueries queries)++    benchWithEnv :: String -> Benchmark+    benchWithEnv name = env (getQueries name) (benchSolver name)
+ bench/SMTUnwind.hs view
@@ -0,0 +1,100 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: MIT AND GPL-3.0-only++module SMTUnwind (unwind) where++import Control.Monad (forM_)+import Control.Monad.State.Strict (State, gets, modify, runState)+import Data.Functor ((<&>))+import SimpleSMT qualified as SMT++data UnwindEnv+  = UnwindEnv+  { assertStack :: [[SMT.SExpr]],+    exprs :: [SMT.SExpr],+    queries :: [[SMT.SExpr]]+  }+  deriving (Show, Eq)++mkUnwindEnv :: UnwindEnv+mkUnwindEnv = UnwindEnv [] [] []++------------------------------------------------------------------------++newAssertLevel :: State UnwindEnv ()+newAssertLevel =+  modify (\s -> s {assertStack = [] : assertStack s})++popAssertLevel :: State UnwindEnv ()+popAssertLevel = modify go+  where+    go s@UnwindEnv {assertStack = []} = s+    go s@UnwindEnv {assertStack = _ : xs} = s {assertStack = xs}++addAssertion :: [SMT.SExpr] -> State UnwindEnv ()+addAssertion assertions = do+  stk <- gets assertStack+  let newStk = case stk of+        (x : xs) -> (x ++ assertions) : xs+        [] -> [assertions]+  modify (\s -> s {assertStack = newStk})++addExpr :: SMT.SExpr -> State UnwindEnv ()+addExpr expr =+  modify (\s -> s {exprs = exprs s ++ [expr]})++getAsserts :: State UnwindEnv [SMT.SExpr]+getAsserts = gets (concat . reverse . assertStack)++completeQuery :: State UnwindEnv ()+completeQuery =+  modify+    ( \s ->+        s+          { queries = queries s ++ [exprs s],+            exprs = []+          }+    )++transExpr :: SMT.SExpr -> State UnwindEnv ()+transExpr (SMT.List [SMT.Atom "push", SMT.Atom arg]) = do+  let num = (read arg :: Integer)+  forM_ [1 .. num] (const newAssertLevel)+transExpr (SMT.List [SMT.Atom "pop", SMT.Atom arg]) = do+  let num = (read arg :: Integer)+  forM_ [1 .. num] (const popAssertLevel)+transExpr (SMT.List ((SMT.Atom "assert") : xs)) =+  addAssertion xs+transExpr (SMT.List [SMT.Atom "check-sat"]) = do+  asserts <- getAsserts+  addExpr $ SMT.List [SMT.Atom "check-sat-assuming", SMT.List asserts]+  completeQuery+transExpr (SMT.List ((SMT.Atom "get-value") : _)) = pure ()+transExpr expr = addExpr expr++transform :: [SMT.SExpr] -> State UnwindEnv ()+transform sexprs = forM_ sexprs transExpr++------------------------------------------------------------------------++readSExprs :: String -> [SMT.SExpr]+readSExprs str = go (SMT.readSExpr str)+  where+    go :: Maybe (SMT.SExpr, String) -> [SMT.SExpr]+    go Nothing = []+    go (Just (acc, rest)) = acc : go (SMT.readSExpr rest)++getQueries :: [SMT.SExpr] -> [[SMT.SExpr]]+getQueries exprs = queries (snd $ runTransform exprs)+  where+    runTransform e = runState (transform e) mkUnwindEnv++unwind :: FilePath -> IO String+unwind origFp = do+  exprs <- readFile origFp <&> readSExprs+  let queries = getQueries exprs+  pure $ serialize (concat queries)+  where+    serialize :: [SMT.SExpr] -> String+    serialize = unlines . map (`SMT.showsSExpr` "")
+ qute-symex.cabal view
@@ -0,0 +1,116 @@+cabal-version:      3.4+name:               qute-symex+version:            0.1.0+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,+  this library provides a [symbolic execution](https://en.wikipedia.org/wiki/Symbolic_execution)+  engine for the QBE intermediate language. Thereby, it enables formal reasoning about a software+  under test using [SMT solvers](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories).++  The underlying vision behind Qute's symbolic execution engine is further described in a+  [separate paper](https://www.ibr.cs.tu-bs.de/vss/Publications/2026/tempel_26_qute.pdf).+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+    -- other-modules:+    hs-source-dirs:   src+    default-language: GHC2021++    build-depends:+      base >= 4.16.4.0 && < 4.23,+      deepseq >= 1.4.6.1 && < 1.6,+      mtl >= 2.2.2 && < 2.4,+      directory >= 1.3.6.2 && < 1.4,+      containers >= 0.6.5.1 && < 0.9,+      exceptions >= 0.10.4 && < 0.11,+      random >= 1.2.1.1 && < 1.4,+      qute == 0.1.*,+      qute-syntax == 0.1.*,+      simple-smt >= 0.9.8 && < 0.10++    exposed-modules:+      SimpleBV,+      Language.QBE.Backend,+      Language.QBE.Backend.Model,+      Language.QBE.Backend.Store,+      Language.QBE.Backend.ExecTree,+      Language.QBE.Backend.DFS,+      Language.QBE.Backend.Tracer,+      Language.QBE.Simulator.Explorer,+      Language.QBE.Simulator.Symbolic.Expression,+      Language.QBE.Simulator.Concolic.State,+      Language.QBE.Simulator.Concolic.Expression++benchmark qute-symex+    import:           warnings, opts+    default-language: GHC2021+    type:             exitcode-stdio-1.0+    hs-source-dirs:   bench+    main-is:          Main.hs++    other-modules:+      SMTUnwind,+      SMT,+      Exec++    build-depends:+      base,+      criterion ^>= 1.6.4.0,+      mtl,+      simple-smt,+      process,+      filepath,+      qute,+      qute-syntax,+      qute-symex++test-suite qute-symex-test+    import:           warnings+    default-language: GHC2021+    type:             exitcode-stdio-1.0+    hs-source-dirs:   test+    main-is:          Main.hs++    other-modules:+      Util,+      Golden,+      Backend,+      Explorer,+      Symbolic,+      Concolic,+      BV++    build-depends:+        base,+        filepath,+        containers,+        random,+        qute,+        qute-syntax,+        qute-symex,+        simple-smt,+        tasty            >=1.4.3,+        tasty-hunit      >=0.10,+        tasty-golden     >=2.3.5,+        tasty-quickcheck >=0.10.2
+ src/Language/QBE/Backend.hs view
@@ -0,0 +1,30 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Language.QBE.Backend+  ( SolverError (..),+    prefixLength,+  )+where++import Control.Exception (Exception)++data SolverError+  = UnknownResult+  deriving (Show)++instance Exception SolverError++------------------------------------------------------------------------++-- | Determine the length of the common prefix of two lists.+prefixLength :: (Eq a) => [a] -> [a] -> Int+prefixLength = prefixLength' 0+  where+    prefixLength' :: (Eq a) => Int -> [a] -> [a] -> Int+    prefixLength' n [] _ = n+    prefixLength' n _ [] = n+    prefixLength' n (x : xs) (y : ys)+      | x == y = prefixLength' (n + 1) xs ys+      | otherwise = n
+ src/Language/QBE/Backend/DFS.hs view
@@ -0,0 +1,73 @@+-- 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.Backend.DFS+  ( PathSel,+    newPathSel,+    trackTrace,+    findUnexplored,+  )+where++import Control.Applicative ((<|>))+import Language.QBE.Backend.ExecTree (BTree (..), ExecTree, addTrace, mkTree)+import Language.QBE.Backend.Model qualified as Model+import Language.QBE.Backend.Tracer (Branch (..), ExecTrace, solveTrace)+import SimpleBV qualified as SMT++-- The 'PathSel' encapsulates data for the Dynamic Symbolic Execution (DSE)+-- algorithm. Specifically for path selection and incremental solving.+data PathSel+  = PathSel+      ExecTree -- The current execution tree for the DSE algorithm+      ExecTrace -- The last solved trace, for incremental solving.++-- Create a new empty 'PathSel' object without anything traced yet.+newPathSel :: PathSel+newPathSel = PathSel (mkTree []) []++-- Track a new 'ExecTrace' in the 'PathSel'.+trackTrace :: PathSel -> ExecTrace -> PathSel+trackTrace (PathSel tree t) trace =+  PathSel (addTrace tree trace) t++-- Find an assignment that causes exploration of a new execution path through+-- the tested software. This function updates the metadata in the execution+-- tree and thus returns a new execution tree, even if no satisfiable+-- assignment was found.+findUnexplored :: SMT.Solver -> [SMT.SExpr] -> PathSel -> IO (Maybe Model.Model, PathSel)+findUnexplored solver inputVars tracer@(PathSel tree oldTrace) = do+  case negateBranch tree of+    Nothing -> pure (Nothing, tracer)+    Just nt -> do+      let nextTracer = PathSel (addTrace tree nt) nt+      res <- solveTrace solver inputVars oldTrace nt+      case res of+        Nothing -> findUnexplored solver inputVars nextTracer+        Just m -> pure (Just m, nextTracer)+  where+    -- Negate an unnegated branch in the execution tree and return an+    -- 'ExecTrace' which leads to an unexplored execution path. If no+    -- such path exists, then 'Nothing' is returned. If such a path+    -- exists a concrete variable assignment for it can be calculated+    -- using 'solveTrace'.+    --+    -- The branch node metadata in the resulting 'ExecTree' is updated+    -- to reflect that negation of the selected branch node was attempted.+    -- If further branches are to be negated, the resulting trace should+    -- be added to the 'ExecTree' using 'addTrace' to update the metadata+    -- in the tree as well.+    negateBranch :: ExecTree -> Maybe ExecTrace+    negateBranch Leaf = Nothing+    negateBranch (Node (Branch wasNeg ast) Nothing _)+      | wasNeg = Nothing+      | otherwise = Just [(True, Branch True ast)]+    negateBranch (Node (Branch wasNeg ast) _ Nothing)+      | wasNeg = Nothing+      | otherwise = Just [(False, Branch True ast)]+    negateBranch (Node br (Just ifTrue) (Just ifFalse)) =+      do+        (++) [(True, br)] <$> negateBranch ifTrue+        <|> (++) [(False, br)] <$> negateBranch ifFalse
+ src/Language/QBE/Backend/ExecTree.hs view
@@ -0,0 +1,83 @@+-- 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.Backend.ExecTree+  ( BTree (..),+    ExecTree,+    mkTree,+    addTrace,+  )+where++import Language.QBE.Backend.Tracer (Branch, ExecTrace, fromBranch)++-- A binary tree.+data BTree a = Node a (Maybe (BTree a)) (Maybe (BTree a)) | Leaf+  deriving (Show, Eq)++-- Execution tree for the exeucted software, represented as follows:+--+--                                 a+--                          True  / \  False+--                               b   …+--                              / \+--                             N   L+--+-- where the edges indicate what happens if branch a is true/false.+-- The left edge covers the true path while the right edge covers the+-- false path.+--+-- The Nothing (N) value indicates that a path has not been explored.+-- In the example above the path `[(True, a), (True, b)]` has not been+-- explored. A Leaf (L) node is used to indicate that a path has been+-- explored but we haven't discored additional branches yet. In the+-- example above the deepest path is hence `[(True a), (False, b)]`.+type ExecTree = BTree Branch++-- Returns 'True' if we can continue exploring on this branch node.+-- This is the case if the node is either a 'Leaf' or 'Nothing'.+canCont :: Maybe (BTree a) -> Bool+canCont Nothing = True+canCont (Just Leaf) = True+canCont _ = False++-- Create a new execution tree from a trace.+mkTree :: ExecTrace -> ExecTree+mkTree [] = Leaf+mkTree [(wasTrue, br)]+  | wasTrue = Node br (Just Leaf) Nothing+  | otherwise = Node br Nothing (Just Leaf)+mkTree ((True, br) : xs) = Node br (Just $ mkTree xs) Nothing+mkTree ((False, br) : xs) = Node br Nothing (Just $ mkTree xs)++-- Add a trace to an existing execution tree. The control flow+-- in the trace must match the existing tree. If it diverges,+-- an error is raised.+--+-- This function prefers the branch nodes from the trace in the+-- resulting 'ExecTree', thus allowing updating their metadata via+-- this function.+--+-- Assertion: The branch encode in the Node and the branch encoded in+-- the trace should also be equal, regarding the encoded condition.+addTrace :: ExecTree -> ExecTrace -> ExecTree+addTrace tree [] = tree+-- The trace takes the True branch and we have taken that previously.+--  ↳ Recursively decent on that branch and look at remaining trace.+addTrace (Node br' (Just tb) fb) ((True, br) : xs) =+  Node (fromBranch br' br) (Just $ addTrace tb xs) fb+-- The trace takes the False branch and we have taken that previously.+--  ↳ Recursively decent on that branch and look at remaining trace.+addTrace (Node br' tb (Just fb)) ((False, br) : xs) =+  Node (fromBranch br' br) tb (Just $ addTrace fb xs)+-- If the trace takes the True/False branch and we have not taken that+-- yet (i.e. canCont is True) we insert the trace at that position.+addTrace (Node br' tb fb) ((wasTrue, br) : xs)+  | canCont tb && wasTrue = Node (fromBranch br' br) (Just $ mkTree xs) fb+  | canCont fb && not wasTrue = Node (fromBranch br' br) tb (Just $ mkTree xs)+  | otherwise = error "unreachable"+-- If we encounter a leaf, this part hasn't been explored yet.+-- That is, we can just insert the trace "as is" at this point.+addTrace Leaf trace = mkTree trace
+ src/Language/QBE/Backend/Model.hs view
@@ -0,0 +1,31 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only+module Language.QBE.Backend.Model+  ( Model,+    toList,+    getModel,+  )+where++import Language.QBE.Simulator.Default.Expression qualified as DE+import SimpleBV qualified as SMT++-- Assignments returned by the Solver for a given query.+newtype Model = Model [(String, SMT.Value)]+  deriving (Show, Eq)++-- | Get a new 'Model.Model' for a list of input variables that should be contained in it.+getModel :: SMT.Solver -> [SMT.SExpr] -> IO Model+getModel solver inputVars = Model <$> SMT.getValues solver inputVars++-- | Convert a model to a list of concrete variable assignments.+toList :: Model -> [(String, DE.RegVal)]+toList (Model lst) = map go lst+  where+    go :: (String, SMT.Value) -> (String, DE.RegVal)+    go (name, SMT.Bits n v) =+      case DE.fromBits n v of+        Just x -> (name, x)+        Nothing -> error "invalid bitvector size"+    go _ = error "unsupported value type"
+ src/Language/QBE/Backend/Store.hs view
@@ -0,0 +1,90 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Language.QBE.Backend.Store+  ( Store (cValues),+    Assign,+    empty,+    sexprs,+    finalize,+    setModel,+    getConcolic,+  )+where++import Data.Map qualified as Map+import Language.QBE.Backend.Model qualified as Model+import Language.QBE.Simulator.Concolic.Expression qualified as CE+import Language.QBE.Simulator.Default.Expression qualified as DE+import Language.QBE.Simulator.Expression qualified as E+import Language.QBE.Simulator.Symbolic.Expression qualified as SE+import Language.QBE.Types qualified as QBE+import SimpleBV qualified as SMT+import System.Random (StdGen, genWord64R)++-- | Concrete variable assignment.+type Assign = Map.Map String DE.RegVal++-- A variable store mapping variable names to concrete values.+data Store+  = Store+  { cValues :: Assign,+    sValues :: Map.Map String SE.BitVector,+    defined :: Map.Map String SE.BitVector,+    randGen :: StdGen+  }++-- | Create a new (empty) store.+empty :: StdGen -> Store+empty = Store Map.empty Map.empty Map.empty++-- | Obtain symbolic values as a list of "SimpleBV" expressions.+sexprs :: Store -> [SMT.SExpr]+sexprs = map SE.toSExpr . Map.elems . sValues++-- | Finalize all pending symbolic variable declarations.+finalize :: SMT.Solver -> Store -> IO Store+finalize solver store@(Store {sValues = m, defined = defs}) = do+  let new = m `Map.difference` defs+  mapM_ (uncurry declareSymbolic) $ Map.toList new++  pure+    store+      { defined = Map.union defs new,+        sValues = Map.empty+      }+  where+    declareSymbolic n v =+      SMT.declareBV solver n $ SE.bitSize v++-- | Create a variable store from a 'Model.Model'.+setModel :: Store -> Model.Model -> Store+setModel store model =+  store {cValues = Map.fromList $ Model.toList model}++-- | Lookup the variable name in the store, if it doesn't exist return+-- an unconstrained 'CE.Concolic' value with a random concrete part.+getConcolic :: Store -> String -> QBE.ExtType -> (Store, CE.Concolic DE.RegVal)+getConcolic store@Store {randGen = rand} name ty =+  ( store+      { sValues = newSymVars,+        cValues = newConVars,+        randGen = nextRand+      },+    CE.Concolic concrete (Just symbolic)+  )+  where+    (symbolic, newSymVars) =+      let bv = SE.symbolic name ty+       in (bv, Map.insert name bv $ sValues store)++    (concrete, newConVars, nextRand) =+      let cm = cValues store+       in case Map.lookup name cm of+            Just cv -> (cv, cm, rand)+            Nothing ->+              let maxValue = (2 ^ QBE.extTypeBitSize ty) - 1+                  (rv, nr) = genWord64R maxValue rand+                  conValue = E.fromLit ty rv+               in (conValue, Map.insert name conValue cm, nr)
+ src/Language/QBE/Backend/Tracer.hs view
@@ -0,0 +1,102 @@+-- 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.Backend.Tracer+  ( Branch (Branch),+    newBranch,+    fromBranch,+    ExecTrace,+    newExecTrace,+    toSExprs,+    appendBranch,+    appendCons,+    solveTrace,+  )+where++import Control.Exception (throwIO)+import Control.Monad (when)+import Language.QBE.Backend (SolverError (UnknownResult), prefixLength)+import Language.QBE.Backend.Model qualified as Model+import Language.QBE.Simulator.Symbolic.Expression qualified as SE+import SimpleBV qualified as SMT++-- Represents a branch condition in the executed code+data Branch+  = Branch+      Bool -- Whether negation of the branch was attempted+      SE.BitVector -- The symbolic branch condition+  deriving (Show, Eq)++-- Create a new branch condition.+newBranch :: SE.BitVector -> Branch+newBranch = Branch False++-- Create a new branch from an existing branch, thereby updating its metadata.+-- It is assumed that the condition, encoded in the branches, is equal.+fromBranch :: Branch -> Branch -> Branch+fromBranch (Branch wasNeg' _) (Branch wasNeg ast) =+  Branch (wasNeg || wasNeg') ast++------------------------------------------------------------------------++-- Represents a single execution through a program, tracking for each+-- symbolic branch condition if it was 'True' or 'False'.+type ExecTrace = [(Bool, Branch)]++-- Create a new empty execution tree.+newExecTrace :: ExecTrace+newExecTrace = []++-- Return all branch conditions of an 'ExecTrace'.+toSExprs :: ExecTrace -> [SMT.SExpr]+toSExprs = map (\(_, Branch _ bv) -> SE.toSExpr bv)++-- Append a branch to the execution trace, denoting via a 'Bool'+-- if the branch was taken or if it was not taken.+appendBranch :: ExecTrace -> Bool -> Branch -> ExecTrace+appendBranch trace wasTrue branch = trace ++ [(wasTrue, branch)]++-- Append a constraint to the execution tree. This constraint must+-- be true and, contrary to appendBranch, negation will not be+-- attempted for it.+appendCons :: ExecTrace -> SE.BitVector -> ExecTrace+appendCons trace cons = trace ++ [(True, Branch True cons)]++-- For a given execution trace, return an assignment (represented+-- as a 'Model.Model') which statisfies all symbolic branch conditions.+-- If such an assignment does not exist, then 'Nothing' is returned.+--+-- Throws a 'SolverError' on an unknown solver result (e.g., on timeout).+solveTrace :: SMT.Solver -> [SMT.SExpr] -> ExecTrace -> ExecTrace -> IO (Maybe Model.Model)+solveTrace solver inputVars oldTrace newTrace = do+  -- Determine the common prefix of the current trace and the old trace+  -- drop constraints beyond this common prefix from the current solver+  -- context. Thereby, keeping the common prefix and making use of+  -- incremental solving capabilities.+  let prefix = prefixLength newTrace oldTrace+  let toDrop = length oldTrace - prefix++  -- Micro optimization: When we don't have anything to drop, then+  -- don't call .popMany thereby avoiding communication with the solver.+  when (toDrop /= 0) $+    SMT.popMany solver (fromIntegral toDrop)++  -- Only enforce new constraints, i.e. those beyond the common prefix.+  assertTrace (drop prefix newTrace)++  isSat <- SMT.check solver+  case isSat of+    SMT.Sat -> Just <$> Model.getModel solver inputVars+    SMT.Unsat -> pure Nothing+    SMT.Unknown -> throwIO UnknownResult+  where+    -- Add all conditions enforced by the given 'ExecTrace' to the solver.+    -- Returns a list of all asserted conditions.+    assertTrace :: ExecTrace -> IO ()+    assertTrace [] = pure ()+    assertTrace t = do+      let conds = map (\(b, Branch _ c) -> SE.toCond b c) t+      mapM_ (\c -> SMT.push solver >> SMT.assert solver c) conds
+ src/Language/QBE/Simulator/Concolic/Expression.hs view
@@ -0,0 +1,146 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Language.QBE.Simulator.Concolic.Expression+  ( Concolic (..),+    hasSymbolic,+  )+where++import Control.DeepSeq (NFData, NFData1)+import Control.Exception (assert)+import Data.Functor ((<&>))+import Data.Maybe (fromMaybe)+import Data.Word (Word8)+import GHC.Generics (Generic, Generic1)+import Language.QBE.Simulator.Default.Expression qualified as D+import Language.QBE.Simulator.Expression qualified as E+import Language.QBE.Simulator.Memory qualified as MEM+import Language.QBE.Simulator.Symbolic.Expression qualified as SE++data Concolic v+  = Concolic+  { concrete :: v,+    symbolic :: Maybe SE.BitVector+  }+  deriving (Show, Generic, Generic1)++instance (NFData a) => NFData (Concolic a)++instance NFData1 Concolic++hasSymbolic :: Concolic v -> Bool+hasSymbolic Concolic {symbolic = Just _} = True+hasSymbolic _ = False++getSymbolicDef :: (v -> SE.BitVector) -> Concolic v -> SE.BitVector+getSymbolicDef conc Concolic {concrete = c, symbolic = s} =+  fromMaybe (conc c) s++------------------------------------------------------------------------++instance MEM.Storable (Concolic D.RegVal) (Concolic Word8) where+  toBytes Concolic {concrete = c, symbolic = s} =+    let cbytes = MEM.toBytes c+        nbytes = length cbytes+        sbytes = maybe (replicate nbytes Nothing) (map Just . MEM.toBytes) s+     in assert (nbytes == length sbytes) $+          zipWith Concolic cbytes sbytes++  fromBytes ty bytes =+    do+      let conBytes = map concrete bytes+      con <- MEM.fromBytes ty conBytes++      let mkConcolic = Concolic con+      if any hasSymbolic bytes+        then do+          let symBVs = map (getSymbolicDef SE.fromByte) bytes+          MEM.fromBytes ty symBVs <&> mkConcolic . Just+        else Just $ mkConcolic Nothing++------------------------------------------------------------------------++unaryOp ::+  (D.RegVal -> Maybe D.RegVal) ->+  (SE.BitVector -> Maybe SE.BitVector) ->+  Concolic D.RegVal ->+  Maybe (Concolic D.RegVal)+unaryOp fnCon fnSym Concolic {concrete = c, symbolic = s} = do+  c' <- fnCon c+  let con = Concolic c'+  case s of+    Just s' -> fnSym s' <&> con . Just+    Nothing -> pure $ con Nothing++binaryOp ::+  (D.RegVal -> D.RegVal -> Maybe D.RegVal) ->+  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->+  Concolic D.RegVal ->+  Concolic D.RegVal ->+  Maybe (Concolic D.RegVal)+binaryOp fnCon fnSym lhs rhs =+  do+    c <- concrete lhs `fnCon` concrete rhs+    if hasSymbolic lhs || hasSymbolic rhs+      then+        let lhsS = getSymbolicDef SE.fromReg lhs+            rhsS = getSymbolicDef SE.fromReg rhs+         in (lhsS `fnSym` rhsS) <&> Concolic c . Just+      else pure $ Concolic c Nothing++instance E.ValueRepr (Concolic D.RegVal) where+  fromLit ty v = Concolic (E.fromLit ty v) Nothing+  fromFloat fl = Concolic (E.fromFloat fl) Nothing+  fromDouble d = Concolic (E.fromDouble d) Nothing+  toWord64 Concolic {concrete = c} = E.toWord64 c+  getType Concolic {concrete = c} = E.getType c++  extend ty s = unaryOp (E.extend ty s) (E.extend ty s)+  extract ty = unaryOp (E.extract ty) (E.extract ty)++  -- TODO: Add constraint which enforces concrete value on+  -- symbolic part instead of silently discarding it. See+  -- the address concretization implementation for details.+  floatToInt ty s Concolic {concrete = c} =+    (`Concolic` Nothing) <$> E.floatToInt ty s c+  intToFloat ty s Concolic {concrete = c} =+    (`Concolic` Nothing) <$> E.intToFloat ty s c+  extendFloat Concolic {concrete = c} =+    (`Concolic` Nothing) <$> E.extendFloat c+  truncFloat Concolic {concrete = c} =+    (`Concolic` Nothing) <$> E.truncFloat c++  add = binaryOp E.add E.add+  sub = binaryOp E.sub E.sub+  mul = binaryOp E.mul E.mul+  div = binaryOp E.div E.div+  or = binaryOp E.or E.or+  xor = binaryOp E.xor E.xor+  and = binaryOp E.and E.and+  urem = binaryOp E.urem E.urem+  srem = binaryOp E.srem E.srem+  udiv = binaryOp E.udiv E.udiv++  neg = unaryOp E.neg E.neg++  sar = binaryOp E.sar E.sar+  shr = binaryOp E.shr E.shr+  shl = binaryOp E.shl E.shl++  eq = binaryOp E.eq E.eq+  ne = binaryOp E.ne E.ne+  sle = binaryOp E.sle E.sle+  slt = binaryOp E.slt E.slt+  sge = binaryOp E.sge E.sge+  sgt = binaryOp E.sgt E.sgt+  ule = binaryOp E.ule E.ule+  ult = binaryOp E.ult E.ult+  uge = binaryOp E.uge E.uge+  ugt = binaryOp E.ugt E.ugt++  -- TODO: Add constraint which enforces concrete value on+  -- symbolic part instead of silently discarding it. See+  -- the address concretization implementation for details.+  ord lhs rhs = (`Concolic` Nothing) <$> E.ord (concrete lhs) (concrete rhs)
+ src/Language/QBE/Simulator/Concolic/State.hs view
@@ -0,0 +1,219 @@+-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Language.QBE.Simulator.Concolic.State+  ( Env (..),+    mkEnv,+    run,+    runPath,+    makeConcolic,+    ErrorState (..),+    ErrorPath (..),+    SimState (..),+  )+where++import Control.Exception (Exception, throwIO, try)+import Control.Monad.Error.Class (MonadError, catchError, throwError)+import Control.Monad.IO.Class (MonadIO, liftIO)+import Control.Monad.State.Strict+  ( MonadState,+    StateT (StateT),+    evalStateT,+    get,+    gets,+    modify,+    runStateT,+  )+import Data.Map qualified as Map+import Data.Word (Word8)+import Language.QBE (Program)+import Language.QBE.Backend.Store qualified as ST+import Language.QBE.Backend.Tracer qualified as T+import Language.QBE.Simulator.Concolic.Expression qualified as CE+import Language.QBE.Simulator.Default.Expression qualified as DE+import Language.QBE.Simulator.Default.Funcs (lookupSimFunc)+import Language.QBE.Simulator.Default.State qualified as DS+import Language.QBE.Simulator.Error (EvalError (FuncArgsMismatch, TypingError))+import Language.QBE.Simulator.Expression qualified as E+import Language.QBE.Simulator.Memory qualified as MEM+import Language.QBE.Simulator.State+import Language.QBE.Simulator.Symbolic.Expression qualified as SE+import Language.QBE.Types qualified as QBE+import System.Random (initStdGen, mkStdGen)++data Env+  = Env+  { envBase :: DS.Env (CE.Concolic DE.RegVal) (CE.Concolic Word8),+    envTracer :: T.ExecTrace,+    envStore :: ST.Store+  }++mkEnv ::+  Program ->+  MEM.Address ->+  MEM.Size ->+  Maybe Int ->+  IO Env+mkEnv prog memStart memSize maySeed = do+  initEnv <- DS.mkEnv prog memStart memSize+  randGen <-+    case maySeed of+      Just sd -> pure $ mkStdGen sd+      Nothing -> initStdGen+  pure $ Env initEnv T.newExecTrace (ST.empty randGen)++liftState ::+  (DS.SimState (CE.Concolic DE.RegVal) (CE.Concolic Word8)) a ->+  SimState a+liftState (DS.SimState toLift) = do+  defEnv <- gets envBase++  -- XXX: Since 'toLift' is run in the DS.SimState monad, it would+  -- use its 'throwError' implementation here. We want to use the+  -- implementation of our t'SimState' though, hence we need to handle+  -- IO exceptions here.+  result <- liftIO $ try (runStateT toLift defEnv)+  case result of+    Left (e :: EvalError) -> throwError e+    Right (a, s) -> do+      modify (\ps -> ps {envBase = s})+      pure a++makeConcolic :: String -> QBE.ExtType -> SimState (CE.Concolic DE.RegVal)+makeConcolic name ty = do+  st <- gets envStore+  let (ns, cv) = ST.getConcolic st name ty+  modify (\e -> e {envStore = ns})+  pure cv++modifyTracer :: (MonadState Env m) => (T.ExecTrace -> T.ExecTrace) -> m ()+modifyTracer f =+  modify (\s@Env {envTracer = t} -> s {envTracer = f t})++makeSymbolicArray ::+  QBE.GlobalIdent ->+  [CE.Concolic DE.RegVal] ->+  SimState (Maybe (CE.Concolic DE.RegVal))+makeSymbolicArray _ [arrayPtr, numElem, elemSize, namePtr] = do+  name <- E.toString <$> (toAddress namePtr >>= readNullArray)+  vlty <- case E.toWord64 elemSize of+    1 -> pure QBE.Byte+    2 -> pure QBE.HalfWord+    4 -> pure (QBE.Base QBE.Word)+    8 -> pure (QBE.Base QBE.Long)+    _ -> throwError TypingError++  values <-+    mapM+      (\n -> makeConcolic (name ++ show n) vlty)+      [1 .. E.toWord64 numElem]++  arrayAddr <- toAddress arrayPtr+  liftState (DS.SimState $ DS.storeValues arrayAddr values) >> pure Nothing+makeSymbolicArray ident _ = throwError $ FuncArgsMismatch ident++findSimFunc :: QBE.GlobalIdent -> Maybe ([CE.Concolic DE.RegVal] -> SimState (Maybe (CE.Concolic DE.RegVal)))+findSimFunc i@(QBE.GlobalIdent "qute_make_symbolic") = Just (makeSymbolicArray i)+findSimFunc ident = lookupSimFunc ident++------------------------------------------------------------------------++-- | State of the concolic executor with which an error was triggered+-- in the application code, which can be reproduced using this state.+data ErrorState+  = ErrorState+  { errTracer :: T.ExecTrace,+    errStore :: ST.Store+  }++-- | Exception thrown upon encountered an t'ErrorState'.+data ErrorPath+  = ErrorPath+  { pathInput :: ErrorState,+    pathError :: EvalError+  }++instance Exception ErrorPath++instance Show ErrorPath where+  show (ErrorPath _ err) = show err++------------------------------------------------------------------------++newtype SimState a = SimState {unSimState :: StateT Env IO a}+  deriving (Functor, Applicative, Monad, MonadIO)++deriving instance MonadState Env SimState++-- Implements 'MonadError' in t'SimState' via 'IOException's. On throw,+-- it also returns the relevant executor state by encapsulting it in+-- an 'ErrorPath'.+--+-- See also: The instance for 'DS.SimState'.+instance MonadError EvalError SimState where+  throwError err = do+    Env {envTracer = t, envStore = s} <- get+    liftIO $ throwIO (ErrorPath (ErrorState t s) err)++  catchError (SimState st) handler =+    SimState $ DS.unliftCatch st (unSimState . handler)++------------------------------------------------------------------------++instance Simulator SimState (CE.Concolic DE.RegVal) where+  isTrue value = do+    let condResult = E.toWord64 (CE.concrete value) /= 0+    case CE.symbolic value of+      Nothing -> pure condResult+      Just sexpr -> do+        -- Track the taken branch in the tracer.+        let branch = T.newBranch sexpr+        modifyTracer (\t -> T.appendBranch t condResult branch)++        pure condResult++  -- Implements address concretization as a memory model.+  toAddress CE.Concolic {CE.concrete = cv, CE.symbolic = svMaybe} =+    case svMaybe of+      Just sv ->+        case sv `E.eq` SE.fromReg cv of+          Just c -> do+            modifyTracer (`T.appendCons` c)+            pure $ E.toWord64 cv+          Nothing -> throwError TypingError+      Nothing -> pure $ E.toWord64 cv++  findFunc ident = do+    funcs <- gets (DS.envFuncs . envBase)+    pure $ case Map.lookup ident funcs of+      Just x -> Just $ SFuncDef x+      Nothing -> SSimFunc <$> findSimFunc ident+  findFuncByAddr addr = do+    fptrs <- gets (DS.envFuncAddrs . envBase)+    case Map.lookup addr fptrs of+      Just fn -> findFunc fn+      Nothing -> pure Nothing++  lookupSymbol = liftState . lookupSymbol+  activeFrame = liftState activeFrame+  pushStackFrame = liftState . pushStackFrame+  popStackFrame = liftState popStackFrame+  getSP = liftState getSP+  setSP = liftState . setSP++  writeMemory a t v = liftState (writeMemory a t v)+  readMemory t a = liftState (readMemory t a)++------------------------------------------------------------------------++runPath :: SimState a -> SimState (T.ExecTrace, ST.Store)+runPath state = do+  _ <- state+  t <- gets envTracer+  s <- gets envStore+  pure (t, s)++run :: Env -> SimState a -> IO (T.ExecTrace, ST.Store)+run env state = evalStateT (unSimState $ runPath state) env
+ src/Language/QBE/Simulator/Explorer.hs view
@@ -0,0 +1,166 @@+-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only+module Language.QBE.Simulator.Explorer+  ( defSolver,+    logSolver,+    PathResult (..),+    Engine (expLastPath),+    newEngine,+    explorePath,+    exploreFunc,+  )+where++import Control.Applicative (empty, (<|>))+import Control.Monad.Catch (try)+import Control.Monad.IO.Class (liftIO)+import Control.Monad.State.Strict (StateT, evalStateT, get, lift, modify, put)+import Data.Map qualified as Map+import Language.QBE.Backend.DFS (PathSel, findUnexplored, newPathSel, trackTrace)+import Language.QBE.Backend.Model (Model)+import Language.QBE.Backend.Store qualified as ST+import Language.QBE.Backend.Tracer qualified as T+import Language.QBE.Simulator (execFunc)+import Language.QBE.Simulator.Concolic.State+  ( Env (envStore),+    ErrorPath (pathError, pathInput),+    ErrorState (errStore, errTracer),+    SimState (..),+    makeConcolic,+    runPath,+  )+import Language.QBE.Simulator.Error (EvalError)+import Language.QBE.Types qualified as QBE+import SimpleBV qualified as SMT+import System.Directory (findExecutable)+import System.IO (Handle)++logic :: String+logic = "QF_BV"++findSolver :: IO (String, [String])+findSolver =+  solver "bitwuzla" []+    <|> solver "z3" ["-smt2", "-in"]+    <|> solver "cvc5" ["--incremental"]+    <|> fail "no suitable sover found in PATH"+  where+    solver :: String -> [String] -> IO (String, [String])+    solver exec args = do+      r <- findExecutable exec+      maybe empty (\_ -> pure (exec, args)) r++defSolver :: IO SMT.Solver+defSolver = do+  -- l <- SMT.newLogger 0+  (solver, args) <- findSolver+  s <- SMT.newSolver solver args Nothing+  SMT.setLogic s logic+  return s++logSolver :: Handle -> IO SMT.Solver+logSolver handle = do+  l <- SMT.newLoggerWithHandle handle 0+  (solver, args) <- findSolver+  s <-+    SMT.newSolverWithConfig+      (SMT.defaultConfig solver args)+        { SMT.solverLogger = SMT.smtSolverLogger l+        }+  SMT.setLogic s logic+  return s++------------------------------------------------------------------------++data PathResult+  = PathResult+  { pathErr :: Maybe EvalError,+    pathTrace :: T.ExecTrace,+    pathVars :: ST.Assign+  }+  deriving (Show, Eq)++initPath :: PathResult+initPath = PathResult Nothing [] Map.empty++data Engine+  = Engine+  { expSolver :: SMT.Solver,+    expPathSel :: PathSel,+    expEnv :: Env,+    expLastPath :: PathResult+  }++newEngine :: Env -> SMT.Solver -> Engine+newEngine env solver =+  Engine+    { expSolver = solver,+      expPathSel = newPathSel,+      expEnv = env,+      expLastPath = initPath+    }++findNext :: [SMT.SExpr] -> T.ExecTrace -> StateT Engine IO (Maybe Model)+findNext symVars eTrace = do+  engine <- get++  let pathSel = trackTrace (expPathSel engine) eTrace+  (model, nextPathSel) <-+    liftIO $ findUnexplored (expSolver engine) symVars pathSel++  put $ engine {expPathSel = nextPathSel}+  pure model++-- TODO: Consider modelling changes of the PathSel (via findNext) and+-- changes of the Store (via ST.finalize and ST.setModel) as a StateT.+explorePath :: SimState a -> StateT Engine IO Bool+explorePath simState = do+  engine@(Engine {expEnv = env}) <- get+  maybePath <- try $ run env+  let (mayErr, eTrace, nStore) =+        case maybePath of+          Left (err :: ErrorPath) ->+            let st = pathInput err+             in (Just $ pathError err, errTracer st, errStore st)+          Right (t, s) -> (Nothing, t, s)++  -- Before finalizing the store, we can extract the variables we encountered+  -- during this concrete execution, as well as the concrete values used for+  -- these variables during the execution.+  let inputVars = ST.sexprs nStore+      varAssign = ST.cValues nStore+  put $ engine {expLastPath = PathResult mayErr eTrace varAssign}++  -- Finalize the store (declare new symbolic vars in solver) and then,+  -- based on the new solver state, solve constraints to find a new input.+  store <- liftIO $ ST.finalize (expSolver engine) nStore+  model <- findNext inputVars eTrace+  case model of+    Nothing -> pure False+    Just newModel -> do+      let nEnv = env {envStore = ST.setModel store newModel}+       in modify (\e -> e {expEnv = nEnv})+      pure True+  where+    run env = lift $ evalStateT (unSimState $ runPath simState) env++------------------------------------------------------------------------++exploreFunc ::+  Engine ->+  QBE.FuncDef ->+  [(String, QBE.ExtType)] ->+  IO [PathResult]+exploreFunc engine entry params = do+  let funcState = mapM (uncurry makeConcolic) params >>= execFunc entry+  evalStateT (exploreFunc' funcState) engine+  where+    exploreFunc' st = do+      morePaths <- explorePath st+      curEngine <- get++      let ret = expLastPath curEngine+       in if morePaths+            then (ret :) <$> exploreFunc' st+            else pure [ret]
+ src/Language/QBE/Simulator/Symbolic/Expression.hs view
@@ -0,0 +1,213 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Language.QBE.Simulator.Symbolic.Expression+  ( BitVector,+    fromByte,+    fromReg,+    toSExpr,+    symbolic,+    bitSize,+    toCond,+  )+where++import Control.DeepSeq (NFData)+import Control.Exception (assert)+import Data.Bits (shiftL, (.&.))+import Data.Word (Word64, Word8)+import GHC.Generics (Generic)+import Language.QBE.Simulator.Default.Expression qualified as D+import Language.QBE.Simulator.Expression qualified as E+import Language.QBE.Simulator.Memory qualified as MEM+import Language.QBE.Types qualified as QBE+import SimpleBV qualified as SMT++-- TODO: Floating point support.+newtype BitVector = BitVector SMT.SExpr+  deriving (Show, Eq, Generic)++instance NFData BitVector++fromByte :: Word8 -> BitVector+fromByte byte = BitVector (SMT.bvLit 8 $ fromIntegral byte)++fromReg :: D.RegVal -> BitVector+fromReg (D.VByte v) = BitVector (SMT.bvLit 8 $ fromIntegral v)+fromReg (D.VHalf v) = BitVector (SMT.bvLit 16 $ fromIntegral v)+fromReg (D.VWord v) = BitVector (SMT.bvLit 32 $ fromIntegral v)+fromReg (D.VLong v) = BitVector (SMT.bvLit 64 $ fromIntegral v)+fromReg (D.VSingle _) = error "symbolic floats not supported"+fromReg (D.VDouble _) = error "symbolic doubles not supported"++toSExpr :: BitVector -> SMT.SExpr+toSExpr (BitVector s) = s++symbolic :: String -> QBE.ExtType -> BitVector+symbolic name ty = BitVector (SMT.const name $ QBE.extTypeBitSize ty)++bitSize :: BitVector -> Int+bitSize = SMT.width . toSExpr++-- In the QBE a condition (see `jnz`) is true if the Word value is not zero.+toCond :: Bool -> BitVector -> SMT.SExpr+toCond isTrue bv =+  -- Equality is only defined for Words.+  assert (bitSize bv == QBE.baseTypeBitSize QBE.Word) $+    let zeroSExpr = toSExpr (fromReg $ E.fromLit (QBE.Base QBE.Word) 0)+     in toCond' (toSExpr bv) zeroSExpr+  where+    toCond' lhs rhs+      | isTrue = SMT.not (SMT.eq lhs rhs) -- /= 0+      | otherwise = SMT.eq lhs rhs -- == 0++------------------------------------------------------------------------++instance MEM.Storable BitVector BitVector where+  toBytes (BitVector s) =+    assert (size `mod` 8 == 0) $+      map (BitVector . nthByte s) [1 .. fromIntegral size `div` 8]+    where+      size :: Integer+      size = fromIntegral $ SMT.width s++      nthByte :: SMT.SExpr -> Int -> SMT.SExpr+      nthByte expr n = SMT.extract expr ((n - 1) * 8) 8++  fromBytes _ [] = Nothing+  fromBytes ty bytes@(BitVector s : xs) =+    if length bytes /= fromIntegral (QBE.loadByteSize ty)+      then Nothing+      else case (ty, bytes) of+        (QBE.LSubWord QBE.UnsignedByte, [_]) ->+          Just (BitVector (SMT.zeroExtend 24 concated))+        (QBE.LSubWord QBE.SignedByte, [_]) ->+          Just (BitVector (SMT.signExtend 24 concated))+        (QBE.LSubWord QBE.SignedHalf, [_, _]) ->+          Just (BitVector (SMT.signExtend 16 concated))+        (QBE.LSubWord QBE.UnsignedHalf, [_, _]) ->+          Just (BitVector (SMT.zeroExtend 16 concated))+        (QBE.LBase QBE.Word, [_, _, _, _]) ->+          Just (BitVector concated)+        (QBE.LBase QBE.Long, [_, _, _, _, _, _, _, _]) ->+          Just (BitVector concated)+        (QBE.LBase QBE.Single, [_, _, _, _]) ->+          error "float loading not implemented"+        (QBE.LBase QBE.Double, [_, _, _, _, _, _, _, _]) ->+          error "double loading not implemented"+        _ -> Nothing+    where+      concated :: SMT.SExpr+      concated = foldl concatBV s xs++      concatBV :: SMT.SExpr -> BitVector -> SMT.SExpr+      concatBV acc (BitVector byte) =+        assert (SMT.width byte == 8) $+          SMT.concat byte acc++------------------------------------------------------------------------++binaryOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector+binaryOp op (BitVector lhs) (BitVector rhs)+  | SMT.width lhs == SMT.width rhs = Just $ BitVector (lhs `op` rhs)+  | otherwise = Nothing++-- TODO: Move this into the expression abstraction.+toShiftAmount :: Word64 -> BitVector -> Maybe BitVector+toShiftAmount size amount = amount `E.urem` E.fromLit (QBE.Base QBE.Word) size++shiftOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector+shiftOp op value amount@(BitVector SMT.Word) =+  case bitSize value of+    32 -> toShiftAmount 32 amount >>= binaryOp op value+    64 -> do+      shiftAmount <- toShiftAmount 64 amount+      E.extend (QBE.Base QBE.Long) False shiftAmount >>= binaryOp op value+    _ -> Nothing+shiftOp _ _ _ = Nothing -- Shift amount must always be a Word.++binaryBoolOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector+binaryBoolOp op lhs rhs = do+  bv <- binaryOp op lhs rhs+  return $ BitVector (SMT.ite (toSExpr bv) trueValue falseValue)+  where+    -- TODO: Declare these as constants.+    trueValue :: SMT.SExpr+    trueValue = toSExpr $ E.fromLit (QBE.Base QBE.Long) 1++    falseValue :: SMT.SExpr+    falseValue = toSExpr $ E.fromLit (QBE.Base QBE.Long) 0++instance E.ValueRepr BitVector where+  fromLit ty n =+    let size = QBE.extTypeBitSize ty+        mask = (1 `shiftL` size) - 1+     in BitVector $ SMT.bvLit (fromIntegral size) $ fromIntegral (n .&. mask)++  fromFloat = error "symbolic floats currently unsupported"+  fromDouble = error "symbolic doubles currently unsupported"++  -- XXX: This only works for constants values, but this is fine since we implement+  -- concolic execution and can obtain the address from the concrete value part.+  toWord64 (BitVector value) =+    case SMT.sexprToVal value of+      SMT.Bits _ n -> fromIntegral n+      _ -> error "unrechable"++  getType v = case bitSize v of+    08 -> QBE.Byte+    16 -> QBE.HalfWord+    32 -> QBE.Base QBE.Word+    64 -> QBE.Base QBE.Long+    _ -> error "unreachable"++  floatToInt = error "symbolic float conversion not supported"+  intToFloat = error "symbolic float conversion not supported"+  extendFloat = error "symbolic float extension not supported"+  truncFloat = error "symbolic float trunction not supported"++  extend extTy isSigned val@(BitVector s)+    | QBE.extTypeBitSize extTy <= bitSize val = Nothing+    | otherwise = Just $ BitVector (extFunc targetSize s)+    where+      targetSize :: Integer+      targetSize = fromIntegral $ QBE.extTypeBitSize extTy - bitSize val++      extFunc :: Integer -> SMT.SExpr -> SMT.SExpr+      extFunc = if isSigned then SMT.signExtend else SMT.zeroExtend++  extract extTy val@(BitVector s)+    | QBE.extTypeBitSize extTy > bitSize val = Nothing+    | otherwise = Just $ BitVector (SMT.extract s 0 $ QBE.extTypeBitSize extTy)++  add = binaryOp SMT.bvAdd+  sub = binaryOp SMT.bvSub+  mul = binaryOp SMT.bvMul+  div = binaryOp SMT.bvSDiv+  or = binaryOp SMT.bvOr+  xor = binaryOp SMT.bvXOr+  and = binaryOp SMT.bvAnd+  urem = binaryOp SMT.bvURem+  srem = binaryOp SMT.bvSRem+  udiv = binaryOp SMT.bvUDiv++  neg (BitVector v) = Just $ BitVector (SMT.bvNeg v)++  sar = shiftOp SMT.bvAShr+  shr = shiftOp SMT.bvLShr+  shl = shiftOp SMT.bvShl++  eq = binaryBoolOp SMT.eq+  ne = binaryBoolOp (\lhs rhs -> SMT.not $ SMT.eq lhs rhs)+  sle = binaryBoolOp SMT.bvSLeq+  slt = binaryBoolOp SMT.bvSLt+  sge = binaryBoolOp SMT.bvSGeq+  sgt = binaryBoolOp SMT.bvSGt+  ule = binaryBoolOp SMT.bvULeq+  ult = binaryBoolOp SMT.bvULt+  uge = binaryBoolOp SMT.bvUGeq+  ugt = binaryBoolOp SMT.bvUGt++  ord = error "symbolic ordered comparison not supported"+  unord = error "symbolic unordered comparison not supported"
+ src/SimpleBV.hs view
@@ -0,0 +1,430 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: MIT AND GPL-3.0-only+{-# LANGUAGE PatternSynonyms #-}++module SimpleBV+  ( SExpr,+    SMT.Solver,+    SMT.defaultConfig,+    SMT.newLogger,+    SMT.newLoggerWithHandle,+    SMT.newSolver,+    SMT.newSolverWithConfig,+    SMT.solverLogger,+    SMT.smtSolverLogger,+    SMT.setLogic,+    SMT.push,+    SMT.pop,+    SMT.popMany,+    SMT.check,+    SMT.Result (..),+    SMT.Value (..),+    pattern W,+    pattern Byte,+    pattern Half,+    pattern Word,+    pattern Long,+    width,+    const,+    declareBV,+    assert,+    sexprToVal,+    getValue,+    getValues,+    toSMT,+    ite,+    and,+    or,+    not,+    eq,+    bvLit,+    bvAdd,+    bvAShr,+    bvLShr,+    bvAnd,+    bvMul,+    bvNeg,+    bvOr,+    bvSDiv,+    bvSLeq,+    bvSLt,+    bvSGeq,+    bvSGt,+    bvSRem,+    bvShl,+    bvSub,+    bvUDiv,+    bvULeq,+    bvUGeq,+    bvUGt,+    bvULt,+    bvURem,+    bvXOr,+    concat,+    extract,+    signExtend,+    zeroExtend,+  )+where++import Control.DeepSeq (NFData, NFData1)+import Data.Bits (shiftL, shiftR, (.&.))+import GHC.Generics (Generic, Generic1)+import SimpleSMT qualified as SMT+import Prelude hiding (and, concat, const, not, or)++data Expr a+  = Var String+  | Int Integer+  | And a a+  | Or a a+  | Neg a+  | Not a+  | Eq a a+  | BvAdd a a+  | BvAShr a a+  | BvLShr a a+  | BvAnd a a+  | BvMul a a+  | BvOr a a+  | BvSDiv a a+  | BvSLeq a a+  | BvSLt a a+  | BvSGeq a a+  | BvSGt a a+  | BvSRem a a+  | BvShl a a+  | BvSub a a+  | BvUDiv a a+  | BvULeq a a+  | BvUGeq a a+  | BvUGt a a+  | BvULt a a+  | BvURem a a+  | BvXOr a a+  | Concat a a+  | Ite a a a+  | Extract Int Int a+  | SignExtend Integer a+  | ZeroExtend Integer a+  deriving (Show, Eq, Generic, Generic1)++instance (NFData a) => NFData (Expr a)++instance NFData1 Expr++data SExpr+  = SExpr+  { width :: Int,+    sexpr :: Expr SExpr+  }+  deriving (Show, Eq, Generic)++instance NFData SExpr++toSMT :: SExpr -> SMT.SExpr+toSMT expr =+  case sexpr expr of+    (Var name) -> SMT.const name+    (Int v) -> SMT.List [SMT.Atom "_", SMT.Atom ("bv" ++ show v), SMT.Atom $ show (width expr)]+    (Or lhs rhs) -> SMT.or (toSMT lhs) (toSMT rhs)+    (Ite cond lhs rhs) -> SMT.ite (toSMT cond) (toSMT lhs) (toSMT rhs)+    (And lhs rhs) -> SMT.and (toSMT lhs) (toSMT rhs)+    (Not v) -> SMT.not (toSMT v)+    (Neg v) -> SMT.bvNeg (toSMT v)+    (SignExtend n v) -> SMT.signExtend n (toSMT v)+    (ZeroExtend n v) -> SMT.zeroExtend n (toSMT v)+    (Eq lhs rhs) -> SMT.eq (toSMT lhs) (toSMT rhs)+    (Concat lhs rhs) -> SMT.concat (toSMT lhs) (toSMT rhs)+    (Extract o w e) -> SMT.extract (toSMT e) (fromIntegral $ o + w - 1) (fromIntegral o)+    (BvAnd lhs rhs) -> SMT.bvAnd (toSMT lhs) (toSMT rhs)+    (BvAShr lhs rhs) -> SMT.bvAShr (toSMT lhs) (toSMT rhs)+    (BvLShr lhs rhs) -> SMT.bvLShr (toSMT lhs) (toSMT rhs)+    (BvAdd lhs rhs) -> SMT.bvAdd (toSMT lhs) (toSMT rhs)+    (BvMul lhs rhs) -> SMT.bvMul (toSMT lhs) (toSMT rhs)+    (BvOr lhs rhs) -> SMT.bvOr (toSMT lhs) (toSMT rhs)+    (BvSDiv lhs rhs) -> SMT.bvSDiv (toSMT lhs) (toSMT rhs)+    (BvSLeq lhs rhs) -> SMT.bvSLeq (toSMT lhs) (toSMT rhs)+    (BvSLt lhs rhs) -> SMT.bvSLt (toSMT lhs) (toSMT rhs)+    (BvSGeq lhs rhs) -> SMT.fun "bvsge" [toSMT lhs, toSMT rhs]+    (BvSGt lhs rhs) -> SMT.fun "bvsgt" [toSMT lhs, toSMT rhs]+    (BvSRem lhs rhs) -> SMT.bvSRem (toSMT lhs) (toSMT rhs)+    (BvShl lhs rhs) -> SMT.bvShl (toSMT lhs) (toSMT rhs)+    (BvSub lhs rhs) -> SMT.bvSub (toSMT lhs) (toSMT rhs)+    (BvUDiv lhs rhs) -> SMT.bvUDiv (toSMT lhs) (toSMT rhs)+    (BvULeq lhs rhs) -> SMT.bvULeq (toSMT lhs) (toSMT rhs)+    (BvUGeq lhs rhs) -> SMT.fun "bvuge" [toSMT lhs, toSMT rhs]+    (BvUGt lhs rhs) -> SMT.fun "bvugt" [toSMT lhs, toSMT rhs]+    (BvULt lhs rhs) -> SMT.bvULt (toSMT lhs) (toSMT rhs)+    (BvURem lhs rhs) -> SMT.bvURem (toSMT lhs) (toSMT rhs)+    (BvXOr lhs rhs) -> SMT.bvXOr (toSMT lhs) (toSMT rhs)++boolWidth :: Int+boolWidth = 1++pattern E :: Expr SExpr -> SExpr+pattern E expr <- SExpr {sexpr = expr, width = _}++pattern W :: Int -> SExpr+pattern W w <- SExpr {width = w}++pattern Byte :: SExpr+pattern Byte <- SExpr {width = 8}++pattern Half :: SExpr+pattern Half <- SExpr {width = 16}++pattern Word :: SExpr+pattern Word <- SExpr {width = 32}++pattern Long :: SExpr+pattern Long <- SExpr {width = 64}++------------------------------------------------------------------------++const :: String -> Int -> SExpr+const name width = SExpr width (Var name)++declareBV :: SMT.Solver -> String -> Int -> IO SExpr+declareBV solver name width = do+  let bits = SMT.tBits $ fromIntegral width+  SMT.declare solver name bits >> pure (const name width)++bvLit :: Int -> Integer -> SExpr+bvLit width value = SExpr width (Int value)++sexprToVal :: SExpr -> SMT.Value+sexprToVal (E (Var n)) = SMT.Other $ SMT.Atom n+sexprToVal e@(E (Int i)) = SMT.Bits (width e) i+sexprToVal _ = SMT.Other $ SMT.Atom "_"++assert :: SMT.Solver -> SExpr -> IO ()+assert solver = SMT.assert solver . toSMT++getValue :: SMT.Solver -> SExpr -> IO SMT.Value+getValue solver = SMT.getExpr solver . toSMT++getValues :: SMT.Solver -> [SExpr] -> IO [(String, SMT.Value)]+getValues solver exprs = do+  map go <$> SMT.getExprs solver (map toSMT exprs)+  where+    go :: (SMT.SExpr, SMT.Value) -> (String, SMT.Value)+    go (SMT.Atom name, value) = (name, value)+    go _ = error "non-atomic variable in inputVars"++---------------------------------------------------------------------------++ite :: SExpr -> SExpr -> SExpr -> SExpr+ite cond ifT ifF = SExpr (width ifT) (Ite cond ifT ifF)++not :: SExpr -> SExpr+not (E (Not cond)) = cond+not expr = expr {sexpr = Not expr}++and :: SExpr -> SExpr -> SExpr+and lhs rhs = lhs {sexpr = And lhs rhs}++or :: SExpr -> SExpr -> SExpr+or lhs rhs = lhs {sexpr = Or lhs rhs}++signExtend :: Integer -> SExpr -> SExpr+signExtend n expr = SExpr (width expr + fromIntegral n) $ SignExtend n expr++zeroExtend :: Integer -> SExpr -> SExpr+zeroExtend n expr = SExpr (width expr + fromIntegral n) $ ZeroExtend n expr++------------------------------------------------------------------------++eq' :: SExpr -> SExpr -> SExpr+eq' lhs rhs = SExpr boolWidth $ Eq lhs rhs++-- Eliminates ITE expressions when comparing with constants values, this is+-- useful in the QBE context to eliminate comparisons with truth values.+eq :: SExpr -> SExpr -> SExpr+eq lexpr@(E (Ite cond (E (Int ifT)) (E (Int ifF)))) rexpr@(E (Int other))+  | other == ifT = cond+  | other == ifF = not cond+  | otherwise = eq' lexpr rexpr+eq lhs rhs = eq' lhs rhs++concat' :: SExpr -> SExpr -> SExpr+concat' lhs rhs =+  SExpr (width lhs + width rhs) $ Concat lhs rhs++-- Replace 0 concats with zero extension: (concat (_ bv0 8) buf6)+concatZeros :: SExpr -> SExpr -> SExpr+concatZeros lhs@(E (Int 0)) rhs = zeroExtend (fromIntegral $ width lhs) rhs+concatZeros lhs rhs = concat' lhs rhs++-- Replaces continuous concat expressions with a single extract expression.+concat :: SExpr -> SExpr -> SExpr+concat+  lhs@(E (Extract loff lwidth latom@(E exprLhs)))+  rhs@(E (Extract roff rwidth (E exprRhs)))+    | exprLhs == exprRhs && (roff + rwidth) == loff = extract latom roff (lwidth + rwidth)+    | otherwise = concatZeros lhs rhs+concat lhs rhs = concatZeros lhs rhs++extract' :: SExpr -> Int -> Int -> SExpr+extract' expr off w = SExpr w $ Extract off w expr++-- Eliminate extract expression where the value already has the desired bits.+extractSameWidth :: SExpr -> Int -> Int -> SExpr+extractSameWidth expr off w+  | off == 0 && width expr == w = expr+  | otherwise = extract' expr off w++-- Eliminate nested extract expression of the same width.+extractNested :: SExpr -> Int -> Int -> SExpr+extractNested expr@(E (Extract ioff iwidth _)) off width =+  if ioff == off && iwidth == width+    then expr+    else extractSameWidth expr off width+extractNested expr off width = extractSameWidth expr off width++-- Performs direct extractions of constant immediate values.+extractConst :: SExpr -> Int -> Int -> SExpr+extractConst (E (Int value)) off w =+  SExpr w . Int $ truncTo (value `shiftR` off) w+  where+    truncTo v bits = v .&. ((1 `shiftL` bits) - 1)+extractConst expr off width = extractNested expr off width++-- This performs constant propagation for subtyping of condition values (i.e.+-- the conversion from long to word).+extractIte :: SExpr -> Int -> Int -> SExpr+extractIte (E (Ite cond ifT@(E (Int _)) ifF@(E (Int _)))) off w =+  let ex x = extractConst x off w+   in SExpr w $ Ite cond (ex ifT) (ex ifF)+extractIte expr off width = extractConst expr off width++extractZeros ::+  SExpr ->+  Int ->+  Int ->+  SExpr+extractZeros expr@(E (ZeroExtend extBits inner)) exOff exWidth+  | exOff >= width inner && extBits > 0 = bvLit exWidth 0 -- only extracting zeros+  | otherwise = extractIte expr exOff exWidth+extractZeros outer exOff exWidth = extractIte outer exOff exWidth++extractExt' ::+  (Integer -> SExpr -> Expr SExpr) ->+  SExpr ->+  Integer ->+  SExpr ->+  Int ->+  Int ->+  SExpr+extractExt' cons outer extBits inner exOff exWidth+  -- If we are only extracting the non-extended bytes...+  | width inner >= exOff + exWidth = extractZeros inner exOff exWidth+  -- Consider: ((_ extract 31 0) ((_ zero_extend 56) byte))+  | exWidth < fromIntegral extBits && exOff == 0 =+      SExpr exWidth $ cons (extBits - fromIntegral exWidth) inner+  -- No folding...+  | otherwise = extractZeros outer exOff exWidth++-- Remove ZeroExtend and SignExtend expression where we don't use+-- the extended bits because we extract below the extended size.+extractExt :: SExpr -> Int -> Int -> SExpr+extractExt expr@(E (SignExtend extBits inner)) exOff exWidth =+  extractExt' SignExtend expr extBits inner exOff exWidth+extractExt expr@(E (ZeroExtend extBits inner)) exOff exWidth =+  extractExt' ZeroExtend expr extBits inner exOff exWidth+extractExt expr off w = extractIte expr off w++extract :: SExpr -> Int -> Int -> SExpr+extract = extractExt++------------------------------------------------------------------------++binOp' :: (SExpr -> SExpr -> Expr SExpr) -> SExpr -> SExpr -> SExpr+binOp' op lhs rhs = lhs {sexpr = op lhs rhs}++binOp :: (SExpr -> SExpr -> Expr SExpr) -> SExpr -> SExpr -> SExpr+-- Consider: (bvslt ((_ zero_extend 24) byte0) ((_ zero_extend 24) byte1))+-- TODO: The following only works if 'op' does not consider sign-bits. Otherwise,+--       there is no semantic expression equivalence after this folding operation.+-- binOp op lhs@(E (ZeroExtend _ lhsInner)) rhs@(E (ZeroExtend _ rhsInner)) =+--   if width lhsInner == width rhsInner+--     then binOp op lhsInner rhsInner+--     else binOp' op lhs rhs+binOp op lhs rhs = binOp' op lhs rhs++-- TODO: Generate these using template-haskell.++bvNeg :: SExpr -> SExpr+bvNeg x = x {sexpr = Neg x}++bvAdd :: SExpr -> SExpr -> SExpr+bvAdd = binOp BvAdd++bvAShr :: SExpr -> SExpr -> SExpr+bvAShr = binOp BvAShr++bvLShr :: SExpr -> SExpr -> SExpr+bvLShr = binOp BvLShr++bvAnd :: SExpr -> SExpr -> SExpr+bvAnd = binOp BvAnd++bvMul :: SExpr -> SExpr -> SExpr+bvMul = binOp BvMul++bvOr :: SExpr -> SExpr -> SExpr+bvOr = binOp BvOr++bvSDiv :: SExpr -> SExpr -> SExpr+bvSDiv = binOp BvSDiv++bvSLeq :: SExpr -> SExpr -> SExpr+bvSLeq = binOp BvSLeq++bvSLt :: SExpr -> SExpr -> SExpr+bvSLt = binOp BvSLt++bvSGeq :: SExpr -> SExpr -> SExpr+bvSGeq = binOp BvSGeq++bvSGt :: SExpr -> SExpr -> SExpr+bvSGt = binOp BvSGt++bvSRem :: SExpr -> SExpr -> SExpr+bvSRem = binOp BvSRem++bvShl :: SExpr -> SExpr -> SExpr+bvShl = binOp BvShl++bvSub :: SExpr -> SExpr -> SExpr+bvSub = binOp BvSub++bvUDiv :: SExpr -> SExpr -> SExpr+bvUDiv = binOp BvUDiv++bvULeq :: SExpr -> SExpr -> SExpr+bvULeq = binOp BvULeq++bvUGeq :: SExpr -> SExpr -> SExpr+bvUGeq = binOp BvUGeq++bvUGt :: SExpr -> SExpr -> SExpr+bvUGt = binOp BvUGt++bvULt :: SExpr -> SExpr -> SExpr+bvULt = binOp BvULt++bvURem :: SExpr -> SExpr -> SExpr+-- Fold constant bvURem operations which are emitted a lot in our generated+-- SMT-LIB because of QBE's "shift-value modulo bitsize"-semantics.+bvURem vlhs@(E (Int lhs)) (E (Int rhs)) =+  SExpr (width vlhs) $+    -- XXX: On urem-by-zero, SMT-LIB returns the lhs.+    if rhs == 0+      then Int lhs+      else Int $ lhs `rem` rhs+bvURem lhs rhs = binOp BvURem lhs rhs++bvXOr :: SExpr -> SExpr -> SExpr+bvXOr = binOp BvXOr
+ test/BV.hs view
@@ -0,0 +1,87 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module BV (bvTests) where++import SimpleBV qualified as SMT+import Test.Tasty+import Test.Tasty.HUnit++foldingTests :: TestTree+foldingTests =+  testGroup+    "foldingTests"+    [ testCase "Folding of continous concat expressions" $+        do+          let val = SMT.const "foo" 32++          let b1 = SMT.extract val 0 8+          let b2 = SMT.extract val 8 8++          SMT.concat b2 b1 @?= SMT.extract val 0 16,+      testCase "Concat with zeros" $+        do+          let lhs = SMT.bvLit 8 0x0+          let rhs = SMT.const "foo" 8++          SMT.concat lhs rhs @?= SMT.zeroExtend 8 rhs,+      testCase "Folding of ite-based equalities" $+        do+          let cond = SMT.const "foo" 32 `SMT.eq` SMT.const "bar" 32++          let ifT = SMT.bvLit 32 0xdeadbeef+          let ifF = SMT.bvLit 32 0xbeefdead+          let val = SMT.ite cond ifT ifF++          SMT.eq val ifT @?= cond+          SMT.eq val ifF @?= SMT.not cond,+      testCase "Folding of same-width extraction" $+        do+          let val = SMT.const "byte" 8+          SMT.extract val 0 8 @?= val,+      testCase "Folding of constant extractions" $+        do+          let val = SMT.bvLit 32 0xdeadbeef+          SMT.extract val 16 16 @?= SMT.bvLit 16 0xdead,+      testCase "Folding of identical nested extracts" $+        do+          let val = SMT.const "foobar" 64++          let ex1 = SMT.extract val 0 16+          let ex2 = SMT.extract ex1 0 16++          ex2 @?= ex1,+      testCase "Folding of ITE expressions" $+        do+          let cond = SMT.const "foo" 32 `SMT.eq` SMT.const "bar" 32+          let val = SMT.ite cond (SMT.bvLit 32 0xdeadbeef) (SMT.bvLit 32 0xbeefdead)++          SMT.extract val 0 16 @?= SMT.ite cond (SMT.bvLit 16 0xbeef) (SMT.bvLit 16 0xdead),+      testCase "Extract reduces size" $+        do+          let val = SMT.bvLit 32 0xdeadbeef+          SMT.extract val 8 8 @?= SMT.bvLit 8 0xbe,+      testCase "Removal of non-extracted zero-extensions" $+        do+          let val = SMT.zeroExtend 24 $ SMT.bvLit 8 0xff+          SMT.extract val 0 8 @?= SMT.bvLit 8 0xff+          SMT.extract val 4 4 @?= SMT.bvLit 4 0xf,+      testCase "Extraction of zero bits" $+        do+          let val = SMT.zeroExtend 24 $ SMT.bvLit 8 0xff+          SMT.extract val 8 24 @?= SMT.bvLit 24 0x0+          SMT.extract val 0 8 @?= SMT.bvLit 8 0xff+          SMT.extract val 24 8 @?= SMT.bvLit 8 0x0,+      -- TODO: constant fold extractions of zeros.+      -- SMT.extract val 8 8 @?= SMT.bvLit 8 0x0+      testCase "Extraction including zero-extended bits" $+        do+          let lit = SMT.bvLit 8 0xab+          let val = SMT.zeroExtend 56 lit+          SMT.extract val 0 32 @?= SMT.zeroExtend 24 lit+          SMT.extract val 0 64 @?= val+    ]++bvTests :: TestTree+bvTests = testGroup "SimpleBV" [foldingTests]
+ test/Backend.hs view
@@ -0,0 +1,133 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Backend (backendTests) where++import Data.Maybe (fromJust)+import Language.QBE.Backend.DFS (findUnexplored, newPathSel, trackTrace)+import Language.QBE.Backend.Model qualified as Model+import Language.QBE.Backend.Store qualified as ST+import Language.QBE.Backend.Tracer qualified as T+import Language.QBE.Simulator.Concolic.Expression qualified as CE+import Language.QBE.Simulator.Default.Expression qualified as DE+import Language.QBE.Simulator.Explorer (defSolver)+import Language.QBE.Simulator.Symbolic.Expression qualified as SE+import Language.QBE.Types qualified as QBE+import System.Random (initStdGen)+import Test.Tasty+import Test.Tasty.HUnit+import Util++storeTests :: TestTree+storeTests =+  testGroup+    "Tests for the Variable Store"+    [ testCase "finalize never forgets defined variables" $+        do+          s0 <- ST.empty <$> initStdGen+          solver <- defSolver++          let s1 = fst $ ST.getConcolic s0 "a" (QBE.Base QBE.Word)+          s2 <- ST.finalize solver s1++          let s3 = fst $ ST.getConcolic s2 "b" (QBE.Base QBE.Word)+          s4 <- ST.finalize solver s3++          -- The 'a' variable returns, but should still be known.+          -- There used to be a bug where this caused an exception.+          let s5 = fst $ ST.getConcolic s4 "a" (QBE.Base QBE.Word)+          _ <- ST.finalize solver s5++          assertBool "finalize does not throw an exception" True+    ]++traceTests :: TestTree+traceTests =+  testGroup+    "Tests for the Symbolic Tracer"+    [ testCase "Branch tracing with single concrete branch" $+        do+          t <-+            parseAndExec+              (QBE.GlobalIdent "main")+              []+              "function $main() {\n\+              \@start.1\n\+              \%cond =w add 0, 1\n\+              \jnz %cond, @branch.1, @branch.2\n\+              \@branch.1\n\+              \ret\n\+              \@branch.2\n\+              \ret\n\+              \}"++          -- Trace must be empty because it doesn't branch on symbolic values.+          length t @?= 0,+      testCase "Branch tracing and solving with single symbolic branch" $+        do+          s <- defSolver+          c <- unconstrained s 0 "input" QBE.Word+          assertBool "created value is symbolic" $ CE.hasSymbolic c+          let inputs = [(SE.toSExpr . fromJust . CE.symbolic) c]++          t <-+            parseAndExec+              (QBE.GlobalIdent "branchOnInput")+              [c]+              "function $branchOnInput(w %cond) {\n\+              \@start.1\n\+              \jnz %cond, @branch.1, @branch.2\n\+              \@branch.1\n\+              \ret\n\+              \@branch.2\n\+              \ret\n\+              \}"++          t @?= [(False, T.newBranch (fromJust $ CE.symbolic c))]++          let pathSel = trackTrace newPathSel t+          (mm, nextPathSel) <- findUnexplored s inputs pathSel++          let assign = Model.toList (fromJust mm)+          case assign of+            [(_, DE.VWord v)] ->+              assertBool "condition must be /= 0" (v /= 0)+            _ -> assertFailure "unexpected model"++          -- There are only two branches: input == 0 and input /= 0+          (nxt, _) <- findUnexplored s inputs nextPathSel+          nxt @?= Nothing,+      testCase "Tracing with multiple branches" $+        do+          s <- defSolver+          c1 <- unconstrained s 0 "cond1" QBE.Word+          c2 <- unconstrained s 0 "cond2" QBE.Word++          t <-+            parseAndExec+              (QBE.GlobalIdent "branchOnInput")+              [c1, c2]+              "function $branchOnInput(w %cond1, w %cond2) {\n\+              \@jump.1\n\+              \jnz %cond1, @branch.1, @branch.2\n\+              \@branch.1\n\+              \jmp @jump.2\n\+              \@branch.2\n\+              \jmp @jump.2\n\+              \@jump.2\n\+              \jnz %cond2, @branch.3, @branch.4\n\+              \@branch.3\n\+              \ret\n\+              \@branch.4\n\+              \ret\n\+              \}"++          length t @?= 2+    ]++backendTests :: TestTree+backendTests =+  testGroup+    "Tests for the Symbolic Data Structures"+    [storeTests, traceTests]
+ test/Concolic.hs view
@@ -0,0 +1,35 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Concolic (exprTests) where++import Data.Maybe (fromJust)+import Data.Word (Word8)+import Language.QBE.Simulator.Concolic.Expression qualified as C+import Language.QBE.Simulator.Default.Expression qualified as D+import Language.QBE.Simulator.Expression qualified as E+import Language.QBE.Simulator.Memory qualified as MEM+import Language.QBE.Types qualified as QBE+import Test.Tasty+import Test.Tasty.HUnit++-- TODO: QuickCheck tests against the default interpreter's implementation.+storeTests :: TestTree+storeTests =+  testGroup+    "Storage Instance Tests"+    -- TODO: Test case for partial concoilc bytes+    [ testCase "Convert concrete concolic value to bytes and back" $+        do+          let value = E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: C.Concolic D.RegVal++          let bytes = MEM.toBytes value :: [C.Concolic Word8]+          length bytes @?= 4++          let valueFromBytes = fromJust $ MEM.fromBytes (QBE.LBase QBE.Word) bytes+          C.concrete value @?= C.concrete valueFromBytes+    ]++exprTests :: TestTree+exprTests = testGroup "Expression tests" [storeTests]
+ test/Explorer.hs view
@@ -0,0 +1,313 @@+-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Explorer (exploreTests) where++import Data.Bifunctor (second)+import Data.List (partition, sort, uncons)+import Data.Map qualified as Map+import Data.Maybe (fromJust, isJust)+import Language.QBE (Program, parseAndFind)+import Language.QBE.Backend.Store qualified as ST+import Language.QBE.Simulator.Concolic.State (mkEnv)+import Language.QBE.Simulator.Default.Expression qualified as DE+import Language.QBE.Simulator.Explorer+  ( PathResult (..),+    defSolver,+    exploreFunc,+    newEngine,+  )+import Language.QBE.Types qualified as QBE+import System.FilePath ((</>))+import Test.Tasty+import Test.Tasty.HUnit++branchPoints :: [PathResult] -> [[Bool]]+branchPoints lst = sort $ map (\(PathResult _ t _) -> map fst t) lst++findAssign :: [PathResult] -> [Bool] -> Maybe ST.Assign+findAssign [] _ = Nothing+findAssign ((PathResult _ eTrace a) : xs) toFind+  | map fst eTrace == toFind = Just a+  | otherwise = findAssign xs toFind++explore' :: Program -> QBE.FuncDef -> [(String, QBE.BaseType)] -> IO [PathResult]+explore' prog entry params = do+  defEnv <- mkEnv prog 0 128 Nothing+  engine <- newEngine defEnv <$> defSolver++  exploreFunc engine entry $ map (second QBE.Base) params++getFuncAndProg :: FilePath -> QBE.GlobalIdent -> IO (Program, QBE.FuncDef)+getFuncAndProg fileName funcName =+  let filePath = "test" </> "testdata" </> fileName+   in readFile filePath >>= parseAndFind funcName++------------------------------------------------------------------------++exploreTests :: TestTree+exploreTests =+  testGroup+    "Tests for Symbolic Program Exploration"+    [ testCase "Explore' program with four execution paths" $+        do+          let qbe =+                "function $branchOnInput(w %cond1, w %cond2) {\n\+                \@jump.1\n\+                \jnz %cond1, @branch.1, @branch.2\n\+                \@branch.1\n\+                \jmp @jump.2\n\+                \@branch.2\n\+                \jmp @jump.2\n\+                \@jump.2\n\+                \jnz %cond2, @branch.3, @branch.4\n\+                \@branch.3\n\+                \ret\n\+                \@branch.4\n\+                \ret\n\+                \}"++          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "branchOnInput") qbe+          eTraces <- explore' prog funcDef [("cond1", QBE.Word), ("cond2", QBE.Word)]++          let branches = branchPoints eTraces+          branches @?= [[False, False], [False, True], [True, False], [True, True]],+      testCase "Unsatisfiable branches" $+        do+          let qbe =+                "function $branchOnInput(w %cond1) {\n\+                \@jump.1\n\+                \jnz %cond1, @branch.1, @branch.2\n\+                \@branch.1\n\+                \jmp @jump.2\n\+                \@branch.2\n\+                \jmp @jump.2\n\+                \@jump.2\n\+                \jnz %cond1, @branch.3, @branch.4\n\+                \@branch.3\n\+                \ret\n\+                \@branch.4\n\+                \ret\n\+                \}"++          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "branchOnInput") qbe+          eTraces <- explore' prog funcDef [("cond1", QBE.Word)]++          let branches = branchPoints eTraces+          branches @?= [[False, False], [True, True]],+      testCase "Branch with overflow arithmetics" $+        do+          let qbe =+                "function $branchArithmetics(w %input) {\n\+                \@start\n\+                \%cond =w add %input, 1\n\+                \jnz %input, @branch.1, @branch.2\n\+                \@branch.1\n\+                \ret\n\+                \@branch.2\n\+                \ret\n\+                \}"++          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "branchArithmetics") qbe+          eTraces <- explore' prog funcDef [("input", QBE.Word)]++          let branches = branchPoints eTraces+          branches @?= [[False], [True]]++          let assign = fromJust $ findAssign eTraces [False]+          Map.lookup "input" assign @?= Just (DE.VWord 0),+      testCase "Store symbolic value and memory, load it and pass it to function" $+        do+          let qbe =+                "function $branchOnInput(w %cond1) {\n\+                \@jump.1\n\+                \jnz %cond1, @branch.1, @branch.2\n\+                \@branch.1\n\+                \jmp @jump.2\n\+                \@branch.2\n\+                \jmp @jump.2\n\+                \@jump.2\n\+                \jnz %cond1, @branch.3, @branch.4\n\+                \@branch.3\n\+                \ret\n\+                \@branch.4\n\+                \ret\n\+                \}\n\+                \function $entry(w %in) {\n\+                \@start\n\+                \%a =l alloc4 4\n\+                \storew %in, %a\n\+                \%l =w loadw %a\n\+                \call $branchOnInput(w %l)\n\+                \ret\n\+                \}"++          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "entry") qbe+          eTraces <- explore' prog funcDef [("x", QBE.Word)]++          let branches = branchPoints eTraces+          branches @?= [[False, False], [True, True]],+      testCase "Branch on a specific concrete 64-bit value" $+        do+          let qbe =+                "function $f(l %input.0) {\n\+                \@start\n\+                \%input.1 =l sub %input.0, 42\n\+                \jnz %input.1, @not42, @is42\n\+                \@not42\n\+                \ret\n\+                \@is42\n\+                \ret\n\+                \}"++          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "f") qbe+          eTraces <- explore' prog funcDef [("y", QBE.Long)]++          branchPoints eTraces @?= [[False], [True]]+          let assign = fromJust $ findAssign eTraces [False]+          Map.lookup "y" assign @?= Just (DE.VLong 42),+      testCase "Branching with subtyping" $+        do+          let qbe =+                "function $f(l %input.0, w %input.1) {\n\+                \@start\n\+                \%added =w add %input.1, 1\n\+                \%subed =w sub %added, %input.1\n\+                \%result =w add %added, %subed\n\+                \jnz %result, @b1, @b2\n\+                \@b1\n\+                \jnz %input.0, @b2, @b2\n\+                \@b2\n\+                \ret\n\+                \}"++          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "f") qbe+          eTraces <- explore' prog funcDef [("y", QBE.Long), ("x", QBE.Word)]++          branchPoints eTraces @?= [[False], [True, False], [True, True]],+      testCase "make a single word symbolic" $+        do+          let qbe =+                "data $name = align 1 {  b \"abcd\", b 0 }\n\+                \function w $main() {\n\+                \@start\n\+                \%ptr =l alloc4 4\n\+                \call extern $qute_make_symbolic(l %ptr, l 1, l 4, l $name)\n\+                \%word =w loadw %ptr\n\+                \jnz %word, @b1, @b2\n\+                \@b1\n\+                \ret 0\n\+                \@b2\n\+                \ret 1\n\+                \}"++          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "main") qbe+          eTraces <- explore' prog funcDef []++          length eTraces @?= 2,+      testCase "make a range of memory symbolic" $+        do+          let qbe =+                "data $name = align 1 {  b \"array\", b 0 }\n\+                \function w $main() {\n\+                \@start\n\+                \%ptr =l alloc4 32\n\+                \call $qute_make_symbolic(l %ptr, l 8, l 4, l $name)\n\+                \%word =w loadw %ptr\n\+                \jnz %word, @b1, @b2\n\+                \@b1\n\+                \%ptr =l add %ptr, 4\n\+                \%word =w loadw %ptr\n\+                \jnz %word, @b3, @b4\n\+                \@b2\n\+                \ret 1\n\+                \@b3\n\+                \ret 0\n\+                \@b4\n\+                \ret 1\n\+                \}"++          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "main") qbe+          eTraces <- explore' prog funcDef []++          length eTraces @?= 3,+      testCase "explore a path with an error case" $+        do+          let qbe =+                "data $.Lstring.1 = align 1 { b \"a\", b 0 }\n\+                \export\n\+                \function w $main() {\n\+                \@body\n\+                \%.1 =l alloc4 4\n\+                \call $qute_make_symbolic(l %.1, l 1, l 4, l $.Lstring.1)\n\+                \%.2 =w loadw %.1\n\+                \%.3 =w ceqw %.2, 42\n\+                \jnz %.3, @error, @okay\n\+                \@error\n\+                \hlt\n\+                \@okay\n\+                \ret 0\n\+                \}"++          (prog, funcDef) <- parseAndFind (QBE.GlobalIdent "main") qbe+          (wErr, woErr) <-+            partition (isJust . pathErr)+              <$> explore' prog funcDef []++          length wErr @?= 1+          length woErr @?= 1++          let errorVars = pathVars $ fst $ fromJust $ uncons wErr+              errorVal = Map.lookup "a1" errorVars+          errorVal @?= Just (DE.VWord 42),+      testCase "explore program with multiple paths to error" $+        do+          (prog, funcDef) <-+            getFuncAndProg+              "insertion-sort-error-on-42.qbe"+              (QBE.GlobalIdent "main")+          (wErr, woErr) <-+            partition (isJust . pathErr)+              <$> explore' prog funcDef []++          length wErr @?= 8+          length woErr @?= 6++          -- every path on the error case must contain 42 in its input.+          let vals = map (Map.elems . pathVars) wErr+          let has42 = elem (DE.VWord 42)+          length (filter has42 vals) @?= length wErr,+      testCase "continue exploration after single path to error" $+        do+          (prog, funcDef) <-+            getFuncAndProg+              "single-error-case.qbe"+              (QBE.GlobalIdent "main")+          (wErr, woErr) <-+            partition (isJust . pathErr)+              <$> explore' prog funcDef []++          length wErr @?= 1+          length woErr @?= 20++          let errorVars = pathVars $ fst $ fromJust $ uncons wErr+              errorVal = Map.lookup "prime1" errorVars+          errorVal @?= Just (DE.VWord 43),+      testCase "exploration with memory error" $+        do+          (prog, funcDef) <-+            getFuncAndProg+              "out-of-bounds-error.qbe"+              (QBE.GlobalIdent "main")+          (wErr, woErr) <-+            partition (isJust . pathErr)+              <$> explore' prog funcDef []++          length wErr @?= 1+          length woErr @?= 3++          let errorVars = pathVars $ fst $ fromJust $ uncons wErr+              errorVal = Map.lookup "a1" errorVars+          errorVal @?= Just (DE.VWord 0x23523929)+    ]
+ test/Golden.hs view
@@ -0,0 +1,64 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Golden (goldenTests) where++import Data.Bifunctor (second)+import Language.QBE (parseAndFind)+import Language.QBE.Simulator.Concolic.State (mkEnv)+import Language.QBE.Simulator.Explorer (defSolver, exploreFunc, newEngine)+import Language.QBE.Types qualified as QBE+import System.FilePath+import Test.Tasty+import Test.Tasty.Golden.Advanced++type Result = Int++entryFunc :: QBE.GlobalIdent+entryFunc = QBE.GlobalIdent "entry"++exploreQBE :: FilePath -> [(String, QBE.BaseType)] -> IO Result+exploreQBE filePath params = do+  (prog, func) <- readFile filePath >>= parseAndFind entryFunc++  defEnv <- mkEnv prog 0 128 Nothing+  engine <- newEngine defEnv <$> defSolver++  traces <-+    exploreFunc engine func $+      map (second QBE.Base) params+  pure $ length traces++simpleCmp :: Result -> Result -> IO (Maybe String)+simpleCmp expt act =+  return $+    if expt == act+      then Nothing+      else Just ("Exploration mismatch: " ++ err)+  where+    err :: String+    err = "expected=" ++ show expt ++ " actual=" ++ show act++runTest :: TestName -> Int -> [(String, QBE.BaseType)] -> TestTree+runTest testName expPaths params =+  goldenTest+    testName+    (pure expPaths)+    (exploreQBE fullPath params)+    simpleCmp+    (\_ -> pure ())+  where+    fullPath :: FilePath+    fullPath = "test" </> "golden" </> (testName ++ ".qbe")++------------------------------------------------------------------------++goldenTests :: TestTree+goldenTests =+  testGroup+    "goldenTests"+    [ runTest "three-branches" 3 [("a", QBE.Word), ("b", QBE.Word)],+      runTest "prime-numbers" 21 [("a", QBE.Word)],+      runTest "address-concretization" 2 [("a", QBE.Word)]+    ]
+ test/Main.hs view
@@ -0,0 +1,28 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Main (main) where++import BV (bvTests)+import Backend (backendTests)+import Concolic qualified as CE+import Explorer (exploreTests)+import Golden (goldenTests)+import Symbolic qualified as SE+import Test.Tasty++main :: IO ()+main = defaultMain tests++tests :: TestTree+tests =+  testGroup+    "Tests"+    [ SE.exprTests,+      CE.exprTests,+      backendTests,+      exploreTests,+      goldenTests,+      bvTests+    ]
+ test/Symbolic.hs view
@@ -0,0 +1,261 @@+-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Symbolic (exprTests) where++import Data.Functor ((<&>))+import Data.Int (Int64)+import Data.Maybe (fromJust)+import Data.Word (Word32, Word64)+import Language.QBE.Simulator.Default.Expression qualified as DE+import Language.QBE.Simulator.Explorer (defSolver)+import Language.QBE.Simulator.Expression qualified as E+import Language.QBE.Simulator.Memory qualified as MEM+import Language.QBE.Simulator.Symbolic.Expression qualified as SE+import Language.QBE.Types qualified as QBE+import SimpleBV qualified as SMT+import Test.Tasty+import Test.Tasty.HUnit+import Test.Tasty.QuickCheck+  ( Arbitrary,+    Property,+    arbitrary,+    elements,+    ioProperty,+    testProperty,+  )++getSolver :: IO SMT.Solver+getSolver = do+  s <- defSolver+  SMT.check s >> pure s++eqConcrete :: Maybe SE.BitVector -> Maybe DE.RegVal -> IO Bool+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+eqConcrete Nothing Nothing = pure True+eqConcrete _ _ = pure False++------------------------------------------------------------------------++data UnaryInput = UnaryInput QBE.BaseType Word64+  deriving (Show)++instance Arbitrary UnaryInput where+  arbitrary = do+    t <- elements [QBE.Word, QBE.Long]+    UnaryInput t <$> arbitrary++unaryProp ::+  (SE.BitVector -> Maybe SE.BitVector) ->+  (DE.RegVal -> Maybe DE.RegVal) ->+  UnaryInput ->+  Property+unaryProp opSym opCon (UnaryInput ty val) = ioProperty $ do+  eqConcrete (opSym $ E.fromLit (QBE.Base ty) val) (opCon $ E.fromLit (QBE.Base ty) val)++negEquiv :: TestTree+negEquiv = testProperty "neg" (unaryProp E.neg E.neg)++------------------------------------------------------------------------++data BinaryInput = BinaryInput QBE.BaseType Word64 Word64+  deriving (Show)++instance Arbitrary BinaryInput where+  arbitrary = do+    ty <- elements [QBE.Word, QBE.Long]+    lhs <- arbitrary+    BinaryInput ty lhs <$> arbitrary++binaryEq ::+  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->+  (DE.RegVal -> DE.RegVal -> Maybe DE.RegVal) ->+  BinaryInput ->+  IO Bool+binaryEq opSym opCon (BinaryInput ty lhs rhs) =+  eqConcrete (opSym (mkS lhs) (mkS rhs)) (opCon (mkC lhs) (mkC rhs))+  where+    mkS :: Word64 -> SE.BitVector+    mkS = E.fromLit (QBE.Base ty)++    mkC :: Word64 -> DE.RegVal+    mkC = E.fromLit (QBE.Base ty)++binaryProp ::+  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->+  (DE.RegVal -> DE.RegVal -> Maybe DE.RegVal) ->+  BinaryInput ->+  Property+binaryProp opSym opCon input = ioProperty $ binaryEq opSym opCon input++opEquiv :: TestTree+opEquiv =+  testGroup+    "Operation equivalence"+    [ testProperty "add" (binaryProp E.add E.add),+      testProperty "sub" (binaryProp E.sub E.sub),+      testProperty "mul" (binaryProp E.mul E.mul),+      testProperty "div" (binaryProp E.div E.div),+      testProperty "or" (binaryProp E.or E.or),+      testProperty "xor" (binaryProp E.xor E.xor),+      testProperty "and" (binaryProp E.and E.and),+      testProperty "urem" (binaryProp E.urem E.urem),+      testProperty "srem" (binaryProp E.srem E.srem),+      testProperty "udiv" (binaryProp E.udiv E.udiv),+      testProperty "eq" (binaryProp E.eq E.eq),+      testProperty "ne" (binaryProp E.ne E.ne),+      testProperty "sle" (binaryProp E.sle E.sle),+      testProperty "slt" (binaryProp E.slt E.slt),+      testProperty "sge" (binaryProp E.sge E.sge),+      testProperty "sgt" (binaryProp E.sgt E.sgt),+      testProperty "ule" (binaryProp E.ule E.ule),+      testProperty "ult" (binaryProp E.ult E.ult),+      testProperty "uge" (binaryProp E.uge E.uge),+      testProperty "ugt" (binaryProp E.ugt E.ugt)+    ]++------------------------------------------------------------------------++data ShiftInput = ShiftInput QBE.BaseType Word64 Word32+  deriving (Show)++instance Arbitrary ShiftInput where+  arbitrary = do+    t <- elements [QBE.Word, QBE.Long]+    v <- arbitrary+    ShiftInput t v <$> arbitrary++shiftProp ::+  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->+  (DE.RegVal -> DE.RegVal -> Maybe DE.RegVal) ->+  ShiftInput ->+  Property+shiftProp opSym opCon (ShiftInput ty val amount) = ioProperty $ do+  let symValue = E.fromLit (QBE.Base ty) val :: SE.BitVector+  let conValue = E.fromLit (QBE.Base ty) val :: DE.RegVal++  let symResult = symValue `opSym` E.fromLit (QBE.Base QBE.Word) (fromIntegral amount)+  let conResult = conValue `opCon` E.fromLit (QBE.Base QBE.Word) (fromIntegral amount)++  eqConcrete symResult conResult++shiftEquiv :: TestTree+shiftEquiv =+  testGroup+    "Concrete and symbolic shifts are equivalent"+    [ testProperty "sar" (shiftProp E.sar E.sar),+      testProperty "shr" (shiftProp E.shr E.shr),+      testProperty "shl" (shiftProp E.shl E.shl)+    ]++------------------------------------------------------------------------++equivTests :: TestTree+equivTests =+  testGroup+    "Equivalence tests for symbolic and default expression interpreter"+    [ shiftEquiv,+      negEquiv,+      opEquiv,+      -- Occurs when the most-negative integer is divided by -1.+      testCase "Signed division overflow on div" $+        do+          let input =+                BinaryInput QBE.Long 0x8000000000000000 $+                  fromIntegral (-1 :: Int64)+          binaryEq E.div E.div input >>= assertBool "signed-div-overflow",+      testCase "Signed division overflow on srem" $+        do+          let input =+                BinaryInput QBE.Long 0x8000000000000000 $+                  fromIntegral (-1 :: Int64)+          binaryEq E.srem E.srem input >>= assertBool "signed-srem-overflow"+    ]++storeTests :: TestTree+storeTests =+  testGroup+    "Storage Instance Tests"+    [ testCase "Create bitvector and convert it to bytes" $+        do+          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+          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+          s <- getSolver++          let bytes = (MEM.toBytes (E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector) :: [SE.BitVector])+          length bytes @?= 4++          value <- case MEM.fromBytes (QBE.LBase QBE.Word) bytes of+            Just x -> SMT.getValue s (SE.toSExpr x) <&> Just+            Nothing -> pure Nothing+          value @?= Just (SMT.Bits 32 0xdeadbeef)+    ]++valueReprTests :: TestTree+valueReprTests =+  testGroup+    "Symbolic ValueRepr Tests"+    [ testCase "create from literal and add" $+        do+          s <- getSolver++          let v1 = E.fromLit (QBE.Base QBE.Word) 127+          let v2 = E.fromLit (QBE.Base QBE.Word) 128++          expr <- SMT.getValue s (SE.toSExpr $ fromJust $ v1 `E.add` v2)+          expr @?= SMT.Bits 32 0xff,+      testCase "add incompatible values" $+        do+          let v1 = E.fromLit (QBE.Base QBE.Word) 0xffffffff :: SE.BitVector+          let v2 = E.fromLit (QBE.Base QBE.Long) 0xff :: SE.BitVector++          -- Note: E.add doesn't do subtyping if invoked directly+          (v1 `E.add` v2) @?= Nothing,+      testCase "extend" $+        do+          s <- getSolver++          let v1 = E.fromLit QBE.Byte 0xff :: SE.BitVector+              ext1 = fromJust $ E.extend QBE.HalfWord False v1+          ext1Val <- SMT.getValue s (SE.toSExpr ext1)+          ext1Val @?= SMT.Bits 16 0x00ff++          let v2 = E.fromLit QBE.Byte 0xab :: SE.BitVector+              ext2 = fromJust $ E.extend (QBE.Base QBE.Word) True v2+          ext2Val <- SMT.getValue s (SE.toSExpr ext2)+          ext2Val @?= SMT.Bits 32 0xffffffab++          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,+      testCase "extract" $+        do+          s <- getSolver++          let value = E.fromLit (QBE.Base QBE.Word) 0xdeadbeef :: SE.BitVector++          let ex1 = fromJust $ E.extract QBE.Byte value+          ex1Val <- SMT.getValue s (SE.toSExpr ex1)+          ex1Val @?= SMT.Bits 8 0xef++          let ex2 = fromJust $ E.extract QBE.HalfWord value+          ex2Val <- SMT.getValue s (SE.toSExpr ex2)+          ex2Val @?= SMT.Bits 16 0xbeef++          E.extract (QBE.Base QBE.Word) value @?= Just value+          E.extract (QBE.Base QBE.Long) value @?= Nothing+    ]++exprTests :: TestTree+exprTests = testGroup "Expression tests" [storeTests, valueReprTests, equivTests]
+ test/Util.hs view
@@ -0,0 +1,44 @@+-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel <soeren+git@soeren-tempel.net>+--+-- SPDX-License-Identifier: GPL-3.0-only++module Util where++import Data.Bifunctor (second)+import Data.Word (Word64)+import Language.QBE (parseAndFind)+import Language.QBE.Backend.Tracer qualified as T+import Language.QBE.Simulator (execFunc)+import Language.QBE.Simulator.Concolic.Expression qualified as CE+import Language.QBE.Simulator.Concolic.State (mkEnv, run)+import Language.QBE.Simulator.Default.Expression qualified as DE+import Language.QBE.Simulator.Explorer (PathResult, defSolver, exploreFunc, newEngine)+import Language.QBE.Simulator.Expression qualified as E+import Language.QBE.Simulator.Symbolic.Expression qualified as SE+import Language.QBE.Types qualified as QBE+import SimpleBV qualified as SMT++parseAndExec :: QBE.GlobalIdent -> [CE.Concolic DE.RegVal] -> String -> IO T.ExecTrace+parseAndExec funcName params input = do+  (prog, entry) <- parseAndFind funcName input++  env <- mkEnv prog 0 128 Nothing+  fst <$> run env (execFunc entry params)++unconstrained :: SMT.Solver -> Word64 -> String -> QBE.BaseType -> IO (CE.Concolic DE.RegVal)+unconstrained solver initCon name ty = do+  let symbolic = SE.symbolic name (QBE.Base ty)+  -- XXX: This is a hack, normally the Store does this for us.+  _ <- SMT.declareBV solver name $ SE.bitSize symbolic++  let concrete = E.fromLit (QBE.Base ty) initCon+  pure $ CE.Concolic concrete (Just symbolic)++explore' :: String -> String -> [(String, QBE.BaseType)] -> IO [PathResult]+explore' input funcName params = do+  (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