Merge pull request #7551 from remi-delmas-3000/contracts-codegen-loop-assigns

CONTRACTS: refactor DFCC code for loop contracts

Author: remi-delmas-3000

src/ansi-c/library/cprover_contracts.c

@@ -72,7 +72,7 @@ typedef struct
   /// \brief Set of freeable pointers derived from the contract (indexed mode)
   __CPROVER_contracts_obj_set_t contract_frees;
   /// \brief Set of freeable pointers derived from the contract (append mode)
-  __CPROVER_contracts_obj_set_t contract_frees_replacement;
+  __CPROVER_contracts_obj_set_t contract_frees_append;
   /// \brief Set of objects allocated by the function under analysis
   /// (indexed mode)
   __CPROVER_contracts_obj_set_t allocated;
@@ -83,12 +83,9 @@ typedef struct
   /// (indexed mode)
   __CPROVER_contracts_obj_set_ptr_t linked_is_fresh;
   /// \brief Object set recording the is_fresh allocations in post conditions
-  /// (replacement mode only)
   __CPROVER_contracts_obj_set_ptr_t linked_allocated;
   /// \brief Object set recording the deallocations (used by was_freed)
   __CPROVER_contracts_obj_set_ptr_t linked_deallocated;
-  /// \brief True iff this write set is used for contract replacement
-  __CPROVER_bool replacement;
   /// \brief True iff the write set checks requires clauses in an assumption ctx
   __CPROVER_bool assume_requires_ctx;
   /// \brief True iff the write set checks requires clauses in an assertion ctx
@@ -97,6 +94,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.
@@ -388,7 +389,6 @@ __CPROVER_HIDE:;
 /// \param[inout] set Pointer to the object to initialise
 /// \param[in] contract_assigns_size Max size of the assigns clause
 /// \param[in] contract_frees_size Max size of the frees clause
-/// \param[in] replacement True iff this write set is used to replace a contract
 /// \param[in] assume_requires_ctx True iff this write set is used to check side
 /// effects in a requires clause in contract checking mode
 /// \param[in] assert_requires_ctx True iff this write set is used to check side
@@ -397,15 +397,20 @@ __CPROVER_HIDE:;
 /// side effects in an ensures clause in contract replacement mode
 /// \param[in] assert_ensures_ctx True iff this write set is used to check for
 /// side effects in an ensures clause in contract checking mode
+/// \param[in] allow_allocate True iff the context gobally allows dynamic
+/// allocation.
+/// \param[in] allow_deallocate True iff the context gobally allows dynamic
+/// deallocation.
 void __CPROVER_contracts_write_set_create(
   __CPROVER_contracts_write_set_ptr_t set,
   __CPROVER_size_t contract_assigns_size,
   __CPROVER_size_t contract_frees_size,
-  __CPROVER_bool replacement,
   __CPROVER_bool assume_requires_ctx,
   __CPROVER_bool assert_requires_ctx,
   __CPROVER_bool assume_ensures_ctx,
-  __CPROVER_bool assert_ensures_ctx)
+  __CPROVER_bool assert_ensures_ctx,
+  __CPROVER_bool allow_allocate,
+  __CPROVER_bool allow_deallocate)
 {
 __CPROVER_HIDE:;
 #ifdef DFCC_DEBUG
@@ -417,16 +422,8 @@ __CPROVER_HIDE:;
     &(set->contract_assigns), contract_assigns_size);
   __CPROVER_contracts_obj_set_create_indexed_by_object_id(
     &(set->contract_frees));
-  set->replacement = replacement;
-  if(replacement)
-  {
-    __CPROVER_contracts_obj_set_create_append(
-      &(set->contract_frees_replacement), contract_frees_size);
-  }
-  else
-  {
-    set->contract_frees_replacement.elems = 0;
-  }
+  __CPROVER_contracts_obj_set_create_append(
+    &(set->contract_frees_append), contract_frees_size);
   __CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->allocated));
   __CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->deallocated));
   set->linked_is_fresh = 0;
@@ -436,6 +433,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 = allow_allocate;
+  set->allow_deallocate = allow_deallocate;
 }
 
 /// \brief Releases resources used by \p set.
@@ -454,20 +453,16 @@ __CPROVER_HIDE:;
     __CPROVER_rw_ok(&(set->contract_frees.elems), 0),
     "contract_frees writable");
   __CPROVER_assert(
-    (set->replacement == 0) ||
-      __CPROVER_rw_ok(&(set->contract_frees_replacement.elems), 0),
-    "contract_frees_replacement writable");
+    __CPROVER_rw_ok(&(set->contract_frees_append.elems), 0),
+    "contract_frees_append writable");
   __CPROVER_assert(
     __CPROVER_rw_ok(&(set->allocated.elems), 0), "allocated writable");
   __CPROVER_assert(
     __CPROVER_rw_ok(&(set->deallocated.elems), 0), "deallocated writable");
 #endif
   __CPROVER_deallocate(set->contract_assigns.elems);
   __CPROVER_deallocate(set->contract_frees.elems);
