Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Synopsis
- data CexVars = CexVars {}
- data BufModel
- data CompressedBuf
- data SMTCex = SMTCex {}
- data RefinementEqs = RefinementEqs [Builder] [Prop]
- flattenBufs :: SMTCex -> Maybe SMTCex
- collapse :: BufModel -> Maybe BufModel
- getVar :: SMTCex -> Text -> W256
- data SMT2 = SMT2 [Builder] RefinementEqs CexVars [Prop]
- formatSMT2 :: SMT2 -> Text
- declareIntermediates :: BufEnv -> StoreEnv -> SMT2
- data AbstState = AbstState {}
- abstractAwayProps :: Config -> [Prop] -> ([Prop], AbstState)
- smt2Line :: Builder -> SMT2
- assertProps :: Config -> [Prop] -> SMT2
- assertPropsNoSimp :: Config -> [Prop] -> SMT2
- referencedAbstractStores :: TraversableTerm a => a -> Set Builder
- referencedWAddrs :: TraversableTerm a => a -> Set Builder
- referencedBufs :: TraversableTerm a => a -> [Builder]
- referencedVars :: TraversableTerm a => a -> [Builder]
- referencedFrameContext :: TraversableTerm a => a -> [(Builder, [Prop])]
- referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])]
- findStorageReads :: Prop -> Map (Expr EAddr, Maybe W256) (Set (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
- declareAddrs :: [Builder] -> SMT2
- declareFrameContext :: [(Builder, [Prop])] -> SMT2
- declareAbstractStores :: [Builder] -> 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 W256 -> Builder
- storeName :: Expr EAddr -> Maybe W256 -> Builder
- formatEAddr :: Expr EAddr -> Builder
- parseAddr :: SpecConstant -> Addr
- 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
- parseEAddr :: Text -> Expr EAddr
- parseBlockCtx :: Text -> Expr EWord
- parseTxCtx :: Text -> Expr EWord
- getAddrs :: (Text -> Expr EAddr) -> (Text -> IO Text) -> [Text] -> IO (Map (Expr EAddr) Addr)
- getVars :: (Text -> Expr EWord) -> (Text -> IO Text) -> [Text] -> IO (Map (Expr EWord) W256)
- getOne :: (SpecConstant -> a) -> (Text -> IO Text) -> Map Text a -> Text -> IO (Map Text a)
- 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) -> Map (Expr EAddr, Maybe W256) (Set (Expr EWord)) -> IO (Map (Expr EAddr) (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
Encoding ** ----------------------------------------------------------------------------------
Data that we need to construct a nice counterexample
CexVars | |
|
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)
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 # | |
Defined in EVM.SMT showsPrec :: Int -> CompressedBuf -> ShowS # show :: CompressedBuf -> String # showList :: [CompressedBuf] -> ShowS # | |
Eq CompressedBuf Source # | |
Defined in EVM.SMT (==) :: CompressedBuf -> CompressedBuf -> Bool # (/=) :: CompressedBuf -> CompressedBuf -> Bool # |
a final post shrinking cex, buffers here are all represented as concrete bytestrings
data RefinementEqs Source #
Used for abstraction-refinement of the SMT formula. Contains assertions that make our query fully precise. These will be added to the assertion stack if we get sat
with the abstracted query.
RefinementEqs [Builder] [Prop] |
Instances
Monoid RefinementEqs Source # | |
Defined in EVM.SMT mempty :: RefinementEqs # mappend :: RefinementEqs -> RefinementEqs -> RefinementEqs # mconcat :: [RefinementEqs] -> RefinementEqs # | |
Semigroup RefinementEqs Source # | |
Defined in EVM.SMT (<>) :: RefinementEqs -> RefinementEqs -> RefinementEqs # sconcat :: NonEmpty RefinementEqs -> RefinementEqs # stimes :: Integral b => b -> RefinementEqs -> RefinementEqs # | |
Show RefinementEqs Source # | |
Defined in EVM.SMT showsPrec :: Int -> RefinementEqs -> ShowS # show :: RefinementEqs -> String # showList :: [RefinementEqs] -> ShowS # | |
Eq RefinementEqs Source # | |
Defined in EVM.SMT (==) :: RefinementEqs -> RefinementEqs -> Bool # (/=) :: RefinementEqs -> RefinementEqs -> Bool # |
collapse :: BufModel -> Maybe BufModel Source #
Attempts 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
referencedAbstractStores :: TraversableTerm a => a -> Set Builder Source #
referencedWAddrs :: TraversableTerm a => a -> Set Builder Source #
referencedBufs :: TraversableTerm a => a -> [Builder] Source #
referencedVars :: TraversableTerm a => a -> [Builder] Source #
referencedFrameContext :: TraversableTerm a => a -> [(Builder, [Prop])] Source #
referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])] Source #
findStorageReads :: Prop -> Map (Expr EAddr, Maybe W256) (Set (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 #
declareAddrs :: [Builder] -> SMT2 Source #
declareAbstractStores :: [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 ** --------------------------------------------------------------------------------
parseAddr :: SpecConstant -> Addr Source #
parseW256 :: SpecConstant -> W256 Source #
parseInteger :: SpecConstant -> Integer Source #
parseW8 :: SpecConstant -> Word8 Source #
getAddrs :: (Text -> Expr EAddr) -> (Text -> IO Text) -> [Text] -> IO (Map (Expr EAddr) Addr) Source #
getVars :: (Text -> Expr EWord) -> (Text -> IO Text) -> [Text] -> IO (Map (Expr EWord) W256) Source #
getOne :: (SpecConstant -> a) -> (Text -> IO Text) -> Map Text a -> Text -> IO (Map Text a) 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) -> Map (Expr EAddr, Maybe W256) (Set (Expr EWord)) -> IO (Map (Expr EAddr) (Map W256 W256)) Source #
Takes a Map containing all reads from a store with an abstract base, as well as the concrete part of the storage prestate and returns a fully concretized storage
queryValue :: (Text -> IO Text) -> Expr EWord -> IO W256 Source #
Ask the solver to give us the concrete value of an arbitrary abstract word