-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.Translation.Monad
-- Description      : Translation monad for LLVM and support operations
-- Copyright        : (c) Galois, Inc 2018
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
-----------------------------------------------------------------------
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE ImplicitParams        #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeOperators         #-}

module Lang.Crucible.LLVM.Translation.Monad
  ( -- * Generator monad
    LLVMGenerator
  , LLVMGenerator'
  , LLVMState(..)
  , identMap
  , blockInfoMap
  , translationWarnings
  , functionSymbol
  , addWarning
  , LLVMTranslationWarning(..)
  , IdentMap
  , LLVMBlockInfo(..)
  , LLVMBlockInfoMap
  , buildBlockInfoMap
  , initialState
  , getMemVar

    -- * Malformed modules
  , MalformedLLVMModule(..)
  , malformedLLVMModule
  , renderMalformedLLVMModule

    -- * LLVMContext
  , LLVMContext(..)
  , llvmTypeCtx
  , mkLLVMContext

  , useTypedVal
  ) where

import Control.Lens hiding (op, (:>), to, from )
import Control.Monad (unless)
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.State.Strict (MonadState(..))
import Data.IORef (IORef, modifyIORef)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import Data.Text (Text)

import qualified Text.LLVM.AST as L

import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.NatRepr as NatRepr
import           Data.Parameterized.Some

import           Lang.Crucible.CFG.Generator
import           Lang.Crucible.Panic ( panic )

import           Lang.Crucible.LLVM.DataLayout
import           Lang.Crucible.LLVM.Extension
import           Lang.Crucible.LLVM.MalformedLLVMModule
import           Lang.Crucible.LLVM.MemModel
import           Lang.Crucible.LLVM.MemType
import           Lang.Crucible.LLVM.Translation.BlockInfo
import           Lang.Crucible.LLVM.Translation.Types
import           Lang.Crucible.LLVM.TypeContext

import           Lang.Crucible.Types

------------------------------------------------------------------------
-- ** LLVMContext

-- | Information about the LLVM module.
data LLVMContext arch
   = LLVMContext
   { -- | Map LLVM symbols to their associated state.
     forall (arch :: LLVMArch). LLVMContext arch -> ArchRepr arch
llvmArch       :: ArchRepr arch
   , forall (arch :: LLVMArch).
LLVMContext arch
-> forall a.
   ((16 <= ArchWidth arch) => NatRepr (ArchWidth arch) -> a) -> a
llvmPtrWidth   :: forall a. (16 <= (ArchWidth arch) => NatRepr (ArchWidth arch) -> a) -> a
   , forall (arch :: LLVMArch). LLVMContext arch -> GlobalVar Mem
llvmMemVar     :: GlobalVar Mem
   , forall (arch :: LLVMArch). LLVMContext arch -> TypeContext
_llvmTypeCtx   :: TypeContext
     -- | For each global variable symbol, compute the set of
     --   aliases to that symbol
   , forall (arch :: LLVMArch).
LLVMContext arch -> Map Symbol (Set GlobalAlias)
llvmGlobalAliases   :: Map L.Symbol (Set L.GlobalAlias)
     -- | For each function symbol, compute the set of
     --   aliases to that symbol
   , forall (arch :: LLVMArch).
LLVMContext arch -> Map Symbol (Set GlobalAlias)
llvmFunctionAliases :: Map L.Symbol (Set L.GlobalAlias)
   }

llvmTypeCtx :: Simple Lens (LLVMContext arch) TypeContext
llvmTypeCtx :: forall (arch :: LLVMArch) (f :: Type -> Type).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx = (LLVMContext arch -> TypeContext)
-> (LLVMContext arch -> TypeContext -> LLVMContext arch)
-> Lens
     (LLVMContext arch) (LLVMContext arch) TypeContext TypeContext
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMContext arch -> TypeContext
forall (arch :: LLVMArch). LLVMContext arch -> TypeContext
_llvmTypeCtx (\LLVMContext arch
s TypeContext
v -> LLVMContext arch
s{ _llvmTypeCtx = v })

