{-# 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
-- Description      : Crucible type definitions related to LLVM
-- Copyright        : (c) Galois, Inc 2015-2016
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------
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

-- | The 'CrucibleType' of an LLVM memory. @'RegValue' sym 'Mem'@ is
-- implemented as @'MemImpl' sym@.
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

-- | This constraint captures the idea that there is a distinguished
--   pointer width in scope which is appropriate according to the C
--   notion of pointer, and object size. In particular, it must be at
--   least 16-bits wide (as required for the @size_t@ type).
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

-- | Crucible type of pointers/bitvector values of width @w@.
type LLVMPointerType w = IntrinsicType "LLVM_pointer" (EmptyCtx ::> BVType w)

-- | Symbolic LLVM pointer or bitvector values of width @w@.
type LLVMPtr sym w = RegValue sym (LLVMPointerType w)

-- | This pattern synonym makes it easy to build and destruct runtime
--   representatives of @'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)

-- | This pattern creates/matches against the TypeRepr for LLVM pointer values
--   that are of the distinguished pointer width.
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

-- | This pattern creates/matches against the TypeRepr for raw bitvector values
--   that are of the distinguished pointer width.
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

-- | This pattern creates/matches against the TypeRepr for raw signed bitvector values
--   that are of the distinguished pointer width.
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