Incremental BMC for CEGIS

regression/Makefile

@@ -6,6 +6,9 @@ DIRS = ansi-c \
        goto-analyzer \
        goto-instrument \
        goto-instrument-typedef \
+       cbmc-incr-oneloop \
+       cbmc-incr \
+       cbmc-with-incr \
        test-script \
        # Empty last line
 
@@ -19,3 +22,4 @@ clean:
 			$(MAKE) -C "$$dir" clean; \
 		fi; \
 	done;
+

regression/array-refinement-with-incr/Array_UF9/main.c

@@ -11,7 +11,7 @@ unsigned int SIZE;
 int linear_search(int *a, int n, int q) {
   unsigned int j=0;
   while (j<n && a[j]!=q) {
-  j;
+  j++;
   if (j==20) j=-1;
   }
   if (j<SIZE) return 1;

regression/cbmc-incr-oneloop/Makefile

@@ -1,11 +1,16 @@
 default: tests.log
 
 test:
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula"
+	@if ! ../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula" ; then \
+	../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 tests.log: ../test.pl
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula"
-
+	@if ! ../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --slice-formula" ; then \
+	../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 show:
 	@for dir in *; do \
 		if [ -d "$$dir" ]; then \

regression/cbmc-incr-oneloop/unwind-forever1/test.desc

@@ -1,4 +1,4 @@
-CORE
+THOROUGH
 main.c
  --incremental-check main.0
 ^EXIT=142$

regression/cbmc-incr-oneloop/unwind-forever2/test.desc

@@ -1,4 +1,4 @@
-CORE
+THOROUGH
 main.c
 --incremental-check main.0
 ^EXIT=142$

regression/cbmc-incr-oneloop/unwinding-assertion1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind-max 10 --incremental-check main.0
+--unwind-max 10 --incremental-check main.0 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-incr/Makefile

@@ -1,13 +1,17 @@
 default: tests.log
 
-PARAM = --incremental --magic-numbers
+PARAM = --incremental 
 # --refine   --slice-formula
 
 test:
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc $(PARAM)"
+	@if ! ../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --incremental" ; then \
+	../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 tests.log: ../test.pl
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc $(PARAM)"
+	@if ! ../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 30 ../../../src/cbmc/cbmc --incremental" ; then \
+	../failed-tests-printer.pl ; \
 
 show:
 	@for dir in *; do \

regression/cbmc-incr/unwinding-assertion1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---unwind-max 10
+--unwind-max 10 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-with-incr/Free1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+--pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
 ^Counterexample:$

regression/cbmc-with-incr/Free2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+--pointer-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
 ^Counterexample:$

regression/cbmc-with-incr/Free3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+--pointer-check --stop-on-fail
 ^SIGNAL=0$
 ^Counterexample:$
 ^VERIFICATION FAILED$

regression/cbmc-with-incr/Free4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check
+--pointer-check --stop-on-fail
 ^SIGNAL=0$
 ^Counterexample:$
 ^VERIFICATION FAILED$

regression/cbmc-with-incr/Function5/test.desc

@@ -1,10 +1,10 @@
 CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --stop-on-fail
 ^SIGNAL=0$
 ^EXIT=10$
 ^Counterexample:$
-^  dereference failure: object bounds in .*$
+^  dereference failure: pointer outside object bounds in .*$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-with-incr/Multi_Dimensional_Array6/test.desc

@@ -3,8 +3,8 @@ main.c
 --unwind-max 3 --no-unwinding-assertions --all-properties
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.1\] assertion matriz\[\(signed long int\)j\]\[\(signed long int\)k\] <= maior: OK$
-^\[main\.assertion\.2\] assertion matriz\[\(signed long int\)0\]\[\(signed long int\)0\] < maior: FAILED$
+
+^\[main\.assertion\.2\] assertion matriz\[\(signed long int\)0\]\[\(signed long int\)0\] \< maior: FAILURE$
 ^\*\* 1 of 2 failed \(2 iterations\)$
 --
 ^warning: ignoring

regression/cbmc-with-incr/Overflow_Addition1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---signed-overflow-check
+--signed-overflow-check --stop-on-fail
 ^SIGNAL=0$
 ^Counterexample:$
 ^VERIFICATION FAILED$

regression/cbmc-with-incr/Pointer_Arithmetic5/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check --bounds-check --function f
+--pointer-check --bounds-check --function f --stop-on-fail
 ^SIGNAL=0$
 ^Counterexample:$
 ^VERIFICATION FAILED$

regression/cbmc-with-incr/Pointer_Arithmetic8/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --stop-on-fail
 ^SIGNAL=0$
 ^Counterexample:$
 ^VERIFICATION FAILED$

regression/cbmc-with-incr/Pointer_byte_extract2/test.desc

