-- |
-- Module           : Lang.Crucible.LLVM.Translation
-- Description      : Translation of LLVM AST into Crucible control-flow graph
-- Copyright        : (c) Galois, Inc 2014-2021
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
-- This module translates an LLVM 'Module' into a collection of Crucible
-- control-flow graphs, one per function.  The tricky parts of this translation
-- are 1) mapping LLVM types onto Crucible types in a sensible way and 2)
-- translating the phi-instructions of LLVM's SSA form.
--
-- To handle the translation of phi-functions, we first perform a
-- pre-pass over all the LLVM basic blocks looking for phi-functions
-- and build a datastructure that tells us what assignments to make
-- when jumping from block l to block l'.  We then emit instructions
-- to make these assignments in a separate Crucible basic block (see
-- 'definePhiBlock').  Thus, the translated CFG will generally have
-- more basic blocks than the original LLVM.
--
-- Points of note:
--
--  * Immediate (i.e., not in memory) structs and packed structs are translated the same.
--  * Undefined values generate special Crucible expressions (e.g., BVUndef) to
--     represent arbitrary bitpatterns.
--  * The floating-point domain is interpreted by IsSymInterface as either
--    the IEEE754 floating-point domain, the real domain, or a domain with
--    bitvector values and uninterpreted operations.
--
-- Some notes on undefined/poison values: (outcome of discussions between JHx and RWD)
--
-- * Continue to add Crucible expressions for undefined values as
-- required (e.g. for floating-point values).  Crucible itself is
-- currently treating undefined values as fresh symbolic inputs; it
-- should instead invent a new category of "arbitrary" values that get
-- passed down into the solvers in a way that is dependent on the task
-- at hand.  For example, in verification tasks, it is appropriate to
-- treat the arbitrary values the same as symbolic inputs.  However,
-- for preimage-finding tasks, the arbitrary values must be treated as
-- universally-quantified, unlike the symbolic inputs which are
-- existentially-quantified.
--
-- * For poison values, our implementation strategy is to assert
-- side conditions onto values that may create poison.  As opposed
-- to assertions (which must be satisfied because you passed through
-- a control-flow point) side conditions are intended to mean that
-- a condition must hold when a value is used (i.e., side conditions
-- follow data-flow).  So if a poison value is created but not examined
-- (e.g., because we later do a test to determine if the value is safe),
-- that should be allowed.
--
-- A (probably) partial list of things we intend to support, but do not yet:
--
--  * Various vector instructions. This includes a variety of instructions
--      that LLVM allows to take vector arguments, but are currently only
--      defined on scalar (nonvector) arguments. (Progress has been made on
--      this, but may not yet be complete).
--
-- A list of things that are unsupported and may never be:
--
--  * Computed jumps and blockaddress expressions
--  * Multithreading primitives
--  * Alternate calling conventions
------------------------------------------------------------------------

{-# 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


------------------------------------------------------------------------
-- Translation results

type ModuleCFGMap = Map L.Symbol CFGMapEntry

data CFGMapEntry
  = TranslatedCFG L.Declare (C.AnyCFG LLVM)
  | UntranslatedCFG L.Define SomeHandle

-- | The result of translating an LLVM module into Crucible CFGs.
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
        -- ^ A map from global names to their (constant) values
        -- Note: Willy-nilly global initialization may be unsound in the
        -- presence of compositional verification.
      , forall (arch :: LLVMArch).
ModuleTranslation arch -> Nonce GlobalNonceGenerator arch
_modTransNonce :: !(Nonce GlobalNonceGenerator arch)
        -- ^ For a reasonably quick 'testEquality' instance
      , forall (arch :: LLVMArch).
ModuleTranslation arch -> [(Declare, SomeHandle)]
_modTransDefs :: ![(L.Declare, SomeHandle)]
        -- ^ A collection of declarations for all the functions
        --   defined in this module.
      , 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

-- | This function pre-computes the types of all the crucible registers by scanning
--   through each basic block and finding the place where that register is assigned.
--   Because LLVM programs are in SSA form, this will occur in exactly one place.
--   The type of the register is inferred from the instruction that assigns to it
--   and is recorded in the ident map.
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


-- | Generate crucible code for each LLVM statement in turn.
generateStmts :: (?transOpts :: TranslationOptions)
        => TypeRepr ret
        -> L.BlockLabel
        -> Set L.Ident {- ^ Set of usable identifiers -}
        -> [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
           -- a result statement assigns the result of the instruction into a register
           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)

           -- an effect statement simply executes the instruction for its effects and discards the result
           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)

