Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
- Constants **
- Stack Ops ** ---------------------------------------------------------------------------------
- Bufs ** --------------------------------------------------------------------------------------
- Storage ** -----------------------------------------------------------------------------------
- Whole Expression Simplification ** -----------------------------------------------------------
- Prop Simplification ** -----------------------------------------------------------------------
- Conversions ** -------------------------------------------------------------------------------
- Helpers ** -----------------------------------------------------------------------------------
- Orphan instances
Helper functions for working with Expr instances. All functions here will return a concrete result if given a concrete input.
Synopsis
- maxLit :: W256
- 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
- bufLengthEnv :: Map Int (Expr Buf) -> Bool -> Expr Buf -> Expr EWord
- minLength :: Map Int (Expr Buf) -> Expr Buf -> Maybe Integer
- concretePrefix :: Expr Buf -> Vector Word8
- word256At :: Expr EWord -> Lens (Expr Buf) (Expr Buf) (Expr EWord) (Expr EWord)
- 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 Storage -> Expr EWord
- readStorage :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)
- 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
- litToArrayPreimage :: W256 -> Maybe (Word8, W256)
- writeStorage :: Expr EWord -> Expr EWord -> Expr Storage -> Expr Storage
- getAddr :: Expr Storage -> Maybe (Expr EAddr)
- getLogicalIdx :: Expr Storage -> Maybe W256
- data StorageType
- safeToDecompose :: Expr a -> Bool
- decomposeStorage :: Expr a -> Maybe (Expr a)
- simplify :: Expr a -> Expr a
- simplifyProps :: [Prop] -> [Prop]
- simplifyProp :: Prop -> Prop
- flattenProps :: [Prop] -> [Prop]
- remRedundantProps :: [Prop] -> [Prop]
- litAddr :: Addr -> Expr EWord
- exprToAddr :: Expr EWord -> Maybe Addr
- wordToAddr :: Expr EWord -> Maybe (Expr EAddr)
- litCode :: ByteString -> [Expr Byte]
- to512 :: W256 -> Word512
- 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
- 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
- max :: Expr EWord -> Expr EWord -> Expr EWord
- numBranches :: Expr End -> Int
- allLit :: [Expr Byte] -> Bool
- containsNode :: (forall a. Expr a -> Bool) -> Expr b -> Bool
- inRange :: Int -> Expr EWord -> Prop
- preImages :: [(W256, Word8)]
- data ConstState = ConstState {}
- constFoldProp :: [Prop] -> Bool
- concKeccakSimpExpr :: Expr a -> Expr a
- concKeccakProps :: [Prop] -> [Prop]
- concKeccakOnePass :: Expr a -> Expr a
Constants **
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 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 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 expression will be returned.
minLength :: Map Int (Expr Buf) -> Expr Buf -> Maybe Integer Source #
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.
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 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.
pattern MappingSlot :: ByteString -> Expr EWord -> Expr EWord Source #
pattern Keccak64Bytes :: Expr EWord Source #
pattern ArraySlotWithOffset :: ByteString -> Expr EWord -> Expr EWord Source #
pattern ArraySlotZero :: ByteString -> Expr EWord Source #
idsDontMatch :: ByteString -> ByteString -> Bool Source #
slotPos :: Word8 -> ByteString Source #
structureArraySlots :: Expr a -> Expr a Source #
Turns Literals into keccak(bytes32(id)) + offset (i.e. writes to arrays)
writeStorage :: 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 ** -----------------------------------------------------------
data StorageType Source #
Instances
Show StorageType Source # | |
Defined in EVM.Expr showsPrec :: Int -> StorageType -> ShowS # show :: StorageType -> String # showList :: [StorageType] -> ShowS # | |
Eq StorageType Source # | |
Defined in EVM.Expr (==) :: StorageType -> StorageType -> Bool # (/=) :: StorageType -> StorageType -> Bool # |
safeToDecompose :: Expr a -> Bool Source #
decomposeStorage :: Expr a -> Maybe (Expr a) Source #
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 Source #
Simple recursive match based AST simplification Note: may not terminate!
Prop Simplification ** -----------------------------------------------------------------------
simplifyProps :: [Prop] -> [Prop] Source #
simplifyProp :: Prop -> Prop Source #
Evaluate the provided proposition down to its most concrete result Also simplifies the inner Expr, if it exists
flattenProps :: [Prop] -> [Prop] Source #
remRedundantProps :: [Prop] -> [Prop] Source #
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?
containsNode :: (forall a. Expr a -> Bool) -> Expr b -> Bool Source #
True if the given expression contains any node that satisfies the input predicate
data ConstState Source #
Instances
Show ConstState Source # | |
Defined in EVM.Expr showsPrec :: Int -> ConstState -> ShowS # show :: ConstState -> String # showList :: [ConstState] -> ShowS # |
constFoldProp :: [Prop] -> Bool Source #
Folds constants
concKeccakSimpExpr :: Expr a -> Expr a Source #
concKeccakProps :: [Prop] -> [Prop] Source #
concKeccakOnePass :: Expr a -> Expr a Source #