Exclude closures defined in formula_fn from analysis and borrowck

src/analyze.rs

@@ -39,10 +39,16 @@ pub fn mir_borrowck_skip_formula_fn(
     local_def_id: rustc_span::def_id::LocalDefId,
 ) -> rustc_middle::query::queries::mir_borrowck::ProvidedValue {
     // TODO: unify impl with local_def::Analyzer
+    // if the def is closure defined in formula_fn
+    let root_def_id = tcx.typeck_root_def_id(local_def_id.to_def_id());
     let is_annotated_as_formula_fn = tcx
         .get_attrs_by_path(local_def_id.to_def_id(), &analyze::annot::formula_fn_path())
         .next()
-        .is_some();
+        .is_some()
+        || tcx
+            .get_attrs_by_path(root_def_id, &analyze::annot::formula_fn_path())
+            .next()
+            .is_some();
 
     if is_annotated_as_formula_fn {
         tracing::debug!(?local_def_id, "skipping borrow check for formula fn");

src/analyze/crate_.rs

@@ -100,6 +100,19 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             return;
         }
 
+        // skip analysis if the def is closure defined in skipped def
+        if let Some(root_local_def_id) = self
+            .tcx
+            .typeck_root_def_id(local_def_id.to_def_id())
+            .as_local()
+        {
+            if root_local_def_id != local_def_id && self.skip_analysis.contains(&root_local_def_id)
+            {
+                self.skip_analysis.insert(local_def_id);
+                return;
+            }
+        }
+
         let target_def_id = if analyzer.is_annotated_as_extern_spec_fn() {
             analyzer.extern_spec_fn_target_def_id()
         } else {

tests/ui/fail/annot_exists_formula_fn_mut.rs

@@ -0,0 +1,30 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[allow(unused_variables)]
+#[thrust::formula_fn]
+fn _thrust_requires_incr(m: thrust_models::model::Mut<i32>, x: i32) -> bool {
+    x > 0
+}
+
+#[allow(unused_variables)]
+#[thrust::formula_fn]
+fn _thrust_ensures_incr(result: (), m: thrust_models::model::Mut<i32>, x: i32) -> bool {
+    thrust_models::exists(|y: i32| !m == y && y > *m)
+}
+
+#[allow(path_statements)]
+fn incr(m: &mut i32, x: i32) {
+    #[thrust::requires_path]
+    _thrust_requires_incr;
+    #[thrust::ensures_path]
+    _thrust_ensures_incr;
+
+    *m -= x;
+}
+
+fn main() {
+    let mut a = 0;
+    incr(&mut a, 1);
+}

tests/ui/pass/annot_exists_formula_fn_mut.rs

@@ -0,0 +1,31 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+#[allow(unused_variables)]
+#[thrust::formula_fn]
+fn _thrust_requires_incr(m: thrust_models::model::Mut<i32>, x: i32) -> bool {
+    x > 0
+}
+
+#[allow(unused_variables)]
+#[thrust::formula_fn]
+fn _thrust_ensures_incr(result: (), m: thrust_models::model::Mut<i32>, x: i32) -> bool {
+    thrust_models::exists(|y: i32| !m == y && y > *m)
+}
+
+#[allow(path_statements)]
+fn incr(m: &mut i32, x: i32) {
+    #[thrust::requires_path]
+    _thrust_requires_incr;
+    #[thrust::ensures_path]
+    _thrust_ensures_incr;
+
+    *m += x;
+}
+
+fn main() {
+    let mut a = 0;
+    incr(&mut a, 1);
+    assert!(a > 0);
+}