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

@@ -25,7 +25,7 @@ set(CPACK_PACKAGE_RESOURCE_FILE_README "${CMAKE_CURRENT_SOURCE_DIR}/README.md")
 set(CPACK_DEBIAN_PACKAGE_SHLIBDEPS YES)
 
 # In addition, we depend on gcc for preprocessing
-set(CPACK_DEBIAN_PACKAGE_DEPENDS gcc)
+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/cbmc.sh.template

@@ -20,10 +20,22 @@ _cbmc_autocomplete()
      return 0
      ;;
    --arch) #for architecture we list the options explicitly
-     COMPREPLY=( $( compgen -W "i386 x86_64" -- $cur ) )
+     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|--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) )

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,22 @@ if(NOT WIN32)
     PATTERN "c*"
     PATTERN "g*")
 endif()
+
+# bash completion
+if(NOT WIN32)
+  install(
+    CODE
+    "
+    execute_process(
+      COMMAND \"${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/extract_switches.sh\")
+    file(MAKE_DIRECTORY \"$ENV{DESTDIR}${CMAKE_INSTALL_PREFIX}/etc/bash_completion.d\")
+    file(
+      INSTALL \"${CMAKE_SOURCE_DIR}/scripts/bash-autocomplete/cbmc.sh\"
+      DESTINATION \"$ENV{DESTDIR}${CMAKE_INSTALL_PREFIX}/etc/bash_completion.d\")
+    file(
+      RENAME
+      \"$ENV{DESTDIR}${CMAKE_INSTALL_PREFIX}/etc/bash_completion.d/cbmc.sh\"
+      \"$ENV{DESTDIR}${CMAKE_INSTALL_PREFIX}/etc/bash_completion.d/cbmc\")
+    "
+  )
+endif()