Pre/post-conditions annotations using Rust expressions

.gitignore

@@ -1 +1 @@
-/target
+target/

Cargo.toml

@@ -1,3 +1,7 @@
+[workspace]
+members = [".", "thrust-macros"]
+resolver = "2"
+
 [package]
 name = "thrust"
 version = "0.1.0"
@@ -18,6 +22,11 @@ name = "ui"
 harness = false
 
 [dependencies]
+# Workaround until thrust supports invocation via cargo: adding thrust-macros as
+# a dependency ensures cargo builds (and rebuilds) it alongside thrust. It is not
+# used as a proc-macro here; the dylib is loaded at runtime via --extern.
+thrust-macros = { path = "thrust-macros" }
+
 anyhow = "1.0.102"
 pretty = { version = "0.12.5", features = ["termcolor"] }
 tempfile = "3.27.0"

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 {

src/main.rs

@@ -66,8 +66,36 @@ impl Callbacks for CompilerCalls {
     }
 }
 
+fn thrust_macros_path() -> Option<std::path::PathBuf> {
+    let exe = std::env::current_exe().ok()?;
+    let dir = exe.parent()?;
+    // When thrust-macros is a cargo dependency it lands in deps/ with a hash
+    // suffix (e.g. libthrust_macros-<hash>.so), so check both locations.
+    let search_dirs = [dir.to_path_buf(), dir.join("deps")];
+    for search_dir in &search_dirs {
+        for ext in ["so", "dylib", "dll"] {
+            // First try the exact name (e.g. when built standalone).
+            let candidate = search_dir.join(format!("libthrust_macros.{ext}"));
+            if candidate.exists() {
+                return Some(candidate);
+            }
+            // Then scan for libthrust_macros-<hash>.<ext>.
+            if let Ok(entries) = std::fs::read_dir(search_dir) {
+                for entry in entries.flatten() {
+                    let name = entry.file_name();
+                    let name = name.to_string_lossy();
+                    if name.starts_with("libthrust_macros-") && name.ends_with(ext) {
+                        return Some(entry.path());
+                    }
+                }
+            }
+        }
+    }
+    None
+}
+
 pub fn main() {
-    let args = std::env::args().collect::<Vec<_>>();
+    let mut args = std::env::args().collect::<Vec<_>>();
 
     use tracing_subscriber::{filter::EnvFilter, prelude::*};
     tracing_subscriber::registry()
@@ -80,6 +108,14 @@ pub fn main() {
         )
         .init();
 
+    if let Some(path) = thrust_macros_path() {
+        args.push("--extern".to_owned());
+        args.push(format!("thrust_macros={}", path.display()));
+        tracing::debug!("linking thrust_macros from {}", path.display());
+    } else {
+        tracing::warn!("could not locate thrust_macros library");
+    }
+
     let code =
         rustc_driver::catch_with_exit_code(|| RunCompiler::new(&args, &mut CompilerCalls {}).run());
     std::process::exit(code);