Infer loop assigns for DFCC with functions inlined

Author: qinheping

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

@@ -1,18 +1,18 @@
-KNOWNBUG
+CORE dfcc-only
 main.c
---dfcc main --apply-loop-contracts
+--dfcc main --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$
 ^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
 ^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
 ^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
-^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
-^\[main.\d+\] .* Check that loop invariant is preserved: 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$
 ^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
 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,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

@@ -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,13 +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, 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)
         {
@@ -379,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())
@@ -400,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,
@@ -436,8 +433,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);
@@ -488,6 +484,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,
@@ -506,6 +503,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);
@@ -526,9 +526,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);
     }
   }
 
@@ -548,10 +562,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(
@@ -561,7 +576,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, delmasrd@amazon.com
 #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)`
@@ -154,10 +157,67 @@ std::unordered_set<irep_idt> gen_loop_locals_set(
   return loop_locals;
 }
 
-assignst dfcc_infer_loop_assigns(
+/// Find all identifiers in `src`.
+static std::unordered_set<irep_idt>
+find_symbol_identifiers(const goto_programt &src)
+{
+  std::unordered_set<irep_idt> identifiers;
+  for(const auto &instruction : src.instructions)
+  {
+    // compute forward edges first
+    switch(instruction.type())
+    {
+    case ASSERT:
+    case ASSUME:
+    case GOTO:
+      find_symbols(instruction.condition(), identifiers);
+      break;
+
+    case FUNCTION_CALL:
+      find_symbols(instruction.call_lhs(), identifiers);
+      for(const auto &e : instruction.call_arguments())
+        find_symbols(e, identifiers);
+      break;
+    case ASSIGN:
+    case OTHER:
+
+    case SET_RETURN_VALUE:
+    case DECL:
+    case DEAD:
+      for(const auto &e : instruction.code().operands())
+      {
+        find_symbols(e, identifiers);
+      }
+      break;
+
+    case END_THREAD:
+    case END_FUNCTION:
+    case ATOMIC_BEGIN:
+    case ATOMIC_END:
+    case SKIP:
+    case LOCATION:
+    case CATCH:
+    case THROW:
+    case START_THREAD:
+      break;
+    case NO_INSTRUCTION_TYPE:
+    case INCOMPLETE_GOTO:
+      UNREACHABLE;
+      break;
+    }
+  }
+  return identifiers;
+}
+
+/// Infer loop assigns in the given `loop`. Loop assigns should depend
+/// on some identifiers in `candidate_targets`. `function_assigns_map`
+/// contains the function contracts used to infer loop assigns of
+/// function_call instructions.
+static assignst dfcc_infer_loop_assigns_for_loop(
   const local_may_aliast &local_may_alias,
   goto_functiont &goto_function,
   const dfcc_loop_nesting_graph_nodet &loop,
+  const std::unordered_set<irep_idt> &candidate_targets,
   message_handlert &message_handler,
   const namespacet &ns)
 {
@@ -176,6 +236,12 @@ assignst dfcc_infer_loop_assigns(
   assignst result;
   for(const auto &expr : assigns)
   {
+    // Skip targets that only depend on non-visible identifiers.
+    if(!depends_on(expr, candidate_targets))
+    {
+      continue;
+    }
+
     if(depends_on(expr, loop_locals))
     {
       // Target depends on loop locals, attempt widening to the root object
@@ -210,3 +276,103 @@ 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,
+  const goto_functiont &goto_function,
+  message_handlert &message_handler,
+  const namespacet &ns)
+{
+  messaget log(message_handler);
+
+  // Collect all candidate targets---identifiers visible in `goto_function`.
+  const auto candidate_targets = find_symbol_identifiers(goto_function.body);
+
+  // We infer loop assigns based on the copy of `goto_function`.
+  goto_functiont goto_function_copy;
+  goto_function_copy.copy_from(goto_function);
+
+  // Build the loop id map before inlining attempt. So that we can later
+  // distinguish loops in the original body and loops added by inlining.
+  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;
+
+  // 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;
+
+  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 are not 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());
+  // Update the body to make sure all goto correctly jump to valid targets.
+  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,
+        candidate_targets,
+        message_handler,
+        ns);
+    }
+  }
+  // Restore the function boyd of `malloc` and `free`.
+  goto_functions.function_map.insert(std::move(malloc_body));
+  goto_functions.function_map.insert(std::move(free_body));
+}