EVM.Expr

Helper functions for working with Expr instances. All functions here will return a concrete result if given a concrete input.

Constants **

maxLit :: W256

Stack Ops ** ---------------------------------------------------------------------------------

op1 :: (Expr EWord -> Expr EWord) -> (W256 -> W256) -> Expr EWord -> Expr EWord

op2 :: (Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord

op3 :: (Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord

normArgs :: (Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord

If a given binary op is commutative, then we always force Lits to the lhs if only one argument is a Lit. This makes writing pattern matches in the simplifier easier.

add :: Expr EWord -> Expr EWord -> Expr EWord

sub :: Expr EWord -> Expr EWord -> Expr EWord

mul :: Expr EWord -> Expr EWord -> Expr EWord

div :: Expr EWord -> Expr EWord -> Expr EWord

sdiv :: Expr EWord -> Expr EWord -> Expr EWord

mod :: Expr EWord -> Expr EWord -> Expr EWord

smod :: Expr EWord -> Expr EWord -> Expr EWord

addmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord

mulmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord

exp :: Expr EWord -> Expr EWord -> Expr EWord

sex :: Expr EWord -> Expr EWord -> Expr EWord

lt :: Expr EWord -> Expr EWord -> Expr EWord

gt :: Expr EWord -> Expr EWord -> Expr EWord

leq :: Expr EWord -> Expr EWord -> Expr EWord

geq :: Expr EWord -> Expr EWord -> Expr EWord

slt :: Expr EWord -> Expr EWord -> Expr EWord

sgt :: Expr EWord -> Expr EWord -> Expr EWord

eq :: Expr EWord -> Expr EWord -> Expr EWord

iszero :: Expr EWord -> Expr EWord

and :: Expr EWord -> Expr EWord -> Expr EWord

or :: Expr EWord -> Expr EWord -> Expr EWord

xor :: Expr EWord -> Expr EWord -> Expr EWord

not :: Expr EWord -> Expr EWord

shl :: Expr EWord -> Expr EWord -> Expr EWord

shr :: Expr EWord -> Expr EWord -> Expr EWord

sar :: Expr EWord -> Expr EWord -> Expr EWord

Bufs ** --------------------------------------------------------------------------------------

readByte :: Expr EWord -> Expr Buf -> Expr Byte

Extracts the byte at a given index from a Buf.

We do our best to return a concrete value wherever possible, but fallback to an abstract expression if necessary. Note that a Buf is an infinite structure, so reads outside of the bounds of a ConcreteBuf return 0. This is inline with the semantics of calldata and memory, but not of returndata.

readBytes :: Int -> Expr EWord -> Expr Buf -> Expr EWord

Reads n bytes starting from idx in buf and returns a left padded word

If n is >= 32 this is the same as readWord

readWord :: Expr EWord -> Expr Buf -> Expr EWord

Reads the word starting at idx from the given buf

readWordFromBytes :: Expr EWord -> Expr Buf -> Expr EWord

maxBytes :: W256

Copies a slice of src into dst.

0 srcOffset srcOffset + size length src ┌--------------┬------------------┬-----------------┐ src: | | ------ sl ------ | | └--------------┴------------------┴-----------------┘

0 dstOffset dstOffset + size length dst ┌--------┬------------------┬-----------------┐ dst: | hd | | tl | └--------┴------------------┴-----------------┘

copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf -> Expr Buf

writeByte :: Expr EWord -> Expr Byte -> Expr Buf -> Expr Buf

writeWord :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf

bufLength :: Expr Buf -> Expr EWord

Returns the length of a given buffer

If there are any writes to abstract locations, or CopySlices with an abstract size or dstOffset, an abstract expression will be returned.

bufLengthEnv :: Map Int (Expr Buf) -> Bool -> Expr Buf -> Expr EWord

minLength :: Map Int (Expr Buf) -> Expr Buf -> Maybe Integer

Return the minimum possible length of a buffer. In the case of an abstract buffer, it is the largest write that is made on a concrete location. Parameterized by an environment for buffer variables.

concretePrefix :: Expr Buf -> Vector Word8

word256At :: Expr EWord -> Lens (Expr Buf) (Expr Buf) (Expr EWord) (Expr EWord)

take :: W256 -> Expr Buf -> Expr Buf

Returns the first n bytes of buf

drop :: W256 -> Expr Buf -> Expr Buf

Returns everything but the first n bytes of buf

slice :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf

toList :: Expr Buf -> Maybe (Vector (Expr Byte))

fromList :: Vector (Expr Byte) -> Expr Buf

simplifyReads :: Expr a -> Expr a

Removes any irrelevant writes when reading from a buffer

stripWrites :: W256 -> W256 -> Expr Buf -> Expr Buf

Strips writes from the buffer that can be statically determined to be out of range TODO: are the bounds here correct? I think there might be some off by one mistakes...

Storage ** -----------------------------------------------------------------------------------

readStorage' :: Expr EWord -> Expr Storage -> Expr EWord

readStorage :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)

Reads the word at the given slot from the given storage expression.

Note that we return a Nothing instead of a 0x0 if we are reading from a store that is backed by a ConcreteStore or an EmptyStore and there have been no explicit writes to the requested slot. This makes implementing rpc storage lookups much easier. If the store is backed by an AbstractStore we always return a symbolic value.

pattern MappingSlot :: ByteString -> Expr EWord -> Expr EWord

pattern Keccak64Bytes :: Expr EWord

pattern ArraySlotWithOffset :: ByteString -> Expr EWord -> Expr EWord

pattern ArraySlotZero :: ByteString -> Expr EWord

idsDontMatch :: ByteString -> ByteString -> Bool

slotPos :: Word8 -> ByteString

structureArraySlots :: Expr a -> Expr a

Turns Literals into keccak(bytes32(id)) + offset (i.e. writes to arrays)

litToArrayPreimage :: W256 -> Maybe (Word8, W256)

writeStorage :: Expr EWord -> Expr EWord -> Expr Storage -> Expr Storage

Writes a value to a key in a storage expression.

Concrete writes on top of a concrete or empty store will produce a new ConcreteStore, otherwise we add a new write to the storage expression.

getAddr :: Expr Storage -> Maybe (Expr EAddr)

getLogicalIdx :: Expr Storage -> Maybe W256

Whole Expression Simplification ** -----------------------------------------------------------

data StorageType

Constructors

SmallSlot

Array

Map

Mixed

UNK

Instances

Show StorageType

Defined in EVM.Expr

Methods

showsPrec :: Int -> StorageType -> ShowS

show :: StorageType -> String

showList :: [StorageType] -> ShowS

Eq StorageType

Defined in EVM.Expr

Methods

(==) :: StorageType -> StorageType -> Bool

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

safeToDecompose :: Expr a -> Bool

decomposeStorage :: Expr a -> Maybe (Expr a)

Splits storage into logical sub-stores if (1) all SLoad->SStore* chains are one of: (1a) Lit < 256, (1b) MappingSlot, (1c) ArraySlotWithOffset, (1d) ArraySlotZero and (2) there is no mixing of different types (e.g. Map with Array) within the same SStore -> SLoad* chain, and (3) there is no mixing of different array/map slots.

Mixing (2) and (3) are attempted to be prevented (if possible) as part of the rewrites done by the readStorage function that is ran before this. If there is still mixing here, we abort with a Nothing.

We do NOT rewrite stand-alone SStore-s (i.e. SStores that are not read), since they are often used to describe a post-state, and are not dispatched as-is to the solver

simplify :: Expr a -> Expr a

Simple recursive match based AST simplification Note: may not terminate!

Prop Simplification ** -----------------------------------------------------------------------

simplifyProps :: [Prop] -> [Prop]

simplifyProp :: Prop -> Prop

Evaluate the provided proposition down to its most concrete result Also simplifies the inner Expr, if it exists

flattenProps :: [Prop] -> [Prop]

remRedundantProps :: [Prop] -> [Prop]

Conversions ** -------------------------------------------------------------------------------

litAddr :: Addr -> Expr EWord

exprToAddr :: Expr EWord -> Maybe Addr

wordToAddr :: Expr EWord -> Maybe (Expr EAddr)

litCode :: ByteString -> [Expr Byte]

to512 :: W256 -> Word512

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

isLitByte :: Expr Byte -> Bool

isLitWord :: Expr EWord -> Bool

isSuccess :: Expr End -> Bool

isFailure :: Expr End -> Bool

isPartial :: Expr End -> Bool

indexWord :: Expr EWord -> Expr EWord -> Expr Byte

Returns the byte at idx from the given word.

padByte :: Expr Byte -> Expr EWord

bytesToW256 :: [Word8] -> W256

Converts a list of bytes into a W256. TODO: semantics if the input is too large?

padBytesLeft :: Int -> [Expr Byte] -> [Expr Byte]

joinBytes :: [Expr Byte] -> Expr EWord

eqByte :: Expr Byte -> Expr Byte -> Expr EWord

min :: Expr EWord -> Expr EWord -> Expr EWord

max :: Expr EWord -> Expr EWord -> Expr EWord

numBranches :: Expr End -> Int

allLit :: [Expr Byte] -> Bool

containsNode :: (forall a. Expr a -> Bool) -> Expr b -> Bool

True if the given expression contains any node that satisfies the input predicate

inRange :: Int -> Expr EWord -> Prop

preImages :: [(W256, Word8)]

images of keccak(bytes32(x)) where 0 <= x < 256

data ConstState

Constructors

ConstState

Fields

• values :: Map (Expr EWord) W256
• canBeSat :: Bool

Instances

Show ConstState

Defined in EVM.Expr

Methods

showsPrec :: Int -> ConstState -> ShowS

show :: ConstState -> String

showList :: [ConstState] -> ShowS

constFoldProp :: [Prop] -> Bool

Folds constants

concKeccakSimpExpr :: Expr a -> Expr a

concKeccakProps :: [Prop] -> [Prop]

concKeccakOnePass :: Expr a -> Expr a

Orphan instances

Monoid (Expr 'Buf)

Methods

mempty :: Expr 'Buf

mappend :: Expr 'Buf -> Expr 'Buf -> Expr 'Buf

mconcat :: [Expr 'Buf] -> Expr 'Buf

Semigroup (Expr 'Buf)

Methods

(<>) :: Expr 'Buf -> Expr 'Buf -> Expr 'Buf

sconcat :: NonEmpty (Expr 'Buf) -> Expr 'Buf

stimes :: Integral b => b -> Expr 'Buf -> Expr 'Buf