@@ -3,7 +3,7 @@ main.c
 --all-properties --little-endian
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.2\] .*: FAILED$
+^\[main\.assertion\.2\] .*: FAILURE$
 ^\*\* 1 of 2 failed \(2 iterations\)$
 --
 ^warning: ignoring

regression/cbmc-with-incr/Pointer_byte_extract5/test.desc

@@ -3,7 +3,7 @@ main.c
 --all-properties --bounds-check --32
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILED$
-^\*\* 1 of 9 failed \(2 iterations\)$
+array\.List dynamic object upper bound in p->List\[2\]: FAILURE
+\*\* 1 of 11 failed \(2 iterations\)
 --
 ^warning: ignoring

regression/cbmc-with-incr/Pointer_byte_extract8/test.desc

@@ -3,7 +3,7 @@ main.c
 --all-properties --bounds-check --32 --no-simplify
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main\.array_bounds\.5\] array.List upper bound: FAILED$
-^\*\* 1 of 9 failed \(2 iterations\)$
+^\[main\.array_bounds\.5\] array.List upper bound: FAILURE$
+^\*\* 1 of 9 failed (2 iterations)$
 --
 ^warning: ignoring

regression/cbmc-with-incr/String2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --stop-on-fail
 ^EXIT=10$
 ^SIGNAL=0$
 ^Counterexample:$

regression/cbmc-with-incr/Undefined_Function1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--stop-on-fail
 ^SIGNAL=0$
 ^\*\*\*\* WARNING: no body for function f$
 ^Counterexample:$

regression/cbmc-with-incr/pipe1/test.desc

@@ -3,7 +3,7 @@ main.c
 --all-properties
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.assertion\.4\] assertion data\[1\]==31: FAILED$
+^\[main\.assertion\.4\] assertion data\[1\]==31: FAILURE$
 ^\*\* 1 of 5 failed \(2 iterations\)$
 --
 ^warning: ignoring

scripts/reformat_docs.py

@@ -95,10 +95,6 @@ def is_block_valid(self, block):
     def convert_sections(self, block):
         return [self.format_module(block)]
 
-    def needs_new_header(self, file_contents):
-        return (re.search(r'^\/\/\/ \\file$', file_contents, flags=re.MULTILINE)
-                is None)
-
 
 class FunctionFormatter(GenericFormatter):
     def __init__(self, doc_width):
