-- |
-- Module           : Lang.Crucible.LLVM.Intrinsics.Libc.Stdlib
-- Description      : Override definitions for C @stdlib.h@ functions
-- Copyright        : (c) Galois, Inc 2026
-- License          : BSD3
-- Maintainer       : Galois, Inc. <crux@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

module Lang.Crucible.LLVM.Intrinsics.Libc.Stdlib
  ( -- * @stdlib.h@ overrides
    stdlibOverrides
    -- * Override declarations
  , llvmMallocOverride
  , llvmCallocOverride
  , llvmFreeOverride
  , llvmReallocOverride
  , posixMemalignOverride
  , llvmAbortOverride
  , llvmExitOverride
  , llvmGetenvOverride
  , llvmAbsOverride
  , llvmLAbsOverride_32
  , llvmLAbsOverride_64
  , llvmLLAbsOverride
  , cxa_atexitOverride
    -- * Implementation functions
  , callMalloc
  , callCalloc
  , callFree
  , callRealloc
  , callPosixMemalign
  , callExit
  , callLibcAbs
  , callLLVMAbs
  , callAbs
  , CheckAbsIntMin(..)
  ) where

import           Control.Monad (when)
import           Control.Monad.IO.Class (liftIO)
import           Lens.Micro ((^.))

import qualified Data.BitVector.Sized as BV
import qualified Data.Parameterized.Context as Ctx

import           What4.Interface
import           What4.ProgramLoc (plSourceLoc)

import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Common
import           Lang.Crucible.Types
import           Lang.Crucible.Simulator.OverrideSim
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Simulator.SimError

import           Lang.Crucible.LLVM.Bytes (toBytes)
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.Generic as G
import           Lang.Crucible.LLVM.MemModel.Partial (annotateUB)
import           Lang.Crucible.LLVM.QQ( llvmOvr )
import           Lang.Crucible.LLVM.TypeContext

import           Lang.Crucible.LLVM.Intrinsics.Common
import           Lang.Crucible.LLVM.Intrinsics.Options

-- | All @stdlib.h@ overrides
stdlibOverrides ::
  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
  , ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
  [SomeLLVMOverride p sym ext]
stdlibOverrides :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?intrinsicsOpts::IntrinsicsOptions,
 ?memOpts::MemOptions) =>
[SomeLLVMOverride p sym ext]
stdlibOverrides =
  [ LLVMOverride
  p sym ext (EmptyCtx ::> BVType wptr) (LLVMPointerType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p sym ext (EmptyCtx ::> BVType wptr) (LLVMPointerType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?memOpts::MemOptions) =>
LLVMOverride
  p sym ext (EmptyCtx ::> BVType wptr) (LLVMPointerType wptr)
llvmMallocOverride
  , LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> BVType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> BVType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> BVType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
llvmCallocOverride
  , LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) UnitType
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) UnitType
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) UnitType
llvmFreeOverride
  , LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
llvmReallocOverride
  , LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
   ::> BVType wptr)
  (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
   ::> BVType wptr)
  (BVType 32)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
   ::> BVType wptr)
  (BVType 32)
posixMemalignOverride
  , LLVMOverride p sym ext EmptyCtx UnitType
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride p sym ext EmptyCtx UnitType
forall sym p ext.
(IsSymInterface sym, ?intrinsicsOpts::IntrinsicsOptions) =>
LLVMOverride p sym ext EmptyCtx UnitType
llvmAbortOverride
  , LLVMOverride p sym ext (EmptyCtx ::> BVType 32) UnitType
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride p sym ext (EmptyCtx ::> BVType 32) UnitType
forall sym p ext.
(IsSymInterface sym, ?intrinsicsOpts::IntrinsicsOptions) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 32) UnitType
llvmExitOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> LLVMPointerType wptr)
  (LLVMPointerType wptr)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> LLVMPointerType wptr)
  (LLVMPointerType wptr)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> LLVMPointerType wptr)
  (LLVMPointerType wptr)
llvmGetenvOverride
  , LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
forall sym p ext.
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
llvmAbsOverride
  , LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
forall sym p ext.
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
llvmLAbsOverride_32
  , LLVMOverride p sym ext (EmptyCtx ::> BVType 64) (BVType 64)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride p sym ext (EmptyCtx ::> BVType 64) (BVType 64)
forall sym p ext.
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 64) (BVType 64)
llvmLAbsOverride_64
  , LLVMOverride p sym ext (EmptyCtx ::> BVType 64) (BVType 64)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride p sym ext (EmptyCtx ::> BVType 64) (BVType 64)
forall sym p ext.
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 64) (BVType 64)
llvmLLAbsOverride
  , LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> LLVMPointerType wptr)
  (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> LLVMPointerType wptr)
  (BVType 32)
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> LLVMPointerType wptr)
  (BVType 32)
cxa_atexitOverride
  ]

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

------------------------------------------------------------------------
-- *** Allocation

llvmCallocOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?lc :: TypeContext, ?memOpts :: MemOptions )
  => LLVMOverride p sym ext
         (EmptyCtx ::> BVType wptr ::> BVType wptr)
         (LLVMPointerType wptr)
llvmCallocOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> BVType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
llvmCallocOverride =
  let alignment :: Alignment
alignment = DataLayout -> Alignment
maxAlignment (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) in
  [llvmOvr| i8* @calloc( size_t, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym) ((EmptyCtx ::> BVType wptr) ::> BVType wptr)
args -> CurryAssignment
  ((EmptyCtx ::> BVType wptr) ::> BVType wptr)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr))
-> Assignment
     (RegEntry sym) ((EmptyCtx ::> BVType wptr) ::> BVType wptr)
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment ((EmptyCtx ::> BVType wptr) ::> BVType wptr) f x
-> Assignment f ((EmptyCtx ::> BVType wptr) ::> BVType wptr) -> x
Ctx.uncurryAssignment (GlobalVar Mem
-> Alignment
-> RegEntry sym (BVType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (LLVMPointerType wptr))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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 GlobalVar Mem
memOps Alignment
alignment) Assignment
  (RegEntry sym) ((EmptyCtx ::> BVType wptr) ::> BVType wptr)
