hevm-0.41.0: Ethereum virtual machine evaluator

Safe HaskellNone
LanguageHaskell2010

EVM.Symbolic

Synopsis

Documentation

data SymWord Source #

Symbolic words of 256 bits, possibly annotated with additional "insightful" information

Constructors

S Whiff (SWord 256) 
Instances
Bounded SymWord Source # 
Instance details

Defined in EVM.Symbolic

Enum SymWord Source # 
Instance details

Defined in EVM.Symbolic

Eq SymWord Source # 
Instance details

Defined in EVM.Symbolic

Methods

(==) :: SymWord -> SymWord -> Bool #

(/=) :: SymWord -> SymWord -> Bool #

Num SymWord Source # 
Instance details

Defined in EVM.Symbolic

Show SymWord Source #

Custom instances for SymWord, many of which have direct analogues for concrete words defined in Concrete.hs

Instance details

Defined in EVM.Symbolic

Bits SymWord Source # 
Instance details

Defined in EVM.Symbolic

EqSymbolic SymWord Source # 
Instance details

Defined in EVM.Symbolic

OrdSymbolic SymWord Source # 
Instance details

Defined in EVM.Symbolic

SDivisible SymWord Source # 
Instance details

Defined in EVM.Symbolic

Mergeable SymWord Source # 
Instance details

Defined in EVM.Symbolic

Methods

symbolicMerge :: Bool -> SBool -> SymWord -> SymWord -> SymWord #

select :: (Ord b, SymVal b, Num b) => [SymWord] -> SymWord -> SBV b -> SymWord #

SDisplay SymWord Source # 
Instance details

Defined in EVM.Emacs

Methods

sexp :: SymWord -> SExpr Text Source #

sw256 :: SWord 256 -> SymWord Source #

Convenience functions transporting between the concrete and symbolic realm

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

sdiv :: SymWord -> SymWord -> SymWord Source #

Arithmetic operations on SymWord

swordAt :: Int -> [SWord 8] -> SymWord Source #

Operations over symbolic memory (list of symbolic bytes)

sliceWithZero' :: Int -> Int -> [SWord 8] -> [SWord 8] Source #

writeMemory' :: [SWord 8] -> Word -> Word -> Word -> [SWord 8] -> [SWord 8] Source #

setMemoryByte' :: Word -> SWord 8 -> [SWord 8] -> [SWord 8] Source #

select' :: (Ord b, Num b, SymVal b, Mergeable a) => [a] -> a -> SBV b -> a Source #

data Buffer Source #

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.

Instances
Show Buffer Source # 
Instance details

Defined in EVM.Symbolic

Semigroup Buffer Source # 
Instance details

Defined in EVM.Symbolic

Monoid Buffer Source # 
Instance details

Defined in EVM.Symbolic

EqSymbolic Buffer Source # 
Instance details

Defined in EVM.Symbolic

SDisplay Buffer Source # 
Instance details

Defined in EVM.Emacs

Methods

sexp :: Buffer -> SExpr Text Source #