Add enumerative loop invariant synthesizer

Implement the functionality described below.

Motivation
---
This loop invariant synthesizer use the idea counter-example-guided synthesis (CEGIS) to synthesize loop invariants for programs with only checks instrumented by `goto-instrument` with flag `--pointer-check`.

This PR contain the driver of the synthesizer and the verifier we use to check invariant candidates.

Verifier
---
The verifier take as input a goto program with pointer checks and a map from loop id to loop invariant candidates. It first annotate and apply the loop invariant candidates into the goto model; and then simulate the CBMC api to verify the instrumented goto program. If there are some violations---loop invariants are not inductive, or some pointer checks fail---, it record valuation from trace generated by the back end to construct a formatted counterexample `cext`.

Counterexample
---
A counterexample `cext` record valuations of variables in the trace, and other information about the violation. The valuation we record including
1. set of live variables upon the entry of the loop.
2. the havoced value of all primitive-typed variables;
3. the havoced offset and the object size of all pointer-typed variables;
4. history values of 2 and 3.

The valuations will be used as true positive (history values) and true negative (havcoed valuation) to filter out bad invariant clause with the idea of the Daikon invariant detector in a following PR. However, in this PR we only construct the valuation but not actually use them.

Synthesizer
---
Loop invariants we synthesize are of the form
`` (in_clause || !guard) && (!guard -> pos_clause)``
where `in_clause` and `out_clause` are predicates we store in two different map, and `guard` is the loop guard. The idea is that we separately synthesize the condition `in_clause` that should hold before the execution of the loop body, and condition `pos_clause` that should hold as post-condition of the loop.

When the violation happen in the loop, we update `in_clause`. When the violation happen after the loop, we update `pos_clause`. When the invariant candidate it not inductive, we enumerate strengthening clause to make it inductive.

To be more efficient, we choose different synthesis strategy for different type of violation
* For out-of-boundary violation, we choose to use the violated predicate as the new clause, which is the WLP of the violation if the violation is only dependent on the havocing instruction. **TODO**: to make it more complete, we need to implement a WLP algorithm
* For null-pointer violation, we choose `__CPROVER_same_object(ptr, __CPROVER_loop_entry(ptr))` as the new clause. That is, the havoced pointer should points to the same object at the start of every iteration of the loop. It is a heuristic choice. This can be extended with the idea of alias analysis if needed.
* For invariant-not-preserved violation, we enumerate strengthening clauses and check that if the invariant will be inductive after strengthening (disjunction with the new clause).

The synthesizer works as follow
1. initialize the two invariant maps,
2. verify the current candidates built from the two maps,
_a. return the candidate if there is no violation
_b. synthesize a new clause to resolve the **first** violation and add it to the correct map,
3. repeat 2.

Author: qinheping

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);
+}