-- |
-- Module           : Lang.Crucible.LLVM.Intrinsics.Common
-- Description      : Types used in override definitions
-- Copyright        : (c) Galois, Inc 2015-2026
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

module Lang.Crucible.LLVM.Intrinsics.Common
  ( LLVMOverride(..)
  , llvmOvSymbol
  , llvmOvName
  , llvmOvArgs
  , llvmOvRet
  , SomeLLVMOverride(..)
  , someLlvmOverrideDeclare
  , MakeOverride(..)
  , llvmSizeT
  , llvmSSizeT
  , OverrideTemplate(..)
  , callStackFromMemVar'
    -- ** register_llvm_override
  , basic_llvm_override
  , polymorphic1_llvm_override
  , polymorphic1_vec_llvm_override
  , polymorphic_cmp_llvm_override

  , llvmOverrideToTypedOverride
  , register_llvm_override
  , register_1arg_polymorphic_override
  , register_1arg_vec_polymorphic_override
  , do_register_llvm_override
  , alloc_and_register_override
  ) where

import qualified Text.LLVM.AST as L

import           Control.Monad (when)
import           Control.Monad.IO.Class (liftIO)
import qualified Data.List as List
import qualified Data.Maybe as Maybe
import qualified Data.Text as Text
import           Lens.Micro ((^.), to)
import           Lens.Micro.Mtl (use)
import           Numeric (readDec)
import qualified System.Info as Info

import qualified ABI.Itanium as ABI
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Some (Some(..))

import           Lang.Crucible.Backend
import           Lang.Crucible.CFG.Common (GlobalVar)
import           Lang.Crucible.Simulator.ExecutionTree (FnState(UseOverride))
import           Lang.Crucible.Simulator.OverrideSim
import           Lang.Crucible.Utils.MonadVerbosity (getLogFunction)
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Types

import           What4.FunctionName

import           Lang.Crucible.LLVM.Extension
import           Lang.Crucible.LLVM.Eval (callStackFromMemVar)
import           Lang.Crucible.LLVM.Functions (registerFunPtr, bindLLVMFunc)
import           Lang.Crucible.LLVM.MemModel
import           Lang.Crucible.LLVM.MemModel.CallStack (CallStack)
import qualified Lang.Crucible.LLVM.Intrinsics.Declare as Decl
import qualified Lang.Crucible.LLVM.Intrinsics.Match as Match
import           Lang.Crucible.LLVM.Translation.Monad

-- | This type represents an implementation of an LLVM intrinsic function in
-- Crucible.
--
-- This is parameterized over @ext@ so that 'LLVMOverride's can more easily be
-- reused in the context of other language extensions that are also based on the
-- LLVM memory model, such as Macaw.
data LLVMOverride p sym ext args ret =
  LLVMOverride
  { forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Declare args ret
llvmOvDecl :: Decl.Declare args ret
  , forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret
-> IsSymInterface sym =>
   GlobalVar Mem
   -> Assignment (RegEntry sym) args
   -> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
      OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
llvmOvDefn ::
      IsSymInterface sym =>
      GlobalVar Mem ->
      Ctx.Assignment (RegEntry sym) args ->
      forall rtp args' ret'.
      OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
    -- ^ The implementation of the intrinsic in the simulator monad
    -- (@OverrideSim@).
  }

llvmOvSymbol :: LLVMOverride p sym ext args ret -> L.Symbol
llvmOvSymbol :: forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Symbol
llvmOvSymbol = Declare args ret -> Symbol
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName (Declare args ret -> Symbol)
-> (LLVMOverride p sym ext args ret -> Declare args ret)
-> LLVMOverride p sym ext args ret
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LLVMOverride p sym ext args ret -> Declare args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Declare args ret
llvmOvDecl

llvmOvName :: LLVMOverride p sym ext args ret -> FunctionName
llvmOvName :: forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> FunctionName
llvmOvName LLVMOverride p sym ext args ret
ov =
  let L.Symbol String
nm = LLVMOverride p sym ext args ret -> Symbol
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Symbol
llvmOvSymbol LLVMOverride p sym ext args ret
ov in
  Text -> FunctionName
functionNameFromText (String -> Text
Text.pack String
nm)

llvmOvArgs :: LLVMOverride p sym ext args ret -> CtxRepr args
llvmOvArgs :: forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> CtxRepr args
llvmOvArgs = Declare args ret -> Assignment TypeRepr args
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Assignment TypeRepr args
Decl.decArgs (Declare args ret -> Assignment TypeRepr args)
-> (LLVMOverride p sym ext args ret -> Declare args ret)
-> LLVMOverride p sym ext args ret
-> Assignment TypeRepr args
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LLVMOverride p sym ext args ret -> Declare args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Declare args ret
llvmOvDecl

llvmOvRet :: LLVMOverride p sym ext args ret -> TypeRepr ret
llvmOvRet :: forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> TypeRepr ret
llvmOvRet = Declare args ret -> TypeRepr ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> TypeRepr ret
Decl.decRet (Declare args ret -> TypeRepr ret)
-> (LLVMOverride p sym ext args ret -> Declare args ret)
-> LLVMOverride p sym ext args ret
-> TypeRepr ret
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LLVMOverride p sym ext args ret -> Declare args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Declare args ret
llvmOvDecl

data SomeLLVMOverride p sym ext =
  forall args ret. SomeLLVMOverride (LLVMOverride p sym ext args ret)

-- | Map 'llvmOverride_decl' inside a 'SomeLLVMOverride'.
someLlvmOverrideDeclare :: SomeLLVMOverride p sym ext -> Decl.SomeDeclare
someLlvmOverrideDeclare :: forall p sym ext. SomeLLVMOverride p sym ext -> SomeDeclare
someLlvmOverrideDeclare (SomeLLVMOverride LLVMOverride p sym ext args ret
ov) =
  Declare args ret -> SomeDeclare
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> SomeDeclare
Decl.SomeDeclare (LLVMOverride p sym ext args ret -> Declare args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Declare args ret
llvmOvDecl LLVMOverride p sym ext args ret
ov)

