{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.Translation.Types
-- Description      : Translation of LLVM AST into Crucible control-flow graph
-- Copyright        : (c) Galois, Inc 2014-2015
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
--
-- This module defines the translation from LLVM types to Crucible types.
--
-- The translation of the LLVM types themselves is not so difficult;
-- however, navigating the fact that Crucible expressions are strongly
-- typed at the Haskell level, whereas the LLVM types are not makes for
-- some slightly strange programming idioms.  In particular, all the
-- functions that do the type translation are written in a polymorphic
-- continuation-passing style.
----------------------------------------------------------------------

module Lang.Crucible.LLVM.Translation.Types
( VarArgs
, varArgsRepr
, llvmTypesAsCtx
, llvmTypeAsRepr
, llvmRetTypeAsRepr
, llvmDeclToFunHandleRepr
, llvmDeclToFunHandleRepr'
, LLVMPointerType
, pattern PtrWidth
, pattern LLVMPointerRepr
, declareFromDefine
, allModuleDeclares
, liftMemType
, liftRetType
, liftDeclare
) where

import qualified Control.Monad.Fail as Fail
import           Data.Foldable
import           Data.String

import qualified Text.LLVM.AST as L
import           Prettyprinter

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


import           Lang.Crucible.Panic(panic)
import           Lang.Crucible.Types

import           Lang.Crucible.LLVM.MemModel.Pointer
import           Lang.Crucible.LLVM.MemType
import           Lang.Crucible.LLVM.MalformedLLVMModule
import qualified Lang.Crucible.LLVM.PrettyPrint as LPP
import           Lang.Crucible.LLVM.TypeContext as TyCtx



type VarArgs   = VectorType AnyType

varArgsRepr :: TypeRepr VarArgs
varArgsRepr :: TypeRepr VarArgs
varArgsRepr = TypeRepr AnyType -> TypeRepr VarArgs
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr AnyType
AnyRepr

------------------------------------------------------------------------
-- LLVM AST utilities

declareFromDefine :: L.Define -> L.Declare
declareFromDefine :: Define -> Declare
declareFromDefine Define
d =
  L.Declare { decLinkage :: Maybe Linkage
L.decLinkage = Define -> Maybe Linkage
L.defLinkage Define
d
            , decVisibility :: Maybe Visibility
L.decVisibility = Define -> Maybe Visibility
L.defVisibility Define
d
            , decRetType :: Type
L.decRetType = Define -> Type
L.defRetType Define
d
            , decName :: Symbol
L.decName = Define -> Symbol
L.defName Define
d
            , decArgs :: [Type]
L.decArgs = Typed Ident -> Type
forall a. Typed a -> Type
L.typedType (Typed Ident -> Type) -> [Typed Ident] -> [Type]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Define -> [Typed Ident]
L.defArgs Define
d
            , decVarArgs :: Bool
L.decVarArgs = Define -> Bool
L.defVarArgs Define
d
            , decAttrs :: [FunAttr]
L.decAttrs   = Define -> [FunAttr]
L.defAttrs Define
d
            , decComdat :: Maybe String
L.decComdat  = Maybe String
forall a. Monoid a => a
mempty
            }

-- | Return all declarations derived from both external symbols and
-- internal definitions.
allModuleDeclares :: L.Module -> [L.Declare]
allModuleDeclares :: Module -> [Declare]
allModuleDeclares Module
m = Module -> [Declare]
L.modDeclares Module
m [Declare] -> [Declare] -> [Declare]
forall a. [a] -> [a] -> [a]
++ [Declare]
def_decls
  where def_decls :: [Declare]
def_decls = Define -> Declare
declareFromDefine (Define -> Declare) -> [Define] -> [Declare]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Module -> [Define]
L.modDefines Module
m

-----------------------------------------------------------------------------------------
-- Type translations

-- | Translate a list of LLVM expressions into a crucible type context,
--   which is passed into the given continuation.
llvmTypesAsCtx :: forall a wptr
                . HasPtrWidth wptr
               => [MemType]
               -> (forall ctx. CtxRepr ctx -> a)
               -> a
llvmTypesAsCtx :: forall a (wptr :: Natural).
HasPtrWidth wptr =>
[MemType]
-> (forall (ctx :: Ctx CrucibleType). CtxRepr ctx -> a) -> a
llvmTypesAsCtx [MemType]
xs forall (ctx :: Ctx CrucibleType). CtxRepr ctx -> a
f = [Some TypeRepr] -> CtxRepr EmptyCtx -> a
forall (ctx :: Ctx CrucibleType).
[Some TypeRepr] -> CtxRepr ctx -> a
go ((MemType -> [Some TypeRepr]) -> [MemType] -> [Some TypeRepr]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap (Maybe (Some TypeRepr) -> [Some TypeRepr]
forall a. Maybe a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (Maybe (Some TypeRepr) -> [Some TypeRepr])
-> (MemType -> Maybe (Some TypeRepr)) -> MemType -> [Some TypeRepr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MemType -> Maybe (Some TypeRepr)
forall (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> Maybe (Some TypeRepr)
llvmTypeToRepr) [MemType]
xs) CtxRepr EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty
 where go :: forall ctx. [Some TypeRepr] -> CtxRepr ctx -> a
       go :: forall (ctx :: Ctx CrucibleType).
[Some TypeRepr] -> CtxRepr ctx -> a
go []       CtxRepr ctx
ctx      = CtxRepr ctx -> a
forall (ctx :: Ctx CrucibleType). CtxRepr ctx -> a
f CtxRepr ctx
ctx
       go (Some TypeRepr x
tp:[Some TypeRepr]
tps) CtxRepr ctx
ctx = [Some TypeRepr] -> CtxRepr (ctx ::> x) -> a
forall (ctx :: Ctx CrucibleType).
[Some TypeRepr] -> CtxRepr ctx -> a
go [Some TypeRepr]
tps (CtxRepr ctx
ctx CtxRepr ctx -> TypeRepr x -> CtxRepr (ctx ::> x)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> TypeRepr x
tp)

-- | Translate an LLVM type into a crucible type, which is passed into
--   the given continuation
llvmTypeAsRepr :: forall a wptr
                . HasPtrWidth wptr
               => MemType
               -> (forall tp. TypeRepr tp -> a)
               -> a
llvmTypeAsRepr :: forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
xs forall (tp :: CrucibleType). TypeRepr tp -> a
f = Maybe (Some TypeRepr) -> a
go (MemType -> Maybe (Some TypeRepr)
forall (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> Maybe (Some TypeRepr)
llvmTypeToRepr MemType
xs)
 where go :: Maybe (Some TypeRepr) -> a
       go :: Maybe (Some TypeRepr) -> a
go Maybe (Some TypeRepr)
Nothing         = TypeRepr 'UnitType -> a
forall (tp :: CrucibleType). TypeRepr tp -> a
f TypeRepr 'UnitType
UnitRepr
       go (Just (Some TypeRepr x
x)) = TypeRepr x -> a
forall (tp :: CrucibleType). TypeRepr tp -> a
f TypeRepr x
x

-- | Translate an LLVM return type into a crucible type, which is passed into
--   the given continuation
llvmRetTypeAsRepr :: forall a wptr
                   . HasPtrWidth wptr
                  => Maybe MemType
                  -> (forall tp. TypeRepr tp -> a)
                  -> a
llvmRetTypeAsRepr :: forall a (wptr :: Natural).
HasPtrWidth wptr =>
Maybe MemType
-> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmRetTypeAsRepr Maybe MemType
Nothing   forall (tp :: CrucibleType). TypeRepr tp -> a
f = TypeRepr 'UnitType -> a
forall (tp :: CrucibleType). TypeRepr tp -> a
f TypeRepr 'UnitType
UnitRepr
llvmRetTypeAsRepr (Just MemType
tp) forall (tp :: CrucibleType). TypeRepr tp -> a
f = MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp TypeRepr tp -> a
forall (tp :: CrucibleType). TypeRepr tp -> a
f

-- | Actually perform the type translation
llvmTypeToRepr :: HasPtrWidth wptr => MemType -> Maybe (Some TypeRepr)
llvmTypeToRepr :: forall (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> Maybe (Some TypeRepr)
llvmTypeToRepr (ArrayType Natural
_ MemType
tp)  = Some TypeRepr -> Maybe (Some TypeRepr)
forall a. a -> Maybe a
Just (Some TypeRepr -> Maybe (Some TypeRepr))
-> Some TypeRepr -> Maybe (Some TypeRepr)
forall a b. (a -> b) -> a -> b
$ MemType
-> (forall (tp :: CrucibleType). TypeRepr tp -> Some TypeRepr)
-> Some TypeRepr
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp (\TypeRepr tp
t -> TypeRepr ('VectorType tp) -> Some TypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (TypeRepr tp -> TypeRepr ('VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
t))
llvmTypeToRepr (VecType Natural
_ MemType
tp)    = Some TypeRepr -> Maybe (Some TypeRepr)
forall a. a -> Maybe a
Just (Some TypeRepr -> Maybe (Some TypeRepr))
-> Some TypeRepr -> Maybe (Some TypeRepr)
forall a b. (a -> b) -> a -> b
$ MemType
-> (forall (tp :: CrucibleType). TypeRepr tp -> Some TypeRepr)
-> Some TypeRepr
forall a (wptr :: Natural).
HasPtrWidth wptr =>
MemType -> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmTypeAsRepr MemType
tp (\TypeRepr tp
t-> TypeRepr ('VectorType tp) -> Some TypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (TypeRepr tp -> TypeRepr ('VectorType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('VectorType tp1)
VectorRepr TypeRepr tp
t))
llvmTypeToRepr (StructType StructInfo
si)   = Some TypeRepr -> Maybe (Some TypeRepr)
forall a. a -> Maybe a
Just (Some TypeRepr -> Maybe (Some TypeRepr))
-> Some TypeRepr -> Maybe (Some TypeRepr)
forall a b. (a -> b) -> a -> b
$ [MemType]
-> (forall (ctx :: Ctx CrucibleType). CtxRepr ctx -> Some TypeRepr)
-> Some TypeRepr
forall a (wptr :: Natural).
HasPtrWidth wptr =>
[MemType]
-> (forall (ctx :: Ctx CrucibleType). CtxRepr ctx -> a) -> a
llvmTypesAsCtx [MemType]
tps (\CtxRepr ctx
ts -> TypeRepr ('StructType ctx) -> Some TypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (CtxRepr ctx -> TypeRepr ('StructType ctx)
forall (ctx :: Ctx CrucibleType).
CtxRepr ctx -> TypeRepr ('StructType ctx)
StructRepr CtxRepr ctx
ts))
  where tps :: [MemType]
tps = (FieldInfo -> MemType) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> [a] -> [b]
map FieldInfo -> MemType
fiType ([FieldInfo] -> [MemType]) -> [FieldInfo] -> [MemType]
forall a b. (a -> b) -> a -> b
$ Vector FieldInfo -> [FieldInfo]
forall a. Vector a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (Vector FieldInfo -> [FieldInfo])
-> Vector FieldInfo -> [FieldInfo]
forall a b. (a -> b) -> a -> b
$ StructInfo -> Vector FieldInfo
siFields StructInfo
si
llvmTypeToRepr (PtrType SymType
_)  = Some TypeRepr -> Maybe (Some TypeRepr)
forall a. a -> Maybe a
Just (Some TypeRepr -> Maybe (Some TypeRepr))
-> Some TypeRepr -> Maybe (Some TypeRepr)
forall a b. (a -> b) -> a -> b
$ TypeRepr (LLVMPointerType wptr) -> Some TypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (NatRepr wptr -> TypeRepr (LLVMPointerType wptr)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth)
llvmTypeToRepr MemType
PtrOpaqueType = Some TypeRepr -> Maybe (Some TypeRepr)
forall a. a -> Maybe a
Just (Some TypeRepr -> Maybe (Some TypeRepr))
-> Some TypeRepr -> Maybe (Some TypeRepr)
forall a b. (a -> b) -> a -> b
$ TypeRepr (LLVMPointerType wptr) -> Some TypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (NatRepr wptr -> TypeRepr (LLVMPointerType wptr)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth)
llvmTypeToRepr MemType
FloatType    = Some TypeRepr -> Maybe (Some TypeRepr)
forall a. a -> Maybe a
Just (Some TypeRepr -> Maybe (Some TypeRepr))
-> Some TypeRepr -> Maybe (Some TypeRepr)
forall a b. (a -> b) -> a -> b
$ TypeRepr ('FloatType 'SingleFloat) -> Some TypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (FloatInfoRepr 'SingleFloat -> TypeRepr ('FloatType 'SingleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'SingleFloat
SingleFloatRepr)
llvmTypeToRepr MemType
DoubleType   = Some TypeRepr -> Maybe (Some TypeRepr)
forall a. a -> Maybe a
Just (Some TypeRepr -> Maybe (Some TypeRepr))
-> Some TypeRepr -> Maybe (Some TypeRepr)
forall a b. (a -> b) -> a -> b
$ TypeRepr ('FloatType 'DoubleFloat) -> Some TypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (FloatInfoRepr 'DoubleFloat -> TypeRepr ('FloatType 'DoubleFloat)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'DoubleFloat
DoubleFloatRepr)
llvmTypeToRepr MemType
X86_FP80Type = Some TypeRepr -> Maybe (Some TypeRepr)
forall a. a -> Maybe a
Just (Some TypeRepr -> Maybe (Some TypeRepr))
-> Some TypeRepr -> Maybe (Some TypeRepr)
forall a b. (a -> b) -> a -> b
$ TypeRepr ('FloatType 'X86_80Float) -> Some TypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (FloatInfoRepr 'X86_80Float -> TypeRepr ('FloatType 'X86_80Float)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr 'X86_80Float
X86_80FloatRepr)
llvmTypeToRepr MemType
MetadataType = Maybe (Some TypeRepr)
forall a. Maybe a
Nothing
llvmTypeToRepr (IntType Natural
n) =
   case Natural -> Some NatRepr
mkNatRepr Natural
n of
     Some NatRepr x
w | Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w -> Some TypeRepr -> Maybe (Some TypeRepr)
forall a. a -> Maybe a
Just (Some TypeRepr -> Maybe (Some TypeRepr))
-> Some TypeRepr -> Maybe (Some TypeRepr)
forall a b. (a -> b) -> a -> b
$ TypeRepr (LLVMPointerType x) -> Some TypeRepr
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (NatRepr x -> TypeRepr (LLVMPointerType x)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr x
w)
     Some NatRepr
_ -> String -> [String] -> Maybe (Some TypeRepr)
forall a. HasCallStack => String -> [String] -> a
panic String
"Translation.Types.llvmTypeToRepr"
              [String
" *** invalid integer width " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
n]

-- | Compute the function Crucible function signature
--   that corresponds to the given LLVM function declaration.
llvmDeclToFunHandleRepr
   :: HasPtrWidth wptr
   => FunDecl
   -> (forall args ret. CtxRepr args -> TypeRepr ret -> a)
   -> a
llvmDeclToFunHandleRepr :: forall (wptr :: Natural) a.
HasPtrWidth wptr =>
FunDecl
-> (forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
    CtxRepr args -> TypeRepr ret -> a)
-> a
llvmDeclToFunHandleRepr FunDecl
decl forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr args -> TypeRepr ret -> a
k =
  [MemType]
-> (forall {ctx :: Ctx CrucibleType}. CtxRepr ctx -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
[MemType]
-> (forall (ctx :: Ctx CrucibleType). CtxRepr ctx -> a) -> a
llvmTypesAsCtx (FunDecl -> [MemType]
fdArgTypes FunDecl
decl) ((forall {ctx :: Ctx CrucibleType}. CtxRepr ctx -> a) -> a)
-> (forall {ctx :: Ctx CrucibleType}. CtxRepr ctx -> a) -> a
forall a b. (a -> b) -> a -> b
$ \CtxRepr ctx
args ->
    Maybe MemType
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a (wptr :: Natural).
HasPtrWidth wptr =>
Maybe MemType
-> (forall (tp :: CrucibleType). TypeRepr tp -> a) -> a
llvmRetTypeAsRepr (FunDecl -> Maybe MemType
fdRetType FunDecl
decl) ((forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a)
-> (forall {tp :: CrucibleType}. TypeRepr tp -> a) -> a
forall a b. (a -> b) -> a -> b
$ \TypeRepr tp
ret ->
      if FunDecl -> Bool
fdVarArgs FunDecl
decl then
        CtxRepr (ctx ::> VarArgs) -> TypeRepr tp -> a
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr args -> TypeRepr ret -> a
k (CtxRepr ctx
args CtxRepr ctx -> TypeRepr VarArgs -> CtxRepr (ctx ::> VarArgs)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> TypeRepr VarArgs
varArgsRepr) TypeRepr tp
ret
      else
        CtxRepr ctx -> TypeRepr tp -> a
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr args -> TypeRepr ret -> a
k CtxRepr ctx
args TypeRepr tp
ret


llvmDeclToFunHandleRepr' ::
   (?lc :: TypeContext, HasPtrWidth wptr, Fail.MonadFail m) =>
   L.Declare ->
   (forall args ret. CtxRepr args -> TypeRepr ret -> m a) ->
   m a
llvmDeclToFunHandleRepr' :: 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 -> m a
k =
  case Declare -> Either String FunDecl
forall (m :: Type -> Type).
(?lc::TypeContext, MonadError String m) =>
Declare -> m FunDecl
liftDeclare Declare
decl of
    Left String
msg ->
      Doc Void -> [Doc Void] -> m a
forall a. Doc Void -> [Doc Void] -> a
malformedLLVMModule
        ( Doc Void
"Invalid declaration for:" Doc Void -> Doc Void -> Doc Void
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc Void
forall a. IsString a => String -> a
fromString (Symbol -> String
forall a. Show a => a -> String
show (Declare -> Symbol
L.decName Declare
decl)) )
        [ String -> Doc Void
forall a. IsString a => String -> a
fromString (Doc -> String
forall a. Show a => a -> String
show (Declare -> Doc
LPP.ppDeclare Declare
decl))
        , String -> Doc Void
forall a. IsString a => String -> a
fromString String
msg
        ]

    Right FunDecl
fd -> FunDecl
-> (forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
    CtxRepr args -> TypeRepr ret -> m a)
-> m a
forall (wptr :: Natural) a.
HasPtrWidth wptr =>
FunDecl
-> (forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
    CtxRepr args -> TypeRepr ret -> a)
-> a
llvmDeclToFunHandleRepr FunDecl
fd CtxRepr args -> TypeRepr ret -> m a
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr args -> TypeRepr ret -> m a
k