diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py index 81c96db6cc3aa..3dfbd9d7213b0 100755 --- a/scripts/kani-std-analysis/kani_std_analysis.py +++ b/scripts/kani-std-analysis/kani_std_analysis.py @@ -26,8 +26,10 @@ def __init__(self): self.results_directory = "/tmp/std_lib_analysis/results" self.unsafe_fns_count = 0 self.safe_abstractions_count = 0 + self.safe_fns_count = 0 self.unsafe_fns = [] self.safe_abstractions = [] + self.safe_fns = [] self.read_std_analysis() @@ -40,6 +42,7 @@ def read_overall_counts(self): counts = {row[0]: int(row[1]) for row in csv_reader if len(row) >= 2} self.unsafe_fns_count = counts.get('unsafe_fns', 0) self.safe_abstractions_count = counts.get('safe_abstractions', 0) + self.safe_fns_count = counts.get('safe_fns', 0) # Read {crate}_scan_functions.csv # and return an array of the unsafe functions and the safe abstractions @@ -66,15 +69,18 @@ def read_scan_functions(self): # An unsafe function is a function for which is_unsafe=true if is_unsafe.strip() == "true": self.unsafe_fns.append(name) - # A safe abstraction is a function that is not unsafe (is_unsafe=false) but has unsafe ops - elif is_unsafe.strip() == "false" and has_unsafe_ops.strip() == "true": - self.safe_abstractions.append(name) + else: + assert is_unsafe.strip() == "false" # sanity check against malformed data + self.safe_fns.append(name) + # A safe abstraction is a safe function with unsafe ops + if has_unsafe_ops.strip() == "true": + self.safe_abstractions.append(name) def read_std_analysis(self): self.read_overall_counts() self.read_scan_functions() - # Sanity checks for the CSV parsing + # 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"UNSAFE_FNS_COUNT: {self.unsafe_fns_count}") @@ -86,6 +92,12 @@ def read_std_analysis(self): 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"SAFE_FNS_COUNT: {self.safe_fns_count}") + print(f"SAFE_FNS length: {len(self.safe_fns)}") + sys.exit(1) # Process the results of running `kani list` against the standard library, # i.e., the Kani STD metrics for a single date (whichever day this script is running). @@ -124,10 +136,11 @@ def __init__(self, metrics_file): 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'] - # Generate two plots per crate: one with metrics about unsafe functions, and one with metrics about safe abstractions. + self.safe_metrics = ['total_safe_fns', 'safe_fns_under_contract', 'verified_safe_fns_under_contract'] # The keys in these dictionaries are unsafe_metrics and safe_abstr_metrics, respectively; see update_plot_metrics() self.unsafe_plot_data = defaultdict(list) self.safe_abstr_plot_data = defaultdict(list) + self.safe_plot_data = defaultdict(list) self.date = datetime.today().date() self.metrics_file = metrics_file @@ -160,6 +173,10 @@ def update_plot_metrics(self, all_data): for metric in self.safe_abstr_metrics: if not metric.startswith("verified"): self.safe_abstr_plot_data[metric].append(data[metric]) + + for metric in self.safe_metrics: + if not metric.startswith("verified"): + self.safe_plot_data[metric].append(data[metric]) # 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} @@ -179,19 +196,21 @@ def compute_metrics(self, kani_list_filepath): unsafe_fns_under_contract += 1 if has_harnesses: verified_unsafe_fns_under_contract += 1 - elif func_under_contract in generic_metrics.safe_abstractions: + if func_under_contract in generic_metrics.safe_abstractions: safe_abstractions_under_contract += 1 if has_harnesses: verified_safe_abstractions_under_contract += 1 - else: + if func_under_contract in generic_metrics.safe_fns: safe_fns_under_contract += 1 if has_harnesses: verified_safe_fns_under_contract += 1 + # 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_safe_abstractions": generic_metrics.safe_abstractions_count, + "total_safe_fns": generic_metrics.safe_fns_count, "unsafe_fns_under_contract": unsafe_fns_under_contract, "verified_unsafe_fns_under_contract": verified_unsafe_fns_under_contract, "safe_abstractions_under_contract": safe_abstractions_under_contract, @@ -252,8 +271,9 @@ def plot_single(self, data, title, outfile): print(f"PNG graph generated: {outfile}") def plot(self): - self.plot_single(self.unsafe_plot_data, title="Contracts on Unsafe Functions in core", outfile="core_unsafe_std_lib_metrics.png") - self.plot_single(self.safe_abstr_plot_data, title="Contracts on Safe Abstractions in core", outfile="core_safe_abstractions_std_lib_metrics.png") + self.plot_single(self.unsafe_plot_data, title="Contracts on Unsafe Functions in core", outfile="core_unsafe_metrics.png") + self.plot_single(self.safe_abstr_plot_data, title="Contracts on Safe Abstractions in core", outfile="core_safe_abstractions_metrics.png") + self.plot_single(self.safe_plot_data, title="Contracts on Safe Functions in core", outfile="core_safe_metrics.png") def main(): parser = argparse.ArgumentParser(description="Generate metrics about Kani's application to the standard library.") diff --git a/scripts/kani-std-analysis/metrics-data.json b/scripts/kani-std-analysis/metrics-data.json index 855007af7958b..2a3ff34d5b51c 100644 --- a/scripts/kani-std-analysis/metrics-data.json +++ b/scripts/kani-std-analysis/metrics-data.json @@ -4,12 +4,13 @@ "date": "2025-01-01", "total_unsafe_fns": 6987, "total_safe_abstractions": 1704, + "total_safe_fns": 14666, "unsafe_fns_under_contract": 144, "verified_unsafe_fns_under_contract": 132, "safe_abstractions_under_contract": 41, "verified_safe_abstractions_under_contract": 41, - "safe_fns_under_contract": 39, - "verified_safe_fns_under_contract": 38, + "safe_fns_under_contract": 80, + "verified_safe_fns_under_contract": 79, "total_functions_under_contract": 224 } ]