Skip to content

Commit dd4f041

Browse files
committed
Remove loan_(read|write)_refined fields from PermissionsData. Revert stepper changes to use the seperate fields so that the snapshots are easier to reason through.
1 parent 260d69e commit dd4f041

16 files changed

+83
-395
lines changed

crates/aquascope/src/analysis/mod.rs

Lines changed: 35 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,8 +57,41 @@ pub struct LoanKey(pub u32);
5757
)]
5858
#[ts(export)]
5959
pub enum LoanRefined<T> {
60-
RefineOnlyWrite { write_key: T },
61-
RefineReadAndWrite { write_key: T },
60+
None,
61+
Read { key: T },
62+
Write { key: T },
63+
}
64+
65+
impl<T> LoanRefined<T> {
66+
pub fn as_read_refinement(self) -> Option<T> {
67+
match self {
68+
Self::Read { key } => Some(key),
69+
_ => None,
70+
}
71+
}
72+
73+
pub fn as_write_refinement(self) -> Option<T> {
74+
match self {
75+
Self::Read { key } | Self::Write { key } => Some(key),
76+
_ => None,
77+
}
78+
}
79+
80+
pub fn not_refined(&self) -> bool {
81+
matches!(self, LoanRefined::None)
82+
}
83+
84+
pub fn is_refined(&self) -> bool {
85+
!self.not_refined()
86+
}
87+
88+
pub fn is_read_refined(&self) -> bool {
89+
matches!(self, LoanRefined::Read { .. })
90+
}
91+
92+
pub fn is_write_refined(&self) -> bool {
93+
self.is_read_refined() || matches!(self, LoanRefined::Write { .. })
94+
}
6295
}
6396

6497
#[derive(

crates/aquascope/src/analysis/permissions/context.rs

Lines changed: 7 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -300,9 +300,7 @@ impl<'tcx> PermissionsCtxt<'tcx> {
300300
type_copyable: ty.is_copyable(self.tcx, self.typing_env),
301301
path_moved: None,
302302
path_uninitialized: false,
303-
loan_read_refined: None,
304-
loan_write_refined: None,
305-
loan_refined: None,
303+
loan_refined: LoanRefined::None,
306304
loan_drop_refined: None,
307305
}
308306
}
@@ -383,20 +381,16 @@ impl<'tcx> PermissionsCtxt<'tcx> {
383381
let loan_write_refined: Option<LoanKey> =
384382
loan_write_refined.get(path).map(Into::<LoanKey>::into);
385383

386-
let loan_refined: Option<LoanRefined<LoanKey>> = match (
384+
let loan_refined: LoanRefined<LoanKey> = match (
387385
loan_read_refined,
388386
loan_write_refined,
389387
) {
390-
(Some(_read_key), Some(write_key)) => {
391-
Some(LoanRefined::RefineReadAndWrite { write_key })
392-
}
393-
(None, Some(write_key)) => {
394-
Some(LoanRefined::RefineOnlyWrite { write_key })
395-
}
396-
(Some(_read_key), None) => {
388+
(Some(..), Some(key)) => LoanRefined::Read { key },
389+
(None, Some(key)) => LoanRefined::Write { key },
390+
(Some(..), None) => {
397391
unreachable!("If read permissions are lost at a point, write permissions are also lost.")
398392
}
399-
(None, None) => None,
393+
(None, None) => LoanRefined::None,
400394
};
401395
let loan_drop_refined: Option<LoanKey> =
402396
loan_drop_refined.get(path).map(Into::<LoanKey>::into);
@@ -408,8 +402,6 @@ impl<'tcx> PermissionsCtxt<'tcx> {
408402
is_live,
409403
path_uninitialized,
410404
path_moved,
411-
loan_read_refined,
412-
loan_write_refined,
413405
loan_refined,
414406
loan_drop_refined,
415407
}
@@ -434,9 +426,7 @@ impl<'tcx> PermissionsCtxt<'tcx> {
434426
type_copyable: false,
435427
path_moved: None,
436428
path_uninitialized: false,
437-
loan_read_refined: None,
438-
loan_write_refined: None,
439-
loan_refined: None,
429+
loan_refined: LoanRefined::None,
440430
loan_drop_refined: None,
441431
})
442432
})

crates/aquascope/src/analysis/permissions/mod.rs

