Add enumerative loop invariant synthesizer

Author: qinheping

regression/contracts/loop_invariant_synthesis_01/main.c renamed to regression/contracts/loop_contract_synthesis_01/main.c

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

regression/contracts/loop_invariant_synthesis_01/test.desc renamed to regression/contracts/loop_contract_synthesis_01/test.desc

@@ -0,0 +1,18 @@
+#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)
+  __CPROVER_assigns(i, s)
+  {
+    if(i == len-1)
+      break;
+    s += array[i];
+  }
+}

regression/contracts/loop_contract_synthesis_02/main.c

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

regression/contracts/loop_contract_synthesis_02/test.desc

@@ -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/contracts/loop_contract_synthesis_03/main.c

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

regression/contracts/loop_contract_synthesis_03/test.desc

@@ -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/contracts/loop_contract_synthesis_04/main.c

@@ -0,0 +1,11 @@
+CORE
+main.c
+--pointer-check --synthesize-loop-invariants
+^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.

regression/contracts/loop_contract_synthesis_04/test.desc

@@ -383,6 +383,53 @@ void dependence_grapht::add_dep(
   nodes[n_to].in[n_from].add(kind);
 }
 
+bool dependence_grapht::is_flow_dependent(
+  const goto_programt::const_targett &from,
+  const goto_programt::const_targett &to)
+{
+  std::set<node_indext> visited = std::set<node_indext>();
+  const dep_graph_domaint from_domain = static_cast<const dep_graph_domaint &>(
+    *storage->abstract_state_before(from, *domain_factory));
+  const dep_graph_domaint to_domain = static_cast<const dep_graph_domaint &>(
+    *storage->abstract_state_before(to, *domain_factory));
+  return is_flow_dependent(from_domain, to_domain, visited);
+}
+
+bool dependence_grapht::is_flow_dependent(
+  const dep_graph_domaint &from,
+  const dep_graph_domaint &to,
+  std::set<node_indext> &visited)
+{
+  // `to` is control dependent on `from`?
+  for(const auto node : to.get_control_deps())
+  {
+    if(visited.count((*this)[node].get_node_id()))
+      continue;
+
+    visited.insert((*this)[node].get_node_id());
+
+    if(
+      from.get_node_id() == (*this)[node].get_node_id() ||
+      is_flow_dependent(from, (*this)[node], visited))
+      return true;
+  }
+
+  // `to` is data dependent on `from`?
+  for(const auto node : to.get_data_deps())
+  {
+    if(visited.count((*this)[node].get_node_id()))
+      continue;
+
+    visited.insert((*this)[node].get_node_id());
+
+    if(
+      from.get_node_id() == (*this)[node].get_node_id() ||
+      is_flow_dependent(from, (*this)[node], visited))
+      return true;
+  }
+  return false;
+}
+
 void dep_graph_domaint::populate_dep_graph(
   dependence_grapht &dep_graph, goto_programt::const_targett this_loc) const
 {

src/analyses/dependence_graph.cpp

@@ -67,6 +67,7 @@ class dep_graph_domaint:public ai_domain_baset
 {
 public:
   typedef grapht<dep_nodet>::node_indext node_indext;
+  typedef std::set<goto_programt::const_targett> depst;
 
   explicit dep_graph_domaint(node_indext id)
     : has_values(false), node_id(id), has_changed(false)
@@ -167,13 +168,20 @@ class dep_graph_domaint:public ai_domain_baset
   void populate_dep_graph(
     dependence_grapht &, goto_programt::const_targett) const;
 
+  depst get_control_deps() const
+  {
+    return control_deps;
+  }
+  depst get_data_deps() const
+  {
+    return data_deps;
+  }
+
 private:
   tvt has_values;
   node_indext node_id;
   bool has_changed;
 
-  typedef std::set<goto_programt::const_targett> depst;
-
   // Set of locations with control instructions on which the instruction at this
   // location has a control dependency on
   depst control_deps;
@@ -279,7 +287,16 @@ class dependence_grapht:
     return rd;
   }
 
+  /// Decide whether the instruction `to` is flow dependent on `from`.
+  bool is_flow_dependent(
+    const goto_programt::const_targett &from,
+    const goto_programt::const_targett &to);
+
 protected:
+  bool is_flow_dependent(
+    const dep_graph_domaint &from,
+    const dep_graph_domaint &to,
+    std::set<node_indext> &visited);
   friend dep_graph_domain_factoryt;
   friend dep_graph_domaint;
   const namespacet &ns;

src/analyses/dependence_graph.h

@@ -13,6 +13,7 @@ target_link_libraries(goto-instrument-lib
     linking
     big-int
     goto-programs
+    goto-checker
     goto-symex
     assembler
     pointer-analysis

src/goto-instrument/CMakeLists.txt

@@ -82,6 +82,7 @@ SRC = accelerate/accelerate.cpp \
       splice_call.cpp \
       stack_depth.cpp \
       synthesizer/enumerative_loop_invariant_synthesizer.cpp \
+      synthesizer/cegis_verifier.cpp \
       synthesizer/expr_enumerator.cpp \
       synthesizer/synthesizer_utils.cpp \
       thread_instrumentation.cpp \

src/goto-instrument/Makefile

@@ -142,7 +142,7 @@ 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, ENTERED_LOOP)
       .symbol_expr();
   pre_loop_head_instrs.add(
     goto_programt::make_decl(entered_loop, loop_head_location));
@@ -173,7 +173,7 @@ void code_contractst::check_apply_loop_contracts(
   // instrumentation of the loop.
   const auto in_base_case =
     new_tmp_symbol(
-      bool_typet(), loop_head_location, mode, symbol_table, "__in_base_case")
+      bool_typet(), loop_head_location, mode, symbol_table, IN_BASE_CASE)
       .symbol_expr();
   pre_loop_head_instrs.add(
     goto_programt::make_decl(in_base_case, loop_head_location));
@@ -294,6 +294,12 @@ void code_contractst::check_apply_loop_contracts(
   // Generate havocing code for assignment targets.
   havoc_assigns_targetst havoc_gen(to_havoc, ns);
   havoc_gen.append_full_havoc_code(loop_head_location, pre_loop_head_instrs);
+  // Add loop number to the havoc_code
+  Forall_goto_program_instructions(havoc_it, pre_loop_head_instrs)
+  {
+    if(is_loop_havoc(havoc_it))
+      havoc_it->loop_number = loop_end->loop_number;
+  }
 
   // Insert the second block of pre_loop_head_instrs: the havocing code.
   // We do not `add_pragma_disable_assigns_check`,

src/goto-instrument/contracts/contracts.cpp

@@ -442,3 +442,35 @@ 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(!target->is_assign())
+  return false;
+
+  return from_expr(target->assign_lhs()).find("__entered_loop") !=
+           std::string::npos &&
+         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 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;
+}

src/goto-instrument/contracts/utils.cpp

@@ -17,6 +17,9 @@ Date: September 2021
 
 #include <goto-programs/goto_convert_class.h>
 
+#define IN_BASE_CASE "__in_base_case"
+#define ENTERED_LOOP "__entered_loop"
+
 /// \brief A class that overrides the low-level havocing functions in the base
 ///        utility class, to havoc only when expressions point to valid memory,
 ///        i.e. if all dereferences within an expression are valid
@@ -205,4 +208,13 @@ void generate_history_variables_initialization(
   const irep_idt &mode,
   goto_programt &program);
 
+/// Return true if `target` is the loop end of some transformed code.
+bool is_transformed_loop_end(const goto_programt::const_targett &target);
+
+/// Return true if `target` is an assignment to an instrumented variable with
+/// name `var_name`.
+bool is_assignment_to_instrumented_variable(
+  const goto_programt::const_targett &target,
+  std::string var_name);
+
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H

src/goto-instrument/contracts/utils.h

@@ -1148,16 +1148,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     goto_model.goto_functions.update();
   }
 
