Handle the case of violation in loop guards in loop-invariant synthesis

In current loop-invariant synthesizer, we synthesize two kinds of clauses separately.
1. `in_clause` that should hold when we enter the loop body---when the loop guard holds, that is ```loop_guard -> in_clause```.
2. `pos_clause` that should hold when we leave the loop---when the loop guard doesn't hold, that is ```!loop_guard -> pos_clause```.

We synthesize `in_clause` when the violations happen in the loop body. We synthesize `pos_clause` when the violation happen after the loop.

This PR handles the case that the violations happen in the loop guard ([loop_contracts_synthesis_06/main.c](https://github.com/diffblue/cbmc/compare/develop...qinheping:goto-synthesizer-violation-location?expand=1#diff-8a05899ddc66b61918f2e6180bfc08f09f895f6a78066c65086a5e7c470a880a) as an example). In the case, the new clause we synthesize should hold for both of the cases that loop guard holds and loop guards doesn't hold.

We introduce a new variable `violation_location` to indicate whether the violation happen in the loop, after the loop, or in the loop guard, and add the new synthesized clause as `in_clause`, `pos_clause`, or both, respectively.

Author: qinheping

regression/goto-synthesizer/loop_contracts_synthesis_06/main.c

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

regression/goto-synthesizer/loop_contracts_synthesis_06/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^\[main.*\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.*\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test is a variation of strlen. It checks that we can synthesize
+loop invariant for checks happen in the loop guard.

regression/goto-synthesizer/loop_contracts_synthesis_06/test_dump.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check _ --dump-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+loop 1 invariant.*\_\_CPROVER\_POINTER\_OFFSET
+assigns i
+--
+This test case checks if synthesized contracts are correctly dumped.

regression/goto-synthesizer/loop_contracts_synthesis_07/main.c

@@ -0,0 +1,18 @@
+#define SIZE 80
+
+void main()
+{
+  unsigned long len;
+  __CPROVER_assume(len <= SIZE);
+  __CPROVER_assume(len >= 8);
+  char *array = malloc(len);
+  __CPROVER_assume(array != 0);
+
+  unsigned i = 0;
+
+  while(i <= len - 2)
+  {
+    i++;
+  }
+  unsigned result = array[i];
+}

regression/goto-synthesizer/loop_contracts_synthesis_07/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.pointer\_dereference.\d+].*SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that we can synthesize loop invariant for violation happen
+after the loop body.

regression/goto-synthesizer/loop_contracts_synthesis_07/test_dump.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check _ --dump-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+loop 1 assigns i
+loop 1 invariant.*\_\_CPROVER\_POINTER\_OFFSET
+--
+This test case checks if synthesized contracts are correctly dumped.

src/goto-synthesizer/cegis_verifier.cpp

@@ -211,6 +211,62 @@ std::list<loop_idt> cegis_verifiert::get_cause_loop_id(
   return result;
 }
 
+cext::violation_locationt cegis_verifiert::get_violation_location(
+  const loop_idt &loop_id,
+  const goto_functiont &function,
+  unsigned location_number_of_target)
+{
+  if(is_instruction_in_transfomed_loop_condition(
+       loop_id, function, location_number_of_target))
+  {
+    return cext::violation_locationt::in_condition;
+  }
+
+  if(is_instruction_in_transfomed_loop(
+       loop_id, function, location_number_of_target))
+  {
+    return cext::violation_locationt::in_loop;
+  }
+
+  return cext::violation_locationt::after_loop;
+}
+
+bool cegis_verifiert::is_instruction_in_transfomed_loop_condition(
+  const loop_idt &loop_id,
+  const goto_functiont &function,
+  unsigned location_number_of_target)
+{
+  // The transformed loop condition are instructions from
+  // loop havocing instructions
+  // to
+  // if(!guard) GOTO EXIT
+  unsigned location_number_of_havocing = 0;
+  for(goto_programt::const_targett it = function.body.instructions.begin();
+      it != function.body.instructions.end();
+      ++it)
+  {
+    // Record the location number of the begin of a transformed loop.
+    if(
+      loop_havoc_set.count(it) &&
+      original_loop_number_map[it] == loop_id.loop_number)
+    {
+      location_number_of_havocing = it->location_number;
+    }
+
+    // Reach the end of the evaluation of the transformed loop condition.
+    if(location_number_of_havocing != 0 && it->is_goto())
+    {
+      if((location_number_of_havocing < location_number_of_target &&
+          location_number_of_target < it->location_number))
+      {
+        return true;
+      }
+      location_number_of_havocing = 0;
+    }
+  }
+  return false;
+}
+
 bool cegis_verifiert::is_instruction_in_transfomed_loop(
   const loop_idt &loop_id,
   const goto_functiont &function,
@@ -622,21 +678,22 @@ optionalt<cext> cegis_verifiert::verify()
       return cext(violation_type);
     }
 
-    // Decide whether the violation is in the cause loop.
-    bool is_violation_in_loop = is_instruction_in_transfomed_loop(
-      cause_loop_ids.front(),
-      goto_model.get_goto_function(cause_loop_ids.front().function_id),
-      property_it.second.pc->location_number);
-
     log.debug() << "Found cause loop with function id: "
                 << cause_loop_ids.front().function_id
                 << ", and loop number: " << cause_loop_ids.front().loop_number
                 << messaget::eom;
 
+    auto violation_location = cext::violation_locationt::in_loop;
     // We always strengthen in_clause if the violation is
     // invariant-not-preserved.
-    if(violation_type == cext::violation_typet::cex_not_preserved)
-      is_violation_in_loop = true;
+    if(violation_type != cext::violation_typet::cex_not_preserved)
+    {
+      // Get the location of the violation
+      violation_location = get_violation_location(
+        cause_loop_ids.front(),
+        goto_model.get_goto_function(cause_loop_ids.front().function_id),
+        property_it.second.pc->location_number);
+    }
 
     restore_functions();
 
@@ -649,7 +706,7 @@ optionalt<cext> cegis_verifiert::verify()
         ->source_location());
     return_cex.violated_predicate = property_it.second.pc->condition();
     return_cex.cause_loop_ids = cause_loop_ids;
-    return_cex.is_violation_in_loop = is_violation_in_loop;
+    return_cex.violation_location = violation_location;
     return_cex.violation_type = violation_type;
 
     // The pointer checked in the null-pointer-check violation.

src/goto-synthesizer/cegis_verifier.h

@@ -35,6 +35,13 @@ class cext
     cex_other
   };
 
