{-# 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(..))
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)
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)
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_)
extractCtors :: L.Value -> Maybe Ctor
Value
val =
case Value
val of
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
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
Just (L.ValArray Type' Ident
_ty [Value]
vs) -> do
[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)
[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')
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 :: (Ctor -> Bool)
-> 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)
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)
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
callCtorsCFG :: forall arch wptr. (HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr)
=> (Ctor -> Bool)
-> 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