EVM.SMT

Encoding ** ----------------------------------------------------------------------------------

data CexVars

Constructors

CexVars

Fields

• calldataV :: [Text]
• buffersV :: [Text]
• blockContextV :: [Text]
• txContextV :: [Text]

Instances

Monoid CexVars

Defined in EVM.SMT

Methods

mempty :: CexVars

mappend :: CexVars -> CexVars -> CexVars

mconcat :: [CexVars] -> CexVars

Semigroup CexVars

Defined in EVM.SMT

Methods

(<>) :: CexVars -> CexVars -> CexVars

sconcat :: NonEmpty CexVars -> CexVars

stimes :: Integral b => b -> CexVars -> CexVars

Show CexVars

Defined in EVM.SMT

Methods

showsPrec :: Int -> CexVars -> ShowS

show :: CexVars -> String

showList :: [CexVars] -> ShowS

Eq CexVars

Defined in EVM.SMT

Methods

(==) :: CexVars -> CexVars -> Bool

(/=) :: CexVars -> CexVars -> Bool

data SMTCex

Constructors

SMTCex

Fields

• vars :: Map (Expr EWord) W256
• buffers :: Map (Expr Buf) ByteString
• blockContext :: Map (Expr EWord) W256
• txContext :: Map (Expr EWord) W256

Instances

Show SMTCex

Defined in EVM.SMT

Methods

showsPrec :: Int -> SMTCex -> ShowS

show :: SMTCex -> String

showList :: [SMTCex] -> ShowS

Eq SMTCex

Defined in EVM.SMT

Methods

(==) :: SMTCex -> SMTCex -> Bool

(/=) :: SMTCex -> SMTCex -> Bool

getVar :: SMTCex -> Text -> W256

data SMT2

Constructors

SMT2 [Builder] CexVars

Instances

Monoid SMT2

Defined in EVM.SMT

Methods

mempty :: SMT2

mappend :: SMT2 -> SMT2 -> SMT2

mconcat :: [SMT2] -> SMT2

Semigroup SMT2

Defined in EVM.SMT

Methods

(<>) :: SMT2 -> SMT2 -> SMT2

sconcat :: NonEmpty SMT2 -> SMT2

stimes :: Integral b => b -> SMT2 -> SMT2

Show SMT2

Defined in EVM.SMT

Methods

showsPrec :: Int -> SMT2 -> ShowS

show :: SMT2 -> String

showList :: [SMT2] -> ShowS

Eq SMT2

Defined in EVM.SMT

Methods

(==) :: SMT2 -> SMT2 -> Bool

(/=) :: SMT2 -> SMT2 -> Bool

formatSMT2 :: SMT2 -> Text

declareIntermediates :: BufEnv -> StoreEnv -> SMT2

Reads all intermediate variables from the builder state and produces SMT declaring them as constants

assertProps :: [Prop] -> SMT2

prelude :: SMT2

declareBufs :: [Builder] -> SMT2

referencedBufs :: Expr a -> [Builder]

referencedBufs' :: Prop -> [Builder]

referencedVars' :: Prop -> [Builder]

referencedFrameContext' :: Prop -> [Builder]

referencedBlockContext' :: Prop -> [Builder]

declareVars :: [Builder] -> SMT2

referencedVars :: Expr a -> [Builder]

declareFrameContext :: [Builder] -> SMT2

referencedFrameContext :: Expr a -> [Builder]

declareBlockContext :: [Builder] -> SMT2

referencedBlockContext :: Expr a -> [Builder]

exprToSMT :: Expr a -> Builder

sp :: Builder -> Builder -> Builder

zero :: Builder

one :: Builder

propToSMT :: Prop -> Builder

Execution ** -------------------------------------------------------------------------------

data Solver

Supported solvers

Constructors

Z3

CVC5

Bitwuzla

Custom Text

Instances

Show Solver

Defined in EVM.SMT

Methods

showsPrec :: Int -> Solver -> ShowS

show :: Solver -> String

showList :: [Solver] -> ShowS

data SolverInstance

A running solver instance

Constructors

SolverInstance

Fields

• _type :: Solver
• _stdin :: Handle
• _stdout :: Handle
• _stderr :: Handle
• _process :: ProcessHandle

newtype SolverGroup

A channel representing a group of solvers

Constructors

SolverGroup (Chan Task)

data Task

A script to be executed, a list of models to be extracted in the case of a sat result, and a channel where the result should be written

Constructors

Task

Fields

• script :: SMT2
• resultChan :: Chan CheckSatResult

data CheckSatResult

The result of a call to (check-sat)

Constructors

Sat SMTCex

Unsat

Unknown

Error Text

Instances

Show CheckSatResult

Defined in EVM.SMT

Methods

showsPrec :: Int -> CheckSatResult -> ShowS

show :: CheckSatResult -> String

showList :: [CheckSatResult] -> ShowS

Eq CheckSatResult

Defined in EVM.SMT

Methods

(==) :: CheckSatResult -> CheckSatResult -> Bool

(/=) :: CheckSatResult -> CheckSatResult -> Bool

isSat :: CheckSatResult -> Bool

isErr :: CheckSatResult -> Bool

isUnsat :: CheckSatResult -> Bool

checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult

parseW256 :: SpecConstant -> W256

parseInteger :: SpecConstant -> Integer

parseW8 :: SpecConstant -> Word8

parseErr :: Show a => a -> b

parseVar :: Text -> Expr EWord

parseBlockCtx :: Text -> Expr EWord

parseFrameCtx :: Text -> Expr EWord

getVars :: (Text -> Expr EWord) -> SolverInstance -> [Text] -> IO (Map (Expr EWord) W256)

getBufs :: SolverInstance -> [Text] -> IO (Map (Expr Buf) ByteString)

parseSC :: (Num a, Eq a) => SpecConstant -> a

withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a

solverArgs :: Solver -> Maybe Natural -> [Text]

Arguments used when spawing a solver instance

spawnSolver :: Solver -> Maybe Natural -> IO SolverInstance

Spawns a solver instance, and sets the various global config options that we use for our queries

stopSolver :: SolverInstance -> IO ()

Cleanly shutdown a running solver instnace

sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())

Sends a list of commands to the solver. Returns the first error, if there was one.

sendCommand :: SolverInstance -> Text -> IO Text

Sends a single command to the solver, returns the first available line from the output buffer

sendLine :: SolverInstance -> Text -> IO Text

Sends a string to the solver and appends a newline, returns the first available line from the output buffer

sendLine' :: SolverInstance -> Text -> IO ()

Sends a string to the solver and appends a newline, doesn't return stdout

getValue :: SolverInstance -> Text -> IO Text

Returns a string representation of the model for the requested variable

readSExpr :: Handle -> IO [Text]

Reads lines from h until we have a balanced sexpr

Helpers ** ---------------------------------------------------------------------------------

copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Builder

Stores a region of src into dst

expandExp :: Expr EWord -> W256 -> Builder

Unrolls an exponentiation into a series of multiplications

concatBytes :: [Expr Byte] -> Builder

Concatenates a list of bytes into a larger bitvector

writeBytes :: ByteString -> Expr Buf -> Builder

Concatenates a list of bytes into a larger bitvector

encodeConcreteStore :: Map W256 (Map W256 W256) -> Builder