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: Coupling Graph #1449

Draft
wants to merge 66 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
66 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
1af955e
Initial experiments with coupling graph
JonasAlaif Aug 22, 2023
1f9441e
Add merge op
JonasAlaif Sep 22, 2023
3d26e32
Almost done
JonasAlaif Sep 27, 2023
0900cef
Merge branch 'master' into free-pcs-engine
JonasAlaif Sep 27, 2023
491f95c
Merge branch 'master' into coupling-graph-engine
JonasAlaif Sep 27, 2023
5933a00
fmt
JonasAlaif Sep 27, 2023
496ebe1
Fix merge issues
JonasAlaif Sep 27, 2023
185a8be
Merge fixes
JonasAlaif Sep 27, 2023
66f7ea2
Clippy fixes
JonasAlaif Sep 27, 2023
16a944e
Add top crates test
JonasAlaif Sep 27, 2023
77326d4
Debug which method we're running on
JonasAlaif Sep 27, 2023
1a9102e
Change repetition tracking
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
be4f7db
Merge branch 'free-pcs-engine' into coupling-graph-engine
JonasAlaif Sep 28, 2023
fc4c881
Add tracing
JonasAlaif Sep 28, 2023
64e742d
Add loop detection analysis
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
509166f
Merge branch 'free-pcs-engine' into coupling-graph-engine
JonasAlaif Sep 28, 2023
0e5f84f
Merge
JonasAlaif Sep 28, 2023
7610848
Only one region per Node
JonasAlaif Sep 28, 2023
62f8e62
Fix `can_deinit` check
JonasAlaif Sep 28, 2023
17ed9fe
fmt
JonasAlaif Sep 29, 2023
452c317
Clean things up
JonasAlaif Sep 29, 2023
a0e1026
Rearrange things
JonasAlaif Sep 29, 2023
6b9d469
Disable printing and dumping when running under top crates
JonasAlaif Sep 29, 2023
d7e85d2
Small bugfixes
JonasAlaif Sep 29, 2023
b554699
Analysis done
JonasAlaif Oct 3, 2023
cda10d4
Remove outlives constraints uniqueness assumption
JonasAlaif Oct 3, 2023
2e47a27
fmt
JonasAlaif Oct 3, 2023
7e19cc7
Improve constant analysis
JonasAlaif Oct 9, 2023
9e79e87
Change constant lifetime analysis
JonasAlaif Oct 10, 2023
6bf38d0
Bugfix
JonasAlaif Oct 11, 2023
c485102
Merge branch 'free-pcs-engine' into coupling-graph-engine
JonasAlaif Oct 11, 2023
598ec91
Fix bug in `ConstantIndex` unpacking
JonasAlaif Oct 12, 2023
0ac0bd4
Ensure that we never expand a Write capability
JonasAlaif Oct 12, 2023
03649f3
fmt
JonasAlaif Oct 12, 2023
ec94390
Start combining the analyses
JonasAlaif Oct 17, 2023
29d695e
Bugfixes
JonasAlaif Oct 17, 2023
89ece29
Loop generalization, two-phase borrows and kill_many
JonasAlaif Oct 18, 2023
58d03fb
Bugfixes
JonasAlaif Oct 19, 2023
58fe3c5
Add weakens before write
JonasAlaif Oct 20, 2023
c700a96
Bugfix to support other capabilities
JonasAlaif Oct 25, 2023
741284e
Add pre and post distinction
JonasAlaif Oct 25, 2023
348623d
Update checker with new fpcs
JonasAlaif Oct 25, 2023
38116a1
fmt and clippy
JonasAlaif Nov 13, 2023
8ac71f4
Make top crates iterator
JonasAlaif Nov 13, 2023
bc36bd2
Disallow expanding through `Projection` at edges
JonasAlaif Nov 13, 2023
54b75fb
Update checker.rs
JonasAlaif Nov 27, 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
23 changes: 23 additions & 0 deletions .github/workflows/test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,29 @@ jobs:
- name: Run quick tests
run: python x.py test --all quick

top-crates:
runs-on: ubuntu-latest
env:
PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin
steps:
- name: Check out the repo
uses: actions/checkout@v3
- name: Set up Java
uses: actions/setup-java@v3
with:
java-version: '15'
distribution: 'zulu'
- name: Set up the environment
run: python x.py setup
- name: Cache cargo
uses: Swatinem/rust-cache@v2
with:
shared-key: "shared"
- name: Build with cargo
run: python x.py build --all
- name: Run quick tests
run: python x.py test --package mir-state-analysis --test top_crates -- top_crates --exact --nocapture

# Run a subset of the tests with the purification optimization enabled
# to ensure that we do not introduce regressions.
purification-tests:
Expand Down
50 changes: 50 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ members = [
"prusti-common",
"prusti-utils",
"tracing",
"mir-state-analysis",
"prusti-interface",
"prusti-viper",
"prusti-server",
Expand Down
12 changes: 8 additions & 4 deletions analysis/tests/utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,12 +31,16 @@ pub fn find_compiled_executable(name: &str) -> PathBuf {
}

pub fn find_sysroot() -> String {
// Taken from https://github.com/Manishearth/rust-clippy/pull/911.
let home = option_env!("RUSTUP_HOME").or(option_env!("MULTIRUST_HOME"));
let toolchain = option_env!("RUSTUP_TOOLCHAIN").or(option_env!("MULTIRUST_TOOLCHAIN"));
// Taken from https://github.com/rust-lang/rust-clippy/commit/f5db351a1d502cb65f8807ec2c84f44756099ef3.
let home = std::env::var("RUSTUP_HOME")
.or_else(|_| std::env::var("MULTIRUST_HOME"))
.ok();
let toolchain = std::env::var("RUSTUP_TOOLCHAIN")
.or_else(|_| std::env::var("MULTIRUST_TOOLCHAIN"))
.ok();
match (home, toolchain) {
(Some(home), Some(toolchain)) => format!("{home}/toolchains/{toolchain}"),
_ => option_env!("RUST_SYSROOT")
_ => std::env::var("RUST_SYSROOT")
.expect("need to specify RUST_SYSROOT env var or use rustup or multirust")
.to_owned(),
}
Expand Down
25 changes: 25 additions & 0 deletions mir-state-analysis/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
[package]
name = "mir-state-analysis"
version = "0.1.0"
authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
edition = "2021"

[dependencies]
derive_more = "0.99"
tracing = { path = "../tracing" }
prusti-rustc-interface = { path = "../prusti-rustc-interface" }
dot = "0.1"
smallvec = { version = "^1.11", features = ["union", "const_new"] }
# TODO: remove
prusti-interface = { path = "../prusti-interface" }
regex = "1"

[dev-dependencies]
reqwest = { version = "^0.11", features = ["blocking"] }
serde = "^1.0"
serde_derive = "^1.0"
serde_json = "^1.0"

[package.metadata.rust-analyzer]
# This crate uses #[feature(rustc_private)]
rustc_private = true
Loading
Loading