Detect loop locals with goto_rw in DFCC

Author: qinheping

regression/contracts-dfcc/loop_assigns_inference-02/main.c

@@ -10,11 +10,14 @@ void main()
 void foo()
 {
   int *b = malloc(SIZE * sizeof(int));
+  int *j;
   for(unsigned i = 0; i < SIZE; i++)
     // clang-format off
     __CPROVER_loop_invariant(i <= SIZE)
     // clang-format on
     {
+      j = malloc(SIZE * sizeof(int));
       b[i] = 1;
+      free(j);
     }
 }

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp

@@ -253,26 +253,6 @@ static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
   return false;
 }
 
-/// Collect identifiers that are local to this loop only
-/// (excluding nested loop).
-static std::unordered_set<irep_idt> gen_loop_locals_set(
-  const dfcc_loop_nesting_grapht &loop_nesting_graph,
-  const std::size_t loop_id)
-{
-  std::unordered_set<irep_idt> loop_locals;
-  for(const auto &target : loop_nesting_graph[loop_id].instructions)
-  {
-    auto loop_id_opt = dfcc_get_loop_id(target);
-    if(
-      target->is_decl() && loop_id_opt.has_value() &&
-      loop_id_opt.value() == loop_id)
-    {
-      loop_locals.insert(target->decl_symbol().get_identifier());
-    }
-  }
-  return loop_locals;
-}
-
 /// Compute subset of locals that must be tracked in the loop's write set.
 /// A local must be tracked if it is dirty or if it may be assigned by one
 /// of the inner loops.