-  if(set->replacement != 0)
-  {
-    __CPROVER_deallocate(set->contract_frees_replacement.elems);
-  }
+  __CPROVER_deallocate(set->contract_frees_append.elems);
   __CPROVER_deallocate(set->allocated.elems);
   __CPROVER_deallocate(set->deallocated.elems);
   // do not free set->linked_is_fresh->elems or set->deallocated_linked->elems
@@ -585,29 +580,44 @@ __CPROVER_HIDE:;
 
   // append pointer if available
 #ifdef DFCC_DEBUG
-  if(set->replacement)
-    __CPROVER_contracts_obj_set_append(&(set->contract_frees_replacement), ptr);
+  __CPROVER_contracts_obj_set_append(&(set->contract_frees_append), ptr);
 #else
-  if(set->replacement)
-  {
-    set->contract_frees_replacement.nof_elems =
-      set->contract_frees_replacement.watermark;
-    set->contract_frees_replacement
-      .elems[set->contract_frees_replacement.watermark] = ptr;
-    set->contract_frees_replacement.watermark += 1;
-    set->contract_frees_replacement.is_empty = 0;
-  }
+  set->contract_frees_append.nof_elems = set->contract_frees_append.watermark;
+  set->contract_frees_append.elems[set->contract_frees_append.watermark] = ptr;
+  set->contract_frees_append.watermark += 1;
+  set->contract_frees_append.is_empty = 0;
 #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