-- | Search for calls to intrinsic 'llvm.dbg.declare' and copy the
-- metadata onto the corresponding 'alloca' statement.  Also copy
-- metadata backwards from 'bitcast' statements toward 'alloca'.
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')
              --error $ "Identifier not found: " ++ show x ++ "\nPossible identifiers: " ++ show (Map.keys m)

        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')

        -- This is needlessly fragile. Let's just ignore debug declarations we don't understand.
        -- L.Effect (L.Call _ _ (L.ValSymbol "llvm.dbg.declare") args) md ->
        --  error $ "Ill-formed arguments to llvm.dbg.declare: " ++ show (args, md)

        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

 -- The typical values available here will be something like:
 --
 -- > L.difDirectory = "/home/joeuser/work"
 -- > L.difFilename  = "src/lib/foo.c"
 --
 -- At the present time, only the 'difFilename' is used for the
 -- relative path because combining these to form an absolute path
 -- would cause superfluous result differences (e.g. golden test
 -- failures) and potentially leak information.
 --
 -- The downside is that relative paths may make it harder for various
 -- tools (e.g. emacs) to locate the offending source file.  The
 -- suggested method for handling this is to have the emacs compile
 -- function emit an initial rooted directory location in the proper
 -- syntax, but if this is problematic, a future direction would be to
 -- add a config option to control whether an absolute or a relative
 -- path is desired (defaulting to the latter).
 --
 -- [The previous implementation always generated absolute paths, but
 -- was careful to check if `difFilename` was already absolute.]
 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

-- | Lookup the block info for the given LLVM block and then define a new crucible block
--   by translating the given LLVM statements.
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!"

-- | Do some initial preprocessing to find all the phi nodes in the program
--   and to preallocate all the crucible registers we will need based on the LLVM
--   types of all the LLVM registers.  Then translate each LLVM basic block in turn.
--
--   This step introduces a new dummy entry point that simply jumps to the LLVM entry
--   point.  It is inconvenient to avoid doing this when using the Generator interface.
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)


-- | Check that the input LLVM CFG satisfies the def/use invariant,
--   and raise an error if some virtual register has a use site that
--   is not dominated by its definition site.
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
--
-- | Translate a single LLVM function definition into a crucible CFG.
--
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

-- | Translate a module into Crucible control-flow graphs.
-- Return the translated module and a list of warning messages
-- generated during translation.
-- Note: We may want to add a map from symbols to existing function handles
-- if we want to support dynamic loading.
translateModule :: (?transOpts :: TranslationOptions)
                => HandleAllocator -- ^ Generator for nonces.
                -> GlobalVar Mem   -- ^ Memory model to associate with this context
                -> L.Module        -- ^ Module to translate
                -> 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 -- implicitly passed to makeGlobalMap
       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)


-- | Given a 'ModuleTranslation' and a function symbol corresponding to a function
--   defined in the module, attempt to look up the symbol name and retrieve the corresponding
--   Crucible CFG. This will load and translate the CFG if this is the first time
--   the given symbol is requested.
--
--   Will return 'Nothing' if the symbol does not refer to a function defined in this
--   module.
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))

-- | Look up the signature and function handle for a function defined in this
--   module translation.  This does not trigger translation of the named function
--   into Crucible if it has not already been requested.
--
--   Will return 'Nothing' if the symbol does not refer to a function defined in this
--   module.
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))