Skip to content

Commit

Permalink
crucible-llvm: Factor out lists of overrides for LLVM intrinsics (#1187)
Browse files Browse the repository at this point in the history 
This makes these `LLVMOverride`s more accessible to downstream
consumers, as they are reified as data (`SomeLLVMOverride`,
`Poly1LLVMOverride`) rather than monadic actions (`OverrideTemplate`).
  • Loading branch information
@langston-barrett
langston-barrett authored Mar 26, 2024
1 parent 1b0bd47 commit e03b20f
Show file tree
Hide file tree
Showing 2 changed files with 189 additions and 145 deletions.
150 changes: 5 additions & 145 deletions crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,6 @@ 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
Expand Down Expand Up @@ -153,151 +151,13 @@ declare_overrides ::
, ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
[OverrideTemplate p sym arch rtp l a]
declare_overrides =
map (\(SomeLLVMOverride ov) -> basic_llvm_override ov) Libc.libc_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
concat
[ map (\(SomeLLVMOverride ov) -> basic_llvm_override ov) Libc.libc_overrides
, map (\(SomeLLVMOverride ov) -> basic_llvm_override ov) LLVM.basic_llvm_overrides
, map (\(pfx, LLVM.Poly1LLVMOverride ov) -> polymorphic1_llvm_override pfx ov) LLVM.poly1_llvm_overrides

-- 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
, [ Libcxx.register_cpp_override Libcxx.endlOverride ]
]


Expand Down
184 changes: 184 additions & 0 deletions crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,7 @@ import Lang.Crucible.LLVM.QQ( llvmOvr )

import Lang.Crucible.LLVM.Intrinsics.Common
import qualified Lang.Crucible.LLVM.Intrinsics.Libc as Libc
import Lang.Crucible.LLVM.TypeContext (TypeContext)

-- | Local helper to make a null pointer in 'OverrideSim'
mkNull
Expand All @@ -67,6 +68,189 @@ mkNull = do
sym <- getSymInterface
liftIO (mkNullPointer sym PtrWidth)

------------------------------------------------------------------------
-- ** Lists

-- | All \"basic\"/\"monomorphic\" LLVM overrides.
--
-- Can be turned into 'Lang.Crucible.LLVM.Intrinsics.Common.OverrideTemplate's
-- via 'Lang.Crucible.LLVM.Intrinsics.Common.basic_llvm_override'.
basic_llvm_overrides ::
( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?memOpts :: MemOptions ) =>
[SomeLLVMOverride p sym ext]
basic_llvm_overrides =
[ SomeLLVMOverride llvmLifetimeStartOverride
, SomeLLVMOverride llvmLifetimeEndOverride
, SomeLLVMOverride (llvmLifetimeOverrideOverload "start" (knownNat @8))
, SomeLLVMOverride (llvmLifetimeOverrideOverload "end" (knownNat @8))
, SomeLLVMOverride (llvmLifetimeOverrideOverload_opaque "start")
, SomeLLVMOverride (llvmLifetimeOverrideOverload_opaque "end")
, SomeLLVMOverride (llvmInvariantStartOverride (knownNat @8))
, SomeLLVMOverride llvmInvariantStartOverride_opaque
, SomeLLVMOverride (llvmInvariantEndOverride (knownNat @8))
, SomeLLVMOverride llvmInvariantEndOverride_opaque

, SomeLLVMOverride llvmAssumeOverride
, SomeLLVMOverride llvmTrapOverride
, SomeLLVMOverride llvmUBSanTrapOverride

, SomeLLVMOverride llvmMemcpyOverride_8_8_32
, SomeLLVMOverride llvmMemcpyOverride_8_8_32_noalign
, SomeLLVMOverride llvmMemcpyOverride_8_8_32_noalign_opaque
, SomeLLVMOverride llvmMemcpyOverride_8_8_64
, SomeLLVMOverride llvmMemcpyOverride_8_8_64_noalign
, SomeLLVMOverride llvmMemcpyOverride_8_8_64_noalign_opaque

, SomeLLVMOverride llvmMemmoveOverride_8_8_32
, SomeLLVMOverride llvmMemmoveOverride_8_8_32_noalign
, SomeLLVMOverride llvmMemmoveOverride_8_8_32_noalign_opaque
, SomeLLVMOverride llvmMemmoveOverride_8_8_64
, SomeLLVMOverride llvmMemmoveOverride_8_8_64_noalign
, SomeLLVMOverride llvmMemmoveOverride_8_8_64_noalign_opaque

, SomeLLVMOverride llvmMemsetOverride_8_32
, SomeLLVMOverride llvmMemsetOverride_8_32_noalign
, SomeLLVMOverride llvmMemsetOverride_8_32_noalign_opaque
, SomeLLVMOverride llvmMemsetOverride_8_64
, SomeLLVMOverride llvmMemsetOverride_8_64_noalign
, SomeLLVMOverride llvmMemsetOverride_8_64_noalign_opaque

, SomeLLVMOverride llvmObjectsizeOverride_32
, SomeLLVMOverride llvmObjectsizeOverride_64

, SomeLLVMOverride llvmObjectsizeOverride_32_null
, SomeLLVMOverride llvmObjectsizeOverride_64_null

, SomeLLVMOverride llvmObjectsizeOverride_32_null_dynamic
, SomeLLVMOverride llvmObjectsizeOverride_64_null_dynamic

, SomeLLVMOverride llvmObjectsizeOverride_32_null_dynamic_opaque
, SomeLLVMOverride llvmObjectsizeOverride_64_null_dynamic_opaque

, SomeLLVMOverride llvmPrefetchOverride
, SomeLLVMOverride llvmPrefetchOverride_opaque
, SomeLLVMOverride llvmPrefetchOverride_preLLVM10

, SomeLLVMOverride llvmStacksave
, SomeLLVMOverride llvmStackrestore

, SomeLLVMOverride (llvmBSwapOverride (knownNat @2)) -- 16 = 2 * 8
, SomeLLVMOverride (llvmBSwapOverride (knownNat @4)) -- 32 = 4 * 8
, SomeLLVMOverride (llvmBSwapOverride (knownNat @6)) -- 48 = 6 * 8
, SomeLLVMOverride (llvmBSwapOverride (knownNat @8)) -- 64 = 8 * 8
, SomeLLVMOverride (llvmBSwapOverride (knownNat @10)) -- 80 = 10 * 8
, SomeLLVMOverride (llvmBSwapOverride (knownNat @12)) -- 96 = 12 * 8
, SomeLLVMOverride (llvmBSwapOverride (knownNat @14)) -- 112 = 14 * 8
, SomeLLVMOverride (llvmBSwapOverride (knownNat @16)) -- 128 = 16 * 8

, SomeLLVMOverride llvmCopysignOverride_F32
, SomeLLVMOverride llvmCopysignOverride_F64
, SomeLLVMOverride llvmFabsF32
, SomeLLVMOverride llvmFabsF64

, SomeLLVMOverride llvmCeilOverride_F32
, SomeLLVMOverride llvmCeilOverride_F64
, SomeLLVMOverride llvmFloorOverride_F32
, SomeLLVMOverride llvmFloorOverride_F64
, SomeLLVMOverride llvmSqrtOverride_F32
, SomeLLVMOverride llvmSqrtOverride_F64
, SomeLLVMOverride llvmSinOverride_F32
, SomeLLVMOverride llvmSinOverride_F64
, SomeLLVMOverride llvmCosOverride_F32
, SomeLLVMOverride llvmCosOverride_F64
, SomeLLVMOverride llvmPowOverride_F32
, SomeLLVMOverride llvmPowOverride_F64
, SomeLLVMOverride llvmExpOverride_F32
, SomeLLVMOverride llvmExpOverride_F64
, SomeLLVMOverride llvmLogOverride_F32
, SomeLLVMOverride llvmLogOverride_F64
, SomeLLVMOverride llvmExp2Override_F32
, SomeLLVMOverride llvmExp2Override_F64
, SomeLLVMOverride llvmLog2Override_F32
, SomeLLVMOverride llvmLog2Override_F64
, SomeLLVMOverride llvmLog10Override_F32
, SomeLLVMOverride llvmLog10Override_F64
, SomeLLVMOverride llvmFmaOverride_F32
, SomeLLVMOverride llvmFmaOverride_F64
, SomeLLVMOverride llvmFmuladdOverride_F32
, SomeLLVMOverride llvmFmuladdOverride_F64
, SomeLLVMOverride llvmIsFpclassOverride_F32
, SomeLLVMOverride llvmIsFpclassOverride_F64

-- Some architecture-dependent intrinsics
, SomeLLVMOverride llvmX86_SSE2_storeu_dq
, SomeLLVMOverride llvmX86_pclmulqdq
]

-- | An LLVM override that is polymorphic in a single argument
newtype Poly1LLVMOverride p sym ext
= Poly1LLVMOverride (forall w. (1 <= w) => NatRepr w -> SomeLLVMOverride p sym ext)

poly1_llvm_overrides ::
( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?memOpts :: MemOptions ) =>
[(String, Poly1LLVMOverride p sym ext)]
poly1_llvm_overrides =
[ ("llvm.ctlz"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmCtlz w)
)
, ("llvm.cttz"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmCttz w)
)
, ("llvm.ctpop"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmCtpop w)
)
, ("llvm.bitreverse"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmBitreverse w)
)
, ("llvm.abs"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmAbsOverride w)
)

, ("llvm.fshl"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmFshl w)
)
, ("llvm.fshr"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmFshr w)
)

, ("llvm.expect"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmExpectOverride w)
)
, ("llvm.sadd.with.overflow"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmSaddWithOverflow w)
)
, ("llvm.uadd.with.overflow"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmUaddWithOverflow w)
)
, ("llvm.ssub.with.overflow"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmSsubWithOverflow w)
)
, ("llvm.usub.with.overflow"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmUsubWithOverflow w)
)
, ("llvm.smul.with.overflow"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmSmulWithOverflow w)
)
, ("llvm.umul.with.overflow"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmUmulWithOverflow w)
)

, ("llvm.smax"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmSmax w)
)
, ("llvm.smin"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmSmin w)
)
, ("llvm.umax"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmUmax w)
)
, ("llvm.umin"
, Poly1LLVMOverride $ \w -> SomeLLVMOverride (llvmUmin w)
)
]

------------------------------------------------------------------------
-- ** Declarations

Expand Down

0 comments on commit e03b20f

Please sign in to comment.