args)


llvmReallocOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?lc :: TypeContext, ?memOpts :: MemOptions )
  => LLVMOverride p sym ext
         (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr)
         (LLVMPointerType wptr)
llvmReallocOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?memOpts::MemOptions) =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (LLVMPointerType wptr)
llvmReallocOverride =
  let alignment :: Alignment
alignment = DataLayout -> Alignment
maxAlignment (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) in
  [llvmOvr| i8* @realloc( i8*, size_t ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
args -> CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr))
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr) f x
-> Assignment
     f ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
-> x
Ctx.uncurryAssignment (GlobalVar Mem
-> Alignment
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (LLVMPointerType wptr))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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 GlobalVar Mem
memOps Alignment
alignment) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
args)

llvmMallocOverride
  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
     , ?lc :: TypeContext, ?memOpts :: MemOptions )
  => LLVMOverride p sym ext
         (EmptyCtx ::> BVType wptr)
         (LLVMPointerType wptr)
llvmMallocOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?memOpts::MemOptions) =>
LLVMOverride
  p sym ext (EmptyCtx ::> BVType wptr) (LLVMPointerType wptr)
llvmMallocOverride =
  let alignment :: Alignment
alignment = DataLayout -> Alignment
maxAlignment (TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc) in
  [llvmOvr| i8* @malloc( size_t ) |]
  (\GlobalVar Mem
memOps Assignment (RegEntry sym) (EmptyCtx ::> BVType wptr)
args -> CurryAssignment
  (EmptyCtx ::> BVType wptr)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr))
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType wptr)
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> BVType wptr) f x
-> Assignment f (EmptyCtx ::> BVType wptr) -> x
Ctx.uncurryAssignment (GlobalVar Mem
-> Alignment
-> RegEntry sym (BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (LLVMPointerType wptr))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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 GlobalVar Mem
memOps Alignment
alignment) Assignment (RegEntry sym) (EmptyCtx ::> BVType wptr)
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 :: forall sym (wptr :: Natural) p ext.
(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 ) |]
  (\GlobalVar Mem
memOps Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
   ::> BVType wptr)
args -> CurryAssignment
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
   ::> BVType wptr)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
      ::> BVType wptr)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
   ::> BVType wptr)
  f
  x
-> Assignment
     f
     (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
      ::> BVType wptr)
-> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> RegEntry sym (BVType wptr)
-> RegEntry sym (BVType wptr)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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 GlobalVar Mem
memOps) Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> BVType wptr)
   ::> BVType wptr)
args)


llvmFreeOverride
  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
  => LLVMOverride p sym ext
         (EmptyCtx ::> LLVMPointerType wptr)
         UnitType
llvmFreeOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) UnitType
llvmFreeOverride =
  [llvmOvr| void @free( i8* ) |]
  (\GlobalVar Mem
memOps Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
args -> CurryAssignment
  (EmptyCtx ::> LLVMPointerType wptr)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' ())
-> Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
-> OverrideSim p sym ext rtp args' ret' ()
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> LLVMPointerType wptr) f x
-> Assignment f (EmptyCtx ::> LLVMPointerType wptr) -> x
Ctx.uncurryAssignment (GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext rtp args' ret' ()
forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret ()
callFree GlobalVar Mem
memOps) Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
args)

------------------------------------------------------------------------
-- *** Process control

llvmAbortOverride
  :: ( IsSymInterface sym
     , ?intrinsicsOpts :: IntrinsicsOptions )
  => LLVMOverride p sym ext EmptyCtx UnitType
llvmAbortOverride :: forall sym p ext.
(IsSymInterface sym, ?intrinsicsOpts::IntrinsicsOptions) =>
LLVMOverride p sym ext EmptyCtx UnitType
llvmAbortOverride =
  [llvmOvr| void @abort() |]
  (\GlobalVar Mem
_ Assignment (RegEntry sym) EmptyCtx
_args ->
     (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType))
-> OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType)
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType))
 -> OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType))
-> OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType)
forall a b. (a -> b) -> a -> b
$ \bak
bak -> IO (RegValue sym UnitType)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType)
forall a. IO a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym UnitType)
 -> OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType))
-> IO (RegValue sym UnitType)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType)
forall a b. (a -> b) -> a -> b
$ do
       let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
       Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (IntrinsicsOptions -> AbnormalExitBehavior
abnormalExitBehavior ?intrinsicsOpts::IntrinsicsOptions
IntrinsicsOptions
?intrinsicsOpts AbnormalExitBehavior -> AbnormalExitBehavior -> Bool
forall a. Eq a => a -> a -> Bool
== AbnormalExitBehavior
AlwaysFail) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
           let err :: SimErrorReason
err = String -> String -> SimErrorReason
AssertFailureSimError String
"Call to abort" String
"" in
           bak -> Pred sym -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) SimErrorReason
err
       ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
       AbortExecReason -> IO ()
forall a. AbortExecReason -> IO a
abortExecBecause (AbortExecReason -> IO ()) -> AbortExecReason -> IO ()
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> AbortExecReason
EarlyExit ProgramLoc
loc
  )

llvmExitOverride
  :: forall sym p ext
   . ( IsSymInterface sym
     , ?intrinsicsOpts :: IntrinsicsOptions )
  => LLVMOverride p sym ext
         (EmptyCtx ::> BVType 32)
         UnitType
llvmExitOverride :: forall sym p ext.
(IsSymInterface sym, ?intrinsicsOpts::IntrinsicsOptions) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 32) UnitType
llvmExitOverride =
  [llvmOvr| void @exit( i32 ) |]
  (\GlobalVar Mem
_ Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args -> CurryAssignment
  (EmptyCtx ::> BVType 32)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' ())
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
-> OverrideSim p sym ext rtp args' ret' ()
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> BVType 32) f x
-> Assignment f (EmptyCtx ::> BVType 32) -> x
Ctx.uncurryAssignment CurryAssignment
  (EmptyCtx ::> BVType 32)
  (RegEntry sym)
  (OverrideSim p sym ext rtp args' ret' ())
