{-# 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
( 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
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
}
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
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)
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
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
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]
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