------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.Ctors
-- Description      : Extract and manipulate the @llvm.global_ctors@ variable
-- Copyright        : (c) Galois, Inc 2018
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveDataTypeable    #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE ImplicitParams        #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeOperators         #-}

module Lang.Crucible.LLVM.Ctors
  ( Ctor(..)
  , globalCtors
  , callCtors
  , callAllCtors
  , callCtorsCFG
  ) where

import           Data.Data (Data)
import           Data.IORef (newIORef)
import           Data.String(fromString)
import           Data.Typeable (Typeable)
import qualified Data.Text as Text
import           GHC.Generics (Generic)
import           Data.Parameterized.Nonce

import           Control.Monad (forM, forM_)
import           Control.Monad.Except (MonadError(..))
import           Data.List (find, sortBy)
import           Data.Ord (comparing, Down(..))
import           Data.Maybe (fromMaybe)

import qualified Text.LLVM.AST as L

import           Lang.Crucible.LLVM.Translation.Instruction (callOrdinaryFunction)
import           Lang.Crucible.LLVM.Translation.Monad (LLVMGenerator, LLVMState(..))

-- Generating CFGs

import           Data.Map.Strict (empty)
import           Data.Text (Text)
import           GHC.TypeNats

import qualified Data.Parameterized.Context.Unsafe as Ctx

import           What4.FunctionName (functionNameFromText)
import           What4.ProgramLoc (Position(InternalPos))

