From 4e9f6b2886f2fc5124e7c17255e75e58b18e8874 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 16 Dec 2024 13:42:47 -0500 Subject: [PATCH 01/10] first attempt at parallel verification --- .github/workflows/kani.yml | 15 ++++++-- scripts/run-kani.sh | 77 +++++++++++++++++++++++++++++++------- 2 files changed, 75 insertions(+), 17 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 89d9096ec3289..10bf91a745fab 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -17,25 +17,34 @@ defaults: jobs: check-kani-on-std: - name: Verify std library + name: Verify std library (partition ${{ matrix.partition }}) runs-on: ${{ matrix.os }} strategy: matrix: os: [ubuntu-latest, macos-latest] + partition: [1, 2, 3, 4] include: - os: ubuntu-latest base: ubuntu - os: macos-latest base: macos + fail-fast: false + + env: + PARALLEL_INDEX: ${{ matrix.partition }} + PARALLEL_TOTAL: 4 + steps: - # Step 1: Check out the repository - name: Checkout Repository uses: actions/checkout@v4 with: path: head submodules: true - # Step 2: Run Kani on the std library (default configuration) + - name: Install jq + if: matrix.os == 'ubuntu-latest' + run: sudo apt-get install -y jq + - name: Run Kani Verification run: head/scripts/run-kani.sh --path ${{github.workspace}}/head diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 652680bd7eb78..29ae925afdf4c 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -151,10 +151,39 @@ get_kani_path() { echo "$(realpath "$build_dir/scripts/kani")" } -run_kani_command() { +get_harnesses() { local kani_path="$1" - shift - "$kani_path" "$@" + # Run kani list with JSON format and process with jq to extract all harness names + # Note: This code is based on `kani list` JSON version 0.1 -- if the version changes, this logic may need to change as well. + "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format json \ + jq -r ' + ([.["standard-harnesses"] | to_entries | .[] | .value[]] + + [.["contract-harnesses"] | to_entries | .[] | .value[]]) | + .[] + ' +} + +run_verification_subset() { + local kani_path="$1" + local harnesses=("${@:2}") # All arguments after kani_path are harness names + + # Build the --harness arguments + local harness_args="" + for harness in "${harnesses[@]}"; do + harness_args="$harness_args --harness $harness" + done + + echo "Running verification for harnesses: ${harnesses[*]}" + "$kani_path" verify-std -Z unstable-options ./library \ + -Z function-contracts \ + -Z mem-predicates \ + -Z loop-contracts \ + -Z float-lib \ + -Z c-ffi \ + $harness_args -- exact \ + $command_args \ + --enable-unstable \ + --cbmc-args --object-bits 12 } # Check if binary exists and is up to date @@ -176,7 +205,6 @@ check_binary_exists() { return 1 } - main() { local build_dir="$WORK_DIR/kani_build" @@ -209,16 +237,37 @@ main() { "$kani_path" --version if [[ "$run_command" == "verify-std" ]]; then - echo "Running Kani verify-std command..." - "$kani_path" verify-std -Z unstable-options ./library \ - -Z function-contracts \ - -Z mem-predicates \ - -Z loop-contracts \ - -Z float-lib \ - -Z c-ffi \ - $command_args \ - --enable-unstable \ - --cbmc-args --object-bits 12 + if [[ -n "$PARALLEL_INDEX" && -n "$PARALLEL_TOTAL" ]]; then + echo "Running as parallel worker $PARALLEL_INDEX of $PARALLEL_TOTAL" + + # Get all harnesses + readarray -t all_harnesses < <(get_harnesses "$kani_path") + total_harnesses=${#all_harnesses[@]} + + # Calculate this worker's portion + chunk_size=$(( (total_harnesses + PARALLEL_TOTAL - 1) / PARALLEL_TOTAL )) + start_idx=$(( (PARALLEL_INDEX - 1) * chunk_size )) + end_idx=$(( start_idx + chunk_size )) + [[ $end_idx -gt $total_harnesses ]] && end_idx=$total_harnesses + + # Extract this worker's harnesses + worker_harnesses=("${all_harnesses[@]:$start_idx:$chunk_size}") + + # Run verification for this subset + run_verification_subset "$kani_path" "${worker_harnesses[@]}" + else + # Run verification for all harnesses (not in parallel) + echo "Running Kani verify-std command..." + "$kani_path" verify-std -Z unstable-options ./library \ + -Z function-contracts \ + -Z mem-predicates \ + -Z loop-contracts \ + -Z float-lib \ + -Z c-ffi \ + $command_args \ + --enable-unstable \ + --cbmc-args --object-bits 12 + fi elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format markdown From 2bf83921a5e55d55d0c196422b60901c1caf54f1 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 16 Dec 2024 16:06:35 -0500 Subject: [PATCH 02/10] read from kani-list.json --- scripts/run-kani.sh | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 29ae925afdf4c..557406116259e 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -77,6 +77,10 @@ TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE} REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL} BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME} +# Kani list related variables, set in get_harnesses(); these are only used to parallelize harness verification +declare -a ALL_HARNESSES +declare -i HARNESS_COUNT + # Function to read commit ID from TOML file read_commit_from_toml() { local file="$1" @@ -151,16 +155,17 @@ get_kani_path() { echo "$(realpath "$build_dir/scripts/kani")" } +# Run kani list with JSON format and process with jq to extract all harness names +# Note: This code is based on `kani list` JSON version 0.1 -- if the version changes, this logic may need to change as well. get_harnesses() { local kani_path="$1" - # Run kani list with JSON format and process with jq to extract all harness names - # Note: This code is based on `kani list` JSON version 0.1 -- if the version changes, this logic may need to change as well. - "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format json \ - jq -r ' + "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format json + ALL_HARNESSES=($(jq -r ' ([.["standard-harnesses"] | to_entries | .[] | .value[]] + - [.["contract-harnesses"] | to_entries | .[] | .value[]]) | + [.["contract-harnesses"] | to_entries | .[] | .value[]]) | .[] - ' + ' $WORK_DIR/kani-list.json)) + HARNESS_COUNT=${#ALL_HARNESSES[@]} } run_verification_subset() { @@ -180,7 +185,7 @@ run_verification_subset() { -Z loop-contracts \ -Z float-lib \ -Z c-ffi \ - $harness_args -- exact \ + $harness_args --exact \ $command_args \ --enable-unstable \ --cbmc-args --object-bits 12 @@ -239,19 +244,16 @@ main() { if [[ "$run_command" == "verify-std" ]]; then if [[ -n "$PARALLEL_INDEX" && -n "$PARALLEL_TOTAL" ]]; then echo "Running as parallel worker $PARALLEL_INDEX of $PARALLEL_TOTAL" - - # Get all harnesses - readarray -t all_harnesses < <(get_harnesses "$kani_path") - total_harnesses=${#all_harnesses[@]} + get_harnesses "$kani_path" # Calculate this worker's portion - chunk_size=$(( (total_harnesses + PARALLEL_TOTAL - 1) / PARALLEL_TOTAL )) + chunk_size=$(( (HARNESS_COUNT + PARALLEL_TOTAL - 1) / PARALLEL_TOTAL )) start_idx=$(( (PARALLEL_INDEX - 1) * chunk_size )) end_idx=$(( start_idx + chunk_size )) - [[ $end_idx -gt $total_harnesses ]] && end_idx=$total_harnesses + [[ $end_idx -gt $HARNESS_COUNT ]] && end_idx=$HARNESS_COUNT # Extract this worker's harnesses - worker_harnesses=("${all_harnesses[@]:$start_idx:$chunk_size}") + worker_harnesses=("${ALL_HARNESSES[@]:$start_idx:$chunk_size}") # Run verification for this subset run_verification_subset "$kani_path" "${worker_harnesses[@]}" From eabaca149f8585d66e7ed39429a239ced2f39304 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 16 Dec 2024 16:37:15 -0500 Subject: [PATCH 03/10] add more debug printing --- scripts/run-kani.sh | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 557406116259e..84d8400d02947 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -178,7 +178,8 @@ run_verification_subset() { harness_args="$harness_args --harness $harness" done - echo "Running verification for harnesses: ${harnesses[*]}" + echo "Running verification for harnesses:" + printf '%s\n' "${harnesses[@]}" "$kani_path" verify-std -Z unstable-options ./library \ -Z function-contracts \ -Z mem-predicates \ @@ -245,12 +246,22 @@ main() { if [[ -n "$PARALLEL_INDEX" && -n "$PARALLEL_TOTAL" ]]; then echo "Running as parallel worker $PARALLEL_INDEX of $PARALLEL_TOTAL" get_harnesses "$kani_path" + + echo "All harnesses:" + printf '%s\n' "${ALL_HARNESSES[@]}" + echo "Total number of harnesses: $HARNESS_COUNT" # Calculate this worker's portion chunk_size=$(( (HARNESS_COUNT + PARALLEL_TOTAL - 1) / PARALLEL_TOTAL )) + echo "Number of harnesses this worker will run: $chunk_size" + start_idx=$(( (PARALLEL_INDEX - 1) * chunk_size )) end_idx=$(( start_idx + chunk_size )) + # If end_idx > HARNESS_COUNT, truncate it to $HARNESS_COUNT [[ $end_idx -gt $HARNESS_COUNT ]] && end_idx=$HARNESS_COUNT + + echo "Start index into ALL_HARNESSES is $start_idx" + echo "End index into ALL_HARNESSES is $end_idx" # Extract this worker's harnesses worker_harnesses=("${ALL_HARNESSES[@]:$start_idx:$chunk_size}") From a455bcb5adbc5b8727fed98b5a1365c5c4c879cf Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 16 Dec 2024 18:00:04 -0500 Subject: [PATCH 04/10] documentation --- .github/workflows/kani.yml | 7 +++++-- scripts/run-kani.sh | 6 ++++-- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 10bf91a745fab..59a0c56a5d49f 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -35,16 +35,19 @@ jobs: PARALLEL_TOTAL: 4 steps: + # Step 1: Check out the repository - name: Checkout Repository uses: actions/checkout@v4 with: path: head submodules: true - + + # Step 2: Install jq - name: Install jq if: matrix.os == 'ubuntu-latest' run: sudo apt-get install -y jq - + + # Step 3: Run Kani on the std library (default configuration) - name: Run Kani Verification run: head/scripts/run-kani.sh --path ${{github.workspace}}/head diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 84d8400d02947..13b2dfc2afaa1 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -155,8 +155,9 @@ get_kani_path() { echo "$(realpath "$build_dir/scripts/kani")" } -# Run kani list with JSON format and process with jq to extract all harness names -# Note: This code is based on `kani list` JSON version 0.1 -- if the version changes, this logic may need to change as well. +# Run kani list with JSON format and process with jq to extract harness names and total number of harnesses. +# Note: The code to extract ALL_HARNESSES is dependent on `kani list --format json` FILE_VERSION 0.1. +# If FILE_VERSION changes, this logic may need to change as well. get_harnesses() { local kani_path="$1" "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format json @@ -168,6 +169,7 @@ get_harnesses() { HARNESS_COUNT=${#ALL_HARNESSES[@]} } +# Given an array of harness names, run verification for those harnesses run_verification_subset() { local kani_path="$1" local harnesses=("${@:2}") # All arguments after kani_path are harness names From 01cba9514762ba1359c4e001089976ddd30d5e3a Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 18 Dec 2024 11:04:49 -0500 Subject: [PATCH 05/10] error if file version neq 1; avoid pipefail problem --- scripts/run-kani.sh | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 13b2dfc2afaa1..03024f9575efa 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -157,10 +157,16 @@ get_kani_path() { # Run kani list with JSON format and process with jq to extract harness names and total number of harnesses. # Note: The code to extract ALL_HARNESSES is dependent on `kani list --format json` FILE_VERSION 0.1. -# If FILE_VERSION changes, this logic may need to change as well. +# If FILE_VERSION changes, first update the ALL_HARNESSES extraction logic to work with the new format, if necessary, +# then update the FILE_VERSION check to check for the new version. get_harnesses() { local kani_path="$1" "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format json + local json_file_version = $(jq -r '.["file-version"]' $WORK_DIR/kani-list.json) + if [[ $json_file_version != "0.1" ]]; then + echo "Error: The JSON file-version in kani-list.json does not equal 0.1." + exit 1 + fi ALL_HARNESSES=($(jq -r ' ([.["standard-harnesses"] | to_entries | .[] | .value[]] + [.["contract-harnesses"] | to_entries | .[] | .value[]]) | @@ -260,7 +266,9 @@ main() { start_idx=$(( (PARALLEL_INDEX - 1) * chunk_size )) end_idx=$(( start_idx + chunk_size )) # If end_idx > HARNESS_COUNT, truncate it to $HARNESS_COUNT - [[ $end_idx -gt $HARNESS_COUNT ]] && end_idx=$HARNESS_COUNT + if [[ $end_idx > $HARNESS_COUNT ]]; then + end_idx=$HARNESS_COUNT + fi echo "Start index into ALL_HARNESSES is $start_idx" echo "End index into ALL_HARNESSES is $end_idx" From 98447cdfe92fe5a67c0d8cfdd3a144882723dfdd Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 18 Dec 2024 12:43:49 -0500 Subject: [PATCH 06/10] Pass -j to Kani to spawn multiple verification threads --- scripts/run-kani.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 03024f9575efa..911cf61bf6ee4 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -195,6 +195,8 @@ run_verification_subset() { -Z float-lib \ -Z c-ffi \ $harness_args --exact \ + -j $VERIFICATION_THREAD_COUNT \ + --output-format=terse \ $command_args \ --enable-unstable \ --cbmc-args --object-bits 12 From b38f871afdf4db2f79afa0d3ed36b9ccb8bfab30 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 18 Dec 2024 12:44:58 -0500 Subject: [PATCH 07/10] documentation & clarity cleanups --- .github/workflows/kani.yml | 6 ++++-- scripts/run-kani.sh | 32 ++++++++++++++++++-------------- 2 files changed, 22 insertions(+), 16 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 59a0c56a5d49f..90463ec8574c6 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -31,8 +31,10 @@ jobs: fail-fast: false env: - PARALLEL_INDEX: ${{ matrix.partition }} - PARALLEL_TOTAL: 4 + # Define the index of this particular worker [1-WORKER_TOTAL] + WORKER_INDEX: ${{ matrix.partition }} + # Total number of workers running this step + WORKER_TOTAL: 4 steps: # Step 1: Check out the repository diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 911cf61bf6ee4..1160ef5270d7f 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -77,9 +77,20 @@ TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE} REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL} BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME} -# Kani list related variables, set in get_harnesses(); these are only used to parallelize harness verification +# Variables used for parallel harness verification +# When we say "parallel," we mean two dimensions of parallelization: +# 1. Sharding verification across multiple workers. The Kani workflow that calls this script defines WORKER_INDEX and WORKER_TOTAL for this purpose: +# we shard verification across WORKER_TOTAL workers, where each worker has a unique WORKER_INDEX that it uses to derive its share of ALL_HARNESSES to verify. +# 2. Within a single worker, we parallelize verification between multiple cores by invoking kani with -j VERIFICATION_THREAD_COUNT. +# For now, VERIFICATION_THREAD_COUNT=4 since the Kani workflow runs on standard Github runners, which have 3-4 cores. +# TODO: If we move to larger runners, we should increase this number. + +# Array of all of the harnesses in the repository, set in get_harnesses() declare -a ALL_HARNESSES +# Length of ALL_HARNESSES, set in get_harnesses() declare -i HARNESS_COUNT +# Number of threads to spawn within a single worker to run Kani. +declare -i VERIFICATION_THREAD_COUNT=4 # Function to read commit ID from TOML file read_commit_from_toml() { @@ -162,7 +173,7 @@ get_kani_path() { get_harnesses() { local kani_path="$1" "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format json - local json_file_version = $(jq -r '.["file-version"]' $WORK_DIR/kani-list.json) + local json_file_version=$(jq -r '.["file-version"]' "$WORK_DIR/kani-list.json") if [[ $json_file_version != "0.1" ]]; then echo "Error: The JSON file-version in kani-list.json does not equal 0.1." exit 1 @@ -253,27 +264,20 @@ main() { "$kani_path" --version if [[ "$run_command" == "verify-std" ]]; then - if [[ -n "$PARALLEL_INDEX" && -n "$PARALLEL_TOTAL" ]]; then - echo "Running as parallel worker $PARALLEL_INDEX of $PARALLEL_TOTAL" + if [[ -n "$WORKER_INDEX" && -n "$WORKER_TOTAL" ]]; then + echo "Running as parallel worker $WORKER_INDEX of $WORKER_TOTAL" get_harnesses "$kani_path" echo "All harnesses:" printf '%s\n' "${ALL_HARNESSES[@]}" echo "Total number of harnesses: $HARNESS_COUNT" - # Calculate this worker's portion - chunk_size=$(( (HARNESS_COUNT + PARALLEL_TOTAL - 1) / PARALLEL_TOTAL )) + # Calculate this worker's portion (add WORKER_TOTAL - 1 to force ceiling division) + chunk_size=$(( (HARNESS_COUNT + WORKER_TOTAL - 1) / WORKER_TOTAL )) echo "Number of harnesses this worker will run: $chunk_size" - start_idx=$(( (PARALLEL_INDEX - 1) * chunk_size )) - end_idx=$(( start_idx + chunk_size )) - # If end_idx > HARNESS_COUNT, truncate it to $HARNESS_COUNT - if [[ $end_idx > $HARNESS_COUNT ]]; then - end_idx=$HARNESS_COUNT - fi - + start_idx=$(( (WORKER_INDEX - 1) * chunk_size )) echo "Start index into ALL_HARNESSES is $start_idx" - echo "End index into ALL_HARNESSES is $end_idx" # Extract this worker's harnesses worker_harnesses=("${ALL_HARNESSES[@]:$start_idx:$chunk_size}") From e566a2480d384998647d82180b216c7bebee7b53 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 18 Dec 2024 14:36:29 -0500 Subject: [PATCH 08/10] Remove VERIFICATION_THREAD_COUNT kani -j with no arguments defaults to the number of CPUs, so no need for a fixed number --- scripts/run-kani.sh | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 1160ef5270d7f..200042ca0e67c 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -81,16 +81,12 @@ BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME} # When we say "parallel," we mean two dimensions of parallelization: # 1. Sharding verification across multiple workers. The Kani workflow that calls this script defines WORKER_INDEX and WORKER_TOTAL for this purpose: # we shard verification across WORKER_TOTAL workers, where each worker has a unique WORKER_INDEX that it uses to derive its share of ALL_HARNESSES to verify. -# 2. Within a single worker, we parallelize verification between multiple cores by invoking kani with -j VERIFICATION_THREAD_COUNT. -# For now, VERIFICATION_THREAD_COUNT=4 since the Kani workflow runs on standard Github runners, which have 3-4 cores. -# TODO: If we move to larger runners, we should increase this number. +# 2. Within a single worker, we parallelize verification between multiple cores by invoking kani with -j. # Array of all of the harnesses in the repository, set in get_harnesses() declare -a ALL_HARNESSES # Length of ALL_HARNESSES, set in get_harnesses() declare -i HARNESS_COUNT -# Number of threads to spawn within a single worker to run Kani. -declare -i VERIFICATION_THREAD_COUNT=4 # Function to read commit ID from TOML file read_commit_from_toml() { @@ -206,7 +202,7 @@ run_verification_subset() { -Z float-lib \ -Z c-ffi \ $harness_args --exact \ - -j $VERIFICATION_THREAD_COUNT \ + -j \ --output-format=terse \ $command_args \ --enable-unstable \ From cb503644de972d0d2adc5c269e469b478385eeee Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 19 Dec 2024 12:39:22 -0500 Subject: [PATCH 09/10] address feedback from PR review --- scripts/run-kani.sh | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 200042ca0e67c..b185ca8e08815 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -77,6 +77,9 @@ TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE} REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL} BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME} +# Unstable arguments to pass to Kani +unstable_args="-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts" + # Variables used for parallel harness verification # When we say "parallel," we mean two dimensions of parallelization: # 1. Sharding verification across multiple workers. The Kani workflow that calls this script defines WORKER_INDEX and WORKER_TOTAL for this purpose: @@ -87,6 +90,8 @@ BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME} declare -a ALL_HARNESSES # Length of ALL_HARNESSES, set in get_harnesses() declare -i HARNESS_COUNT +# `kani list` JSON FILE_VERSION that the parallel verification command expects +EXPECTED_JSON_FILE_VERSION="0.1" # Function to read commit ID from TOML file read_commit_from_toml() { @@ -164,16 +169,19 @@ get_kani_path() { # Run kani list with JSON format and process with jq to extract harness names and total number of harnesses. # Note: The code to extract ALL_HARNESSES is dependent on `kani list --format json` FILE_VERSION 0.1. +# (The FILE_VERSION variable is defined in Kani in the list module's output code, current path kani-driver/src/list/output.rs) # If FILE_VERSION changes, first update the ALL_HARNESSES extraction logic to work with the new format, if necessary, -# then update the FILE_VERSION check to check for the new version. +# then update EXPECTED_JSON_FILE_VERSION. get_harnesses() { local kani_path="$1" - "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format json + "$kani_path" list -Z list $unstable_args ./library --std --format json local json_file_version=$(jq -r '.["file-version"]' "$WORK_DIR/kani-list.json") - if [[ $json_file_version != "0.1" ]]; then - echo "Error: The JSON file-version in kani-list.json does not equal 0.1." + if [[ $json_file_version != $EXPECTED_JSON_FILE_VERSION ]]; then + echo "Error: The JSON file-version in kani-list.json does not equal $EXPECTED_JSON_FILE_VERSION" exit 1 fi + # Extract the harnesses inside "standard-harnesses" and "contract-harnesses" + # into an array called ALL_HARNESSES and the length of that array into HARNESS_COUNT ALL_HARNESSES=($(jq -r ' ([.["standard-harnesses"] | to_entries | .[] | .value[]] + [.["contract-harnesses"] | to_entries | .[] | .value[]]) | @@ -196,11 +204,7 @@ run_verification_subset() { echo "Running verification for harnesses:" printf '%s\n' "${harnesses[@]}" "$kani_path" verify-std -Z unstable-options ./library \ - -Z function-contracts \ - -Z mem-predicates \ - -Z loop-contracts \ - -Z float-lib \ - -Z c-ffi \ + $unstable_args \ $harness_args --exact \ -j \ --output-format=terse \ @@ -284,18 +288,14 @@ main() { # Run verification for all harnesses (not in parallel) echo "Running Kani verify-std command..." "$kani_path" verify-std -Z unstable-options ./library \ - -Z function-contracts \ - -Z mem-predicates \ - -Z loop-contracts \ - -Z float-lib \ - -Z c-ffi \ + $unstable_args $command_args \ --enable-unstable \ --cbmc-args --object-bits 12 fi elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." - "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format markdown + "$kani_path" list -Z list $unstable_flags ./library --std --format markdown fi } From 99c960a73eef3ca58c612e3d1c67b10941f4e8b6 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 19 Dec 2024 12:48:03 -0500 Subject: [PATCH 10/10] fix typo --- scripts/run-kani.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index b185ca8e08815..72aa8ef176056 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -295,7 +295,7 @@ main() { fi elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." - "$kani_path" list -Z list $unstable_flags ./library --std --format markdown + "$kani_path" list -Z list $unstable_args ./library --std --format markdown fi }