Proper handling of intrinsics with #[rustc_intrinsic_must_be_overridden]
#79
Comments
celinval
added a commit
to celinval/kani-dev
that referenced
this issue
Jun 12, 2024
- Enable Kani to use fallback fn body for intrinsics, so they can
be verified.
- Until <rust-lang/project-stable-mir#79>
is implemented, we have to check has_body and must_be_overridden
- Export all kani_macro definitions. Rename `unstable` to avoid
conflict with the Rust standard library one.
- Dump stable mir body since transformations are made at that level.
- I just did this as I was debugging things.
tautschnig
added a commit
to model-checking/kani
that referenced
this issue
Jun 12, 2024
- Enable Kani to use fallback fn body for intrinsics, so they can be verified. - Until <rust-lang/project-stable-mir#79> is implemented, we have to check has_body and must_be_overridden - Export all kani_macro definitions. Rename `unstable` to avoid conflict with the Rust standard library one. - Dump stable mir body since transformations are made at that level. - I just did this as I was debugging things. Co-authored-by: Michael Tautschnig <[email protected]>
matthiaskrgr
added a commit
to matthiaskrgr/rust
that referenced
this issue
Jun 15, 2024
…li-obk Unify intrinsics body handling in StableMIR rust-lang#120675 introduced a new mechanism to declare intrinsics which will potentially replace the rust-intrinsic ABI. The new mechanism introduces a placeholder body and mark the intrinsic with `#[rustc_intrinsic_must_be_overridden]`. In practice, this means that a backend should not generate code for the placeholder, and shim the intrinsic. The new annotation is an internal compiler implementation, and it doesn't need to be exposed to StableMIR users. In this PR, we unify the interface for intrinsics marked with `rustc_intrinsic_must_be_overridden` and intrinsics that do not have a body. Fixes rust-lang/project-stable-mir#79 r? `@oli-obk` cc: `@momvart`
matthiaskrgr
added a commit
to matthiaskrgr/rust
that referenced
this issue
Jun 15, 2024
…li-obk Unify intrinsics body handling in StableMIR rust-lang#120675 introduced a new mechanism to declare intrinsics which will potentially replace the rust-intrinsic ABI. The new mechanism introduces a placeholder body and mark the intrinsic with `#[rustc_intrinsic_must_be_overridden]`. In practice, this means that a backend should not generate code for the placeholder, and shim the intrinsic. The new annotation is an internal compiler implementation, and it doesn't need to be exposed to StableMIR users. In this PR, we unify the interface for intrinsics marked with `rustc_intrinsic_must_be_overridden` and intrinsics that do not have a body. Fixes rust-lang/project-stable-mir#79 r? ``@oli-obk`` cc: ``@momvart``
rust-timer
added a commit
to rust-lang-ci/rust
that referenced
this issue
Jun 15, 2024
Rollup merge of rust-lang#126361 - celinval:issue-0079-intrinsic, r=oli-obk Unify intrinsics body handling in StableMIR rust-lang#120675 introduced a new mechanism to declare intrinsics which will potentially replace the rust-intrinsic ABI. The new mechanism introduces a placeholder body and mark the intrinsic with `#[rustc_intrinsic_must_be_overridden]`. In practice, this means that a backend should not generate code for the placeholder, and shim the intrinsic. The new annotation is an internal compiler implementation, and it doesn't need to be exposed to StableMIR users. In this PR, we unify the interface for intrinsics marked with `rustc_intrinsic_must_be_overridden` and intrinsics that do not have a body. Fixes rust-lang/project-stable-mir#79 r? ``@oli-obk`` cc: ``@momvart``
github-actions bot
pushed a commit
to rust-lang/miri
that referenced
this issue
Jun 17, 2024
Unify intrinsics body handling in StableMIR rust-lang/rust#120675 introduced a new mechanism to declare intrinsics which will potentially replace the rust-intrinsic ABI. The new mechanism introduces a placeholder body and mark the intrinsic with `#[rustc_intrinsic_must_be_overridden]`. In practice, this means that a backend should not generate code for the placeholder, and shim the intrinsic. The new annotation is an internal compiler implementation, and it doesn't need to be exposed to StableMIR users. In this PR, we unify the interface for intrinsics marked with `rustc_intrinsic_must_be_overridden` and intrinsics that do not have a body. Fixes rust-lang/project-stable-mir#79 r? ``@oli-obk`` cc: ``@momvart``
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
rust-lang/rust#120675 introduced a new mechanism to declare intrinsics which will potentially replace the
rust-intrinsicABI. The new mechanism introduces a dummy body and mark the intrinsic with#[rustc_intrinsic_must_be_overridden].I believe we can maintain the same interface we have so far, and we can change the
has_bodycheck for instances. For the case of an intrinsic, we return that a body is not available ifrustc_intrinsic_must_be_overriddenannotation is present.@oli-obk, would that make sense?
The text was updated successfully, but these errors were encountered: