Merge pull request #7430 from qinheping/goto-synthesizer

SYNTHESIZER: Add enumerative loop invariant synthesizer

Author: tautschnig

regression/goto-synthesizer/CMakeLists.txt

@@ -12,9 +12,8 @@ else()
   set(gcc_only_string "")
 endif()
 
-
 add_test_pl_tests(
-    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-synthesizer> $<TARGET_FILE:cbmc> ${is_windows}"
+  "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:goto-synthesizer> $<TARGET_FILE:cbmc> ${is_windows}"
 )
 
 ## Enabling these causes a very significant increase in the time taken to run the regressions

regression/goto-synthesizer/Makefile

@@ -14,16 +14,16 @@ else
 endif
 
 test:
-	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-synthesizer/goto-synthesizer ../../../src/cbmc/cbmc $(is_windows)' -X smt-backend $(GCC_ONLY)
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/goto-synthesizer/goto-synthesizer ../../../src/cbmc/cbmc $(is_windows)' -X smt-backend $(GCC_ONLY)
 
 test-cprover-smt2:
-	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-synthesizer/goto-synthesizer "../../../src/cbmc/cbmc --cprover-smt2" $(is_windows)' \
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/goto-synthesizer/goto-synthesizer "../../../src/cbmc/cbmc --cprover-smt2" $(is_windows)' \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
 					  -s cprover-smt2 $(GCC_ONLY)
 
 test-z3:
-	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-synthesizer/goto-synthesizer "../../../src/cbmc/cbmc --z3" $(is_windows)' \
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/goto-synthesizer/goto-synthesizer "../../../src/cbmc/cbmc --z3" $(is_windows)' \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
 					  -s z3 $(GCC_ONLY)

regression/goto-synthesizer/chain.sh

@@ -3,14 +3,15 @@
 set -e
 
 goto_cc=$1
-goto_synthesizer=$2
-cbmc=$3
-is_windows=$4
+goto_instrument=$2
+goto_synthesizer=$3
+cbmc=$4
+is_windows=$5
 
 name=${*:$#}
 name=${name%.c}
 
-args=${*:5:$#-5}
+args=${*:6:$#-6}
 if [[ "$args" != *" _ "* ]]
 then
   args_inst=$args
@@ -27,7 +28,9 @@ else
 fi
 
 rm -f "${name}-mod.gb"
-$goto_synthesizer ${args_inst} "${name}.gb" "${name}-mod.gb"
+rm -f "${name}-mod-2.gb"
+echo "Running goto-instrument: "
+$goto_instrument ${args_inst} "${name}.gb" "${name}-mod.gb"
 if [ ! -e "${name}-mod.gb" ] ; then
   cp "$name.gb" "${name}-mod.gb"
 elif echo $args_inst | grep -q -- "--dump-c" ; then
@@ -41,4 +44,7 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
 
   rm "${name}-mod.c"
 fi
-$cbmc "${name}-mod.gb" ${args_cbmc}
+echo "Running goto-synthesizer: "
+$goto_synthesizer "${name}-mod.gb" "${name}-mod-2.gb"
+echo "Running CBMC: "
+$cbmc "${name}-mod-2.gb" ${args_cbmc}

regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] line 10 Check loop invariant before entry: SUCCESS$

regression/goto-synthesizer/loop_contracts_synthesis_02/main.c

@@ -0,0 +1,17 @@
+#define SIZE 80
+
+void main()
+{
+  unsigned len;
+  __CPROVER_assume(len <= SIZE);
+  __CPROVER_assume(len >= 8);
+  char *array = malloc(len);
+  unsigned s = 0;
+
+  for(unsigned i = 0; i < SIZE; ++i)
+  {
+    if(i == len - 1)
+      break;
+    s += array[i];
+  }
+}

regression/goto-synthesizer/loop_contracts_synthesis_02/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^\[main.pointer\_dereference.\d+\] .* SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test shows that loop invariants using range predicates can be correctly
+synthesized for programs with only pointer checks but no other assertions.

regression/goto-synthesizer/loop_contracts_synthesis_03/main.c

@@ -0,0 +1,16 @@
+#define SIZE 80
+
+void main()
+{
+  unsigned long len;
+  __CPROVER_assume(len <= SIZE);
+  __CPROVER_assume(len >= 8);
+  char *array = malloc(len);
+  const char *end = array + len;
+  unsigned s = 0;
+
+  while(array != end)
+  {
+    s += *array++;
+  }
+}

regression/goto-synthesizer/loop_contracts_synthesis_03/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^\[main.pointer\_dereference.\d+\] .* SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test shows that loop invariants using range predicates and same-object
+predicates can be correctly synthesized for programs with only pointer
+checks but no other assertions.

regression/goto-synthesizer/loop_contracts_synthesis_04/main.c

@@ -0,0 +1,17 @@
+#define SIZE 80
+
+void main()
+{
+  unsigned long len;
+  __CPROVER_assume(len <= SIZE);
+  __CPROVER_assume(len >= 8);
+  char *array = malloc(len);
+  unsigned long s = 0;
+
+  unsigned long j = 0;
+  for(unsigned long i = 0; i < len; i++)
+  {
+    s += array[j];
+    j++;
+  }
+}

regression/goto-synthesizer/loop_contracts_synthesis_04/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^\[main.pointer\_dereference.\d+\] .* SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test shows that the loop-invariant synthesizer can enumerate
+strengthening clauses for invariant-not-preserved violation.