RegEntry sym (BVType 32)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym UnitType)
forall sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, ?intrinsicsOpts::IntrinsicsOptions) =>
RegEntry sym (BVType 32)
-> OverrideSim p sym ext r args ret (RegValue sym UnitType)
callExit Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args)

llvmGetenvOverride
  :: (IsSymInterface sym, HasPtrWidth wptr)
  => LLVMOverride p sym ext
        (EmptyCtx ::> LLVMPointerType wptr)
        (LLVMPointerType wptr)
llvmGetenvOverride :: forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasPtrWidth wptr) =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> LLVMPointerType wptr)
  (LLVMPointerType wptr)
llvmGetenvOverride =
  [llvmOvr| i8* @getenv( i8* ) |]
  (\GlobalVar Mem
_ Assignment (RegEntry sym) (EmptyCtx ::> LLVMPointerType wptr)
_args -> do
    sym
sym <- OverrideSim p sym ext rtp args' ret' sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
    IO (LLVMPointer sym wptr)
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall a. IO a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (LLVMPointer sym wptr)
 -> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr))
-> IO (LLVMPointer sym wptr)
-> OverrideSim p sym ext rtp args' ret' (LLVMPointer sym wptr)
forall a b. (a -> b) -> a -> b
$ sym -> NatRepr wptr -> IO (RegValue sym (LLVMPointerType wptr))
forall (w :: Natural) sym.
(1 <= w, IsSymInterface sym) =>
sym -> NatRepr w -> IO (LLVMPtr sym w)
mkNullPointer sym
sym NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth)

------------------------------------------------------------------------
-- *** Integer functions

llvmAbsOverride ::
  (IsSymInterface sym, HasLLVMAnn sym) =>
  LLVMOverride p sym ext
      (EmptyCtx ::> BVType 32)
      (BVType 32)
llvmAbsOverride :: forall sym p ext.
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
llvmAbsOverride =
  [llvmOvr| i32 @abs( i32 ) |]
  (\GlobalVar Mem
mvar Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args ->
     do CallStack
callStack <- GlobalVar Mem -> OverrideSim p sym ext rtp args' ret' CallStack
forall p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
GlobalVar Mem -> OverrideSim p sym ext r args ret CallStack
callStackFromMemVar' GlobalVar Mem
mvar
        CurryAssignment
  (EmptyCtx ::> BVType 32)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> BVType 32) f x
-> Assignment f (EmptyCtx ::> BVType 32) -> x
Ctx.uncurryAssignment (CallStack
-> NatRepr 32
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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
callStack (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32)) Assignment (RegEntry sym) (EmptyCtx ::> BVType 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 :: forall sym p ext.
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 32) (BVType 32)
llvmLAbsOverride_32 =
  [llvmOvr| i32 @labs( i32 ) |]
  (\GlobalVar Mem
mvar Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args ->
     do CallStack
callStack <- GlobalVar Mem -> OverrideSim p sym ext rtp args' ret' CallStack
forall p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
GlobalVar Mem -> OverrideSim p sym ext r args ret CallStack
callStackFromMemVar' GlobalVar Mem
mvar
        CurryAssignment
  (EmptyCtx ::> BVType 32)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> BVType 32) f x
-> Assignment f (EmptyCtx ::> BVType 32) -> x
Ctx.uncurryAssignment (CallStack
-> NatRepr 32
-> RegEntry sym (BVType 32)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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
callStack (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32)) Assignment (RegEntry sym) (EmptyCtx ::> BVType 32)
args)

llvmLAbsOverride_64 ::
  (IsSymInterface sym, HasLLVMAnn sym) =>
  LLVMOverride p sym ext
      (EmptyCtx ::> BVType 64)
      (BVType 64)
llvmLAbsOverride_64 :: forall sym p ext.
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 64) (BVType 64)
llvmLAbsOverride_64 =
  [llvmOvr| i64 @labs( i64 ) |]
  (\GlobalVar Mem
mvar Assignment (RegEntry sym) (EmptyCtx ::> BVType 64)
args ->
     do CallStack
callStack <- GlobalVar Mem -> OverrideSim p sym ext rtp args' ret' CallStack
forall p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
GlobalVar Mem -> OverrideSim p sym ext r args ret CallStack
callStackFromMemVar' GlobalVar Mem
mvar
        CurryAssignment
  (EmptyCtx ::> BVType 64)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 64)))
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 64)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 64))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> BVType 64) f x
-> Assignment f (EmptyCtx ::> BVType 64) -> x
Ctx.uncurryAssignment (CallStack
-> NatRepr 64
-> RegEntry sym (BVType 64)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 64))
forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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
callStack (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64)) Assignment (RegEntry sym) (EmptyCtx ::> BVType 64)
args)

llvmLLAbsOverride ::
  (IsSymInterface sym, HasLLVMAnn sym) =>
  LLVMOverride p sym ext
      (EmptyCtx ::> BVType 64)
      (BVType 64)
llvmLLAbsOverride :: forall sym p ext.
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMOverride p sym ext (EmptyCtx ::> BVType 64) (BVType 64)
llvmLLAbsOverride =
  [llvmOvr| i64 @llabs( i64 ) |]
  (\GlobalVar Mem
mvar Assignment (RegEntry sym) (EmptyCtx ::> BVType 64)
args ->
     do CallStack
callStack <- GlobalVar Mem -> OverrideSim p sym ext rtp args' ret' CallStack
forall p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
GlobalVar Mem -> OverrideSim p sym ext r args ret CallStack
callStackFromMemVar' GlobalVar Mem
mvar
        CurryAssignment
  (EmptyCtx ::> BVType 64)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 64)))
-> Assignment (RegEntry sym) (EmptyCtx ::> BVType 64)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 64))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> BVType 64) f x
-> Assignment f (EmptyCtx ::> BVType 64) -> x
Ctx.uncurryAssignment (CallStack
-> NatRepr 64
-> RegEntry sym (BVType 64)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 64))
forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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
callStack (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64)) Assignment (RegEntry sym) (EmptyCtx ::> BVType 64)
args)

