diff --git a/mir-state-analysis/src/coupling_graph/context/outlives_info/mod.rs b/mir-state-analysis/src/coupling_graph/context/outlives_info/mod.rs index a07133b408e..2906e77c377 100644 --- a/mir-state-analysis/src/coupling_graph/context/outlives_info/mod.rs +++ b/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>, // but with no location info pub type_ascription_constraints: Vec>, pub location_constraints: FxHashMap>>, - 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(), } } diff --git a/mir-state-analysis/tests/top_crates.rs b/mir-state-analysis/tests/top_crates.rs index c20053d2382..4f146573846 100644 --- a/mir-state-analysis/tests/top_crates.rs +++ b/mir-state-analysis/tests/top_crates.rs @@ -63,9 +63,10 @@ fn run_on_crate(name: &str, version: &str) { .collect::(), ); println!("Running: {prusti:?}"); - let exit = std::process::Command::new(prusti) - // .env("PRUSTI_TEST_FREE_PCS", "true") - .env("PRUSTI_TEST_COUPLING_GRAPH", "true") + + // FreePCS + let exit = std::process::Command::new(&prusti) + .env("PRUSTI_TEST_FREE_PCS", "true") .env("PRUSTI_SKIP_UNSUPPORTED_FEATURES", "true") // .env("PRUSTI_LOG", "debug") .env("PRUSTI_NO_VERIFY_DEPS", "true") @@ -75,6 +76,26 @@ fn run_on_crate(name: &str, version: &str) { .status() .unwrap(); assert!(exit.success()); + + // cargo clean + let exit = std::process::Command::new("cargo") + .arg("clean") + .current_dir(&dirname) + .status() + .unwrap(); + assert!(exit.success()); + + // Coupling Graph + let exit = std::process::Command::new(&prusti) + .env("PRUSTI_TEST_COUPLING_GRAPH", "true") + .env("PRUSTI_SKIP_UNSUPPORTED_FEATURES", "true") + .env("PRUSTI_NO_VERIFY_DEPS", "true") + .env("PRUSTI_CAP_LINTS", "allow") + .env("PRUSTI_TOP_CRATES", "true") + .current_dir(&dirname) + .status() + .unwrap(); + assert!(exit.success()); // std::fs::remove_dir_all(dirname).unwrap(); } diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index d7323730b05..cf7e44ac201 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -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); } }