Safe Haskell	None
Language	Haskell2010

Lang.Crucible.FunctionHandle

Contents

Function handle
Allocate handle.
FnHandleMap
Reference cells

Synopsis

data FnHandle (args :: Ctx CrucibleType) (ret :: CrucibleType)
handleID :: FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret)
handleName :: FnHandle args ret -> FunctionName
handleArgTypes :: FnHandle args ret -> CtxRepr args
handleReturnType :: FnHandle args ret -> TypeRepr ret
handleType :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType). FnHandle args ret -> TypeRepr (FunctionHandleType args ret)
data SomeHandle where
- SomeHandle :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType). !(FnHandle args ret) -> SomeHandle
data HandleAllocator
haCounter :: HandleAllocator -> NonceGenerator IO GlobalNonceGenerator
newHandleAllocator :: IO HandleAllocator
withHandleAllocator :: (HandleAllocator -> IO a) -> IO a
mkHandle :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType). (KnownCtx TypeRepr args, KnownRepr TypeRepr ret) => HandleAllocator -> FunctionName -> IO (FnHandle args ret)
mkHandle' :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType). HandleAllocator -> FunctionName -> Assignment TypeRepr args -> TypeRepr ret -> IO (FnHandle args ret)
data FnHandleMap (f :: Ctx CrucibleType -> CrucibleType -> Type)
emptyHandleMap :: forall (f :: Ctx CrucibleType -> CrucibleType -> Type). FnHandleMap f
insertHandleMap :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) f. FnHandle args ret -> f args ret -> FnHandleMap f -> FnHandleMap f
lookupHandleMap :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) f. FnHandle args ret -> FnHandleMap f -> Maybe (f args ret)
updateHandleMap :: forall f (args :: Ctx CrucibleType) (ret :: CrucibleType). (f args ret -> f args ret) -> FnHandle args ret -> FnHandleMap f -> FnHandleMap f
searchHandleMap :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) f. FunctionName -> TypeRepr (FunctionHandleType args ret) -> FnHandleMap f -> Maybe (FnHandle args ret, f args ret)
handleMapToHandles :: forall (f :: Ctx CrucibleType -> CrucibleType -> Type). FnHandleMap f -> [SomeHandle]
data RefCell (tp :: CrucibleType)
freshRefCell :: forall (tp :: CrucibleType). HandleAllocator -> TypeRepr tp -> IO (RefCell tp)
refType :: forall (tp :: CrucibleType). RefCell tp -> TypeRepr tp

Function handle

data FnHandle (args :: Ctx CrucibleType) (ret :: CrucibleType) Source #

A handle uniquely identifies a function. The signature indicates the expected argument types and the return type of the function.

Instances

Instances details

LitExpr e (FunctionHandleType args ret) (FnHandle args ret) Source #
Instance details Defined in Lang.Crucible.Syntax Methods litExpr :: FnHandle args ret -> e (FunctionHandleType args ret) Source #
Show (FnHandle args ret) Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods showsPrec :: Int -> FnHandle args ret -> ShowS # show :: FnHandle args ret -> String # showList :: [FnHandle args ret] -> ShowS #
Eq (FnHandle args ret) Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods (==) :: FnHandle args ret -> FnHandle args ret -> Bool # (/=) :: FnHandle args ret -> FnHandle args ret -> Bool #
Ord (FnHandle args ret) Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods compare :: FnHandle args ret -> FnHandle args ret -> Ordering # (<) :: FnHandle args ret -> FnHandle args ret -> Bool # (<=) :: FnHandle args ret -> FnHandle args ret -> Bool # (>) :: FnHandle args ret -> FnHandle args ret -> Bool # (>=) :: FnHandle args ret -> FnHandle args ret -> Bool # max :: FnHandle args ret -> FnHandle args ret -> FnHandle args ret # min :: FnHandle args ret -> FnHandle args ret -> FnHandle args ret #
Hashable (FnHandle args ret) Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods hashWithSalt :: Int -> FnHandle args ret -> Int # hash :: FnHandle args ret -> Int #

handleID :: FnHandle args ret -> Nonce GlobalNonceGenerator (args ::> ret) Source #

A unique identifier for the function.

handleName :: FnHandle args ret -> FunctionName Source #

The name of the function (not necessarily unique)

handleArgTypes :: FnHandle args ret -> CtxRepr args Source #

The arguments types for the function

handleReturnType :: FnHandle args ret -> TypeRepr ret Source #

The return type of the function.

handleType :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType). FnHandle args ret -> TypeRepr (FunctionHandleType args ret) Source #

Return type of handle.

data SomeHandle where Source #

A function handle is a reference to a function in a given run of the simulator. It has a set of expected arguments and return type.

Constructors

SomeHandle :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType). !(FnHandle args ret) -> SomeHandle

Instances

Instances details

