Add counterexample-guided loop assigns synthesis

Implement the functionality described below.

Motivation
---
This loop assigns synthesizer use the idea counter-example-guided synthesis (CEGIS) to synthesize loop assigns targets. It is based on the same CEGIS framework as the loop invariant synthesizer w
ith the following difference.

Cause Loop ID
---
In the loop invariant synthesizer, we say a loop is a cause loop if the violation is dependent on the loop's havoc instructions. Because invariant clauses affect the havoced values which could flow into variables outside the loop.
In the loop assigns synthesizer, we say a loop is a cause loop if the violation is in the loop. Because assigns clauses only affect the CAR of its own loop body.

Synthesizer
---
For an assignable violation with checked target `T`, the new assigns target will be `T`. If `T` is a non-constant target, e.g., `ptr[i]` with `i` also an assigns target, we widen it to `__CPROVER_POINTER_OBJECT(T)`. We add the new target to cause loop one by one starting from the most-inner one. Until the assignable violation is resolved.

Author: qinheping

regression/goto-synthesizer/loop_contracts_synthesis_05/main.c

@@ -0,0 +1,48 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+struct blob
+{
+  char *data;
+};
+
+void main()
+{
+  struct blob *b = malloc(sizeof(struct blob));
+  b->data = malloc(SIZE);
+
+  b->data[5] = 0;
+  unsigned result = 0;
+
+  unsigned arr[3] = {0, 0, 0};
+
+  for(unsigned int i = 0; i < SIZE; i++)
+  // clang-format off
+  // __CPROVER_assigns(i, result)
+  // clang-format on
+  {
+    result += 1;
+  }
+
+  for(unsigned int i = 0; i < SIZE; i++)
+  // clang-format off
+  // __CPROVER_assigns(i, arr[0])
+  // clang-format on
+  {
+    arr[0] += 1;
+  }
+
+  for(unsigned j = 0; j < SIZE; j++)
+  // __CPROVER_assigns(j, __CPROVER_POINTER_OBJECT(b->data))
+  {
+    for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    // __CPROVER_assigns(i, j, __CPROVER_POINTER_OBJECT(b->data))
+    // clang-format on
+    {
+      b->data[i] = 1;
+    }
+  }
+}

regression/goto-synthesizer/loop_contracts_synthesis_05/test.desc

@@ -0,0 +1,18 @@
+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.assigns.\d+\] .* Check that j is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that result is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that arr\[(.*)0\] is assignable: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test is a variation of contracts/loop_assigns-01.
+It shows that we can synthesize loop assigns pointer_object(b->data) that
+cannot be inferred by goto-instrument.

src/goto-instrument/contracts/contracts.cpp

