Merge pull request #39 from carolynzech/metrics-test

Metrics test

.github/workflows/book.yml

@@ -10,6 +10,7 @@ on:
     paths:
       - 'doc/**'
       - '.github/workflows/book.yml'
+      - 'scripts/kani-std-analysis/**'
 
 jobs:
   build:
@@ -18,12 +19,28 @@ 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
           echo "${HOME}/.cargo/bin" >> $GITHUB_PATH
 
-      # Removed --locked for now since it is broken due to old proc_macro feature.
       - name: Install linkchecker
         run: cargo install mdbook-linkcheck --version "^0.7"
 
@@ -33,7 +50,7 @@ jobs:
       - name: Upload book
         uses: actions/upload-pages-artifact@v3
         with:
-          path: book/html
+          path: doc/book
           retention-days: "2"
 
   deploy:

.github/workflows/kani-metrics.yml

@@ -2,7 +2,7 @@ name: Kani Metrics Update
 
 on:
   schedule:
-    - cron: '0 0 1,15 * *'  # Run on the 1st and 15th of every month
+    - cron: '0 0 * * 0'  # Run at 00:00 UTC every Sunday
   workflow_dispatch:
 
 defaults:

.gitignore

@@ -45,7 +45,6 @@ package-lock.json
 # Tools
 ## Kani
 *.out
-kani-list.*
 
 # Added by cargo
 #

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

@@ -29,8 +29,8 @@
 # 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):
-        self.results_directory = "/tmp/std_lib_analysis/results"
+    def __init__(self, results_dir):
+        self.results_directory = results_dir
         self.unsafe_fns_count = 0
         self.safe_abstractions_count = 0
         self.safe_fns_count = 0
@@ -144,7 +144,7 @@ def __init__(self, metrics_file):
         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']
-        # The keys in these dictionaries are unsafe_metrics and safe_abstr_metrics, respectively; see update_plot_metrics()
+        # 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)
         self.safe_plot_data = defaultdict(list)
@@ -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.
@@ -187,10 +184,12 @@ 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):
+    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()
+        generic_metrics = GenericSTDMetrics(analysis_results_dir)
 
         print("Comparing kani-list output to std-analysis.sh output and computing metrics...")
 
@@ -292,11 +291,22 @@ def main():
                     type=str, 
                     default="kani-list.json", 
                     help="Path to the JSON file containing the Kani list data (default: kani-list.json)")
+    # The default is /tmp/std_lib_analysis/results because, as of writing, that's always where std-analysis.sh outputs its results.
+    parser.add_argument('--analysis-results-dir', 
+                    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)
-    metrics.plot()
+
+    if args.plot_only:
+        metrics.plot()
+    else:
+        metrics.compute_metrics(args.kani_list_file, args.analysis_results_dir)
 
 if __name__ == "__main__":
-    main()
+    main()

scripts/kani-std-analysis/requirements.txt

@@ -1 +1 @@
-matplotlib
+matplotlib

scripts/run-kani.sh

@@ -299,18 +299,19 @@ main() {
         echo "Running Kani list command..."
         "$kani_path" list -Z list $unstable_args ./library --std --format markdown
     elif [[ "$run_command" == "metrics" ]]; then
-        echo "Computing Kani-specific metrics..."
+        local current_dir=$(pwd)
         echo "Running Kani list command..."
         "$kani_path" list -Z list $unstable_args ./library --std --format json
-        mv $(pwd)/kani-list.json scripts/kani-std-analysis/kani-list.json
         echo "Running Kani's std-analysis command..."
         pushd $build_dir
         ./scripts/std-analysis.sh
         popd
         pushd scripts/kani-std-analysis
         pip install -r requirements.txt
-        ./kani_std_analysis.py
+        echo "Computing Kani-specific metrics..."
+        ./kani_std_analysis.py --kani-list-file $current_dir/kani-list.json
         popd
+        rm kani-list.json
     fi
 }