Support Primitive Proptests

[YoshikiTakashima]

Requested feature: Support primitive proptests.

Use case: Automatically converting proptests to Kani harnesses allow
us to serve large number of customers like tokio that have proptests
implemented but no Kani harnesses.

Test case:
https://github.com/YoshikiTakashima/kani/tree/yoshi-proptest-primitive/tests/proptest/primitive

Feature Branch on Fork: https://github.com/YoshikiTakashima/kani/tree/yoshi-proptest-primitive/

• Figure out how to hijack proptest import and substitute our own.
  • See 334ec6e, for the overall import hijacking technique.
  • Change to kani-driver at
    a26fbcf makes it purge the old
    import. This avoids conflicting imports issue, and allows the
    hacked version of proptest to be the only one available.
• Modify the proptest macro to build basic Kani harnessing.
• Make the corresponding API:
  • any<T> for primitive T
  • Arbitrary and Strategy
  • Ranges of primitive values. Blocked until linking with -L is fixed.

Hacks/should be fixed before merge:

• Only hard-coded path works for --extern import.
• cargo-kani is not running the recovery part of modifying
  Cargo.toml.

[YoshikiTakashima]

Replicating linker issue.

First, replicate the kani version.

git clone https://github.com/YoshikiTakashima/kani.git
cd kani
git checkout yoshi-proptest-primitive
git checkout eac76a7e -- library/proptest/src/sugar.rs
cargo clean; cargo build --workspace

Then run it on the case that replicates this.

git clone https://github.com/YoshikiTakashima/simplified-prost-rs-timestamp.git
cd simplified-prost-rs-timestamp
cargo kani

[YoshikiTakashima]

Info from deep dive: The following is required for kani to work. Currently, we only provide the rlib

• *.rlib
• symtab.json

Possible
--enable-unstable --c-lib <path to gotobinary> where gotobinary is *.goto

[YoshikiTakashima]

Code changes implemented to link proptest. After cleanup, we can merge.

[YoshikiTakashima]

See the following comment for way to integrate proptest w/o significant changes. #1435 (comment)