v0.5

New Features

• Added experimental support for basic, non-compositional verification
  of x86 machine code for use in conjunction with LLVM verification.

    crucible_llvm_verify_x86 :
      LLVMModule -> String -> String ->
      [(String, Int)] -> Bool -> CrucibleSetup () ->
      TopLevel CrucibleMethodSpec
  

  The first argument specifies the LLVM module containing the caller.
  The second and third specify the ELF file name and symbol name of the
  function to be verifier. The fourth specifies the names and sizes (in
  bytes) of global variables to initialize, and the fifth whether to
  perform path satisfiability checking. The last argument is the LLVM
  specification of the calling context against which to verify the
  function.

• Added support for using the SMT theory of arrays in the LLVM memory
  model. In some cases, this can significantly improve performance.

    enable_smt_array_memory_model : TopLevel ()
    disable_smt_array_memory_model : TopLevel ()
  

• Added support for specifying alignment in LLVM allocations. The
  crucible_alloc_aligned and crucible_alloc_readonly_aligned
  functions allocate read-write and read-only memory regions,
  respectively, with the specified alignment (in bytes).

• Added a conditional points-to function,
  crucible_conditional_points_to, that allows an LLVM function to
  conditionally modify memory, leaving it in its previous state
  (potentially uninitialized) when the condition is false.

• Added several new options:

  • New functions enable_what4_hash_consing and
    disable_what4_hash_consing to enable or disable hash consing to
    increase sub-formula sharing during symbolic execution.

  • New functions enable_crucible_assert_then_assume and
    disable_crucible_assert_then_assume to control whether
    predicates are assumed after asserting them during symbolic
    execution. The default is now to not assume them, whereas
    previously they were assumed.

  • New command-line option --no-color to print an ASCII logo
    without ANSI color or Unicode.

Performance Improvements

• Improved performance of the LLVM memory model.

• Improved performance of bitvector operations during symbolic execution.

• Improved performance of rewriting SAWCore terms.

Bug Fixes

• Fixed SBV interface to fail more gracefully when it cannot find the
  solver executable.

• Fixed SMT-Lib export negation issues.

Fixes issues #286, #489, #491, #564, #580, #583, #585, #586, #587, #590,
#592, #594, #597, #598, #602, #603, #612, #613, #622, #626, #633, #638,
#639, and #647.