{-# Language DeriveAnyClass #-}
{-# Language DeriveGeneric #-}
{-# Language ImplicitParams #-}
{-# Language LambdaCase #-}
{-# Language OverloadedStrings #-}
{-# Language RankNTypes #-}

module CruxLLVMMain
  ( CruxLLVMLogging
  , cruxLLVMLoggingToSayWhat
  , defaultOutputConfig
  , mainWithOptions
  , mainWithOutputTo
  , mainWithOutputConfig
  , Crux.mkOutputConfig
  , processLLVMOptions
  , withCruxLLVMLogging
  )
  where

import           Data.Aeson ( ToJSON )
import           GHC.Generics ( Generic )
import           System.Directory ( createDirectoryIfMissing )
import           System.Exit ( ExitCode )
import           System.FilePath ( dropExtension, takeFileName, (</>) )
import           System.IO ( Handle )

-- crux
import qualified Crux
import qualified Crux.Log as Log
import           Crux.Config.Common (CruxOptions(..), OutputOptions)

-- local
import           Crux.LLVM.Config
import           Crux.LLVM.Compile
import qualified Crux.LLVM.Log as Log
import           Crux.LLVM.Simulate
import           Paths_crux_llvm (version)


mainWithOutputTo :: Handle -> IO ExitCode
mainWithOutputTo :: Handle -> IO ExitCode
mainWithOutputTo Handle
h = (Maybe OutputOptions -> OutputConfig CruxLLVMLogging)
-> IO ExitCode
mainWithOutputConfig ((Maybe OutputOptions -> OutputConfig CruxLLVMLogging)
 -> IO ExitCode)
-> (Maybe OutputOptions -> OutputConfig CruxLLVMLogging)
-> IO ExitCode
forall a b. (a -> b) -> a -> b
$
  (Handle, Bool)
-> (Handle, Bool)
-> (CruxLLVMLogging -> SayWhat)
-> Maybe OutputOptions
-> OutputConfig CruxLLVMLogging
forall msgs.
ToJSON msgs =>
(Handle, Bool)
-> (Handle, Bool)
-> (msgs -> SayWhat)
-> Maybe OutputOptions
-> OutputConfig msgs
Crux.mkOutputConfig (Handle
h, Bool
True) (Handle
h, Bool
True) CruxLLVMLogging -> SayWhat
cruxLLVMLoggingToSayWhat

data CruxLLVMLogging
  = LoggingCrux Crux.CruxLogMessage
  | LoggingCruxLLVM Log.CruxLLVMLogMessage
  deriving ( (forall x. CruxLLVMLogging -> Rep CruxLLVMLogging x)
-> (forall x. Rep CruxLLVMLogging x -> CruxLLVMLogging)
-> Generic CruxLLVMLogging
forall x. Rep CruxLLVMLogging x -> CruxLLVMLogging
forall x. CruxLLVMLogging -> Rep CruxLLVMLogging x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CruxLLVMLogging -> Rep CruxLLVMLogging x
from :: forall x. CruxLLVMLogging -> Rep CruxLLVMLogging x
$cto :: forall x. Rep CruxLLVMLogging x -> CruxLLVMLogging
to :: forall x. Rep CruxLLVMLogging x -> CruxLLVMLogging
Generic, [CruxLLVMLogging] -> Value
[CruxLLVMLogging] -> Encoding
CruxLLVMLogging -> Bool
CruxLLVMLogging -> Value
CruxLLVMLogging -> Encoding
(CruxLLVMLogging -> Value)
-> (CruxLLVMLogging -> Encoding)
-> ([CruxLLVMLogging] -> Value)
-> ([CruxLLVMLogging] -> Encoding)
-> (CruxLLVMLogging -> Bool)
-> ToJSON CruxLLVMLogging
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: CruxLLVMLogging -> Value
toJSON :: CruxLLVMLogging -> Value
$ctoEncoding :: CruxLLVMLogging -> Encoding
toEncoding :: CruxLLVMLogging -> Encoding
$ctoJSONList :: [CruxLLVMLogging] -> Value
toJSONList :: [CruxLLVMLogging] -> Value
$ctoEncodingList :: [CruxLLVMLogging] -> Encoding
toEncodingList :: [CruxLLVMLogging] -> Encoding
$comitField :: CruxLLVMLogging -> Bool
omitField :: CruxLLVMLogging -> Bool
ToJSON )

cruxLLVMLoggingToSayWhat :: CruxLLVMLogging -> Crux.SayWhat
cruxLLVMLoggingToSayWhat :: CruxLLVMLogging -> SayWhat
cruxLLVMLoggingToSayWhat (LoggingCrux CruxLogMessage
msg) = CruxLogMessage -> SayWhat
Log.cruxLogMessageToSayWhat CruxLogMessage
msg
cruxLLVMLoggingToSayWhat (LoggingCruxLLVM CruxLLVMLogMessage
msg) = CruxLLVMLogMessage -> SayWhat
Log.cruxLLVMLogMessageToSayWhat CruxLLVMLogMessage
msg

defaultOutputConfig :: IO (Maybe OutputOptions -> Log.OutputConfig CruxLLVMLogging)
defaultOutputConfig :: IO (Maybe OutputOptions -> OutputConfig CruxLLVMLogging)
defaultOutputConfig = (CruxLLVMLogging -> SayWhat)
-> IO (Maybe OutputOptions -> OutputConfig CruxLLVMLogging)
forall msgs.
ToJSON msgs =>
(msgs -> SayWhat) -> IO (Maybe OutputOptions -> OutputConfig msgs)
Crux.defaultOutputConfig CruxLLVMLogging -> SayWhat
cruxLLVMLoggingToSayWhat

withCruxLLVMLogging ::
  (
    Log.SupportsCruxLogMessage CruxLLVMLogging =>
    Log.SupportsCruxLLVMLogMessage CruxLLVMLogging =>
    a
  ) -> a
withCruxLLVMLogging :: forall a.
((SupportsCruxLogMessage CruxLLVMLogging,
  SupportsCruxLLVMLogMessage CruxLLVMLogging) =>
 a)
-> a
withCruxLLVMLogging (SupportsCruxLogMessage CruxLLVMLogging,
 SupportsCruxLLVMLogMessage CruxLLVMLogging) =>
a
a =
  let
    ?injectCruxLogMessage = SupportsCruxLogMessage CruxLLVMLogging
CruxLogMessage -> CruxLLVMLogging
LoggingCrux
    ?injectCruxLLVMLogMessage = SupportsCruxLLVMLogMessage CruxLLVMLogging
CruxLLVMLogMessage -> CruxLLVMLogging
LoggingCruxLLVM
  in a
(SupportsCruxLogMessage CruxLLVMLogging,
 SupportsCruxLLVMLogMessage CruxLLVMLogging) =>
a
a

mainWithOutputConfig ::
  (Maybe OutputOptions -> Log.OutputConfig CruxLLVMLogging) ->
  IO ExitCode
mainWithOutputConfig :: (Maybe OutputOptions -> OutputConfig CruxLLVMLogging)
-> IO ExitCode
mainWithOutputConfig Maybe OutputOptions -> OutputConfig CruxLLVMLogging
mkOutCfg = ((SupportsCruxLogMessage CruxLLVMLogging,
  SupportsCruxLLVMLogMessage CruxLLVMLogging) =>
 IO ExitCode)
-> IO ExitCode
forall a.
((SupportsCruxLogMessage CruxLLVMLogging,
  SupportsCruxLLVMLogMessage CruxLLVMLogging) =>
 a)
-> a
withCruxLLVMLogging (((SupportsCruxLogMessage CruxLLVMLogging,
   SupportsCruxLLVMLogMessage CruxLLVMLogging) =>
  IO ExitCode)
 -> IO ExitCode)
-> ((SupportsCruxLogMessage CruxLLVMLogging,
     SupportsCruxLLVMLogMessage CruxLLVMLogging) =>
    IO ExitCode)
-> IO ExitCode
forall a b. (a -> b) -> a -> b
$ do
  Config LLVMOptions
cfg <- IO (Config LLVMOptions)
llvmCruxConfig
  (Maybe OutputOptions -> OutputConfig CruxLLVMLogging)
-> Text
-> Version
-> Config LLVMOptions
-> (Logs CruxLLVMLogging =>
    (CruxOptions, LLVMOptions) -> IO ExitCode)
-> IO ExitCode
forall msgs opts a.
SupportsCruxLogMessage msgs =>
(Maybe OutputOptions -> OutputConfig msgs)
-> Text
-> Version
-> Config opts
-> (Logs msgs => (CruxOptions, opts) -> IO a)
-> IO a
Crux.loadOptions Maybe OutputOptions -> OutputConfig CruxLLVMLogging
mkOutCfg Text
"crux-llvm" Version
version Config LLVMOptions
cfg Logs CruxLLVMLogging => (CruxOptions, LLVMOptions) -> IO ExitCode
(CruxOptions, LLVMOptions) -> IO ExitCode
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs,
 SupportsCruxLLVMLogMessage msgs) =>
(CruxOptions, LLVMOptions) -> IO ExitCode
mainWithOptions

mainWithOptions ::
  Log.Logs msgs =>
  Log.SupportsCruxLogMessage msgs =>
  Log.SupportsCruxLLVMLogMessage msgs =>
  (CruxOptions, LLVMOptions) -> IO ExitCode
mainWithOptions :: forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs,
 SupportsCruxLLVMLogMessage msgs) =>
(CruxOptions, LLVMOptions) -> IO ExitCode
mainWithOptions (CruxOptions, LLVMOptions)
initOpts =
  do
    (CruxOptions
cruxOpts, LLVMOptions
llvmOpts) <- (CruxOptions, LLVMOptions) -> IO (CruxOptions, LLVMOptions)
processLLVMOptions (CruxOptions, LLVMOptions)
initOpts
    FilePath
bcFile <- CruxOptions -> LLVMOptions -> IO FilePath
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxOptions -> LLVMOptions -> IO FilePath
genBitCode CruxOptions
cruxOpts LLVMOptions
llvmOpts
    CruxSimulationResult
res <- CruxOptions
-> SimulatorCallbacks msgs CruxSimulationResult
-> IO CruxSimulationResult
forall msgs r.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> SimulatorCallbacks msgs r -> IO r
Crux.runSimulator CruxOptions
cruxOpts (SimulatorCallbacks msgs CruxSimulationResult
 -> IO CruxSimulationResult)
-> SimulatorCallbacks msgs CruxSimulationResult
-> IO CruxSimulationResult
forall a b. (a -> b) -> a -> b
$ FilePath
-> LLVMOptions -> SimulatorCallbacks msgs CruxSimulationResult
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
FilePath
-> LLVMOptions -> SimulatorCallbacks msgs CruxSimulationResult
simulateLLVMFile FilePath
bcFile LLVMOptions
llvmOpts
    CruxOptions -> LLVMOptions -> CruxSimulationResult -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxOptions -> LLVMOptions -> CruxSimulationResult -> IO ()
makeCounterExamplesLLVM CruxOptions
cruxOpts LLVMOptions
llvmOpts CruxSimulationResult
res
    Bool -> CruxOptions -> CruxSimulationResult -> IO ExitCode
forall msgs.
Logs msgs =>
Bool -> CruxOptions -> CruxSimulationResult -> IO ExitCode
Crux.postprocessSimResult Bool
True CruxOptions
cruxOpts CruxSimulationResult
res

processLLVMOptions :: (CruxOptions,LLVMOptions) -> IO (CruxOptions,LLVMOptions)
processLLVMOptions :: (CruxOptions, LLVMOptions) -> IO (CruxOptions, LLVMOptions)
processLLVMOptions (CruxOptions
cruxOpts,LLVMOptions
llvmOpts) =
  do -- keep looking for clangBin if it is unset
     FilePath
clangFilePath <- if LLVMOptions -> FilePath
clangBin LLVMOptions
llvmOpts FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
""
                        then IO FilePath
getClang
                        else FilePath -> IO FilePath
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (LLVMOptions -> FilePath
clangBin LLVMOptions
llvmOpts)

     let llvmOpts2 :: LLVMOptions
llvmOpts2 = LLVMOptions
llvmOpts { clangBin = clangFilePath }

     -- update outDir if unset
     FilePath
name <- case CruxOptions -> [FilePath]
Crux.inputFiles CruxOptions
cruxOpts of
               FilePath
x : [FilePath]
_ -> FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FilePath -> FilePath
dropExtension (FilePath -> FilePath
takeFileName FilePath
x))
                          -- use the first file as output directory
               [] -> CError -> IO FilePath
forall (m :: * -> *) b. MonadIO m => CError -> m b
throwCError CError
NoFiles

     let cruxOpts2 :: CruxOptions
cruxOpts2 = if CruxOptions -> FilePath
Crux.outDir CruxOptions
cruxOpts FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
""
                       then CruxOptions
cruxOpts { Crux.outDir = "results" </> name }
                       else CruxOptions
cruxOpts

         odir :: FilePath
odir      = CruxOptions -> FilePath
Crux.outDir CruxOptions
cruxOpts2

     Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True FilePath
odir

     (CruxOptions, LLVMOptions) -> IO (CruxOptions, LLVMOptions)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CruxOptions
cruxOpts2, LLVMOptions
llvmOpts2)