Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Synopsis
- data CexVars = CexVars {}
- data BufModel
- data CompressedBuf
- data SMTCex = SMTCex {}
- flattenBufs :: SMTCex -> Maybe SMTCex
- collapse :: BufModel -> Maybe BufModel
- getVar :: SMTCex -> Text -> W256
- data SMT2 = SMT2 [Builder] CexVars
- formatSMT2 :: SMT2 -> Text
- declareIntermediates :: BufEnv -> StoreEnv -> SMT2
- 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, [Prop])]
- referencedFrameContext :: Expr a -> [(Builder, [Prop])]
- referencedFrameContext' :: Prop -> [(Builder, [Prop])]
- referencedBlockContextGo :: Expr a -> [(Builder, [Prop])]
- referencedBlockContext :: Expr a -> [(Builder, [Prop])]
- referencedBlockContext' :: Prop -> [(Builder, [Prop])]
- findStorageReads :: Prop -> [(Expr EWord, Expr EWord)]
- findBufferAccess :: TraversableTerm a => [a] -> [(Expr EWord, Expr EWord, Expr Buf)]
- assertReads :: [Prop] -> BufEnv -> StoreEnv -> [Prop]
- discoverMaxReads :: [Prop] -> BufEnv -> StoreEnv -> Map Text (Expr EWord)
- declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2
- declareVars :: [Builder] -> SMT2
- declareFrameContext :: [(Builder, [Prop])] -> SMT2
- declareBlockContext :: [(Builder, [Prop])] -> SMT2
- prelude :: SMT2
- exprToSMT :: Expr a -> Builder
- sp :: Builder -> Builder -> Builder
- zero :: Builder
- one :: Builder
- propToSMT :: Prop -> Builder
- copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Builder
- expandExp :: Expr EWord -> W256 -> Builder
- concatBytes :: [Expr Byte] -> Builder
- writeBytes :: ByteString -> Expr Buf -> Builder
- encodeConcreteStore :: Map W256 (Map W256 W256) -> Builder
- 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)
- queryMaxReads :: (Text -> IO Text) -> Map Text (Expr EWord) -> IO (Map Text W256)
- getBufs :: (Text -> IO Text) -> [Text] -> IO (Map (Expr Buf) BufModel)
- getStore :: (Text -> IO Text) -> [(Expr EWord, Expr EWord)] -> IO (Map W256 (Map W256 W256))
- queryValue :: (Text -> IO Text) -> Expr EWord -> IO W256
- interpretNDArray :: (Map Symbol Term -> Term -> a) -> Map Symbol Term -> Term -> W256 -> a
- interpret1DArray :: Map Symbol Term -> Term -> W256 -> W256
- interpret2DArray :: Map Symbol Term -> Term -> W256 -> W256 -> W256
Encoding ** ----------------------------------------------------------------------------------
A model for a buffer, either in it's compressed form (for storing parsed models from a solver), or as a bytestring (for presentation to users)
Instances
data CompressedBuf Source #
This representation lets us store buffers of arbitrary length without exhausting the available memory, it closely matches the format used by smt-lib when returning models for arrays
Instances
Show CompressedBuf Source # | |
Eq CompressedBuf Source # | |
Defined in EVM.SMT (==) :: CompressedBuf -> CompressedBuf -> Bool Source # (/=) :: CompressedBuf -> CompressedBuf -> Bool Source # |
a final post shrinking cex, buffers here are all represented as concrete bytestrings
collapse :: BufModel -> Maybe BufModel Source #
Attemps to collapse a compressed buffer representation down to a flattened one
formatSMT2 :: SMT2 -> Text Source #
declareIntermediates :: BufEnv -> StoreEnv -> SMT2 Source #
Reads all intermediate variables from the builder state and produces SMT declaring them as constants
assertProps :: [Prop] -> SMT2 Source #
referencedBufsGo :: Expr a -> [Builder] Source #
referencedBufs :: Expr a -> [Builder] Source #
referencedBufs' :: Prop -> [Builder] Source #
referencedVarsGo :: Expr a -> [Builder] Source #
referencedVars :: Expr a -> [Builder] Source #
referencedVars' :: Prop -> [Builder] Source #
findStorageReads :: Prop -> [(Expr EWord, Expr EWord)] Source #
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.
findBufferAccess :: TraversableTerm a => [a] -> [(Expr EWord, Expr EWord, Expr Buf)] Source #
assertReads :: [Prop] -> BufEnv -> StoreEnv -> [Prop] Source #
Asserts that buffer reads beyond the size of the buffer are equal to zero. Looks for buffer reads in the a list of given predicates and the buffer and storage environments.
discoverMaxReads :: [Prop] -> BufEnv -> StoreEnv -> Map Text (Expr EWord) Source #
Finds the maximum read index for each abstract buffer in the input props
declareBufs :: [Prop] -> BufEnv -> StoreEnv -> SMT2 Source #
Returns an SMT2 object with all buffers referenced from the input props declared, and with the appropriate cex extraction metadata attached
declareVars :: [Builder] -> SMT2 Source #
Helpers ** ---------------------------------------------------------------------------------
copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Builder Source #
Stores a region of src into dst
expandExp :: Expr EWord -> W256 -> Builder Source #
Unrolls an exponentiation into a series of multiplications
writeBytes :: ByteString -> Expr Buf -> Builder Source #
Concatenates a list of bytes into a larger bitvector
Cex parsing ** --------------------------------------------------------------------------------
parseW256 :: SpecConstant -> W256 Source #
parseInteger :: SpecConstant -> Integer Source #
parseW8 :: SpecConstant -> Word8 Source #
getVars :: (Text -> Expr EWord) -> (Text -> IO Text) -> [Text] -> IO (Map (Expr EWord) W256) Source #
queryMaxReads :: (Text -> IO Text) -> Map Text (Expr EWord) -> IO (Map Text W256) Source #
Queries the solver for models for each of the expressions representing the max read index for a given buffer
getBufs :: (Text -> IO Text) -> [Text] -> IO (Map (Expr Buf) BufModel) Source #
Gets the initial model for each buffer, these will often be much too large for our purposes
getStore :: (Text -> IO Text) -> [(Expr EWord, Expr EWord)] -> IO (Map W256 (Map W256 W256)) Source #
interpretNDArray :: (Map Symbol Term -> Term -> a) -> Map Symbol Term -> Term -> W256 -> a Source #
Interpret an N-dimensional array as a value of type a. Parameterized by an interpretation function for array values.