EVM.SMT

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

data CexVars

Data that we need to construct a nice counterexample

Constructors

CexVars

Fields

• calldata :: [Text]

  variable names that we need models for to reconstruct calldata

• addrs :: [Text]

  symbolic address names

• buffers :: Map Text (Expr EWord)

  buffer names and guesses at their maximum size

• storeReads :: Map (Expr EAddr, Maybe W256) (Set (Expr EWord))

  reads from abstract storage

• blockContext :: [Text]

  the names of any block context variables

• txContext :: [Text]

  the names of any tx context variables

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
• addrs :: Map (Expr EAddr) Addr
• buffers :: Map (Expr Buf) BufModel
• store :: Map (Expr EAddr) (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

data RefinementEqs

Used for abstraction-refinement of the SMT formula. Contains assertions that make our query fully precise. These will be added to the assertion stack if we get sat with the abstracted query.

Constructors

RefinementEqs [Builder] [Prop]

Instances

Monoid RefinementEqs

Defined in EVM.SMT

Methods

mempty :: RefinementEqs

mappend :: RefinementEqs -> RefinementEqs -> RefinementEqs

mconcat :: [RefinementEqs] -> RefinementEqs

Semigroup RefinementEqs

Defined in EVM.SMT

Methods

(<>) :: RefinementEqs -> RefinementEqs -> RefinementEqs

sconcat :: NonEmpty RefinementEqs -> RefinementEqs

stimes :: Integral b => b -> RefinementEqs -> RefinementEqs

Show RefinementEqs

Defined in EVM.SMT

Methods

showsPrec :: Int -> RefinementEqs -> ShowS

show :: RefinementEqs -> String

showList :: [RefinementEqs] -> ShowS

Eq RefinementEqs

Defined in EVM.SMT

Methods

(==) :: RefinementEqs -> RefinementEqs -> Bool

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

flattenBufs :: SMTCex -> Maybe SMTCex

collapse :: BufModel -> Maybe BufModel

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

getVar :: SMTCex -> Text -> W256

data SMT2

Constructors

SMT2 [Builder] RefinementEqs CexVars [Prop]

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

data AbstState

Constructors

AbstState

Fields

• words :: Map (Expr EWord) Int
• count :: Int

Instances

Show AbstState

Defined in EVM.SMT

Methods

showsPrec :: Int -> AbstState -> ShowS

show :: AbstState -> String

showList :: [AbstState] -> ShowS

abstractAwayProps :: Config -> [Prop] -> ([Prop], AbstState)

smt2Line :: Builder -> SMT2

assertProps :: Config -> [Prop] -> SMT2

assertPropsNoSimp :: Config -> [Prop] -> SMT2

referencedAbstractStores :: TraversableTerm a => a -> Set Builder

referencedWAddrs :: TraversableTerm a => a -> Set Builder

referencedBufs :: TraversableTerm a => a -> [Builder]

referencedVars :: TraversableTerm a => a -> [Builder]

referencedFrameContext :: TraversableTerm a => a -> [(Builder, [Prop])]

referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])]

findStorageReads :: Prop -> Map (Expr EAddr, Maybe W256) (Set (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

declareAddrs :: [Builder] -> SMT2

declareFrameContext :: [(Builder, [Prop])] -> SMT2

declareAbstractStores :: [Builder] -> SMT2

declareBlockContext :: [(Builder, [Prop])] -> 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 W256 -> Builder

storeName :: Expr EAddr -> Maybe W256 -> Builder

formatEAddr :: Expr EAddr -> Builder

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

parseAddr :: SpecConstant -> Addr

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

parseEAddr :: Text -> Expr EAddr

parseBlockCtx :: Text -> Expr EWord

parseTxCtx :: Text -> Expr EWord

getAddrs :: (Text -> Expr EAddr) -> (Text -> IO Text) -> [Text] -> IO (Map (Expr EAddr) Addr)

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

getOne :: (SpecConstant -> a) -> (Text -> IO Text) -> Map Text a -> Text -> IO (Map Text a)

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) -> Map (Expr EAddr, Maybe W256) (Set (Expr EWord)) -> IO (Map (Expr EAddr) (Map W256 W256))

Takes a Map containing all reads from a store with an abstract base, as well as the concrete part of the storage prestate and returns a fully concretized storage

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

Ask the solver to give us the concrete value of an arbitrary abstract word

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