hevm-0.50.1: Ethereum virtual machine evaluator
Safe HaskellSafe-Inferred
LanguageGHC2021

EVM.Expr

Description

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

Synopsis

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

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

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.

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

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

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 Source #

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 Source #

Reads the word starting at idx from the given buf

maxBytes :: W256 Source #

Copies a slice of src into dst.

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

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

bufLength :: Expr Buf -> Expr EWord Source #

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.

concPrefix :: Expr Buf -> Maybe Integer Source #

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

word256At :: Functor f => Expr EWord -> (Expr EWord -> f (Expr EWord)) -> Expr Buf -> f (Expr Buf) Source #

take :: W256 -> Expr Buf -> Expr Buf Source #

Returns the first n bytes of buf

drop :: W256 -> Expr Buf -> Expr Buf Source #

Returns everything but the first n bytes of buf

simplifyReads :: Expr a -> Expr a Source #

Removes any irrelevant writes when reading from a buffer

stripWrites :: W256 -> W256 -> Expr Buf -> Expr Buf Source #

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) Source #

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.

writeStorage :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Storage -> Expr Storage Source #

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 Source #

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

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

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

indexWord :: Expr EWord -> Expr EWord -> Expr Byte Source #

Returns the byte at idx from the given word.

bytesToW256 :: [Word8] -> W256 Source #

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

Orphan instances

Monoid (Expr 'Buf) Source # 
Instance details

Methods

mempty :: Expr 'Buf #

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

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

Semigroup (Expr 'Buf) Source # 
Instance details

Methods

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

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

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