EVM.Symbolic

Documentation

litWord :: Word -> SymWord

litAddr :: Addr -> SAddr

maybeLitAddr :: SAddr -> Maybe Addr

maybeLitBytes :: [SWord 8] -> Maybe ByteString

forceLit :: SymWord -> Word

Note: the (force*) functions 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

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

Signed less than

sgt :: SymWord -> SymWord -> SymWord

Signed greater than

Operations over symbolic memory (list of symbolic bytes)

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 :: SymWord -> Buffer -> SymWord -> SymWord

Read 32 bytes from index from a bounded list of bytes.

len :: Buffer -> Int

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

index :: Int -> Buffer -> SWord8

Uninterpreted functions

symSHA256N :: SInteger -> SInteger -> SWord 256

symkeccakN :: SInteger -> SInteger -> SWord 256

toSInt :: [SWord 8] -> SInteger

symkeccak' :: [SWord 8] -> SWord 256

Although we'd like to define this directly as an uninterpreted function, we cannot because [a] is not a symbolic type. We must convert the list into a suitable symbolic type first. The only important property of this conversion is that it is injective. We embedd the bytestring as a pair of symbolic integers, this is a fairly easy solution.

symSHA256 :: [SWord 8] -> [SWord 8]

rawVal :: SymWord -> SWord 256

whiffValue :: Whiff -> SWord 256

Reconstruct the smt/sbv value from a whiff Should satisfy (rawVal x .== whiffValue x)

simplifyCondition :: SBool -> Whiff -> SBool

Special cases that have proven useful in practice