EVM.SMT

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

data CexVars

Constructors

CexVars

Fields

• calldata :: [Text]
• buffers :: Map Text (Expr EWord)
• storeReads :: [(Expr EWord, Expr EWord)]
• blockContext :: [Text]
• txContext :: [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 BufModel

A model for a buffer, either in it's compressed form (for storing parsed models from a solver), or as a bytestring (for presentation to users)

Constructors

Comp CompressedBuf

Flat ByteString

Instances

Show BufModel

Defined in EVM.SMT

Methods

showsPrec :: Int -> BufModel -> ShowS

show :: BufModel -> String

showList :: [BufModel] -> ShowS

Eq BufModel

Defined in EVM.SMT

Methods

(==) :: BufModel -> BufModel -> Bool

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

data CompressedBuf

This representation lets us store buffers of arbitrary length without exhausting the available memory, it closely matches the format used by smt-lib when returning models for arrays

Constructors

Base

Fields

• byte :: Word8
• length :: W256

Write

Fields

• byte :: Word8
• idx :: W256
• next :: CompressedBuf

Instances

Show CompressedBuf

Defined in EVM.SMT

Methods

showsPrec :: Int -> CompressedBuf -> ShowS

show :: CompressedBuf -> String

showList :: [CompressedBuf] -> ShowS

Eq CompressedBuf

Defined in EVM.SMT

Methods

(==) :: CompressedBuf -> CompressedBuf -> Bool

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

data SMTCex

a final post shrinking cex, buffers here are all represented as concrete bytestrings

Constructors

SMTCex

Fields

• vars :: Map (Expr EWord) W256
• buffers :: Map (Expr Buf) BufModel
• store :: Map W256 (Map W256 W256)
• 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

flattenBufs :: SMTCex -> Maybe SMTCex

collapse :: BufModel -> Maybe BufModel

Attemps to collapse a compressed buffer representation down to a flattened one

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

referencedBufsGo :: Expr a -> [Builder]

referencedBufs :: Expr a -> [Builder]

referencedBufs' :: Prop -> [Builder]

referencedVarsGo :: Expr a -> [Builder]

referencedVars :: Expr a -> [Builder]

referencedVars' :: Prop -> [Builder]

referencedFrameContextGo :: Expr a -> [Builder]

referencedFrameContext :: Expr a -> [Builder]

referencedFrameContext' :: Prop -> [Builder]

referencedBlockContextGo :: Expr a -> [Builder]

referencedBlockContext :: Expr a -> [Builder]

referencedBlockContext' :: Prop -> [Builder]

findStorageReads :: Prop -> [(Expr EWord, Expr EWord)]

This function overapproximates the reads from the abstract storage. Potentially, it can return locations that do not read a slot directly from the abstract store but from subsequent writes on the store (e.g, SLoad addr idx (SStore addr idx val AbstractStore)). However, we expect that most of such reads will have been simplified away.

findBufferAccess :: TraversableTerm a => [a] -> [(Expr EWord, Expr EWord, Expr Buf)]

assertReads :: [Prop] -> BufEnv -> StoreEnv -> [Prop]

Asserts that buffer reads beyond the size of the buffer are equal to zero. Looks for buffer reads in the a list of given predicates and the buffer and storage environments.

discoverMaxReads :: [Prop] -> BufEnv -> StoreEnv -> Map Text (Expr EWord)

Finds the maximum read index for each abstract buffer in the input props

declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2

Returns an SMT2 object with all buffers referenced from the input props declared, and with the appropriate cex extraction metadata attached

declareVars :: [Builder] -> SMT2

declareFrameContext :: [Builder] -> SMT2

declareBlockContext :: [Builder] -> SMT2

prelude :: SMT2

exprToSMT :: Expr a -> Builder

sp :: Builder -> Builder -> Builder

zero :: Builder

one :: Builder

propToSMT :: Prop -> Builder

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

Cex parsing ** --------------------------------------------------------------------------------

parseW256 :: SpecConstant -> W256

parseInteger :: SpecConstant -> Integer

parseW8 :: SpecConstant -> Word8

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

parseErr :: Show a => a -> b

parseVar :: Text -> Expr EWord

parseBlockCtx :: Text -> Expr EWord

parseFrameCtx :: Text -> Expr EWord

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

queryMaxReads :: (Text -> IO Text) -> Map Text (Expr EWord) -> IO (Map Text W256)

Queries the solver for models for each of the expressions representing the max read index for a given buffer

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

Gets the initial model for each buffer, these will often be much too large for our purposes

getStore :: (Text -> IO Text) -> [(Expr EWord, Expr EWord)] -> IO (Map W256 (Map W256 W256))

queryValue :: (Text -> IO Text) -> Expr EWord -> IO W256

interpretNDArray :: (Map Symbol Term -> Term -> a) -> Map Symbol Term -> Term -> W256 -> a

Interpret an N-dimensional array as a value of type a. Parameterized by an interpretation function for array values.

interpret1DArray :: Map Symbol Term -> Term -> W256 -> W256

Interpret an 1-dimensional array as a function

interpret2DArray :: Map Symbol Term -> Term -> W256 -> W256 -> W256

Interpret an 2-dimensional array as a function