Get rid of all old-style string literals and string types in the compiler #2907

msullivan · 2012-07-13T21:15:03Z

This is part of #2653, and depends on #2906.

We should should replace str with ~str and "foo" with ~"foo" throughout the compiler, once it is supported. We should also replace all str/~ with ~str.

The text was updated successfully, but these errors were encountered:

Changes: ```` rustup to rust-lang#70043 map_clone: avoid suggesting `copied()` for &mut fix redundant_pattern_matching lint Add tests for rust-lang#1654 Don't trigger while_let_on_iterator when the iterator is recreated every iteration Update issue_2356.stderr reference file Update while_let_on_iterator tests Fix while_let_on_iterator suggestion and make it MachineApplicable Add lifetime test case for `new_ret_no_self` rustup rust-lang#71215 Downgrade match_bool to pedantic Run fetch before testing if master contains beta The beta branch update should not require a force push Add a note to the beta sections of release.md Remove apt-get upgrade again Always use the deploy script and templates of the master branch README: fix lit count line clippy_dev: make it fatal when the regex for updating lint count does not match `predecessors_for` will be removed soon Rustup "Remove `BodyAndCache`" Only run (late) internal lints, when they are warn/deny/forbid Only run cargo lints, when they are warn/deny/forbid span_lint_and_note now takes an Option<Span> for the note_span instead of just a span Make lint also capture blocks and closures, adjust language to mention other mutex types don't test the code in the lint docs Switch to matching against full paths instead of just the last element of the path Lint for holding locks across await points Also mention `--fix` for nightly users fix crash on issue-69020-assoc-const-arith-overflow.rs Address review comments remark fixes Update CHANGELOG.md for Rust 1.43 and 1.44 update stderr file util/fetch_prs_between.sh: Add Markdown formatted Link factor ifs into function, add differing mutex test Update the changelog update documentation Apply suggestions from PR review update span_lint_and_help call to six args test for mutex eq, add another test case use if chain cargo dev fmt fix map import to rustc_middle dev update_lints fix internal clippy warnings change visitor name to OppVisitor use Visitor api to find Mutex::lock calls add note about update-all-refs script, revert redundant pat to master move closures to seperate fns, remove known problems use span_lint_and_help, cargo dev fmt creating suggestion progress work on suggestion for auto fix Implement unsafe_derive_deserialize lint Update empty_enum.stderr Formatting and naming Formatting and naming Cleanup: `node_id` -> `hir_id` Fix issue rust-lang#2907. Don't trigger toplevel_ref_arg for `for` loops Cleanup: future_not_send: use `return_ty` method Remove badge FIXME from Cargo.toml Change note_span argument for span_lint_and_note. Add an Option<Span> argument to span_lint_and_help. Fixes internal lint warning in code base. Implement collapsible_span_lint_calls lint. ```` Fixes rust-lang#71453

@Dylan-DPC

submodules: update clippy from 891e1a8 to d01a498 Changes: ```` `predecessors_for` will be removed soon Rustup "Remove `BodyAndCache`" span_lint_and_note now takes an Option<Span> for the note_span instead of just a span Make lint also capture blocks and closures, adjust language to mention other mutex types don't test the code in the lint docs Switch to matching against full paths instead of just the last element of the path Lint for holding locks across await points fix crash on issue-69020-assoc-const-arith-overflow.rs update stderr file util/fetch_prs_between.sh: Add Markdown formatted Link factor ifs into function, add differing mutex test Update the changelog update documentation Apply suggestions from PR review update span_lint_and_help call to six args test for mutex eq, add another test case use if chain cargo dev fmt fix map import to rustc_middle dev update_lints fix internal clippy warnings change visitor name to OppVisitor use Visitor api to find Mutex::lock calls add note about update-all-refs script, revert redundant pat to master move closures to seperate fns, remove known problems use span_lint_and_help, cargo dev fmt creating suggestion progress work on suggestion for auto fix Implement unsafe_derive_deserialize lint Update empty_enum.stderr Formatting and naming Formatting and naming Cleanup: `node_id` -> `hir_id` Fix issue rust-lang#2907. Don't trigger toplevel_ref_arg for `for` loops Cleanup: future_not_send: use `return_ty` method Remove badge FIXME from Cargo.toml Change note_span argument for span_lint_and_note. Add an Option<Span> argument to span_lint_and_help. Fixes internal lint warning in code base. Implement collapsible_span_lint_calls lint. ```` Fixes rust-lang#71453 r? @Dylan-DPC

Update the "borrow box" lint to avoid recommending the following conversion: ``` // Old pub fn f(&mut Box<T>) {...} // New pub fn f(&mut T) {...} ``` Given a mutable reference to a box, functions may want to change "which" object the Box is pointing at. This change avoids recommending removing the "Box" parameter for mutable references.

