Crux.LLVM.Compile

Documentation

isCPlusPlus :: FilePath -> Bool

anyCPPFiles :: [FilePath] -> Bool

getClang :: IO FilePath

attempt to find Clang executable by searching the file system throw an error if it cannot be found this way. (NOTE: do not look for environment var CLANG. That is assumed to be tried already.)

runClang :: Logs msgs => SupportsCruxLLVMLogMessage msgs => LLVMOptions -> [String] -> IO ()

llvmLink :: LLVMOptions -> [FilePath] -> FilePath -> IO ()

parseLLVMLinkVersion :: String -> String

llvmLinkVersion :: LLVMOptions -> IO String

genBitCode :: Logs msgs => SupportsCruxLLVMLogMessage msgs => CruxOptions -> LLVMOptions -> IO FilePath

Generates compiled LLVM bitcode for the set of input files specified in the CruxOptions argument, writing the output to a pre-determined filename in the build directory specified in CruxOptions.

genBitCodeToFile :: Logs msgs => SupportsCruxLLVMLogMessage msgs => String -> [FilePath] -> CruxOptions -> LLVMOptions -> Bool -> IO FilePath

Given the target filename and a list of input files, along with the crux and llvm options, bitcode-compile each input .c file and link the resulting files, along with any input .ll files into the target bitcode (BC) file. Returns the filepath of the target bitcode file.

crucibleFlagsFromSrc :: FilePath -> IO [String]

A C source file being compiled and evaluated by crux can contain zero or more lines matching the following:

  /* CRUCIBLE clang_flags: {FLAGS} */
  // CRUCIBLE clang_flags: {FLAGS}
  /* CRUX clang_flags: {FLAGS} */
  // CRUX clang_flags: {FLAGS}

Note that the "clang_flags" portion is case-insensitive, although the CRUCIBLE or CRUX prefix is case sensitive and must be capitalized.

All {FLAGS} will be collected as a set of space-separated words. Flags from multiple lines will be concatenated together (without any attempt to eliminate duplicates or conflicts) and the result will be passed as additional flags to the clang compilation of the source by Crux.

The above line matching is whitespace-sensitive and case-sensitive. When C-style comment syntax is used, the comment must be closed on the same line as it was opened (although there is no line length restriction).

makeCounterExamplesLLVM :: Logs msgs => SupportsCruxLLVMLogMessage msgs => CruxOptions -> LLVMOptions -> CruxSimulationResult -> IO ()

buildModelExes :: Logs msgs => SupportsCruxLLVMLogMessage msgs => CruxOptions -> LLVMOptions -> String -> String -> IO (FilePath, FilePath)

ppValsC :: BaseTypeRepr ty -> Vals ty -> [String]

ppModelC :: ModelView -> String

llvmModelTypes :: [Some BaseTypeRepr]