------------------------------------------------------------------------
-- *** atexit

cxa_atexitOverride
  :: (IsSymInterface sym, HasPtrWidth wptr)
  => LLVMOverride p sym ext
        (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr ::> LLVMPointerType wptr)
        (BVType 32)
cxa_atexitOverride :: forall sym (wptr :: Natural) p ext.
(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* ) |]
  (\GlobalVar Mem
_ Assignment
  (RegEntry sym)
  (((EmptyCtx ::> LLVMPointerType wptr) ::> LLVMPointerType wptr)
   ::> LLVMPointerType wptr)
_args -> do
    sym
sym <- OverrideSim p sym ext rtp args' ret' sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
    IO (SymExpr sym ('BaseBVType 32))
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall a. IO a -> OverrideSim p sym ext rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType 32))
 -> OverrideSim
      p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> IO (SymExpr sym ('BaseBVType 32))
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall a b. (a -> b) -> a -> b
$ sym -> NatRepr 32 -> IO (SymExpr sym ('BaseBVType 32))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr 32
forall (n :: Natural). KnownNat n => NatRepr n
knownNat)

------------------------------------------------------------------------
-- ** 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 :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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 GlobalVar Mem
mvar Alignment
alignment (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
ptr) (RegEntry sym (BVType wptr) -> RegValue sym (BVType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType wptr)
sz) =
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
    let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
    SymExpr sym BaseBoolType
szZero  <- IO (SymExpr sym BaseBoolType)
-> OverrideSim p sym ext r args ret (SymExpr sym BaseBoolType)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym wptr -> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNonzero sym
sym RegValue sym (BVType wptr)
SymBV sym wptr
sz)
    SymExpr sym BaseBoolType
ptrNull <- IO (SymExpr sym BaseBoolType)
-> OverrideSim p sym ext r args ret (SymExpr sym BaseBoolType)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (sym
-> NatRepr wptr
-> RegValue sym (LLVMPointerType wptr)
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural) sym.
(1 <= w, IsSymInterface sym) =>
sym -> NatRepr w -> LLVMPtr sym w -> IO (Pred sym)
ptrIsNull sym
sym NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth RegValue sym (LLVMPointerType wptr)
ptr)
    Position
loc <- IO Position -> OverrideSim p sym ext r args ret Position
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (ProgramLoc -> Position
plSourceLoc (ProgramLoc -> Position) -> IO ProgramLoc -> IO Position
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym)
    let displayString :: String
displayString = String
"<realloc> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Position -> String
forall a. Show a => a -> String
show Position
loc

    RegMap sym EmptyCtx
-> [(SymExpr sym BaseBoolType,
     OverrideSim
       p sym ext r (args <+> EmptyCtx) ret (LLVMPointer sym wptr),
     Maybe Position)]
-> OverrideSim p sym ext r args ret (LLVMPointer sym wptr)
forall p sym ext rtp (args :: Ctx CrucibleType)
       (new_args :: Ctx CrucibleType) (res :: CrucibleType) a.
IsSymInterface sym =>
RegMap sym new_args
-> [(Pred sym, OverrideSim p sym ext rtp (args <+> new_args) res a,
     Maybe Position)]
-> OverrideSim p sym ext rtp args res a
symbolicBranches RegMap sym EmptyCtx
forall sym. RegMap sym EmptyCtx
emptyRegMap
      -- If the pointer is null, behave like malloc
      [ ( SymExpr sym BaseBoolType
ptrNull
        , GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         (args <+> EmptyCtx)
         ret
         (LLVMPointer sym wptr, RegValue sym Mem))
-> OverrideSim
     p sym ext r (args <+> EmptyCtx) ret (LLVMPointer sym wptr)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim
       p
       sym
       ext
       r
       (args <+> EmptyCtx)
       ret
       (LLVMPointer sym wptr, RegValue sym Mem))
 -> OverrideSim
      p sym ext r (args <+> EmptyCtx) ret (LLVMPointer sym wptr))
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         (args <+> EmptyCtx)
         ret
         (LLVMPointer sym wptr, RegValue sym Mem))
-> OverrideSim
     p sym ext r (args <+> EmptyCtx) ret (LLVMPointer sym wptr)
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO (LLVMPointer sym wptr, RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     (args <+> EmptyCtx)
     ret
     (LLVMPointer sym wptr, RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext r (args <+> EmptyCtx) ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (LLVMPointer sym wptr, RegValue sym Mem)
 -> OverrideSim
      p
      sym
      ext
      r
      (args <+> EmptyCtx)
      ret
      (LLVMPointer sym wptr, RegValue sym Mem))
-> IO (LLVMPointer sym wptr, RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     (args <+> EmptyCtx)
     ret
     (LLVMPointer sym wptr, RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$ bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (RegValue sym (LLVMPointerType wptr), MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
doMalloc bak
bak AllocType
G.HeapAlloc Mutability
G.Mutable String
displayString RegValue sym Mem
MemImpl sym
mem RegValue sym (BVType wptr)
SymBV sym wptr
sz Alignment
alignment
        , Maybe Position
forall a. Maybe a
Nothing
        )

      -- If the size is zero, behave like malloc (of zero bytes) then free
      , (SymExpr sym BaseBoolType
szZero
        , GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         (args <+> EmptyCtx)
         ret
         (LLVMPointer sym wptr, RegValue sym Mem))
-> OverrideSim
     p sym ext r (args <+> EmptyCtx) ret (LLVMPointer sym wptr)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim
       p
       sym
       ext
       r
       (args <+> EmptyCtx)
       ret
       (LLVMPointer sym wptr, RegValue sym Mem))
 -> OverrideSim
      p sym ext r (args <+> EmptyCtx) ret (LLVMPointer sym wptr))
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         (args <+> EmptyCtx)
         ret
         (LLVMPointer sym wptr, RegValue sym Mem))