import qualified Lang.Crucible.CFG.Core as Core
import           Lang.Crucible.CFG.Expr (App(EmptyApp))
import           Lang.Crucible.CFG.Generator (FunctionDef, defineFunction)
import           Lang.Crucible.CFG.Reg (Expr(App))
import qualified Lang.Crucible.CFG.Reg as Reg
import           Lang.Crucible.CFG.SSAConversion (toSSA)
import           Lang.Crucible.FunctionHandle (HandleAllocator, mkHandle')
import           Lang.Crucible.Types (UnitType, TypeRepr(UnitRepr))
import           Lang.Crucible.LLVM.Extension (LLVM, ArchWidth)
import           Lang.Crucible.LLVM.Translation.Monad (LLVMContext, _llvmTypeCtx, malformedLLVMModule)
import           Lang.Crucible.LLVM.Types (HasPtrWidth)

{- Example:

@llvm.global_ctors = appending global [3 x { i32, void ()*, i8* }] [{ i32, void ()*, i8* } { i32 65535, void ()* @_GLOBAL__sub_I_HkdfTest.cpp, i8* null }, { i32, void ()*, i8* } { i32 65535, void ()* @_GLOBAL__sub_I_gtest_all.cc, i8* null }, { i32, void ()*, i8* } { i32 65535, void ()* @_GLOBAL__sub_I_iostream.cpp, i8* null }]

-}

-- | A representation of well-typed inhabitants of the @llvm.global_ctors@ array
--
-- See https://llvm.org/docs/LangRef.html#the-llvm-global-ctors-global-variable
data Ctor = Ctor
  { Ctor -> Integer
ctorPriority :: Integer
  , Ctor -> Symbol
ctorFunction :: L.Symbol
  , Ctor -> Maybe Symbol
ctorData     :: Maybe L.Symbol
  } deriving (Typeable Ctor
Typeable Ctor =>
(forall (c :: Type -> Type).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Ctor -> c Ctor)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Ctor)
-> (Ctor -> Constr)
-> (Ctor -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Ctor))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ctor))
-> ((forall b. Data b => b -> b) -> Ctor -> Ctor)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ctor -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctor -> r)
-> (forall u. (forall d. Data d => d -> u) -> Ctor -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Ctor -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> Ctor -> m Ctor)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ctor -> m Ctor)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ctor -> m Ctor)
-> Data Ctor
Ctor -> Constr
Ctor -> DataType
(forall b. Data b => b -> b) -> Ctor -> Ctor
forall a.
Typeable a =>
(forall (c :: Type -> Type).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Ctor -> u
forall u. (forall d. Data d => d -> u) -> Ctor -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ctor -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctor -> r
forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Ctor -> m Ctor
forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ctor -> m Ctor
forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ctor
forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ctor -> c Ctor
forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ctor)
forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ctor)
$cgfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ctor -> c Ctor
gfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ctor -> c Ctor
$cgunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ctor
gunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Ctor
$ctoConstr :: Ctor -> Constr
toConstr :: Ctor -> Constr
$cdataTypeOf :: Ctor -> DataType
dataTypeOf :: Ctor -> DataType
$cdataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ctor)
dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Ctor)
$cdataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ctor)
dataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ctor)
$cgmapT :: (forall b. Data b => b -> b) -> Ctor -> Ctor
gmapT :: (forall b. Data b => b -> b) -> Ctor -> Ctor
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ctor -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ctor -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctor -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ctor -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Ctor -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Ctor -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ctor -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ctor -> u
$cgmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Ctor -> m Ctor
gmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Ctor -> m Ctor
$cgmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ctor -> m Ctor
gmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ctor -> m Ctor
$cgmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ctor -> m Ctor
gmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ctor -> m Ctor
Data, Ctor -> Ctor -> Bool
(Ctor -> Ctor -> Bool) -> (Ctor -> Ctor -> Bool) -> Eq Ctor
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Ctor -> Ctor -> Bool
== :: Ctor -> Ctor -> Bool
$c/= :: Ctor -> Ctor -> Bool
/= :: Ctor -> Ctor -> Bool
Eq, (forall x. Ctor -> Rep Ctor x)
-> (forall x. Rep Ctor x -> Ctor) -> Generic Ctor
forall x. Rep Ctor x -> Ctor
forall x. Ctor -> Rep Ctor x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Ctor -> Rep Ctor x
from :: forall x. Ctor -> Rep Ctor x
$cto :: forall x. Rep Ctor x -> Ctor
to :: forall x. Rep Ctor x -> Ctor
Generic, Eq Ctor
Eq Ctor =>
(Ctor -> Ctor -> Ordering)
-> (Ctor -> Ctor -> Bool)
-> (Ctor -> Ctor -> Bool)
-> (Ctor -> Ctor -> Bool)
-> (Ctor -> Ctor -> Bool)
-> (Ctor -> Ctor -> Ctor)
-> (Ctor -> Ctor -> Ctor)
-> Ord Ctor
Ctor -> Ctor -> Bool
Ctor -> Ctor -> Ordering
Ctor -> Ctor -> Ctor
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 :: Ctor -> Ctor -> Ordering
compare :: Ctor -> Ctor -> Ordering
$c< :: Ctor -> Ctor -> Bool
< :: Ctor -> Ctor -> Bool
$c<= :: Ctor -> Ctor -> Bool
<= :: Ctor -> Ctor -> Bool
$c> :: Ctor -> Ctor -> Bool
> :: Ctor -> Ctor -> Bool
$c>= :: Ctor -> Ctor -> Bool
>= :: Ctor -> Ctor -> Bool
$cmax :: Ctor -> Ctor -> Ctor
max :: Ctor -> Ctor -> Ctor
$cmin :: Ctor -> Ctor -> Ctor
min :: Ctor -> Ctor -> Ctor
Ord, Int -> Ctor -> ShowS
[Ctor] -> ShowS
Ctor -> String
(Int -> Ctor -> ShowS)
-> (Ctor -> String) -> ([Ctor] -> ShowS) -> Show Ctor
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Ctor -> ShowS
showsPrec :: Int -> Ctor -> ShowS
$cshow :: Ctor -> String
show :: Ctor -> String
$cshowList :: [Ctor] -> ShowS
showList :: [Ctor] -> ShowS
Show, Typeable)

-- | Get the global variable representing @llvm.global_ctors@.
getGlobalCtorsGlobal :: L.Module -> Maybe L.Global
getGlobalCtorsGlobal :: Module -> Maybe Global
getGlobalCtorsGlobal Module
mod_ =
  let symb :: Symbol
