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.

src/goto-instrument/contracts/contracts.cpp

@@ -59,6 +59,7 @@ void code_contractst::check_apply_loop_contracts(
   const irep_idt &mode)
 {
   const auto loop_head_location = loop_head->source_location();
+  const auto loop_number = loop_end->loop_number;
 
   // Vector representing a (possibly multidimensional) decreases clause
   const auto &decreases_clause_exprs = decreases_clause.operands();
@@ -95,10 +96,12 @@ void code_contractst::check_apply_loop_contracts(
   //                        |    STEP:
   //                  --.   |      assert (initial_invariant_val);
   // loop assigns check |   |      in_base_case = false;
-  //  - not applicable   >=======  havoc (assigns_set);
-  // func assigns check |   |      assume (invariant_expr);
-  //  + deferred        |   `-     old_variant_val = decreases_clause_expr;
-  //                  --'      * HEAD:
+  //  - not applicable   >=======  in_loop_havoc_block = true;
+  // func assigns check |   |      havoc (assigns_set);
+  //  + deferred        |   |      in_loop_havoc_block = false;
+  //                  --'   |      assume (invariant_expr);
+  //                        `-     old_variant_val = decreases_clause_expr;
+  //                           * HEAD:
   // loop assigns check     ,-     ... eval guard ...
   //  + assertions added    |      if (!guard)
   // func assigns check     |        goto EXIT;
@@ -142,7 +145,11 @@ void code_contractst::check_apply_loop_contracts(
   // i.e., the loop guard was satisfied.
   const auto entered_loop =
     new_tmp_symbol(
-      bool_typet(), loop_head_location, mode, symbol_table, "__entered_loop")
+      bool_typet(),
+      loop_head_location,
+      mode,
+      symbol_table,
+      std::string(ENTERED_LOOP) + "__" + std::to_string(loop_number))
       .symbol_expr();
   pre_loop_head_instrs.add(
     goto_programt::make_decl(entered_loop, loop_head_location));
@@ -153,7 +160,7 @@ void code_contractst::check_apply_loop_contracts(
   // if the loop is not vacuous and must be abstracted with contracts.
   const auto initial_invariant_val =
     new_tmp_symbol(
-      bool_typet(), loop_head_location, mode, symbol_table, "__init_invariant")
+      bool_typet(), loop_head_location, mode, symbol_table, INIT_INVARIANT)
       .symbol_expr();
   pre_loop_head_instrs.add(
     goto_programt::make_decl(initial_invariant_val, loop_head_location));
@@ -292,8 +299,25 @@ void code_contractst::check_apply_loop_contracts(
     loop_head, add_pragma_disable_assigns_check(pre_loop_head_instrs));
 
   // Generate havocing code for assignment targets.
+  // ASSIGN in_loop_havoc_block = true;
+  // havoc (assigns_set);
+  // ASSIGN in_loop_havoc_block = false;
+  const auto in_loop_havoc_block =
+    new_tmp_symbol(
+      bool_typet(),
+      loop_head_location,
+      mode,
+      symbol_table,
+      std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(loop_number))
+      .symbol_expr();
+  pre_loop_head_instrs.add(
+    goto_programt::make_decl(in_loop_havoc_block, loop_head_location));
+  pre_loop_head_instrs.add(
+    goto_programt::make_assignment(in_loop_havoc_block, true_exprt{}));
   havoc_assigns_targetst havoc_gen(to_havoc, ns);
   havoc_gen.append_full_havoc_code(loop_head_location, pre_loop_head_instrs);
+  pre_loop_head_instrs.add(
+    goto_programt::make_assignment(in_loop_havoc_block, false_exprt{}));
 
   // Insert the second block of pre_loop_head_instrs: the havocing code.
   // We do not `add_pragma_disable_assigns_check`,
@@ -1414,6 +1438,66 @@ void code_contractst::apply_loop_contracts(
   unwindset.parse_unwindset(loop_names, log.get_message_handler());
   goto_unwindt goto_unwind;
   goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME);
+
+  remove_skip(goto_model);
+
+  // Record original loop number for some instrumented instructions.
+  for(auto &goto_function_entry : goto_functions.function_map)
+  {
+    auto &goto_function = goto_function_entry.second;
+    bool is_in_loop_havoc_block = false;
+
+    unsigned loop_number_of_loop_havoc = 0;
+    for(goto_programt::const_targett it_instr =
+          goto_function.body.instructions.begin();
+        it_instr != goto_function.body.instructions.end();
+        it_instr++)
+    {
+      // Don't override original loop numbers.
+      if(original_loop_number_map.count(it_instr) != 0)
+        continue;
+
+      // Store loop number for
+      // ASSIGN ENTERED_LOOP = TRUE
+      if(
+        is_assignment_to_instrumented_variable(it_instr, ENTERED_LOOP) &&
+        it_instr->assign_rhs() == true_exprt())
+      {
+        const auto &assign_lhs =
+          expr_try_dynamic_cast<symbol_exprt>(it_instr->assign_lhs());
+        original_loop_number_map[it_instr] = get_suffix_unsigned(
+          id2string(assign_lhs->get_identifier()),
+          std::string(ENTERED_LOOP) + "__");
+        continue;
+      }
+
+      // Loop havocs are assignments between
+      // ASSIGN IN_LOOP_HAVOC_BLOCK = true
+      // and
+      // ASSIGN IN_LOOP_HAVOC_BLOCK = false
+
+      // Entering the loop-havoc block.
+      if(is_assignment_to_instrumented_variable(it_instr, IN_LOOP_HAVOC_BLOCK))
+      {
+        is_in_loop_havoc_block = it_instr->assign_rhs() == true_exprt();
+        const auto &assign_lhs =
+          expr_try_dynamic_cast<symbol_exprt>(it_instr->assign_lhs());
+        loop_number_of_loop_havoc = get_suffix_unsigned(
+          id2string(assign_lhs->get_identifier()),
+          std::string(IN_LOOP_HAVOC_BLOCK) + "__");
+        continue;
+      }
+
+      // Assignments in loop-havoc block are loop havocs.
+      if(is_in_loop_havoc_block && it_instr->is_assign())
+      {
+        loop_havoc_set.emplace(it_instr);
+
+        // Store loop number for loop havoc.
+        original_loop_number_map[it_instr] = loop_number_of_loop_havoc;
+      }
+    }
+  }
 }
 
 void code_contractst::enforce_contracts(

src/goto-instrument/contracts/contracts.h

@@ -122,6 +122,18 @@ class code_contractst
   symbol_tablet &get_symbol_table();
   goto_functionst &get_goto_functions();
 
+  std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
+  get_original_loop_number_map() const
+  {
+    return original_loop_number_map;
+  }
+
+  std::unordered_set<goto_programt::const_targett, const_target_hash>
+  get_loop_havoc_set() const
+  {
+    return loop_havoc_set;
+  }
+
   namespacet ns;
 
 protected:
@@ -137,6 +149,17 @@ class code_contractst
   /// Name of loops we are going to unwind.
   std::list<std::string> loop_names;
 
+  /// Store the map from instrumented instructions for loop contracts to their
+  /// original loop numbers. Following instrumented instructions are stored.
+  /// 1. loop-havoc   ---   begin of transformed loops
+  /// 2. ASSIGN ENTERED_LOOP = TRUE   ---   end of transformed loops
+  std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
+    original_loop_number_map;
+
+  /// Loop havoc instructions instrumneted during applying loop contracts.
+  std::unordered_set<goto_programt::const_targett, const_target_hash>
+    loop_havoc_set;
+
 public:
   /// \brief Enforce contract of a single function
   void enforce_contract(const irep_idt &function);

src/goto-instrument/contracts/utils.cpp

@@ -447,3 +447,49 @@ void generate_history_variables_initialization(
   // Add all the history variable initialization instructions
   program.destructive_append(history);
 }
+
+bool is_transformed_loop_end(const goto_programt::const_targett &target)
+{
+  // The end of the loop end of transformed loop is
+  // ASSIGN entered_loop = true
+  if(!is_assignment_to_instrumented_variable(target, ENTERED_LOOP))
+    return false;
+
+  return target->assign_rhs() == true_exprt();
+}
+
+bool is_assignment_to_instrumented_variable(
+  const goto_programt::const_targett &target,
+  std::string var_name)
+{
+  INVARIANT(
+    var_name == IN_BASE_CASE || var_name == ENTERED_LOOP ||
+      var_name == IN_LOOP_HAVOC_BLOCK,
+    "var_name is not of instrumented variables.");
+
+  if(!target->is_assign())
+    return false;
+
+  if(can_cast_expr<symbol_exprt>(target->assign_lhs()))
+  {
+    const auto &lhs = to_symbol_expr(target->assign_lhs());
+    return id2string(lhs.get_identifier()).find("::" + var_name) !=
+           std::string::npos;
+  }
+
+  return false;
+}
+
+unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
+{
+  // first_index is the end of the `prefix`.
+  auto first_index = str.find(prefix);
+  INVARIANT(
+    first_index != std::string::npos, "Prefix not found in the given string");
+  first_index += prefix.length();
+
+  // last_index is the index of not-digit.
+  auto last_index = str.find_first_not_of("0123456789", first_index);
+  std::string result = str.substr(first_index, last_index - first_index);
+  return std::stol(result);
+}