Create a performance test suite and add s2n-quic as a test (rust-lang…

…#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

@@ -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:

.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

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

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.

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