-- |
-- Module           : Lang.Crucible.LLVM.Intrinsics
-- Description      : Override definitions for LLVM intrinsic and basic
--                    library functions
-- Copyright        : (c) Galois, Inc 2015-2016
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}

module Lang.Crucible.LLVM.Intrinsics
( LLVM
, llvmIntrinsicTypes
, LLVMOverride(..)

, register_llvm_overrides
, register_llvm_overrides_
, llvmDeclToFunHandleRepr

, module Lang.Crucible.LLVM.Intrinsics.Common
, module Lang.Crucible.LLVM.Intrinsics.Options
, module Lang.Crucible.LLVM.Intrinsics.Match
) where

import           Control.Lens hiding (op, (:>), Empty)
import           Control.Monad (forM)
import           Data.Maybe (catMaybes)
import qualified Text.LLVM.AST as L

import qualified ABI.Itanium as ABI
import qualified Data.Parameterized.Map as MapF

import           Lang.Crucible.Backend
import           Lang.Crucible.Types
import           Lang.Crucible.Simulator.Intrinsics
import           Lang.Crucible.Simulator.OverrideSim

import           Lang.Crucible.LLVM.Extension (ArchWidth, LLVM)
import           Lang.Crucible.LLVM.MemModel
import           Lang.Crucible.LLVM.Translation.Monad
import           Lang.Crucible.LLVM.Translation.Types
import           Lang.Crucible.LLVM.TypeContext (TypeContext)

import           Lang.Crucible.LLVM.Intrinsics.Common
import qualified Lang.Crucible.LLVM.Intrinsics.LLVM as LLVM
import qualified Lang.Crucible.LLVM.Intrinsics.Libc as Libc
import qualified Lang.Crucible.LLVM.Intrinsics.Libcxx as Libcxx
import           Lang.Crucible.LLVM.Intrinsics.Match
import           Lang.Crucible.LLVM.Intrinsics.Options

llvmIntrinsicTypes :: IsSymInterface sym => IntrinsicTypes sym
llvmIntrinsicTypes :: forall sym. IsSymInterface sym => IntrinsicTypes sym
llvmIntrinsicTypes =
   SymbolRepr "LLVM_memory"
-> IntrinsicMuxFn sym "LLVM_memory"
-> MapF SymbolRepr (IntrinsicMuxFn sym)
-> MapF SymbolRepr (IntrinsicMuxFn sym)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert (SymbolRepr "LLVM_memory"
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol :: SymbolRepr "LLVM_memory") IntrinsicMuxFn sym "LLVM_memory"
forall sym (nm :: Symbol).
IntrinsicClass sym nm =>
IntrinsicMuxFn sym nm
IntrinsicMuxFn (MapF SymbolRepr (IntrinsicMuxFn sym)
 -> MapF SymbolRepr (IntrinsicMuxFn sym))
-> MapF SymbolRepr (IntrinsicMuxFn sym)
-> MapF SymbolRepr (IntrinsicMuxFn sym)
forall a b. (a -> b) -> a -> b
$
   SymbolRepr "LLVM_pointer"
-> IntrinsicMuxFn sym "LLVM_pointer"
-> MapF SymbolRepr (IntrinsicMuxFn sym)
-> MapF SymbolRepr (IntrinsicMuxFn sym)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert (SymbolRepr "LLVM_pointer"
forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol :: SymbolRepr "LLVM_pointer") IntrinsicMuxFn sym "LLVM_pointer"
forall sym (nm :: Symbol).
IntrinsicClass sym nm =>
IntrinsicMuxFn sym nm
IntrinsicMuxFn (MapF SymbolRepr (IntrinsicMuxFn sym)
 -> MapF SymbolRepr (IntrinsicMuxFn sym))
-> MapF SymbolRepr (IntrinsicMuxFn sym)
-> MapF SymbolRepr (IntrinsicMuxFn sym)
forall a b. (a -> b) -> a -> b
$
   MapF SymbolRepr (IntrinsicMuxFn sym)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty

