Add code scanner tool (#3120)

This is just a utility tool that allow us to scan a crate and extract
some metrics out of it. I also added a script to scan the standard
library.

Currently, the tool will produce a few CSV files with raw data.

---------

Co-authored-by: Qinheping Hu <qinhh@amazon.com>

Cargo.lock

@@ -288,6 +288,27 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "csv"
+version = "1.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ac574ff4d437a7b5ad237ef331c17ccca63c46479e5b5453eb8e10bb99a759fe"
+dependencies = [
+ "csv-core",
+ "itoa",
+ "ryu",
+ "serde",
+]
+
+[[package]]
+name = "csv-core"
+version = "0.1.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5efa2b3d7902f4b634a20cae3c9c4e6209dc4779feb6863329607560143efa70"
+dependencies = [
+ "memchr",
+]
+
 [[package]]
 name = "either"
 version = "1.13.0"
@@ -892,6 +913,16 @@ dependencies = [
  "winapi-util",
 ]
 
+[[package]]
+name = "scanner"
+version = "0.0.0"
+dependencies = [
+ "csv",
+ "serde",
+ "strum",
+ "strum_macros",
+]
+
 [[package]]
 name = "scopeguard"
 version = "1.2.0"

Cargo.toml

@@ -40,6 +40,7 @@ members = [
  "library/std",
  "tools/compiletest",
  "tools/build-kani",
+ "tools/scanner",
  "kani-driver",
  "kani-compiler",
  "kani_metadata",

scripts/std-analysis.sh

@@ -0,0 +1,115 @@
+#!/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
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+KANI_DIR=$(dirname "$SCRIPT_DIR")
+
+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
+
+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 "-------------------------------------------------------"

tests/script-based-pre/tool-scanner/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: scanner-test.sh
+expected: scanner-test.expected

tests/script-based-pre/tool-scanner/scanner-test.expected

@@ -0,0 +1,6 @@
+2 test_scan_fn_loops.csv
+16 test_scan_functions.csv
+5 test_scan_input_tys.csv
+14 test_scan_overall.csv
+3 test_scan_recursion.csv
+5 test_scan_unsafe_ops.csv

tests/script-based-pre/tool-scanner/scanner-test.sh

@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -e
+
+# Run this inside a tmp folder in the current directory
+OUT_DIR=output_dir
+# Ensure output folder is clean
+rm -rf ${OUT_DIR}
+mkdir output_dir
+# Move the original source to the output folder since it will be modified
+cp test.rs ${OUT_DIR}
+pushd $OUT_DIR
+
+cargo run -p scanner test.rs --crate-type lib
+wc -l *csv
+
+popd
+rm -rf ${OUT_DIR}

tests/script-based-pre/tool-scanner/test.rs

@@ -0,0 +1,77 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Sanity check for the utility tool `scanner`.
+
+pub fn check_outer_coercion() {
+ assert!(false);
+}
+
+unsafe fn do_nothing() {}
+
+pub fn generic<T: Default>() -> T {
+ unsafe { do_nothing() };
+ T::default()
+}
+
+pub struct RecursiveType {
+ pub inner: Option<*const RecursiveType>,
+}
+
+pub enum RecursiveEnum {
+ Base,
+ Recursion(Box<RecursiveEnum>),
+ RefCell(std::cell::RefCell<f32>),
+}
+
+pub fn recursive_type(input1: RecursiveType, input2: RecursiveEnum) {
+ let _ = (input1, input2);
+}
+
+pub fn with_iterator(input: &[usize]) -> usize {
+ input
+ .iter()
+ .copied()
+ .find(|e| *e == 0)
+ .unwrap_or_else(|| input.iter().fold(0, |acc, i| acc + 1))
+}
+
+static mut COUNTER: Option<usize> = Some(0);
+static OK: bool = true;
+
+pub unsafe fn next_id() -> usize {
+ let sum = COUNTER.unwrap() + 1;
+ COUNTER = Some(sum);
+ sum
+}
+
+pub unsafe fn current_id() -> usize {
+ COUNTER.unwrap()
+}
+
+pub fn ok() -> bool {
+ OK
+}
+
+pub unsafe fn raw_to_ref<'a, T>(raw: *const T) -> &'a T {
+ &*raw
+}
+
+pub fn recursion_begin(stop: bool) {
+ if !stop {
+ recursion_tail()
+ }
+}
+
+pub fn recursion_tail() {
+ recursion_begin(false);
+ not_recursive();
+}
+
+pub fn start_recursion() {
+ recursion_begin(true);
+}
+
+pub fn not_recursive() {
+ let _ = ok();
+}

tools/scanner/Cargo.toml

@@ -0,0 +1,23 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+
+[package]
+name = "scanner"
+description = "A rustc extension used to scan rust features in a crate"
+version = "0.0.0"
+edition = "2021"
+license = "MIT OR Apache-2.0"
+publish = false
+
+[dependencies]
+csv = "1.3"
+serde = {version = "1", features = ["derive"]}
+strum = "0.26"
+strum_macros = "0.26"
+
+[package.metadata.rust-analyzer]
+# This crate uses rustc crates.
+# More info: https://github.com/rust-analyzer/rust-analyzer/pull/7891
+rustc_private = true
+

tools/scanner/build.rs

@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use std::env;
+use std::path::PathBuf;
+
+macro_rules! path_str {
+ ($input:expr) => {
+ String::from(
+ $input
+ .iter()
+ .collect::<PathBuf>()
+ .to_str()
+ .unwrap_or_else(|| panic!("Invalid path {}", stringify!($input))),
+ )
+ };
+}
+
+/// Configure the compiler to properly link the scanner binary with rustc's library.
+pub fn main() {
+ // Add rustup to the rpath in order to properly link with the correct rustc version.
+ let rustup_home = env::var("RUSTUP_HOME").unwrap();
+ let rustup_tc = env::var("RUSTUP_TOOLCHAIN").unwrap();
+ let rustup_lib = path_str!([&rustup_home, "toolchains", &rustup_tc, "lib"]);
+ println!("cargo:rustc-link-arg-bin=scan=-Wl,-rpath,{rustup_lib}");
+}