Support for Primitive Proptests #1435

YoshikiTakashima · 2022-08-02T04:25:20Z

Description of changes:

Adds support for running proptests with primitive inputs using kani.

Resolved issues:

Resolves #1363

Call-outs:

Feature only runs with cargo kani.
Since we are only merging a small portion of proptest, we cannot support proptests like tests/cargo-kani/rectangle-example. This means we disable the proptest import in that test case.

Testing:

How is this change tested? tests/cargo-kani/proptest
Is this a refactor change? No.

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

…test-primitive

TOOD: API implementation, BODY1

…test-primitive

danielsn

Can you add some documentation on what you're doing in the proptest override? Maybe a README.md?

.cargo/config.toml

docs/src/tutorial/first-steps-v1/Cargo.toml

docs/src/tutorial/first-steps-v2/Cargo.toml

kani-compiler/build.rs

docs/src/tutorial/kinds-of-failure/Cargo.toml

scripts/cargo-kani

scripts/refresh-kani-proptest.sh

tests/cargo-kani/rectangle-example/Cargo.toml

scripts/kani-regression.sh

danielsn · 2022-08-08T17:53:42Z

We now have a fork of propest. What's the best way to maintain this.

…test-primitive

celinval

I don't think we should add the proptest code in our repository. We should probably do one of the following:

Refactor the changes so we can extend proptest instead of forking from it.
If we do need to fork proptest, we should create a separate repository with the fork. We should then add a submodule here to this fork.

Feel free to ping me offline if you want to discuss this further or if you have any suggestions.

library/kani/src/invariant.rs

celinval · 2022-08-09T16:34:45Z

kani-compiler/build.rs

    setup_lib(&out_dir, &lib_out, "kani");
    setup_lib(&out_dir, &lib_out, "kani_macros");
    setup_lib(&out_dir, &lib_out, "std");
    println!("cargo:rustc-env=KANI_LIB_PATH={}", lib_out);
+    println!("cargo:rustc-env=TARGET={}", target);
+    println!(
+        "cargo:rustc-env=KANI_EXTERN_OUT_DIR={}",


Is there a reason why you are not using out_dir?

cargo kani compiles to the directory with target/$ARCH/debug/deps automatically.

I've found the incremental build to be a bit more finichy when using target/debug/deps perhaps because cargo build --workspace will also compile to the same directory. I can give it a try if needed.

I see. Yeah, that is a problem that we have with our libraries today. We are compiling them twice.

Is that one of the issues addressed in your linker update? If so, I can hold off on this one until that is in, and both std/proptest can take advantage.

celinval · 2022-08-09T16:48:31Z

kani-driver/src/call_cargo.rs

@@ -80,10 +82,18 @@ impl KaniSession {
            });
        }

+        let mut symtabs = glob(&outdir.join("*.symtab.json"))?;
+        let mut metadata = glob(&outdir.join("*.kani-metadata.json"))?;
+        if std::env::var("IS_KANI_PROPTEST").is_ok() {


I posted a comment in the issue you created. Can you please check?

celinval · 2022-08-09T16:50:10Z

kani-driver/src/call_cargo.rs

@@ -80,10 +82,18 @@ impl KaniSession {
            });
        }

+        let mut symtabs = glob(&outdir.join("*.symtab.json"))?;
+        let mut metadata = glob(&outdir.join("*.kani-metadata.json"))?;
+        if std::env::var("IS_KANI_PROPTEST").is_ok() {


Are we planning to enable this as a compilation flag or a runtime option?

As of now, scripts/cargo-kani detects proptests automatically. I would be OK making it an argument, perhaps via -Z

Yeah, it's probably better if the user has to opt-in at this point.

celinval

A few more comments. :)

celinval · 2022-08-09T20:55:06Z

scripts/cargo-kani

@@ -19,4 +19,26 @@ then
 fi
 KANI_PATH=${KANI_CANDIDATES[0]}

