Crux v0.9

Crux Updates

MIR Updates

• Add support for GHC 9.8
• Constant slice updates in accordance with downstream changes from crucible-mir.

LLVM Updates

• Add support for GHC 9.8
• The type signatures in Crux.LLVM.Overrides now use fewer type parameters in the OverrideTemplates that they return, in accordance with downstream changes from crucible-llvm.

Crux v0.8

New features

• [LLVM] Add support for LLVM bitcode files produced by Apple Clang on macOS.
• [LLVM] Implement overrides for the LLVM llvm.is.fpclass.f* intrinsics.
• [LLVM] Implement overrides for the isinf, __isinf, and __isinff C functions.
• [LLVM] Implement overrides for the LLVM llvm.fma.f* and llvm.fmuladd.f* intrinsics.
• [LLVM] Implement overrides for the fma and fmaf C functions.
• [MIR] Support the nightly-2023-01-23 Rust toolchain. Some of the highlights of this include:
  • Properly support for Rust's new constant forms
  • Better support for zero-sized constants
  • Encoding enum discriminant types so that crux-mir can know about non-isize discriminant types (e.g., Ordering, which uses an i8 discriminant)
  • A more intelligent way of computing crate disambiguators for looking up known types such as MaybeUninit and Option
• [MIR] Support enums marked with repr(transparent).

Crux v0.7

New features

• [LLVM and MIR] Added support for the cvc5 SMT solver.

• [LLVM] 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.

• [LLVM] 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.

• [LLVM] Support LLVM versions up to 16.

Crux v0.6

New features

• [LLVM] Improved support for translating LLVM debug metadata when the debug-intrinsics option is enabled, including metadata that defines metadata nodes after they are used.

• [LLVM] 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.

• [LLVM] Certain error messages now print the call stack of functions leading up to the error.

Bug fixes

• [LLVM] Make --help and --version respect the --no-colors flag.

• [MIR] Any-typed local variables are no longer initialized to a default value, which prevents spurious assertion failures if these variables become involved in symbolic branches in certain cases.

Crux v0.5

Changes

• [LLVM] Define CRUCIBLE when compiling input source code, making it easier for analysis harnesses to behave differently when running under Crux than during normal compilation.

• [LLVM] Support for LLVM 11 and 12.

• [MIR] We no longer bundle binaries for mir-json, since getting Cargo to find them is a little awkward. Instead, you'll need to install mir-json using Cargo yourself before running crux-mir. See the mir-json README for details.

New Features

• [LLVM] Include header files in HTML source rendering.

• [LLVM] Include crux-llvm-svcomp, a front end that can process the metadata used in the Software Verification Competition.

• [LLVM] Include crux-llvm-for-ide to support IDE integration. Can be used with an associated Visual Studio Code extension.

• [LLVM] Support detection of freeing already-freed pointers as distinct from frees of non-pointers.

• [LLVM] Support for symbolic I/O.

• [LLVM] Allow arguments to the entry point function, using the supply-main-arguments option. The entry point is assumed to have the typical (int argc, char **argv) type signature typical of the main function. A line of words will be passed to the entry point in the same way as done by the shell. The single word empty implies argc=0 and argv = {}.

• [MIR] Include checks for overflow of multiplication, division, and remainder calculations.

Performance Improvements

• [LLVM] Optimization of early loop exits, as described in issue #478.

Docker Notes

• [MIR] To use the crux-mir Docker container, the following command is useful for running cargo crux-test on the package in the current directory:

    docker run --rm -it --mount type=bind,source=$(pwd),target="/crux-mir/workspace" ghcr.io/galoisinc/crux-mir:0.5
  

Crux v0.4

This is the first official release of Crux, and currently includes binaries for the C/C++ (LLVM) and Rust (MIR) versions of the tool. An overview of Crux and its capabilities can be found here.

The LLVM version requires the clang and llvm-link executables included in LLVM releases, and is has been tested with LLVM versions from 3.6 through 10.

The MIR version is currently tied to the nightly-2020-03-22 version of the Rust compiler.