From f711e7a25b96d5f6cbb59af97c846e001df3f082 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Fri, 10 Jun 2022 07:02:13 -0700
Subject: [PATCH] Create a performance test suite and add s2n-quic as a test
 (#1267)

* Add s2n-quic as a submodule

* Add a script for running performance tests

* Add a CI workflow for running performance tests
---
 .github/workflows/kani.yml                    | 19 +++++++++
 .gitmodules                                   |  4 ++
 scripts/kani-perf.sh                          | 42 +++++++++++++++++++
 tests/perf/overlays/README.md                 | 11 +++++
 .../vectored_copy_fuzz_test.expected          | 22 ++++++++++
 tests/perf/s2n-quic                           |  1 +
 6 files changed, 99 insertions(+)
 create mode 100755 scripts/kani-perf.sh
 create mode 100644 tests/perf/overlays/README.md
 create mode 100644 tests/perf/overlays/s2n-quic/quic/s2n-quic-core/vectored_copy_fuzz_test.expected
 create mode 160000 tests/perf/s2n-quic

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index c27a5c63b6157..c7444754e53b9 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -26,6 +26,25 @@ jobs:
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
+  perf:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v2
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+            os: ubuntu-20.04
+
+      - name: Build Kani
+        run: |
+          export RUST_BACKTRACE=1
+          cargo build --workspace
+
+      - name: Execute Kani performance tests
+        run: ./scripts/kani-perf.sh
+
   bookrunner:
     runs-on: ubuntu-20.04
     permissions:
diff --git a/.gitmodules b/.gitmodules
index 340b8368311f1..7246d4c1e60b4 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -10,3 +10,7 @@
 [submodule "firecracker"]
 	path = firecracker
 	url = https://github.com/firecracker-microvm/firecracker.git
+[submodule "tests/perf/s2n-quic"]
+	path = tests/perf/s2n-quic
+	url = https://github.com/aws/s2n-quic
+	branch = main
diff --git a/scripts/kani-perf.sh b/scripts/kani-perf.sh
new file mode 100755
index 0000000000000..484aadab55a35
--- /dev/null
+++ b/scripts/kani-perf.sh
@@ -0,0 +1,42 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -o pipefail
+set -o nounset
+
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+KANI_DIR=$SCRIPT_DIR/..
+
+# Build all packages in the workspace
+cargo build --workspace
+
+PERF_DIR="${KANI_DIR}/tests/perf"
+
+# Copy expected files from overlay directories
+to_delete=
+for overlay_dir in ${PERF_DIR}/overlays/*/; do
+  orig_dir=$(basename ${overlay_dir})
+  echo "Copying overlays for $orig_dir"
+  copy_output=$(cp -r -v ${overlay_dir}* ${PERF_DIR}/${orig_dir}/)
+  copied_files=$(echo ${copy_output} | rev | cut -d' ' -f 1 | rev | tr -d "'")
+  # Add to the list of files to delete
+  to_delete="${to_delete} ${copied_files}"
+done
+
+suite="perf"
+mode="cargo-kani"
+echo "Check compiletest suite=$suite mode=$mode"
+cargo run -p compiletest -- --suite $suite --mode $mode
+exit_code=$?
+
+echo "Cleaning up..."
+rm ${to_delete}
+
+echo
+if [ $exit_code -eq 0 ]; then
+  echo "All Kani perf tests completed successfully."
+else
+  echo "***Kani perf tests failed."
+fi
+echo
diff --git a/tests/perf/overlays/README.md b/tests/perf/overlays/README.md
new file mode 100644
index 0000000000000..8a58ca19a32e7
--- /dev/null
+++ b/tests/perf/overlays/README.md
@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+This directory contains "overlay" files (e.g. expected files) that should be copied into directories under perf before running compiletest.
+
+Explanation: compiletest's cargo-kani mode (which is used for running the perf tests) looks for "<harness-name>.expected" files and runs `cargo kani --harness <harness-name>` for each.
+Some of the perf tests are external repositories that are integrated as git submodules, so we cannot commit files in their subtrees.
+Thus, we instead commit any files needed under the "overlays" directory, which then get copied over by `kani-perf.sh` before it calls compiletest.
+
+To create overlay files for `perf/foo`, place them in a `perf/overlays/foo` directory.
+They will get copied over following the same directory structure.
diff --git a/tests/perf/overlays/s2n-quic/quic/s2n-quic-core/vectored_copy_fuzz_test.expected b/tests/perf/overlays/s2n-quic/quic/s2n-quic-core/vectored_copy_fuzz_test.expected
new file mode 100644
index 0000000000000..c0b7bedc0fcf2
--- /dev/null
+++ b/tests/perf/overlays/s2n-quic/quic/s2n-quic-core/vectored_copy_fuzz_test.expected
@@ -0,0 +1,22 @@
+Status: SUCCESS\
+Description: "assertion failed: a == b"
+
+Status: SUCCESS\
+Description: "assertion failed: from.len() > from_index"
+
+Status: SUCCESS\
+Description: "assertion failed: to.len() > to_index"
+
+Status: SUCCESS\
+Description: "assertion failed: from.len() >= from_offset"
+
+Status: SUCCESS\
+Description: "assertion failed: to.len() >= to_offset"
+
+Status: SUCCESS\
+Description: "assertion failed: from.len() >= len"
+
+Status: SUCCESS\
+Description: "assertion failed: to.len() >= len"
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic
new file mode 160000
index 0000000000000..2158407ada569
--- /dev/null
+++ b/tests/perf/s2n-quic
@@ -0,0 +1 @@
+Subproject commit 2158407ada56905d9627331923263bfc6f6b43d6