From 130df89bfd88c48081ece20e67dd88af24b56dca Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 14 Apr 2025 10:57:53 +0000
Subject: [PATCH] Add script to text-extract all contracts

This is a helper script to collect all existing contracts for subsequent
review or analysis. This facilitates metrics we want to report.
---
 scripts/find-contracts.sh | 42 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100755 scripts/find-contracts.sh

diff --git a/scripts/find-contracts.sh b/scripts/find-contracts.sh
new file mode 100755
index 0000000000000..e682e9efb074e
--- /dev/null
+++ b/scripts/find-contracts.sh
@@ -0,0 +1,42 @@
+#!/bin/bash
+
+# Script to find files with specific annotations and print contracts
+# containing those annotations up to a line with "fn"
+PATTERN_STRING='^\s*#\[((safety::)?(requires|ensures)\(|cfg_attr\((kani|not\(kani\)))'
+
+# Find all files in the git repository that contain any of the patterns
+FILES=$(git grep -l -P "$PATTERN_STRING" library/)
+
+if [ -z "$FILES" ]; then
+  echo "No files found with the specified patterns."
+  exit 1
+fi
+
+# Process each file
+for FILE in $FILES; do
+  echo "=== $FILE ==="
+
+  # Use perl to find contracts starting with any pattern and ending at "fn"
+  cat $FILE | perl -e "
+    \$in_contract = 0;
+    \$ws = 0;
+    while(<>) {
+      \$line = \$_;
+      if (!\$in_contract && /$PATTERN_STRING/ && !/^\s*#\[cfg_attr\(kani, derive\(/) {
+        \$in_contract = 1;
+        /^(\s*)/;
+        \$ws = length(\$1);
+      }
+      if (\$in_contract) {
+        \$line =~ s/^ {\$ws}//;
+        print \$line; 
+        if (\$line =~ /(^| )fn /) {
+          \$in_contract = 0;
+          print \"\n\";
+        }
+      }
+    }
+  "
+
+  echo
+done