Use demonic tracking for fresh ID set, check pointer predicate uniqueness

Replaces the array used to track fresh object IDs with a single nondet variable.
Add another nondet variable to track locations that store pointers on which
some pointer predicate was assumed or successfully asserted, and ensures
that at most one pointer predicate is established at any time.
Allows ensures clauses to establish different predicates wrt ensures,
by resetting the nondet tracker between requires and ensures clauses
evaluation in the contract wrapper.

Author: Remi Delmas

src/ansi-c/library/cprover_contracts.c

@@ -62,6 +62,15 @@ typedef struct
   /// \brief Array of void *pointers, indexed by their object ID
   /// or some other order
   void **elems;
+  /// \brief Equal to 1 if `fresh_id` is empty, 0 otherwise.
+  unsigned char fresh_id_empty;
+  /// \brief Demonic nondet variable ranging over the set of fresh object IDs.
+  __CPROVER_size_t fresh_id;
+  /// \brief Equal to 1 if `ptr_pred` is empty, 0 otherwise.
+  unsigned char ptr_pred_empty;
+  /// \brief Demonic nondet variable ranging over the set of locations storing
+  /// pointers on which predicates were assumed/asserted.
+  void **ptr_pred;
 } __CPROVER_contracts_obj_set_t;
 
 /// \brief Type of pointers to \ref __CPROVER_contracts_car_set_t.
@@ -261,7 +270,11 @@ __CPROVER_HIDE:;
     .nof_elems = 0,
     .is_empty = 1,
     .indexed_by_object_id = 1,
-    .elems = __CPROVER_allocate(nof_objects * sizeof(*(set->elems)), 1)};
+    .elems = __CPROVER_allocate(nof_objects * sizeof(*(set->elems)), 1),
+    .fresh_id_empty = 1,
+    .fresh_id = 0,
+    .ptr_pred_empty = 1,
+    .ptr_pred = 0};
 }
 
 /// \brief Initialises a \ref __CPROVER_contracts_obj_set_t object to use it
@@ -285,7 +298,74 @@ __CPROVER_HIDE:;
     .nof_elems = 0,
     .is_empty = 1,
     .indexed_by_object_id = 0,
-    .elems = __CPROVER_allocate(max_elems * sizeof(*(set->elems)), 1)};
+    .elems = __CPROVER_allocate(max_elems * sizeof(*(set->elems)), 1),
+    .fresh_id_empty = 1,
+    .fresh_id = 0,
+    .ptr_pred_empty = 1,
+    .ptr_pred = 0};
+}
+
+__CPROVER_bool __CPROVER_contracts_not_seen_is_fresh(
+  __CPROVER_contracts_obj_set_ptr_t set,
+  void *ptr)
+{
+__CPROVER_HIDE:;
+  return set->fresh_id_empty || __CPROVER_POINTER_OBJECT(ptr) != set->fresh_id;
+}
+
+void __CPROVER_contracts_record_fresh_id(
+  __CPROVER_contracts_obj_set_ptr_t set,
+  void *ptr)
+{
+__CPROVER_HIDE:;
+  if(set->fresh_id_empty)
+  {
+    set->fresh_id_empty = 0;
+    set->fresh_id = __CPROVER_POINTER_OBJECT(ptr);
+  }
+  else
+  {
+    set->fresh_id = __VERIFIER_nondet___CPROVER_bool()
+                      ? __CPROVER_POINTER_OBJECT(ptr)
+                      : set->fresh_id;
+  }
+}
+
+__CPROVER_bool __CPROVER_contracts_check_ptr_not_in_ptr_pred(
+  __CPROVER_contracts_obj_set_ptr_t set,
+  void **ptr)
+{
+__CPROVER_HIDE:;
+  return set->ptr_pred_empty || ptr != set->ptr_pred;
+}
+
+/// \brief Resets the nondet tracker for pointer predicates in \p set.
+/// Invoked right before evaluating contract ensures clauses. Since functions
+/// are allowed to modify the program state, resetting the tracker allows
+/// ensures clauses to establish a different pointer predicate on a pointer that
+/// was already targeted by the requires clause.
+void __CPROVER_contracts_obj_set_reset_ptr_pred(
+  __CPROVER_contracts_obj_set_ptr_t set)
+{
+__CPROVER_HIDE:;
+  set->ptr_pred_empty = 1;
+  set->ptr_pred = 0;
+}
+
+void __CPROVER_contracts_record_ptr_in_ptr_pred(
+  __CPROVER_contracts_obj_set_ptr_t set,
+  void **ptr)
+{
+__CPROVER_HIDE:;
+  if(set->ptr_pred_empty)
+  {
+    set->ptr_pred_empty = 0;
+    set->ptr_pred = ptr;
+  }
+  else
+  {
+    set->ptr_pred = __VERIFIER_nondet___CPROVER_bool() ? ptr : set->ptr_pred;
+  }
 }
 
 /// @brief Releases resources used by \p set.
