Skip to content

Move std-analysis.sh script from Kani repository #261

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Mar 4, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
120 changes: 120 additions & 0 deletions scripts/kani-std-analysis/std-analysis.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,120 @@
#!/usr/bin/env bash
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT

# Collect some metrics related to the crates that compose the standard library.
#
# Files generates so far:
#
# - ${crate}_scan_overall.csv: Summary of function metrics, such as safe vs unsafe.
# - ${crate}_scan_input_tys.csv: Detailed information about the inputs' type of each
# function found in this crate.
#
# How we collect metrics:
#
# - Compile the standard library using the `scan` tool to collect some metrics.
# - After compilation, move all CSV files that were generated by the scanner,
# to the results folder.
set -eu

# Test for platform
PLATFORM=$(uname -sp)
if [[ $PLATFORM == "Linux x86_64" ]]
then
TARGET="x86_64-unknown-linux-gnu"
# 'env' necessary to avoid bash built-in 'time'
WRAPPER="env time -v"
elif [[ $PLATFORM == "Darwin i386" ]]
then
TARGET="x86_64-apple-darwin"
# mac 'time' doesn't have -v
WRAPPER="time"
elif [[ $PLATFORM == "Darwin arm" ]]
then
TARGET="aarch64-apple-darwin"
# mac 'time' doesn't have -v
WRAPPER="time"
else
echo
echo "Std-Lib codegen regression only works on Linux or OSX x86 platforms, skipping..."
echo
exit 0
fi

# Get Kani root
if [[ $# -ne 1 ]]
then
echo "Required command-line argument <KANI-DIR> missing"
exit 1
fi
KANI_DIR=$1

echo "-------------------------------------------------------"
echo "-- Starting analysis of the Rust standard library... --"
echo "-------------------------------------------------------"

echo "-- Build scanner"
cd $KANI_DIR
cargo build -p scanner

echo "-- Build std"
cd /tmp
if [ -d std_lib_analysis ]
then
rm -rf std_lib_analysis
fi
cargo new std_lib_analysis --lib
cd std_lib_analysis
sed -i '1i cargo-features = ["edition2024"]' Cargo.toml

echo '
pub fn dummy() {
}
' > src/lib.rs

# Use same nightly toolchain used to build Kani
cp ${KANI_DIR}/rust-toolchain.toml .

export RUST_BACKTRACE=1
export RUSTC_LOG=error

RUST_FLAGS=(
"-Cpanic=abort"
"-Zalways-encode-mir"
)
export RUSTFLAGS="${RUST_FLAGS[@]}"
export RUSTC="$KANI_DIR/target/debug/scan"
# Compile rust with our extension
$WRAPPER cargo build --verbose -Z build-std --lib --target $TARGET

echo "-- Process results"

# Move files to results folder
results=/tmp/std_lib_analysis/results
mkdir $results
find /tmp/std_lib_analysis/target -name "*.csv" -exec mv {} $results \;

# Create a summary table
summary=$results/summary.csv

# write header
echo -n "crate," > $summary
tr -d "[:digit:],;" < $results/alloc_scan_overall.csv \
| tr -s '\n' ',' >> $summary
echo "" >> $summary

# write body
for f in $results/*overall.csv; do
# Join all crate summaries into one table
fname=$(basename $f)
crate=${fname%_scan_overall.csv}
echo -n "$crate," >> $summary
tr -d '[:alpha:]_,;' < $f | tr -s '\n' ',' \
>> $summary
echo "" >> $summary
done

echo "-------------------------------------------------------"
echo "Finished analysis successfully..."
echo "- See results at ${results}"
echo "-------------------------------------------------------"
6 changes: 2 additions & 4 deletions scripts/run-kani.sh
Original file line number Diff line number Diff line change
Expand Up @@ -302,11 +302,9 @@ main() {
local current_dir=$(pwd)
echo "Running Kani list command..."
"$kani_path" list -Z list $unstable_args ./library --std --format json
echo "Running Kani's std-analysis command..."
pushd $build_dir
./scripts/std-analysis.sh
popd
pushd scripts/kani-std-analysis
echo "Running Kani's std-analysis command..."
./std-analysis.sh $build_dir
pip install -r requirements.txt
echo "Computing Kani-specific metrics..."
./kani_std_analysis.py --kani-list-file $current_dir/kani-list.json
Expand Down
Loading