Add contract support to intrinsics #3345
Labels
[C] Feature / Enhancement
A new feature request or enhancement to an existing feature.
Z-Contracts
Issue related to code contracts
Milestone
Comments
celinval
added
the
[C] Feature / Enhancement
celinval
added a commit
to model-checking/verify-rust-std
that referenced
this issue
Dec 7, 2024
Here are a few limitations:
1. Harness for`write_bytes` was disabled due to:
- Issue model-checking/kani#90.
2. The harnesses explicitly disable cases where a pointer is dangling.
- Kani cannot make assumptions on pointer allocation for dead or
dangling pointers (model-checking/kani#2300).
3. Actual intrinsics are very hard to verify with Kani. The cases we can
verify are those that have wrappers around the actual intrinsic.
- Issue model-checking/kani#3345
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---------
Co-authored-by: Michael Tautschnig <[email protected]>
Co-authored-by: Michael Tautschnig <[email protected]>
github-merge-queue bot
pushed a commit
to model-checking/verify-rust-std
that referenced
this issue
Feb 4, 2025
This is a draft pull request towards solving #19. ## Changes - Added wrappers for `transmute_unchecked()` - Annotated these wrappers with contracts - Wrote harnesses that verify these wrappers Note: the reason we write wrappers for `transmute_unchecked()` and we annotate those wrappers is that function contracts do not appear to be currently supported for compiler intrinsics (as discussed in [rust-lang#3345](model-checking/kani#3345)). Also, rather than using a single wrapper for `transmute_unchecked()`, we write several with different constraints on the input (since leaving the function parameters completely generic severely restricts what we can do in the contracts, e.g., testing for equality). This is not intended to be a complete solution for verifying `transmute_unchecked()`, but instead a proof of concept to see how aligned this is with the expected solution. Any feedback would be greatly appreciated -- thank you! By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: AlexLB99 <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Requested feature: Enable users to verify and stub compiler intrinsics with Kani contract
Use case: Intrinsics are functions implemented in the compiler. Today there are three possible intrinsics definitions:
extern "rust-intrinsics"without any body.#[rustc_intrinsic]and annotated with#[rustc_intrinsic_must_be_overridden]. These functions have a dummy body that is ignored by the compiler. For StableMIR, 1 and 2 are handled the same way, i.e., they are intrinsics without a body.#[rustc_intrinsic]and not annotated with#[rustc_intrinsic_must_be_overridden]. These functions are marked as intrinsics, but they provide a fallback body.Kani contract support for those are very limited. Users cannot annotate intrinsics from category 1 with Kani contract due to #3325. Users can add contracts to the other categories, but their contracts are ignored.
The text was updated successfully, but these errors were encountered: