crucible-llvm-0.6: src/Lang/Crucible/LLVM/Intrinsics.hs
-- |
-- Module : Lang.Crucible.LLVM.Intrinsics
-- Description : Override definitions for LLVM intrinsic and basic
-- library functions
-- Copyright : (c) Galois, Inc 2015-2016
-- License : BSD3
-- Maintainer : Rob Dockins <rdockins@galois.com>
-- Stability : provisional
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
module Lang.Crucible.LLVM.Intrinsics
( LLVM
, llvmIntrinsicTypes
, LLVMOverride(..)
, register_llvm_overrides
, register_llvm_overrides_
, llvmDeclToFunHandleRepr
, module Lang.Crucible.LLVM.Intrinsics.Common
, module Lang.Crucible.LLVM.Intrinsics.Options
) where
import Control.Lens hiding (op, (:>), Empty)
import Control.Monad (forM_)
import Control.Monad.Reader (ReaderT(..))
import Control.Monad.Trans.Maybe
import Data.Foldable (asum)
import Data.List (stripPrefix, tails, isPrefixOf)
import qualified Text.LLVM.AST as L
import qualified ABI.Itanium as ABI
import qualified Data.Parameterized.Map as MapF
import What4.Interface
import Lang.Crucible.Backend
import Lang.Crucible.Types
import Lang.Crucible.Simulator.Intrinsics
import Lang.Crucible.Simulator.OverrideSim
import Lang.Crucible.LLVM.Extension (ArchWidth, LLVM)
import Lang.Crucible.LLVM.MemModel
import Lang.Crucible.LLVM.Translation.Monad
import Lang.Crucible.LLVM.Translation.Types
import Lang.Crucible.LLVM.TypeContext (TypeContext)
import Lang.Crucible.LLVM.Intrinsics.Common
import qualified Lang.Crucible.LLVM.Intrinsics.LLVM as LLVM
import qualified Lang.Crucible.LLVM.Intrinsics.Libc as Libc
import qualified Lang.Crucible.LLVM.Intrinsics.Libcxx as Libcxx
import Lang.Crucible.LLVM.Intrinsics.Options
llvmIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym
llvmIntrinsicTypes =
MapF.insert (knownSymbol :: SymbolRepr "LLVM_memory") IntrinsicMuxFn $
MapF.insert (knownSymbol :: SymbolRepr "LLVM_pointer") IntrinsicMuxFn $
MapF.empty
-- | Register all declare and define overrides
register_llvm_overrides ::
( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
L.Module ->
[OverrideTemplate p sym arch rtp l a] {- ^ Additional "define" overrides -} ->
[OverrideTemplate p sym arch rtp l a] {- ^ Additional "declare" overrides -} ->
LLVMContext arch ->
OverrideSim p sym LLVM rtp l a ()
register_llvm_overrides llvmModule defineOvrs declareOvrs llvmctx =
do register_llvm_define_overrides llvmModule defineOvrs llvmctx
register_llvm_declare_overrides llvmModule declareOvrs llvmctx
-- | Filter the initial list of templates to only those that could
-- possibly match the given declaration based on straightforward,
-- relatively cheap string tests on the name of the declaration.
--
-- Any remaining templates will then examine the declaration in
-- more detail, including examining function arguments
-- and the structure of C++ demangled names to extract more information.
filterTemplates ::
[OverrideTemplate p sym arch rtp l a] ->
L.Declare ->
[OverrideTemplate p sym arch rtp l a]
filterTemplates ts decl = filter (f . overrideTemplateMatcher) ts
where
L.Symbol nm = L.decName decl
f (ExactMatch x) = x == nm
f (PrefixMatch pfx) = pfx `isPrefixOf` nm
f (SubstringsMatch as) = filterSubstrings as nm
filterSubstrings [] _ = True
filterSubstrings (a:as) xs =
case restAfterSubstring a xs of
Nothing -> False
Just rest -> filterSubstrings as rest
restAfterSubstring :: String -> String -> Maybe String
restAfterSubstring sub xs = asum [ stripPrefix sub tl | tl <- tails xs ]
-- | Helper function for registering overrides
register_llvm_overrides_ ::
LLVMContext arch ->
[OverrideTemplate p sym arch rtp l a] ->
[L.Declare] ->
OverrideSim p sym LLVM rtp l a ()
register_llvm_overrides_ llvmctx acts decls =
forM_ decls $ \decl ->
do let acts' = filterTemplates acts decl
let L.Symbol nm = L.decName decl
let declnm = either (const Nothing) Just $ ABI.demangleName nm
runMaybeT (flip runReaderT (decl,declnm,llvmctx) $ asum (map overrideTemplateAction acts'))
register_llvm_define_overrides ::
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
L.Module ->
[OverrideTemplate p sym arch rtp l a] ->
LLVMContext arch ->
OverrideSim p sym LLVM rtp l a ()
register_llvm_define_overrides llvmModule addlOvrs llvmctx =
let ?lc = llvmctx^.llvmTypeCtx in
register_llvm_overrides_ llvmctx (addlOvrs ++ define_overrides) $
(allModuleDeclares llvmModule)
register_llvm_declare_overrides ::
( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
L.Module ->
[OverrideTemplate p sym arch rtp l a] ->
LLVMContext arch ->
OverrideSim p sym LLVM rtp l a ()
register_llvm_declare_overrides llvmModule addlOvrs llvmctx =
let ?lc = llvmctx^.llvmTypeCtx
in register_llvm_overrides_ llvmctx (addlOvrs ++ declare_overrides) $
L.modDeclares llvmModule
-- | Register overrides for declared-but-not-defined functions
declare_overrides ::
( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
, ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
[OverrideTemplate p sym arch rtp l a]
declare_overrides =
[ basic_llvm_override LLVM.llvmLifetimeStartOverride
, basic_llvm_override LLVM.llvmLifetimeEndOverride
, basic_llvm_override (LLVM.llvmLifetimeOverrideOverload "start" (knownNat @8))
, basic_llvm_override (LLVM.llvmLifetimeOverrideOverload "end" (knownNat @8))
, basic_llvm_override (LLVM.llvmLifetimeOverrideOverload_opaque "start")
, basic_llvm_override (LLVM.llvmLifetimeOverrideOverload_opaque "end")
, basic_llvm_override (LLVM.llvmInvariantStartOverride (knownNat @8))
, basic_llvm_override LLVM.llvmInvariantStartOverride_opaque
, basic_llvm_override (LLVM.llvmInvariantEndOverride (knownNat @8))
, basic_llvm_override LLVM.llvmInvariantEndOverride_opaque
, basic_llvm_override LLVM.llvmAssumeOverride
, basic_llvm_override LLVM.llvmTrapOverride
, basic_llvm_override LLVM.llvmUBSanTrapOverride
, basic_llvm_override LLVM.llvmMemcpyOverride_8_8_32
, basic_llvm_override LLVM.llvmMemcpyOverride_8_8_32_noalign
, basic_llvm_override LLVM.llvmMemcpyOverride_8_8_32_noalign_opaque
, basic_llvm_override LLVM.llvmMemcpyOverride_8_8_64
, basic_llvm_override LLVM.llvmMemcpyOverride_8_8_64_noalign
, basic_llvm_override LLVM.llvmMemcpyOverride_8_8_64_noalign_opaque
, basic_llvm_override LLVM.llvmMemmoveOverride_8_8_32
, basic_llvm_override LLVM.llvmMemmoveOverride_8_8_32_noalign
, basic_llvm_override LLVM.llvmMemmoveOverride_8_8_32_noalign_opaque
, basic_llvm_override LLVM.llvmMemmoveOverride_8_8_64
, basic_llvm_override LLVM.llvmMemmoveOverride_8_8_64_noalign
, basic_llvm_override LLVM.llvmMemmoveOverride_8_8_64_noalign_opaque
, basic_llvm_override LLVM.llvmMemsetOverride_8_32
, basic_llvm_override LLVM.llvmMemsetOverride_8_32_noalign
, basic_llvm_override LLVM.llvmMemsetOverride_8_32_noalign_opaque
, basic_llvm_override LLVM.llvmMemsetOverride_8_64
, basic_llvm_override LLVM.llvmMemsetOverride_8_64_noalign
, basic_llvm_override LLVM.llvmMemsetOverride_8_64_noalign_opaque
, basic_llvm_override LLVM.llvmObjectsizeOverride_32
, basic_llvm_override LLVM.llvmObjectsizeOverride_64
, basic_llvm_override LLVM.llvmObjectsizeOverride_32_null
, basic_llvm_override LLVM.llvmObjectsizeOverride_64_null
, basic_llvm_override LLVM.llvmObjectsizeOverride_32_null_dynamic
, basic_llvm_override LLVM.llvmObjectsizeOverride_64_null_dynamic
, basic_llvm_override LLVM.llvmObjectsizeOverride_32_null_dynamic_opaque
, basic_llvm_override LLVM.llvmObjectsizeOverride_64_null_dynamic_opaque
, basic_llvm_override LLVM.llvmPrefetchOverride
, basic_llvm_override LLVM.llvmPrefetchOverride_opaque
, basic_llvm_override LLVM.llvmPrefetchOverride_preLLVM10
, basic_llvm_override LLVM.llvmStacksave
, basic_llvm_override LLVM.llvmStackrestore
, polymorphic1_llvm_override "llvm.ctlz"
(\w -> SomeLLVMOverride (LLVM.llvmCtlz w))
, polymorphic1_llvm_override "llvm.cttz"
(\w -> SomeLLVMOverride (LLVM.llvmCttz w))
, polymorphic1_llvm_override "llvm.ctpop"
(\w -> SomeLLVMOverride (LLVM.llvmCtpop w))
, polymorphic1_llvm_override "llvm.bitreverse"
(\w -> SomeLLVMOverride (LLVM.llvmBitreverse w))
, polymorphic1_llvm_override "llvm.abs"
(\w -> SomeLLVMOverride (LLVM.llvmAbsOverride w))
, basic_llvm_override (LLVM.llvmBSwapOverride (knownNat @2)) -- 16 = 2 * 8
, basic_llvm_override (LLVM.llvmBSwapOverride (knownNat @4)) -- 32 = 4 * 8
, basic_llvm_override (LLVM.llvmBSwapOverride (knownNat @6)) -- 48 = 6 * 8
, basic_llvm_override (LLVM.llvmBSwapOverride (knownNat @8)) -- 64 = 8 * 8
, basic_llvm_override (LLVM.llvmBSwapOverride (knownNat @10)) -- 80 = 10 * 8
, basic_llvm_override (LLVM.llvmBSwapOverride (knownNat @12)) -- 96 = 12 * 8
, basic_llvm_override (LLVM.llvmBSwapOverride (knownNat @14)) -- 112 = 14 * 8
, basic_llvm_override (LLVM.llvmBSwapOverride (knownNat @16)) -- 128 = 16 * 8
, polymorphic1_llvm_override "llvm.fshl"
(\w -> SomeLLVMOverride (LLVM.llvmFshl w))
, polymorphic1_llvm_override "llvm.fshr"
(\w -> SomeLLVMOverride (LLVM.llvmFshr w))
, polymorphic1_llvm_override "llvm.expect"
(\w -> SomeLLVMOverride (LLVM.llvmExpectOverride w))
, polymorphic1_llvm_override "llvm.sadd.with.overflow"
(\w -> SomeLLVMOverride (LLVM.llvmSaddWithOverflow w))
, polymorphic1_llvm_override "llvm.uadd.with.overflow"
(\w -> SomeLLVMOverride (LLVM.llvmUaddWithOverflow w))
, polymorphic1_llvm_override "llvm.ssub.with.overflow"
(\w -> SomeLLVMOverride (LLVM.llvmSsubWithOverflow w))
, polymorphic1_llvm_override "llvm.usub.with.overflow"
(\w -> SomeLLVMOverride (LLVM.llvmUsubWithOverflow w))
, polymorphic1_llvm_override "llvm.smul.with.overflow"
(\w -> SomeLLVMOverride (LLVM.llvmSmulWithOverflow w))
, polymorphic1_llvm_override "llvm.umul.with.overflow"
(\w -> SomeLLVMOverride (LLVM.llvmUmulWithOverflow w))
, polymorphic1_llvm_override "llvm.smax"
(\w -> SomeLLVMOverride (LLVM.llvmSmax w))
, polymorphic1_llvm_override "llvm.smin"
(\w -> SomeLLVMOverride (LLVM.llvmSmin w))
, polymorphic1_llvm_override "llvm.umax"
(\w -> SomeLLVMOverride (LLVM.llvmUmax w))
, polymorphic1_llvm_override "llvm.umin"
(\w -> SomeLLVMOverride (LLVM.llvmUmin w))
, basic_llvm_override LLVM.llvmCopysignOverride_F32
, basic_llvm_override LLVM.llvmCopysignOverride_F64
, basic_llvm_override LLVM.llvmFabsF32
, basic_llvm_override LLVM.llvmFabsF64
, basic_llvm_override LLVM.llvmCeilOverride_F32
, basic_llvm_override LLVM.llvmCeilOverride_F64
, basic_llvm_override LLVM.llvmFloorOverride_F32
, basic_llvm_override LLVM.llvmFloorOverride_F64
, basic_llvm_override LLVM.llvmSqrtOverride_F32
, basic_llvm_override LLVM.llvmSqrtOverride_F64
, basic_llvm_override LLVM.llvmSinOverride_F32
, basic_llvm_override LLVM.llvmSinOverride_F64
, basic_llvm_override LLVM.llvmCosOverride_F32
, basic_llvm_override LLVM.llvmCosOverride_F64
, basic_llvm_override LLVM.llvmPowOverride_F32
, basic_llvm_override LLVM.llvmPowOverride_F64
, basic_llvm_override LLVM.llvmExpOverride_F32
, basic_llvm_override LLVM.llvmExpOverride_F64
, basic_llvm_override LLVM.llvmLogOverride_F32
, basic_llvm_override LLVM.llvmLogOverride_F64
, basic_llvm_override LLVM.llvmExp2Override_F32
, basic_llvm_override LLVM.llvmExp2Override_F64
, basic_llvm_override LLVM.llvmLog2Override_F32
, basic_llvm_override LLVM.llvmLog2Override_F64
, basic_llvm_override LLVM.llvmLog10Override_F32
, basic_llvm_override LLVM.llvmLog10Override_F64
, basic_llvm_override LLVM.llvmFmaOverride_F32
, basic_llvm_override LLVM.llvmFmaOverride_F64
, basic_llvm_override LLVM.llvmFmuladdOverride_F32
, basic_llvm_override LLVM.llvmFmuladdOverride_F64
, basic_llvm_override LLVM.llvmIsFpclassOverride_F32
, basic_llvm_override LLVM.llvmIsFpclassOverride_F64
-- C standard library functions
, basic_llvm_override Libc.llvmAbortOverride
, basic_llvm_override Libc.llvmAssertRtnOverride
, basic_llvm_override Libc.llvmAssertFailOverride
, basic_llvm_override Libc.llvmMemcpyOverride
, basic_llvm_override Libc.llvmMemcpyChkOverride
, basic_llvm_override Libc.llvmMemmoveOverride
, basic_llvm_override Libc.llvmMemsetOverride
, basic_llvm_override Libc.llvmMemsetChkOverride
, basic_llvm_override Libc.llvmMallocOverride
, basic_llvm_override Libc.llvmCallocOverride
, basic_llvm_override Libc.llvmFreeOverride
, basic_llvm_override Libc.llvmReallocOverride
, basic_llvm_override Libc.llvmStrlenOverride
, basic_llvm_override Libc.llvmPrintfOverride
, basic_llvm_override Libc.llvmPrintfChkOverride
, basic_llvm_override Libc.llvmPutsOverride
, basic_llvm_override Libc.llvmPutCharOverride
, basic_llvm_override Libc.llvmExitOverride
, basic_llvm_override Libc.llvmGetenvOverride
, basic_llvm_override Libc.llvmHtonlOverride
, basic_llvm_override Libc.llvmHtonsOverride
, basic_llvm_override Libc.llvmNtohlOverride
, basic_llvm_override Libc.llvmNtohsOverride
, basic_llvm_override Libc.llvmAbsOverride
, basic_llvm_override Libc.llvmLAbsOverride_32
, basic_llvm_override Libc.llvmLAbsOverride_64
, basic_llvm_override Libc.llvmLLAbsOverride
, basic_llvm_override Libc.llvmCeilOverride
, basic_llvm_override Libc.llvmCeilfOverride
, basic_llvm_override Libc.llvmFloorOverride
, basic_llvm_override Libc.llvmFloorfOverride
, basic_llvm_override Libc.llvmFmaOverride
, basic_llvm_override Libc.llvmFmafOverride
, basic_llvm_override Libc.llvmIsinfOverride
, basic_llvm_override Libc.llvm__isinfOverride
, basic_llvm_override Libc.llvm__isinffOverride
, basic_llvm_override Libc.llvmIsnanOverride
, basic_llvm_override Libc.llvm__isnanOverride
, basic_llvm_override Libc.llvm__isnanfOverride
, basic_llvm_override Libc.llvmSqrtOverride
, basic_llvm_override Libc.llvmSqrtfOverride
, basic_llvm_override Libc.llvmSinOverride
, basic_llvm_override Libc.llvmSinfOverride
, basic_llvm_override Libc.llvmCosOverride
, basic_llvm_override Libc.llvmCosfOverride
, basic_llvm_override Libc.llvmTanOverride
, basic_llvm_override Libc.llvmTanfOverride
, basic_llvm_override Libc.llvmAsinOverride
, basic_llvm_override Libc.llvmAsinfOverride
, basic_llvm_override Libc.llvmAcosOverride
, basic_llvm_override Libc.llvmAcosfOverride
, basic_llvm_override Libc.llvmAtanOverride
, basic_llvm_override Libc.llvmAtanfOverride
, basic_llvm_override Libc.llvmSinhOverride
, basic_llvm_override Libc.llvmSinhfOverride
, basic_llvm_override Libc.llvmCoshOverride
, basic_llvm_override Libc.llvmCoshfOverride
, basic_llvm_override Libc.llvmTanhOverride
, basic_llvm_override Libc.llvmTanhfOverride
, basic_llvm_override Libc.llvmAsinhOverride
, basic_llvm_override Libc.llvmAsinhfOverride
, basic_llvm_override Libc.llvmAcoshOverride
, basic_llvm_override Libc.llvmAcoshfOverride
, basic_llvm_override Libc.llvmAtanhOverride
, basic_llvm_override Libc.llvmAtanhfOverride
, basic_llvm_override Libc.llvmHypotOverride
, basic_llvm_override Libc.llvmHypotfOverride
, basic_llvm_override Libc.llvmAtan2Override
, basic_llvm_override Libc.llvmAtan2fOverride
, basic_llvm_override Libc.llvmPowfOverride
, basic_llvm_override Libc.llvmPowOverride
, basic_llvm_override Libc.llvmExpOverride
, basic_llvm_override Libc.llvmExpfOverride
, basic_llvm_override Libc.llvmLogOverride
, basic_llvm_override Libc.llvmLogfOverride
, basic_llvm_override Libc.llvmExpm1Override
, basic_llvm_override Libc.llvmExpm1fOverride
, basic_llvm_override Libc.llvmLog1pOverride
, basic_llvm_override Libc.llvmLog1pfOverride
, basic_llvm_override Libc.llvmExp2Override
, basic_llvm_override Libc.llvmExp2fOverride
, basic_llvm_override Libc.llvmLog2Override
, basic_llvm_override Libc.llvmLog2fOverride
, basic_llvm_override Libc.llvmExp10Override
, basic_llvm_override Libc.llvmExp10fOverride
, basic_llvm_override Libc.llvmLog10Override
, basic_llvm_override Libc.llvmLog10fOverride
, basic_llvm_override Libc.cxa_atexitOverride
, basic_llvm_override Libc.posixMemalignOverride
-- C++ standard library functions
, Libcxx.register_cpp_override Libcxx.endlOverride
-- Some architecture-dependent intrinsics
, basic_llvm_override LLVM.llvmX86_SSE2_storeu_dq
, basic_llvm_override LLVM.llvmX86_pclmulqdq
]
-- | Register those overrides that should apply even when the corresponding
-- function has a definition
define_overrides ::
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch, ?lc :: TypeContext) =>
[OverrideTemplate p sym arch rtp l a]
define_overrides =
[ Libcxx.register_cpp_override Libcxx.putToOverride12
, Libcxx.register_cpp_override Libcxx.putToOverride9
, Libcxx.register_cpp_override Libcxx.endlOverride
, Libcxx.register_cpp_override Libcxx.sentryOverride
, Libcxx.register_cpp_override Libcxx.sentryBoolOverride
]
{-
Note [Overrides involving (unsigned) long]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Registering overrides for functions with `long` argument or result types is
tricky, as the size of a `long` varies wildly between different operating
systems and architectures. On Linux and macOS, `long` is 32 or 64 bits on
32- or 64-bit architectures, respectively. On Windows, however, `long` is
always 32 bits, regardless of architecture. There is a similar story for the
`unsigned long` type as well.
To ensure that overrides for functions involving `long` are (at least to some
degree) portable, we register each override for `long`-using function twice:
once where `long` is assumed to be 32 bits, and once again where `long` is
assumed to be 64 bits. This is a somewhat heavy-handed solution, but it avoids
the need to predict what size `long` will be on a given target ahead of time.
-}