+# if the crate uses proptest, get ready to run that. Make sure local
+# proptest import and kani's proptest does not clash.
+function has-direct-proptest-import() {


We shouldn't add any logic to these scripts. They are meant to be a proxy that enables development and it will actually not run with our pre-build code.

Is there a reason why this is not inside kani-driver? We are already invoking cargo metadata there which already has this information.

Is there a reason why this is not inside kani-driver? We are already invoking cargo metadata there which already has this information.

If it already has Cargo.toml info, I'll move to that

celinval · 2022-08-09T21:01:37Z

tests/cargo-kani/rectangle-example/Cargo.toml

+# not support any integers, which crashes this test case. See
+# https://github.com/model-checking/kani/issues/1473 for details.
+# [dev-dependencies]
+# proptest = "1.0.0"


I prefer if you add a runtime option for users to enable proptest analysis.

I'll resolve this along with the comment with IS_KANI_PROPTEST

YoshikiTakashima · 2022-08-11T17:56:36Z

Until the ticket for approving the separate repository goes through, code review for proptests will be managed through the features/proptest branch. The proptest fork will be imported through submodules.

YoshikiTakashima · 2022-08-15T14:58:05Z

Closing in favor of the following approaches.

The following proptest injection scheme works fine once proptest's kanilib dependency is under [target.'cfg(not(kani))'.dependencies] to avoid clash.

proptest = { path = "$PATH_TO/STUBBED/proptest"}

Long-term, we probably can support injection done by appending the following to Cargo.toml. We cannot immidately use this b/c the patch feature requires that the offered features of the overriding library match up with the original library. While the override is cleaner, there is no good way to condition this on being specific to cfg(kani).

[patch.crates-io]
proptest = { path = "$PATH_TO/STUBBED/proptest"}

Yoshi Takashima added 30 commits July 1, 2022 15:30

Added proptest test cases.

21014e2

Merge branch 'main' of github.com:model-checking/kani into yoshi-prop…

6f28fb8

…test-primitive

Added prototype translator.

e797964

Added missing recurisve case. Separated to helper.

988892c

Removed panic put in for debugging.

7b4568a

Changed name of translator

a0669f5

Refactored test case for proptest integration.

005bb7c

Fixed typo in variable name.

6b0c65e

Added multi-argument and combo tests for proptest.

7d43e49

purged redundant spaces.

690d1fa

Merge branch 'main' of github.com:model-checking/kani into yoshi-prop…

a0e92f4

…test-primitive

Rustfmt on library/kani_macros/src/lib.rs

7f9836d

Initial prototype to hijack proptest.

334ec6e

Added todo not for hard-coded path.

5697a90

Partially working cargo kani hack. Recovery is not running though.

a26fbcf

Merge branch 'main' of github.com:model-checking/kani into yoshi-prop…

e3adb09

…test-primitive

fixed empty var check

ef368d0

Merge branch 'main' of github.com:model-checking/kani into yoshi-prop…

b78bda8

…test-primitive

Merge branch 'main' of github.com:model-checking/kani into yoshi-prop…

7291ac6

…test-primitive

Added expanded macro printing to kani-compiler. Remove later.

8c604f0

Added flags to mark rules in expanded form.

b34431d

Merge branch 'main' of github.com:model-checking/kani into yoshi-prop…

471f246

…test-primitive

Make the var names unique to detect rule firing.

75a8621

Prototyped new BODY2 rule. Need to push the API side for testing.

c71f185

TOOD: API implementation, BODY1

Moved macros out to proper sugar.rs file.

52733ec

Supported Minimum Strategy.

e3e4226

Got new proptest to type check. TODO: cleanup

0386207

Merge branch 'main' of github.com:model-checking/kani into yoshi-prop…

f4af6eb

…test-primitive

Removed expansion. Somehow fixes the "finding proof" issue.

490f87b

Fixed missing tuple implementation.

efe3cb4

Yoshi Takashima and others added 4 commits August 3, 2022 23:15

Fixed license.

f744b7c

Fixed license for new test case.

933751a

More temporary disabling of proptest

3262c1e

Merge branch 'main' of github.com:model-checking/kani into yoshi-prop…

f3e6e55

…test-primitive

YoshikiTakashima mentioned this pull request Aug 5, 2022

[Blocked on #1435] Support proptest arbitrary generation for bool and tuple #1467

Closed

4 tasks

Yoshi Takashima added 2 commits August 5, 2022 18:56

Merge branch 'main' of github.com:model-checking/kani into yoshi-prop…

2258b94

…test-primitive

Merge branch 'main' into yoshi-proptest-primitive

0102218

danielsn reviewed Aug 8, 2022

View reviewed changes

Merge branch 'main' of github.com:model-checking/kani into yoshi-prop…

7b1fc35

…test-primitive

YoshikiTakashima mentioned this pull request Aug 8, 2022

Tracking Issue: Incremental PR for Primitive Types in Proptests #1473

Closed

7 tasks

Yoshi Takashima added 12 commits August 8, 2022 16:32

Changed comment to point to kani tracking issue.

9ebad12

Moved to using paths rather than string concat.

b835517

Made search for symtab more specific.

dbcbd2a

Set -eu like other scripts.

3b0f475

Moved to using tomlq wrapper around jq. Both installed.

bcebad6

Fixed typo.

4e4b0e5

Added docs.

1a549a4

Fixed dependency install after ci broke.

ab9922d

Merge branch 'main' of github.com:model-checking/kani into yoshi-prop…

7239441

…test-primitive

Fixed cargo kani misclassifying proptest cases.

fa80a27

Purged unneeded refresh.

44a4074

Fixed clippy warning regarding derived traits.

526538c

celinval requested changes Aug 9, 2022

View reviewed changes

celinval reviewed Aug 9, 2022

View reviewed changes

YoshikiTakashima closed this Aug 15, 2022

This was referenced Aug 16, 2022

Extra Symtabs leads to conflicting proof harnesses #1478

Closed

Support Primitive Proptests #1363

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support for Primitive Proptests #1435

Support for Primitive Proptests #1435

YoshikiTakashima commented Aug 2, 2022 •

edited

Loading

danielsn left a comment

danielsn commented Aug 8, 2022

celinval left a comment

celinval Aug 9, 2022

YoshikiTakashima Aug 9, 2022 •

edited

Loading

celinval Aug 9, 2022

YoshikiTakashima Aug 10, 2022

celinval Aug 9, 2022

celinval Aug 9, 2022

YoshikiTakashima Aug 9, 2022

celinval Aug 9, 2022

celinval left a comment

celinval Aug 9, 2022

YoshikiTakashima Aug 9, 2022

celinval Aug 9, 2022

YoshikiTakashima Aug 9, 2022

YoshikiTakashima commented Aug 11, 2022

YoshikiTakashima commented Aug 15, 2022 •

edited

Loading

Support for Primitive Proptests #1435

Support for Primitive Proptests #1435

Conversation

YoshikiTakashima commented Aug 2, 2022 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

danielsn left a comment

Choose a reason for hiding this comment

danielsn commented Aug 8, 2022

celinval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

YoshikiTakashima Aug 9, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

YoshikiTakashima commented Aug 11, 2022

YoshikiTakashima commented Aug 15, 2022 • edited Loading

YoshikiTakashima commented Aug 2, 2022 •

edited

Loading

YoshikiTakashima Aug 9, 2022 •

edited

Loading

YoshikiTakashima commented Aug 15, 2022 •

edited

Loading