From d94e63e43a3d3cf211e49a166a22e85b2ca0e3d5 Mon Sep 17 00:00:00 2001
From: Zack Grannan <zgrannan@protonmail.com>
Date: Fri, 1 Dec 2023 11:43:07 -0800
Subject: [PATCH] Put stuff in the right spots

---
 prusti-contracts-build/build.rs | 32 +++++++++++++++++++-------------
 prusti-utils/src/launch/mod.rs  | 12 ++++++------
 2 files changed, 25 insertions(+), 19 deletions(-)

diff --git a/prusti-contracts-build/build.rs b/prusti-contracts-build/build.rs
index aa6d88f8756..71fdac4fa7c 100644
--- a/prusti-contracts-build/build.rs
+++ b/prusti-contracts-build/build.rs
@@ -1,6 +1,16 @@
 use std::{path::PathBuf, process::Command};
 
-use prusti_utils::launch::get_prusti_contracts_build_destination_dir;
+use prusti_utils::launch::get_prusti_contracts_build_target_dir;
+
+fn executable_name(name: &str) -> String {
+    #[cfg(windows)]
+    let name = format!("{}.exe", name);
+
+    #[cfg(not(windows))]
+    let name = name.to_string();
+
+    name
+}
 
 fn main() {
     // Rerun if running with e.g. cargo clippy
@@ -16,30 +26,26 @@ fn main() {
     let target: PathBuf = ["..", "target"].iter().collect();
     force_reexport_specs(target.join("verify").as_path());
 
-    let bin_dir = get_prusti_contracts_build_destination_dir(&target);
-
+    let target = get_prusti_contracts_build_target_dir(&target);
+    let bin_dir = target.join("bin");
     std::fs::create_dir_all(&bin_dir).unwrap();
 
+    // Copies all files into `bin_dir`. `cargo_prusti` cannot be run directly
+    // from std::env::var("CARGO_BIN_FILE_PRUSTI_LAUNCH_cargo-prusti")
+    // because it requires `prusti-rustc` and `prusti-driver` to be in the same
+    // path.
     for (krate, file) in [
         ("PRUSTI_LAUNCH", "cargo-prusti"),
         ("PRUSTI_LAUNCH", "prusti-rustc"),
         ("PRUSTI", "prusti-driver"),
     ] {
         let file_from = std::env::var(format!("CARGO_BIN_FILE_{krate}_{file}")).unwrap();
-        let file_to = &format!("{file}{}", if cfg!(windows) { ".exe" } else { "" });
+        let file_to = executable_name(file);
         let file_to = bin_dir.join(file_to);
         std::fs::copy(file_from, file_to).unwrap();
     }
 
-    // Run `cargo-prusti`
-    let cargo_prusti = format!("cargo-prusti{}", if cfg!(windows) { ".exe" } else { "" });
-    let cargo_prusti = bin_dir.join(cargo_prusti);
-
-    // In theory we should build to here (i.e. set `CARGO_TARGET_DIR` to this),
-    // but this is hard to find for linking. So instead build to the `prusti-contracts` dir.
-    // let out_dir = std::env::var("OUT_DIR").unwrap();
-    // println!("cargo:warning=out_dir: {}", out_dir);
-
+    let cargo_prusti = bin_dir.join(executable_name("cargo-prusti"));
     let mut cmd = Command::new(cargo_prusti);
     cmd.env("CARGO_TARGET_DIR", target.as_os_str());
     cmd.current_dir(&prusti_contracts);
diff --git a/prusti-utils/src/launch/mod.rs b/prusti-utils/src/launch/mod.rs
index e0a5cb79f3b..51ed671b713 100644
--- a/prusti-utils/src/launch/mod.rs
+++ b/prusti-utils/src/launch/mod.rs
@@ -43,9 +43,8 @@ pub fn get_target_dir(exe_dir: &Path) -> PathBuf {
     root_dir.to_path_buf()
 }
 
-pub fn get_prusti_contracts_build_destination_dir(target_dir: &Path) -> PathBuf {
-    let target_dir = target_dir.join("prusti-contracts");
-    target_dir.join("verify").join(BUILD_MODE)
+pub fn get_prusti_contracts_build_target_dir(target_dir: &Path) -> PathBuf {
+    target_dir.join("prusti-contracts").join(BUILD_MODE)
 }
 
 pub fn get_prusti_contracts_dir(exe_dir: &Path) -> Option<PathBuf> {
@@ -54,10 +53,11 @@ pub fn get_prusti_contracts_dir(exe_dir: &Path) -> Option<PathBuf> {
     let target_dir = get_target_dir(exe_dir);
     let candidates = [
         // Libraries in the Prusti artifact will show up here
-        get_prusti_contracts_build_destination_dir(&target_dir),
+        get_prusti_contracts_build_target_dir(&target_dir),
         // Libraries when building Prusti will show up here
-        target_dir.join("verify").join(BUILD_MODE),
-    ];
+        target_dir,
+    ]
+    .map(|path| path.join("verify").join(BUILD_MODE));
     candidates
         .into_iter()
         .find(|candidate| candidate.join(&a_prusti_contracts_file).exists())