Synthesize loop assigns before loop invariants.

Loop invariants synthesis is dependent on loop-assigns clauses. So we target non assignable-violations until all assignable-violations are fixed.

Author: qinheping

regression/goto-synthesizer/loop_contracts_synthesis_08/main.c

@@ -0,0 +1,17 @@
+#include <stdlib.h>
+#define SIZE 80
+
+void main()
+{
+  unsigned long len;
+  __CPROVER_assume(len <= SIZE);
+  __CPROVER_assume(len >= 8);
+  const char *i = malloc(len);
+  const char *end = i + len;
+  char s = 0;
+
+  while(i != end)
+  {
+    s = *i++;
+  }
+}

regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^\[main.pointer\_dereference.\d+\] .* SUCCESS$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Check whether assigns clauses are synthesize before invariant clauses.

src/goto-synthesizer/cegis_verifier.cpp

@@ -586,143 +586,159 @@ optionalt<cext> cegis_verifiert::verify()
   }
 
   properties = checker->get_properties();
-  // Find the violation and construct counterexample from its trace.
-  for(const auto &property_it : properties)
+  bool target_violation_found = false;
+  auto target_violation_info = properties.begin()->second;
+
+  // Find target violation---the violation we want to fix next.
+  // A target violation is an assignable violation or the first violation that
+  // is not assignable violation.
+  for(const auto &property : properties)
   {
-    if(property_it.second.status != property_statust::FAIL)
+    if(property.second.status != property_statust::FAIL)
       continue;
 
-    // Store the violation that we want to fix with synthesized
-    // assigns/invariant.
-    first_violation = property_it.first;
-
-    // Type of the violation
-    cext::violation_typet violation_type = cext::violation_typet::cex_other;
-
-    // Decide the violation type from the description of violation
-
-    // The violation is a pointer OOB check.
-    if((property_it.second.description.find(
-          "dereference failure: pointer outside object bounds in") !=
-        std::string::npos))
+    // assignable violation found
+    if(property.second.description.find("assignable") != std::string::npos)
     {
-      violation_type = cext::violation_typet::cex_out_of_boundary;
-    }
-
-    // The violation is a null pointer check.
-    if(property_it.second.description.find("pointer NULL") != std::string::npos)
-    {
-      violation_type = cext::violation_typet::cex_null_pointer;
+      target_violation = property.first;
+      target_violation_info = property.second;
+      break;
     }
 
-    // The violation is a loop-invariant-preservation check.
-    if(property_it.second.description.find("preserved") != std::string::npos)
+    // Store the violation that we want to fix with synthesized
+    // assigns/invariant.
+    if(!target_violation_found)
     {
-      violation_type = cext::violation_typet::cex_not_preserved;
+      target_violation = property.first;
+      target_violation_info = property.second;
+      target_violation_found = true;
     }
+  }
 
-    // The violation is a loop-invariant-preservation check.
-    if(
-      property_it.second.description.find("invariant before entry") !=
-      std::string::npos)
-    {
-      violation_type = cext::violation_typet::cex_not_hold_upon_entry;
-    }
+  // Construct counterexample from first violation's trace.
+  // Type of the violation
+  cext::violation_typet violation_type = cext::violation_typet::cex_other;
 
-    // The violation is an assignable check.
-    if(property_it.second.description.find("assignable") != std::string::npos)
-    {
-      violation_type = cext::violation_typet::cex_assignable;
-    }
+  // Decide the violation type from the description of violation
 
-    // Compute the cause loop---the loop for which we synthesize loop contracts,
-    // and the counterexample.
+  // The violation is a pointer OOB check.
+  if((target_violation_info.description.find(
+        "dereference failure: pointer outside object bounds in") !=
+      std::string::npos))
+  {
+    violation_type = cext::violation_typet::cex_out_of_boundary;
+  }
 
-    // If the violation is an assignable check, we synthesize assigns targets.
-    // In the case, cause loops are all loops the violation is in. We keep
-    // adding the new assigns target to the most-inner loop that does not
-    // contain the new target until the assignable violation is resolved.
+  // The violation is a null pointer check.
+  if(
+    target_violation_info.description.find("pointer NULL") != std::string::npos)
+  {
+    violation_type = cext::violation_typet::cex_null_pointer;
+  }
 