@@ -1202,7 +1282,13 @@ __CPROVER_HIDE:;
     }
     __CPROVER_assert(
       (ptr2 == 0) || __CPROVER_r_ok(ptr2, 0),
-      "pointer_equals is only called with valid pointers");
+      "__CPROVER_pointer_equals is only called with valid pointers");
+    __CPROVER_assert(
+      __CPROVER_contracts_check_ptr_not_in_ptr_pred(
+        write_set->linked_is_fresh, ptr1),
+      "__CPROVER_pointer_equals does not conflict with other predicate");
+    __CPROVER_contracts_record_ptr_in_ptr_pred(
+      write_set->linked_is_fresh, ptr1);
     *ptr1 = ptr2;
     return 1;
   }
@@ -1211,11 +1297,21 @@ __CPROVER_HIDE:;
     void *derefd = *ptr1;
     __CPROVER_assert(
       (derefd == 0) || __CPROVER_r_ok(derefd, 0),
-      "pointer_equals is only called with valid pointers");
+      "__CPROVER_pointer_equals is only called with valid pointers");
     __CPROVER_assert(
       (ptr2 == 0) || __CPROVER_r_ok(ptr2, 0),
-      "pointer_equals is only called with valid pointers");
-    return derefd == ptr2;
+      "__CPROVER_pointer_equals is only called with valid pointers");
+    if(derefd != ptr2)
+    {
+      return 0;
+    }
+    __CPROVER_assert(
+      __CPROVER_contracts_check_ptr_not_in_ptr_pred(
+        write_set->linked_is_fresh, ptr1),
+      "__CPROVER_pointer_equals does not conflict with other predicate");
+    __CPROVER_contracts_record_ptr_in_ptr_pred(
+      write_set->linked_is_fresh, ptr1);
+    return 1;
   }
 }
 
@@ -1294,9 +1390,15 @@ __CPROVER_HIDE:;
       __CPROVER_contracts_make_invalid_pointer(elem);
       return 0;
     }
-
     void *ptr = __CPROVER_allocate(size, 0);
     *elem = ptr;
+    __CPROVER_assert(
+      __CPROVER_contracts_check_ptr_not_in_ptr_pred(
+        write_set->linked_is_fresh, elem),
+      "__CPROVER_is_fresh does not conflict with other predicate");
+    __CPROVER_contracts_record_ptr_in_ptr_pred(
+      write_set->linked_is_fresh, elem);
+    __CPROVER_contracts_record_fresh_id(write_set->linked_is_fresh, ptr);
 
     // record the object size for non-determistic bounds checking
     __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
@@ -1308,18 +1410,6 @@ __CPROVER_HIDE:;
     // __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
     // __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
 
-#ifdef __CPROVER_DFCC_DEBUG_LIB
-    // manually inlined below
-    __CPROVER_contracts_obj_set_add(write_set->linked_is_fresh, ptr);
-#else
-    __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
-    write_set->linked_is_fresh->nof_elems =
-      (write_set->linked_is_fresh->elems[object_id] != 0)
-        ? write_set->linked_is_fresh->nof_elems
-        : write_set->linked_is_fresh->nof_elems + 1;
-    write_set->linked_is_fresh->elems[object_id] = ptr;
-    write_set->linked_is_fresh->is_empty = 0;
-#endif
     return 1;
   }
   else if(write_set->assume_ensures_ctx)
