Skip to content

v0.4
Compare
Choose a tag to compare
@atomb atomb released this 23 Oct 16:01
v0.4
1a9a45b

  • Fixed a long-standing soundness issue (#30) in compositional verification of LLVM programs. Previously, a specification for a function that neglected to mention an effect that the function in fact caused could be successfully verified. When verifying a caller of that function, only the effects mentioned in the specification would be used. The fix for this issue may break some proof scripts: any pointer mentioned using crucible_points_to in the initial state of a specification but not in the final state will be assigned a final value of "invalid", and any subsequent reads from the pointer will fail. To fix this issue, make sure that every specification you use provides a final value for every pointer it touches (which in many cases will be the same as its initial value).

  • Added an experimental command, llvm_boilerplate, that emits skeleton function specifications for every function defined in an LLVM module. The additional crucible_llvm_array_size_profile command can be used to refine the results of llvm_boilerplate based on the array sizes used by calls that arise from a call to the named top-level function.

  • Added support for using the symbolic execution profiler available in Crucible. The enable_crucible_profiling command causes profiling information to be written to the given directory. This can then be visualized using the rendering code available here.

  • Added proof tactics to use Yices (w4_unint_yices) and CVC4 (w4_unint_cvc4) through the What4 backend instead of SBV.

  • Modified the messages emitted for failed points-to assertions to be in terms of LLVM values.

  • Added support for using the SMT array memory model to reason about the LLVM heap. The enable_smt_array_memory_model command enables it for all future proofs.

  • LLVM bitcode format support is improved. Versions 3.5 to 9.0 are known to be mostly well-supported. We consider parsing failures with any version newer than 3.5 to be a bug, so please report them on GitHub.

  • New experimental model counting commands sharpSAT and approxmc bind to the external tools of the same name. These were mistakenly listed as included in 0.3.

  • Built against Cryptol 2.8.0.

  • Improved error messages in general.

  • Fixed various additional bugs, including #211, #455, #479, #484, #493, #496, #511, #521, #522, #534, #563

Assets 8
Loading