From 880725c5da6503cfab34846a88b64085a72d72d8 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 9 Jun 2022 09:29:35 +0000
Subject: [PATCH] Check completeness of help output in CI

This commit adds a new script to run post-build that assesses the
completeness of --help for all binaries except for goto-cc.
---
 .github/workflows/pull-request-checks.yaml |   4 +
 scripts/check_help.sh                      | 107 +++++++++++++++++++++
 2 files changed, 111 insertions(+)
 create mode 100755 scripts/check_help.sh

diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml
index 79d4e176dab..fe9f7edb259 100644
--- a/.github/workflows/pull-request-checks.yaml
+++ b/.github/workflows/pull-request-checks.yaml
@@ -55,6 +55,8 @@ jobs:
           make -C jbmc/unit -j2 CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
       - name: Print ccache stats
         run: ccache -s
+      - name: Checking completeness of help output
+        run: scripts/check_help.sh
       - name: Run unit tests
         run: |
           make -C unit test IPASIR=$PWD/riss.git/riss
@@ -233,6 +235,8 @@ jobs:
         run: cd build; ninja -j2
       - name: Print ccache stats
         run: ccache -s
+      - name: Checking completeness of help output
+        run: scripts/check_help.sh build/bin
       - name: Check if package building works
         run: |
           cd build
diff --git a/scripts/check_help.sh b/scripts/check_help.sh
new file mode 100755
index 00000000000..830976425ea
--- /dev/null
+++ b/scripts/check_help.sh
@@ -0,0 +1,107 @@
+#!/bin/bash
+
+set -e
+
+# if a command-line argument is provided, use it as a path to built binaries
+# (CMake-style build); otherwise assume we use Makefile-based in-tree build
+if [ $# -eq 1 ] ; then
+  bin_dir=$(cd $1 ; pwd)
+else
+  unset bin_dir
+fi
+echo $bin_dir
+
+# make sure we execute the remainder in the directory containing this script
+cd `dirname $0`
+
+missing_options=0
+
+# we don't check goto-cc for now
+# we omit crangler for it doesn't take options other than help or a file name
+for t in  \
+  ../jbmc/src/janalyzer \
+  ../jbmc/src/jbmc \
+  ../jbmc/src/jdiff \
+  ../src/cbmc \
+  ../src/goto-analyzer \
+  ../src/goto-diff \
+  ../src/goto-harness \
+  ../src/goto-instrument \
+  ../src/memory-analyzer \
+  ../src/symtab2gb \
+; do
+  tool_name=$(basename $t)
+  opt_name=$(echo $tool_name | tr 'a-z-' 'A-Z_')
+	echo "Extracting the raw list of parameters from $tool_name"
+  g++ -E -dM -std=c++11 -I../src -I../jbmc/src $t/*_parse_options.cpp -o macros.c
+  # goto-analyzer partly uses the spelling "analyser" within the code base
+  echo ${opt_name}_OPTIONS | sed 's/GOTO_ANALYZER/GOTO_ANALYSER/' >> macros.c
+  rawstring="`gcc -E -P -w macros.c` \"?h(help)\""
+  rm macros.c
+
+  # now the main bit, convert from raw format to a proper list of switches
+  cleanstring=`(
+    # extract 2-hyphen switches, such as --foo
+    # grep for '(foo)' expressions, and then use sed to remove parantheses and
+    # put '-' at the start (we accept both --X and -X)
+    (echo $rawstring | grep -o "([^)]*)" | sed "s/^.\(.*\).$/-\1/") ;
+    # extract 1-hyphen switches, such as -F
+    # use sed to remove all (foo) expressions, then you're left with switches
+    # and ':', so grep the colons out and then use sed to include the '-'
+    (echo $rawstring | sed "s/([^)]*)//g" | grep -o "[a-zA-Z0-9?]" | sed "s/\(.*\)/-\1/")
+  ) | sed 's/" "//g'`
+
+  if [ "x$bin_dir" = "x" ] ; then
+    tool_bin=$t/$tool_name
+  else
+    tool_bin=$bin_dir/$tool_name
+  fi
+
+  if [ ! -x $tool_bin ] ; then
+    echo "$tool_bin is not an executable"
+    exit 1
+  fi
+  $tool_bin --help > help_string
+
+  # some options are intentionally undocumented
+  case $tool_name in
+    cbmc)
+      echo "-all-claims -all-properties -claim -show-claims" >> help_string
+      echo "-document-subgoals" >> help_string
+      echo "-no-propagation -no-simplify -no-simplify-if" >> help_string
+      echo "-floatbv -no-unwinding-assertions" >> help_string
+      echo "-slice-by-trace" >> help_string
+      ;;
+    goto-analyzer)
+      echo "-show-intervals -show-non-null" >> help_string
+      ;;
+    goto-instrument)
+      echo "-document-claims-html -document-claims-latex -show-claims" >> help_string
+      echo "-no-simplify" >> help_string
+      ;;
+    janalyzer)
+      echo "-show-intervals -show-non-null" >> help_string
+      ;;
+    jbmc)
+      echo "-document-subgoals" >> help_string
+      echo "-no-propagation -no-simplify -no-simplify-if" >> help_string
+      echo "-no-unwinding-assertions" >> help_string
+      ;;
+  esac
+
+  for opt in $cleanstring ; do
+    if ! grep -q -- $opt help_string ; then
+      echo "Option $opt of $tool_name is undocumented"
+      missing_options=1
+    fi
+  done
+  rm help_string
+done
+
+if [ $missing_options -eq 1 ] ; then
+  echo "Undocumented options found"
+  exit 1
+else
+  echo "All options are documented"
+  exit 0
+fi