Infer loop assigns for DFCC with functions inlined

Author: qinheping

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.

regression/contracts/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/loop_assigns_inference-04/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--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

@@ -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);
@@ -527,9 +530,23 @@ dfcc_cfg_infot::dfcc_cfg_infot(
 
     auto topsorted = loop_nesting_graph.topsort();
 
+    bool has_loops_with_contracts = false;
     for(const auto idx : topsorted)
     {
       topsorted_loops.push_back(idx);
+      has_loops_with_contracts |= has_contract(
+        loop_nesting_graph[idx].latch, loop_contract_config.check_side_effect);
+    }
+
+    // We infer loop assigns for all loops in the function.
+    if(has_loops_with_contracts)
+    {
+      dfcc_infer_loop_assigns_for_function(
+        inferred_loop_assigns_map,
+        goto_model.goto_functions,
+        goto_function,
+        message_handler,
+        ns);
     }
   }
 
@@ -549,19 +566,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,