{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}

module Crux.LLVM.Config where

import           Config.Schema
import           Control.Applicative ( Alternative(..) )
import           Control.Exception ( Exception, displayException, throwIO )
import           Control.Monad ( guard )
import           Control.Monad.State ( liftIO, MonadIO )
import qualified Data.Text as Text
import           System.Directory ( doesDirectoryExist )
import           System.Environment ( getExecutablePath )
import           System.FilePath ( (</>), joinPath, normalise, splitPath, takeDirectory )

import qualified Data.LLVM.BitCode as LLVM

import           Lang.Crucible.LLVM.Intrinsics ( IntrinsicsOptions(..), AbnormalExitBehavior(..) )
import           Lang.Crucible.LLVM.MemModel ( MemOptions(..), IndeterminateLoadBehavior(..), laxPointerMemOptions )
import           Lang.Crucible.LLVM.Translation ( TranslationOptions(..) )

import qualified Crux
import           Paths_crux_llvm ( getDataDir )


--
-- LLVM specific errors
--
data CError =
    ClangError Int String String
  | LLVMParseError LLVM.Error
  | MissingFun String
  | BadFun String {- The function name -}
           Bool   {- Is is the main() function?
                     If so, we can recommend the use of the
                     `supply-main-arguments` option. -}
  | EnvError String
  | NoFiles
    deriving Show

instance Exception CError where
  displayException = ppCError

ppCError :: CError -> String
ppCError err = case err of
    NoFiles                -> "crux-llvm requires at least one input file."
    EnvError msg           -> msg
    BadFun fnName isMain   -> unlines $
                                [ "The '" ++ fnName ++ "' function should have no arguments"] ++
                                [ "Enable `supply-main-arguments` to relax this restriction"
                                | isMain
                                ]
    MissingFun x           -> "Cannot find code for " ++ show x
    LLVMParseError e       -> LLVM.formatError e
    ClangError n sout serr ->
      unlines $ [ "`clang` compilation failed."
                , "*** Exit code: " ++ show n
                , "*** Standard out:"
                ] ++
                [ "   " ++ l | l <- lines sout ] ++
                [ "*** Standard error:" ] ++
                [ "   " ++ l | l <- lines serr ]


throwCError :: MonadIO m => CError -> m b
throwCError e = liftIO (throwIO e)


abnormalExitBehaviorSpec :: ValueSpec AbnormalExitBehavior
abnormalExitBehaviorSpec =
  (AlwaysFail <$ atomSpec "always-fail") <!>
  (OnlyAssertFail <$ atomSpec "only-assert-fail") <!>
  (NeverFail <$ atomSpec "never-fail")

-- | What sort of @main@ functions should @crux-llvm@ support simulating?
data SupplyMainArguments
  = NoArguments
    -- ^ Only support simulating @main@ functions with the signature
    --   @int main()@. Attempting to simulate a @main@ function that
    --   takes arguments will result in an error. This is @crux-llvm@'s default
    --   behavior.

  | EmptyArguments
    -- ^ Support simulating both @int main()@ and
    --   @int(main argc, char *argv[])@. If simulating the latter, supply the
    --   arguments @argc=0@ and @argv={}@. This is a reasonable choice for
    --   programs whose @main@ function is declared with the latter signature
    --   but never make use of @argc@ or @argv@.
  deriving Show

supplyMainArgumentsSpec :: ValueSpec SupplyMainArguments
supplyMainArgumentsSpec =
  (NoArguments <$ atomSpec "none") <!>
  (EmptyArguments <$ atomSpec "empty")

indeterminateLoadBehaviorSpec :: ValueSpec IndeterminateLoadBehavior
indeterminateLoadBehaviorSpec =
  (StableSymbolic <$ atomSpec "stable-symbolic") <!>
  (UnstableSymbolic <$ atomSpec "unstable-symbolic")

data LLVMOptions = LLVMOptions
  { clangBin   :: FilePath
  , linkBin    :: FilePath
  , clangOpts  :: [String]
  , libDir     :: FilePath
  , incDirs    :: [FilePath]
  , targetArch :: Maybe String
  , ubSanitizers :: [String]
  , intrinsicsOpts :: IntrinsicsOptions
  , memOpts        :: MemOptions
  , transOpts      :: TranslationOptions
  , entryPoint :: String
  , lazyCompile :: Bool
  , noCompile :: Bool
  , optLevel :: Int
  , symFSRoot :: Maybe FilePath
  , supplyMainArguments :: SupplyMainArguments
  }

