{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}

module Crux.LLVM.Log
  ( CruxLLVMLogMessage (..),
    SupportsCruxLLVMLogMessage,
    cruxLLVMLogMessageToSayWhat,
    sayCruxLLVM,
  )
where

import Crux.Log (SayLevel (..), SayWhat (..), cruxLogTag)
import qualified Crux.Log as Log
import Data.Aeson (ToJSON)
import Data.Text as Text (Text, pack, unwords)
import GHC.Generics (Generic)

data CruxLLVMLogMessage
  = Breakpoint Text
  | ClangInvocation [Text]
  | Executable Text
  | FailedToBuildCounterexampleExecutable
  | SimulatingFunction Text
  | UsingPointerWidthForFile Integer Text
  | TranslationWarning Text Text Text -- Function name, position, msg
  deriving ( (forall x. CruxLLVMLogMessage -> Rep CruxLLVMLogMessage x)
-> (forall x. Rep CruxLLVMLogMessage x -> CruxLLVMLogMessage)
-> Generic CruxLLVMLogMessage
forall x. Rep CruxLLVMLogMessage x -> CruxLLVMLogMessage
forall x. CruxLLVMLogMessage -> Rep CruxLLVMLogMessage x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CruxLLVMLogMessage -> Rep CruxLLVMLogMessage x
from :: forall x. CruxLLVMLogMessage -> Rep CruxLLVMLogMessage x
$cto :: forall x. Rep CruxLLVMLogMessage x -> CruxLLVMLogMessage
to :: forall x. Rep CruxLLVMLogMessage x -> CruxLLVMLogMessage
Generic, [CruxLLVMLogMessage] -> Value
[CruxLLVMLogMessage] -> Encoding
CruxLLVMLogMessage -> Bool
CruxLLVMLogMessage -> Value
CruxLLVMLogMessage -> Encoding
(CruxLLVMLogMessage -> Value)
-> (CruxLLVMLogMessage -> Encoding)
-> ([CruxLLVMLogMessage] -> Value)
-> ([CruxLLVMLogMessage] -> Encoding)
-> (CruxLLVMLogMessage -> Bool)
-> ToJSON CruxLLVMLogMessage
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: CruxLLVMLogMessage -> Value
toJSON :: CruxLLVMLogMessage -> Value
$ctoEncoding :: CruxLLVMLogMessage -> Encoding
toEncoding :: CruxLLVMLogMessage -> Encoding
$ctoJSONList :: [CruxLLVMLogMessage] -> Value
toJSONList :: [CruxLLVMLogMessage] -> Value
$ctoEncodingList :: [CruxLLVMLogMessage] -> Encoding
toEncodingList :: [CruxLLVMLogMessage] -> Encoding
$comitField :: CruxLLVMLogMessage -> Bool
omitField :: CruxLLVMLogMessage -> Bool
ToJSON )

type SupportsCruxLLVMLogMessage msgs =
  (?injectCruxLLVMLogMessage :: CruxLLVMLogMessage -> msgs)

sayCruxLLVM ::
  Log.Logs msgs =>
  SupportsCruxLLVMLogMessage msgs =>
  CruxLLVMLogMessage ->
  IO ()
sayCruxLLVM :: forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxLLVMLogMessage -> IO ()
sayCruxLLVM CruxLLVMLogMessage
msg =
  let ?injectMessage = SupportsCruxLLVMLogMessage msgs
?injectMessage::CruxLLVMLogMessage -> msgs
CruxLLVMLogMessage -> msgs
?injectCruxLLVMLogMessage
   in CruxLLVMLogMessage -> IO ()
forall msgs msg.
(Logs msgs, ?injectMessage::msg -> msgs) =>
msg -> IO ()
Log.say CruxLLVMLogMessage
msg

clangLogTag :: Text
clangLogTag :: Text
clangLogTag = Text
"CLANG"

cruxLLVMLogMessageToSayWhat :: CruxLLVMLogMessage -> SayWhat
cruxLLVMLogMessageToSayWhat :: CruxLLVMLogMessage -> SayWhat
cruxLLVMLogMessageToSayWhat (ClangInvocation [Text]
params) =
  SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Noisily Text
clangLogTag ([Text] -> Text
Text.unwords [Text]
params)
cruxLLVMLogMessageToSayWhat (Breakpoint Text
line) =
  SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Simply Text
cruxLogTag (Text
"*** break on line: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
line)
cruxLLVMLogMessageToSayWhat (Executable Text
exe) =
  SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Simply Text
cruxLogTag (Text
"*** debug executable: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
exe)
cruxLLVMLogMessageToSayWhat CruxLLVMLogMessage
FailedToBuildCounterexampleExecutable =
  SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Fail Text
cruxLogTag Text
"Failed to build counterexample executable"
cruxLLVMLogMessageToSayWhat (SimulatingFunction Text
function) =
  SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Simply Text
cruxLogTag (Text
"Simulating function " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
function)
cruxLLVMLogMessageToSayWhat (UsingPointerWidthForFile Integer
width Text
file) =
  SayLevel -> Text -> Text -> SayWhat
SayWhat
    SayLevel
Simply
    Text
cruxLogTag
    ( [Text] -> Text
Text.unwords
        [ Text
"Using pointer width:",
          String -> Text
pack (Integer -> String
forall a. Show a => a -> String
show Integer
width),
          Text
"for file",
          Text
file
        ]
    )
cruxLLVMLogMessageToSayWhat (TranslationWarning Text
nm Text
p Text
msg) =
  SayLevel -> Text -> Text -> SayWhat
SayWhat SayLevel
Warn Text
cruxLogTag
    ( [Text] -> Text
Text.unwords
        [ Text
"Translation warning at"
        , Text
p
        , Text
"in"
        , Text
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
":"
        , Text
msg
        ]
    )