Port of changes to test-gen-support to master (6)

regression/cbmc-java/assume1/Assume1.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class Assume1
+{
+  static void foo(int x)
+  {
+    CProver.assume(x>3);
+    assert x>0;
+  }
+}

regression/cbmc-java/assume1/test.desc

@@ -0,0 +1,8 @@
+CORE
+Assume1.class
+--function Assume1.foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/assume2/Assume2.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class Assume2
+{
+  static void foo(int x)
+  {
+    CProver.assume(x>3);    
+    assert x>4;
+  }
+}

regression/cbmc-java/assume2/test.desc

@@ -0,0 +1,8 @@
+CORE
+Assume2.class
+--function Assume2.foo
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/assume3/Assume3.java

@@ -0,0 +1,10 @@
+import org.cprover.CProver;
+
+class Assume3
+{
+  public static void main(String[] args)
+  {
+    CProver.assume(false);
+    assert false;
+  }
+}

regression/cbmc-java/assume3/test.desc

@@ -0,0 +1,8 @@
+CORE
+Assume3.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/covered1/covered1.java

@@ -0,0 +1,37 @@
+public class covered1
+{
+  // this is a variable
+  int x=1;
+  //these are two, one line off the first
+  int y=2;
+  int z=3;
+  //this is part of static init
+  static int z0=0;
+
+  //another non-static
+  int a;
+  int b;
+  static boolean odd;
+
+  static
+  {
+    odd=(z0+1)%2==0;
+  }
+
+  covered1(int a, int b)
+  {
+    this.a=a*b;
+    this.b=a+b;
+    if(this.a==a)
+      z0++;
+    else
+      odd=!odd;
+  }
+  // at the back
+  int z1=2;
+  int z2=3;
+  int z3=4;
+  //
+  static int z4=5;
+  int z5=5;
+}

regression/cbmc-java/covered1/test.desc

@@ -0,0 +1,19 @@
+CORE
+covered1.class
+--cover location --json-ui --show-properties
+^EXIT=0$
+^SIGNAL=0$
+.*\"coveredLines\": \"22\",$
+.*\"coveredLines\": \"4,6,7,23-25,31-33,36\",$
+.*\"coveredLines\": \"26\",$
+.*\"coveredLines\": \"28\",$
+.*\"coveredLines\": \"28\",$
+.*\"coveredLines\": \"28\",$
+.*\"coveredLines\": \"28\",$
+.*\"coveredLines\": \"29\",$
+.*\"coveredLines\": \"9,18\",$
+.*\"coveredLines\": \"18\",$
+.*\"coveredLines\": \"18\",$
+.*\"coveredLines\": \"18,35\",$
+--
+^warning: ignoring

scripts/bash-autocomplete/.gitignore

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

scripts/bash-autocomplete/Readme.md

@@ -0,0 +1,31 @@
+# CBMC Autocomplete Scripts for Bash
+This directory contains an autocomplete script for bash.
+## Installation
+1. Compile cbmc and
+
+2. `cd scripts/bash-autocomplete`
+
+3.  `./extract-switches.sh`
+
+4. Put the following at the end of you in 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
+    ```
+## 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
+     _filedir
+     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
+  _filedir "@(class|jar|cpp|cc|c\+\+|ii|cxx|c|i|gb)"
+}
+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

src/Makefile

@@ -84,4 +84,12 @@ glucose-download:
 	@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
 	@rm glucose-syrup.tgz
 
-.PHONY: minisat2-download glucose-download
+cprover-jar-build:
+	@echo "Building org.cprover.jar"
+	@(cd java_bytecode/library/; \
+	mkdir -p target; \
+	javac -d target/ `find src/ -name "*.java"`; \
+	cd target; jar cf org.cprover.jar `find . -name "*.class"`; \
+	mv org.cprover.jar ../../../)
+
+.PHONY: minisat2-download glucose-download cprover-jar-build

src/cbmc/cbmc_parse_options.cpp

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/c_preprocess.h>
 
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/string_refine_preprocess.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_instanceof.h>
@@ -288,6 +289,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("refine-arithmetic", true);
   }
 
+  if(cmdline.isset("refine-strings"))
+  {
+    options.set_option("refine-strings", true);
+  }
+
   if(cmdline.isset("max-node-refinement"))
     options.set_option(
       "max-node-refinement",
@@ -811,6 +817,14 @@ bool cbmc_parse_optionst::process_goto_program(
     status() << "Partial Inlining" << eom;
     goto_partial_inline(goto_functions, ns, ui_message_handler);
 
+
+    if(cmdline.isset("refine-strings"))
+    {
+      status() << "Preprocessing for string refinement" << eom;
+      string_refine_preprocesst(
+        symbol_table, goto_functions, ui_message_handler);
+    }
+
     // remove returns, gcc vectors, complex
     remove_returns(symbol_table, goto_functions);
     remove_vector(symbol_table, goto_functions);
@@ -1070,6 +1084,7 @@ void cbmc_parse_optionst::help()
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"
+    " --refine-strings             use string refinement (experimental)\n"
     " --outfile filename           output formula to given file\n"
     " --arrays-uf-never            never turn arrays into uninterpreted functions\n" // NOLINT(*)
     " --arrays-uf-always           always turn arrays into uninterpreted functions\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -41,6 +41,7 @@ class optionst;
   "(no-sat-preprocessor)" \
   "(no-pretty-names)(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\
+  "(refine-strings)" \
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-loops)" \

src/cbmc/cbmc_solvers.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/bv_refinement.h>
+#include <solvers/refinement/string_refinement.h>
 #include <solvers/smt1/smt1_dec.h>
 #include <solvers/smt2/smt2_dec.h>
 #include <solvers/cvc/cvc_dec.h>

src/cbmc/cbmc_solvers.h

@@ -108,15 +108,17 @@ class cbmc_solverst:public messaget
     solvert *solver;
 
     if(options.get_bool_option("dimacs"))
-      solver = get_dimacs();
+      solver=get_dimacs();
     else if(options.get_bool_option("refine"))
-      solver = get_bv_refinement();
+      solver=get_bv_refinement();
+    else if(options.get_bool_option("refine-strings"))
+      solver=get_string_refinement();
     else if(options.get_bool_option("smt1"))
-      solver = get_smt1(get_smt1_solver_type());
+      solver=get_smt1(get_smt1_solver_type());
     else if(options.get_bool_option("smt2"))
-      solver = get_smt2(get_smt2_solver_type());
+      solver=get_smt2(get_smt2_solver_type());
     else
-      solver = get_default();
+      solver=get_default();
 
     return std::unique_ptr<solvert>(solver);
   }
@@ -138,6 +140,7 @@ class cbmc_solverst:public messaget
   solvert *get_default();
   solvert *get_dimacs();
   solvert *get_bv_refinement();
+  solvert *get_string_refinement();
   solvert *get_smt1(smt1_dect::solvert solver);
   solvert *get_smt2(smt2_dect::solvert solver);