-- | Match two sets of 'OverrideTemplate's against the @declare@s and @define@s
-- in a 'L.Module', registering all the overrides that apply and returning them
-- as a list.
register_llvm_overrides ::
  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
  , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
  L.Module ->
  [OverrideTemplate p sym LLVM arch] {- ^ Additional \"define\" overrides -} ->
  [OverrideTemplate p sym LLVM arch] {- ^ Additional \"declare\" overrides -} ->
  LLVMContext arch ->
  -- | Applied (@define@ overrides, @declare@ overrides)
  OverrideSim p sym LLVM rtp l a ([SomeLLVMOverride p sym LLVM], [SomeLLVMOverride p sym LLVM])
register_llvm_overrides :: forall sym (wptr :: Natural) (arch :: LLVMArch) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch, ?intrinsicsOpts::IntrinsicsOptions,
 ?memOpts::MemOptions) =>
Module
-> [OverrideTemplate p sym LLVM arch]
-> [OverrideTemplate p sym LLVM arch]
-> LLVMContext arch
-> OverrideSim
     p
     sym
     LLVM
     rtp
     l
     a
     ([SomeLLVMOverride p sym LLVM], [SomeLLVMOverride p sym LLVM])
register_llvm_overrides Module
llvmModule [OverrideTemplate p sym LLVM arch]
defineOvrs [OverrideTemplate p sym LLVM arch]
declareOvrs LLVMContext arch
llvmctx =
  do [SomeLLVMOverride p sym LLVM]
defOvs <- Module
-> [OverrideTemplate p sym LLVM arch]
-> LLVMContext arch
-> OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
forall sym (wptr :: Natural) (arch :: LLVMArch) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch) =>
Module
-> [OverrideTemplate p sym LLVM arch]
-> LLVMContext arch
-> OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
register_llvm_define_overrides Module
llvmModule [OverrideTemplate p sym LLVM arch]
defineOvrs LLVMContext arch
llvmctx
     [SomeLLVMOverride p sym LLVM]
declOvs <- Module
-> [OverrideTemplate p sym LLVM arch]
-> LLVMContext arch
-> OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
forall sym (wptr :: Natural) (arch :: LLVMArch) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch, ?intrinsicsOpts::IntrinsicsOptions,
 ?memOpts::MemOptions) =>
Module
-> [OverrideTemplate p sym LLVM arch]
-> LLVMContext arch
-> OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
register_llvm_declare_overrides Module
llvmModule [OverrideTemplate p sym LLVM arch]
declareOvrs LLVMContext arch
llvmctx
     ([SomeLLVMOverride p sym LLVM], [SomeLLVMOverride p sym LLVM])
-> OverrideSim
     p
     sym
     LLVM
     rtp
     l
     a
     ([SomeLLVMOverride p sym LLVM], [SomeLLVMOverride p sym LLVM])
forall a. a -> OverrideSim p sym LLVM rtp l a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([SomeLLVMOverride p sym LLVM]
defOvs,  [SomeLLVMOverride p sym LLVM]
declOvs)

-- | Filter the initial list of templates to only those that could
-- possibly match the given declaration based on straightforward,
-- relatively cheap string tests on the name of the declaration.
--
-- Any remaining templates will then examine the declaration in
-- more detail, including examining function arguments
-- and the structure of C++ demangled names to extract more information.
filterTemplates ::
  [OverrideTemplate p sym ext arch] ->
  L.Declare ->
  [OverrideTemplate p sym ext arch]
filterTemplates :: forall p sym ext (arch :: LLVMArch).
[OverrideTemplate p sym ext arch]
-> Declare -> [OverrideTemplate p sym ext arch]
filterTemplates [OverrideTemplate p sym ext arch]
ts Declare
decl = (OverrideTemplate p sym ext arch -> Bool)
-> [OverrideTemplate p sym ext arch]
-> [OverrideTemplate p sym ext arch]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> TemplateMatcher -> Bool
matches String
nm (TemplateMatcher -> Bool)
-> (OverrideTemplate p sym ext arch -> TemplateMatcher)
-> OverrideTemplate p sym ext arch
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OverrideTemplate p sym ext arch -> TemplateMatcher
forall p sym ext (arch :: LLVMArch).
OverrideTemplate p sym ext arch -> TemplateMatcher
overrideTemplateMatcher) [OverrideTemplate p sym ext arch]
ts
 where L.Symbol String
nm = Declare -> Symbol
L.decName Declare
decl

-- | Match a set of 'OverrideTemplate's against a single 'L.Declare',
-- registering all the overrides that apply and returning them as a list.
match_llvm_overrides ::
  (IsSymInterface sym, HasLLVMAnn sym) =>
  LLVMContext arch ->
  -- | Overrides to attempt to match against this declaration
  [OverrideTemplate p sym ext arch] ->
  -- | Declaration of the function that might get overridden
  L.Declare ->
  OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
