qute-symex-0.1.0: A symbolic execution engine for the QBE intermediate language.

Safe Haskell	None
Language	GHC2021

Language.QBE.Backend.Store

Synopsis

data Store
type Assign = Map String RegVal
empty :: StdGen -> Store
sexprs :: Store -> [SExpr]
finalize :: Solver -> Store -> IO Store
setModel :: Store -> Model -> Store
getConcolic :: Store -> String -> ExtType -> (Store, Concolic RegVal)

Documentation

data Store Source #

type Assign = Map String RegVal Source #

Concrete variable assignment.

empty :: StdGen -> Store Source #

Create a new (empty) store.

sexprs :: Store -> [SExpr] Source #

Obtain symbolic values as a list of SimpleBV expressions.

finalize :: Solver -> Store -> IO Store Source #

Finalize all pending symbolic variable declarations.

setModel :: Store -> Model -> Store Source #

Create a variable store from a Model.

getConcolic :: Store -> String -> ExtType -> (Store, Concolic RegVal) Source #

Lookup the variable name in the store, if it doesn't exist return an unconstrained Concolic value with a random concrete part.