{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
module Lang.Crucible.CFG.Common
(
GlobalVar(..)
, freshGlobalVar
, BreakpointName(..)
) where
import Data.Text (Text)
import qualified Data.Text as Text
import Prettyprinter
import Data.Parameterized.Classes
import Data.Parameterized.Nonce
import Lang.Crucible.FunctionHandle
import Lang.Crucible.Types
data GlobalVar (tp :: CrucibleType)
= GlobalVar { forall (tp :: CrucibleType).
GlobalVar tp -> Nonce GlobalNonceGenerator tp
globalNonce :: {-# UNPACK #-} !(Nonce GlobalNonceGenerator tp)
, forall (tp :: CrucibleType). GlobalVar tp -> Text
globalName :: !Text
, forall (tp :: CrucibleType). GlobalVar tp -> TypeRepr tp
globalType :: !(TypeRepr tp)
}
instance TestEquality GlobalVar where
GlobalVar a
x testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
GlobalVar a -> GlobalVar b -> Maybe (a :~: b)
`testEquality` GlobalVar b
y = GlobalVar a -> Nonce GlobalNonceGenerator a
forall (tp :: CrucibleType).
GlobalVar tp -> Nonce GlobalNonceGenerator tp
globalNonce GlobalVar a
x Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator b -> Maybe (a :~: b)
`testEquality` GlobalVar b -> Nonce GlobalNonceGenerator b
forall (tp :: CrucibleType).
GlobalVar tp -> Nonce GlobalNonceGenerator tp
globalNonce GlobalVar b
y
instance OrdF GlobalVar where
GlobalVar x
x compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
GlobalVar x -> GlobalVar y -> OrderingF x y
`compareF` GlobalVar y
y = GlobalVar x -> Nonce GlobalNonceGenerator x
forall (tp :: CrucibleType).
GlobalVar tp -> Nonce GlobalNonceGenerator tp
globalNonce GlobalVar x
x Nonce GlobalNonceGenerator x
-> Nonce GlobalNonceGenerator y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Nonce GlobalNonceGenerator x
-> Nonce GlobalNonceGenerator y -> OrderingF x y
`compareF` GlobalVar y -> Nonce GlobalNonceGenerator y
forall (tp :: CrucibleType).
GlobalVar tp -> Nonce GlobalNonceGenerator tp
globalNonce GlobalVar y
y
instance Show (GlobalVar tp) where
show :: GlobalVar tp -> String
show = Text -> String
Text.unpack (Text -> String)
-> (GlobalVar tp -> Text) -> GlobalVar tp -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalVar tp -> Text
forall (tp :: CrucibleType). GlobalVar tp -> Text
globalName
instance ShowF GlobalVar
instance Pretty (GlobalVar tp) where
pretty :: forall ann. GlobalVar tp -> Doc ann
pretty = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann)
-> (GlobalVar tp -> Text) -> GlobalVar tp -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalVar tp -> Text
forall (tp :: CrucibleType). GlobalVar tp -> Text
globalName
freshGlobalVar :: HandleAllocator
-> Text
-> TypeRepr tp
-> IO (GlobalVar tp)
freshGlobalVar :: forall (tp :: CrucibleType).
HandleAllocator -> Text -> TypeRepr tp -> IO (GlobalVar tp)
freshGlobalVar HandleAllocator
halloc Text
nm TypeRepr tp
tp = do
Nonce GlobalNonceGenerator tp
nonce <- NonceGenerator IO GlobalNonceGenerator
-> IO (Nonce GlobalNonceGenerator tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce (HandleAllocator -> NonceGenerator IO GlobalNonceGenerator
haCounter HandleAllocator
halloc)
GlobalVar tp -> IO (GlobalVar tp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return GlobalVar
{ globalNonce :: Nonce GlobalNonceGenerator tp
globalNonce = Nonce GlobalNonceGenerator tp
nonce
, globalName :: Text
globalName = Text
nm
, globalType :: TypeRepr tp
globalType = TypeRepr tp
tp
}
newtype BreakpointName = BreakpointName { BreakpointName -> Text
breakpointNameText :: Text }
deriving (BreakpointName -> BreakpointName -> Bool
(BreakpointName -> BreakpointName -> Bool)
-> (BreakpointName -> BreakpointName -> Bool) -> Eq BreakpointName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BreakpointName -> BreakpointName -> Bool
== :: BreakpointName -> BreakpointName -> Bool
$c/= :: BreakpointName -> BreakpointName -> Bool
/= :: BreakpointName -> BreakpointName -> Bool
Eq, Eq BreakpointName
Eq BreakpointName =>
(BreakpointName -> BreakpointName -> Ordering)
-> (BreakpointName -> BreakpointName -> Bool)
-> (BreakpointName -> BreakpointName -> Bool)
-> (BreakpointName -> BreakpointName -> Bool)
-> (BreakpointName -> BreakpointName -> Bool)
-> (BreakpointName -> BreakpointName -> BreakpointName)
-> (BreakpointName -> BreakpointName -> BreakpointName)
-> Ord BreakpointName
BreakpointName -> BreakpointName -> Bool
BreakpointName -> BreakpointName -> Ordering
BreakpointName -> BreakpointName -> BreakpointName
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 :: BreakpointName -> BreakpointName -> Ordering
compare :: BreakpointName -> BreakpointName -> Ordering
$c< :: BreakpointName -> BreakpointName -> Bool
< :: BreakpointName -> BreakpointName -> Bool
$c<= :: BreakpointName -> BreakpointName -> Bool
<= :: BreakpointName -> BreakpointName -> Bool
$c> :: BreakpointName -> BreakpointName -> Bool
> :: BreakpointName -> BreakpointName -> Bool
$c>= :: BreakpointName -> BreakpointName -> Bool
>= :: BreakpointName -> BreakpointName -> Bool
$cmax :: BreakpointName -> BreakpointName -> BreakpointName
max :: BreakpointName -> BreakpointName -> BreakpointName
$cmin :: BreakpointName -> BreakpointName -> BreakpointName
min :: BreakpointName -> BreakpointName -> BreakpointName
Ord, Int -> BreakpointName -> ShowS
[BreakpointName] -> ShowS
BreakpointName -> String
(Int -> BreakpointName -> ShowS)
-> (BreakpointName -> String)
-> ([BreakpointName] -> ShowS)
-> Show BreakpointName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BreakpointName -> ShowS
showsPrec :: Int -> BreakpointName -> ShowS
$cshow :: BreakpointName -> String
show :: BreakpointName -> String
$cshowList :: [BreakpointName] -> ShowS
showList :: [BreakpointName] -> ShowS
Show)
instance Pretty BreakpointName where
pretty :: forall ann. BreakpointName -> Doc ann
pretty = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann)
-> (BreakpointName -> Text) -> BreakpointName -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BreakpointName -> Text
breakpointNameText