-> OverrideSim
     p sym ext r (args <+> EmptyCtx) ret (LLVMPointer sym wptr)
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO (LLVMPointer sym wptr, RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     (args <+> EmptyCtx)
     ret
     (LLVMPointer sym wptr, RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext r (args <+> EmptyCtx) ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (LLVMPointer sym wptr, RegValue sym Mem)
 -> OverrideSim
      p
      sym
      ext
      r
      (args <+> EmptyCtx)
      ret
      (LLVMPointer sym wptr, RegValue sym Mem))
-> IO (LLVMPointer sym wptr, RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     (args <+> EmptyCtx)
     ret
     (LLVMPointer sym wptr, RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$
             do (LLVMPointer sym wptr
newp, MemImpl sym
mem1) <- bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (RegValue sym (LLVMPointerType wptr), MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
doMalloc bak
bak AllocType
G.HeapAlloc Mutability
G.Mutable String
displayString RegValue sym Mem
MemImpl sym
mem RegValue sym (BVType wptr)
SymBV sym wptr
sz Alignment
alignment
                MemImpl sym
mem2 <- bak
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym) =>
bak -> MemImpl sym -> LLVMPtr sym wptr -> IO (MemImpl sym)
doFree bak
bak MemImpl sym
mem1 RegValue sym (LLVMPointerType wptr)
ptr
                (LLVMPointer sym wptr, MemImpl sym)
-> IO (LLVMPointer sym wptr, MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMPointer sym wptr
newp, MemImpl sym
mem2)
        , Maybe Position
forall a. Maybe a
Nothing
        )

      -- Otherwise, allocate a new region, memcopy `sz` bytes and free the old pointer
      , (sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym
        , GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         (args <+> EmptyCtx)
         ret
         (LLVMPointer sym wptr, RegValue sym Mem))
-> OverrideSim
     p sym ext r (args <+> EmptyCtx) ret (LLVMPointer sym wptr)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim
       p
       sym
       ext
       r
       (args <+> EmptyCtx)
       ret
       (LLVMPointer sym wptr, RegValue sym Mem))
 -> OverrideSim
      p sym ext r (args <+> EmptyCtx) ret (LLVMPointer sym wptr))
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         (args <+> EmptyCtx)
         ret
         (LLVMPointer sym wptr, RegValue sym Mem))
-> OverrideSim
     p sym ext r (args <+> EmptyCtx) ret (LLVMPointer sym wptr)
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO (LLVMPointer sym wptr, RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     (args <+> EmptyCtx)
     ret
     (LLVMPointer sym wptr, RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext r (args <+> EmptyCtx) ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (LLVMPointer sym wptr, RegValue sym Mem)
 -> OverrideSim
      p
      sym
      ext
      r
      (args <+> EmptyCtx)
      ret
      (LLVMPointer sym wptr, RegValue sym Mem))
-> IO (LLVMPointer sym wptr, RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     (args <+> EmptyCtx)
     ret
     (LLVMPointer sym wptr, RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$
             do (LLVMPointer sym wptr
newp, MemImpl sym
mem1) <- bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (RegValue sym (LLVMPointerType wptr), MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
doMalloc bak
bak AllocType
G.HeapAlloc Mutability
G.Mutable String
displayString RegValue sym Mem
MemImpl sym
mem RegValue sym (BVType wptr)
SymBV sym wptr
sz Alignment
alignment
                MemImpl sym
mem2 <- sym
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
-> SymBV sym wptr
-> IO (MemImpl sym)
forall sym (wptr :: Natural).
(IsSymInterface sym, HasPtrWidth wptr) =>
sym
-> MemImpl sym
-> LLVMPtr sym wptr
-> LLVMPtr sym wptr
-> SymBV sym wptr
-> IO (MemImpl sym)
uncheckedMemcpy sym
sym MemImpl sym
mem1 RegValue sym (LLVMPointerType wptr)
LLVMPointer sym wptr
newp RegValue sym (LLVMPointerType wptr)
ptr RegValue sym (BVType wptr)
SymBV sym wptr
sz
                MemImpl sym
mem3 <- bak
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym) =>
bak -> MemImpl sym -> LLVMPtr sym wptr -> IO (MemImpl sym)
doFree bak
bak MemImpl sym
mem2 RegValue sym (LLVMPointerType wptr)
ptr
                (LLVMPointer sym wptr, MemImpl sym)
-> IO (LLVMPointer sym wptr, MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMPointer sym wptr
newp, MemImpl sym
mem3)
        , Maybe Position
forall a. Maybe a
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 :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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 GlobalVar Mem
mvar (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
outPtr) (RegEntry sym (BVType wptr) -> RegValue sym (BVType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType wptr)
align) (RegEntry sym (BVType wptr) -> RegValue sym (BVType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType wptr)
sz) =
  (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak in
    case SymExpr sym (BaseBVType wptr) -> Maybe (BV wptr)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV RegValue sym (BVType wptr)
SymExpr sym (BaseBVType wptr)
align of
      Maybe (BV wptr)
Nothing -> String
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall a. String -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> String
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"posix_memalign: alignment value must be concrete:", Doc Any -> String
forall a. Show a => a -> String
show (SymExpr sym (BaseBVType wptr) -> Doc Any
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr RegValue sym (BVType wptr)
SymExpr sym (BaseBVType wptr)
align)]
      Just BV wptr
concrete_align ->
        case Bytes -> Maybe Alignment
toAlignment (Integer -> Bytes
forall a. Integral a => a -> Bytes
toBytes (BV wptr -> Integer
forall (w :: Natural). BV w -> Integer
BV.asUnsigned BV wptr
concrete_align)) of
          Maybe Alignment
Nothing -> String
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall a. String -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> String
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [String
"posix_memalign: invalid alignment value:", BV wptr -> String
forall a. Show a => a -> String
show BV wptr
concrete_align]
          Just Alignment
a ->
            let dl :: DataLayout
dl = TypeContext -> DataLayout
llvmDataLayout ?lc::TypeContext
TypeContext
?lc in
            GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim
         p sym ext r args ret (RegValue sym (BVType 32), RegValue sym Mem))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim
       p sym ext r args ret (RegValue sym (BVType 32), RegValue sym Mem))
 -> OverrideSim p sym ext r args ret (RegValue sym (BVType 32)))
