{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
module Lang.Crucible.LLVM.Intrinsics.Libcxx
( register_cpp_override
, putToOverride12
, putToOverride9
, endlOverride
, sentryOverride
, sentryBoolOverride
) where
import qualified ABI.Itanium as ABI
import Control.Monad.Reader
import Data.List (isInfixOf)
import Data.Type.Equality ((:~:)(Refl), testEquality)
import qualified Text.LLVM.AST as L
import qualified Data.BitVector.Sized as BV
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.NatRepr (knownNat)
import What4.Interface (bvLit, natLit)
import Lang.Crucible.Backend
import Lang.Crucible.CFG.Common (GlobalVar)
import Lang.Crucible.Simulator.OverrideSim (OverrideSim, getSymInterface)
import Lang.Crucible.Simulator.RegMap (RegEntry, RegValue, regValue)
import Lang.Crucible.Panic (panic)
import Lang.Crucible.Types (TypeRepr(UnitRepr))
import Lang.Crucible.LLVM.Extension
import Lang.Crucible.LLVM.Intrinsics.Common
import qualified Lang.Crucible.LLVM.Intrinsics.Declare as Decl
import qualified Lang.Crucible.LLVM.Intrinsics.Match as Match
import Lang.Crucible.LLVM.MemModel
import Lang.Crucible.LLVM.Translation.Monad (LLVMContext)
register_cpp_override ::
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
SomeCPPOverride p sym arch ->
OverrideTemplate p sym LLVM arch
register_cpp_override :: forall sym (wptr :: Natural) p (arch :: LLVMArch).
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
SomeCPPOverride p sym arch -> OverrideTemplate p sym LLVM arch
register_cpp_override SomeCPPOverride p sym arch
someCPPOverride =
TemplateMatcher
-> MakeOverride p sym LLVM arch -> OverrideTemplate p sym LLVM arch
forall p sym ext (arch :: LLVMArch).
TemplateMatcher
-> MakeOverride p sym ext arch -> OverrideTemplate p sym ext arch
OverrideTemplate ([String] -> TemplateMatcher
Match.SubstringsMatch (String
"_Z" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: SomeCPPOverride p sym arch -> [String]
forall p sym (arch :: LLVMArch).
SomeCPPOverride p sym arch -> [String]
cppOverrideSubstrings SomeCPPOverride p sym arch
someCPPOverride)) (MakeOverride p sym LLVM arch -> OverrideTemplate p sym LLVM arch)
-> MakeOverride p sym LLVM arch -> OverrideTemplate p sym LLVM arch
forall a b. (a -> b) -> a -> b
$
(SomeDeclare
-> Maybe DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym LLVM))
-> MakeOverride p sym LLVM 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 LLVM))
-> MakeOverride p sym LLVM arch)
-> (SomeDeclare
-> Maybe DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym LLVM))
-> MakeOverride p sym LLVM arch
forall a b. (a -> b) -> a -> b
$ \SomeDeclare
requestedDecl Maybe DecodedName
decName LLVMContext arch
llvmctx -> do
DecodedName
nm <- Maybe DecodedName
decName
SomeCPPOverride p sym arch
-> SomeDeclare
-> DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym LLVM)
forall p sym (arch :: LLVMArch).
SomeCPPOverride p sym arch
-> SomeDeclare
-> DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym LLVM)
cppOverrideAction SomeCPPOverride p sym arch
someCPPOverride SomeDeclare
requestedDecl DecodedName
nm LLVMContext arch
llvmctx
data SomeCPPOverride p sym arch =
SomeCPPOverride
{ forall p sym (arch :: LLVMArch).
SomeCPPOverride p sym arch -> [String]
cppOverrideSubstrings :: [String]
, forall p sym (arch :: LLVMArch).
SomeCPPOverride p sym arch
-> SomeDeclare
-> DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym LLVM)
cppOverrideAction ::
Decl.SomeDeclare ->
ABI.DecodedName ->
LLVMContext arch ->
Maybe (SomeLLVMOverride p sym LLVM)
}
matchSymbolName :: (L.Symbol -> ABI.DecodedName -> Bool)
-> Decl.SomeDeclare
-> ABI.DecodedName
-> Maybe a
-> Maybe a
matchSymbolName :: forall a.
(Symbol -> DecodedName -> Bool)
-> SomeDeclare -> DecodedName -> Maybe a -> Maybe a
matchSymbolName Symbol -> DecodedName -> Bool
match (Decl.SomeDeclare Declare args ret
decl) DecodedName
decodedName =
if Bool -> Bool
not (Symbol -> DecodedName -> Bool
match (Declare args ret -> Symbol
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName Declare args ret
decl) DecodedName
decodedName)
then Maybe a -> Maybe a -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing
else Maybe a -> Maybe a
forall a. a -> a
id
panic_ :: String -> Decl.SomeDeclare -> c
panic_ :: forall c. String -> SomeDeclare -> c
panic_ String
from (Decl.SomeDeclare Declare args ret
decl) =
String -> [String] -> c
forall a. HasCallStack => String -> [String] -> a
panic String
from [ String
"Ill-typed override"
, String
"Name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm
, String
"Args: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Assignment TypeRepr args -> String
forall a. Show a => a -> String
show (Declare args ret -> Assignment TypeRepr args
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Assignment TypeRepr args
Decl.decArgs Declare args ret
decl)
, String
"Ret: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRepr ret -> String
forall a. Show a => a -> String
show (Declare args ret -> TypeRepr ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> TypeRepr ret
Decl.decRet Declare args ret
decl)
]
where L.Symbol String
nm = Declare args ret -> Symbol
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName Declare args ret
decl
mkOverride :: (IsSymInterface sym, HasPtrWidth (ArchWidth arch))
=> [String]
-> (Decl.SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (L.Symbol -> ABI.DecodedName -> Bool)
-> SomeCPPOverride p sym arch
mkOverride :: forall sym (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth (ArchWidth arch)) =>
[String]
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
mkOverride [String]
substrings SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM)
ov Symbol -> DecodedName -> Bool
filt =
[String]
-> (SomeDeclare
-> DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym LLVM))
-> SomeCPPOverride p sym arch
forall p sym (arch :: LLVMArch).
[String]
-> (SomeDeclare
-> DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym LLVM))
-> SomeCPPOverride p sym arch
SomeCPPOverride [String]
substrings ((SomeDeclare
-> DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym LLVM))
-> SomeCPPOverride p sym arch)
-> (SomeDeclare
-> DecodedName
-> LLVMContext arch
-> Maybe (SomeLLVMOverride p sym LLVM))
-> SomeCPPOverride p sym arch
forall a b. (a -> b) -> a -> b
$ \SomeDeclare
requestedDecl DecodedName
decodedName LLVMContext arch
_llvmCtx ->
(Symbol -> DecodedName -> Bool)
-> SomeDeclare
-> DecodedName
-> Maybe (SomeLLVMOverride p sym LLVM)
-> Maybe (SomeLLVMOverride p sym LLVM)
forall a.
(Symbol -> DecodedName -> Bool)
-> SomeDeclare -> DecodedName -> Maybe a -> Maybe a
matchSymbolName Symbol -> DecodedName -> Bool
filt SomeDeclare
requestedDecl DecodedName
decodedName (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM)
ov SomeDeclare
requestedDecl)
someOv ::
L.Symbol ->
Ctx.Assignment TypeRepr args ->
TypeRepr ret ->
(IsSymInterface sym =>
GlobalVar Mem ->
Ctx.Assignment (RegEntry sym) args ->
forall rtp args' ret'.
OverrideSim p sym ext rtp args' ret' (RegValue sym ret)) ->
SomeLLVMOverride p sym ext
someOv :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType) sym p ext.
Symbol
-> Assignment TypeRepr args
-> TypeRepr 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))
-> SomeLLVMOverride p sym ext
someOv Symbol
nm Assignment TypeRepr args
argTys TypeRepr ret
retTy 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)
def =
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 (Declare 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))
-> LLVMOverride p sym ext args ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare 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))
-> LLVMOverride p sym ext args ret
LLVMOverride (Symbol
-> Assignment TypeRepr args -> TypeRepr ret -> Declare args ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Symbol
-> Assignment TypeRepr args -> TypeRepr ret -> Declare args ret
Decl.Declare Symbol
nm Assignment TypeRepr args
argTys TypeRepr ret
retTy) 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)
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall rtp (args' :: Ctx CrucibleType) (ret' :: CrucibleType).
OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
def)
voidOverride :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)
=> [String]
-> (L.Symbol -> ABI.DecodedName -> Bool)
-> SomeCPPOverride p sym arch
voidOverride :: forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
voidOverride [String]
substrings =
[String]
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
forall sym (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth (ArchWidth arch)) =>
[String]
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
mkOverride [String]
substrings ((SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch)
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
forall a b. (a -> b) -> a -> b
$
\sd :: SomeDeclare
sd@(Decl.SomeDeclare
(Decl.Declare
{ decName :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName = Symbol
nm
, decArgs :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Assignment TypeRepr args
Decl.decArgs = Assignment TypeRepr args
argTys
, decRet :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> TypeRepr ret
Decl.decRet = TypeRepr ret
retTy
})) ->
SomeLLVMOverride p sym LLVM -> Maybe (SomeLLVMOverride p sym LLVM)
forall a. a -> Maybe a
Just (SomeLLVMOverride p sym LLVM
-> Maybe (SomeLLVMOverride p sym LLVM))
-> SomeLLVMOverride p sym LLVM
-> Maybe (SomeLLVMOverride p sym LLVM)
forall a b. (a -> b) -> a -> b
$
case TypeRepr ret
retTy of
TypeRepr ret
UnitRepr -> Symbol
-> Assignment TypeRepr args
-> TypeRepr ret
-> (IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret))
-> SomeLLVMOverride p sym LLVM
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) sym p ext.
Symbol
-> Assignment TypeRepr args
-> TypeRepr 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))
-> SomeLLVMOverride p sym ext
someOv Symbol
nm Assignment TypeRepr args
argTys TypeRepr ret
retTy ((IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret))
-> SomeLLVMOverride p sym LLVM)
-> (IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret))
-> SomeLLVMOverride p sym LLVM
forall a b. (a -> b) -> a -> b
$ \GlobalVar Mem
_mem Assignment (RegEntry sym) args
_args -> () -> OverrideSim p sym LLVM rtp args' ret' ()
forall a. a -> OverrideSim p sym LLVM rtp args' ret' a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
TypeRepr ret
_ -> String -> SomeDeclare -> SomeLLVMOverride p sym LLVM
forall c. String -> SomeDeclare -> c
panic_ String
"voidOverride" SomeDeclare
sd
identityOverride :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)
=> [String]
-> (L.Symbol -> ABI.DecodedName -> Bool)
-> SomeCPPOverride p sym arch
identityOverride :: forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
identityOverride [String]
substrings =
[String]
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
forall sym (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth (ArchWidth arch)) =>
[String]
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
mkOverride [String]
substrings ((SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch)
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
forall a b. (a -> b) -> a -> b
$
\sd :: SomeDeclare
sd@(Decl.SomeDeclare
(Decl.Declare
{ decName :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName = Symbol
nm
, decArgs :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Assignment TypeRepr args
Decl.decArgs = Assignment TypeRepr args
argTys
, decRet :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> TypeRepr ret
Decl.decRet = TypeRepr ret
retTy
})) ->
SomeLLVMOverride p sym LLVM -> Maybe (SomeLLVMOverride p sym LLVM)
forall a. a -> Maybe a
Just (SomeLLVMOverride p sym LLVM
-> Maybe (SomeLLVMOverride p sym LLVM))
-> SomeLLVMOverride p sym LLVM
-> Maybe (SomeLLVMOverride p sym LLVM)
forall a b. (a -> b) -> a -> b
$
case Assignment TypeRepr args
argTys of
(Assignment TypeRepr ctx
Ctx.Empty Ctx.:> TypeRepr tp
argTy)
| Just tp :~: ret
Refl <- TypeRepr tp -> TypeRepr ret -> Maybe (tp :~: 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 tp
argTy TypeRepr ret
retTy ->
Symbol
-> Assignment TypeRepr args
-> TypeRepr ret
-> (IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret))
-> SomeLLVMOverride p sym LLVM
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) sym p ext.
Symbol
-> Assignment TypeRepr args
-> TypeRepr 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))
-> SomeLLVMOverride p sym ext
someOv Symbol
nm Assignment TypeRepr args
argTys TypeRepr ret
retTy ((IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret))
-> SomeLLVMOverride p sym LLVM)
-> (IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret))
-> SomeLLVMOverride p sym LLVM
forall a b. (a -> b) -> a -> b
$ \GlobalVar Mem
_mem Assignment (RegEntry sym) args
args ->
RegValue sym ret
-> OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret)
forall a. a -> OverrideSim p sym LLVM rtp args' ret' a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (CurryAssignment args (RegEntry sym) (RegValue sym ret)
-> Assignment (RegEntry sym) args -> RegValue sym 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 args f x -> Assignment f args -> x
Ctx.uncurryAssignment CurryAssignment args (RegEntry sym) (RegValue sym ret)
RegEntry sym ret -> RegValue sym ret
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue Assignment (RegEntry sym) args
args)
Assignment TypeRepr args
_ -> String -> SomeDeclare -> SomeLLVMOverride p sym LLVM
forall c. String -> SomeDeclare -> c
panic_ String
"identityOverride" SomeDeclare
sd
constOverride :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)
=> [String]
-> (L.Symbol -> ABI.DecodedName -> Bool)
-> SomeCPPOverride p sym arch
constOverride :: forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
constOverride [String]
substrings =
[String]
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
forall sym (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth (ArchWidth arch)) =>
[String]
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
mkOverride [String]
substrings ((SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch)
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
forall a b. (a -> b) -> a -> b
$
\sd :: SomeDeclare
sd@(Decl.SomeDeclare
(Decl.Declare
{ decName :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName = Symbol
nm
, decArgs :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Assignment TypeRepr args
Decl.decArgs = Assignment TypeRepr args
argTys
, decRet :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> TypeRepr ret
Decl.decRet = TypeRepr ret
retTy
})) ->
SomeLLVMOverride p sym LLVM -> Maybe (SomeLLVMOverride p sym LLVM)
forall a. a -> Maybe a
Just (SomeLLVMOverride p sym LLVM
-> Maybe (SomeLLVMOverride p sym LLVM))
-> SomeLLVMOverride p sym LLVM
-> Maybe (SomeLLVMOverride p sym LLVM)
forall a b. (a -> b) -> a -> b
$
case Assignment TypeRepr args
argTys of
(Assignment TypeRepr ctx
Ctx.Empty Ctx.:> TypeRepr tp
fstTy Ctx.:> TypeRepr tp
_)
| Just tp :~: ret
Refl <- TypeRepr tp -> TypeRepr ret -> Maybe (tp :~: 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 tp
fstTy TypeRepr ret
retTy ->
Symbol
-> Assignment TypeRepr args
-> TypeRepr ret
-> (IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret))
-> SomeLLVMOverride p sym LLVM
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) sym p ext.
Symbol
-> Assignment TypeRepr args
-> TypeRepr 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))
-> SomeLLVMOverride p sym ext
someOv Symbol
nm Assignment TypeRepr args
argTys TypeRepr ret
retTy ((IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret))
-> SomeLLVMOverride p sym LLVM)
-> (IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret))
-> SomeLLVMOverride p sym LLVM
forall a b. (a -> b) -> a -> b
$ \GlobalVar Mem
_mem Assignment (RegEntry sym) args
args ->
RegValue sym ret
-> OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret)
forall a. a -> OverrideSim p sym LLVM rtp args' ret' a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (CurryAssignment args (RegEntry sym) (RegValue sym ret)
-> Assignment (RegEntry sym) args -> RegValue sym 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 args f x -> Assignment f args -> x
Ctx.uncurryAssignment (RegValue sym ret -> RegEntry sym tp -> RegValue sym ret
forall a b. a -> b -> a
const (RegValue sym ret -> RegEntry sym tp -> RegValue sym ret)
-> (RegEntry sym ret -> RegValue sym ret)
-> RegEntry sym ret
-> RegEntry sym tp
-> RegValue sym ret
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RegEntry sym ret -> RegValue sym ret
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue) Assignment (RegEntry sym) args
args)
Assignment TypeRepr args
_ -> String -> SomeDeclare -> SomeLLVMOverride p sym LLVM
forall c. String -> SomeDeclare -> c
panic_ String
"constOverride" SomeDeclare
sd
fixedOverride :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)
=> TypeRepr ty
-> (GlobalVar Mem -> sym -> IO (RegValue sym ty))
-> [String]
-> (L.Symbol -> ABI.DecodedName -> Bool)
-> SomeCPPOverride p sym arch
fixedOverride :: forall sym (wptr :: Natural) (arch :: LLVMArch)
(ty :: CrucibleType) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
TypeRepr ty
-> (GlobalVar Mem -> sym -> IO (RegValue sym ty))
-> [String]
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
fixedOverride TypeRepr ty
ty GlobalVar Mem -> sym -> IO (RegValue sym ty)
regval [String]
substrings =
[String]
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
forall sym (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth (ArchWidth arch)) =>
[String]
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
mkOverride [String]
substrings ((SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch)
-> (SomeDeclare -> Maybe (SomeLLVMOverride p sym LLVM))
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
forall a b. (a -> b) -> a -> b
$
\sd :: SomeDeclare
sd@(Decl.SomeDeclare
(Decl.Declare
{ decName :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
Decl.decName = Symbol
nm
, decArgs :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Assignment TypeRepr args
Decl.decArgs = Assignment TypeRepr args
argTys
, decRet :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> TypeRepr ret
Decl.decRet = TypeRepr ret
retTy
})) ->
SomeLLVMOverride p sym LLVM -> Maybe (SomeLLVMOverride p sym LLVM)
forall a. a -> Maybe a
Just (SomeLLVMOverride p sym LLVM
-> Maybe (SomeLLVMOverride p sym LLVM))
-> SomeLLVMOverride p sym LLVM
-> Maybe (SomeLLVMOverride p sym LLVM)
forall a b. (a -> b) -> a -> b
$
case TypeRepr ret -> TypeRepr ty -> Maybe (ret :~: ty)
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
retTy TypeRepr ty
ty of
Just ret :~: ty
Refl ->
Symbol
-> Assignment TypeRepr args
-> TypeRepr ret
-> (IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret))
-> SomeLLVMOverride p sym LLVM
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) sym p ext.
Symbol
-> Assignment TypeRepr args
-> TypeRepr 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))
-> SomeLLVMOverride p sym ext
someOv Symbol
nm Assignment TypeRepr args
argTys TypeRepr ret
retTy ((IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret))
-> SomeLLVMOverride p sym LLVM)
-> (IsSymInterface sym =>
GlobalVar Mem
-> Assignment (RegEntry sym) args
-> forall {rtp} {args' :: Ctx CrucibleType} {ret' :: CrucibleType}.
OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret))
-> SomeLLVMOverride p sym LLVM
forall a b. (a -> b) -> a -> b
$ \GlobalVar Mem
mem Assignment (RegEntry sym) args
_args -> do
sym
sym <- OverrideSim p sym LLVM rtp args' ret' sym
forall p sym ext rtp (args :: Ctx CrucibleType)
(ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
IO (RegValue sym ty)
-> OverrideSim p sym LLVM rtp args' ret' (RegValue sym ty)
forall a. IO a -> OverrideSim p sym LLVM rtp args' ret' a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (GlobalVar Mem -> sym -> IO (RegValue sym ty)
regval GlobalVar Mem
mem sym
sym)
Maybe (ret :~: ty)
_ -> String -> SomeDeclare -> SomeLLVMOverride p sym LLVM
forall c. String -> SomeDeclare -> c
panic_ String
"fixedOverride" SomeDeclare
sd
trueOverride :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)
=> [String]
-> (L.Symbol -> ABI.DecodedName -> Bool)
-> SomeCPPOverride p sym arch
trueOverride :: forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
trueOverride =
TypeRepr (LLVMPointerType 1)
-> (GlobalVar Mem -> sym -> IO (RegValue sym (LLVMPointerType 1)))
-> [String]
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
forall sym (wptr :: Natural) (arch :: LLVMArch)
(ty :: CrucibleType) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
TypeRepr ty
-> (GlobalVar Mem -> sym -> IO (RegValue sym ty))
-> [String]
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
fixedOverride (NatRepr 1 -> TypeRepr (LLVMPointerType 1)
forall (ty :: CrucibleType) (w :: Natural).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat) ((GlobalVar Mem -> sym -> IO (RegValue sym (LLVMPointerType 1)))
-> [String]
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch)
-> (GlobalVar Mem -> sym -> IO (RegValue sym (LLVMPointerType 1)))
-> [String]
-> (Symbol -> DecodedName -> Bool)
-> SomeCPPOverride p sym arch
forall a b. (a -> b) -> a -> b
$ \GlobalVar Mem
_mem sym
sym ->
SymNat sym -> SymBV sym 1 -> LLVMPointer sym 1
forall sym (w :: Natural).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer (SymNat sym -> SymBV sym 1 -> LLVMPointer sym 1)
-> IO (SymNat sym) -> IO (SymBV sym 1 -> LLVMPointer sym 1)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
0 IO (SymBV sym 1 -> LLVMPointer sym 1)
-> IO (SymBV sym 1) -> IO (LLVMPointer sym 1)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym -> NatRepr 1 -> BV 1 -> IO (SymBV sym 1)
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 (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) (NatRepr 1 -> BV 1
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w
BV.one NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat)
putToOverride12 :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)
=> SomeCPPOverride p sym arch
putToOverride12 :: forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
SomeCPPOverride p sym arch
putToOverride12 =
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
constOverride [String
"St",String
"ls",String
"basic_ostream"] ((Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch)
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
forall a b. (a -> b) -> a -> b
$ \Symbol
_ DecodedName
decodedName ->
case DecodedName
decodedName of
ABI.Function
(ABI.NestedName
[]
[ ABI.SubstitutionPrefix Substitution
ABI.SubStdNamespace
, Prefix
_
, ABI.UnqualifiedPrefix (ABI.SourceName String
"basic_ostream")
, ABI.TemplateArgsPrefix [TemplateArg]
_
]
(ABI.OperatorName Operator
ABI.OpShl))
[ABI.PointerToType (ABI.FunctionType [CXXType]
_)] -> Bool
True
DecodedName
_ -> Bool
False
putToOverride9 :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)
=> SomeCPPOverride p sym arch
putToOverride9 :: forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
SomeCPPOverride p sym arch
putToOverride9 =
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
constOverride [String
"NSt3__1lsINS_11char_traitsIcEEEERNS_13basic_ostreamIcT_EES6_PKc"] ((Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch)
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
forall a b. (a -> b) -> a -> b
$ \(L.Symbol String
nm) DecodedName
_ ->
String
nm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"_ZNSt3__1lsINS_11char_traitsIcEEEERNS_13basic_ostreamIcT_EES6_PKc"
endlOverride :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)
=> SomeCPPOverride p sym arch
endlOverride :: forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
SomeCPPOverride p sym arch
endlOverride =
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
identityOverride [String
"endl",String
"char_traits",String
"basic_ostream"] ((Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch)
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
forall a b. (a -> b) -> a -> b
$ \(L.Symbol String
nm) DecodedName
_decodedName ->
[Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
and [ String
"endl" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` String
nm
, String
"char_traits" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` String
nm
, String
"basic_ostream" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` String
nm
]
sentryOverride :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)
=> SomeCPPOverride p sym arch
sentryOverride :: forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
SomeCPPOverride p sym arch
sentryOverride =
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
voidOverride [String
"basic_ostream", String
"sentry"] ((Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch)
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
forall a b. (a -> b) -> a -> b
$ \Symbol
_nm DecodedName
decodedName ->
case DecodedName
decodedName of
ABI.Function
(ABI.NestedName
[]
[ ABI.SubstitutionPrefix Substitution
ABI.SubStdNamespace
, Prefix
_
, ABI.UnqualifiedPrefix (ABI.SourceName String
"basic_ostream")
, Prefix
_
, ABI.UnqualifiedPrefix (ABI.SourceName String
"sentry")
]
UnqualifiedName
_)
[CXXType]
_ -> Bool
True
DecodedName
_ -> Bool
False
sentryBoolOverride :: (IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch)
=> SomeCPPOverride p sym arch
sentryBoolOverride :: forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
SomeCPPOverride p sym arch
sentryBoolOverride =
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
forall sym (wptr :: Natural) (arch :: LLVMArch) p.
(IsSymInterface sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
[String]
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
trueOverride [String
"basic_ostream", String
"sentry"] ((Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch)
-> (Symbol -> DecodedName -> Bool) -> SomeCPPOverride p sym arch
forall a b. (a -> b) -> a -> b
$ \Symbol
_nm DecodedName
decodedName ->
case DecodedName
decodedName of
ABI.Function
(ABI.NestedName
[CVQualifier
ABI.Const]
[ ABI.SubstitutionPrefix Substitution
ABI.SubStdNamespace
, Prefix
_
, ABI.UnqualifiedPrefix (ABI.SourceName String
"basic_ostream")
, Prefix
_
, ABI.UnqualifiedPrefix (ABI.SourceName String
"sentry")
]
(ABI.OperatorName (ABI.OpCast CXXType
ABI.BoolType)))
[CXXType
ABI.VoidType] -> Bool
True
DecodedName
_ -> Bool
False