CONTRACTS: new context tracking flag in write set

This is meant to forbid dynamic allocations in loops.
Calls to `add_allocated` will fail an assertion when
called on a write set with `allow_allocate` set to false.

Author: Remi Delmas

src/ansi-c/library/cprover_contracts.c

@@ -97,6 +97,8 @@ typedef struct
   __CPROVER_bool assume_ensures_ctx;
   /// \brief True iff this write set checks ensures clauses in an assertion ctx
   __CPROVER_bool assert_ensures_ctx;
+  /// \brief True iff dynamic allocation is allowed (default: true)
+  __CPROVER_bool allow_allocate;
 } __CPROVER_contracts_write_set_t;
 
 /// \brief Type of pointers to \ref __CPROVER_contracts_write_set_t.
@@ -436,6 +438,7 @@ __CPROVER_HIDE:;
   set->assert_requires_ctx = assert_requires_ctx;
   set->assume_ensures_ctx = assume_ensures_ctx;
   set->assert_ensures_ctx = assert_ensures_ctx;
+  set->allow_allocate = 1;
 }
 
 /// \brief Releases resources used by \p set.
@@ -474,6 +477,13 @@ __CPROVER_HIDE:;
   // since they are owned by someone else.
 }
 
+/// \brief Forbids dynamic allocation in functions that receive that write set.
+void __CPROVER_contracts_write_set_forbid_allocate(
+  __CPROVER_contracts_write_set_ptr_t set)
+{
+  set->allow_allocate = 0;
+}
+
 /// \brief Inserts a snapshot of the range starting at \p ptr of size \p size
 /// at index \p idx in \p set->contract_assigns.
 /// \param[inout] set The set to update
@@ -600,14 +610,35 @@ __CPROVER_HIDE:;
 #endif
 }
 
-/// \brief Adds the pointer \p ptr to \p set->allocated.
+/// \brief Adds the dynamically allocated pointer \p ptr to \p set->allocated.
 /// \param[inout] set The set to update
