More reliable finding of executables

viperproject · Nov 30, 2023 · 1d7c0d0 · 1d7c0d0
1 parent cc4b9f6
commit 1d7c0d0
Show file tree

Hide file tree

Showing 2 changed files with 31 additions and 32 deletions.
diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs
@@ -350,7 +350,7 @@ pub fn viper_home() -> String {
         if let Some(path) = find_viper_home(&current_executable_dir) {
             path.to_str().unwrap().to_owned()
         } else {
-            panic!("Failed to detect Vipe home, please set viper_home configuration flag")
+            panic!("Failed to detect Viper home, please set viper_home configuration flag")
         }
     }
 }

diff --git a/prusti-utils/src/launch/mod.rs b/prusti-utils/src/launch/mod.rs
@@ -26,25 +26,28 @@ pub fn get_current_executable_dir() -> PathBuf {
         .to_path_buf()
 }
 
+pub fn get_target_dir(exe_dir: &Path) -> PathBuf {
+    let mut root_dir = exe_dir;
+    while root_dir.file_name().unwrap() != "target" {
+        root_dir = root_dir.parent().unwrap();
+    }
+    root_dir.to_path_buf()
+}
+
 pub fn get_prusti_contracts_dir(exe_dir: &Path) -> Option<PathBuf> {
     let a_prusti_contracts_file = format!("lib{}.rlib", PRUSTI_LIBS[0].replace('-', "_"));
-    let target_dir = if cfg!(debug_assertions) {
+    let build_mode = if cfg!(debug_assertions) {
         "debug"
     } else {
         "release"
     };
+
+    let target_dir = get_target_dir(exe_dir);
     let candidates = [
         // Libraries in the Prusti artifact will show up here
         exe_dir.to_path_buf(),
         // Libraries when building Prusti will show up here
-        exe_dir
-            .parent()
-            .unwrap()
-            .parent()
-            .unwrap()
-            .join("target")
-            .join("verify")
-            .join(target_dir),
+        target_dir.join("verify").join(build_mode),
     ];
     candidates
         .into_iter()
@@ -178,28 +181,24 @@ fn get_sysroot_from_rustup() -> Option<PathBuf> {
 
 /// Find Viper home
 pub fn find_viper_home(base_dir: &Path) -> Option<PathBuf> {
-    let candidates = vec![
-        base_dir.join("viper_tools").join("server"),
-        base_dir
-            .join("..")
-            .join("..")
-            .join("viper_tools")
-            .join("server"),
-        base_dir.join("viper_tools").join("backends"),
-        base_dir
-            .join("..")
-            .join("..")
-            .join("viper_tools")
-            .join("backends"),
-        base_dir
-            .join("..")
-            .join("..")
-            .join("..")
-            .join("viper_tools")
-            .join("backends"),
-    ];
-
-    candidates.into_iter().find(|candidate| candidate.is_dir())
+    let mut dir = base_dir;
+    loop {
+        if dir.join("viper_tools").is_dir() {
+            let viper_tools_dir = dir.join("viper_tools");
+            let backends_dir = viper_tools_dir.join("backends");
+            if backends_dir.is_dir() {
+                return Some(backends_dir);
+            }
+            let server_dir = viper_tools_dir.join("server");
+            if server_dir.is_dir() {
+                return Some(server_dir);
+            }
+        }
+        match dir.parent() {
+            Some(parent) => dir = parent,
+            None => return None,
+        }
+    }
 }
 
 /// Find Z3 executable