crux-llvm-0.8: src/CruxLLVMMain.hs

{-# 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 h = mainWithOutputConfig $
  Crux.mkOutputConfig (h, True) (h, True) cruxLLVMLoggingToSayWhat

data CruxLLVMLogging
  = LoggingCrux Crux.CruxLogMessage
  | LoggingCruxLLVM Log.CruxLLVMLogMessage
  deriving ( Generic, ToJSON )

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

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

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

mainWithOutputConfig ::
  (Maybe OutputOptions -> Log.OutputConfig CruxLLVMLogging) ->
  IO ExitCode
mainWithOutputConfig mkOutCfg = withCruxLLVMLogging $ do
  cfg <- llvmCruxConfig
  Crux.loadOptions mkOutCfg "crux-llvm" version cfg mainWithOptions

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

processLLVMOptions :: (CruxOptions,LLVMOptions) -> IO (CruxOptions,LLVMOptions)
processLLVMOptions (cruxOpts,llvmOpts) =
  do -- keep looking for clangBin if it is unset
     clangFilePath <- if clangBin llvmOpts == ""
                        then getClang
                        else return (clangBin llvmOpts)

     let llvmOpts2 = llvmOpts { clangBin = clangFilePath }

     -- update outDir if unset
     name <- case Crux.inputFiles cruxOpts of
               x : _ -> pure (dropExtension (takeFileName x))
                          -- use the first file as output directory
               [] -> throwCError NoFiles

     let cruxOpts2 = if Crux.outDir cruxOpts == ""
                       then cruxOpts { Crux.outDir = "results" </> name }
                       else cruxOpts

         odir      = Crux.outDir cruxOpts2

     createDirectoryIfMissing True odir

     return (cruxOpts2, llvmOpts2)