| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
EVM.Symbolic
Synopsis
- data SymWord = S Whiff (SWord 256)
- sw256 :: SWord 256 -> SymWord
- litWord :: Word -> SymWord
- w256lit :: W256 -> SymWord
- litAddr :: Addr -> SAddr
- litBytes :: ByteString -> [SWord 8]
- maybeLitWord :: SymWord -> Maybe Word
- maybeLitAddr :: SAddr -> Maybe Addr
- maybeLitBytes :: [SWord 8] -> Maybe ByteString
- forceLit :: SymWord -> Word
- forceLitBytes :: [SWord 8] -> ByteString
- sdiv :: SymWord -> SymWord -> SymWord
- smod :: SymWord -> SymWord -> SymWord
- addmod :: SymWord -> SymWord -> SymWord -> SymWord
- mulmod :: SymWord -> SymWord -> SymWord -> SymWord
- slt :: SymWord -> SymWord -> SymWord
- sgt :: SymWord -> SymWord -> SymWord
- swordAt :: Int -> [SWord 8] -> SymWord
- readByteOrZero' :: Int -> [SWord 8] -> SWord 8
- sliceWithZero' :: Int -> Int -> [SWord 8] -> [SWord 8]
- writeMemory' :: [SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8]
- readMemoryWord' :: Word -> [SWord 8] -> SymWord
- readMemoryWord32' :: Word -> [SWord 8] -> SWord 32
- setMemoryWord' :: Word -> SymWord -> [SWord 8] -> [SWord 8]
- setMemoryByte' :: Word -> SWord 8 -> [SWord 8] -> [SWord 8]
- readSWord' :: Word -> [SWord 8] -> SymWord
- select' :: (Ord b, Num b, SymVal b, Mergeable a) => [a] -> a -> SBV b -> a
- readSWordWithBound :: SWord 32 -> Buffer -> SWord 32 -> SymWord
- data Buffer
- len :: Buffer -> Int
- grab :: Int -> Buffer -> Buffer
- ditch :: Int -> Buffer -> Buffer
- readByteOrZero :: Int -> Buffer -> SWord 8
- sliceWithZero :: Int -> Int -> Buffer -> Buffer
- writeMemory :: Buffer -> Word -> Word -> Word -> Buffer -> Buffer
- readMemoryWord :: Word -> Buffer -> SymWord
- readMemoryWord32 :: Word -> Buffer -> SWord 32
- setMemoryWord :: Word -> SymWord -> Buffer -> Buffer
- setMemoryByte :: Word -> SWord 8 -> Buffer -> Buffer
- readSWord :: Word -> Buffer -> SymWord
Documentation
Symbolic words of 256 bits, possibly annotated with additional "insightful" information
Instances
sw256 :: SWord 256 -> SymWord Source #
Convenience functions transporting between the concrete and symbolic realm
litBytes :: ByteString -> [SWord 8] Source #
maybeLitBytes :: [SWord 8] -> Maybe ByteString Source #
forceLit :: SymWord -> Word Source #
Note: these forms are crude and in general,
the continuation passing style forceConcrete
alternatives should be prefered for better error
handling when used during EVM execution
forceLitBytes :: [SWord 8] -> ByteString Source #
swordAt :: Int -> [SWord 8] -> SymWord Source #
Operations over symbolic memory (list of symbolic bytes)
Operations over buffers (concrete or symbolic)
A buffer is a list of bytes. For concrete execution, this is simply ByteString.
In symbolic settings, it is a list of symbolic bitvectors of size 8.
Constructors
| ConcreteBuffer ByteString | |
| SymbolicBuffer [SWord 8] |
Instances
| Show Buffer Source # | |
| Semigroup Buffer Source # | |
| Monoid Buffer Source # | |
| EqSymbolic Buffer Source # | |
Defined in EVM.Symbolic Methods (.==) :: Buffer -> Buffer -> SBool # (./=) :: Buffer -> Buffer -> SBool # (.===) :: Buffer -> Buffer -> SBool # (./==) :: Buffer -> Buffer -> SBool # distinct :: [Buffer] -> SBool # distinctExcept :: [Buffer] -> [Buffer] -> SBool # allEqual :: [Buffer] -> SBool # | |
| SDisplay Buffer Source # | |