Merge pull request #7763 from remi-delmas-3000/contracts-fix-loop-assigns-function-parameter

CONTRACTS: track function parameters explicitly

Author: remi-delmas-3000

regression/contracts-dfcc/loop_assigns_function_paramters/main.c

@@ -0,0 +1,19 @@
+#include <stdlib.h>
+
+void decr(size_t n)
+{
+  for(; n--;)
+    // clang-format off
+    __CPROVER_assigns(n)
+    __CPROVER_decreases(n)
+    // clang-format on
+    {
+    }
+}
+
+int main()
+{
+  size_t n;
+  decr(n);
+  return 0;
+}

regression/contracts-dfcc/loop_assigns_function_paramters/test.desc

@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts --enforce-contract decr
+^\[decr.loop_assigns.\d+] line \d+ Check assigns clause inclusion for loop decr.0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test checks that function parameters are automatically added to the function
+write set when they are assigned from the body of a loop.

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

@@ -291,6 +291,13 @@ class dfcc_cfg_infot
     return top_level_write_set;
   }
 
+  /// Returns the set of top level symbols that must be tracked explicitly in
+  /// the top level write set of the function.
+  const std::unordered_set<irep_idt> &get_top_level_tracked()
+  {
+    return top_level_tracked;
+  }
+
 private:
   const irep_idt &function_id;
   goto_functiont &goto_function;

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

@@ -490,6 +490,25 @@ void dfcc_instrumentt::instrument_goto_function(
     insert_record_dead_call(function_id, write_set, local_static, end, body);
   }
 
+  const code_typet &code_type = to_code_type(
+    dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id)
+      .type);
+  const auto &top_level_tracked = cfg_info.get_top_level_tracked();
+
+  // automatically add/remove function parameters that must be tracked in the
+  // function write set (they must be explicitly tracked if they are assigned
+  // in the body of a loop)
+  for(const auto &param : code_type.parameters())
+  {
+    const irep_idt &param_id = param.get_identifier();
+    if(top_level_tracked.find(param_id) != top_level_tracked.end())
+    {
+      symbol_exprt param_symbol{param.get_identifier(), param.type()};
+      insert_add_decl_call(function_id, write_set, param_symbol, begin, body);
+      insert_record_dead_call(function_id, write_set, param_symbol, end, body);
+    }
+  }
+
   remove_skip(body);
 
   // recalculate numbers, etc.