Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make compatible with earlier rust versions + mutation testing #23

Open
wants to merge 103 commits into
base: zgrannan/next3
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
103 commits
Select commit Hold shift + click to select a range
32ed356
WIP
zgrannan Feb 28, 2025
e808ec4
WIP
zgrannan Feb 28, 2025
f4f417b
WIP
zgrannan Feb 28, 2025
c569eb2
Fix clippy
zgrannan Feb 28, 2025
cfd3d8e
fix project deeper
zgrannan Feb 28, 2025
9476b5b
Fix test
zgrannan Feb 28, 2025
0561a67
move edge
zgrannan Feb 28, 2025
2a2cb30
rename
zgrannan Feb 28, 2025
c32b5a9
fix a small bug
zgrannan Feb 28, 2025
95d4243
Fix some bugs
zgrannan Feb 28, 2025
aaf2f16
fix a permissions issue
zgrannan Feb 28, 2025
8fcfbf1
WIP
zgrannan Mar 3, 2025
959bbb6
WIP
zgrannan Mar 3, 2025
c5eb584
WIP
zgrannan Mar 3, 2025
93d1e03
Finish some refactoring
zgrannan Mar 3, 2025
4425ace
Change representation of abstraction edges
zgrannan Mar 3, 2025
70e1f9b
Update bench results
zgrannan Mar 3, 2025
6017ad1
WIP
zgrannan Mar 4, 2025
84c8d36
WIP
zgrannan Mar 4, 2025
ddd85e8
Very large refactoring
zgrannan Mar 4, 2025
8d3fe0c
More benchmark
zgrannan Mar 4, 2025
58c3311
WIP
zgrannan Mar 5, 2025
b8ef93f
WIP
zgrannan Mar 6, 2025
43a3fe4
working
zgrannan Mar 6, 2025
09b2851
Make some more changes
zgrannan Mar 6, 2025
6d92ac3
WIP
zgrannan Mar 7, 2025
023a6e7
some fixes
zgrannan Mar 7, 2025
bd24e52
Update benchmark results
zgrannan Mar 7, 2025
a7d7935
Make things slightly more lenient
zgrannan Mar 7, 2025
571ca37
Add a testing heuristic
zgrannan Mar 7, 2025
d46f976
Much better loop logic
zgrannan Mar 8, 2025
f3ba27a
ring doesn't compile for some reason
zgrannan Mar 8, 2025
64b3ee8
ring doesn't compile for some reason
zgrannan Mar 8, 2025
69db5e4
WIP
zgrannan Mar 8, 2025
3b6e695
Fix a bug
zgrannan Mar 8, 2025
2d80d04
Prepare for generated top-crates log
zgrannan Mar 9, 2025
d2e33da
Try allowing more casts
zgrannan Mar 10, 2025
1bd8ea5
WIP
zgrannan Mar 10, 2025
99c93c6
Fix a bug
zgrannan Mar 10, 2025
d9e8d06
WIP
zgrannan Mar 11, 2025
510e9f6
pub more things I need
jaspergeer Mar 11, 2025
0eb63f4
Corrections based on Markus's examples
zgrannan Mar 11, 2025
f6da1b1
More fixes
zgrannan Mar 11, 2025
4ed35b6
Add an annotation
zgrannan Mar 11, 2025
8481389
WIP
zgrannan Mar 12, 2025
6cdd8a7
WIP
zgrannan Mar 12, 2025
46d2733
WIP
zgrannan Mar 12, 2025
f55475c
Update
zgrannan Mar 12, 2025
32d6ab5
Some fixes for loops and closures
zgrannan Mar 12, 2025
e27bc00
Add parallelism to top_crates
zgrannan Mar 12, 2025
3a71569
Fix bug
zgrannan Mar 13, 2025
c5b9202
Update benchmarks
zgrannan Mar 13, 2025
fc2de6d
Lock crates used for testing
zgrannan Mar 13, 2025
f31f571
remove build.rs
zgrannan Mar 13, 2025
bdd2146
WIP
zgrannan Mar 14, 2025
870fe8d
Two-phase borrows
zgrannan Mar 14, 2025
d6bd313
Appease clippy
zgrannan Mar 14, 2025
d494c1c
Polonius fixes
zgrannan Mar 14, 2025
c5dc61c
No capabilities on region projections
zgrannan Mar 14, 2025
3b9b9c6
Use dyn
zgrannan Mar 15, 2025
3e79b1a
Fix liveness computation for RP graph
zgrannan Mar 15, 2025
be168b1
Support for havocing of nested references in fn calls
zgrannan Mar 16, 2025
d5a0e03
Render alias edges
zgrannan Mar 16, 2025
847f086
Graph rendering improvements
zgrannan Mar 16, 2025
210bcf9
Support an additional case
zgrannan Mar 17, 2025
fcee230
another case
zgrannan Mar 17, 2025
3858593
Fix dotgraph tooltip
zgrannan Mar 17, 2025
6459a50
Small stuff
zgrannan Mar 17, 2025
fe89a48
Fix visualization
zgrannan Mar 17, 2025
a36d5d2
pub things I need, make compatible with earlier rust versions
jaspergeer Mar 17, 2025
ba37052
Merge branch 'viperproject:zgrannan/next3' into zgrannan/next3
jaspergeer Mar 17, 2025
edf505f
minor changes
jaspergeer Mar 17, 2025
812827c
Make two required fields public
JonasAlaif Mar 21, 2025
e8a633e
Add entry BorrowsState to PcgSuccessor
JonasAlaif Mar 21, 2025
6b48112
add additional test
zgrannan Mar 19, 2025
e35e789
cleanup
zgrannan Mar 20, 2025
30e5c61
Add a fix for loops
zgrannan Mar 21, 2025
c7e5883
Fix for polonius
zgrannan Mar 21, 2025
87a6c7d
loop fixes
zgrannan Mar 22, 2025
94e45d7
update benchmarks
zgrannan Mar 22, 2025
e01c35d
typecheck only version for comparison
zgrannan Mar 23, 2025
f9bd0ed
Save cached lockfiles
zgrannan Mar 23, 2025
1b1297a
Add all the lockfiles
zgrannan Mar 23, 2025
4f33d49
WIP
zgrannan Mar 24, 2025
4eb1885
Try not merging sccs
zgrannan Mar 24, 2025
4ca2d56
Try not merging sccs
zgrannan Mar 24, 2025
a1c3b00
ignore crate
zgrannan Mar 24, 2025
03589fc
loop fix
zgrannan Mar 24, 2025
0ef5006
WIP
zgrannan Mar 24, 2025
e7791e0
CI fixes
zgrannan Mar 24, 2025
c1b3699
CI fixes
zgrannan Mar 24, 2025
5e5c695
Disable validity checks on this crate for now
zgrannan Mar 24, 2025
b6fb4bd
WIP
zgrannan Mar 24, 2025
c37ef6e
Fix Jonas's example
zgrannan Mar 24, 2025
f0091a0
Mostly fix visualization
zgrannan Mar 24, 2025
8a11cca
Maybe improvements for rpa construction
zgrannan Mar 25, 2025
436618f
Fix issues Jasper identified
zgrannan Mar 25, 2025
cd40e14
Performance improvements for serde_derive
zgrannan Mar 25, 2025
0e75d0c
pub things I need, make compatible with earlier rust versions
jaspergeer Mar 17, 2025
f768efc
pub a thing
jaspergeer Mar 24, 2025
4b6de10
pub
jaspergeer Mar 25, 2025
1076ec6
FIXES
jaspergeer Mar 25, 2025
2acb6c0
oops actually finish merge
jaspergeer Mar 25, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Make some more changes
  • Loading branch information
zgrannan committed Mar 6, 2025
commit 09b2851a70e8f3017c7c5b9ab6f28d66e74d98b3
2 changes: 1 addition & 1 deletion src/borrow_pcg/action/actions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ impl<'tcx> BorrowPCGActions<'tcx> {
..
},
..
} => Some(Conditioned::new(edge.clone(), conditions.clone())),
} => Some(Conditioned::new(*edge, conditions.clone())),
_ => None,
})
.collect()
Expand Down
2 changes: 1 addition & 1 deletion src/borrow_pcg/domain.rs
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ impl<'mir, 'tcx> BorrowsDomain<'mir, 'tcx> {
fn introduce_initial_borrows(&mut self, local: Local) {
let local_decl = &self.repacker.body().local_decls[local];
let arg_place: Place<'tcx> = local.into();
if let ty::TyKind::Ref(region, _, mutability) = local_decl.ty.kind() {
if let ty::TyKind::Ref(_, _, mutability) = local_decl.ty.kind() {
let entry_state = Rc::<BorrowsState<'tcx>>::make_mut(&mut self.data.entry_state);
assert!(entry_state.set_capability(
MaybeRemotePlace::place_assigned_to_local(local).into(),
Expand Down
119 changes: 0 additions & 119 deletions src/borrow_pcg/edge/block.rs

This file was deleted.

8 changes: 4 additions & 4 deletions src/borrow_pcg/edge/borrow.rs
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ impl<'tcx> EdgeData<'tcx> for RemoteBorrow<'tcx> {
}
}

impl<'tcx> RemoteBorrow<'tcx> {
impl RemoteBorrow<'_> {
pub(crate) fn new(local: mir::Local) -> Self {
Self {
local,
Expand Down Expand Up @@ -156,7 +156,7 @@ impl<'tcx> BorrowEdge<'tcx> {
) -> RegionProjection<'tcx, MaybeOldPlace<'tcx>> {
match self {
BorrowEdge::Local(borrow) => borrow.assigned_region_projection(repacker),
BorrowEdge::Remote(borrow) => borrow.assigned_region_projection(repacker).into(),
BorrowEdge::Remote(borrow) => borrow.assigned_region_projection(repacker),
}
}

Expand All @@ -170,14 +170,14 @@ impl<'tcx> BorrowEdge<'tcx> {
pub fn deref_place(&self, repacker: PlaceRepacker<'_, 'tcx>) -> MaybeOldPlace<'tcx> {
match self {
BorrowEdge::Local(borrow) => borrow.deref_place(repacker),
BorrowEdge::Remote(borrow) => borrow.deref_place(repacker).into(),
BorrowEdge::Remote(borrow) => borrow.deref_place(repacker),
}
}

pub(crate) fn assigned_ref(&self) -> MaybeOldPlace<'tcx> {
match self {
BorrowEdge::Local(borrow) => borrow.assigned_ref,
BorrowEdge::Remote(remote) => remote.assigned_ref().into(),
BorrowEdge::Remote(remote) => remote.assigned_ref()
}
}
}
Expand Down
1 change: 0 additions & 1 deletion src/borrow_pcg/edge/mod.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
pub mod abstraction;
pub mod block;
pub mod borrow;
pub mod kind;
pub mod outlives;
Expand Down
5 changes: 5 additions & 0 deletions src/borrow_pcg/edge/region_projection_member.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ use crate::{
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub(crate) enum RpMemberDirection {
PlaceOutlivesRegion,
#[allow(dead_code)]
RegionOutlivesPlace,
}

Expand Down Expand Up @@ -78,6 +79,10 @@ impl<'tcx> RegionProjectionMember<'tcx> {
}
}
}

pub(crate) fn direction(&self) -> RpMemberDirection {
self.direction
}
}

impl<'tcx> EdgeData<'tcx> for RegionProjectionMember<'tcx> {
Expand Down
2 changes: 1 addition & 1 deletion src/borrow_pcg/state/obtain.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use crate::borrow_pcg::unblock_graph::UnblockGraph;
use crate::combined_pcs::{PCGError, PCGNodeLike};
use crate::free_pcs::CapabilityKind;
use crate::rustc_interface::middle::mir::{BorrowKind, Location, MutBorrowKind};
use crate::rustc_interface::middle::ty::{Mutability};
use crate::rustc_interface::middle::ty::Mutability;
use crate::utils::maybe_old::MaybeOldPlace;
use crate::utils::{Place, PlaceRepacker};
use crate::visualization::dot_graph::DotGraph;
Expand Down
2 changes: 1 addition & 1 deletion src/utils/place/maybe_old.rs
Original file line number Diff line number Diff line change
Expand Up @@ -220,7 +220,7 @@ impl<'tcx> MaybeOldPlace<'tcx> {
) -> Option<RegionProjection<'tcx, Self>> {
self.place()
.base_region_projection(repacker)
.map(|rp| rp.set_base((*self).into(), repacker))
.map(|rp| rp.set_base(*self, repacker))
}

pub(crate) fn is_owned(&self, repacker: PlaceRepacker<'_, 'tcx>) -> bool {
Expand Down
12 changes: 1 addition & 11 deletions src/utils/place/remote.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ use crate::borrow_pcg::region_projection::{
use crate::borrow_pcg::visitor::extract_regions;
use crate::combined_pcs::{PCGNode, PCGNodeLike};
use crate::rustc_interface::index::IndexVec;
use crate::rustc_interface::middle::{mir, ty::TyCtxt};
use crate::rustc_interface::middle::mir;
use crate::utils::display::DisplayWithRepacker;
use crate::utils::json::ToJsonWithRepacker;
use crate::utils::validity::HasValidityCheck;
Expand All @@ -15,16 +15,6 @@ pub struct RemotePlace {
pub(crate) local: mir::Local,
}

impl RemotePlace {
pub(crate) fn deref_place<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Place<'tcx> {
let place: Place<'_> = self.local.into();
place
.0
.project_deeper(&[mir::ProjectionElem::Deref], tcx)
.into()
}
}

impl<'tcx> ToJsonWithRepacker<'tcx> for RemotePlace {
fn to_json(&self, _repacker: PlaceRepacker<'_, 'tcx>) -> serde_json::Value {
todo!()
Expand Down
10 changes: 9 additions & 1 deletion src/visualization/graph_constructor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -368,7 +368,15 @@ trait PlaceGrapher<'mir, 'tcx: 'mir> {
kind: format!("{}", member.kind),
});
}
BorrowPCGEdgeKind::RegionProjectionMember(region_projection_member) => todo!(),
BorrowPCGEdgeKind::RegionProjectionMember(member) => {
let input_node = self.insert_pcg_node(member.blocked_node());
let output_node = self.insert_local_node(member.blocked_by_node(self.repacker()));
self.constructor().edges.insert(GraphEdge::Block {
source: input_node,
target: output_node,
kind: format!("{:?}", member.direction()),
});
}
}
}
}
Expand Down
Loading