Fix and install bash completion for cbmc

1) Use a pragma-free (and working) approach to extract CBMC_OPTIONS.
2) Add completion of all completable arguments to command-line options.
3) Make CMake's install target install the resulting bash completion
script in etc/bash_completion.d
4) Make the .deb package depend on bash-completion for the now-included
completion snippet to be useful.

Author: tautschnig

cmake/packaging.cmake

@@ -24,8 +24,9 @@ set(CPACK_PACKAGE_RESOURCE_FILE_README "${CMAKE_CURRENT_SOURCE_DIR}/README.md")
 # Automatically find dependencies for shared libraries
 set(CPACK_DEBIAN_PACKAGE_SHLIBDEPS YES)
 
-# In addition, we depend on gcc for preprocessing
-set(CPACK_DEBIAN_PACKAGE_DEPENDS gcc)
+# In addition, we depend on gcc for preprocessing and bash-completion to make
+# CBMC's bash completion work
+set(CPACK_DEBIAN_PACKAGE_DEPENDS "gcc, bash-completion")
 
 # Enable debug output so that we can see the dependencies being generated in the
 # logs

scripts/bash-autocomplete/Readme.md

@@ -23,6 +23,8 @@ Follow 1. 2. and 3. as above.
 
 4. Put the following at the end of your `~/.zshrc`, with the directories adapted to your directory structure:
     ```bash
+    autoload -Uz compinit
+    compinit
     autoload bashcompinit
     bashcompinit
     cbmcautocomplete=~/diffblue/cbmc/scripts/bash-autocomplete/cbmc.sh

scripts/bash-autocomplete/cbmc.sh.template

@@ -19,14 +19,30 @@ _cbmc_autocomplete()
      COMPREPLY=( $( compgen -W "sc tso pso" -- $cur ) )
      return 0
      ;;
-   --arch) #for architecture we list the options explicitly
-     COMPREPLY=( $( compgen -W "i386 x86_64" -- $cur ) )
+   --arch) #for architecture we list the options explicitly; this list is populated using
+     # `grep -w 'arch[[:space:]]*==' src/util/config.cpp | cut # -f2 -d'"' | sort`
+     COMPREPLY=( $( compgen -W "alpha arm arm64 armel armhf hppa i386 ia64 mips mips64 mips64el mipsel mipsn32 mipsn32el none powerpc ppc64 ppc64le riscv64 s390 s390x sh4 sparc sparc64 v850 x32 x86_64" -- $cur ) )
      return 0
      ;;
-   -I|--classpath|-cp|--outfile|--existing-coverage|--graphml-cex)
+   --os) #for architecture we list the options explicitly
+     COMPREPLY=( $( compgen -W "freebsd linux macos solaris windows" -- $cur ) )
+     return 0
+     ;;
+   --timestamp) #for timestamp we list the options explicitly
+     COMPREPLY=( $( compgen -W "monotonic wall" -- $cur ) )
+     return 0
+     ;;
+   --paths) #for paths we list the options explicitly
+     COMPREPLY=( $( compgen -W "fifo lifo" -- $cur ) )
+     return 0
+     ;;
+   -I|--classpath|-cp) # a directory
+     _filedir -d
+     return 0
+     ;;
+   --external-sat-solver|--incremental-smt2-solver)
      #a switch that takes a file parameter of which we don't know an extension
-     #TODO probably we can do more for -I, --classpath, -cp
-     COMPREPLY=( $(compgen -f -- $cur) )
+     _filedir -f
      return 0
      ;;
   esac

scripts/bash-autocomplete/extract_switches.sh

@@ -1,23 +1,17 @@
 #!/bin/bash
-echo "Compiling the helper file to extract the raw list of parameters from cbmc"
-g++ -c -MMD -MP -std=c++11 -Wall -I ../../src/ -ftrack-macro-expansion=0 -fno-diagnostics-show-caret switch_extractor_helper.c  -o tmp.o 2> pragma.txt
 
-retval=$?
+set -e
 
-#clean up compiled files, we don't need them.
-rm tmp.o 2> /dev/null
-rm tmp.d 2> /dev/null
+# make sure we execute the remainder in the directory containing this script
+cd `dirname $0`
 
-#check if compilation went fine
-if [ $retval -ne 0 ]; then
-  echo "Problem compiling the helper file, parameter list not extracted."
-  exit 1;
-fi
+echo "Compiling the helper file to extract the raw list of parameters from cbmc"
+g++ -E -dM -std=c++11 -I../../src ../../src/cbmc/cbmc_parse_options.cpp -o macros.c
+echo CBMC_OPTIONS >> macros.c
 
 echo "Converting the raw parameter list to the format required by autocomplete scripts"
-rawstring=`sed "s/^.*pragma message: \(.*\)/\1/" pragma.txt`
-#delete pragma file, we won't need it
-rm pragma.txt 2> /dev/null
+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=`(
@@ -26,7 +20,7 @@ cleanstring=`(
   (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/")
+  (echo $rawstring | sed "s/([^)]*)//g" | grep -o "[a-zA-Z0-9?]" | sed "s/\(.*\)/-\1/")
  ) | tr '\n' ' '`
 
 #sanity check that there is only one line of output
@@ -36,13 +30,10 @@ if [ `echo $cleanstring | wc -l | awk '{print $1}'` -ne 1 ]; then
 fi
 
 #sanity check that there are no dangerous characters
-echo $cleanstring | grep -q "[^a-zA-Z0-9 -]"
-if [ $? -eq 0 ]; then
+if echo $cleanstring | grep -q "[^a-zA-Z0-9? -]"; then
  echo "Problem converting the parameter list to the correct format, illegal characters detected. This is likely to be an error in this conversion script."
  exit 1;
 fi
 
 echo "Injecting the parameter list to the autocomplete file."
 sed "5 s/.*/  local switches=\"$cleanstring\"/" cbmc.sh.template > cbmc.sh
-
-rm pragma.txt 2> /dev/null

src/cbmc/CMakeLists.txt

@@ -57,3 +57,19 @@ if(NOT WIN32)
     PATTERN "c*"
     PATTERN "g*")
 endif()
+
+# bash completion
+if(NOT WIN32)
+  add_custom_command(OUTPUT "${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/cbmc.sh"
+    COMMAND "${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/extract_switches.sh"
+    DEPENDS $<TARGET_FILE:cbmc>
+  )
+  add_custom_target(cbmc.sh ALL
+    DEPENDS "${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/cbmc.sh"
+  )
+  install(
+    FILES ${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/cbmc.sh
+    DESTINATION etc/bash_completion.d
+    RENAME cbmc
+  )
+endif()