-- | The @c-src@ directory, which contains @crux-llvm@–specific files such as
-- @crucible.h@, can live in different locations depending on how @crux-llvm@
-- was built. This function looks in a couple of common places:
--
-- 1. A directory relative to the @crux-llvm@ binary itself. This is the case
--    when running a @crux-llvm@ binary distribution. If that can't be found,
--    default to...
--
-- 2. The @data-files@ directory, as reported by @cabal@'s 'getDataDir'
--    function.
--
-- This isn't always guaranteed to work in every situation, but it should cover
-- enough common cases to be useful in practice.
findDefaultLibDir :: IO FilePath
findDefaultLibDir = getDirRelativeToBin <|> getCabalDataDir
  where
    getDirRelativeToBin :: IO FilePath
    getDirRelativeToBin = do
      binDir <- takeDirectory `fmap` getExecutablePath
      let libDirPrefix = normalise . joinPath . init . splitPath $ binDir
          libDir       = libDirPrefix </> cSrc
      libDirExists <- doesDirectoryExist libDir
      guard libDirExists
      pure libDir

    getCabalDataDir :: IO FilePath
    getCabalDataDir = do
      libDirPrefix <- getDataDir
      pure $ libDirPrefix </> cSrc

    cSrc :: FilePath
    cSrc = "c-src"

