EVM.SMT

Encoding ** ----------------------------------------------------------------------------------

data CexVars

Constructors

CexVars

Fields

• calldataV :: [Text]
• buffersV :: [Text]
• storeReads :: [(Expr EWord, Expr EWord)]
• blockContextV :: [Text]
• txContextV :: [Text]

Instances

Monoid CexVars

Defined in EVM.SMT

Methods

mempty :: CexVars

mappend :: CexVars -> CexVars -> CexVars

mconcat :: [CexVars] -> CexVars

Semigroup CexVars

Defined in EVM.SMT

Methods

(<>) :: CexVars -> CexVars -> CexVars

sconcat :: NonEmpty CexVars -> CexVars

stimes :: Integral b => b -> CexVars -> CexVars

Show CexVars

Defined in EVM.SMT

Methods

showsPrec :: Int -> CexVars -> ShowS

show :: CexVars -> String

showList :: [CexVars] -> ShowS

Eq CexVars

Defined in EVM.SMT

Methods

(==) :: CexVars -> CexVars -> Bool

(/=) :: CexVars -> CexVars -> Bool

data SMTCex

Constructors

SMTCex

Fields

• vars :: Map (Expr EWord) W256
• buffers :: Map (Expr Buf) ByteString
• store :: Map W256 (Map W256 W256)
• blockContext :: Map (Expr EWord) W256
• txContext :: Map (Expr EWord) W256

Instances

Show SMTCex

Defined in EVM.SMT

Methods

showsPrec :: Int -> SMTCex -> ShowS

show :: SMTCex -> String

showList :: [SMTCex] -> ShowS

Eq SMTCex

Defined in EVM.SMT

Methods

(==) :: SMTCex -> SMTCex -> Bool

(/=) :: SMTCex -> SMTCex -> Bool

getVar :: SMTCex -> Text -> W256

data SMT2

Constructors

SMT2 [Builder] CexVars

Instances

Monoid SMT2

Defined in EVM.SMT

Methods

mempty :: SMT2

mappend :: SMT2 -> SMT2 -> SMT2

mconcat :: [SMT2] -> SMT2

Semigroup SMT2

Defined in EVM.SMT

Methods

(<>) :: SMT2 -> SMT2 -> SMT2

sconcat :: NonEmpty SMT2 -> SMT2

stimes :: Integral b => b -> SMT2 -> SMT2

Show SMT2

Defined in EVM.SMT

Methods

showsPrec :: Int -> SMT2 -> ShowS

show :: SMT2 -> String

showList :: [SMT2] -> ShowS

Eq SMT2

Defined in EVM.SMT

Methods

(==) :: SMT2 -> SMT2 -> Bool

(/=) :: SMT2 -> SMT2 -> Bool

formatSMT2 :: SMT2 -> Text

declareIntermediates :: BufEnv -> StoreEnv -> SMT2

Reads all intermediate variables from the builder state and produces SMT declaring them as constants

assertProps :: [Prop] -> SMT2

referencedBufsGo :: Expr a -> [Builder]

referencedBufs :: Expr a -> [Builder]

referencedBufs' :: Prop -> [Builder]

referencedVarsGo :: Expr a -> [Builder]

referencedVars :: Expr a -> [Builder]

referencedVars' :: Prop -> [Builder]

referencedFrameContextGo :: Expr a -> [Builder]

referencedFrameContext :: Expr a -> [Builder]

referencedFrameContext' :: Prop -> [Builder]

referencedBlockContextGo :: Expr a -> [Builder]

referencedBlockContext :: Expr a -> [Builder]

referencedBlockContext' :: Prop -> [Builder]

isAbstractStorage :: Expr Storage -> Bool

findStorageReads :: Prop -> [(Expr EWord, Expr EWord)]

This function overapproximates the reads from the abstract storage. Potentially, it can return locations that do not read a slot directly from the abstract store but from subsequent writes on the store (e.g, SLoad addr idx (SStore addr idx val AbstractStore)). However, we expect that most of such reads will have been simplified away.

declareBufs :: [Builder] -> SMT2

declareVars :: [Builder] -> SMT2

declareFrameContext :: [Builder] -> SMT2

declareBlockContext :: [Builder] -> SMT2

prelude :: SMT2

exprToSMT :: Expr a -> Builder

sp :: Builder -> Builder -> Builder

zero :: Builder

one :: Builder

propToSMT :: Prop -> Builder

Helpers ** ---------------------------------------------------------------------------------

copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Builder

Stores a region of src into dst

expandExp :: Expr EWord -> W256 -> Builder

Unrolls an exponentiation into a series of multiplications

concatBytes :: [Expr Byte] -> Builder

Concatenates a list of bytes into a larger bitvector

writeBytes :: ByteString -> Expr Buf -> Builder

Concatenates a list of bytes into a larger bitvector

encodeConcreteStore :: Map W256 (Map W256 W256) -> Builder

Cex parsing ** --------------------------------------------------------------------------------

parseW256 :: SpecConstant -> W256

parseInteger :: SpecConstant -> Integer

parseW8 :: SpecConstant -> Word8

parseSC :: (Num a, Eq a) => SpecConstant -> a

parseErr :: Show a => a -> b

parseVar :: Text -> Expr EWord

parseBlockCtx :: Text -> Expr EWord

parseFrameCtx :: Text -> Expr EWord

getVars :: (Text -> Expr EWord) -> (Text -> IO Text) -> [Text] -> IO (Map (Expr EWord) W256)

getBufs :: (Text -> IO Text) -> [Text] -> IO (Map (Expr Buf) ByteString)

getStore :: (Text -> IO Text) -> [(Expr EWord, Expr EWord)] -> IO (Map W256 (Map W256 W256))

interpretNDArray :: (Map Symbol Term -> Term -> a) -> Map Symbol Term -> Term -> W256 -> a

Interpret an N-dimensional array as a value of type a. Parameterized by an interpretation function for array values.

interpret1DArray :: Map Symbol Term -> Term -> W256 -> W256

Interpret an 1-dimensional array as a function

interpret2DArray :: Map Symbol Term -> Term -> W256 -> W256 -> W256

Interpret an 2-dimensional array as a function