Fix issue rust-lang#2907. Update the "borrow box" lint to avoid recommending the following conversion: ``` // Old pub fn f(&mut Box<T>) {...} // New pub fn f(&mut T) {...} ``` Given a mutable reference to a box, functions may want to change "which" object the Box is pointing at. This change avoids recommending removing the "Box" parameter for mutable references. changelog: Don't trigger [`borrow_box`] lint on `&mut Box` references

Rustup

Extends the function contract functionality with a `modifies` clause. The design is different from rust-lang#2594 but serves a similar purpose. The `modifies` clause allows the user to specify which parts of a structure a function may assign to. Essentially refining the `mut` annotation. We allow arbitrary (side-effect free) expressions in the `modifies` clause. The expressions are evaluated as part of the preconditions and passed to the function-under-verification as additional arguments. CBMC is then instructed to check that those locations are assigned. Aliasing means that this also adds the location in the original structure to the write set. Each expression must return a pointer to a value that implements `Arbitrary`. On replacement we then simply assign `*ptr = kani::any()`, relying again on aliasing to update the original structure. Additional tests for the new functionality are provided. Resolves rust-lang#2594 ## Open Questions ### API divergence from CBMC (accepted) The current design goes roughly as follows: We start with a `modifies` annotation on a function ```rs #[modifies(obj.some_expr())] fn target(obj: ...) { ... } ``` And from this we generate code to the effect of (simplified here) ```rs fn target_check(obj: ...) { // Undo the lifetime entanglements let modified_1 = std::mem::transmute::<&'a _, &'b _>(obj.some_expr()); target_wrapper(obj, modified_1); } #[cbmc::assigns(*modified_1)] fn target_wrapper(obj: ..., modified_1: &impl kani::Arbitrary) { ... } ``` Unlike CBMC we expect `obj.some_expr()` to be of a **pointer type** (`*const`, `*mut`, `&mut` or `&`) that points to the object which is target of the modification. So if we had a `t : &mut T` that was modified, CBMC would expect its assigns clause to say `*t`, but we expect `t` (no dereference). The reason is that the code we generate uses the workaround of creating an alias to whichever part of `obj` is modified and registers the alias with CBMC (thereby registering the original also). If we generated code where the right side of `let modified_1 =` is not of pointer type, then the object is moved to the stack and the aliasing destroyed. The open questions is whether we are happy with this change in API. (Yes) ### Test cases when expressions are used in the clause. With more complex expressions in the modifies clause it becomes hard to define good test cases because they reference generated code as in this case: ```rs #[kani::requires(**ptr < 100)] #[kani::modifies(ptr.as_ref())] fn modify(ptr: &mut Box<u32>) { *ptr.as_mut() += 1; } ``` This passes (as it should) and when commenting out the `modifies` clause we get this error: ``` Check 56: modify_wrapper_895c4e.assigns.2 - Status: FAILURE - Description: "Check that *var_2 is assignable" - Location: assigns_expr_pass.rs:8:5 in function modify_wrapper_895c4e ``` The information in this error is very non-specific, hard to read and brittle. How should we define robust "expected" test cases for such errors? ### Corner Cases / Future Improvements - rust-lang#2907 - rust-lang#2908 - rust-lang#2909 ## TODOs - [ ] Test Cases where the clause contains - [x] `Rc` + (`RefCell` or `unsafe`) (see rust-lang#2907) - [x] Fields - [x] Statement expressions - [x] `Vec` (see rust-lang#2909) - [ ] Fat pointers - [ ] update contracts documentation - [x] Make sure the wrapper arguments are unique. - [x] Ensure `nondet-static-exclude` always uses the correct filepath (relative or absolute) - [ ] Test case for multiple `modifies` clauses. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>

ghost assigned msullivan Jul 13, 2012

msullivan mentioned this issue Jul 13, 2012

Stop accepting /~, /@, and /& vstore symbols #2908

Closed

msullivan closed this as completed in 92743dc Jul 14, 2012

msullivan removed their assignment Jun 16, 2014

RalfJung pushed a commit to RalfJung/rust that referenced this issue Jun 3, 2023

Auto merge of rust-lang#2907 - RalfJung:rustup, r=RalfJung

fb35803

Rustup

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Get rid of all old-style string literals and string types in the compiler #2907

Get rid of all old-style string literals and string types in the compiler #2907

msullivan commented Jul 13, 2012

Get rid of all old-style string literals and string types in the compiler #2907

Get rid of all old-style string literals and string types in the compiler #2907

Comments

msullivan commented Jul 13, 2012