Infer loop assigns for DFCC with functions inlined

Author: qinheping

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE dfcc-only
 main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=0$
@@ -15,4 +15,3 @@ main.c
 --
 This test checks loop locals are correctly removed during assigns inference so
 that the assign clause is correctly inferred.
-This test failed when using dfcc for loop contracts.

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,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks assigns h->pos is inferred correctly.

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

@@ -309,8 +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 assignst &inferred_assigns,
   const bool check_side_effect,
   message_handlert &message_handler,
   const namespacet &ns)
@@ -361,18 +360,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,
-        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 {";
       bool first = true;
-      for(const auto &expr : inferred)
+      for(const auto &expr : inferred_assigns)
       {
         if(!first)
         {
@@ -384,7 +376,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())
@@ -405,7 +397,7 @@ static dfcc_loop_infot gen_dfcc_loop_info(
   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,
@@ -429,8 +421,7 @@ static dfcc_loop_infot gen_dfcc_loop_info(
     loop_nesting_graph,
     loop_id,
     function_id,
-    goto_function,
-    local_may_alias,
+    inferred_assigns,
     check_side_effect,
     message_handler,
     ns);
@@ -481,6 +472,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,
@@ -499,6 +491,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);
@@ -523,6 +518,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
@@ -541,10 +544,11 @@ 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(
@@ -554,7 +558,7 @@ dfcc_cfg_infot::dfcc_cfg_infot(
          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,10 +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)`
@@ -117,7 +120,7 @@ std::unordered_set<irep_idt> gen_loop_locals_set(
   return loop_locals;
 }
 
-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,
@@ -132,11 +135,6 @@ assignst dfcc_infer_loop_assigns(
   // compute 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())
-      loop_locals.insert(target->decl_symbol().get_identifier());
-  }
 
   // widen or drop targets that depend on loop-locals or are non-constant,
   // ie. depend on other locations assigned by the loop.
@@ -179,3 +177,99 @@ assignst dfcc_infer_loop_assigns(
 
   return result;
 }
+
+/// Replace all assignment to `__CPROVER_dead_object` to avoid aliasing all targets
+/// 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 assign targets.
+  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

@@ -19,22 +19,31 @@ class messaget;
 class namespacet;
 class message_handlert;
 
+/// 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);
+
 // \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,
+   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,
+// \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);
 

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,