SYNTHESIZER: Add counterexample-guided loop assigns synthesis

regression/goto-synthesizer/loop_contracts_synthesis_05/main.c

@@ -0,0 +1,51 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+struct blob
+{
+  char *data;
+};
+
+void main()
+{
+  struct blob *b = malloc(sizeof(struct blob));
+  __CPROVER_assume(b != NULL);
+
+  b->data = malloc(SIZE);
+  __CPROVER_assume(b->data != NULL);
+
+  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

@@ -1457,11 +1457,11 @@ void code_contractst::apply_loop_contracts(
       if(original_loop_number_map.count(it_instr) != 0)
         continue;
 
-      // Store loop number for
-      // ASSIGN ENTERED_LOOP = TRUE
+      // Store loop number for two type of instrumented instructions.
+      // ASSIGN ENTERED_LOOP = false  ---   head of transformed loops.
+      // ASSIGN ENTERED_LOOP = true   ---   end of transformed loops.
       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,14 @@ void instrument_spec_assignst::inclusion_check_assertion(
   comment += " is assignable";
   source_location.set_comment(comment);
 
-  dest.add(goto_programt::make_assertion(
-    inclusion_check_full(car, allow_null_lhs, include_stack_allocated),
-    source_location));
+  exprt inclusion_check =
+    inclusion_check_full(car, allow_null_lhs, include_stack_allocated);
+  // Record what target is checked.
+  auto &checked_assigns =
+    static_cast<exprt &>(inclusion_check.add(ID_checked_assigns));
+  checked_assigns = car.target();
+
+  dest.add(goto_programt::make_assertion(inclusion_check, source_location));
 }
 
 exprt instrument_spec_assignst::inclusion_check_single(

src/goto-instrument/contracts/utils.cpp

@@ -448,14 +448,20 @@ 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
+  return is_assignment_to_instrumented_variable(target, ENTERED_LOOP) &&
+         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;
-
-  return target->assign_rhs() == true_exprt();
+  return is_assignment_to_instrumented_variable(target, ENTERED_LOOP) &&
+         target->assign_rhs() == true_exprt();
 }
 
 bool is_assignment_to_instrumented_variable(

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,47 @@ 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)
+  {
+    // We are entering a loop.
+    if(is_transformed_loop_head(step.pc))
+    {
+      result.push_front(
+        loop_idt(step.function_id, original_loop_number_map[step.pc]));
+    }
+    // We are leaving a loop.
+    else 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 haven'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 +202,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 +472,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();
@@ -495,15 +536,15 @@ optionalt<cext> cegis_verifiert::verify()
     if(property_it.second.status != property_statust::FAIL)
       continue;
 
+    // Store the violation that we want to fix with synthesized
+    // assigns/invariant.
     first_violation = property_it.first;
-    exprt violated_predicate = property_it.second.pc->condition();
-
-    // The pointer checked in the null-pointer-check 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") !=
@@ -516,11 +557,6 @@ optionalt<cext> cegis_verifiert::verify()
     if(property_it.second.description.find("pointer NULL") != std::string::npos)
     {
       violation_type = cext::violation_typet::cex_null_pointer;
-      checked_pointer = property_it.second.pc->condition()
-                          .operands()[0]
-                          .operands()[1]
-                          .operands()[0];
-      INVARIANT(checked_pointer.id() == ID_symbol, "Checking pointer symbol");
     }
 
     // The violation is a loop-invariant-preservation check.
@@ -537,51 +573,97 @@ optionalt<cext> cegis_verifiert::verify()
       violation_type = cext::violation_typet::cex_not_hold_upon_entry;
     }
 
-    // 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);
+    // The violation is an assignable check.
+    if(property_it.second.description.find("assignable") != std::string::npos)
+    {
+      violation_type = cext::violation_typet::cex_assignable;
+    }
 
-    if(!cause_loop_id.has_value())
+    // 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;
+
+    const auto &trace = checker->get_traces()[property_it.first];
+
+    // 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;
+    }
+
+    // We construct the full counterexample only for violations other than
+    // assignable checks.
+
+    // 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);
+
+    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),
+    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;
+
     // 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.checked_pointer = checked_pointer;
-    return_cex.is_violation_in_loop = violation_in_loop;
+    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_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 return_cex;
   }