@@ -1357,6 +1447,13 @@ __CPROVER_HIDE:;
 
     void *ptr = __CPROVER_allocate(size, 0);
     *elem = ptr;
+    __CPROVER_assert(
+      __CPROVER_contracts_check_ptr_not_in_ptr_pred(
+        write_set->linked_is_fresh, elem),
+      "__CPROVER_is_fresh does not conflict with other predicate");
+    __CPROVER_contracts_record_ptr_in_ptr_pred(
+      write_set->linked_is_fresh, elem);
+    __CPROVER_contracts_record_fresh_id(write_set->linked_is_fresh, ptr);
 
     // record the object size for non-determistic bounds checking
     __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
@@ -1369,17 +1466,6 @@ __CPROVER_HIDE:;
     __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
     __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
 
-#ifdef __CPROVER_DFCC_DEBUG_LIB
-    __CPROVER_contracts_obj_set_add(write_set->linked_allocated, ptr);
-#else
-    __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
-    write_set->linked_allocated->nof_elems =
-      (write_set->linked_allocated->elems[object_id] != 0)
-        ? write_set->linked_allocated->nof_elems
-        : write_set->linked_allocated->nof_elems + 1;
-    write_set->linked_allocated->elems[object_id] = ptr;
-    write_set->linked_allocated->is_empty = 0;
-#endif
     return 1;
   }
   else if(write_set->assert_requires_ctx | write_set->assert_ensures_ctx)
@@ -1390,34 +1476,22 @@ __CPROVER_HIDE:;
         (write_set->assume_ensures_ctx == 0),
       "only one context flag at a time");
 #endif
-    __CPROVER_contracts_obj_set_ptr_t seen = write_set->linked_is_fresh;
     void *ptr = *elem;
-    // null pointers or already seen pointers are not fresh
-#ifdef __CPROVER_DFCC_DEBUG_LIB
-    // manually inlined below
-    if((ptr == 0) || (__CPROVER_contracts_obj_set_contains(seen, ptr)))
-      return 0;
-#else
-    if(ptr == 0)
-      return 0;
-
-    __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
-
-    if(seen->elems[object_id] != 0)
-      return 0;
-#endif
-
-#ifdef __CPROVER_DFCC_DEBUG_LIB
-    // manually inlined below
-    __CPROVER_contracts_obj_set_add(seen, ptr);
-#else
-    seen->nof_elems =
-      (seen->elems[object_id] != 0) ? seen->nof_elems : seen->nof_elems + 1;
-    seen->elems[object_id] = ptr;
-    seen->is_empty = 0;
-#endif
-    // check size
-    return __CPROVER_r_ok(ptr, size);
+    if(
+      ptr != (void *)0 &&
+      __CPROVER_contracts_not_seen_is_fresh(write_set->linked_is_fresh, ptr) &&
+      __CPROVER_r_ok(ptr, size))
+    {
+      __CPROVER_assert(
+        __CPROVER_contracts_check_ptr_not_in_ptr_pred(
+          write_set->linked_is_fresh, elem),
+        "__CPROVER_is_fresh does not conflict with other predicate");
+      __CPROVER_contracts_record_ptr_in_ptr_pred(
+        write_set->linked_is_fresh, elem);
+      __CPROVER_contracts_record_fresh_id(write_set->linked_is_fresh, ptr);
+      return 1;
+    }
+    return 0;
   }
   else
   {
@@ -1484,13 +1558,33 @@ __CPROVER_HIDE:;
     __CPROVER_size_t max_offset = ub_offset - lb_offset;
     __CPROVER_assume(offset <= max_offset);
     *ptr = (char *)lb + offset;
+    __CPROVER_assert(
+      __CPROVER_contracts_check_ptr_not_in_ptr_pred(
+        write_set->linked_is_fresh, ptr),
+      "__CPROVER_pointer_in_range_dfcc does not conflict with other predicate");
+    __CPROVER_contracts_record_ptr_in_ptr_pred(write_set->linked_is_fresh, ptr);
     return 1;
   }
   else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */
   {
     __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(*ptr);
-    return __CPROVER_same_object(lb, *ptr) && lb_offset <= offset &&
-           offset <= ub_offset;
+    if(
+      __CPROVER_same_object(lb, *ptr) && lb_offset <= offset &&
+      offset <= ub_offset)
+    {
+      __CPROVER_assert(
+        __CPROVER_contracts_check_ptr_not_in_ptr_pred(
+          write_set->linked_is_fresh, ptr),
+        "__CPROVER_pointer_in_range_dfcc does not conflict with other "
+        "predicate");
+      __CPROVER_contracts_record_ptr_in_ptr_pred(
+        write_set->linked_is_fresh, ptr);
+      return 1;
+    }
+    else
+    {
+      return 0;
+    }
   }
 }
 

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

