Infer loop assigns for DFCC with functions inlined

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

@@ -0,0 +1,22 @@
+struct hole
+{
+  int pos;
+};
+
+void set_len(struct hole *h, unsigned long int new_len)
+{
+  h->pos = new_len;
+}
+
+int main()
+{
+  int i = 0;
+  struct hole h;
+  h.pos = 0;
+  for(i = 0; i < 5; i++)
+    // __CPROVER_assigns(h.pos, i)
+    __CPROVER_loop_invariant(h.pos == i)
+    {
+      set_len(&h, h.pos + 1);
+    }
+}

regression/contracts-dfcc/loop_assigns_inference-04/test.desc

@@ -0,0 +1,14 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.loop_invariant_base.\d+\] line \d+ Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line \d+ Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line \d+ Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line \d+ Check step was unwound for loop .*: SUCCESS$
+^\[set_len.assigns.\d+\] line \d+ Check that h\-\>pos is assignable: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks assigns h->pos is inferred correctly.

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

@@ -329,7 +329,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,
-  local_may_aliast &local_may_alias,
+  const assignst &inferred_assigns,
   const bool check_side_effect,
   message_handlert &message_handler,
   const namespacet &ns)
@@ -380,13 +380,11 @@ static struct contract_clausest default_loop_contract_clauses(
     else
     {
       // infer assigns clause targets if none given
-      auto inferred = dfcc_infer_loop_assigns(
-        local_may_alias, loop.instructions, loop.head->source_location(), ns);
       log.warning() << "No assigns clause provided for loop " << function_id
                     << "." << loop.latch->loop_number << " at "
                     << loop.head->source_location() << ". The inferred set {";
       bool first = true;
-      for(const auto &expr : inferred)
+      for(const auto &expr : inferred_assigns)
       {
         if(!first)
         {
@@ -398,7 +396,7 @@ static struct contract_clausest default_loop_contract_clauses(
       log.warning() << "} might be incomplete or imprecise, please provide an "
                        "assigns clause if the analysis fails."
                     << messaget::eom;
-      result.assigns.swap(inferred);
+      result.assigns = inferred_assigns;
     }
 
     if(result.decreases_clauses.empty())
@@ -416,14 +414,16 @@ 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,
+  const assignst &inferred_assigns,
   const bool check_side_effect,
   message_handlert &message_handler,
   dfcc_libraryt &library,
   symbol_table_baset &symbol_table)
 {
+  const namespacet ns(symbol_table);
   std::unordered_set<irep_idt> loop_locals =
     gen_loop_locals_set(loop_nesting_graph, loop_id);
 
@@ -433,12 +433,11 @@ static dfcc_loop_infot gen_dfcc_loop_info(
     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,
-    local_may_alias,
+    inferred_assigns,
     check_side_effect,
     message_handler,
     ns);
@@ -489,6 +488,7 @@ static dfcc_loop_infot gen_dfcc_loop_info(
 }
 
 dfcc_cfg_infot::dfcc_cfg_infot(
+  goto_modelt &goto_model,
   const irep_idt &function_id,
   goto_functiont &goto_function,
   const exprt &top_level_write_set,
@@ -507,6 +507,9 @@ dfcc_cfg_infot::dfcc_cfg_infot(
   // Clean up possible fake loops that are due to do { ... } while(0);
   simplify_gotos(goto_program, ns);
 
+  // From loop number to the inferred loop assigns.
+  std::map<std::size_t, assignst> inferred_loop_assigns_map;
+
   if(loop_contract_config.apply_loop_contracts)
   {
     messaget log(message_handler);
@@ -531,6 +534,14 @@ dfcc_cfg_infot::dfcc_cfg_infot(
     {
       topsorted_loops.push_back(idx);
     }
+
+    // We infer loop assigns for all loops in the function.
+    dfcc_infer_loop_assigns_for_function(
+      inferred_loop_assigns_map,
+      goto_model.goto_functions,
+      goto_function,
+      message_handler,
+      ns);
   }
 
   // At this point, either loop contracts were activated and the loop nesting
@@ -549,19 +560,21 @@ dfcc_cfg_infot::dfcc_cfg_infot(
 
   // generate dfcc_cfg_loop_info for loops and add to loop_info_map
   dirtyt dirty(goto_function);
-  local_may_aliast local_may_alias(goto_function);
 
   for(const auto &loop_id : topsorted_loops)
   {
+    auto inferred_loop_assigns =
+      inferred_loop_assigns_map[loop_nesting_graph[loop_id].latch->loop_number];
     loop_info_map.insert(
       {loop_id,
        gen_dfcc_loop_info(
          loop_nesting_graph,
          loop_id,
          function_id,
+         goto_function,
          loop_info_map,
          dirty,
-         local_may_alias,
+         inferred_loop_assigns,
          loop_contract_config.check_side_effect,
          message_handler,
          library,

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

@@ -21,6 +21,7 @@ Date: March 2023
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
+#include <goto-programs/goto_model.h>
 #include <goto-programs/goto_program.h>
 
 #include <goto-instrument/contracts/loop_contract_config.h>
@@ -242,6 +243,7 @@ class dfcc_cfg_infot
 {
 public:
   dfcc_cfg_infot(
+    goto_modelt &goto_model,
     const irep_idt &function_id,
     goto_functiont &goto_function,
     const exprt &top_level_write_set,

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

@@ -13,9 +13,13 @@ Author: Remi Delmas, [email protected]
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
 
+#include <goto-programs/goto_inline.h>
+
+#include <analyses/goto_rw.h>
 #include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/havoc_utils.h>
 
+#include "dfcc_loop_nesting_graph.h"
 #include "dfcc_root_object.h"
 
 /// Builds a call expression `object_whole(expr)`
@@ -46,10 +50,12 @@ depends_on(const exprt &expr, std::unordered_set<irep_idt> identifiers)
   return false;
 }
 
-assignst dfcc_infer_loop_assigns(
+assignst dfcc_infer_loop_assigns_for_loop(
   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
@@ -105,3 +111,99 @@ assignst dfcc_infer_loop_assigns(
 
   return result;
 }
+
+/// Remove assignments to `__CPROVER_dead_object` to avoid aliasing all targets
+/// that are assigned to `__CPROVER_dead_object`.
+static void remove_dead_object_assignment(goto_functiont &goto_function)
+{
+  Forall_goto_program_instructions(i_it, goto_function.body)
+  {
+    if(i_it->is_assign())
+    {
+      auto &lhs = i_it->assign_lhs();
+
+      if(
+        lhs.id() == ID_symbol &&
+        to_symbol_expr(lhs).get_identifier() == CPROVER_PREFIX "dead_object")
+      {
+        i_it->turn_into_skip();
+      }
+    }
+  }
+}
+
+void dfcc_infer_loop_assigns_for_function(
+  std::map<std::size_t, assignst> &inferred_loop_assigns_map,
+  goto_functionst &goto_functions,
+  goto_functiont &goto_function,
+  message_handlert &message_handler,
+  const namespacet &ns)
+{
+  messaget log(message_handler);
+
+  // We infer loop assigns based on the copy of `goto_function`.
+  goto_functiont goto_function_copy;
+  goto_function_copy.copy_from(goto_function);
+
+  // Map from targett in `goto_function_copy` to loop number.
+  std::
+    unordered_map<goto_programt::const_targett, std::size_t, const_target_hash>
+      loop_number_map;
+
+  // Build the loop id map before inlining attempt.
+  const auto loop_nesting_graph =
+    build_loop_nesting_graph(goto_function_copy.body);
+  {
+    auto topsorted = loop_nesting_graph.topsort();
+    // skip function without loop.
+    if(topsorted.empty())
+      return;
+
+    for(const auto id : topsorted)
+    {
+      loop_number_map.emplace(
+        loop_nesting_graph[id].head, loop_nesting_graph[id].latch->loop_number);
+    }
+  }
+
+  // We avoid inlining `malloc` and `free` whose variables should not be assigns.
+  auto malloc_body = goto_functions.function_map.extract(irep_idt("malloc"));
+  auto free_body = goto_functions.function_map.extract(irep_idt("free"));
+
+  // Inline all function calls in goto_function_copy.
+  goto_program_inline(
+    goto_functions, goto_function_copy.body, ns, log.get_message_handler());
+  goto_function_copy.body.update();
+  // Build the loop graph after inlining.
+  const auto inlined_loop_nesting_graph =
+    build_loop_nesting_graph(goto_function_copy.body);
+
+  // Alias analysis.
+  remove_dead_object_assignment(goto_function_copy);
+  local_may_aliast local_may_alias(goto_function_copy);
+
+  auto inlined_topsorted = inlined_loop_nesting_graph.topsort();
+
+  for(const auto inlined_id : inlined_topsorted)
+  {
+    // We only infer loop assigns for loops in the original function.
+    if(
+      loop_number_map.find(inlined_loop_nesting_graph[inlined_id].head) !=
+      loop_number_map.end())
+    {
+      const auto loop_number =
+        loop_number_map[inlined_loop_nesting_graph[inlined_id].head];
+      const auto inlined_loop = inlined_loop_nesting_graph[inlined_id];
+
+      inferred_loop_assigns_map[loop_number] = dfcc_infer_loop_assigns_for_loop(
+        local_may_alias,
+        goto_function_copy,
+        inlined_loop.instructions,
+        inlined_loop.head->source_location(),
+        message_handler,
+        ns);
+    }
+  }
+  goto_functions.function_map.insert(std::move(malloc_body));
+  goto_functions.function_map.insert(std::move(free_body));
+}

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(
+assignst dfcc_infer_loop_assigns_for_loop(
   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);
+
+// \brief Infer assigns clause targets for loops in `goto_function` from their
+// instructions and a may alias analysis at the function level (with inlining).
+void dfcc_infer_loop_assigns_for_function(
+  std::map<std::size_t, assignst> &inferred_loop_assigns_map,
+  goto_functionst &goto_functions,
+  goto_functiont &goto_function,
+  message_handlert &message_handler,
   const namespacet &ns);
 
 #endif

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

@@ -399,6 +399,7 @@ void dfcc_instrumentt::instrument_goto_program(
 
   // build control flow graph information
   dfcc_cfg_infot cfg_info(
+    goto_model,
     function_id,
     goto_function,
     write_set,
@@ -448,6 +449,7 @@ void dfcc_instrumentt::instrument_goto_function(
 
   // build control flow graph information
   dfcc_cfg_infot cfg_info(
+    goto_model,
     function_id,
     goto_function,
     write_set,