-/// \param[in] ptr Pointer to an object declared using a `DECL x` or
-/// `x = __CPROVER_allocate(...)` GOTO instruction.
+/// \param[in] ptr Pointer to a dynamic object `x = __CPROVER_allocate(...)`.
 void __CPROVER_contracts_write_set_add_allocated(
   __CPROVER_contracts_write_set_ptr_t set,
   void *ptr)
 {
+__CPROVER_HIDE:;
+  __CPROVER_assert(set->allow_allocate, "dynamic allocation is allowed");
+#if DFCC_DEBUG
+  // call inlined below
+  __CPROVER_contracts_obj_set_add(&(set->allocated), ptr);
+#else
+  __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
+  set->allocated.nof_elems = (set->allocated.elems[object_id] != 0)
+                               ? set->allocated.nof_elems
+                               : set->allocated.nof_elems + 1;
+  set->allocated.elems[object_id] = ptr;
+  set->allocated.is_empty = 0;
+#endif
+}
+
+/// \brief Adds the pointer \p ptr to \p set->allocated.
+/// \param[inout] set The set to update
+/// \param[in] ptr Pointer to an object declared using `DECL x`.
+void __CPROVER_contracts_write_set_add_decl(
+  __CPROVER_contracts_write_set_ptr_t set,
+  void *ptr)
+{
 __CPROVER_HIDE:;
 #if DFCC_DEBUG
   // call inlined below

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

@@ -380,8 +380,7 @@ void dfcc_instrumentt::instrument_function_body(
   for(const auto &local_static : local_statics)
   {
     // automatically add local statics to the write set
-    insert_add_allocated_call(
-      function_id, write_set, local_static, begin, body);
+    insert_add_decl_call(function_id, write_set, local_static, begin, body);
 
     // automatically remove local statics to the write set
     insert_record_dead_call(function_id, write_set, local_static, end, body);
@@ -510,7 +509,7 @@ bool dfcc_instrumentt::must_track_decl_or_dead(
   return retval;
 }
 
-void dfcc_instrumentt::insert_add_allocated_call(
+void dfcc_instrumentt::insert_add_decl_call(
   const irep_idt &function_id,
   const exprt &write_set,
   const symbol_exprt &symbol_expr,
@@ -523,7 +522,7 @@ void dfcc_instrumentt::insert_add_allocated_call(
 
   payload.add(goto_programt::make_function_call(
     code_function_callt{
-      library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_ALLOCATED].symbol_expr(),
+      library.dfcc_fun_symbol[dfcc_funt::WRITE_SET_ADD_DECL].symbol_expr(),
       {write_set, address_of_exprt(symbol_expr)}},
     target->source_location()));
 
@@ -538,7 +537,7 @@ void dfcc_instrumentt::insert_add_allocated_call(
 /// ```c
 /// DECL x;
 /// ----
-/// insert_add_allocated_call(...);
+/// insert_add_decl_call(...);
 /// ```
 void dfcc_instrumentt::instrument_decl(
   const irep_idt &function_id,
@@ -552,7 +551,7 @@ void dfcc_instrumentt::instrument_decl(
 
   const auto &decl_symbol = target->decl_symbol();
   target++;
-  insert_add_allocated_call(
+  insert_add_decl_call(
     function_id, write_set, decl_symbol, target, goto_program);
   target--;
 }

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

@@ -175,15 +175,15 @@ class dfcc_instrumentt
   /// forward.
   /// ```
   /// IF !write_set GOTO skip_target;
-  /// CALL __CPROVER_contracts_write_set_add_allocated(write_set, &x);
+  /// CALL __CPROVER_contracts_write_set_add_decl(write_set, &x);
   /// skip_target: SKIP;
   /// ```
   /// \param function_id Name of the function in which the instructions is added
   /// \param write_set The write set to the symbol expr to
   /// \param symbol_expr The symbol to add to the write set
   /// \param target The instruction pointer to insert at
   /// \param goto_program the goto_program being instrumented
-  void insert_add_allocated_call(
+  void insert_add_decl_call(
     const irep_idt &function_id,
     const exprt &write_set,
     const symbol_exprt &symbol_expr,

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

@@ -79,6 +79,8 @@ const std::map<dfcc_funt, irep_idt> create_dfcc_fun_to_name()
      CONTRACTS_PREFIX "obj_set_contains_exact"},
     {dfcc_funt::WRITE_SET_CREATE, CONTRACTS_PREFIX "write_set_create"},
     {dfcc_funt::WRITE_SET_RELEASE, CONTRACTS_PREFIX "write_set_release"},
+    {dfcc_funt::WRITE_SET_FORBID_ALLOCATE,
+     CONTRACTS_PREFIX "write_set_forbid_allocate"},
     {dfcc_funt::WRITE_SET_INSERT_ASSIGNABLE,
      CONTRACTS_PREFIX "write_set_insert_assignable"},
     {dfcc_funt::WRITE_SET_INSERT_OBJECT_WHOLE,
@@ -91,6 +93,7 @@ const std::map<dfcc_funt, irep_idt> create_dfcc_fun_to_name()
      CONTRACTS_PREFIX "write_set_add_freeable"},
     {dfcc_funt::WRITE_SET_ADD_ALLOCATED,
      CONTRACTS_PREFIX "write_set_add_allocated"},
+    {dfcc_funt::WRITE_SET_ADD_DECL, CONTRACTS_PREFIX "write_set_add_decl"},
     {dfcc_funt::WRITE_SET_RECORD_DEAD,
      CONTRACTS_PREFIX "write_set_record_dead"},
     {dfcc_funt::WRITE_SET_RECORD_DEALLOCATED,

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

@@ -75,6 +75,8 @@ enum class dfcc_funt
   WRITE_SET_CREATE,
   /// \see __CPROVER_contracts_write_set_release
   WRITE_SET_RELEASE,
+  /// \see __CPROVER_contracts_write_set_forbid_allocate
+  WRITE_SET_FORBID_ALLOCATE,
   /// \see __CPROVER_contracts_write_set_insert_assignable
   WRITE_SET_INSERT_ASSIGNABLE,
   /// \see __CPROVER_contracts_write_set_insert_object_whole
@@ -87,6 +89,8 @@ enum class dfcc_funt
   WRITE_SET_ADD_FREEABLE,
   /// \see __CPROVER_contracts_write_set_add_allocated
   WRITE_SET_ADD_ALLOCATED,
+  /// \see __CPROVER_contracts_write_set_add_decl
+  WRITE_SET_ADD_DECL,
   /// \see __CPROVER_contracts_write_set_record_dead
   WRITE_SET_RECORD_DEAD,
   /// \see __CPROVER_contracts_write_set_record_deallocated