Changelog for crux-llvm-0.10

0.10 -- 2025-03-24

Sync the version number with crux-mir-0.10 as part of the overall Crux 0.10 release.

Add support for the Bitwuzla SMT solver in the test suite.
Add --debug option for starting the Crucible debugger.
Emit a warning when parsing an LLVM bitcode metadata record that crux-llvm does not support. (Previously, crux-llvm would throw a fatal error if this occurred, so this change makes crux-llvm more permissive with respect to unsupported LLVM versions.)

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.

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.

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.

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.