{- |
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
  , CutpointName(..)
  ) 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 CutpointName = CutpointName { CutpointName -> Text
cutpointNameText :: Text }
  deriving (CutpointName -> CutpointName -> Bool
(CutpointName -> CutpointName -> Bool)
-> (CutpointName -> CutpointName -> Bool) -> Eq CutpointName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CutpointName -> CutpointName -> Bool
== :: CutpointName -> CutpointName -> Bool
$c/= :: CutpointName -> CutpointName -> Bool
/= :: CutpointName -> CutpointName -> Bool
Eq, Eq CutpointName
Eq CutpointName =>
(CutpointName -> CutpointName -> Ordering)
-> (CutpointName -> CutpointName -> Bool)
-> (CutpointName -> CutpointName -> Bool)
-> (CutpointName -> CutpointName -> Bool)
-> (CutpointName -> CutpointName -> Bool)
-> (CutpointName -> CutpointName -> CutpointName)
-> (CutpointName -> CutpointName -> CutpointName)
-> Ord CutpointName
CutpointName -> CutpointName -> Bool
CutpointName -> CutpointName -> Ordering
CutpointName -> CutpointName -> CutpointName
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 :: CutpointName -> CutpointName -> Ordering
compare :: CutpointName -> CutpointName -> Ordering
$c< :: CutpointName -> CutpointName -> Bool
< :: CutpointName -> CutpointName -> Bool
$c<= :: CutpointName -> CutpointName -> Bool
<= :: CutpointName -> CutpointName -> Bool
$c> :: CutpointName -> CutpointName -> Bool
> :: CutpointName -> CutpointName -> Bool
$c>= :: CutpointName -> CutpointName -> Bool
>= :: CutpointName -> CutpointName -> Bool
$cmax :: CutpointName -> CutpointName -> CutpointName
max :: CutpointName -> CutpointName -> CutpointName
$cmin :: CutpointName -> CutpointName -> CutpointName
min :: CutpointName -> CutpointName -> CutpointName
Ord, Int -> CutpointName -> ShowS
[CutpointName] -> ShowS
CutpointName -> String
(Int -> CutpointName -> ShowS)
-> (CutpointName -> String)
-> ([CutpointName] -> ShowS)
-> Show CutpointName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CutpointName -> ShowS
showsPrec :: Int -> CutpointName -> ShowS
$cshow :: CutpointName -> String
show :: CutpointName -> String
$cshowList :: [CutpointName] -> ShowS
showList :: [CutpointName] -> ShowS
Show)

instance Pretty CutpointName where
  pretty :: forall ann. CutpointName -> Doc ann
pretty = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ann)
-> (CutpointName -> Text) -> CutpointName -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CutpointName -> Text
cutpointNameText