From 01539d2a41400a68ca75c73380d143157ae31069 Mon Sep 17 00:00:00 2001
From: Zack Grannan <zgrannan@protonmail.com>
Date: Wed, 6 Dec 2023 09:09:07 -0800
Subject: [PATCH] Fix `get_target_dir` and build.py to make packaging work
 properly with new prusti_contracts dir (#1479)

* Fix `get_target_dir` and deploy.yml to make packaging work properly

* Add some comments, also reduce parallelism for carbon tests
---
 .github/workflows/deploy.yml   |  4 ++--
 .github/workflows/test.yml     |  2 +-
 prusti-utils/src/launch/mod.rs | 37 ++++++++++++++++++++--------------
 x.py                           | 16 +++++++--------
 4 files changed, 33 insertions(+), 26 deletions(-)

diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml
index 7b9837c3dec..4ff31d77c0e 100644
--- a/.github/workflows/deploy.yml
+++ b/.github/workflows/deploy.yml
@@ -36,10 +36,10 @@ jobs:
         run: python x.py setup
 
       - name: Build with cargo --release
-        run: python x.py build --release --all
+        run: python x.py build --release --all --jobs 1
 
       - name: Run cargo tests --release
-        run: python x.py test --release --all
+        run: python x.py test --release --all --jobs 1
 
       - name: Package Prusti artifact
         run: python x.py package release prusti_artifact
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index f9f53aff1cc..0603b9bbcdd 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -255,7 +255,7 @@ jobs:
         run: python x.py test --all --jobs 1
       - name: Run a subset of tests with Carbon
         run: |
-            python x.py test pass/no-annotation --all --verbose
+            python x.py test pass/no-annotation --all --verbose --jobs 1
         env:
           PRUSTI_VIPER_BACKEND: carbon
       - name: Check prusti-contracts
diff --git a/prusti-utils/src/launch/mod.rs b/prusti-utils/src/launch/mod.rs
index 51ed671b713..71dfdf8cf16 100644
--- a/prusti-utils/src/launch/mod.rs
+++ b/prusti-utils/src/launch/mod.rs
@@ -35,12 +35,17 @@ pub fn get_current_executable_dir() -> PathBuf {
 /// Finds the closest `target` directory in the current path.
 /// This should be the target directory at the root of the repository,
 /// i.e. `prusti-dev/target`.
-pub fn get_target_dir(exe_dir: &Path) -> PathBuf {
+fn get_target_dir(exe_dir: &Path) -> Option<PathBuf> {
     let mut root_dir = exe_dir;
-    while root_dir.file_name().unwrap() != "target" {
-        root_dir = root_dir.parent().unwrap();
+    loop {
+        if root_dir.file_name().unwrap() == "target" {
+            return Some(root_dir.to_path_buf());
+        }
+        match root_dir.parent() {
+            Some(parent) => root_dir = parent,
+            None => return None,
+        }
     }
-    root_dir.to_path_buf()
 }
 
 pub fn get_prusti_contracts_build_target_dir(target_dir: &Path) -> PathBuf {
@@ -50,17 +55,19 @@ pub fn get_prusti_contracts_build_target_dir(target_dir: &Path) -> PathBuf {
 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 = get_target_dir(exe_dir);
-    let candidates = [
-        // Libraries in the Prusti artifact will show up here
-        get_prusti_contracts_build_target_dir(&target_dir),
-        // Libraries when building Prusti will show up here
-        target_dir,
-    ]
-    .map(|path| path.join("verify").join(BUILD_MODE));
-    candidates
-        .into_iter()
-        .find(|candidate| candidate.join(&a_prusti_contracts_file).exists())
+    if exe_dir.join(&a_prusti_contracts_file).exists() {
+        // If this branch is entered, then this is the Prusti Artifact
+        return Some(exe_dir.to_path_buf());
+    } else if let Some(target_dir) = get_target_dir(exe_dir) {
+        // If this branch is entered, then we're building Prusti
+        let candidate = get_prusti_contracts_build_target_dir(&target_dir)
+            .join("verify")
+            .join(BUILD_MODE);
+        if candidate.join(&a_prusti_contracts_file).exists() {
+            return Some(candidate);
+        }
+    }
+    None
 }
 
 /// Append paths to the loader environment variable
diff --git a/x.py b/x.py
index 951db082581..3a841ed2a3a 100755
--- a/x.py
+++ b/x.py
@@ -233,17 +233,17 @@ def package(mode: str, package_path: str):
         (f"target/{mode}/prusti-server*", "."),
         (f"target/{mode}/prusti-rustc*", "."),
         (f"target/{mode}/cargo-prusti*", "."),
-        (f"target/verify/{mode}/libprusti_contracts.*", "."),
-        (f"target/verify/{mode}/deps/libprusti_contracts_proc_macros-*", "deps"),
-        (f"target/verify/{mode}/deps/prusti_contracts_proc_macros-*.dll", "deps"),
-        (f"target/verify/{mode}/libprusti_std.*", "."),
-        (f"target/verify/{mode}/deps/libprusti_contracts-*", "deps"),
-        (f"target/verify/{mode}/deps/prusti_contracts-*.dll", "deps"),
+        (f"target/prusti-contracts/{mode}/verify/{mode}/libprusti_contracts.*", "."),
+        (f"target/prusti-contracts/{mode}/verify/{mode}/deps/libprusti_contracts_proc_macros-*", "deps"),
+        (f"target/prusti-contracts/{mode}/verify/{mode}/deps/prusti_contracts_proc_macros-*.dll", "deps"),
+        (f"target/prusti-contracts/{mode}/verify/{mode}/libprusti_std.*", "."),
+        (f"target/prusti-contracts/{mode}/verify/{mode}/deps/libprusti_contracts-*", "deps"),
+        (f"target/prusti-contracts/{mode}/verify/{mode}/deps/prusti_contracts-*.dll", "deps"),
     ]
     exclude_paths = [
         f"target/{mode}/*.d",
-        f"target/verify/{mode}/*.d",
-        f"target/verify/{mode}/deps/*.d",
+        f"target/prusti-contracts/{mode}/verify/{mode}/*.d",
+        f"target/prusti-contracts/{mode}/verify/{mode}/deps/*.d",
     ]
     actual_exclude_set = set(path for pattern in exclude_paths for path in glob.glob(pattern))
     logging.debug(f"The number of excluded paths is: {len(actual_exclude_set)}")