Use demonic tracking for fresh ID set, checking ptr 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.

Author: Remi Delmas

Diff for: 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,61 @@ __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;
+}
+
+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 +1269,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 +1284,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 +1377,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 +1397,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 +1434,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 +1453,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 +1463,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 +1545,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;
+    }
   }
 }