Copyright	(c) Galois Inc 2014
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Stability	provisional
Safe Haskell	Safe-Inferred
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 = BaseToType (BaseStructType flds)
type ComplexRealType = BaseToType BaseComplexType
type BVType w = BaseToType (BaseBVType w)
type FloatType = 'FloatType
type IEEEFloatType p = BaseToType (BaseFloatType p)
type CharType = 'CharType
type StringType si = BaseToType (BaseStringType si)
type FunctionHandleType = 'FunctionHandleType
type MaybeType = 'MaybeType
type RecursiveType = 'RecursiveType
type IntrinsicType ctx = '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 xs = BaseToType (BaseArrayType idx xs)
class IsRecursiveType (nm :: Symbol) where
- type UnrollType nm (ctx :: Ctx CrucibleType) :: CrucibleType
- unrollType :: SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
type BaseToType = 'BaseToType
baseToType :: BaseTypeRepr bt -> TypeRepr (BaseToType bt)
data AsBaseType tp where
- AsBaseType :: tp ~ BaseToType bt => BaseTypeRepr bt -> AsBaseType tp
- NotBaseType :: AsBaseType tp
asBaseType :: TypeRepr tp -> AsBaseType tp
type CtxRepr = Assignment TypeRepr
pattern KnownBV :: forall n. (1 <= n, KnownNat n) => TypeRepr (BVType n)
data TypeRepr (tp :: CrucibleType) where
- AnyRepr :: TypeRepr AnyType
- UnitRepr :: TypeRepr UnitType
- BoolRepr :: TypeRepr BoolType
- NatRepr :: TypeRepr NatType
- IntegerRepr :: TypeRepr IntegerType
- RealValRepr :: TypeRepr RealValType
- ComplexRealRepr :: TypeRepr ComplexRealType
- BVRepr :: 1 <= n => !(NatRepr n) -> TypeRepr (BVType n)
- IntrinsicRepr :: !(SymbolRepr nm) -> !(CtxRepr ctx) -> TypeRepr (IntrinsicType nm ctx)
- RecursiveRepr :: IsRecursiveType nm => SymbolRepr nm -> CtxRepr ctx -> TypeRepr (RecursiveType nm ctx)
- FloatRepr :: !(FloatInfoRepr flt) -> TypeRepr (FloatType flt)
- IEEEFloatRepr :: !(FloatPrecisionRepr ps) -> TypeRepr (IEEEFloatType ps)
- CharRepr :: TypeRepr CharType
- StringRepr :: StringInfoRepr si -> TypeRepr (StringType si)
- FunctionHandleRepr :: !(CtxRepr ctx) -> !(TypeRepr ret) -> TypeRepr (FunctionHandleType ctx ret)
- MaybeRepr :: !(TypeRepr tp) -> TypeRepr (MaybeType tp)
- SequenceRepr :: !(TypeRepr tp) -> TypeRepr (SequenceType tp)
- VectorRepr :: !(TypeRepr tp) -> TypeRepr (VectorType tp)
- StructRepr :: !(CtxRepr ctx) -> TypeRepr (StructType ctx)
- VariantRepr :: !(CtxRepr ctx) -> TypeRepr (VariantType ctx)
- ReferenceRepr :: !(TypeRepr a) -> TypeRepr (ReferenceType a)
- WordMapRepr :: 1 <= n => !(NatRepr n) -> !(BaseTypeRepr tp) -> TypeRepr (WordMapType n tp)
- StringMapRepr :: !(TypeRepr tp) -> TypeRepr (StringMapType tp)
- SymbolicArrayRepr :: !(Assignment BaseTypeRepr (idx ::> tp)) -> !(BaseTypeRepr t) -> TypeRepr (SymbolicArrayType (idx ::> tp) t)
- SymbolicStructRepr :: Assignment BaseTypeRepr ctx -> TypeRepr (SymbolicStructType ctx)
module Data.Parameterized.Ctx
module Data.Parameterized.NatRepr
module Data.Parameterized.SymbolRepr
module What4.BaseTypes
data FloatInfo
type HalfFloat = 'HalfFloat
type SingleFloat = 'SingleFloat
type DoubleFloat = 'DoubleFloat
type QuadFloat = 'QuadFloat
type X86_80Float = 'X86_80Float
type DoubleDoubleFloat = 'DoubleDoubleFloat
data FloatInfoRepr (fi :: FloatInfo) where
- HalfFloatRepr :: FloatInfoRepr 'HalfFloat
- SingleFloatRepr :: FloatInfoRepr 'SingleFloat
- DoubleFloatRepr :: FloatInfoRepr 'DoubleFloat
- QuadFloatRepr :: FloatInfoRepr 'QuadFloat
- X86_80FloatRepr :: FloatInfoRepr 'X86_80Float
- DoubleDoubleFloatRepr :: FloatInfoRepr 'DoubleDoubleFloat
type family FloatInfoToBitWidth (fi :: FloatInfo) :: Nat where ...
floatInfoToBVTypeRepr :: forall (fi :: FloatInfo). FloatInfoRepr fi -> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))

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 :: k) (b :: k). GlobalVar a -> GlobalVar b -> Maybe (a :~: b) #
TestEquality RefCell Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods testEquality :: forall (a :: k) (b :: k). RefCell a -> RefCell b -> Maybe (a :~: b) #
TestEquality TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods testEquality :: forall (a :: k) (b :: k). TypeRepr a -> TypeRepr b -> Maybe (a :~: b) #
PrettyApp EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods ppApp :: (forall (x :: k). f x -> Doc ann) -> forall (x :: k). EmptyExprExtension f x -> Doc ann Source #
PrettyApp EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods ppApp :: (forall (x :: k). f x -> Doc ann) -> forall (x :: k). EmptyStmtExtension f x -> Doc ann Source #
HashableF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods hashWithSaltF :: forall (tp :: k). Int -> TypeRepr tp -> Int # hashF :: forall (tp :: k). TypeRepr tp -> Int #
OrdF GlobalVar Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods compareF :: forall (x :: k) (y :: k). GlobalVar x -> GlobalVar y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). GlobalVar x -> GlobalVar y -> Bool # ltF :: forall (x :: k) (y :: k). GlobalVar x -> GlobalVar y -> Bool # geqF :: forall (x :: k) (y :: k). GlobalVar x -> GlobalVar y -> Bool # gtF :: forall (x :: k) (y :: k). GlobalVar x -> GlobalVar y -> Bool #
OrdF RefCell Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods compareF :: forall (x :: k) (y :: k). RefCell x -> RefCell y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). RefCell x -> RefCell y -> Bool # ltF :: forall (x :: k) (y :: k). RefCell x -> RefCell y -> Bool # geqF :: forall (x :: k) (y :: k). RefCell x -> RefCell y -> Bool # gtF :: forall (x :: k) (y :: k). RefCell x -> RefCell y -> Bool #
OrdF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods compareF :: forall (x :: k) (y :: k). TypeRepr x -> TypeRepr y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). TypeRepr x -> TypeRepr y -> Bool # ltF :: forall (x :: k) (y :: k). TypeRepr x -> TypeRepr y -> Bool # geqF :: forall (x :: k) (y :: k). TypeRepr x -> TypeRepr y -> Bool # gtF :: forall (x :: k) (y :: k). TypeRepr x -> TypeRepr y -> Bool #
ShowF GlobalVar Source #
Instance details Defined in Lang.Crucible.CFG.Common Methods withShow :: forall p q (tp :: k) a. p GlobalVar -> q tp -> (Show (GlobalVar tp) => a) -> a # showF :: forall (tp :: k). GlobalVar tp -> String # showsPrecF :: forall (tp :: k). Int -> GlobalVar tp -> String -> String #
ShowF RefCell Source #
Instance details Defined in Lang.Crucible.FunctionHandle Methods withShow :: forall p q (tp :: k) a. p RefCell -> q tp -> (Show (RefCell tp) => a) -> a # showF :: forall (tp :: k). RefCell tp -> String # showsPrecF :: forall (tp :: k). Int -> RefCell tp -> String -> String #
ShowF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods withShow :: forall p q (tp :: k) a. p TypeRepr -> q tp -> (Show (TypeRepr tp) => a) -> a # showF :: forall (tp :: k). TypeRepr tp -> String # showsPrecF :: forall (tp :: k). 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 k) (ctx' :: Ctx k) (v :: k'). 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 k) (ctx' :: Ctx k) (v :: k'). 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 :: k). f x -> m) -> forall (x :: l). EmptyExprExtension f x -> m # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> EmptyExprExtension f x -> b # foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> EmptyExprExtension f x -> b # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> EmptyExprExtension f x -> b # foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> EmptyExprExtension f x -> b # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). EmptyExprExtension f x -> [a] #
FoldableFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). EmptyStmtExtension f x -> m # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> EmptyStmtExtension f x -> b # foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> EmptyStmtExtension f x -> b # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> EmptyStmtExtension f x -> b # foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> EmptyStmtExtension f x -> b # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). EmptyStmtExtension f x -> [a] #
FoldableFC BaseTerm Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods foldMapFC :: forall f m. Monoid m => (forall (x :: k). f x -> m) -> forall (x :: l). BaseTerm f x -> m # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> BaseTerm f x -> b # foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> BaseTerm f x -> b # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> BaseTerm f x -> b # foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> BaseTerm f x -> b # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). BaseTerm f x -> [a] #
FunctorFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). EmptyExprExtension f x -> EmptyExprExtension g x #
FunctorFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). EmptyStmtExtension f x -> EmptyStmtExtension g x #
FunctorFC BaseTerm Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods fmapFC :: (forall (x :: k). f x -> g x) -> forall (x :: l). BaseTerm f x -> BaseTerm g x #
HashableFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods hashWithSaltFC :: (forall (x :: k). Int -> f x -> Int) -> forall (x :: l). Int -> EmptyExprExtension f x -> Int #
HashableFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods hashWithSaltFC :: (forall (x :: k). Int -> f x -> Int) -> forall (x :: l). Int -> EmptyStmtExtension f x -> Int #
OrdFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). EmptyExprExtension f x -> EmptyExprExtension f y -> OrderingF x y #
OrdFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). EmptyStmtExtension f x -> EmptyStmtExtension f y -> OrderingF x y #
OrdFC BaseTerm Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods compareFC :: (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). BaseTerm f x -> BaseTerm f y -> OrderingF x y #
ShowFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods showFC :: (forall (x :: k). f x -> String) -> forall (x :: l). EmptyExprExtension f x -> String # showsPrecFC :: (forall (x :: k). Int -> f x -> ShowS) -> forall (x :: l). Int -> EmptyExprExtension f x -> ShowS #
ShowFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods showFC :: (forall (x :: k). f x -> String) -> forall (x :: l). EmptyStmtExtension f x -> String # showsPrecFC :: (forall (x :: k). Int -> f x -> ShowS) -> forall (x :: l). Int -> EmptyStmtExtension f x -> ShowS #
TestEqualityFC EmptyExprExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). EmptyExprExtension f x -> EmptyExprExtension f y -> Maybe (x :~: y) #
TestEqualityFC EmptyStmtExtension Source #
Instance details Defined in Lang.Crucible.CFG.Extension Methods testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). EmptyStmtExtension f x -> EmptyStmtExtension f y -> Maybe (x :~: y) #
TestEqualityFC BaseTerm Source #
Instance details Defined in Lang.Crucible.CFG.Expr Methods testEqualityFC :: (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). 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 :: k). f x -> m (g x)) -> forall (x :: l). 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 :: k). f x -> m (g x)) -> forall (x :: l). 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 :: k). f x -> m (g x)) -> forall (x :: l). 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 k) (ctx' :: Ctx k) (v :: k'). 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 k) (ctx' :: Ctx k) (v :: k'). 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 k) (ctx' :: Ctx k) (v :: k'). 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 k) (ctx' :: Ctx k) (v :: k'). 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 :: k). f x -> m) -> forall (x :: l). App ext f x -> m # foldrFC :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> App ext f x -> b # foldlFC :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> App ext f x -> b # foldrFC' :: (forall (x :: k). f x -> b -> b) -> forall (x :: l). b -> App ext f x -> b # foldlFC' :: forall f b. (forall (x :: k). b -> f x -> b) -> forall (x :: l). b -> App ext f x -> b # toListFC :: (forall (x :: k). f x -> a) -> forall (x :: l). 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 :: k). f x -> g x) -> forall (x :: l). 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 :: k) (y :: k). f x -> f y -> OrderingF x y) -> forall (x :: l) (y :: l). 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 :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> forall (x :: l) (y :: l). 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 :: k). f x -> m (g x)) -> forall (x :: l). 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 :: k) (b :: k). 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 :: k) (b :: k). 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 :: k) (b :: k). 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 :: k) (b :: k). 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 :: k) (b :: k). 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 :: k). f x -> Doc ann) -> forall (x :: k). 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 :: k) (y :: k). Reg ctx x -> Reg ctx y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). Reg ctx x -> Reg ctx y -> Bool # ltF :: forall (x :: k) (y :: k). Reg ctx x -> Reg ctx y -> Bool # geqF :: forall (x :: k) (y :: k). Reg ctx x -> Reg ctx y -> Bool # gtF :: forall (x :: k) (y :: k). 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 :: k) (y :: k). Atom s x -> Atom s y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). Atom s x -> Atom s y -> Bool # ltF :: forall (x :: k) (y :: k). Atom s x -> Atom s y -> Bool # geqF :: forall (x :: k) (y :: k). Atom s x -> Atom s y -> Bool # gtF :: forall (x :: k) (y :: k). 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 :: k) (y :: k). LambdaLabel s x -> LambdaLabel s y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). LambdaLabel s x -> LambdaLabel s y -> Bool # ltF :: forall (x :: k) (y :: k). LambdaLabel s x -> LambdaLabel s y -> Bool # geqF :: forall (x :: k) (y :: k). LambdaLabel s x -> LambdaLabel s y -> Bool # gtF :: forall (x :: k) (y :: k). 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 :: k) (y :: k). Reg s x -> Reg s y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). Reg s x -> Reg s y -> Bool # ltF :: forall (x :: k) (y :: k). Reg s x -> Reg s y -> Bool # geqF :: forall (x :: k) (y :: k). Reg s x -> Reg s y -> Bool # gtF :: forall (x :: k) (y :: k). 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 :: k) (y :: k). Value s x -> Value s y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). Value s x -> Value s y -> Bool # ltF :: forall (x :: k) (y :: k). Value s x -> Value s y -> Bool # geqF :: forall (x :: k) (y :: k). Value s x -> Value s y -> Bool # gtF :: forall (x :: k) (y :: k). 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 :: k) a. p (Pointed dom) -> q tp -> (Show (Pointed dom tp) => a) -> a # showF :: forall (tp :: k). Pointed dom tp -> String # showsPrecF :: forall (tp :: k). 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 :: k) a. p (Reg ctx) -> q tp -> (Show (Reg ctx tp) => a) -> a # showF :: forall (tp :: k). Reg ctx tp -> String # showsPrecF :: forall (tp :: k). 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 :: k) a. p (Reg s) -> q tp -> (Show (Reg s tp) => a) -> a # showF :: forall (tp :: k). Reg s tp -> String # showsPrecF :: forall (tp :: k). 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 :: k) a. p (Value s) -> q tp -> (Show (Value s tp) => a) -> a # showF :: forall (tp :: k). Value s tp -> String # showsPrecF :: forall (tp :: k). 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 k) (ctx' :: Ctx k). 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 k) (ctx' :: Ctx k). 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 :: k) (b :: k). 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 :: k) (y :: k). App ext f x -> App ext f y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). App ext f x -> App ext f y -> Bool # ltF :: forall (x :: k) (y :: k). App ext f x -> App ext f y -> Bool # geqF :: forall (x :: k) (y :: k). App ext f x -> App ext f y -> Bool # gtF :: forall (x :: k) (y :: k). 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 :: k) a. p (Expr ext s) -> q tp -> (Show (Expr ext s tp) => a) -> a # showF :: forall (tp :: k). Expr ext s tp -> String # showsPrecF :: forall (tp :: k). 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 k) (ctx' :: Ctx k). 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 k) (ctx' :: Ctx k). 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 k) (ctx' :: Ctx k). 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 :: k) (b :: k). 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 :: k) (b :: k). 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 :: k) (y :: k). BlockID blocks x -> BlockID blocks y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). BlockID blocks x -> BlockID blocks y -> Bool # ltF :: forall (x :: k) (y :: k). BlockID blocks x -> BlockID blocks y -> Bool # geqF :: forall (x :: k) (y :: k). BlockID blocks x -> BlockID blocks y -> Bool # gtF :: forall (x :: k) (y :: k). 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 :: k) a. p (BlockID blocks) -> q tp -> (Show (BlockID blocks tp) => a) -> a # showF :: forall (tp :: k). BlockID blocks tp -> String # showsPrecF :: forall (tp :: k). 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 :: k) a. p (PointAbstraction blocks dom) -> q tp -> (Show (PointAbstraction blocks dom tp) => a) -> a # showF :: forall (tp :: k). PointAbstraction blocks dom tp -> String # showsPrecF :: forall (tp :: k). 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 :: k) a. p (Block ext blocks ret) -> q tp -> (Show (Block ext blocks ret tp) => a) -> a # showF :: forall (tp :: k). Block ext blocks ret tp -> String # showsPrecF :: forall (tp :: k). 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 Source #

