{- |
Module           : Lang.Crucible.CFG.Common
Description      : Common CFG datastructure definitions
Copyright        : (c) Galois, Inc 2014-2016
License          : BSD3
Maintainer       : Joe Hendrix <jhendrix@galois.com>

Data structures and operations that are common to both the
registerized and the SSA form CFG representations.
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
module Lang.Crucible.CFG.Common
  ( -- * Global variables
    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

------------------------------------------------------------------------
-- GlobalVar

-- | A global variable.
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