-    // For other cases, we synthesize loop invariant clauses. We synthesize
-    // invariants for one loop at a time. So we return only the first cause loop
-    // although there can be multiple ones.
+  // The violation is a loop-invariant-preservation check.
+  if(target_violation_info.description.find("preserved") != std::string::npos)
+  {
+    violation_type = cext::violation_typet::cex_not_preserved;
+  }
 
-    log.debug() << "Start to compute cause loop ids." << messaget::eom;
+  // The violation is a loop-invariant-preservation check.
+  if(
+    target_violation_info.description.find("invariant before entry") !=
+    std::string::npos)
+  {
+    violation_type = cext::violation_typet::cex_not_hold_upon_entry;
+  }
 
-    const auto &trace = checker->get_traces()[property_it.first];
+  // The violation is an assignable check.
+  if(target_violation_info.description.find("assignable") != std::string::npos)
+  {
+    violation_type = cext::violation_typet::cex_assignable;
+  }
 
-    // Doing assigns-synthesis or invariant-synthesis
-    if(violation_type == cext::violation_typet::cex_assignable)
-    {
-      cext result(violation_type);
-      result.cause_loop_ids = get_cause_loop_id_for_assigns(trace);
-      result.checked_pointer = static_cast<const exprt &>(
-        property_it.second.pc->condition().find(ID_checked_assigns));
-      restore_functions();
-      return result;
-    }
+  // Compute the cause loop---the loop for which we synthesize loop contracts,
+  // and the counterexample.
 
-    // We construct the full counterexample only for violations other than
-    // assignable checks.
+  // If the violation is an assignable check, we synthesize assigns targets.
+  // In the case, cause loops are all loops the violation is in. We keep
+  // adding the new assigns target to the most-inner loop that does not
+  // contain the new target until the assignable violation is resolved.
 
-    // Although there can be multiple cause loop ids. We only synthesize
-    // loop invariants for the first cause loop.
-    const std::list<loop_idt> cause_loop_ids =
-      get_cause_loop_id(trace, property_it.second.pc);
+  // For other cases, we synthesize loop invariant clauses. We synthesize
+  // invariants for one loop at a time. So we return only the first cause loop
+  // although there can be multiple ones.
 
-    if(cause_loop_ids.empty())
-    {
-      log.debug() << "No cause loop found!" << messaget::eom;
-      restore_functions();
+  log.debug() << "Start to compute cause loop ids." << messaget::eom;
 
-      return cext(violation_type);
-    }
+  const auto &trace = checker->get_traces()[target_violation];
+  // Doing assigns-synthesis or invariant-synthesis
+  if(violation_type == cext::violation_typet::cex_assignable)
+  {
+    cext result(violation_type);
+    result.cause_loop_ids = get_cause_loop_id_for_assigns(trace);
+    result.checked_pointer = static_cast<const exprt &>(
+      target_violation_info.pc->condition().find(ID_checked_assigns));
+    restore_functions();
+    return result;
+  }
 
-    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;
+  // We construct the full counterexample only for violations other than
+  // assignable checks.
 
-    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)
-    {
-      // 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);
-    }
+  // Although there can be multiple cause loop ids. We only synthesize
+  // loop invariants for the first cause loop.
+  const std::list<loop_idt> cause_loop_ids =
+    get_cause_loop_id(trace, target_violation_info.pc);
 
+  if(cause_loop_ids.empty())
+  {
+    log.debug() << "No cause loop found!" << messaget::eom;
     restore_functions();
 
-    auto return_cex = build_cex(
-      trace,
-      get_loop_head(
-        cause_loop_ids.front().loop_number,
-        goto_model.goto_functions
-          .function_map[cause_loop_ids.front().function_id])
-        ->source_location());
-    return_cex.violated_predicate = property_it.second.pc->condition();
-    return_cex.cause_loop_ids = cause_loop_ids;
-    return_cex.violation_location = violation_location;
-    return_cex.violation_type = violation_type;
-
-    // The pointer checked in the null-pointer-check violation.
-    if(violation_type == cext::violation_typet::cex_null_pointer)
-    {
-      return_cex.checked_pointer = property_it.second.pc->condition()
-                                     .operands()[0]
-                                     .operands()[1]
-                                     .operands()[0];
-      INVARIANT(
-        return_cex.checked_pointer.id() == ID_symbol,
-        "Checking pointer symbol");
-    }
+    return cext(violation_type);
+  }
 
