Skip to content

Commit 0662535

Browse files
committed
Better support for arrays
1 parent e7fd76f commit 0662535

7 files changed

+92
-22
lines changed

src/borrows/borrow_pcg_expansion.rs

+5-4
Original file line numberDiff line numberDiff line change
@@ -140,10 +140,11 @@ impl<'tcx> BorrowExpansion<'tcx> {
140140
BorrowExpansion::Fields(fields) => {
141141
assert!(fields.len() <= 1024, "Too many fields: {:?}", fields);
142142
fields
143-
.iter()
144-
.sorted_by_key(|(idx, _)| *idx)
145-
.map(|(idx, ty)| PlaceElem::Field(*idx, *ty))
146-
.collect()},
143+
.iter()
144+
.sorted_by_key(|(idx, _)| *idx)
145+
.map(|(idx, ty)| PlaceElem::Field(*idx, *ty))
146+
.collect()
147+
}
147148
BorrowExpansion::Deref => vec![PlaceElem::Deref],
148149
BorrowExpansion::Downcast(symbol, variant_idx) => {
149150
vec![PlaceElem::Downcast(*symbol, *variant_idx)]

src/borrows/borrows_graph/aliases.rs

+30-16
Original file line numberDiff line numberDiff line change
@@ -79,7 +79,7 @@ impl<'tcx> BorrowsGraph<'tcx> {
7979
for blocked in blocked_nodes {
8080
if seen.insert(blocked) {
8181
let blocked_node = egraph.add(get_node(blocked, place_ids));
82-
add_to_egraph(blocked_node, blocking_node, edge, egraph);
82+
add_to_egraph(blocked_node, blocking_node, edge, egraph, repacker);
8383
collect_nodes_up(graph, blocked, egraph, seen, place_ids, repacker);
8484
}
8585
}
@@ -109,22 +109,36 @@ impl<'tcx> BorrowsGraph<'tcx> {
109109
RPRelType::Unknown
110110
}
111111

112-
fn add_to_egraph(
112+
fn add_to_egraph<'mir, 'tcx>(
113113
blocked_node: Id,
114114
blocking_node: Id,
115-
edge: BorrowPCGEdgeRef<'_, '_>,
115+
edge: BorrowPCGEdgeRef<'tcx, '_>,
116116
egraph: &mut EGraph<EggPcgNode, ()>,
117+
repacker: PlaceRepacker<'mir, 'tcx>,
117118
) {
118119
match edge.kind() {
120+
BorrowPCGEdgeKind::RegionProjectionMember(member)
121+
if member.is_toplevel(repacker) =>
122+
{
123+
match member.kind {
124+
RegionProjectionMemberKind::BorrowOutlives => {
125+
record_deref(blocked_node, blocking_node, egraph);
126+
}
127+
RegionProjectionMemberKind::DerefBorrowOutlives => {
128+
record_deref(blocking_node, blocked_node, egraph);
129+
}
130+
_ => unreachable!(),
131+
}
132+
}
119133
BorrowPCGEdgeKind::BorrowPCGExpansion(expansion) => match expansion {
120134
BorrowPCGExpansion::FromOwned(_) => {
121-
record_deref(blocked_node, blocking_node, egraph)
135+
// record_deref(blocked_node, blocking_node, egraph)
122136
}
123137
BorrowPCGExpansion::FromBorrow(e) => {
124138
if e.expansion.is_deref() {
125-
record_deref(blocked_node, blocking_node, egraph);
139+
// record_deref(blocked_node, blocking_node, egraph);
126140
} else {
127-
egraph.union(blocked_node, blocking_node);
141+
// egraph.union(blocked_node, blocking_node);
128142
}
129143
}
130144
},
@@ -149,7 +163,7 @@ impl<'tcx> BorrowsGraph<'tcx> {
149163
let node: PCGNode<'tcx> = blocking.into();
150164
if seen.insert(node) {
151165
let blocking_id = egraph.add(get_node(node, place_ids));
152-
add_to_egraph(blocking_id, blocked_id, edge, egraph);
166+
add_to_egraph(blocking_id, blocked_id, edge, egraph, repacker);
153167
collect_nodes_down(graph, node, egraph, seen, place_ids, repacker);
154168
}
155169
}
@@ -256,15 +270,15 @@ fn main() {
256270
let temp: mir::Place<'_> = mir::Local::from(4 as usize).into();
257271
let star_temp = temp.project_deeper(&[mir::ProjectionElem::Deref], tcx);
258272
let repacker = PlaceRepacker::new(&body.body, tcx);
259-
// check_all_statements(&body.body, &mut pcg, |location, stmt| {
260-
// assert!(
261-
// !stmt
262-
// .aliases(star_temp.into(), repacker)
263-
// .contains(&temp.into()),
264-
// "Bad alias for {:?}",
265-
// location
266-
// );
267-
// });
273+
check_all_statements(&body.body, &mut pcg, |location, stmt| {
274+
assert!(
275+
!stmt
276+
.aliases(star_temp.into(), repacker)
277+
.contains(&temp.into()),
278+
"Bad alias for {:?}",
279+
location
280+
);
281+
});
268282
});
269283

270284
let input = r#"

src/borrows/borrows_visitor.rs

+12-1
Original file line numberDiff line numberDiff line change
@@ -323,6 +323,11 @@ impl<'tcx, 'mir, 'state> BorrowsVisitor<'tcx, 'mir, 'state> {
323323
location: Location,
324324
kind: impl Fn(usize) -> RegionProjectionMemberKind,
325325
) {
326+
tracing::info!(
327+
"Connect outliving projections {:?} -> {:?}",
328+
source_proj,
329+
target
330+
);
326331
for (idx, target_proj) in target
327332
.region_projections(self.repacker)
328333
.into_iter()
@@ -332,6 +337,11 @@ impl<'tcx, 'mir, 'state> BorrowsVisitor<'tcx, 'mir, 'state> {
332337
source_proj.region(self.repacker),
333338
target_proj.region(self.repacker),
334339
) {
340+
tracing::info!(
341+
"Adding region projection member {:?} -> {:?}",
342+
source_proj,
343+
target_proj
344+
);
335345
self.apply_action(BorrowPCGAction::add_region_projection_member(
336346
RegionProjectionMember::new(
337347
smallvec![source_proj.into()],
@@ -362,11 +372,12 @@ impl<'tcx, 'mir, 'state> BorrowsVisitor<'tcx, 'mir, 'state> {
362372
}
363373
match rvalue {
364374
Rvalue::Aggregate(
365-
box (AggregateKind::Adt(..) | AggregateKind::Tuple),
375+
box (AggregateKind::Adt(..) | AggregateKind::Tuple | AggregateKind::Array(..)),
366376
fields,
367377
) => {
368378
let target: utils::Place<'tcx> = (*target).into();
369379
for field in fields.iter() {
380+
tracing::info!("Field {:?}", field);
370381
let operand_place: utils::Place<'tcx> =
371382
if let Some(place) = field.place() {
372383
place.into()

src/borrows/region_projection_member.rs

+29
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,9 @@ use crate::utils::PlaceRepacker;
1111

1212
use super::borrow_pcg_edge::{BlockedNode, LocalNode};
1313
use super::edge_data::EdgeData;
14+
use super::region_projection::MaybeRemoteRegionProjectionBase;
1415
use super::{has_pcs_elem::HasPcsElems, region_projection::RegionProjection};
16+
use crate::rustc_interface::middle::ty;
1517
use crate::utils::json::ToJsonWithRepacker;
1618

1719
pub(crate) type RegionProjectionMemberInputs<'tcx> = SmallVec<[PCGNode<'tcx>; 8]>;
@@ -144,6 +146,33 @@ impl<'tcx> HasPcsElems<MaybeOldPlace<'tcx>> for RegionProjectionMember<'tcx> {
144146
}
145147

146148
impl<'tcx> RegionProjectionMember<'tcx> {
149+
pub(crate) fn is_toplevel(&self, repacker: PlaceRepacker<'_, 'tcx>) -> bool {
150+
match self.kind {
151+
RegionProjectionMemberKind::BorrowOutlives
152+
| RegionProjectionMemberKind::DerefBorrowOutlives => {
153+
match (self.inputs[0], self.outputs[0]) {
154+
(PCGNode::RegionProjection(rp1), PCGNode::RegionProjection(rp2)) => {
155+
match (rp1.place(), rp2.place()) {
156+
(
157+
MaybeRemoteRegionProjectionBase::Place(p1),
158+
MaybeOldPlace::Current { place: p2 },
159+
) => match (p1.ty(repacker).ty.kind(), p2.ty(repacker).ty.kind()) {
160+
(ty::TyKind::Ref(r1, ..), ty::TyKind::Ref(r2, ..)) => {
161+
rp1.region(repacker) == (*r1).into()
162+
&& rp2.region(repacker) == (*r2).into()
163+
}
164+
_ => false,
165+
},
166+
_ => false,
167+
}
168+
}
169+
_ => unreachable!(),
170+
}
171+
}
172+
_ => false,
173+
}
174+
}
175+
147176
/// Returns `true` iff the lifetime projections are mutable
148177
pub(crate) fn mutability(&self, repacker: PlaceRepacker<'_, 'tcx>) -> Mutability {
149178
let mut_values = self

src/visualization/graph_constructor.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ use crate::{
1919
use super::{dot_graph::DotSubgraph, Graph, GraphEdge, GraphNode, NodeId, NodeType};
2020
use crate::borrows::edge::abstraction::AbstractionType;
2121
use crate::borrows::edge::kind::BorrowPCGEdgeKind;
22-
use crate::rustc_interface::middle::ty::{self, TyCtxt};
22+
use crate::rustc_interface::middle::ty::TyCtxt;
2323
use crate::utils::place::maybe_old::MaybeOldPlace;
2424
use crate::utils::place::maybe_remote::MaybeRemotePlace;
2525
use crate::utils::place::remote::RemotePlace;
+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
fn foo() {
2+
let x = 1;
3+
let y = &&&x;
4+
let a = ***y;
5+
}
6+
7+
fn main(){
8+
9+
}

test-files/57_slice_ptr_elem_write.rs

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
fn main() {
2+
let mut x = 1;
3+
let y = [&mut x];
4+
*y[0] = 0;
5+
x;
6+
}

0 commit comments

Comments
 (0)