Arguments

= BaseToType (BaseStructType flds)

:: Ctx BaseType -> CrucibleType.

type ComplexRealType Source #

Arguments

= BaseToType BaseComplexType

:: CrucibleType.

type BVType w 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 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 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 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 xs 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 (ctx :: Ctx CrucibleType) :: CrucibleType Source #

Methods

unrollType :: SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx) Source #

Base type injection

type BaseToType Source #

Arguments

= 'BaseToType

:: BaseType -> CrucibleType.

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

data AsBaseType tp where Source #

Constructors

AsBaseType :: tp ~ BaseToType bt => BaseTypeRepr bt -> AsBaseType tp
NotBaseType :: AsBaseType tp

asBaseType :: TypeRepr tp -> AsBaseType tp Source #

Other stuff

type CtxRepr = Assignment TypeRepr Source #

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

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

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 BoolType
NatRepr :: TypeRepr NatType
IntegerRepr :: TypeRepr IntegerType
RealValRepr :: TypeRepr RealValType
ComplexRealRepr :: TypeRepr ComplexRealType
BVRepr :: 1 <= n => !(NatRepr n) -> TypeRepr (BVType n)
IntrinsicRepr :: !(SymbolRepr nm) -> !(CtxRepr ctx) -> TypeRepr (IntrinsicType nm ctx)
RecursiveRepr :: IsRecursiveType nm => SymbolRepr nm -> CtxRepr ctx -> TypeRepr (RecursiveType nm ctx)
FloatRepr :: !(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 :: !(FloatPrecisionRepr ps) -> TypeRepr (IEEEFloatType ps)	This is a float with user-definable mantissa and exponent that maps directly to the what4 base type.
CharRepr :: TypeRepr CharType
StringRepr :: StringInfoRepr si -> TypeRepr (StringType si)
FunctionHandleRepr :: !(CtxRepr ctx) -> !(TypeRepr ret) -> TypeRepr (FunctionHandleType ctx ret)
MaybeRepr :: !(TypeRepr tp) -> TypeRepr (MaybeType tp)
SequenceRepr :: !(TypeRepr tp) -> TypeRepr (SequenceType tp)
VectorRepr :: !(TypeRepr tp) -> TypeRepr (VectorType tp)
StructRepr :: !(CtxRepr ctx) -> TypeRepr (StructType ctx)
VariantRepr :: !(CtxRepr ctx) -> TypeRepr (VariantType ctx)
ReferenceRepr :: !(TypeRepr a) -> TypeRepr (ReferenceType a)
WordMapRepr :: 1 <= n => !(NatRepr n) -> !(BaseTypeRepr tp) -> TypeRepr (WordMapType n tp)
StringMapRepr :: !(TypeRepr tp) -> TypeRepr (StringMapType tp)
SymbolicArrayRepr :: !(Assignment BaseTypeRepr (idx ::> tp)) -> !(BaseTypeRepr t) -> TypeRepr (SymbolicArrayType (idx ::> tp) t)
SymbolicStructRepr :: Assignment BaseTypeRepr ctx -> TypeRepr (SymbolicStructType ctx)

Instances

Instances details

TestEquality TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods testEquality :: forall (a :: k) (b :: k). TypeRepr a -> TypeRepr b -> Maybe (a :~: b) #
HashableF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods hashWithSaltF :: forall (tp :: k). Int -> TypeRepr tp -> Int # hashF :: forall (tp :: k). TypeRepr tp -> Int #
OrdF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods compareF :: forall (x :: k) (y :: k). TypeRepr x -> TypeRepr y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). TypeRepr x -> TypeRepr y -> Bool # ltF :: forall (x :: k) (y :: k). TypeRepr x -> TypeRepr y -> Bool # geqF :: forall (x :: k) (y :: k). TypeRepr x -> TypeRepr y -> Bool # gtF :: forall (x :: k) (y :: k). TypeRepr x -> TypeRepr y -> Bool #
ShowF TypeRepr Source #
Instance details Defined in Lang.Crucible.Types Methods withShow :: forall p q (tp :: k) a. p TypeRepr -> q tp -> (Show (TypeRepr tp) => a) -> a # showF :: forall (tp :: k). TypeRepr tp -> String # showsPrecF :: forall (tp :: k). 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 #
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

