-- |
-- Module           : Lang.Crucible.LLVM.Intrinsics.Declare
-- Description      : Function declarations
-- Copyright        : (c) Galois, Inc 2026
-- License          : BSD3
-- Maintainer       : Langston Barrett <langston@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImplicitParams #-}

module Lang.Crucible.LLVM.Intrinsics.Declare
  ( Declare(..)
  , SomeDeclare(SomeDeclare)
  , fromHandle
  , fromSomeHandle
  , fromLLVM
  , fromLLVMWithWarnings
  ) where

import qualified Control.Monad.Fail as Fail
import           Control.Monad.IO.Class (liftIO)
import qualified Data.Maybe as Maybe
import qualified Data.Text as Text
import           Data.Traversable (for)

import qualified Text.LLVM.AST as L

import qualified Data.Parameterized.Context as Ctx

import qualified What4.FunctionName as WFN

import qualified Lang.Crucible.FunctionHandle as CFH
import           Lang.Crucible.Simulator.OverrideSim (OverrideSim)
import qualified Lang.Crucible.Types as CT
import           Lang.Crucible.Utils.MonadVerbosity (getLogFunction)

import           Lang.Crucible.LLVM.MemModel.Pointer (HasPtrWidth)
import           Lang.Crucible.LLVM.Translation.Types (llvmDeclToFunHandleRepr')
import           Lang.Crucible.LLVM.TypeContext (TypeContext)

-- | The declaration of a function.
--
-- Used primarily for matching LLVM overrides to the declarations in LLVM
-- modules or S-expression programs.
data Declare args ret
  = Declare
    { forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Symbol
decName :: L.Symbol
    , forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> Assignment TypeRepr args
decArgs :: Ctx.Assignment CT.TypeRepr args
    , forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> TypeRepr ret
decRet :: CT.TypeRepr ret
    }
  deriving Int -> Declare args ret -> ShowS
[Declare args ret] -> ShowS
Declare args ret -> String
(Int -> Declare args ret -> ShowS)
-> (Declare args ret -> String)
-> ([Declare args ret] -> ShowS)
-> Show (Declare args ret)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Int -> Declare args ret -> ShowS
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
[Declare args ret] -> ShowS
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> String
$cshowsPrec :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Int -> Declare args ret -> ShowS
showsPrec :: Int -> Declare args ret -> ShowS
$cshow :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> String
show :: Declare args ret -> String
$cshowList :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
[Declare args ret] -> ShowS
showList :: [Declare args ret] -> ShowS
Show

data SomeDeclare = forall args ret. SomeDeclare (Declare args ret)

fromHandle :: CFH.FnHandle args ret -> Declare args ret
fromHandle :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Declare args ret
fromHandle FnHandle args ret
hdl =
  Declare
  { decName :: Symbol
decName = String -> Symbol
L.Symbol (Text -> String
Text.unpack (FunctionName -> Text
WFN.functionName (FnHandle args ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
CFH.handleName FnHandle args ret
hdl)))
  , decArgs :: Assignment TypeRepr args
decArgs = FnHandle args ret -> Assignment TypeRepr args
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> CtxRepr args
CFH.handleArgTypes FnHandle args ret
hdl
  , decRet :: TypeRepr ret
decRet = FnHandle args ret -> TypeRepr ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr ret
CFH.handleReturnType FnHandle args ret
hdl
  }

fromSomeHandle :: CFH.SomeHandle -> SomeDeclare
fromSomeHandle :: SomeHandle -> SomeDeclare
fromSomeHandle (CFH.SomeHandle FnHandle args ret
hdl) = Declare args ret -> SomeDeclare
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> SomeDeclare
SomeDeclare (FnHandle args ret -> Declare args ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> Declare args ret
fromHandle FnHandle args ret
hdl)

fromLLVM ::
  ( ?lc :: TypeContext
  , HasPtrWidth wptr
  , Fail.MonadFail m
  ) =>
  L.Declare ->
  m SomeDeclare
fromLLVM :: forall (wptr :: Natural) (m :: Type -> Type).
(?lc::TypeContext, HasPtrWidth wptr, MonadFail m) =>
Declare -> m SomeDeclare
fromLLVM Declare
decl =
  Declare
-> (forall {args :: Ctx CrucibleType} {ret :: CrucibleType}.
    CtxRepr args -> TypeRepr ret -> m SomeDeclare)
-> m SomeDeclare
forall (wptr :: Natural) (m :: Type -> Type) a.
(?lc::TypeContext, HasPtrWidth wptr, MonadFail m) =>
Declare
-> (forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
    CtxRepr args -> TypeRepr ret -> m a)
-> m a
llvmDeclToFunHandleRepr' Declare
decl ((forall {args :: Ctx CrucibleType} {ret :: CrucibleType}.
  CtxRepr args -> TypeRepr ret -> m SomeDeclare)
 -> m SomeDeclare)
-> (forall {args :: Ctx CrucibleType} {ret :: CrucibleType}.
    CtxRepr args -> TypeRepr ret -> m SomeDeclare)
-> m SomeDeclare
forall a b. (a -> b) -> a -> b
$ \CtxRepr args
args TypeRepr ret
ret ->
    SomeDeclare -> m SomeDeclare
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SomeDeclare -> m SomeDeclare) -> SomeDeclare -> m SomeDeclare
forall a b. (a -> b) -> a -> b
$
      Declare args ret -> SomeDeclare
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
Declare args ret -> SomeDeclare
SomeDeclare (Declare args ret -> SomeDeclare)
-> Declare args ret -> SomeDeclare
forall a b. (a -> b) -> a -> b
$
        Declare
        { decName :: Symbol
decName = Declare -> Symbol
L.decName Declare
decl
        , decArgs :: CtxRepr args
decArgs = CtxRepr args
args
        , decRet :: TypeRepr ret
decRet = TypeRepr ret
ret
        }

