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

Prusti 2.0: Free PCS #1398

Open
wants to merge 36 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
36 commits
Select commit Hold shift + click to select a range
9a8e1f0
Start work on MicroMir
JonasAlaif Feb 23, 2023
9c967ed
More work on MicroMir
JonasAlaif Mar 1, 2023
d86eabb
More work on MicroMir
JonasAlaif Mar 6, 2023
aa67674
Clippy/fmt fix
JonasAlaif Mar 8, 2023
18a6a0e
Merge branch 'master' into free-pcs
JonasAlaif Apr 17, 2023
0a533ae
Switch to using rustc dataflow engine
JonasAlaif Apr 18, 2023
a64df48
Add results cursor
JonasAlaif Apr 18, 2023
d85ed76
Display repacks in graphviz
JonasAlaif Apr 18, 2023
b914d79
Add `ShallowExclusive` capability
JonasAlaif Apr 19, 2023
d176fb8
Update
JonasAlaif Apr 24, 2023
2f8fbba
Bugfix
JonasAlaif Apr 25, 2023
330e61a
More changes
JonasAlaif Apr 25, 2023
9cebf2c
Merge branch 'master' into free-pcs-engine
JonasAlaif Aug 22, 2023
adf559b
Merge update fixes
JonasAlaif Aug 22, 2023
0900cef
Merge branch 'master' into free-pcs-engine
JonasAlaif Sep 27, 2023
5933a00
fmt
JonasAlaif Sep 27, 2023
496ebe1
Fix merge issues
JonasAlaif Sep 27, 2023
66f7ea2
Clippy fixes
JonasAlaif Sep 27, 2023
362788c
Bugfix for shallow exclusive
JonasAlaif Sep 28, 2023
813c87f
Remove check
JonasAlaif Sep 28, 2023
55bd039
fmt
JonasAlaif Sep 28, 2023
135065c
Bugfix
JonasAlaif Sep 28, 2023
a7a892b
Fix `PlaceMention` triple
JonasAlaif Sep 28, 2023
878b7da
Merge branch 'master' into free-pcs-engine
JonasAlaif Sep 28, 2023
62f8e62
Fix `can_deinit` check
JonasAlaif Sep 28, 2023
17ed9fe
fmt
JonasAlaif Sep 29, 2023
210d37a
Fix bug in `ConstantIndex` unpacking
JonasAlaif Oct 12, 2023
4047beb
Ensure that we never expand a Write capability
JonasAlaif Oct 12, 2023
4467796
fmt
JonasAlaif Oct 12, 2023
8e4030c
Add weakens before write
JonasAlaif Oct 20, 2023
7e12a2e
Bugfix to support other capabilities
JonasAlaif Oct 25, 2023
786a22d
Add pre and post distinction
JonasAlaif Oct 25, 2023
87d41e8
Add `ty` utility function
JonasAlaif Oct 25, 2023
09dcd1e
fmt and clippy
JonasAlaif Nov 13, 2023
54651c9
Make top crates iterator
JonasAlaif Nov 13, 2023
b9ba878
Disallow expanding through `Projection` at edges
JonasAlaif Nov 13, 2023
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
Bugfix to support other capabilities
JonasAlaif committed Oct 25, 2023

Verified

This commit was signed with the committer’s verified signature.
snyk-bot Snyk bot
commit 7e12a2e78f772b3b8740acfc7a8cdb97c6ef9fb0
12 changes: 8 additions & 4 deletions mir-state-analysis/src/free_pcs/impl/update.rs
Original file line number Diff line number Diff line change
@@ -55,11 +55,15 @@ impl<'tcx> Fpcs<'_, 'tcx> {
let cp: &mut CapabilityProjections = self.summary[place.local].get_allocated_mut();
let ops = cp.repack(place, self.repacker);
self.repackings.extend(ops);
let kind = cp.insert(place, cap).unwrap();
let kind = cp[&place];
if cap.is_write() {
// Requires write should deinit an exclusive
cp.insert(place, cap);
if kind != cap {
self.repackings.push(RepackOp::Weaken(place, kind, cap));
}
};
assert!(kind >= cap);
if kind != cap {
self.repackings.push(RepackOp::Weaken(place, kind, cap));
}
}

pub(crate) fn ensures_unalloc(&mut self, local: Local) {