Run EVM tests with --rts-statistics and collect the results (#2533)

* Run tests with --rts-statistics and collect the results

* test-statistics.sh: Output a CSV file for easy manipulation

* Add scripts/join-statistics.sh

* Allow running test-statistics.sh from test.nix shell

* Add Performance workflow

* Do not run Performance workflow on macOS

* Fix statistics script invocation

* Pull from runtimeverification in Performance workflow

* Use test.nix for running test-statistics.sh

* Use nix/shell.performance.nix for performance testing

* Fetch from origin in Performance workflow

* test-statistics.sh: Build own kore-exec

* test-statistics.sh: Build kore-exec from other trees

* Use test.nix for running test-statistics.sh

* Use tabular JSON format

* Fix path to test-statistics.sh

* Comment on pull request with performance data

* Use CSV for intermediate tables

* Integrate performance testing into Test workflow

* test-statistics.sh: accept multiple test directories

* test.yml: Test wasm-semantics, too

Co-authored-by: Thomas Tuegel <[email protected]>
Co-authored-by: Thomas Tuegel <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: 3 people

.github/workflows/test.yml

@@ -214,3 +214,49 @@ jobs:
 
       - name: Run hlint
         run: curl -sSL https://raw.github.com/ndmitchell/hlint/master/misc/run.sh | sh -s kore -j
+
+  performance:
+    needs: [nix-build]
+    name: 'Performance'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check out code
+        uses: actions/[email protected]
+        with:
+          # Check out pull request HEAD instead of merge commit.
+          ref: ${{ github.event.pull_request.head.sha }}
+          submodules: recursive
+
+      - name: Install Nix
+        uses: cachix/install-nix-action@v12
+        with:
+          extra_nix_config: |
+            substituters = http://cache.nixos.org https://hydra.iohk.io
+            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
+
+      - name: Install Cachix
+        uses: cachix/cachix-action@v8
+        with:
+          name: kore
+          extraPullNames: runtimeverification
+          signingKey: '${{ secrets.KORE_CACHIX_SIGNING_KEY }}'
+          skipPush: true
+
+      - name: Collect performance statistics
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          ./scripts/test-statistics.sh ./. \
+            test/regression-evm \
+            test/regression-wasm \
+            > pull-request.json
+          git fetch origin
+          git worktree add kore-master master
+          ./scripts/test-statistics.sh ./kore-master \
+            test/regression-evm \
+            test/regression-wasm \
+            > master.json
+          ./scripts/join-statistics.sh master.json pull-request.json \
+            | ./scripts/format-statistics.sh \
+            > comment.md
+          gh pr comment ${{ github.event.pull_request.number }} -F comment.md

scripts/format-statistics.sh

@@ -0,0 +1,4 @@
+#!/usr/bin/env nix-shell
+#!nix-shell ../test.nix -i bash
+
+mlr --icsv --omd cut -o -f name,allocated_bytes,diff_allocated_bytes,max_live_bytes,diff_max_live_bytes

scripts/join-statistics.sh

@@ -0,0 +1,12 @@
+#!/usr/bin/env nix-shell
+#!nix-shell ../test.nix -i bash
+
+old=${1:?}; shift
+new=${1:?}; shift
+
+# 1. Join the statistics files by row according to name.
+#    Give the columns from each file a unique prefix.
+# 2. Add a column for the (relative) difference between old and new values.
+mlr --ijson --ocsv join -j name --lp old_ --rp new_ -f "$old" "$new" \
+  | mlr --csv put '$diff_allocated_bytes = ($new_allocated_bytes - $old_allocated_bytes) / $old_allocated_bytes' \
+  | mlr --csv put '$diff_max_live_bytes = ($new_max_live_bytes - $old_max_live_bytes) / $old_max_live_bytes'

scripts/test-statistics.sh

@@ -0,0 +1,28 @@
+#!/usr/bin/env nix-shell
+#!nix-shell ../test.nix -i bash
+
+# Usage: test-statistics.sh KORE_DIR TEST_DIR TEST_DIR ...
+# Output: tabular JSON on standard output
+
+set -eou pipefail
+
+kore_dir="${1:?}"; shift
+export KORE_EXEC="$(nix-build "$kore_dir" -A kore --arg release true --no-out-link)/bin/kore-exec"
+
+while [[ $# -gt 0 ]]
+do
+    test_dir="${1:?}"; shift
+    (
+        cd "$test_dir"
+        for each in $(find ./ -name 'test-*.sh')
+        do
+            json="${each%sh}.json"
+            "${each}" --rts-statistics "$json" >/dev/null
+            jq ". | { name: \"$test_dir${each#.}\", allocated_bytes: .allocated_bytes, max_live_bytes: .max_live_bytes }" < "$json"
+            rm "$json"
+        done
+    )
+done
+
+
+

test.nix

@@ -9,7 +9,7 @@ in
 
 let
   inherit (pkgs) stdenv lib;
-  inherit (pkgs) bison diffutils ncurses z3;
+  inherit (pkgs) bison diffutils jq miller ncurses z3;
 
   ttuegel =
     let
@@ -44,11 +44,13 @@ stdenv.mkDerivation {
   buildInputs = [
     k kore  # some tests use kore-exec directly, others run through the frontend
     ncurses  # TODO: .../lib/kframework/setenv: line 31: tput: command not found
+    jq miller # processing test statistics
     z3
   ];
   configurePhase = ''
     export TOP=$(pwd)
   '';
+  KORE_EXEC = "${lib.getBin kore}/bin/kore-exec";
   buildFlags =
     [
       "KORE_PARSER=kore-parser"