symb = String -> Symbol
L.Symbol String
"llvm.global_ctors"
  in (Global -> Bool) -> [Global] -> Maybe Global
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
find (\Global
x -> Global -> Symbol
L.globalSym Global
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
symb) (Module -> [Global]
L.modGlobals Module
mod_)

-- | Unpack a @ctors@ value of type @{ i32, void ()*, i8* }@ from the AST
extractCtors :: L.Value -> Maybe Ctor
extractCtors :: Value -> Maybe Ctor
extractCtors Value
val =
  case Value
val of
    -- This is permissive about the integer widths... No reason to get caught up.
    L.ValStruct [ L.Typed (L.PrimType (L.Integer Word32
_w0)) (L.ValInteger Integer
priority)
                , L.Typed (L.PtrTo (L.FunTy (L.PrimType PrimType
L.Void) [] Bool
_bool)) (L.ValSymbol Symbol
symb)
                , L.Typed (L.PtrTo (L.PrimType (L.Integer Word32
_w1))) Value
data0_
                ] -> Ctor -> Maybe Ctor
forall a. a -> Maybe a
Just (Ctor -> Maybe Ctor)
-> (Maybe Symbol -> Ctor) -> Maybe Symbol -> Maybe Ctor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Symbol -> Maybe Symbol -> Ctor
Ctor Integer
priority Symbol
symb (Maybe Symbol -> Maybe Ctor) -> Maybe Symbol -> Maybe Ctor
forall a b. (a -> b) -> a -> b
$
                       case Value
data0_ of
                         L.ValSymbol Symbol
data_ -> Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
data_
                         Value
_                 -> Maybe Symbol
forall a. Maybe a
Nothing
    Value
_ -> Maybe Ctor
forall a. Maybe a
Nothing

-- | Unpack and sort the values in @llvm.global_ctors@ by priority
globalCtors :: (MonadError String m)
            => L.Module
            -> m [Ctor]
globalCtors :: forall (m :: Type -> Type).
MonadError String m =>
Module -> m [Ctor]
globalCtors Module
mod_ =
  case Module -> Maybe Global
getGlobalCtorsGlobal Module
mod_ Maybe Global -> (Global -> Maybe Value) -> Maybe Value
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Global -> Maybe Value
L.globalValue of -- in the Maybe monad
    Just (L.ValArray Type' Ident
_ty [Value]
vs) -> do

      -- Assert that each value is of the expected type.
      [Ctor]
vs' <- [Value] -> (Value -> m Ctor) -> m [Ctor]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Value]
vs ((Value -> m Ctor) -> m [Ctor]) -> (Value -> m Ctor) -> m [Ctor]
forall a b. (a -> b) -> a -> b
$ \Value
v ->
        m Ctor -> Maybe (m Ctor) -> m Ctor
forall a. a -> Maybe a -> a
fromMaybe
          (String -> m Ctor
forall a. String -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> m Ctor) -> String -> m Ctor
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ String
"Ill-typed value in llvm.global_ctors: "
                                  , Value -> String
forall a. Show a => a -> String
show Value
v
                                  ])
          (Ctor -> m Ctor
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Ctor -> m Ctor) -> Maybe Ctor -> Maybe (m Ctor)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Value -> Maybe Ctor
extractCtors Value
v)

      -- Sort the values by priority, highest to lowest.
      [Ctor] -> m [Ctor]
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((Ctor -> Ctor -> Ordering) -> [Ctor] -> [Ctor]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Ctor -> Down Integer) -> Ctor -> Ctor -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Integer -> Down Integer
forall a. a -> Down a
Down (Integer -> Down Integer)
-> (Ctor -> Integer) -> Ctor -> Down Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctor -> Integer
ctorPriority)) [Ctor]
vs')

    -- @llvm.ctors value not found, assume there are no global_ctors to run
    Maybe Value
Nothing -> [Ctor] -> m [Ctor]
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return []

    Just Value
v  -> String -> m [Ctor]
forall a. String -> m a
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> m [Ctor]) -> String -> m [Ctor]
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
      [ String
"llvm.global_ctors wasn't an array"
      , String
"Value: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value -> String
forall a. Show a => a -> String
show Value
v
      ]

