crucible-llvm-0.7: src/Lang/Crucible/LLVM/Intrinsics/Libc.hs
-- |
-- Module : Lang.Crucible.LLVM.Intrinsics.Libc
-- Description : Override definitions for C standard library functions
-- Copyright : (c) Galois, Inc 2015-2019
-- License : BSD3
-- Maintainer : Rob Dockins <rdockins@galois.com>
-- Stability : provisional
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
module Lang.Crucible.LLVM.Intrinsics.Libc where
import Control.Lens ((^.), _1, _2, _3)
import qualified Codec.Binary.UTF8.Generic as UTF8
import Control.Monad (when)
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.State (MonadState(..), StateT(..))
import Control.Monad.Trans.Class (MonadTrans(..))
import qualified Data.ByteString as BS
import qualified Data.Vector as V
import System.IO
import qualified GHC.Stack as GHC
import qualified Data.BitVector.Sized as BV
import Data.Parameterized.Context ( pattern (:>), pattern Empty )
import qualified Data.Parameterized.Context as Ctx
import What4.Interface
import What4.ProgramLoc (plSourceLoc)
import qualified What4.SpecialFunctions as W4
import Lang.Crucible.Backend
import Lang.Crucible.CFG.Common
import Lang.Crucible.Types
import Lang.Crucible.Simulator.ExecutionTree
import Lang.Crucible.Simulator.OverrideSim
import Lang.Crucible.Simulator.RegMap
import Lang.Crucible.Simulator.SimError
import Lang.Crucible.LLVM.Bytes
import Lang.Crucible.LLVM.DataLayout
import qualified Lang.Crucible.LLVM.Errors.Poison as Poison
import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB
import Lang.Crucible.LLVM.MalformedLLVMModule
import Lang.Crucible.LLVM.MemModel
import Lang.Crucible.LLVM.MemModel.CallStack (CallStack)
import qualified Lang.Crucible.LLVM.MemModel.Type as G
import qualified Lang.Crucible.LLVM.MemModel.Generic as G
import Lang.Crucible.LLVM.MemModel.Partial
import qualified Lang.Crucible.LLVM.MemModel.Pointer as Ptr
import Lang.Crucible.LLVM.Printf
import Lang.Crucible.LLVM.QQ( llvmOvr )
import Lang.Crucible.LLVM.TypeContext
import Lang.Crucible.LLVM.Intrinsics.Common
import Lang.Crucible.LLVM.Intrinsics.Options
-- | All libc overrides.
--
-- This list is useful to other Crucible frontends based on the LLVM memory
-- model (e.g., Macaw).
libc_overrides ::
( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
[SomeLLVMOverride p sym ext]
libc_overrides =
[ SomeLLVMOverride llvmAbortOverride
, SomeLLVMOverride llvmAssertRtnOverride
, SomeLLVMOverride llvmAssertFailOverride
, SomeLLVMOverride llvmMemcpyOverride
, SomeLLVMOverride llvmMemcpyChkOverride
, SomeLLVMOverride llvmMemmoveOverride
, SomeLLVMOverride llvmMemsetOverride
, SomeLLVMOverride llvmMemsetChkOverride
, SomeLLVMOverride llvmMallocOverride
, SomeLLVMOverride llvmCallocOverride
, SomeLLVMOverride llvmFreeOverride
, SomeLLVMOverride llvmReallocOverride
, SomeLLVMOverride llvmStrlenOverride
, SomeLLVMOverride llvmPrintfOverride
, SomeLLVMOverride llvmPrintfChkOverride
, SomeLLVMOverride llvmPutsOverride
, SomeLLVMOverride llvmPutCharOverride
, SomeLLVMOverride llvmExitOverride
, SomeLLVMOverride llvmGetenvOverride
, SomeLLVMOverride llvmHtonlOverride
, SomeLLVMOverride llvmHtonsOverride
, SomeLLVMOverride llvmNtohlOverride
, SomeLLVMOverride llvmNtohsOverride
, SomeLLVMOverride llvmAbsOverride
, SomeLLVMOverride llvmLAbsOverride_32
, SomeLLVMOverride llvmLAbsOverride_64
, SomeLLVMOverride llvmLLAbsOverride
, SomeLLVMOverride llvmCeilOverride
, SomeLLVMOverride llvmCeilfOverride
, SomeLLVMOverride llvmFloorOverride
, SomeLLVMOverride llvmFloorfOverride
, SomeLLVMOverride llvmFmaOverride
, SomeLLVMOverride llvmFmafOverride
, SomeLLVMOverride llvmIsinfOverride
, SomeLLVMOverride llvm__isinfOverride
, SomeLLVMOverride llvm__isinffOverride
, SomeLLVMOverride llvmIsnanOverride
, SomeLLVMOverride llvm__isnanOverride
, SomeLLVMOverride llvm__isnanfOverride
, SomeLLVMOverride llvm__isnandOverride
, SomeLLVMOverride llvmSqrtOverride
, SomeLLVMOverride llvmSqrtfOverride
, SomeLLVMOverride llvmSinOverride
, SomeLLVMOverride llvmSinfOverride
, SomeLLVMOverride llvmCosOverride
, SomeLLVMOverride llvmCosfOverride
, SomeLLVMOverride llvmTanOverride
, SomeLLVMOverride llvmTanfOverride
, SomeLLVMOverride llvmAsinOverride
, SomeLLVMOverride llvmAsinfOverride
, SomeLLVMOverride llvmAcosOverride
, SomeLLVMOverride llvmAcosfOverride
, SomeLLVMOverride llvmAtanOverride
, SomeLLVMOverride llvmAtanfOverride
, SomeLLVMOverride llvmSinhOverride
, SomeLLVMOverride llvmSinhfOverride
, SomeLLVMOverride llvmCoshOverride
, SomeLLVMOverride llvmCoshfOverride
, SomeLLVMOverride llvmTanhOverride
, SomeLLVMOverride llvmTanhfOverride
, SomeLLVMOverride llvmAsinhOverride
, SomeLLVMOverride llvmAsinhfOverride
, SomeLLVMOverride llvmAcoshOverride
, SomeLLVMOverride llvmAcoshfOverride
, SomeLLVMOverride llvmAtanhOverride
, SomeLLVMOverride llvmAtanhfOverride
, SomeLLVMOverride llvmHypotOverride
, SomeLLVMOverride llvmHypotfOverride
, SomeLLVMOverride llvmAtan2Override
, SomeLLVMOverride llvmAtan2fOverride
, SomeLLVMOverride llvmPowfOverride
, SomeLLVMOverride llvmPowOverride
, SomeLLVMOverride llvmExpOverride
, SomeLLVMOverride llvmExpfOverride
, SomeLLVMOverride llvmLogOverride
, SomeLLVMOverride llvmLogfOverride
, SomeLLVMOverride llvmExpm1Override
, SomeLLVMOverride llvmExpm1fOverride
, SomeLLVMOverride llvmLog1pOverride
, SomeLLVMOverride llvmLog1pfOverride
, SomeLLVMOverride llvmExp2Override
, SomeLLVMOverride llvmExp2fOverride
, SomeLLVMOverride llvmLog2Override
, SomeLLVMOverride llvmLog2fOverride
, SomeLLVMOverride llvmExp10Override
, SomeLLVMOverride llvmExp10fOverride
, SomeLLVMOverride llvm__exp10Override
, SomeLLVMOverride llvm__exp10fOverride
, SomeLLVMOverride llvmLog10Override
, SomeLLVMOverride llvmLog10fOverride
, SomeLLVMOverride cxa_atexitOverride
, SomeLLVMOverride posixMemalignOverride
]
------------------------------------------------------------------------
-- ** Declarations
llvmMemcpyOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> LLVMOverride p sym ext
(EmptyCtx ::> LLVMPointerType wptr
::> LLVMPointerType wptr
::> BVType wptr)
(LLVMPointerType wptr)
llvmMemcpyOverride =
[llvmOvr| i8* @memcpy( i8*, i8*, size_t ) |]
(\memOps args ->
do sym <- getSymInterface
volatile <- liftIO $ RegEntry knownRepr <$> bvZero sym knownNat
Ctx.uncurryAssignment (callMemcpy memOps)
(args :> volatile)
return $ regValue $ args^._1 -- return first argument
)
llvmMemcpyChkOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> LLVMOverride p sym ext
(EmptyCtx ::> LLVMPointerType wptr
::> LLVMPointerType wptr
::> BVType wptr
::> BVType wptr)
(LLVMPointerType wptr)
llvmMemcpyChkOverride =
[llvmOvr| i8* @__memcpy_chk ( i8*, i8*, size_t, size_t ) |]
(\memOps args ->
do let args' = Empty :> (args^._1) :> (args^._2) :> (args^._3)
sym <- getSymInterface
volatile <- liftIO $ RegEntry knownRepr <$> bvZero sym knownNat
Ctx.uncurryAssignment (callMemcpy memOps)
(args' :> volatile)
return $ regValue $ args^._1 -- return first argument
)
llvmMemmoveOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> LLVMOverride p sym ext
(EmptyCtx ::> (LLVMPointerType wptr)
::> (LLVMPointerType wptr)
::> BVType wptr)
(LLVMPointerType wptr)
llvmMemmoveOverride =
[llvmOvr| i8* @memmove( i8*, i8*, size_t ) |]
(\memOps args ->
do sym <- getSymInterface
volatile <- liftIO (RegEntry knownRepr <$> bvZero sym knownNat)
Ctx.uncurryAssignment (callMemmove memOps)
(args :> volatile)
return $ regValue $ args^._1 -- return first argument
)
llvmMemsetOverride :: forall p sym ext wptr.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
=> LLVMOverride p sym ext
(EmptyCtx ::> LLVMPointerType wptr
::> BVType 32
::> BVType wptr)
(LLVMPointerType wptr)
llvmMemsetOverride =
[llvmOvr| i8* @memset( i8*, i32, size_t ) |]
(\memOps args ->
do sym <- getSymInterface
LeqProof <- return (leqTrans @9 @16 @wptr LeqProof LeqProof)
let dest = args^._1
val <- liftIO (RegEntry knownRepr <$> bvTrunc sym (knownNat @8) (regValue (args^._2)))
let len = args^._3
volatile <- liftIO
(RegEntry knownRepr <$> bvZero sym knownNat)
callMemset memOps dest val len volatile
return (regValue dest)
)
llvmMemsetChkOverride
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
=> LLVMOverride p sym ext
(EmptyCtx ::> LLVMPointerType wptr
::> BVType 32
::> BVType wptr
::> BVType wptr)
(LLVMPointerType wptr)
llvmMemsetChkOverride =
[llvmOvr| i8* @__memset_chk( i8*, i32, size_t, size_t ) |]
(\memOps args ->
do sym <- getSymInterface
let dest = args^._1
val <- liftIO
(RegEntry knownRepr <$> bvTrunc sym knownNat (regValue (args^._2)))
let len = args^._3
volatile <- liftIO
(RegEntry knownRepr <$> bvZero sym knownNat)
callMemset memOps dest val len volatile
return (regValue dest)
)
------------------------------------------------------------------------
-- *** Allocation
llvmCallocOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?memOpts :: MemOptions )
=> LLVMOverride p sym ext
(EmptyCtx ::> BVType wptr ::> BVType wptr)
(LLVMPointerType wptr)
llvmCallocOverride =
let alignment = maxAlignment (llvmDataLayout ?lc) in
[llvmOvr| i8* @calloc( size_t, size_t ) |]
(\memOps args -> Ctx.uncurryAssignment (callCalloc memOps alignment) args)
llvmReallocOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?memOpts :: MemOptions )
=> LLVMOverride p sym ext
(EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr)
(LLVMPointerType wptr)
llvmReallocOverride =
let alignment = maxAlignment (llvmDataLayout ?lc) in
[llvmOvr| i8* @realloc( i8*, size_t ) |]
(\memOps args -> Ctx.uncurryAssignment (callRealloc memOps alignment) args)
llvmMallocOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?memOpts :: MemOptions )
=> LLVMOverride p sym ext
(EmptyCtx ::> BVType wptr)
(LLVMPointerType wptr)
llvmMallocOverride =
let alignment = maxAlignment (llvmDataLayout ?lc) in
[llvmOvr| i8* @malloc( size_t ) |]
(\memOps args -> Ctx.uncurryAssignment (callMalloc memOps alignment) args)
posixMemalignOverride ::
( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?memOpts :: MemOptions ) =>
LLVMOverride p sym ext
(EmptyCtx ::> LLVMPointerType wptr
::> BVType wptr
::> BVType wptr)
(BVType 32)
posixMemalignOverride =
[llvmOvr| i32 @posix_memalign( i8**, size_t, size_t ) |]
(\memOps args -> Ctx.uncurryAssignment (callPosixMemalign memOps) args)
llvmFreeOverride
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
=> LLVMOverride p sym ext
(EmptyCtx ::> LLVMPointerType wptr)
UnitType
llvmFreeOverride =
[llvmOvr| void @free( i8* ) |]
(\memOps args -> Ctx.uncurryAssignment (callFree memOps) args)
------------------------------------------------------------------------
-- *** Strings and I/O
llvmPrintfOverride
:: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
, ?memOpts :: MemOptions )
=> LLVMOverride p sym ext
(EmptyCtx ::> LLVMPointerType wptr
::> VectorType AnyType)
(BVType 32)
llvmPrintfOverride =
[llvmOvr| i32 @printf( i8*, ... ) |]
(\memOps args -> Ctx.uncurryAssignment (callPrintf memOps) args)
llvmPrintfChkOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> LLVMOverride p sym ext
(EmptyCtx ::> BVType 32
::> LLVMPointerType wptr
::> VectorType AnyType)
(BVType 32)
llvmPrintfChkOverride =
[llvmOvr| i32 @__printf_chk( i32, i8*, ... ) |]
(\memOps args -> Ctx.uncurryAssignment (\_flg -> callPrintf memOps) args)
llvmPutCharOverride
:: (IsSymInterface sym, HasPtrWidth wptr)
=> LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
llvmPutCharOverride =
[llvmOvr| i32 @putchar( i32 ) |]
(\memOps args -> Ctx.uncurryAssignment (callPutChar memOps) args)
llvmPutsOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType 32)
llvmPutsOverride =
[llvmOvr| i32 @puts( i8* ) |]
(\memOps args -> Ctx.uncurryAssignment (callPuts memOps) args)
llvmStrlenOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (BVType wptr)
llvmStrlenOverride =
[llvmOvr| size_t @strlen( i8* ) |]
(\memOps args -> Ctx.uncurryAssignment (callStrlen memOps) args)
------------------------------------------------------------------------
-- ** Implementations
------------------------------------------------------------------------
-- *** Allocation
callRealloc
:: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
, ?memOpts :: MemOptions )
=> GlobalVar Mem
-> Alignment
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callRealloc mvar alignment (regValue -> ptr) (regValue -> sz) =
ovrWithBackend $ \bak -> do
let sym = backendGetSym bak
szZero <- liftIO (notPred sym =<< bvIsNonzero sym sz)
ptrNull <- liftIO (ptrIsNull sym PtrWidth ptr)
loc <- liftIO (plSourceLoc <$> getCurrentProgramLoc sym)
let displayString = "<realloc> " ++ show loc
symbolicBranches emptyRegMap
-- If the pointer is null, behave like malloc
[ ( ptrNull
, modifyGlobal mvar $ \mem -> liftIO $ doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment
, Nothing
)
-- If the size is zero, behave like malloc (of zero bytes) then free
, (szZero
, modifyGlobal mvar $ \mem -> liftIO $
do (newp, mem1) <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment
mem2 <- doFree bak mem1 ptr
return (newp, mem2)
, Nothing
)
-- Otherwise, allocate a new region, memcopy `sz` bytes and free the old pointer
, (truePred sym
, modifyGlobal mvar $ \mem -> liftIO $
do (newp, mem1) <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment
mem2 <- uncheckedMemcpy sym mem1 newp ptr sz
mem3 <- doFree bak mem2 ptr
return (newp, mem3)
, Nothing)
]
callPosixMemalign
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?memOpts :: MemOptions )
=> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPosixMemalign mvar (regValue -> outPtr) (regValue -> align) (regValue -> sz) =
ovrWithBackend $ \bak ->
let sym = backendGetSym bak in
case asBV align of
Nothing -> fail $ unwords ["posix_memalign: alignment value must be concrete:", show (printSymExpr align)]
Just concrete_align ->
case toAlignment (toBytes (BV.asUnsigned concrete_align)) of
Nothing -> fail $ unwords ["posix_memalign: invalid alignment value:", show concrete_align]
Just a ->
let dl = llvmDataLayout ?lc in
modifyGlobal mvar $ \mem -> liftIO $
do loc <- plSourceLoc <$> getCurrentProgramLoc sym
let displayString = "<posix_memaign> " ++ show loc
(p, mem') <- doMalloc bak G.HeapAlloc G.Mutable displayString mem sz a
mem'' <- storeRaw bak mem' outPtr (bitvectorType (dl^.ptrSize)) (dl^.ptrAlign) (ptrToPtrVal p)
z <- bvZero sym knownNat
return (z, mem'')
callMalloc
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> GlobalVar Mem
-> Alignment
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callMalloc mvar alignment (regValue -> sz) =
ovrWithBackend $ \bak ->
modifyGlobal mvar $ \mem -> liftIO $
do loc <- plSourceLoc <$> getCurrentProgramLoc (backendGetSym bak)
let displayString = "<malloc> " ++ show loc
doMalloc bak G.HeapAlloc G.Mutable displayString mem sz alignment
callCalloc
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> GlobalVar Mem
-> Alignment
-> RegEntry sym (BVType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callCalloc mvar alignment
(regValue -> sz)
(regValue -> num) =
ovrWithBackend $ \bak ->
modifyGlobal mvar $ \mem -> liftIO $
doCalloc bak mem sz num alignment
callFree
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
=> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret ()
callFree mvar
(regValue -> ptr) =
ovrWithBackend $ \bak ->
modifyGlobal mvar $ \mem -> liftIO $
do mem' <- doFree bak mem ptr
return ((), mem')
------------------------------------------------------------------------
-- *** Memory manipulation
callMemcpy
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType w)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext r args ret ()
callMemcpy mvar
(regValue -> dest)
(regValue -> src)
(RegEntry (BVRepr w) len)
_volatile =
ovrWithBackend $ \bak ->
modifyGlobal mvar $ \mem -> liftIO $
do mem' <- doMemcpy bak w mem True dest src len
return ((), mem')
-- NB the only difference between memcpy and memove
-- is that memmove does not assert that the memory
-- ranges are disjoint. The underlying operation
-- works correctly in both cases.
callMemmove
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType w)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext r args ret ()
callMemmove mvar
(regValue -> dest)
(regValue -> src)
(RegEntry (BVRepr w) len)
_volatile =
-- FIXME? add assertions about alignment
ovrWithBackend $ \bak ->
modifyGlobal mvar $ \mem -> liftIO $
do mem' <- doMemcpy bak w mem False dest src len
return ((), mem')
callMemset
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
=> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType 8)
-> RegEntry sym (BVType w)
-> RegEntry sym (BVType 1)
-> OverrideSim p sym ext r args ret ()
callMemset mvar
(regValue -> dest)
(regValue -> val)
(RegEntry (BVRepr w) len)
_volatile =
ovrWithBackend $ \bak ->
modifyGlobal mvar $ \mem -> liftIO $
do mem' <- doMemset bak w mem dest val len
return ((), mem')
------------------------------------------------------------------------
-- *** Strings and I/O
callPutChar
:: IsSymInterface sym
=> GlobalVar Mem
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPutChar _mvar
(regValue -> ch) = do
h <- printHandle <$> getContext
let chval = maybe '?' (toEnum . fromInteger) (BV.asUnsigned <$> asBV ch)
liftIO $ hPutChar h chval
return ch
callPuts
:: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
, ?memOpts :: MemOptions )
=> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPuts mvar
(regValue -> strPtr) =
ovrWithBackend $ \bak -> do
mem <- readGlobal mvar
str <- liftIO $ loadString bak mem strPtr Nothing
h <- printHandle <$> getContext
liftIO $ hPutStrLn h (UTF8.toString str)
-- return non-negative value on success
liftIO $ bvLit (backendGetSym bak) knownNat (BV.one knownNat)
callStrlen
:: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
, ?memOpts :: MemOptions )
=> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
callStrlen mvar (regValue -> strPtr) =
ovrWithBackend $ \bak -> do
mem <- readGlobal mvar
liftIO $ strLen bak mem strPtr
callAssert
:: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions )
=> GlobalVar Mem
-> Ctx.Assignment (RegEntry sym)
(EmptyCtx ::> LLVMPointerType wptr
::> LLVMPointerType wptr
::> BVType 32
::> LLVMPointerType wptr)
-> forall r args reg.
OverrideSim p sym ext r args reg (RegValue sym UnitType)
callAssert mvar (Empty :> _pfn :> _pfile :> _pline :> ptxt ) =
ovrWithBackend $ \bak -> do
let sym = backendGetSym bak
when failUponExit $
do mem <- readGlobal mvar
txt <- liftIO $ loadString bak mem (regValue ptxt) Nothing
let err = AssertFailureSimError "Call to assert()" (UTF8.toString txt)
liftIO $ addFailedAssertion bak err
liftIO $
do loc <- liftIO $ getCurrentProgramLoc sym
abortExecBecause $ EarlyExit loc
where
failUponExit :: Bool
failUponExit
= abnormalExitBehavior ?intrinsicsOpts `elem` [AlwaysFail, OnlyAssertFail]
callExit :: ( IsSymInterface sym
, ?intrinsicsOpts :: IntrinsicsOptions )
=> RegEntry sym (BVType 32)
-> OverrideSim p sym ext r args ret (RegValue sym UnitType)
callExit ec =
ovrWithBackend $ \bak -> liftIO $ do
let sym = backendGetSym bak
when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $
do cond <- bvEq sym (regValue ec) =<< bvZero sym knownNat
-- If the argument is non-zero, throw an assertion failure. Otherwise,
-- simply stop the current thread of execution.
assert bak cond "Call to exit() with non-zero argument"
loc <- getCurrentProgramLoc sym
abortExecBecause $ EarlyExit loc
callPrintf
:: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
, ?memOpts :: MemOptions )
=> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (VectorType AnyType)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPrintf mvar
(regValue -> strPtr)
(regValue -> valist) =
ovrWithBackend $ \bak -> do
mem <- readGlobal mvar
formatStr <- liftIO $ loadString bak mem strPtr Nothing
case parseDirectives formatStr of
Left err -> overrideError $ AssertFailureSimError "Format string parsing failed" err
Right ds -> do
((str, n), mem') <- liftIO $ runStateT (executeDirectives (printfOps bak valist) ds) mem
writeGlobal mvar mem'
h <- printHandle <$> getContext
liftIO $ BS.hPutStr h str
liftIO $ bvLit (backendGetSym bak) knownNat (BV.mkBV knownNat (toInteger n))
printfOps :: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> bak
-> V.Vector (AnyValue sym)
-> PrintfOperations (StateT (MemImpl sym) IO)
printfOps bak valist =
let sym = backendGetSym bak in
PrintfOperations
{ printfUnsupported = \x -> lift $ addFailedAssertion bak
$ Unsupported GHC.callStack x
, printfGetInteger = \i sgn _len ->
case valist V.!? (i-1) of
Just (AnyValue (LLVMPointerRepr w) p@(LLVMPointer _blk bv)) ->
do isBv <- liftIO (Ptr.ptrIsBv sym p)
liftIO $ assert bak isBv $
AssertFailureSimError
"Passed a pointer to printf where a bitvector was expected"
""
if sgn then
return $ BV.asSigned w <$> asBV bv
else
return $ BV.asUnsigned <$> asBV bv
Just (AnyValue tpr _) ->
lift $ addFailedAssertion bak
$ AssertFailureSimError
"Type mismatch in printf"
(unwords ["Expected integer, but got:", show tpr])
Nothing ->
lift $ addFailedAssertion bak
$ AssertFailureSimError
"Out-of-bounds argument access in printf"
(unwords ["Index:", show i])
, printfGetFloat = \i _len ->
case valist V.!? (i-1) of
Just (AnyValue (FloatRepr (_fi :: FloatInfoRepr fi)) x) ->
do xr <- liftIO (iFloatToReal @_ @fi sym x)
return (asRational xr)
Just (AnyValue tpr _) ->
lift $ addFailedAssertion bak
$ AssertFailureSimError
"Type mismatch in printf."
(unwords ["Expected floating-point, but got:", show tpr])
Nothing ->
lift $ addFailedAssertion bak
$ AssertFailureSimError
"Out-of-bounds argument access in printf:"
(unwords ["Index:", show i])
, printfGetString = \i numchars ->
case valist V.!? (i-1) of
Just (AnyValue PtrRepr ptr) ->
do mem <- get
liftIO $ loadString bak mem ptr numchars
Just (AnyValue tpr _) ->
lift $ addFailedAssertion bak
$ AssertFailureSimError
"Type mismatch in printf."
(unwords ["Expected char*, but got:", show tpr])
Nothing ->
lift $ addFailedAssertion bak
$ AssertFailureSimError
"Out-of-bounds argument access in printf:"
(unwords ["Index:", show i])
, printfGetPointer = \i ->
case valist V.!? (i-1) of
Just (AnyValue PtrRepr ptr) ->
return $ show (G.ppPtr ptr)
Just (AnyValue tpr _) ->
lift $ addFailedAssertion bak
$ AssertFailureSimError
"Type mismatch in printf."
(unwords ["Expected void*, but got:", show tpr])
Nothing ->
lift $ addFailedAssertion bak
$ AssertFailureSimError
"Out-of-bounds argument access in printf:"
(unwords ["Index:", show i])
, printfSetInteger = \i len v ->
case valist V.!? (i-1) of
Just (AnyValue PtrRepr ptr) ->
do mem <- get
case len of
Len_Byte -> do
let w8 = knownNat :: NatRepr 8
let tp = G.bitvectorType 1
x <- liftIO (llvmPointer_bv sym =<< bvLit sym w8 (BV.mkBV w8 (toInteger v)))
mem' <- liftIO $ doStore bak mem ptr (LLVMPointerRepr w8) tp noAlignment x
put mem'
Len_Short -> do
let w16 = knownNat :: NatRepr 16
let tp = G.bitvectorType 2
x <- liftIO (llvmPointer_bv sym =<< bvLit sym w16 (BV.mkBV w16 (toInteger v)))
mem' <- liftIO $ doStore bak mem ptr (LLVMPointerRepr w16) tp noAlignment x
put mem'
Len_NoMod -> do
let w32 = knownNat :: NatRepr 32
let tp = G.bitvectorType 4
x <- liftIO (llvmPointer_bv sym =<< bvLit sym w32 (BV.mkBV w32 (toInteger v)))
mem' <- liftIO $ doStore bak mem ptr (LLVMPointerRepr w32) tp noAlignment x
put mem'
Len_Long -> do
let w64 = knownNat :: NatRepr 64
let tp = G.bitvectorType 8
x <- liftIO (llvmPointer_bv sym =<< bvLit sym w64 (BV.mkBV w64 (toInteger v)))
mem' <- liftIO $ doStore bak mem ptr (LLVMPointerRepr w64) tp noAlignment x
put mem'
_ ->
lift $ addFailedAssertion bak
$ Unsupported GHC.callStack
$ unwords ["Unsupported size modifier in %n conversion:", show len]
Just (AnyValue tpr _) ->
lift $ addFailedAssertion bak
$ AssertFailureSimError
"Type mismatch in printf."
(unwords ["Expected void*, but got:", show tpr])
Nothing ->
lift $ addFailedAssertion bak
$ AssertFailureSimError
"Out-of-bounds argument access in printf:"
(unwords ["Index:", show i])
}
------------------------------------------------------------------------
-- *** Math
llvmCeilOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmCeilOverride =
[llvmOvr| double @ceil( double ) |]
(\_memOps args -> Ctx.uncurryAssignment callCeil args)
llvmCeilfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmCeilfOverride =
[llvmOvr| float @ceilf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment callCeil args)
llvmFloorOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmFloorOverride =
[llvmOvr| double @floor( double ) |]
(\_memOps args -> Ctx.uncurryAssignment callFloor args)
llvmFloorfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmFloorfOverride =
[llvmOvr| float @floorf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment callFloor args)
llvmFmafOverride ::
forall sym p ext
. IsSymInterface sym
=> LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat
::> FloatType SingleFloat
::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmFmafOverride =
[llvmOvr| float @fmaf( float, float, float ) |]
(\_memOps args -> Ctx.uncurryAssignment callFMA args)
llvmFmaOverride ::
forall sym p ext
. IsSymInterface sym
=> LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat
::> FloatType DoubleFloat
::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmFmaOverride =
[llvmOvr| double @fma( double, double, double ) |]
(\_memOps args -> Ctx.uncurryAssignment callFMA args)
-- math.h defines isinf() and isnan() as macros, so you might think it unusual
-- to provide function overrides for them. However, if you write, say,
-- (isnan)(x) instead of isnan(x), Clang will compile the former as a direct
-- function call rather than as a macro application. Some experimentation
-- reveals that the isnan function's argument is always a double, so we give its
-- argument the type double here to match this unstated convention. We follow
-- suit similarly with isinf.
--
-- Clang does not yet provide direct function call versions of isfinite() or
-- isnormal(), so we do not provide overrides for them.
llvmIsinfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(BVType 32)
llvmIsinfOverride =
[llvmOvr| i32 @isinf( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args)
-- __isinf and __isinff are like the isinf macro, except their arguments are
-- known to be double or float, respectively. They are not mentioned in the
-- POSIX source standard, only the binary standard. See
-- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isinf.html and
-- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isinff.html.
llvm__isinfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(BVType 32)
llvm__isinfOverride =
[llvmOvr| i32 @__isinf( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args)
llvm__isinffOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(BVType 32)
llvm__isinffOverride =
[llvmOvr| i32 @__isinff( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callIsinf (knownNat @32)) args)
llvmIsnanOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(BVType 32)
llvmIsnanOverride =
[llvmOvr| i32 @isnan( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args)
-- __isnan and __isnanf are like the isnan macro, except their arguments are
-- known to be double or float, respectively. They are not mentioned in the
-- POSIX source standard, only the binary standard. See
-- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isnan.html and
-- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isnanf.html.
llvm__isnanOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(BVType 32)
llvm__isnanOverride =
[llvmOvr| i32 @__isnan( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args)
llvm__isnanfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(BVType 32)
llvm__isnanfOverride =
[llvmOvr| i32 @__isnanf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args)
-- macOS compiles isnan() to __isnand() when the argument is a double.
llvm__isnandOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(BVType 32)
llvm__isnandOverride =
[llvmOvr| i32 @__isnand( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callIsnan (knownNat @32)) args)
llvmSqrtOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmSqrtOverride =
[llvmOvr| double @sqrt( double ) |]
(\_memOps args -> Ctx.uncurryAssignment callSqrt args)
llvmSqrtfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmSqrtfOverride =
[llvmOvr| float @sqrtf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment callSqrt args)
callSpecialFunction1 ::
forall fi p sym ext r args ret.
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
W4.SpecialFunction (EmptyCtx ::> W4.R) ->
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 fn (regValue -> x) = do
sym <- getSymInterface
liftIO $ iFloatSpecialFunction1 sym (knownRepr :: FloatInfoRepr fi) fn x
callSpecialFunction2 ::
forall fi p sym ext r args ret.
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
W4.SpecialFunction (EmptyCtx ::> W4.R ::> W4.R) ->
RegEntry sym (FloatType fi) ->
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction2 fn (regValue -> x) (regValue -> y) = do
sym <- getSymInterface
liftIO $ iFloatSpecialFunction2 sym (knownRepr :: FloatInfoRepr fi) fn x y
callCeil ::
forall fi p sym ext r args ret.
IsSymInterface sym =>
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callCeil (regValue -> x) = do
sym <- getSymInterface
liftIO $ iFloatRound @_ @fi sym RTP x
callFloor ::
forall fi p sym ext r args ret.
IsSymInterface sym =>
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFloor (regValue -> x) = do
sym <- getSymInterface
liftIO $ iFloatRound @_ @fi sym RTN x
-- | An implementation of @libc@'s @fma@ function.
callFMA ::
forall fi p sym ext r args ret
. IsSymInterface sym
=> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFMA (regValue -> x) (regValue -> y) (regValue -> z) = do
sym <- getSymInterface
liftIO $ iFloatFMA @_ @fi sym defaultRM x y z
-- | An implementation of @libc@'s @isinf@ macro. This returns @1@ when the
-- argument is positive infinity, @-1@ when the argument is negative infinity,
-- and zero otherwise.
callIsinf ::
forall fi w p sym ext r args ret.
(IsSymInterface sym, 1 <= w) =>
NatRepr w ->
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsinf w (regValue -> x) = do
sym <- getSymInterface
liftIO $ do
isInf <- iFloatIsInf @_ @fi sym x
isNeg <- iFloatIsNeg @_ @fi sym x
isPos <- iFloatIsPos @_ @fi sym x
isInfN <- andPred sym isInf isNeg
isInfP <- andPred sym isInf isPos
bv1 <- bvOne sym w
bvNeg1 <- bvNeg sym bv1
bv0 <- bvZero sym w
res0 <- bvIte sym isInfP bv1 bv0
bvIte sym isInfN bvNeg1 res0
callIsnan ::
forall fi w p sym ext r args ret.
(IsSymInterface sym, 1 <= w) =>
NatRepr w ->
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsnan w (regValue -> x) = do
sym <- getSymInterface
liftIO $ do
isnan <- iFloatIsNaN @_ @fi sym x
bv1 <- bvOne sym w
bv0 <- bvZero sym w
-- isnan() is allowed to return any nonzero value if the argument is NaN, and
-- out of all the possible nonzero values, `1` is certainly one of them.
bvIte sym isnan bv1 bv0
callSqrt ::
forall fi p sym ext r args ret.
IsSymInterface sym =>
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSqrt (regValue -> x) = do
sym <- getSymInterface
liftIO $ iFloatSqrt @_ @fi sym defaultRM x
------------------------------------------------------------------------
-- **** Circular trigonometry functions
-- sin(f)
llvmSinOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmSinOverride =
[llvmOvr| double @sin( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sin) args)
llvmSinfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmSinfOverride =
[llvmOvr| float @sinf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sin) args)
-- cos(f)
llvmCosOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmCosOverride =
[llvmOvr| double @cos( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cos) args)
llvmCosfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmCosfOverride =
[llvmOvr| float @cosf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cos) args)
-- tan(f)
llvmTanOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmTanOverride =
[llvmOvr| double @tan( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tan) args)
llvmTanfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmTanfOverride =
[llvmOvr| float @tanf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tan) args)
-- asin(f)
llvmAsinOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAsinOverride =
[llvmOvr| double @asin( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsin) args)
llvmAsinfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAsinfOverride =
[llvmOvr| float @asinf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsin) args)
-- acos(f)
llvmAcosOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAcosOverride =
[llvmOvr| double @acos( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccos) args)
llvmAcosfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAcosfOverride =
[llvmOvr| float @acosf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccos) args)
-- atan(f)
llvmAtanOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAtanOverride =
[llvmOvr| double @atan( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctan) args)
llvmAtanfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAtanfOverride =
[llvmOvr| float @atanf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctan) args)
------------------------------------------------------------------------
-- **** Hyperbolic trigonometry functions
-- sinh(f)
llvmSinhOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmSinhOverride =
[llvmOvr| double @sinh( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sinh) args)
llvmSinhfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmSinhfOverride =
[llvmOvr| float @sinhf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Sinh) args)
-- cosh(f)
llvmCoshOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmCoshOverride =
[llvmOvr| double @cosh( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cosh) args)
llvmCoshfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmCoshfOverride =
[llvmOvr| float @coshf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Cosh) args)
-- tanh(f)
llvmTanhOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmTanhOverride =
[llvmOvr| double @tanh( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tanh) args)
llvmTanhfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmTanhfOverride =
[llvmOvr| float @tanhf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Tanh) args)
-- asinh(f)
llvmAsinhOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAsinhOverride =
[llvmOvr| double @asinh( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsinh) args)
llvmAsinhfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAsinhfOverride =
[llvmOvr| float @asinhf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arcsinh) args)
-- acosh(f)
llvmAcoshOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAcoshOverride =
[llvmOvr| double @acosh( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccosh) args)
llvmAcoshfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAcoshfOverride =
[llvmOvr| float @acoshf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arccosh) args)
-- atanh(f)
llvmAtanhOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAtanhOverride =
[llvmOvr| double @atanh( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctanh) args)
llvmAtanhfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAtanhfOverride =
[llvmOvr| float @atanhf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Arctanh) args)
------------------------------------------------------------------------
-- **** Rectangular to polar coordinate conversion
-- hypot(f)
llvmHypotOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmHypotOverride =
[llvmOvr| double @hypot( double, double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Hypot) args)
llvmHypotfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmHypotfOverride =
[llvmOvr| float @hypotf( float, float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Hypot) args)
-- atan2(f)
llvmAtan2Override ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAtan2Override =
[llvmOvr| double @atan2( double, double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Arctan2) args)
llvmAtan2fOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAtan2fOverride =
[llvmOvr| float @atan2f( float, float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Arctan2) args)
------------------------------------------------------------------------
-- **** Exponential and logarithm functions
-- pow(f)
llvmPowfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmPowfOverride =
[llvmOvr| float @powf( float, float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Pow) args)
llvmPowOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmPowOverride =
[llvmOvr| double @pow( double, double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction2 W4.Pow) args)
-- exp(f)
llvmExpOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmExpOverride =
[llvmOvr| double @exp( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp) args)
llvmExpfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmExpfOverride =
[llvmOvr| float @expf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp) args)
-- log(f)
llvmLogOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmLogOverride =
[llvmOvr| double @log( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log) args)
llvmLogfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmLogfOverride =
[llvmOvr| float @logf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log) args)
-- expm1(f)
llvmExpm1Override ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmExpm1Override =
[llvmOvr| double @expm1( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Expm1) args)
llvmExpm1fOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmExpm1fOverride =
[llvmOvr| float @expm1f( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Expm1) args)
-- log1p(f)
llvmLog1pOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmLog1pOverride =
[llvmOvr| double @log1p( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log1p) args)
llvmLog1pfOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmLog1pfOverride =
[llvmOvr| float @log1pf( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log1p) args)
------------------------------------------------------------------------
-- **** Base 2 exponential and logarithm
-- exp2(f)
llvmExp2Override ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmExp2Override =
[llvmOvr| double @exp2( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp2) args)
llvmExp2fOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmExp2fOverride =
[llvmOvr| float @exp2f( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp2) args)
-- log2(f)
llvmLog2Override ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmLog2Override =
[llvmOvr| double @log2( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log2) args)
llvmLog2fOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmLog2fOverride =
[llvmOvr| float @log2f( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log2) args)
------------------------------------------------------------------------
-- **** Base 10 exponential and logarithm
-- exp10(f)
llvmExp10Override ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmExp10Override =
[llvmOvr| double @exp10( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args)
llvmExp10fOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmExp10fOverride =
[llvmOvr| float @exp10f( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args)
-- macOS uses __exp10(f) instead of exp10(f).
llvm__exp10Override ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvm__exp10Override =
[llvmOvr| double @__exp10( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args)
llvm__exp10fOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvm__exp10fOverride =
[llvmOvr| float @__exp10f( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Exp10) args)
-- log10(f)
llvmLog10Override ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmLog10Override =
[llvmOvr| double @log10( double ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log10) args)
llvmLog10fOverride ::
IsSymInterface sym =>
LLVMOverride p sym ext
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmLog10fOverride =
[llvmOvr| float @log10f( float ) |]
(\_memOps args -> Ctx.uncurryAssignment (callSpecialFunction1 W4.Log10) args)
------------------------------------------------------------------------
-- *** Other
-- from OSX libc
llvmAssertRtnOverride
:: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions )
=> LLVMOverride p sym ext
(EmptyCtx ::> LLVMPointerType wptr
::> LLVMPointerType wptr
::> BVType 32
::> LLVMPointerType wptr)
UnitType
llvmAssertRtnOverride =
[llvmOvr| void @__assert_rtn( i8*, i8*, i32, i8* ) |]
callAssert
-- From glibc
llvmAssertFailOverride
:: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions )
=> LLVMOverride p sym ext
(EmptyCtx ::> LLVMPointerType wptr
::> LLVMPointerType wptr
::> BVType 32
::> LLVMPointerType wptr)
UnitType
llvmAssertFailOverride =
[llvmOvr| void @__assert_fail( i8*, i8*, i32, i8* ) |]
callAssert
llvmAbortOverride
:: ( IsSymInterface sym
, ?intrinsicsOpts :: IntrinsicsOptions )
=> LLVMOverride p sym ext EmptyCtx UnitType
llvmAbortOverride =
[llvmOvr| void @abort() |]
(\_ _args ->
ovrWithBackend $ \bak -> liftIO $ do
let sym = backendGetSym bak
when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $
let err = AssertFailureSimError "Call to abort" "" in
assert bak (falsePred sym) err
loc <- getCurrentProgramLoc sym
abortExecBecause $ EarlyExit loc
)
llvmExitOverride
:: forall sym p ext
. ( IsSymInterface sym
, ?intrinsicsOpts :: IntrinsicsOptions )
=> LLVMOverride p sym ext
(EmptyCtx ::> BVType 32)
UnitType
llvmExitOverride =
[llvmOvr| void @exit( i32 ) |]
(\_ args -> Ctx.uncurryAssignment callExit args)
llvmGetenvOverride
:: (IsSymInterface sym, HasPtrWidth wptr)
=> LLVMOverride p sym ext
(EmptyCtx ::> LLVMPointerType wptr)
(LLVMPointerType wptr)
llvmGetenvOverride =
[llvmOvr| i8* @getenv( i8* ) |]
(\_ _args -> do
sym <- getSymInterface
liftIO $ mkNullPointer sym PtrWidth)
llvmHtonlOverride ::
(IsSymInterface sym, ?lc :: TypeContext) =>
LLVMOverride p sym ext
(EmptyCtx ::> BVType 32)
(BVType 32)
llvmHtonlOverride =
[llvmOvr| i32 @htonl( i32 ) |]
(\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args)
llvmHtonsOverride ::
(IsSymInterface sym, ?lc :: TypeContext) =>
LLVMOverride p sym ext
(EmptyCtx ::> BVType 16)
(BVType 16)
llvmHtonsOverride =
[llvmOvr| i16 @htons( i16 ) |]
(\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args)
llvmNtohlOverride ::
(IsSymInterface sym, ?lc :: TypeContext) =>
LLVMOverride p sym ext
(EmptyCtx ::> BVType 32)
(BVType 32)
llvmNtohlOverride =
[llvmOvr| i32 @ntohl( i32 ) |]
(\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @4)) args)
llvmNtohsOverride ::
(IsSymInterface sym, ?lc :: TypeContext) =>
LLVMOverride p sym ext
(EmptyCtx ::> BVType 16)
(BVType 16)
llvmNtohsOverride =
[llvmOvr| i16 @ntohs( i16 ) |]
(\_memOps args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian (knownNat @2)) args)
llvmAbsOverride ::
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym ext
(EmptyCtx ::> BVType 32)
(BVType 32)
llvmAbsOverride =
[llvmOvr| i32 @abs( i32 ) |]
(\mvar args ->
do callStack <- callStackFromMemVar' mvar
Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @32)) args)
-- @labs@ uses `long` as its argument and result type, so we need two overrides
-- for @labs@. See Note [Overrides involving (unsigned) long] in
-- Lang.Crucible.LLVM.Intrinsics.
llvmLAbsOverride_32 ::
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym ext
(EmptyCtx ::> BVType 32)
(BVType 32)
llvmLAbsOverride_32 =
[llvmOvr| i32 @labs( i32 ) |]
(\mvar args ->
do callStack <- callStackFromMemVar' mvar
Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @32)) args)
llvmLAbsOverride_64 ::
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym ext
(EmptyCtx ::> BVType 64)
(BVType 64)
llvmLAbsOverride_64 =
[llvmOvr| i64 @labs( i64 ) |]
(\mvar args ->
do callStack <- callStackFromMemVar' mvar
Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @64)) args)
llvmLLAbsOverride ::
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym ext
(EmptyCtx ::> BVType 64)
(BVType 64)
llvmLLAbsOverride =
[llvmOvr| i64 @llabs( i64 ) |]
(\mvar args ->
do callStack <- callStackFromMemVar' mvar
Ctx.uncurryAssignment (callLibcAbs callStack (knownNat @64)) args)
callBSwap ::
(1 <= width, IsSymInterface sym) =>
NatRepr width ->
RegEntry sym (BVType (width * 8)) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwap widthRepr (regValue -> vec) = do
sym <- getSymInterface
liftIO $ bvSwap sym widthRepr vec
-- | This determines under what circumstances @callAbs@ should check if its
-- argument is equal to the smallest signed integer of a particular size
-- (e.g., @INT_MIN@), and if it is equal to that value, what kind of error
-- should be reported.
data CheckAbsIntMin
= LibcAbsIntMinUB
-- ^ For the @abs@, @labs@, and @llabs@ functions, always check if the
-- argument is equal to @INT_MIN@. If so, report it as undefined
-- behavior per the C standard.
| LLVMAbsIntMinPoison Bool
-- ^ For the @llvm.abs.*@ family of LLVM intrinsics, check if the argument
-- is equal to @INT_MIN@ only when the 'Bool' argument is 'True'. If it
-- is 'True' and the argument is equal to @INT_MIN@, return poison.
-- | The workhorse for the @abs@, @labs@, and @llabs@ functions, as well as the
-- @llvm.abs.*@ family of overloaded intrinsics.
callAbs ::
forall w p sym ext r args ret.
(1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>
CallStack ->
CheckAbsIntMin ->
NatRepr w ->
RegEntry sym (BVType w) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callAbs callStack checkIntMin widthRepr (regValue -> src) = do
sym <- getSymInterface
ovrWithBackend $ \bak -> liftIO $ do
bvIntMin <- bvLit sym widthRepr (BV.minSigned widthRepr)
isNotIntMin <- notPred sym =<< bvEq sym src bvIntMin
when shouldCheckIntMin $ do
isNotIntMinUB <- annotateUB sym callStack ub isNotIntMin
let err = AssertFailureSimError "Undefined behavior encountered" $
show $ UB.explain ub
assert bak isNotIntMinUB err
isSrcNegative <- bvIsNeg sym src
srcNegated <- bvNeg sym src
bvIte sym isSrcNegative srcNegated src
where
shouldCheckIntMin :: Bool
shouldCheckIntMin =
case checkIntMin of
LibcAbsIntMinUB -> True
LLVMAbsIntMinPoison shouldCheck -> shouldCheck
ub :: UB.UndefinedBehavior (RegValue' sym)
ub = case checkIntMin of
LibcAbsIntMinUB ->
UB.AbsIntMin $ RV src
LLVMAbsIntMinPoison{} ->
UB.PoisonValueCreated $ Poison.LLVMAbsIntMin $ RV src
callLibcAbs ::
(1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>
CallStack ->
NatRepr w ->
RegEntry sym (BVType w) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callLibcAbs callStack = callAbs callStack LibcAbsIntMinUB
callLLVMAbs ::
(1 <= w, IsSymInterface sym, HasLLVMAnn sym) =>
CallStack ->
NatRepr w ->
RegEntry sym (BVType w) ->
RegEntry sym (BVType 1) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callLLVMAbs callStack widthRepr src (regValue -> isIntMinPoison) = do
shouldCheckIntMin <- liftIO $
-- Per https://releases.llvm.org/12.0.0/docs/LangRef.html#id451, the second
-- argument must be a constant.
case asBV isIntMinPoison of
Just bv -> pure (bv /= BV.zero (knownNat @1))
Nothing -> malformedLLVMModule
"Call to llvm.abs.* with non-constant second argument"
[printSymExpr isIntMinPoison]
callAbs callStack (LLVMAbsIntMinPoison shouldCheckIntMin) widthRepr src
-- | If the data layout is little-endian, run 'callBSwap' on the input.
-- Otherwise, return the input unchanged. This is the workhorse for the
-- @hton{s,l}@ and @ntoh{s,l}@ overrides.
callBSwapIfLittleEndian ::
(1 <= width, IsSymInterface sym, ?lc :: TypeContext) =>
NatRepr width ->
RegEntry sym (BVType (width * 8)) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwapIfLittleEndian widthRepr vec =
case (llvmDataLayout ?lc)^.intLayout of
BigEndian -> pure (regValue vec)
LittleEndian -> callBSwap widthRepr vec
----------------------------------------------------------------------------
-- atexit stuff
cxa_atexitOverride
:: (IsSymInterface sym, HasPtrWidth wptr)
=> LLVMOverride p sym ext
(EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr ::> LLVMPointerType wptr)
(BVType 32)
cxa_atexitOverride =
[llvmOvr| i32 @__cxa_atexit( void (i8*)*, i8*, i8* ) |]
(\_ _args -> do
sym <- getSymInterface
liftIO $ bvZero sym knownNat)
----------------------------------------------------------------------------
-- | IEEE 754 declares 'RNE' to be the default rounding mode, and most @libc@
-- implementations agree with this in practice. The only places where we do not
-- use this as the default are operations that specifically require the behavior
-- of a particular rounding mode, such as @ceil@ or @floor@.
defaultRM :: RoundingMode
defaultRM = RNE