match_llvm_overrides :: forall sym (arch :: LLVMArch) p ext rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMContext arch
-> [OverrideTemplate p sym ext arch]
-> Declare
-> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
match_llvm_overrides LLVMContext arch
llvmctx [OverrideTemplate p sym ext arch]
acts Declare
decl =
  LLVMContext arch
-> forall a.
   ((16 <= ArchWidth arch) => NatRepr (ArchWidth arch) -> a) -> a
forall (arch :: LLVMArch).
LLVMContext arch
-> forall a.
   ((16 <= ArchWidth arch) => NatRepr (ArchWidth arch) -> a) -> a
llvmPtrWidth LLVMContext arch
llvmctx (((16 <= ArchWidth arch) =>
  NatRepr (ArchWidth arch)
  -> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext])
 -> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext])
-> ((16 <= ArchWidth arch) =>
    NatRepr (ArchWidth arch)
    -> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext])
-> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
forall a b. (a -> b) -> a -> b
$ \NatRepr (ArchWidth arch)
wptr -> NatRepr (ArchWidth arch)
-> (HasPtrWidth (ArchWidth arch) =>
    OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext])
-> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
forall (w :: Natural) a.
(16 <= w) =>
NatRepr w -> (HasPtrWidth w => a) -> a
withPtrWidth NatRepr (ArchWidth arch)
wptr ((HasPtrWidth (ArchWidth arch) =>
  OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext])
 -> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext])
-> (HasPtrWidth (ArchWidth arch) =>
    OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext])
-> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
forall a b. (a -> b) -> a -> b
$ do
    let acts' :: [OverrideTemplate p sym ext arch]
acts' = [OverrideTemplate p sym ext arch]
-> Declare -> [OverrideTemplate p sym ext arch]
forall p sym ext (arch :: LLVMArch).
[OverrideTemplate p sym ext arch]
-> Declare -> [OverrideTemplate p sym ext arch]
filterTemplates [OverrideTemplate p sym ext arch]
acts Declare
decl
    let L.Symbol String
nm = Declare -> Symbol
L.decName Declare
decl
    let declnm :: Maybe DecodedName
declnm = (String -> Maybe DecodedName)
-> (DecodedName -> Maybe DecodedName)
-> Either String DecodedName
-> Maybe DecodedName
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe DecodedName -> String -> Maybe DecodedName
forall a b. a -> b -> a
const Maybe DecodedName
forall a. Maybe a
Nothing) DecodedName -> Maybe DecodedName
forall a. a -> Maybe a
Just (Either String DecodedName -> Maybe DecodedName)
-> Either String DecodedName -> Maybe DecodedName
forall a b. (a -> b) -> a -> b
$ String -> Either String DecodedName
ABI.demangleName String
nm
    [Maybe (SomeLLVMOverride p sym ext)]
mbOvs <-
      [MakeOverride p sym ext arch]
-> (MakeOverride p sym ext arch
    -> OverrideSim
         p sym ext rtp l a (Maybe (SomeLLVMOverride p sym ext)))
-> OverrideSim
     p sym ext rtp l a [Maybe (SomeLLVMOverride p sym ext)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ((OverrideTemplate p sym ext arch -> MakeOverride p sym ext arch)
-> [OverrideTemplate p sym ext arch]
-> [MakeOverride p sym ext arch]
forall a b. (a -> b) -> [a] -> [b]
map OverrideTemplate p sym ext arch -> MakeOverride p sym ext arch
forall p sym ext (arch :: LLVMArch).
OverrideTemplate p sym ext arch -> MakeOverride p sym ext arch
overrideTemplateAction [OverrideTemplate p sym ext arch]
acts') ((MakeOverride p sym ext arch
  -> OverrideSim
       p sym ext rtp l a (Maybe (SomeLLVMOverride p sym ext)))
 -> OverrideSim
      p sym ext rtp l a [Maybe (SomeLLVMOverride p sym ext)])
-> (MakeOverride p sym ext arch
    -> OverrideSim
         p sym ext rtp l a (Maybe (SomeLLVMOverride p sym ext)))
-> OverrideSim
     p sym ext rtp l a [Maybe (SomeLLVMOverride p sym ext)]
forall a b. (a -> b) -> a -> b
$ \(MakeOverride Declare
-> Maybe DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym ext)
act) ->
        case Declare
-> Maybe DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym ext)
act Declare
decl Maybe DecodedName
declnm LLVMContext arch
llvmctx of
          Maybe (SomeLLVMOverride p sym ext)
