fix: re-enable count_line

src/verus.rs

@@ -3,7 +3,7 @@ use indexmap::IndexMap;
 use memoize::memoize;
 use std::collections::{HashMap, HashSet};
 use std::ffi::OsStr;
-use std::fs::{self, File};
+use std::fs::{self, File, OpenOptions};
 use std::io::{BufRead, BufReader, IsTerminal, Read, Write};
 use std::path::{Path, PathBuf};
 use std::process::{Command, Stdio};
@@ -609,13 +609,146 @@ fn move_verus_log_files(crate_name: &str) {
     }
 }
 
-pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(), DynError> {
-    if options.count_line {
-        eprintln!("Error: --count-line is currently unsupported with cargo-verus");
-        // TODO: Re-enable this path once cargo-verus can produce the dep-info expected by Verus' line_count tool.
-        return Err("--count-line is currently unsupported with cargo-verus".into());
+fn dep_info_dirs(target_dir: &Path) -> Vec<PathBuf> {
+    let triple = VERIFICATION_RUST_TARGET;
+    [target_dir.join("verus-partial"), target_dir.to_path_buf()]
+        .into_iter()
+        .flat_map(|base| {
+            ["debug", "release"]
+                .into_iter()
+                .map(move |profile| base.join(triple).join(profile).join("deps"))
+        })
+        .collect()
+}
+
+fn dep_info_source_root(
+    dep_info: &Path,
+    target: &VerusTarget,
+    workspace_root: &Path,
+) -> Option<PathBuf> {
+    let first_line = BufReader::new(File::open(dep_info).ok()?)
+        .lines()
+        .next()?
+        .ok()?;
+    let target_file = target.file.canonicalize().ok()?;
+
+    for root in [workspace_root, target.dir.as_path()] {
+        if first_line
+            .split_whitespace()
+            .skip(1)
+            .map(|dependency| dependency.trim_end_matches('\\'))
+            .map(Path::new)
+            .map(|dependency| {
+                if dependency.is_absolute() {
+                    dependency.to_path_buf()
+                } else {
+                    root.join(dependency)
+                }
+            })
+            .filter_map(|dependency| dependency.canonicalize().ok())
+            .any(|dependency| dependency == target_file)
+        {
+            return Some(root.to_path_buf());
+        }
+    }
+
+    None
+}
+
+fn find_dep_info(target: &VerusTarget) -> Option<(PathBuf, PathBuf)> {
+    let target_dir = get_target_dir();
+    let workspace_root = get_workspace_root();
+
+    dep_info_dirs(&target_dir)
+        .into_iter()
+        .filter_map(|dir| fs::read_dir(dir).ok())
+        .flatten()
+        .filter_map(|entry| entry.ok())
+        .map(|entry| entry.path())
+        .filter(|path| path.extension() == Some(OsStr::new("d")))
+        .filter_map(|path| {
+            let source_root = dep_info_source_root(&path, target, &workspace_root)?;
+            let modified = path.metadata().ok()?.modified().ok()?;
+            Some((modified, path, source_root))
+        })
+        .max_by_key(|(modified, _, _)| *modified)
+        .map(|(_, path, source_root)| (path, source_root))
+}
+
+struct TemporaryDepInfo {
+    path: PathBuf,
+}
+
+impl TemporaryDepInfo {
+    fn copy_into(source: &Path, root: &Path, crate_name: &str) -> Result<Self, DynError> {
+        for suffix in 0..100 {
+            let path = root.join(format!(
+                ".dv-line-count-{}-{}-{}.d",
+                crate_name,
+                std::process::id(),
+                suffix
+            ));
+            match OpenOptions::new().write(true).create_new(true).open(&path) {
+                Ok(mut destination) => {
+                    let temporary_dep_info = Self { path };
+                    let mut source = File::open(source)?;
+                    std::io::copy(&mut source, &mut destination)?;
+                    return Ok(temporary_dep_info);
+                }
+                Err(error) if error.kind() == std::io::ErrorKind::AlreadyExists => continue,
+                Err(error) => return Err(error.into()),
+            }
+        }
+
+        Err(format!(
+            "failed to create a temporary dep-info file in {}",
+            root.display()
+        )
+        .into())
+    }
+}
+
+impl Drop for TemporaryDepInfo {
+    fn drop(&mut self) {
+        if let Err(error) = fs::remove_file(&self.path) {
+            warn!(
+                "Failed to remove temporary dep-info file {}: {}",
+                self.path.display(),
+                error
+            );
+        }
+    }
+}
+
+fn run_line_count(target: &VerusTarget) -> Result<(), DynError> {
+    let (dep_info, source_root) = find_dep_info(target).ok_or_else(|| {
+        format!(
+            "could not find cargo-verus dep-info for target {} under {}",
+            target.name,
+            get_target_dir().display()
+        )
+    })?;
+    let temporary_dep_info = TemporaryDepInfo::copy_into(&dep_info, &source_root, &target.name)?;
+    let line_count_dir = install::verus_dir().join("source/tools/line_count");
+
+    println!("Counting lines for {}", target.name);
+    let status = Command::new("cargo")
+        .current_dir(&line_count_dir)
+        .arg("run")
+        .arg("--release")
+        .arg("--")
+        .arg("--deps")
+        .arg(&temporary_dep_info.path)
+        .arg("-p")
+        .status()?;
+    if !status.success() {
+        return Err(format!("line_count failed for target {}", target.name).into());
     }
 
+    Ok(())
+}
+
+pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(), DynError> {
     let z3 = get_z3();
     let run = |target: Option<&VerusTarget>| -> Result<(), DynError> {
         let ts_start = Instant::now();
@@ -689,26 +822,15 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<()
         }
 
         if options.count_line {
-            let verus_root = install::verus_dir();
-            let line_count_dir = verus_root.join("source/tools/line_count");
-            let current_dir = std::env::current_dir()?;
-            let dependency_file = current_dir.join("lib.d");
-            std::env::set_current_dir(&line_count_dir)?;
-            let mut cargo_cmd = Command::new("cargo");
-            cargo_cmd
-                .arg("run")
-                .arg("--release")
-                .arg(&dependency_file)
-                .arg("-p");
-
-            println!(
-                "Counting lines for {}",
-                target.map(|t| t.name.as_str()).unwrap_or("workspace")
-            );
-            let line_count_result = cargo_cmd.status();
-            std::env::set_current_dir(current_dir)?;
-            line_count_result?;
-            fs::remove_file(&dependency_file)?;
+            let mut count_targets = match target {
+                Some(target) => vec![target.clone()],
+                None => verus_targets().into_values().collect(),
+            };
+            count_targets.sort_by(|left, right| left.name.cmp(&right.name));
+
+            for count_target in &count_targets {
+                run_line_count(count_target)?;
+            }
         }
         Ok(())
     };