Support Primitive Proptests

[YoshikiTakashima]

trafficstars

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/

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

Hacks/should be fixed before merge:

• [x] 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. https://github.com/model-checking/kani/pull/1435#issuecomment-1215117585