Nothing -> Maybe (SomeLLVMOverride p sym ext)
-> OverrideSim
     p sym ext rtp l a (Maybe (SomeLLVMOverride p sym ext))
forall a. a -> OverrideSim p sym ext rtp l a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe (SomeLLVMOverride p sym ext)
forall a. Maybe a
Nothing
          Just sov :: SomeLLVMOverride p sym ext
sov@(SomeLLVMOverride LLVMOverride p sym ext args ret
ov) -> do
            LLVMOverride p sym ext args ret
-> Declare -> LLVMContext arch -> OverrideSim p sym ext rtp l a ()
forall p (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 -> LLVMContext arch -> OverrideSim p sym ext rtp l a ()
register_llvm_override LLVMOverride p sym ext args ret
ov Declare
decl LLVMContext arch
llvmctx
            Maybe (SomeLLVMOverride p sym ext)
-> OverrideSim
     p sym ext rtp l a (Maybe (SomeLLVMOverride p sym ext))
forall a. a -> OverrideSim p sym ext rtp l a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SomeLLVMOverride p sym ext -> Maybe (SomeLLVMOverride p sym ext)
forall a. a -> Maybe a
Just SomeLLVMOverride p sym ext
sov)
    [SomeLLVMOverride p sym ext]
-> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
forall a. a -> OverrideSim p sym ext rtp l a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Maybe (SomeLLVMOverride p sym ext)]
-> [SomeLLVMOverride p sym ext]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (SomeLLVMOverride p sym ext)]
mbOvs)

-- | Match a set of 'OverrideTemplate's against a set of 'L.Declare's,
-- registering all the overrides that apply and returning them as a list.
register_llvm_overrides_ ::
  (IsSymInterface sym, HasLLVMAnn sym) =>
  LLVMContext arch ->
  -- | Overrides to attempt to match against these declarations
  [OverrideTemplate p sym ext arch] ->
  -- | Declarations of the functions that might get overridden
  [L.Declare] ->
  OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
register_llvm_overrides_ :: forall sym (arch :: LLVMArch) p ext rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMContext arch
-> [OverrideTemplate p sym ext arch]
-> [Declare]
-> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
register_llvm_overrides_ LLVMContext arch
llvmctx [OverrideTemplate p sym ext arch]
acts [Declare]
decls =
  [[SomeLLVMOverride p sym ext]] -> [SomeLLVMOverride p sym ext]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat ([[SomeLLVMOverride p sym ext]] -> [SomeLLVMOverride p sym ext])
-> OverrideSim p sym ext rtp l a [[SomeLLVMOverride p sym ext]]
-> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Declare]
-> (Declare
    -> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext])
-> OverrideSim p sym ext rtp l a [[SomeLLVMOverride p sym ext]]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Declare]
decls (\Declare
decl -> LLVMContext arch
-> [OverrideTemplate p sym ext arch]
-> Declare
-> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
forall sym (arch :: LLVMArch) p ext rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMContext arch
-> [OverrideTemplate p sym ext arch]
-> Declare
-> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
match_llvm_overrides LLVMContext arch
llvmctx [OverrideTemplate p sym ext arch]
acts Declare
decl)

-- | Match a set of 'OverrideTemplate's against all the @declare@s and @define@s
-- in a 'L.Module', registering all the overrides that apply and returning them
-- as a list.
--
-- Registers a default set of overrides, in addition to the ones passed as an
-- argument.
register_llvm_define_overrides ::
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
  L.Module ->
  -- | Additional (non-default) @define@ overrides
  [OverrideTemplate p sym LLVM arch] ->
  LLVMContext arch ->
  OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
register_llvm_define_overrides :: forall sym (wptr :: Natural) (arch :: LLVMArch) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch) =>
Module
-> [OverrideTemplate p sym LLVM arch]
-> LLVMContext arch
-> OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
register_llvm_define_overrides Module
llvmModule [OverrideTemplate p sym LLVM arch]
addlOvrs 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 in
  LLVMContext arch
-> [OverrideTemplate p sym LLVM arch]
-> [Declare]
-> OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
forall sym (arch :: LLVMArch) p ext rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMContext arch
-> [OverrideTemplate p sym ext arch]
-> [Declare]
-> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
register_llvm_overrides_ LLVMContext arch
llvmctx ([OverrideTemplate p sym LLVM arch]
addlOvrs [OverrideTemplate p sym LLVM arch]
-> [OverrideTemplate p sym LLVM arch]
-> [OverrideTemplate p sym LLVM arch]
forall a. [a] -> [a] -> [a]
++ [OverrideTemplate p sym LLVM arch]
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch, ?lc::TypeContext) =>
[OverrideTemplate p sym LLVM arch]
define_overrides) ([Declare]
 -> OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM])