@@ -329,6 +309,7 @@ static struct contract_clausest default_loop_contract_clauses(
   const dfcc_loop_nesting_grapht &loop_nesting_graph,
   const std::size_t loop_id,
   const irep_idt &function_id,
+  goto_functiont &goto_function,
   local_may_aliast &local_may_alias,
   const bool check_side_effect,
   message_handlert &message_handler,
@@ -381,7 +362,12 @@ static struct contract_clausest default_loop_contract_clauses(
     {
       // infer assigns clause targets if none given
       auto inferred = dfcc_infer_loop_assigns(
-        local_may_alias, loop.instructions, loop.head->source_location(), ns);
+        local_may_alias,
+        goto_function,
+        loop.instructions,
+        loop.head->source_location(),
+        message_handler,
+        ns);
       log.warning() << "No assigns clause provided for loop " << function_id
                     << "." << loop.latch->loop_number << " at "
                     << loop.head->source_location() << ". The inferred set {";
@@ -416,6 +402,7 @@ static dfcc_loop_infot gen_dfcc_loop_info(
   const dfcc_loop_nesting_grapht &loop_nesting_graph,
   const std::size_t loop_id,
   const irep_idt &function_id,
+  goto_functiont &goto_function,
   const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
   dirtyt &dirty,
   local_may_aliast &local_may_alias,
@@ -424,20 +411,25 @@ static dfcc_loop_infot gen_dfcc_loop_info(
   dfcc_libraryt &library,
   symbol_table_baset &symbol_table)
 {
-  std::unordered_set<irep_idt> loop_locals =
-    gen_loop_locals_set(loop_nesting_graph, loop_id);
+  const namespacet ns(symbol_table);
+  std::unordered_set<irep_idt> loop_locals = gen_loop_locals_set(
+    function_id,
+    goto_function,
+    loop_nesting_graph[loop_id].instructions,
+    message_handler,
+    ns);
 
   std::unordered_set<irep_idt> loop_tracked = gen_tracked_set(
     loop_nesting_graph.get_predecessors(loop_id),
     loop_locals,
     dirty,
     loop_info_map);
 
-  const namespacet ns(symbol_table);
   struct contract_clausest contract_clauses = default_loop_contract_clauses(
     loop_nesting_graph,
     loop_id,
     function_id,
+    goto_function,
     local_may_alias,
     check_side_effect,
     message_handler,
@@ -559,6 +551,7 @@ dfcc_cfg_infot::dfcc_cfg_infot(
          loop_nesting_graph,
          loop_id,
          function_id,
+         goto_function,
          loop_info_map,
          dirty,
          local_may_alias,

src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp

@@ -13,6 +13,7 @@ Author: Remi Delmas, [email protected]
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
 
+#include <analyses/goto_rw.h>
 #include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/havoc_utils.h>
 
@@ -46,18 +47,91 @@ depends_on(const exprt &expr, std::unordered_set<irep_idt> identifiers)
   return false;
 }
 
+/// Collect identifiers that are local to this loop only
+/// (excluding nested loop).
+/// A target is a loop local if
+/// 1. it is declared inside the loop, or
+/// 2. there is no write or read of it outside the loop.
+std::unordered_set<irep_idt> gen_loop_locals_set(
+  const irep_idt &function_id,
+  goto_functiont &goto_function,
+  const loopt &loop,
+  message_handlert &message_handler,
+  const namespacet &ns)
+{
+  std::unordered_set<irep_idt> loop_locals;
+  std::unordered_set<irep_idt> non_loop_locals;
+  // Ranges of all variables declared outside the loop.
+  rw_range_sett decl_rw_range_set(ns, message_handler);
+  // Ranges of all read/write outside the loop.
+  rw_range_sett non_loop_rw_range_set(ns, message_handler);
+
+  Forall_goto_program_instructions(i_it, goto_function.body)
+  {
+    // All variables declared in loops are loop locals.
+    if(i_it->is_decl() && loop.contains(i_it))
+    {
+      loop_locals.insert(i_it->decl_symbol().get_identifier());
+    }
+    // Record all other declared variables and their ranges.
+    else if(i_it->is_decl())
+    {
+      goto_rw(function_id, i_it, decl_rw_range_set);
+    }
+    // Record all writing/reading outside the loop.
+    else if(
+      (i_it->is_assign() || i_it->is_function_call()) && !loop.contains(i_it))
+    {
+      goto_rw(function_id, i_it, non_loop_rw_range_set);
+    }
+  }
+
+  // Check if declared variables are loop locals.
+  for(const auto &decl_rw : decl_rw_range_set.get_w_set())
+  {
+    bool is_loop_local = true;
+    // No write to the declared variable.
+    for(const auto &writing_rw : non_loop_rw_range_set.get_w_set())
+    {
+      if(decl_rw.first == writing_rw.first)
+      {
+        is_loop_local = false;
+        break;
+      }
+    }
+
+    // No read to the declared variable.
+    for(const auto &writing_rw : non_loop_rw_range_set.get_r_set())
+    {
+      if(decl_rw.first == writing_rw.first)
+      {
+        is_loop_local = false;
+        break;
+      }
+    }
+
+    if(is_loop_local)
+      loop_locals.insert(decl_rw.first);
+  }
+
+  return loop_locals;
+}
+
 assignst dfcc_infer_loop_assigns(
   const local_may_aliast &local_may_alias,
+  goto_functiont &goto_function,
   const loopt &loop_instructions,
   const source_locationt &loop_head_location,
+  message_handlert &message_handler,
   const namespacet &ns)
 {
   // infer
   assignst assigns;
   infer_loop_assigns(local_may_alias, loop_instructions, assigns);
 
   // compute locals
-  std::unordered_set<irep_idt> loop_locals;
+  std::unordered_set<irep_idt> loop_locals = gen_loop_locals_set(
+    irep_idt(), goto_function, loop_instructions, message_handler, ns);
   for(const auto &target : loop_instructions)
   {
     if(target->is_decl())

src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h

@@ -17,13 +17,25 @@ Author: Remi Delmas, [email protected]
 class source_locationt;
 class messaget;
 class namespacet;
+class message_handlert;
 
 // \brief Infer assigns clause targets for a loop from its instructions and a
 // may alias analysis at the function level.
 assignst dfcc_infer_loop_assigns(
   const local_may_aliast &local_may_alias,
+  goto_functiont &goto_function,
   const loopt &loop_instructions,
   const source_locationt &loop_head_location,
+  message_handlert &message_handler,
+  const namespacet &ns);
+
+/// Collect identifiers that are local to this loop only
+/// (excluding nested loop).
+std::unordered_set<irep_idt> gen_loop_locals_set(
+  const irep_idt &function_id,
+  goto_functiont &goto_function,
+  const loopt &loop,
+  message_handlert &message_handler,
   const namespacet &ns);
 
 #endif

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

@@ -298,6 +298,13 @@ dfcc_instrument_loopt::add_prehead_instructions(
     code_function_callt call = library.write_set_create_call(
       addr_of_loop_write_set,
       from_integer(assigns.size(), size_type()),
+      from_integer(0, size_type()),
+      false_exprt(),
+      false_exprt(),
+      false_exprt(),
+      false_exprt(),
+      true_exprt(),
+      true_exprt(),
       loop_head_location);
     pre_loop_head_instrs.add(
       goto_programt::make_function_call(call, loop_head_location));