data FloatInfo #

This data kind describes the types of floating-point formats. This consist of the standard IEEE 754-2008 binary floating point formats, as well as the X86 extended 80-bit format and the double-double format.

Instances

Instances details

TestEquality FloatInfoRepr
Instance details Defined in What4.InterpretedFloatingPoint Methods testEquality :: forall (a :: k) (b :: k). FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b) #
HashableF FloatInfoRepr
Instance details Defined in What4.InterpretedFloatingPoint Methods hashWithSaltF :: forall (tp :: k). Int -> FloatInfoRepr tp -> Int # hashF :: forall (tp :: k). FloatInfoRepr tp -> Int #
OrdF FloatInfoRepr
Instance details Defined in What4.InterpretedFloatingPoint Methods compareF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool # ltF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool # geqF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool # gtF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool #
ShowF FloatInfoRepr
Instance details Defined in What4.InterpretedFloatingPoint Methods withShow :: forall p q (tp :: k) a. p FloatInfoRepr -> q tp -> (Show (FloatInfoRepr tp) => a) -> a # showF :: forall (tp :: k). FloatInfoRepr tp -> String # showsPrecF :: forall (tp :: k). Int -> FloatInfoRepr tp -> String -> String #
KnownRepr FloatInfoRepr DoubleDoubleFloat
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleDoubleFloat #
KnownRepr FloatInfoRepr DoubleFloat
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleFloat #
KnownRepr FloatInfoRepr HalfFloat
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr HalfFloat #
KnownRepr FloatInfoRepr QuadFloat
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr QuadFloat #
KnownRepr FloatInfoRepr SingleFloat
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr SingleFloat #
KnownRepr FloatInfoRepr X86_80Float
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr X86_80Float #