-- | Internal, for 'Fail.MonadFail' instance
newtype EitherString a = EitherString (Either String a)
  deriving (Functor EitherString
Functor EitherString =>
(forall a. a -> EitherString a)
-> (forall a b.
    EitherString (a -> b) -> EitherString a -> EitherString b)
-> (forall a b c.
    (a -> b -> c)
    -> EitherString a -> EitherString b -> EitherString c)
-> (forall a b. EitherString a -> EitherString b -> EitherString b)
-> (forall a b. EitherString a -> EitherString b -> EitherString a)
-> Applicative EitherString
forall a. a -> EitherString a
forall a b. EitherString a -> EitherString b -> EitherString a
forall a b. EitherString a -> EitherString b -> EitherString b
forall a b.
EitherString (a -> b) -> EitherString a -> EitherString b
forall a b c.
(a -> b -> c) -> EitherString a -> EitherString b -> EitherString c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> EitherString a
pure :: forall a. a -> EitherString a
$c<*> :: forall a b.
EitherString (a -> b) -> EitherString a -> EitherString b
<*> :: forall a b.
EitherString (a -> b) -> EitherString a -> EitherString b
$cliftA2 :: forall a b c.
(a -> b -> c) -> EitherString a -> EitherString b -> EitherString c
liftA2 :: forall a b c.
(a -> b -> c) -> EitherString a -> EitherString b -> EitherString c
$c*> :: forall a b. EitherString a -> EitherString b -> EitherString b
*> :: forall a b. EitherString a -> EitherString b -> EitherString b
$c<* :: forall a b. EitherString a -> EitherString b -> EitherString a
<* :: forall a b. EitherString a -> EitherString b -> EitherString a
Applicative, (forall a b. (a -> b) -> EitherString a -> EitherString b)
-> (forall a b. a -> EitherString b -> EitherString a)
-> Functor EitherString
forall a b. a -> EitherString b -> EitherString a
forall a b. (a -> b) -> EitherString a -> EitherString b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> EitherString a -> EitherString b
fmap :: forall a b. (a -> b) -> EitherString a -> EitherString b
$c<$ :: forall a b. a -> EitherString b -> EitherString a
<$ :: forall a b. a -> EitherString b -> EitherString a
Functor, Applicative EitherString
Applicative EitherString =>
(forall a b.
 EitherString a -> (a -> EitherString b) -> EitherString b)
-> (forall a b. EitherString a -> EitherString b -> EitherString b)
-> (forall a. a -> EitherString a)
-> Monad EitherString
forall a. a -> EitherString a
forall a b. EitherString a -> EitherString b -> EitherString b
forall a b.
EitherString a -> (a -> EitherString b) -> EitherString b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b.
EitherString a -> (a -> EitherString b) -> EitherString b
>>= :: forall a b.
EitherString a -> (a -> EitherString b) -> EitherString b
$c>> :: forall a b. EitherString a -> EitherString b -> EitherString b
>> :: forall a b. EitherString a -> EitherString b -> EitherString b
$creturn :: forall a. a -> EitherString a
return :: forall a. a -> EitherString a
Monad)