-- | Convenient LLVM representation of the @size_t@ type.
llvmSizeT :: HasPtrWidth wptr => L.Type
llvmSizeT :: forall (wptr :: Natural). HasPtrWidth wptr => Type
llvmSizeT = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (PrimType -> Type) -> PrimType -> Type
forall a b. (a -> b) -> a -> b
$ Word32 -> PrimType
L.Integer (Word32 -> PrimType) -> Word32 -> PrimType
forall a b. (a -> b) -> a -> b
$ Natural -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Word32) -> Natural -> Word32
forall a b. (a -> b) -> a -> b
$ NatRepr wptr -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue (NatRepr wptr -> Natural) -> NatRepr wptr -> Natural
forall a b. (a -> b) -> a -> b
$ NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth

-- | Convenient LLVM representation of the @ssize_t@ type.
llvmSSizeT :: HasPtrWidth wptr => L.Type
llvmSSizeT :: forall (wptr :: Natural). HasPtrWidth wptr => Type
llvmSSizeT = PrimType -> Type
forall ident. PrimType -> Type' ident
L.PrimType (PrimType -> Type) -> PrimType -> Type
forall a b. (a -> b) -> a -> b
$ Word32 -> PrimType
L.Integer (Word32 -> PrimType) -> Word32 -> PrimType
forall a b. (a -> b) -> a -> b
$ Natural -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Word32) -> Natural -> Word32
forall a b. (a -> b) -> a -> b
$ NatRepr wptr -> Natural
forall (n :: Natural). NatRepr n -> Natural
natValue (NatRepr wptr -> Natural) -> NatRepr wptr -> Natural
forall a b. (a -> b) -> a -> b
$ NatRepr wptr
forall (w :: Natural) (w' :: Natural).
(HasPtrWidth w, w ~ w') =>
NatRepr w'
PtrWidth

-- | A funcion that inspects an LLVM declaration (along with some other data),
-- and constructs an override for the declaration if it can.
newtype MakeOverride p sym ext arch =
  MakeOverride
    { forall p sym ext (arch :: LLVMArch).
MakeOverride p sym ext arch
-> SomeDeclare
-> Maybe DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym ext)
runMakeOverride ::
        Decl.SomeDeclare ->
        -- Decoded version of the name in the declaration
        Maybe ABI.DecodedName ->
        LLVMContext arch ->
        Maybe (SomeLLVMOverride p sym ext)
    }

-- | Checking if an override applies to a given declaration happens in two
-- \"phases\", corresponding to the fields of this struct.
data OverrideTemplate p sym ext arch =
  OverrideTemplate
  { -- | An initial, quick, string-based check if an override might apply to a
    -- given declaration, based on its name
    forall p sym ext (arch :: LLVMArch).
OverrideTemplate p sym ext arch -> TemplateMatcher
overrideTemplateMatcher :: Match.TemplateMatcher
    -- | If the 'Match.TemplateMatcher' does indeed match, this slower
    -- 'MakeOverride' performs additional checks and potentially constructs
    -- a 'SomeLLVMOverride'.
  , forall p sym ext (arch :: LLVMArch).
OverrideTemplate p sym ext arch -> MakeOverride p sym ext arch
overrideTemplateAction :: MakeOverride p sym ext arch
  }

callStackFromMemVar' ::
  GlobalVar Mem ->
  OverrideSim p sym ext r args ret CallStack
callStackFromMemVar' :: forall p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
GlobalVar Mem -> OverrideSim p sym ext r args ret CallStack
callStackFromMemVar' GlobalVar Mem
mvar = Getting
  CallStack
  (SimState p sym ext r (OverrideLang ret) ('Just args))
  CallStack
-> OverrideSim p sym ext r args ret CallStack
forall s (m :: Type -> Type) a.
MonadState s m =>
Getting a s a -> m a
use ((SimState p sym ext r (OverrideLang ret) ('Just args) -> CallStack)
-> SimpleGetter
     (SimState p sym ext r (OverrideLang ret) ('Just args)) CallStack
forall s a. (s -> a) -> SimpleGetter s a
to ((SimState p sym ext r (OverrideLang ret) ('Just args)
 -> GlobalVar Mem -> CallStack)
-> GlobalVar Mem
-> SimState p sym ext r (OverrideLang ret) ('Just args)
-> CallStack
forall a b c. (a -> b -> c) -> b -> a -> c
flip SimState p sym ext r (OverrideLang ret) ('Just args)
-> GlobalVar Mem -> CallStack
forall p sym ext rtp lang (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp lang args -> GlobalVar Mem -> CallStack
callStackFromMemVar GlobalVar Mem
mvar))

------------------------------------------------------------------------
-- ** register_llvm_override


llvmOverrideToTypedOverride ::
  IsSymInterface sym =>
  HasLLVMAnn sym =>
  GlobalVar Mem ->
  LLVMOverride p sym ext args ret ->
  TypedOverride p sym ext args ret
llvmOverrideToTypedOverride :: forall sym p ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym) =>
GlobalVar Mem
-> LLVMOverride p sym ext args ret
-> TypedOverride p sym ext args ret
llvmOverrideToTypedOverride GlobalVar Mem
mvar LLVMOverride p sym ext args ret
ov =
  TypedOverride
  { typedOverrideArgs :: CtxRepr args
typedOverrideArgs = LLVMOverride p sym ext args ret -> CtxRepr args
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> CtxRepr args
llvmOvArgs LLVMOverride p sym ext args ret
ov
  , typedOverrideRet :: TypeRepr ret
typedOverrideRet = LLVMOverride p sym ext args ret -> TypeRepr ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> TypeRepr ret
llvmOvRet LLVMOverride p sym ext args ret
ov
  , typedOverrideHandler :: forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
Assignment (RegValue' sym) args
-> OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
typedOverrideHandler =
      \Assignment (RegValue' sym) args
args -> do
        let argEntries :: Assignment (RegEntry sym) args
argEntries =
              (forall (x :: CrucibleType).
 TypeRepr x -> RegValue' sym x -> RegEntry sym x)
-> CtxRepr args
-> Assignment (RegValue' sym) args
-> Assignment (RegEntry sym) args
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
       (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
Ctx.zipWith (\TypeRepr x
t (RV RegValue sym x
v) -> TypeRepr x -> RegValue sym x -> RegEntry sym x
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr x
t RegValue sym x
v) (LLVMOverride p sym ext args ret -> CtxRepr args
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> CtxRepr args
llvmOvArgs LLVMOverride p sym ext args ret
ov) Assignment (RegValue' sym) args
args
        LLVMOverride p sym ext args ret
-> IsSymInterface sym =>
   GlobalVar Mem
   -> Assignment (RegEntry sym) args
   -> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
      OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret
-> IsSymInterface sym =>
   GlobalVar Mem
   -> Assignment (RegEntry sym) args
   -> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
      OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
llvmOvDefn LLVMOverride p sym ext args ret
ov GlobalVar Mem
mvar Assignment (RegEntry sym) args
argEntries
  }

polymorphic1_llvm_override :: forall p sym ext arch wptr.
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  String ->
  (forall w. (1 <= w) => NatRepr w -> SomeLLVMOverride p sym ext) ->
  OverrideTemplate p sym ext arch
polymorphic1_llvm_override :: forall p sym ext (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
String
-> (forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> SomeLLVMOverride p sym ext)
-> OverrideTemplate p sym ext arch
polymorphic1_llvm_override String
prefix forall (w :: Natural).
(1 <= w) =>
NatRepr w -> SomeLLVMOverride p sym ext
fn =
  TemplateMatcher
-> MakeOverride p sym ext arch -> OverrideTemplate p sym ext arch
forall p sym ext (arch :: LLVMArch).
TemplateMatcher
-> MakeOverride p sym ext arch -> OverrideTemplate p sym ext arch
OverrideTemplate (String -> TemplateMatcher
Match.PrefixMatch String
prefix) (String
-> (forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> SomeLLVMOverride p sym ext)
-> MakeOverride p sym ext arch
forall p sym ext (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
String
-> (forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> SomeLLVMOverride p sym ext)
-> MakeOverride p sym ext arch
register_1arg_polymorphic_override String
prefix NatRepr w -> SomeLLVMOverride p sym ext
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> SomeLLVMOverride p sym ext
fn)

-- | Create an 'OverrideTemplate' for a polymorphic LLVM override involving
-- a vector type. For example, the @llvm.vector.reduce.add.*@ intrinsic can be
-- instantiated at multiple types, including:
--
-- * @i32 \@llvm.vector.reduce.add.v4i32(<4 x i32>)@
--
-- * @i64 \@llvm.vector.reduce.add.v2i64(<2 x i64>)@
--
-- * etc.
--
-- Note that the intrinsic can vary both by the size of the vector type (@4@,
-- @2@, etc.) and the size of the integer type used as the vector element type
-- (@i32@, @i64@, etc.) Therefore, the @fn@ argument that this function accepts
-- is parameterized by both the vector size (@vecSz@) and the integer size
-- (@intSz@).
polymorphic1_vec_llvm_override :: forall p sym ext arch wptr.
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  String ->
  (forall vecSz intSz.
    (1 <= intSz) =>
    NatRepr vecSz ->
    NatRepr intSz ->
    SomeLLVMOverride p sym ext) ->
  OverrideTemplate p sym ext arch
polymorphic1_vec_llvm_override :: forall p sym ext (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
String
-> (forall (vecSz :: Natural) (intSz :: Natural).
    (1 <= intSz) =>
    NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym ext)
-> OverrideTemplate p sym ext arch
polymorphic1_vec_llvm_override String
prefix forall (vecSz :: Natural) (intSz :: Natural).
(1 <= intSz) =>
NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym ext
fn =
  TemplateMatcher
-> MakeOverride p sym ext arch -> OverrideTemplate p sym ext arch
forall p sym ext (arch :: LLVMArch).
TemplateMatcher
-> MakeOverride p sym ext arch -> OverrideTemplate p sym ext arch
OverrideTemplate (String -> TemplateMatcher
Match.PrefixMatch String
prefix) (String
-> (forall (vecSz :: Natural) (intSz :: Natural).
    (1 <= intSz) =>
    NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym ext)
-> MakeOverride p sym ext arch
forall p sym ext (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
String
-> (forall (vecSz :: Natural) (intSz :: Natural).
    (1 <= intSz) =>
    NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym ext)
-> MakeOverride p sym ext arch
register_1arg_vec_polymorphic_override String
prefix NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym ext
forall (vecSz :: Natural) (intSz :: Natural).
(1 <= intSz) =>
NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym ext
fn)

-- | Create an 'OverrideTemplate' for an intrinsic in the @llvm.{s,u}cmp.*@
-- family. These can be instantiated at multiple types, including:
--
-- * @i2 \@llvm.scmp.i2.i32(i32, i32)@

-- * @i8 \@llvm.scmp.i8.i8(i8, i8)@
--
-- * etc.
--
-- Note that the argument and result types are allowed to be different, so the
-- @fn@ argument is parameterized by two separate 'NatRepr's.
polymorphic_cmp_llvm_override :: forall p sym ext arch wptr.
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  String ->
  (forall argSz resSz.
    (1 <= argSz, 2 <= resSz) =>
    NatRepr argSz ->
    NatRepr resSz ->
    SomeLLVMOverride p sym ext) ->
  OverrideTemplate p sym ext arch
polymorphic_cmp_llvm_override :: forall p sym ext (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
String
-> (forall (argSz :: Natural) (resSz :: Natural).
    (1 <= argSz, 2 <= resSz) =>
    NatRepr argSz -> NatRepr resSz -> SomeLLVMOverride p sym ext)
-> OverrideTemplate p sym ext arch
polymorphic_cmp_llvm_override String
prefix forall (argSz :: Natural) (resSz :: Natural).
(1 <= argSz, 2 <= resSz) =>
NatRepr argSz -> NatRepr resSz -> SomeLLVMOverride p sym ext
fn =
  TemplateMatcher
-> MakeOverride p sym ext arch -> OverrideTemplate p sym ext arch
forall p sym ext (arch :: LLVMArch).
TemplateMatcher
-> MakeOverride p sym ext arch -> OverrideTemplate p sym ext arch
OverrideTemplate (String -> TemplateMatcher
Match.PrefixMatch String
prefix) (String
-> (forall (argSz :: Natural) (resSz :: Natural).
    (1 <= argSz, 2 <= resSz) =>
    NatRepr argSz -> NatRepr resSz -> SomeLLVMOverride p sym ext)
-> MakeOverride p sym ext arch
forall p sym ext (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
String
-> (forall (argSz :: Natural) (resSz :: Natural).
    (1 <= argSz, 2 <= resSz) =>
    NatRepr argSz -> NatRepr resSz -> SomeLLVMOverride p sym ext)
-> MakeOverride p sym ext arch
register_cmp_polymorphic_override String
prefix NatRepr argSz -> NatRepr resSz -> SomeLLVMOverride p sym ext
forall (argSz :: Natural) (resSz :: Natural).
(1 <= argSz, 2 <= resSz) =>
NatRepr argSz -> NatRepr resSz -> SomeLLVMOverride p sym ext
fn)

register_1arg_polymorphic_override :: forall p sym ext arch wptr.
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  String ->
  (forall w. (1 <= w) => NatRepr w -> SomeLLVMOverride p sym ext) ->
  MakeOverride p sym ext arch
register_1arg_polymorphic_override :: forall p sym ext (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
String
-> (forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> SomeLLVMOverride p sym ext)
-> MakeOverride p sym ext arch
register_1arg_polymorphic_override String
prefix forall (w :: Natural).
(1 <= w) =>
NatRepr w -> SomeLLVMOverride p sym ext
overrideFn =
  (SomeDeclare
 -> Maybe DecodedName
 -> LLVMContext arch
 -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
forall p sym ext (arch :: LLVMArch).
(SomeDeclare
 -> Maybe DecodedName
 -> LLVMContext arch
 -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
MakeOverride ((SomeDeclare
  -> Maybe DecodedName
  -> LLVMContext arch
  -> Maybe (SomeLLVMOverride p sym ext))
 -> MakeOverride p sym ext arch)
-> (SomeDeclare
    -> Maybe DecodedName
    -> LLVMContext arch
    -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
forall a b. (a -> b) -> a -> b
$ \(Decl.SomeDeclare (Decl.Declare{ decName :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName = L.Symbol String
nm })) Maybe DecodedName
_ LLVMContext arch
_ ->
    case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
List.stripPrefix String
prefix String
nm of
      Just (Char
'.':Char
'i': (ReadS Natural
forall a. (Eq a, Num a) => ReadS a
readDec -> (Natural
sz,[]):[(Natural, String)]
_))
        | Some NatRepr x
w <- Natural -> Some NatRepr
mkNatRepr Natural
sz
        , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
w
        -> SomeLLVMOverride p sym ext -> Maybe (SomeLLVMOverride p sym ext)
forall a. a -> Maybe a
Just (NatRepr x -> SomeLLVMOverride p sym ext
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> SomeLLVMOverride p sym ext
overrideFn NatRepr x
w)
      Maybe String
_ -> Maybe (SomeLLVMOverride p sym ext)
forall a. Maybe a
Nothing

-- | Register a polymorphic LLVM override involving a vector type. (See the
-- Haddocks for 'polymorphic1_vec_llvm_override' for details on what this
-- means.) This function is responsible for parsing the suffix in the
-- intrinsic's name, which encodes the sizes of the vector and integer types.
-- As some examples:
--
-- * @.v4i32@ (vector size @4@, integer size @32@)
--
-- * @.v2i64@ (vector size @2@, integer size @64@)
register_1arg_vec_polymorphic_override :: forall p sym ext arch wptr.
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  String ->
  (forall vecSz intSz.
    (1 <= intSz) =>
    NatRepr vecSz ->
    NatRepr intSz ->
    SomeLLVMOverride p sym ext) ->
  MakeOverride p sym ext arch
register_1arg_vec_polymorphic_override :: forall p sym ext (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
String
-> (forall (vecSz :: Natural) (intSz :: Natural).
    (1 <= intSz) =>
    NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym ext)
-> MakeOverride p sym ext arch
register_1arg_vec_polymorphic_override String
prefix forall (vecSz :: Natural) (intSz :: Natural).
(1 <= intSz) =>
NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym ext
overrideFn =
  (SomeDeclare
 -> Maybe DecodedName
 -> LLVMContext arch
 -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
forall p sym ext (arch :: LLVMArch).
(SomeDeclare
 -> Maybe DecodedName
 -> LLVMContext arch
 -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
MakeOverride ((SomeDeclare
  -> Maybe DecodedName
  -> LLVMContext arch
  -> Maybe (SomeLLVMOverride p sym ext))
 -> MakeOverride p sym ext arch)
-> (SomeDeclare
    -> Maybe DecodedName
    -> LLVMContext arch
    -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
forall a b. (a -> b) -> a -> b
$ \(Decl.SomeDeclare (Decl.Declare{ decName :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName = L.Symbol String
nm })) Maybe DecodedName
_ LLVMContext arch
_ ->
    case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
List.stripPrefix String
prefix String
nm of
      Just (Char
'.':Char
'v':String
suffix1)
        | (String
vecSzStr, Char
'i':String
intSzStr) <- (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'i') String
suffix1
        , (Natural
vecSzNat, []):[(Natural, String)]
_ <- ReadS Natural
forall a. (Eq a, Num a) => ReadS a
readDec String
vecSzStr
        , (Natural
intSzNat, []):[(Natural, String)]
_ <- ReadS Natural
forall a. (Eq a, Num a) => ReadS a
readDec String
intSzStr
        , Some NatRepr x
vecSzRepr <- Natural -> Some NatRepr
mkNatRepr Natural
vecSzNat
        , Some NatRepr x
intSzRepr <- Natural -> Some NatRepr
mkNatRepr Natural
intSzNat
        , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
intSzRepr
        -> SomeLLVMOverride p sym ext -> Maybe (SomeLLVMOverride p sym ext)
forall a. a -> Maybe a
Just (NatRepr x -> NatRepr x -> SomeLLVMOverride p sym ext
forall (vecSz :: Natural) (intSz :: Natural).
(1 <= intSz) =>
NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym ext
overrideFn NatRepr x
vecSzRepr NatRepr x
intSzRepr)
      Maybe String
_ -> Maybe (SomeLLVMOverride p sym ext)
forall a. Maybe a
Nothing

-- | Register an override for an intrinsic in the @llvm.{s,u}cmp.*@ family.
-- (See the Haddocks for 'polymorphic_cmp_llvm_override' for details on what
-- this means.) This function is responsible for parsing the suffixes in the
-- intrinsic's name, which encodes the sizes of the argument and result types.
-- As some examples:
--
-- * @.i2.i32@ (argument size @32@, result size @2@)
--
-- * @.i8.i64@ (argument size @64@, result size @8@)
register_cmp_polymorphic_override :: forall p sym ext arch wptr.
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  String ->
  (forall argSz resSz.
    (1 <= argSz, 2 <= resSz) =>
    NatRepr argSz ->
    NatRepr resSz ->
    SomeLLVMOverride p sym ext) ->
  MakeOverride p sym ext arch
register_cmp_polymorphic_override :: forall p sym ext (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
String
-> (forall (argSz :: Natural) (resSz :: Natural).
    (1 <= argSz, 2 <= resSz) =>
    NatRepr argSz -> NatRepr resSz -> SomeLLVMOverride p sym ext)
-> MakeOverride p sym ext arch
register_cmp_polymorphic_override String
prefix forall (argSz :: Natural) (resSz :: Natural).
(1 <= argSz, 2 <= resSz) =>
NatRepr argSz -> NatRepr resSz -> SomeLLVMOverride p sym ext
overrideFn =
  (SomeDeclare
 -> Maybe DecodedName
 -> LLVMContext arch
 -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
forall p sym ext (arch :: LLVMArch).
(SomeDeclare
 -> Maybe DecodedName
 -> LLVMContext arch
 -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
MakeOverride ((SomeDeclare
  -> Maybe DecodedName
  -> LLVMContext arch
  -> Maybe (SomeLLVMOverride p sym ext))
 -> MakeOverride p sym ext arch)
-> (SomeDeclare
    -> Maybe DecodedName
    -> LLVMContext arch
    -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
forall a b. (a -> b) -> a -> b
$ \(Decl.SomeDeclare (Decl.Declare{ decName :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName = L.Symbol String
nm })) Maybe DecodedName
_ LLVMContext arch
_ ->
    case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
List.stripPrefix String
prefix String
nm of
      Just (Char
'.':Char
'i': (ReadS Natural
forall a. (Eq a, Num a) => ReadS a
readDec -> (Natural
resSz,String
rest):[(Natural, String)]
_))
        | Char
'.':Char
'i': (ReadS Natural
forall a. (Eq a, Num a) => ReadS a
readDec -> (Natural
argSz,[]):[(Natural, String)]
_) <- String
rest
        , Some NatRepr x
argW <- Natural -> Some NatRepr
mkNatRepr Natural
argSz
        , Some NatRepr x
resW <- Natural -> Some NatRepr
mkNatRepr Natural
resSz
        , Just LeqProof 1 x
LeqProof <- NatRepr 1 -> NatRepr x -> Maybe (LeqProof 1 x)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) NatRepr x
argW
        , Just LeqProof 2 x
LeqProof <- NatRepr 2 -> NatRepr x -> Maybe (LeqProof 2 x)
forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @2) NatRepr x
resW
        -> SomeLLVMOverride p sym ext -> Maybe (SomeLLVMOverride p sym ext)
forall a. a -> Maybe a
Just (NatRepr x -> NatRepr x -> SomeLLVMOverride p sym ext
forall (argSz :: Natural) (resSz :: Natural).
(1 <= argSz, 2 <= resSz) =>
NatRepr argSz -> NatRepr resSz -> SomeLLVMOverride p sym ext
overrideFn NatRepr x
argW NatRepr x
resW)
      Maybe String
_ -> Maybe (SomeLLVMOverride p sym ext)
forall a. Maybe a
Nothing

basic_llvm_override :: forall p args ret sym ext arch wptr.
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
  LLVMOverride p sym ext args ret ->
  OverrideTemplate p sym ext arch
basic_llvm_override :: forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym ext
       (arch :: LLVMArch) (wptr :: Natural).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
LLVMOverride p sym ext args ret -> OverrideTemplate p sym ext arch
basic_llvm_override LLVMOverride p sym ext args ret
ovr = TemplateMatcher
-> MakeOverride p sym ext arch -> OverrideTemplate p sym ext arch
forall p sym ext (arch :: LLVMArch).
TemplateMatcher
-> MakeOverride p sym ext arch -> OverrideTemplate p sym ext arch
OverrideTemplate TemplateMatcher
matcher MakeOverride p sym ext arch
regOvr
  where
    L.Symbol String
ovrNm = LLVMOverride p sym ext args ret -> Symbol
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Symbol
llvmOvSymbol LLVMOverride p sym ext args ret
ovr
    isDarwin :: Bool
isDarwin = String
Info.os String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"darwin"

    matcher :: Match.TemplateMatcher
    matcher :: TemplateMatcher
matcher | Bool
isDarwin  = String -> TemplateMatcher
Match.DarwinAliasMatch String
ovrNm
            | Bool
otherwise = String -> TemplateMatcher
Match.ExactMatch String
ovrNm

    regOvr :: MakeOverride p sym ext arch
    regOvr :: MakeOverride p sym ext arch
regOvr = do
      (SomeDeclare
 -> Maybe DecodedName
 -> LLVMContext arch
 -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
forall p sym ext (arch :: LLVMArch).
(SomeDeclare
 -> Maybe DecodedName
 -> LLVMContext arch
 -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
MakeOverride ((SomeDeclare
  -> Maybe DecodedName
  -> LLVMContext arch
  -> Maybe (SomeLLVMOverride p sym ext))
 -> MakeOverride p sym ext arch)
-> (SomeDeclare
    -> Maybe DecodedName
    -> LLVMContext arch
    -> Maybe (SomeLLVMOverride p sym ext))
-> MakeOverride p sym ext arch
forall a b. (a -> b) -> a -> b
$ \(Decl.SomeDeclare Declare args ret
requestedDecl) Maybe DecodedName
_ LLVMContext arch
_ -> do
        let L.Symbol String
requestedNm = Declare args ret -> Symbol
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName Declare args ret
requestedDecl
        -- If we are on Darwin and the function name contains Darwin-specific
        -- prefixes or suffixes, change the name of the override to the
        -- name containing prefixes/suffixes. See Note [Darwin aliases] in
        -- Lang.Crucible.LLVM.Intrinsics.Match for an explanation of why we
        -- do this.
        let ovr' :: LLVMOverride p sym ext args ret
ovr' | Bool
isDarwin
                 , String
ovrNm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String -> String
Match.stripDarwinAliases String
requestedNm
                 = let decl :: Declare args ret
decl = (LLVMOverride p sym ext args ret -> Declare args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Declare args ret
llvmOvDecl LLVMOverride p sym ext args ret
ovr) { Decl.decName = L.Symbol requestedNm } in
                   LLVMOverride p sym ext args ret
ovr { llvmOvDecl = decl }

                 | Bool
otherwise
                 = LLVMOverride p sym ext args ret
ovr
        SomeLLVMOverride p sym ext -> Maybe (SomeLLVMOverride p sym ext)
forall a. a -> Maybe a
Just (LLVMOverride p sym ext args ret -> 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 args ret
ovr')

-- | Check that the requested declaration matches the provided declaration. In
-- this context, \"matching\" means that both declarations have identical names,
-- as well as equal argument and result types. When checking types for equality,
-- we consider opaque pointer types to be equal to non-opaque pointer types so
-- that we do not have to define quite so many overrides with different
-- combinations of pointer types.
isMatchingDeclaration ::
  Decl.Declare args' ret' {- ^ Requested declaration -} ->
  LLVMOverride p sym ext args ret ->
  Bool
isMatchingDeclaration :: forall (args' :: Ctx CrucibleType) (ret' :: CrucibleType) p sym ext
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args' ret' -> LLVMOverride p sym ext args ret -> Bool
isMatchingDeclaration Declare args' ret'
requested LLVMOverride p sym ext args ret
provided =
  let args :: Assignment TypeRepr args'
args = Declare args' ret' -> Assignment TypeRepr args'
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Assignment TypeRepr args
Decl.decArgs Declare args' ret'
requested in
  let ret :: TypeRepr ret'
ret = Declare args' ret' -> TypeRepr ret'
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> TypeRepr ret
Decl.decRet Declare args' ret'
requested in
  [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
and
  [ Declare args' ret' -> Symbol
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName Declare args' ret'
requested Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== LLVMOverride p sym ext args ret -> Symbol
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Symbol
llvmOvSymbol LLVMOverride p sym ext args ret
provided
  , Assignment TypeRepr args' -> Assignment TypeRepr args -> Bool
forall (ctx1 :: Ctx CrucibleType) (ctx2 :: Ctx CrucibleType).
Assignment TypeRepr ctx1 -> Assignment TypeRepr ctx2 -> Bool
matchingArgList Assignment TypeRepr args'
args (LLVMOverride p sym ext args ret -> Assignment TypeRepr args
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> CtxRepr args
llvmOvArgs LLVMOverride p sym ext args ret
provided)
  , Maybe (ret' :~: ret) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (TypeRepr ret' -> TypeRepr ret -> Maybe (ret' :~: ret)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr ret'
ret (LLVMOverride p sym ext args ret -> TypeRepr ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> TypeRepr ret
llvmOvRet LLVMOverride p sym ext args ret
provided))
  ]

  where
  matchingArgList ::
    Ctx.Assignment TypeRepr ctx1 ->
    Ctx.Assignment TypeRepr ctx2 ->
    Bool
  -- Ignore varargs as long as the rest of the arguments match (VectorRepr
  -- AnyRepr is how Crucible-LLVM represents varargs).
  matchingArgList :: forall (ctx1 :: Ctx CrucibleType) (ctx2 :: Ctx CrucibleType).
Assignment TypeRepr ctx1 -> Assignment TypeRepr ctx2 -> Bool
matchingArgList (Assignment TypeRepr ctx
rest Ctx.:> VectorRepr TypeRepr tp1
AnyRepr) Assignment TypeRepr ctx2
ys = Assignment TypeRepr ctx -> Assignment TypeRepr ctx2 -> Bool
forall (ctx1 :: Ctx CrucibleType) (ctx2 :: Ctx CrucibleType).
Assignment TypeRepr ctx1 -> Assignment TypeRepr ctx2 -> Bool
matchingArgList Assignment TypeRepr ctx
rest Assignment TypeRepr ctx2
ys
  matchingArgList Assignment TypeRepr ctx1
xs (Assignment TypeRepr ctx
rest Ctx.:> VectorRepr TypeRepr tp1
AnyRepr) = Assignment TypeRepr ctx1 -> Assignment TypeRepr ctx -> Bool
forall (ctx1 :: Ctx CrucibleType) (ctx2 :: Ctx CrucibleType).
Assignment TypeRepr ctx1 -> Assignment TypeRepr ctx2 -> Bool
matchingArgList Assignment TypeRepr ctx1
xs Assignment TypeRepr ctx
rest
  matchingArgList Assignment TypeRepr ctx1
xs Assignment TypeRepr ctx2
ys = Maybe (ctx1 :~: ctx2) -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (Assignment TypeRepr ctx1
-> Assignment TypeRepr ctx2 -> Maybe (ctx1 :~: ctx2)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
Assignment TypeRepr a -> Assignment TypeRepr b -> Maybe (a :~: b)
testEquality Assignment TypeRepr ctx1
xs Assignment TypeRepr ctx2
ys)

register_llvm_override ::
  forall p args ret args' ret' sym ext arch wptr rtp l a.
  (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
  LLVMOverride p sym ext args ret ->
  Decl.Declare args' ret' ->
  LLVMContext arch ->
  OverrideSim p sym ext rtp l a ()
register_llvm_override :: forall p (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (args' :: Ctx CrucibleType) (ret' :: CrucibleType) sym ext
       (arch :: LLVMArch) (wptr :: Natural) rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
LLVMOverride p sym ext args ret
-> Declare args' ret'
-> LLVMContext arch
-> OverrideSim p sym ext rtp l a ()
register_llvm_override LLVMOverride p sym ext args ret
llvmOverride Declare args' ret'
requestedDecl LLVMContext arch
llvmctx = do
  let ?lc = LLVMContext arch
llvmctxLLVMContext arch
-> Getting TypeContext (LLVMContext arch) TypeContext
-> TypeContext
forall s a. s -> Getting a s a -> a
^.Getting TypeContext (LLVMContext arch) TypeContext
forall (arch :: LLVMArch) (f :: Type -> Type).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx
  if Bool -> Bool
not (Declare args' ret' -> LLVMOverride p sym ext args ret -> Bool
forall (args' :: Ctx CrucibleType) (ret' :: CrucibleType) p sym ext
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args' ret' -> LLVMOverride p sym ext args ret -> Bool
isMatchingDeclaration Declare args' ret'
requestedDecl LLVMOverride p sym ext args ret
llvmOverride) then
    do Bool
-> OverrideSim p sym ext rtp l a ()
-> OverrideSim p sym ext rtp l a ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Declare args' ret' -> Symbol
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName Declare args' ret'
requestedDecl Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== LLVMOverride p sym ext args ret -> Symbol
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Symbol
llvmOvSymbol LLVMOverride p sym ext args ret
llvmOverride) (OverrideSim p sym ext rtp l a ()
 -> OverrideSim p sym ext rtp l a ())
-> OverrideSim p sym ext rtp l a ()
-> OverrideSim p sym ext rtp l a ()
forall a b. (a -> b) -> a -> b
$
         do Int -> String -> IO ()
logFn <- OverrideSim p sym ext rtp l a (Int -> String -> IO ())
forall (m :: Type -> Type).
MonadVerbosity m =>
m (Int -> String -> IO ())
getLogFunction
            IO () -> OverrideSim p sym ext rtp l a ()
forall a. IO a -> OverrideSim p sym ext rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO () -> OverrideSim p sym ext rtp l a ())
-> IO () -> OverrideSim p sym ext rtp l a ()
forall a b. (a -> b) -> a -> b
$ Int -> String -> IO ()
logFn Int
3 (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
              [ String
"Mismatched declaration signatures"
              , String
" *** requested: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Declare args' ret' -> String
forall a. Show a => a -> String
show Declare args' ret'
requestedDecl
              , String
" *** found args: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CtxRepr args -> String
forall a. Show a => a -> String
show (LLVMOverride p sym ext args ret -> CtxRepr args
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> CtxRepr args
llvmOvArgs LLVMOverride p sym ext args ret
llvmOverride)
              , String
" *** found ret: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRepr ret -> String
forall a. Show a => a -> String
show (LLVMOverride p sym ext args ret -> TypeRepr ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> TypeRepr ret
llvmOvRet LLVMOverride p sym ext args ret
llvmOverride)
              ]
  else LLVMContext arch
-> LLVMOverride p sym ext args ret
-> OverrideSim p sym ext rtp l a ()
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym ext
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
LLVMContext arch
-> LLVMOverride p sym ext args ret
-> OverrideSim p sym ext rtp l a ()
do_register_llvm_override LLVMContext arch
llvmctx LLVMOverride p sym ext args ret
llvmOverride

-- | Low-level function to register LLVM overrides.
--
-- Creates and binds a function handle, and also binds the function to the
-- global function allocation in the LLVM memory.
--
-- Useful when you don\'t have access to a full LLVM AST, e.g., when parsing
-- Crucible CFGs written in crucible-syntax. For more usual cases, use
-- 'Lang.Crucible.LLVM.Intrinsics.register_llvm_overrides'.
do_register_llvm_override :: forall p args ret sym ext arch wptr l a rtp.
  (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
  LLVMContext arch ->
  LLVMOverride p sym ext args ret ->
  OverrideSim p sym ext rtp l a ()
do_register_llvm_override :: forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym ext
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
LLVMContext arch
-> LLVMOverride p sym ext args ret
-> OverrideSim p sym ext rtp l a ()
do_register_llvm_override LLVMContext arch
llvmctx LLVMOverride p sym ext args ret
llvmOverride = do
  let nm :: Symbol
nm@(L.Symbol String
str_nm) = LLVMOverride p sym ext args ret -> Symbol
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Symbol
llvmOvSymbol LLVMOverride p sym ext args ret
llvmOverride
  let fnm :: FunctionName
fnm  = Text -> FunctionName
functionNameFromText (String -> Text
Text.pack String
str_nm)

  let mvar :: GlobalVar Mem
mvar = LLVMContext arch -> GlobalVar Mem
forall (arch :: LLVMArch). LLVMContext arch -> GlobalVar Mem
llvmMemVar LLVMContext arch
llvmctx
  let ?lc = LLVMContext arch
llvmctxLLVMContext arch
-> Getting TypeContext (LLVMContext arch) TypeContext
-> TypeContext
forall s a. s -> Getting a s a -> a
^.Getting TypeContext (LLVMContext arch) TypeContext
forall (arch :: LLVMArch) (f :: Type -> Type).
Functor f =>
(TypeContext -> f TypeContext)
-> LLVMContext arch -> f (LLVMContext arch)
llvmTypeCtx

  let typedOv :: TypedOverride p sym ext args ret
typedOv = GlobalVar Mem
-> LLVMOverride p sym ext args ret
-> TypedOverride p sym ext args ret
forall sym p ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym) =>
GlobalVar Mem
-> LLVMOverride p sym ext args ret
-> TypedOverride p sym ext args ret
llvmOverrideToTypedOverride GlobalVar Mem
mvar LLVMOverride p sym ext args ret
llvmOverride
  let o :: Override p sym ext args ret
o = FunctionName
-> TypedOverride p sym ext args ret -> Override p sym ext args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
FunctionName
-> TypedOverride p sym ext args ret -> Override p sym ext args ret
runTypedOverride FunctionName
fnm TypedOverride p sym ext args ret
typedOv
  let args :: CtxRepr args
args = TypedOverride p sym ext args ret -> CtxRepr args
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
TypedOverride p sym ext args ret -> CtxRepr args
typedOverrideArgs TypedOverride p sym ext args ret
typedOv
  let ret :: TypeRepr ret
ret = TypedOverride p sym ext args ret -> TypeRepr ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
TypedOverride p sym ext args ret -> TypeRepr ret
typedOverrideRet TypedOverride p sym ext args ret
typedOv
  GlobalVar Mem
-> Symbol
-> CtxRepr args
-> TypeRepr ret
-> FnState p sym ext args ret
-> OverrideSim p sym ext rtp l a ()
forall sym (wptr :: Natural) (args :: Ctx CrucibleType)
       (ret :: CrucibleType) p ext rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasPtrWidth wptr) =>
GlobalVar Mem
-> Symbol
-> Assignment TypeRepr args
-> TypeRepr ret
-> FnState p sym ext args ret
-> OverrideSim p sym ext rtp l a ()
bindLLVMFunc GlobalVar Mem
mvar Symbol
nm CtxRepr args
args TypeRepr ret
ret (Override p sym ext args ret -> FnState p sym ext args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Override p sym ext args ret -> FnState p sym ext args ret
UseOverride Override p sym ext args ret
o)

-- | Create an allocation for an override and register it.
--
-- Useful when registering an override for a function in an LLVM memory that
-- wasn't initialized with the functions in "Lang.Crucible.LLVM.Globals", e.g.,
-- when parsing Crucible CFGs written in crucible-syntax. For more usual cases,
-- use 'Lang.Crucible.LLVM.Intrinsics.register_llvm_overrides'.
--
-- c.f. 'Lang.Crucible.LLVM.Globals.allocLLVMFunPtr'
alloc_and_register_override ::
  (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) =>
  bak ->
  LLVMContext arch ->
  LLVMOverride p sym LLVM args ret ->
  -- | Aliases
  [L.Symbol] ->
  OverrideSim p sym LLVM rtp l a ()
alloc_and_register_override :: forall sym bak (wptr :: Natural) (arch :: LLVMArch) p
       (args :: Ctx CrucibleType) (ret :: CrucibleType) rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> LLVMContext arch
-> LLVMOverride p sym LLVM args ret
-> [Symbol]
-> OverrideSim p sym LLVM rtp l a ()
alloc_and_register_override bak
bak LLVMContext arch
llvmctx LLVMOverride p sym LLVM args ret
llvmOverride [Symbol]
aliases = do
  let symb :: Symbol
symb@(L.Symbol String
nm) = LLVMOverride p sym LLVM args ret -> Symbol
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> Symbol
llvmOvSymbol LLVMOverride p sym LLVM args ret
llvmOverride
  let mvar :: GlobalVar Mem
mvar = LLVMContext arch -> GlobalVar Mem
forall (arch :: LLVMArch). LLVMContext arch -> GlobalVar Mem
llvmMemVar LLVMContext arch
llvmctx
  MemImpl sym
mem <- GlobalVar Mem -> OverrideSim p sym LLVM rtp l a (RegValue sym Mem)
forall sym (tp :: CrucibleType) p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
IsSymInterface sym =>
GlobalVar tp
-> OverrideSim p sym ext rtp args ret (RegValue sym tp)
readGlobal GlobalVar Mem
mvar
  (LLVMPointer sym wptr
_ptr, MemImpl sym
mem') <- IO (LLVMPointer sym wptr, MemImpl sym)
-> OverrideSim
     p sym LLVM rtp l a (LLVMPointer sym wptr, MemImpl sym)
forall a. IO a -> OverrideSim p sym LLVM rtp l a a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (bak
-> MemImpl sym
-> String
-> Symbol
-> [Symbol]
-> IO (LLVMPtr sym wptr, MemImpl sym)
forall sym bak (wptr :: Natural).
(IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym,
 ?memOpts::MemOptions) =>
bak
-> MemImpl sym
-> String
-> Symbol
-> [Symbol]
-> IO (LLVMPtr sym wptr, MemImpl sym)
registerFunPtr bak
bak MemImpl sym
mem String
nm Symbol
symb [Symbol]
aliases)
  GlobalVar Mem
-> RegValue sym Mem -> OverrideSim p sym LLVM rtp l a ()
forall (tp :: CrucibleType) sym p ext rtp
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
GlobalVar tp
-> RegValue sym tp -> OverrideSim p sym ext rtp args ret ()
writeGlobal GlobalVar Mem
mvar RegValue sym Mem
MemImpl sym
mem'
  LLVMContext arch
-> LLVMOverride p sym LLVM args ret
-> OverrideSim p sym LLVM rtp l a ()
forall p (args :: Ctx CrucibleType) (ret :: CrucibleType) sym ext
       (arch :: LLVMArch) (wptr :: Natural) (l :: Ctx CrucibleType)
       (a :: CrucibleType) rtp.
(IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
LLVMContext arch
-> LLVMOverride p sym ext args ret
-> OverrideSim p sym ext rtp l a ()
do_register_llvm_override LLVMContext arch
llvmctx LLVMOverride p sym LLVM args ret
llvmOverride