Track metrics for core and std crates, add loop metrics (model-checking#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.

Author: tautschnig

doc/mdbook-metrics/src/main.rs

@@ -44,6 +44,25 @@ fn run_kani_metrics_script() -> Result<(), Error> {
     Command::new("python")
         .args(&[
             "kani_std_analysis.py",
+            "--crate",
+            "core",
+            "--metrics-file",
+            "metrics-data-core.json",
+            "--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",
+            "--metrics-file",
+            "metrics-data-std.json",
             "--plot-only",
             "--plot-dir",
             &tools_path.to_string_lossy(),
@@ -83,12 +102,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

@@ -27,24 +27,38 @@
 #   But `kani list` runs on this fork, so it can still see it and add it to the total functions under contract.
 # - See #TODOs for known limitations.
 
+def str_to_bool(string: str):
+    match string.strip().lower():
+        case "true":
+            return True
+        case "false":
+            return False
+        case _:
+            print(f"Unexpected to-be-Boolean string {string}")
+            sys.exit(1)
+
+
 # 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
         self.unsafe_fns = []
+        self.unsafe_fns_with_loop = []
         self.safe_abstractions = []
+        self.safe_abstractions_with_loop = []
         self.safe_fns = [] 
+        self.safe_fns_with_loop = []
 
         self.read_std_analysis()
 
     # 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}
@@ -55,54 +69,60 @@ def read_overall_counts(self):
     # Read {crate}_scan_functions.csv
     # 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"
+        expected_header_start = "name;is_unsafe;has_unsafe_ops;has_unsupported_input;has_loop"
+        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='"')
 
             # The row parsing logic below assumes the column structure in expected_header_start,
             # so assert that is how the header begins before continuing
             header = next(csv_reader)
-            header_str = ';'.join(header[:3])
+            header_str = ';'.join(header[:5])
             if not header_str.startswith(expected_header_start):
                 print(f"Error: Unexpected CSV header in {file_path}")
                 print(f"Expected header to start with: {expected_header_start}")
                 print(f"Actual header: {header_str}")
                 sys.exit(1)
 
             for row in csv_reader:
-                if len(row) >= 3:
+                if len(row) >= 5:
                     name, is_unsafe, has_unsafe_ops = row[0], row[1], row[2]
+                    has_unsupported_input, has_loop = row[3], row[4]
                     # An unsafe function is a function for which is_unsafe=true
-                    if is_unsafe.strip() == "true":
+                    if str_to_bool(is_unsafe):
                         self.unsafe_fns.append(name)
+                        if str_to_bool(has_loop):
+                            self.unsafe_fns_with_loop.append(name)
                     else:
-                        assert is_unsafe.strip() == "false" # sanity check against malformed data
                         self.safe_fns.append(name)
+                        if str_to_bool(has_loop):
+                            self.safe_fns_with_loop.append(name)
                         # A safe abstraction is a safe function with unsafe ops
-                        if has_unsafe_ops.strip() == "true":
+                        if str_to_bool(has_unsafe_ops):
                             self.safe_abstractions.append(name)
+                            if str_to_bool(has_loop):
+                                self.safe_abstractions_with_loop.append(name)
 
     def read_std_analysis(self):
         self.read_overall_counts()
         self.read_scan_functions()
 
         # 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,11 +160,33 @@ 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']
-        self.safe_metrics = ['total_safe_fns', 'safe_fns_under_contract', 'verified_safe_fns_under_contract']
+        self.unsafe_metrics = [
+                'total_unsafe_fns',
+                'total_unsafe_fns_with_loop',
+                'unsafe_fns_under_contract',
+                'unsafe_fns_with_loop_under_contract',
+                'verified_unsafe_fns_under_contract',
+                'verified_unsafe_fns_with_loop_under_contract'
+                ]
+        self.safe_abstr_metrics = [
+                'total_safe_abstractions',
+                'total_safe_abstractions_with_loop',
+                'safe_abstractions_under_contract',
+                'safe_abstractions_with_loop_under_contract',
+                'verified_safe_abstractions_under_contract',
+                'verified_safe_abstractions_with_loop_under_contract'
+                ]
+        self.safe_metrics = [
+                'total_safe_fns',
+                'total_safe_fns_with_loop',
+                'safe_fns_under_contract',
+                'safe_fns_with_loop_under_contract',
+                'verified_safe_fns_under_contract',
+                'verified_safe_fns_with_loop_under_contract'
+                ]
         # The keys in these dictionaries are unsafe_metrics, safe_abstr_metrics, and safe_metrics, respectively; see update_plot_metrics()
         self.unsafe_plot_data = defaultdict(list)
         self.safe_abstr_plot_data = defaultdict(list)
@@ -157,12 +199,9 @@ def __init__(self, metrics_file):
 
     # Read historical data from self.metrics_file and initialize the date range.    
     def read_historical_data(self):
-        try:
-            with open(self.metrics_file, 'r') as f:
-                all_data = json.load(f)["results"]
-                self.update_plot_metrics(all_data)
-        except FileNotFoundError:
-            all_data = {}
+        with open(self.metrics_file, 'r') as f:
+            all_data = json.load(f)["results"]
+            self.update_plot_metrics(all_data)
 
         self.dates = [datetime.strptime(data["date"], '%Y-%m-%d').date() for data in all_data]
 
@@ -173,15 +212,15 @@ def update_plot_metrics(self, all_data):
         for data in all_data:
             for metric in self.unsafe_metrics:
                 if not metric.startswith("verified"):
-                    self.unsafe_plot_data[metric].append(data[metric])
+                    self.unsafe_plot_data[metric].append(data.get(metric, 0))
 
             for metric in self.safe_abstr_metrics:
                 if not metric.startswith("verified"):
-                    self.safe_abstr_plot_data[metric].append(data[metric])
+                    self.safe_abstr_plot_data[metric].append(data.get(metric, 0))
 
             for metric in self.safe_metrics:
                 if not metric.startswith("verified"):
-                    self.safe_plot_data[metric].append(data[metric])
+                    self.safe_plot_data[metric].append(data.get(metric, 0))
 
     # Read output from kani list and std-analysis.sh, then compare their outputs to compute Kani-specific metrics
     # and write the results to {self.metrics_file}
@@ -190,41 +229,68 @@ 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...")
 
         (unsafe_fns_under_contract, verified_unsafe_fns_under_contract) = (0, 0)
+        unsafe_fns_with_loop_under_contract = 0
+        verified_unsafe_fns_with_loop_under_contract = 0
         (safe_abstractions_under_contract, verified_safe_abstractions_under_contract) = (0, 0)
+        safe_abstractions_with_loop_under_contract = 0
+        verified_safe_abstractions_with_loop_under_contract = 0
         (safe_fns_under_contract, verified_safe_fns_under_contract) = (0, 0)
+        safe_fns_with_loop_under_contract = 0
+        verified_safe_fns_with_loop_under_contract = 0
 
         for (func_under_contract, has_harnesses) in kani_data.fns_under_contract:
             if func_under_contract in generic_metrics.unsafe_fns:
+                has_loop = int(func_under_contract in
+                               generic_metrics.unsafe_fns_with_loop)
                 unsafe_fns_under_contract += 1
+                unsafe_fns_with_loop_under_contract += has_loop
                 if has_harnesses:
                     verified_unsafe_fns_under_contract += 1
+                    verified_unsafe_fns_with_loop_under_contract += has_loop
             if func_under_contract in generic_metrics.safe_abstractions:
+                has_loop = int(func_under_contract in
+                               generic_metrics.safe_abstractions_with_loop)
                 safe_abstractions_under_contract += 1
+                safe_abstractions_with_loop_under_contract += has_loop
                 if has_harnesses:
                     verified_safe_abstractions_under_contract += 1
+                    verified_safe_abstractions_with_loop_under_contract += has_loop
             if func_under_contract in generic_metrics.safe_fns:
+                has_loop = int(func_under_contract in
+                               generic_metrics.safe_fns_with_loop)
                 safe_fns_under_contract += 1
+                safe_fns_with_loop_under_contract += has_loop
                 if has_harnesses:
                     verified_safe_fns_under_contract += 1
+                    verified_safe_fns_with_loop_under_contract += has_loop
 
         # Keep the keys here in sync with unsafe_metrics, safe_metrics, and safe_abstr_metrics
         data = {
             "date": self.date,
             "total_unsafe_fns": generic_metrics.unsafe_fns_count,
+            "total_unsafe_fns_with_loop": len(generic_metrics.unsafe_fns_with_loop),
             "total_safe_abstractions": generic_metrics.safe_abstractions_count,
+            "total_safe_abstractions_with_loop": len(generic_metrics.safe_abstractions_with_loop),
             "total_safe_fns": generic_metrics.safe_fns_count,
+            "total_safe_fns_with_loop": len(generic_metrics.safe_fns_with_loop),
             "unsafe_fns_under_contract": unsafe_fns_under_contract,
+            "unsafe_fns_with_loop_under_contract": unsafe_fns_with_loop_under_contract,
             "verified_unsafe_fns_under_contract": verified_unsafe_fns_under_contract,
+            "verified_unsafe_fns_with_loop_under_contract": verified_unsafe_fns_with_loop_under_contract,
             "safe_abstractions_under_contract": safe_abstractions_under_contract,
+            "safe_abstractions_with_loop_under_contract": safe_abstractions_with_loop_under_contract,
             "verified_safe_abstractions_under_contract": verified_safe_abstractions_under_contract,
+            "verified_safe_abstractions_with_loop_under_contract": verified_safe_abstractions_with_loop_under_contract,
             "safe_fns_under_contract": safe_fns_under_contract,
+            "safe_fns_with_loop_under_contract": safe_fns_with_loop_under_contract,
             "verified_safe_fns_under_contract": verified_safe_fns_under_contract,
-            "total_functions_under_contract": kani_data.total_fns_under_contract,
+            "verified_safe_fns_with_loop_under_contract": verified_safe_fns_with_loop_under_contract,
+            "total_functions_under_contract_all_crates": kani_data.total_fns_under_contract,
         }
 
         self.update_plot_metrics([data])
@@ -243,7 +309,27 @@ def compute_metrics(self, kani_list_filepath, analysis_results_dir):
     def plot_single(self, data, title, filename, plot_dir):
         plt.figure(figsize=(14, 8))
 
-        colors = ['#1f77b4', '#ff7f0e', '#2ca02c', '#d62728', '#946F7bd', '#8c564b', '#e377c2', '#7f7f7f', '#bcbd22', '#17becf']
+        colors = [
+                '#1f77b4', #total_unsafe_fns
+                '#941fb4', #total_unsafe_fns_with_loop
+                '#ff7f0e', #total_safe_abstractions
+                '#abff0e', #total_safe_abstractions_with_loop
+                '#2ca02c', #total_safe_fns
+                '#a02c8d', #total_safe_fns_with_loop
+                '#d62728', #unsafe_fns_under_contract
+                '#27d6aa', #unsafe_fns_with_loop_under_contract
+                '#9467bd', #verified_unsafe_fns_under_contract
+                '#67acbd', #verified_unsafe_fns_with_loop_under_contract
+                '#8c564b', #safe_abstractions_under_contract
+                '#8c814b', #safe_abstractions_with_loop_under_contract
+                '#e377c2', #verified_safe_abstractions_under_contract
+                '#a277e3', #verified_safe_abstractions_with_loop_under_contract
+                '#7f7f7f', #safe_fns_under_contract
+                '#9e6767', #safe_fns_with_loop_under_contract
+                '#bcbd22', #verified_safe_fns_under_contract
+                '#49bd22', #verified_safe_fns_with_loop_under_contract
+                '#17becf' #total_functions_under_contract
+                ]
 
         for i, (metric, values) in enumerate(data.items()):
             color = colors[i % len(colors)]
@@ -280,16 +366,32 @@ 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", 
-                    help="Path to the JSON file containing metrics data (default: metrics-data.json)")
+                    required=True,
+                    help="Path to the JSON file containing metrics data")
     parser.add_argument('--kani-list-file', 
                     type=str, 
                     default="kani-list.json", 
@@ -308,7 +410,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

@@ -65,7 +65,6 @@ then
 fi
 cargo new std_lib_analysis --lib
 cd std_lib_analysis
-sed -i '1i cargo-features = ["edition2024"]' Cargo.toml
 
 echo '
 pub fn dummy() {