crux-llvm-0.8: src/Crux/LLVM/Config.hs
{-# 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 }
]
}