Skip to content

Commit b30d70d

Browse files
committed
Move std-analysis.sh script from Kani repository
Copied from model-checking/kani@8d46dc61d89b8b1cb8a with the change that the generated Cargo.toml is forced to edition2024 support to make it work with Rust releases after 2025-02-26.
1 parent eef04d8 commit b30d70d

File tree

2 files changed

+118
-4
lines changed

2 files changed

+118
-4
lines changed
+116
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
#!/usr/bin/env bash
2+
# Copyright Kani Contributors
3+
# SPDX-License-Identifier: Apache-2.0 OR MIT
4+
5+
# Collect some metrics related to the crates that compose the standard library.
6+
#
7+
# Files generates so far:
8+
#
9+
# - ${crate}_scan_overall.csv: Summary of function metrics, such as safe vs unsafe.
10+
# - ${crate}_scan_input_tys.csv: Detailed information about the inputs' type of each
11+
# function found in this crate.
12+
#
13+
# How we collect metrics:
14+
#
15+
# - Compile the standard library using the `scan` tool to collect some metrics.
16+
# - After compilation, move all CSV files that were generated by the scanner,
17+
# to the results folder.
18+
set -eu
19+
20+
# Test for platform
21+
PLATFORM=$(uname -sp)
22+
if [[ $PLATFORM == "Linux x86_64" ]]
23+
then
24+
TARGET="x86_64-unknown-linux-gnu"
25+
# 'env' necessary to avoid bash built-in 'time'
26+
WRAPPER="env time -v"
27+
elif [[ $PLATFORM == "Darwin i386" ]]
28+
then
29+
TARGET="x86_64-apple-darwin"
30+
# mac 'time' doesn't have -v
31+
WRAPPER="time"
32+
elif [[ $PLATFORM == "Darwin arm" ]]
33+
then
34+
TARGET="aarch64-apple-darwin"
35+
# mac 'time' doesn't have -v
36+
WRAPPER="time"
37+
else
38+
echo
39+
echo "Std-Lib codegen regression only works on Linux or OSX x86 platforms, skipping..."
40+
echo
41+
exit 0
42+
fi
43+
44+
# Get Kani root
45+
SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
46+
KANI_DIR=$(dirname "$SCRIPT_DIR")
47+
48+
echo "-------------------------------------------------------"
49+
echo "-- Starting analysis of the Rust standard library... --"
50+
echo "-------------------------------------------------------"
51+
52+
echo "-- Build scanner"
53+
cd $KANI_DIR
54+
cargo build -p scanner
55+
56+
echo "-- Build std"
57+
cd /tmp
58+
if [ -d std_lib_analysis ]
59+
then
60+
rm -rf std_lib_analysis
61+
fi
62+
cargo new std_lib_analysis --lib
63+
cd std_lib_analysis
64+
sed -i '1i cargo-features = ["edition2024"]' Cargo.toml
65+
66+
echo '
67+
pub fn dummy() {
68+
}
69+
' > src/lib.rs
70+
71+
# Use same nightly toolchain used to build Kani
72+
cp ${KANI_DIR}/rust-toolchain.toml .
73+
74+
export RUST_BACKTRACE=1
75+
export RUSTC_LOG=error
76+
77+
RUST_FLAGS=(
78+
"-Cpanic=abort"
79+
"-Zalways-encode-mir"
80+
)
81+
export RUSTFLAGS="${RUST_FLAGS[@]}"
82+
export RUSTC="$KANI_DIR/target/debug/scan"
83+
# Compile rust with our extension
84+
$WRAPPER cargo build --verbose -Z build-std --lib --target $TARGET
85+
86+
echo "-- Process results"
87+
88+
# Move files to results folder
89+
results=/tmp/std_lib_analysis/results
90+
mkdir $results
91+
find /tmp/std_lib_analysis/target -name "*.csv" -exec mv {} $results \;
92+
93+
# Create a summary table
94+
summary=$results/summary.csv
95+
96+
# write header
97+
echo -n "crate," > $summary
98+
tr -d "[:digit:],;" < $results/alloc_scan_overall.csv \
99+
| tr -s '\n' ',' >> $summary
100+
echo "" >> $summary
101+
102+
# write body
103+
for f in $results/*overall.csv; do
104+
# Join all crate summaries into one table
105+
fname=$(basename $f)
106+
crate=${fname%_scan_overall.csv}
107+
echo -n "$crate," >> $summary
108+
tr -d '[:alpha:]_,;' < $f | tr -s '\n' ',' \
109+
>> $summary
110+
echo "" >> $summary
111+
done
112+
113+
echo "-------------------------------------------------------"
114+
echo "Finished analysis successfully..."
115+
echo "- See results at ${results}"
116+
echo "-------------------------------------------------------"

scripts/run-kani.sh

+2-4
Original file line numberDiff line numberDiff line change
@@ -302,11 +302,9 @@ main() {
302302
local current_dir=$(pwd)
303303
echo "Running Kani list command..."
304304
"$kani_path" list -Z list $unstable_args ./library --std --format json
305-
echo "Running Kani's std-analysis command..."
306-
pushd $build_dir
307-
./scripts/std-analysis.sh
308-
popd
309305
pushd scripts/kani-std-analysis
306+
echo "Running Kani's std-analysis command..."
307+
./std-analysis.sh
310308
pip install -r requirements.txt
311309
echo "Computing Kani-specific metrics..."
312310
./kani_std_analysis.py --kani-list-file $current_dir/kani-list.json

0 commit comments

Comments
 (0)