Prusti 2.0: Free PCS

Cargo.toml

@@ -7,6 +7,7 @@ members = [
     "prusti-common",
     "prusti-utils",
     "tracing",
+    "mir-state-analysis",
     "prusti-interface",
     "prusti-viper",
     "prusti-server",

analysis/tests/utils.rs

@@ -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(),
     }

mir-state-analysis/Cargo.toml

@@ -0,0 +1,20 @@
+[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" }
+
+[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

mir-state-analysis/src/free_pcs/check/checker.rs

@@ -0,0 +1,202 @@
+// © 2023, ETH Zurich
+//
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+
+use prusti_rustc_interface::{
+    data_structures::fx::FxHashMap,
+    middle::mir::{visit::Visitor, Location, ProjectionElem},
+};
+
+use crate::{
+    free_pcs::{
+        CapabilityKind, CapabilityLocal, CapabilitySummary, Fpcs, FreePcsAnalysis, RepackOp,
+    },
+    utils::PlaceRepacker,
+};
+
+use super::consistency::CapabilityConistency;
+
+pub(crate) fn check(mut cursor: FreePcsAnalysis<'_, '_>) {
+    let rp = cursor.repacker();
+    let body = rp.body();
+    for (block, data) in body.basic_blocks.iter_enumerated() {
+        cursor.analysis_for_bb(block);
+        let mut fpcs = Fpcs {
+            summary: cursor.initial_state().clone(),
+            apply_pre_effect: true,
+            bottom: false,
+            repackings: Vec::new(),
+            repacker: rp,
+        };
+        // Consistency
+        fpcs.summary.consistency_check(rp);
+        for (statement_index, stmt) in data.statements.iter().enumerate() {
+            let loc = Location {
+                block,
+                statement_index,
+            };
+            let fpcs_after = cursor.next(loc);
+            assert_eq!(fpcs_after.location, loc);
+            // Repacks
+            for &op in &fpcs_after.repacks_middle {
+                op.update_free(&mut fpcs.summary, data.is_cleanup, true, rp);
+            }
+            // Consistency
+            fpcs.summary.consistency_check(rp);
+            // Statement pre
+            assert!(fpcs.repackings.is_empty());
+            fpcs.apply_pre_effect = true;
+            fpcs.visit_statement(stmt, loc);
+            assert!(fpcs.repackings.is_empty());
+
+            // Repacks
+            for op in fpcs_after.repacks {
+                op.update_free(&mut fpcs.summary, data.is_cleanup, true, rp);
+            }
+            // Statement post
+            fpcs.apply_pre_effect = false;
+            fpcs.visit_statement(stmt, loc);
+            assert!(fpcs.repackings.is_empty());
+            // Consistency
+            fpcs.summary.consistency_check(rp);
+        }
+        let loc = Location {
+            block,
+            statement_index: data.statements.len(),
+        };
+        let fpcs_after = cursor.next(loc);
+        assert_eq!(fpcs_after.location, loc);
+        // Repacks
+        for op in fpcs_after.repacks_middle {
+            op.update_free(&mut fpcs.summary, data.is_cleanup, true, rp);
+        }
+        // Consistency
+        fpcs.summary.consistency_check(rp);
+        // Statement pre
+        assert!(fpcs.repackings.is_empty());
+        fpcs.apply_pre_effect = true;
+        fpcs.visit_terminator(data.terminator(), loc);
+        assert!(fpcs.repackings.is_empty());
+
+        // Repacks
+        for op in fpcs_after.repacks {
+            op.update_free(&mut fpcs.summary, data.is_cleanup, true, rp);
+        }
+        // Statement post
+        fpcs.apply_pre_effect = false;
+        fpcs.visit_terminator(data.terminator(), loc);
+        assert!(fpcs.repackings.is_empty());
+        // Consistency
+        fpcs.summary.consistency_check(rp);
+        assert_eq!(fpcs.summary, fpcs_after.state);
+
+        let fpcs_end = cursor.terminator();
+
+        for succ in fpcs_end.succs {
+            // Repacks
+            let mut from = fpcs.clone();
+            for op in succ.repacks {
+                op.update_free(
+                    &mut from.summary,
+                    body.basic_blocks[succ.location.block].is_cleanup,
+                    false,
+                    rp,
+                );
+            }
+            assert_eq!(from.summary, succ.state);
+        }
+    }
+}
+
+impl<'tcx> RepackOp<'tcx> {
+    #[tracing::instrument(level = "debug", skip(rp))]
+    fn update_free(
+        self,
+        state: &mut CapabilitySummary<'tcx>,
+        is_cleanup: bool,
+        can_downcast: bool,
+        rp: PlaceRepacker<'_, 'tcx>,
+    ) {
+        match self {
+            RepackOp::StorageDead(local) => {
+                let curr_state = state[local].get_allocated_mut();
+                assert_eq!(curr_state.len(), 1);
+                assert!(
+                    curr_state.contains_key(&local.into()),
+                    "{self:?}, {curr_state:?}"
+                );
+                assert_eq!(curr_state[&local.into()], CapabilityKind::Write);
+                state[local] = CapabilityLocal::Unallocated;
+            }
+            RepackOp::IgnoreStorageDead(local) => {
+                assert_eq!(state[local], CapabilityLocal::Unallocated);
+                // Add write permission so that the `mir::StatementKind::StorageDead` can
+                // deallocate without producing any repacks, which would cause the
+                // `assert!(fpcs.repackings.is_empty());` above to fail.
+                state[local] = CapabilityLocal::new(local, CapabilityKind::Write);
+            }
+            RepackOp::Weaken(place, from, to) => {
+                assert!(from >= to, "{self:?}");
+                let curr_state = state[place.local].get_allocated_mut();
+                let old = curr_state.insert(place, to);
+                assert_eq!(old, Some(from), "{self:?}, {curr_state:?}");
+            }
+            RepackOp::Expand(place, guide, kind) => {
+                assert_eq!(kind, CapabilityKind::Exclusive, "{self:?}");
+                assert!(place.is_prefix_exact(guide), "{self:?}");
+                assert!(
+                    can_downcast
+                        || !matches!(
+                            guide.projection.last().unwrap(),
+                            ProjectionElem::Downcast(..)
+                        ),
+                    "{self:?}"
+                );
+                let curr_state = state[place.local].get_allocated_mut();
+                assert_eq!(
+                    curr_state.remove(&place),
+                    Some(kind),
+                    "{self:?} ({curr_state:?})"
+                );
+
+                let (p, others, _) = place.expand_one_level(guide, rp);
+                curr_state.insert(p, kind);
+                curr_state.extend(others.into_iter().map(|p| (p, kind)));
+            }
+            RepackOp::Collapse(place, guide, kind) => {
+                assert_ne!(kind, CapabilityKind::ShallowExclusive, "{self:?}");
+                assert!(place.is_prefix_exact(guide), "{self:?}");
+                let curr_state = state[place.local].get_allocated_mut();
+                let mut removed = curr_state
+                    .extract_if(|p, _| place.related_to(*p))
+                    .collect::<FxHashMap<_, _>>();
+
+                let (p, mut others, _) = place.expand_one_level(guide, rp);
+                others.push(p);
+                for other in others {
+                    assert_eq!(removed.remove(&other), Some(kind), "{self:?}");
+                }
+                assert!(removed.is_empty(), "{self:?}, {removed:?}");
+                let old = curr_state.insert(place, kind);
+                assert_eq!(old, None);
+            }
+            RepackOp::DerefShallowInit(place, guide) => {
+                assert!(place.is_prefix_exact(guide), "{self:?}");
+                assert_eq!(*guide.projection.last().unwrap(), ProjectionElem::Deref);
+                let curr_state = state[place.local].get_allocated_mut();
+                assert_eq!(
+                    curr_state.remove(&place),
+                    Some(CapabilityKind::ShallowExclusive),
+                    "{self:?} ({curr_state:?})"
+                );
+
+                let (p, others, pkind) = place.expand_one_level(guide, rp);
+                assert!(pkind.is_box());
+                curr_state.insert(p, CapabilityKind::Write);
+                assert!(others.is_empty());
+            }
+        }
+    }
+}

mir-state-analysis/src/free_pcs/check/consistency.rs

@@ -0,0 +1,58 @@
+// © 2023, ETH Zurich
+//
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+
+use crate::{
+    free_pcs::{CapabilityKind, CapabilityLocal, CapabilityProjections, Summary},
+    utils::{Place, PlaceRepacker},
+};
+
+pub trait CapabilityConistency<'tcx> {
+    fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>);
+}
+
+impl<'tcx, T: CapabilityConistency<'tcx>> CapabilityConistency<'tcx> for Summary<T> {
+    fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>) {
+        for p in self.iter() {
+            p.consistency_check(repacker)
+        }
+    }
+}
+
+impl<'tcx> CapabilityConistency<'tcx> for CapabilityLocal<'tcx> {
+    fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>) {
+        match self {
+            CapabilityLocal::Unallocated => {}
+            CapabilityLocal::Allocated(cp) => cp.consistency_check(repacker),
+        }
+    }
+}
+
+impl<'tcx> CapabilityConistency<'tcx> for CapabilityProjections<'tcx> {
+    fn consistency_check(&self, repacker: PlaceRepacker<'_, 'tcx>) {
+        // All keys unrelated to each other
+        let keys = self.keys().copied().collect::<Vec<_>>();
+        for (i, p1) in keys.iter().enumerate() {
+            for p2 in keys[i + 1..].iter() {
+                assert!(!p1.related_to(*p2), "{p1:?} {p2:?}",);
+            }
+            // Cannot be inside of uninitialized pointers.
+            if !p1.can_deinit(repacker) {
+                assert!(matches!(self[p1], CapabilityKind::Exclusive), "{self:?}");
+            }
+            // Cannot have Read or None here
+            assert!(self[p1] >= CapabilityKind::Write);
+            // Can only have `ShallowExclusive` for box typed places
+            if self[p1].is_shallow_exclusive() {
+                assert!(p1.ty(repacker).ty.is_box());
+            }
+        }
+        // Can always pack up to the root
+        let root: Place = self.get_local().into();
+        let mut keys = self.keys().copied().collect();
+        root.collapse(&mut keys, repacker);
+        assert!(keys.is_empty());
+    }
+}