@@ -192,7 +188,6 @@ def convert_sections(self, block):
 
 def replace_block(
         block_contents,
-        file_contents,
         file,
         header_formatter,
         class_formatter,
@@ -204,10 +199,9 @@ def replace_block(
             {f.name: f.contents for f in parse_fields(block_contents.group(1))})
 
     if header_formatter.is_block_valid(block):
-        converted = header_formatter.convert(header_from_block(block))
-        if header_formatter.needs_new_header(file_contents) and converted:
-            return block_contents.group(0) + converted + '\n'
-        return block_contents.group(0)
+        return '%s%s\n' % (
+                block_contents.group(0),
+                header_formatter.convert(header_from_block(block)))
 
     if class_formatter.is_block_valid(block):
         return class_formatter.convert(class_from_block(block))
@@ -237,7 +231,6 @@ def convert_file(file, inplace):
     new_contents = block_re.sub(
             lambda match: replace_block(
                 match,
-                contents,
                 file,
                 header_formatter,
                 class_formatter,

src/ansi-c/expr2c.cpp

@@ -3166,7 +3166,6 @@ std::string expr2ct::convert_code_array_replace(
   unsigned indent)
 {
   std::string dest=indent_str(indent)+"ARRAY_REPLACE(";
-
   forall_operands(it, src)
   {
     unsigned p;

src/ansi-c/get-gcc-builtins.sh

@@ -25,7 +25,6 @@ cat > gcc-builtins.h <<EOF
 #include <unistd.h>
 #include <stdio.h>
 #include <wctype.h>
-
 typedef   char   __gcc_v8qi  __attribute__ ((__vector_size__ (8)));
 typedef   char   __gcc_v16qi __attribute__ ((__vector_size__ (16)));
 typedef   char   __gcc_v32qi __attribute__ ((__vector_size__ (32)));
@@ -50,7 +49,6 @@ typedef   long long __gcc_v2di __attribute__ ((__vector_size__ (16)));
 typedef   long long __gcc_v4di __attribute__ ((__vector_size__ (32)));
 typedef   long long __gcc_v8di __attribute__ ((__vector_size__ (64)));
 typedef   unsigned long long __gcc_di;
-
 EOF
 
 cat > builtins.h <<EOF
@@ -98,17 +96,14 @@ cat > builtins.h <<EOF
 #define short_unsigned_type_node unsigned short
 #define short_integer_type_node short
 #define unsigned_char_type_node unsigned char
-
 // some newer versions of GCC apparently support __floatXYZ
 #define dfloat32_type_node __float32
 #define dfloat64_type_node __float64
 #define dfloat128_type_node __float128
-
 #define build_qualified_type(t, q) q t
 #define build_pointer_type(t) t*
 #define TYPE_QUAL_VOLATILE volatile
 #define TYPE_QUAL_CONST const
-
 #define DEF_PRIMITIVE_TYPE(ENUM, TYPE) \
 NEXTDEF ENUM TYPE
 #define DEF_FUNCTION_TYPE_0(ENUM, RETURN) \
@@ -135,7 +130,6 @@ NEXTDEF ENUM(name) RETURN name(ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ARG7, ARG8, A
 NEXTDEF ENUM(name) RETURN name(ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ARG7, ARG8, ARG9, ARG10)
 #define DEF_FUNCTION_TYPE_11(ENUM, RETURN, ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ARG7, ARG8, ARG9, ARG10, ARG11) \
 NEXTDEF ENUM(name) RETURN name(ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ARG7, ARG8, ARG9, ARG10, ARG11)
-
 #define DEF_FUNCTION_TYPE_VAR_0(ENUM, RETURN) \
 NEXTDEF ENUM(name) RETURN name()
 #define DEF_FUNCTION_TYPE_VAR_1(ENUM, RETURN, ARG1) \
@@ -152,21 +146,15 @@ NEXTDEF ENUM(name) RETURN name(ARG1, ARG2, ARG3, ARG4, ARG5, ...)
 NEXTDEF ENUM(name) RETURN name(ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ...)
 #define DEF_FUNCTION_TYPE_VAR_7(ENUM, RETURN, ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ARG7) \
 NEXTDEF ENUM(name) RETURN name(ARG1, ARG2, ARG3, ARG4, ARG5, ARG6, ARG7, ...)
-
 #define DEF_POINTER_TYPE(ENUM, TYPE) \
 NEXTDEF ENUM TYPE*
-
 #define DEF_POINTER_TYPE_CONST(ENUM, TYPE, C) \
 NEXTDEF ENUM const TYPE*
-
 #include "builtin-types.def"
-
 NEXTDEF DEF_BUILTIN(ENUM, NAME, CLASS, TYPE, LIBTYPE, BOTH_P, \
                   FALLBACK_P, NONANSI_P, ATTRS, IMPLICIT, COND) \
 TYPE(MANGLE(NAME));
-
 #include "i386-builtin-types-expanded.def"
-
 NEXTDEF BDESC(mask, icode, name, code, comparison, flag) \
 flag(MANGLEi386(name));
 NEXTDEF BDESC_FIRST(kind, KIND, mask, icode, name, code, comparison, flag) \
@@ -176,12 +164,10 @@ EOF
 grep '^DEF_VECTOR_TYPE' i386-builtin-types.def | \
   awk -F '[,() \t]' '{ print "#define " $3 " __gcc_" tolower($3) }' \
   > i386-builtin-types-expanded.def
-
 grep -v '^DEF_FUNCTION_TYPE[[:space:]]' i386-builtin-types.def | \
   grep '^DEF_P' | \
   sed '/^DEF_POINTER_TYPE[^,]*, [^,]*, [^,]*$/ s/_TYPE/_TYPE_CONST/' \
   >> i386-builtin-types-expanded.def
-
 cat i386-builtin-types.def | \
   sed '/^DEF_FUNCTION_TYPE[[:space:]]/! s/.*//' | \
   sed 's/^DEF_FUNCTION_TYPE[[:space:]]*(\([^,]*\))/\1_FTYPE_VOID/' | \
@@ -272,4 +258,4 @@ cat gcc-builtins.h | sed 's/__builtin/XX__builtin/' | \
   gcc -D__CPROVER_size_t=size_t -c -fno-builtin -x c - -o gcc-builtins.o
 rm gcc-builtins.o
 
-echo "Successfully built gcc-builtins.h"
+echo "Successfully built gcc-builtins.h"

src/cbmc/Makefile

@@ -1,6 +1,8 @@
 SRC = all_properties.cpp \
       bmc.cpp \
       bmc_cover.cpp \
+      bmc_incremental.cpp \
+      bmc_incremental_one_loop.cpp \
       bv_cbmc.cpp \
       cbmc_dimacs.cpp \
       cbmc_languages.cpp \
@@ -11,6 +13,8 @@ SRC = all_properties.cpp \
       fault_localization.cpp \
       show_vcc.cpp \
       symex_bmc.cpp \
+      symex_bmc_incremental.cpp \
+      symex_bmc_incremental_one_loop.cpp \
       symex_coverage.cpp \
       xml_interface.cpp \
       # Empty last line