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. 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,19 @@
+#include <stdlib.h>
+#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,12 @@
+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$
+--
+--
+Checks whether CBMC synthesizes loop invariants for checks 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
+--
+Checks if synthesized contracts are dumped correctly.

regression/goto-synthesizer/loop_contracts_synthesis_07/main.c

@@ -0,0 +1,19 @@
+#include <stdlib.h>
+#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,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$
+^\[main.pointer\_dereference.\d+].*SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether CBMC synthesizes loop invariants for checks located 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
+--
+Checks if synthesized contracts are dumped correctly.

src/goto-synthesizer/cegis_verifier.cpp

@@ -211,7 +211,63 @@ std::list<loop_idt> cegis_verifiert::get_cause_loop_id(
   return result;
 }
 
-bool cegis_verifiert::is_instruction_in_transfomed_loop(
+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_transformed_loop_condition(
+       loop_id, function, location_number_of_target))
+  {
+    return cext::violation_locationt::in_condition;
+  }
+
+  if(is_instruction_in_transformed_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_transformed_loop_condition(
+  const loop_idt &loop_id,
+  const goto_functiont &function,
+  unsigned location_number_of_target)
+{
+  // The transformed loop condition is a set of instructions from
+  // loop havocing instructions
+  // to
+  // if(!guard) GOTO EXIT
+  unsigned location_number_of_havocing = 0;
+  for(auto it = function.body.instructions.begin();
+      it != function.body.instructions.end();
+      ++it)
+  {
+    // Record the location number of the beginning 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_transformed_loop(
   const loop_idt &loop_id,
   const goto_functiont &function,
   unsigned location_number_of_target)
@@ -458,7 +514,7 @@ optionalt<cext> cegis_verifiert::verify()
   //
   // 1. annotate and apply the loop contracts stored in `invariant_candidates`.
   //
-  // 2. run the CBMC API to verify the intrumented goto model. As the API is not
+  // 2. run the CBMC API to verify the instrumented goto model. As the API is not
   //    merged yet, we preprocess the goto model and run the symex checker on it
   //    to simulate CBMC API.
   // TODO: ^^^ replace the symex checker once the real API is merged.
@@ -530,7 +586,7 @@ optionalt<cext> cegis_verifiert::verify()
   }
 
   properties = checker->get_properties();
-  // Find the violation and construct conterexample from its trace.
+  // Find the violation and construct counterexample from its trace.
   for(const auto &property_it : properties)
   {
     if(property_it.second.status != property_statust::FAIL)
@@ -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,16 +68,15 @@ 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 happens
+  violation_locationt violation_location = violation_locationt::in_loop;
 
   // We collect havoced evaluations of havoced variables and their object sizes
   // and pointer offsets.
 
   // __CPROVER_OBJECT_SIZE
   std::unordered_map<exprt, mp_integer, irep_hash> object_sizes;
-  // all the valuation of havoced variables with primitived type.
+  // all the valuation of havoced variables with primitive type.
   std::unordered_map<exprt, mp_integer, irep_hash> havoced_values;
   // __CPROVER_POINTER_OFFSET
   std::unordered_map<exprt, mp_integer, irep_hash> havoced_pointer_offsets;
@@ -88,7 +94,7 @@ class cext
   std::list<loop_idt> cause_loop_ids;
 };
 
-/// Verifier that take a goto program as input, and ouptut formatted
+/// Verifier that take a goto program as input, and output formatted
 /// counterexamples for counterexample-guided-synthesis.
 class cegis_verifiert
 {
@@ -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();
 
@@ -141,7 +153,14 @@ class cegis_verifiert
 
   /// Decide whether the target instruction is in the body of the transformed
   /// loop specified by `loop_id`.
-  bool is_instruction_in_transfomed_loop(
+  bool is_instruction_in_transformed_loop(
+    const loop_idt &loop_id,
+    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_transformed_loop_condition(
     const loop_idt &loop_id,
     const goto_functiont &function,
     unsigned location_number_of_target);
@@ -160,7 +179,7 @@ class cegis_verifiert
   std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
     original_loop_number_map;
 
-  /// Loop havoc instructions instrumneted during applying loop contracts.
+  /// Loop havoc instructions instrumented during applying loop contracts.
   std::unordered_set<goto_programt::const_targett, const_target_hash>
     loop_havoc_set;
 };

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

@@ -217,7 +217,7 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_same_object_predicate(
 {
   // The same object predicate says that the checked pointer points to the
   // same object as it pointed before entering the loop.
-  // It works for the array-manuplating loops where only offset of pointer
+  // It works for the array-manipulating loops where only offset of pointer
   // are modified but not the object pointers point to.
   return same_object(
     checked_pointer, unary_exprt(ID_loop_entry, checked_pointer));
@@ -228,7 +228,7 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause(
   const loop_idt &cause_loop_id,
   const irep_idt &violation_id)
 {
-  // Synthesis of strengthning clauses is a enumerate-and-check proecess.
+  // Synthesis of strengthening clauses is a enumerate-and-check process.
   // We first construct the enumerator for the following grammar.
   // And then enumerate clause and check that if it can make the invariant
   // inductive.
@@ -343,17 +343,17 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
   cegis_verifiert verifier(combined_invariant, assigns_map, goto_model, log);
 
   // Set of symbols the violation may be dependent on.
-  // We enumerate strenghening clauses built from symbols from the set.
+  // We enumerate strengthening clauses built from symbols from the set.
   std::set<symbol_exprt> dependent_symbols;
-  // Set of symbols we used to enumerate strenghening clauses.
+  // Set of symbols we used to enumerate strengthening clauses.
   std::vector<exprt> terminal_symbols;
 
   auto return_cex = verifier.verify();
 
   while(return_cex.has_value())
   {
     exprt new_invariant_clause = true_exprt();
-    // Synthsize the new_clause
+    // Synthesize the new_clause
     // We use difference strategies for different type of violations.
     switch(return_cex->violation_type)
     {
@@ -394,7 +394,7 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
         new_invariant_clause != true_exprt(),
         "failed to synthesized meaningful clause");
 
-      // There could be tmp_post varialbes in the synthesized clause.
+      // There could be tmp_post variables in the synthesized clause.
       // We substitute them with their original variables.
       replace_tmp_post(new_invariant_clause, tmp_post_map);
 
@@ -403,15 +403,34 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
       dependent_symbols = compute_dependent_symbols(
         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)
+      // add the new clause to the candidate invariants.
+      if(
+        return_cex->violation_location ==
+        cext::violation_locationt::in_condition)
+      {
+        // When the violation happens 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 happens 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 happens 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);
       }