Merge pull request #1263 from tautschnig/shell-auto-complete

[tgs->master] Shell auto completion scripts

Author: Daniel Kroening

scripts/bash-autocomplete/.gitignore

@@ -0,0 +1 @@
+cbmc.sh

scripts/bash-autocomplete/Readme.md

@@ -0,0 +1,49 @@
+# CBMC Autocomplete Scripts for Bash
+This directory contains an autocomplete script for bash.
+
+## Installation for bash
+1. Compile cbmc and
+
+2. `cd scripts/bash-autocomplete`
+
+3.  `./extract-switches.sh`
+
+4. Put the following at the end of your `~/.bashrc`, with the directories adapted to your directory structure:
+    ```bash
+    cbmcautocomplete=~/diffblue/cbmc/scripts/bash-autocomplete/cbmc.sh
+    if [ -f $cbmcautocomplete ]; then
+      . $cbmcautocomplete
+    fi
+    ```
+
+5. `source ~/.bashrc`
+
+## Installation for zsh
+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 bashcompinit
+    bashcompinit
+    cbmcautocomplete=~/diffblue/cbmc/scripts/bash-autocomplete/cbmc.sh
+    if [ -f $cbmcautocomplete ]; then
+      . $cbmcautocomplete
+    fi
+    ```
+5. `source ~/.zshrc`
+
+## Usage
+As with the usual autocomplete in bash, start typing a switch to complete it, for example:
+```
+cbmc --clas<TAB>
+```
+will complete to
+```
+cbmc --classpath
+```
+
+## Features implemented
+
+* Completing all switches
+* Completing values for `--cover`, `--mm` and `--arch`
+* When completing a name of a file to analyze, only files with supported extensions are shown.

scripts/bash-autocomplete/cbmc.sh.template

@@ -0,0 +1,43 @@
+#!/bin/bash
+_cbmc_autocomplete()
+{
+  #list of all switches cbmc has. IMPORTANT: in the template file, this variable must be defined on line 5.
+  local switches=""
+  #word on which the cursor is
+  local cur=${COMP_WORDS[COMP_CWORD]}
+  #previous word (in case it is a switch with a parameter)
+  local prev=${COMP_WORDS[COMP_CWORD-1]}
+ 
+  #check if the command before cursor is a switch that takes parameters, if yes,
+  #offer a choice of parameters
+  case "$prev" in
+   --cover) #for coverage we list the options explicitly
+     COMPREPLY=( $( compgen -W "assertion path branch location decision condition mcdc cover" -- $cur ) )
+     return 0
+     ;;
+   --mm) #for memory models we list the options explicitly
+     COMPREPLY=( $( compgen -W "sc tso pso" -- $cur ) )
+     return 0
+     ;;
+   --arch) #for architecture we list the options explicitly
+     COMPREPLY=( $( compgen -W "i386 x86_64" -- $cur ) )
+     return 0
+     ;;
+   -I|--classpath|-cp|--outfile|--existing-coverage|--graphml-cex)
+     #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) )
+     return 0
+     ;;
+  esac
+ 
+  #complete a switch from a standard list, if the parameter under cursor starts with a hyphen
+  if [[ "$cur" == -* ]]; then
+     COMPREPLY=( $( compgen -W "$switches" -- $cur ) )
+     return 0
+  fi
+
+  #if none of the above applies, offer directories and files that we can analyze
+  COMPREPLY=( $(compgen -G '*.class|*.jar|*.cpp|*.cc|*.c\+\+|*.ii|*.cxx|*.c|*.i|*.gb' -- $cur) )
+}
+complete -F _cbmc_autocomplete cbmc

scripts/bash-autocomplete/extract_switches.sh

@@ -0,0 +1,48 @@
+#!/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=$?
+
+#clean up compiled files, we don't need them.
+rm tmp.o 2> /dev/null
+rm tmp.d 2> /dev/null
+
+#check if compilation went fine
+if [ $retval -ne 0 ]; then
+  echo "Problem compiling the helper file, parameter list not extracted."
+  exit 1;
+fi
+
+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
+
+#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
+  (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/")
+ ) | tr '\n' ' '`
+
+#sanity check that there is only one line of output
+if [ `echo $cleanstring | wc -l | awk '{print $1}'` -ne 1 ]; then
+ echo "Problem converting the parameter list to the correct format, I was expecting one line but either got 0 or >2. This is likely to be an error in this conversion script."
+ exit 1;
+fi
+
+#sanity check that there are no dangerous characters
+echo $cleanstring | grep -q "[^a-zA-Z0-9 -]"
+if [ $? -eq 0 ]; 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

scripts/bash-autocomplete/switch_extractor_helper.c

@@ -0,0 +1,3 @@
+#include "cbmc/cbmc_parse_options.h"
+
+#pragma message CBMC_OPTIONS