diff --git a/metrics-data.json b/metrics-data.json deleted file mode 100644 index 9e9aceefc0b7..000000000000 --- a/metrics-data.json +++ /dev/null @@ -1,28 +0,0 @@ -{ - "results": [ - { - "date": "2024-12-01", - "total_unsafe_fns": 4552, - "total_safe_abstractions": 1748, - "unsafe_fns_under_contract": 109, - "verified_unsafe_fns_under_contract": 99, - "safe_abstractions_under_contract": 40, - "verified_safe_abstractions_under_contract": 40, - "safe_fns_under_contract": 18, - "verified_safe_fns_under_contract": 18, - "total_functions_under_contract": 167 - }, - { - "date": "2025-01-01", - "total_unsafe_fns": 4552, - "total_safe_abstractions": 1748, - "unsafe_fns_under_contract": 143, - "verified_unsafe_fns_under_contract": 132, - "safe_abstractions_under_contract": 41, - "verified_safe_abstractions_under_contract": 41, - "safe_fns_under_contract": 39, - "verified_safe_fns_under_contract": 38, - "total_functions_under_contract": 223 - } - ] -} \ No newline at end of file diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py index 62a40d7362a0..81c96db6cc3a 100755 --- a/scripts/kani-std-analysis/kani_std_analysis.py +++ b/scripts/kani-std-analysis/kani_std_analysis.py @@ -16,6 +16,8 @@ # 3. Comparing the output of steps #1 and #2 to compare the Kani-verified portion of the standard library to the overall library, # e.g., what fraction of unsafe functions have Kani contracts. # Note that this script assumes that std-analysis.sh and `kani list` have already run, since we expect to invoke this script from `run-kani.sh`. +# Also note that the results are architecture-dependent: the standard library has functions that are only present for certain architectures, +# and https://github.com/model-checking/verify-rust-std/pull/122 has Kani harnesses that only run on x86-64. # Process the results from Kani's std-analysis.sh script for each crate. # TODO For now, we just handle "core", but we should process all crates in the library. @@ -256,13 +258,13 @@ def plot(self): def main(): parser = argparse.ArgumentParser(description="Generate metrics about Kani's application to the standard library.") parser.add_argument('--metrics-file', - type=str, - required=True, - help="Path to the JSON file containing metrics data") + type=str, + default="metrics-data.json", + help="Path to the JSON file containing metrics data (default: metrics-data.json)") parser.add_argument('--kani-list-file', - type=str, - required=True, - help="Path to the JSON file containing the Kani list data") + type=str, + default="kani-list.json", + help="Path to the JSON file containing the Kani list data (default: kani-list.json)") args = parser.parse_args() metrics = KaniSTDMetricsOverTime(args.metrics_file) diff --git a/scripts/kani-std-analysis/metrics-data.json b/scripts/kani-std-analysis/metrics-data.json new file mode 100644 index 000000000000..855007af7958 --- /dev/null +++ b/scripts/kani-std-analysis/metrics-data.json @@ -0,0 +1,16 @@ +{ + "results": [ + { + "date": "2025-01-01", + "total_unsafe_fns": 6987, + "total_safe_abstractions": 1704, + "unsafe_fns_under_contract": 144, + "verified_unsafe_fns_under_contract": 132, + "safe_abstractions_under_contract": 41, + "verified_safe_abstractions_under_contract": 41, + "safe_fns_under_contract": 39, + "verified_safe_fns_under_contract": 38, + "total_functions_under_contract": 224 + } + ] +} \ No newline at end of file diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 06a377cb54c7..a86526d3fc0e 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -297,17 +297,17 @@ main() { echo "Running Kani list command..." "$kani_path" list -Z list $unstable_args ./library --std --format markdown elif [[ "$run_command" == "metrics" ]]; then - local current_dir=$(pwd) echo "Computing Kani-specific metrics..." echo "Running Kani list command..." "$kani_path" list -Z list $unstable_args ./library --std --format json + mv $(pwd)/kani-list.json scripts/kani-std-analysis/kani-list.json echo "Running Kani's std-analysis command..." pushd $build_dir ./scripts/std-analysis.sh popd pushd scripts/kani-std-analysis pip install -r requirements.txt - ./kani_std_analysis.py --metrics-file ${current_dir}/metrics-data.json --kani-list-file ${current_dir}/kani-list.json + ./kani_std_analysis.py popd fi }