----------------------------------------------------------------------
-- ** callCtors

-- | Call some or all of the functions in @llvm.global_ctors@
callCtors :: (Ctor -> Bool) -- ^ Filter function
          -> L.Module
          -> LLVMGenerator s arch UnitType (Expr LLVM s UnitType)
callCtors :: forall s (arch :: LLVMArch).
(Ctor -> Bool)
-> Module -> LLVMGenerator s arch UnitType (Expr LLVM s UnitType)
callCtors Ctor -> Bool
select Module
mod_ = do
  let err :: String -> a
err String
msg = Doc Void -> [Doc Void] -> a
forall a. Doc Void -> [Doc Void] -> a
malformedLLVMModule Doc Void
"Error loading @llvm.global_ctors" [String -> Doc Void
forall a. IsString a => String -> a
fromString String
msg]
  let ty :: Type' ident
ty = Type' ident -> [Type' ident] -> Bool -> Type' ident
forall ident. Type' ident -> [Type' ident] -> Bool -> Type' ident
L.FunTy (PrimType -> Type' ident
forall ident. PrimType -> Type' ident
L.PrimType PrimType
L.Void) [] Bool
False

  [Ctor]
ctors <- (String -> Generator LLVM s (LLVMState arch) UnitType IO [Ctor])
-> ([Ctor] -> Generator LLVM s (LLVMState arch) UnitType IO [Ctor])
-> Either String [Ctor]
-> Generator LLVM s (LLVMState arch) UnitType IO [Ctor]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> Generator LLVM s (LLVMState arch) UnitType IO [Ctor]
forall {a}. String -> a
err ([Ctor] -> Generator LLVM s (LLVMState arch) UnitType IO [Ctor]
forall a. a -> Generator LLVM s (LLVMState arch) UnitType IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Ctor] -> Generator LLVM s (LLVMState arch) UnitType IO [Ctor])
-> ([Ctor] -> [Ctor])
-> [Ctor]
-> Generator LLVM s (LLVMState arch) UnitType IO [Ctor]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ctor -> Bool) -> [Ctor] -> [Ctor]
forall a. (a -> Bool) -> [a] -> [a]
filter Ctor -> Bool
select) (Module -> Either String [Ctor]
forall (m :: Type -> Type).
MonadError String m =>
Module -> m [Ctor]
globalCtors Module
mod_)
  [Ctor]
-> (Ctor -> Generator LLVM s (LLVMState arch) UnitType IO ())
-> Generator LLVM s (LLVMState arch) UnitType IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Ctor]
ctors ((Ctor -> Generator LLVM s (LLVMState arch) UnitType IO ())
 -> Generator LLVM s (LLVMState arch) UnitType IO ())
-> (Ctor -> Generator LLVM s (LLVMState arch) UnitType IO ())
-> Generator LLVM s (LLVMState arch) UnitType IO ()
forall a b. (a -> b) -> a -> b
$ \Ctor
ctor ->
    Maybe Instr
-> Bool
-> Type' Ident
-> Value
-> [Typed Value]
-> (LLVMExpr s arch -> LLVMGenerator s arch UnitType ())
-> LLVMGenerator s arch UnitType ()
forall s (arch :: LLVMArch) (ret :: CrucibleType).
Maybe Instr
-> Bool
-> Type' Ident
-> Value
-> [Typed Value]
-> (LLVMExpr s arch -> LLVMGenerator s arch ret ())
-> LLVMGenerator s arch ret ()
callOrdinaryFunction Maybe Instr
forall a. Maybe a
Nothing Bool
False Type' Ident
forall {ident}. Type' ident
ty (Symbol -> Value
forall lab. Symbol -> Value' lab
L.ValSymbol (Ctor -> Symbol
ctorFunction Ctor
ctor)) [] (\LLVMExpr s arch
_ -> () -> Generator LLVM s (LLVMState arch) UnitType IO ()
forall a. a -> Generator LLVM s (LLVMState arch) UnitType IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ())
  Expr LLVM s UnitType
