----------------------------------------------------------------------- -- | -- Module : Lang.Crucible.Types -- Description : This module exports the types used in Crucible -- expressions. -- Copyright : (c) Galois, Inc 2014 -- License : BSD3 -- Maintainer : Joe Hendrix -- Stability : provisional -- -- 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. ------------------------------------------------------------------------ {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} module Lang.Crucible.Types ( -- * CrucibleType data kind type CrucibleType -- ** Constructors for kind CrucibleType , AnyType , UnitType , BoolType , NatType , IntegerType , RealValType , SymbolicStructType , ComplexRealType , BVType , FloatType , IEEEFloatType , CharType , StringType , FunctionHandleType , MaybeType , RecursiveType , IntrinsicType , VectorType , SequenceType , StructType , VariantType , ReferenceType , WordMapType , StringMapType , SymbolicArrayType -- * IsRecursiveType , IsRecursiveType(..) -- * Base type injection , BaseToType , baseToType , AsBaseType(..) , asBaseType -- * Other stuff , CtxRepr , pattern KnownBV -- * Representation of Crucible types , TypeRepr(..) -- * Re-exports , module Data.Parameterized.Ctx , module Data.Parameterized.NatRepr , module Data.Parameterized.SymbolRepr , module What4.BaseTypes , FloatInfo , HalfFloat , SingleFloat , DoubleFloat , QuadFloat , X86_80Float , DoubleDoubleFloat , FloatInfoRepr(..) , FloatInfoToBitWidth , floatInfoToBVTypeRepr ) where import Data.Hashable import Data.Type.Equality import GHC.TypeNats (Nat, KnownNat) import Data.Parameterized.Classes import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Ctx import Data.Parameterized.NatRepr import Data.Parameterized.SymbolRepr import qualified Data.Parameterized.TH.GADT as U import Prettyprinter import What4.BaseTypes import What4.InterpretedFloatingPoint ------------------------------------------------------------------------ -- Crucible types -- | 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'. class IsRecursiveType (nm::Symbol) where type UnrollType nm (ctx :: Ctx CrucibleType) :: CrucibleType unrollType :: SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx) type CtxRepr = Ctx.Assignment TypeRepr -- | This data kind describes the types of values and expressions that -- can occur in Crucible CFGs. data CrucibleType where -- | An injection of solver interface types into Crucible types BaseToType :: BaseType -> CrucibleType -- | A dynamic type that can contain values of any type. AnyType :: CrucibleType -- | A type containing a single value "Unit" UnitType :: CrucibleType -- | A type for natural numbers. NatType :: CrucibleType -- | A type index for floating point numbers, whose interpretation -- depends on the symbolic backend. FloatType :: FloatInfo -> CrucibleType -- | A single character, as a 16-bit wide char. CharType :: CrucibleType -- | A function handle taking a context of formal arguments and a return type FunctionHandleType :: Ctx CrucibleType -> CrucibleType -> CrucibleType -- The Maybe type lifted into crucible expressions MaybeType :: 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. VectorType :: 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. SequenceType :: CrucibleType -> CrucibleType -- A structure is an aggregate type consisting of a sequence of values. -- The type of each value is known statically. StructType :: Ctx CrucibleType -> CrucibleType -- The type of mutable reference cells. ReferenceType :: CrucibleType -> CrucibleType -- A variant is a disjoint union of the types listed in the context. VariantType :: Ctx CrucibleType -> 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. WordMapType :: Nat -> BaseType -> 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. RecursiveType :: 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, or via the language extension mechanism. See the -- `IntrinsicClass` typeclass and the `Intrinsic` type family -- defined in "Lang.Crucible.Simulator.Intrinsics". -- -- The context of crucible types are type arguments to the intrinsic type. IntrinsicType :: Symbol -> Ctx CrucibleType -> CrucibleType -- A partial map from strings to values. StringMapType :: CrucibleType -> CrucibleType type BaseToType = 'BaseToType -- ^ @:: 'BaseType' -> 'CrucibleType'@. type BoolType = BaseToType BaseBoolType -- ^ @:: 'CrucibleType'@. type BVType w = BaseToType (BaseBVType w) -- ^ @:: 'Nat' -> 'CrucibleType'@. type ComplexRealType = BaseToType BaseComplexType -- ^ @:: 'CrucibleType'@. type IntegerType = BaseToType BaseIntegerType -- ^ @:: 'CrucibleType'@. type StringType si = BaseToType (BaseStringType si) -- ^ @:: 'StringInfo' -> 'CrucibleType'@. type RealValType = BaseToType BaseRealType -- ^ @:: 'CrucibleType'@. type IEEEFloatType p = BaseToType (BaseFloatType p) -- ^ @:: FloatPrecision -> CrucibleType@ type SymbolicArrayType idx xs = BaseToType (BaseArrayType idx xs) -- ^ @:: 'Ctx.Ctx' 'BaseType' -> 'BaseType' -> 'CrucibleType'@. type SymbolicStructType flds = BaseToType (BaseStructType flds) -- ^ @:: 'Ctx.Ctx' 'BaseType' -> 'CrucibleType'@. -- | A dynamic type that can contain values of any type. type AnyType = 'AnyType -- ^ @:: 'CrucibleType'@. -- | A single character, as a 16-bit wide char. type CharType = 'CharType -- ^ @:: 'CrucibleType'@. -- | A type index for floating point numbers, whose interpretation -- depends on the symbolic backend. type FloatType = 'FloatType -- ^ @:: 'FloatInfo' -> 'CrucibleType'@. -- | A function handle taking a context of formal arguments and a return type. type FunctionHandleType = 'FunctionHandleType -- ^ @:: 'Ctx' 'CrucibleType' -> '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 'Lang.Crucible.CFG.Expr.RollRecursive' and -- 'Lang.Crucible.CFG.Expr.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 RecursiveType = 'RecursiveType -- ^ @:: '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 'Lang.Crucible.Simulator.Intrinsics.IntrinsicClass' typeclass -- and the 'Lang.Crucible.Simulator.Intrinsics.Intrinsic' type family -- defined in "Lang.Crucible.Simulator.Intrinsics". type IntrinsicType ctx = 'IntrinsicType ctx -- ^ @:: 'Symbol' -> 'Ctx' 'CrucibleType' -> 'CrucibleType'@. -- | The type of mutable reference cells. type ReferenceType = 'ReferenceType -- ^ @:: 'CrucibleType' -> 'CrucibleType'@. -- | The 'Maybe' type lifted into Crucible expressions. type MaybeType = 'MaybeType -- ^ @:: 'CrucibleType' -> 'CrucibleType'@. -- | A partial map from strings to values. type StringMapType = 'StringMapType -- ^ @:: 'CrucibleType' -> 'CrucibleType'@. -- | A structure is an aggregate type consisting of a sequence of -- values. The type of each value is known statically. type StructType = 'StructType -- ^ @:: 'Ctx' 'CrucibleType' -> 'CrucibleType'@. -- | A type containing a single value "Unit". type UnitType = 'UnitType -- ^ @:: 'CrucibleType'@. -- | A type for natural numbers. type NatType = 'NatType -- ^ @:: 'CrucibleType'@. -- | A variant is a disjoint union of the types listed in the context. type VariantType = 'VariantType -- ^ @:: 'Ctx' '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 VectorType = 'VectorType -- ^ @:: '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 SequenceType = 'SequenceType -- ^ @:: 'CrucibleType' -> '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 WordMapType = 'WordMapType -- ^ @:: 'Nat' -> 'BaseType' -> 'CrucibleType'@. ---------------------------------------------------------------- -- Base Type Injection baseToType :: BaseTypeRepr bt -> TypeRepr (BaseToType bt) baseToType bt = case bt of BaseBoolRepr -> BoolRepr BaseIntegerRepr -> IntegerRepr BaseRealRepr -> RealValRepr BaseStringRepr si -> StringRepr si BaseBVRepr w -> BVRepr w BaseComplexRepr -> ComplexRealRepr BaseArrayRepr idx xs -> SymbolicArrayRepr idx xs BaseStructRepr flds -> SymbolicStructRepr flds BaseFloatRepr ps -> IEEEFloatRepr ps data AsBaseType tp where AsBaseType :: tp ~ BaseToType bt => BaseTypeRepr bt -> AsBaseType tp NotBaseType :: AsBaseType tp asBaseType :: TypeRepr tp -> AsBaseType tp asBaseType tp = case tp of BoolRepr -> AsBaseType BaseBoolRepr IntegerRepr -> AsBaseType BaseIntegerRepr RealValRepr -> AsBaseType BaseRealRepr StringRepr si -> AsBaseType (BaseStringRepr si) BVRepr w -> AsBaseType (BaseBVRepr w) ComplexRealRepr -> AsBaseType BaseComplexRepr SymbolicArrayRepr idx xs -> AsBaseType (BaseArrayRepr idx xs) IEEEFloatRepr ps -> AsBaseType (BaseFloatRepr ps) SymbolicStructRepr flds -> AsBaseType (BaseStructRepr flds) _ -> NotBaseType ---------------------------------------------------------------- -- Type representatives -- | A family of representatives for Crucible types. Parameter @tp@ -- has kind 'CrucibleType'. 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) -- | This is a representation of floats that works at known fixed -- mantissa and exponent widths, but the symbolic backend may pick -- the representation. FloatRepr :: !(FloatInfoRepr flt) -> TypeRepr (FloatType flt) -- | This is a float with user-definable mantissa and exponent that -- maps directly to the what4 base type. 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 :: !(Ctx.Assignment BaseTypeRepr (idx::>tp)) -> !(BaseTypeRepr t) -> TypeRepr (SymbolicArrayType (idx::>tp) t) -- A reference to a symbolic struct. SymbolicStructRepr :: Ctx.Assignment BaseTypeRepr ctx -> TypeRepr (SymbolicStructType ctx) ------------------------------------------------------------------------------ -- Representable class instances instance KnownRepr TypeRepr AnyType where knownRepr = AnyRepr instance KnownRepr TypeRepr UnitType where knownRepr = UnitRepr instance KnownRepr TypeRepr CharType where knownRepr = CharRepr instance KnownRepr TypeRepr NatType where knownRepr = NatRepr instance KnownRepr BaseTypeRepr bt => KnownRepr TypeRepr (BaseToType bt) where knownRepr = baseToType knownRepr instance KnownCtx TypeRepr ctx => KnownRepr TypeRepr (StructType ctx) where knownRepr = StructRepr knownRepr instance KnownCtx TypeRepr ctx => KnownRepr TypeRepr (VariantType ctx) where knownRepr = VariantRepr knownRepr instance KnownRepr TypeRepr a => KnownRepr TypeRepr (ReferenceType a) where knownRepr = ReferenceRepr knownRepr instance (KnownSymbol s, KnownCtx TypeRepr ctx) => KnownRepr TypeRepr (IntrinsicType s ctx) where knownRepr = IntrinsicRepr knownSymbol knownRepr instance (KnownSymbol s, KnownCtx TypeRepr ctx, IsRecursiveType s) => KnownRepr TypeRepr (RecursiveType s ctx) where knownRepr = RecursiveRepr knownSymbol knownRepr instance (1 <= w, KnownNat w, KnownRepr BaseTypeRepr tp) => KnownRepr TypeRepr (WordMapType w tp) where knownRepr = WordMapRepr (knownNat :: NatRepr w) (knownRepr :: BaseTypeRepr tp) instance (KnownCtx TypeRepr ctx, KnownRepr TypeRepr ret) => KnownRepr TypeRepr (FunctionHandleType ctx ret) where knownRepr = FunctionHandleRepr knownRepr knownRepr instance KnownRepr FloatInfoRepr flt => KnownRepr TypeRepr (FloatType flt) where knownRepr = FloatRepr knownRepr instance KnownRepr FloatPrecisionRepr ps => KnownRepr TypeRepr (IEEEFloatType ps) where knownRepr = IEEEFloatRepr knownRepr instance KnownRepr TypeRepr tp => KnownRepr TypeRepr (VectorType tp) where knownRepr = VectorRepr knownRepr instance KnownRepr TypeRepr tp => KnownRepr TypeRepr (SequenceType tp) where knownRepr = SequenceRepr knownRepr instance KnownRepr TypeRepr tp => KnownRepr TypeRepr (MaybeType tp) where knownRepr = MaybeRepr knownRepr instance KnownRepr TypeRepr tp => KnownRepr TypeRepr (StringMapType tp) where knownRepr = StringMapRepr knownRepr -- | Pattern synonym specifying bitvector TypeReprs. Intended to be use -- with type applications, e.g., @KnownBV \@32@. pattern KnownBV :: forall n. (1 <= n, KnownNat n) => TypeRepr (BVType n) pattern KnownBV <- BVRepr (testEquality (knownRepr :: NatRepr n) -> Just Refl) where KnownBV = knownRepr ------------------------------------------------------------------------ -- Misc typeclass instances -- Force TypeRepr, etc. to be in context for next slice. $(return []) instance HashableF TypeRepr where hashWithSaltF = hashWithSalt instance Hashable (TypeRepr ty) where hashWithSalt = $(U.structuralHashWithSalt [t|TypeRepr|] []) instance Pretty (TypeRepr tp) where pretty = viaShow instance Show (TypeRepr tp) where showsPrec = $(U.structuralShowsPrec [t|TypeRepr|]) instance ShowF TypeRepr instance TestEquality TypeRepr where testEquality = $(U.structuralTypeEquality [t|TypeRepr|] [ (U.TypeApp (U.ConType [t|NatRepr|]) U.AnyType, [|testEquality|]) , (U.TypeApp (U.ConType [t|SymbolRepr|]) U.AnyType, [|testEquality|]) , (U.TypeApp (U.ConType [t|FloatInfoRepr|]) U.AnyType, [|testEquality|]) , (U.TypeApp (U.ConType [t|FloatPrecisionRepr|]) U.AnyType, [|testEquality|]) , (U.TypeApp (U.ConType [t|CtxRepr|]) U.AnyType, [|testEquality|]) , (U.TypeApp (U.ConType [t|BaseTypeRepr|]) U.AnyType, [|testEquality|]) , (U.TypeApp (U.ConType [t|StringInfoRepr|]) U.AnyType, [|testEquality|]) , (U.TypeApp (U.ConType [t|TypeRepr|]) U.AnyType, [|testEquality|]) , (U.TypeApp (U.TypeApp (U.ConType [t|Ctx.Assignment|]) U.AnyType) U.AnyType , [|testEquality|]) ] ) instance Eq (TypeRepr tp) where x == y = isJust (testEquality x y) instance OrdF TypeRepr where compareF = $(U.structuralTypeOrd [t|TypeRepr|] [ (U.TypeApp (U.ConType [t|NatRepr|]) U.AnyType, [|compareF|]) , (U.TypeApp (U.ConType [t|SymbolRepr|]) U.AnyType, [|compareF|]) , (U.TypeApp (U.ConType [t|FloatInfoRepr|]) U.AnyType, [|compareF|]) , (U.TypeApp (U.ConType [t|FloatPrecisionRepr|]) U.AnyType, [|compareF|]) , (U.TypeApp (U.ConType [t|BaseTypeRepr|]) U.AnyType, [|compareF|]) , (U.TypeApp (U.ConType [t|StringInfoRepr|]) U.AnyType, [|compareF|]) , (U.TypeApp (U.ConType [t|TypeRepr|]) U.AnyType, [|compareF|]) , (U.TypeApp (U.ConType [t|CtxRepr|]) U.AnyType, [|compareF|]) , (U.TypeApp (U.TypeApp (U.ConType [t|Ctx.Assignment|]) U.AnyType) U.AnyType , [|compareF|]) ] )