Changelog for crux-llvm-0.8
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
returnsn
abducts for each goal that the SMT solver found to besat
. An abduct is a formula that makes the goalunsat
(would help the SMT solver prove the goal). This feature only works with thecvc5
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, socrux-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 anindeterminateLoadBehavior
flag to control theMemOptions
option of the same name. Refer to thecrucible-llvm
changelog for more details.- A
?memOpts :: MemOptions
constraint has been added toCrux.LLVM.Simulate.checkFun
.