Track metrics for core and std crates

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.

Author: tautschnig

doc/mdbook-metrics/src/main.rs

@@ -44,6 +44,21 @@ fn run_kani_metrics_script() -> Result<(), Error> {
     Command::new("python")
         .args(&[
             "kani_std_analysis.py",
+            "--crate",
+            "core",
+            "--plot-only",
+            "--plot-dir",
+            &tools_path.to_string_lossy(),
+        ])
+        .stdout(std::process::Stdio::null())
+        .stderr(std::process::Stdio::null())
+        .status()?;
+
+    Command::new("python")
+        .args(&[
+            "kani_std_analysis.py",
+            "--crate",
+            "std",
             "--plot-only",
             "--plot-dir",
             &tools_path.to_string_lossy(),
@@ -83,12 +98,19 @@ fn add_graphs(chapter: &mut Chapter) {
 
 Note that these metrics are for x86-64 architectures.
 
-## `core`
+### `core`
 ![Unsafe Metrics](core_unsafe_metrics.png)
 
 ![Safe Abstractions Metrics](core_safe_abstractions_metrics.png)
 
 ![Safe Metrics](core_safe_metrics.png)
+
+### `std`
+![Unsafe Metrics](std_unsafe_metrics.png)
+
+![Safe Abstractions Metrics](std_safe_abstractions_metrics.png)
+
+![Safe Metrics](std_safe_metrics.png)
 "#;
 
     chapter.content.push_str(new_content);

scripts/kani-std-analysis/kani_std_analysis.py

@@ -28,10 +28,10 @@
 # - See #TODOs for known limitations.
 
 # Process the results from Kani's std-analysis.sh script for each crate.
-# TODO For now, we just handle "core", but we should process all crates in the library.
 class GenericSTDMetrics():
-    def __init__(self, results_dir):
+    def __init__(self, results_dir, crate):
         self.results_directory = results_dir
+        self.crate = crate
         self.unsafe_fns_count = 0
         self.safe_abstractions_count = 0
         self.safe_fns_count = 0
@@ -44,7 +44,7 @@ def __init__(self, results_dir):
     # Read {crate}_overall_counts.csv
     # and return the number of unsafe functions and safe abstractions
     def read_overall_counts(self):
-        file_path = f"{self.results_directory}/core_scan_overall.csv"
+        file_path = f"{self.results_directory}/{self.crate}_scan_overall.csv"
         with open(file_path, 'r') as f:
             csv_reader = csv.reader(f, delimiter=';')
             counts = {row[0]: int(row[1]) for row in csv_reader if len(row) >= 2}
@@ -56,7 +56,7 @@ def read_overall_counts(self):
     # and return an array of the unsafe functions and the safe abstractions
     def read_scan_functions(self):
         expected_header_start = "name;is_unsafe;has_unsafe_ops"
-        file_path = f"{self.results_directory}/core_scan_functions.csv"
+        file_path = f"{self.results_directory}/{self.crate}_scan_functions.csv"
 
         with open(file_path, 'r') as f:
             csv_reader = csv.reader(f, delimiter=';', quotechar='"')
@@ -90,19 +90,19 @@ def read_std_analysis(self):
 
         # Sanity checks
         if len(self.unsafe_fns) != self.unsafe_fns_count:
-            print(f"Number of unsafe functions does not match core_scan_functions.csv")
+            print(f"Number of unsafe functions does not match {self.crate}_scan_functions.csv")
             print(f"UNSAFE_FNS_COUNT: {self.unsafe_fns_count}")
             print(f"UNSAFE_FNS length: {len(self.unsafe_fns)}")
             sys.exit(1)
 
         if len(self.safe_abstractions) != self.safe_abstractions_count:
-            print(f"Number of safe abstractions does not match core_scan_functions.csv")
+            print(f"Number of safe abstractions does not match {self.crate}_scan_functions.csv")
             print(f"SAFE_ABSTRACTIONS_COUNT: {self.safe_abstractions_count}")
             print(f"SAFE_ABSTRACTIONS length: {len(self.safe_abstractions)}")
             sys.exit(1)
 
         if len(self.safe_fns) != self.safe_fns_count:
-            print(f"Number of safe functions does not match core_scan_functions.csv")
+            print(f"Number of safe functions does not match {self.crate}_scan_functions.csv")
             print(f"SAFE_FNS_COUNT: {self.safe_fns_count}")
             print(f"SAFE_FNS length: {len(self.safe_fns)}")
             sys.exit(1)
@@ -140,7 +140,8 @@ def read_kani_list_data(self, kani_list_filepath):
 # Generate metrics about Kani's application to the standard library over time
 # by reading past metrics from metrics_file, then computing today's metrics.
 class KaniSTDMetricsOverTime():
-    def __init__(self, metrics_file):
+    def __init__(self, metrics_file, crate):
+        self.crate = crate
         self.dates = []
         self.unsafe_metrics = ['total_unsafe_fns', 'unsafe_fns_under_contract', 'verified_unsafe_fns_under_contract']
         self.safe_abstr_metrics = ['total_safe_abstractions', 'safe_abstractions_under_contract', 'verified_safe_abstractions_under_contract']
@@ -190,7 +191,7 @@ def compute_metrics(self, kani_list_filepath, analysis_results_dir):
 
         # Process the `kani list` and `std-analysis.sh` data
         kani_data = KaniListSTDMetrics(kani_list_filepath)
-        generic_metrics = GenericSTDMetrics(analysis_results_dir)
+        generic_metrics = GenericSTDMetrics(analysis_results_dir, self.crate)
 
         print("Comparing kani-list output to std-analysis.sh output and computing metrics...")
 
@@ -280,12 +281,28 @@ def plot_single(self, data, title, filename, plot_dir):
         print(f"PNG graph generated: {outfile}")
 
     def plot(self, plot_dir):
-        self.plot_single(self.unsafe_plot_data, title="Contracts on Unsafe Functions in core", filename="core_unsafe_metrics.png", plot_dir=plot_dir)
-        self.plot_single(self.safe_abstr_plot_data, title="Contracts on Safe Abstractions in core", filename="core_safe_abstractions_metrics.png", plot_dir=plot_dir)
-        self.plot_single(self.safe_plot_data, title="Contracts on Safe Functions in core", filename="core_safe_metrics.png", plot_dir=plot_dir)
+        self.plot_single(
+            self.unsafe_plot_data,
+            title=f"Contracts on Unsafe Functions in {self.crate}",
+            filename=f"{self.crate}_unsafe_metrics.png",
+            plot_dir=plot_dir)
+        self.plot_single(
+            self.safe_abstr_plot_data,
+            title=f"Contracts on Safe Abstractions in {self.crate}",
+            filename=f"{self.crate}_safe_abstractions_metrics.png",
+            plot_dir=plot_dir)
+        self.plot_single(
+            self.safe_plot_data,
+            title=f"Contracts on Safe Functions in {self.crate}",
+            filename=f"{self.crate}_safe_metrics.png",
+            plot_dir=plot_dir)
 
 def main():
     parser = argparse.ArgumentParser(description="Generate metrics about Kani's application to the standard library.")
+    parser.add_argument('--crate',
+                    type=str,
+                    required=True,
+                    help="Name of standard library crate to produce metrics for")
     parser.add_argument('--metrics-file', 
                     type=str, 
                     default="metrics-data.json", 
@@ -308,7 +325,7 @@ def main():
 
     args = parser.parse_args()
 
-    metrics = KaniSTDMetricsOverTime(args.metrics_file)
+    metrics = KaniSTDMetricsOverTime(args.metrics_file, args.crate)
 
     if args.plot_only:
         metrics.plot(args.plot_dir)

scripts/kani-std-analysis/metrics-data.json renamed to scripts/kani-std-analysis/metrics-data-core.json

@@ -0,0 +1,4 @@
+{
+  "results": [
+  ]
+}

scripts/kani-std-analysis/metrics-data-std.json

@@ -309,7 +309,8 @@ main() {
         pushd scripts/kani-std-analysis
         pip install -r requirements.txt
         echo "Computing Kani-specific metrics..."
-        ./kani_std_analysis.py --kani-list-file $current_dir/kani-list.json
+        ./kani_std_analysis.py --crate core --kani-list-file $current_dir/kani-list.json
+        ./kani_std_analysis.py --crate std --kani-list-file $current_dir/kani-list.json
         popd
         rm kani-list.json
     fi