Skip to content

Commit

Permalink
Prevent kani crash during setup for first time (model-checking#2799)
Browse files Browse the repository at this point in the history
> 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 model-checking#1545 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
jaisnan authored Oct 3, 2023
1 parent ed2df13 commit 62f136c
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 2 deletions.
11 changes: 10 additions & 1 deletion src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};

Expand All @@ -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)
}
Expand Down
21 changes: 20 additions & 1 deletion src/setup.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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()?;
Expand Down Expand Up @@ -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);
Expand Down

0 comments on commit 62f136c

Please sign in to comment.