Add support for LLVM-based verification tools

[alastairreid]

List of LLVM-based verifiers that we know of (edit this issue to add new ones)

• KLEE
• KLEE-Native
• SeaHorn
• SMACK
• Crux-LLVM

Some typical steps involved (edit this issue if new ones are found)

• Figure out how to invoke verifier directly on bitcode file (e.g., see docs/using-klee.md)
• Handle unimplemented LLVM intrinsics
  • Try to compile/optimize so that intrinsic disappears (-optlevel 1, dead code elimination, restrict CPU version, etc.)
  • For symbolic execution, ensure that symbolic execution fails only if the current path executes an unimplemented intrinsic (e.g., see More robust handling of unknown intrinsics klee/klee#1295)
  • Implement missing intrinsics by converting them to simpler intrinsics
  • Implement missing intrinsics by converting them to SMT (e.g., see Implement fshr/fshl intrinsics klee/klee#1278)
• Make sure that weak symbols are supported (e.g., see Handle global variables klee/klee#1271 ?) (This affects 'atexit' support)
• Handle libc/etc dependencies in libcore/libstd including
  • memory allocator
  • syscalls
  • pthread functions
• Create FFI binding for verification annotation API
• Add support to scripts/cargo-verify
  • New/different flags for compiling Rust code
  • Invoke verifier
    • Filter stdout/stderr to discover verification result
    • Filter stdout/stderr to decide what tool output to produce at each verbosity level
  • If counterexamples are generated by tool, add "replay" support to display cex using Rust print functions