-> Generator
     LLVM s (LLVMState arch) UnitType IO (Expr LLVM s UnitType)
forall a. a -> Generator LLVM s (LLVMState arch) UnitType IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (App LLVM (Expr LLVM s) UnitType -> Expr LLVM s UnitType
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App App LLVM (Expr LLVM s) UnitType
forall ext (f :: CrucibleType -> Type). App ext f UnitType
EmptyApp)

-- | Call each function in @llvm.global_ctors@ in order of decreasing priority
callAllCtors :: L.Module -> LLVMGenerator s arch UnitType (Expr LLVM s UnitType)
callAllCtors :: forall s (arch :: LLVMArch).
Module -> LLVMGenerator s arch UnitType (Expr LLVM s UnitType)
callAllCtors = (Ctor -> Bool)
-> Module -> LLVMGenerator s arch UnitType (Expr LLVM s UnitType)
forall s (arch :: LLVMArch).
(Ctor -> Bool)
-> Module -> LLVMGenerator s arch UnitType (Expr LLVM s UnitType)
callCtors (Bool -> Ctor -> Bool
forall a b. a -> b -> a
const Bool
True)

----------------------------------------------------------------------
-- ** callCtorsCFG

-- | Make a 'LLVMGenerator' into a CFG by making it a function with no arguments
-- that returns unit.
generatorToCFG :: forall arch wptr ret. (HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr)
               => Text
               -> HandleAllocator
               -> LLVMContext arch
               -> (forall s. LLVMGenerator s arch ret (Expr LLVM s ret))
               -> TypeRepr ret
               -> IO (Core.SomeCFG LLVM Core.EmptyCtx ret)
generatorToCFG :: forall (arch :: LLVMArch) (wptr :: Natural) (ret :: CrucibleType).
(HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr) =>
Text
-> HandleAllocator
-> LLVMContext arch
-> (forall s. LLVMGenerator s arch ret (Expr LLVM s ret))
-> TypeRepr ret
-> IO (SomeCFG LLVM EmptyCtx ret)
generatorToCFG Text
name HandleAllocator
halloc LLVMContext arch
llvmctx forall s. LLVMGenerator s arch ret (Expr LLVM s ret)
gen TypeRepr ret
ret = do
  IORef [LLVMTranslationWarning]
ref <- [LLVMTranslationWarning] -> IO (IORef [LLVMTranslationWarning])
forall a. a -> IO (IORef a)
newIORef []
  let ?lc = LLVMContext arch -> TypeContext
forall (arch :: LLVMArch). LLVMContext arch -> TypeContext
_llvmTypeCtx LLVMContext arch
llvmctx
  let def :: forall args. FunctionDef LLVM (LLVMState arch) args ret IO
      def :: forall (args :: Ctx CrucibleType) s.
Assignment (Atom s) args
-> (LLVMState arch s,
    Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s ret))
def Assignment (Atom s) args
_inputs = (LLVMState arch s
state, Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s ret)
forall s. LLVMGenerator s arch ret (Expr LLVM s ret)
gen)
        where state :: LLVMState arch s
state = LLVMState { _identMap :: IdentMap s
_identMap     = IdentMap s
forall k a. Map k a
empty
                                , _blockInfoMap :: LLVMBlockInfoMap s
_blockInfoMap = LLVMBlockInfoMap s
forall k a. Map k a
empty
                                , llvmContext :: LLVMContext arch
llvmContext   = LLVMContext arch
llvmctx
                                , _translationWarnings :: IORef [LLVMTranslationWarning]
_translationWarnings = IORef [LLVMTranslationWarning]
ref
                                , _functionSymbol :: Symbol
_functionSymbol = String -> Symbol
L.Symbol (Text -> String
Text.unpack Text
name)
                                }

  FnHandle EmptyCtx ret
