{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.LLVM.Translation
( ModuleTranslation
, getTranslatedCFG
, getTranslatedFnHandle
, transContext
, globalInitMap
, modTransDefs
, modTransModule
, modTransHalloc
, LLVMContext(..)
, llvmTypeCtx
, translateModule
, LLVMTranslationWarning(..)
, module Lang.Crucible.LLVM.Translation.Constant
, module Lang.Crucible.LLVM.Translation.Options
, module Lang.Crucible.LLVM.Translation.Types
) where
import Control.Lens hiding (op, (:>) )
import Control.Monad (foldM)
import Data.IORef (IORef, newIORef, readIORef, modifyIORef)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Maybe
import Data.String
import qualified Data.Text as Text
import Prettyprinter (pretty)
import qualified Text.LLVM.AST as L
import Data.Parameterized.NatRepr as NatRepr
import Data.Parameterized.Some
import Data.Parameterized.Nonce
import What4.FunctionName
import What4.ProgramLoc
import qualified Lang.Crucible.CFG.Core as C
import Lang.Crucible.CFG.Generator
import Lang.Crucible.CFG.SSAConversion( toSSA )
import Lang.Crucible.FunctionHandle
import Lang.Crucible.LLVM.Extension
import Lang.Crucible.LLVM.MemType
import Lang.Crucible.LLVM.Globals
import Lang.Crucible.LLVM.MemModel
import qualified Lang.Crucible.LLVM.PrettyPrint as LPP
import Lang.Crucible.LLVM.Translation.Aliases
import Lang.Crucible.LLVM.Translation.Constant
import Lang.Crucible.LLVM.Translation.Expr
import Lang.Crucible.LLVM.Translation.Monad
import Lang.Crucible.LLVM.Translation.Options
import Lang.Crucible.LLVM.Translation.Instruction
import Lang.Crucible.LLVM.Translation.Types
import Lang.Crucible.LLVM.TypeContext
import Lang.Crucible.Types
type ModuleCFGMap = Map L.Symbol CFGMapEntry
data CFGMapEntry
= TranslatedCFG L.Declare (C.AnyCFG LLVM)
| UntranslatedCFG L.Define SomeHandle
data ModuleTranslation arch
= ModuleTranslation
{ forall (arch :: LLVMArch).
ModuleTranslation arch -> IORef ModuleCFGMap
_cfgMap :: IORef ModuleCFGMap
, forall (arch :: LLVMArch).
ModuleTranslation arch -> LLVMContext arch
_transContext :: LLVMContext arch
, forall (arch :: LLVMArch).
ModuleTranslation arch -> GlobalInitializerMap
_globalInitMap :: GlobalInitializerMap
, forall (arch :: LLVMArch).
ModuleTranslation arch -> Nonce GlobalNonceGenerator arch
_modTransNonce :: !(Nonce GlobalNonceGenerator arch)
, forall (arch :: LLVMArch).
ModuleTranslation arch -> [(Declare, SomeHandle)]
_modTransDefs :: ![(L.Declare, SomeHandle)]
, forall (arch :: LLVMArch).
ModuleTranslation arch -> HandleAllocator
_modTransHalloc :: HandleAllocator
, forall (arch :: LLVMArch). ModuleTranslation arch -> Module
_modTransModule :: L.Module
, forall (arch :: LLVMArch).
ModuleTranslation arch -> TranslationOptions
_modTransOpts :: TranslationOptions
}
instance TestEquality ModuleTranslation where
testEquality :: forall (a :: LLVMArch) (b :: LLVMArch).
ModuleTranslation a -> ModuleTranslation b -> Maybe (a :~: b)
testEquality ModuleTranslation a
mt1 ModuleTranslation b
mt2 =
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 :: LLVMArch) (b :: LLVMArch).
Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator b -> Maybe (a :~: b)
testEquality (ModuleTranslation a -> Nonce GlobalNonceGenerator a
forall (arch :: LLVMArch).
ModuleTranslation arch -> Nonce GlobalNonceGenerator arch
_modTransNonce ModuleTranslation a
mt1) (ModuleTranslation b -> Nonce GlobalNonceGenerator b
forall (arch :: LLVMArch).
ModuleTranslation arch -> Nonce GlobalNonceGenerator arch
_modTransNonce ModuleTranslation b
mt2)
transContext :: Getter (ModuleTranslation arch) (LLVMContext arch)
transContext :: forall (arch :: LLVMArch) (f :: Type -> Type).
(Contravariant f, Functor f) =>
(LLVMContext arch -> f (LLVMContext arch))
-> ModuleTranslation arch -> f (ModuleTranslation arch)
transContext = (ModuleTranslation arch -> LLVMContext arch)
-> (LLVMContext arch -> f (LLVMContext arch))
-> ModuleTranslation arch
-> f (ModuleTranslation arch)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ModuleTranslation arch -> LLVMContext arch
forall (arch :: LLVMArch).
ModuleTranslation arch -> LLVMContext arch
_transContext
globalInitMap :: Getter (ModuleTranslation arch) GlobalInitializerMap
globalInitMap :: forall (arch :: LLVMArch) (f :: Type -> Type).
(Contravariant f, Functor f) =>
(GlobalInitializerMap -> f GlobalInitializerMap)
-> ModuleTranslation arch -> f (ModuleTranslation arch)
globalInitMap = (ModuleTranslation arch -> GlobalInitializerMap)
-> (GlobalInitializerMap -> f GlobalInitializerMap)
-> ModuleTranslation arch
-> f (ModuleTranslation arch)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ModuleTranslation arch -> GlobalInitializerMap
forall (arch :: LLVMArch).
ModuleTranslation arch -> GlobalInitializerMap
_globalInitMap
modTransDefs :: Getter (ModuleTranslation arch) [(L.Declare,SomeHandle)]
modTransDefs :: forall (arch :: LLVMArch) (f :: Type -> Type).
(Contravariant f, Functor f) =>
([(Declare, SomeHandle)] -> f [(Declare, SomeHandle)])
-> ModuleTranslation arch -> f (ModuleTranslation arch)
modTransDefs = (ModuleTranslation arch -> [(Declare, SomeHandle)])
-> ([(Declare, SomeHandle)] -> f [(Declare, SomeHandle)])
-> ModuleTranslation arch
-> f (ModuleTranslation arch)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ModuleTranslation arch -> [(Declare, SomeHandle)]
forall (arch :: LLVMArch).
ModuleTranslation arch -> [(Declare, SomeHandle)]
_modTransDefs
modTransModule :: Getter (ModuleTranslation arch) L.Module
modTransModule :: forall (arch :: LLVMArch) (f :: Type -> Type).
(Contravariant f, Functor f) =>
(Module -> f Module)
-> ModuleTranslation arch -> f (ModuleTranslation arch)
modTransModule = (ModuleTranslation arch -> Module)
-> (Module -> f Module)
-> ModuleTranslation arch
-> f (ModuleTranslation arch)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ModuleTranslation arch -> Module
forall (arch :: LLVMArch). ModuleTranslation arch -> Module
_modTransModule
modTransHalloc :: Getter (ModuleTranslation arch) HandleAllocator
modTransHalloc :: forall (arch :: LLVMArch) (f :: Type -> Type).
(Contravariant f, Functor f) =>
(HandleAllocator -> f HandleAllocator)
-> ModuleTranslation arch -> f (ModuleTranslation arch)
modTransHalloc = (ModuleTranslation arch -> HandleAllocator)
-> (HandleAllocator -> f HandleAllocator)
-> ModuleTranslation arch
-> f (ModuleTranslation arch)
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ModuleTranslation arch -> HandleAllocator
forall (arch :: LLVMArch).
ModuleTranslation arch -> HandleAllocator
_modTransHalloc
typeToRegExpr :: MemType -> LLVMGenerator s arch ret (Some (Reg s))
typeToRegExpr :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
MemType -> LLVMGenerator s arch ret (Some (Reg s))
typeToRegExpr MemType
tp = do
MemType
-> (forall {tp :: CrucibleType}.
TypeRepr tp
-> Generator LLVM s (LLVMState arch) ret IO (Some (Reg s)))
-> Generator LLVM s (LLVMState arch) ret IO (Some (Reg s))
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp ((forall {tp :: CrucibleType}.
TypeRepr tp
-> Generator LLVM s (LLVMState arch) ret IO (Some (Reg s)))
-> Generator LLVM s (LLVMState arch) ret IO (Some (Reg s)))
-> (forall {tp :: CrucibleType}.
TypeRepr tp
-> Generator LLVM s (LLVMState arch) ret IO (Some (Reg s)))
-> Generator LLVM s (LLVMState arch) ret IO (Some (Reg s))
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
tpr ->
Reg s tp -> Some (Reg s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Reg s tp -> Some (Reg s))
-> Generator LLVM s (LLVMState arch) ret IO (Reg s tp)
-> Generator LLVM s (LLVMState arch) ret IO (Some (Reg s))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeRepr tp -> Generator LLVM s (LLVMState arch) ret IO (Reg s tp)
forall (m :: Type -> Type) (tp :: CrucibleType) ext s
(t :: Type -> Type) (ret :: CrucibleType).
Monad m =>
TypeRepr tp -> Generator ext s t ret m (Reg s tp)
newUnassignedReg TypeRepr tp
tpr
buildRegMap :: IdentMap s -> L.Define -> LLVMGenerator s arch reg (IdentMap s)
buildRegMap :: forall s (arch :: LLVMArch) (reg :: CrucibleType).
IdentMap s -> Define -> LLVMGenerator s arch reg (IdentMap s)
buildRegMap IdentMap s
m Define
d = (IdentMap s
-> BasicBlock
-> Generator LLVM s (LLVMState arch) reg IO (IdentMap s))
-> IdentMap s
-> [BasicBlock]
-> Generator LLVM s (LLVMState arch) reg IO (IdentMap s)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\IdentMap s
m0 BasicBlock
bb -> IdentMap s -> BasicBlock -> LLVMGenerator s arch reg (IdentMap s)
forall s (arch :: LLVMArch) (ret :: CrucibleType).
IdentMap s -> BasicBlock -> LLVMGenerator s arch ret (IdentMap s)
buildRegTypeMap IdentMap s
m0 BasicBlock
bb) IdentMap s
m ([BasicBlock]
-> Generator LLVM s (LLVMState arch) reg IO (IdentMap s))
-> [BasicBlock]
-> Generator LLVM s (LLVMState arch) reg IO (IdentMap s)
forall a b. (a -> b) -> a -> b
$ Define -> [BasicBlock]
L.defBody Define
d
buildRegTypeMap :: IdentMap s
-> L.BasicBlock
-> LLVMGenerator s arch ret (IdentMap s)
buildRegTypeMap :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
IdentMap s -> BasicBlock -> LLVMGenerator s arch ret (IdentMap s)
buildRegTypeMap IdentMap s
m0 BasicBlock
bb = (IdentMap s
-> Stmt' BlockLabel
-> Generator LLVM s (LLVMState arch) ret IO (IdentMap s))
-> IdentMap s
-> [Stmt' BlockLabel]
-> Generator LLVM s (LLVMState arch) ret IO (IdentMap s)
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM IdentMap s
-> Stmt' BlockLabel
-> Generator LLVM s (LLVMState arch) ret IO (IdentMap s)
forall {arch :: LLVMArch} {s} {b} {ret :: CrucibleType}.
(Assert
(OrdCond (CmpNat 1 (ArchWidth arch)) 'True 'True 'False)
(TypeError ...),
Assert
(OrdCond (CmpNat 16 (ArchWidth arch)) 'True 'True 'False)
(TypeError ...),
?ptrWidth::NatRepr (ArchWidth arch), ?lc::TypeContext) =>
Map Ident (Either (Some (Reg s)) b)
-> Stmt' BlockLabel
-> Generator
LLVM
s
(LLVMState arch)
ret
IO
(Map Ident (Either (Some (Reg s)) b))
stmt IdentMap s
m0 (BasicBlock -> [Stmt' BlockLabel]
forall lab. BasicBlock' lab -> [Stmt' lab]
L.bbStmts BasicBlock
bb)
where
err :: Instr -> String -> a
err Instr
instr String
msg =
Doc Void -> [Doc Void] -> a
forall a. Doc Void -> [Doc Void] -> a
malformedLLVMModule Doc Void
"Invalid type in instruction result"
[ String -> Doc Void
forall a. IsString a => String -> a
fromString (Instr -> String
showInstr Instr
instr)
, String -> Doc Void
forall a. IsString a => String -> a
fromString String
msg
]
stmt :: Map Ident (Either (Some (Reg s)) b)
-> Stmt' BlockLabel
-> Generator
LLVM
s
(LLVMState arch)
ret
IO
(Map Ident (Either (Some (Reg s)) b))
stmt Map Ident (Either (Some (Reg s)) b)
m (L.Effect Instr
_ [(String, ValMd' BlockLabel)]
_) = Map Ident (Either (Some (Reg s)) b)
-> Generator
LLVM
s
(LLVMState arch)
ret
IO
(Map Ident (Either (Some (Reg s)) b))
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Map Ident (Either (Some (Reg s)) b)
m
stmt Map Ident (Either (Some (Reg s)) b)
m (L.Result Ident
ident Instr
instr [(String, ValMd' BlockLabel)]
_) = do
MemType
ty <- (String -> Generator LLVM s (LLVMState arch) ret IO MemType)
-> (MemType -> Generator LLVM s (LLVMState arch) ret IO MemType)
-> Either String MemType
-> Generator LLVM s (LLVMState arch) ret IO MemType
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Instr -> String -> Generator LLVM s (LLVMState arch) ret IO MemType
forall {a}. Instr -> String -> a
err Instr
instr) MemType -> Generator LLVM s (LLVMState arch) ret IO MemType
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Either String MemType
-> Generator LLVM s (LLVMState arch) ret IO MemType)
-> Either String MemType
-> Generator LLVM s (LLVMState arch) ret IO MemType
forall a b. (a -> b) -> a -> b
$ Instr -> Either String MemType
forall (m :: Type -> Type) (wptr :: Natural).
(?lc::TypeContext, MonadError String m, HasPtrWidth wptr) =>
Instr -> m MemType
instrResultType Instr
instr
Some (Reg s)
ex <- MemType -> LLVMGenerator s arch ret (Some (Reg s))
forall s (arch :: LLVMArch) (ret :: CrucibleType).
MemType -> LLVMGenerator s arch ret (Some (Reg s))
typeToRegExpr MemType
ty
case Ident
-> Map Ident (Either (Some (Reg s)) b)
-> Maybe (Either (Some (Reg s)) b)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
ident Map Ident (Either (Some (Reg s)) b)
m of
Just Either (Some (Reg s)) b
_ ->
Doc Void
-> [Doc Void]
-> Generator
LLVM
s
(LLVMState arch)
ret
IO
(Map Ident (Either (Some (Reg s)) b))
forall a. Doc Void -> [Doc Void] -> a
malformedLLVMModule Doc Void
"Register not used in SSA fashion"
[ String -> Doc Void
forall a. IsString a => String -> a
fromString (Ident -> String
forall a. Show a => a -> String
show Ident
ident)
, String -> Doc Void
forall a. IsString a => String -> a
fromString (Instr -> String
showInstr Instr
instr)
]
Maybe (Either (Some (Reg s)) b)
Nothing -> Map Ident (Either (Some (Reg s)) b)
-> Generator
LLVM
s
(LLVMState arch)
ret
IO
(Map Ident (Either (Some (Reg s)) b))
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Map Ident (Either (Some (Reg s)) b)
-> Generator
LLVM
s
(LLVMState arch)
ret
IO
(Map Ident (Either (Some (Reg s)) b)))
-> Map Ident (Either (Some (Reg s)) b)
-> Generator
LLVM
s
(LLVMState arch)
ret
IO
(Map Ident (Either (Some (Reg s)) b))
forall a b. (a -> b) -> a -> b
$ Ident
-> Either (Some (Reg s)) b
-> Map Ident (Either (Some (Reg s)) b)
-> Map Ident (Either (Some (Reg s)) b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
ident (Some (Reg s) -> Either (Some (Reg s)) b
forall a b. a -> Either a b
Left Some (Reg s)
ex) Map Ident (Either (Some (Reg s)) b)
m
generateStmts :: (?transOpts :: TranslationOptions)
=> TypeRepr ret
-> L.BlockLabel
-> Set L.Ident
-> [L.Stmt]
-> LLVMGenerator s arch ret a
generateStmts :: forall (ret :: CrucibleType) s (arch :: LLVMArch) a.
(?transOpts::TranslationOptions) =>
TypeRepr ret
-> BlockLabel
-> Set Ident
-> [Stmt' BlockLabel]
-> LLVMGenerator s arch ret a
generateStmts TypeRepr ret
retType BlockLabel
lab Set Ident
defSet0 [Stmt' BlockLabel]
stmts = Set Ident
-> [Stmt' BlockLabel] -> Generator LLVM s (LLVMState arch) ret IO a
go Set Ident
defSet0 ([Stmt' BlockLabel] -> [Stmt' BlockLabel]
processDbgDeclare [Stmt' BlockLabel]
stmts)
where go :: Set Ident
-> [Stmt' BlockLabel] -> Generator LLVM s (LLVMState arch) ret IO a
go Set Ident
_ [] = String -> Generator LLVM s (LLVMState arch) ret IO a
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"LLVM basic block ended without a terminating instruction"
go Set Ident
defSet (Stmt' BlockLabel
x:[Stmt' BlockLabel]
xs) =
case Stmt' BlockLabel
x of
L.Result Ident
ident Instr
instr [(String, ValMd' BlockLabel)]
md ->
do [(String, ValMd' BlockLabel)] -> LLVMGenerator s arch ret ()
forall s (arch :: LLVMArch) (ret :: CrucibleType).
[(String, ValMd' BlockLabel)] -> LLVMGenerator s arch ret ()
setLocation [(String, ValMd' BlockLabel)]
md
TypeRepr ret
-> BlockLabel
-> Set Ident
-> Instr
-> (LLVMExpr s arch -> LLVMGenerator s arch ret ())
-> LLVMGenerator s arch ret a
-> LLVMGenerator s arch ret a
forall s (arch :: LLVMArch) (ret :: CrucibleType) a.
(?transOpts::TranslationOptions) =>
TypeRepr ret
-> BlockLabel
-> Set Ident
-> Instr
-> (LLVMExpr s arch -> LLVMGenerator s arch ret ())
-> LLVMGenerator s arch ret a
-> LLVMGenerator s arch ret a
generateInstr TypeRepr ret
retType BlockLabel
lab Set Ident
defSet Instr
instr
(Ident -> LLVMExpr s arch -> LLVMGenerator s arch ret ()
forall s (arch :: LLVMArch) (ret :: CrucibleType).
Ident -> LLVMExpr s arch -> LLVMGenerator s arch ret ()
assignLLVMReg Ident
ident)
(Set Ident
-> [Stmt' BlockLabel] -> Generator LLVM s (LLVMState arch) ret IO a
go (Ident -> Set Ident -> Set Ident
forall a. Ord a => a -> Set a -> Set a
Set.insert Ident
ident Set Ident
defSet) [Stmt' BlockLabel]
xs)
L.Effect Instr
instr [(String, ValMd' BlockLabel)]
md ->
do [(String, ValMd' BlockLabel)] -> LLVMGenerator s arch ret ()
forall s (arch :: LLVMArch) (ret :: CrucibleType).
[(String, ValMd' BlockLabel)] -> LLVMGenerator s arch ret ()
setLocation [(String, ValMd' BlockLabel)]
md
TypeRepr ret
-> BlockLabel
-> Set Ident
-> Instr
-> (LLVMExpr s arch -> LLVMGenerator s arch ret ())
-> LLVMGenerator s arch ret a
-> LLVMGenerator s arch ret a
forall s (arch :: LLVMArch) (ret :: CrucibleType) a.
(?transOpts::TranslationOptions) =>
TypeRepr ret
-> BlockLabel
-> Set Ident
-> Instr
-> (LLVMExpr s arch -> LLVMGenerator s arch ret ())
-> LLVMGenerator s arch ret a
-> LLVMGenerator s arch ret a
generateInstr TypeRepr ret
retType BlockLabel
lab Set Ident
defSet Instr
instr
(\LLVMExpr s arch
_ -> () -> Generator LLVM s (LLVMState arch) ret IO ()
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ())
(Set Ident
-> [Stmt' BlockLabel] -> Generator LLVM s (LLVMState arch) ret IO a
go Set Ident
defSet [Stmt' BlockLabel]
xs)
processDbgDeclare :: [L.Stmt] -> [L.Stmt]
processDbgDeclare :: [Stmt' BlockLabel] -> [Stmt' BlockLabel]
processDbgDeclare = (Map Ident [(String, ValMd' BlockLabel)], [Stmt' BlockLabel])
-> [Stmt' BlockLabel]
forall a b. (a, b) -> b
snd ((Map Ident [(String, ValMd' BlockLabel)], [Stmt' BlockLabel])
-> [Stmt' BlockLabel])
-> ([Stmt' BlockLabel]
-> (Map Ident [(String, ValMd' BlockLabel)], [Stmt' BlockLabel]))
-> [Stmt' BlockLabel]
-> [Stmt' BlockLabel]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Stmt' BlockLabel]
-> (Map Ident [(String, ValMd' BlockLabel)], [Stmt' BlockLabel])
go
where
go :: [L.Stmt] -> (Map L.Ident [(String, L.ValMd)] , [L.Stmt])
go :: [Stmt' BlockLabel]
-> (Map Ident [(String, ValMd' BlockLabel)], [Stmt' BlockLabel])
go [] = (Map Ident [(String, ValMd' BlockLabel)]
forall k a. Map k a
Map.empty, [])
go (Stmt' BlockLabel
stmt : [Stmt' BlockLabel]
stmts) =
let (Map Ident [(String, ValMd' BlockLabel)]
m, [Stmt' BlockLabel]
stmts') = [Stmt' BlockLabel]
-> (Map Ident [(String, ValMd' BlockLabel)], [Stmt' BlockLabel])
go [Stmt' BlockLabel]
stmts in
case Stmt' BlockLabel
stmt of
L.Result Ident
x instr :: Instr
instr@L.Alloca{} [(String, ValMd' BlockLabel)]
md ->
case Ident
-> Map Ident [(String, ValMd' BlockLabel)]
-> Maybe [(String, ValMd' BlockLabel)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
x Map Ident [(String, ValMd' BlockLabel)]
m of
Just [(String, ValMd' BlockLabel)]
md' -> (Map Ident [(String, ValMd' BlockLabel)]
m, Ident -> Instr -> [(String, ValMd' BlockLabel)] -> Stmt' BlockLabel
forall lab.
Ident -> Instr' lab -> [(String, ValMd' lab)] -> Stmt' lab
L.Result Ident
x Instr
instr ([(String, ValMd' BlockLabel)]
md' [(String, ValMd' BlockLabel)]
-> [(String, ValMd' BlockLabel)] -> [(String, ValMd' BlockLabel)]
forall a. [a] -> [a] -> [a]
++ [(String, ValMd' BlockLabel)]
md) Stmt' BlockLabel -> [Stmt' BlockLabel] -> [Stmt' BlockLabel]
forall a. a -> [a] -> [a]
: [Stmt' BlockLabel]
stmts')
Maybe [(String, ValMd' BlockLabel)]
Nothing -> (Map Ident [(String, ValMd' BlockLabel)]
m, Stmt' BlockLabel
stmt Stmt' BlockLabel -> [Stmt' BlockLabel] -> [Stmt' BlockLabel]
forall a. a -> [a] -> [a]
: [Stmt' BlockLabel]
stmts')
L.Result Ident
x (L.Conv ConvOp
L.BitCast (L.Typed Type
_ (L.ValIdent Ident
y)) Type
_) [(String, ValMd' BlockLabel)]
md ->
let md' :: [(String, ValMd' BlockLabel)]
md' = [(String, ValMd' BlockLabel)]
md [(String, ValMd' BlockLabel)]
-> [(String, ValMd' BlockLabel)] -> [(String, ValMd' BlockLabel)]
forall a. [a] -> [a] -> [a]
++ [(String, ValMd' BlockLabel)]
-> Maybe [(String, ValMd' BlockLabel)]
-> [(String, ValMd' BlockLabel)]
forall a. a -> Maybe a -> a
fromMaybe [] (Ident
-> Map Ident [(String, ValMd' BlockLabel)]
-> Maybe [(String, ValMd' BlockLabel)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
x Map Ident [(String, ValMd' BlockLabel)]
m)
m' :: Map Ident [(String, ValMd' BlockLabel)]
m' = (Maybe [(String, ValMd' BlockLabel)]
-> Maybe [(String, ValMd' BlockLabel)])
-> Ident
-> Map Ident [(String, ValMd' BlockLabel)]
-> Map Ident [(String, ValMd' BlockLabel)]
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter ([(String, ValMd' BlockLabel)]
-> Maybe [(String, ValMd' BlockLabel)]
forall a. a -> Maybe a
Just ([(String, ValMd' BlockLabel)]
-> Maybe [(String, ValMd' BlockLabel)])
-> (Maybe [(String, ValMd' BlockLabel)]
-> [(String, ValMd' BlockLabel)])
-> Maybe [(String, ValMd' BlockLabel)]
-> Maybe [(String, ValMd' BlockLabel)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, ValMd' BlockLabel)]
-> ([(String, ValMd' BlockLabel)] -> [(String, ValMd' BlockLabel)])
-> Maybe [(String, ValMd' BlockLabel)]
-> [(String, ValMd' BlockLabel)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [(String, ValMd' BlockLabel)]
md' ([(String, ValMd' BlockLabel)]
md'[(String, ValMd' BlockLabel)]
-> [(String, ValMd' BlockLabel)] -> [(String, ValMd' BlockLabel)]
forall a. [a] -> [a] -> [a]
++)) Ident
y Map Ident [(String, ValMd' BlockLabel)]
m
in (Map Ident [(String, ValMd' BlockLabel)]
m', Stmt' BlockLabel
stmtStmt' BlockLabel -> [Stmt' BlockLabel] -> [Stmt' BlockLabel]
forall a. a -> [a] -> [a]
:[Stmt' BlockLabel]
stmts)
L.Effect (L.Call Bool
_ Type
_ (L.ValSymbol Symbol
"llvm.dbg.declare") (L.Typed Type
_ (L.ValMd (L.ValMdValue (L.Typed Type
_ (L.ValIdent Ident
x)))) : [Typed (Value' BlockLabel)]
_)) [(String, ValMd' BlockLabel)]
md ->
(Ident
-> [(String, ValMd' BlockLabel)]
-> Map Ident [(String, ValMd' BlockLabel)]
-> Map Ident [(String, ValMd' BlockLabel)]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Ident
x [(String, ValMd' BlockLabel)]
md Map Ident [(String, ValMd' BlockLabel)]
m, Stmt' BlockLabel
stmt Stmt' BlockLabel -> [Stmt' BlockLabel] -> [Stmt' BlockLabel]
forall a. a -> [a] -> [a]
: [Stmt' BlockLabel]
stmts')
Stmt' BlockLabel
_ -> (Map Ident [(String, ValMd' BlockLabel)]
m, Stmt' BlockLabel
stmt Stmt' BlockLabel -> [Stmt' BlockLabel] -> [Stmt' BlockLabel]
forall a. a -> [a] -> [a]
: [Stmt' BlockLabel]
stmts')
setLocation
:: [(String,L.ValMd)]
-> LLVMGenerator s arch ret ()
setLocation :: forall s (arch :: LLVMArch) (ret :: CrucibleType).
[(String, ValMd' BlockLabel)] -> LLVMGenerator s arch ret ()
setLocation [] = () -> Generator LLVM s (LLVMState arch) ret IO ()
forall a. a -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
setLocation ((String, ValMd' BlockLabel)
x:[(String, ValMd' BlockLabel)]
xs) =
case (String, ValMd' BlockLabel)
x of
(String
"dbg",L.ValMdLoc DebugLoc' BlockLabel
dl) ->
let ln :: Int
ln = Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Int) -> Word32 -> Int
forall a b. (a -> b) -> a -> b
$ DebugLoc' BlockLabel -> Word32
forall lab. DebugLoc' lab -> Word32
L.dlLine DebugLoc' BlockLabel
dl
col :: Int
col = Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Int) -> Word32 -> Int
forall a b. (a -> b) -> a -> b
$ DebugLoc' BlockLabel -> Word32
forall lab. DebugLoc' lab -> Word32
L.dlCol DebugLoc' BlockLabel
dl
file :: Text
file = ValMd' BlockLabel -> Text
getFile (ValMd' BlockLabel -> Text) -> ValMd' BlockLabel -> Text
forall a b. (a -> b) -> a -> b
$ DebugLoc' BlockLabel -> ValMd' BlockLabel
forall lab. DebugLoc' lab -> ValMd' lab
L.dlScope DebugLoc' BlockLabel
dl
in Position -> Generator LLVM s (LLVMState arch) ret IO ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Position -> Generator ext s t ret m ()
setPosition (Text -> Int -> Int -> Position
SourcePos Text
file Int
ln Int
col)
(String
"dbg",L.ValMdDebugInfo (L.DebugInfoSubprogram DISubprogram' BlockLabel
subp))
| Just ValMd' BlockLabel
file' <- DISubprogram' BlockLabel -> Maybe (ValMd' BlockLabel)
forall lab. DISubprogram' lab -> Maybe (ValMd' lab)
L.dispFile DISubprogram' BlockLabel
subp
-> let ln :: Int
ln = Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word32 -> Int) -> Word32 -> Int
forall a b. (a -> b) -> a -> b
$ DISubprogram' BlockLabel -> Word32
forall lab. DISubprogram' lab -> Word32
L.dispLine DISubprogram' BlockLabel
subp
file :: Text
file = ValMd' BlockLabel -> Text
getFile ValMd' BlockLabel
file'
in Position -> Generator LLVM s (LLVMState arch) ret IO ()
forall ext s (t :: Type -> Type) (ret :: CrucibleType)
(m :: Type -> Type).
Position -> Generator ext s t ret m ()
setPosition (Text -> Int -> Int -> Position
SourcePos Text
file Int
ln Int
0)
(String, ValMd' BlockLabel)
_ -> [(String, ValMd' BlockLabel)] -> LLVMGenerator s arch ret ()
forall s (arch :: LLVMArch) (ret :: CrucibleType).
[(String, ValMd' BlockLabel)] -> LLVMGenerator s arch ret ()
setLocation [(String, ValMd' BlockLabel)]
xs
where
getFile :: ValMd' BlockLabel -> Text
getFile = String -> Text
Text.pack (String -> Text)
-> (ValMd' BlockLabel -> String) -> ValMd' BlockLabel -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> (DIFile -> String) -> Maybe DIFile -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" DIFile -> String
filenm (Maybe DIFile -> String)
-> (ValMd' BlockLabel -> Maybe DIFile)
-> ValMd' BlockLabel
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (?lc::TypeContext) => ValMd' BlockLabel -> Maybe DIFile
ValMd' BlockLabel -> Maybe DIFile
findFile
filenm :: DIFile -> String
filenm = DIFile -> String
L.difFilename
findFile :: (?lc :: TypeContext) => L.ValMd -> Maybe L.DIFile
findFile :: (?lc::TypeContext) => ValMd' BlockLabel -> Maybe DIFile
findFile (L.ValMdRef Int
x) = (?lc::TypeContext) => ValMd' BlockLabel -> Maybe DIFile
ValMd' BlockLabel -> Maybe DIFile
findFile (ValMd' BlockLabel -> Maybe DIFile)
-> Maybe (ValMd' BlockLabel) -> Maybe DIFile
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< (?lc::TypeContext) => Int -> Maybe (ValMd' BlockLabel)
Int -> Maybe (ValMd' BlockLabel)
lookupMetadata Int
x
findFile (L.ValMdNode (Maybe (ValMd' BlockLabel)
_:Just (L.ValMdRef Int
y):[Maybe (ValMd' BlockLabel)]
_)) =
case (?lc::TypeContext) => Int -> Maybe (ValMd' BlockLabel)
Int -> Maybe (ValMd' BlockLabel)
lookupMetadata Int
y of
Just (L.ValMdNode [Just (L.ValMdString String
fname), Just (L.ValMdString String
fpath)]) ->
DIFile -> Maybe DIFile
forall a. a -> Maybe a
Just (String -> String -> DIFile
L.DIFile String
fname String
fpath)
Maybe (ValMd' BlockLabel)
_ -> Maybe DIFile
forall a. Maybe a
Nothing
findFile (L.ValMdDebugInfo DebugInfo' BlockLabel
di) =
case DebugInfo' BlockLabel
di of
L.DebugInfoFile DIFile
dif -> DIFile -> Maybe DIFile
forall a. a -> Maybe a
Just DIFile
dif
L.DebugInfoLexicalBlock DILexicalBlock' BlockLabel
dilex
| Just ValMd' BlockLabel
md <- DILexicalBlock' BlockLabel -> Maybe (ValMd' BlockLabel)
forall lab. DILexicalBlock' lab -> Maybe (ValMd' lab)
L.dilbFile DILexicalBlock' BlockLabel
dilex -> (?lc::TypeContext) => ValMd' BlockLabel -> Maybe DIFile
ValMd' BlockLabel -> Maybe DIFile
findFile ValMd' BlockLabel
md
| Just ValMd' BlockLabel
md <- DILexicalBlock' BlockLabel -> Maybe (ValMd' BlockLabel)
forall lab. DILexicalBlock' lab -> Maybe (ValMd' lab)
L.dilbScope DILexicalBlock' BlockLabel
dilex -> (?lc::TypeContext) => ValMd' BlockLabel -> Maybe DIFile
ValMd' BlockLabel -> Maybe DIFile
findFile ValMd' BlockLabel
md
L.DebugInfoLexicalBlockFile DILexicalBlockFile' BlockLabel
dilexFile
| Just ValMd' BlockLabel
md <- DILexicalBlockFile' BlockLabel -> Maybe (ValMd' BlockLabel)
forall lab. DILexicalBlockFile' lab -> Maybe (ValMd' lab)
L.dilbfFile DILexicalBlockFile' BlockLabel
dilexFile -> (?lc::TypeContext) => ValMd' BlockLabel -> Maybe DIFile
ValMd' BlockLabel -> Maybe DIFile
findFile ValMd' BlockLabel
md
| Bool
otherwise -> (?lc::TypeContext) => ValMd' BlockLabel -> Maybe DIFile
ValMd' BlockLabel -> Maybe DIFile
findFile (DILexicalBlockFile' BlockLabel -> ValMd' BlockLabel
forall lab. DILexicalBlockFile' lab -> ValMd' lab
L.dilbfScope DILexicalBlockFile' BlockLabel
dilexFile)
L.DebugInfoSubprogram DISubprogram' BlockLabel
disub
| Just ValMd' BlockLabel
md <- DISubprogram' BlockLabel -> Maybe (ValMd' BlockLabel)
forall lab. DISubprogram' lab -> Maybe (ValMd' lab)
L.dispFile DISubprogram' BlockLabel
disub -> (?lc::TypeContext) => ValMd' BlockLabel -> Maybe DIFile
ValMd' BlockLabel -> Maybe DIFile
findFile ValMd' BlockLabel
md
| Just ValMd' BlockLabel
md <- DISubprogram' BlockLabel -> Maybe (ValMd' BlockLabel)
forall lab. DISubprogram' lab -> Maybe (ValMd' lab)
L.dispScope DISubprogram' BlockLabel
disub -> (?lc::TypeContext) => ValMd' BlockLabel -> Maybe DIFile
ValMd' BlockLabel -> Maybe DIFile
findFile ValMd' BlockLabel
md
DebugInfo' BlockLabel
_ -> Maybe DIFile
forall a. Maybe a
Nothing
findFile ValMd' BlockLabel
_ = Maybe DIFile
forall a. Maybe a
Nothing
defineLLVMBlock
:: (?transOpts :: TranslationOptions)
=> TypeRepr ret
-> LLVMBlockInfoMap s
-> L.BasicBlock
-> LLVMGenerator s arch ret ()
defineLLVMBlock :: forall (ret :: CrucibleType) s (arch :: LLVMArch).
(?transOpts::TranslationOptions) =>
TypeRepr ret
-> LLVMBlockInfoMap s -> BasicBlock -> LLVMGenerator s arch ret ()
defineLLVMBlock TypeRepr ret
retType LLVMBlockInfoMap s
lm L.BasicBlock{ bbLabel :: forall lab. BasicBlock' lab -> Maybe lab
L.bbLabel = Just BlockLabel
lab, bbStmts :: forall lab. BasicBlock' lab -> [Stmt' lab]
L.bbStmts = [Stmt' BlockLabel]
stmts } = do
case BlockLabel -> LLVMBlockInfoMap s -> Maybe (LLVMBlockInfo s)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BlockLabel
lab LLVMBlockInfoMap s
lm of
Just LLVMBlockInfo s
bi -> Label s
-> (forall a. Generator LLVM s (LLVMState arch) ret IO a)
-> Generator LLVM s (LLVMState arch) ret IO ()
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType).
(Monad m, IsSyntaxExtension ext) =>
Label s
-> (forall a. Generator ext s t ret m a)
-> Generator ext s t ret m ()
defineBlock (LLVMBlockInfo s -> Label s
forall s. LLVMBlockInfo s -> Label s
block_label LLVMBlockInfo s
bi) (TypeRepr ret
-> BlockLabel
-> Set Ident
-> [Stmt' BlockLabel]
-> LLVMGenerator s arch ret a
forall (ret :: CrucibleType) s (arch :: LLVMArch) a.
(?transOpts::TranslationOptions) =>
TypeRepr ret
-> BlockLabel
-> Set Ident
-> [Stmt' BlockLabel]
-> LLVMGenerator s arch ret a
generateStmts TypeRepr ret
retType BlockLabel
lab (LLVMBlockInfo s -> Set Ident
forall s. LLVMBlockInfo s -> Set Ident
block_use_set LLVMBlockInfo s
bi) [Stmt' BlockLabel]
stmts)
Maybe (LLVMBlockInfo s)
Nothing -> String -> Generator LLVM s (LLVMState arch) ret IO ()
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> Generator LLVM s (LLVMState arch) ret IO ())
-> String -> Generator LLVM s (LLVMState arch) ret IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"LLVM basic block not found in block info map", BlockLabel -> String
forall a. Show a => a -> String
show BlockLabel
lab]
defineLLVMBlock TypeRepr ret
_ LLVMBlockInfoMap s
_ BasicBlock
_ = String -> Generator LLVM s (LLVMState arch) ret IO ()
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"LLVM basic block has no label!"
genDefn :: (?transOpts :: TranslationOptions)
=> L.Define
-> TypeRepr ret
-> LLVMGenerator s arch ret (Expr ext s ret)
genDefn :: forall (ret :: CrucibleType) s (arch :: LLVMArch) ext.
(?transOpts::TranslationOptions) =>
Define -> TypeRepr ret -> LLVMGenerator s arch ret (Expr ext s ret)
genDefn Define
defn TypeRepr ret
retType =
case Define -> [BasicBlock]
L.defBody Define
defn of
[] -> String -> Generator LLVM s (LLVMState arch) ret IO (Expr ext s ret)
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"LLVM define with no blocks!"
( L.BasicBlock{ bbLabel :: forall lab. BasicBlock' lab -> Maybe lab
L.bbLabel = Maybe BlockLabel
Nothing } : [BasicBlock]
_ ) -> String -> Generator LLVM s (LLVMState arch) ret IO (Expr ext s ret)
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
-> Generator LLVM s (LLVMState arch) ret IO (Expr ext s ret))
-> String
-> Generator LLVM s (LLVMState arch) ret IO (Expr ext s ret)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"entry block has no label"]
( L.BasicBlock{ bbLabel :: forall lab. BasicBlock' lab -> Maybe lab
L.bbLabel = Just BlockLabel
entry_lab } : [BasicBlock]
_ ) -> do
let (L.Symbol String
nm) = Define -> Symbol
L.defName Define
defn
Text -> LLVMGenerator s arch ret ()
forall s (arch :: LLVMArch) (ret :: CrucibleType).
Text -> LLVMGenerator s arch ret ()
callPushFrame (Text -> LLVMGenerator s arch ret ())
-> Text -> LLVMGenerator s arch ret ()
forall a b. (a -> b) -> a -> b
$ String -> Text
Text.pack String
nm
[(String, ValMd' BlockLabel)] -> LLVMGenerator s arch ret ()
forall s (arch :: LLVMArch) (ret :: CrucibleType).
[(String, ValMd' BlockLabel)] -> LLVMGenerator s arch ret ()
setLocation ([(String, ValMd' BlockLabel)] -> LLVMGenerator s arch ret ())
-> [(String, ValMd' BlockLabel)] -> LLVMGenerator s arch ret ()
forall a b. (a -> b) -> a -> b
$ Map String (ValMd' BlockLabel) -> [(String, ValMd' BlockLabel)]
forall k a. Map k a -> [(k, a)]
Map.toList (Define -> Map String (ValMd' BlockLabel)
L.defMetadata Define
defn)
LLVMBlockInfoMap s
bim <- Define
-> Generator LLVM s (LLVMState arch) ret IO (LLVMBlockInfoMap s)
forall (m :: Type -> Type) l s (st :: Type -> Type)
(ret :: CrucibleType).
Monad m =>
Define -> Generator l s st ret m (LLVMBlockInfoMap s)
buildBlockInfoMap Define
defn
(LLVMBlockInfoMap s -> Identity (LLVMBlockInfoMap s))
-> LLVMState arch s -> Identity (LLVMState arch s)
forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(LLVMBlockInfoMap s -> f (LLVMBlockInfoMap s))
-> LLVMState arch s -> f (LLVMState arch s)
blockInfoMap ((LLVMBlockInfoMap s -> Identity (LLVMBlockInfoMap s))
-> LLVMState arch s -> Identity (LLVMState arch s))
-> LLVMBlockInfoMap s
-> Generator LLVM s (LLVMState arch) ret IO ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= LLVMBlockInfoMap s
bim
IdentMap s
im <- Getting (IdentMap s) (LLVMState arch s) (IdentMap s)
-> Generator LLVM s (LLVMState arch) ret IO (IdentMap s)
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use Getting (IdentMap s) (LLVMState arch s) (IdentMap s)
forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(IdentMap s -> f (IdentMap s))
-> LLVMState arch s -> f (LLVMState arch s)
identMap
IdentMap s
im' <- IdentMap s -> Define -> LLVMGenerator s arch ret (IdentMap s)
forall s (arch :: LLVMArch) (reg :: CrucibleType).
IdentMap s -> Define -> LLVMGenerator s arch reg (IdentMap s)
buildRegMap IdentMap s
im Define
defn
(IdentMap s -> Identity (IdentMap s))
-> LLVMState arch s -> Identity (LLVMState arch s)
forall (arch :: LLVMArch) s (f :: Type -> Type).
Functor f =>
(IdentMap s -> f (IdentMap s))
-> LLVMState arch s -> f (LLVMState arch s)
identMap ((IdentMap s -> Identity (IdentMap s))
-> LLVMState arch s -> Identity (LLVMState arch s))
-> IdentMap s -> Generator LLVM s (LLVMState arch) ret IO ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= IdentMap s
im'
case BlockLabel -> LLVMBlockInfoMap s -> Maybe (LLVMBlockInfo s)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BlockLabel
entry_lab LLVMBlockInfoMap s
bim of
Maybe (LLVMBlockInfo s)
Nothing -> String -> Generator LLVM s (LLVMState arch) ret IO (Expr ext s ret)
forall a. String -> Generator LLVM s (LLVMState arch) ret IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
-> Generator LLVM s (LLVMState arch) ret IO (Expr ext s ret))
-> String
-> Generator LLVM s (LLVMState arch) ret IO (Expr ext s ret)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"entry label not found in label map:", BlockLabel -> String
forall a. Show a => a -> String
show BlockLabel
entry_lab]
Just LLVMBlockInfo s
entry_bi -> do
String
-> LLVMBlockInfo s -> [Typed Ident] -> LLVMGenerator s arch ret ()
forall s (arg :: LLVMArch) (ret :: CrucibleType).
String
-> LLVMBlockInfo s -> [Typed Ident] -> LLVMGenerator s arg ret ()
checkEntryPointUseSet String
nm LLVMBlockInfo s
entry_bi (Define -> [Typed Ident]
L.defArgs Define
defn)
(BasicBlock -> Generator LLVM s (LLVMState arch) ret IO ())
-> [BasicBlock] -> Generator LLVM s (LLVMState arch) ret IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\BasicBlock
bb -> TypeRepr ret
-> LLVMBlockInfoMap s -> BasicBlock -> LLVMGenerator s arch ret ()
forall (ret :: CrucibleType) s (arch :: LLVMArch).
(?transOpts::TranslationOptions) =>
TypeRepr ret
-> LLVMBlockInfoMap s -> BasicBlock -> LLVMGenerator s arch ret ()
defineLLVMBlock TypeRepr ret
retType LLVMBlockInfoMap s
bim BasicBlock
bb) (Define -> [BasicBlock]
L.defBody Define
defn)
Label s
-> Generator LLVM s (LLVMState arch) ret IO (Expr ext s ret)
forall (m :: Type -> Type) ext s (t :: Type -> Type)
(ret :: CrucibleType) a.
(Monad m, IsSyntaxExtension ext) =>
Label s -> Generator ext s t ret m a
jump (LLVMBlockInfo s -> Label s
forall s. LLVMBlockInfo s -> Label s
block_label LLVMBlockInfo s
entry_bi)
checkEntryPointUseSet ::
String ->
LLVMBlockInfo s ->
[L.Typed L.Ident] ->
LLVMGenerator s arg ret ()
checkEntryPointUseSet :: forall s (arg :: LLVMArch) (ret :: CrucibleType).
String
-> LLVMBlockInfo s -> [Typed Ident] -> LLVMGenerator s arg ret ()
checkEntryPointUseSet String
nm LLVMBlockInfo s
bi [Typed Ident]
args
| Set Ident -> Bool
forall a. Set a -> Bool
Set.null Set Ident
unsatisfiedUses = () -> Generator LLVM s (LLVMState arg) ret IO ()
forall a. a -> Generator LLVM s (LLVMState arg) ret IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
| Bool
otherwise =
Doc Void
-> [Doc Void] -> Generator LLVM s (LLVMState arg) ret IO ()
forall a. Doc Void -> [Doc Void] -> a
malformedLLVMModule (Doc Void
"Invalid SSA form for function: " Doc Void -> Doc Void -> Doc Void
forall a. Semigroup a => a -> a -> a
<> String -> Doc Void
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
nm)
([ Doc Void
"The following LLVM virtual registers have at least one use site that"
, Doc Void
"is not dominated by the corresponding definition:" ] [Doc Void] -> [Doc Void] -> [Doc Void]
forall a. [a] -> [a] -> [a]
++
[ Doc Void
" " Doc Void -> Doc Void -> Doc Void
forall a. Semigroup a => a -> a -> a
<> String -> Doc Void
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Doc -> String
forall a. Show a => a -> String
show (Ident -> Doc
LPP.ppIdent Ident
i)) | Ident
i <- Set Ident -> [Ident]
forall a. Set a -> [a]
Set.toList Set Ident
unsatisfiedUses ])
where
argSet :: Set Ident
argSet = [Ident] -> Set Ident
forall a. Ord a => [a] -> Set a
Set.fromList ((Typed Ident -> Ident) -> [Typed Ident] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map Typed Ident -> Ident
forall a. Typed a -> a
L.typedValue [Typed Ident]
args)
useSet :: Set Ident
useSet = LLVMBlockInfo s -> Set Ident
forall s. LLVMBlockInfo s -> Set Ident
block_use_set LLVMBlockInfo s
bi
unsatisfiedUses :: Set Ident
unsatisfiedUses = Set Ident -> Set Ident -> Set Ident
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set Ident
useSet Set Ident
argSet
transDefine :: forall arch wptr args ret.
(HasPtrWidth wptr, wptr ~ ArchWidth arch, ?transOpts :: TranslationOptions) =>
FnHandle args ret ->
LLVMContext arch ->
IORef [LLVMTranslationWarning] ->
L.Define ->
IO (L.Declare, C.AnyCFG LLVM)
transDefine :: forall (arch :: LLVMArch) (wptr :: Natural)
(args :: Ctx CrucibleType) (ret :: CrucibleType).
(HasPtrWidth wptr, wptr ~ ArchWidth arch,
?transOpts::TranslationOptions) =>
FnHandle args ret
-> LLVMContext arch
-> IORef [LLVMTranslationWarning]
-> Define
-> IO (Declare, AnyCFG LLVM)
transDefine FnHandle args ret
h LLVMContext arch
ctx IORef [LLVMTranslationWarning]
warnRef Define
d = do
let ?lc = LLVMContext arch
ctxLLVMContext arch
-> Getting TypeContext (LLVMContext arch) TypeContext
-> TypeContext
forall s a. s -> Getting a s a -> a
^.Getting TypeContext (LLVMContext arch) TypeContext
forall (arch :: LLVMArch) (f :: Type -> Type).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx
let decl :: Declare
decl = Define -> Declare
declareFromDefine Define
d
let L.Symbol String
fstr = Define -> Symbol
L.defName Define
d
Declare
-> (forall {args :: Ctx CrucibleType} {ret :: CrucibleType}.
CtxRepr args -> TypeRepr ret -> IO (Declare, AnyCFG LLVM))
-> IO (Declare, AnyCFG LLVM)
forall (wptr :: Natural) (m :: Type -> Type) a.
(?lc::TypeContext, HasPtrWidth wptr, MonadFail m) =>
Declare
-> (forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr args -> TypeRepr ret -> m a)
-> m a
llvmDeclToFunHandleRepr' Declare
decl ((forall {args :: Ctx CrucibleType} {ret :: CrucibleType}.
CtxRepr args -> TypeRepr ret -> IO (Declare, AnyCFG LLVM))
-> IO (Declare, AnyCFG LLVM))
-> (forall {args :: Ctx CrucibleType} {ret :: CrucibleType}.
CtxRepr args -> TypeRepr ret -> IO (Declare, AnyCFG LLVM))
-> IO (Declare, AnyCFG LLVM)
forall a b. (a -> b) -> a -> b
$ \CtxRepr args
argTys TypeRepr ret
retTy ->
case (CtxRepr args -> Assignment TypeRepr args -> Maybe (args :~: args)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
Assignment TypeRepr a -> Assignment TypeRepr b -> Maybe (a :~: b)
testEquality CtxRepr args
argTys (FnHandle args ret -> Assignment TypeRepr args
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> CtxRepr args
handleArgTypes FnHandle args ret
h),
TypeRepr ret -> TypeRepr ret -> Maybe (ret :~: ret)
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 ret
retTy (FnHandle args ret -> TypeRepr ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr ret
handleReturnType FnHandle args ret
h)) of
(Maybe (args :~: args)
Nothing, Maybe (ret :~: ret)
_) -> String -> IO (Declare, AnyCFG LLVM)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (Declare, AnyCFG LLVM))
-> String -> IO (Declare, AnyCFG LLVM)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ String
"Argument type mismatch when defining function: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fstr
, CtxRepr args -> String
forall a. Show a => a -> String
show CtxRepr args
argTys
, FnHandle args ret -> String
forall a. Show a => a -> String
show FnHandle args ret
h ]
(Maybe (args :~: args)
_, Maybe (ret :~: ret)
Nothing) -> String -> IO (Declare, AnyCFG LLVM)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (Declare, AnyCFG LLVM))
-> String -> IO (Declare, AnyCFG LLVM)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
[ String
"Return type mismatch when bootstrapping function: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fstr
, TypeRepr ret -> String
forall a. Show a => a -> String
show TypeRepr ret
retTy, FnHandle args ret -> String
forall a. Show a => a -> String
show FnHandle args ret
h
]
(Just args :~: args
Refl, Just ret :~: ret
Refl) ->
do let def :: FunctionDef LLVM (LLVMState arch) args ret IO
def :: FunctionDef LLVM (LLVMState arch) args ret IO
def Assignment (Atom s) args
inputs = (LLVMState arch s
s, Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s ret)
Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s ret)
f)
where s :: LLVMState arch s
s = Define
-> LLVMContext arch
-> CtxRepr args
-> Assignment (Atom s) args
-> IORef [LLVMTranslationWarning]
-> LLVMState arch s
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
ctx CtxRepr args
argTys Assignment (Atom s) args
Assignment (Atom s) args
inputs IORef [LLVMTranslationWarning]
warnRef
f :: Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s ret)
f = Define
-> TypeRepr ret -> LLVMGenerator s arch ret (Expr LLVM s ret)
forall (ret :: CrucibleType) s (arch :: LLVMArch) ext.
(?transOpts::TranslationOptions) =>
Define -> TypeRepr ret -> LLVMGenerator s arch ret (Expr ext s ret)
genDefn Define
d TypeRepr ret
retTy
Some (NonceGenerator IO)
sng <- IO (Some (NonceGenerator IO))
newIONonceGenerator
(SomeCFG CFG LLVM s args ret
g, []) <- Position
-> Some (NonceGenerator IO)
-> FnHandle args ret
-> FunctionDef LLVM (LLVMState arch) args ret IO
-> (forall {s}.
NonceGenerator IO s
-> CFG LLVM s args ret -> IO (CFG LLVM s args ret))
-> IO (SomeCFG LLVM args 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
-> (forall s.
NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret))
-> m (SomeCFG ext init ret, [AnyCFG ext])
defineFunctionOpt Position
InternalPos Some (NonceGenerator IO)
sng FnHandle args ret
h Assignment (Atom s) args
-> (LLVMState arch s,
Generator LLVM s (LLVMState arch) ret IO (Expr LLVM s ret))
FunctionDef LLVM (LLVMState arch) args ret IO
def ((forall {s}.
NonceGenerator IO s
-> CFG LLVM s args ret -> IO (CFG LLVM s args ret))
-> IO (SomeCFG LLVM args ret, [AnyCFG LLVM]))
-> (forall {s}.
NonceGenerator IO s
-> CFG LLVM s args ret -> IO (CFG LLVM s args ret))
-> IO (SomeCFG LLVM args ret, [AnyCFG LLVM])
forall a b. (a -> b) -> a -> b
$ \NonceGenerator IO s
ng CFG LLVM s args ret
cfg ->
if TranslationOptions -> Bool
optLoopMerge ?transOpts::TranslationOptions
TranslationOptions
?transOpts then NonceGenerator IO s
-> CFG LLVM s args ret -> IO (CFG LLVM s args ret)
forall ext (m :: Type -> Type) s (init :: Ctx CrucibleType)
(ret :: CrucibleType).
(TraverseExt ext, Monad m, Show (CFG ext s init ret)) =>
NonceGenerator m s -> CFG ext s init ret -> m (CFG ext s init ret)
earlyMergeLoops NonceGenerator IO s
ng CFG LLVM s args ret
cfg else CFG LLVM s args ret -> IO (CFG LLVM s args ret)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return CFG LLVM s args ret
cfg
case CFG LLVM s args ret -> SomeCFG LLVM args ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
IsSyntaxExtension ext =>
CFG ext s init ret -> SomeCFG ext init ret
toSSA CFG LLVM s args ret
g of
C.SomeCFG CFG LLVM blocks args ret
g_ssa -> CFG LLVM blocks args ret
g_ssa CFG LLVM blocks args ret
-> IO (Declare, AnyCFG LLVM) -> IO (Declare, AnyCFG LLVM)
forall a b. a -> b -> b
`seq` (Declare, AnyCFG LLVM) -> IO (Declare, AnyCFG LLVM)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Declare
decl, CFG LLVM blocks args ret -> AnyCFG LLVM
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> AnyCFG ext
C.AnyCFG CFG LLVM blocks args ret
g_ssa)
translateModule :: (?transOpts :: TranslationOptions)
=> HandleAllocator
-> GlobalVar Mem
-> L.Module
-> IO (Some ModuleTranslation)
translateModule :: (?transOpts::TranslationOptions) =>
HandleAllocator
-> GlobalVar Mem -> Module -> IO (Some ModuleTranslation)
translateModule HandleAllocator
halloc GlobalVar Mem
mvar Module
m = do
Some LLVMContext x
ctx <- GlobalVar Mem -> Module -> IO (Some LLVMContext)
mkLLVMContext GlobalVar Mem
mvar Module
m
let nonceGen :: NonceGenerator IO GlobalNonceGenerator
nonceGen = HandleAllocator -> NonceGenerator IO GlobalNonceGenerator
haCounter HandleAllocator
halloc
LLVMContext x
-> forall a.
((16 <= ArchWidth x) => NatRepr (ArchWidth x) -> a) -> a
forall (arch :: LLVMArch).
LLVMContext arch
-> forall a.
((16 <= ArchWidth arch) => NatRepr (ArchWidth arch) -> a) -> a
llvmPtrWidth LLVMContext x
ctx (((16 <= ArchWidth x) =>
NatRepr (ArchWidth x) -> IO (Some ModuleTranslation))
-> IO (Some ModuleTranslation))
-> ((16 <= ArchWidth x) =>
NatRepr (ArchWidth x) -> IO (Some ModuleTranslation))
-> IO (Some ModuleTranslation)
forall a b. (a -> b) -> a -> b
$ \NatRepr (ArchWidth x)
wptr -> NatRepr (ArchWidth x)
-> (HasPtrWidth (ArchWidth x) => IO (Some ModuleTranslation))
-> IO (Some ModuleTranslation)
forall (w :: Natural) a.
(16 <= w) =>
NatRepr w -> (HasPtrWidth w => a) -> a
withPtrWidth NatRepr (ArchWidth x)
wptr ((HasPtrWidth (ArchWidth x) => IO (Some ModuleTranslation))
-> IO (Some ModuleTranslation))
-> (HasPtrWidth (ArchWidth x) => IO (Some ModuleTranslation))
-> IO (Some ModuleTranslation)
forall a b. (a -> b) -> a -> b
$
do let ?lc = LLVMContext x
ctxLLVMContext x
-> Getting TypeContext (LLVMContext x) TypeContext -> TypeContext
forall s a. s -> Getting a s a -> a
^.Getting TypeContext (LLVMContext x) TypeContext
forall (arch :: LLVMArch) (f :: Type -> Type).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx
let ctx' :: LLVMContext x
ctx' = LLVMContext x
ctx{ llvmGlobalAliases = globalAliases m
, llvmFunctionAliases = functionAliases m
}
Nonce GlobalNonceGenerator x
nonce <- NonceGenerator IO GlobalNonceGenerator
-> IO (Nonce GlobalNonceGenerator x)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO GlobalNonceGenerator
nonceGen
[(Define, Declare, SomeHandle)]
prep <- (Define -> IO (Define, Declare, SomeHandle))
-> [Define] -> IO [(Define, Declare, SomeHandle)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> [a] -> m [b]
mapM (HandleAllocator -> Define -> IO (Define, Declare, SomeHandle)
forall (wptr :: Natural).
(HasPtrWidth wptr, ?lc::TypeContext) =>
HandleAllocator -> Define -> IO (Define, Declare, SomeHandle)
prepareCFGMapEntry HandleAllocator
halloc) (Module -> [Define]
L.modDefines Module
m)
IORef ModuleCFGMap
cfgRef <- ModuleCFGMap -> IO (IORef ModuleCFGMap)
forall a. a -> IO (IORef a)
newIORef (ModuleCFGMap -> IO (IORef ModuleCFGMap))
-> ModuleCFGMap -> IO (IORef ModuleCFGMap)
forall a b. (a -> b) -> a -> b
$! [(Symbol, CFGMapEntry)] -> ModuleCFGMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Define -> Symbol
L.defName Define
def, Define -> SomeHandle -> CFGMapEntry
UntranslatedCFG Define
def SomeHandle
h) | (Define
def,Declare
_,SomeHandle
h) <- [(Define, Declare, SomeHandle)]
prep ]
Some ModuleTranslation -> IO (Some ModuleTranslation)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ModuleTranslation x -> Some ModuleTranslation
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (ModuleTranslation { _cfgMap :: IORef ModuleCFGMap
_cfgMap = IORef ModuleCFGMap
cfgRef
, _globalInitMap :: GlobalInitializerMap
_globalInitMap = LLVMContext x -> Module -> GlobalInitializerMap
forall (arch :: LLVMArch) (wptr :: Natural).
(?lc::TypeContext, HasPtrWidth wptr) =>
LLVMContext arch -> Module -> GlobalInitializerMap
makeGlobalMap LLVMContext x
ctx' Module
m
, _transContext :: LLVMContext x
_transContext = LLVMContext x
ctx'
, _modTransNonce :: Nonce GlobalNonceGenerator x
_modTransNonce = Nonce GlobalNonceGenerator x
nonce
, _modTransDefs :: [(Declare, SomeHandle)]
_modTransDefs = [ (Declare
decl,SomeHandle
h) | (Define
_,Declare
decl,SomeHandle
h) <- [(Define, Declare, SomeHandle)]
prep ]
, _modTransHalloc :: HandleAllocator
_modTransHalloc = HandleAllocator
halloc
, _modTransModule :: Module
_modTransModule = Module
m
, _modTransOpts :: TranslationOptions
_modTransOpts = ?transOpts::TranslationOptions
TranslationOptions
?transOpts
}))
prepareCFGMapEntry ::
(HasPtrWidth wptr, ?lc :: TypeContext) =>
HandleAllocator ->
L.Define ->
IO (L.Define, L.Declare, SomeHandle)
prepareCFGMapEntry :: forall (wptr :: Natural).
(HasPtrWidth wptr, ?lc::TypeContext) =>
HandleAllocator -> Define -> IO (Define, Declare, SomeHandle)
prepareCFGMapEntry HandleAllocator
halloc Define
def =
let decl :: Declare
decl = Define -> Declare
declareFromDefine Define
def in
let L.Symbol String
fstr = Define -> Symbol
L.defName Define
def in
let fn_name :: FunctionName
fn_name = Text -> FunctionName
functionNameFromText (Text -> FunctionName) -> Text -> FunctionName
forall a b. (a -> b) -> a -> b
$ String -> Text
Text.pack String
fstr in
Declare
-> (forall {args :: Ctx CrucibleType} {ret :: CrucibleType}.
CtxRepr args -> TypeRepr ret -> IO (Define, Declare, SomeHandle))
-> IO (Define, Declare, SomeHandle)
forall (wptr :: Natural) (m :: Type -> Type) a.
(?lc::TypeContext, HasPtrWidth wptr, MonadFail m) =>
Declare
-> (forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr args -> TypeRepr ret -> m a)
-> m a
llvmDeclToFunHandleRepr' Declare
decl ((forall {args :: Ctx CrucibleType} {ret :: CrucibleType}.
CtxRepr args -> TypeRepr ret -> IO (Define, Declare, SomeHandle))
-> IO (Define, Declare, SomeHandle))
-> (forall {args :: Ctx CrucibleType} {ret :: CrucibleType}.
CtxRepr args -> TypeRepr ret -> IO (Define, Declare, SomeHandle))
-> IO (Define, Declare, SomeHandle)
forall a b. (a -> b) -> a -> b
$ \CtxRepr args
argTys TypeRepr ret
retTy ->
do FnHandle args ret
h <- HandleAllocator
-> FunctionName
-> CtxRepr args
-> TypeRepr ret
-> IO (FnHandle args ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
HandleAllocator
-> FunctionName
-> Assignment TypeRepr args
-> TypeRepr ret
-> IO (FnHandle args ret)
mkHandle' HandleAllocator
halloc FunctionName
fn_name CtxRepr args
argTys TypeRepr ret
retTy
(Define, Declare, SomeHandle) -> IO (Define, Declare, SomeHandle)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Define
def, Declare
decl, FnHandle args ret -> SomeHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeHandle
SomeHandle FnHandle args ret
h)
getTranslatedCFG ::
ModuleTranslation arch ->
L.Symbol ->
IO (Maybe (L.Declare, C.AnyCFG LLVM, [LLVMTranslationWarning]))
getTranslatedCFG :: forall (arch :: LLVMArch).
ModuleTranslation arch
-> Symbol
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
getTranslatedCFG ModuleTranslation arch
mt Symbol
s =
do ModuleCFGMap
m <- IORef ModuleCFGMap -> IO ModuleCFGMap
forall a. IORef a -> IO a
readIORef (ModuleTranslation arch -> IORef ModuleCFGMap
forall (arch :: LLVMArch).
ModuleTranslation arch -> IORef ModuleCFGMap
_cfgMap ModuleTranslation arch
mt)
case Symbol -> ModuleCFGMap -> Maybe CFGMapEntry
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
s ModuleCFGMap
m of
Maybe CFGMapEntry
Nothing -> Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
forall a. Maybe a
Nothing
Just (TranslatedCFG Declare
decl AnyCFG LLVM
cfg) -> Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Declare, AnyCFG LLVM, [LLVMTranslationWarning])
-> Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
forall a. a -> Maybe a
Just (Declare
decl, AnyCFG LLVM
cfg, []))
Just (UntranslatedCFG Define
def (SomeHandle FnHandle args ret
h)) ->
let ?transOpts = ModuleTranslation arch -> TranslationOptions
forall (arch :: LLVMArch).
ModuleTranslation arch -> TranslationOptions
_modTransOpts ModuleTranslation arch
mt in
let ctx :: LLVMContext arch
ctx = ModuleTranslation arch -> LLVMContext arch
forall (arch :: LLVMArch).
ModuleTranslation arch -> LLVMContext arch
_transContext ModuleTranslation arch
mt in
LLVMContext arch
-> forall a.
((16 <= ArchWidth arch) => NatRepr (ArchWidth arch) -> a) -> a
forall (arch :: LLVMArch).
LLVMContext arch
-> forall a.
((16 <= ArchWidth arch) => NatRepr (ArchWidth arch) -> a) -> a
llvmPtrWidth LLVMContext arch
ctx (((16 <= ArchWidth arch) =>
NatRepr (ArchWidth arch)
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])))
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])))
-> ((16 <= ArchWidth arch) =>
NatRepr (ArchWidth arch)
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])))
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall a b. (a -> b) -> a -> b
$ \NatRepr (ArchWidth arch)
wptr -> NatRepr (ArchWidth arch)
-> (HasPtrWidth (ArchWidth arch) =>
IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])))
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall (w :: Natural) a.
(16 <= w) =>
NatRepr w -> (HasPtrWidth w => a) -> a
withPtrWidth NatRepr (ArchWidth arch)
wptr ((HasPtrWidth (ArchWidth arch) =>
IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])))
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])))
-> (HasPtrWidth (ArchWidth arch) =>
IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])))
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall a b. (a -> b) -> a -> b
$
do IORef [LLVMTranslationWarning]
warnRef <- [LLVMTranslationWarning] -> IO (IORef [LLVMTranslationWarning])
forall a. a -> IO (IORef a)
newIORef []
(Declare
decl, AnyCFG LLVM
cfg) <- FnHandle args ret
-> LLVMContext arch
-> IORef [LLVMTranslationWarning]
-> Define
-> IO (Declare, AnyCFG LLVM)
forall (arch :: LLVMArch) (wptr :: Natural)
(args :: Ctx CrucibleType) (ret :: CrucibleType).
(HasPtrWidth wptr, wptr ~ ArchWidth arch,
?transOpts::TranslationOptions) =>
FnHandle args ret
-> LLVMContext arch
-> IORef [LLVMTranslationWarning]
-> Define
-> IO (Declare, AnyCFG LLVM)
transDefine FnHandle args ret
h LLVMContext arch
ctx IORef [LLVMTranslationWarning]
warnRef Define
def
[LLVMTranslationWarning]
warns <- [LLVMTranslationWarning] -> [LLVMTranslationWarning]
forall a. [a] -> [a]
reverse ([LLVMTranslationWarning] -> [LLVMTranslationWarning])
-> IO [LLVMTranslationWarning] -> IO [LLVMTranslationWarning]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [LLVMTranslationWarning] -> IO [LLVMTranslationWarning]
forall a. IORef a -> IO a
readIORef IORef [LLVMTranslationWarning]
warnRef
IORef ModuleCFGMap -> (ModuleCFGMap -> ModuleCFGMap) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef (ModuleTranslation arch -> IORef ModuleCFGMap
forall (arch :: LLVMArch).
ModuleTranslation arch -> IORef ModuleCFGMap
_cfgMap ModuleTranslation arch
mt) (Symbol -> CFGMapEntry -> ModuleCFGMap -> ModuleCFGMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
s (Declare -> AnyCFG LLVM -> CFGMapEntry
TranslatedCFG Declare
decl AnyCFG LLVM
cfg))
Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
-> IO (Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning]))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Declare, AnyCFG LLVM, [LLVMTranslationWarning])
-> Maybe (Declare, AnyCFG LLVM, [LLVMTranslationWarning])
forall a. a -> Maybe a
Just (Declare
decl, AnyCFG LLVM
cfg, [LLVMTranslationWarning]
warns))
getTranslatedFnHandle ::
ModuleTranslation arch ->
L.Symbol ->
IO (Maybe (L.Declare, SomeHandle))
getTranslatedFnHandle :: forall (arch :: LLVMArch).
ModuleTranslation arch
-> Symbol -> IO (Maybe (Declare, SomeHandle))
getTranslatedFnHandle ModuleTranslation arch
mt Symbol
s =
do ModuleCFGMap
m <- IORef ModuleCFGMap -> IO ModuleCFGMap
forall a. IORef a -> IO a
readIORef (ModuleTranslation arch -> IORef ModuleCFGMap
forall (arch :: LLVMArch).
ModuleTranslation arch -> IORef ModuleCFGMap
_cfgMap ModuleTranslation arch
mt)
case Symbol -> ModuleCFGMap -> Maybe CFGMapEntry
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
s ModuleCFGMap
m of
Maybe CFGMapEntry
Nothing -> Maybe (Declare, SomeHandle) -> IO (Maybe (Declare, SomeHandle))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe (Declare, SomeHandle)
forall a. Maybe a
Nothing
Just (TranslatedCFG Declare
decl (C.AnyCFG CFG LLVM blocks init ret
cfg)) -> Maybe (Declare, SomeHandle) -> IO (Maybe (Declare, SomeHandle))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Declare, SomeHandle) -> Maybe (Declare, SomeHandle)
forall a. a -> Maybe a
Just (Declare
decl, FnHandle init ret -> SomeHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeHandle
SomeHandle (CFG LLVM blocks init ret -> FnHandle init ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
C.cfgHandle CFG LLVM blocks init ret
cfg)))
Just (UntranslatedCFG Define
def SomeHandle
h) -> Maybe (Declare, SomeHandle) -> IO (Maybe (Declare, SomeHandle))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Declare, SomeHandle) -> Maybe (Declare, SomeHandle)
forall a. a -> Maybe a
Just (Define -> Declare
declareFromDefine Define
def, SomeHandle
h))