diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,51 @@
+# 0.8 -- 2024-02-05
+
+* Add support for LLVM bitcode files generated by Apple Clang on macOS.
+
+# 0.7 -- 2023-06-26
+
+## New features
+
+* When loading bitcode to execute, we now make use of a new feature
+of `crucible-llvm` which delays the translation of the LLVM bitcode
+until functions are actually called. This should speed up startup
+times and reduce memory usage for verification tasks where a small
+subset of functions in a bitcode module are actually executed.
+
+* Added support for the `cvc5` SMT solver.
+
+* Added support for getting abducts during online goal solving. With
+the `--get-abducts n` option, `crux-llvm` returns `n` abducts for
+each goal that the SMT solver found to be `sat`. An abduct is a formula
+that makes the goal `unsat` (would help the SMT solver prove the goal).
+This feature only works with the `cvc5` SMT solver.
+
+* Support LLVM versions up to 16.
+
+# 0.6
+
+## New features
+
+* Improved support for translating LLVM debug metadata when the
+ `debug-intrinsics` option is enabled, including metadata that defines
+ metadata nodes after they are used.
+
+* Add overrides for certain floating-point operations such as `sin`, `cos`,
+ `tan`, etc. At the solver level, `crux-llvm` treats these as uninterpreted
+ functions, so `crux-llvm` is limited to reasoning about them up to basic,
+ syntactic equivalence checking.
+
+* Certain error messages now print the call stack of functions leading up to
+ the error.
+
+## Bug fixes
+
+* Make `--help` and `--version` respect the `--no-colors` flag.
+
+## Library changes
+
+* `LLVMConfig` now has an `indeterminateLoadBehavior` flag to control the
+ `MemOptions` option of the same name. Refer to the `crucible-llvm` changelog
+ for more details.
+* A `?memOpts :: MemOptions` constraint has been added to
+ `Crux.LLVM.Simulate.checkFun`.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2018-2022 Galois Inc.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+ * Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+ * Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in
+ the documentation and/or other materials provided with the
+ distribution.
+
+ * Neither the name of Galois, Inc. nor the names of its contributors
+ may be used to endorse or promote products derived from this
+ software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,581 @@
+# Overview
+
+The `crux-llvm` tool (and corresponding C library) are intended for
+verifying C programs containing inline specifications (in the form of
+function calls to create non-deterministic values and assert
+properties). For more information about Crux itself, refer to the
+[official website](https://crux.galois.com).
+
+# Licensing and bundled tools
+
+`crux-llvm` is licensed under the 3-Clause BSD license. For more details, refer
+to the `LICENSE` file. Some binary distributions of `crux-llvm` come bundled
+with external compilers and SMT solvers:
+
+* `clang` and `llvm-link` (Apache v2.0 licensed)
+* CVC4 (BSD-3 licensed)
+* Yices (GPLv3 licensed)
+* Z3 (MIT licensed)
+
+These tools are only invoked by `crux-llvm` as subprocesses. That is,
+`crux-llvm` does not link against any of these tools directly. As a result,
+`crux-llvm` adheres to the GPLv3 licensing terms in Yices.
+
+# Prerequisites
+
+Before running `crux-llvm`, you'll need to install the following
+software:
+
+* GHC and `cabal`. We recommend using `ghcup`:
+
+
+* The Yices SMT solver:
+
+* The Z3 SMT solver:
+
+* The Clang compiler and LLVM toolchain:
+
+ If you are on macOS, one way to install LLVM is with [`brew`](https://brew.sh/).
+ To install LLVM with `brew`, run the following commands:
+ * `xcode-select --install`
+ * `brew install llvm`
+ * `echo 'export PATH="/usr/local/opt/llvm/bin:$PATH"' >> ~/.bash_profile`
+ * run `crux-llvm` in a new console to reload `.bash_profile`
+
+We have tested `crux-llvm` most heavily with GHC 8.10.7, GHC 9.2.7, GHC 9.4.4,
+and `cabal` version 3.8.1.0. We recommend Yices 2.6.x, and Z3
+4.8.x. Technically, only one of Yices or Z3 is required, and CVC4 is
+also supported. However, in practice, having both tends to be
+convenient. Finally, LLVM versions from 3.6 through 16 are likely to
+work well, and any failures with versions in that range should be
+[reported as bugs](https://github.com/GaloisInc/crucible/issues).
+
+# Building
+
+The `crux-llvm` tool can be built by doing the following:
+
+* Clone (incl. the submodules) the `crucible` repository:
+
+ git clone --recurse-submodules https://github.com/GaloisInc/crucible.git
+
+* Build the `crux-llvm` package:
+
+ cabal build crux-llvm
+
+This will compile `crux-llvm` and supporting libraries such that they
+can be executed with `cabal run`. To install the binaries in the
+standard Cabal binary path (usually `$HOME/.cabal/bin`), run the
+following:
+
+ cabal install exe:crux-llvm --overwrite-policy=always
+
+You can also use the `--installdir` flag to install binaries in a
+different location.
+
+# Invocation
+
+In the `crux-llvm` directory (either in the repository or the root of
+the directory extracted from a distribution tarball), to analyze
+`file.c`, run
+
+ cabal run exe:crux-llvm file.c
+
+If you've installed `crux-llvm` somewhere on your `PATH`, you can
+instead run
+
+ crux-llvm file.c
+
+You'll see output indicating the progress of analysis, how many proof
+goals are generated, and how many were successfully proved. In addition,
+the `results` directory will contain a subdirectory for the file you
+provided. This directory will contain an `index.html` file that shows a
+visualization of proof results overlaid on the C source code. If
+`crux-llvm` found a counter-example to any of the attempted proofs, the
+values of that counter-example will be overlaid on the source code (at
+the location of calls to create non-deterministic values), and the
+following two executable files will also exist in the `results`
+directory:
+
+* `debug-NNN`: an executable file that runs the program and provides it
+ with the counter-example values. The number `NNN` indicates the line
+ of the source on which the error occurred (and where it may make sense
+ to set a breakpoint in a debugger to examine the state of the
+ program).
+
+* `print-model-NNN`: an executable file that prints out the values
+ associated with the counter-example.
+
+To define properties and assumptions about the code to analyze, you can
+annotate the source code with inline properties. When `crux-llvm`
+compiles your code, it defines the CPP macro `CRUCIBLE` to help specify
+Crucible-specific functionality such as inline properties. The following
+simple example includes on version of `main` when running with
+`crux-llvm` and different one when compiled normally.
+
+~~~~ .c
+#include
+#ifdef CRUCIBLE
+#include
+#endif
+
+int8_t f(int8_t x) {
+ return x + 1;
+}
+
+#ifdef CRUCIBLE
+int main() {
+ int8_t x = crucible_int8_t("x");
+ assuming(x < 100);
+ check(f(x) < 100);
+ return 0;
+}
+#else
+int main(int argc, char **argv) {
+ return f(argc);
+}
+#endif
+~~~~
+
+When running under `crux-llvm`, this file includes the `crucible.h`
+header file that declares functions and macros such as
+`crucible_int8_t`, `assuming`, and `check`. The call to
+`crucible_int8_t` marks variable `x` as a symbolic variable whose value
+can be any 8-bit signed integer. The C expression within the assuming
+statement states that `x` must be less than 100. The expression within
+the check statement is a proof goal: `crux-llvm` will attempt to prove
+that property `f(x) < 100` holds whenever the assumption on `x` is
+satisfied. The proof will fail in this case and `crux-llvm` will produce
+a counterexample describing the case where `x` is 99.
+
+## Counterexample limitations
+
+All counterexamples assume that the entrypoint function is `main`, even
+if `entry-point` option is used to specify a different entrypoint during
+simulation. Counterexamples also do not respect the `supply-main-arguments`
+option. That is, if you simulate a `main(int argc, char *argv[])` function
+and use `supply-main-arguments: empty` to pass `argc=0` and `argv={}` to
+`main`, these arguments will _not_ be passed automatically to the
+counterexample executables.
+
+# API
+
+The [`crucible.h` header file](c-src/includes/crucible.h) contains
+declarations of several functions that can be used to describe the
+properties of a program that you would like to prove.
+
+* The `crucible_assume` function states an assumption as a C expression.
+ Any proofs after this point will assume this expression is true. The
+ macro `assuming` will automatically fill in its location arguments.
+
+* The `crucible_assert` function states an property to check as a C
+ expression. Every call to this function will create an additional
+ proof goal. The `check` macro will automatically fill in its location
+ arguments.
+
+* The `crucible_*_t` functions create fresh (non-deterministic) values
+ of the corresponding type. The verification process ensures that
+ whatever results are returned by these functions, out of all possible
+ values for the corresponding type, all `crucible_assert` calls will
+ succeed.
+
+For programs that have been written for the [SV-COMP
+competition](https://sv-comp.sosy-lab.org/), the `__VERIFIER_nondet_*`
+functions create non-deterministic values of the corresponding type.
+These symbolic values all have the name `x`. To supply distinct names,
+use the `crucible_*_t` functions, instead.
+
+Note that support for the SV-COMP API exists primarily for backward
+compatibility, since a large number of benchmarks already exist in that
+form. The `crucible.h` API allows for better explanations by a) allowing
+user-specified names for non-deterministic variables, and b) ensuring
+that the conditions used in assertions are directly available and not
+obscured by a conditional wrapper around an error function.
+
+# Standard C and C++ Libraries
+
+The code supplied to `crux-llvm` should be largely self-contained,
+without calls to external code. However, some standard library functions
+have built-in support. For C code, the following functions are understood:
+
+* `__assert_rtn`
+* `calloc`
+* `free`
+* `getenv` (always returns `NULL`)
+* `malloc`
+* `memcpy`
+* `__memcpy_chk`
+* `memmove`
+* `memset`
+* `__memset_chk`
+* `posix_memalign`
+* `printf` (supports a subset of standard printf formatting codes)
+* `__printf_chk`
+* `putchar`
+* `puts`
+* `realloc`
+* `strlen`
+* `open`
+* `read`
+* `write`
+* `close`
+
+In addition, the following LLVM intrinsic functions are supported:
+
+* `llvm.assume`
+* `llvm.bitreverse.*`
+* `llvm.bswap.*`
+* `llvm.ctlz.*`
+* `llvm.ctpop.*`
+* `llvm.cttz.*`
+* `llvm.expect.*`
+* `llvm.invariant.end.*`
+* `llvm.invariant.start.*`
+* `llvm.lifetime.end.*`
+* `llvm.lifetime.start.*`
+* `llvm.memcpy.*`
+* `llvm.memmove.*`
+* `llvm.memset.*`
+* `llvm.objectsize.*`
+* `llvm.sadd.with.overflow.*`
+* `llvm.smul.with.overflow.*`
+* `llvm.ssub.with.overflow.*`
+* `llvm.stackrestore`
+* `llvm.stacksave`
+* `llvm.uadd.with.overflow.*`
+* `llvm.umul.with.overflow.*`
+* `llvm.usub.with.overflow.*`
+* `llvm.x86.pclmulqdq`
+* `llvm.x86.sse2.storeu.dq`
+
+For C++ code, several core functions have built-in support, but
+`crux-llvm` will also link with a precompiled LLVM bitcode file
+containing the `libc++` library included with the `clang` compiler, so
+most C++ code that doesn't use third-party libraries (or that includes
+those libraries linked into a single bitcode file) should work.
+
+# Command-line Flags
+
+The most important and only required argument to `crux-llvm` is the
+source file or list of source files to analyze. In the case that
+multiple files are provided, they will be compiled independently and
+linked together with `llvm-link`.
+
+In addition, the following flags can optionally be provided:
+
+* `--help`, `-h`, `-?`: Print all options with brief descriptions.
+
+* `--include-dirs=DIRS`, `-I DIRS`: Set directories to search for C/C++
+ include files. This will be passed along to `clang`.
+
+* `-O NUM`: Set the optimization level for `clang`.
+
+* `--version`, `-V`: Show the version of the tool.
+
+* `--sim-verbose=NUM`, `-d NUM`: Set the verbosity level of the symbolic
+ simulator to `N`.
+
+* `--floating-point=FPREP`, `-f FPREP`: Select the floating point
+ representation to use. The value of `FPREP` can be one of `real`,
+ `ieee`, `uninterpreted`, or `default`. Default representation is
+ solver specific: `real` for CVC4 and Yices, and `ieee` for Z3.
+
+* `--iteration-bound=N`, `-i N`: Set a bound on the number of times a
+ single loop can iterate. This can also make it more likely to get at
+ least a partial verification result for complex programs, and can be
+ more clearly connected to the execution of the program than a
+ time-based bound.
+
+* `--profiling-period=N`, `-p N`: Set how many seconds to wait between
+ each dump of profiling data (default: 5). Intermediate profiling data
+ can be helpful for diagnosing a run that does not terminate in a
+ reasonable amount of time.
+
+* `--quiet`, `-q`: Quiet mode; produce minimal output.
+
+* `--recursion-bound=N`, `-i N`: Set a bound on the number of times a
+ single function can recur. This can also make it more likely to get at
+ least a partial verification result for complex programs, and can be
+ more clearly connected to the execution of the program than a
+ time-based bound.
+
+* `--solver=NAME`, `-s NAME`: Use the given SMT solver to discharge
+ proof obligations. Valid values for `NAME` are `cvc4`, `cvc5`, `yices`, and
+ `z3`.
+
+* `--timeout=N`, `-t N`: Set the timeout for the first phase of analysis
+ (symbolic execution) which happens before sending the main goals to an
+ SMT solver. Setting this to a low value can give you a result more
+ quickly, but the result is more likely to be "Unknown" (default: 60).
+
+* `--no-execs`, `-x`: Do not create executables to demonstrate
+ counter-examples.
+
+* `--branch-coverage`: Record branch coverage information.
+
+* `--config=FILE`: Load configuration from `FILE`. A configuration file
+ can specify the same settings as command-line flags. Details of the
+ format for configuration files appear in the next section.
+
+* `--entry-point=SYMBOL`: Start symbolic execution at `SYMBOL`.
+
+* `--fail-fast`: Stop attempting to prove goals as soon as one of them
+ is disproved.
+
+* `--force-offline-goal-solving`: Force goals to be solved using an
+ offline solver, even if the selected solver could have been used in
+ online mode.
+
+* `--goal-timeout=N`: Set the timeout for each call to the SMT solver to
+ `N` seconds.
+
+* `--hash-consing`: Enable hash-consing in the symbolic expression
+ backend.
+
+* `--lax-arithmetic`: Allow arithmetic overflow.
+
+* `--lax-pointers`: Allow order comparisons between pointers from
+ different allocation blocks.
+
+* `--lazy-compile`: Avoid compiling bitcode from source if intermediate
+ files already exist.
+
+* `--mcsat`: Enable the MC-SAT engine when using the Yices SMT solver.
+ This disables the use of UNSAT cores, so the HTML rendering of proved
+ goals won't include highlighting a set of the assumptions that were
+ necessary for proving the goal.
+
+* `--no-unsat-cores`: Disable computing unsat cores for successful
+ proofs.
+
+* `--online-solver-output=FILE`: Store a log of interaction with the
+ online goal solver in `FILE`.
+
+* `--opt-loop-merge`: Insert merge blocks in loops with early exits.
+
+* `--output-directory=DIR`: Set the directory to use to store output
+ files (default: `results`).
+
+* `--path-sat`: Enable path satisfiability checking, which can help
+ programs terminate, particularly in the case where the bounds on loops
+ are complex.
+
+* `--path-sat-solver=SOLVER`: Select the solver to use for path
+ satisfiability checking, in order to use a different solver than for
+ discharging goals.
+
+* `--path-sat-solver-output`: Store a log of interaction with the path
+ satisfiability solver in `FILE`.
+
+* `--path-strategy=STRATEGY`: Set the strategy to use for exploring
+ paths during symbolic execution. A `STRATEGY` of `always-merge` (the
+ default) causes all paths being explored to be merged into a single
+ symbolic state at every post-dominator node in the control flow graph.
+ The `split-dfs` strategy explores each path independently in
+ depth-first order. The former is typically more appropriate for full
+ verification whereas the latter can be more effective for bug finding.
+ Sometimes, however `split-dfs` can lead to faster full verification
+ times.
+
+* `--profile-crucible`: Enable profiling of the symbolic execution
+ process. Produces an additional HTML file in the output directory that
+ provides a graphical and tabular depiction of the execution time
+ profile.
+
+* `--profile-solver`: Include profiling of SMT solver calls in the
+ symbolic execution profile.
+
+* `--skip-incomplete-reports`: Skip reporting on proof obligations that
+ arise from timeouts and resource exhaustion.
+
+* `--skip-print-failures`: Skip printing messages related to failed
+ verification goals.
+
+* `--skip-report`: Skip producing the HTML report following
+ verification.
+
+* `--skip-success-reports`: Skip reporting on successful proof
+ obligations.
+
+* `--target=ARCH`: Pass `ARCH` as the target architecture to LLVM build
+ operations.
+
+* `--no-compile`: Assume the input file is an LLVM bitcode module, rather than a
+ C program.
+
+* `--symbolic-fs-root=DIR`: Specify a directory containing the initial contents of
+ a symbolic filesystem to use during symbolic execution. See the Symbolic I/O
+ documentation for the format of this directory. [Experimental]
+
+# Environment Variables
+
+The following environment variables are supported:
+
+* `BLDDIR`: Specify the directory for writing build files generated from
+ the input files.
+
+* `CLANG`: Specify the name of the `clang` compiler command used to
+ translate from C/C++ to LLVM.
+
+* `CLANG_OPTS`: Specify additional options to pass to `clang`.
+
+* `LLVM_LINK`: Specify the name of the `llvm-link` command used to
+ combine multiple LLVM bitcode files.
+
+# Configuration Files
+
+In addition to command-line flags and environment variables, `crux-llvm`
+can be configured with a key-value input file. The file consists of a
+set of `KEY: VALUE` entries, each on a separate line, where each `KEY`
+generally corresponds to the textual part of the long version of a
+command-line flag. For example, one can set the iteration bound to 10 as
+follows:
+
+ iteration-bound: 10
+
+Options that take a list of arguments can be written with either a
+single value (for a list of length one) or with multiple values on
+successive lines, each starting with `*`. For example, the following is
+a valid input file:
+
+ llvm-link: "llvm-link-6.0"
+ clang: "clang-6.0"
+ make-executables: no
+ files:
+ * "a.c"
+ * "b.c"
+
+This specifies the name of the command to run for `clang` and
+`llvm-link`, instructs `crux-llvm` not to create counter-example
+demonstration executables, and provides a list of input files.
+
+# Symbolic I/O [Experimental]
+
+Note that Symbolic I/O is currently experimental. We expect that the API (both
+internal and command line) will change.
+
+`crux-llvm` supports *symbolic* I/O operations via the POSIX `open`, `read`,
+`write`, and `close` functions. These operations are symbolic in the sense that
+the contents of files in the symbolic filesystem can be a mix of concrete and
+symbolic values. The original motivation of the work was to support checking
+assertions for programs with configuration files; by supporting symbolic file
+contents, `crux-llvm` can check entire families of configuration at once.
+
+## Symbolic Filesystem Contents
+
+The `--symbolic-fs-root` option (and corresponding configuration file option)
+enable users to specify the initial contents of the symbolic filesystem. The
+directory pointed to by this options contains:
+
+* A sub-directory named `root` that contains concrete files that will exist in
+ the initial filesystem. The directory layout within `root` is preserved. For
+ example, a file named `root/etc/fstab` will be mapped to `/etc/fstab` in the
+ initial symbolic filesystem.
+* An optional file named `stdin`, which contains the standard input of the program.
+* A manifest named `system-manifest.json` that describes the contents of symbolic files.
+
+The manifest maps absolute file paths to specifications of what parts of the
+corresponding file are symbolic. Note that the specification is currently
+coarse and only supports fully-symbolic files. The format of the system
+manifest is:
+
+```
+{ "symbolicFiles": [],
+ "useStdout": bool,
+ "useStderr": bool
+}
+
+SymFilePair := [ FilePath, ]
+
+FilePath := string (an absolute file path)
+
+SymbolicFileContents := { "symbolicContentSize": Word64 }
+
+```
+
+If no initial filesystem is specified, `crux-llvm` defaults to an empty standard
+input, while allowing output to standard output and standard error. Note that
+if a program attempts to use the symbolic I/O primitives without being backed by
+appropriate files (e.g., opening a file that does not exist), the symbolic I/O
+backend will simply report that those functions fail in the expected way (i.e.,
+returning -1).
+
+## Interaction with Standard I/O
+
+If the program being verified writes to standard output or standard error (via
+the POSIX `STDOUT_FILENO` or `STDERR_FILENO` handles, which correspond to file
+descriptors 1 and 2), the symbolic I/O backend reflects as much of the output as
+it can to the actual standard output and standard error of `crux-llvm`. Note
+that only *concrete* writes are mirrored to the real world; symbolic writes
+still take effect in the symbolic files representing standard output and
+standard error.
+
+Note that, due to the branching structure of symbolic execution, the same output
+may appear more than once if a call to `write` occurs on a symbolic branch.
+
+## Current Limitations
+
+* Filenames must be concrete
+* Filenames must be absolute paths (relative paths require additionally modeling the current working directory)
+* Many file operations are not yet modeled
+* Files can currently only be entirely concrete or entirely symbolic
+* The `open` function does not accept a mode (i.e., file permissions are not yet modeled)
+* The `open` function accepts flags (but currently ignores them)
+* The `open` function cannot create new files that do not exist in the filesystem
+* The special handling of `printf` does not yet interact with the symbolic standard output file descriptor
+
+It is intended that the symbolic I/O facility will be extended over time to
+support more operations.
+
+Also note that the order in which file descriptor numbers are handed out to
+client code can be subtly different than in the real program. In particular, on
+a symbolic branch where both branches open a new file, the two branches will get
+sequential file descriptors. In contrast, the real program would allocate the
+same file descriptor to both (as only one branch would be taken).
+
+# Test suite
+
+The `crux-llvm` test suite is implemented in `test/Test.hs`, and the
+accompanying test case data can be found under `test-data`. Each test case
+comprises a C or LLVM bitcode file that is provided as input to `crux-llvm`,
+along with an expected output file. For most test cases, this expected output
+file will be named `.z3.good`; this picks Z3 as a default solver to
+use when simulating the test case. There are also a handful of tests that
+require other solvers, e.g., `abd-test-file-32.cvc5.good`.
+
+Some of the test cases have slightly different output depending on which Clang
+version is used. These test cases will have accompanying
+`.pre-clang.<...>.good` files, where `pre-clang`
+indicates that this test output is used for all Clang versions up to (but not
+including) ``. Note that if a test case has multiple
+`pre-clang` `.good` files, then the `` that is closest to the
+current Clang version (without going over) is picked.
+
+To illustrate this with a concrete example, consider suppose we have a test
+case `foo` with the following `.good` files
+
+* `foo.pre-clang11.z3.good`
+* `foo.pre-clang13.z3.good`
+* `foo.z3.good`
+
+The following `.good` files would be used for the following Clang versions:
+
+* Clang 10: `foo.pre-clang11.z3.good`
+* Clang 11: `foo.pre-clang13.z3.good`
+* Clang 12: `foo.pre-clang13.z3.good`
+* Clang 13 or later: `foo.z3.good`
+
+There are some test cases that require a sufficiently recent Clang version to
+run. To indicate that a test should not be run on Clangs older than
+``, create a `pre-clang` `.good` file with `SKIP_TEST` as the
+first line. The use of `SKIP_TEST` signals that this test should be skipped
+when using Clangs older than ``. Note that the test suite will not
+read anything past `SKIP_TEST`, so the rest of the file can be used to document
+why the test is skipped on that particular configuration.
+
+# Acknowledgements
+
+Crux is partly based upon work supported by the Defense Advanced
+Research Projects Agency (DARPA) under Contract No. N66001-18-C-4011.
+Any opinions, findings and conclusions or recommendations expressed in
+this material are those of the author(s) and do not necessarily reflect
+the views of the Defense Advanced Research Projects Agency (DARPA).
diff --git a/c-src/concrete-backend.c b/c-src/concrete-backend.c
new file mode 100644
--- /dev/null
+++ b/c-src/concrete-backend.c
@@ -0,0 +1,45 @@
+#include
+#include
+#include
+#include
+
+void crucible_assume(uint8_t x, const char* file, int line) {
+ if (x) return;
+ fprintf(stderr, "%s:%d: Violated assumption.\n", file, line);
+ exit(1);
+}
+
+void crucible_assert(uint8_t x, const char* file, int line) {
+ if (x) return;
+ fprintf(stderr, "%s:%d: Assertion failed.\n", file, line);
+ exit(2);
+}
+
+#define mk_crux_func(ty) \
+ ty crucible_##ty (const char *name) { \
+ (void)(name); \
+ static unsigned long i = 0; \
+ if (i < crux_value_num(ty)) return crux_values(ty)[i++]; \
+ return 0; \
+ }
+
+mk_crux_func(int8_t)
+mk_crux_func(int16_t)
+mk_crux_func(int32_t)
+mk_crux_func(int64_t)
+mk_crux_func(float)
+mk_crux_func(double)
+
+unsigned long __VERIFIER_nondet_ulong (void) { return crucible_int64_t("x"); }
+long __VERIFIER_nondet_long (void) { return crucible_int64_t("x"); }
+unsigned int __VERIFIER_nondet_uint (void) { return crucible_int32_t("x"); }
+int __VERIFIER_nondet_int (void) { return crucible_int32_t("x"); }
+unsigned short __VERIFIER_nondet_ushort (void) { return crucible_int16_t("x"); }
+short __VERIFIER_nondet_short (void) { return crucible_int16_t("x"); }
+unsigned char __VERIFIER_nondet_uchar (void) { return crucible_int8_t("x"); }
+char __VERIFIER_nondet_char (void) { return crucible_int8_t("x"); }
+int __VERIFIER_nondet_bool (void) { return crucible_int32_t("x"); }
+float __VERIFIER_nondet_float (void) { return crucible_float("x"); }
+double __VERIFIER_nondet_double (void) { return crucible_double("x"); }
+
+
diff --git a/c-src/includes/crucible-model.h b/c-src/includes/crucible-model.h
new file mode 100644
--- /dev/null
+++ b/c-src/includes/crucible-model.h
@@ -0,0 +1,32 @@
+#ifndef CRUCIBLE_MODEL_H
+#define CRUCIBLE_MODEL_H
+
+#ifdef __cplusplus__
+extern "C" {
+#endif //__cplusplus__
+
+#include
+#include
+
+#define crux_names(ty) crucible_names_##ty
+#define crux_values(ty) crucible_values_##ty
+#define crux_value_num(ty) crucible_values_number_##ty
+
+#define mk_model_ty(ty) \
+ extern const size_t crux_value_num(ty); \
+ extern const char* crux_names(ty)[]; \
+ extern const ty crux_values(ty) [];
+
+mk_model_ty(int8_t)
+mk_model_ty(int16_t)
+mk_model_ty(int32_t)
+mk_model_ty(int64_t)
+mk_model_ty(float)
+mk_model_ty(double)
+
+#ifdef __cplusplus__
+}
+#endif //__cplusplus__
+
+#endif
+
diff --git a/c-src/includes/crucible.h b/c-src/includes/crucible.h
new file mode 100644
--- /dev/null
+++ b/c-src/includes/crucible.h
@@ -0,0 +1,55 @@
+#ifndef CRUCIBLE_H
+#define CRUCIBLE_H
+
+#ifdef __cplusplus
+extern "C" {
+#endif //__cplusplus
+
+#include
+#include
+#include
+
+void crucible_assume(uint8_t x, const char *file, int line);
+void crucible_assert(uint8_t x, const char *file, int line);
+
+int8_t crucible_int8_t (const char *name);
+int16_t crucible_int16_t (const char *name);
+int32_t crucible_int32_t (const char *name);
+int64_t crucible_int64_t (const char *name);
+float crucible_float (const char *name);
+double crucible_double (const char *name);
+
+size_t crucible_size_t (const char *name);
+
+// Allocate a string of fixed length with symbolic contents
+//
+// The string has @max_len@ symbolic bytes plus a fixed NUL terminator. Each
+// character is unconstrained and may also be NUL, allowing for verification of
+// algorithms over strings up to a certain length.
+//
+// The string contents are read-only.
+const char* crucible_string(const char *name, size_t max_len);
+
+// Fill a region of memory with fresh symbolic bytes
+void crucible_havoc_memory( void* p, size_t len );
+
+// Print a symbolic value to stdout
+void crucible_print_uint32( uint32_t val );
+
+// Print the current state of the symbolic memory to stdout
+void crucible_dump_memory(void);
+
+
+#define crucible_uint8_t(n) ((uint8_t)crucible_int8_t(n))
+#define crucible_uint16_t(n) ((uint16_t)crucible_int16_t(n))
+#define crucible_uint32_t(n) ((uint32_t)crucible_int32_t(n))
+#define crucible_uint64_t(n) ((uint64_t)crucible_int64_t(n))
+
+#define assuming(e) crucible_assume(e, __FILE__, __LINE__)
+#define check(e) crucible_assert(e, __FILE__, __LINE__)
+
+#ifdef __cplusplus
+}
+#endif //__cplusplus
+
+#endif
diff --git a/c-src/libcxx-3.6.2.bc b/c-src/libcxx-3.6.2.bc
new file mode 100644
# file too large to diff: c-src/libcxx-3.6.2.bc
diff --git a/c-src/libcxx-7.1.0.bc b/c-src/libcxx-7.1.0.bc
new file mode 100644
# file too large to diff: c-src/libcxx-7.1.0.bc
diff --git a/c-src/print-model.c b/c-src/print-model.c
new file mode 100644
--- /dev/null
+++ b/c-src/print-model.c
@@ -0,0 +1,26 @@
+#include
+#include
+#include
+
+int main () {
+ size_t i;
+ for (i = 0; i < crux_value_num(int8_t); ++i)
+ printf("%s = %"PRId8", %"PRIu8", 0x%"PRIx8"\n", crux_names(int8_t)[i], crux_values(int8_t)[i], crux_values(int8_t)[i], crux_values(int8_t)[i]);
+
+ for (i = 0; i < crux_value_num(int16_t); ++i)
+ printf("%s = %"PRId16", %"PRIu16", 0x%"PRIx16"\n", crux_names(int16_t)[i], crux_values(int16_t)[i], crux_values(int16_t)[i], crux_values(int16_t)[i]);
+
+ for (i = 0; i < crux_value_num(int32_t); ++i)
+ printf("%s = %"PRId32", %"PRIu32", 0x%"PRIx32"\n", crux_names(int32_t)[i], crux_values(int32_t)[i], crux_values(int32_t)[i], crux_values(int32_t)[i]);
+
+ for (i = 0; i < crux_value_num(int64_t); ++i)
+ printf("%s = %"PRId64", %"PRIu64", 0x%"PRIx64"\n", crux_names(int64_t)[i], crux_values(int64_t)[i], crux_values(int64_t)[i], crux_values(int64_t)[i]);
+
+ for (i = 0; i < crux_value_num(float); ++i)
+ printf("%s = %f, %a\n", crux_names(float)[i], crux_values(float)[i], crux_values(float)[i]);
+
+ for (i = 0; i < crux_value_num(double); ++i)
+ printf("%s = %f, %a\n", crux_names(double)[i], crux_values(double)[i], crux_values(double)[i]);
+
+ return 0;
+}
diff --git a/crux-llvm.cabal b/crux-llvm.cabal
new file mode 100644
--- /dev/null
+++ b/crux-llvm.cabal
@@ -0,0 +1,184 @@
+Cabal-version: 2.2
+Name: crux-llvm
+Version: 0.8
+Author: Galois Inc.
+Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com
+Copyright: (c) Galois, Inc 2014-2022
+License: BSD-3-Clause
+License-file: LICENSE
+Build-type: Simple
+Category: Language
+Synopsis: A verification tool for C programs.
+Description:
+ .
+ This tool (and corresponding C library) are intended for verifying C
+ programs using verification specifications embedded in the input
+ source files (i.e. it allows for writing Crucible specifications
+ by using C as the specification language).
+ .
+ This tool provides:
+ .
+ * a Haskell library with the core functionality,
+ .
+ * a @crux-llvm@ executable used to run the verification when given one
+ or more C or C++ source files
+ .
+ * a set of supplemental C source files, include files, and LLVM
+ runtime library bitcode files to use for building the input C
+ files into verifiable LLVM BC files.
+ .
+ * a @crux-llvm-svcomp@ executable that is designed to run verification
+ of challenge inputs for the SV-COMP competition, generating
+ results tailored to the format that SV-COMP expects.
+
+
+data-files:
+ c-src/includes/crucible.h
+ c-src/includes/crucible-model.h
+ c-src/concrete-backend.c
+ c-src/print-model.c
+ c-src/libcxx-3.6.2.bc
+ c-src/libcxx-7.1.0.bc
+extra-source-files: CHANGELOG.md, README.md
+
+source-repository head
+ type: git
+ location: https://github.com/GaloisInc/crucible
+ subdir: crux-llvm
+
+common bldflags
+ ghc-options: -Wall
+ -Werror=incomplete-patterns
+ -Werror=missing-methods
+ -Werror=overlapping-patterns
+ -Wpartial-fields
+ -Wincomplete-uni-patterns
+ ghc-prof-options: -O2
+ default-language: Haskell2010
+ build-depends: base >= 4.8 && < 4.19
+ , bytestring
+ , containers
+ , crucible
+ , crucible-symio
+ , crucible-llvm
+ , crux
+ , directory
+ , filepath
+ , lens
+ , process
+ , text
+ , what4
+
+common testdefs
+ build-depends: tasty >= 0.10
+ , tasty-hunit >= 0.10
+ , tasty-sugar >= 2.2 && < 2.3
+
+
+library
+ import: bldflags
+ hs-source-dirs: src
+
+ exposed-modules:
+ CruxLLVMMain
+ Crux.LLVM.Compile
+ Crux.LLVM.Config
+ Crux.LLVM.Log
+ Crux.LLVM.Overrides
+ Crux.LLVM.Simulate
+ Paths_crux_llvm
+
+ autogen-modules:
+ Paths_crux_llvm
+
+ build-depends:
+ aeson,
+ bv-sized,
+ config-schema >= 1.2.2.0,
+ logict,
+ llvm-pretty,
+ llvm-pretty-bc-parser,
+ mtl,
+ parameterized-utils,
+ prettyprinter >= 1.7.0
+
+
+executable crux-llvm
+ import: bldflags
+
+ hs-source-dirs: exe
+
+ build-depends:
+ crux-llvm
+
+ main-is: Main.hs
+
+ if os(windows)
+ hs-source-dirs: exe/windows
+ else
+ hs-source-dirs: exe/unix
+ build-depends: unix
+
+ other-modules: RealMain
+
+
+executable crux-llvm-for-ide
+ import: bldflags
+
+ hs-source-dirs: for-ide
+
+ build-depends:
+ aeson,
+ crux-llvm,
+ lumberjack,
+ websockets >= 0.12
+
+ main-is: Main.hs
+
+ if os(windows)
+ hs-source-dirs: for-ide/windows
+ else
+ hs-source-dirs: for-ide/unix
+ build-depends: unix
+
+ other-modules:
+ Paths_crux_llvm
+ RealMain
+
+
+executable crux-llvm-svcomp
+ import: bldflags
+ hs-source-dirs: svcomp
+ main-is: Main.hs
+
+ build-depends:
+ aeson,
+ attoparsec,
+ base16-bytestring,
+ crux-llvm,
+ cryptohash-sha256,
+ extra,
+ indexed-traversable,
+ time
+
+ other-modules:
+ SVComp.Log
+ Paths_crux_llvm
+
+ autogen-modules:
+ Paths_crux_llvm
+
+
+test-suite crux-llvm-test
+ import: bldflags, testdefs
+ type: exitcode-stdio-1.0
+ hs-source-dirs: test
+
+ main-is: Test.hs
+
+ build-depends:
+ crux-llvm,
+ extra,
+ regex-base,
+ regex-posix,
+ versions
diff --git a/exe/Main.hs b/exe/Main.hs
new file mode 100644
--- /dev/null
+++ b/exe/Main.hs
@@ -0,0 +1,6 @@
+{- | This is the main executable for running the Crux LLVM verification
+ on LLVM BitCode objects that can be built from C and C++ sources
+ using Clang and llvm-link. -}
+
+module Main (main) where
+import RealMain (main)
diff --git a/exe/unix/RealMain.hs b/exe/unix/RealMain.hs
new file mode 100644
--- /dev/null
+++ b/exe/unix/RealMain.hs
@@ -0,0 +1,25 @@
+module RealMain (main) where
+
+import Control.Monad
+import System.Exit
+import System.Posix.Signals
+import System.Posix.Process
+
+import CruxLLVMMain (mainWithOutputConfig, defaultOutputConfig)
+
+-- Rebroadcast SIGTERM to the entire process group. The CatchOnce
+-- handler keeps this from handling and retransmitting SIGTERM to
+-- itself over and over.
+installSIGTERMHandler :: IO ()
+installSIGTERMHandler =
+ do gid <- getProcessGroupID
+ void $ installHandler sigTERM (CatchOnce (handler gid)) Nothing
+ where
+ handler gid = signalProcessGroup sigTERM gid
+
+
+main :: IO ()
+main =
+ do installSIGTERMHandler
+ ec <- mainWithOutputConfig =<< defaultOutputConfig
+ exitWith ec
diff --git a/exe/windows/RealMain.hs b/exe/windows/RealMain.hs
new file mode 100644
--- /dev/null
+++ b/exe/windows/RealMain.hs
@@ -0,0 +1,9 @@
+module RealMain (main) where
+
+import System.Exit
+import CruxLLVMMain (mainWithOutputConfig, defaultOutputConfig)
+
+main :: IO ()
+main =
+ do ec <- mainWithOutputConfig =<< defaultOutputConfig
+ exitWith ec
diff --git a/for-ide/Main.hs b/for-ide/Main.hs
new file mode 100644
--- /dev/null
+++ b/for-ide/Main.hs
@@ -0,0 +1,94 @@
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module Main (main) where
+
+import Control.Lens (makeLenses, set, view)
+import Crux (OutputConfig)
+import qualified Crux
+import Crux.Config.Common (OutputOptions)
+import Crux.LLVM.Config (LLVMOptions, llvmCruxConfig)
+import CruxLLVMMain
+ ( CruxLLVMLogging,
+ mainWithOptions,
+ withCruxLLVMLogging,
+ )
+import qualified Data.Aeson as JSON
+import Data.Text as Text (Text, unpack)
+import qualified Lumberjack as LJ
+import qualified Network.WebSockets as WS
+import Paths_crux_llvm (version)
+import RealMain (makeMain)
+import System.Exit (ExitCode)
+import Text.Read (readEither)
+
+data ForIDEOptions = ForIDEOptions
+ { _cruxLLVMOptions :: LLVMOptions,
+ _ideHost :: String,
+ _idePort :: Int
+ }
+
+makeLenses ''ForIDEOptions
+
+ideHostDoc :: Text
+ideHostDoc = "Host where the IDE is listening"
+
+idePortDoc :: Text
+idePortDoc = "Port at which the IDE is listening"
+
+forIDEConfig :: IO (Crux.Config ForIDEOptions)
+forIDEConfig = do
+ llvmOpts <- llvmCruxConfig
+ return
+ Crux.Config
+ { Crux.cfgFile =
+ ForIDEOptions
+ <$> Crux.cfgFile llvmOpts
+ <*> Crux.section
+ "ide-host"
+ Crux.stringSpec
+ "127.0.0.1"
+ ideHostDoc
+ <*> Crux.section
+ "ide-port"
+ Crux.numSpec
+ 0
+ idePortDoc,
+ Crux.cfgEnv = Crux.liftEnvDescr cruxLLVMOptions <$> Crux.cfgEnv llvmOpts,
+ Crux.cfgCmdLineFlag =
+ (Crux.liftOptDescr cruxLLVMOptions <$> Crux.cfgCmdLineFlag llvmOpts)
+ ++ [ Crux.Option
+ []
+ ["ide-host"]
+ (Text.unpack ideHostDoc)
+ $ Crux.ReqArg "STR" $
+ \v opts -> Right (set ideHost v opts),
+ Crux.Option
+ []
+ ["ide-port"]
+ (Text.unpack idePortDoc)
+ $ Crux.ReqArg "INT" $
+ \v opts -> set idePort <$> readEither v <*> pure opts
+ ]
+ }
+
+mainWithOutputConfig ::
+ (Maybe OutputOptions -> OutputConfig CruxLLVMLogging) -> IO ExitCode
+mainWithOutputConfig mkOutCfg =
+ CruxLLVMMain.withCruxLLVMLogging $
+ do
+ conf <- forIDEConfig
+ Crux.loadOptions mkOutCfg "crux-llvm-for-ide" version conf $ \(cruxOpts, forIDEOpts) ->
+ WS.runClient (view ideHost forIDEOpts) (view idePort forIDEOpts) "/" $ \conn ->
+ do
+ let ?outputConfig =
+ ?outputConfig
+ { Crux._logMsg =
+ Crux._logMsg ?outputConfig
+ <> LJ.LogAction (WS.sendTextData conn . JSON.encode)
+ }
+ mainWithOptions (cruxOpts, view cruxLLVMOptions forIDEOpts)
+
+main :: IO ()
+main = makeMain mainWithOutputConfig
diff --git a/for-ide/unix/RealMain.hs b/for-ide/unix/RealMain.hs
new file mode 100644
--- /dev/null
+++ b/for-ide/unix/RealMain.hs
@@ -0,0 +1,34 @@
+module RealMain (makeMain) where
+
+import Control.Monad (void)
+import Crux.Log ( OutputConfig )
+import Crux.Config.Common (OutputOptions)
+import CruxLLVMMain ( CruxLLVMLogging, defaultOutputConfig )
+import System.Exit (ExitCode, exitWith)
+import System.Posix.Process (getProcessGroupID)
+import System.Posix.Signals
+ ( Handler (CatchOnce),
+ installHandler,
+ sigTERM,
+ signalProcessGroup,
+ )
+
+-- Rebroadcast SIGTERM to the entire process group. The CatchOnce
+-- handler keeps this from handling and retransmitting SIGTERM to
+-- itself over and over.
+installSIGTERMHandler :: IO ()
+installSIGTERMHandler =
+ do
+ gid <- getProcessGroupID
+ void $ installHandler sigTERM (CatchOnce (handler gid)) Nothing
+ where
+ handler gid = signalProcessGroup sigTERM gid
+
+makeMain ::
+ ((Maybe OutputOptions -> OutputConfig CruxLLVMLogging) -> IO ExitCode) ->
+ IO ()
+makeMain mainWithOutputConfig =
+ do
+ installSIGTERMHandler
+ ec <- mainWithOutputConfig =<< defaultOutputConfig
+ exitWith ec
diff --git a/for-ide/windows/RealMain.hs b/for-ide/windows/RealMain.hs
new file mode 100644
--- /dev/null
+++ b/for-ide/windows/RealMain.hs
@@ -0,0 +1,14 @@
+module RealMain (makeMain) where
+
+import Crux.Log ( OutputConfig )
+import Crux.Config.Common (OutputOptions)
+import CruxLLVMMain ( CruxLLVMLogging, defaultOutputConfig )
+import System.Exit (ExitCode, exitWith)
+
+makeMain ::
+ ((Maybe OutputOptions -> OutputConfig CruxLLVMLogging) -> IO ExitCode) ->
+ IO ()
+makeMain mainWithOutputConfig =
+ do
+ ec <- mainWithOutputConfig =<< defaultOutputConfig
+ exitWith ec
diff --git a/src/Crux/LLVM/Compile.hs b/src/Crux/LLVM/Compile.hs
new file mode 100644
--- /dev/null
+++ b/src/Crux/LLVM/Compile.hs
@@ -0,0 +1,365 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Crux.LLVM.Compile where
+
+import Control.Applicative
+import Control.Exception ( SomeException(..), try )
+import Control.Monad ( guard, unless, when, forM_ )
+import Control.Monad.Logic ( observeAll )
+import qualified Data.Foldable as Fold
+import Data.List ( intercalate, isSuffixOf )
+import qualified Data.Parameterized.Map as MapF
+import Data.Parameterized.Some
+import qualified Data.Text as T
+import qualified Data.Text.IO as TIO
+import System.Directory ( doesFileExist, findExecutable, removeFile
+ , createDirectoryIfMissing, copyFile )
+import System.Exit ( ExitCode(..) )
+import System.FilePath ( takeExtension, (), (-<.>)
+ , takeDirectory, takeFileName )
+import System.Process ( readProcessWithExitCode )
+
+import What4.Interface
+import What4.ProgramLoc
+
+import Lang.Crucible.Simulator.SimError
+
+import Crux
+import qualified Crux.Config.Common as CC
+import Crux.Model ( toDouble, showBVLiteral, showFloatLiteral
+ , showDoubleLiteral )
+import Crux.Types
+
+import Crux.LLVM.Config
+import qualified Crux.LLVM.Log as Log
+
+
+isCPlusPlus :: FilePath -> Bool
+isCPlusPlus file =
+ case takeExtension file of
+ ".cpp" -> True
+ ".cxx" -> True
+ ".C" -> True
+ ".bc" -> False
+ _ -> False
+
+anyCPPFiles :: [FilePath] -> Bool
+anyCPPFiles = any isCPlusPlus
+
+-- | 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.)
+getClang :: IO FilePath
+getClang = attempt (map findExecutable clangs)
+ where
+ clangs = "clang"
+ : [ "clang-" ++ ver
+ | ver <- ["3.6", "3.7", "3.8", "3.9", "4.0", "5.0", "6.0"]
+ -- Starting with LLVM 7, the version numbers used in binaries only display the major version. See
+ -- https://releases.llvm.org/7.0.0/tools/clang/docs/ReleaseNotes.html#non-comprehensive-list-of-changes-in-this-release
+ ++ ["7", "8", "9", "10", "11"] ]
+
+ attempt :: [IO (Maybe FilePath)] -> IO FilePath
+ attempt ms =
+ case ms of
+ [] -> throwCError $ EnvError $
+ unlines [ "Failed to find `clang`."
+ , "You may use CLANG to provide path to executable."
+ ]
+ m : more -> do x <- m
+ case x of
+ Nothing -> attempt more
+ Just a -> return a
+
+runClang ::
+ Logs msgs =>
+ Log.SupportsCruxLLVMLogMessage msgs =>
+ LLVMOptions -> [String] -> IO ()
+runClang llvmOpts params =
+ do let clang = clangBin llvmOpts
+ allParams = clangOpts llvmOpts ++ params
+ Log.sayCruxLLVM (Log.ClangInvocation (T.pack <$> (clang : map show allParams)))
+ (res,sout,serr) <- readProcessWithExitCode clang allParams ""
+ case res of
+ ExitSuccess -> return ()
+ ExitFailure n -> throwCError (ClangError n sout serr)
+
+llvmLink :: LLVMOptions -> [FilePath] -> FilePath -> IO ()
+llvmLink llvmOpts ins out =
+ do let params = ins ++ [ "-o", out ]
+ (res, sout, serr) <- readProcessWithExitCode (linkBin llvmOpts) params ""
+ case res of
+ ExitSuccess -> return ()
+ ExitFailure n -> throwCError (ClangError n sout serr)
+
+parseLLVMLinkVersion :: String -> String
+parseLLVMLinkVersion = go . map words . lines
+ where
+ go (("LLVM" : "version" : version : _) : _) = version
+ go (_ : rest) = go rest
+ go [] = ""
+
+llvmLinkVersion :: LLVMOptions -> IO String
+llvmLinkVersion llvmOpts =
+ do (res, sout, serr) <- readProcessWithExitCode (linkBin llvmOpts) ["--version"] ""
+ case res of
+ ExitSuccess -> return (parseLLVMLinkVersion sout)
+ ExitFailure n -> throwCError (ClangError n sout serr)
+
+-- | 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'.
+genBitCode ::
+ Logs msgs =>
+ Log.SupportsCruxLLVMLogMessage msgs =>
+ CruxOptions -> LLVMOptions -> IO FilePath
+genBitCode cruxOpts llvmOpts =
+ -- n.b. use of head here is OK because inputFiles should not be
+ -- empty (and was previously verified as such in CruxLLVMMain).
+ if noCompile llvmOpts
+ then return (head (Crux.inputFiles cruxOpts))
+ else do
+ let ofn = "crux~" <> (takeFileName $ head $ Crux.inputFiles cruxOpts) -<.> ".bc"
+ genBitCodeToFile ofn (Crux.inputFiles cruxOpts) cruxOpts llvmOpts False
+
+-- | 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.
+genBitCodeToFile :: Crux.Logs msgs
+ => Log.SupportsCruxLLVMLogMessage msgs
+ => String -> [FilePath] -> CruxOptions -> LLVMOptions -> Bool
+ -> IO FilePath
+genBitCodeToFile finalBCFileName files cruxOpts llvmOpts copySrc = do
+ let srcBCNames = [ (src, CC.bldDir cruxOpts takeFileName src -<.> ".bc")
+ | src <- files ]
+ finalBCFile = CC.bldDir cruxOpts finalBCFileName
+ incs src = takeDirectory src :
+ (libDir llvmOpts "includes") :
+ incDirs llvmOpts
+ commonFlags = [ "-c", "-DCRUCIBLE", "-emit-llvm" ] <>
+ case targetArch llvmOpts of
+ Nothing -> []
+ Just a -> [ "--target=" <> a ]
+ params (src, srcBC)
+ | ".ll" `isSuffixOf` src =
+ return $ commonFlags <> ["-O0", "-o", srcBC, src]
+
+ | otherwise =
+ -- Specify commonFlags after flags embedded in the src
+ -- under the /assumption/ that the latter takes
+ -- precedence.
+ let flgs =
+ commonFlags <> [ "-g" ] ++
+ concat [ [ "-I", dir ] | dir <- incs src ] ++
+ concat [ [ "-fsanitize="++san, "-fsanitize-trap="++san ]
+ | san <- ubSanitizers llvmOpts ] ++
+ [ "-O" ++ show (optLevel llvmOpts), "-o", srcBC, src ]
+ in (<> flgs) <$> crucibleFlagsFromSrc src
+
+ finalBCExists <- doesFileExist finalBCFile
+ unless (finalBCExists && lazyCompile llvmOpts) $
+ do forM_ srcBCNames $ \f@(src,bc) -> do
+ when (copySrc) $ copyFile src (takeDirectory bc takeFileName src)
+ bcExists <- doesFileExist bc
+ unless (or [ ".bc" `isSuffixOf` src
+ , bcExists && lazyCompile llvmOpts
+ ]) $
+ runClang llvmOpts =<< params f
+ ver <- llvmLinkVersion llvmOpts
+ let libcxxBitcode | anyCPPFiles files = [libDir llvmOpts "libcxx-" ++ ver ++ ".bc"]
+ | otherwise = []
+ allBCInputFiles = map snd srcBCNames ++ libcxxBitcode
+ case allBCInputFiles of
+ [bcInputFile]
+ -> -- If there is only one input .bc file, just copy it to the
+ -- output destination instead of using llvm-link to produce it.
+ -- Not only is invoking llvm-link needlessly expensive, it can
+ -- sometimes rearrange the order of declarations in the bitcode,
+ -- which makes certain test cases fragile (see #1011).
+ copyFile bcInputFile finalBCFile
+ _ -> llvmLink llvmOpts allBCInputFiles finalBCFile
+ mapM_ (\(src,bc) -> unless (src == bc) (removeFile bc)) srcBCNames
+ return finalBCFile
+
+
+-- | 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).
+
+crucibleFlagsFromSrc :: FilePath -> IO [String]
+crucibleFlagsFromSrc srcFile = do
+ let marker1 = [ "CRUCIBLE ", "CRUX "]
+ marker2 = [ "clang_flags: " ]
+ flagLines fileLines =
+ do let eachFrom = foldr ((<|>) . pure) empty
+ l <- eachFrom fileLines
+ (pfx, sfx) <- eachFrom [ ("/* ", " */"), ("// ", "") ]
+ guard $ pfx `T.isPrefixOf` l
+ let l1 = T.drop (T.length pfx) l
+ guard $ sfx `T.isSuffixOf` l1
+ let l2 = T.take (T.length l1 - T.length sfx) l1
+ m1 <- eachFrom marker1
+ guard $ m1 `T.isPrefixOf` l2
+ let l3 = T.drop (T.length m1) l2
+ m2 <- eachFrom marker2
+ let (l3pfx, l4) = T.splitAt (T.length m2) l3
+ guard $ T.toLower l3pfx == m2
+ pure l4
+ in fmap T.unpack .
+ concatMap T.words .
+ observeAll . flagLines .
+ T.lines <$>
+ TIO.readFile srcFile
+
+
+makeCounterExamplesLLVM ::
+ Crux.Logs msgs =>
+ Log.SupportsCruxLLVMLogMessage msgs =>
+ CruxOptions -> LLVMOptions -> CruxSimulationResult -> IO ()
+makeCounterExamplesLLVM cruxOpts llvmOpts res
+ | makeCexes cruxOpts = mapM_ (go . snd) . Fold.toList $ (cruxSimResultGoals res)
+ | otherwise = return ()
+
+ where
+ go gs =
+ case gs of
+ Branch g1 g2 -> go g1 >> go g2
+ -- skip proved goals
+ ProvedGoal{} -> return ()
+ -- skip unknown goals
+ NotProvedGoal _ _ _ _ Nothing _ -> return ()
+ -- skip resource exhausted goals
+ NotProvedGoal _ (simErrorReason -> ResourceExhausted{}) _ _ _ _ -> return ()
+ -- counterexample to non-resource-exhaustion goal
+ NotProvedGoal _ c _ _ (Just (m,_evs)) _ ->
+ do let suff = case plSourceLoc (simErrorLoc c) of
+ SourcePos _ l _ -> show l
+ _ -> "unknown"
+ try (buildModelExes cruxOpts llvmOpts suff (ppModelC m)) >>= \case
+ Left (ex :: SomeException) -> do
+ logGoal gs
+ Log.sayCruxLLVM Log.FailedToBuildCounterexampleExecutable
+ logException ex
+ Right (_prt,dbg) -> do
+ Log.sayCruxLLVM (Log.Executable (T.pack dbg))
+ Log.sayCruxLLVM (Log.Breakpoint (T.pack suff))
+
+buildModelExes ::
+ Crux.Logs msgs =>
+ Log.SupportsCruxLLVMLogMessage msgs =>
+ CruxOptions -> LLVMOptions -> String -> String -> IO (FilePath,FilePath)
+buildModelExes cruxOpts llvmOpts suff counter_src =
+ do let dir = Crux.outDir cruxOpts
+ createDirectoryIfMissing True dir
+
+ let counterFile = dir ("counter-example-" ++ suff ++ ".c")
+ let printExe = dir ("print-model-" ++ suff)
+ let debugExe = dir ("debug-" ++ suff)
+ writeFile counterFile counter_src
+
+ let libs = libDir llvmOpts
+ incs = (libs "includes") :
+ (map takeDirectory files ++ incDirs llvmOpts)
+ files = (Crux.inputFiles cruxOpts)
+ libcxx | anyCPPFiles files = ["-lstdc++"]
+ | otherwise = []
+
+ runClang llvmOpts
+ [ "-I", libs "includes"
+ , counterFile
+ , libs "print-model.c"
+ , "-o", printExe
+ ]
+
+ runClang llvmOpts $
+ concat [ [ "-I", idir ] | idir <- incs ] ++
+ [ counterFile
+ , libs "concrete-backend.c"
+ , "-O0", "-g"
+ , "-o", debugExe
+ ] ++ files ++ libcxx
+
+ return (printExe, debugExe)
+
+
+ppValsC :: BaseTypeRepr ty -> Vals ty -> [String]
+ppValsC ty (Vals xs) =
+ let (cty, cnm, ppRawVal) = case ty of
+ BaseBVRepr n ->
+ ("int" ++ show n ++ "_t", "int" ++ show n ++ "_t", showBVLiteral n)
+ BaseFloatRepr (FloatingPointPrecisionRepr eb sb)
+ | Just Refl <- testEquality eb (knownNat @8)
+ , Just Refl <- testEquality sb (knownNat @24)
+ -> ("float", "float", showFloatLiteral)
+ BaseFloatRepr (FloatingPointPrecisionRepr eb sb)
+ | Just Refl <- testEquality eb (knownNat @11)
+ , Just Refl <- testEquality sb (knownNat @53)
+ -> ("double", "double", showDoubleLiteral)
+ BaseRealRepr -> ("double", "real", (show . toDouble))
+
+ _ -> error ("Type not implemented: " ++ show ty)
+ in [ "size_t const crucible_values_number_" ++ cnm ++
+ " = " ++ show (length xs) ++ ";"
+
+ , "const char* crucible_names_" ++ cnm ++ "[] = { " ++
+ intercalate "," (map (show . entryName) xs) ++ " };"
+
+ , cty ++ " const crucible_values_" ++ cnm ++ "[] = { " ++
+ intercalate "," (map (ppRawVal . entryValue) xs) ++ " };"
+ ]
+
+ppModelC :: ModelView -> String
+ppModelC m = unlines
+ $ "#include "
+ : "#include "
+ : "#include "
+ : ""
+ : concatMap ppModelForType llvmModelTypes
+ where
+ ppModelForType (Some tpr) =
+ case MapF.lookup tpr (modelVals m) of
+ -- NB, produce the declarations even if there are no variables
+ Nothing -> ppValsC tpr (Vals [])
+ Just vals -> ppValsC tpr vals
+
+
+llvmModelTypes :: [Some BaseTypeRepr]
+llvmModelTypes =
+ [ Some (BaseBVRepr (knownNat @8))
+ , Some (BaseBVRepr (knownNat @16))
+ , Some (BaseBVRepr (knownNat @32))
+ , Some (BaseBVRepr (knownNat @64))
+ , Some (BaseFloatRepr (FloatingPointPrecisionRepr (knownNat @8) (knownNat @24)))
+ , Some (BaseFloatRepr (FloatingPointPrecisionRepr (knownNat @11) (knownNat @53)))
+ ]
diff --git a/src/Crux/LLVM/Config.hs b/src/Crux/LLVM/Config.hs
new file mode 100644
--- /dev/null
+++ b/src/Crux/LLVM/Config.hs
@@ -0,0 +1,318 @@
+{-# 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 }
+ ]
+ }
diff --git a/src/Crux/LLVM/Log.hs b/src/Crux/LLVM/Log.hs
new file mode 100644
--- /dev/null
+++ b/src/Crux/LLVM/Log.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Crux.LLVM.Log
+ ( CruxLLVMLogMessage (..),
+ SupportsCruxLLVMLogMessage,
+ cruxLLVMLogMessageToSayWhat,
+ sayCruxLLVM,
+ )
+where
+
+import Crux.Log (SayLevel (..), SayWhat (..), cruxLogTag)
+import qualified Crux.Log as Log
+import Data.Aeson (ToJSON)
+import Data.Text as Text (Text, pack, unwords)
+import GHC.Generics (Generic)
+
+data CruxLLVMLogMessage
+ = Breakpoint Text
+ | ClangInvocation [Text]
+ | Executable Text
+ | FailedToBuildCounterexampleExecutable
+ | SimulatingFunction Text
+ | UsingPointerWidthForFile Integer Text
+ | TranslationWarning Text Text Text -- Function name, position, msg
+ deriving ( Generic, ToJSON )
+
+type SupportsCruxLLVMLogMessage msgs =
+ (?injectCruxLLVMLogMessage :: CruxLLVMLogMessage -> msgs)
+
+sayCruxLLVM ::
+ Log.Logs msgs =>
+ SupportsCruxLLVMLogMessage msgs =>
+ CruxLLVMLogMessage ->
+ IO ()
+sayCruxLLVM msg =
+ let ?injectMessage = ?injectCruxLLVMLogMessage
+ in Log.say msg
+
+clangLogTag :: Text
+clangLogTag = "CLANG"
+
+cruxLLVMLogMessageToSayWhat :: CruxLLVMLogMessage -> SayWhat
+cruxLLVMLogMessageToSayWhat (ClangInvocation params) =
+ SayWhat Noisily clangLogTag (Text.unwords params)
+cruxLLVMLogMessageToSayWhat (Breakpoint line) =
+ SayWhat Simply cruxLogTag ("*** break on line: " <> line)
+cruxLLVMLogMessageToSayWhat (Executable exe) =
+ SayWhat Simply cruxLogTag ("*** debug executable: " <> exe)
+cruxLLVMLogMessageToSayWhat FailedToBuildCounterexampleExecutable =
+ SayWhat Fail cruxLogTag "Failed to build counterexample executable"
+cruxLLVMLogMessageToSayWhat (SimulatingFunction function) =
+ SayWhat Simply cruxLogTag ("Simulating function " <> function)
+cruxLLVMLogMessageToSayWhat (UsingPointerWidthForFile width file) =
+ SayWhat
+ Simply
+ cruxLogTag
+ ( Text.unwords
+ [ "Using pointer width:",
+ pack (show width),
+ "for file",
+ file
+ ]
+ )
+cruxLLVMLogMessageToSayWhat (TranslationWarning nm p msg) =
+ SayWhat Warn cruxLogTag
+ ( Text.unwords
+ [ "Translation warning at"
+ , p
+ , "in"
+ , nm <> ":"
+ , msg
+ ]
+ )
diff --git a/src/Crux/LLVM/Overrides.hs b/src/Crux/LLVM/Overrides.hs
new file mode 100644
--- /dev/null
+++ b/src/Crux/LLVM/Overrides.hs
@@ -0,0 +1,570 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MagicHash #-}
+{-# Language ConstraintKinds #-}
+{-# Language DataKinds #-}
+{-# Language ImplicitParams #-}
+{-# Language LambdaCase #-}
+{-# Language PatternSynonyms #-}
+{-# Language QuasiQuotes #-}
+{-# Language RankNTypes #-}
+{-# Language TypeApplications #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeOperators #-}
+{-# Language ViewPatterns #-}
+module Crux.LLVM.Overrides
+ ( cruxLLVMOverrides
+ , svCompOverrides
+ , cbmcOverrides
+ , ArchOk
+ , TPtr
+ ) where
+
+import qualified Data.ByteString as BS
+import qualified Data.ByteString.Char8 as BS8
+import Control.Monad (when)
+import Control.Monad.IO.Class(liftIO)
+import GHC.Exts ( Proxy# )
+import System.IO (hPutStrLn)
+import qualified Data.Text as T
+
+import qualified Data.BitVector.Sized as BV
+import Data.Parameterized.Context.Unsafe (Assignment)
+import Data.Parameterized.Context(pattern Empty, pattern (:>), singleton)
+
+import What4.ProgramLoc( Position(..), ProgramLoc(..) )
+import What4.Symbol(userSymbol, emptySymbol, safeSymbol)
+import What4.Interface
+ (freshConstant, bvLit, bvAdd, asBV, predToBV,
+ getCurrentProgramLoc, printSymExpr, arrayUpdate, bvIsNonzero)
+
+import Lang.Crucible.Types
+import Lang.Crucible.CFG.Core(GlobalVar)
+import Lang.Crucible.Simulator.RegMap(regValue,RegValue,RegEntry)
+import Lang.Crucible.Simulator.ExecutionTree( printHandle )
+import Lang.Crucible.Simulator.OverrideSim
+ ( getContext
+ , readGlobal
+ , writeGlobal
+ , ovrWithBackend
+ )
+import Lang.Crucible.Simulator.SimError (SimErrorReason(..),SimError(..))
+import Lang.Crucible.Backend
+ ( IsSymInterface, IsSymBackend, addDurableAssertion
+ , addAssumption, LabeledPred(..), CrucibleAssumption(..)
+ , backendGetSym
+ )
+import Lang.Crucible.LLVM.QQ( llvmOvr )
+import Lang.Crucible.LLVM.DataLayout
+ (noAlignment)
+import Lang.Crucible.LLVM.MemModel
+ (Mem, LLVMPointerType, loadString, HasPtrWidth,
+ doMalloc, AllocType(HeapAlloc), Mutability(Mutable),
+ doArrayStore, doArrayConstStore, HasLLVMAnn,
+ isAllocatedAlignedPointer, Mutability(..),
+ pattern PtrWidth, doDumpMem, MemOptions
+ )
+
+import Lang.Crucible.LLVM.TypeContext( TypeContext )
+import Lang.Crucible.LLVM.Intrinsics
+
+import Lang.Crucible.LLVM.Extension ( ArchWidth )
+
+import qualified Crux.Overrides as Crux
+import Crux.Types
+
+-- | This happens quite a lot, so just a shorter name
+type ArchOk arch = HasPtrWidth (ArchWidth arch)
+type TPtr arch = LLVMPointerType (ArchWidth arch)
+type TBits n = BVType n
+
+
+cruxLLVMOverrides ::
+ ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
+ , ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
+ Proxy# arch ->
+ [OverrideTemplate (personality sym) sym arch rtp l a]
+cruxLLVMOverrides arch =
+ [ basic_llvm_override $
+ [llvmOvr| i8 @crucible_int8_t( i8* ) |]
+ (fresh_bits arch (knownNat @8))
+
+ , basic_llvm_override $
+ [llvmOvr| i16 @crucible_int16_t( i8* ) |]
+ (fresh_bits arch (knownNat @16))
+
+ , basic_llvm_override $
+ [llvmOvr| i32 @crucible_int32_t( i8* ) |]
+ (fresh_bits arch (knownNat @32))
+
+ , basic_llvm_override $
+ [llvmOvr| i64 @crucible_int64_t( i8* ) |]
+ (fresh_bits arch (knownNat @64))
+
+ , basic_llvm_override $
+ [llvmOvr| i8 @crucible_uint8_t( i8* ) |]
+ (fresh_bits arch (knownNat @8))
+
+ , basic_llvm_override $
+ [llvmOvr| i16 @crucible_uint16_t( i8* ) |]
+ (fresh_bits arch (knownNat @16))
+
+ , basic_llvm_override $
+ [llvmOvr| i32 @crucible_uint32_t( i8* ) |]
+ (fresh_bits arch (knownNat @32))
+
+ , basic_llvm_override $
+ [llvmOvr| i64 @crucible_uint64_t( i8* ) |]
+ (fresh_bits arch (knownNat @64))
+
+ , basic_llvm_override $
+ [llvmOvr| float @crucible_float( i8* ) |]
+ (fresh_float arch SingleFloatRepr)
+
+ , basic_llvm_override $
+ [llvmOvr| double @crucible_double( i8* ) |]
+ (fresh_float arch DoubleFloatRepr)
+
+ , basic_llvm_override $
+ [llvmOvr| i8* @crucible_string( i8*, size_t ) |]
+ (fresh_str arch)
+
+ , basic_llvm_override $
+ [llvmOvr| void @crucible_assume( i8, i8*, i32 ) |]
+ (do_assume arch)
+
+ , basic_llvm_override $
+ [llvmOvr| void @crucible_assert( i8, i8*, i32 ) |]
+ (do_assert arch)
+
+ , basic_llvm_override $
+ [llvmOvr| void @crucible_print_uint32( i32 ) |]
+ do_print_uint32
+
+ , basic_llvm_override $
+ [llvmOvr| void @crucible_havoc_memory( i8*, size_t ) |]
+ (do_havoc_memory arch)
+
+ , basic_llvm_override $
+ [llvmOvr| void @crucible_dump_memory( ) |]
+ (\mvar _sym _args ->
+ do mem <- readGlobal mvar
+ h <- printHandle <$> getContext
+ liftIO (doDumpMem h mem))
+ ]
+
+
+cbmcOverrides ::
+ ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
+ , ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
+ Proxy# arch ->
+ [OverrideTemplate (personality sym) sym arch rtp l a]
+cbmcOverrides arch =
+ [ basic_llvm_override $
+ [llvmOvr| void @__CPROVER_assume( i32 ) |]
+ cprover_assume
+ , basic_llvm_override $
+ [llvmOvr| void @__CPROVER_assert( i32, i8* ) |]
+ (cprover_assert arch)
+ , basic_llvm_override $
+ [llvmOvr| i1 @__CPROVER_r_ok( i8*, size_t ) |]
+ (cprover_r_ok arch)
+ , basic_llvm_override $
+ [llvmOvr| i1 @__CPROVER_w_ok( i8*, size_t ) |]
+ (cprover_w_ok arch)
+
+ , basic_llvm_override $
+ [llvmOvr| i1 @nondet_bool() |]
+ (sv_comp_fresh_bits (knownNat @1))
+ , basic_llvm_override $
+ [llvmOvr| i8 @nondet_char() |]
+ (sv_comp_fresh_bits (knownNat @8))
+ , basic_llvm_override $
+ [llvmOvr| i8 @nondet_uchar() |]
+ (sv_comp_fresh_bits (knownNat @8))
+ , basic_llvm_override $
+ [llvmOvr| i8 @nondet_uint8_t() |]
+ (sv_comp_fresh_bits (knownNat @8))
+ , basic_llvm_override $
+ [llvmOvr| i8 @nondet_int8_t() |]
+ (sv_comp_fresh_bits (knownNat @8))
+
+ , basic_llvm_override $
+ [llvmOvr| i16 @nondet_short() |]
+ (sv_comp_fresh_bits (knownNat @16))
+ , basic_llvm_override $
+ [llvmOvr| i16 @nondet_ushort() |]
+ (sv_comp_fresh_bits (knownNat @16))
+ , basic_llvm_override $
+ [llvmOvr| i16 @nondet_int16_t() |]
+ (sv_comp_fresh_bits (knownNat @16))
+ , basic_llvm_override $
+ [llvmOvr| i16 @nondet_uint16_t() |]
+ (sv_comp_fresh_bits (knownNat @16))
+
+ , basic_llvm_override $
+ [llvmOvr| i32 @nondet_int() |]
+ (sv_comp_fresh_bits (knownNat @32))
+ , basic_llvm_override $
+ [llvmOvr| i32 @nondet_uint() |]
+ (sv_comp_fresh_bits (knownNat @32))
+ , basic_llvm_override $
+ [llvmOvr| i32 @nondet_int32_t() |]
+ (sv_comp_fresh_bits (knownNat @32))
+ , basic_llvm_override $
+ [llvmOvr| i32 @nondet_uint32_t() |]
+ (sv_comp_fresh_bits (knownNat @32))
+
+ , basic_llvm_override $
+ [llvmOvr| i64 @nondet_int64_t() |]
+ (sv_comp_fresh_bits (knownNat @64))
+ , basic_llvm_override $
+ [llvmOvr| i64 @nondet_uint64_t() |]
+ (sv_comp_fresh_bits (knownNat @64))
+
+ -- @nondet_long@ returns a `long`, so we need two overrides for
+ -- @nondet_long@. Similarly for @nondet_ulong@.
+ -- See Note [Overrides involving (unsigned) long] in
+ -- crucible-llvm:Lang.Crucible.LLVM.Intrinsics.
+ , basic_llvm_override $
+ [llvmOvr| i32 @nondet_long() |]
+ (sv_comp_fresh_bits (knownNat @32))
+ , basic_llvm_override $
+ [llvmOvr| i64 @nondet_long() |]
+ (sv_comp_fresh_bits (knownNat @64))
+ , basic_llvm_override $
+ [llvmOvr| i32 @nondet_ulong() |]
+ (sv_comp_fresh_bits (knownNat @32))
+ , basic_llvm_override $
+ [llvmOvr| i64 @nondet_ulong() |]
+ (sv_comp_fresh_bits (knownNat @64))
+ , basic_llvm_override $
+ [llvmOvr| size_t @nondet_size_t() |]
+ (sv_comp_fresh_bits ?ptrWidth)
+
+ , basic_llvm_override $
+ [llvmOvr| float @nondet_float() |]
+ (sv_comp_fresh_float SingleFloatRepr)
+
+ , basic_llvm_override $
+ [llvmOvr| double @nondet_double() |]
+ (sv_comp_fresh_float DoubleFloatRepr)
+
+{-
+ , basic_llvm_override $
+ [llvmOvr| i8* @nondet_voidp() |]
+ (sv_comp_fresh_bits ?ptrWidth)
+-}
+ ]
+
+
+svCompOverrides ::
+ (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
+ [OverrideTemplate (personality sym) sym arch rtp l a]
+svCompOverrides =
+ [ basic_llvm_override $
+ [llvmOvr| i64 @__VERIFIER_nondet_longlong() |]
+ (sv_comp_fresh_bits (knownNat @64))
+
+ -- loff_t is pretty Linux-specific, so we can't point to the C or POSIX
+ -- standards for justification about what size it should be. The man page
+ -- for lseek64 (https://linux.die.net/man/3/lseek64) is as close to a
+ -- definitive reference for this as I can find, which says
+ -- "The type loff_t is a 64-bit signed type".
+ , basic_llvm_override $
+ [llvmOvr| i64 @__VERIFIER_nondet_loff_t() |]
+ (sv_comp_fresh_bits (knownNat @64))
+
+ -- @__VERIFIER_nondet_ulong@ returns an `unsigned long`, so we need two
+ -- overrides for @__VERIFIER_nondet_ulong@. Similarly for
+ -- @__VERIFIER_nondet_long@. See Note [Overrides involving (unsigned) long]
+ -- in crucible-llvm:Lang.Crucible.LLVM.Intrinsics.
+ , basic_llvm_override $
+ [llvmOvr| i32 @__VERIFIER_nondet_ulong() |]
+ (sv_comp_fresh_bits (knownNat @32))
+ , basic_llvm_override $
+ [llvmOvr| i64 @__VERIFIER_nondet_ulong() |]
+ (sv_comp_fresh_bits (knownNat @64))
+
+ , basic_llvm_override $
+ [llvmOvr| i32 @__VERIFIER_nondet_long() |]
+ (sv_comp_fresh_bits (knownNat @32))
+ , basic_llvm_override $
+ [llvmOvr| i64 @__VERIFIER_nondet_long() |]
+ (sv_comp_fresh_bits (knownNat @64))
+
+ , basic_llvm_override $
+ [llvmOvr| i32 @__VERIFIER_nondet_unsigned() |]
+ (sv_comp_fresh_bits (knownNat @32))
+
+ , basic_llvm_override $
+ [llvmOvr| i32 @__VERIFIER_nondet_u32() |]
+ (sv_comp_fresh_bits (knownNat @32))
+
+ , basic_llvm_override $
+ [llvmOvr| i32 @__VERIFIER_nondet_uint() |]
+ (sv_comp_fresh_bits (knownNat @32))
+
+ , basic_llvm_override $
+ [llvmOvr| i32 @__VERIFIER_nondet_int() |]
+ (sv_comp_fresh_bits (knownNat @32))
+
+ , basic_llvm_override $
+ [llvmOvr| i16 @__VERIFIER_nondet_u16() |]
+ (sv_comp_fresh_bits (knownNat @16))
+
+ , basic_llvm_override $
+ [llvmOvr| i16 @__VERIFIER_nondet_ushort() |]
+ (sv_comp_fresh_bits (knownNat @16))
+
+ , basic_llvm_override $
+ [llvmOvr| i16 @__VERIFIER_nondet_short() |]
+ (sv_comp_fresh_bits (knownNat @16))
+
+ , basic_llvm_override $
+ [llvmOvr| i8 @__VERIFIER_nondet_u8() |]
+ (sv_comp_fresh_bits (knownNat @8))
+
+ , basic_llvm_override $
+ [llvmOvr| i8 @__VERIFIER_nondet_uchar() |]
+ (sv_comp_fresh_bits (knownNat @8))
+
+ , basic_llvm_override $
+ [llvmOvr| i8 @__VERIFIER_nondet_char() |]
+ (sv_comp_fresh_bits (knownNat @8))
+
+ , basic_llvm_override $
+ [llvmOvr| i1 @__VERIFIER_nondet_bool() |]
+ (sv_comp_fresh_bits (knownNat @1))
+
+ , basic_llvm_override $
+ [llvmOvr| size_t @__VERIFIER_nondet_size_t() |]
+ (sv_comp_fresh_bits ?ptrWidth)
+
+ , basic_llvm_override $
+ [llvmOvr| float @__VERIFIER_nondet_float() |]
+ (sv_comp_fresh_float SingleFloatRepr)
+
+ , basic_llvm_override $
+ [llvmOvr| double @__VERIFIER_nondet_double() |]
+ (sv_comp_fresh_float DoubleFloatRepr)
+ ]
+
+--------------------------------------------------------------------------------
+
+lookupString ::
+ ( IsSymInterface sym, HasLLVMAnn sym, ArchOk arch
+ , ?memOpts :: MemOptions ) =>
+ Proxy# arch ->
+ GlobalVar Mem -> RegEntry sym (TPtr arch) -> OverM personality sym ext String
+lookupString _ mvar ptr =
+ ovrWithBackend $ \bak ->
+ do mem <- readGlobal mvar
+ bytes <- liftIO (loadString bak mem (regValue ptr) Nothing)
+ return (BS8.unpack (BS.pack bytes))
+
+sv_comp_fresh_bits ::
+ (IsSymBackend sym bak, 1 <= w) =>
+ NatRepr w ->
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) EmptyCtx ->
+ OverM personality sym ext (RegValue sym (BVType w))
+sv_comp_fresh_bits w _mvar _bak Empty = Crux.mkFresh (safeSymbol "X") (BaseBVRepr w)
+
+sv_comp_fresh_float ::
+ (IsSymBackend sym bak) =>
+ FloatInfoRepr fi ->
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) EmptyCtx ->
+ OverM personality sym ext (RegValue sym (FloatType fi))
+sv_comp_fresh_float fi _mvar _bak Empty = Crux.mkFreshFloat (safeSymbol "X") fi
+
+fresh_bits ::
+ ( ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w
+ , ?memOpts :: MemOptions ) =>
+ Proxy# arch ->
+ NatRepr w ->
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch) ->
+ OverM personality sym ext (RegValue sym (BVType w))
+fresh_bits arch w mvar _ (Empty :> pName) =
+ do name <- lookupString arch mvar pName
+ Crux.mkFresh (safeSymbol name) (BaseBVRepr w)
+
+fresh_float ::
+ ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym
+ , ?memOpts :: MemOptions ) =>
+ Proxy# arch ->
+ FloatInfoRepr fi ->
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch) ->
+ OverM personality sym ext (RegValue sym (FloatType fi))
+fresh_float arch fi mvar _ (Empty :> pName) =
+ do name <- lookupString arch mvar pName
+ Crux.mkFreshFloat (safeSymbol name) fi
+
+fresh_str ::
+ ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym
+ , ?memOpts :: MemOptions ) =>
+ Proxy# arch ->
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> BVType (ArchWidth arch)) ->
+ OverM personality sym ext (RegValue sym (TPtr arch))
+fresh_str arch mvar bak (Empty :> pName :> maxLen) =
+ do let sym = backendGetSym bak
+ name <- lookupString arch mvar pName
+
+ -- Compute the allocation length, which is the requested length plus one
+ -- to hold the NUL terminator
+ one <- liftIO $ bvLit sym ?ptrWidth (BV.one ?ptrWidth)
+ -- maxLenBV <- liftIO $ projectLLVM_bv sym (regValue maxLen)
+ len <- liftIO $ bvAdd sym (regValue maxLen) one
+ mem0 <- readGlobal mvar
+
+ -- Allocate memory to hold the string
+ (ptr, mem1) <- liftIO $ doMalloc bak HeapAlloc Mutable name mem0 len noAlignment
+
+ -- Allocate contents for the string - we want to make each byte symbolic,
+ -- so we allocate a fresh array (which has unbounded length) with symbolic
+ -- contents and write it into our allocation. This write does not cover
+ -- the NUL terminator.
+ contentsName <- case userSymbol (name ++ "_contents") of
+ Left err -> fail (show err)
+ Right nm -> return nm
+ let arrayRep = BaseArrayRepr (Empty :> BaseBVRepr ?ptrWidth) (BaseBVRepr (knownNat @8))
+ initContents <- liftIO $ freshConstant sym contentsName arrayRep
+ zeroByte <- liftIO $ bvLit sym (knownNat @8) (BV.zero knownNat)
+ -- Put the NUL terminator in place
+ initContentsZ <- liftIO $ arrayUpdate sym initContents (singleton (regValue maxLen)) zeroByte
+ mem2 <- liftIO $ doArrayConstStore bak mem1 ptr noAlignment initContentsZ len
+
+ writeGlobal mvar mem2
+ return ptr
+
+do_assume ::
+ ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym
+ , ?memOpts :: MemOptions ) =>
+ Proxy# arch ->
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) (EmptyCtx ::> TBits 8 ::> TPtr arch ::> TBits 32) ->
+ OverM personality sym ext (RegValue sym UnitType)
+do_assume arch mvar bak (Empty :> p :> pFile :> line) =
+ do let sym = backendGetSym bak
+ cond <- liftIO $ bvIsNonzero sym (regValue p)
+ file <- lookupString arch mvar pFile
+ l <- case asBV (regValue line) of
+ Just (BV.BV l) -> return (fromInteger l)
+ Nothing -> return 0
+ let pos = SourcePos (T.pack file) l 0
+ loc <- liftIO $ getCurrentProgramLoc sym
+ let loc' = loc{ plSourceLoc = pos }
+ liftIO $ addAssumption bak (GenericAssumption loc' "crucible_assume" cond)
+
+do_assert ::
+ ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym
+ , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
+ Proxy# arch ->
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) (EmptyCtx ::> TBits 8 ::> TPtr arch ::> TBits 32) ->
+ OverM personality sym ext (RegValue sym UnitType)
+do_assert arch mvar bak (Empty :> p :> pFile :> line) =
+ when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $
+ do let sym = backendGetSym bak
+ cond <- liftIO $ bvIsNonzero sym (regValue p)
+ file <- lookupString arch mvar pFile
+ l <- case asBV (regValue line) of
+ Just (BV.BV l) -> return (fromInteger l)
+ Nothing -> return 0
+ let pos = SourcePos (T.pack file) l 0
+ loc <- liftIO $ getCurrentProgramLoc sym
+ let loc' = loc{ plSourceLoc = pos }
+ let msg = GenericSimError "crucible_assert"
+ liftIO $ addDurableAssertion bak (LabeledPred cond (SimError loc' msg))
+
+do_print_uint32 ::
+ (IsSymBackend sym bak) =>
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) (EmptyCtx ::> TBits 32) ->
+ OverM personality sym ext (RegValue sym UnitType)
+do_print_uint32 _mvar _bak (Empty :> x) =
+ do h <- printHandle <$> getContext
+ liftIO $ hPutStrLn h (show (printSymExpr (regValue x)))
+
+do_havoc_memory ::
+ (ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) =>
+ Proxy# arch ->
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> TBits (ArchWidth arch)) ->
+ OverM personality sym ext (RegValue sym UnitType)
+do_havoc_memory _ mvar bak (Empty :> ptr :> len) =
+ do let sym = backendGetSym bak
+ let tp = BaseArrayRepr (Empty :> BaseBVRepr ?ptrWidth) (BaseBVRepr (knownNat @8))
+ mem <- readGlobal mvar
+ mem' <- liftIO $ do
+ arr <- freshConstant sym emptySymbol tp
+ doArrayStore bak mem (regValue ptr) noAlignment arr (regValue len)
+ writeGlobal mvar mem'
+
+cprover_assume ::
+ (IsSymBackend sym bak) =>
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) (EmptyCtx ::> TBits 32) ->
+ OverM personality sym ext (RegValue sym UnitType)
+cprover_assume _mvar bak (Empty :> p) = liftIO $
+ do let sym = backendGetSym bak
+ cond <- bvIsNonzero sym (regValue p)
+ loc <- getCurrentProgramLoc sym
+ addAssumption bak (GenericAssumption loc "__CPROVER_assume" cond)
+
+
+cprover_assert ::
+ ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym
+ , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
+ Proxy# arch ->
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) (EmptyCtx ::> TBits 32 ::> TPtr arch) ->
+ OverM personality sym ext (RegValue sym UnitType)
+cprover_assert arch mvar bak (Empty :> p :> pMsg) =
+ when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $
+ do let sym = backendGetSym bak
+ cond <- liftIO $ bvIsNonzero sym (regValue p)
+ str <- lookupString arch mvar pMsg
+ loc <- liftIO $ getCurrentProgramLoc sym
+ let msg = AssertFailureSimError "__CPROVER_assert" str
+ liftIO $ addDurableAssertion bak (LabeledPred cond (SimError loc msg))
+
+cprover_r_ok ::
+ (ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) =>
+ Proxy# arch ->
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> BVType (ArchWidth arch)) ->
+ OverM personality sym ext (RegValue sym (BVType 1))
+cprover_r_ok _ mvar bak (Empty :> (regValue -> p) :> (regValue -> sz)) =
+ do let sym = backendGetSym bak
+ mem <- readGlobal mvar
+ x <- liftIO $ isAllocatedAlignedPointer sym PtrWidth noAlignment Immutable p (Just sz) mem
+ liftIO $ predToBV sym x knownNat
+
+cprover_w_ok ::
+ (ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) =>
+ Proxy# arch ->
+ GlobalVar Mem ->
+ bak ->
+ Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> BVType (ArchWidth arch)) ->
+ OverM personality sym ext (RegValue sym (BVType 1))
+cprover_w_ok _ mvar bak (Empty :> (regValue -> p) :> (regValue -> sz)) =
+ do let sym = backendGetSym bak
+ mem <- readGlobal mvar
+ x <- liftIO $ isAllocatedAlignedPointer sym PtrWidth noAlignment Mutable p (Just sz) mem
+ liftIO $ predToBV sym x knownNat
diff --git a/src/Crux/LLVM/Simulate.hs b/src/Crux/LLVM/Simulate.hs
new file mode 100644
--- /dev/null
+++ b/src/Crux/LLVM/Simulate.hs
@@ -0,0 +1,414 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Crux.LLVM.Simulate where
+
+import qualified Data.BitVector.Sized as BV
+import Data.String (fromString)
+import qualified Data.Map.Strict as Map
+import Data.IORef
+import qualified Data.List as List
+import Data.Maybe ( fromMaybe )
+import qualified Data.Parameterized.Map as MapF
+import qualified Data.Traversable as T
+import Control.Lens ((&), (%~), (%=), (^.), use, view)
+import Control.Monad.IO.Class (liftIO)
+import Data.Text as Text (Text, pack)
+import GHC.Exts ( proxy# )
+
+import System.IO (stdout)
+
+import Data.Parameterized.Some (Some(..))
+import Data.Parameterized.Context (pattern Empty, pattern (:>))
+
+import Data.LLVM.BitCode (parseBitCodeFromFile)
+import qualified Text.LLVM as LLVM
+import Prettyprinter
+
+-- what4
+import qualified What4.Expr.Builder as WEB
+import What4.Interface (bvLit, natLit)
+
+-- crucible
+import Lang.Crucible.Backend
+import Lang.Crucible.Types
+import Lang.Crucible.CFG.Core(AnyCFG(..), CFG, cfgArgTypes)
+import Lang.Crucible.FunctionHandle(newHandleAllocator,HandleAllocator)
+import Lang.Crucible.Simulator
+ ( RegMap(..), assignReg, emptyRegMap
+ , fnBindingsFromList, runOverrideSim, callCFG
+ , initSimContext, profilingMetrics
+ , ExecState( InitialState ), GlobalVar
+ , SimState, defaultAbortHandler, printHandle
+ , ppSimError, ovrWithBackend
+ )
+import Lang.Crucible.Simulator.ExecutionTree ( actFrame, gpGlobals, stateGlobals, stateTree )
+import Lang.Crucible.Simulator.GlobalState ( insertGlobal, lookupGlobal )
+import Lang.Crucible.Simulator.Profiling ( Metric(Metric) )
+
+
+-- crucible-llvm
+import Lang.Crucible.LLVM(llvmExtensionImpl, llvmGlobals, registerLazyModule )
+import Lang.Crucible.LLVM.Bytes ( bytesToBV )
+import Lang.Crucible.LLVM.Globals
+ ( initializeAllMemory, populateAllGlobals )
+import Lang.Crucible.LLVM.MemModel
+ ( Mem, MemImpl, mkMemVar, withPtrWidth, memAllocCount, memWriteCount
+ , MemOptions(..), HasLLVMAnn, LLVMAnnMap
+ , explainCex, CexExplanation(..), doAlloca
+ , pattern LLVMPointer, pattern LLVMPointerRepr, LLVMPointerType
+ , pattern PtrRepr, pattern PtrWidth
+ )
+import Lang.Crucible.LLVM.MemModel.CallStack (ppCallStack)
+import Lang.Crucible.LLVM.MemType (MemType(..), SymType(..), i8, memTypeAlign, memTypeSize)
+import Lang.Crucible.LLVM.PrettyPrint (ppSymbol)
+import Lang.Crucible.LLVM.Translation
+ ( translateModule, ModuleTranslation, globalInitMap
+ , transContext, getTranslatedCFG, llvmPtrWidth, llvmTypeCtx
+ , LLVMTranslationWarning(..)
+ )
+import Lang.Crucible.LLVM.Intrinsics
+ (llvmIntrinsicTypes, register_llvm_overrides )
+
+import Lang.Crucible.LLVM.Errors( ppBB )
+import Lang.Crucible.LLVM.Extension( LLVM, ArchWidth )
+import Lang.Crucible.LLVM.SymIO
+ ( LLVMFileSystem, llvmSymIOIntrinsicTypes, symio_overrides, initialLLVMFileSystem, SomeOverrideSim(..) )
+import Lang.Crucible.LLVM.TypeContext (llvmDataLayout)
+import qualified Lang.Crucible.SymIO as SymIO
+import qualified Lang.Crucible.SymIO.Loader as SymIO.Loader
+
+-- crux
+import qualified Crux
+
+import Crux.Types
+import Crux.Log ( outputHandle )
+
+import Crux.LLVM.Config
+import qualified Crux.LLVM.Log as Log
+import Crux.LLVM.Overrides
+
+-- | Create a simulator context for the given architecture.
+setupSimCtxt ::
+ (IsSymBackend sym bak, HasLLVMAnn sym) =>
+ HandleAllocator ->
+ bak ->
+ MemOptions ->
+ GlobalVar Mem ->
+ SimCtxt Crux sym LLVM
+setupSimCtxt halloc bak mo memVar =
+ initSimContext bak
+ (MapF.union llvmIntrinsicTypes llvmSymIOIntrinsicTypes)
+ halloc
+ stdout
+ (fnBindingsFromList [])
+ (llvmExtensionImpl mo)
+ CruxPersonality
+ & profilingMetrics %~ Map.union (memMetrics memVar)
+
+-- | Parse an LLVM bit-code file.
+parseLLVM :: FilePath -> IO LLVM.Module
+parseLLVM file =
+ do ok <- parseBitCodeFromFile file
+ case ok of
+ Left err -> throwCError (LLVMParseError err)
+ Right m -> return m
+
+registerFunctions ::
+ Crux.Logs msgs =>
+ Log.SupportsCruxLLVMLogMessage msgs =>
+ (ArchOk arch, IsSymInterface sym, HasLLVMAnn sym, ptrW ~ ArchWidth arch) =>
+ LLVMOptions ->
+ LLVM.Module ->
+ ModuleTranslation arch ->
+ Maybe (LLVMFileSystem ptrW) ->
+ OverM Crux sym LLVM ()
+registerFunctions llvmOpts llvm_module mtrans fs0 =
+ do let llvm_ctx = mtrans ^. transContext
+ let ?lc = llvm_ctx ^. llvmTypeCtx
+ ?intrinsicsOpts = intrinsicsOpts llvmOpts
+ ?memOpts = memOpts llvmOpts
+
+ -- register the callable override functions
+ register_llvm_overrides llvm_module []
+ (concat [ cruxLLVMOverrides proxy#
+ , svCompOverrides
+ , cbmcOverrides proxy#
+ , maybe [] symio_overrides fs0
+ ])
+ llvm_ctx
+
+ -- register all the functions defined in the LLVM module
+ registerLazyModule sayTranslationWarning mtrans
+
+simulateLLVMFile ::
+ Crux.Logs msgs =>
+ Log.SupportsCruxLLVMLogMessage msgs =>
+ -- | Path to the LLVM module
+ FilePath ->
+ LLVMOptions ->
+ Crux.SimulatorCallbacks msgs Crux.Types.CruxSimulationResult
+simulateLLVMFile llvm_file llvmOpts =
+ Crux.SimulatorCallbacks $
+ do bbMapRef <- newIORef (Map.empty :: LLVMAnnMap sym)
+ let ?recordLLVMAnnotation =
+ \callStack an bb ->
+ modifyIORef bbMapRef (Map.insert an (callStack, bb))
+ return $
+ Crux.SimulatorHooks
+ { Crux.setupHook =
+ \bak maybeOnline ->
+ do halloc <- newHandleAllocator
+ setupFileSim halloc llvm_file llvmOpts bak maybeOnline
+ , Crux.onErrorHook =
+ \bak -> return (explainFailure (backendGetSym bak) bbMapRef)
+ , Crux.resultHook = \_sym result -> return result
+ }
+
+setupFileSim :: forall sym bak t st fs msgs
+ . Crux.Logs msgs
+ => Log.SupportsCruxLLVMLogMessage msgs
+ => IsSymBackend sym bak
+ => sym ~ WEB.ExprBuilder t st fs
+ => HasLLVMAnn sym
+ => HandleAllocator
+ -> FilePath
+ -> LLVMOptions
+ -> bak
+ -> Maybe (Crux.SomeOnlineSolver sym bak)
+ -> IO (Crux.RunnableState sym)
+setupFileSim halloc llvm_file llvmOpts bak _maybeOnline =
+ do let sym = backendGetSym bak
+ memVar <- mkMemVar "crux:llvm_memory" halloc
+
+ let simctx = (setupSimCtxt halloc bak (memOpts llvmOpts) memVar)
+ { printHandle = view outputHandle ?outputConfig }
+
+ prepped <- prepLLVMModule llvmOpts halloc bak llvm_file memVar
+
+ let globSt = llvmGlobals memVar (prepMem prepped)
+
+ Some trans <- return $ prepSomeTrans prepped
+ llvmPtrWidth (trans ^. transContext) $ \ptrW -> withPtrWidth ptrW $ do
+ mContents <- T.traverse (SymIO.Loader.loadInitialFiles sym) (symFSRoot llvmOpts)
+ -- We modify the defaults, which are extremely conservative. Unless the
+ -- user directs otherwise, we default to connecting stdin, stdout, and stderr.
+ let defaultFileContents = (SymIO.emptyInitialFileSystemContents @sym)
+ { SymIO.useStderr = True
+ , SymIO.useStdout = True
+ , SymIO.concreteFiles = Map.fromList [(SymIO.StdinTarget, mempty)]
+ }
+ let fsContents = fromMaybe defaultFileContents mContents
+ let mirroredOutputs = [ (SymIO.StdoutTarget, ?outputConfig ^. Crux.outputHandle)
+ , (SymIO.StderrTarget, ?outputConfig ^. Crux.outputHandle)
+ ]
+ (fs0, globSt', SomeOverrideSim initFSOverride) <- initialLLVMFileSystem halloc sym ptrW fsContents mirroredOutputs globSt
+ return $ Crux.RunnableState $
+ InitialState simctx globSt' defaultAbortHandler UnitRepr $
+ runOverrideSim UnitRepr $
+ withPtrWidth ptrW $
+ do registerFunctions llvmOpts (prepLLVMMod prepped) trans (Just fs0)
+ initFSOverride
+ checkFun llvmOpts trans memVar
+
+
+data PreppedLLVM sym = PreppedLLVM { prepLLVMMod :: LLVM.Module
+ , prepSomeTrans :: Some ModuleTranslation
+ , prepMemVar :: GlobalVar Mem
+ , prepMem :: MemImpl sym
+ }
+
+-- | Given an LLVM Bitcode file, and a GlobalVar memory, translate the
+-- file into the Crucible representation and add the globals and
+-- definitions from the file to the GlobalVar memory.
+
+prepLLVMModule :: IsSymBackend sym bak
+ => HasLLVMAnn sym
+ => Crux.Logs msgs
+ => Log.SupportsCruxLLVMLogMessage msgs
+ => LLVMOptions
+ -> HandleAllocator
+ -> bak
+ -> FilePath -- for the LLVM bitcode file
+ -> GlobalVar Mem
+ -> IO (PreppedLLVM sym)
+prepLLVMModule llvmOpts halloc bak bcFile memVar = do
+ llvmMod <- parseLLVM bcFile
+ Some trans <-
+ let ?transOpts = transOpts llvmOpts
+ in translateModule halloc memVar llvmMod
+ mem <- let llvmCtxt = trans ^. transContext in
+ let ?lc = llvmCtxt ^. llvmTypeCtx
+ ?memOpts = memOpts llvmOpts
+ in llvmPtrWidth llvmCtxt $ \ptrW ->
+ withPtrWidth ptrW $ do
+ Log.sayCruxLLVM (Log.UsingPointerWidthForFile (intValue ptrW) (Text.pack bcFile))
+ populateAllGlobals bak (trans ^. globalInitMap)
+ =<< initializeAllMemory bak llvmCtxt llvmMod
+ return $ PreppedLLVM llvmMod (Some trans) memVar mem
+
+sayTranslationWarning ::
+ Log.SupportsCruxLLVMLogMessage msgs =>
+ Crux.Logs msgs =>
+ LLVMTranslationWarning -> IO ()
+sayTranslationWarning = Log.sayCruxLLVM . f
+ where
+ f (LLVMTranslationWarning s p msg) =
+ Log.TranslationWarning (Text.pack (show (ppSymbol s))) (Text.pack (show p)) msg
+
+checkFun ::
+ forall arch msgs personality sym.
+ IsSymInterface sym =>
+ HasLLVMAnn sym =>
+ ArchOk arch =>
+ Crux.Logs msgs =>
+ Log.SupportsCruxLLVMLogMessage msgs =>
+ LLVMOptions ->
+ ModuleTranslation arch ->
+ GlobalVar Mem ->
+ OverM personality sym LLVM ()
+checkFun llvmOpts trans memVar =
+ liftIO (getTranslatedCFG trans (fromString nm)) >>= \case
+ Just (_, AnyCFG anyCfg, warns) ->
+ do liftIO (mapM_ sayTranslationWarning warns)
+ case cfgArgTypes anyCfg of
+ Empty -> simulateFun anyCfg emptyRegMap
+
+ (Empty :> LLVMPointerRepr w :> PtrRepr)
+ | isMain, shouldSupplyMainArguments
+ , Just Refl <- testEquality w (knownNat @32)
+ -> checkMainWithArguments anyCfg
+
+ _ -> throwCError (BadFun nm isMain) -- TODO(lb): Suggest uc-crux-llvm?
+
+ Nothing -> throwCError (MissingFun nm)
+ where
+ nm = entryPoint llvmOpts
+ isMain = nm == "main"
+ shouldSupplyMainArguments =
+ case supplyMainArguments llvmOpts of
+ NoArguments -> False
+ EmptyArguments -> True
+
+ simulateFun :: CFG LLVM blocks ctx ret ->
+ RegMap sym ctx ->
+ OverM personality sym LLVM ()
+ simulateFun anyCfg args = do
+ liftIO $ Log.sayCruxLLVM (Log.SimulatingFunction (Text.pack nm))
+ callCFG anyCfg args >> return ()
+
+ -- Simulate a function with the signature @int main(int argc, char* argv[])@.
+ -- We do so by behaving as if we are starting from this entrypoint:
+ --
+ -- int crucible_main() {
+ -- int argc = 0;
+ -- char *argv[] = {};
+ -- return main(argc, argv);
+ -- }
+ --
+ -- @argc@ can easily be created with 'bvLit'. For @argv@, we have to choose
+ -- what sort of allocation we want when creating its @LLVMPointer@. We've
+ -- opted for 'doAlloca' since the LLVM bitcode to allocate @argv@ will use
+ -- the @alloca@ instruction. This means that @argv@ will be
+ -- stack-allocated, which is a reasonable choice, given that the @main@
+ -- function's @argv@ argument actually lives on the stack in most binaries.
+ checkMainWithArguments ::
+ CFG LLVM blocks (EmptyCtx ::> LLVMPointerType 32 ::> TPtr arch) ret ->
+ OverM personality sym LLVM ()
+ checkMainWithArguments anyCfg = ovrWithBackend $ \bak -> do
+ let ?memOpts = memOpts llvmOpts
+ let w = knownNat @32
+ dl = llvmDataLayout (trans^.transContext.llvmTypeCtx)
+ tp = ArrayType 0 (PtrType (MemType i8))
+ tp_sz = memTypeSize dl tp
+ alignment = memTypeAlign dl tp
+ loc = "crux-llvm main(argc, argv) simulation"
+ sym = backendGetSym bak
+
+ gs <- use (stateTree.actFrame.gpGlobals)
+ mem <- case lookupGlobal memVar gs of
+ Just mem -> pure mem
+ Nothing -> fail "checkFun.checkMainWithArguments: Memory missing from global vars"
+ argc <- liftIO $ LLVMPointer <$> natLit sym 0 <*> bvLit sym w (BV.zero w)
+ sz <- liftIO $ bvLit sym PtrWidth $ bytesToBV PtrWidth tp_sz
+ (argv, mem') <- liftIO $ doAlloca bak mem sz alignment loc
+ stateTree.actFrame.gpGlobals %= insertGlobal memVar mem'
+
+ let args = assignReg PtrRepr argv $
+ assignReg (LLVMPointerRepr w) argc emptyRegMap
+ simulateFun anyCfg args
+
+---------------------------------------------------------------------
+-- Profiling
+
+memMetrics :: forall p sym ext
+ . GlobalVar Mem
+ -> Map.Map Text (Metric p sym ext)
+memMetrics memVar = Map.fromList
+ -- Note: These map keys are used by profile.js in
+ -- https://github.com/GaloisInc/sympro-ui and must
+ -- match the names there.
+ [ ("LLVM.allocs", allocs)
+ , ("LLVM.writes", writes)
+ ]
+ where
+ allocs = Metric $ measureMemBy memAllocCount
+ writes = Metric $ measureMemBy memWriteCount
+
+ measureMemBy :: (MemImpl sym -> Int)
+ -> SimState p sym ext r f args
+ -> IO Integer
+ measureMemBy f st = do
+ let globals = st ^. stateGlobals
+ case lookupGlobal memVar globals of
+ Just mem -> return $ toInteger (f mem)
+ Nothing -> fail "Memory missing from global vars"
+
+----------------------------------------------------------------------
+
+-- arbitrary, we should probably make this limit configurable
+detailLimit :: Int
+detailLimit = 10
+
+explainFailure :: IsSymInterface sym
+ => sym ~ WEB.ExprBuilder t st fs
+ => sym
+ -> IORef (LLVMAnnMap sym)
+ -> Crux.Explainer sym t ann
+explainFailure sym bbMapRef evalFn gl =
+ do bb <- readIORef bbMapRef
+ ex <- explainCex sym bb evalFn >>= \f -> f (gl ^. labeledPred)
+ let details =
+ case ex of
+ NoExplanation -> mempty
+ DisjOfFailures xs ->
+ case ppBBPair <$> xs of
+ [] -> mempty
+ [x] -> indent 2 x
+ xs' ->
+ let xs'' = List.take detailLimit xs'
+ xs'l = length xs'
+ msg1 = "Failing conditions::"
+ msg2 = if xs'l > detailLimit
+ then "[only displaying the first"
+ <+> pretty detailLimit
+ <+> "of" <+> pretty xs'l
+ <+> "failed conditions]"
+ else "Total failed conditions:" <+> pretty xs'l
+ in nest 2 $ vcat $ msg1 : xs'' <> [msg2]
+ return $ vcat [ ppSimError (gl^. labeledPredMsg), details ]
+ where ppBBPair (callStack, bb) =
+ vsep [ ppBB bb
+ , "in context:"
+ , indent 2 (ppCallStack callStack)
+ ]
diff --git a/src/CruxLLVMMain.hs b/src/CruxLLVMMain.hs
new file mode 100644
--- /dev/null
+++ b/src/CruxLLVMMain.hs
@@ -0,0 +1,112 @@
+{-# Language DeriveAnyClass #-}
+{-# Language DeriveGeneric #-}
+{-# Language ImplicitParams #-}
+{-# Language LambdaCase #-}
+{-# Language OverloadedStrings #-}
+{-# Language RankNTypes #-}
+
+module CruxLLVMMain
+ ( CruxLLVMLogging
+ , cruxLLVMLoggingToSayWhat
+ , defaultOutputConfig
+ , mainWithOptions
+ , mainWithOutputTo
+ , mainWithOutputConfig
+ , Crux.mkOutputConfig
+ , processLLVMOptions
+ , withCruxLLVMLogging
+ )
+ where
+
+import Data.Aeson ( ToJSON )
+import GHC.Generics ( Generic )
+import System.Directory ( createDirectoryIfMissing )
+import System.Exit ( ExitCode )
+import System.FilePath ( dropExtension, takeFileName, () )
+import System.IO ( Handle )
+
+-- crux
+import qualified Crux
+import qualified Crux.Log as Log
+import Crux.Config.Common (CruxOptions(..), OutputOptions)
+
+-- local
+import Crux.LLVM.Config
+import Crux.LLVM.Compile
+import qualified Crux.LLVM.Log as Log
+import Crux.LLVM.Simulate
+import Paths_crux_llvm (version)
+
+
+mainWithOutputTo :: Handle -> IO ExitCode
+mainWithOutputTo h = mainWithOutputConfig $
+ Crux.mkOutputConfig (h, True) (h, True) cruxLLVMLoggingToSayWhat
+
+data CruxLLVMLogging
+ = LoggingCrux Crux.CruxLogMessage
+ | LoggingCruxLLVM Log.CruxLLVMLogMessage
+ deriving ( Generic, ToJSON )
+
+cruxLLVMLoggingToSayWhat :: CruxLLVMLogging -> Crux.SayWhat
+cruxLLVMLoggingToSayWhat (LoggingCrux msg) = Log.cruxLogMessageToSayWhat msg
+cruxLLVMLoggingToSayWhat (LoggingCruxLLVM msg) = Log.cruxLLVMLogMessageToSayWhat msg
+
+defaultOutputConfig :: IO (Maybe OutputOptions -> Log.OutputConfig CruxLLVMLogging)
+defaultOutputConfig = Crux.defaultOutputConfig cruxLLVMLoggingToSayWhat
+
+withCruxLLVMLogging ::
+ (
+ Log.SupportsCruxLogMessage CruxLLVMLogging =>
+ Log.SupportsCruxLLVMLogMessage CruxLLVMLogging =>
+ a
+ ) -> a
+withCruxLLVMLogging a =
+ let
+ ?injectCruxLogMessage = LoggingCrux
+ ?injectCruxLLVMLogMessage = LoggingCruxLLVM
+ in a
+
+mainWithOutputConfig ::
+ (Maybe OutputOptions -> Log.OutputConfig CruxLLVMLogging) ->
+ IO ExitCode
+mainWithOutputConfig mkOutCfg = withCruxLLVMLogging $ do
+ cfg <- llvmCruxConfig
+ Crux.loadOptions mkOutCfg "crux-llvm" version cfg mainWithOptions
+
+mainWithOptions ::
+ Log.Logs msgs =>
+ Log.SupportsCruxLogMessage msgs =>
+ Log.SupportsCruxLLVMLogMessage msgs =>
+ (CruxOptions, LLVMOptions) -> IO ExitCode
+mainWithOptions initOpts =
+ do
+ (cruxOpts, llvmOpts) <- processLLVMOptions initOpts
+ bcFile <- genBitCode cruxOpts llvmOpts
+ res <- Crux.runSimulator cruxOpts $ simulateLLVMFile bcFile llvmOpts
+ makeCounterExamplesLLVM cruxOpts llvmOpts res
+ Crux.postprocessSimResult True cruxOpts res
+
+processLLVMOptions :: (CruxOptions,LLVMOptions) -> IO (CruxOptions,LLVMOptions)
+processLLVMOptions (cruxOpts,llvmOpts) =
+ do -- keep looking for clangBin if it is unset
+ clangFilePath <- if clangBin llvmOpts == ""
+ then getClang
+ else return (clangBin llvmOpts)
+
+ let llvmOpts2 = llvmOpts { clangBin = clangFilePath }
+
+ -- update outDir if unset
+ name <- case Crux.inputFiles cruxOpts of
+ x : _ -> pure (dropExtension (takeFileName x))
+ -- use the first file as output directory
+ [] -> throwCError NoFiles
+
+ let cruxOpts2 = if Crux.outDir cruxOpts == ""
+ then cruxOpts { Crux.outDir = "results" name }
+ else cruxOpts
+
+ odir = Crux.outDir cruxOpts2
+
+ createDirectoryIfMissing True odir
+
+ return (cruxOpts2, llvmOpts2)
diff --git a/svcomp/Main.hs b/svcomp/Main.hs
new file mode 100644
--- /dev/null
+++ b/svcomp/Main.hs
@@ -0,0 +1,255 @@
+{- | This is the SVCOMP utility for crux-llvm. It is designed to run
+ the inputs for the "Competition on Software Verification" (SV-COMP).
+ Specifically, it takes as inputs:
+
+ * A file containing a specification to check, and
+
+ * An architecture (either @32bit@ or @64bit@) to assume, and
+
+ * A input C file.
+
+ It will then attempt to verify the file against that specification,
+ eventually printing @VERIFIED@, @FALSIFIED@, or @UNKNOWN@ depending on the
+ results. If the result is @VERIFIED@ or @FALSFIED@, it will also produce a
+ witness automaton which represents a proof that the program does or does not
+ meet the specification.
+-}
+
+{-# Language DeriveAnyClass #-}
+{-# Language DeriveGeneric #-}
+{-# Language ImplicitParams #-}
+{-# Language OverloadedStrings #-}
+{-# Language RankNTypes #-}
+
+module Main (main) where
+
+import Control.Applicative ( Alternative(..) )
+import Control.Exception ( SomeException, try )
+import Control.Monad.Extra ( whenJust )
+import qualified Crypto.Hash.SHA256 as SHA256 ( hash )
+import Data.Aeson ( ToJSON )
+import qualified Data.Attoparsec.Text as Atto
+import qualified Data.ByteString.Base16 as B16 ( encode )
+import qualified Data.ByteString.Char8 as B ( readFile, unpack )
+import Data.Foldable ( traverse_, toList )
+import Data.Function ( on )
+import Data.Functor.Identity ( Identity(..) )
+import Data.Functor.WithIndex ( FunctorWithIndex(..) )
+import qualified Data.List.Extra as L
+import Data.Maybe ( mapMaybe )
+import Data.Sequence ( Seq )
+import qualified Data.Text as T
+import qualified Data.Text.Encoding as T
+import Data.Time.LocalTime ( getZonedTime )
+import Data.Version ( showVersion )
+import GHC.Generics ( Generic )
+import System.Exit ( exitFailure, exitSuccess )
+import System.FilePath ( () )
+
+-- crucible
+import Lang.Crucible.Backend ( CrucibleEvent(..) )
+
+-- crux
+import qualified Crux
+import Crux.Config.Common ( CruxOptions(..), outputOptions )
+import qualified Crux.Log as Log
+import Crux.Report
+import Crux.SVCOMP hiding (SVCompLanguage(..))
+import Crux.SVCOMP.Witness
+import Crux.Types as Crux
+
+-- what4
+import What4.Expr.GroundEval ( GroundValueWrapper )
+import What4.ProgramLoc ( Position(..), ProgramLoc, plFunction, plSourceLoc )
+
+-- local
+import Crux.LLVM.Compile
+import Crux.LLVM.Config
+import qualified Crux.LLVM.Log as Log
+import Crux.LLVM.Simulate
+import CruxLLVMMain ( processLLVMOptions )
+import Paths_crux_llvm (version)
+import qualified SVComp.Log as Log
+
+data SVCompLogging
+ = LoggingCrux Log.CruxLogMessage
+ | LoggingCruxLLVM Log.CruxLLVMLogMessage
+ | LoggingSVComp Log.SVCompLogMessage
+ deriving (Generic, ToJSON)
+
+svCompLoggingToSayWhat :: SVCompLogging -> SayWhat
+svCompLoggingToSayWhat (LoggingCrux msg) = Log.cruxLogMessageToSayWhat msg
+svCompLoggingToSayWhat (LoggingCruxLLVM msg) = Log.cruxLLVMLogMessageToSayWhat msg
+svCompLoggingToSayWhat (LoggingSVComp msg) = Log.svCompLogMessageToSayWhat msg
+
+withSVCompLogging ::
+ ( ( Log.SupportsCruxLogMessage SVCompLogging
+ , Log.SupportsCruxLLVMLogMessage SVCompLogging
+ , Log.SupportsSVCompLogMessage SVCompLogging
+ ) => computation ) ->
+ computation
+withSVCompLogging computation = do
+ let ?injectCruxLogMessage = LoggingCrux
+ ?injectCruxLLVMLogMessage = LoggingCruxLLVM
+ ?injectSVCompLogMessage = LoggingSVComp
+ in computation
+
+main :: IO ()
+main = withSVCompLogging $ do
+ cfg <- llvmCruxConfig
+ let opts = Crux.cfgJoin cfg svcompOptions
+ mkOutCfg <- Crux.defaultOutputConfig svCompLoggingToSayWhat
+ Crux.loadOptions mkOutCfg "crux-llvm-svcomp" version opts
+ $ \(co0,(lo0,svOpts)) ->
+ do (cruxOpts, llvmOpts) <- processLLVMOptions (co0{ outDir = "results" "SVCOMP" },lo0)
+ svOpts' <- processSVCOMPOptions svOpts
+ let tgt = case runIdentity $ svcompArch svOpts' of
+ Arch32 -> "i386-unknown-linux-elf"
+ Arch64 -> "x86_64-unknown-linux-elf"
+ llvmOpts' = llvmOpts { targetArch = Just tgt }
+ processInputFiles cruxOpts llvmOpts' svOpts'
+
+processInputFiles :: Log.Logs msgs
+ => Log.SupportsCruxLLVMLogMessage msgs
+ => Log.SupportsSVCompLogMessage msgs
+ => CruxOptions -> LLVMOptions -> SVCOMPOptions Identity
+ -> IO ()
+processInputFiles cruxOpts llvmOpts svOpts =
+ traverse_ process $ Crux.inputFiles cruxOpts
+ where
+ process :: FilePath -> IO ()
+ process inputFile = do
+ mbBcFile <- genBitCodeMaybe inputFile
+ whenJust mbBcFile $ \bcFile ->
+ evaluateBitCode inputFile bcFile
+
+ genBitCodeMaybe :: FilePath -> IO (Maybe FilePath)
+ genBitCodeMaybe inputFile
+ | or [ L.isSuffixOf bl inputFile | bl <- svcompBlacklist svOpts ]
+ = do Log.saySVComp (Log.Skipping Log.DueToBlacklist (T.pack inputFile))
+ return Nothing
+ | otherwise
+ = Just <$> genBitCode cruxOpts llvmOpts
+
+ evaluateBitCode :: FilePath -> FilePath -> IO ()
+ evaluateBitCode inputFile bcFile = withSVCompLogging $ do
+ mkOutCfg <- Crux.defaultOutputConfig svCompLoggingToSayWhat
+ let ?outputConfig = mkOutCfg (Just (outputOptions cruxOpts))
+ mres <- try $
+ do res <- Crux.runSimulator cruxOpts (simulateLLVMFile bcFile llvmOpts)
+ generateReport cruxOpts res
+ return res
+
+ case mres of
+ Left e ->
+ do Log.saySVComp Log.SimulatorThrewException
+ Log.logException (e :: SomeException)
+ exitFailure
+
+ Right res@(CruxSimulationResult cmpl gls) ->
+ do let numTotalGoals = sum (Crux.totalProcessedGoals . fst <$> gls)
+ let numDisprovedGoals = sum (Crux.disprovedGoals . fst <$> gls)
+ let numProvedGoals = sum (Crux.provedGoals . fst <$> gls)
+
+ let verdict
+ | numDisprovedGoals > 0 = Falsified
+ | ProgramComplete <- cmpl
+ , numProvedGoals == numTotalGoals = Verified
+ | otherwise = Unknown
+
+ specFileContents <- B.readFile $ runIdentity $ svcompSpec svOpts
+ let specFileText = T.decodeUtf8 specFileContents
+ prop <- case Atto.parseOnly propParse specFileText of
+ Left msg ->
+ do Log.saySVComp $ Log.PropertyParseError specFileText (T.pack msg)
+ exitFailure
+ Right p -> return p
+
+ witType <- case verdict of
+ Verified -> do Crux.logSimResult True res
+ Log.saySVComp $ Log.Verdict Verified prop
+ pure CorrectnessWitness
+ Falsified -> do Crux.logSimResult True res
+ Log.saySVComp $ Log.Verdict Falsified prop
+ pure ViolationWitness
+ Unknown -> do Log.saySVComp $ Log.Verdict Unknown prop
+ exitSuccess
+
+ inputFileContents <- B.readFile inputFile
+ creationTime <- getZonedTime
+ let mkWitness nodes edges = Witness
+ { witnessType = witType
+ , witnessSourceCodeLang = C
+ , witnessProducer = "crux-llvm-" ++ showVersion version
+ , witnessSpecification = L.trim $ B.unpack specFileContents
+ , witnessProgramFile = inputFile
+ , witnessProgramHash = B16.encode $ SHA256.hash inputFileContents
+ , witnessArchitecture = runIdentity $ svcompArch svOpts
+ , witnessCreationTime = creationTime
+ , witnessNodes = nodes
+ , witnessEdges = edges
+ }
+ trivialCorrectnessWitness = mkWitness [(mkNode 0) { nodeEntry = Just True }] []
+
+ writeFile (svcompWitnessOutput svOpts) $ ppWitness $ case witType of
+ CorrectnessWitness -> trivialCorrectnessWitness
+ ViolationWitness -> let (nodes, edges) = mkViolationWitness $ fmap snd gls
+ in mkWitness nodes edges
+
+mkViolationWitness :: Seq ProvedGoals -> ([WitnessNode], [WitnessEdge])
+mkViolationWitness gs =
+ case L.firstJust findNotProvedGoal $ toList gs of
+ Nothing -> error "Could not find event log for counterexample"
+ Just (_mv, events) ->
+ let locs = -- It is possible for certain LLVM instructions which do not
+ -- directly map back to source locations to be given a line
+ -- number of 0. (See #862 for an example.) Line number 0
+ -- wreaks havoc on witness validators, so we filter out such
+ -- locations to avoid this.
+ filter ((/= Just 0) . programLocSourcePosLine) $
+ -- Witness validators aren't hugely fond of using the same
+ -- line number multiple times successively, so remove
+ -- consecutive duplicates.
+ removeRepeatsBy ((==) `on` programLocSourcePosLine) $
+ mapMaybe locationReachedEventLoc events
+ edges = imap violationEdge locs
+ nodes = violationNodes $ length edges
+ in (nodes, edges)
+ where
+ findNotProvedGoal :: ProvedGoals -> Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
+ findNotProvedGoal (Branch pg1 pg2) = findNotProvedGoal pg1 <|> findNotProvedGoal pg2
+ findNotProvedGoal (NotProvedGoal _ _ _ _ x _) = x
+ findNotProvedGoal ProvedGoal{} = Nothing
+
+ violationNodes :: Int -> [WitnessNode]
+ violationNodes numEdges =
+ map (\idx -> (mkNode idx)
+ { nodeEntry = if idx == 0 then Just True else Nothing
+ , nodeViolation = if idx == numEdges then Just True else Nothing
+ })
+ [0..numEdges]
+
+ locationReachedEventLoc :: CrucibleEvent GroundValueWrapper -> Maybe ProgramLoc
+ locationReachedEventLoc (LocationReachedEvent loc) = Just loc
+ locationReachedEventLoc CreateVariableEvent{} = Nothing
+
+ violationEdge :: Int -> ProgramLoc -> WitnessEdge
+ violationEdge idx loc =
+ let mbSourcePos = programLocSourcePos loc in
+ (mkEdge idx (idx+1))
+ { edgeStartLine = fst <$> mbSourcePos
+ , edgeAssumptionScope = Just $ show $ plFunction loc
+ -- crux-llvm–specific extensions
+ , edgeStartColumn = snd <$> mbSourcePos
+ }
+
+ programLocSourcePos :: ProgramLoc -> Maybe (Int, Int)
+ programLocSourcePos pl =
+ case plSourceLoc pl of
+ SourcePos _ l c -> Just (l, c)
+ BinaryPos{} -> Nothing
+ OtherPos{} -> Nothing
+ InternalPos -> Nothing
+
+ programLocSourcePosLine :: ProgramLoc -> Maybe Int
+ programLocSourcePosLine = fmap fst . programLocSourcePos
diff --git a/svcomp/SVComp/Log.hs b/svcomp/SVComp/Log.hs
new file mode 100644
--- /dev/null
+++ b/svcomp/SVComp/Log.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module SVComp.Log
+ ( SupportsSVCompLogMessage,
+ SVCompLogMessage (..),
+ SVCompSkipReason (..),
+ saySVComp,
+ svCompLogMessageToSayWhat,
+ )
+where
+
+import Crux (SayLevel (..), SayWhat (..))
+import qualified Crux.Log as Log
+import Crux.SVCOMP (ComputedVerdict (..), SVCompProperty (..))
+import Data.Aeson (ToJSON)
+import qualified Data.Text as T
+import GHC.Generics (Generic)
+
+data SVCompSkipReason
+ = DueToBlacklist
+ | NoInputFiles
+ deriving (Generic, ToJSON)
+
+svCompSkipReasonSuffix :: SVCompSkipReason -> T.Text
+svCompSkipReasonSuffix DueToBlacklist = " due to blacklist"
+svCompSkipReasonSuffix NoInputFiles = " because no input files are present"
+
+data SVCompLogMessage
+ = SimulatorThrewException
+ | PropertyParseError T.Text T.Text
+ | Skipping SVCompSkipReason T.Text
+ | Verdict ComputedVerdict SVCompProperty
+ deriving (Generic, ToJSON)
+
+type SupportsSVCompLogMessage msgs =
+ (?injectSVCompLogMessage :: SVCompLogMessage -> msgs)
+
+saySVComp ::
+ Log.Logs msgs =>
+ SupportsSVCompLogMessage msgs =>
+ SVCompLogMessage ->
+ IO ()
+saySVComp msg =
+ let ?injectMessage = ?injectSVCompLogMessage
+ in Log.say msg
+
+
+svCompTag :: T.Text
+svCompTag = "SVCOMP"
+
+svCompFail :: T.Text -> SayWhat
+svCompFail = SayWhat Fail svCompTag
+
+svCompOK :: T.Text -> SayWhat
+svCompOK = SayWhat OK svCompTag
+
+svCompWarn :: T.Text -> SayWhat
+svCompWarn = SayWhat Warn svCompTag
+
+resultPrefix :: T.Text
+resultPrefix = "Verification result: "
+
+svCompLogMessageToSayWhat :: SVCompLogMessage -> SayWhat
+svCompLogMessageToSayWhat SimulatorThrewException =
+ svCompFail $ T.unlines
+ [ resultPrefix <> "ERROR"
+ , "Simulator threw exception"
+ ]
+svCompLogMessageToSayWhat (PropertyParseError prop msg) =
+ svCompFail $ T.unlines
+ [ resultPrefix <> "ERROR"
+ , "Could not parse property:" <> prop
+ , msg
+ ]
+svCompLogMessageToSayWhat (Skipping reason path) =
+ svCompWarn
+ ( T.unlines
+ [ "Skipping:",
+ " " <> path <> svCompSkipReasonSuffix reason
+ ]
+ )
+svCompLogMessageToSayWhat (Verdict verdict prop) =
+ case verdict of
+ Verified -> svCompOK $ resultPrefix <> "VERIFIED"
+ Falsified -> svCompOK $ resultPrefix <> "FALSIFIED (" <> displayProp prop <> ")"
+ Unknown -> svCompWarn $ resultPrefix <> "UNKNOWN"
+ where
+ displayProp CheckValidFree = "valid-free"
+ displayProp CheckValidDeref = "valid-deref"
+ displayProp CheckValidMemtrack = "valid-memtrack"
+ displayProp CheckValidMemCleanup = "valid-memcleanup"
+ displayProp CheckNoOverflow = "no-overflow"
+ displayProp CheckTerminates = "termination"
+ displayProp CheckNoError{} = "unreach-call"
+ displayProp CheckDefBehavior = "def-behavior"
+ displayProp CoverageFQL{} = "coverage"
diff --git a/test/Test.hs b/test/Test.hs
new file mode 100644
--- /dev/null
+++ b/test/Test.hs
@@ -0,0 +1,411 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Main where
+
+import Control.Exception ( SomeException, catches, try, Handler(..), IOException )
+import Control.Lens ( (^?), _Right )
+import Control.Monad ( unless, when )
+import Data.Bifunctor ( first )
+import qualified Data.ByteString.Lazy as BSIO
+import qualified Data.ByteString.Lazy.Char8 as BSC
+import Data.Char ( isLetter, isSpace )
+import Data.List.Extra ( isInfixOf, isPrefixOf )
+import Data.Maybe ( catMaybes, fromMaybe )
+import qualified Data.Text as T
+import Data.Versions ( Versioning, versioning, prettyV, major )
+import qualified GHC.IO.Exception as GE
+import Numeric.Natural
+import System.Environment ( withArgs, lookupEnv )
+import System.Exit ( ExitCode(..) )
+import System.FilePath ( (-<.>) )
+import System.IO
+import System.Process ( readProcess )
+import Text.Read ( readMaybe )
+import Text.Regex.Base ( makeRegex, match, matchM )
+import Text.Regex.Posix.ByteString.Lazy ( Regex )
+
+import qualified Test.Tasty as TT
+import Test.Tasty.HUnit ( testCase, assertFailure )
+import qualified Test.Tasty.Sugar as TS
+
+import qualified CruxLLVMMain as C
+
+
+cube :: TS.CUBE
+cube = TS.mkCUBE { TS.inputDirs = ["test-data/golden"]
+ , TS.rootName = "*.c"
+ , TS.separators = "."
+ , TS.expectedSuffix = "good"
+ , TS.validParams = [ ("solver", Just ["z3", "cvc5"])
+ , ("loop-merging", Just ["loopmerge", "loop"])
+ , ("clang-range", Just [ "recent-clang"
+ , "pre-clang11"
+ , "pre-clang12"
+ , "pre-clang13"
+ , "pre-clang14"
+ , "pre-clang15"
+ , "pre-clang16"
+ ])
+ ]
+ , TS.associatedNames = [ ("config", "config")
+ , ("test-result", "result")
+ ]
+ }
+
+main :: IO ()
+main = do clangVer <- getClangVersion
+ let cubes = [ cube { TS.inputDirs = [dir]
+ , TS.rootName = rootName
+ , TS.sweetAdjuster =
+ TS.rangedParamAdjuster
+ "clang-range"
+ (readMaybe . drop (length ("pre-clang"::String)))
+ (<)
+ (vcVersioning clangVer ^? (_Right . major))
+ }
+ | dir <- [ "test-data/golden"
+ , "test-data/golden/golden"
+ , "test-data/golden/golden-loop-merging"
+ , "test-data/golden/stdio"
+ ]
+ , rootName <- [ "*.c", "*.ll" ]
+ ]
+ sweets <- concat <$> mapM TS.findSugar cubes
+
+ tests <- TS.withSugarGroups sweets TT.testGroup mkTest
+
+ let ingredients = TT.includingOptions TS.sugarOptions :
+ TS.sugarIngredients cubes <>
+ TT.defaultIngredients
+ TT.defaultMainWithIngredients ingredients $
+ TT.testGroup "crux-llvm"
+ [ TT.testGroup (showVC clangVer) $ tests ]
+
+
+-- lack of decipherable version is not fatal to running the tests
+data VersionCheck = VC String (Either T.Text Versioning)
+
+showVC :: VersionCheck -> String
+showVC (VC nm v) = nm <> " " <> (T.unpack $ either id prettyV v)
+
+vcVersioning :: VersionCheck -> Either T.Text Versioning
+vcVersioning (VC _ v) = v
+
+mkVC :: String -> String -> VersionCheck
+mkVC nm raw = let r = T.pack raw in VC nm $ first (const r) $ versioning r
+
+getClangVersion :: IO VersionCheck
+getClangVersion = do
+ -- Determine which version of clang will be used for these tests.
+ -- An exception (E.g. in the readProcess if clang is not found) will
+ -- result in termination (test failure). Uses partial 'head' but
+ -- this is just tests, and failure is captured.
+ clangBin <- fromMaybe "clang" <$> lookupEnv "CLANG"
+ let isVerLine = isInfixOf "clang version"
+ dropLetter = dropWhile (all isLetter)
+ -- Remove any characters that give `versions` parsers a hard time, such
+ -- as tildes (cf. https://github.com/fosskers/versions/issues/62).
+ -- These have been observed in the wild (e.g., 12.0.0-3ubuntu1~20.04.5).
+ scrubProblemChars = filter (/= '~')
+ getVer (Right inp) =
+ -- example inp: "clang version 10.0.1"
+ scrubProblemChars $ head $ dropLetter $ words $
+ head $ filter isVerLine $ lines inp
+ getVer (Left full) = full
+ mkVC "clang" . getVer <$> readProcessVersion clangBin
+
+getZ3Version :: IO VersionCheck
+getZ3Version =
+ let getVer (Right inp) =
+ -- example inp: "Z3 version 4.8.7 - 64 bit"
+ let w = words inp
+ in if and [ length w > 2, head w == "Z3" ]
+ then w !! 2 else "?"
+ getVer (Left full) = full
+ in mkVC "z3" . getVer <$> readProcessVersion "z3"
+
+getYicesVersion :: IO VersionCheck
+getYicesVersion =
+ let getVer (Right inp) =
+ -- example inp: "Yices 2.6.1\nCopyright ..."
+ let w = words inp
+ in if and [ length w > 1, head w == "Yices" ]
+ then w !! 1 else "?"
+ getVer (Left full) = full
+ in mkVC "yices" . getVer <$> readProcessVersion "yices"
+
+getSTPVersion :: IO VersionCheck
+getSTPVersion =
+ let getVer (Right inp) =
+ -- example inp: "STP version 2.3.3\n..."
+ let w = words inp
+ in if and [ length w > 2
+ , head w == "STP"
+ , w !! 1 == "version" ]
+ then w !! 2 else "?"
+ getVer (Left full) = full
+ in mkVC "stp" . getVer <$> readProcessVersion "stp"
+
+getCVC4Version :: IO VersionCheck
+getCVC4Version =
+ let getVer (Right inp) =
+ -- example inp: "This is CVC4 version 1.8\ncompiled ..."
+ let w = words inp
+ in if and [ length w > 4
+ , "This is CVC4 version" `isPrefixOf` inp
+ ]
+ then w !! 4 else "?"
+ getVer (Left full) = full
+ in mkVC "cvc4" . getVer <$> readProcessVersion "cvc4"
+
+getCVC5Version :: IO VersionCheck
+getCVC5Version =
+ let getVer (Right inp) =
+ -- example inp: "This is cvc5 version 1.0.2\ncompiled ..."
+ let w = words inp
+ in if and [ length w > 4
+ , "This is cvc5 version" `isPrefixOf` inp
+ ]
+ then w !! 4 else "?"
+ getVer (Left full) = full
+ in mkVC "cvc5" . getVer <$> readProcessVersion "cvc5"
+
+getBoolectorVersion :: IO VersionCheck
+getBoolectorVersion =
+ let getVer (Right inp) =
+ -- example inp: "3.2.1"
+ let w = words inp
+ in if not (null w) then head w else "?"
+ getVer (Left full) = full
+ in mkVC "boolector" . getVer <$> readProcessVersion "boolector"
+
+readProcessVersion :: String -> IO (Either String String)
+readProcessVersion forTool =
+ catches (Right <$> readProcess forTool [ "--version" ] "")
+ [ Handler $ \(e :: IOException) ->
+ if GE.ioe_type e == GE.NoSuchThing
+ then return $ Left "[missing]" -- tool executable not found
+ else do putStrLn $ "Warning: IO error attempting to determine " <> forTool <> " version:"
+ putStrLn $ show e
+ return $ Left "unknown"
+ , Handler $ \(e :: SomeException) -> do
+ putStrLn $ "Warning: error attempting to determine " <> forTool <> " version:"
+ putStrLn $ show e
+ return $ Left "??"
+ ]
+
+sanitize :: [BSC.ByteString] -> [BSC.ByteString]
+sanitize blines =
+ let -- when a Callstack is reported in the result output, it contains lines like:
+ --
+ -- > error, called at src/foo.hs:369:3 in pkgname-1.0.3.5-{cabal-hash-loc}:Foo
+ --
+ -- and the problem is that {cabal-hash-loc} varies, so
+ -- removeHashedLoc attempts to strip that portion from these
+ -- lines.
+ removeHashedLoc l =
+ let w = BSC.words l
+ in if take 3 w == ["error,", "called", "at"]
+ then BSC.unwords $ take 4 w
+ else l
+ -- If crux tries to generate and compile counter-examples, but
+ -- the original source is incomplete (e.g. contains references
+ -- to unresolved externals) then the crux attempt to link will
+ -- fail. The linking output generates lines like:
+ --
+ -- /absolute/path/of/ld: /absolute/path/for/ex3-undef-XXXXXX.o: in function `generate_value':
+ -- /absolute/path/to/ex3-undef.c:11: undefined reference to `update_value'
+ --
+ -- Both of these outputs are problematic:
+ -- 1 - they contain absolute paths, which can change in different environments
+ -- (the first one contains two absolute paths).
+ -- 2 - The XXXXXX portion is a mktemp file substitution value that will change
+ -- each time the test is run.
+ --
+ -- The fix here is to remove the first word on the line
+ -- (recursively) if it starts with a / character and ends with a
+ -- : character.
+ cleanLinkerOutput l =
+ if BSC.null l then l
+ else let (w1,rest) = BSC.break isSpace $ BSC.dropWhile isSpace l
+ in if and [ "/" == BSC.take 1 w1
+ , ":" == (BSC.take 1 $ BSC.reverse w1)
+ ]
+ then cleanLinkerOutput rest
+ else l
+
+ -- The SMT formulas suggested by the --get-abducts flag are extremely
+ -- sensitive to which versions of CVC5 and LLVM you are using. To avoid
+ -- checking in a ridiculous number of expected output combinations for
+ -- --get-abducts test cases, we scrub out the SMT formulas post facto.
+ -- This ensures that all of the relevant code paths are being exercised
+ -- while maintaining a single expected output file for each test case.
+ cleanAbductOutput :: [BSC.ByteString] -> [BSC.ByteString]
+ cleanAbductOutput [] = []
+ cleanAbductOutput (l:ls) =
+ if | -- If a line matches the error message regex, then scrub the SMT
+ -- formulas from the next lines of output.
+ match reSingle l
+ , l':ls' <- ls
+ -> l : cleanSMTFormula l' : cleanAbductOutput ls'
+ | Just ( _before :: BSC.ByteString
+ , _matched :: BSC.ByteString
+ , _after :: BSC.ByteString
+ , [numBS]
+ ) <- matchM rePlural l
+
+ , Just num <- readMaybe (BSC.unpack numBS)
+ -> let (before, after) = splitAt num ls in
+ l : map cleanSMTFormula before ++ cleanAbductOutput after
+
+ -- Otherwise, leave the line unchanged.
+ | otherwise
+ -> l : cleanAbductOutput ls
+ where
+ reSingle, rePlural :: Regex
+ reSingle = makeRegex bsSingle
+ rePlural = makeRegex bsPlural
+
+ -- NB: These are the same error messages that is printed out in crux's
+ -- Crux.FormatOut module, but with some regex-specific twists on top
+ -- of them. This code should stay in sync with any chages to those
+ -- error messages.
+ bsSingle, bsPlural :: BSC.ByteString
+ bsSingle = "The following fact would entail the goal"
+ bsPlural = "One of the following ([0-9]+) facts would entail the goal"
+
+ cleanSMTFormula :: BSC.ByteString -> BSC.ByteString
+ cleanSMTFormula line =
+ BSC.takeWhile (/= '*') line <> "* "
+
+ in cleanAbductOutput $
+ cleanLinkerOutput . removeHashedLoc <$> blines
+
+assertBSEq :: FilePath -> FilePath -> IO ()
+assertBSEq expectedFile actualFile = do
+ expected <- BSIO.readFile expectedFile
+ actual <- BSIO.readFile actualFile
+ let el = sanitize $ BSC.lines expected
+ al = sanitize $ BSC.lines actual
+ unless (el == al) $ do
+ let dl (e,a) = if e == a then db e else de e <> da a
+ db b = [" F |" <> b]
+ de e = [" F-expect>|" <> e]
+ da a = [" F-actual>|" <> a]
+ let details = concat $
+ [ [ "MISMATCH for expected (" <> BSC.pack expectedFile <> ")"
+ , " and actual (" <> BSC.pack actualFile <> ") output:"
+ ]
+ -- Highly simplistic "diff" output assumes
+ -- correlated lines: added or removed lines just
+ -- cause everything to shown as different from
+ -- that point forward.
+ , concatMap dl $ zip el al
+ , concatMap de $ drop (length al) el
+ , concatMap da $ drop (length el) al
+ ]
+ assertFailure $ BSC.unpack (BSC.unlines details)
+
+
+mkTest :: TS.Sweets -> Natural -> TS.Expectation -> IO [TT.TestTree]
+mkTest sweet _ expct =
+ let solver = maybe "z3"
+ (\case
+ (TS.Explicit s) -> s
+ (TS.Assumed s) -> s
+ TS.NotSpecified -> "z3")
+ $ lookup "solver" (TS.expParamsMatch expct)
+ outFile = TS.expectedFile expct -<.> "." <> solver <> ".out"
+ tname = TS.rootBaseName sweet
+ runCruxName = tname <> " crux run"
+ resFName = outFile -<.> ".result.out"
+
+ runCrux = Just $ testCase runCruxName $ do
+ let cfargs = catMaybes
+ [
+ ("--config=" <>) <$> lookup "config" (TS.associated expct)
+ , Just $ "--solver=" <> solver
+ , Just "--quiet"
+ ]
+ failureMsg = let bss = BSIO.pack . fmap (toEnum . fromEnum) . show in \case
+ Left e -> "***[test]*** Crux failed with exception: " <> bss (show (e :: SomeException)) <> "\n"
+ Right (ExitFailure v) -> "***[test]*** Crux failed with non-zero result: " <> bss (show v) <> "\n"
+ Right ExitSuccess -> ""
+ r <- withFile outFile WriteMode $ \h ->
+ (try $
+ withArgs (cfargs <> [TS.rootFile sweet]) $
+ let coloredOutput = False
+ in (C.mainWithOutputConfig $ C.mkOutputConfig (h, coloredOutput) (h, coloredOutput) C.cruxLLVMLoggingToSayWhat))
+ BSIO.writeFile resFName $ failureMsg r
+
+ checkResult =
+ let runTest s = testCase (tname <> " crux result") $
+ assertBSEq s resFName
+ in runTest <$> lookup "test-result" (TS.associated expct)
+
+ checkOutput = Just $ testCase (tname <> " crux output") $
+ assertBSEq (TS.expectedFile expct) outFile
+
+ in do
+ solverVer <- showVC <$> case solver of
+ "z3" -> getZ3Version
+ "yices" -> getYicesVersion
+ "stp" -> getSTPVersion
+ "cvc4" -> getCVC4Version
+ "cvc5" -> getCVC5Version
+ "boolector" -> getBoolectorVersion
+ _ -> return $ VC solver $ Left "unknown-solver-for-version"
+
+ -- Some tests take longer, so only run one of them in fast-test mode
+
+ testLevel <- fromMaybe "0" <$> lookupEnv "CI_TEST_LEVEL"
+
+ -- Allow issue_478_unsafe/loop-merging to always run, but identify
+ -- all other tests taking 20s or greater as longTests.
+
+ let longTests = or [ and [ TS.rootBaseName sweet == "issue_478_unsafe"
+ , fromMaybe True
+ (TS.paramMatchVal "loop" <$>
+ lookup "loop-merging" (TS.expParamsMatch expct))
+ ]
+ , TS.rootBaseName sweet == "nested"
+ , TS.rootBaseName sweet == "nested_unsafe"
+ ]
+
+ -- If a .good file begins with SKIP_TEST, skip that test entirely. For test
+ -- cases that require a minimum Clang version, this technique is used to
+ -- prevent running the test on older Clang versions.
+
+ skipTest <- ("SKIP_TEST" `BSIO.isPrefixOf`) <$> BSIO.readFile (TS.expectedFile expct)
+
+ if or [ skipTest, testLevel == "0" && longTests ]
+ then do
+ when (testLevel == "0" && longTests) $
+ putStrLn "*** Longer running test skipped; set CI_TEST_LEVEL=1 env var to enable"
+ return []
+ else do
+ let isLoopMerge = TS.paramMatchVal "loopmerge" <$>
+ lookup "loop-merging" (TS.expParamsMatch expct)
+ cfg = lookup "config" (TS.associated expct)
+ case (isLoopMerge, cfg) of
+ (Just True, Nothing) ->
+ -- No config for loopmerge, so suppress identical run.
+ -- This is an optimization: it would not be wrong to run
+ -- these tests, but since the loopmerge and loop
+ -- configurations are identical, extra tests are run that
+ -- don't provide any additional information.
+ return []
+ _ -> return
+ [
+ TT.testGroup solverVer
+ [ TT.testGroup (TS.rootBaseName sweet) $ catMaybes
+ [
+ runCrux
+ , TT.after TT.AllSucceed runCruxName <$> checkResult
+ , TT.after TT.AllSucceed runCruxName <$> checkOutput
+ ]
+ ]
+ ]