-> (RegValue sym Mem
    -> OverrideSim
         p sym ext r args ret (RegValue sym (BVType 32), RegValue sym Mem))
-> OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO (RegValue sym (BVType 32), RegValue sym Mem)
-> OverrideSim
     p sym ext r args ret (RegValue sym (BVType 32), RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym (BVType 32), RegValue sym Mem)
 -> OverrideSim
      p sym ext r args ret (RegValue sym (BVType 32), RegValue sym Mem))
-> IO (RegValue sym (BVType 32), RegValue sym Mem)
-> OverrideSim
     p sym ext r args ret (RegValue sym (BVType 32), RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$
               do Position
loc <- ProgramLoc -> Position
plSourceLoc (ProgramLoc -> Position) -> IO ProgramLoc -> IO Position
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
                  let displayString :: String
displayString = String
"<posix_memaign> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Position -> String
forall a. Show a => a -> String
show Position
loc
                  (LLVMPointer sym wptr
p, MemImpl sym
mem') <- bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymExpr sym (BaseBVType wptr)
-> Alignment
-> IO (RegValue sym (LLVMPointerType wptr), MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
doMalloc bak
bak AllocType
G.HeapAlloc Mutability
G.Mutable String
displayString RegValue sym Mem
MemImpl sym
mem RegValue sym (BVType wptr)
SymExpr sym (BaseBVType wptr)
sz Alignment
a
                  MemImpl sym
mem'' <- bak
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> StorageType
-> Alignment
-> LLVMVal sym
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> LLVMPtr sym wptr
-> StorageType
-> Alignment
-> LLVMVal sym
-> IO (MemImpl sym)
storeRaw bak
bak MemImpl sym
mem' RegValue sym (LLVMPointerType wptr)
outPtr (Bytes -> StorageType
bitvectorType (DataLayout
dlDataLayout -> Getting Bytes DataLayout Bytes -> Bytes
forall s a. s -> Getting a s a -> a
^.Getting Bytes DataLayout Bytes
Lens' DataLayout Bytes
ptrSize)) (DataLayout
dlDataLayout -> Getting Alignment DataLayout Alignment -> Alignment
forall s a. s -> Getting a s a -> a
^.Getting Alignment DataLayout Alignment
Lens' DataLayout Alignment
ptrAlign) (RegValue sym (LLVMPointerType wptr) -> LLVMVal sym
forall (w :: Natural) sym. (1 <= w) => LLVMPtr sym w -> LLVMVal sym
ptrToPtrVal RegValue sym (LLVMPointerType wptr)
LLVMPointer sym wptr
p)
                  SymExpr sym ('BaseBVType 32)
z <- sym -> NatRepr 32 -> IO (SymExpr sym ('BaseBVType 32))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr 32
forall (n :: Natural). KnownNat n => NatRepr n
knownNat
                  (SymExpr sym ('BaseBVType 32), MemImpl sym)
-> IO (SymExpr sym ('BaseBVType 32), MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymExpr sym ('BaseBVType 32)
z, MemImpl sym
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 :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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 GlobalVar Mem
mvar Alignment
alignment (RegEntry sym (BVType wptr) -> RegValue sym (BVType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType wptr)
sz) =
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         args
         ret
         (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim
       p
       sym
       ext
       r
       args
       ret
       (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         args
         ret
         (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     args
     ret
     (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
 -> OverrideSim
      p
      sym
      ext
      r
      args
      ret
      (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> IO (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     args
     ret
     (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$
      do Position
loc <- ProgramLoc -> Position
plSourceLoc (ProgramLoc -> Position) -> IO ProgramLoc -> IO Position
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc (bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak)
         let displayString :: String
displayString = String
"<malloc> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Position -> String
forall a. Show a => a -> String
show Position
loc
         bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (RegValue sym (LLVMPointerType wptr), MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> AllocType
-> Mutability
-> String
-> MemImpl sym
-> SymBV sym wptr
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
doMalloc bak
bak AllocType
G.HeapAlloc Mutability
G.Mutable String
displayString RegValue sym Mem
MemImpl sym
mem RegValue sym (BVType wptr)
SymBV sym wptr
sz Alignment
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 :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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 GlobalVar Mem
mvar Alignment
alignment
           (RegEntry sym (BVType wptr) -> RegValue sym (BVType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType wptr)
sz)
           (RegEntry sym (BVType wptr) -> RegValue sym (BVType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType wptr)
num) =
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim
       p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim
         p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         args
         ret
         (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim
       p
       sym
       ext
       r
       args
       ret
       (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
 -> OverrideSim
      p sym ext r args ret (RegValue sym (LLVMPointerType wptr)))
-> (RegValue sym Mem
    -> OverrideSim
         p
         sym
         ext
         r
         args
         ret
         (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> OverrideSim
     p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     args
     ret
     (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
 -> OverrideSim
      p
      sym
      ext
      r
      args
      ret
      (RegValue sym (LLVMPointerType wptr), RegValue sym Mem))
-> IO (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
-> OverrideSim
     p
     sym
     ext
     r
     args
     ret
     (RegValue sym (LLVMPointerType wptr), RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$
      bak
-> MemImpl sym
-> SymBV sym wptr
-> SymBV sym wptr
-> Alignment
-> IO (RegValue sym (LLVMPointerType wptr), MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> SymBV sym wptr
-> SymBV sym wptr
-> Alignment
-> IO (LLVMPtr sym wptr, MemImpl sym)
doCalloc bak
bak RegValue sym Mem
MemImpl sym
mem RegValue sym (BVType wptr)
SymBV sym wptr
sz RegValue sym (BVType wptr)
SymBV sym wptr
num Alignment
alignment

callFree
  :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr)
  => GlobalVar Mem
  -> RegEntry sym (LLVMPointerType wptr)
  -> OverrideSim p sym ext r args ret ()
callFree :: forall sym (wptr :: Natural) p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> RegEntry sym (LLVMPointerType wptr)
-> OverrideSim p sym ext r args ret ()
callFree GlobalVar Mem
mvar
           (RegEntry sym (LLVMPointerType wptr)
-> RegValue sym (LLVMPointerType wptr)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (LLVMPointerType wptr)
ptr) =
  (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args ret ())
-> OverrideSim p sym ext r args ret ()
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext r args ret ())
 -> OverrideSim p sym ext r args ret ())
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args ret ())
-> OverrideSim p sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ \bak
bak ->
    GlobalVar Mem
-> (RegValue sym Mem
    -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
-> OverrideSim p sym ext r args ret ()
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType) a.
IsSymInterface sym =>
GlobalVar tp
-> (RegValue sym tp
    -> OverrideSim p sym ext rtp args ret (a, RegValue sym tp))
-> OverrideSim p sym ext rtp args ret a
modifyGlobal GlobalVar Mem
mvar ((RegValue sym Mem
  -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
 -> OverrideSim p sym ext r args ret ())
-> (RegValue sym Mem
    -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
-> OverrideSim p sym ext r args ret ()
forall a b. (a -> b) -> a -> b
$ \RegValue sym Mem
mem -> IO ((), RegValue sym Mem)
-> OverrideSim p sym ext r args ret ((), RegValue sym Mem)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO ((), RegValue sym Mem)
 -> OverrideSim p sym ext r args ret ((), RegValue sym Mem))
-> IO ((), RegValue sym Mem)
-> OverrideSim p sym ext r args ret ((), RegValue sym Mem)
forall a b. (a -> b) -> a -> b
$
      do MemImpl sym
mem' <- bak
-> MemImpl sym
-> RegValue sym (LLVMPointerType wptr)
-> IO (MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym) =>
bak -> MemImpl sym -> LLVMPtr sym wptr -> IO (MemImpl sym)
doFree bak
bak RegValue sym Mem
MemImpl sym
mem RegValue sym (LLVMPointerType wptr)
ptr
         ((), MemImpl sym) -> IO ((), MemImpl sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((), MemImpl sym
mem')

------------------------------------------------------------------------
-- *** Process control

callExit :: ( IsSymInterface sym
            , ?intrinsicsOpts :: IntrinsicsOptions )
         => RegEntry sym (BVType 32)
         -> OverrideSim p sym ext r args ret (RegValue sym UnitType)
callExit :: forall sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, ?intrinsicsOpts::IntrinsicsOptions) =>
RegEntry sym (BVType 32)
-> OverrideSim p sym ext r args ret (RegValue sym UnitType)
callExit RegEntry sym (BVType 32)
ec =
  (forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext r args ret (RegValue sym UnitType))
-> OverrideSim p sym ext r args ret (RegValue sym UnitType)
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak -> OverrideSim p sym ext r args ret (RegValue sym UnitType))
 -> OverrideSim p sym ext r args ret (RegValue sym UnitType))
-> (forall bak.
    IsSymBackend sym bak =>
    bak -> OverrideSim p sym ext r args ret (RegValue sym UnitType))
-> OverrideSim p sym ext r args ret (RegValue sym UnitType)
forall a b. (a -> b) -> a -> b
$ \bak
bak -> IO (RegValue sym UnitType)
-> OverrideSim p sym ext r args ret (RegValue sym UnitType)
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (RegValue sym UnitType)
 -> OverrideSim p sym ext r args ret (RegValue sym UnitType))
-> IO (RegValue sym UnitType)
-> OverrideSim p sym ext r args ret (RegValue sym UnitType)
forall a b. (a -> b) -> a -> b
$ do
    let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
    Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (IntrinsicsOptions -> AbnormalExitBehavior
abnormalExitBehavior ?intrinsicsOpts::IntrinsicsOptions
IntrinsicsOptions
?intrinsicsOpts AbnormalExitBehavior -> AbnormalExitBehavior -> Bool
forall a. Eq a => a -> a -> Bool
== AbnormalExitBehavior
AlwaysFail) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
      do SymExpr sym BaseBoolType
cond <- sym
-> SymExpr sym ('BaseBVType 32)
-> SymExpr sym ('BaseBVType 32)
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym (RegEntry sym (BVType 32) -> RegValue sym (BVType 32)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue RegEntry sym (BVType 32)
ec) (SymExpr sym ('BaseBVType 32) -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym ('BaseBVType 32))
-> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr 32 -> IO (SymExpr sym ('BaseBVType 32))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr 32
forall (n :: Natural). KnownNat n => NatRepr n
knownNat
         -- If the argument is non-zero, throw an assertion failure. Otherwise,
         -- simply stop the current thread of execution.
         bak -> SymExpr sym BaseBoolType -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak SymExpr sym BaseBoolType
cond SimErrorReason
"Call to exit() with non-zero argument"
    ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
    AbortExecReason -> IO ()
forall a. AbortExecReason -> IO a
abortExecBecause (AbortExecReason -> IO ()) -> AbortExecReason -> IO ()
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> AbortExecReason
EarlyExit ProgramLoc
loc

------------------------------------------------------------------------
-- *** Integer functions

-- | 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 :: forall (w :: Natural) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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
callStack CheckAbsIntMin
checkIntMin NatRepr w
widthRepr (RegEntry sym (BVType w) -> RegValue sym (BVType w)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType w)
src) = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  (forall bak.
 IsSymBackend sym bak =>
 bak
 -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w)))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w))
forall sym p ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType) a.
(forall bak.
 IsSymBackend sym bak =>
 bak -> OverrideSim p sym ext rtp args ret a)
-> OverrideSim p sym ext rtp args ret a
ovrWithBackend ((forall bak.
  IsSymBackend sym bak =>
  bak
  -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w)))
 -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w)))
-> (forall bak.
    IsSymBackend sym bak =>
    bak
    -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w)))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w))
forall a b. (a -> b) -> a -> b
$ \bak
bak -> IO (SymExpr sym ('BaseBVType w))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType w))
 -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w)))
-> IO (SymExpr sym ('BaseBVType w))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w))
forall a b. (a -> b) -> a -> b
$ do
    SymExpr sym ('BaseBVType w)
bvIntMin    <- sym -> NatRepr w -> BV w -> IO (SymExpr sym ('BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
widthRepr (NatRepr w -> BV w
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.minSigned NatRepr w
widthRepr)
    SymExpr sym BaseBoolType
isNotIntMin <- sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym RegValue sym (BVType w)
SymExpr sym ('BaseBVType w)
src SymExpr sym ('BaseBVType w)
bvIntMin

    Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when Bool
shouldCheckIntMin (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
      SymExpr sym BaseBoolType
isNotIntMinUB <- sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
(IsSymInterface sym, HasLLVMAnn sym) =>
sym
-> CallStack
-> UndefinedBehavior (RegValue' sym)
-> Pred sym
-> IO (Pred sym)
annotateUB sym
sym CallStack
callStack UndefinedBehavior (RegValue' sym)
ub SymExpr sym BaseBoolType
isNotIntMin
      let err :: SimErrorReason
err = String -> String -> SimErrorReason
AssertFailureSimError String
"Undefined behavior encountered" (String -> SimErrorReason) -> String -> SimErrorReason
forall a b. (a -> b) -> a -> b
$
                Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ UndefinedBehavior (RegValue' sym) -> Doc Any
forall (e :: CrucibleType -> Type) ann.
UndefinedBehavior e -> Doc ann
UB.explain UndefinedBehavior (RegValue' sym)
ub
      bak -> SymExpr sym BaseBoolType -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak SymExpr sym BaseBoolType
isNotIntMinUB SimErrorReason
err

    SymExpr sym BaseBoolType
isSrcNegative <- sym -> SymExpr sym ('BaseBVType w) -> IO (SymExpr sym BaseBoolType)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
bvIsNeg sym
sym RegValue sym (BVType w)
SymExpr sym ('BaseBVType w)
src
    SymExpr sym ('BaseBVType w)
srcNegated    <- sym
-> SymExpr sym ('BaseBVType w) -> IO (SymExpr sym ('BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
bvNeg sym
sym RegValue sym (BVType w)
SymExpr sym ('BaseBVType w)
src
    sym
-> SymExpr sym BaseBoolType
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym ('BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
isSrcNegative SymExpr sym ('BaseBVType w)
srcNegated RegValue sym (BVType w)
SymExpr sym ('BaseBVType w)
src
    where
      shouldCheckIntMin :: Bool
      shouldCheckIntMin :: Bool
shouldCheckIntMin =
        case CheckAbsIntMin
checkIntMin of
          CheckAbsIntMin
LibcAbsIntMinUB                 -> Bool
True
          LLVMAbsIntMinPoison Bool
shouldCheck -> Bool
shouldCheck

      ub :: UB.UndefinedBehavior (RegValue' sym)
      ub :: UndefinedBehavior (RegValue' sym)
ub = case CheckAbsIntMin
checkIntMin of
             CheckAbsIntMin
LibcAbsIntMinUB ->
               RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> UndefinedBehavior e
UB.AbsIntMin (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym)
forall a b. (a -> b) -> a -> b
$ RegValue sym (BVType w) -> RegValue' sym (BVType w)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV RegValue sym (BVType w)
src
             LLVMAbsIntMinPoison{} ->
               Poison (RegValue' sym) -> UndefinedBehavior (RegValue' sym)
forall (e :: CrucibleType -> Type). Poison e -> UndefinedBehavior e
UB.PoisonValueCreated (Poison (RegValue' sym) -> UndefinedBehavior (RegValue' sym))
-> Poison (RegValue' sym) -> UndefinedBehavior (RegValue' sym)
forall a b. (a -> b) -> a -> b
$ RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> Poison e
Poison.LLVMAbsIntMin (RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall a b. (a -> b) -> a -> b
$ RegValue sym (BVType w) -> RegValue' sym (BVType w)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV RegValue sym (BVType w)
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 :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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
callStack = CallStack
-> CheckAbsIntMin
-> NatRepr w
-> RegEntry sym ('BaseToType ('BaseBVType w))
-> OverrideSim
     p sym ext r args ret (RegValue sym ('BaseToType ('BaseBVType w)))
forall (w :: Natural) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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
callStack CheckAbsIntMin
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 :: forall (w :: Natural) sym p ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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
callStack NatRepr w
widthRepr RegEntry sym (BVType w)
src (RegEntry sym (BVType 1) -> RegValue sym (BVType 1)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (BVType 1)
isIntMinPoison) = do
  Bool
shouldCheckIntMin <- IO Bool -> OverrideSim p sym ext r args ret Bool
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> OverrideSim p sym ext r args ret Bool)
-> IO Bool -> OverrideSim p sym ext r args ret Bool
forall a b. (a -> b) -> a -> b
$
    -- Per https://releases.llvm.org/12.0.0/docs/LangRef.html#id451, the second
    -- argument must be a constant.
    case SymExpr sym (BaseBVType 1) -> Maybe (BV 1)
forall (w :: Natural). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV RegValue sym (BVType 1)
SymExpr sym (BaseBVType 1)
isIntMinPoison of
      Just BV 1
bv -> Bool -> IO Bool
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (BV 1
bv BV 1 -> BV 1 -> Bool
forall a. Eq a => a -> a -> Bool
/= NatRepr 1 -> BV 1
forall (w :: Natural). NatRepr w -> BV w
BV.zero (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1))
      Maybe (BV 1)
Nothing -> Doc Void -> [Doc Void] -> IO Bool
forall a. Doc Void -> [Doc Void] -> a
malformedLLVMModule
                   Doc Void
"Call to llvm.abs.* with non-constant second argument"
                   [SymExpr sym (BaseBVType 1) -> Doc Void
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr RegValue sym (BVType 1)
SymExpr sym (BaseBVType 1)
isIntMinPoison]
  CallStack
-> CheckAbsIntMin
-> NatRepr w
-> RegEntry sym (BVType w)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
forall (w :: Natural) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(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
callStack (Bool -> CheckAbsIntMin
LLVMAbsIntMinPoison Bool
shouldCheckIntMin) NatRepr w
widthRepr RegEntry sym (BVType w)
src