{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Lang.Crucible.LLVM.Types
( Mem
, memRepr
, LLVMPointerType
, LLVMPtr
, pattern LLVMPointerRepr
, pattern PtrRepr
, pattern SizeT
, pattern SSizeT
, withPtrWidth
, HasPtrWidth
, pattern PtrWidth
, GlobalSymbol(..)
, globalSymbolName
) where
import GHC.TypeNats
import Data.Typeable
import Data.Parameterized.Context
import qualified Text.LLVM.AST as L
import Lang.Crucible.Simulator.RegValue
import Lang.Crucible.Types
newtype GlobalSymbol = GlobalSymbol L.Symbol
deriving (Typeable, GlobalSymbol -> GlobalSymbol -> Bool
(GlobalSymbol -> GlobalSymbol -> Bool)
-> (GlobalSymbol -> GlobalSymbol -> Bool) -> Eq GlobalSymbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GlobalSymbol -> GlobalSymbol -> Bool
== :: GlobalSymbol -> GlobalSymbol -> Bool
$c/= :: GlobalSymbol -> GlobalSymbol -> Bool
/= :: GlobalSymbol -> GlobalSymbol -> Bool
Eq, Eq GlobalSymbol
Eq GlobalSymbol =>
(GlobalSymbol -> GlobalSymbol -> Ordering)
-> (GlobalSymbol -> GlobalSymbol -> Bool)
-> (GlobalSymbol -> GlobalSymbol -> Bool)
-> (GlobalSymbol -> GlobalSymbol -> Bool)
-> (GlobalSymbol -> GlobalSymbol -> Bool)
-> (GlobalSymbol -> GlobalSymbol -> GlobalSymbol)
-> (GlobalSymbol -> GlobalSymbol -> GlobalSymbol)
-> Ord GlobalSymbol
GlobalSymbol -> GlobalSymbol -> Bool
GlobalSymbol -> GlobalSymbol -> Ordering
GlobalSymbol -> GlobalSymbol -> GlobalSymbol
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: GlobalSymbol -> GlobalSymbol -> Ordering
compare :: GlobalSymbol -> GlobalSymbol -> Ordering
$c< :: GlobalSymbol -> GlobalSymbol -> Bool
< :: GlobalSymbol -> GlobalSymbol -> Bool
$c<= :: GlobalSymbol -> GlobalSymbol -> Bool
<= :: GlobalSymbol -> GlobalSymbol -> Bool
$c> :: GlobalSymbol -> GlobalSymbol -> Bool
> :: GlobalSymbol -> GlobalSymbol -> Bool
$c>= :: GlobalSymbol -> GlobalSymbol -> Bool
>= :: GlobalSymbol -> GlobalSymbol -> Bool
$cmax :: GlobalSymbol -> GlobalSymbol -> GlobalSymbol
max :: GlobalSymbol -> GlobalSymbol -> GlobalSymbol
$cmin :: GlobalSymbol -> GlobalSymbol -> GlobalSymbol
min :: GlobalSymbol -> GlobalSymbol -> GlobalSymbol
Ord, Int -> GlobalSymbol -> ShowS
[GlobalSymbol] -> ShowS
GlobalSymbol -> String
(Int -> GlobalSymbol -> ShowS)
-> (GlobalSymbol -> String)
-> ([GlobalSymbol] -> ShowS)
-> Show GlobalSymbol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GlobalSymbol -> ShowS
showsPrec :: Int -> GlobalSymbol -> ShowS
$cshow :: GlobalSymbol -> String
show :: GlobalSymbol -> String
$cshowList :: [GlobalSymbol] -> ShowS
showList :: [GlobalSymbol] -> ShowS
Show)
globalSymbolName :: GlobalSymbol -> String
globalSymbolName :: GlobalSymbol -> String
globalSymbolName (GlobalSymbol (L.Symbol String
nm)) = String
nm
type Mem = IntrinsicType "LLVM_memory" EmptyCtx
memRepr :: TypeRepr Mem
memRepr :: TypeRepr Mem
memRepr = TypeRepr Mem
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
type HasPtrWidth w = (1 <= w, 16 <= w, ?ptrWidth :: NatRepr w)
pattern PtrWidth :: HasPtrWidth w => w ~ w' => NatRepr w'
pattern $mPtrWidth :: forall {r} {w :: Natural} {w' :: Natural}.
HasPtrWidth w =>
NatRepr w' -> ((w ~ w') => r) -> ((# #) -> r) -> r
$bPtrWidth :: forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth <- (testEquality ?ptrWidth -> Just Refl)
where PtrWidth = ?ptrWidth::NatRepr w'
NatRepr w'
?ptrWidth
withPtrWidth :: forall w a. (16 <= w) => NatRepr w -> (HasPtrWidth w => a) -> a
withPtrWidth :: forall (w :: Natural) a.
(16 <= w) =>
NatRepr w -> (HasPtrWidth w => a) -> a
withPtrWidth NatRepr w
w HasPtrWidth w => a
a =
case LeqProof 1 16 -> LeqProof 16 w -> LeqProof 1 w
forall (m :: Natural) (n :: Natural) (p :: Natural).
LeqProof m n -> LeqProof n p -> LeqProof m p
leqTrans (LeqProof 1 16
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 1 16) (LeqProof 16 w
forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof :: LeqProof 16 w) of
LeqProof 1 w
LeqProof -> let ?ptrWidth = ?ptrWidth::NatRepr w
NatRepr w
w in a
HasPtrWidth w => a
a
type LLVMPointerType w = IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w)
type LLVMPtr sym w = RegValue sym (LLVMPointerType w)
pattern LLVMPointerRepr :: () => (1 <= w, ty ~ LLVMPointerType w) => NatRepr w -> TypeRepr ty
pattern $mLLVMPointerRepr :: forall {r} {ty :: CrucibleType}.
TypeRepr ty
-> (forall {w :: Natural}.
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> r)
-> ((# #) -> r)
-> r
$bLLVMPointerRepr :: forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr w <- IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "LLVM_pointer") -> Just Refl)
(Empty :> BVRepr w)
where
LLVMPointerRepr NatRepr w
w = SymbolRepr "LLVM_pointer"
-> CtxRepr (EmptyCtx ::> BVType w) -> TypeRepr (LLVMPointerType w)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType).
SymbolRepr nm -> CtxRepr ctx -> TypeRepr ('IntrinsicType nm ctx)
IntrinsicRepr SymbolRepr "LLVM_pointer"
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol (Assignment TypeRepr EmptyCtx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty Assignment TypeRepr EmptyCtx
-> TypeRepr (BVType w) -> CtxRepr (EmptyCtx ::> BVType w)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
(tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> NatRepr w -> TypeRepr (BVType w)
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr w
w)
pattern PtrRepr :: HasPtrWidth wptr => (ty ~ LLVMPointerType wptr) => TypeRepr ty
pattern $mPtrRepr :: forall {r} {wptr :: Natural} {ty :: CrucibleType}.
HasPtrWidth wptr =>
TypeRepr ty
-> ((ty ~ LLVMPointerType wptr) => r) -> ((# #) -> r) -> r
$bPtrRepr :: forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ LLVMPointerType wptr) =>
TypeRepr ty
PtrRepr = LLVMPointerRepr PtrWidth
pattern SizeT :: HasPtrWidth wptr => (ty ~ BVType wptr) => TypeRepr ty
pattern $mSizeT :: forall {r} {wptr :: Natural} {ty :: CrucibleType}.
HasPtrWidth wptr =>
TypeRepr ty -> ((ty ~ BVType wptr) => r) -> ((# #) -> r) -> r
$bSizeT :: forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ BVType wptr) =>
TypeRepr ty
SizeT = BVRepr PtrWidth
pattern SSizeT :: HasPtrWidth wptr => (ty ~ BVType wptr) => TypeRepr ty
pattern $mSSizeT :: forall {r} {wptr :: Natural} {ty :: CrucibleType}.
HasPtrWidth wptr =>
TypeRepr ty -> ((ty ~ BVType wptr) => r) -> ((# #) -> r) -> r
$bSSizeT :: forall (wptr :: Natural) (ty :: CrucibleType).
(HasPtrWidth wptr, ty ~ BVType wptr) =>
TypeRepr ty
SSizeT = BVRepr PtrWidth