Merge pull request #579 from peterschrammel/test-gen-support

Test-gen support

Author: peterschrammel

regression/cbmc-java/assume1/Assume1.class

@@ -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/Assume1.java

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

regression/cbmc-java/assume1/test.desc

@@ -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/Assume2.class

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

regression/cbmc-java/assume2/Assume2.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/assume2/test.desc

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

regression/cbmc-java/assume3/Assume3.class

@@ -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/assume3/Assume3.java

@@ -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

regression/cbmc-java/assume3/test.desc

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

regression/cbmc-java/covered1/covered1.class

@@ -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.

regression/cbmc-java/covered1/covered1.java

@@ -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

regression/cbmc-java/covered1/test.desc

@@ -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/.gitignore

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

scripts/bash-autocomplete/Readme.md

@@ -108,4 +108,12 @@ libzip-build:
 	@echo "Building libzip"
 	@(cd ../libzip; BASE=`pwd`; ./configure --with-zlib=$(BASE)/zlib ; make)
 
-.PHONY: minisat2-download glucose-download zlib-download libzip-download libzip-build
+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 zlib-download libzip-download libzip-build cprover-jar-build

scripts/bash-autocomplete/cbmc.sh.template

@@ -10,8 +10,11 @@ Date: May 2016
 
 #include <algorithm>
 #include <iterator>
+#include <unordered_set>
 
+#include <util/format_number_range.h>
 #include <util/prefix.h>
+#include <util/string2int.h>
 
 #include "cover.h"
 
@@ -28,14 +31,38 @@ class basic_blockst
       if(next_is_target || it->is_target())
         block_count++;
 
+      const irep_idt &line=it->source_location.get_line();
+      if(!line.empty())
+        block_line_cover_map[block_count]
+          .insert(unsafe_string2unsigned(id2string(line)));
+
       block_map[it]=block_count;
 
       if(!it->source_location.is_nil() &&
          source_location_map.find(block_count)==source_location_map.end())
         source_location_map[block_count]=it->source_location;
 
       next_is_target=
+#if 0
+        // Disabled for being too messy
         it->is_goto() || it->is_function_call() || it->is_assume();
+#else
+        it->is_goto() || it->is_function_call();
+#endif
+    }
+
+    // create list of covered lines as CSV string and set as property of source
+    // location of basic block, compress to ranges if applicable
+    format_number_ranget format_lines;
+    for(const auto &cover_set : block_line_cover_map)
+    {
+      assert(!cover_set.second.empty());
+      std::vector<unsigned>
+        line_list{cover_set.second.begin(), cover_set.second.end()};
+
+      std::string covered_lines=format_lines(line_list);
+      source_location_map[cover_set.first]
+        .set_basic_block_covered_lines(covered_lines);
     }
   }
 
@@ -47,6 +74,11 @@ class basic_blockst
   typedef std::map<unsigned, source_locationt> source_location_mapt;
   source_location_mapt source_location_map;
 
+  // map block numbers to set of line numbers
+  typedef std::map<unsigned, std::unordered_set<unsigned> >
+    block_line_cover_mapt;
+  block_line_cover_mapt block_line_cover_map;
+
   inline unsigned operator[](goto_programt::const_targett t)
   {
     return block_map[t];
@@ -414,7 +446,7 @@ std::set<exprt> collect_mcdc_controlling_nested(
   const std::set<exprt> &decisions)
 {
   // To obtain the 1st-level controlling conditions
-  std::set<exprt> controlling = collect_mcdc_controlling(decisions);
+  std::set<exprt> controlling=collect_mcdc_controlling(decisions);
 
   std::set<exprt> result;
   // For each controlling condition, to check if it contains
@@ -627,7 +659,7 @@ void remove_repetition(std::set<exprt> &exprs)
      **/
     for(auto &y : new_exprs)
     {
-      bool iden = true;
+      bool iden=true;
       for(auto &c : conditions)
       {
         std::set<signed> signs1=sign_of_expr(c, x);
@@ -669,7 +701,7 @@ void remove_repetition(std::set<exprt> &exprs)
   }
 
   // update the original ''exprs''
-  exprs = new_exprs;
+  exprs=new_exprs;
 }
 
 /*******************************************************************\
@@ -838,7 +870,8 @@ bool is_mcdc_pair(
 
   if(diff_count==1)
     return true;
-  else return false;
+  else
+    return false;
 }
 
 /*******************************************************************\
@@ -963,7 +996,8 @@ void minimize_mcdc_controlling(
     {
       controlling=new_controlling;
     }
-    else break;
+    else
+      break;
   }
 }
 
@@ -1297,9 +1331,12 @@ void instrument_cover_goals(
         const std::set<exprt> decisions=collect_decisions(i_it);
 
         std::set<exprt> both;
-        std::set_union(conditions.begin(), conditions.end(),
-                       decisions.begin(), decisions.end(),
-                       inserter(both, both.end()));
+        std::set_union(
+          conditions.begin(),
+          conditions.end(),
+          decisions.begin(),
+          decisions.end(),
+          inserter(both, both.end()));
 
         const source_locationt source_location=i_it->source_location;
 
@@ -1397,6 +1434,9 @@ void instrument_cover_goals(
        f_it->first=="__CPROVER_initialize")
       continue;
 
-    instrument_cover_goals(symbol_table, f_it->second.body, criterion);
+    instrument_cover_goals(
+      symbol_table,
+      f_it->second.body,
+      criterion);
   }
 }