@@ -52,6 +52,7 @@ init_function_symbols(std::unordered_set<irep_idt> &function_symbols)
     function_symbols.insert(CPROVER_PREFIX
                             "contracts_obj_set_create_indexed_by_object_id");
     function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_release");
+    function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_reset_ptr_pred");
     function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_remove");
     function_symbols.insert(CPROVER_PREFIX "contracts_pointer_equals");
     function_symbols.insert(CPROVER_PREFIX "contracts_pointer_in_range_dfcc");

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

@@ -71,6 +71,8 @@ const std::map<dfcc_funt, irep_idt> create_dfcc_fun_to_name()
     {dfcc_funt::OBJ_SET_CREATE_APPEND,
      CONTRACTS_PREFIX "obj_set_create_append"},
     {dfcc_funt::OBJ_SET_RELEASE, CONTRACTS_PREFIX "obj_set_release"},
+    {dfcc_funt::OBJ_SET_RESET_PTR_PRED,
+     CONTRACTS_PREFIX "obj_set_reset_ptr_pred"},
     {dfcc_funt::OBJ_SET_ADD, CONTRACTS_PREFIX "obj_set_add"},
     {dfcc_funt::OBJ_SET_APPEND, CONTRACTS_PREFIX "obj_set_append"},
     {dfcc_funt::OBJ_SET_REMOVE, CONTRACTS_PREFIX "obj_set_remove"},
@@ -882,3 +884,14 @@ const code_function_callt dfcc_libraryt::obj_set_release_call(
   call.add_source_location() = source_location;
   return call;
 }
+
+const code_function_callt dfcc_libraryt::obj_set_reset_ptr_pred_call(
+  const exprt &obj_set_ptr,
+  const source_locationt &source_location)
+{
+  code_function_callt call(
+    dfcc_fun_symbol[dfcc_funt::OBJ_SET_RESET_PTR_PRED].symbol_expr(),
+    {obj_set_ptr});
+  call.add_source_location() = source_location;
+  return call;
+}

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

@@ -62,6 +62,8 @@ enum class dfcc_funt
   OBJ_SET_CREATE_APPEND,
   /// \see __CPROVER_contracts_obj_set_release
   OBJ_SET_RELEASE,
+  /// \see __CPROVER_contracts_obj_set_reset_ptr_pred
+  OBJ_SET_RESET_PTR_PRED,
   /// \see __CPROVER_contracts_obj_set_add
   OBJ_SET_ADD,
   /// \see __CPROVER_contracts_obj_set_append
@@ -451,6 +453,12 @@ class dfcc_libraryt
   const code_function_callt obj_set_release_call(
     const exprt &obj_set_ptr,
     const source_locationt &source_location);
+
+  /// \brief Builds call to
+  /// \ref __CPROVER_contracts_obj_set_reset_ptr_pred
+  const code_function_callt obj_set_reset_ptr_pred_call(
+    const exprt &obj_set_ptr,
+    const source_locationt &source_location);
 };
 
 #endif

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

@@ -631,6 +631,11 @@ void dfcc_wrapper_programt::encode_ensures_clauses()
       addr_of_ensures_write_set, addr_of_contract_write_set, wrapper_sl),
     wrapper_sl));
 
+  // reset the tracker of target pointers for pointer predicates
+  link_deallocated_contract.add(goto_programt::make_function_call(
+    library.obj_set_reset_ptr_pred_call(addr_of_is_fresh_set, wrapper_sl),
+    wrapper_sl));
+
   // fix calls to user-defined user-defined memory predicates
   memory_predicates.fix_calls(ensures_program);