Bugfix

viperproject · Oct 11, 2023 · 050bdb2 · 050bdb2
1 parent 9e79e87
commit 050bdb2
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 10 deletions.
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
@@ -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(),
         }
     }
 

diff --git 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::<PathBuf>(),
     );
     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
@@ -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);
                 }
             }