-
Notifications
You must be signed in to change notification settings - Fork 13.7k
std_detect: RISC-V: implement implication to "C" #145415
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
Looks like we should see the situation of #145489 (if that PR is merged, it's better to substitute |
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.
1e398ae
to
ee7627e
Compare
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. |
Replaced |
@bors r+ |
…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.
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
…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.
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
…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.
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
…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.
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
…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.
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
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.
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).
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