-    return return_cex;
+  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)
+  {
+    // 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),
+      target_violation_info.pc->location_number);
+  }
+
+  restore_functions();
+
+  auto return_cex = build_cex(
+    trace,
+    get_loop_head(
+      cause_loop_ids.front().loop_number,
+      goto_model.goto_functions
+        .function_map[cause_loop_ids.front().function_id])
+      ->source_location());
+  return_cex.violated_predicate = target_violation_info.pc->condition();
+  return_cex.cause_loop_ids = cause_loop_ids;
+  return_cex.violation_location = violation_location;
+  return_cex.violation_type = violation_type;
+
+  // The pointer checked in the null-pointer-check violation.
+  if(violation_type == cext::violation_typet::cex_null_pointer)
+  {
+    return_cex.checked_pointer = target_violation_info.pc->condition()
+                                   .operands()[0]
+                                   .operands()[1]
+                                   .operands()[0];
+    INVARIANT(
+      return_cex.checked_pointer.id() == ID_symbol, "Checking pointer symbol");
   }
 
-  UNREACHABLE;
+  return return_cex;
 }

src/goto-synthesizer/cegis_verifier.h

@@ -117,7 +117,7 @@ class cegis_verifiert
 
   /// Result counterexample.
   propertiest properties;
-  irep_idt first_violation;
+  irep_idt target_violation;
 
 protected:
   // Get the options same as using CBMC api without any flag, and

src/goto-synthesizer/dump_loop_contracts.cpp

@@ -91,16 +91,16 @@ void dump_loop_contracts(
         "loop " + std::to_string(invariant_entry.first.loop_number + 1) +
         " assigns ";
 
-      bool in_fisrt_iter = true;
+      bool in_first_iter = true;
       for(const auto &a : it_assigns->second)
       {
-        if(!in_fisrt_iter)
+        if(!in_first_iter)
         {
           assign_string += ",";
         }
         else
         {
-          in_fisrt_iter = false;
+          in_first_iter = false;
         }
         assign_string += expr2c(
           simplify_expr(a, ns), ns, expr2c_configurationt::clean_configuration);

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

@@ -94,6 +94,9 @@ void enumerative_loop_contracts_synthesizert::init_candidates()
 
       loop_idt new_id(function_p.first, loop_end->loop_number);
 
+      log.debug() << "Initialize candidates for the loop at "
+                  << loop_end->source_location() << messaget::eom;
+
       // we only synthesize invariants and assigns for unannotated loops
       if(loop_end->condition().find(ID_C_spec_loop_invariant).is_nil())
       {
@@ -372,7 +375,7 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
       new_invariant_clause = synthesize_strengthening_clause(
         terminal_symbols,
         return_cex->cause_loop_ids.front(),
-        verifier.first_violation);
+        verifier.target_violation);
       break;
 
     case cext::violation_typet::cex_assignable:

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h

@@ -53,7 +53,7 @@ class enumerative_loop_contracts_synthesizert
   /// to their original variables.
   void build_tmp_post_map();
 
-  /// Compute the depedent symbols for a loop with invariant-not-preserved
+  /// Compute the dependent symbols for a loop with invariant-not-preserved
   /// violation which happen after `new_clause` was added.
   std::set<symbol_exprt> compute_dependent_symbols(
     const loop_idt &cause_loop_id,

src/goto-synthesizer/expr_enumerator.cpp

@@ -208,7 +208,7 @@ std::vector<std::size_t> get_ones_pos(std::size_t v)
   return result;
 }
 
-/// Construct parition of `n` elements from a bit vector `v`.
+/// Construct partition of `n` elements from a bit vector `v`.
 /// For a bit vector with ones at positions (computed by `get_ones_pos`)
 /// (ones[0], ones[1], ..., ones[k-2]),
 /// the corresponding partition is
@@ -255,7 +255,7 @@ std::list<partitiont> non_leaf_enumeratort::get_partitions(
 
   // Initial `v` is with ones at positions (n-k+1, n-k+2, ..., n-2, n-1).
   std::size_t v = 0;
-  // Initial `end` (the last bit vectorr we enumerate) is with ones at
+  // Initial `end` (the last bit vector we enumerate) is with ones at
   // positions (1, 2, 3, ..., k-1).
   std::size_t end = 0;
   for(size_t i = 0; i < k - 1; i++)
@@ -412,5 +412,5 @@ void enumerator_factoryt::attach_productions(
 {
   const auto &ret = productions_map.insert({id, enumerators});
   INVARIANT(
-    ret.second, "Cannnot attach enumerators to a non-existing nonterminal.");
+    ret.second, "Cannot attach enumerators to a non-existing nonterminal.");
 }