Synthesize loop assigns before loop invariants.

qinheping · qinheping · commit ae7d464166f1 · 2023-01-09T16:29:49.000-06:00
Loop invariants synthesis is dependent on loop-assigns clauses. So we don't target non assignable-violations until all assignable-violations are fixed.
diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_08/main.c b/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++;
+  }
+}
diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_08/test.desc b/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.
diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp
@@ -53,6 +53,44 @@ static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
   return false;
 }
 
+static const exprt &
+get_checked_pointer_from_null_pointer_check(const exprt &violation)
+{
+  // A NULL-pointer check is the negation of an equation between the checked
+  // pointer and a NULL pointer.
+  // ! (POINTER_OBJECT(NULL) == POINTER_OBJECT(ptr))
+  const equal_exprt &equal_expr = to_equal_expr(to_not_expr(violation).op());
+
+  const exprt &lhs_pointer_object = equal_expr.lhs();
+  const exprt &rhs_pointer_object = equal_expr.rhs();
+  INVARIANT(
+    lhs_pointer_object.id() == ID_pointer_object &&
+      rhs_pointer_object.id() == ID_pointer_object,
+    "Null pointer check is an equation between two pointer objects of "
+    "pointer-type operands.");
+
+  const exprt &lhs_pointer = lhs_pointer_object.operands()[0];
+  const exprt &rhs_pointer = rhs_pointer_object.operands()[0];
+
+  // NULL == ptr
+  if(
+    can_cast_expr<constant_exprt>(lhs_pointer) &&
+    is_null_pointer(*expr_try_dynamic_cast<constant_exprt>(lhs_pointer)))
+  {
+    return rhs_pointer;
+  }
+  // ptr == NULL
+  else if(
+    can_cast_expr<constant_exprt>(rhs_pointer) &&
+    is_null_pointer(*expr_try_dynamic_cast<constant_exprt>(rhs_pointer)))
+  {
+    return lhs_pointer;
+  }
+
+  // Not a equation with NULL on one side.
+  UNREACHABLE;
+}
+
 optionst cegis_verifiert::get_options()
 {
   optionst options;
@@ -94,6 +132,45 @@ optionst cegis_verifiert::get_options()
   return options;
 }
 
+cext::violation_typet
+cegis_verifiert::extract_violation_type(const std::string &description)
+{
+  cext::violation_typet violation_type = cext::violation_typet::cex_other;
+
+  // The violation is a pointer OOB check.
+  if((description.find(
+        "dereference failure: pointer outside object bounds in") !=
+      std::string::npos))
+  {
+    violation_type = cext::violation_typet::cex_out_of_boundary;
+  }
+
+  // The violation is a null pointer check.
+  if(description.find("pointer NULL") != std::string::npos)
+  {
+    violation_type = cext::violation_typet::cex_null_pointer;
+  }
+
+  // The violation is a loop-invariant-preservation check.
+  if(description.find("preserved") != std::string::npos)
+  {
+    violation_type = cext::violation_typet::cex_not_preserved;
+  }
+
+  // The violation is a loop-invariant-preservation check.
+  if(description.find("invariant before entry") != std::string::npos)
+  {
+    violation_type = cext::violation_typet::cex_not_hold_upon_entry;
+  }
+
+  // The violation is an assignable check.
+  if(description.find("assignable") != std::string::npos)
+  {
+    violation_type = cext::violation_typet::cex_assignable;
+  }
+  return violation_type;
+}
+
 std::list<loop_idt>
 cegis_verifiert::get_cause_loop_id_for_assigns(const goto_tracet &goto_trace)
 {
@@ -586,143 +663,118 @@ 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;
-    }
-
-    // The violation is a loop-invariant-preservation check.
-    if(property_it.second.description.find("preserved") != std::string::npos)
-    {
-      violation_type = cext::violation_typet::cex_not_preserved;
-    }
-
-    // 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;
+      target_violation = property.first;
+      target_violation_info = property.second;
+      break;
     }
 
-    // The violation is an assignable check.
-    if(property_it.second.description.find("assignable") != 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_assignable;
+      target_violation = property.first;
+      target_violation_info = property.second;
+      target_violation_found = true;
     }
+  }
 
-    // Compute the cause loop---the loop for which we synthesize loop contracts,
-    // and the counterexample.
-
-    // 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.
-
-    // 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.
+  // Decide the violation type from the description of violation
+  cext::violation_typet violation_type =
+    extract_violation_type(target_violation_info.description);
 
-    log.debug() << "Start to compute cause loop ids." << messaget::eom;
+  // Compute the cause loop---the loop for which we synthesize loop contracts,
+  // and the counterexample.
 
-    const auto &trace = checker->get_traces()[property_it.first];
+  // 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.
 
-    // 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;
-    }
+  // 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.
 
-    // We construct the full counterexample only for violations other than
-    // assignable checks.
+  log.debug() << "Start to compute cause loop ids." << messaget::eom;
 
-    // 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);
+  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;
+  }
 
-    if(cause_loop_ids.empty())
-    {
-      log.debug() << "No cause loop found!" << messaget::eom;
-      restore_functions();
+  // We construct the full counterexample only for violations other than
+  // assignable checks.
 
-      return cext(violation_type);
-    }
+  // 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);
 
-    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;
+  if(cause_loop_ids.empty())
+  {
+    log.debug() << "No cause loop found!" << messaget::eom;
+    restore_functions();
 
-    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);
-    }
+    return cext(violation_type);
+  }
 
-    restore_functions();
+  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 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");
-    }
+  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);
+  }
 
-    return return_cex;
+  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 = get_checked_pointer_from_null_pointer_check(
+      target_violation_info.pc->condition());
   }
 
-  UNREACHABLE;
+  return return_cex;
 }
diff --git a/src/goto-synthesizer/cegis_verifier.h b/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
@@ -137,6 +137,9 @@ class cegis_verifiert
   std::list<loop_idt>
   get_cause_loop_id_for_assigns(const goto_tracet &goto_trace);
 
+  // Extract the violation type from violation description.
+  cext::violation_typet extract_violation_type(const std::string &description);
+
   // Compute the location of the violation.
   cext::violation_locationt get_violation_location(
     const loop_idt &loop_id,
diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp b/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:
