Rewrite loops with multiple back edges to having a single back edge only#900
Closed
tautschnig wants to merge 10000 commits intomodel-checking:mainfrom
Closed
Rewrite loops with multiple back edges to having a single back edge only#900tautschnig wants to merge 10000 commits intomodel-checking:mainfrom
tautschnig wants to merge 10000 commits intomodel-checking:mainfrom
Conversation
Fix unclosed boxes in pretty printing of TraitAlias
This was causing trait aliases to not even render at all in stringified / pretty printed output.
```rust
macro_rules! repro {
($item:item) => {
stringify!($item)
};
}
fn main() {
println!("{:?}", repro!(pub trait Trait<T> = Sized where T: 'a;));
}
```
Before: `""`
After: `"pub trait Trait<T> = Sized where T: 'a;"`
The fix is copied from how `head`/`end` for `ItemKind::Use`, `ItemKind::ExternCrate`, and `ItemKind::Mod` are all done in the pretty printer:
https://github.com/rust-lang/rust/blob/dd3ac41495e85a9b7b5cb3186379d02ce17e51fe/compiler/rustc_ast_pretty/src/pprust/state.rs#L1178-L1184
ARMv6K Horizon - Enable default libraries Due to the nature of the external gcc linker, default libraries are required, even for `no_std` programs.
…asper Add diagnostic items for macros For use in Clippy, it adds diagnostic items to all the stable public macros Clippy has lints that look for almost all of these (currently by name or path), but there are a few that aren't currently part of any lint, I could remove those if it's preferred to add them as needed rather than ahead of time
rustdoc: Yet more intra-doc links cleanup r? `@Manishearth`
feat: rustc_pass_by_value lint attribute Useful for thin wrapper attributes that are best passed as value instead of reference. Fixes #76935
Clarify explicitly that BTree{Map,Set} are ordered.
One of the main reasons one would want to use a BTree{Map,Set} rather than a Hash{Map,Set} is because they maintain their keys in sorted order; but this was never explicitly stated in the top-level docs (it was only indirectly alluded to there, and stated explicitly in the docs for `iter`, `values`, etc.)
This PR states the ordering guarantee more prominently.
Include Projections when elaborating TypeOutlives Fixes #92280 In `Elaborator`, we elaborate that `Foo<<Bar as Baz>::Assoc>: 'a` -> `<Bar as Baz>::Assoc: 'a`. This is the same rule that would be applied to any other `Param`. If there are escaping vars, we continue to do nothing. r? `@nikomatsakis`
Parse `Ty?` as `Option<Ty>` and provide structured suggestion Swift has specific syntax that desugars to `Option<T>` similar to our `?` operator, which means that people might try to use it in Rust. Parse it and gracefully recover.
…elid rustdoc: fix intra-link for generic trait impls fixes #92662 r? `````@camelid`````
remove unused FIXME #56935 seems to be fixed.
Rollup of 10 pull requests
Successful merges:
- #92487 (Fix unclosed boxes in pretty printing of TraitAlias)
- #92581 (ARMv6K Horizon - Enable default libraries)
- #92619 (Add diagnostic items for macros)
- #92635 (rustdoc: Yet more intra-doc links cleanup)
- #92646 (feat: rustc_pass_by_value lint attribute)
- #92706 (Clarify explicitly that BTree{Map,Set} are ordered.)
- #92710 (Include Projections when elaborating TypeOutlives)
- #92746 (Parse `Ty?` as `Option<Ty>` and provide structured suggestion)
- #92792 (rustdoc: fix intra-link for generic trait impls)
- #92814 (remove unused FIXME)
Failed merges:
r? `@ghost`
`@rustbot` modify labels: rollup
New lint: `iter_overeager_cloned` Closes #8202 changelog: New lint: [`iter_overeager_cloned`]
Update RLS and drop rustc-ap-packages Closes #91543 r? `@pietroalbini` cc `@calebcartwright` `@flip1995`
expand: Pick `cfg`s and `cfg_attrs` one by one, like other attributes This is a rebase of rust-lang/rust#83354, but without any language-changing parts ~(except for rust-lang/rust#84110, i.e. the attribute expansion order is the same. This is a pre-requisite for any other changes making cfg attributes closer to regular macro attributes - Possibly changing their expansion order (rust-lang/rust#83331) - Keeping macro backtraces for cfg attributes, or otherwise making them visible after expansion without keeping them in place literally (rust-lang/rust#84110). Two exceptions to the "one by one" behavior are: - cfgs eagerly expanded by `derive` and `cfg_eval`, they are still expanded in a batch, that's by design. - cfgs at the crate root, they are currently expanded not during the main expansion pass, but before that, during `#![feature]` collection. I'll try to disentangle that logic later in a separate PR. r? `@Aaron1011`
Link sidebar "location" heading to top of page This makes it easy, when you are scrolled far down in a page, to jump back to the top. Demo: https://rustdoc.crud.net/jsha/link-to-top/std/string/struct.String.html r? ``@GuillaumeGomez``
Remove some unnecessary uses of `FieldDef::ident` Followup from #92533. cc ``@Aaron1011`` ``@petrochenkov``
…in-variant, r=davidtwco Fix `try wrapping expression in variant` suggestion with struct field shorthand Fixes a broken suggestion: [playground](https://play.rust-lang.org/?version=nightly&mode=debug&edition=2021&gist=83fe2dbfe1485f8cfca1aef2a6582e77) before: ``` error[E0308]: mismatched types --> src/main.rs:7:19 | 7 | let x = Foo { bar }; | ^^^ expected enum `Option`, found integer | = note: expected enum `Option<i32>` found type `{integer}` help: try wrapping the expression in `Some` | 7 | let x = Foo { Some(bar) }; | +++++ + ``` after: ``` error[E0308]: mismatched types --> src/main.rs:7:19 | 7 | let x = Foo { bar }; | ^^^ expected enum `Option`, found integer | = note: expected enum `Option<i32>` found type `{integer}` help: try wrapping the expression in `Some` | 7 | let x = Foo { bar: Some(bar) }; | ~~~~~~~~~~~~~~ ``` r? ``@m-ou-se`` since you touched the code last in #91080
rustdoc: remove hand-rolled isatty This PR replaces bindings to the platform-specific isatty APIs with the `isatty` crate, as done elsewhere in the repository.
…stion, r=nagisa Fix suggesting turbofish with lifetime arguments Now we suggest turbofish correctly given exprs like `foo<'_>`. Also fix suggestion when we have `let x = foo<bar, baz>;` which was broken.
…ing#985) * Documentation: Updates for "Failures that Kani can spot" * Remove "future work" * Address comments - Restore "Limitations"
* Improve kani-compiler logs
1. Add option to force colored output.
- This is useful for IDEs and potentially to be used in cargo-kani.
2. Add a few info_span to make the logs more readable.
- This will indent the log related to each statement, in every
function.
…signed to unsigned overflow failures (model-checking#995)
* Documentation: Workarounds (new section) * Update docs/src/workarounds.md Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
* Add harness to VecDeque CVE
* Documentation: Updates for "Regression testing" * Add `ui` to the Kani testing suites
* Documentation: Updates for "First steps" * Use "preferred" instead of "favorite"
* Documentation: Updates for "Rust feature support" * Documentation: Updates for "Overrides" * Add contents to main chapter * Restore empty "Guarantees" section
* Documentation: Updates for "Book runner" * Use "overwritten" instead of "gone"
* Documentation: Applications (new section) * Address Jai's comments.
* Updates for `README.md` * Address comments * Use lowercase in bullet list
…el-checking#1002) * Replace cprover_Asserts * Add Tests for Property Classes
* Remove "The" in documentation title * Use `**NOTE**:` for all notes * Use "code available here" for links to example files. * Use `<directory>` as labels for links to directories * Use more contractions
* Update readme for readability
* Add a test for `discriminant_value` * Split into 4 proofs
* This separates "setup" from "build"
rustc reasonably translates if statements at end of a loop body to backwards jumps to the loop head. This, however, causes CBMC's symbolic execution to spuriously treat these as nested loops. This commit now enables a rewrite step that had previously been built for exactly such cases.
4 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description of changes:
rustc reasonably translates if statements at end of a loop body to
backwards jumps to the loop head. This, however, causes CBMC's symbolic
execution to spuriously treat these as nested loops. This commit now
enables a rewrite step that had previously been built for exactly such
cases.
Testing:
How is this change tested? Not yet - @adpaco-aws has an example that exercises this.
Is this a refactor change? No.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.