Skip to content

std_detect: RISC-V: implement implication to "C"#145415

Merged
bors merged 1 commit intorust-lang:masterfrom
a4lg:riscv-implication-to-c
Aug 21, 2025
Merged

std_detect: RISC-V: implement implication to "C"#145415
bors merged 1 commit intorust-lang:masterfrom
a4lg:riscv-implication-to-c

Conversation

@a4lg
Copy link
Contributor

@a4lg a4lg commented Aug 15, 2025 •
edited
Loading

Just like we implemented relatively complex rules to imply other extensions from "C" (and some others), this commit implements implication to the "C" extension from others, complying the following text in the ISA Manual (although there's no direct imply/depend references).

The C extension is the superset of the following extensions:

  • Zca
  • Zcf if F is specified (RV32 only)
  • Zcd if D is specified

This is formally verified so that no other extension combinations (not in this implementation) can (currently) imply the "C" extension.

Note: this is a std_detect change and not main target feature handling.

Actual Formal Proof: riscv-c-implications.py

r? @Amanieu
@rustbot label +O-riscv

@rustbot rustbot added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. T-libs Relevant to the library team, which will review and decide on the PR/issue. O-riscv Target: RISC-V architecture labels Aug 15, 2025
@a4lg
Copy link
Contributor Author

a4lg commented Aug 17, 2025

Looks like we should see the situation of #145489 (if that PR is merged, it's better to substitute cfg_if::cfg_if! in this PR to built-in cfg_select!).

@a4lg
std_detect: RISC-V: implement implication to "C"
ee7627e 
Just like we implemented relatively complex rules to imply other extensions
**from** "C" (and some others), this commit implements implication
**to** the "C" extension from others, complying the following text
in the ISA Manual (although there's no direct imply/depend references).

> The C extension is the superset of the following extensions:
>
> - Zca
> - Zcf if F is specified (RV32 only)
> - Zcd if D is specified

This is formally verified so that no other extension combinations
(*not* in this implementation) can (currently) imply the "C" extension.
@a4lg a4lg force-pushed the riscv-implication-to-c branch from 1e398ae to ee7627e Compare August 19, 2025 01:39
@rustbot
Copy link
Collaborator

rustbot commented Aug 19, 2025

This PR was rebased onto a different master commit. Here's a range-diff highlighting what actually changed.

Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers.

@a4lg
Copy link
Contributor Author

a4lg commented Aug 19, 2025

Replaced cfg_if::cfg_if! with cfg_select! and made a minor change to the commit message.

Amanieu
Amanieu reviewed Aug 20, 2025
View reviewed changes
@Amanieu
Copy link
Member

Amanieu commented Aug 20, 2025

@bors r+

@bors
Copy link
Collaborator

bors commented Aug 20, 2025

📌 Commit ee7627e has been approved by Amanieu

It is now in the queue for this repository.

@bors bors added S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Aug 20, 2025
Zalathar added a commit to Zalathar/rust that referenced this pull request Aug 20, 2025
@Zalathar
Rollup merge of rust-lang#145415 - a4lg:riscv-implication-to-c, r=Ama…
8c15d25 
…nieu

std_detect: RISC-V: implement implication to "C"

Just like we implemented relatively complex rules to imply other extensions **from** "C" (and some others), this commit implements implication **to** the "C" extension from others, complying the following text in the ISA Manual (although there's no direct imply/depend references).

> The C extension is the superset of the following extensions:
>
> - Zca
> - Zcf if F is specified (RV32 only)
> - Zcd if D is specified

This is formally verified so that no other extension combinations (*not* in this implementation) can (currently) imply the "C" extension.

Note: this is a `std_detect` change and not main target feature handling.
@Zalathar Zalathar mentioned this pull request Aug 20, 2025
Closed
bors added a commit that referenced this pull request Aug 20, 2025
@bors
Auto merge of #145658 - Zalathar:rollup-ccqb8hk, r=Zalathar
339e4d8 
Rollup of 5 pull requests

Successful merges:

 - #144915 (Defer tail call ret ty equality to check_tail_calls)
 - #145256 (Add new `--test-codegen-backend` bootstrap option)
 - #145415 (std_detect: RISC-V: implement implication to "C")
 - #145647 (miri subtree update)
 - #145650 (Fix JS search scripts path)

r? `@ghost`
`@rustbot` modify labels: rollup
jhpratt added a commit to jhpratt/rust that referenced this pull request Aug 20, 2025
@jhpratt
Rollup merge of rust-lang#145415 - a4lg:riscv-implication-to-c, r=Ama…
6a0539a 
…nieu

std_detect: RISC-V: implement implication to "C"

Just like we implemented relatively complex rules to imply other extensions **from** "C" (and some others), this commit implements implication **to** the "C" extension from others, complying the following text in the ISA Manual (although there's no direct imply/depend references).

> The C extension is the superset of the following extensions:
>
> - Zca
> - Zcf if F is specified (RV32 only)
> - Zcd if D is specified

This is formally verified so that no other extension combinations (*not* in this implementation) can (currently) imply the "C" extension.

Note: this is a `std_detect` change and not main target feature handling.
@jhpratt jhpratt mentioned this pull request Aug 20, 2025
Closed
bors added a commit that referenced this pull request Aug 20, 2025
@bors
Auto merge of #145680 - jhpratt:rollup-cokwvpc, r=jhpratt
5bea2c6 
Rollup of 12 pull requests

Successful merges:

 - #143383 (stabilize `const_array_each_ref`)
 - #144443 (Make target pointer width in target json an integer)
 - #144758 ([Doc] Add links to the various collections)
 - #144915 (Defer tail call ret ty equality to check_tail_calls)
 - #145256 (Add new `--test-codegen-backend` bootstrap option)
 - #145415 (std_detect: RISC-V: implement implication to "C")
 - #145573 (Add an experimental unsafe(force_target_feature) attribute.)
 - #145642 (Do not use effective_visibilities query for Adt types of a local trait while proving a where-clause)
 - #145650 (Fix JS search scripts path)
 - #145654 (Download CI GCC into the correct directory)
 - #145662 (Enforce correct number of arguments for `"x86-interrupt"` functions)
 - #145674 (Enable triagebot `[review-changes-since]` feature)

Failed merges:

 - #145647 (miri subtree update)

r? `@ghost`
`@rustbot` modify labels: rollup
jhpratt added a commit to jhpratt/rust that referenced this pull request Aug 20, 2025
@jhpratt
Rollup merge of rust-lang#145415 - a4lg:riscv-implication-to-c, r=Ama…
a3c768d 
…nieu

std_detect: RISC-V: implement implication to "C"

Just like we implemented relatively complex rules to imply other extensions **from** "C" (and some others), this commit implements implication **to** the "C" extension from others, complying the following text in the ISA Manual (although there's no direct imply/depend references).

> The C extension is the superset of the following extensions:
>
> - Zca
> - Zcf if F is specified (RV32 only)
> - Zcd if D is specified

This is formally verified so that no other extension combinations (*not* in this implementation) can (currently) imply the "C" extension.

Note: this is a `std_detect` change and not main target feature handling.
@jhpratt jhpratt mentioned this pull request Aug 20, 2025
Closed
bors added a commit that referenced this pull request Aug 20, 2025
@bors
Auto merge of #145681 - jhpratt:rollup-7hn0ii7, r=jhpratt
5a72bc9 
Rollup of 14 pull requests

Successful merges:

 - #143383 (stabilize `const_array_each_ref`)
 - #144443 (Make target pointer width in target json an integer)
 - #144758 ([Doc] Add links to the various collections)
 - #144915 (Defer tail call ret ty equality to check_tail_calls)
 - #145137 (Consolidate panicking functions in `slice/index.rs`)
 - #145256 (Add new `--test-codegen-backend` bootstrap option)
 - #145297 (fix(debuginfo): handle false positives in overflow check)
 - #145415 (std_detect: RISC-V: implement implication to "C")
 - #145642 (Do not use effective_visibilities query for Adt types of a local trait while proving a where-clause)
 - #145650 (Fix JS search scripts path)
 - #145654 (Download CI GCC into the correct directory)
 - #145662 (Enforce correct number of arguments for `"x86-interrupt"` functions)
 - #145674 (Enable triagebot `[review-changes-since]` feature)
 - #145678 (Fix typo in docstring)

r? `@ghost`
`@rustbot` modify labels: rollup
jhpratt added a commit to jhpratt/rust that referenced this pull request Aug 21, 2025
@jhpratt
Rollup merge of rust-lang#145415 - a4lg:riscv-implication-to-c, r=Ama…
7eb8cd3 
…nieu

std_detect: RISC-V: implement implication to "C"

Just like we implemented relatively complex rules to imply other extensions **from** "C" (and some others), this commit implements implication **to** the "C" extension from others, complying the following text in the ISA Manual (although there's no direct imply/depend references).

> The C extension is the superset of the following extensions:
>
> - Zca
> - Zcf if F is specified (RV32 only)
> - Zcd if D is specified

This is formally verified so that no other extension combinations (*not* in this implementation) can (currently) imply the "C" extension.

Note: this is a `std_detect` change and not main target feature handling.
@jhpratt jhpratt mentioned this pull request Aug 21, 2025
Closed
bors added a commit that referenced this pull request Aug 21, 2025
@bors
Auto merge of #145691 - jhpratt:rollup-fekj1bx, r=jhpratt
b499c5c 
Rollup of 15 pull requests

Successful merges:

 - #143383 (stabilize `const_array_each_ref`)
 - #144758 ([Doc] Add links to the various collections)
 - #144915 (Defer tail call ret ty equality to check_tail_calls)
 - #145137 (Consolidate panicking functions in `slice/index.rs`)
 - #145256 (Add new `--test-codegen-backend` bootstrap option)
 - #145297 (fix(debuginfo): handle false positives in overflow check)
 - #145415 (std_detect: RISC-V: implement implication to "C")
 - #145590 (Prevent impossible combinations in `ast::ModKind`.)
 - #145621 (Fix some doc typos)
 - #145642 (Do not use effective_visibilities query for Adt types of a local trait while proving a where-clause)
 - #145650 (Fix JS search scripts path)
 - #145654 (Download CI GCC into the correct directory)
 - #145662 (Enforce correct number of arguments for `"x86-interrupt"` functions)
 - #145674 (Enable triagebot `[review-changes-since]` feature)
 - #145678 (Fix typo in docstring)

r? `@ghost`
`@rustbot` modify labels: rollup
jhpratt added a commit to jhpratt/rust that referenced this pull request Aug 21, 2025
@jhpratt
Rollup merge of rust-lang#145415 - a4lg:riscv-implication-to-c, r=Ama…
218dd94 
…nieu

std_detect: RISC-V: implement implication to "C"

Just like we implemented relatively complex rules to imply other extensions **from** "C" (and some others), this commit implements implication **to** the "C" extension from others, complying the following text in the ISA Manual (although there's no direct imply/depend references).

> The C extension is the superset of the following extensions:
>
> - Zca
> - Zcf if F is specified (RV32 only)
> - Zcd if D is specified

This is formally verified so that no other extension combinations (*not* in this implementation) can (currently) imply the "C" extension.

Note: this is a `std_detect` change and not main target feature handling.
This was referenced Aug 21, 2025
Closed
Merged
bors added a commit that referenced this pull request Aug 21, 2025
@bors
Auto merge of #145701 - jhpratt:rollup-a0kg33p, r=jhpratt
57e620e 
Rollup of 19 pull requests

Successful merges:

 - #143383 (stabilize `const_array_each_ref`)
 - #144758 ([Doc] Add links to the various collections)
 - #144915 (Defer tail call ret ty equality to check_tail_calls)
 - #145256 (Add new `--test-codegen-backend` bootstrap option)
 - #145297 (fix(debuginfo): handle false positives in overflow check)
 - #145390 (Shorten some dependency chains in the compiler)
 - #145415 (std_detect: RISC-V: implement implication to "C")
 - #145525 (stdlib: Replace typedef -> type alias in doc comment)
 - #145590 (Prevent impossible combinations in `ast::ModKind`.)
 - #145593 (UnsafePinned::raw_get: sync signature with get)
 - #145621 (Fix some doc typos)
 - #145627 (Unconditionally-const supertraits are considered not dyn compatible)
 - #145642 (Do not use effective_visibilities query for Adt types of a local trait while proving a where-clause)
 - #145650 (Fix JS search scripts path)
 - #145654 (Download CI GCC into the correct directory)
 - #145662 (Enforce correct number of arguments for `"x86-interrupt"` functions)
 - #145673 (Add flock support for cygwin)
 - #145674 (Enable triagebot `[review-changes-since]` feature)
 - #145678 (Fix typo in docstring)

r? `@ghost`
`@rustbot` modify labels: rollup
@bors bors merged commit 03aa3b8 into rust-lang:master Aug 21, 2025
10 checks passed
@rustbot rustbot added this to the 1.91.0 milestone Aug 21, 2025
rust-timer added a commit that referenced this pull request Aug 21, 2025
@rust-timer
Unrolled build for #145415
54e8fe5 
Rollup merge of #145415 - a4lg:riscv-implication-to-c, r=Amanieu

std_detect: RISC-V: implement implication to "C"

Just like we implemented relatively complex rules to imply other extensions **from** "C" (and some others), this commit implements implication **to** the "C" extension from others, complying the following text in the ISA Manual (although there's no direct imply/depend references).

> The C extension is the superset of the following extensions:
>
> - Zca
> - Zcf if F is specified (RV32 only)
> - Zcd if D is specified

This is formally verified so that no other extension combinations (*not* in this implementation) can (currently) imply the "C" extension.

Note: this is a `std_detect` change and not main target feature handling.
github-actions bot pushed a commit to model-checking/verify-rust-std that referenced this pull request Aug 26, 2025
@jhpratt
Rollup merge of rust-lang#145415 - a4lg:riscv-implication-to-c, r=Ama…
755ebb7 
…nieu

std_detect: RISC-V: implement implication to "C"

Just like we implemented relatively complex rules to imply other extensions **from** "C" (and some others), this commit implements implication **to** the "C" extension from others, complying the following text in the ISA Manual (although there's no direct imply/depend references).

> The C extension is the superset of the following extensions:
>
> - Zca
> - Zcf if F is specified (RV32 only)
> - Zcd if D is specified

This is formally verified so that no other extension combinations (*not* in this implementation) can (currently) imply the "C" extension.

Note: this is a `std_detect` change and not main target feature handling.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Amanieu Amanieu Amanieu left review comments

Assignees

@Amanieu Amanieu

Labels

O-riscv Target: RISC-V architecture S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. T-libs Relevant to the library team, which will review and decide on the PR/issue.

Projects

None yet

Milestone

1.91.0

Development

Successfully merging this pull request may close these issues.

4 participants

@a4lg @rustbot @Amanieu @bors