diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 90463ec8574c6..7ca0ca81b8ea8 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -79,3 +79,30 @@ 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: | + 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 200bd957180d6..d3edc34bc064a 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,31 @@ main() { --metrics-file metrics-data-std.json popd rm kani-list.json + elif [[ "$run_command" == "autoharness-analyzer" ]]; then + 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 + # 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 + popd + echo "Running autoharness-analyzer command..." + git clone --depth 1 https://github.com/carolynzech/autoharness_analyzer + cd autoharness_analyzer + 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 }