Skip to content

Improve run-kani script to use default target #172

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.

Sign up for GitHub

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

Merged
merged 2 commits into from
Nov 20, 2024
Merged

Improve run-kani script to use default target #172

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
06ce4c4
Improve run-kani script to use default target
celinval Nov 20, 2024
3fdedab
Merge branch 'main' into chores-170-target
celinval Nov 20, 2024
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
63 changes: 36 additions & 27 deletions scripts/run-kani.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,15 +80,26 @@ read_commit_from_toml() {
echo "$commit"
}

clone_kani_repo() {
setup_kani_repo() {
local repo_url="$1"
local directory="$2"
local branch="$3"
local commit="$4"
git clone "$repo_url" "$directory"
pushd "$directory"
git checkout "$commit"
popd

if [[ ! -d "${directory}" ]]; then
mkdir -p "${directory}"
pushd "${directory}" > /dev/null

git init . >& /dev/null
git remote add origin "${repo_url}" >& /dev/null
else
pushd "${directory}" > /dev/null
fi

git fetch --depth 1 origin "$commit" --quiet
git checkout "$commit" --quiet
git submodule update --init --recursive --depth 1 --quiet
popd > /dev/null
}

get_current_commit() {
Expand All @@ -103,17 +114,22 @@ get_current_commit() {
build_kani() {
local directory="$1"
pushd "$directory"
os_name=$(uname -s)

if [[ "$os_name" == "Linux" ]]; then
./scripts/setup/ubuntu/install_deps.sh
elif [[ "$os_name" == "Darwin" ]]; then
./scripts/setup/macos/install_deps.sh
source "kani-dependencies"
# Check if installed versions are correct.
if ./scripts/check-cbmc-version.py --major ${CBMC_MAJOR} --minor ${CBMC_MINOR} && ./scripts/check_kissat_version.sh; then
echo "Dependencies are up-to-date"
else
echo "Unknown operating system"
os_name=$(uname -s)

if [[ "$os_name" == "Linux" ]]; then
./scripts/setup/ubuntu/install_deps.sh
elif [[ "$os_name" == "Darwin" ]]; then
./scripts/setup/macos/install_deps.sh
else
echo "Unknown operating system"
fi
fi

git submodule update --init --recursive
cargo build-dev --release
popd
}
Expand All @@ -135,19 +151,22 @@ check_binary_exists() {
local expected_commit="$2"
local kani_path=$(get_kani_path "$build_dir")

if [[ -f "$kani_path" ]]; then
if [[ -d "${build_dir}" ]]; then
local current_commit=$(get_current_commit "$build_dir")
if [[ "$current_commit" = "$expected_commit" ]]; then
return 0
else
echo "Kani repository is out of date. Rebuilding..."
fi
else
echo "Kani repository not found. Creating..."
fi
return 1
}


main() {
local build_dir="$WORK_DIR/kani_build"
local temp_dir_target=$(mktemp -d)

echo "Using TOML file: $TOML_FILE"
echo "Using repository URL: $REPO_URL"
Expand All @@ -161,12 +180,8 @@ main() {
else
echo "Building Kani from commit: $commit"

# Remove old build directory if it exists
rm -rf "$build_dir"
mkdir -p "$build_dir"

# Clone repository and checkout specific commit
clone_kani_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"
setup_kani_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"

# Build project
build_kani "$build_dir"
Expand All @@ -183,14 +198,8 @@ main() {

echo "Running Kani verify-std command..."

"$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates -Z loop-contracts --output-format=terse $command_args --enable-unstable --cbmc-args --object-bits 12
"$kani_path" verify-std -Z unstable-options ./library -Z function-contracts -Z mem-predicates -Z loop-contracts --output-format=terse $command_args --enable-unstable --cbmc-args --object-bits 12
}

main

cleanup()
{
rm -rf "$temp_dir_target"
}

trap cleanup EXIT
Loading