Lines changed: 4 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -102,17 +102,9 @@ pub struct PermissionsData {
102102
#[serde(skip_serializing_if = "Option::is_none")]
103103
pub path_moved: Option<MoveKey>,
104104

105-
#[serde(skip_serializing_if = "Option::is_none")]
106-
/// Is a live loan removing `read` permissions?
107-
pub loan_read_refined: Option<LoanKey>,
108-
109-
#[serde(skip_serializing_if = "Option::is_none")]
110-
/// Is a live loan removing `write` permissions?
111-
pub loan_write_refined: Option<LoanKey>,
112-
113-
#[serde(skip_serializing_if = "Option::is_none")]
105+
#[serde(skip_serializing_if = "LoanRefined::not_refined")]
114106
/// Is a live loan removing `read` or `write` permissions?
115-
pub loan_refined: Option<LoanRefined<LoanKey>>,
107+
pub loan_refined: LoanRefined<LoanKey>,
116108

117109
#[serde(skip_serializing_if = "Option::is_none")]
118110
/// Is a live loan removing `drop` permissions?
@@ -147,9 +139,9 @@ impl PermissionsData {
147139
/// - no drop-refining loan exists at this point.
148140
pub fn permissions_ignore_liveness(&self) -> Permissions {
149141
let mem_uninit = self.path_moved.is_some() || self.path_uninitialized;
150-
let read = !mem_uninit && self.loan_read_refined.is_none();
142+
let read = !mem_uninit && !self.loan_refined.is_read_refined();
151143
let write =
152-
self.type_writeable && read && self.loan_write_refined.is_none();
144+
self.type_writeable && read && !self.loan_refined.is_write_refined();
153145
let drop = self.type_droppable && read && self.loan_drop_refined.is_none();
154146
Permissions { read, write, drop }
155147
}

crates/aquascope/src/analysis/stepper/mod.rs

Lines changed: 35 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ use rustc_utils::source_map::range::CharRange;
1717
use serde::{Deserialize, Serialize};
1818
use ts_rs::TS;
1919

20-
use super::LoanRefined;
2120
use crate::analysis::{
2221
permissions::{
2322
Permissions, PermissionsCtxt, PermissionsData, PermissionsDomain,
@@ -106,6 +105,18 @@ pub enum ValueStep<A: Stepable> {
106105
}
107106

108107
impl<A: Stepable> ValueStep<A> {
108+
fn high(value: A) -> Self {
109+
Self::High { value }
110+
}
111+
112+
fn none() -> Self {
113+
Self::None { value: None }
114+
}
115+
116+
fn already(value: A) -> Self {
117+
Self::None { value: Some(value) }
118+
}
119+
109120
// TODO: this is a loose surface-level notion of symmetry.
110121
fn is_symmetric_diff(&self, rhs: &Self) -> bool {
111122
matches!(
@@ -168,9 +179,8 @@ pub struct PermissionsDataDiff {
168179
pub type_writeable: ValueStep<bool>,
169180
pub path_moved: ValueStep<MoveKey>,
170181
pub path_uninitialized: ValueStep<bool>,
171-
pub loan_read_refined: ValueStep<LoanKey>, // ValueStep<LoanRefined<LoanKey>> where LoanRefined is ReadOnly or ReadPlusWrite
182+
pub loan_read_refined: ValueStep<LoanKey>,
172183
pub loan_write_refined: ValueStep<LoanKey>,
173-
pub loan_refined: ValueStep<LoanRefined<LoanKey>>,
174184
pub loan_drop_refined: ValueStep<LoanKey>,
175185
pub permissions: PermissionsDiff,
176186
}
@@ -183,8 +193,16 @@ impl std::fmt::Debug for PermissionsDataDiff {
183193
writeln!(f, " type_droppable: {:?}", self.type_droppable)?;
184194
writeln!(f, " type_writeable: {:?}", self.type_writeable)?;
185195
writeln!(f, " path_moved: {:?}", self.path_moved)?;
186-
writeln!(f, " loan_write_refined: {:?}", self.loan_write_refined)?;
187-
writeln!(f, " loan_refined: {:?}", self.loan_refined)?;
196+
writeln!(
197+
f,
198+
" loan_read_refined: {:?}",
199+
self.loan_read_refined
200+
)?;
201+
writeln!(
202+
f,
203+
" loan_write_refined: {:?}",
204+
self.loan_write_refined
205+
)?;
188206
writeln!(f, " loan_drop_refined: {:?}", self.loan_drop_refined)?;
189207
Ok(())
190208
}
@@ -211,9 +229,9 @@ impl Difference for bool {
211229
if *self && !rhs {
212230
ValueStep::Low
213231
} else if !*self && rhs {
214-
ValueStep::High { value: true }
232+
ValueStep::high(true)
215233
} else {
216-
ValueStep::None { value: Some(*self) }
234+
ValueStep::already(*self)
217235
}
218236
}
219237
}
@@ -229,9 +247,9 @@ impl<A: Stepable> Difference for Option<A> {
229247

230248
fn diff(&self, rhs: Option<A>) -> Self::Diff {
231249
match (self, rhs) {
232-
(None, None) => ValueStep::None { value: None },
250+
(None, None) => ValueStep::none(),
233251
(Some(_), None) => ValueStep::Low,
234-
(None, Some(value)) => ValueStep::High { value },
252+
(None, Some(value)) => ValueStep::high(value),
235253
(Some(v0), Some(v1)) => {
236254
if *v0 != v1 {
237255
log::warn!(
@@ -264,9 +282,14 @@ impl Difference for PermissionsData {
264282
is_live: self.is_live.diff(rhs.is_live),
265283
type_droppable: self.type_droppable.diff(rhs.type_droppable),
266284
type_writeable: self.type_writeable.diff(rhs.type_writeable),
267-
loan_read_refined: self.loan_read_refined.diff(rhs.loan_read_refined),
268-
loan_write_refined: self.loan_write_refined.diff(rhs.loan_write_refined),
269-
loan_refined: self.loan_refined.diff(rhs.loan_refined),
285+
loan_read_refined: self
286+
.loan_refined
287+
.as_read_refinement()
288+
.diff(rhs.loan_refined.as_read_refinement()),
289+
loan_write_refined: self
290+
.loan_refined
291+
.as_write_refinement()
292+
.diff(rhs.loan_refined.as_write_refinement()),
270293
loan_drop_refined: self.loan_drop_refined.diff(rhs.loan_drop_refined),
271294
path_moved: self.path_moved.diff(rhs.path_moved),
272295
path_uninitialized: self.path_uninitialized.diff(rhs.path_uninitialized),

crates/aquascope/tests/snapshots/boundaries__main@assignop_path_resolution.test.snap

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -70,10 +70,9 @@ description: main@assignop_path_resolution.test
7070
type_copyable: true
7171
is_live: true
7272
path_uninitialized: false
73-
loan_write_refined: 0
7473
loan_refined:
75-
RefineOnlyWrite:
76-
write_key: 0
74+
Write:
75+
key: 0
7776
loan_drop_refined: 0
7877
- location:
7978
line: 8

0 commit comments

Comments
 (0)