CONTRACTS: new context tracking flags in write set

Enables checking for the presence of dynamic
allocations or deallocations in loop bodies
and transitively in the functions called from
loop bodies.

- Adds `allow_allocate` and `allow_deallocate`
  flags in the write set struct
- Adds two functions to set the flags.
- Modify `add_allocated` to fail an assertion when
  called on a write set with `allow_allocate`
  set to false.
- Modify `check_deallocate` to return false when
  called on a write set with `allow_deallocate`
  set to false.

Author: Remi Delmas

src/ansi-c/library/cprover_contracts.c

@@ -97,6 +97,10 @@ 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;
+  /// \brief True iff dynamic deallocation is allowed (default: true)
+  __CPROVER_bool allow_deallocate;
 } __CPROVER_contracts_write_set_t;
 
 /// \brief Type of pointers to \ref __CPROVER_contracts_write_set_t.
@@ -436,6 +440,8 @@ __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;
+  set->allow_deallocate = 1;
 }
 
 /// \brief Releases resources used by \p set.
@@ -474,6 +480,20 @@ __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 Forbids deallocation in functions that receive that write set.
+void __CPROVER_contracts_write_set_forbid_deallocate(
+  __CPROVER_contracts_write_set_ptr_t set)
+{
+  set->allow_deallocate = 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 +620,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
@@ -904,8 +945,8 @@ __CPROVER_HIDE:;
 /// \param[in] set Write set to check the deallocation against
 /// \param[in] ptr Deallocated pointer to check set to check the deallocation
 /// against
-/// \return True iff \p ptr is contained in \p set->contract_frees or
-/// \p set->allocated.
+/// \return True iff deallocation is allowed and \p ptr is contained in
+/// \p set->contract_frees or \p set->allocated.
 __CPROVER_bool __CPROVER_contracts_write_set_check_deallocate(
   __CPROVER_contracts_write_set_ptr_t set,
   void *ptr)
@@ -924,8 +965,9 @@ __CPROVER_HIDE:;
     set->allocated.indexed_by_object_id,
     "set->allocated is indexed by object id");
 #endif
-  return (ptr == 0) | (set->contract_frees.elems[object_id] == ptr) |
-         (set->allocated.elems[object_id] == ptr);
+  return (set->allow_deallocate) &
+         ((ptr == 0) | (set->contract_frees.elems[object_id] == ptr) |
+          (set->allocated.elems[object_id] == ptr));
 }
 
 /// \brief Checks the inclusion of the \p candidate->contract_assigns elements

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,10 @@ 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_FORBID_DEALLOCATE,
+     CONTRACTS_PREFIX "write_set_forbid_deallocate"},
     {dfcc_funt::WRITE_SET_INSERT_ASSIGNABLE,
      CONTRACTS_PREFIX "write_set_insert_assignable"},
     {dfcc_funt::WRITE_SET_INSERT_OBJECT_WHOLE,
@@ -91,6 +95,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,10 @@ 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_forbid_deallocate
+  WRITE_SET_FORBID_DEALLOCATE,
   /// \see __CPROVER_contracts_write_set_insert_assignable
   WRITE_SET_INSERT_ASSIGNABLE,
   /// \see __CPROVER_contracts_write_set_insert_object_whole
@@ -87,6 +91,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