@@ -659,10 +669,6 @@ void __CPROVER_contracts_write_set_record_deallocated(
   void *ptr)
 {
 __CPROVER_HIDE:;
-#ifdef DFCC_DEBUG
-  __CPROVER_assert(set->replacement == 0, "!replacement");
-#endif
-
 #if DFCC_DEBUG
   // we record the deallocation to be able to evaluate was_freed post conditions
   __CPROVER_contracts_obj_set_add(&(set->deallocated), ptr);
@@ -735,7 +741,6 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_assignment(
 // manually inlined below
 {
 __CPROVER_HIDE:;
-  __CPROVER_assert(set->replacement == 0, "!replacement");
   __CPROVER_assert(
     ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
     "ptr NULL or writable up to size");
@@ -904,16 +909,13 @@ __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)
 {
 __CPROVER_HIDE:;
-#ifdef DFCC_DEBUG
-  __CPROVER_assert(set->replacement == 0, "!replacement");
-#endif
   __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
 
 #ifdef DFCC_DEBUG
@@ -924,16 +926,15 @@ __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
 /// in \p reference->contract_assigns or \p reference->allocated.
 ///
-/// \pre \p reference must not be in replacement mode.
-/// \pre \p candidate must be in replacement mode and \p candidate->allocated
-/// must be empty.
+/// \pre \p candidate->allocated must be empty.
 ///
 /// \param[in] reference Reference write set from a caller
 /// \param[in] candidate Candidate write set from a contract being replaced
@@ -944,11 +945,6 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_assigns_clause_inclusion(
   __CPROVER_contracts_write_set_ptr_t candidate)
 {
 __CPROVER_HIDE:;
-#ifdef DFCC_DEBUG
-  __CPROVER_assert(
-    reference->replacement == 0, "reference set in !replacement");
-  __CPROVER_assert(candidate->replacement != 0, "candidate set in replacement");
-#endif
   __CPROVER_bool incl = 1;
   __CPROVER_contracts_car_t *current = candidate->contract_assigns.elems;
   __CPROVER_size_t idx = candidate->contract_assigns.max_elems;
@@ -969,9 +965,7 @@ __CPROVER_HIDE:;
 /// \brief Checks the inclusion of the \p candidate->contract_frees elements
 /// in \p reference->contract_frees or \p reference->allocated.
 ///
-/// \pre \p reference must not be in replacement mode.
-/// \pre \p candidate must be in replacement mode and \p candidate->allocated
-/// must be empty.
+/// \pre \p candidate->allocated must be empty.
 ///
 /// \param[in] reference Reference write set from a caller
 /// \param[in] candidate Candidate write set from a contract being replaced
@@ -983,9 +977,6 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_frees_clause_inclusion(
 {
 __CPROVER_HIDE:;
 #ifdef DFCC_DEBUG
-  __CPROVER_assert(
-    reference->replacement == 0, "reference set in !replacement");
-  __CPROVER_assert(candidate->replacement != 0, "candidate set in replacement");
   __CPROVER_assert(
     reference->contract_frees.indexed_by_object_id,
     "reference->contract_frees is indexed by object id");
@@ -994,8 +985,8 @@ __CPROVER_HIDE:;
     "reference->allocated is indexed by object id");
 #endif
   __CPROVER_bool all_incl = 1;
-  void **current = candidate->contract_frees_replacement.elems;
-  __CPROVER_size_t idx = candidate->contract_frees_replacement.max_elems;
+  void **current = candidate->contract_frees_append.elems;
+  __CPROVER_size_t idx = candidate->contract_frees_append.max_elems;
 
 SET_CHECK_FREES_CLAUSE_INCLUSION_LOOP:
   while(idx != 0)
@@ -1030,13 +1021,8 @@ void __CPROVER_contracts_write_set_deallocate_freeable(
   __CPROVER_contracts_write_set_ptr_t target)
 {
 __CPROVER_HIDE:;
-#ifdef DFCC_DEBUG
-  __CPROVER_assert(set->replacement == 1, "set is in replacement");
-  __CPROVER_assert(
-    (target == 0) | (target->replacement == 0), "target is in !replacement");
-#endif
-  void **current = set->contract_frees_replacement.elems;
-  __CPROVER_size_t idx = set->contract_frees_replacement.max_elems;
+  void **current = set->contract_frees_append.elems;
+  __CPROVER_size_t idx = set->contract_frees_append.max_elems;
 SET_DEALLOCATE_FREEABLE_LOOP:
   while(idx != 0)
   {

src/goto-instrument/Makefile

@@ -26,6 +26,7 @@ SRC = accelerate/accelerate.cpp \
       contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp \
       contracts/dynamic-frames/dfcc_instrument.cpp \
       contracts/dynamic-frames/dfcc_spec_functions.cpp \
+      contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp \
       contracts/dynamic-frames/dfcc_contract_functions.cpp \
       contracts/dynamic-frames/dfcc_wrapper_program.cpp \
       contracts/dynamic-frames/dfcc_contract_handler.cpp \

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

@@ -92,14 +92,14 @@ parse_function_contract_pair(const irep_idt &cli_flag)
   else if(split.size() == 2)
   {
     auto function_name = split[0];
-    if(function_name.size() == 0)
+    if(function_name.empty())
     {
       throw invalid_function_contract_pair_exceptiont{
         "couldn't find function name before '/' in '" + cli_flag_str + "'",
         correct_format_message};
     }
     auto contract_name = split[1];
-    if(contract_name.size() == 0)
+    if(contract_name.empty())
     {
       throw invalid_function_contract_pair_exceptiont{
         "couldn't find contract name after '/' in '" + cli_flag_str + "'",
@@ -191,14 +191,21 @@ dfcct::dfcct(
     instrument(goto_model, message_handler, utils, library),
     memory_predicates(goto_model, utils, library, instrument, message_handler),
     spec_functions(goto_model, message_handler, utils, library, instrument),
+    contract_clauses_codegen(
+      goto_model,
+      message_handler,
+      utils,
+      library,
+      spec_functions),
     contract_handler(
       goto_model,
       message_handler,
       utils,
       library,
       instrument,
       memory_predicates,
-      spec_functions),
+      spec_functions,
+      contract_clauses_codegen),
     swap_and_wrap(
       goto_model,
       message_handler,
@@ -483,6 +490,8 @@ void dfcct::instrument_other_functions()
 
   goto_model.goto_functions.update();
 
+  // TODO specialise the library functions for the max size of
+  // loop and function contracts
   if(to_check.has_value())
   {
     log.status() << "Specializing cprover_contracts functions for assigns "

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

@@ -33,6 +33,7 @@ Author: Remi Delmas, [email protected]
 #include <util/irep.h>
 #include <util/message.h>
 
+#include "dfcc_contract_clauses_codegen.h"
 #include "dfcc_contract_handler.h"
 #include "dfcc_instrument.h"
 #include "dfcc_library.h"
@@ -208,13 +209,15 @@ class dfcct
   message_handlert &message_handler;
   messaget log;
 
-  // hold the global state of the transformation (caches etc.)
+  // Singletons that hold the global state of the program transformation
+  // (caches etc.)
   dfcc_utilst utils;
   dfcc_libraryt library;
   namespacet ns;
   dfcc_instrumentt instrument;
   dfcc_lift_memory_predicatest memory_predicates;
   dfcc_spec_functionst spec_functions;
+  dfcc_contract_clauses_codegent contract_clauses_codegen;
   dfcc_contract_handlert contract_handler;
   dfcc_swap_and_wrapt swap_and_wrap;