{-# 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 )
data CError =
ClangError Int String String
| LLVMParseError LLVM.Error
| MissingFun String
| BadFun String
Bool
| 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")
data SupplyMainArguments
= NoArguments
| EmptyArguments
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
}
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 }
]
}