Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Prevent kani crash during setup for first time #2799

Merged
merged 5 commits into from
Oct 3, 2023
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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 it's presence
jaisnan marked this conversation as resolved.
Show resolved Hide resolved
// 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 and restarting the setup step",
jaisnan marked this conversation as resolved.
Show resolved Hide resolved
)?;
} else {
let filename = download_filename();
println!("[2/5] Downloading Kani release bundle: {}", &filename);
Expand Down