-> [Declare]
-> OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
forall a b. (a -> b) -> a -> b
$
     (Module -> [Declare]
allModuleDeclares Module
llvmModule)

-- | Match a set of 'OverrideTemplate's against all the @declare@s in a
-- 'L.Module', registering all the overrides that apply and returning them as
-- a list.
--
-- Registers a default set of overrides, in addition to the ones passed as an
-- argument.
register_llvm_declare_overrides ::
  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
  , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
  L.Module ->
  -- | Additional (non-default) @declare@ overrides
  [OverrideTemplate p sym LLVM arch] ->
  LLVMContext arch ->
  OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
register_llvm_declare_overrides :: forall sym (wptr :: Natural) (arch :: LLVMArch) p rtp
       (l :: Ctx CrucibleType) (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch, ?intrinsicsOpts::IntrinsicsOptions,
 ?memOpts::MemOptions) =>
Module
-> [OverrideTemplate p sym LLVM arch]
-> LLVMContext arch
-> OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
register_llvm_declare_overrides Module
llvmModule [OverrideTemplate p sym LLVM arch]
addlOvrs 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
  in LLVMContext arch
-> [OverrideTemplate p sym LLVM arch]
-> [Declare]
-> OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
forall sym (arch :: LLVMArch) p ext rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMContext arch
-> [OverrideTemplate p sym ext arch]
-> [Declare]
-> OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
register_llvm_overrides_ LLVMContext arch
llvmctx ([OverrideTemplate p sym LLVM arch]
addlOvrs [OverrideTemplate p sym LLVM arch]
-> [OverrideTemplate p sym LLVM arch]
-> [OverrideTemplate p sym LLVM arch]
forall a. [a] -> [a] -> [a]
++ [OverrideTemplate p sym LLVM arch]
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch, ?lc::TypeContext,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
[OverrideTemplate p sym LLVM arch]
declare_overrides) ([Declare]
 -> OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM])
-> [Declare]
-> OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
forall a b. (a -> b) -> a -> b
$
       Module -> [Declare]
L.modDeclares Module
llvmModule

-- | Register overrides for declared-but-not-defined functions
declare_overrides ::
  ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
  , ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
  [OverrideTemplate p sym LLVM arch]
declare_overrides :: forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch, ?lc::TypeContext,
 ?intrinsicsOpts::IntrinsicsOptions, ?memOpts::MemOptions) =>
[OverrideTemplate p sym LLVM arch]
declare_overrides =
  [[OverrideTemplate p sym LLVM arch]]
-> [OverrideTemplate p sym LLVM arch]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat
  [ (SomeLLVMOverride p sym LLVM -> OverrideTemplate p sym LLVM arch)
-> [SomeLLVMOverride p sym LLVM]
-> [OverrideTemplate p sym LLVM arch]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeLLVMOverride LLVMOverride p sym LLVM args ret
ov) -> LLVMOverride p sym LLVM args ret
-> OverrideTemplate p sym LLVM arch
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 LLVM args ret
ov) [SomeLLVMOverride p sym LLVM]
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?intrinsicsOpts::IntrinsicsOptions,
 ?memOpts::MemOptions) =>
[SomeLLVMOverride p sym ext]
Libc.libc_overrides
  , (SomeLLVMOverride p sym LLVM -> OverrideTemplate p sym LLVM arch)
-> [SomeLLVMOverride p sym LLVM]
-> [OverrideTemplate p sym LLVM arch]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeLLVMOverride LLVMOverride p sym LLVM args ret
ov) -> LLVMOverride p sym LLVM args ret
-> OverrideTemplate p sym LLVM arch
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 LLVM args ret
ov) [SomeLLVMOverride p sym LLVM]
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?memOpts::MemOptions) =>
[SomeLLVMOverride p sym ext]
LLVM.basic_llvm_overrides
  , ((String, Poly1LLVMOverride p sym LLVM)
 -> OverrideTemplate p sym LLVM arch)
-> [(String, Poly1LLVMOverride p sym LLVM)]
-> [OverrideTemplate p sym LLVM arch]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
pfx, LLVM.Poly1LLVMOverride forall (w :: Natural).
(1 <= w) =>
NatRepr w -> SomeLLVMOverride p sym LLVM
ov) -> String
-> (forall (w :: Natural).
    (1 <= w) =>
    NatRepr w -> SomeLLVMOverride p sym LLVM)
