EVM.Expr

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

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 expresion if nescessary. 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 expresion will be returned.

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

concPrefix :: Expr Buf -> Maybe Integer

If a buffer has a concrete prefix, we return it's length here

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.

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 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.

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

writeStorage :: Expr EWord -> 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.

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

simplify :: Expr a -> Expr a

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

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

litAddr :: Addr -> Expr EWord

exprToAddr :: Expr EWord -> Maybe Addr

litCode :: ByteString -> [Expr Byte]

to512 :: W256 -> Word512

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

isLitByte :: Expr Byte -> Bool

isLitWord :: Expr EWord -> 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

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