Skip to content

Commit 1062f31

Browse files
committed
add NLL-like imprecision examples
These tests showcase the same imprecision as NLLs, unlike the datalog implementation, when using reachability as a liveness approximation.
1 parent a2323a9 commit 1062f31

12 files changed

+344
-0
lines changed
Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
error: lifetime may not live long enough
2+
--> $DIR/flow-sensitive-invariance.rs:20:17
3+
|
4+
LL | fn use_it<'a, 'b>(choice: bool) -> Result<Invariant<'a>, Invariant<'b>> {
5+
| -- -- lifetime `'b` defined here
6+
| |
7+
| lifetime `'a` defined here
8+
LL | let returned_value = create_invariant();
9+
LL | if choice { Ok(returned_value) } else { Err(returned_value) }
10+
| ^^^^^^^^^^^^^^^^^^ function was supposed to return data with lifetime `'a` but it is returning data with lifetime `'b`
11+
|
12+
= help: consider adding the following bound: `'b: 'a`
13+
= note: requirement occurs because of the type `Invariant<'_>`, which makes the generic argument `'_` invariant
14+
= note: the struct `Invariant<'l>` is invariant over the parameter `'l`
15+
= help: see <https://doc.rust-lang.org/nomicon/subtyping.html> for more information about variance
16+
17+
error: lifetime may not live long enough
18+
--> $DIR/flow-sensitive-invariance.rs:20:45
19+
|
20+
LL | fn use_it<'a, 'b>(choice: bool) -> Result<Invariant<'a>, Invariant<'b>> {
21+
| -- -- lifetime `'b` defined here
22+
| |
23+
| lifetime `'a` defined here
24+
LL | let returned_value = create_invariant();
25+
LL | if choice { Ok(returned_value) } else { Err(returned_value) }
26+
| ^^^^^^^^^^^^^^^^^^^ function was supposed to return data with lifetime `'b` but it is returning data with lifetime `'a`
27+
|
28+
= help: consider adding the following bound: `'a: 'b`
29+
= note: requirement occurs because of the type `Invariant<'_>`, which makes the generic argument `'_` invariant
30+
= note: the struct `Invariant<'l>` is invariant over the parameter `'l`
31+
= help: see <https://doc.rust-lang.org/nomicon/subtyping.html> for more information about variance
32+
33+
help: `'a` and `'b` must be the same: replace one with the other
34+
35+
error: aborting due to 2 previous errors
36+
Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
error: lifetime may not live long enough
2+
--> $DIR/flow-sensitive-invariance.rs:20:17
3+
|
4+
LL | fn use_it<'a, 'b>(choice: bool) -> Result<Invariant<'a>, Invariant<'b>> {
5+
| -- -- lifetime `'b` defined here
6+
| |
7+
| lifetime `'a` defined here
8+
LL | let returned_value = create_invariant();
9+
LL | if choice { Ok(returned_value) } else { Err(returned_value) }
10+
| ^^^^^^^^^^^^^^^^^^ function was supposed to return data with lifetime `'a` but it is returning data with lifetime `'b`
11+
|
12+
= help: consider adding the following bound: `'b: 'a`
13+
= note: requirement occurs because of the type `Invariant<'_>`, which makes the generic argument `'_` invariant
14+
= note: the struct `Invariant<'l>` is invariant over the parameter `'l`
15+
= help: see <https://doc.rust-lang.org/nomicon/subtyping.html> for more information about variance
16+
17+
error: lifetime may not live long enough
18+
--> $DIR/flow-sensitive-invariance.rs:20:45
19+
|
20+
LL | fn use_it<'a, 'b>(choice: bool) -> Result<Invariant<'a>, Invariant<'b>> {
21+
| -- -- lifetime `'b` defined here
22+
| |
23+
| lifetime `'a` defined here
24+
LL | let returned_value = create_invariant();
25+
LL | if choice { Ok(returned_value) } else { Err(returned_value) }
26+
| ^^^^^^^^^^^^^^^^^^^ function was supposed to return data with lifetime `'b` but it is returning data with lifetime `'a`
27+
|
28+
= help: consider adding the following bound: `'a: 'b`
29+
= note: requirement occurs because of the type `Invariant<'_>`, which makes the generic argument `'_` invariant
30+
= note: the struct `Invariant<'l>` is invariant over the parameter `'l`
31+
= help: see <https://doc.rust-lang.org/nomicon/subtyping.html> for more information about variance
32+
33+
help: `'a` and `'b` must be the same: replace one with the other
34+
35+
error: aborting due to 2 previous errors
36+
Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
// An example (from @steffahn) of reachability as an approximation of liveness where the polonius
2+
// alpha analysis shows the same imprecision as NLLs, unlike the datalog implementation.
3+
4+
//@ ignore-compare-mode-polonius (explicit revisions)
5+
//@ revisions: nll polonius legacy
6+
//@ [polonius] compile-flags: -Z polonius=next
7+
//@ [legacy] check-pass
8+
//@ [legacy] compile-flags: -Z polonius=legacy
9+
10+
use std::cell::Cell;
11+
12+
struct Invariant<'l>(Cell<&'l ()>);
13+
14+
fn create_invariant<'l>() -> Invariant<'l> {
15+
Invariant(Cell::new(&()))
16+
}
17+
18+
fn use_it<'a, 'b>(choice: bool) -> Result<Invariant<'a>, Invariant<'b>> {
19+
let returned_value = create_invariant();
20+
if choice { Ok(returned_value) } else { Err(returned_value) }
21+
//[nll]~^ ERROR lifetime may not live long enough
22+
//[nll]~| ERROR lifetime may not live long enough
23+
//[polonius]~^^^ ERROR lifetime may not live long enough
24+
//[polonius]~| ERROR lifetime may not live long enough
25+
}
26+
27+
fn use_it_buth_its_the_same<'a: 'b, 'b: 'a>(choice: bool) -> Result<Invariant<'a>, Invariant<'b>> {
28+
let returned_value = create_invariant();
29+
if choice { Ok(returned_value) } else { Err(returned_value) }
30+
}
31+
32+
fn main() {}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
error[E0499]: cannot borrow `*elements` as mutable more than once at a time
2+
--> $DIR/iterating-updating-cursor-108704.rs:36:26
3+
|
4+
LL | for (idx, el) in elements.iter_mut().enumerate() {
5+
| ^^^^^^^^
6+
| |
7+
| `*elements` was mutably borrowed here in the previous iteration of the loop
8+
| first borrow used here, in later iteration of loop
9+
10+
error: aborting due to 1 previous error
11+
12+
For more information about this error, try `rustc --explain E0499`.
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
error[E0499]: cannot borrow `*elements` as mutable more than once at a time
2+
--> $DIR/iterating-updating-cursor-108704.rs:36:26
3+
|
4+
LL | for (idx, el) in elements.iter_mut().enumerate() {
5+
| ^^^^^^^^
6+
| |
7+
| `*elements` was mutably borrowed here in the previous iteration of the loop
8+
| first borrow used here, in later iteration of loop
9+
10+
error: aborting due to 1 previous error
11+
12+
For more information about this error, try `rustc --explain E0499`.
Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
// An example from #108704 of the linked-list cursor-like pattern of #46859/#48001, where the
2+
// polonius alpha analysis shows the same imprecision as NLLs, unlike the datalog implementation.
3+
4+
//@ ignore-compare-mode-polonius (explicit revisions)
5+
//@ revisions: nll polonius legacy
6+
//@ [polonius] compile-flags: -Z polonius=next
7+
//@ [legacy] check-pass
8+
//@ [legacy] compile-flags: -Z polonius=legacy
9+
10+
struct Root {
11+
children: Vec<Node>,
12+
}
13+
14+
struct Node {
15+
name: String,
16+
children: Vec<Node>,
17+
}
18+
19+
fn merge_tree_ok(root: &mut Root, path: Vec<String>) {
20+
let mut elements = &mut root.children;
21+
22+
for p in path.iter() {
23+
for (idx, el) in elements.iter_mut().enumerate() {
24+
if el.name == *p {
25+
elements = &mut elements[idx].children;
26+
break;
27+
}
28+
}
29+
}
30+
}
31+
32+
fn merge_tree_ko(root: &mut Root, path: Vec<String>) {
33+
let mut elements = &mut root.children;
34+
35+
for p in path.iter() {
36+
for (idx, el) in elements.iter_mut().enumerate() {
37+
//[nll]~^ ERROR cannot borrow `*elements` as mutable more than once at a time
38+
//[polonius]~^^ ERROR cannot borrow `*elements` as mutable more than once at a time
39+
if el.name == *p {
40+
elements = &mut el.children;
41+
break;
42+
}
43+
}
44+
}
45+
}
46+
47+
fn main() {}
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
error[E0499]: cannot borrow `p.0` as mutable more than once at a time
2+
--> $DIR/iterating-updating-cursor-57165.rs:25:20
3+
|
4+
LL | while let Some(now) = p {
5+
| ^^^ - first borrow used here, in later iteration of loop
6+
| |
7+
| `p.0` was mutably borrowed here in the previous iteration of the loop
8+
9+
error[E0503]: cannot use `*p` because it was mutably borrowed
10+
--> $DIR/iterating-updating-cursor-57165.rs:25:27
11+
|
12+
LL | while let Some(now) = p {
13+
| --- ^
14+
| | |
15+
| | use of borrowed `p.0`
16+
| | borrow later used here
17+
| `p.0` is borrowed here
18+
19+
error: aborting due to 2 previous errors
20+
21+
Some errors have detailed explanations: E0499, E0503.
22+
For more information about an error, try `rustc --explain E0499`.
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
error[E0499]: cannot borrow `p.0` as mutable more than once at a time
2+
--> $DIR/iterating-updating-cursor-57165.rs:25:20
3+
|
4+
LL | while let Some(now) = p {
5+
| ^^^ - first borrow used here, in later iteration of loop
6+
| |
7+
| `p.0` was mutably borrowed here in the previous iteration of the loop
8+
9+
error[E0503]: cannot use `*p` because it was mutably borrowed
10+
--> $DIR/iterating-updating-cursor-57165.rs:25:27
11+
|
12+
LL | while let Some(now) = p {
13+
| --- ^
14+
| | |
15+
| | use of borrowed `p.0`
16+
| | borrow later used here
17+
| `p.0` is borrowed here
18+
19+
error: aborting due to 2 previous errors
20+
21+
Some errors have detailed explanations: E0499, E0503.
22+
For more information about an error, try `rustc --explain E0499`.
Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
// An example from #57165 of the linked-list cursor-like pattern of #46859/#48001, where the
2+
// polonius alpha analysis shows the same imprecision as NLLs, unlike the datalog implementation.
3+
4+
//@ ignore-compare-mode-polonius (explicit revisions)
5+
//@ revisions: nll polonius legacy
6+
//@ [polonius] compile-flags: -Z polonius=next
7+
//@ [legacy] check-pass
8+
//@ [legacy] compile-flags: -Z polonius=legacy
9+
10+
struct X {
11+
next: Option<Box<X>>,
12+
}
13+
14+
fn no_control_flow() {
15+
let mut b = Some(Box::new(X { next: None }));
16+
let mut p = &mut b;
17+
while let Some(now) = p {
18+
p = &mut now.next;
19+
}
20+
}
21+
22+
fn conditional() {
23+
let mut b = Some(Box::new(X { next: None }));
24+
let mut p = &mut b;
25+
while let Some(now) = p {
26+
//[nll]~^ ERROR cannot borrow `p.0` as mutable more than once at a time
27+
//[nll]~| ERROR cannot use `*p` because it was mutably borrowed
28+
//[polonius]~^^^ ERROR cannot borrow `p.0` as mutable more than once at a time
29+
//[polonius]~| ERROR cannot use `*p` because it was mutably borrowed
30+
if true {
31+
p = &mut now.next;
32+
}
33+
}
34+
}
35+
36+
fn conditional_with_indirection() {
37+
let mut b = Some(Box::new(X { next: None }));
38+
let mut p = &mut b;
39+
while let Some(now) = p {
40+
if true {
41+
p = &mut p.as_mut().unwrap().next;
42+
}
43+
}
44+
}
45+
46+
fn main() {}
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
error[E0506]: cannot assign to `*node_ref` because it is borrowed
2+
--> $DIR/iterating-updating-cursor-63908.rs:38:5
3+
|
4+
LL | fn remove_last_node_iterative<T>(mut node_ref: &mut List<T>) {
5+
| - let's call the lifetime of this reference `'1`
6+
LL | loop {
7+
LL | let next_ref = &mut node_ref.as_mut().unwrap().next;
8+
| -------- `*node_ref` is borrowed here
9+
...
10+
LL | node_ref = next_ref;
11+
| ------------------- assignment requires that `*node_ref` is borrowed for `'1`
12+
...
13+
LL | *node_ref = None;
14+
| ^^^^^^^^^ `*node_ref` is assigned to here but it was already borrowed
15+
16+
error: aborting due to 1 previous error
17+
18+
For more information about this error, try `rustc --explain E0506`.
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
error[E0506]: cannot assign to `*node_ref` because it is borrowed
2+
--> $DIR/iterating-updating-cursor-63908.rs:38:5
3+
|
4+
LL | fn remove_last_node_iterative<T>(mut node_ref: &mut List<T>) {
5+
| - let's call the lifetime of this reference `'1`
6+
LL | loop {
7+
LL | let next_ref = &mut node_ref.as_mut().unwrap().next;
8+
| -------- `*node_ref` is borrowed here
9+
...
10+
LL | node_ref = next_ref;
11+
| ------------------- assignment requires that `*node_ref` is borrowed for `'1`
12+
...
13+
LL | *node_ref = None;
14+
| ^^^^^^^^^ `*node_ref` is assigned to here but it was already borrowed
15+
16+
error: aborting due to 1 previous error
17+
18+
For more information about this error, try `rustc --explain E0506`.
Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
// An example from #63908 of the linked-list cursor-like pattern of #46859/#48001, where the
2+
// polonius alpha analysis shows the same imprecision as NLLs, unlike the datalog implementation.
3+
4+
//@ ignore-compare-mode-polonius (explicit revisions)
5+
//@ revisions: nll polonius legacy
6+
//@ [polonius] compile-flags: -Z polonius=next
7+
//@ [legacy] check-pass
8+
//@ [legacy] compile-flags: -Z polonius=legacy
9+
10+
struct Node<T> {
11+
value: T,
12+
next: Option<Box<Self>>,
13+
}
14+
15+
type List<T> = Option<Box<Node<T>>>;
16+
17+
fn remove_last_node_recursive<T>(node_ref: &mut List<T>) {
18+
let next_ref = &mut node_ref.as_mut().unwrap().next;
19+
20+
if next_ref.is_some() {
21+
remove_last_node_recursive(next_ref);
22+
} else {
23+
*node_ref = None;
24+
}
25+
}
26+
27+
fn remove_last_node_iterative<T>(mut node_ref: &mut List<T>) {
28+
loop {
29+
let next_ref = &mut node_ref.as_mut().unwrap().next;
30+
31+
if next_ref.is_some() {
32+
node_ref = next_ref;
33+
} else {
34+
break;
35+
}
36+
}
37+
38+
*node_ref = None;
39+
//[nll]~^ ERROR cannot assign to `*node_ref` because it is borrowed
40+
//[polonius]~^^ ERROR cannot assign to `*node_ref` because it is borrowed
41+
}
42+
43+
fn main() {}

0 commit comments

Comments
 (0)