-> OverrideTemplate p sym LLVM 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)
-> OverrideTemplate p sym ext arch
polymorphic1_llvm_override String
pfx NatRepr w -> SomeLLVMOverride p sym LLVM
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> SomeLLVMOverride p sym LLVM
ov) [(String, Poly1LLVMOverride p sym LLVM)]
forall sym (wptr :: Natural) p ext.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 ?lc::TypeContext, ?memOpts::MemOptions) =>
[(String, Poly1LLVMOverride p sym ext)]
LLVM.poly1_llvm_overrides
  , ((String, Poly1VecLLVMOverride p sym LLVM)
 -> OverrideTemplate p sym LLVM arch)
-> [(String, Poly1VecLLVMOverride p sym LLVM)]
-> [OverrideTemplate p sym LLVM arch]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
pfx, LLVM.Poly1VecLLVMOverride forall (vecSz :: Natural) (intSz :: Natural).
(1 <= intSz) =>
NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym LLVM
ov) -> String
-> (forall (vecSz :: Natural) (intSz :: Natural).
    (1 <= intSz) =>
    NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym LLVM)
-> OverrideTemplate p sym LLVM 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)
-> OverrideTemplate p sym ext arch
polymorphic1_vec_llvm_override String
pfx NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym LLVM
forall (vecSz :: Natural) (intSz :: Natural).
(1 <= intSz) =>
NatRepr vecSz -> NatRepr intSz -> SomeLLVMOverride p sym LLVM
ov) [(String, Poly1VecLLVMOverride p sym LLVM)]
forall sym p ext.
IsSymInterface sym =>
[(String, Poly1VecLLVMOverride p sym ext)]
LLVM.poly1_vec_llvm_overrides

  -- C++ standard library functions
  , [ SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
forall sym (wptr :: Natural) p (arch :: LLVMArch).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
Libcxx.register_cpp_override SomeCPPOverride p sym arch
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
SomeCPPOverride p sym arch
Libcxx.endlOverride ]
  ]


-- | Register those overrides that should apply even when the corresponding
-- function has a definition
define_overrides ::
  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch, ?lc :: TypeContext) =>
  [OverrideTemplate p sym LLVM arch]
define_overrides :: forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr,
 wptr ~ ArchWidth arch, ?lc::TypeContext) =>
[OverrideTemplate p sym LLVM arch]
define_overrides =
  [ SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
forall sym (wptr :: Natural) p (arch :: LLVMArch).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
Libcxx.register_cpp_override SomeCPPOverride p sym arch
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
SomeCPPOverride p sym arch
Libcxx.putToOverride12
  , SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
forall sym (wptr :: Natural) p (arch :: LLVMArch).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
Libcxx.register_cpp_override SomeCPPOverride p sym arch
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
SomeCPPOverride p sym arch
Libcxx.putToOverride9
  , SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
forall sym (wptr :: Natural) p (arch :: LLVMArch).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
Libcxx.register_cpp_override SomeCPPOverride p sym arch
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
SomeCPPOverride p sym arch
Libcxx.endlOverride
  , SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
forall sym (wptr :: Natural) p (arch :: LLVMArch).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
Libcxx.register_cpp_override SomeCPPOverride p sym arch
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
SomeCPPOverride p sym arch
Libcxx.sentryOverride
  , SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
forall sym (wptr :: Natural) p (arch :: LLVMArch).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
Libcxx.register_cpp_override SomeCPPOverride p sym arch
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
SomeCPPOverride p sym arch
Libcxx.sentryBoolOverride
  ]

{-
Note [Overrides involving (unsigned) long]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Registering overrides for functions with `long` argument or result types is
tricky, as the size of a `long` varies wildly between different operating
systems and architectures. On Linux and macOS, `long` is 32 or 64 bits on
32- or 64-bit architectures, respectively. On Windows, however, `long` is
always 32 bits, regardless of architecture. There is a similar story for the
`unsigned long` type as well.

To ensure that overrides for functions involving `long` are (at least to some
degree) portable, we register each override for `long`-using function twice:
once where `long` is assumed to be 32 bits, and once again where `long` is
assumed to be 64 bits. This is a somewhat heavy-handed solution, but it avoids
the need to predict what size `long` will be on a given target ahead of time.
-}