llvmCruxConfig :: IO (Crux.Config LLVMOptions)
llvmCruxConfig = do
  libDirDefault <- findDefaultLibDir
  return Crux.Config
   { Crux.cfgFile =
      do clangBin <- Crux.section "clang" Crux.fileSpec "clang"
                     "Binary to use for `clang`."

         linkBin  <- Crux.section "llvm-link" Crux.fileSpec "llvm-link"
                     "Binary to use for `llvm-link`."

         clangOpts <- Crux.section "clang-opts"
                                    (Crux.oneOrList Crux.stringSpec) []
                      "Additional options for `clang`."

         libDir <- Crux.section "lib-dir" Crux.dirSpec libDirDefault
                   "Locations of `crux-llvm` support library."

         incDirs <- Crux.section "include-dirs"
                        (Crux.oneOrList Crux.dirSpec) []
                    "Additional include directories."

         targetArch <- Crux.sectionMaybe "target-architecture" Crux.stringSpec
                       "Target architecture to pass to LLVM build operations.\
                       \ Default is no specification for current system architecture"

         intrinsicsOpts <- do abnormalExitBehavior <-
                                Crux.section "abnormal-exit-behavior" abnormalExitBehaviorSpec AlwaysFail
                                  (Text.unwords
                                    [ "Should Crux fail when simulating a function which triggers an"
                                    , "abnormal exit, such as abort()? Possible options are:"
                                    , "'always-fail' (default); 'only-assert-fail', which only fails"
                                    , "when simulating __assert_fail(); and 'never-fail'."
                                    , "The latter two options are primarily useful for SV-COMP."
                                    ])
                              return IntrinsicsOptions{..}

         memOpts <- do laxPointerOrdering <-
                         Crux.section "lax-pointer-ordering" Crux.yesOrNoSpec False
                           "Allow order comparisons between pointers from different allocation blocks"
                       laxConstantEquality <-
                         Crux.section "lax-constant-equality" Crux.yesOrNoSpec False
                           "Allow equality comparisons between pointers to constant data"
                       laxLoadsAndStores <-
                         Crux.section "lax-loads-and-stores" Crux.yesOrNoSpec False
                           "Relax some of Crucible's validity checks for memory loads and stores"
                       indeterminateLoadBehavior <-
                         Crux.section "indeterminate-load-behavior" indeterminateLoadBehaviorSpec StableSymbolic
                           (Text.unwords
                             [ "(Only takes effect is 'lax-loads-and-stores' is enabled.)"
                             , "What should the semantics of reading from uninitialized"
                             , "memory be? Possible options are:"
                             , "'stable-symbolic' (default), which causes all allocations to"
                             , "be initialized with a fresh symbolic value; and"
                             , "'unstable-symbolic', which causes each read from uninitialized"
                             , "memory to return a fresh symbolic value."
                             ])
                       return MemOptions{..}

         transOpts <- do laxArith <-
                           Crux.section "lax-arithmetic" Crux.yesOrNoSpec False
                             "Do not produce proof obligations related to arithmetic overflow, etc."
                         optLoopMerge <-
                           Crux.section "opt-loop-merge" Crux.yesOrNoSpec False
                             "Insert merge blocks in loops with early exits (i.e. breaks or returns). This may improve simulation performance."
                         debugIntrinsics <- Crux.section "debug-intrinsics" Crux.yesOrNoSpec False
                              "Translate statements using certain llvm.dbg intrinsic functions."
                         return TranslationOptions{..}

         entryPoint <- Crux.section "entry-point" Crux.stringSpec "main"
                           "Name of the entry point function to begin simulation."

         lazyCompile <- Crux.section "lazy-compile" Crux.yesOrNoSpec False
                           "Avoid compiling bitcode from source if intermediate files already exist"

         noCompile <- Crux.section "no-compile" Crux.yesOrNoSpec False
                        "Treat the input file as an LLVM module, do not compile it"

         ubSanitizers <- Crux.section "ub-sanitizers" (Crux.listSpec Crux.stringSpec) []
                           "Undefined Behavior sanitizers to enable in `clang`"

         optLevel <- Crux.section "opt-level" Crux.numSpec 1
                           "Optimization level to request from `clang`"

         symFSRoot <- Crux.sectionMaybe "symbolic-fs-root" Crux.stringSpec
                      "The root of a symbolic filesystem to make available to\
                      \ the program during symbolic execution"

         supplyMainArguments <-
           Crux.section "supply-main-arguments" supplyMainArgumentsSpec NoArguments
             (Text.unwords
               [ "One of `none` or `empty` (default: none). If `none`, only"
               , "support simulating `main` entrypoint functions with the"
               , "signature `int main()`. If `empty`, also support simulating"
               , "`int main(int argc, char *argv[])` such that argc=0 and"
               , "argv={} are chosen as the arguments."
               ])

         return LLVMOptions { .. }

   , Crux.cfgEnv  =
      [ Crux.EnvVar "CLANG"      "Binary to use for `clang`."
        $ \v opts -> Right opts { clangBin = v }

      , Crux.EnvVar "CLANG_OPTS" "Options to pass to `clang`."
        $ \v opts -> Right opts { clangOpts = words v }

      , Crux.EnvVar "LLVM_LINK" "Use this binary to link LLVM bitcode (`llvm-link`)."
        $ \v opts -> Right opts { linkBin = v }

      ]

   , Crux.cfgCmdLineFlag =
      [ Crux.Option ['I'] ["include-dirs"]
        "Additional include directories."
        $ Crux.ReqArg "DIR"
        $ \d opts -> Right opts { incDirs = d : incDirs opts }

      , Crux.Option [] ["target"]
        "Target architecture to pass to LLVM build operations"
        $ Crux.OptArg "ARCH"
        $ \a opts -> Right opts { targetArch = a }

      , Crux.Option [] ["lax-pointers"]
        "Turn on lax rules for pointer comparisons"
        $ Crux.NoArg
        $ \opts -> Right opts{ memOpts = laxPointerMemOptions }

      , Crux.Option [] ["lax-arithmetic"]
        "Turn on lax rules for arithemetic overflow"
        $ Crux.NoArg
        $ \opts -> Right opts { transOpts = (transOpts opts) { laxArith = True } }

      , Crux.Option [] ["opt-loop-merge"]
        "Insert merge blocks in loops with early exits"
        $ Crux.NoArg
        $ \opts -> Right opts { transOpts = (transOpts opts) { optLoopMerge = True } }

      , Crux.Option [] ["lazy-compile"]
        "Avoid compiling bitcode from source if intermediate files already exist (default: off)"
        $ Crux.NoArg
        $ \opts -> Right opts{ lazyCompile = True }

      , Crux.Option [] ["no-compile"]
        "Treat the input file as an LLVM module, do not compile it"
        $ Crux.NoArg
        $ \opts -> Right opts{ noCompile = True }

      , Crux.Option [] ["entry-point"]
        "Name of the entry point to begin simulation"
        $ Crux.ReqArg "SYMBOL"
        $ \s opts -> Right opts{ entryPoint = s }

      , Crux.Option "O" []
        "Optimization level for `clang`"
        $ Crux.ReqArg "NUM"
        $ Crux.parsePosNum "NUM"
        $ \v opts -> opts { optLevel = v }

      , Crux.Option [] ["symbolic-fs-root"]
        "The root of a symbolic filesystem to make available to the program during symbolic execution"
        $ Crux.OptArg "DIR"
        $ \a opts -> Right opts { symFSRoot = a }
      ]
   }