@@ -1458,10 +1458,10 @@ void code_contractst::apply_loop_contracts(
         continue;
 
       // Store loop number for
-      // ASSIGN ENTERED_LOOP = TRUE
+      // ASSIGN ENTERED_LOOP = true
+      // ASSIGN ENTERED_LOOP = false
       if(
-        is_assignment_to_instrumented_variable(it_instr, ENTERED_LOOP) &&
-        it_instr->assign_rhs() == true_exprt())
+        is_transformed_loop_end(it_instr) || is_transformed_loop_head(it_instr))
       {
         const auto &assign_lhs =
           expr_try_dynamic_cast<symbol_exprt>(it_instr->assign_lhs());

src/goto-instrument/contracts/instrument_spec_assigns.cpp

@@ -708,9 +708,15 @@ void instrument_spec_assignst::inclusion_check_assertion(
   comment += " is assignable";
   source_location.set_comment(comment);
 
-  dest.add(goto_programt::make_assertion(
+  goto_programt::instructiont to_add = goto_programt::make_assertion(
     inclusion_check_full(car, allow_null_lhs, include_stack_allocated),
-    source_location));
+    source_location);
+  // Record what target is checked.
+  auto &checked_assigns =
+    static_cast<exprt &>(to_add.condition_nonconst().add(ID_checked_assigns));
+  checked_assigns = car.target();
+
+  dest.add(std::move(to_add));
 }
 
 exprt instrument_spec_assignst::inclusion_check_single(

src/goto-instrument/contracts/utils.cpp

@@ -448,9 +448,19 @@ void generate_history_variables_initialization(
   program.destructive_append(history);
 }
 
+bool is_transformed_loop_head(const goto_programt::const_targett &target)
+{
+  // The head of a transformed loop is
+  // ASSIGN entered_loop = false
+  if(!is_assignment_to_instrumented_variable(target, ENTERED_LOOP))
+    return false;
+
+  return target->assign_rhs() == false_exprt();
+}
+
 bool is_transformed_loop_end(const goto_programt::const_targett &target)
 {
-  // The end of the loop end of transformed loop is
+  // The end of a transformed loop is
   // ASSIGN entered_loop = true
   if(!is_assignment_to_instrumented_variable(target, ENTERED_LOOP))
     return false;

src/goto-instrument/contracts/utils.h

@@ -210,7 +210,10 @@ void generate_history_variables_initialization(
   const irep_idt &mode,
   goto_programt &program);
 
-/// Return true if `target` is the loop end of some transformed code.
+/// Return true if `target` is the head of some transformed loop.
+bool is_transformed_loop_head(const goto_programt::const_targett &target);
+
+/// Return true if `target` is the end of some transformed loop.
 bool is_transformed_loop_end(const goto_programt::const_targett &target);
 
 /// Return true if `target` is an assignment to an instrumented variable with

src/goto-synthesizer/cegis_verifier.cpp

@@ -32,6 +32,7 @@ Author: Qinheping Hu
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>
 #include <goto-checker/multi_path_symex_checker.h>
 #include <goto-instrument/contracts/contracts.h>
+#include <goto-instrument/contracts/instrument_spec_assigns.h>
 #include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/havoc_utils.h>
 #include <langapi/language_util.h>
@@ -93,11 +94,45 @@ optionst cegis_verifiert::get_options()
   return options;
 }
 
-optionalt<loop_idt> cegis_verifiert::get_cause_loop_id(
+std::list<loop_idt>
+cegis_verifiert::get_cause_loop_id_for_assigns(const goto_tracet &goto_trace)
+{
+  std::list<loop_idt> result;
+
+  // We say a loop is the cause loop of an assignable-violation if the inclusion
+  // check is in the loop.
+
+  // So we check what loops the last step of the trace is in.
+  // Transformed loop head:
+  // ASSIGN entered_loop = false
+  // Transformed loop end:
+  // ASSIGN entered_loop = true
+  for(const auto &step : goto_trace.steps)
+  {
+    if(is_transformed_loop_head(step.pc))
+    {
+      result.push_front(
+        loop_idt(step.function_id, original_loop_number_map[step.pc]));
+      continue;
+    }
+
+    if(is_transformed_loop_end(step.pc))
+    {
+      const loop_idt loop_id(
+        step.function_id, original_loop_number_map[step.pc]);
+      INVARIANT(result.front() == loop_id, "Leaving a loop we havn't entered.");
+      result.pop_front();
+    }
+  }
+  INVARIANT(!result.empty(), "The assignable violation is not in a loop.");
+  return result;
+}
+
+std::list<loop_idt> cegis_verifiert::get_cause_loop_id(
   const goto_tracet &goto_trace,
   const goto_programt::const_targett violation)
 {
-  optionalt<loop_idt> result;
+  std::list<loop_idt> result;
 
   // build the dependence graph
   const namespacet ns(goto_model.symbol_table);
@@ -165,7 +200,8 @@ optionalt<loop_idt> cegis_verifiert::get_cause_loop_id(
       // if it is dependent on the loop havoc.
       if(reachable_set.count(dependence_graph[from].get_node_id()))
       {
-        result = loop_idt(step.function_id, original_loop_number_map[step.pc]);
+        result.push_back(
+          loop_idt(step.function_id, original_loop_number_map[step.pc]));
         return result;
       }
     }
@@ -434,9 +470,12 @@ optionalt<cext> cegis_verifiert::verify()
     original_functions[fun_entry.first].copy_from(fun_entry.second.body);
   }
 
-  // Annotate the candidates tot the goto_model for checking.
+  // Annotate the candidates to the goto_model for checking.
   annotate_invariants(invariant_candidates, goto_model);
 
+  // Annotate assigns
+  annotate_assigns(assigns_map, goto_model);
+
   // Control verbosity.
   // We allow non-error output message only when verbosity is set to at least 9.
   const unsigned original_verbosity = log.get_message_handler().get_verbosity();
@@ -496,14 +535,18 @@ optionalt<cext> cegis_verifiert::verify()
       continue;
 
     first_violation = property_it.first;
-    exprt violated_predicate = property_it.second.pc->condition();
+    const auto &trace = checker->get_traces()[property_it.first];
+    const exprt &violated_predicate = property_it.second.pc->condition();
 
-    // The pointer checked in the null-pointer-check violation.
+    // The pointer checked in the null-pointer-check violation and assignable
+    // violation.
     exprt checked_pointer = true_exprt();
 
     // 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") !=
@@ -537,49 +580,89 @@ optionalt<cext> cegis_verifiert::verify()
       violation_type = cext::violation_typet::cex_not_hold_upon_entry;
     }
 
+    // The violation is an assignable check.
+    if(property_it.second.description.find("assignable") != std::string::npos)
+    {
+      violation_type = cext::violation_typet::cex_assignable;
+    }
+
+    // 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.
+
+    log.debug() << "Start to compute cause loop ids." << messaget::eom;
+
     // The loop which could be the cause of the violation.
-    // We say a loop is the cause loop if the violated predicate is dependent
-    // upon the write set of the loop.
-    optionalt<loop_idt> cause_loop_id = get_cause_loop_id(
-      checker->get_traces()[property_it.first], property_it.second.pc);
+    std::list<loop_idt> cause_loop_ids;
+    // Decide whether the violation is in the cause loop.
+    bool is_violation_in_loop;
+
+    // Doing assigns-synthesis or invariant-synthesis
+    if(violation_type == cext::violation_typet::cex_assignable)
+    {
+      is_violation_in_loop = true;
+
+      checked_pointer = static_cast<const exprt &>(
+        property_it.second.pc->condition().find(ID_checked_assigns));
+      cause_loop_ids = get_cause_loop_id_for_assigns(trace);
+      cext result(violation_type);
+      result.cause_loop_ids = cause_loop_ids;
+      result.checked_pointer = checked_pointer;
+      restore_functions();
+      return result;
+    }
+
+    // We construct the full counterexample only for violations other than
+    // assignable checks.
 
-    if(!cause_loop_id.has_value())
+    // Although there can be multiple cause loop ids. We only synthesize
+    // loop invariants for the first cause loop.
+    cause_loop_ids = get_cause_loop_id(trace, property_it.second.pc);
+
+    if(cause_loop_ids.empty())
     {
-      log.debug() << "No cause loop found!\n";
+      log.debug() << "No cause loop found!" << messaget::eom;
       restore_functions();
 
       return cext(violation_type);
     }
 
-    log.debug() << "Found cause loop with function id: "
-                << cause_loop_id.value().function_id
-                << ", and loop number: " << cause_loop_id.value().loop_number
-                << "\n";
-
-    // Decide whether the violation is in the cause loop.
-    bool violation_in_loop = is_instruction_in_transfomed_loop(
-      cause_loop_id.value(),
-      goto_model.get_goto_function(cause_loop_id.value().function_id),
+    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;
+
     // We always strengthen in_clause if the violation is
     // invariant-not-preserved.
     if(violation_type == cext::violation_typet::cex_not_preserved)
-      violation_in_loop = true;
+      is_violation_in_loop = true;
 
     restore_functions();
 
     auto return_cex = build_cex(
-      checker->get_traces()[property_it.first],
+      trace,
       get_loop_head(
-        cause_loop_id.value().loop_number,
+        cause_loop_ids.front().loop_number,
         goto_model.goto_functions
-          .function_map[cause_loop_id.value().function_id])
+          .function_map[cause_loop_ids.front().function_id])
         ->source_location());
     return_cex.violated_predicate = violated_predicate;
-    return_cex.cause_loop_id = cause_loop_id;
+    return_cex.cause_loop_ids = cause_loop_ids;
     return_cex.checked_pointer = checked_pointer;
-    return_cex.is_violation_in_loop = violation_in_loop;
+    return_cex.is_violation_in_loop = is_violation_in_loop;
     return_cex.violation_type = violation_type;
 
     return return_cex;