| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
EVM.Expr
Contents
- Stack Ops ** ---------------------------------------------------------------------------------
- Bufs ** --------------------------------------------------------------------------------------
- Storage ** -----------------------------------------------------------------------------------
- Whole Expression Simplification ** -----------------------------------------------------------
- Conversions ** -------------------------------------------------------------------------------
- Helpers ** -----------------------------------------------------------------------------------
- Orphan instances
Description
Helper functions for working with Expr instances. All functions here will return a concrete result if given a concrete input.
Synopsis
- 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
- 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
- readByte :: Expr EWord -> Expr Buf -> Expr Byte
- readBytes :: Int -> Expr EWord -> Expr Buf -> Expr EWord
- readWord :: Expr EWord -> Expr Buf -> Expr EWord
- readWordFromBytes :: Expr EWord -> Expr Buf -> Expr EWord
- maxBytes :: W256
- 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
- concPrefix :: Expr Buf -> Maybe Integer
- word256At :: Functor f => Expr EWord -> (Expr EWord -> f (Expr EWord)) -> Expr Buf -> f (Expr Buf)
- take :: W256 -> Expr Buf -> Expr Buf
- drop :: W256 -> Expr Buf -> Expr 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
- stripWrites :: W256 -> W256 -> Expr Buf -> Expr Buf
- readStorage :: Expr EWord -> Expr EWord -> Expr Storage -> Maybe (Expr EWord)
- readStorage' :: Expr EWord -> Expr EWord -> Expr Storage -> Expr EWord
- writeStorage :: Expr EWord -> Expr EWord -> Expr EWord -> Expr Storage -> Expr Storage
- simplify :: Expr a -> Expr a
- litAddr :: Addr -> Expr EWord
- litCode :: ByteString -> [Expr Byte]
- to512 :: W256 -> Word512
- isLitByte :: Expr Byte -> Bool
- isLitWord :: Expr EWord -> Bool
- indexWord :: Expr EWord -> Expr EWord -> Expr Byte
- padByte :: Expr Byte -> Expr EWord
- bytesToW256 :: [Word8] -> W256
- 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
- numBranches :: Expr End -> Int
- allLit :: [Expr Byte] -> Bool
Stack Ops ** ---------------------------------------------------------------------------------
op2 :: (Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord Source #
op3 :: (Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord) -> (W256 -> W256 -> W256 -> W256) -> Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord Source #
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
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 #
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?