| Copyright | (c) Galois Inc 2015-2016 |
|---|---|
| License | BSD3 |
| Maintainer | Rob Dockins <rdockins@galois.com> |
| Stability | provisional |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Lang.Crucible.Simulator.Intrinsics
Contents
Description
Intrinsic types can be used to extend the basic set of types available
to the Crucible simulator. A new intrinsic type is defined by
implementing an IntrinsicClass instance, which binds a type-level name
to a particular impelementation. To use an intrinsic type, one must
register the associated IntrinsicMuxFn value with the simulator
prior to starting it. This is done by building an IntrinsicMuxFns
map to be passed to the initSimContext function.
Synopsis
- class IntrinsicClass (sym :: Type) (nm :: Symbol) where
- type Intrinsic (sym :: Type) (nm :: Symbol) (ctx :: Ctx CrucibleType) :: Type
- pushBranchIntrinsic :: sym -> IntrinsicTypes sym -> SymbolRepr nm -> CtxRepr ctx -> Intrinsic sym nm ctx -> IO (Intrinsic sym nm ctx)
- abortBranchIntrinsic :: sym -> IntrinsicTypes sym -> SymbolRepr nm -> CtxRepr ctx -> Intrinsic sym nm ctx -> IO (Intrinsic sym nm ctx)
- muxIntrinsic :: sym -> IntrinsicTypes sym -> SymbolRepr nm -> CtxRepr ctx -> Pred sym -> Intrinsic sym nm ctx -> Intrinsic sym nm ctx -> IO (Intrinsic sym nm ctx)
- type family GetIntrinsic sym ity where ...
- data IntrinsicMuxFn (sym :: Type) (nm :: Symbol) where
- IntrinsicMuxFn :: IntrinsicClass sym nm => IntrinsicMuxFn sym nm
- type IntrinsicTypes sym = MapF SymbolRepr (IntrinsicMuxFn sym)
- emptyIntrinsicTypes :: IntrinsicTypes sym
- typeError :: HasCallStack => SymbolRepr nm -> CtxRepr ctx -> b
Intrinsic types
class IntrinsicClass (sym :: Type) (nm :: Symbol) where Source #
Type family for intrinsic type representations. Intrinsic types
are identified by a type-level Symbol, and this typeclass allows
backends to define implementations for these types.
An instance of this class defines both an instance for the
Intrinsic type family (which defines the runtime representation
for this intrinsic type) and also the muxIntrinsic method
(which defines how to merge to intrinsic values when the simulator
reaches a merge point).
Note: Instances of this will typically end up as orphan instances.
This warning is normally quite important, as orphan instances allow
one to define multiple instances for a particular class. However, in
this case, IntrinsicClass contains a type family, and GHC will globally
check consistency of all type family instances. Consequently, there
can be at most one implementation of IntrinsicClass in a program.
Minimal complete definition
Associated Types
type Intrinsic (sym :: Type) (nm :: Symbol) (ctx :: Ctx CrucibleType) :: Type Source #
The Intrinsic type family defines, for a given backend and symbol name,
the runtime implementation of that Crucible intrinsic type.
Methods
pushBranchIntrinsic :: sym -> IntrinsicTypes sym -> SymbolRepr nm -> CtxRepr ctx -> Intrinsic sym nm ctx -> IO (Intrinsic sym nm ctx) Source #
The push branch function is called when an intrinsic value is passed through a symbolic branch. This allows it to do any necessary bookkeeping to prepare for an upcoming merge. A push branch should eventually be followed by a matching abort or mux call.
abortBranchIntrinsic :: sym -> IntrinsicTypes sym -> SymbolRepr nm -> CtxRepr ctx -> Intrinsic sym nm ctx -> IO (Intrinsic sym nm ctx) Source #
The abort branch function is called when an intrinsic value reaches a merge point, but the sibling branch has aborted.
muxIntrinsic :: sym -> IntrinsicTypes sym -> SymbolRepr nm -> CtxRepr ctx -> Pred sym -> Intrinsic sym nm ctx -> Intrinsic sym nm ctx -> IO (Intrinsic sym nm ctx) Source #
The muxIntrinsic method defines the if-then-else operation that is used
when paths are merged in the simulator and intrinsic types need to be used.
Instances
| IntrinsicClass sym "BoundedExecFrameData" Source # | |
Defined in Lang.Crucible.Simulator.BoundedExec Methods pushBranchIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "BoundedExecFrameData" -> CtxRepr ctx -> Intrinsic sym "BoundedExecFrameData" ctx -> IO (Intrinsic sym "BoundedExecFrameData" ctx) Source # abortBranchIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "BoundedExecFrameData" -> CtxRepr ctx -> Intrinsic sym "BoundedExecFrameData" ctx -> IO (Intrinsic sym "BoundedExecFrameData" ctx) Source # muxIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "BoundedExecFrameData" -> CtxRepr ctx -> Pred sym -> Intrinsic sym "BoundedExecFrameData" ctx -> Intrinsic sym "BoundedExecFrameData" ctx -> IO (Intrinsic sym "BoundedExecFrameData" ctx) Source # | |
| IntrinsicClass sym "BoundedRecursionData" Source # | |
Defined in Lang.Crucible.Simulator.BoundedRecursion Methods pushBranchIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "BoundedRecursionData" -> CtxRepr ctx -> Intrinsic sym "BoundedRecursionData" ctx -> IO (Intrinsic sym "BoundedRecursionData" ctx) Source # abortBranchIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "BoundedRecursionData" -> CtxRepr ctx -> Intrinsic sym "BoundedRecursionData" ctx -> IO (Intrinsic sym "BoundedRecursionData" ctx) Source # muxIntrinsic :: forall (ctx :: Ctx CrucibleType). sym -> IntrinsicTypes sym -> SymbolRepr "BoundedRecursionData" -> CtxRepr ctx -> Pred sym -> Intrinsic sym "BoundedRecursionData" ctx -> Intrinsic sym "BoundedRecursionData" ctx -> IO (Intrinsic sym "BoundedRecursionData" ctx) Source # | |
type family GetIntrinsic sym ity where ... Source #
Sometimes it is convenient to provide a CrucibleType as the type
argument to Intrinsic, rather than the symbol and context. If you
accidentally supply a non-IntrinsicType type, this family will be stuck.
Equations
| GetIntrinsic sym (IntrinsicType nm ctx) = Intrinsic sym nm ctx | |
| GetIntrinsic sym x = TypeError ((('Text "Type mismatch:" ':$$: 'Text " Expected \8216IntrinsicType a b\8217") ':$$: ('Text " Actual " ':<>: 'ShowType x)) ':$$: (((('Text "In type family application \8216GetIntrinsic (" ':<>: 'ShowType sym) ':<>: 'Text ") (") ':<>: 'ShowType x) ':<>: 'Text ")\8217")) |
data IntrinsicMuxFn (sym :: Type) (nm :: Symbol) where Source #
The IntrinsicMuxFn datatype allows an IntrinsicClass instance
to be packaged up into a value. This allows us to get access to IntrinsicClass
instance methods (the muxIntrinsic method in particular) at runtime even
for symbol names that are not known statically.
By packaging up a type class instance (rather than just providing some method with the
same signature as muxIntrinsic) we get the compiler to ensure that a single
distinguished implementation is always used for each backend/symbol name combination.
This prevents any possible confusion between different parts of the system.
Constructors
| IntrinsicMuxFn :: IntrinsicClass sym nm => IntrinsicMuxFn sym nm |
type IntrinsicTypes sym = MapF SymbolRepr (IntrinsicMuxFn sym) Source #
IntrinsicTypes is a map from symbol name representatives to IntrinsicMuxFn
values. Such a map is useful for providing access to intrinsic type implementations
that are not known statically at compile time.
emptyIntrinsicTypes :: IntrinsicTypes sym Source #
An empty collection of intrinsic types, for cases where no additional types are required
typeError :: HasCallStack => SymbolRepr nm -> CtxRepr ctx -> b Source #
Utility function for reporting errors when improper Crucible type arguments are applied to an intrinsic type symbol.