Skip to content

Commit 61f68cf

Browse files
jaisnantautschnig
jaisnan
and
tautschnig
authored
Add script to automate build & running kani (model-checking#78)
1. Adds a one-click command to pull, build and run kani 2. Adds a toml file to store the commit info about the HEAD of `kani/features/verify-std` 3. Checks for caching to prevent re-pulling, and building already compatible kani binary 4. Modifies CI to re-use this script instead of the previous script 5. Add `--kani-args` to pass arguments to kani command. `-p` sets the working directory. 6. Adds a CI job to test the entrypoint workflow itself. 7. Default output-format to terse #### Extras Cleans up some print statements in the `run_update_with_checks` script. ## Call-out 1. This does not allow command configuration, so it essentially all proofs in the library by default, which CAN get expensive. I can very easily add a harness filter to ensure that we can process only relevent harnesses. 2. Need to change documentation to use this command instead of using kani directly as is currently suggested. 3. Need to consider move to python, argument parsing with bash is a bad experience. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Michael Tautschnig <[email protected]>
1 parent 38d490c commit 61f68cf

File tree

5 files changed

+239
-63
lines changed

5 files changed

+239
-63
lines changed

‎.github/workflows/kani.yml‎

Lines changed: 37 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
1-
# This workflow is responsible for verifying the standard library with Kani.
2-
31
name: Kani
2+
43
on:
54
workflow_dispatch:
65
pull_request:
@@ -9,30 +8,60 @@ on:
98
paths:
109
- 'library/**'
1110
- '.github/workflows/kani.yml'
12-
- 'scripts/check_kani.sh'
11+
- 'scripts/run-kani.sh'
1312

1413
defaults:
1514
run:
1615
shell: bash
1716

1817
jobs:
19-
build:
18+
check-kani-on-std:
19+
name: Verify std library
2020
runs-on: ${{ matrix.os }}
2121
strategy:
2222
matrix:
23-
# Kani does not support windows.
2423
os: [ubuntu-latest, macos-latest]
2524
include:
2625
- os: ubuntu-latest
2726
base: ubuntu
2827
- os: macos-latest
2928
base: macos
3029
steps:
31-
- name: Checkout Library
30+
# Step 1: Check out the repository
31+
- name: Checkout Repository
3232
uses: actions/checkout@v4
3333
with:
3434
path: head
3535
submodules: true
3636

37-
- name: Run Kani Script
38-
run: bash ./head/scripts/check_kani.sh ${{github.workspace}}/head
37+
# Step 2: Run Kani on the std library (default configuration)
38+
- name: Run Kani Verification
39+
run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
40+
41+
test-kani-script:
42+
name: Test Kani script
43+
runs-on: ${{ matrix.os }}
44+
strategy:
45+
matrix:
46+
os: [ubuntu-latest, macos-latest]
47+
include:
48+
- os: ubuntu-latest
49+
base: ubuntu
50+
- os: macos-latest
51+
base: macos
52+
steps:
53+
# Step 1: Check out the repository
54+
- name: Checkout Repository
55+
uses: actions/checkout@v4
56+
with:
57+
path: head
58+
submodules: true
59+
60+
# Step 2: Test Kani verification script with specific arguments
61+
- name: Test Kani script (Custom Args)
62+
run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr --output-format=terse
63+
64+
# Step 3: Test Kani verification script in the repository directory
65+
- name: Test Kani script (In Repo Directory)
66+
working-directory: ${{github.workspace}}/head
67+
run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ Session.vim
1919
## Build
2020
/book/
2121
/build/
22+
/kani_build/
2223
/target
2324
library/target
2425
*.rlib

‎scripts/check_kani.sh‎

Lines changed: 0 additions & 55 deletions
This file was deleted.

‎scripts/run-kani.sh‎

Lines changed: 196 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,196 @@
1+
#!/bin/bash
2+
3+
set -e
4+
5+
usage() {
6+
echo "Usage: $0 [options] [-p <path>] [--kani-args <command arguments>]"
7+
echo "Options:"
8+
echo " -h, --help Show this help message"
9+
echo " -p, --path <path> Optional: Specify a path to a copy of the std library. For example, if you want to run the script from an outside directory."
10+
echo " --kani-args <command arguments to kani> Optional: Arguments to pass to the command. Simply pass them in the same way you would to the Kani binary. This should be the last argument."
11+
exit 1
12+
}
13+
14+
# Initialize variables
15+
command_args=""
16+
path=""
17+
18+
# Parse command line arguments
19+
# TODO: Improve parsing with getopts
20+
while [[ $# -gt 0 ]]; do
21+
case $1 in
22+
-h|--help)
23+
usage
24+
;;
25+
-p|--path)
26+
if [[ -n $2 ]]; then
27+
path=$2
28+
shift 2
29+
else
30+
echo "Error: Path argument is missing"
31+
usage
32+
fi
33+
;;
34+
--kani-args)
35+
shift
36+
command_args="$@"
37+
break
38+
;;
39+
*)
40+
break
41+
;;
42+
esac
43+
done
44+
45+
# Set working directory
46+
if [[ -n "$path" ]]; then
47+
if [[ ! -d "$path" ]]; then
48+
echo "Error: Specified directory does not exist."
49+
usage
50+
fi
51+
WORK_DIR=$(realpath "$path")
52+
else
53+
WORK_DIR=$(pwd)
54+
fi
55+
56+
cd "$WORK_DIR"
57+
58+
# Default values
59+
DEFAULT_TOML_FILE="tool_config/kani-version.toml"
60+
DEFAULT_REPO_URL="https://github.com/model-checking/kani.git"
61+
DEFAULT_BRANCH_NAME="features/verify-rust-std"
62+
63+
# Use environment variables if set, otherwise use defaults
64+
TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE}
65+
REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL}
66+
BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME}
67+
68+
# Function to read commit ID from TOML file
69+
read_commit_from_toml() {
70+
local file="$1"
71+
if [[ ! -f "$file" ]]; then
72+
echo "Error: TOML file not found: $file" >&2
73+
exit 1
74+
fi
75+
local commit=$(grep '^commit *=' "$file" | sed 's/^commit *= *"\(.*\)"/\1/')
76+
if [[ -z "$commit" ]]; then
77+
echo "Error: 'commit' field not found in TOML file" >&2
78+
exit 1
79+
fi
80+
echo "$commit"
81+
}
82+
83+
clone_kani_repo() {
84+
local repo_url="$1"
85+
local directory="$2"
86+
local branch="$3"
87+
local commit="$4"
88+
git clone "$repo_url" "$directory"
89+
pushd "$directory"
90+
git checkout "$commit"
91+
popd
92+
}
93+
94+
get_current_commit() {
95+
local directory="$1"
96+
if [ -d "$directory/.git" ]; then
97+
git -C "$directory" rev-parse HEAD
98+
else
99+
echo ""
100+
fi
101+
}
102+
103+
build_kani() {
104+
local directory="$1"
105+
pushd "$directory"
106+
os_name=$(uname -s)
107+
108+
if [[ "$os_name" == "Linux" ]]; then
109+
./scripts/setup/ubuntu/install_deps.sh
110+
elif [[ "$os_name" == "Darwin" ]]; then
111+
./scripts/setup/macos/install_deps.sh
112+
else
113+
echo "Unknown operating system"
114+
fi
115+
116+
git submodule update --init --recursive
117+
cargo build-dev --release
118+
popd
119+
}
120+
121+
get_kani_path() {
122+
local build_dir="$1"
123+
echo "$(realpath "$build_dir/scripts/kani")"
124+
}
125+
126+
run_kani_command() {
127+
local kani_path="$1"
128+
shift
129+
"$kani_path" "$@"
130+
}
131+
132+
# Check if binary exists and is up to date
133+
check_binary_exists() {
134+
local build_dir="$1"
135+
local expected_commit="$2"
136+
local kani_path=$(get_kani_path "$build_dir")
137+
138+
if [[ -f "$kani_path" ]]; then
139+
local current_commit=$(get_current_commit "$build_dir")
140+
if [[ "$current_commit" = "$expected_commit" ]]; then
141+
return 0
142+
fi
143+
fi
144+
return 1
145+
}
146+
147+
148+
main() {
149+
local build_dir="$WORK_DIR/kani_build"
150+
local temp_dir_target=$(mktemp -d)
151+
152+
echo "Using TOML file: $TOML_FILE"
153+
echo "Using repository URL: $REPO_URL"
154+
155+
# Read commit ID from TOML file
156+
commit=$(read_commit_from_toml "$TOML_FILE")
157+
158+
# Check if binary already exists and is up to date
159+
if check_binary_exists "$build_dir" "$commit"; then
160+
echo "Kani binary is up to date. Skipping build."
161+
else
162+
echo "Building Kani from commit: $commit"
163+
164+
# Remove old build directory if it exists
165+
rm -rf "$build_dir"
166+
mkdir -p "$build_dir"
167+
168+
# Clone repository and checkout specific commit
169+
clone_kani_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit"
170+
171+
# Build project
172+
build_kani "$build_dir"
173+
174+
echo "Kani build completed successfully!"
175+
fi
176+
177+
# Get the path to the Kani executable
178+
kani_path=$(get_kani_path "$build_dir")
179+
echo "Kani executable path: $kani_path"
180+
181+
echo "Running Kani command..."
182+
"$kani_path" --version
183+
184+
echo "Running Kani verify-std command..."
185+
186+
"$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args
187+
}
188+
189+
main
190+
191+
cleanup()
192+
{
193+
rm -rf "$temp_dir_target"
194+
}
195+
196+
trap cleanup EXIT

‎tool_config/kani-version.toml‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
# This version should be updated whenever there is a change that makes this version of kani
2+
# incomaptible with the verify-std repo.
3+
4+
[kani]
5+
commit = "5f8f513d297827cfdce4c48065e51973ba563068"

0 commit comments

Comments
 (0)