From 62f136c9c2c99334f9830e8ef61404c50c7ca7b5 Mon Sep 17 00:00:00 2001
From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
Date: Tue, 3 Oct 2023 12:15:20 -0400
Subject: [PATCH] Prevent kani crash during setup for first time (#2799)

> Please ensure your PR description includes the following:
> 1. A description of how your changes improve Kani.
> 2. Some context on the problem you are solving.
> 3. A list of issues that are resolved by this PR.
> 4. If you had to perform any manual test, please describe them.
>
> **Make sure you remove this list from the final PR description.**

By using the `tar` file as a lock mechanism, we can detect incomplete
setups i.e when both `kani's` working directory and the tar file present
before setup, we can simply use the local bundle to start setup again.

Resolves #1545

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 src/lib.rs   | 11 ++++++++++-
 src/setup.rs | 21 ++++++++++++++++++++-
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/src/lib.rs b/src/lib.rs
index 4639354d8d02..9a1ac90f5dda 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -16,11 +16,11 @@ mod cmd;
 mod os_hacks;
 mod setup;
 
-use std::env;
 use std::ffi::OsString;
 use std::os::unix::prelude::CommandExt;
 use std::path::{Path, PathBuf};
 use std::process::Command;
+use std::{env, fs};
 
 use anyhow::{bail, Context, Result};
 
@@ -33,6 +33,15 @@ pub fn proxy(bin: &str) -> Result<()> {
             fail_if_in_dev_environment()?;
             if !setup::appears_setup() {
                 setup::setup(None)?;
+            } else {
+                // This handles cases where the setup was left incomplete due to an interrupt
+                // For example - https://github.com/model-checking/kani/issues/1545
+                if let Some(path_to_bundle) = setup::appears_incomplete() {
+                    setup::setup(Some(path_to_bundle.clone().into_os_string()))?;
+                    // Suppress warning with unused assignment
+                    // and remove the bundle if it still exists
+                    let _ = fs::remove_file(path_to_bundle);
+                }
             }
             exec(bin)
         }
diff --git a/src/setup.rs b/src/setup.rs
index b7fc48fcf83d..2d2c643bbdd5 100644
--- a/src/setup.rs
+++ b/src/setup.rs
@@ -53,6 +53,22 @@ pub fn appears_setup() -> bool {
     kani_dir().expect("couldn't find kani directory").exists()
 }
 
+// Ensure that the tar file does not exist, essentially using its presence
+// to detect setup completion as if it were a lock file.
+pub fn appears_incomplete() -> Option<PathBuf> {
+    let kani_dir = kani_dir().expect("couldn't find kani directory");
+    let kani_dir_parent = kani_dir.parent().unwrap();
+
+    for entry in std::fs::read_dir(&kani_dir_parent).ok()?.flatten() {
+        if let Some(file_name) = entry.file_name().to_str() {
+            if file_name.ends_with(".tar.gz") {
+                return Some(kani_dir_parent.join(file_name));
+            }
+        }
+    }
+    None
+}
+
 /// Sets up Kani by unpacking/installing to `~/.kani/kani-VERSION`
 pub fn setup(use_local_bundle: Option<OsString>) -> Result<()> {
     let kani_dir = kani_dir()?;
@@ -92,7 +108,10 @@ fn setup_kani_bundle(kani_dir: &Path, use_local_bundle: Option<OsString>) -> Res
             .arg("-zxf")
             .arg(&path)
             .current_dir(&kani_dir)
-            .run()?;
+            .run()
+            .context(
+                "Failed to extract tar file, try removing Kani setup located in .kani in your home directory and restarting",
+            )?;
     } else {
         let filename = download_filename();
         println!("[2/5] Downloading Kani release bundle: {}", &filename);