content: -- |
  -- 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.MemModel.Strings as CStr
  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 $ CStr.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 $ CStr.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 $ CStr.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 $ CStr.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
  