Skip to content

Rewrite loops with multiple back edges to having a single back edge only#900

Closed
tautschnig wants to merge 10000 commits intomodel-checking:mainfrom
tautschnig:loop-fix
Closed

Rewrite loops with multiple back edges to having a single back edge only#900
tautschnig wants to merge 10000 commits intomodel-checking:mainfrom
tautschnig:loop-fix

Conversation

@tautschnig
Copy link
Member

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

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Xanewok and others added 30 commits January 16, 2022 15:30
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:&ensp;`""`
After:&ensp;`"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.
adpaco-aws and others added 24 commits March 30, 2022 19:20
…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.
* 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
* 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.