instance Fail.MonadFail EitherString where
  fail :: forall a. String -> EitherString a
fail = Either String a -> EitherString a
forall a. Either String a -> EitherString a
EitherString (Either String a -> EitherString a)
-> (String -> Either String a) -> String -> EitherString a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either String a
forall a b. a -> Either a b
Left

-- | Apply 'fromLLVM' in a loop, warning on failures
fromLLVMWithWarnings ::
  ( ?lc :: TypeContext
  , HasPtrWidth wptr
  ) =>
  [L.Declare] ->
  OverrideSim p sym ext rtp l a [SomeDeclare]
fromLLVMWithWarnings :: forall (wptr :: Natural) p sym ext rtp (l :: Ctx CrucibleType)
       (a :: CrucibleType).
(?lc::TypeContext, HasPtrWidth wptr) =>
[Declare] -> OverrideSim p sym ext rtp l a [SomeDeclare]
fromLLVMWithWarnings [Declare]
decls =
  ([Maybe SomeDeclare] -> [SomeDeclare])
-> OverrideSim p sym ext rtp l a [Maybe SomeDeclare]
-> OverrideSim p sym ext rtp l a [SomeDeclare]
forall a b.
(a -> b)
-> OverrideSim p sym ext rtp l a a
-> OverrideSim p sym ext rtp l a b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe SomeDeclare] -> [SomeDeclare]
forall a. [Maybe a] -> [a]
Maybe.catMaybes (OverrideSim p sym ext rtp l a [Maybe SomeDeclare]
 -> OverrideSim p sym ext rtp l a [SomeDeclare])
-> OverrideSim p sym ext rtp l a [Maybe SomeDeclare]
-> OverrideSim p sym ext rtp l a [SomeDeclare]
forall a b. (a -> b) -> a -> b
$
    [Declare]
-> (Declare -> OverrideSim p sym ext rtp l a (Maybe SomeDeclare))
-> OverrideSim p sym ext rtp l a [Maybe SomeDeclare]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Declare]
decls ((Declare -> OverrideSim p sym ext rtp l a (Maybe SomeDeclare))
 -> OverrideSim p sym ext rtp l a [Maybe SomeDeclare])
-> (Declare -> OverrideSim p sym ext rtp l a (Maybe SomeDeclare))
-> OverrideSim p sym ext rtp l a [Maybe SomeDeclare]
forall a b. (a -> b) -> a -> b
$ \Declare
decl -> do
      case Declare -> EitherString SomeDeclare
forall (wptr :: Natural) (m :: Type -> Type).
(?lc::TypeContext, HasPtrWidth wptr, MonadFail m) =>
Declare -> m SomeDeclare
fromLLVM Declare
decl of
        EitherString (Left String
err) -> 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
          let msg :: String
msg = [String] -> String
unlines [String
"Unliftable LLVM declaration", Declare -> String
forall a. Show a => a -> String
show Declare
decl, ShowS
forall a. Show a => a -> String
show String
err]
          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
msg
          Maybe SomeDeclare
-> OverrideSim p sym ext rtp l a (Maybe SomeDeclare)
forall a. a -> OverrideSim p sym ext rtp l a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Maybe SomeDeclare
forall a. Maybe a
Nothing
        EitherString (Right SomeDeclare
d) ->
          Maybe SomeDeclare
-> OverrideSim p sym ext rtp l a (Maybe SomeDeclare)
forall a. a -> OverrideSim p sym ext rtp l a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SomeDeclare -> Maybe SomeDeclare
forall a. a -> Maybe a
Just SomeDeclare
d)