Show SomeHandle Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods showsPrec :: Int -> SomeHandle -> ShowS # show :: SomeHandle -> String # showList :: [SomeHandle] -> ShowS #
Eq SomeHandle Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods (==) :: SomeHandle -> SomeHandle -> Bool # (/=) :: SomeHandle -> SomeHandle -> Bool #
Ord SomeHandle Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods compare :: SomeHandle -> SomeHandle -> Ordering # (<) :: SomeHandle -> SomeHandle -> Bool # (<=) :: SomeHandle -> SomeHandle -> Bool # (>) :: SomeHandle -> SomeHandle -> Bool # (>=) :: SomeHandle -> SomeHandle -> Bool # max :: SomeHandle -> SomeHandle -> SomeHandle # min :: SomeHandle -> SomeHandle -> SomeHandle #
Hashable SomeHandle Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods hashWithSalt :: Int -> SomeHandle -> Int # hash :: SomeHandle -> Int #

Allocate handle.

data HandleAllocator Source #

Used to allocate function handles.

haCounter :: HandleAllocator -> NonceGenerator IO GlobalNonceGenerator Source #

newHandleAllocator :: IO HandleAllocator Source #

Create a new handle allocator.

withHandleAllocator :: (HandleAllocator -> IO a) -> IO a Source #

Create a new handle allocator and run the given computation.

mkHandle :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType). (KnownCtx TypeRepr args, KnownRepr TypeRepr ret) => HandleAllocator -> FunctionName -> IO (FnHandle args ret) Source #

Allocate a new function handle with requested args and ret types

mkHandle' :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType). HandleAllocator -> FunctionName -> Assignment TypeRepr args -> TypeRepr ret -> IO (FnHandle args ret) Source #

Allocate a new function handle.

FnHandleMap

data FnHandleMap (f :: Ctx CrucibleType -> CrucibleType -> Type) Source #

emptyHandleMap :: forall (f :: Ctx CrucibleType -> CrucibleType -> Type). FnHandleMap f Source #

insertHandleMap :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) f. FnHandle args ret -> f args ret -> FnHandleMap f -> FnHandleMap f Source #

lookupHandleMap :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) f. FnHandle args ret -> FnHandleMap f -> Maybe (f args ret) Source #

Lookup the function specification in the map via the Nonce index in the FnHandle argument.

updateHandleMap :: forall f (args :: Ctx CrucibleType) (ret :: CrucibleType). (f args ret -> f args ret) -> FnHandle args ret -> FnHandleMap f -> FnHandleMap f Source #

Update the entry of the function handle in the map.

searchHandleMap :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) f. FunctionName -> TypeRepr (FunctionHandleType args ret) -> FnHandleMap f -> Maybe (FnHandle args ret, f args ret) Source #

Lookup the function name in the map by a linear scan of all entries. This will be much slower than using lookupHandleMap to find the function by ID, so the latter should be used if possible.

handleMapToHandles :: forall (f :: Ctx CrucibleType -> CrucibleType -> Type). FnHandleMap f -> [SomeHandle] Source #

Reference cells

data RefCell (tp :: CrucibleType) Source #

Instances

Instances details

TestEquality RefCell Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). RefCell a -> RefCell b -> Maybe (a :~: b) #
OrdF RefCell Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). RefCell x -> RefCell y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). RefCell x -> RefCell y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). RefCell x -> RefCell y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). RefCell x -> RefCell y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). RefCell x -> RefCell y -> Bool #
ShowF RefCell Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods withShow :: forall p q (tp :: CrucibleType) a. p RefCell -> q tp -> (Show (RefCell tp) => a) -> a # showF :: forall (tp :: CrucibleType). RefCell tp -> String # showsPrecF :: forall (tp :: CrucibleType). Int -> RefCell tp -> String -> String #
Show (RefCell tp) Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods showsPrec :: Int -> RefCell tp -> ShowS # show :: RefCell tp -> String # showList :: [RefCell tp] -> ShowS #
Eq (RefCell tp) Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods (==) :: RefCell tp -> RefCell tp -> Bool # (/=) :: RefCell tp -> RefCell tp -> Bool #
Ord (RefCell tp) Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods compare :: RefCell tp -> RefCell tp -> Ordering # (<) :: RefCell tp -> RefCell tp -> Bool # (<=) :: RefCell tp -> RefCell tp -> Bool # (>) :: RefCell tp -> RefCell tp -> Bool # (>=) :: RefCell tp -> RefCell tp -> Bool # max :: RefCell tp -> RefCell tp -> RefCell tp # min :: RefCell tp -> RefCell tp -> RefCell tp #

freshRefCell :: forall (tp :: CrucibleType). HandleAllocator -> TypeRepr tp -> IO (RefCell tp) Source #

refType :: forall (tp :: CrucibleType). RefCell tp -> TypeRepr tp Source #