diff options
| author | bors <bors@rust-lang.org> | 2024-08-16 15:48:55 +0000 |
|---|---|---|
| committer | bors <bors@rust-lang.org> | 2024-08-16 15:48:55 +0000 |
| commit | 1a51dd9247c5ecf9efa99ebf644bb12e33dcf3b5 (patch) | |
| tree | 45b98300bf22532abcb9bed6b5b47b83b6aa56c2 /src/tools/miri/tests | |
| parent | 86783bef33457473c5e96c8a89d71e11a7d1a5ba (diff) | |
| parent | 2c166f4f55f4b3062f907e8a72cff56a98978e58 (diff) | |
| download | rust-1a51dd9247c5ecf9efa99ebf644bb12e33dcf3b5.tar.gz rust-1a51dd9247c5ecf9efa99ebf644bb12e33dcf3b5.zip | |
Auto merge of #3754 - Vanille-N:master, r=RalfJung
Make unused states of Reserved unrepresentable
In the [previous TB update](https://github.com/rust-lang/miri/pull/3742) we discovered that the existence of `Reserved + !ty_is_freeze + protected` is undesirable.
This has the side effect of making `Reserved { conflicted: true, ty_is_freeze: false }` unreachable.
As such it is desirable that this state would also be unrepresentable.
This PR eliminates the unused configuration by changing
```rs
enum PermissionPriv {
Reserved { ty_is_freeze: bool, conflicted: bool },
...
}
```
into
```rs
enum PermissionPriv {
ReservedFrz { conflicted: bool },
ReservedIM,
...
}
```
but this is not the only solution and `Reserved(Activable | Conflicted | InteriorMut)` could be discussed.
In addition to making the unreachable state not representable anymore, this change has the nice side effect of enabling `foreign_read` to no longer depend explicitly on the `protected` flag.
Currently waiting for
- `@JoJoDeveloping` to confirm that this is the same representation of `Reserved` as what is being implemented in simuliris,
- `@RalfJung` to approve that this does not introduce too much overhead in the trusted codebase.
Diffstat (limited to 'src/tools/miri/tests')
10 files changed, 46 insertions, 46 deletions
diff --git a/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr b/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr index ce9a5b7f158..133a50938f2 100644 --- a/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr +++ b/src/tools/miri/tests/fail/tree_borrows/reserved/cell-protected-write.stderr @@ -2,11 +2,11 @@ Warning: this tree is indicative only. Some tags may have been hidden. 0.. 1 | Act | └─┬──<TAG=root of the allocation> -| RsM | └─┬──<TAG=base> -| RsM | ├─┬──<TAG=x> -| RsM | │ └─┬──<TAG=caller:x> -| Rs | │ └────<TAG=callee:x> Strongly protected -| RsM | └────<TAG=y, callee:y, caller:y> +| ReIM| └─┬──<TAG=base> +| ReIM| ├─┬──<TAG=x> +| ReIM| │ └─┬──<TAG=caller:x> +| Res | │ └────<TAG=callee:x> Strongly protected +| ReIM| └────<TAG=y, callee:y, caller:y> ────────────────────────────────────────────────── error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) at ALLOC[0x0] is forbidden --> $DIR/cell-protected-write.rs:LL:CC diff --git a/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr b/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr index 41559587bda..a4dc123979e 100644 --- a/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr +++ b/src/tools/miri/tests/fail/tree_borrows/reserved/int-protected-write.stderr @@ -2,11 +2,11 @@ Warning: this tree is indicative only. Some tags may have been hidden. 0.. 1 | Act | └─┬──<TAG=root of the allocation> -| Rs | └─┬──<TAG=n> -| Rs | ├─┬──<TAG=x> -| Rs | │ └─┬──<TAG=caller:x> -| Rs | │ └────<TAG=callee:x> Strongly protected -| Rs | └────<TAG=y, callee:y, caller:y> +| Res | └─┬──<TAG=n> +| Res | ├─┬──<TAG=x> +| Res | │ └─┬──<TAG=caller:x> +| Res | │ └────<TAG=callee:x> Strongly protected +| Res | └────<TAG=y, callee:y, caller:y> ────────────────────────────────────────────────── error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) at ALLOC[0x0] is forbidden --> $DIR/int-protected-write.rs:LL:CC diff --git a/src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr b/src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr index 57caa09c888..d13e9ad0215 100644 --- a/src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr +++ b/src/tools/miri/tests/pass/tree_borrows/cell-alternate-writes.stderr @@ -2,7 +2,7 @@ Warning: this tree is indicative only. Some tags may have been hidden. 0.. 1 | Act | └─┬──<TAG=root of the allocation> -| RsM | └────<TAG=data, x, y> +| ReIM| └────<TAG=data, x, y> ────────────────────────────────────────────────── ────────────────────────────────────────────────── Warning: this tree is indicative only. Some tags may have been hidden. diff --git a/src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr b/src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr index 69b8a17dc5e..4d77d96776d 100644 --- a/src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr +++ b/src/tools/miri/tests/pass/tree_borrows/end-of-protector.stderr @@ -2,27 +2,27 @@ Warning: this tree is indicative only. Some tags may have been hidden. 0.. 1 | Act | └─┬──<TAG=root of the allocation> -| Rs | └─┬──<TAG=data> -| Rs | └────<TAG=x> +| Res | └─┬──<TAG=data> +| Res | └────<TAG=x> ────────────────────────────────────────────────── ────────────────────────────────────────────────── Warning: this tree is indicative only. Some tags may have been hidden. 0.. 1 | Act | └─┬──<TAG=root of the allocation> -| Rs | └─┬──<TAG=data> -| Rs | └─┬──<TAG=x> -| Rs | └─┬──<TAG=caller:x> -| Rs | └────<TAG=callee:x> Strongly protected +| Res | └─┬──<TAG=data> +| Res | └─┬──<TAG=x> +| Res | └─┬──<TAG=caller:x> +| Res | └────<TAG=callee:x> Strongly protected ────────────────────────────────────────────────── ────────────────────────────────────────────────── Warning: this tree is indicative only. Some tags may have been hidden. 0.. 1 | Act | └─┬──<TAG=root of the allocation> -| Rs | └─┬──<TAG=data> -| Rs | ├─┬──<TAG=x> -| Rs | │ └─┬──<TAG=caller:x> -| Rs | │ └────<TAG=callee:x> -| Rs | └────<TAG=y> +| Res | └─┬──<TAG=data> +| Res | ├─┬──<TAG=x> +| Res | │ └─┬──<TAG=caller:x> +| Res | │ └────<TAG=callee:x> +| Res | └────<TAG=y> ────────────────────────────────────────────────── ────────────────────────────────────────────────── Warning: this tree is indicative only. Some tags may have been hidden. diff --git a/src/tools/miri/tests/pass/tree_borrows/formatting.stderr b/src/tools/miri/tests/pass/tree_borrows/formatting.stderr index 235ab68fe01..29f99034bab 100644 --- a/src/tools/miri/tests/pass/tree_borrows/formatting.stderr +++ b/src/tools/miri/tests/pass/tree_borrows/formatting.stderr @@ -2,7 +2,7 @@ Warning: this tree is indicative only. Some tags may have been hidden. 0.. 1.. 2.. 10.. 11.. 100.. 101..1000..1001..1024 | Act | Act | Act | Act | Act | Act | Act | Act | Act | └─┬──<TAG=root of the allocation> -| Rs | Act | Rs | Act | Rs | Act | Rs | Act | Rs | └─┬──<TAG=data, data> +| Res | Act | Res | Act | Res | Act | Res | Act | Res | └─┬──<TAG=data, data> |-----| Act |-----|?Dis |-----|?Dis |-----|?Dis |-----| ├────<TAG=data[1]> |-----|-----|-----| Act |-----|?Dis |-----|?Dis |-----| ├────<TAG=data[10]> |-----|-----|-----|-----|-----| Frz |-----|?Dis |-----| ├────<TAG=data[100]> diff --git a/src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr b/src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr index f09aa52f1a1..d589a062111 100644 --- a/src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr +++ b/src/tools/miri/tests/pass/tree_borrows/reborrow-is-read.stderr @@ -11,5 +11,5 @@ Warning: this tree is indicative only. Some tags may have been hidden. | Act | └─┬──<TAG=root of the allocation> | Act | └─┬──<TAG=parent> | Frz | ├────<TAG=x> -| Rs | └────<TAG=y> +| Res | └────<TAG=y> ────────────────────────────────────────────────── diff --git a/src/tools/miri/tests/pass/tree_borrows/reserved.stderr b/src/tools/miri/tests/pass/tree_borrows/reserved.stderr index d149a4065f9..be90382640b 100644 --- a/src/tools/miri/tests/pass/tree_borrows/reserved.stderr +++ b/src/tools/miri/tests/pass/tree_borrows/reserved.stderr @@ -3,20 +3,20 @@ Warning: this tree is indicative only. Some tags may have been hidden. 0.. 1 | Act | └─┬──<TAG=root of the allocation> -| RsM | └─┬──<TAG=base> -| RsM | ├─┬──<TAG=x> -| RsM | │ └─┬──<TAG=caller:x> -| RsC | │ └────<TAG=callee:x> -| RsM | └────<TAG=y, caller:y, callee:y> +| ReIM| └─┬──<TAG=base> +| ReIM| ├─┬──<TAG=x> +| ReIM| │ └─┬──<TAG=caller:x> +| ResC| │ └────<TAG=callee:x> +| ReIM| └────<TAG=y, caller:y, callee:y> ────────────────────────────────────────────────── [interior mut] Foreign Read: Re* -> Re* ────────────────────────────────────────────────── Warning: this tree is indicative only. Some tags may have been hidden. 0.. 8 | Act | └─┬──<TAG=root of the allocation> -| RsM | └─┬──<TAG=base> -| RsM | ├────<TAG=x> -| RsM | └────<TAG=y> +| ReIM| └─┬──<TAG=base> +| ReIM| ├────<TAG=x> +| ReIM| └────<TAG=y> ────────────────────────────────────────────────── [interior mut] Foreign Write: Re* -> Re* ────────────────────────────────────────────────── @@ -24,7 +24,7 @@ Warning: this tree is indicative only. Some tags may have been hidden. 0.. 8 | Act | └─┬──<TAG=root of the allocation> | Act | └─┬──<TAG=base> -| RsM | ├────<TAG=x> +| ReIM| ├────<TAG=x> | Act | └────<TAG=y> ────────────────────────────────────────────────── [protected] Foreign Read: Res -> Frz @@ -32,20 +32,20 @@ Warning: this tree is indicative only. Some tags may have been hidden. Warning: this tree is indicative only. Some tags may have been hidden. 0.. 1 | Act | └─┬──<TAG=root of the allocation> -| Rs | └─┬──<TAG=base> -| Rs | ├─┬──<TAG=x> -| Rs | │ └─┬──<TAG=caller:x> -| RsC | │ └────<TAG=callee:x> -| Rs | └────<TAG=y, caller:y, callee:y> +| Res | └─┬──<TAG=base> +| Res | ├─┬──<TAG=x> +| Res | │ └─┬──<TAG=caller:x> +| ResC| │ └────<TAG=callee:x> +| Res | └────<TAG=y, caller:y, callee:y> ────────────────────────────────────────────────── [] Foreign Read: Res -> Res ────────────────────────────────────────────────── Warning: this tree is indicative only. Some tags may have been hidden. 0.. 1 | Act | └─┬──<TAG=root of the allocation> -| Rs | └─┬──<TAG=base> -| Rs | ├────<TAG=x> -| Rs | └────<TAG=y> +| Res | └─┬──<TAG=base> +| Res | ├────<TAG=x> +| Res | └────<TAG=y> ────────────────────────────────────────────────── [] Foreign Write: Res -> Dis ────────────────────────────────────────────────── diff --git a/src/tools/miri/tests/pass/tree_borrows/unique.default.stderr b/src/tools/miri/tests/pass/tree_borrows/unique.default.stderr index 6e774e5014d..6098c855bde 100644 --- a/src/tools/miri/tests/pass/tree_borrows/unique.default.stderr +++ b/src/tools/miri/tests/pass/tree_borrows/unique.default.stderr @@ -2,8 +2,8 @@ Warning: this tree is indicative only. Some tags may have been hidden. 0.. 1 | Act | └─┬──<TAG=root of the allocation> -| Rs | └─┬──<TAG=base> -| Rs | └────<TAG=raw, uniq, uniq> +| Res | └─┬──<TAG=base> +| Res | └────<TAG=raw, uniq, uniq> ────────────────────────────────────────────────── ────────────────────────────────────────────────── Warning: this tree is indicative only. Some tags may have been hidden. diff --git a/src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr b/src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr index 26d9ad2ad38..960c7e216e1 100644 --- a/src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr +++ b/src/tools/miri/tests/pass/tree_borrows/unique.uniq.stderr @@ -2,8 +2,8 @@ Warning: this tree is indicative only. Some tags may have been hidden. 0.. 1 | Act | └─┬──<TAG=root of the allocation> -| Rs | └─┬──<TAG=base> -| Rs | └─┬──<TAG=raw> +| Res | └─┬──<TAG=base> +| Res | └─┬──<TAG=raw> |-----| └────<TAG=uniq, uniq> ────────────────────────────────────────────────── ────────────────────────────────────────────────── diff --git a/src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr b/src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr index f63aa1f6834..254eba061f4 100644 --- a/src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr +++ b/src/tools/miri/tests/pass/tree_borrows/vec_unique.default.stderr @@ -2,5 +2,5 @@ Warning: this tree is indicative only. Some tags may have been hidden. 0.. 2 | Act | └─┬──<TAG=root of the allocation> -| Rs | └────<TAG=base.as_ptr(), base.as_ptr(), raw_parts.0, reconstructed.as_ptr(), reconstructed.as_ptr()> +| Res | └────<TAG=base.as_ptr(), base.as_ptr(), raw_parts.0, reconstructed.as_ptr(), reconstructed.as_ptr()> ────────────────────────────────────────────────── |