-  if(cmdline.isset("synthesize-loop-invariants"))
-  {
-    log.warning() << "Loop invariant synthesizer is still work in progress. "
-                     "It only generates TRUE as invariants."
-                  << messaget::eom;
-
-    // Synthesize loop invariants and annotate them into `goto_model`
-    enumerative_loop_invariant_synthesizert synthesizer(goto_model, log);
-    annotate_invariants(synthesizer.synthesize_all(), goto_model, log);
-  }
 
   bool use_dfcc = cmdline.isset(FLAG_DFCC);
   if(use_dfcc)
@@ -1432,6 +1422,33 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   goto_check_c(options, goto_model, ui_message_handler);
   transform_assertions_assumptions(options, goto_model);
 
+  if(cmdline.isset(FLAG_SYNTHESIZE_LOOP_INVARIANTS))
+  {
+    if(cmdline.isset(FLAG_LOOP_CONTRACTS))
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "Incompatible options detected",
+        "--" FLAG_SYNTHESIZE_LOOP_INVARIANTS " and --" FLAG_LOOP_CONTRACTS,
+        "Use either --" FLAG_SYNTHESIZE_LOOP_INVARIANTS
+        " or --" FLAG_LOOP_CONTRACTS);
+    }
+
+    log.warning() << "Loop invariant synthesizer is still work in progress. "
+                     "It only generates TRUE as invariants."
+                  << messaget::eom;
+
+    // Synthesize loop invariants and annotate them into `goto_model`
+    enumerative_loop_invariant_synthesizert synthesizer(goto_model, log);
+    annotate_invariants(synthesizer.synthesize_all(), goto_model);
+
+    // Apply loop contracts.
+    std::set<std::string> to_exclude_from_nondet_static(
+      cmdline.get_values("nondet-static-exclude").begin(),
+      cmdline.get_values("nondet-static-exclude").end());
+    code_contractst contracts(goto_model, log);
+    contracts.apply_loop_contracts(to_exclude_from_nondet_static);
+  }
+
   // check for uninitalized local variables
   if(cmdline.isset("uninitialized-check"))
   {

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -16,7 +16,14 @@ Date: July 2021
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
 
-#include <goto-programs/goto_program.h>
+bool is_loop_havoc(const goto_programt::const_targett &instruction)
+{
+  if(
+    id2string(instruction->source_location().get_comment()) ==
+    "Loop havocing instrumented by appling loop contracts")
+    return true;
+  return false;
+}
 
 void havoc_utilst::append_full_havoc_code(
   const source_locationt location,
@@ -52,6 +59,8 @@ void havoc_utilst::append_object_havoc_code_for_expr(
   havoc.add_source_location() = location;
   havoc.add_to_operands(expr);
   dest.add(goto_programt::make_other(havoc, location));
+  dest.instructions.back().source_location_nonconst().set_comment(
+    "Loop havocing instrumented by appling loop contracts");
 }
 
 void havoc_utilst::append_scalar_havoc_code_for_expr(
@@ -62,4 +71,6 @@ void havoc_utilst::append_scalar_havoc_code_for_expr(
   side_effect_expr_nondett rhs(expr.type(), location);
   dest.add(goto_programt::make_assignment(
     code_assignt{expr, std::move(rhs), location}, location));
+  dest.instructions.back().source_location_nonconst().set_comment(
+    "Loop havocing instrumented by appling loop contracts");
 }