hand <- HandleAllocator
-> FunctionName
-> Assignment TypeRepr EmptyCtx
-> TypeRepr ret
-> IO (FnHandle EmptyCtx ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
HandleAllocator
-> FunctionName
-> Assignment TypeRepr args
-> TypeRepr ret
-> IO (FnHandle args ret)
mkHandle' HandleAllocator
halloc (Text -> FunctionName
functionNameFromText Text
name) Assignment TypeRepr EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty TypeRepr ret
ret
  Some (NonceGenerator IO)
sng <- IO (Some (NonceGenerator IO))
newIONonceGenerator
  (Reg.SomeCFG CFG LLVM s EmptyCtx ret
g, []) <- Position
-> Some (NonceGenerator IO)
-> FnHandle EmptyCtx ret
-> FunctionDef LLVM (LLVMState arch) EmptyCtx ret IO
-> IO (SomeCFG LLVM EmptyCtx ret, [AnyCFG LLVM])
forall (m :: Type -> Type) ext (init :: Ctx CrucibleType)
       (ret :: CrucibleType) (t :: Type -> Type).
(Monad m, IsSyntaxExtension ext) =>
Position
-> Some (NonceGenerator m)
-> FnHandle init ret
-> FunctionDef ext t init ret m
-> m (SomeCFG ext init ret, [AnyCFG ext])
defineFunction Position
InternalPos Some (NonceGenerator IO)
sng FnHandle EmptyCtx ret
hand Assignment (Atom s) EmptyCtx
-> (LLVMState arch s,
    Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s ret))
FunctionDef LLVM (LLVMState arch) EmptyCtx ret IO
forall (args :: Ctx CrucibleType) s.
Assignment (Atom s) args
-> (LLVMState arch s,
    Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s ret))
def
  SomeCFG LLVM EmptyCtx ret -> IO (SomeCFG LLVM EmptyCtx ret)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SomeCFG LLVM EmptyCtx ret -> IO (SomeCFG LLVM EmptyCtx ret))
-> SomeCFG LLVM EmptyCtx ret -> IO (SomeCFG LLVM EmptyCtx ret)
forall a b. (a -> b) -> a -> b
$! CFG LLVM s EmptyCtx ret -> SomeCFG LLVM EmptyCtx ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
IsSyntaxExtension ext =>
CFG ext s init ret -> SomeCFG ext init ret
toSSA CFG LLVM s EmptyCtx ret
g

-- | Create a CFG that calls some of the functions in @llvm.global_ctors@.
callCtorsCFG :: forall arch wptr. (HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr)
             => (Ctor -> Bool) -- ^ Filter function
             -> L.Module
             -> HandleAllocator
             -> LLVMContext arch
             -> IO (Core.SomeCFG LLVM Core.EmptyCtx UnitType)
callCtorsCFG :: forall (arch :: LLVMArch) (wptr :: Natural).
(HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr) =>
(Ctor -> Bool)
-> Module
-> HandleAllocator
-> LLVMContext arch
-> IO (SomeCFG LLVM EmptyCtx UnitType)
callCtorsCFG Ctor -> Bool
select Module
mod_ HandleAllocator
halloc LLVMContext arch
llvmctx = do
  Text
-> HandleAllocator
-> LLVMContext arch
-> (forall s. LLVMGenerator s arch UnitType (Expr LLVM s UnitType))
-> TypeRepr UnitType
-> IO (SomeCFG LLVM EmptyCtx UnitType)
forall (arch :: LLVMArch) (wptr :: Natural) (ret :: CrucibleType).
(HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr) =>
Text
-> HandleAllocator
-> LLVMContext arch
-> (forall s. LLVMGenerator s arch ret (Expr LLVM s ret))
-> TypeRepr ret
-> IO (SomeCFG LLVM EmptyCtx ret)
generatorToCFG Text
"llvm_global_ctors" HandleAllocator
halloc LLVMContext arch
llvmctx ((Ctor -> Bool)
-> Module -> LLVMGenerator s arch UnitType (Expr LLVM s UnitType)
forall s (arch :: LLVMArch).
(Ctor -> Bool)
-> Module -> LLVMGenerator s arch UnitType (Expr LLVM s UnitType)
callCtors Ctor -> Bool
select Module
mod_) TypeRepr UnitType
UnitRepr