diff --git a/bench/Exec.hs b/bench/Exec.hs new file mode 100644 --- /dev/null +++ b/bench/Exec.hs @@ -0,0 +1,41 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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 + ] diff --git a/bench/Main.hs b/bench/Main.hs new file mode 100644 --- /dev/null +++ b/bench/Main.hs @@ -0,0 +1,12 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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] diff --git a/bench/SMT.hs b/bench/SMT.hs new file mode 100644 --- /dev/null +++ b/bench/SMT.hs @@ -0,0 +1,79 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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) diff --git a/bench/SMTUnwind.hs b/bench/SMTUnwind.hs new file mode 100644 --- /dev/null +++ b/bench/SMTUnwind.hs @@ -0,0 +1,100 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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` "") diff --git a/qute-symex.cabal b/qute-symex.cabal new file mode 100644 --- /dev/null +++ b/qute-symex.cabal @@ -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 diff --git a/src/Language/QBE/Backend.hs b/src/Language/QBE/Backend.hs new file mode 100644 --- /dev/null +++ b/src/Language/QBE/Backend.hs @@ -0,0 +1,30 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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 diff --git a/src/Language/QBE/Backend/DFS.hs b/src/Language/QBE/Backend/DFS.hs new file mode 100644 --- /dev/null +++ b/src/Language/QBE/Backend/DFS.hs @@ -0,0 +1,73 @@ +-- SPDX-FileCopyrightText: 2024 University of Bremen +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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 diff --git a/src/Language/QBE/Backend/ExecTree.hs b/src/Language/QBE/Backend/ExecTree.hs new file mode 100644 --- /dev/null +++ b/src/Language/QBE/Backend/ExecTree.hs @@ -0,0 +1,83 @@ +-- SPDX-FileCopyrightText: 2024 University of Bremen +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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 diff --git a/src/Language/QBE/Backend/Model.hs b/src/Language/QBE/Backend/Model.hs new file mode 100644 --- /dev/null +++ b/src/Language/QBE/Backend/Model.hs @@ -0,0 +1,31 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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" diff --git a/src/Language/QBE/Backend/Store.hs b/src/Language/QBE/Backend/Store.hs new file mode 100644 --- /dev/null +++ b/src/Language/QBE/Backend/Store.hs @@ -0,0 +1,90 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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) diff --git a/src/Language/QBE/Backend/Tracer.hs b/src/Language/QBE/Backend/Tracer.hs new file mode 100644 --- /dev/null +++ b/src/Language/QBE/Backend/Tracer.hs @@ -0,0 +1,102 @@ +-- SPDX-FileCopyrightText: 2024 University of Bremen +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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 diff --git a/src/Language/QBE/Simulator/Concolic/Expression.hs b/src/Language/QBE/Simulator/Concolic/Expression.hs new file mode 100644 --- /dev/null +++ b/src/Language/QBE/Simulator/Concolic/Expression.hs @@ -0,0 +1,146 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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) diff --git a/src/Language/QBE/Simulator/Concolic/State.hs b/src/Language/QBE/Simulator/Concolic/State.hs new file mode 100644 --- /dev/null +++ b/src/Language/QBE/Simulator/Concolic/State.hs @@ -0,0 +1,219 @@ +-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel +-- +-- 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 diff --git a/src/Language/QBE/Simulator/Explorer.hs b/src/Language/QBE/Simulator/Explorer.hs new file mode 100644 --- /dev/null +++ b/src/Language/QBE/Simulator/Explorer.hs @@ -0,0 +1,166 @@ +-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel +-- +-- 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] diff --git a/src/Language/QBE/Simulator/Symbolic/Expression.hs b/src/Language/QBE/Simulator/Symbolic/Expression.hs new file mode 100644 --- /dev/null +++ b/src/Language/QBE/Simulator/Symbolic/Expression.hs @@ -0,0 +1,213 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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" diff --git a/src/SimpleBV.hs b/src/SimpleBV.hs new file mode 100644 --- /dev/null +++ b/src/SimpleBV.hs @@ -0,0 +1,430 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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 diff --git a/test/BV.hs b/test/BV.hs new file mode 100644 --- /dev/null +++ b/test/BV.hs @@ -0,0 +1,87 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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] diff --git a/test/Backend.hs b/test/Backend.hs new file mode 100644 --- /dev/null +++ b/test/Backend.hs @@ -0,0 +1,133 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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] diff --git a/test/Concolic.hs b/test/Concolic.hs new file mode 100644 --- /dev/null +++ b/test/Concolic.hs @@ -0,0 +1,35 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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] diff --git a/test/Explorer.hs b/test/Explorer.hs new file mode 100644 --- /dev/null +++ b/test/Explorer.hs @@ -0,0 +1,313 @@ +-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel +-- +-- 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) + ] diff --git a/test/Golden.hs b/test/Golden.hs new file mode 100644 --- /dev/null +++ b/test/Golden.hs @@ -0,0 +1,64 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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)] + ] diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,28 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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 + ] diff --git a/test/Symbolic.hs b/test/Symbolic.hs new file mode 100644 --- /dev/null +++ b/test/Symbolic.hs @@ -0,0 +1,261 @@ +-- SPDX-FileCopyrightText: 2025 Sören Tempel +-- +-- 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] diff --git a/test/Util.hs b/test/Util.hs new file mode 100644 --- /dev/null +++ b/test/Util.hs @@ -0,0 +1,44 @@ +-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel +-- +-- 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