crucible-llvm-0.6: 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.InterpretedFloatingPoint (IsInterpretedFloatExprBuilder(..))
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 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
------------------------------------------------------------------------
-- ** Declarations
llvmMemcpyOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> LLVMOverride p sym
(EmptyCtx ::> LLVMPointerType wptr
::> LLVMPointerType wptr
::> BVType wptr)
(LLVMPointerType wptr)
llvmMemcpyOverride =
[llvmOvr| i8* @memcpy( i8*, i8*, size_t ) |]
(\memOps bak args ->
do volatile <- liftIO $ RegEntry knownRepr <$> bvLit (backendGetSym bak) knownNat (BV.zero knownNat)
Ctx.uncurryAssignment (callMemcpy bak memOps)
(args :> volatile)
return $ regValue $ args^._1 -- return first argument
)
llvmMemcpyChkOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> LLVMOverride p sym
(EmptyCtx ::> LLVMPointerType wptr
::> LLVMPointerType wptr
::> BVType wptr
::> BVType wptr)
(LLVMPointerType wptr)
llvmMemcpyChkOverride =
[llvmOvr| i8* @__memcpy_chk ( i8*, i8*, size_t, size_t ) |]
(\memOps bak args ->
do let args' = Empty :> (args^._1) :> (args^._2) :> (args^._3)
volatile <- liftIO $ RegEntry knownRepr <$> bvLit (backendGetSym bak) knownNat (BV.zero knownNat)
Ctx.uncurryAssignment (callMemcpy bak memOps)
(args' :> volatile)
return $ regValue $ args^._1 -- return first argument
)
llvmMemmoveOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> LLVMOverride p sym
(EmptyCtx ::> (LLVMPointerType wptr)
::> (LLVMPointerType wptr)
::> BVType wptr)
(LLVMPointerType wptr)
llvmMemmoveOverride =
[llvmOvr| i8* @memmove( i8*, i8*, size_t ) |]
(\memOps bak args ->
do volatile <- liftIO (RegEntry knownRepr <$> bvLit (backendGetSym bak) knownNat (BV.zero knownNat))
Ctx.uncurryAssignment (callMemmove bak memOps)
(args :> volatile)
return $ regValue $ args^._1 -- return first argument
)
llvmMemsetOverride :: forall p sym wptr.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
=> LLVMOverride p sym
(EmptyCtx ::> LLVMPointerType wptr
::> BVType 32
::> BVType wptr)
(LLVMPointerType wptr)
llvmMemsetOverride =
[llvmOvr| i8* @memset( i8*, i32, size_t ) |]
(\memOps bak args ->
do let sym = backendGetSym bak
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 <$> bvLit sym knownNat (BV.zero knownNat))
callMemset bak memOps dest val len volatile
return (regValue dest)
)
llvmMemsetChkOverride
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
=> LLVMOverride p sym
(EmptyCtx ::> LLVMPointerType wptr
::> BVType 32
::> BVType wptr
::> BVType wptr)
(LLVMPointerType wptr)
llvmMemsetChkOverride =
[llvmOvr| i8* @__memset_chk( i8*, i32, size_t, size_t ) |]
(\memOps bak args ->
do let sym = backendGetSym bak
let dest = args^._1
val <- liftIO
(RegEntry knownRepr <$> bvTrunc sym knownNat (regValue (args^._2)))
let len = args^._3
volatile <- liftIO
(RegEntry knownRepr <$> bvLit sym knownNat (BV.zero knownNat))
callMemset bak memOps dest val len volatile
return (regValue dest)
)
------------------------------------------------------------------------
-- *** Allocation
llvmCallocOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?memOpts :: MemOptions )
=> LLVMOverride p sym
(EmptyCtx ::> BVType wptr ::> BVType wptr)
(LLVMPointerType wptr)
llvmCallocOverride =
let alignment = maxAlignment (llvmDataLayout ?lc) in
[llvmOvr| i8* @calloc( size_t, size_t ) |]
(\memOps bak args -> Ctx.uncurryAssignment (callCalloc bak memOps alignment) args)
llvmReallocOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?memOpts :: MemOptions )
=> LLVMOverride p sym
(EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr)
(LLVMPointerType wptr)
llvmReallocOverride =
let alignment = maxAlignment (llvmDataLayout ?lc) in
[llvmOvr| i8* @realloc( i8*, size_t ) |]
(\memOps bak args -> Ctx.uncurryAssignment (callRealloc bak memOps alignment) args)
llvmMallocOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?memOpts :: MemOptions )
=> LLVMOverride p sym
(EmptyCtx ::> BVType wptr)
(LLVMPointerType wptr)
llvmMallocOverride =
let alignment = maxAlignment (llvmDataLayout ?lc) in
[llvmOvr| i8* @malloc( size_t ) |]
(\memOps bak args -> Ctx.uncurryAssignment (callMalloc bak memOps alignment) args)
posixMemalignOverride ::
( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?memOpts :: MemOptions ) =>
LLVMOverride p sym
(EmptyCtx ::> LLVMPointerType wptr
::> BVType wptr
::> BVType wptr)
(BVType 32)
posixMemalignOverride =
[llvmOvr| i32 @posix_memalign( i8**, size_t, size_t ) |]
(\memOps bak args -> Ctx.uncurryAssignment (callPosixMemalign bak memOps) args)
llvmFreeOverride
:: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
=> LLVMOverride p sym
(EmptyCtx ::> LLVMPointerType wptr)
UnitType
llvmFreeOverride =
[llvmOvr| void @free( i8* ) |]
(\memOps bak args -> Ctx.uncurryAssignment (callFree bak memOps) args)
------------------------------------------------------------------------
-- *** Strings and I/O
llvmPrintfOverride
:: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
, ?memOpts :: MemOptions )
=> LLVMOverride p sym
(EmptyCtx ::> LLVMPointerType wptr
::> VectorType AnyType)
(BVType 32)
llvmPrintfOverride =
[llvmOvr| i32 @printf( i8*, ... ) |]
(\memOps bak args -> Ctx.uncurryAssignment (callPrintf bak memOps) args)
llvmPrintfChkOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> LLVMOverride p sym
(EmptyCtx ::> BVType 32
::> LLVMPointerType wptr
::> VectorType AnyType)
(BVType 32)
llvmPrintfChkOverride =
[llvmOvr| i32 @__printf_chk( i32, i8*, ... ) |]
(\memOps bak args -> Ctx.uncurryAssignment (\_flg -> callPrintf bak memOps) args)
llvmPutCharOverride
:: (IsSymInterface sym, HasPtrWidth wptr)
=> LLVMOverride p sym (EmptyCtx ::> BVType 32) (BVType 32)
llvmPutCharOverride =
[llvmOvr| i32 @putchar( i32 ) |]
(\memOps bak args -> Ctx.uncurryAssignment (callPutChar bak memOps) args)
llvmPutsOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> LLVMOverride p sym (EmptyCtx ::> LLVMPointerType wptr) (BVType 32)
llvmPutsOverride =
[llvmOvr| i32 @puts( i8* ) |]
(\memOps bak args -> Ctx.uncurryAssignment (callPuts bak memOps) args)
llvmStrlenOverride
:: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> LLVMOverride p sym (EmptyCtx ::> LLVMPointerType wptr) (BVType wptr)
llvmStrlenOverride =
[llvmOvr| size_t @strlen( i8* ) |]
(\memOps bak args -> Ctx.uncurryAssignment (callStrlen bak memOps) args)
------------------------------------------------------------------------
-- ** Implementations
------------------------------------------------------------------------
-- *** Allocation
callRealloc
:: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
, ?memOpts :: MemOptions )
=> bak
-> GlobalVar Mem
-> Alignment
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callRealloc bak mvar alignment (regValue -> ptr) (regValue -> sz) =
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
:: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr
, ?lc :: TypeContext, ?memOpts :: MemOptions )
=> bak
-> 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 bak mvar (regValue -> outPtr) (regValue -> align) (regValue -> sz) =
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 <- bvLit sym knownNat (BV.zero knownNat)
return (z, mem'')
callMalloc
:: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> bak
-> GlobalVar Mem
-> Alignment
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callMalloc bak mvar alignment (regValue -> sz) =
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
:: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> bak
-> GlobalVar Mem
-> Alignment
-> RegEntry sym (BVType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
callCalloc bak mvar alignment
(regValue -> sz)
(regValue -> num) =
modifyGlobal mvar $ \mem -> liftIO $
doCalloc bak mem sz num alignment
callFree
:: (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr)
=> bak
-> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret ()
callFree bak mvar
(regValue -> ptr) =
modifyGlobal mvar $ \mem -> liftIO $
do mem' <- doFree bak mem ptr
return ((), mem')
------------------------------------------------------------------------
-- *** Memory manipulation
callMemcpy
:: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> bak
-> 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 bak mvar
(regValue -> dest)
(regValue -> src)
(RegEntry (BVRepr w) len)
_volatile =
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
:: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr
, ?memOpts :: MemOptions )
=> bak
-> 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 bak mvar
(regValue -> dest)
(regValue -> src)
(RegEntry (BVRepr w) len)
_volatile =
-- FIXME? add assertions about alignment
modifyGlobal mvar $ \mem -> liftIO $
do mem' <- doMemcpy bak w mem False dest src len
return ((), mem')
callMemset
:: (IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr)
=> bak
-> 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 bak mvar
(regValue -> dest)
(regValue -> val)
(RegEntry (BVRepr w) len)
_volatile =
modifyGlobal mvar $ \mem -> liftIO $
do mem' <- doMemset bak w mem dest val len
return ((), mem')
------------------------------------------------------------------------
-- *** Strings and I/O
callPutChar
:: (IsSymBackend sym bak)
=> bak
-> GlobalVar Mem
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPutChar _bak _mvar
(regValue -> ch) = do
h <- printHandle <$> getContext
let chval = maybe '?' (toEnum . fromInteger) (BV.asUnsigned <$> asBV ch)
liftIO $ hPutChar h chval
return ch
callPuts
:: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
, ?memOpts :: MemOptions )
=> bak
-> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPuts bak mvar
(regValue -> strPtr) = 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
:: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
, ?memOpts :: MemOptions )
=> bak
-> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
callStrlen bak mvar (regValue -> strPtr) = do
mem <- readGlobal mvar
liftIO $ strLen bak mem strPtr
callAssert
:: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions )
=> Bool -- ^ 'True' if this is @__assert_fail()@, 'False' otherwise.
-> GlobalVar Mem
-> bak
-> 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 assert_fail mvar bak (Empty :> _pfn :> _pfile :> _pline :> ptxt ) =
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
| assert_fail
= abnormalExitBehavior ?intrinsicsOpts `elem` [AlwaysFail, OnlyAssertFail]
| otherwise
= abnormalExitBehavior ?intrinsicsOpts == AlwaysFail
callExit :: ( IsSymBackend sym bak
, ?intrinsicsOpts :: IntrinsicsOptions )
=> bak
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext r args ret (RegValue sym UnitType)
callExit bak ec = liftIO $
do let sym = backendGetSym bak
when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $
do cond <- bvEq sym (regValue ec) =<< bvLit sym knownNat (BV.zero 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
:: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym
, ?memOpts :: MemOptions )
=> bak
-> GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (VectorType AnyType)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
callPrintf bak mvar
(regValue -> strPtr)
(regValue -> valist) = 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) x) ->
do bv <- liftIO (projectLLVM_bv bak x)
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
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmCeilOverride =
[llvmOvr| double @ceil( double ) |]
(\_memOps sym args -> Ctx.uncurryAssignment (callCeil sym) args)
llvmCeilfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmCeilfOverride =
[llvmOvr| float @ceilf( float ) |]
(\_memOps sym args -> Ctx.uncurryAssignment (callCeil sym) args)
llvmFloorOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmFloorOverride =
[llvmOvr| double @floor( double ) |]
(\_memOps sym args -> Ctx.uncurryAssignment (callFloor sym) args)
llvmFloorfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmFloorfOverride =
[llvmOvr| float @floorf( float ) |]
(\_memOps sym args -> Ctx.uncurryAssignment (callFloor sym) args)
llvmFmafOverride ::
forall sym p
. IsSymInterface sym
=> LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat
::> FloatType SingleFloat
::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmFmafOverride =
[llvmOvr| float @fmaf( float, float, float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callFMA bak) args)
llvmFmaOverride ::
forall sym p
. IsSymInterface sym
=> LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat
::> FloatType DoubleFloat
::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmFmaOverride =
[llvmOvr| double @fma( double, double, double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callFMA bak) 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
(EmptyCtx ::> FloatType DoubleFloat)
(BVType 32)
llvmIsinfOverride =
[llvmOvr| i32 @isinf( double ) |]
(\_memOps sym args -> Ctx.uncurryAssignment (callIsinf sym (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
(EmptyCtx ::> FloatType DoubleFloat)
(BVType 32)
llvm__isinfOverride =
[llvmOvr| i32 @__isinf( double ) |]
(\_memOps sym args -> Ctx.uncurryAssignment (callIsinf sym (knownNat @32)) args)
llvm__isinffOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(BVType 32)
llvm__isinffOverride =
[llvmOvr| i32 @__isinff( float ) |]
(\_memOps sym args -> Ctx.uncurryAssignment (callIsinf sym (knownNat @32)) args)
llvmIsnanOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(BVType 32)
llvmIsnanOverride =
[llvmOvr| i32 @isnan( double ) |]
(\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym (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
(EmptyCtx ::> FloatType DoubleFloat)
(BVType 32)
llvm__isnanOverride =
[llvmOvr| i32 @__isnan( double ) |]
(\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym (knownNat @32)) args)
llvm__isnanfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(BVType 32)
llvm__isnanfOverride =
[llvmOvr| i32 @__isnanf( float ) |]
(\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym (knownNat @32)) args)
llvmSqrtOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmSqrtOverride =
[llvmOvr| double @sqrt( double ) |]
(\_memOps sym args -> Ctx.uncurryAssignment (callSqrt sym) args)
llvmSqrtfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmSqrtfOverride =
[llvmOvr| float @sqrtf( float ) |]
(\_memOps sym args -> Ctx.uncurryAssignment (callSqrt sym) args)
callSpecialFunction1 ::
forall fi p sym bak ext r args ret.
(IsSymBackend sym bak, KnownRepr FloatInfoRepr fi) =>
bak ->
W4.SpecialFunction (EmptyCtx ::> W4.R) ->
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 bak fn (regValue -> x) = liftIO $
iFloatSpecialFunction1 (backendGetSym bak) (knownRepr :: FloatInfoRepr fi) fn x
callSpecialFunction2 ::
forall fi p sym bak ext r args ret.
(IsSymBackend sym bak, KnownRepr FloatInfoRepr fi) =>
bak ->
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 bak fn (regValue -> x) (regValue -> y) = liftIO $
iFloatSpecialFunction2 (backendGetSym bak) (knownRepr :: FloatInfoRepr fi) fn x y
callCeil ::
forall fi p sym bak ext r args ret.
(IsSymBackend sym bak) =>
bak ->
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callCeil bak (regValue -> x) = liftIO $ iFloatRound @_ @fi (backendGetSym bak) RTP x
callFloor ::
forall fi p sym bak ext r args ret.
(IsSymBackend sym bak) =>
bak ->
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFloor bak (regValue -> x) = liftIO $ iFloatRound @_ @fi (backendGetSym bak) RTN x
-- | An implementation of @libc@'s @fma@ function.
callFMA ::
forall fi p sym bak ext r args ret
. IsSymBackend sym bak
=> bak
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFMA bak (regValue -> x) (regValue -> y) (regValue -> z) = liftIO $
iFloatFMA @_ @fi (backendGetSym bak) 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 bak ext r args ret.
(IsSymBackend sym bak, 1 <= w) =>
bak ->
NatRepr w ->
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsinf bak w (regValue -> x) = liftIO $ do
let sym = backendGetSym bak
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
bvOne <- bvLit sym w (BV.one w)
bvNegOne <- bvNeg sym bvOne
bvZero <- bvLit sym w (BV.zero w)
res0 <- bvIte sym isInfP bvOne bvZero
bvIte sym isInfN bvNegOne res0
callIsnan ::
forall fi w p sym bak ext r args ret.
(IsSymBackend sym bak, 1 <= w) =>
bak ->
NatRepr w ->
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsnan bak w (regValue -> x) = liftIO $ do
let sym = backendGetSym bak
isnan <- iFloatIsNaN @_ @fi sym x
bvOne <- bvLit sym w (BV.one w)
bvZero <- bvLit sym w (BV.zero 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 bvOne bvZero
callSqrt ::
forall fi p sym bak ext r args ret.
(IsSymBackend sym bak) =>
bak ->
RegEntry sym (FloatType fi) ->
OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSqrt bak (regValue -> x) = liftIO $ iFloatSqrt @_ @fi (backendGetSym bak) defaultRM x
------------------------------------------------------------------------
-- **** Circular trigonometry functions
-- sin(f)
llvmSinOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmSinOverride =
[llvmOvr| double @sin( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Sin) args)
llvmSinfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmSinfOverride =
[llvmOvr| float @sinf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Sin) args)
-- cos(f)
llvmCosOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmCosOverride =
[llvmOvr| double @cos( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Cos) args)
llvmCosfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmCosfOverride =
[llvmOvr| float @cosf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Cos) args)
-- tan(f)
llvmTanOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmTanOverride =
[llvmOvr| double @tan( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Tan) args)
llvmTanfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmTanfOverride =
[llvmOvr| float @tanf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Tan) args)
-- asin(f)
llvmAsinOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAsinOverride =
[llvmOvr| double @asin( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arcsin) args)
llvmAsinfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAsinfOverride =
[llvmOvr| float @asinf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arcsin) args)
-- acos(f)
llvmAcosOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAcosOverride =
[llvmOvr| double @acos( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arccos) args)
llvmAcosfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAcosfOverride =
[llvmOvr| float @acosf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arccos) args)
-- atan(f)
llvmAtanOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAtanOverride =
[llvmOvr| double @atan( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arctan) args)
llvmAtanfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAtanfOverride =
[llvmOvr| float @atanf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arctan) args)
------------------------------------------------------------------------
-- **** Hyperbolic trigonometry functions
-- sinh(f)
llvmSinhOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmSinhOverride =
[llvmOvr| double @sinh( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Sinh) args)
llvmSinhfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmSinhfOverride =
[llvmOvr| float @sinhf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Sinh) args)
-- cosh(f)
llvmCoshOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmCoshOverride =
[llvmOvr| double @cosh( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Cosh) args)
llvmCoshfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmCoshfOverride =
[llvmOvr| float @coshf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Cosh) args)
-- tanh(f)
llvmTanhOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmTanhOverride =
[llvmOvr| double @tanh( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Tanh) args)
llvmTanhfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmTanhfOverride =
[llvmOvr| float @tanhf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Tanh) args)
-- asinh(f)
llvmAsinhOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAsinhOverride =
[llvmOvr| double @asinh( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arcsinh) args)
llvmAsinhfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAsinhfOverride =
[llvmOvr| float @asinhf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arcsinh) args)
-- acosh(f)
llvmAcoshOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAcoshOverride =
[llvmOvr| double @acosh( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arccosh) args)
llvmAcoshfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAcoshfOverride =
[llvmOvr| float @acoshf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arccosh) args)
-- atanh(f)
llvmAtanhOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAtanhOverride =
[llvmOvr| double @atanh( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arctanh) args)
llvmAtanhfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAtanhfOverride =
[llvmOvr| float @atanhf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Arctanh) args)
------------------------------------------------------------------------
-- **** Rectangular to polar coordinate conversion
-- hypot(f)
llvmHypotOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmHypotOverride =
[llvmOvr| double @hypot( double, double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction2 bak W4.Hypot) args)
llvmHypotfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmHypotfOverride =
[llvmOvr| float @hypotf( float, float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction2 bak W4.Hypot) args)
-- atan2(f)
llvmAtan2Override ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmAtan2Override =
[llvmOvr| double @atan2( double, double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction2 bak W4.Arctan2) args)
llvmAtan2fOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmAtan2fOverride =
[llvmOvr| float @atan2f( float, float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction2 bak W4.Arctan2) args)
------------------------------------------------------------------------
-- **** Exponential and logarithm functions
-- pow(f)
llvmPowfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmPowfOverride =
[llvmOvr| float @powf( float, float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction2 bak W4.Pow) args)
llvmPowOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmPowOverride =
[llvmOvr| double @pow( double, double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction2 bak W4.Pow) args)
-- exp(f)
llvmExpOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmExpOverride =
[llvmOvr| double @exp( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp) args)
llvmExpfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmExpfOverride =
[llvmOvr| float @expf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp) args)
-- log(f)
llvmLogOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmLogOverride =
[llvmOvr| double @log( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log) args)
llvmLogfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmLogfOverride =
[llvmOvr| float @logf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log) args)
-- expm1(f)
llvmExpm1Override ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmExpm1Override =
[llvmOvr| double @expm1( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Expm1) args)
llvmExpm1fOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmExpm1fOverride =
[llvmOvr| float @expm1f( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Expm1) args)
-- log1p(f)
llvmLog1pOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmLog1pOverride =
[llvmOvr| double @log1p( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log1p) args)
llvmLog1pfOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmLog1pfOverride =
[llvmOvr| float @log1pf( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log1p) args)
------------------------------------------------------------------------
-- **** Base 2 exponential and logarithm
-- exp2(f)
llvmExp2Override ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmExp2Override =
[llvmOvr| double @exp2( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp2) args)
llvmExp2fOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmExp2fOverride =
[llvmOvr| float @exp2f( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp2) args)
-- log2(f)
llvmLog2Override ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmLog2Override =
[llvmOvr| double @log2( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log2) args)
llvmLog2fOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmLog2fOverride =
[llvmOvr| float @log2f( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log2) args)
------------------------------------------------------------------------
-- **** Base 10 exponential and logarithm
-- exp10(f)
llvmExp10Override ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmExp10Override =
[llvmOvr| double @exp10( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp10) args)
llvmExp10fOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmExp10fOverride =
[llvmOvr| float @exp10f( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Exp10) args)
-- log10(f)
llvmLog10Override ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType DoubleFloat)
(FloatType DoubleFloat)
llvmLog10Override =
[llvmOvr| double @log10( double ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log10) args)
llvmLog10fOverride ::
IsSymInterface sym =>
LLVMOverride p sym
(EmptyCtx ::> FloatType SingleFloat)
(FloatType SingleFloat)
llvmLog10fOverride =
[llvmOvr| float @log10f( float ) |]
(\_memOps bak args -> Ctx.uncurryAssignment (callSpecialFunction1 bak W4.Log10) args)
------------------------------------------------------------------------
-- *** Other
-- from OSX libc
llvmAssertRtnOverride
:: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions )
=> LLVMOverride p sym
(EmptyCtx ::> LLVMPointerType wptr
::> LLVMPointerType wptr
::> BVType 32
::> LLVMPointerType wptr)
UnitType
llvmAssertRtnOverride =
[llvmOvr| void @__assert_rtn( i8*, i8*, i32, i8* ) |]
(callAssert False)
-- From glibc
llvmAssertFailOverride
:: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions )
=> LLVMOverride p sym
(EmptyCtx ::> LLVMPointerType wptr
::> LLVMPointerType wptr
::> BVType 32
::> LLVMPointerType wptr)
UnitType
llvmAssertFailOverride =
[llvmOvr| void @__assert_fail( i8*, i8*, i32, i8* ) |]
(callAssert True)
llvmAbortOverride
:: ( IsSymInterface sym
, ?intrinsicsOpts :: IntrinsicsOptions )
=> LLVMOverride p sym EmptyCtx UnitType
llvmAbortOverride =
[llvmOvr| void @abort() |]
(\_ bak _args -> 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
. ( IsSymInterface sym
, ?intrinsicsOpts :: IntrinsicsOptions )
=> LLVMOverride p sym
(EmptyCtx ::> BVType 32)
UnitType
llvmExitOverride =
[llvmOvr| void @exit( i32 ) |]
(\_ bak args -> Ctx.uncurryAssignment (callExit bak) args)
llvmGetenvOverride
:: (IsSymInterface sym, HasPtrWidth wptr)
=> LLVMOverride p sym
(EmptyCtx ::> LLVMPointerType wptr)
(LLVMPointerType wptr)
llvmGetenvOverride =
[llvmOvr| i8* @getenv( i8* ) |]
(\_ bak _args -> liftIO $ mkNullPointer (backendGetSym bak) PtrWidth)
llvmHtonlOverride ::
(IsSymInterface sym, ?lc :: TypeContext) =>
LLVMOverride p sym
(EmptyCtx ::> BVType 32)
(BVType 32)
llvmHtonlOverride =
[llvmOvr| i32 @htonl( i32 ) |]
(\_ bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian bak (knownNat @4)) args)
llvmHtonsOverride ::
(IsSymInterface sym, ?lc :: TypeContext) =>
LLVMOverride p sym
(EmptyCtx ::> BVType 16)
(BVType 16)
llvmHtonsOverride =
[llvmOvr| i16 @htons( i16 ) |]
(\_ bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian bak (knownNat @2)) args)
llvmNtohlOverride ::
(IsSymInterface sym, ?lc :: TypeContext) =>
LLVMOverride p sym
(EmptyCtx ::> BVType 32)
(BVType 32)
llvmNtohlOverride =
[llvmOvr| i32 @ntohl( i32 ) |]
(\_ bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian bak (knownNat @4)) args)
llvmNtohsOverride ::
(IsSymInterface sym, ?lc :: TypeContext) =>
LLVMOverride p sym
(EmptyCtx ::> BVType 16)
(BVType 16)
llvmNtohsOverride =
[llvmOvr| i16 @ntohs( i16 ) |]
(\_ bak args -> Ctx.uncurryAssignment (callBSwapIfLittleEndian bak (knownNat @2)) args)
llvmAbsOverride ::
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym
(EmptyCtx ::> BVType 32)
(BVType 32)
llvmAbsOverride =
[llvmOvr| i32 @abs( i32 ) |]
(\mvar bak args ->
do callStack <- callStackFromMemVar' mvar
Ctx.uncurryAssignment (callLibcAbs bak 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
(EmptyCtx ::> BVType 32)
(BVType 32)
llvmLAbsOverride_32 =
[llvmOvr| i32 @labs( i32 ) |]
(\mvar bak args ->
do callStack <- callStackFromMemVar' mvar
Ctx.uncurryAssignment (callLibcAbs bak callStack (knownNat @32)) args)
llvmLAbsOverride_64 ::
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym
(EmptyCtx ::> BVType 64)
(BVType 64)
llvmLAbsOverride_64 =
[llvmOvr| i64 @labs( i64 ) |]
(\mvar bak args ->
do callStack <- callStackFromMemVar' mvar
Ctx.uncurryAssignment (callLibcAbs bak callStack (knownNat @64)) args)
llvmLLAbsOverride ::
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym
(EmptyCtx ::> BVType 64)
(BVType 64)
llvmLLAbsOverride =
[llvmOvr| i64 @llabs( i64 ) |]
(\mvar bak args ->
do callStack <- callStackFromMemVar' mvar
Ctx.uncurryAssignment (callLibcAbs bak callStack (knownNat @64)) args)
callBSwap ::
(1 <= width, IsSymBackend sym bak) =>
bak ->
NatRepr width ->
RegEntry sym (BVType (width * 8)) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwap bak widthRepr (regValue -> vec) =
liftIO $ bvSwap (backendGetSym bak) 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 bak ext r args ret.
(1 <= w, IsSymBackend sym bak, HasLLVMAnn sym) =>
bak ->
CallStack ->
CheckAbsIntMin ->
NatRepr w ->
RegEntry sym (BVType w) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callAbs bak callStack checkIntMin widthRepr (regValue -> src) = liftIO $ do
let sym = backendGetSym bak
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, IsSymBackend sym bak, HasLLVMAnn sym) =>
bak ->
CallStack ->
NatRepr w ->
RegEntry sym (BVType w) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callLibcAbs bak callStack = callAbs bak callStack LibcAbsIntMinUB
callLLVMAbs ::
(1 <= w, IsSymBackend sym bak, HasLLVMAnn sym) =>
bak ->
CallStack ->
NatRepr w ->
RegEntry sym (BVType w) ->
RegEntry sym (BVType 1) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callLLVMAbs bak 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 bak 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, IsSymBackend sym bak, ?lc :: TypeContext) =>
bak ->
NatRepr width ->
RegEntry sym (BVType (width * 8)) ->
OverrideSim p sym ext r args ret (RegValue sym (BVType (width * 8)))
callBSwapIfLittleEndian bak widthRepr vec =
case (llvmDataLayout ?lc)^.intLayout of
BigEndian -> pure (regValue vec)
LittleEndian -> callBSwap bak widthRepr vec
----------------------------------------------------------------------------
-- atexit stuff
cxa_atexitOverride
:: (IsSymInterface sym, HasPtrWidth wptr)
=> LLVMOverride p sym
(EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr ::> LLVMPointerType wptr)
(BVType 32)
cxa_atexitOverride =
[llvmOvr| i32 @__cxa_atexit( void (i8*)*, i8*, i8* ) |]
(\_ bak _args -> liftIO $ bvLit (backendGetSym bak) knownNat (BV.zero 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