+  enum class violation_locationt
+  {
+    in_loop,
+    after_loop,
+    in_condition
+  };
+
   cext(
     const std::unordered_map<exprt, mp_integer, irep_hash> &object_sizes,
     const std::unordered_map<exprt, mp_integer, irep_hash> &havoced_values,
@@ -61,9 +68,8 @@ class cext
   exprt checked_pointer;
   exprt violated_predicate;
 
-  // true if the violation happens in the cause loop
-  // false if the violation happens after the cause loop
-  bool is_violation_in_loop = true;
+  // Location where the violation happen.
+  violation_locationt violation_location = violation_locationt::in_loop;
 
   // We collect havoced evaluations of havoced variables and their object sizes
   // and pointer offsets.
@@ -131,6 +137,12 @@ class cegis_verifiert
   std::list<loop_idt>
   get_cause_loop_id_for_assigns(const goto_tracet &goto_trace);
 
+  // Compute the location of the violation.
+  cext::violation_locationt get_violation_location(
+    const loop_idt &loop_id,
+    const goto_functiont &function,
+    unsigned location_number_of_target);
+
   /// Restore transformed functions to original functions.
   void restore_functions();
 
@@ -146,6 +158,13 @@ class cegis_verifiert
     const goto_functiont &function,
     unsigned location_number_of_target);
 
+  /// Decide whether the target instruction is between the loop-havoc and the
+  /// evaluation of the loop guard.
+  bool is_instruction_in_transfomed_loop_condition(
+    const loop_idt &loop_id,
+    const goto_functiont &function,
+    unsigned location_number_of_target);
+
   const invariant_mapt &invariant_candidates;
   const std::map<loop_idt, std::set<exprt>> &assigns_map;
   goto_modelt &goto_model;

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

@@ -404,14 +404,33 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
         cause_loop_id, new_invariant_clause, return_cex->live_variables);
 
       // add the new cluase to the candidate invariants.
-      if(return_cex->is_violation_in_loop)
+      if(
+        return_cex->violation_location ==
+        cext::violation_locationt::in_condition)
+      {
+        // When the violation is happen in the loop guard, the new clause
+        // should hold for the both cases of
+        // 1. loop guard holds        --- loop_guard -> in_invariant
+        // 2. loop guard doesn't hold --- !loop_guard -> pos_invariant
+        in_invariant_clause_map[cause_loop_id] = and_exprt(
+          in_invariant_clause_map[cause_loop_id], new_invariant_clause);
+        pos_invariant_clause_map[cause_loop_id] = and_exprt(
+          pos_invariant_clause_map[cause_loop_id], new_invariant_clause);
+      }
+      else if(
+        return_cex->violation_location == cext::violation_locationt::in_loop)
       {
+        // When the violation is happen in the loop body, the new clause
+        // should hold for the case of
+        // loop guard holds        --- loop_guard -> in_invariant
         in_invariant_clause_map[cause_loop_id] = and_exprt(
           in_invariant_clause_map[cause_loop_id], new_invariant_clause);
       }
       else
       {
-        // violation happens post-loop.
+        // When the violation is happen after the loop body, the new clause
+        // should hold for the case of
+        // loop guard doesn't hold --- !loop_guard -> pos_invariant
         pos_invariant_clause_map[cause_loop_id] = and_exprt(
           pos_invariant_clause_map[cause_loop_id], new_invariant_clause);
       }