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 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 <mt@debian.org>
Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
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: