From c714230dd8999e60a42f5a3cc4909a8b388a1790 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= <jonas.fiala@inf.ethz.ch>
Date: Wed, 11 Oct 2023 14:22:38 +0200
Subject: [PATCH] Bugfix

---
 .../src/coupling_graph/context/outlives_info/mod.rs   | 11 ++++++-----
 mir-state-analysis/tests/top_crates.rs                |  4 ++--
 prusti/src/callbacks.rs                               |  6 ++++--
 3 files changed, 12 insertions(+), 9 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
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<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
index c20053d2382..be0e664f38a 100644
--- a/mir-state-analysis/tests/top_crates.rs
+++ b/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")
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);
                 }
             }