Skip to content

Commit

Permalink
Move std-analysis.sh script from Kani repository (#261)
Browse files Browse the repository at this point in the history
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. This will re-enable
successfully gathering metrics.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
tautschnig authored Mar 4, 2025
1 parent 0027317 commit 214f966
Show file tree
Hide file tree
Showing 2 changed files with 122 additions and 4 deletions.
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 @@ -304,11 +304,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

0 comments on commit 214f966

Please sign in to comment.