{-# 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 )
import qualified Crux
import qualified Crux.Log as Log
import Crux.Config.Common (CruxOptions(..), OutputOptions)
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
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 }
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))
[] -> 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)