Skip to content

Commit ab4179e

Browse files
authored
Track metrics for core and std crates, add loop metrics (#258)
The crate that we compute metrics for is now configurable when invoking `kani_std_analysis.py`. Should we find a need for further crates beyond `core` or `std` we just need to invoke it more times. We are now also reporting loop/no-loop information across all the kinds of functions we are tracking as metrics. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 18c4e95 commit ab4179e

8 files changed

Lines changed: 176 additions & 40 deletions

File tree

doc/mdbook-metrics/src/main.rs

Lines changed: 27 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,25 @@ fn run_kani_metrics_script() -> Result<(), Error> {
4444
Command::new("python")
4545
.args(&[
4646
"kani_std_analysis.py",
47+
"--crate",
48+
"core",
49+
"--metrics-file",
50+
"metrics-data-core.json",
51+
"--plot-only",
52+
"--plot-dir",
53+
&tools_path.to_string_lossy(),
54+
])
55+
.stdout(std::process::Stdio::null())
56+
.stderr(std::process::Stdio::null())
57+
.status()?;
58+
59+
Command::new("python")
60+
.args(&[
61+
"kani_std_analysis.py",
62+
"--crate",
63+
"std",
64+
"--metrics-file",
65+
"metrics-data-std.json",
4766
"--plot-only",
4867
"--plot-dir",
4968
&tools_path.to_string_lossy(),
@@ -83,12 +102,19 @@ fn add_graphs(chapter: &mut Chapter) {
83102
84103
Note that these metrics are for x86-64 architectures.
85104
86-
## `core`
105+
### `core`
87106
![Unsafe Metrics](core_unsafe_metrics.png)
88107
89108
![Safe Abstractions Metrics](core_safe_abstractions_metrics.png)
90109
91110
![Safe Metrics](core_safe_metrics.png)
111+
112+
### `std`
113+
![Unsafe Metrics](std_unsafe_metrics.png)
114+
115+
![Safe Abstractions Metrics](std_safe_abstractions_metrics.png)
116+
117+
![Safe Metrics](std_safe_metrics.png)
92118
"#;
93119

94120
chapter.content.push_str(new_content);

library/stdarch

Submodule stdarch updated 190 files

scripts/kani-std-analysis/kani_std_analysis.py

Lines changed: 137 additions & 35 deletions
Large diffs are not rendered by default.
File renamed without changes.
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
{
2+
"results": [
3+
]
4+
}

scripts/kani-std-analysis/std-analysis.sh

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,6 @@ then
6565
fi
6666
cargo new std_lib_analysis --lib
6767
cd std_lib_analysis
68-
sed -i '1i cargo-features = ["edition2024"]' Cargo.toml
6968

7069
echo '
7170
pub fn dummy() {

scripts/run-kani.sh

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -309,7 +309,12 @@ main() {
309309
./std-analysis.sh $build_dir
310310
pip install -r requirements.txt
311311
echo "Computing Kani-specific metrics..."
312-
./kani_std_analysis.py --kani-list-file $current_dir/kani-list.json
312+
./kani_std_analysis.py --crate core \
313+
--kani-list-file $current_dir/kani-list.json \
314+
--metrics-file metrics-data-core.json
315+
./kani_std_analysis.py --crate std \
316+
--kani-list-file $current_dir/kani-list.json \
317+
--metrics-file metrics-data-std.json
313318
popd
314319
rm kani-list.json
315320
fi

0 commit comments

Comments
 (0)