Merge pull request #7457 from qinheping/goto-synthesizer-violation-location

SYNTHESIZER: Handle the case of violation in loop guards

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,9 +514,9 @@ 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
-  //    merged yet, we preprocess the goto model and run the symex checker on it
-  //    to simulate CBMC API.
+  // 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.
   //
   // 3. construct the formatted counterexample from the violated property and
@@ -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);
       }