From eff5200169f133189ad2cc1611945a907237a63a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 08:23:36 +0000 Subject: [PATCH 1/9] Add autoharness-analyzer CI job Run https://github.com/carolynzech/autoharness_analyzer and push its results to the job summary. --- .github/workflows/kani.yml | 18 ++++++++++++++++++ scripts/run-kani.sh | 22 ++++++++++++++++++++-- 2 files changed, 38 insertions(+), 2 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 90463ec8574c6..3af27ee746961 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -79,3 +79,21 @@ jobs: .addHeading('Kani List Output', 2) .addRaw(kaniOutput, false) .write(); + + run-autoharness-analyzer: + name: Kani Autoharness Analyzer + runs-on: ubuntu-latest + steps: + # Step 1: Check out the repository + - name: Checkout Repository + uses: actions/checkout@v4 + with: + submodules: true + + # Step 2: Run autoharness analyzer on the std library + - name: Run Autoharness Analyzer + run: scripts/run-kani.sh --run autoharness-analyzer + + # Step 3: Add output to job summary + - name: Add Autoharness Analyzer output to job summary + run: cat autoharness_analyzer/autoharness_data.md >> "$GITHUB_STEP_SUMMARY" diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 200bd957180d6..274a9fdc57aa0 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -7,7 +7,7 @@ usage() { echo "Options:" echo " -h, --help Show this help message" echo " -p, --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." - echo " --run Optional: Specify whether to run the 'kani verify-std' command, 'kani list' command, or collect Kani-specific metrics. Defaults to 'verify-std' if not specified." + echo " --run Optional: Specify whether to run the 'kani verify-std' command, 'kani list' command, collect Kani-specific metrics, or summarize autoharness failure reasons. Defaults to 'verify-std' if not specified." echo " --kani-args 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." exit 1 } @@ -34,7 +34,7 @@ while [[ $# -gt 0 ]]; do fi ;; --run) - if [[ -n $2 && ($2 == "verify-std" || $2 == "list" || $2 == "metrics") ]]; then + if [[ -n $2 && ($2 == "verify-std" || $2 == "list" || $2 == "metrics" || $2 == "autoharness-analyzer") ]]; then run_command=$2 shift 2 else @@ -317,6 +317,24 @@ main() { --metrics-file metrics-data-std.json popd rm kani-list.json + elif [[ "$run_command" == "autoharness-analyzer" ]]; then + local current_dir=$(pwd) + echo "Running Kani's std-analysis command..." + pushd scripts/kani-std-analysis + ./std-analysis.sh $build_dir + popd + echo "Running Kani autoharness codegen command..." + "$kani_path" autoharness -Z autoharness -Z unstable-options --std ./library \ + --only-codegen -j --output-format=terse + $unstable_args \ + --no-assert-contracts \ + $command_args \ + --enable-unstable \ + --cbmc-args --object-bits 12 + echo "Running autoharness-analyzer command..." + git clone https://github.com/carolynzech/autoharness_analyzer + cd autoharness_analyzer + cargo run ../metadata /tmp/std_lib_analysis/results/ fi } From a8d4419892c9a41fa01a53a915c37dd3a7a5407f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 08:45:26 +0000 Subject: [PATCH 2/9] Fix missing backslash --- 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 274a9fdc57aa0..cfa7f1ca5802d 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -325,7 +325,7 @@ main() { popd echo "Running Kani autoharness codegen command..." "$kani_path" autoharness -Z autoharness -Z unstable-options --std ./library \ - --only-codegen -j --output-format=terse + --only-codegen -j --output-format=terse \ $unstable_args \ --no-assert-contracts \ $command_args \ From f0a410acf555e650d50b2875f44197c022c358ed Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 09:44:00 +0000 Subject: [PATCH 3/9] Fix metadata path --- scripts/run-kani.sh | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index cfa7f1ca5802d..4722cd7cc2e13 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -334,7 +334,9 @@ main() { echo "Running autoharness-analyzer command..." git clone https://github.com/carolynzech/autoharness_analyzer cd autoharness_analyzer - cargo run ../metadata /tmp/std_lib_analysis/results/ + cargo run \ + ../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \ + /tmp/std_lib_analysis/results/ fi } From 10d0ee98bc03b3058c76d429a300991429c1d4bd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 10:17:03 +0000 Subject: [PATCH 4/9] Avoid dummy crate --- scripts/run-kani.sh | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 4722cd7cc2e13..daa1efff313d1 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -318,11 +318,6 @@ main() { popd rm kani-list.json elif [[ "$run_command" == "autoharness-analyzer" ]]; then - local current_dir=$(pwd) - echo "Running Kani's std-analysis command..." - pushd scripts/kani-std-analysis - ./std-analysis.sh $build_dir - popd echo "Running Kani autoharness codegen command..." "$kani_path" autoharness -Z autoharness -Z unstable-options --std ./library \ --only-codegen -j --output-format=terse \ @@ -331,6 +326,10 @@ main() { $command_args \ --enable-unstable \ --cbmc-args --object-bits 12 + echo "Running Kani's std-analysis command..." + pushd scripts/kani-std-analysis + ./std-analysis.sh $build_dir + popd echo "Running autoharness-analyzer command..." git clone https://github.com/carolynzech/autoharness_analyzer cd autoharness_analyzer From c2dd4da39483886adb90f5cfd9789307ef1affa0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 10:55:55 +0000 Subject: [PATCH 5/9] Remove file --- scripts/run-kani.sh | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index daa1efff313d1..279deb698038a 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -326,6 +326,9 @@ main() { $command_args \ --enable-unstable \ --cbmc-args --object-bits 12 + # remove metadata file for Kani-generated "dummy" crate that we won't + # get scanner data for + rm ../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/dummy-* echo "Running Kani's std-analysis command..." pushd scripts/kani-std-analysis ./std-analysis.sh $build_dir From fef4e96b5bd312daff6decd42c41bab63c7a7a2e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 11:44:39 +0000 Subject: [PATCH 6/9] Fix path --- 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 279deb698038a..8924fac783f8e 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -328,7 +328,7 @@ main() { --cbmc-args --object-bits 12 # remove metadata file for Kani-generated "dummy" crate that we won't # get scanner data for - rm ../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/dummy-* + rm target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/dummy-* echo "Running Kani's std-analysis command..." pushd scripts/kani-std-analysis ./std-analysis.sh $build_dir From a8b90786560ab7b8248f4119b017ab86dc9d0c34 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 16:33:20 +0000 Subject: [PATCH 7/9] Limit clone depth, add new per-crate option --- scripts/run-kani.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 8924fac783f8e..dc185bb180590 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -334,9 +334,9 @@ main() { ./std-analysis.sh $build_dir popd echo "Running autoharness-analyzer command..." - git clone https://github.com/carolynzech/autoharness_analyzer + git clone --depth 1 https://github.com/carolynzech/autoharness_analyzer cd autoharness_analyzer - cargo run \ + cargo run --per-crate \ ../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \ /tmp/std_lib_analysis/results/ fi From 519c2277ff3a5553abb98c040de8bbebadf0d36c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 16:36:48 +0000 Subject: [PATCH 8/9] Fix syntax --- 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 dc185bb180590..ecc9e2c75bad5 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -336,7 +336,7 @@ main() { echo "Running autoharness-analyzer command..." git clone --depth 1 https://github.com/carolynzech/autoharness_analyzer cd autoharness_analyzer - cargo run --per-crate \ + cargo run -- --per-crate \ ../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \ /tmp/std_lib_analysis/results/ fi From efb3a9f812770790ea69fc1d59fec7ace882dcc7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 28 Apr 2025 16:42:42 +0000 Subject: [PATCH 9/9] Add unsafe data, fix file names, section headings --- .github/workflows/kani.yml | 11 ++++++++++- scripts/run-kani.sh | 3 +++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 3af27ee746961..7ca0ca81b8ea8 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -96,4 +96,13 @@ jobs: # Step 3: Add output to job summary - name: Add Autoharness Analyzer output to job summary - run: cat autoharness_analyzer/autoharness_data.md >> "$GITHUB_STEP_SUMMARY" + run: | + echo "# Autoharness Failure Summary" >> "$GITHUB_STEP_SUMMARY" + echo "## Crate core, all functions" >> "$GITHUB_STEP_SUMMARY" + cat autoharness_analyzer/core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY" + echo "## Crate core, unsafe functions" >> "$GITHUB_STEP_SUMMARY" + cat autoharness_analyzer/core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY" + echo "## Crate std, all functions" >> "$GITHUB_STEP_SUMMARY" + cat autoharness_analyzer/std_autoharness_data.md >> "$GITHUB_STEP_SUMMARY" + echo "## Crate std, unsafe functions" >> "$GITHUB_STEP_SUMMARY" + cat autoharness_analyzer/std_unsafe_autoharness_data.md >> "$GITHUB_STEP_SUMMARY" diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index ecc9e2c75bad5..d3edc34bc064a 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -339,6 +339,9 @@ main() { cargo run -- --per-crate \ ../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \ /tmp/std_lib_analysis/results/ + cargo run -- --per-crate --unsafe-fns-only \ + ../target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps/ \ + /tmp/std_lib_analysis/results/ fi }