Copyright	(c) Galois Inc 2014
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

Lang.Crucible.Types

Contents

CrucibleType data kind
- Constructors for kind CrucibleType
IsRecursiveType
Base type injection
Other stuff
Representation of Crucible types
Re-exports

Description

This module exports the types used in Crucible expressions.

These types are largely used as indexes to various GADTs and type families as a way to let the GHC typechecker help us keep expressions of the embedded CFG language apart.

In addition, we provide a value-level reification of the type indices that can be examined by pattern matching, called TypeRepr. The KnownRepr class computes the value-level representation of a given type index, when the type is known at compile time. Similar setups exist for other components of the type system: bitvector data and type contexts.

Synopsis

data CrucibleType
type AnyType = 'AnyType
type UnitType = 'UnitType
type BoolType = BaseToType BaseBoolType
type NatType = 'NatType
type IntegerType = BaseToType BaseIntegerType
type RealValType = BaseToType BaseRealType
type SymbolicStructType (flds :: Ctx BaseType) = BaseToType (BaseStructType flds)
type ComplexRealType = BaseToType BaseComplexType
type BVType (w :: Nat) = BaseToType (BaseBVType w)
type FloatType = 'FloatType
type IEEEFloatType (p :: FloatPrecision) = BaseToType (BaseFloatType p)
type CharType = 'CharType
type StringType (si :: StringInfo) = BaseToType (BaseStringType si)
type FunctionHandleType = 'FunctionHandleType
type MaybeType = 'MaybeType
type RecursiveType = 'RecursiveType
type IntrinsicType (ctx :: Symbol) = 'IntrinsicType ctx
type VectorType = 'VectorType
type SequenceType = 'SequenceType
type StructType = 'StructType
type VariantType = 'VariantType
type ReferenceType = 'ReferenceType
type WordMapType = 'WordMapType
type StringMapType = 'StringMapType
type SymbolicArrayType (idx :: Ctx BaseType) (xs :: BaseType) = BaseToType (BaseArrayType idx xs)
class IsRecursiveType (nm :: Symbol) where
- type UnrollType (nm :: Symbol) (ctx :: Ctx CrucibleType) :: CrucibleType
- unrollType :: forall (ctx :: Ctx CrucibleType). SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
type BaseToType = 'BaseToType
baseToType :: forall (bt :: BaseType). BaseTypeRepr bt -> TypeRepr (BaseToType bt)
data AsBaseType (tp :: CrucibleType) where
- AsBaseType :: forall (tp :: CrucibleType) (bt :: BaseType). tp ~ BaseToType bt => BaseTypeRepr bt -> AsBaseType tp
- NotBaseType :: forall (tp :: CrucibleType). AsBaseType tp
asBaseType :: forall (tp :: CrucibleType). TypeRepr tp -> AsBaseType tp
type CtxRepr = Assignment TypeRepr
pattern KnownBV :: forall (n :: Natural). (1 <= n, KnownNat n) => TypeRepr (BVType n)
ppTypeRepr :: forall f ann (tp :: CrucibleType). Monad f => (forall (s :: Symbol) (ctx :: Ctx CrucibleType). SymbolRepr s -> CtxRepr ctx -> f (Doc ann)) -> TypeRepr tp -> f (Doc ann)
ppIntrinsicDefault :: forall (s :: Symbol) (ctx :: Ctx CrucibleType) ann. SymbolRepr s -> CtxRepr ctx -> Doc ann
data TypeRepr (tp :: CrucibleType) where
- AnyRepr :: TypeRepr 'AnyType
- UnitRepr :: TypeRepr 'UnitType
- BoolRepr :: TypeRepr ('BaseToType BaseBoolType)
- NatRepr :: TypeRepr 'NatType
- IntegerRepr :: TypeRepr ('BaseToType BaseIntegerType)
- RealValRepr :: TypeRepr ('BaseToType BaseRealType)
- ComplexRealRepr :: TypeRepr ('BaseToType BaseComplexType)
- BVRepr :: forall (n :: Natural). 1 <= n => !(NatRepr n) -> TypeRepr ('BaseToType (BaseBVType n))
- IntrinsicRepr :: forall (nm :: Symbol) (ctx :: Ctx CrucibleType). !(SymbolRepr nm) -> !(CtxRepr ctx) -> TypeRepr ('IntrinsicType nm ctx)
- RecursiveRepr :: forall (nm :: Symbol) (ctx :: Ctx CrucibleType). IsRecursiveType nm => SymbolRepr nm -> CtxRepr ctx -> TypeRepr ('RecursiveType nm ctx)
- FloatRepr :: forall (flt :: FloatInfo). !(FloatInfoRepr flt) -> TypeRepr ('FloatType flt)
- IEEEFloatRepr :: forall (ps :: FloatPrecision). !(FloatPrecisionRepr ps) -> TypeRepr ('BaseToType (BaseFloatType ps))
- CharRepr :: TypeRepr 'CharType
- StringRepr :: forall (si :: StringInfo). StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
- FunctionHandleRepr :: forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType). !(CtxRepr ctx) -> !(TypeRepr ret) -> TypeRepr ('FunctionHandleType ctx ret)
- MaybeRepr :: forall (tp1 :: CrucibleType). !(TypeRepr tp1) -> TypeRepr ('MaybeType tp1)
- SequenceRepr :: forall (tp1 :: CrucibleType). !(TypeRepr tp1) -> TypeRepr ('SequenceType tp1)
- VectorRepr :: forall (tp1 :: CrucibleType). !(TypeRepr tp1) -> TypeRepr ('VectorType tp1)
- StructRepr :: forall (ctx :: Ctx CrucibleType). !(CtxRepr ctx) -> TypeRepr ('StructType ctx)
- VariantRepr :: forall (ctx :: Ctx CrucibleType). !(CtxRepr ctx) -> TypeRepr ('VariantType ctx)
- ReferenceRepr :: forall (a :: CrucibleType). !(TypeRepr a) -> TypeRepr ('ReferenceType a)
- WordMapRepr :: forall (n :: Natural) (tp1 :: BaseType). 1 <= n => !(NatRepr n) -> !(BaseTypeRepr tp1) -> TypeRepr ('WordMapType n tp1)
- StringMapRepr :: forall (tp1 :: CrucibleType). !(TypeRepr tp1) -> TypeRepr ('StringMapType tp1)
- SymbolicArrayRepr :: forall (idx :: Ctx BaseType) (tp1 :: BaseType) (t :: BaseType). !(Assignment BaseTypeRepr (idx ::> tp1)) -> !(BaseTypeRepr t) -> TypeRepr ('BaseToType (BaseArrayType (idx ::> tp1) t))
- SymbolicStructRepr :: forall (ctx :: Ctx BaseType). Assignment BaseTypeRepr ctx -> TypeRepr ('BaseToType (BaseStructType ctx))
module Data.Parameterized.Ctx
module Data.Parameterized.NatRepr
module Data.Parameterized.SymbolRepr
module What4.BaseTypes
module What4.InterpretedFloatingPoint

CrucibleType data kind

data CrucibleType Source #

This data kind describes the types of values and expressions that can occur in Crucible CFGs.

Instances

Instances details

TestEquality GlobalVar Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). GlobalVar a -> GlobalVar b -> Maybe (a :~: b) #
TestEquality RefCell Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). RefCell a -> RefCell b -> Maybe (a :~: b) #
TestEquality TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). TypeRepr a -> TypeRepr b -> Maybe (a :~: b) #
PrettyApp EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods ppApp :: (forall (x :: CrucibleType). f x -> Doc ann) -> forall (x :: CrucibleType). EmptyExprExtension f x -> Doc ann Source #
PrettyApp EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods ppApp :: (forall (x :: CrucibleType). f x -> Doc ann) -> forall (x :: CrucibleType). EmptyStmtExtension f x -> Doc ann Source #
EqF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods eqF :: forall (a :: CrucibleType). TypeRepr a -> TypeRepr a -> Bool #
HashableF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods hashWithSaltF :: forall (tp :: CrucibleType). Int -> TypeRepr tp -> Int # hashF :: forall (tp :: CrucibleType). TypeRepr tp -> Int #
OrdF GlobalVar Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). GlobalVar x -> GlobalVar y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). GlobalVar x -> GlobalVar y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). GlobalVar x -> GlobalVar y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). GlobalVar x -> GlobalVar y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). GlobalVar x -> GlobalVar y -> Bool #
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 #
OrdF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). TypeRepr x -> TypeRepr y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). TypeRepr x -> TypeRepr y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). TypeRepr x -> TypeRepr y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). TypeRepr x -> TypeRepr y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). TypeRepr x -> TypeRepr y -> Bool #
ShowF GlobalVar Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods withShow :: forall p q (tp :: CrucibleType) a. p GlobalVar -> q tp -> (Show (GlobalVar tp) => a) -> a # showF :: forall (tp :: CrucibleType). GlobalVar tp -> String # showsPrecF :: forall (tp :: CrucibleType). Int -> GlobalVar tp -> String -> String #
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 #
ShowF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods withShow :: forall p q (tp :: CrucibleType) a. p TypeRepr -> q tp -> (Show (TypeRepr tp) => a) -> a # showF :: forall (tp :: CrucibleType). TypeRepr tp -> String # showsPrecF :: forall (tp :: CrucibleType). Int -> TypeRepr tp -> String -> String #
KnownRepr TypeRepr AnyType Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr AnyType #
KnownRepr TypeRepr CharType Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr CharType #
KnownRepr TypeRepr NatType Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr NatType #
KnownRepr TypeRepr UnitType Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr UnitType #
ApplyEmbedding' Reg Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods applyEmbedding' :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) (v :: CrucibleType). CtxEmbedding ctx ctx' -> Reg ctx v -> Reg ctx' v #
ExtendContext' Reg Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods extendContext' :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) (v :: CrucibleType). Diff ctx ctx' -> Reg ctx v -> Reg ctx' v #
FoldableFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods foldMapFC :: forall f m. Monoid m => (forall (x :: CrucibleType). f x -> m) -> forall (x :: CrucibleType). EmptyExprExtension f x -> m # foldrFC :: (forall (x :: CrucibleType). f x -> b -> b) -> forall (x :: CrucibleType). b -> EmptyExprExtension f x -> b # foldlFC :: forall f b. (forall (x :: CrucibleType). b -> f x -> b) -> forall (x :: CrucibleType). b -> EmptyExprExtension f x -> b # foldrFC' :: (forall (x :: CrucibleType). f x -> b -> b) -> forall (x :: CrucibleType). b -> EmptyExprExtension f x -> b # foldlFC' :: forall f b. (forall (x :: CrucibleType). b -> f x -> b) -> forall (x :: CrucibleType). b -> EmptyExprExtension f x -> b # toListFC :: (forall (x :: CrucibleType). f x -> a) -> forall (x :: CrucibleType). EmptyExprExtension f x -> [a] #
FoldableFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods foldMapFC :: forall f m. Monoid m => (forall (x :: CrucibleType). f x -> m) -> forall (x :: CrucibleType). EmptyStmtExtension f x -> m # foldrFC :: (forall (x :: CrucibleType). f x -> b -> b) -> forall (x :: CrucibleType). b -> EmptyStmtExtension f x -> b # foldlFC :: forall f b. (forall (x :: CrucibleType). b -> f x -> b) -> forall (x :: CrucibleType). b -> EmptyStmtExtension f x -> b # foldrFC' :: (forall (x :: CrucibleType). f x -> b -> b) -> forall (x :: CrucibleType). b -> EmptyStmtExtension f x -> b # foldlFC' :: forall f b. (forall (x :: CrucibleType). b -> f x -> b) -> forall (x :: CrucibleType). b -> EmptyStmtExtension f x -> b # toListFC :: (forall (x :: CrucibleType). f x -> a) -> forall (x :: CrucibleType). EmptyStmtExtension f x -> [a] #
FoldableFC BaseTerm Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods foldMapFC :: forall f m. Monoid m => (forall (x :: CrucibleType). f x -> m) -> forall (x :: BaseType). BaseTerm f x -> m # foldrFC :: (forall (x :: CrucibleType). f x -> b -> b) -> forall (x :: BaseType). b -> BaseTerm f x -> b # foldlFC :: forall f b. (forall (x :: CrucibleType). b -> f x -> b) -> forall (x :: BaseType). b -> BaseTerm f x -> b # foldrFC' :: (forall (x :: CrucibleType). f x -> b -> b) -> forall (x :: BaseType). b -> BaseTerm f x -> b # foldlFC' :: forall f b. (forall (x :: CrucibleType). b -> f x -> b) -> forall (x :: BaseType). b -> BaseTerm f x -> b # toListFC :: (forall (x :: CrucibleType). f x -> a) -> forall (x :: BaseType). BaseTerm f x -> [a] #
FunctorFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods fmapFC :: (forall (x :: CrucibleType). f x -> g x) -> forall (x :: CrucibleType). EmptyExprExtension f x -> EmptyExprExtension g x #
FunctorFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods fmapFC :: (forall (x :: CrucibleType). f x -> g x) -> forall (x :: CrucibleType). EmptyStmtExtension f x -> EmptyStmtExtension g x #
FunctorFC BaseTerm Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods fmapFC :: (forall (x :: CrucibleType). f x -> g x) -> forall (x :: BaseType). BaseTerm f x -> BaseTerm g x #
HashableFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods hashWithSaltFC :: (forall (x :: CrucibleType). Int -> f x -> Int) -> forall (x :: CrucibleType). Int -> EmptyExprExtension f x -> Int #
HashableFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods hashWithSaltFC :: (forall (x :: CrucibleType). Int -> f x -> Int) -> forall (x :: CrucibleType). Int -> EmptyStmtExtension f x -> Int #
OrdFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods compareFC :: (forall (x :: CrucibleType) (y :: CrucibleType). f x -> f y -> OrderingF x y) -> forall (x :: CrucibleType) (y :: CrucibleType). EmptyExprExtension f x -> EmptyExprExtension f y -> OrderingF x y #
OrdFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods compareFC :: (forall (x :: CrucibleType) (y :: CrucibleType). f x -> f y -> OrderingF x y) -> forall (x :: CrucibleType) (y :: CrucibleType). EmptyStmtExtension f x -> EmptyStmtExtension f y -> OrderingF x y #
OrdFC BaseTerm Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods compareFC :: (forall (x :: CrucibleType) (y :: CrucibleType). f x -> f y -> OrderingF x y) -> forall (x :: BaseType) (y :: BaseType). BaseTerm f x -> BaseTerm f y -> OrderingF x y #
ShowFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods showFC :: (forall (x :: CrucibleType). f x -> String) -> forall (x :: CrucibleType). EmptyExprExtension f x -> String # showsPrecFC :: (forall (x :: CrucibleType). Int -> f x -> ShowS) -> forall (x :: CrucibleType). Int -> EmptyExprExtension f x -> ShowS #
ShowFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods showFC :: (forall (x :: CrucibleType). f x -> String) -> forall (x :: CrucibleType). EmptyStmtExtension f x -> String # showsPrecFC :: (forall (x :: CrucibleType). Int -> f x -> ShowS) -> forall (x :: CrucibleType). Int -> EmptyStmtExtension f x -> ShowS #
TestEqualityFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods testEqualityFC :: (forall (x :: CrucibleType) (y :: CrucibleType). f x -> f y -> Maybe (x :~: y)) -> forall (x :: CrucibleType) (y :: CrucibleType). EmptyExprExtension f x -> EmptyExprExtension f y -> Maybe (x :~: y) #
TestEqualityFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods testEqualityFC :: (forall (x :: CrucibleType) (y :: CrucibleType). f x -> f y -> Maybe (x :~: y)) -> forall (x :: CrucibleType) (y :: CrucibleType). EmptyStmtExtension f x -> EmptyStmtExtension f y -> Maybe (x :~: y) #
TestEqualityFC BaseTerm Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods testEqualityFC :: (forall (x :: CrucibleType) (y :: CrucibleType). f x -> f y -> Maybe (x :~: y)) -> forall (x :: BaseType) (y :: BaseType). BaseTerm f x -> BaseTerm f y -> Maybe (x :~: y) #
TraversableFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods traverseFC :: forall f g m. Applicative m => (forall (x :: CrucibleType). f x -> m (g x)) -> forall (x :: CrucibleType). EmptyExprExtension f x -> m (EmptyExprExtension g x) #
TraversableFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods traverseFC :: forall f g m. Applicative m => (forall (x :: CrucibleType). f x -> m (g x)) -> forall (x :: CrucibleType). EmptyStmtExtension f x -> m (EmptyStmtExtension g x) #
TraversableFC BaseTerm Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods traverseFC :: forall f g m. Applicative m => (forall (x :: CrucibleType). f x -> m (g x)) -> forall (x :: BaseType). BaseTerm f x -> m (BaseTerm g x) #
KnownRepr BaseTypeRepr bt => KnownRepr TypeRepr (BaseToType bt :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (BaseToType bt) #
KnownRepr FloatInfoRepr flt => KnownRepr TypeRepr (FloatType flt :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (FloatType flt) #
KnownRepr FloatPrecisionRepr ps => KnownRepr TypeRepr (IEEEFloatType ps :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (IEEEFloatType ps) #
KnownRepr TypeRepr tp => KnownRepr TypeRepr (MaybeType tp :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (MaybeType tp) #
KnownRepr TypeRepr a => KnownRepr TypeRepr (ReferenceType a :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (ReferenceType a) #
KnownRepr TypeRepr tp => KnownRepr TypeRepr (SequenceType tp :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (SequenceType tp) #
KnownRepr TypeRepr tp => KnownRepr TypeRepr (StringMapType tp :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (StringMapType tp) #
KnownCtx TypeRepr ctx => KnownRepr TypeRepr (StructType ctx :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (StructType ctx) #
KnownCtx TypeRepr ctx => KnownRepr TypeRepr (VariantType ctx :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (VariantType ctx) #
KnownRepr TypeRepr tp => KnownRepr TypeRepr (VectorType tp :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (VectorType tp) #
TraversableFC (ExprExtension ext) => ApplyEmbedding' (Expr ext :: Ctx CrucibleType -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods applyEmbedding' :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) (v :: CrucibleType). CtxEmbedding ctx ctx' -> Expr ext ctx v -> Expr ext ctx' v #
ApplyEmbedding' (SwitchTarget blocks :: Ctx CrucibleType -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods applyEmbedding' :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) (v :: CrucibleType). CtxEmbedding ctx ctx' -> SwitchTarget blocks ctx v -> SwitchTarget blocks ctx' v #
TraversableFC (ExprExtension ext) => ExtendContext' (Expr ext :: Ctx CrucibleType -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods extendContext' :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) (v :: CrucibleType). Diff ctx ctx' -> Expr ext ctx v -> Expr ext ctx' v #
ExtendContext' (SwitchTarget blocks :: Ctx CrucibleType -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods extendContext' :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) (v :: CrucibleType). Diff ctx ctx' -> SwitchTarget blocks ctx v -> SwitchTarget blocks ctx' v #
TraversableFC (ExprExtension ext) => FoldableFC (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods foldMapFC :: forall f m. Monoid m => (forall (x :: CrucibleType). f x -> m) -> forall (x :: CrucibleType). App ext f x -> m # foldrFC :: (forall (x :: CrucibleType). f x -> b -> b) -> forall (x :: CrucibleType). b -> App ext f x -> b # foldlFC :: forall f b. (forall (x :: CrucibleType). b -> f x -> b) -> forall (x :: CrucibleType). b -> App ext f x -> b # foldrFC' :: (forall (x :: CrucibleType). f x -> b -> b) -> forall (x :: CrucibleType). b -> App ext f x -> b # foldlFC' :: forall f b. (forall (x :: CrucibleType). b -> f x -> b) -> forall (x :: CrucibleType). b -> App ext f x -> b # toListFC :: (forall (x :: CrucibleType). f x -> a) -> forall (x :: CrucibleType). App ext f x -> [a] #
TraversableFC (ExprExtension ext) => FunctorFC (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods fmapFC :: (forall (x :: CrucibleType). f x -> g x) -> forall (x :: CrucibleType). App ext f x -> App ext g x #
OrdFC (ExprExtension ext) => OrdFC (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods compareFC :: (forall (x :: CrucibleType) (y :: CrucibleType). f x -> f y -> OrderingF x y) -> forall (x :: CrucibleType) (y :: CrucibleType). App ext f x -> App ext f y -> OrderingF x y #
TestEqualityFC (ExprExtension ext) => TestEqualityFC (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods testEqualityFC :: (forall (x :: CrucibleType) (y :: CrucibleType). f x -> f y -> Maybe (x :~: y)) -> forall (x :: CrucibleType) (y :: CrucibleType). App ext f x -> App ext f y -> Maybe (x :~: y) #
TraversableFC (ExprExtension ext) => TraversableFC (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods traverseFC :: forall f g m. Applicative m => (forall (x :: CrucibleType). f x -> m (g x)) -> forall (x :: CrucibleType). App ext f x -> m (App ext g x) #
(KnownCtx TypeRepr ctx, KnownRepr TypeRepr ret) => KnownRepr TypeRepr (FunctionHandleType ctx ret :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (FunctionHandleType ctx ret) #
(KnownSymbol s, KnownCtx TypeRepr ctx) => KnownRepr TypeRepr (IntrinsicType s ctx :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (IntrinsicType s ctx) #
(KnownSymbol s, KnownCtx TypeRepr ctx, IsRecursiveType s) => KnownRepr TypeRepr (RecursiveType s ctx :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (RecursiveType s ctx) #
(1 <= w, KnownNat w, KnownRepr BaseTypeRepr tp) => KnownRepr TypeRepr (WordMapType w tp :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (WordMapType w tp) #
TestEquality (Reg ctx :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). Reg ctx a -> Reg ctx b -> Maybe (a :~: b) #
TestEquality (Atom s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). Atom s a -> Atom s b -> Maybe (a :~: b) #
TestEquality (LambdaLabel s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). LambdaLabel s a -> LambdaLabel s b -> Maybe (a :~: b) #
TestEquality (Reg s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). Reg s a -> Reg s b -> Maybe (a :~: b) #
TestEquality (Value s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). Value s a -> Value s b -> Maybe (a :~: b) #
PrettyApp (ExprExtension ext) => PrettyApp (App ext :: (CrucibleType -> Type) -> CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods ppApp :: (forall (x :: CrucibleType). f x -> Doc ann) -> forall (x :: CrucibleType). App ext f x -> Doc ann Source #
OrdF (Reg ctx :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg ctx x -> Reg ctx y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg ctx x -> Reg ctx y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg ctx x -> Reg ctx y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg ctx x -> Reg ctx y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg ctx x -> Reg ctx y -> Bool #
OrdF (Atom s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). Atom s x -> Atom s y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). Atom s x -> Atom s y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). Atom s x -> Atom s y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). Atom s x -> Atom s y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). Atom s x -> Atom s y -> Bool #
OrdF (LambdaLabel s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). LambdaLabel s x -> LambdaLabel s y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). LambdaLabel s x -> LambdaLabel s y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). LambdaLabel s x -> LambdaLabel s y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). LambdaLabel s x -> LambdaLabel s y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). LambdaLabel s x -> LambdaLabel s y -> Bool #
OrdF (Reg s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg s x -> Reg s y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg s x -> Reg s y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg s x -> Reg s y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg s x -> Reg s y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). Reg s x -> Reg s y -> Bool #
OrdF (Value s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). Value s x -> Value s y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). Value s x -> Value s y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). Value s x -> Value s y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). Value s x -> Value s y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). Value s x -> Value s y -> Bool #
ShowF dom => ShowF (Pointed dom :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.Analysis.Fixpoint Methods withShow :: forall p q (tp :: CrucibleType) a. p (Pointed dom) -> q tp -> (Show (Pointed dom tp) => a) -> a # showF :: forall (tp :: CrucibleType). Pointed dom tp -> String # showsPrecF :: forall (tp :: CrucibleType). Int -> Pointed dom tp -> String -> String #
ShowF (Reg ctx :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods withShow :: forall p q (tp :: CrucibleType) a. p (Reg ctx) -> q tp -> (Show (Reg ctx tp) => a) -> a # showF :: forall (tp :: CrucibleType). Reg ctx tp -> String # showsPrecF :: forall (tp :: CrucibleType). Int -> Reg ctx tp -> String -> String #
ShowF (Reg s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods withShow :: forall p q (tp :: CrucibleType) a. p (Reg s) -> q tp -> (Show (Reg s tp) => a) -> a # showF :: forall (tp :: CrucibleType). Reg s tp -> String # showsPrecF :: forall (tp :: CrucibleType). Int -> Reg s tp -> String -> String #
ShowF (Value s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods withShow :: forall p q (tp :: CrucibleType) a. p (Value s) -> q tp -> (Show (Value s tp) => a) -> a # showF :: forall (tp :: CrucibleType). Value s tp -> String # showsPrecF :: forall (tp :: CrucibleType). Int -> Value s tp -> String -> String #
ApplyEmbedding (JumpTarget blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods applyEmbedding :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType). CtxEmbedding ctx ctx' -> JumpTarget blocks ctx -> JumpTarget blocks ctx' #
ExtendContext (JumpTarget blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods extendContext :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType). Diff ctx ctx' -> JumpTarget blocks ctx -> JumpTarget blocks ctx' #
(TestEqualityFC (ExprExtension ext), TestEquality f) => TestEquality (App ext f :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). App ext f a -> App ext f b -> Maybe (a :~: b) #
(OrdFC (ExprExtension ext), OrdF f) => OrdF (App ext f :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). App ext f x -> App ext f y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). App ext f x -> App ext f y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). App ext f x -> App ext f y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). App ext f x -> App ext f y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). App ext f x -> App ext f y -> Bool #
PrettyExt ext => ShowF (Expr ext s :: CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods withShow :: forall p q (tp :: CrucibleType) a. p (Expr ext s) -> q tp -> (Show (Expr ext s tp) => a) -> a # showF :: forall (tp :: CrucibleType). Expr ext s tp -> String # showsPrecF :: forall (tp :: CrucibleType). Int -> Expr ext s tp -> String -> String #
ApplyEmbedding (TermStmt blocks ret :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods applyEmbedding :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType). CtxEmbedding ctx ctx' -> TermStmt blocks ret ctx -> TermStmt blocks ret ctx' #
ExtendContext (TermStmt blocks ret :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods extendContext :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType). Diff ctx ctx' -> TermStmt blocks ret ctx -> TermStmt blocks ret ctx' #
TraverseExt ext => ApplyEmbedding (StmtSeq ext blocks ret :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods applyEmbedding :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType). CtxEmbedding ctx ctx' -> StmtSeq ext blocks ret ctx -> StmtSeq ext blocks ret ctx' #
Pretty (ValueSet s) Source #
Instance details Defined in Lang.Crucible.CFG.Reg Methods pretty :: ValueSet s -> Doc ann # prettyList :: [ValueSet s] -> Doc ann #
TestEquality (BlockID blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods testEquality :: forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType). BlockID blocks a -> BlockID blocks b -> Maybe (a :~: b) #
TestEquality (CrucibleBranchTarget f :: Maybe (Ctx CrucibleType) -> Type) Source #
Instance details Defined in Lang.Crucible.Simulator.CallFrame Methods testEquality :: forall (a :: Maybe (Ctx CrucibleType)) (b :: Maybe (Ctx CrucibleType)). CrucibleBranchTarget f a -> CrucibleBranchTarget f b -> Maybe (a :~: b) #
OrdF (BlockID blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods compareF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> OrderingF x y # leqF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> Bool # ltF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> Bool # geqF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> Bool # gtF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType). BlockID blocks x -> BlockID blocks y -> Bool #
ShowF (BlockID blocks :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods withShow :: forall p q (tp :: Ctx CrucibleType) a. p (BlockID blocks) -> q tp -> (Show (BlockID blocks tp) => a) -> a # showF :: forall (tp :: Ctx CrucibleType). BlockID blocks tp -> String # showsPrecF :: forall (tp :: Ctx CrucibleType). Int -> BlockID blocks tp -> String -> String #
ShowF dom => ShowF (PointAbstraction blocks dom :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.Analysis.Fixpoint Methods withShow :: forall p q (tp :: Ctx CrucibleType) a. p (PointAbstraction blocks dom) -> q tp -> (Show (PointAbstraction blocks dom tp) => a) -> a # showF :: forall (tp :: Ctx CrucibleType). PointAbstraction blocks dom tp -> String # showsPrecF :: forall (tp :: Ctx CrucibleType). Int -> PointAbstraction blocks dom tp -> String -> String #
PrettyExt ext => ShowF (Block ext blocks ret :: Ctx CrucibleType -> Type) Source #
Instance details Defined in Lang.Crucible.CFG.Core Methods withShow :: forall p q (tp :: Ctx CrucibleType) a. p (Block ext blocks ret) -> q tp -> (Show (Block ext blocks ret tp) => a) -> a # showF :: forall (tp :: Ctx CrucibleType). Block ext blocks ret tp -> String # showsPrecF :: forall (tp :: Ctx CrucibleType). Int -> Block ext blocks ret tp -> String -> String #
MonadState (SimState p sym ext rtp (OverrideLang ret) ('Just args)) (OverrideSim p sym ext rtp args ret) Source #
Instance details Defined in Lang.Crucible.Simulator.OverrideSim Methods get :: OverrideSim p sym ext rtp args ret (SimState p sym ext rtp (OverrideLang ret) ('Just args)) # put :: SimState p sym ext rtp (OverrideLang ret) ('Just args) -> OverrideSim p sym ext rtp args ret () # state :: (SimState p sym ext rtp (OverrideLang ret) ('Just args) -> (a, SimState p sym ext rtp (OverrideLang ret) ('Just args))) -> OverrideSim p sym ext rtp args ret a #

Constructors for kind CrucibleType

type AnyType Source #

Arguments

= 'AnyType

:: CrucibleType.

A dynamic type that can contain values of any type.

type UnitType Source #

Arguments

= 'UnitType

:: CrucibleType.

A type containing a single value Unit.

type BoolType Source #

Arguments

= BaseToType BaseBoolType

:: CrucibleType.

type NatType Source #

Arguments

= 'NatType

:: CrucibleType.

A type for natural numbers.

type IntegerType Source #

Arguments

= BaseToType BaseIntegerType

:: CrucibleType.

type RealValType Source #

Arguments

= BaseToType BaseRealType

:: CrucibleType.

type SymbolicStructType (flds :: Ctx BaseType) Source #

Arguments

= BaseToType (BaseStructType flds)

:: Ctx BaseType -> CrucibleType.

type ComplexRealType Source #

Arguments

= BaseToType BaseComplexType

:: CrucibleType.

type BVType (w :: Nat) Source #

Arguments

= BaseToType (BaseBVType w)

:: Nat -> CrucibleType.

type FloatType Source #

Arguments

= 'FloatType

:: FloatInfo -> CrucibleType.

A type index for floating point numbers, whose interpretation depends on the symbolic backend.

type IEEEFloatType (p :: FloatPrecision) Source #

Arguments

= BaseToType (BaseFloatType p)

:: FloatPrecision -> CrucibleType

type CharType Source #

Arguments

= 'CharType

:: CrucibleType.

A single character, as a 16-bit wide char.

type StringType (si :: StringInfo) Source #

Arguments

= BaseToType (BaseStringType si)

:: StringInfo -> CrucibleType.

type FunctionHandleType Source #

Arguments

= 'FunctionHandleType

:: Ctx CrucibleType -> CrucibleType -> CrucibleType.

A function handle taking a context of formal arguments and a return type.

type MaybeType Source #

Arguments

= 'MaybeType

:: CrucibleType -> CrucibleType.

The Maybe type lifted into Crucible expressions.

type RecursiveType Source #

Arguments

= 'RecursiveType

:: Symbol -> Ctx CrucibleType -> CrucibleType.

Named recursive types, named by the given symbol. To use recursive types you must provide an instance of the IsRecursiveType class that gives the unfolding of this recursive type. The RollRecursive and UnrollRecursive operations witness the isomorphism between a recursive type and its one-step unrolling. Similar to Haskell's newtype, recursive types do not necessarily have to mention the recursive type being defined; in which case, the type is simply a new named type which is isomorphic to its definition.

type IntrinsicType (ctx :: Symbol) Source #

Arguments

= 'IntrinsicType ctx

:: Symbol -> Ctx CrucibleType -> CrucibleType.

Named intrinsic types. Intrinsic types are a way to extend the Crucible type system after-the-fact and add new type implementations. Core Crucible provides no operations on intrinsic types; they must be provided as built-in override functions. See the IntrinsicClass typeclass and the Intrinsic type family defined in Lang.Crucible.Simulator.Intrinsics.

type VectorType Source #

Arguments

= 'VectorType

:: CrucibleType -> CrucibleType.

A finite (one-dimensional) sequence of values. Vectors are optimized for random-access indexing and updating. Vectors of different lengths may not be combined at join points.

type SequenceType Source #

Arguments

= 'SequenceType

:: CrucibleType -> CrucibleType.

Sequences of values, represented as linked lists of cons cells. Sequences only allow access to the front. Unlike Vectors, sequences of different lengths may be combined at join points.

type StructType Source #

Arguments

= 'StructType

:: Ctx CrucibleType -> CrucibleType.

A structure is an aggregate type consisting of a sequence of values. The type of each value is known statically.

type VariantType Source #

Arguments

= 'VariantType

:: Ctx CrucibleType -> CrucibleType.

A variant is a disjoint union of the types listed in the context.

type ReferenceType Source #

Arguments

= 'ReferenceType

:: CrucibleType -> CrucibleType.

The type of mutable reference cells.

type WordMapType Source #

Arguments

= 'WordMapType

:: Nat -> BaseType -> CrucibleType.

A finite map from bitvector values to the given Crucible type. The Nat index gives the width of the bitvector values used to index the map.

type StringMapType Source #

Arguments

= 'StringMapType

:: CrucibleType -> CrucibleType.

A partial map from strings to values.

type SymbolicArrayType (idx :: Ctx BaseType) (xs :: BaseType) Source #

Arguments

= BaseToType (BaseArrayType idx xs)

:: Ctx BaseType -> BaseType -> CrucibleType.

IsRecursiveType

class IsRecursiveType (nm :: Symbol) where Source #

This typeclass is used to register recursive Crucible types with the compiler. This class defines, for a given symbol, both the type-level and the representative-level unrolling of a named recursive type.

The symbol constitutes a unique compile-time identifier for the recursive type, allowing recursive types to be unrolled at run time without requiring dynamic checks.

Parameter nm has kind Symbol.

Associated Types

type UnrollType (nm :: Symbol) (ctx :: Ctx CrucibleType) :: CrucibleType Source #

Methods

unrollType :: forall (ctx :: Ctx CrucibleType). SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx) Source #

Base type injection

type BaseToType Source #

Arguments

= 'BaseToType

:: BaseType -> CrucibleType.

baseToType :: forall (bt :: BaseType). BaseTypeRepr bt -> TypeRepr (BaseToType bt) Source #

data AsBaseType (tp :: CrucibleType) where Source #

Constructors

AsBaseType :: forall (tp :: CrucibleType) (bt :: BaseType). tp ~ BaseToType bt => BaseTypeRepr bt -> AsBaseType tp
NotBaseType :: forall (tp :: CrucibleType). AsBaseType tp

asBaseType :: forall (tp :: CrucibleType). TypeRepr tp -> AsBaseType tp Source #

Other stuff

type CtxRepr = Assignment TypeRepr Source #

pattern KnownBV :: forall (n :: Natural). (1 <= n, KnownNat n) => TypeRepr (BVType n) Source #

Pattern synonym specifying bitvector TypeReprs. Intended to be use with type applications, e.g., KnownBV @32.

ppTypeRepr Source #

Arguments

:: forall f ann (tp :: CrucibleType). Monad f
=> (forall (s :: Symbol) (ctx :: Ctx CrucibleType). SymbolRepr s -> CtxRepr ctx -> f (Doc ann))	How to print `IntrinsicRepr`, see `ppIntrinsicDefault`
-> TypeRepr tp
-> f (Doc ann)

Pretty-print a type.

Attempts to be consistent with the syntax provided in the crucible-syntax package.

This is monadic mostly to allow failure, e.g., in case the caller finds an intrinsic type that it doesn't expect.

ppIntrinsicDefault :: forall (s :: Symbol) (ctx :: Ctx CrucibleType) ann. SymbolRepr s -> CtxRepr ctx -> Doc ann Source #

A default printer for IntrinsicRepr, suitable for use with ppTypeRepr.

Representation of Crucible types

data TypeRepr (tp :: CrucibleType) where Source #

A family of representatives for Crucible types. Parameter tp has kind CrucibleType.

Constructors

AnyRepr :: TypeRepr 'AnyType
UnitRepr :: TypeRepr 'UnitType
BoolRepr :: TypeRepr ('BaseToType BaseBoolType)
NatRepr :: TypeRepr 'NatType
IntegerRepr :: TypeRepr ('BaseToType BaseIntegerType)
RealValRepr :: TypeRepr ('BaseToType BaseRealType)
ComplexRealRepr :: TypeRepr ('BaseToType BaseComplexType)
BVRepr :: forall (n :: Natural). 1 <= n => !(NatRepr n) -> TypeRepr ('BaseToType (BaseBVType n))
IntrinsicRepr :: forall (nm :: Symbol) (ctx :: Ctx CrucibleType). !(SymbolRepr nm) -> !(CtxRepr ctx) -> TypeRepr ('IntrinsicType nm ctx)
RecursiveRepr :: forall (nm :: Symbol) (ctx :: Ctx CrucibleType). IsRecursiveType nm => SymbolRepr nm -> CtxRepr ctx -> TypeRepr ('RecursiveType nm ctx)
FloatRepr :: forall (flt :: FloatInfo). !(FloatInfoRepr flt) -> TypeRepr ('FloatType flt)	This is a representation of floats that works at known fixed mantissa and exponent widths, but the symbolic backend may pick the representation.
IEEEFloatRepr :: forall (ps :: FloatPrecision). !(FloatPrecisionRepr ps) -> TypeRepr ('BaseToType (BaseFloatType ps))	This is a float with user-definable mantissa and exponent that maps directly to the what4 base type.
CharRepr :: TypeRepr 'CharType
StringRepr :: forall (si :: StringInfo). StringInfoRepr si -> TypeRepr ('BaseToType (BaseStringType si))
FunctionHandleRepr :: forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType). !(CtxRepr ctx) -> !(TypeRepr ret) -> TypeRepr ('FunctionHandleType ctx ret)
MaybeRepr :: forall (tp1 :: CrucibleType). !(TypeRepr tp1) -> TypeRepr ('MaybeType tp1)
SequenceRepr :: forall (tp1 :: CrucibleType). !(TypeRepr tp1) -> TypeRepr ('SequenceType tp1)
VectorRepr :: forall (tp1 :: CrucibleType). !(TypeRepr tp1) -> TypeRepr ('VectorType tp1)
StructRepr :: forall (ctx :: Ctx CrucibleType). !(CtxRepr ctx) -> TypeRepr ('StructType ctx)
VariantRepr :: forall (ctx :: Ctx CrucibleType). !(CtxRepr ctx) -> TypeRepr ('VariantType ctx)
ReferenceRepr :: forall (a :: CrucibleType). !(TypeRepr a) -> TypeRepr ('ReferenceType a)
WordMapRepr :: forall (n :: Natural) (tp1 :: BaseType). 1 <= n => !(NatRepr n) -> !(BaseTypeRepr tp1) -> TypeRepr ('WordMapType n tp1)
StringMapRepr :: forall (tp1 :: CrucibleType). !(TypeRepr tp1) -> TypeRepr ('StringMapType tp1)
SymbolicArrayRepr :: forall (idx :: Ctx BaseType) (tp1 :: BaseType) (t :: BaseType). !(Assignment BaseTypeRepr (idx ::> tp1)) -> !(BaseTypeRepr t) -> TypeRepr ('BaseToType (BaseArrayType (idx ::> tp1) t))
SymbolicStructRepr :: forall (ctx :: Ctx BaseType). Assignment BaseTypeRepr ctx -> TypeRepr ('BaseToType (BaseStructType ctx))

Instances

Instances details

TestEquality TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods testEquality :: forall (a :: CrucibleType) (b :: CrucibleType). TypeRepr a -> TypeRepr b -> Maybe (a :~: b) #
EqF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods eqF :: forall (a :: CrucibleType). TypeRepr a -> TypeRepr a -> Bool #
HashableF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods hashWithSaltF :: forall (tp :: CrucibleType). Int -> TypeRepr tp -> Int # hashF :: forall (tp :: CrucibleType). TypeRepr tp -> Int #
OrdF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods compareF :: forall (x :: CrucibleType) (y :: CrucibleType). TypeRepr x -> TypeRepr y -> OrderingF x y # leqF :: forall (x :: CrucibleType) (y :: CrucibleType). TypeRepr x -> TypeRepr y -> Bool # ltF :: forall (x :: CrucibleType) (y :: CrucibleType). TypeRepr x -> TypeRepr y -> Bool # geqF :: forall (x :: CrucibleType) (y :: CrucibleType). TypeRepr x -> TypeRepr y -> Bool # gtF :: forall (x :: CrucibleType) (y :: CrucibleType). TypeRepr x -> TypeRepr y -> Bool #
ShowF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods withShow :: forall p q (tp :: CrucibleType) a. p TypeRepr -> q tp -> (Show (TypeRepr tp) => a) -> a # showF :: forall (tp :: CrucibleType). TypeRepr tp -> String # showsPrecF :: forall (tp :: CrucibleType). Int -> TypeRepr tp -> String -> String #
KnownRepr TypeRepr AnyType Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr AnyType #
KnownRepr TypeRepr CharType Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr CharType #
KnownRepr TypeRepr NatType Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr NatType #
KnownRepr TypeRepr UnitType Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr UnitType #
KnownRepr BaseTypeRepr bt => KnownRepr TypeRepr (BaseToType bt :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (BaseToType bt) #
KnownRepr FloatInfoRepr flt => KnownRepr TypeRepr (FloatType flt :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (FloatType flt) #
KnownRepr FloatPrecisionRepr ps => KnownRepr TypeRepr (IEEEFloatType ps :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (IEEEFloatType ps) #
KnownRepr TypeRepr tp => KnownRepr TypeRepr (MaybeType tp :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (MaybeType tp) #
KnownRepr TypeRepr a => KnownRepr TypeRepr (ReferenceType a :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (ReferenceType a) #
KnownRepr TypeRepr tp => KnownRepr TypeRepr (SequenceType tp :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (SequenceType tp) #
KnownRepr TypeRepr tp => KnownRepr TypeRepr (StringMapType tp :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (StringMapType tp) #
KnownCtx TypeRepr ctx => KnownRepr TypeRepr (StructType ctx :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (StructType ctx) #
KnownCtx TypeRepr ctx => KnownRepr TypeRepr (VariantType ctx :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (VariantType ctx) #
KnownRepr TypeRepr tp => KnownRepr TypeRepr (VectorType tp :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (VectorType tp) #
(KnownCtx TypeRepr ctx, KnownRepr TypeRepr ret) => KnownRepr TypeRepr (FunctionHandleType ctx ret :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (FunctionHandleType ctx ret) #
(KnownSymbol s, KnownCtx TypeRepr ctx) => KnownRepr TypeRepr (IntrinsicType s ctx :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (IntrinsicType s ctx) #
(KnownSymbol s, KnownCtx TypeRepr ctx, IsRecursiveType s) => KnownRepr TypeRepr (RecursiveType s ctx :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (RecursiveType s ctx) #
(1 <= w, KnownNat w, KnownRepr BaseTypeRepr tp) => KnownRepr TypeRepr (WordMapType w tp :: CrucibleType) Source #
Instance details Defined in Lang.Crucible.Types Methods knownRepr :: TypeRepr (WordMapType w tp) #
Show (TypeRepr tp) Source #
Instance details Defined in Lang.Crucible.Types Methods showsPrec :: Int -> TypeRepr tp -> ShowS # show :: TypeRepr tp -> String # showList :: [TypeRepr tp] -> ShowS #
Eq (TypeRepr tp) Source #
Instance details Defined in Lang.Crucible.Types Methods (==) :: TypeRepr tp -> TypeRepr tp -> Bool # (/=) :: TypeRepr tp -> TypeRepr tp -> Bool #
Hashable (TypeRepr ty) Source #
Instance details Defined in Lang.Crucible.Types Methods hashWithSalt :: Int -> TypeRepr ty -> Int # hash :: TypeRepr ty -> Int #
Pretty (TypeRepr tp) Source #	Pretty-print a type. Based on `ppTypeRepr`, using `ppIntrinsicDefault`.
Instance details Defined in Lang.Crucible.Types Methods pretty :: TypeRepr tp -> Doc ann # prettyList :: [TypeRepr tp] -> Doc ann #

Re-exports

module Data.Parameterized.Ctx

module Data.Parameterized.NatRepr

module Data.Parameterized.SymbolRepr

module What4.BaseTypes

module What4.InterpretedFloatingPoint