| 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
- maybeLitWord :: SymWord -> Maybe Word
- maybeLitAddr :: SAddr -> Maybe Addr
- maybeLitBytes :: [SWord 8] -> Maybe ByteString
- forceLit :: SymWord -> Word
- forceLitBytes :: [SWord 8] -> ByteString
- forceBuffer :: Buffer -> 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
- shiftRight' :: 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
- 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
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 #
forceBuffer :: Buffer -> ByteString Source #