{-# 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 Int -> CError -> ShowS
[CError] -> ShowS
CError -> FilePath
(Int -> CError -> ShowS)
-> (CError -> FilePath) -> ([CError] -> ShowS) -> Show CError
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CError -> ShowS
showsPrec :: Int -> CError -> ShowS
$cshow :: CError -> FilePath
show :: CError -> FilePath
$cshowList :: [CError] -> ShowS
showList :: [CError] -> ShowS
Show

instance Exception CError where
  displayException :: CError -> FilePath
displayException = CError -> FilePath
ppCError

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


throwCError :: MonadIO m => CError -> m b
throwCError :: forall (m :: * -> *) b. MonadIO m => CError -> m b
throwCError CError
e = IO b -> m b
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (CError -> IO b
forall e a. Exception e => e -> IO a
throwIO CError
e)


abnormalExitBehaviorSpec :: ValueSpec AbnormalExitBehavior
abnormalExitBehaviorSpec :: ValueSpec AbnormalExitBehavior
abnormalExitBehaviorSpec =
  (AbnormalExitBehavior
AlwaysFail AbnormalExitBehavior
-> ValueSpec () -> ValueSpec AbnormalExitBehavior
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"always-fail") ValueSpec AbnormalExitBehavior
-> ValueSpec AbnormalExitBehavior -> ValueSpec AbnormalExitBehavior
forall a. ValueSpec a -> ValueSpec a -> ValueSpec a
forall (f :: * -> *) a. Alt f => f a -> f a -> f a
<!>
  (AbnormalExitBehavior
OnlyAssertFail AbnormalExitBehavior
-> ValueSpec () -> ValueSpec AbnormalExitBehavior
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"only-assert-fail") ValueSpec AbnormalExitBehavior
-> ValueSpec AbnormalExitBehavior -> ValueSpec AbnormalExitBehavior
forall a. ValueSpec a -> ValueSpec a -> ValueSpec a
forall (f :: * -> *) a. Alt f => f a -> f a -> f a
<!>
  (AbnormalExitBehavior
NeverFail AbnormalExitBehavior
-> ValueSpec () -> ValueSpec AbnormalExitBehavior
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"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 Int -> SupplyMainArguments -> ShowS
[SupplyMainArguments] -> ShowS
SupplyMainArguments -> FilePath
(Int -> SupplyMainArguments -> ShowS)
-> (SupplyMainArguments -> FilePath)
-> ([SupplyMainArguments] -> ShowS)
-> Show SupplyMainArguments
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SupplyMainArguments -> ShowS
showsPrec :: Int -> SupplyMainArguments -> ShowS
$cshow :: SupplyMainArguments -> FilePath
show :: SupplyMainArguments -> FilePath
$cshowList :: [SupplyMainArguments] -> ShowS
showList :: [SupplyMainArguments] -> ShowS
Show

supplyMainArgumentsSpec :: ValueSpec SupplyMainArguments
supplyMainArgumentsSpec :: ValueSpec SupplyMainArguments
supplyMainArgumentsSpec =
  (SupplyMainArguments
NoArguments SupplyMainArguments
-> ValueSpec () -> ValueSpec SupplyMainArguments
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"none") ValueSpec SupplyMainArguments
-> ValueSpec SupplyMainArguments -> ValueSpec SupplyMainArguments
forall a. ValueSpec a -> ValueSpec a -> ValueSpec a
forall (f :: * -> *) a. Alt f => f a -> f a -> f a
<!>
  (SupplyMainArguments
EmptyArguments SupplyMainArguments
-> ValueSpec () -> ValueSpec SupplyMainArguments
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"empty")

indeterminateLoadBehaviorSpec :: ValueSpec IndeterminateLoadBehavior
indeterminateLoadBehaviorSpec :: ValueSpec IndeterminateLoadBehavior
indeterminateLoadBehaviorSpec =
  (IndeterminateLoadBehavior
StableSymbolic IndeterminateLoadBehavior
-> ValueSpec () -> ValueSpec IndeterminateLoadBehavior
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"stable-symbolic") ValueSpec IndeterminateLoadBehavior
-> ValueSpec IndeterminateLoadBehavior
-> ValueSpec IndeterminateLoadBehavior
forall a. ValueSpec a -> ValueSpec a -> ValueSpec a
forall (f :: * -> *) a. Alt f => f a -> f a -> f a
<!>
  (IndeterminateLoadBehavior
UnstableSymbolic IndeterminateLoadBehavior
-> ValueSpec () -> ValueSpec IndeterminateLoadBehavior
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"unstable-symbolic")

data LLVMOptions = LLVMOptions
  { LLVMOptions -> FilePath
clangBin   :: FilePath
  , LLVMOptions -> FilePath
linkBin    :: FilePath
  , LLVMOptions -> [FilePath]
clangOpts  :: [String]
  , LLVMOptions -> FilePath
libDir     :: FilePath
  , LLVMOptions -> [FilePath]
incDirs    :: [FilePath]
  , LLVMOptions -> Maybe FilePath
targetArch :: Maybe String
  , LLVMOptions -> [FilePath]
ubSanitizers :: [String]
  , LLVMOptions -> IntrinsicsOptions
intrinsicsOpts :: IntrinsicsOptions
  , LLVMOptions -> MemOptions
memOpts        :: MemOptions
  , LLVMOptions -> TranslationOptions
transOpts      :: TranslationOptions
  , LLVMOptions -> FilePath
entryPoint :: String
  , LLVMOptions -> Bool
lazyCompile :: Bool
  , LLVMOptions -> Bool
noCompile :: Bool
  , LLVMOptions -> Int
optLevel :: Int
  , LLVMOptions -> Maybe FilePath
symFSRoot :: Maybe FilePath
  , LLVMOptions -> SupplyMainArguments
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 :: IO FilePath
findDefaultLibDir = IO FilePath
getDirRelativeToBin IO FilePath -> IO FilePath -> IO FilePath
forall a. IO a -> IO a -> IO a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IO FilePath
getCabalDataDir
  where
    getDirRelativeToBin :: IO FilePath
    getDirRelativeToBin :: IO FilePath
getDirRelativeToBin = do
      FilePath
binDir <- ShowS
takeDirectory ShowS -> IO FilePath -> IO FilePath
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` IO FilePath
getExecutablePath
      let libDirPrefix :: FilePath
libDirPrefix = ShowS
normalise ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FilePath] -> FilePath
joinPath ([FilePath] -> FilePath) -> (FilePath -> [FilePath]) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FilePath] -> [FilePath]
forall a. HasCallStack => [a] -> [a]
init ([FilePath] -> [FilePath])
-> (FilePath -> [FilePath]) -> FilePath -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
splitPath ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FilePath
binDir
          libDir :: FilePath
libDir       = FilePath
libDirPrefix FilePath -> ShowS
</> FilePath
cSrc
      Bool
libDirExists <- FilePath -> IO Bool
doesDirectoryExist FilePath
libDir
      Bool -> IO ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
libDirExists
      pure FilePath
libDir

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

    cSrc :: FilePath
    cSrc :: FilePath
cSrc = FilePath
"c-src"

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

         FilePath
linkBin  <- Text
-> ValueSpec FilePath -> FilePath -> Text -> SectionsSpec FilePath
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
Crux.section Text
"llvm-link" ValueSpec FilePath
Crux.fileSpec FilePath
"llvm-link"
                     Text
"Binary to use for `llvm-link`."

         [FilePath]
clangOpts <- Text
-> ValueSpec [FilePath]
-> [FilePath]
-> Text
-> SectionsSpec [FilePath]
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
Crux.section Text
"clang-opts"
                                    (ValueSpec FilePath -> ValueSpec [FilePath]
forall a. ValueSpec a -> ValueSpec [a]
Crux.oneOrList ValueSpec FilePath
Crux.stringSpec) []
                      Text
"Additional options for `clang`."

         FilePath
libDir <- Text
-> ValueSpec FilePath -> FilePath -> Text -> SectionsSpec FilePath
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
Crux.section Text
"lib-dir" ValueSpec FilePath
Crux.dirSpec FilePath
libDirDefault
                   Text
"Locations of `crux-llvm` support library."

         [FilePath]
incDirs <- Text
-> ValueSpec [FilePath]
-> [FilePath]
-> Text
-> SectionsSpec [FilePath]
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
Crux.section Text
"include-dirs"
                        (ValueSpec FilePath -> ValueSpec [FilePath]
forall a. ValueSpec a -> ValueSpec [a]
Crux.oneOrList ValueSpec FilePath
Crux.dirSpec) []
                    Text
"Additional include directories."

         Maybe FilePath
targetArch <- Text -> ValueSpec FilePath -> Text -> SectionsSpec (Maybe FilePath)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
Crux.sectionMaybe Text
"target-architecture" ValueSpec FilePath
Crux.stringSpec
                       Text
"Target architecture to pass to LLVM build operations.\
                       \ Default is no specification for current system architecture"

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

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

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

         FilePath
entryPoint <- Text
-> ValueSpec FilePath -> FilePath -> Text -> SectionsSpec FilePath
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
Crux.section Text
"entry-point" ValueSpec FilePath
Crux.stringSpec FilePath
"main"
                           Text
"Name of the entry point function to begin simulation."

         Bool
lazyCompile <- Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
Crux.section Text
"lazy-compile" ValueSpec Bool
Crux.yesOrNoSpec Bool
False
                           Text
"Avoid compiling bitcode from source if intermediate files already exist"

         Bool
noCompile <- Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
Crux.section Text
"no-compile" ValueSpec Bool
Crux.yesOrNoSpec Bool
False
                        Text
"Treat the input file as an LLVM module, do not compile it"

         [FilePath]
ubSanitizers <- Text
-> ValueSpec [FilePath]
-> [FilePath]
-> Text
-> SectionsSpec [FilePath]
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
Crux.section Text
"ub-sanitizers" (ValueSpec FilePath -> ValueSpec [FilePath]
forall a. ValueSpec a -> ValueSpec [a]
Crux.listSpec ValueSpec FilePath
Crux.stringSpec) []
                           Text
"Undefined Behavior sanitizers to enable in `clang`"

         Int
optLevel <- Text -> ValueSpec Int -> Int -> Text -> SectionsSpec Int
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
Crux.section Text
"opt-level" ValueSpec Int
forall a. Num a => ValueSpec a
Crux.numSpec Int
1
                           Text
"Optimization level to request from `clang`"

         Maybe FilePath
symFSRoot <- Text -> ValueSpec FilePath -> Text -> SectionsSpec (Maybe FilePath)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
Crux.sectionMaybe Text
"symbolic-fs-root" ValueSpec FilePath
Crux.stringSpec
                      Text
"The root of a symbolic filesystem to make available to\
                      \ the program during symbolic execution"

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

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

   , cfgEnv :: [EnvDescr LLVMOptions]
Crux.cfgEnv  =
      [ FilePath
-> FilePath
-> (FilePath -> OptSetter LLVMOptions)
-> EnvDescr LLVMOptions
forall opts.
FilePath
-> FilePath -> (FilePath -> OptSetter opts) -> EnvDescr opts
Crux.EnvVar FilePath
"CLANG"      FilePath
"Binary to use for `clang`."
        ((FilePath -> OptSetter LLVMOptions) -> EnvDescr LLVMOptions)
-> (FilePath -> OptSetter LLVMOptions) -> EnvDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
v LLVMOptions
opts -> OptSetter LLVMOptions
forall a b. b -> Either a b
Right LLVMOptions
opts { clangBin = v }

      , FilePath
-> FilePath
-> (FilePath -> OptSetter LLVMOptions)
-> EnvDescr LLVMOptions
forall opts.
FilePath
-> FilePath -> (FilePath -> OptSetter opts) -> EnvDescr opts
Crux.EnvVar FilePath
"CLANG_OPTS" FilePath
"Options to pass to `clang`."
        ((FilePath -> OptSetter LLVMOptions) -> EnvDescr LLVMOptions)
-> (FilePath -> OptSetter LLVMOptions) -> EnvDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
v LLVMOptions
opts -> OptSetter LLVMOptions
forall a b. b -> Either a b
Right LLVMOptions
opts { clangOpts = words v }

      , FilePath
-> FilePath
-> (FilePath -> OptSetter LLVMOptions)
-> EnvDescr LLVMOptions
forall opts.
FilePath
-> FilePath -> (FilePath -> OptSetter opts) -> EnvDescr opts
Crux.EnvVar FilePath
"LLVM_LINK" FilePath
"Use this binary to link LLVM bitcode (`llvm-link`)."
        ((FilePath -> OptSetter LLVMOptions) -> EnvDescr LLVMOptions)
-> (FilePath -> OptSetter LLVMOptions) -> EnvDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
v LLVMOptions
opts -> OptSetter LLVMOptions
forall a b. b -> Either a b
Right LLVMOptions
opts { linkBin = v }

      ]

   , cfgCmdLineFlag :: [OptDescr LLVMOptions]
Crux.cfgCmdLineFlag =
      [ FilePath
-> [FilePath]
-> FilePath
-> ArgDescr LLVMOptions
-> OptDescr LLVMOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Crux.Option [Char
'I'] [FilePath
"include-dirs"]
        FilePath
"Additional include directories."
        (ArgDescr LLVMOptions -> OptDescr LLVMOptions)
-> ArgDescr LLVMOptions -> OptDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter LLVMOptions) -> ArgDescr LLVMOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
Crux.ReqArg FilePath
"DIR"
        ((FilePath -> OptSetter LLVMOptions) -> ArgDescr LLVMOptions)
-> (FilePath -> OptSetter LLVMOptions) -> ArgDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
d LLVMOptions
opts -> OptSetter LLVMOptions
forall a b. b -> Either a b
Right LLVMOptions
opts { incDirs = d : incDirs opts }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr LLVMOptions
-> OptDescr LLVMOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Crux.Option [] [FilePath
"target"]
        FilePath
"Target architecture to pass to LLVM build operations"
        (ArgDescr LLVMOptions -> OptDescr LLVMOptions)
-> ArgDescr LLVMOptions -> OptDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Maybe FilePath -> OptSetter LLVMOptions)
-> ArgDescr LLVMOptions
forall a. FilePath -> (Maybe FilePath -> OptSetter a) -> ArgDescr a
Crux.OptArg FilePath
"ARCH"
        ((Maybe FilePath -> OptSetter LLVMOptions) -> ArgDescr LLVMOptions)
-> (Maybe FilePath -> OptSetter LLVMOptions)
-> ArgDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ \Maybe FilePath
a LLVMOptions
opts -> OptSetter LLVMOptions
forall a b. b -> Either a b
Right LLVMOptions
opts { targetArch = a }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr LLVMOptions
-> OptDescr LLVMOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Crux.Option [] [FilePath
"lax-pointers"]
        FilePath
"Turn on lax rules for pointer comparisons"
        (ArgDescr LLVMOptions -> OptDescr LLVMOptions)
-> ArgDescr LLVMOptions -> OptDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ OptSetter LLVMOptions -> ArgDescr LLVMOptions
forall a. OptSetter a -> ArgDescr a
Crux.NoArg
        (OptSetter LLVMOptions -> ArgDescr LLVMOptions)
-> OptSetter LLVMOptions -> ArgDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ \LLVMOptions
opts -> OptSetter LLVMOptions
forall a b. b -> Either a b
Right LLVMOptions
opts{ memOpts = laxPointerMemOptions }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr LLVMOptions
-> OptDescr LLVMOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Crux.Option [] [FilePath
"lax-arithmetic"]
        FilePath
"Turn on lax rules for arithemetic overflow"
        (ArgDescr LLVMOptions -> OptDescr LLVMOptions)
-> ArgDescr LLVMOptions -> OptDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ OptSetter LLVMOptions -> ArgDescr LLVMOptions
forall a. OptSetter a -> ArgDescr a
Crux.NoArg
        (OptSetter LLVMOptions -> ArgDescr LLVMOptions)
-> OptSetter LLVMOptions -> ArgDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ \LLVMOptions
opts -> OptSetter LLVMOptions
forall a b. b -> Either a b
Right LLVMOptions
opts { transOpts = (transOpts opts) { laxArith = True } }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr LLVMOptions
-> OptDescr LLVMOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Crux.Option [] [FilePath
"opt-loop-merge"]
        FilePath
"Insert merge blocks in loops with early exits"
        (ArgDescr LLVMOptions -> OptDescr LLVMOptions)
-> ArgDescr LLVMOptions -> OptDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ OptSetter LLVMOptions -> ArgDescr LLVMOptions
forall a. OptSetter a -> ArgDescr a
Crux.NoArg
        (OptSetter LLVMOptions -> ArgDescr LLVMOptions)
-> OptSetter LLVMOptions -> ArgDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ \LLVMOptions
opts -> OptSetter LLVMOptions
forall a b. b -> Either a b
Right LLVMOptions
opts { transOpts = (transOpts opts) { optLoopMerge = True } }

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

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr LLVMOptions
-> OptDescr LLVMOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Crux.Option [] [FilePath
"no-compile"]
        FilePath
"Treat the input file as an LLVM module, do not compile it"
        (ArgDescr LLVMOptions -> OptDescr LLVMOptions)
-> ArgDescr LLVMOptions -> OptDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ OptSetter LLVMOptions -> ArgDescr LLVMOptions
forall a. OptSetter a -> ArgDescr a
Crux.NoArg
        (OptSetter LLVMOptions -> ArgDescr LLVMOptions)
-> OptSetter LLVMOptions -> ArgDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ \LLVMOptions
opts -> OptSetter LLVMOptions
forall a b. b -> Either a b
Right LLVMOptions
opts{ noCompile = True }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr LLVMOptions
-> OptDescr LLVMOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Crux.Option [] [FilePath
"entry-point"]
        FilePath
"Name of the entry point to begin simulation"
        (ArgDescr LLVMOptions -> OptDescr LLVMOptions)
-> ArgDescr LLVMOptions -> OptDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter LLVMOptions) -> ArgDescr LLVMOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
Crux.ReqArg FilePath
"SYMBOL"
        ((FilePath -> OptSetter LLVMOptions) -> ArgDescr LLVMOptions)
-> (FilePath -> OptSetter LLVMOptions) -> ArgDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
s LLVMOptions
opts -> OptSetter LLVMOptions
forall a b. b -> Either a b
Right LLVMOptions
opts{ entryPoint = s }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr LLVMOptions
-> OptDescr LLVMOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Crux.Option FilePath
"O" []
        FilePath
"Optimization level for `clang`"
        (ArgDescr LLVMOptions -> OptDescr LLVMOptions)
-> ArgDescr LLVMOptions -> OptDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter LLVMOptions) -> ArgDescr LLVMOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
Crux.ReqArg FilePath
"NUM"
        ((FilePath -> OptSetter LLVMOptions) -> ArgDescr LLVMOptions)
-> (FilePath -> OptSetter LLVMOptions) -> ArgDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Int -> LLVMOptions -> LLVMOptions)
-> FilePath
-> OptSetter LLVMOptions
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
Crux.parsePosNum FilePath
"NUM"
        ((Int -> LLVMOptions -> LLVMOptions)
 -> FilePath -> OptSetter LLVMOptions)
-> (Int -> LLVMOptions -> LLVMOptions)
-> FilePath
-> OptSetter LLVMOptions
forall a b. (a -> b) -> a -> b
$ \Int
v LLVMOptions
opts -> LLVMOptions
opts { optLevel = v }

      , FilePath
-> [FilePath]
-> FilePath
-> ArgDescr LLVMOptions
-> OptDescr LLVMOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Crux.Option [] [FilePath
"symbolic-fs-root"]
        FilePath
"The root of a symbolic filesystem to make available to the program during symbolic execution"
        (ArgDescr LLVMOptions -> OptDescr LLVMOptions)
-> ArgDescr LLVMOptions -> OptDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Maybe FilePath -> OptSetter LLVMOptions)
-> ArgDescr LLVMOptions
forall a. FilePath -> (Maybe FilePath -> OptSetter a) -> ArgDescr a
Crux.OptArg FilePath
"DIR"
        ((Maybe FilePath -> OptSetter LLVMOptions) -> ArgDescr LLVMOptions)
-> (Maybe FilePath -> OptSetter LLVMOptions)
-> ArgDescr LLVMOptions
forall a b. (a -> b) -> a -> b
$ \Maybe FilePath
a LLVMOptions
opts -> OptSetter LLVMOptions
forall a b. b -> Either a b
Right LLVMOptions
opts { symFSRoot = a }
      ]
   }