Copyright	(c) Galois Inc 2015
Maintainer	Joe Hendrix <jhendrix@galois.com>
Safe Haskell	None
Language	Haskell2010

Data.Macaw.Types

Description

The type of machine words, including bit vectors and floating point

Synopsis

data Type
- = BVType Nat
- | FloatType FloatInfo
- | BoolType
- | TupleType [Type]
- | VecType Nat Type
data FloatInfoRepr (fi :: FloatInfo) where
- HalfFloatRepr :: FloatInfoRepr 'HalfFloat
- SingleFloatRepr :: FloatInfoRepr 'SingleFloat
- DoubleFloatRepr :: FloatInfoRepr 'DoubleFloat
- QuadFloatRepr :: FloatInfoRepr 'QuadFloat
- X86_80FloatRepr :: FloatInfoRepr 'X86_80Float
n0 :: NatRepr 0
n1 :: NatRepr 1
n64 :: NatRepr 64
type BoolType = 'BoolType
type FloatType = 'FloatType
n4 :: NatRepr 4
n8 :: NatRepr 8
n16 :: NatRepr 16
n32 :: NatRepr 32
n80 :: NatRepr 80
n128 :: NatRepr 128
n256 :: NatRepr 256
n512 :: NatRepr 512
data FloatInfo
- = HalfFloat
- | SingleFloat
- | DoubleFloat
- | QuadFloat
- | X86_80Float
type HalfFloat = 'HalfFloat
type SingleFloat = 'SingleFloat
type DoubleFloat = 'DoubleFloat
type QuadFloat = 'QuadFloat
type X86_80Float = 'X86_80Float
type family FloatInfoBytes (fi :: FloatInfo) :: Nat where ...
floatInfoBytes :: forall (fi :: FloatInfo). FloatInfoRepr fi -> NatRepr (FloatInfoBytes fi)
floatInfoBytesIsPos :: forall (fi :: FloatInfo). FloatInfoRepr fi -> LeqProof 1 (FloatInfoBytes fi)
type FloatInfoBits (fi :: FloatInfo) = 8 * FloatInfoBytes fi
floatInfoBits :: forall (fi :: FloatInfo). FloatInfoRepr fi -> NatRepr (FloatInfoBits fi)
floatInfoBitsIsPos :: forall (fi :: FloatInfo). FloatInfoRepr fi -> LeqProof 1 (FloatInfoBits fi)
type BVType = 'BVType
type TupleType = 'TupleType
type VecType = 'VecType
type family TypeBytes (tp :: Type) :: Nat where ...
type family TypeBits (tp :: Type) :: Nat where ...
type FloatBVType (fi :: FloatInfo) = BVType (FloatInfoBits fi)
data TypeRepr (tp :: Type) where
- BoolTypeRepr :: TypeRepr 'BoolType
- BVTypeRepr :: forall (n :: Natural). 1 <= n => !(NatRepr n) -> TypeRepr ('BVType n)
- FloatTypeRepr :: forall (fi :: FloatInfo). !(FloatInfoRepr fi) -> TypeRepr ('FloatType fi)
- TupleTypeRepr :: forall (ctx :: [Type]). !(List TypeRepr ctx) -> TypeRepr ('TupleType ctx)
- VecTypeRepr :: forall (n :: Nat) (tp1 :: Type). NatRepr n -> TypeRepr tp1 -> TypeRepr ('VecType n tp1)
type_width :: forall (n :: Nat). TypeRepr (BVType n) -> NatRepr n
floatBVTypeRepr :: forall (fi :: FloatInfo). FloatInfoRepr fi -> TypeRepr (FloatBVType fi)
class HasRepr (f :: k -> Type) (v :: k -> Type) | f -> v where
- typeRepr :: forall (tp :: k). f tp -> v tp
typeWidth :: forall f (w :: Nat). HasRepr f TypeRepr => f (BVType w) -> NatRepr w
class KnownNat (n :: Nat)
type Nat = Natural
data NatRepr (n :: Nat)
knownNat :: forall (n :: Nat). KnownNat n => NatRepr n

Documentation

data Type Source #

Constructors

BVType Nat	A bitvector with the given number of bits.
FloatType FloatInfo	A floating point in the given format.
BoolType	A Boolean value
TupleType [Type]	A tuple of types
VecType Nat Type	A vector of types

Instances

Instances details

TestEquality MemRepr Source #
Instance details Defined in Data.Macaw.CFG.AssignRhs Methods testEquality :: forall (a :: Type) (b :: Type). MemRepr a -> MemRepr b -> Maybe (a :~: b) #
TestEquality TypeRepr Source #
Instance details Defined in Data.Macaw.Types Methods testEquality :: forall (a :: Type) (b :: Type). TypeRepr a -> TypeRepr b -> Maybe (a :~: b) #
HashableF MemRepr
Instance details Defined in Data.Macaw.CFG.AssignRhs Methods hashWithSaltF :: forall (tp :: Type). Int -> MemRepr tp -> Int hashF :: forall (tp :: Type). MemRepr tp -> Int
OrdF MemRepr
Instance details Defined in Data.Macaw.CFG.AssignRhs Methods compareF :: forall (x :: Type) (y :: Type). MemRepr x -> MemRepr y -> OrderingF x y leqF :: forall (x :: Type) (y :: Type). MemRepr x -> MemRepr y -> Bool ltF :: forall (x :: Type) (y :: Type). MemRepr x -> MemRepr y -> Bool geqF :: forall (x :: Type) (y :: Type). MemRepr x -> MemRepr y -> Bool gtF :: forall (x :: Type) (y :: Type). MemRepr x -> MemRepr y -> Bool
OrdF TypeRepr Source #
Instance details Defined in Data.Macaw.Types Methods compareF :: forall (x :: Type) (y :: Type). TypeRepr x -> TypeRepr y -> OrderingF x y leqF :: forall (x :: Type) (y :: Type). TypeRepr x -> TypeRepr y -> Bool ltF :: forall (x :: Type) (y :: Type). TypeRepr x -> TypeRepr y -> Bool geqF :: forall (x :: Type) (y :: Type). TypeRepr x -> TypeRepr y -> Bool gtF :: forall (x :: Type) (y :: Type). TypeRepr x -> TypeRepr y -> Bool
ShowF TypeRepr Source #
Instance details Defined in Data.Macaw.Types Methods withShow :: forall p q (tp :: Type) a. p TypeRepr -> q tp -> (Show (TypeRepr tp) => a) -> a showF :: forall (tp :: Type). TypeRepr tp -> String showsPrecF :: forall (tp :: Type). Int -> TypeRepr tp -> String -> String
HasRepr MemRepr TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.AssignRhs Methods typeRepr :: forall (tp :: Type). MemRepr tp -> TypeRepr tp Source #
KnownRepr TypeRepr BoolType Source #
Instance details Defined in Data.Macaw.Types Methods knownRepr :: TypeRepr BoolType
FoldableFC App Source #
Instance details Defined in Data.Macaw.CFG.App Methods foldMapFC :: forall f m. Monoid m => (forall (x :: Type). f x -> m) -> forall (x :: Type). App f x -> m # foldrFC :: (forall (x :: Type). f x -> b -> b) -> forall (x :: Type). b -> App f x -> b # foldlFC :: forall f b. (forall (x :: Type). b -> f x -> b) -> forall (x :: Type). b -> App f x -> b # foldrFC' :: (forall (x :: Type). f x -> b -> b) -> forall (x :: Type). b -> App f x -> b # foldlFC' :: forall f b. (forall (x :: Type). b -> f x -> b) -> forall (x :: Type). b -> App f x -> b # toListFC :: (forall (x :: Type). f x -> a) -> forall (x :: Type). App f x -> [a] #
FunctorFC App
Instance details Defined in Data.Macaw.CFG.App Methods fmapFC :: (forall (x :: Type). f x -> g x) -> forall (x :: Type). App f x -> App g x
TraversableFC App
Instance details Defined in Data.Macaw.CFG.App Methods traverseFC :: forall f g m. Applicative m => (forall (x :: Type). f x -> m (g x)) -> forall (x :: Type). App f x -> m (App g x)
(KnownNat n, 1 <= n) => KnownRepr TypeRepr (BVType n :: Type) Source #
Instance details Defined in Data.Macaw.Types Methods knownRepr :: TypeRepr (BVType n)
KnownRepr FloatInfoRepr fi => KnownRepr TypeRepr (FloatType fi :: Type) Source #
Instance details Defined in Data.Macaw.Types Methods knownRepr :: TypeRepr (FloatType fi)
KnownRepr (List TypeRepr) l => KnownRepr TypeRepr (TupleType l :: Type) Source #
Instance details Defined in Data.Macaw.Types Methods knownRepr :: TypeRepr (TupleType l)
FoldableFC (ArchFn arch) => FoldableFC (AssignRhs arch :: (Type -> Type) -> Type -> Type) Source #
Instance details Defined in Data.Macaw.CFG.AssignRhs Methods foldMapFC :: forall f m. Monoid m => (forall (x :: Type). f x -> m) -> forall (x :: Type). AssignRhs arch f x -> m # foldrFC :: (forall (x :: Type). f x -> b -> b) -> forall (x :: Type). b -> AssignRhs arch f x -> b # foldlFC :: forall f b. (forall (x :: Type). b -> f x -> b) -> forall (x :: Type). b -> AssignRhs arch f x -> b # foldrFC' :: (forall (x :: Type). f x -> b -> b) -> forall (x :: Type). b -> AssignRhs arch f x -> b # foldlFC' :: forall f b. (forall (x :: Type). b -> f x -> b) -> forall (x :: Type). b -> AssignRhs arch f x -> b # toListFC :: (forall (x :: Type). f x -> a) -> forall (x :: Type). AssignRhs arch f x -> [a] #
(KnownNat n, KnownRepr TypeRepr r) => KnownRepr TypeRepr (VecType n r :: Type) Source #
Instance details Defined in Data.Macaw.Types Methods knownRepr :: TypeRepr (VecType n r)
TestEquality r => TestEquality (BoundLoc r :: Type -> Type) Source #
Instance details Defined in Data.Macaw.AbsDomain.StackAnalysis Methods testEquality :: forall (a :: Type) (b :: Type). BoundLoc r a -> BoundLoc r b -> Maybe (a :~: b) #
TestEquality (ArchReg arch) => TestEquality (InitInferValue arch :: Type -> Type) Source #
Instance details Defined in Data.Macaw.Analysis.RegisterUse Methods testEquality :: forall (a :: Type) (b :: Type). InitInferValue arch a -> InitInferValue arch b -> Maybe (a :~: b) #
TestEquality (MemSlice wtp :: Type -> Type) Source #
Instance details Defined in Data.Macaw.Analysis.RegisterUse Methods testEquality :: forall (a :: Type) (b :: Type). MemSlice wtp a -> MemSlice wtp b -> Maybe (a :~: b) #
TestEquality f => TestEquality (App f :: Type -> Type) Source #
Instance details Defined in Data.Macaw.CFG.App Methods testEquality :: forall (a :: Type) (b :: Type). App f a -> App f b -> Maybe (a :~: b) #
TestEquality (AssignId ids :: Type -> Type) Source #
Instance details Defined in Data.Macaw.CFG.Core Methods testEquality :: forall (a :: Type) (b :: Type). AssignId ids a -> AssignId ids b -> Maybe (a :~: b) #
TestEquality (CValue arch :: Type -> Type) Source #
Instance details Defined in Data.Macaw.CFG.Core Methods testEquality :: forall (a :: Type) (b :: Type). CValue arch a -> CValue arch b -> Maybe (a :~: b) #
ShowF r => PrettyF (BoundLoc r :: Type -> Type) Source #
Instance details Defined in Data.Macaw.AbsDomain.StackAnalysis Methods prettyF :: forall (tp :: Type) ann. BoundLoc r tp -> Doc ann Source #
EqF (AbsValue w :: Type -> Type)
Instance details Defined in Data.Macaw.AbsDomain.AbsState Methods eqF :: forall (a :: Type). AbsValue w a -> AbsValue w a -> Bool
(HashableF f, TestEquality f) => HashableF (App f :: Type -> Type)
Instance details Defined in Data.Macaw.CFG.App Methods hashWithSaltF :: forall (tp :: Type). Int -> App f tp -> Int hashF :: forall (tp :: Type). App f tp -> Int
HashableF (CValue arch :: Type -> Type)
Instance details Defined in Data.Macaw.CFG.Core Methods hashWithSaltF :: forall (tp :: Type). Int -> CValue arch tp -> Int hashF :: forall (tp :: Type). CValue arch tp -> Int
OrdF r => OrdF (BoundLoc r :: Type -> Type)
Instance details Defined in Data.Macaw.AbsDomain.StackAnalysis Methods compareF :: forall (x :: Type) (y :: Type). BoundLoc r x -> BoundLoc r y -> OrderingF x y leqF :: forall (x :: Type) (y :: Type). BoundLoc r x -> BoundLoc r y -> Bool ltF :: forall (x :: Type) (y :: Type). BoundLoc r x -> BoundLoc r y -> Bool geqF :: forall (x :: Type) (y :: Type). BoundLoc r x -> BoundLoc r y -> Bool gtF :: forall (x :: Type) (y :: Type). BoundLoc r x -> BoundLoc r y -> Bool
OrdF (ArchReg arch) => OrdF (InitInferValue arch :: Type -> Type)
Instance details Defined in Data.Macaw.Analysis.RegisterUse Methods compareF :: forall (x :: Type) (y :: Type). InitInferValue arch x -> InitInferValue arch y -> OrderingF x y leqF :: forall (x :: Type) (y :: Type). InitInferValue arch x -> InitInferValue arch y -> Bool ltF :: forall (x :: Type) (y :: Type). InitInferValue arch x -> InitInferValue arch y -> Bool geqF :: forall (x :: Type) (y :: Type). InitInferValue arch x -> InitInferValue arch y -> Bool gtF :: forall (x :: Type) (y :: Type). InitInferValue arch x -> InitInferValue arch y -> Bool
OrdF (MemSlice wtp :: Type -> Type)
Instance details Defined in Data.Macaw.Analysis.RegisterUse Methods compareF :: forall (x :: Type) (y :: Type). MemSlice wtp x -> MemSlice wtp y -> OrderingF x y leqF :: forall (x :: Type) (y :: Type). MemSlice wtp x -> MemSlice wtp y -> Bool ltF :: forall (x :: Type) (y :: Type). MemSlice wtp x -> MemSlice wtp y -> Bool geqF :: forall (x :: Type) (y :: Type). MemSlice wtp x -> MemSlice wtp y -> Bool gtF :: forall (x :: Type) (y :: Type). MemSlice wtp x -> MemSlice wtp y -> Bool
OrdF f => OrdF (App f :: Type -> Type)
Instance details Defined in Data.Macaw.CFG.App Methods compareF :: forall (x :: Type) (y :: Type). App f x -> App f y -> OrderingF x y leqF :: forall (x :: Type) (y :: Type). App f x -> App f y -> Bool ltF :: forall (x :: Type) (y :: Type). App f x -> App f y -> Bool geqF :: forall (x :: Type) (y :: Type). App f x -> App f y -> Bool gtF :: forall (x :: Type) (y :: Type). App f x -> App f y -> Bool
OrdF (AssignId ids :: Type -> Type)
Instance details Defined in Data.Macaw.CFG.Core Methods compareF :: forall (x :: Type) (y :: Type). AssignId ids x -> AssignId ids y -> OrderingF x y leqF :: forall (x :: Type) (y :: Type). AssignId ids x -> AssignId ids y -> Bool ltF :: forall (x :: Type) (y :: Type). AssignId ids x -> AssignId ids y -> Bool geqF :: forall (x :: Type) (y :: Type). AssignId ids x -> AssignId ids y -> Bool gtF :: forall (x :: Type) (y :: Type). AssignId ids x -> AssignId ids y -> Bool
OrdF (CValue arch :: Type -> Type)
Instance details Defined in Data.Macaw.CFG.Core Methods compareF :: forall (x :: Type) (y :: Type). CValue arch x -> CValue arch y -> OrderingF x y leqF :: forall (x :: Type) (y :: Type). CValue arch x -> CValue arch y -> Bool ltF :: forall (x :: Type) (y :: Type). CValue arch x -> CValue arch y -> Bool geqF :: forall (x :: Type) (y :: Type). CValue arch x -> CValue arch y -> Bool gtF :: forall (x :: Type) (y :: Type). CValue arch x -> CValue arch y -> Bool
ShowF r => ShowF (BoundLoc r :: Type -> Type)
Instance details Defined in Data.Macaw.AbsDomain.StackAnalysis Methods withShow :: forall p q (tp :: Type) a. p (BoundLoc r) -> q tp -> (Show (BoundLoc r tp) => a) -> a showF :: forall (tp :: Type). BoundLoc r tp -> String showsPrecF :: forall (tp :: Type). Int -> BoundLoc r tp -> String -> String
ShowF (ArchReg arch) => ShowF (InitInferValue arch :: Type -> Type)
Instance details Defined in Data.Macaw.Analysis.RegisterUse Methods withShow :: forall p q (tp :: Type) a. p (InitInferValue arch) -> q tp -> (Show (InitInferValue arch tp) => a) -> a showF :: forall (tp :: Type). InitInferValue arch tp -> String showsPrecF :: forall (tp :: Type). Int -> InitInferValue arch tp -> String -> String
ShowF (AssignId ids :: Type -> Type)
Instance details Defined in Data.Macaw.CFG.Core Methods withShow :: forall p q (tp :: Type) a. p (AssignId ids) -> q tp -> (Show (AssignId ids tp) => a) -> a showF :: forall (tp :: Type). AssignId ids tp -> String showsPrecF :: forall (tp :: Type). Int -> AssignId ids tp -> String -> String
HasRepr r TypeRepr => HasRepr (BoundLoc r :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.AbsDomain.StackAnalysis Methods typeRepr :: forall (tp :: Type). BoundLoc r tp -> TypeRepr tp Source #
HasRepr (App f :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.App Methods typeRepr :: forall (tp :: Type). App f tp -> TypeRepr tp Source #
HasRepr (CValue arch :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.Core Methods typeRepr :: forall (tp :: Type). CValue arch tp -> TypeRepr tp Source #
TestEquality (ArchReg arch) => TestEquality (BlockInferValue arch ids :: Type -> Type) Source #
Instance details Defined in Data.Macaw.Analysis.RegisterUse Methods testEquality :: forall (a :: Type) (b :: Type). BlockInferValue arch ids a -> BlockInferValue arch ids b -> Maybe (a :~: b) #
OrdF (ArchReg arch) => TestEquality (Value arch ids :: Type -> Type) Source #
Instance details Defined in Data.Macaw.CFG.Core Methods testEquality :: forall (a :: Type) (b :: Type). Value arch ids a -> Value arch ids b -> Maybe (a :~: b) #
OrdF (ArchReg arch) => EqF (Value arch ids :: Type -> Type)
Instance details Defined in Data.Macaw.CFG.Core Methods eqF :: forall (a :: Type). Value arch ids a -> Value arch ids a -> Bool
OrdF (ArchReg arch) => OrdF (BlockInferValue arch ids :: Type -> Type)
Instance details Defined in Data.Macaw.Analysis.RegisterUse Methods compareF :: forall (x :: Type) (y :: Type). BlockInferValue arch ids x -> BlockInferValue arch ids y -> OrderingF x y leqF :: forall (x :: Type) (y :: Type). BlockInferValue arch ids x -> BlockInferValue arch ids y -> Bool ltF :: forall (x :: Type) (y :: Type). BlockInferValue arch ids x -> BlockInferValue arch ids y -> Bool geqF :: forall (x :: Type) (y :: Type). BlockInferValue arch ids x -> BlockInferValue arch ids y -> Bool gtF :: forall (x :: Type) (y :: Type). BlockInferValue arch ids x -> BlockInferValue arch ids y -> Bool
OrdF (ArchReg arch) => OrdF (Value arch ids :: Type -> Type)
Instance details Defined in Data.Macaw.CFG.Core Methods compareF :: forall (x :: Type) (y :: Type). Value arch ids x -> Value arch ids y -> OrderingF x y leqF :: forall (x :: Type) (y :: Type). Value arch ids x -> Value arch ids y -> Bool ltF :: forall (x :: Type) (y :: Type). Value arch ids x -> Value arch ids y -> Bool geqF :: forall (x :: Type) (y :: Type). Value arch ids x -> Value arch ids y -> Bool gtF :: forall (x :: Type) (y :: Type). Value arch ids x -> Value arch ids y -> Bool
ShowF (ArchReg arch) => ShowF (BlockInferValue arch ids :: Type -> Type)
Instance details Defined in Data.Macaw.Analysis.RegisterUse Methods withShow :: forall p q (tp :: Type) a. p (BlockInferValue arch ids) -> q tp -> (Show (BlockInferValue arch ids tp) => a) -> a showF :: forall (tp :: Type). BlockInferValue arch ids tp -> String showsPrecF :: forall (tp :: Type). Int -> BlockInferValue arch ids tp -> String -> String
HasRepr (AssignRhs arch f :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.AssignRhs Methods typeRepr :: forall (tp :: Type). AssignRhs arch f tp -> TypeRepr tp Source #
HasRepr (ArchReg arch) TypeRepr => HasRepr (Value arch ids :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.Core Methods typeRepr :: forall (tp :: Type). Value arch ids tp -> TypeRepr tp Source #
PrettyRegValue r f => Show (RegState r f) Source #
Instance details Defined in Data.Macaw.CFG.Core Methods showsPrec :: Int -> RegState r f -> ShowS # show :: RegState r f -> String # showList :: [RegState r f] -> ShowS #
PrettyRegValue r f => Pretty (RegState r f)
Instance details Defined in Data.Macaw.CFG.Core Methods pretty :: RegState r f -> Doc ann prettyList :: [RegState r f] -> Doc ann

data FloatInfoRepr (fi :: FloatInfo) where Source #

Constructors

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

Instances

Instances details

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

n0 :: NatRepr 0 Source #

n1 :: NatRepr 1 Source #

n64 :: NatRepr 64 Source #

type BoolType = 'BoolType Source #

type FloatType = 'FloatType Source #

n4 :: NatRepr 4 Source #

n8 :: NatRepr 8 Source #

n16 :: NatRepr 16 Source #

n32 :: NatRepr 32 Source #

n80 :: NatRepr 80 Source #

n128 :: NatRepr 128 Source #

n256 :: NatRepr 256 Source #

n512 :: NatRepr 512 Source #

data FloatInfo Source #

Constructors

HalfFloat	16 bit binary IEE754*
SingleFloat	32 bit binary IEE754
DoubleFloat	64 bit binary IEE754
QuadFloat	128 bit binary IEE754
X86_80Float	X86 80-bit extended floats

Instances

Instances details

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

type HalfFloat = 'HalfFloat Source #

type SingleFloat = 'SingleFloat Source #

type DoubleFloat = 'DoubleFloat Source #

type QuadFloat = 'QuadFloat Source #

type X86_80Float = 'X86_80Float Source #

type family FloatInfoBytes (fi :: FloatInfo) :: Nat where ... Source #

Equations

FloatInfoBytes HalfFloat = 2
FloatInfoBytes SingleFloat = 4
FloatInfoBytes DoubleFloat = 8
FloatInfoBytes QuadFloat = 16
FloatInfoBytes X86_80Float = 10

floatInfoBytes :: forall (fi :: FloatInfo). FloatInfoRepr fi -> NatRepr (FloatInfoBytes fi) Source #

floatInfoBytesIsPos :: forall (fi :: FloatInfo). FloatInfoRepr fi -> LeqProof 1 (FloatInfoBytes fi) Source #

type FloatInfoBits (fi :: FloatInfo) = 8 * FloatInfoBytes fi Source #

floatInfoBits :: forall (fi :: FloatInfo). FloatInfoRepr fi -> NatRepr (FloatInfoBits fi) Source #

floatInfoBitsIsPos :: forall (fi :: FloatInfo). FloatInfoRepr fi -> LeqProof 1 (FloatInfoBits fi) Source #

type BVType = 'BVType Source #

type TupleType = 'TupleType Source #

type VecType = 'VecType Source #

type family TypeBytes (tp :: Type) :: Nat where ... Source #

Equations

TypeBytes (BVType 8) = 1
TypeBytes (BVType 16) = 2
TypeBytes (BVType 32) = 4
TypeBytes (BVType 64) = 8
TypeBytes (FloatType fi) = FloatInfoBytes fi
TypeBytes (VecType n tp) = n * TypeBytes tp

type family TypeBits (tp :: Type) :: Nat where ... Source #

Equations

TypeBits (BVType n) = n
TypeBits (FloatType fi) = 8 * FloatInfoBytes fi

type FloatBVType (fi :: FloatInfo) = BVType (FloatInfoBits fi) Source #

The bitvector associated with the given floating-point format.

data TypeRepr (tp :: Type) where Source #

A runtime representation of Type for case matching purposes.

Constructors

BoolTypeRepr :: TypeRepr 'BoolType
BVTypeRepr :: forall (n :: Natural). 1 <= n => !(NatRepr n) -> TypeRepr ('BVType n)
FloatTypeRepr :: forall (fi :: FloatInfo). !(FloatInfoRepr fi) -> TypeRepr ('FloatType fi)
TupleTypeRepr :: forall (ctx :: [Type]). !(List TypeRepr ctx) -> TypeRepr ('TupleType ctx)
VecTypeRepr :: forall (n :: Nat) (tp1 :: Type). NatRepr n -> TypeRepr tp1 -> TypeRepr ('VecType n tp1)

Instances

Instances details

TestEquality TypeRepr Source #
Instance details Defined in Data.Macaw.Types Methods testEquality :: forall (a :: Type) (b :: Type). TypeRepr a -> TypeRepr b -> Maybe (a :~: b) #
OrdF TypeRepr Source #
Instance details Defined in Data.Macaw.Types Methods compareF :: forall (x :: Type) (y :: Type). TypeRepr x -> TypeRepr y -> OrderingF x y leqF :: forall (x :: Type) (y :: Type). TypeRepr x -> TypeRepr y -> Bool ltF :: forall (x :: Type) (y :: Type). TypeRepr x -> TypeRepr y -> Bool geqF :: forall (x :: Type) (y :: Type). TypeRepr x -> TypeRepr y -> Bool gtF :: forall (x :: Type) (y :: Type). TypeRepr x -> TypeRepr y -> Bool
ShowF TypeRepr Source #
Instance details Defined in Data.Macaw.Types Methods withShow :: forall p q (tp :: Type) a. p TypeRepr -> q tp -> (Show (TypeRepr tp) => a) -> a showF :: forall (tp :: Type). TypeRepr tp -> String showsPrecF :: forall (tp :: Type). Int -> TypeRepr tp -> String -> String
HasRepr MemRepr TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.AssignRhs Methods typeRepr :: forall (tp :: Type). MemRepr tp -> TypeRepr tp Source #
KnownRepr TypeRepr BoolType Source #
Instance details Defined in Data.Macaw.Types Methods knownRepr :: TypeRepr BoolType
(KnownNat n, 1 <= n) => KnownRepr TypeRepr (BVType n :: Type) Source #
Instance details Defined in Data.Macaw.Types Methods knownRepr :: TypeRepr (BVType n)
KnownRepr FloatInfoRepr fi => KnownRepr TypeRepr (FloatType fi :: Type) Source #
Instance details Defined in Data.Macaw.Types Methods knownRepr :: TypeRepr (FloatType fi)
KnownRepr (List TypeRepr) l => KnownRepr TypeRepr (TupleType l :: Type) Source #
Instance details Defined in Data.Macaw.Types Methods knownRepr :: TypeRepr (TupleType l)
(KnownNat n, KnownRepr TypeRepr r) => KnownRepr TypeRepr (VecType n r :: Type) Source #
Instance details Defined in Data.Macaw.Types Methods knownRepr :: TypeRepr (VecType n r)
HasRepr r TypeRepr => HasRepr (BoundLoc r :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.AbsDomain.StackAnalysis Methods typeRepr :: forall (tp :: Type). BoundLoc r tp -> TypeRepr tp Source #
HasRepr (App f :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.App Methods typeRepr :: forall (tp :: Type). App f tp -> TypeRepr tp Source #
HasRepr (CValue arch :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.Core Methods typeRepr :: forall (tp :: Type). CValue arch tp -> TypeRepr tp Source #
HasRepr (AssignRhs arch f :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.AssignRhs Methods typeRepr :: forall (tp :: Type). AssignRhs arch f tp -> TypeRepr tp Source #
HasRepr (ArchReg arch) TypeRepr => HasRepr (Value arch ids :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.Core Methods typeRepr :: forall (tp :: Type). Value arch ids tp -> TypeRepr tp Source #
Show (TypeRepr tp) Source #
Instance details Defined in Data.Macaw.Types Methods showsPrec :: Int -> TypeRepr tp -> ShowS # show :: TypeRepr tp -> String # showList :: [TypeRepr tp] -> ShowS #
Pretty (TypeRepr tp) Source #
Instance details Defined in Data.Macaw.Types Methods pretty :: TypeRepr tp -> Doc ann prettyList :: [TypeRepr tp] -> Doc ann

type_width :: forall (n :: Nat). TypeRepr (BVType n) -> NatRepr n Source #

floatBVTypeRepr :: forall (fi :: FloatInfo). FloatInfoRepr fi -> TypeRepr (FloatBVType fi) Source #

class HasRepr (f :: k -> Type) (v :: k -> Type) | f -> v where Source #

A multi-parameter type class that allows one to represent that a parameterized type value has some representative type such as a TypeRepr.

Methods

typeRepr :: forall (tp :: k). f tp -> v tp Source #

Instances

Instances details

HasRepr MemRepr TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.AssignRhs Methods typeRepr :: forall (tp :: Type). MemRepr tp -> TypeRepr tp Source #
HasRepr r TypeRepr => HasRepr (BoundLoc r :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.AbsDomain.StackAnalysis Methods typeRepr :: forall (tp :: Type). BoundLoc r tp -> TypeRepr tp Source #
HasRepr (App f :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.App Methods typeRepr :: forall (tp :: Type). App f tp -> TypeRepr tp Source #
HasRepr (CValue arch :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.Core Methods typeRepr :: forall (tp :: Type). CValue arch tp -> TypeRepr tp Source #
HasRepr (AssignRhs arch f :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.AssignRhs Methods typeRepr :: forall (tp :: Type). AssignRhs arch f tp -> TypeRepr tp Source #
HasRepr (ArchReg arch) TypeRepr => HasRepr (Value arch ids :: Type -> Type) TypeRepr Source #
Instance details Defined in Data.Macaw.CFG.Core Methods typeRepr :: forall (tp :: Type). Value arch ids tp -> TypeRepr tp Source #

typeWidth :: forall f (w :: Nat). HasRepr f TypeRepr => f (BVType w) -> NatRepr w Source #

class KnownNat (n :: Nat) #

This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.

Since: base-4.7.0.0

Minimal complete definition

natSing

type Nat = Natural #

A type synonym for Natural.

Previously, this was an opaque data type, but it was changed to a type synonym.

Since: base-4.16.0.0

data NatRepr (n :: Nat) #

Instances

Instances details

TestEquality NatRepr
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Maybe (a :~: b) #
HashableF NatRepr
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods hashWithSaltF :: forall (tp :: Nat). Int -> NatRepr tp -> Int hashF :: forall (tp :: Nat). NatRepr tp -> Int
OrdF NatRepr
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods compareF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> OrderingF x y leqF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool ltF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool geqF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool gtF :: forall (x :: Nat) (y :: Nat). NatRepr x -> NatRepr y -> Bool
ShowF NatRepr
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods withShow :: forall p q (tp :: Nat) a. p NatRepr -> q tp -> (Show (NatRepr tp) => a) -> a showF :: forall (tp :: Nat). NatRepr tp -> String showsPrecF :: forall (tp :: Nat). Int -> NatRepr tp -> String -> String
DecidableEq NatRepr
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods decEq :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Either (a :~: b) ((a :~: b) -> Void)
IsRepr NatRepr
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Nat) r. NatRepr a -> (KnownRepr NatRepr a => r) -> r
KnownNat n => KnownRepr NatRepr (n :: Nat)
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods knownRepr :: NatRepr n
KnownNat n => Data (NatRepr n)
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (NatRepr n) # toConstr :: NatRepr n -> Constr # dataTypeOf :: NatRepr n -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (NatRepr n)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (NatRepr n)) # gmapT :: (forall b. Data b => b -> b) -> NatRepr n -> NatRepr n # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r # gmapQ :: (forall d. Data d => d -> u) -> NatRepr n -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NatRepr n -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) #
Show (NatRepr n)
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods showsPrec :: Int -> NatRepr n -> ShowS # show :: NatRepr n -> String # showList :: [NatRepr n] -> ShowS #
Eq (NatRepr m)
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods (==) :: NatRepr m -> NatRepr m -> Bool # (/=) :: NatRepr m -> NatRepr m -> Bool #
Hashable (NatRepr n)
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods hashWithSalt :: Int -> NatRepr n -> Int hash :: NatRepr n -> Int
PolyEq (NatRepr m) (NatRepr n)
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods polyEqF :: NatRepr m -> NatRepr n -> Maybe (NatRepr m :~: NatRepr n) polyEq :: NatRepr m -> NatRepr n -> Bool

knownNat :: forall (n :: Nat). KnownNat n => NatRepr n #