mkLLVMContext :: GlobalVar Mem
              -> L.Module
              -> IO (Some LLVMContext)
mkLLVMContext :: GlobalVar Mem -> Module -> IO (Some LLVMContext)
mkLLVMContext GlobalVar Mem
mvar Module
m = do
  let ([Doc Void]
errs, TypeContext
typeCtx) = Module -> ([Doc Void], TypeContext)
forall ann. Module -> ([Doc ann], TypeContext)
typeContextFromModule Module
m
  Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
unless ([Doc Void] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [Doc Void]
errs) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
    Doc Void -> [Doc Void] -> IO ()
forall a. Doc Void -> [Doc Void] -> a
malformedLLVMModule Doc Void
"Failed to construct LLVM type context" [Doc Void]
errs
  let dl :: DataLayout
dl = TypeContext -> DataLayout
llvmDataLayout TypeContext
typeCtx

  case Natural -> Some NatRepr
mkNatRepr (DataLayout -> Natural
ptrBitwidth DataLayout
dl) of
    Some (NatRepr x
wptr :: NatRepr wptr) | Just LeqProof 16 x
LeqProof <- NatRepr 16 -> NatRepr x -> Maybe (LeqProof 16 x)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16) NatRepr x
wptr ->
      NatRepr x
-> (HasPtrWidth x => IO (Some LLVMContext))
-> IO (Some LLVMContext)
forall (w :: Natural) a.
(16 <= w) =>
NatRepr w -> (HasPtrWidth w => a) -> a
withPtrWidth NatRepr x
wptr ((HasPtrWidth x => IO (Some LLVMContext)) -> IO (Some LLVMContext))
-> (HasPtrWidth x => IO (Some LLVMContext))
-> IO (Some LLVMContext)
forall a b. (a -> b) -> a -> b
$
        do let archRepr :: ArchRepr ('X86 x)
archRepr = NatRepr x -> ArchRepr ('X86 x)
forall (w :: Natural). NatRepr w -> ArchRepr ('X86 w)
X86Repr NatRepr x
wptr -- FIXME! we should select the architecture based on
                                       -- the target triple, but llvm-pretty doesn't capture this
                                       -- currently.
           let ctx :: LLVMContext (X86 wptr)
               ctx :: LLVMContext ('X86 x)
ctx = LLVMContext
                     { llvmArch :: ArchRepr ('X86 x)
llvmArch     = ArchRepr ('X86 x)
archRepr
                     , llvmMemVar :: GlobalVar Mem
llvmMemVar   = GlobalVar Mem
mvar
                     , llvmPtrWidth :: forall a.
((16 <= ArchWidth ('X86 x)) => NatRepr (ArchWidth ('X86 x)) -> a)
-> a
llvmPtrWidth = \(16 <= ArchWidth ('X86 x)) => NatRepr (ArchWidth ('X86 x)) -> a
x -> (16 <= ArchWidth ('X86 x)) => NatRepr (ArchWidth ('X86 x)) -> a
NatRepr (ArchWidth ('X86 x)) -> a
x NatRepr x
NatRepr (ArchWidth ('X86 x))
wptr
                     , _llvmTypeCtx :: TypeContext
_llvmTypeCtx = TypeContext
typeCtx
                     , llvmGlobalAliases :: Map Symbol (Set GlobalAlias)
llvmGlobalAliases = Map Symbol (Set GlobalAlias)
forall a. Monoid a => a
mempty   -- these are computed later
                     , llvmFunctionAliases :: Map Symbol (Set GlobalAlias)
llvmFunctionAliases = Map Symbol (Set GlobalAlias)
forall a. Monoid a => a
mempty -- these are computed later
                     }
           Some LLVMContext -> IO (Some LLVMContext)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMContext ('X86 x) -> Some LLVMContext
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some LLVMContext ('X86 x)
ctx)
    Some NatRepr
_ ->
      [Char] -> IO (Some LLVMContext)
forall a. [Char] -> IO a
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char]
"Cannot load LLVM bitcode file with illegal pointer width: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bytes -> [Char]
forall a. Show a => a -> [Char]
show (DataLayout
dlDataLayout -> Getting Bytes DataLayout Bytes -> Bytes
forall s a. s -> Getting a s a -> a
^.Getting Bytes DataLayout Bytes
Lens' DataLayout Bytes
ptrSize))


-- | A monad providing state and continuations for translating LLVM expressions
-- to CFGs.
type LLVMGenerator s arch ret a =
  (?lc :: TypeContext, HasPtrWidth (ArchWidth arch)) =>
    Generator LLVM s (LLVMState arch) ret IO a

-- | @LLVMGenerator@ without the constraint, can be nested further inside monads.
type LLVMGenerator' s arch ret =
  Generator LLVM s (LLVMState arch) ret IO


-- LLVMState

getMemVar :: LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar :: forall s (arch :: LLVMArch) (reg :: CrucibleType).
LLVMGenerator s arch reg (GlobalVar Mem)
getMemVar = LLVMContext arch -> GlobalVar Mem
forall (arch :: LLVMArch). LLVMContext arch -> GlobalVar Mem
llvmMemVar (LLVMContext arch -> GlobalVar Mem)
-> (LLVMState arch s -> LLVMContext arch)
-> LLVMState arch s
-> GlobalVar Mem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LLVMState arch s -> LLVMContext arch
forall (arch :: LLVMArch) s. LLVMState arch s -> LLVMContext arch
llvmContext (LLVMState arch s -> GlobalVar Mem)
-> Generator LLVM s (LLVMState arch) reg IO (LLVMState arch s)
-> Generator LLVM s (LLVMState arch) reg IO (GlobalVar Mem)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Generator LLVM s (LLVMState arch) reg IO (LLVMState arch s)
forall s (m :: Type -> Type). MonadState s m => m s
get

-- | Maps identifiers to an associated register or defined expression.
type IdentMap s = Map L.Ident (Either (Some (Reg s)) (Some (Atom s)))

-- | A warning generated during translation
data LLVMTranslationWarning =
  LLVMTranslationWarning
    L.Symbol  -- ^ Function name in which the warning was generated
    Position  -- ^ Source position where the warning was generated
    Text      -- ^ Description of the warning

data LLVMState arch s
   = LLVMState
   { -- | Map from identifiers to associated register shape
     forall (arch :: LLVMArch) s. LLVMState arch s -> IdentMap s
_identMap :: !(IdentMap s)
   , forall (arch :: LLVMArch) s. LLVMState arch s -> LLVMBlockInfoMap s
_blockInfoMap :: !(LLVMBlockInfoMap s)
   , forall (arch :: LLVMArch) s. LLVMState arch s -> LLVMContext arch
llvmContext :: LLVMContext arch
   , forall (arch :: LLVMArch) s.
LLVMState arch s -> IORef [LLVMTranslationWarning]
_translationWarnings :: IORef [LLVMTranslationWarning]
   , forall (arch :: LLVMArch) s. LLVMState arch s -> Symbol
_functionSymbol :: L.Symbol
   }

identMap :: Lens' (LLVMState arch s) (IdentMap s)
identMap :: forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(IdentMap s -> f (IdentMap s))
-> LLVMState arch s -> f (LLVMState arch s)
identMap = (LLVMState arch s -> IdentMap s)
-> (LLVMState arch s -> IdentMap s -> LLVMState arch s)
-> Lens
     (LLVMState arch s) (LLVMState arch s) (IdentMap s) (IdentMap s)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMState arch s -> IdentMap s
forall (arch :: LLVMArch) s. LLVMState arch s -> IdentMap s
_identMap (\LLVMState arch s
s IdentMap s
v -> LLVMState arch s
s { _identMap = v })

blockInfoMap :: Lens' (LLVMState arch s) (LLVMBlockInfoMap s)
blockInfoMap :: forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(LLVMBlockInfoMap s -> f (LLVMBlockInfoMap s))
-> LLVMState arch s -> f (LLVMState arch s)
blockInfoMap = (LLVMState arch s -> LLVMBlockInfoMap s)
-> (LLVMState arch s -> LLVMBlockInfoMap s -> LLVMState arch s)
-> Lens
     (LLVMState arch s)
     (LLVMState arch s)
     (LLVMBlockInfoMap s)
     (LLVMBlockInfoMap s)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMState arch s -> LLVMBlockInfoMap s
forall (arch :: LLVMArch) s. LLVMState arch s -> LLVMBlockInfoMap s
_blockInfoMap (\LLVMState arch s
s LLVMBlockInfoMap s
v -> LLVMState arch s
s { _blockInfoMap = v })

translationWarnings :: Lens' (LLVMState arch s) (IORef [LLVMTranslationWarning])
translationWarnings :: forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(IORef [LLVMTranslationWarning]
 -> f (IORef [LLVMTranslationWarning]))
-> LLVMState arch s -> f (LLVMState arch s)
translationWarnings = (LLVMState arch s -> IORef [LLVMTranslationWarning])
-> (LLVMState arch s
    -> IORef [LLVMTranslationWarning] -> LLVMState arch s)
-> Lens
     (LLVMState arch s)
     (LLVMState arch s)
     (IORef [LLVMTranslationWarning])
     (IORef [LLVMTranslationWarning])
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMState arch s -> IORef [LLVMTranslationWarning]
forall (arch :: LLVMArch) s.
LLVMState arch s -> IORef [LLVMTranslationWarning]
_translationWarnings (\LLVMState arch s
s IORef [LLVMTranslationWarning]
v -> LLVMState arch s
s { _translationWarnings = v })

functionSymbol :: Lens' (LLVMState arch s) L.Symbol
functionSymbol :: forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(Symbol -> f Symbol) -> LLVMState arch s -> f (LLVMState arch s)
functionSymbol = (LLVMState arch s -> Symbol)
-> (LLVMState arch s -> Symbol -> LLVMState arch s)
-> Lens (LLVMState arch s) (LLVMState arch s) Symbol Symbol
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens LLVMState arch s -> Symbol
forall (arch :: LLVMArch) s. LLVMState arch s -> Symbol
_functionSymbol (\LLVMState arch s
s Symbol
v -> LLVMState arch s
s{ _functionSymbol = v })

addWarning :: Text -> LLVMGenerator s arch ret ()
addWarning :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
Text -> LLVMGenerator s arch ret ()
addWarning Text
warn =
  do IORef [LLVMTranslationWarning]
r <- Getting
  (IORef [LLVMTranslationWarning])
  (LLVMState arch s)
  (IORef [LLVMTranslationWarning])
-> Generator
     LLVM s (LLVMState arch) ret IO (IORef [LLVMTranslationWarning])
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting
  (IORef [LLVMTranslationWarning])
  (LLVMState arch s)
  (IORef [LLVMTranslationWarning])
forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(IORef [LLVMTranslationWarning]
 -> f (IORef [LLVMTranslationWarning]))
-> LLVMState arch s -> f (LLVMState arch s)
translationWarnings
     Symbol
s <- Getting Symbol (LLVMState arch s) Symbol
-> Generator LLVM s (LLVMState arch) ret IO Symbol
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting Symbol (LLVMState arch s) Symbol
forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(Symbol -> f Symbol) -> LLVMState arch s -> f (LLVMState arch s)
functionSymbol
     Position
p <- Generator LLVM s (LLVMState arch) ret IO Position
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
       (m :: Type -> Type).
Generator ext s t ret m Position
getPosition
     IO () -> Generator LLVM s (LLVMState arch) ret IO ()
forall a. IO a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IORef [LLVMTranslationWarning]
-> ([LLVMTranslationWarning] -> [LLVMTranslationWarning]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [LLVMTranslationWarning]
r ((Symbol -> Position -> Text -> LLVMTranslationWarning
LLVMTranslationWarning Symbol
s Position
p Text
warn)LLVMTranslationWarning
-> [LLVMTranslationWarning] -> [LLVMTranslationWarning]
forall a. a -> [a] -> [a]
:))


-- | Given a list of LLVM formal parameters and a corresponding crucible
-- register assignment, build an IdentMap mapping LLVM identifiers to
-- corresponding crucible registers.
buildIdentMap :: (?lc :: TypeContext, HasPtrWidth wptr)
              => [L.Typed L.Ident]
              -> Bool -- ^ varargs
              -> CtxRepr ctx
              -> Ctx.Assignment (Atom s) ctx
              -> IdentMap s
              -> IdentMap s
buildIdentMap :: forall (wptr :: Natural) (ctx :: Ctx CrucibleType) s.
(?lc::TypeContext, HasPtrWidth wptr) =>
[Typed Ident]
-> Bool
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> IdentMap s
-> IdentMap s
buildIdentMap [Typed Ident]
ts Bool
True CtxRepr ctx
ctx Assignment (Atom s) ctx
asgn IdentMap s
m =
  -- Vararg functions are translated as taking a vector of extra arguments
  TypeRepr ('VectorType 'AnyType)
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall {ctx' :: Ctx CrucibleType}.
    Some (Atom s)
    -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> IdentMap s)
-> IdentMap s
forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) s a.
TypeRepr tp
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall (ctx' :: Ctx CrucibleType).
    Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a)
-> a
packBase (TypeRepr 'AnyType -> TypeRepr ('VectorType 'AnyType)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr 'AnyType
AnyRepr) CtxRepr ctx
ctx Assignment (Atom s) ctx
asgn ((forall {ctx' :: Ctx CrucibleType}.
  Some (Atom s)
  -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> IdentMap s)
 -> IdentMap s)
-> (forall {ctx' :: Ctx CrucibleType}.
    Some (Atom s)
    -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> IdentMap s)
-> IdentMap s
forall a b. (a -> b) -> a -> b
$ \Some (Atom s)
_x CtxRepr ctx'
ctx' Assignment (Atom s) ctx'
asgn' ->
    [Typed Ident]
-> Bool
-> CtxRepr ctx'
-> Assignment (Atom s) ctx'
-> IdentMap s
-> IdentMap s
forall (wptr :: Natural) (ctx :: Ctx CrucibleType) s.
(?lc::TypeContext, HasPtrWidth wptr) =>
[Typed Ident]
-> Bool
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> IdentMap s
-> IdentMap s
buildIdentMap [Typed Ident]
ts Bool
False CtxRepr ctx'
ctx' Assignment (Atom s) ctx'
asgn' IdentMap s
m
buildIdentMap [] Bool
_ CtxRepr ctx
ctx Assignment (Atom s) ctx
_ IdentMap s
m
  | CtxRepr ctx -> Bool
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Bool
Ctx.null CtxRepr ctx
ctx = IdentMap s
m
  | Bool
otherwise =
      [Char] -> [[Char]] -> IdentMap s
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"crucible-llvm:Translation.buildIdentMap"
      [ [Char]
"buildIdentMap: passed arguments do not match LLVM input signature" ]
buildIdentMap (Typed Ident
ti:[Typed Ident]
ts) Bool
_ CtxRepr ctx
ctx Assignment (Atom s) ctx
asgn IdentMap s
m = do
  let ty :: MemType
ty = case Type -> Either [Char] MemType
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError [Char] m) =>
Type -> m MemType
liftMemType (Typed Ident -> Type
forall a. Typed a -> Type
L.typedType Typed Ident
ti) of
             Right MemType
t -> MemType
t
             Left [Char]
err -> [Char] -> [[Char]] -> MemType
forall a. HasCallStack => [Char] -> [[Char]] -> a
panic [Char]
"crucible-llvm:Translation.buildIdentMap"
                         [ [Char]
"Error attempting to lift type " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Typed Ident -> [Char]
forall a. Show a => a -> [Char]
show Typed Ident
ti
                         , [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
err
                         ]
  MemType
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall {ctx' :: Ctx CrucibleType}.
    Some (Atom s)
    -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> IdentMap s)
-> IdentMap s
forall (wptr :: Natural) (ctx :: Ctx CrucibleType) s a.
HasPtrWidth wptr =>
MemType
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall (ctx' :: Ctx CrucibleType).
    Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a)
-> a
packType MemType
ty CtxRepr ctx
ctx Assignment (Atom s) ctx
asgn ((forall {ctx' :: Ctx CrucibleType}.
  Some (Atom s)
  -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> IdentMap s)
 -> IdentMap s)
-> (forall {ctx' :: Ctx CrucibleType}.
    Some (Atom s)
    -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> IdentMap s)
-> IdentMap s
forall a b. (a -> b) -> a -> b
$ \Some (Atom s)
x CtxRepr ctx'
ctx' Assignment (Atom s) ctx'
asgn' ->
     [Typed Ident]
-> Bool
-> CtxRepr ctx'
-> Assignment (Atom s) ctx'
-> IdentMap s
-> IdentMap s
forall (wptr :: Natural) (ctx :: Ctx CrucibleType) s.
(?lc::TypeContext, HasPtrWidth wptr) =>
[Typed Ident]
-> Bool
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> IdentMap s
-> IdentMap s
buildIdentMap [Typed Ident]
ts Bool
False CtxRepr ctx'
ctx' Assignment (Atom s) ctx'
asgn' (Ident
-> Either (Some (Reg s)) (Some (Atom s))
-> IdentMap s
-> IdentMap s
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Typed Ident -> Ident
forall a. Typed a -> a
L.typedValue Typed Ident
ti) (Some (Atom s) -> Either (Some (Reg s)) (Some (Atom s))
forall a b. b -> Either a b
Right Some (Atom s)
x) IdentMap s
m)

-- | Build the initial LLVM generator state upon entry to to the entry point of a function.
initialState :: (?lc :: TypeContext, HasPtrWidth wptr)
             => L.Define
             -> LLVMContext arch
             -> CtxRepr args
             -> Ctx.Assignment (Atom s) args
             -> IORef [LLVMTranslationWarning]
             -> LLVMState arch s
initialState :: forall (wptr :: Natural) (arch :: LLVMArch)
       (args :: Ctx CrucibleType) s.
(?lc::TypeContext, HasPtrWidth wptr) =>
Define
-> LLVMContext arch
-> CtxRepr args
-> Assignment (Atom s) args
-> IORef [LLVMTranslationWarning]
-> LLVMState arch s
initialState Define
d LLVMContext arch
llvmctx CtxRepr args
args Assignment (Atom s) args
asgn IORef [LLVMTranslationWarning]
warnRef =
   let m :: IdentMap s
m = [Typed Ident]
-> Bool
-> CtxRepr args
-> Assignment (Atom s) args
-> IdentMap s
-> IdentMap s
forall (wptr :: Natural) (ctx :: Ctx CrucibleType) s.
(?lc::TypeContext, HasPtrWidth wptr) =>
[Typed Ident]
-> Bool
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> IdentMap s
-> IdentMap s
buildIdentMap ([Typed Ident] -> [Typed Ident]
forall a. [a] -> [a]
reverse (Define -> [Typed Ident]
L.defArgs Define
d)) (Define -> Bool
L.defVarArgs Define
d) CtxRepr args
args Assignment (Atom s) args
asgn IdentMap s
forall k a. Map k a
Map.empty in
     LLVMState { _identMap :: IdentMap s
_identMap = IdentMap s
m
               , _blockInfoMap :: LLVMBlockInfoMap s
_blockInfoMap = LLVMBlockInfoMap s
forall k a. Map k a
Map.empty
               , llvmContext :: LLVMContext arch
llvmContext = LLVMContext arch
llvmctx
               , _translationWarnings :: IORef [LLVMTranslationWarning]
_translationWarnings = IORef [LLVMTranslationWarning]
warnRef
               , _functionSymbol :: Symbol
_functionSymbol = Define -> Symbol
L.defName Define
d
               }

-- | Given an LLVM type and a type context and a register assignment,
--   peel off the rightmost register from the assignment, which is
--   expected to match the given LLVM type.  Pass the register and
--   the remaining type and register context to the given continuation.
--
--   This procedure is used to set up the initial state of the
--   registers at the entry point of a function.
packType :: HasPtrWidth wptr
         => MemType
         -> CtxRepr ctx
         -> Ctx.Assignment (Atom s) ctx
         -> (forall ctx'. Some (Atom s) -> CtxRepr ctx' -> Ctx.Assignment (Atom s) ctx' -> a)
         -> a
packType :: forall (wptr :: Natural) (ctx :: Ctx CrucibleType) s a.
HasPtrWidth wptr =>
MemType
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall (ctx' :: Ctx CrucibleType).
    Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a)
-> a
packType MemType
tp CtxRepr ctx
ctx Assignment (Atom s) ctx
asgn forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a
k =
   MemType -> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp ((forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a)
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
repr ->
     TypeRepr tp
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall (ctx' :: Ctx CrucibleType).
    Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a)
-> a
forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) s a.
TypeRepr tp
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall (ctx' :: Ctx CrucibleType).
    Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a)
-> a
packBase TypeRepr tp
repr CtxRepr ctx
ctx Assignment (Atom s) ctx
asgn Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a
forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a
k

packBase
    :: TypeRepr tp
    -> CtxRepr ctx
    -> Ctx.Assignment (Atom s) ctx
    -> (forall ctx'. Some (Atom s) -> CtxRepr ctx' -> Ctx.Assignment (Atom s) ctx' -> a)
    -> a
packBase :: forall (tp :: CrucibleType) (ctx :: Ctx CrucibleType) s a.
TypeRepr tp
-> CtxRepr ctx
-> Assignment (Atom s) ctx
-> (forall (ctx' :: Ctx CrucibleType).
    Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a)
-> a
packBase TypeRepr tp
ctp CtxRepr ctx
ctx0 Assignment (Atom s) ctx
asgn forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a
k =
  case CtxRepr ctx
ctx0 of
    Assignment TypeRepr ctx
ctx' Ctx.:> TypeRepr tp
ctp' ->
      case TypeRepr tp -> TypeRepr tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr tp
ctp TypeRepr tp
ctp' of
        Maybe (tp :~: tp)
Nothing -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [[Char]
"crucible type mismatch",TypeRepr tp -> [Char]
forall a. Show a => a -> [Char]
show TypeRepr tp
ctp,TypeRepr tp -> [Char]
forall a. Show a => a -> [Char]
show TypeRepr tp
ctp']
        Just tp :~: tp
Refl ->
          let asgn' :: Assignment (Atom s) ctx
asgn' = Assignment (Atom s) (ctx '::> tp) -> Assignment (Atom s) ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f (ctx '::> tp) -> Assignment f ctx
Ctx.init Assignment (Atom s) ctx
Assignment (Atom s) (ctx '::> tp)
asgn
              idx :: Index (ctx '::> tp) tp
idx   = Size ctx -> Index (ctx '::> tp) tp
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
Ctx.nextIndex (Assignment (Atom s) ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment (Atom s) ctx
asgn')
           in Some (Atom s)
-> Assignment TypeRepr ctx -> Assignment (Atom s) ctx -> a
forall (ctx' :: Ctx CrucibleType).
Some (Atom s) -> CtxRepr ctx' -> Assignment (Atom s) ctx' -> a
k (Atom s tp -> Some (Atom s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Assignment (Atom s) ctx
asgn Assignment (Atom s) ctx -> Index ctx tp -> Atom s tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
Index (ctx '::> tp) tp
idx))
                Assignment TypeRepr ctx
ctx'
                Assignment (Atom s) ctx
asgn'
    CtxRepr ctx
_ -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"packType: ran out of actual arguments!"