crux-llvm (empty) → 0.8
raw patch · 25 files changed
+3808/−0 lines, 25 filesdep +aesondep +attoparsecdep +base
Dependencies added: aeson, attoparsec, base, base16-bytestring, bv-sized, bytestring, config-schema, containers, crucible, crucible-llvm, crucible-symio, crux, crux-llvm, cryptohash-sha256, directory, extra, filepath, indexed-traversable, lens, llvm-pretty, llvm-pretty-bc-parser, logict, lumberjack, mtl, parameterized-utils, prettyprinter, process, regex-base, regex-posix, tasty, tasty-hunit, tasty-sugar, text, time, unix, versions, websockets, what4
Files
- CHANGELOG.md +51/−0
- LICENSE +30/−0
- README.md +581/−0
- c-src/concrete-backend.c +45/−0
- c-src/includes/crucible-model.h +32/−0
- c-src/includes/crucible.h +55/−0
- c-src/libcxx-3.6.2.bc too large to diff
- c-src/libcxx-7.1.0.bc too large to diff
- c-src/print-model.c +26/−0
- crux-llvm.cabal +184/−0
- exe/Main.hs +6/−0
- exe/unix/RealMain.hs +25/−0
- exe/windows/RealMain.hs +9/−0
- for-ide/Main.hs +94/−0
- for-ide/unix/RealMain.hs +34/−0
- for-ide/windows/RealMain.hs +14/−0
- src/Crux/LLVM/Compile.hs +365/−0
- src/Crux/LLVM/Config.hs +318/−0
- src/Crux/LLVM/Log.hs +77/−0
- src/Crux/LLVM/Overrides.hs +570/−0
- src/Crux/LLVM/Simulate.hs +414/−0
- src/CruxLLVMMain.hs +112/−0
- svcomp/Main.hs +255/−0
- svcomp/SVComp/Log.hs +100/−0
- test/Test.hs +411/−0
+ CHANGELOG.md view
@@ -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`.
+ LICENSE view
@@ -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.
+ README.md view
@@ -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`:+ <https://www.haskell.org/ghcup/>++* The Yices SMT solver: <http://yices.csl.sri.com/>++* The Z3 SMT solver: <https://github.com/Z3Prover/z3/releases>++* The Clang compiler and LLVM toolchain: <http://releases.llvm.org/download.html>++ 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 <stdint.h>+#ifdef CRUCIBLE+#include <crucible.h>+#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": [<SymFilePair>],+ "useStdout": bool,+ "useStderr": bool+}++SymFilePair := [ FilePath, <SymbolicFileContents> ]++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 `<test-case>.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+`<test-case>.pre-clang<version>.<...>.good` files, where `pre-clang<version>`+indicates that this test output is used for all Clang versions up to (but not+including) `<version>`. Note that if a test case has multiple+`pre-clang<version>` `.good` files, then the `<version>` 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+`<version>`, create a `pre-clang<version>` `.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 `<version>`. 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).
+ c-src/concrete-backend.c view
@@ -0,0 +1,45 @@+#include <stdio.h>+#include <stdlib.h>+#include <crucible.h>+#include <crucible-model.h>++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"); }++
+ c-src/includes/crucible-model.h view
@@ -0,0 +1,32 @@+#ifndef CRUCIBLE_MODEL_H+#define CRUCIBLE_MODEL_H++#ifdef __cplusplus__+extern "C" {+#endif //__cplusplus__++#include <stdint.h>+#include <stddef.h>++#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+
+ c-src/includes/crucible.h view
@@ -0,0 +1,55 @@+#ifndef CRUCIBLE_H+#define CRUCIBLE_H++#ifdef __cplusplus+extern "C" {+#endif //__cplusplus++#include <stdbool.h>+#include <stdint.h>+#include <stddef.h>++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
+ c-src/libcxx-3.6.2.bc view
file too large to diff
+ c-src/libcxx-7.1.0.bc view
file too large to diff
+ c-src/print-model.c view
@@ -0,0 +1,26 @@+#include <crucible-model.h>+#include <stdio.h>+#include <inttypes.h>++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;+}
+ crux-llvm.cabal view
@@ -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
+ exe/Main.hs view
@@ -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)
+ exe/unix/RealMain.hs view
@@ -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
+ exe/windows/RealMain.hs view
@@ -0,0 +1,9 @@+module RealMain (main) where++import System.Exit+import CruxLLVMMain (mainWithOutputConfig, defaultOutputConfig)++main :: IO ()+main =+ do ec <- mainWithOutputConfig =<< defaultOutputConfig+ exitWith ec
+ for-ide/Main.hs view
@@ -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
+ for-ide/unix/RealMain.hs view
@@ -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
+ for-ide/windows/RealMain.hs view
@@ -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
+ src/Crux/LLVM/Compile.hs view
@@ -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 <stdint.h>"+ : "#include <stddef.h>"+ : "#include <math.h>"+ : ""+ : 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)))+ ]
+ src/Crux/LLVM/Config.hs view
@@ -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 }+ ]+ }
+ src/Crux/LLVM/Log.hs view
@@ -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+ ]+ )
+ src/Crux/LLVM/Overrides.hs view
@@ -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
+ src/Crux/LLVM/Simulate.hs view
@@ -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)+ ]
+ src/CruxLLVMMain.hs view
@@ -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)
+ svcomp/Main.hs view
@@ -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
+ svcomp/SVComp/Log.hs view
@@ -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"
+ test/Test.hs view
@@ -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 <num> 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 <> "* <unstable SMT formula output removed>"++ 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+ ]+ ]+ ]