Bugfix

Author: JonasAlaif

mir-state-analysis/src/coupling_graph/context/outlives_info/mod.rs

@@ -10,7 +10,7 @@ use prusti_rustc_interface::{
         borrow_set::BorrowData,
         consumers::{BorrowIndex, Borrows, OutlivesConstraint, PoloniusInput, RustcFacts},
     },
-    data_structures::fx::FxHashMap,
+    data_structures::fx::{FxHashMap, FxHashSet},
     dataflow::{Analysis, ResultsCursor},
     index::IndexVec,
     middle::{
@@ -30,7 +30,6 @@ pub struct OutlivesInfo<'tcx> {
     pub local_constraints: Vec<OutlivesConstraint<'tcx>>, // but with no location info
     pub type_ascription_constraints: Vec<OutlivesConstraint<'tcx>>,
     pub location_constraints: FxHashMap<Location, Vec<OutlivesConstraint<'tcx>>>,
-
     pub universal_constraints: Vec<(RegionVid, RegionVid)>,
 }
 
@@ -40,7 +39,8 @@ impl<'tcx> OutlivesInfo<'tcx> {
         facts2: &BorrowckFacts2<'tcx>,
         ri: &RegionInfo<'tcx>,
     ) -> Self {
-        let universal_constraints = input_facts.known_placeholder_subset.clone();
+        let mut universal_constraints =
+            FxHashSet::from_iter(input_facts.known_placeholder_subset.iter().copied());
 
         let mut universal_local_constraints = Vec::new();
         let mut local_constraints = Vec::new();
@@ -57,7 +57,8 @@ impl<'tcx> OutlivesInfo<'tcx> {
                 if ri.map.is_universal(constraint.sup) && ri.map.is_universal(constraint.sub) {
                     // Not sure why the `region_inference_context` can rarely contain inter-universal constraints,
                     // but we should already have all of these in `universal_constraints`.
-                    assert!(universal_constraints.contains(&(constraint.sup, constraint.sub)));
+                    // Except for even more rare situations...
+                    universal_constraints.insert((constraint.sup, constraint.sub));
                 } else {
                     universal_local_constraints.push(constraint);
                 }
@@ -72,7 +73,7 @@ impl<'tcx> OutlivesInfo<'tcx> {
             local_constraints,
             type_ascription_constraints,
             location_constraints,
-            universal_constraints,
+            universal_constraints: universal_constraints.into_iter().collect(),
         }
     }
 

mir-state-analysis/tests/top_crates.rs

@@ -63,8 +63,8 @@ fn run_on_crate(name: &str, version: &str) {
             .collect::<PathBuf>(),
     );
     println!("Running: {prusti:?}");
-    let exit = std::process::Command::new(prusti)
-        // .env("PRUSTI_TEST_FREE_PCS", "true")
+    let exit = std::process::Command::new(&prusti)
+        .env("PRUSTI_TEST_FREE_PCS", "true")
         .env("PRUSTI_TEST_COUPLING_GRAPH", "true")
         .env("PRUSTI_SKIP_UNSUPPORTED_FEATURES", "true")
         // .env("PRUSTI_LOG", "debug")

prusti/src/callbacks.rs

@@ -37,7 +37,7 @@ fn mir_borrowck<'tcx>(tcx: TyCtxt<'tcx>, def_id: LocalDefId) -> &BorrowCheckResu
     if !is_anon_const {
         let consumer_opts = if is_spec_fn(tcx, def_id.to_def_id())
             || config::no_verify()
-            || config::test_free_pcs()
+            || (config::test_free_pcs() && !config::test_coupling_graph())
         {
             consumers::ConsumerOptions::RegionInferenceContext
         } else if config::test_coupling_graph() {
@@ -172,7 +172,8 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls {
                         println!("Calculating FPCS for: {name} ({:?})", mir.span);
                         test_free_pcs(&mir, tcx);
                     }
-                } else if config::test_coupling_graph() {
+                }
+                if config::test_coupling_graph() {
                     for proc_id in env.get_annotated_procedures_and_types().0.iter() {
                         let mir = env.body.get_impure_fn_body_identity(proc_id.expect_local());
                         let facts = env
@@ -188,7 +189,8 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls {
                         println!("Calculating CG for: {name} ({:?})", mir.span);
                         test_coupling_graph(&*mir, &*facts, &*facts2, tcx, config::top_crates());
                     }
-                } else {
+                }
+                if !config::test_free_pcs() && !config::test_coupling_graph() {
                     verify(env, def_spec);
                 }
             }