Generate Kani Metrics

.github/workflows/book.yml

@@ -10,6 +10,7 @@ on:
     paths:
       - 'doc/**'
       - '.github/workflows/book.yml'
+      - 'scripts/kani-std-analysis/**'
 
 jobs:
   build:
@@ -18,6 +19,23 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v4
 
+      - name: Set up Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.x'
+
+      - name: Install Python dependencies
+        run: |
+          python -m pip install --upgrade pip
+          pip install -r scripts/kani-std-analysis/requirements.txt
+
+      - name: Generate Metrics Graphs
+        run: |
+          cd scripts/kani-std-analysis/
+          python kani_std_analysis.py --plot-only
+          cd ../..
+          mv scripts/kani-std-analysis/*.png doc/src/metrics/kani/
+
       - name: Install mdbook
         run: |
           cargo install mdbook --version "^0.4" --locked

doc/src/SUMMARY.md

@@ -9,6 +9,8 @@
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)
 
+- [Metrics](./metrics.md)
+  - [Kani](./metrics/kani/kani.md)
 
 ---
 

doc/src/metrics.md

@@ -0,0 +1,3 @@
+# Metrics
+
+Each approved tool can (optionally) publish metrics here about how their tool has been applied to the effort thus far.

doc/src/metrics/kani/kani.md

@@ -0,0 +1,10 @@
+# Kani Metrics
+
+Note that these metrics are for x86-64 architectures.
+
+## `core`
+![Unsafe Metrics](core_unsafe_metrics.png)
+
+![Safe Abstractions Metrics](core_safe_abstractions_metrics.png)
+
+![Safe Metrics](core_safe_metrics.png)

scripts/kani-std-analysis/kani_std_analysis.py

@@ -164,9 +164,6 @@ def read_historical_data(self):
             all_data = {}
 
         self.dates = [datetime.strptime(data["date"], '%Y-%m-%d').date() for data in all_data]
-        self.dates.append(self.date)
-
-        print(f"Dates are {self.dates}\n")
 
     # TODO For now, we don't plot how many of the contracts have been verified, since the line overlaps with how many are under contract.
     # If we want to plot this data, we should probably generate separate plots.
@@ -188,6 +185,8 @@ def update_plot_metrics(self, all_data):
     # 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}
     def compute_metrics(self, kani_list_filepath, analysis_results_dir):
+        self.dates.append(self.date)
+
         # Process the `kani list` and `std-analysis.sh` data
         kani_data = KaniListSTDMetrics(kani_list_filepath)
         generic_metrics = GenericSTDMetrics(analysis_results_dir)
@@ -297,11 +296,17 @@ def main():
                     type=str, 
                     default="/tmp/std_lib_analysis/results", 
                     help="Path to the folder file containing the std-analysis.sh results (default: /tmp/std_lib_analysis/results)")
+    parser.add_argument('--plot-only', 
+                    action='store_true',
+                    help="Instead of computing the metrics, just read existing metrics from --metrics-file and plot the results.")
     args = parser.parse_args()
 
     metrics = KaniSTDMetricsOverTime(args.metrics_file)
-    metrics.compute_metrics(args.kani_list_file, args.analysis_results_dir)
-    metrics.plot()
+
+    if args.plot_only:
+        metrics.plot()
+    else:
+        metrics.compute_metrics(args.kani_list_file, args.analysis_results_dir)
 
 if __name__ == "__main__":
     main()