Incremental BMC

Author: Peter Schrammel

regression/Makefile

@@ -1,4 +1,8 @@
-DIRS = ansi-c cbmc cpp goto-instrument goto-instrument-unwind
+DIRS = ansi-c cbmc cpp goto-instrument goto-instrument-unwind \
+       cbmc-incr-oneloop cbmc-incr cbmc-with-incr
 
 test:
-	$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)
+	$(foreach var,$(DIRS), make -C $(var) test;)
+
+clean:
+	$(foreach var,$(DIRS), make -C $(var) clean;)

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/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,6 +1,6 @@
 default: tests.log
 
-PARAM = --incremental --magic-numbers
+PARAM = --incremental 
 # --refine   --slice-formula
 
 test:

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,6 +1,6 @@
 CORE
 main.c
---pointer-check --bounds-check
+--pointer-check --bounds-check --stop-on-fail
 ^SIGNAL=0$
 ^EXIT=10$
 ^Counterexample:$

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

@@ -3,8 +3,10 @@ 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\.1\] assertion matriz\[(signed long int)j\]\[(signed long int)k\] <= maior:
+SUCCESS$
+^\[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$
+^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILURE$
 ^\*\* 1 of 9 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$
+^\[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

src/cbmc/Makefile

@@ -2,7 +2,8 @@ SRC = cbmc_main.cpp cbmc_parse_options.cpp bmc.cpp cbmc_dimacs.cpp \
       cbmc_languages.cpp counterexample_beautification.cpp \
       bv_cbmc.cpp symex_bmc.cpp show_vcc.cpp cbmc_solvers.cpp \
       xml_interface.cpp bmc_cover.cpp all_properties.cpp \
-      fault_localization.cpp
+      symex_bmc_incremental_one_loop.cpp bmc_incremental_one_loop.cpp \
+      symex_bmc_incremental.cpp bmc_incremental.cpp fault_localization.cpp
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \

src/cbmc/all_properties.cpp

@@ -97,7 +97,8 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
       it!=bmc.equation.SSA_steps.end();
       it++)
   {
-    if(it->is_assert())
+    if(it->is_assert() &&
+       it->comment!=SYMEX_CONTINUATION_CHECK)
     {
       irep_idt property_id;
 
@@ -114,6 +115,9 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
       else
         continue;
 
+      //need to convert again as the context of the expression
+      //  may have changed
+      it->cond_literal=solver.convert(it->cond_expr);
       goal_map[property_id].instances.push_back(it);
     }
   }
@@ -122,6 +126,14 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
   cover_goalst cover_goals(solver);
 
+  //set activation literal for incremental checking
+  cover_goals.activation_literal=bmc.equation.current_activation_literal();
+
+#if 0
+  std::cout << "cover_goals.activation_literal = "
+            << cover_goals.activation_literal << std::endl;
+#endif
+
   cover_goals.set_message_handler(get_message_handler());
   cover_goals.register_observer(*this);
 
@@ -137,6 +149,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
 
   bool error=false;
 
+  solver.set_assumptions(bmc.equation.activate_assertions);
   decision_proceduret::resultt result=cover_goals();
 
   if(result==decision_proceduret::D_ERROR)