type HalfFloat #

Arguments

= 'HalfFloat

16 bit binary IEEE754.

type SingleFloat #

Arguments

= 'SingleFloat

32 bit binary IEEE754.

type DoubleFloat #

Arguments

= 'DoubleFloat

64 bit binary IEEE754.

type QuadFloat #

Arguments

= 'QuadFloat

128 bit binary IEEE754.

type X86_80Float #

Arguments

= 'X86_80Float

X86 80-bit extended floats.

type DoubleDoubleFloat #

Arguments

= 'DoubleDoubleFloat

Two 64-bit floats fused in the "double-double" style.

data FloatInfoRepr (fi :: FloatInfo) where #

A family of value-level representatives for floating-point types.

Constructors

HalfFloatRepr :: FloatInfoRepr 'HalfFloat
SingleFloatRepr :: FloatInfoRepr 'SingleFloat
DoubleFloatRepr :: FloatInfoRepr 'DoubleFloat
QuadFloatRepr :: FloatInfoRepr 'QuadFloat
X86_80FloatRepr :: FloatInfoRepr 'X86_80Float
DoubleDoubleFloatRepr :: FloatInfoRepr 'DoubleDoubleFloat

Instances

Instances details

TestEquality FloatInfoRepr
Instance details Defined in What4.InterpretedFloatingPoint Methods testEquality :: forall (a :: k) (b :: k). FloatInfoRepr a -> FloatInfoRepr b -> Maybe (a :~: b) #
HashableF FloatInfoRepr
Instance details Defined in What4.InterpretedFloatingPoint Methods hashWithSaltF :: forall (tp :: k). Int -> FloatInfoRepr tp -> Int # hashF :: forall (tp :: k). FloatInfoRepr tp -> Int #
OrdF FloatInfoRepr
Instance details Defined in What4.InterpretedFloatingPoint Methods compareF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool # ltF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool # geqF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool # gtF :: forall (x :: k) (y :: k). FloatInfoRepr x -> FloatInfoRepr y -> Bool #
ShowF FloatInfoRepr
Instance details Defined in What4.InterpretedFloatingPoint Methods withShow :: forall p q (tp :: k) a. p FloatInfoRepr -> q tp -> (Show (FloatInfoRepr tp) => a) -> a # showF :: forall (tp :: k). FloatInfoRepr tp -> String # showsPrecF :: forall (tp :: k). Int -> FloatInfoRepr tp -> String -> String #
KnownRepr FloatInfoRepr DoubleDoubleFloat
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleDoubleFloat #
KnownRepr FloatInfoRepr DoubleFloat
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr DoubleFloat #
KnownRepr FloatInfoRepr HalfFloat
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr HalfFloat #
KnownRepr FloatInfoRepr QuadFloat
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr QuadFloat #
KnownRepr FloatInfoRepr SingleFloat
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr SingleFloat #
KnownRepr FloatInfoRepr X86_80Float
Instance details Defined in What4.InterpretedFloatingPoint Methods knownRepr :: FloatInfoRepr X86_80Float #
Show (FloatInfoRepr fi)
Instance details Defined in What4.InterpretedFloatingPoint Methods showsPrec :: Int -> FloatInfoRepr fi -> ShowS # show :: FloatInfoRepr fi -> String # showList :: [FloatInfoRepr fi] -> ShowS #
Eq (FloatInfoRepr fi)
Instance details Defined in What4.InterpretedFloatingPoint Methods (==) :: FloatInfoRepr fi -> FloatInfoRepr fi -> Bool # (/=) :: FloatInfoRepr fi -> FloatInfoRepr fi -> Bool #
Hashable (FloatInfoRepr fi)
Instance details Defined in What4.InterpretedFloatingPoint Methods hashWithSalt :: Int -> FloatInfoRepr fi -> Int # hash :: FloatInfoRepr fi -> Int #
Pretty (FloatInfoRepr fi)
Instance details Defined in What4.InterpretedFloatingPoint Methods pretty :: FloatInfoRepr fi -> Doc ann # prettyList :: [FloatInfoRepr fi] -> Doc ann #

type family FloatInfoToBitWidth (fi :: FloatInfo) :: Nat where ... #

Equations

FloatInfoToBitWidth HalfFloat = 16
FloatInfoToBitWidth SingleFloat = 32
FloatInfoToBitWidth DoubleFloat = 64
FloatInfoToBitWidth X86_80Float = 80
FloatInfoToBitWidth QuadFloat = 128
FloatInfoToBitWidth DoubleDoubleFloat = 128

floatInfoToBVTypeRepr :: forall (fi :: FloatInfo). FloatInfoRepr fi -> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi)) #