Add new __CPROVER_pointer_equals(p, q) predicate

Meant to replace `p == q in contract clauses, works as a hook
to override equality behaviour in assume contexts to make it
constructive. Add TODOs to remember overriding built-in ptr
equality with new predicate in requires/ensures clauses
expressions and user-defined ptr predicates bodies.

regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/main.c

@@ -0,0 +1,16 @@
+void foo(int *x, int *y)
+  // clang-format off
+  __CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+  __CPROVER_requires(__CPROVER_pointer_equals(y, x) || 1)
+  __CPROVER_assigns(*y)
+// clang-format on
+{
+  *y = 0;
+}
+
+void main()
+{
+  int *x;
+  int *y;
+  foo(x, y);
+}

regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/test.desc

@@ -0,0 +1,20 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
+^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: (UNKNOWN|FAILURE)$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: (UNKNOWN|FAILURE)$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that when `__CPROVER_pointer_equals` is used in disjunctions,
+the program accepts models where `__CPROVER_pointer_equals` evaluates to
+false and the target pointer remains invalid.

regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/main.c

@@ -0,0 +1,34 @@
+#include <stdlib.h>
+void foo(int *a, int *x, int *y)
+  // clang-format off
+  __CPROVER_requires(__CPROVER_is_fresh(a, sizeof(int)))
+  __CPROVER_requires(
+    (__CPROVER_pointer_equals(x,a) && y == NULL) ||
+    (x == NULL && __CPROVER_pointer_equals(y,a))
+  )
+  __CPROVER_assigns(y == NULL: *x)
+  __CPROVER_assigns(x == NULL: *y)
+// clang-format on
+{
+  if(y == NULL)
+  {
+    assert(0);
+    assert(__CPROVER_same_object(a, x));
+    *x = 0;
+  }
+  else
+  {
+    assert(0);
+    assert(x == NULL);
+    assert(__CPROVER_same_object(a, y));
+    *y = 0;
+  }
+}
+
+void main()
+{
+  int *a;
+  int *x;
+  int *y;
+  foo(a, x, y);
+}

regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/test.desc

@@ -0,0 +1,32 @@
+CORE dfcc-only
+main.c
+--dfcc main --enforce-contract foo
+^\[foo.assertion.\d+\] line 15 assertion 0: FAILURE$
+^\[foo.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)x\): SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: SUCCESS$
+^\[foo.assertion.\d+\] line 21 assertion 0: FAILURE$
+^\[foo.assertion.\d+\] line \d+ assertion x == \(\(.*\)NULL\): SUCCESS$
+^\[foo.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)y\): SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Illustrates the behaviour of `__CPROVER_pointer_equals` under disjunctions in assume contexts.
+The precondition of `foo` describes a disjunction of cases, either `x` equals `a` and `y` is null,
+or `x` is null and `y` equals `a`. The function `foo` branches on `y == NULL`.
+The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows
+that both cases of the disjunction expressed in the requires clause are reachable.

regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/main.c

@@ -0,0 +1,28 @@
+
+typedef struct
+{
+  int *a;
+  int *x;
+} ret_t;
+
+ret_t foo()
+  // clang-format off
+  __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, sizeof(int)))
+  __CPROVER_ensures(
+    __CPROVER_pointer_equals(
+      __CPROVER_return_value.x,
+      __CPROVER_return_value.a) || 1)
+  // clang-format on
+  ;
+
+void bar()
+{
+  ret_t ret = foo();
+  int *x = ret.x;
+  *x = 0; //expected to fail
+}
+
+void main()
+{
+  bar();
+}

regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/test.desc

@@ -0,0 +1,17 @@
+CORE dfcc-only
+main.c
+--dfcc main --replace-call-with-contract foo
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: (UNKNOWN|FAILURE)$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: (UNKNOWN|FAILURE)$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that when `__CPROVER_pointer_equals` is used in disjunctions,
+the program accepts models where `__CPROVER_pointer_equals` evaluates to
+false and the target pointer remains invalid.

regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/main.c

@@ -0,0 +1,49 @@
+#include <stdlib.h>
+typedef struct
+{
+  int *a;
+  int *x;
+  int *y;
+} ret_t;
+
+ret_t foo()
+  // clang-format off
+  __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, sizeof(int)))
+  __CPROVER_ensures((
+      __CPROVER_pointer_equals(
+        __CPROVER_return_value.x,
+        __CPROVER_return_value.a) &&
+      __CPROVER_return_value.y == NULL
+    ) || (
+      __CPROVER_return_value.x == NULL &&
+      __CPROVER_pointer_equals(
+        __CPROVER_return_value.y,
+        __CPROVER_return_value.a)))
+  // clang-format on
+  ;
+
+void bar()
+{
+  ret_t ret = foo();
+  int *a = ret.a;
+  int *x = ret.x;
+  int *y = ret.y;
+  if(y == NULL)
+  {
+    assert(0);
+    assert(__CPROVER_same_object(x, a));
+    *x = 0;
+  }
+  else
+  {
+    assert(0);
+    assert(x == NULL);
+    assert(__CPROVER_same_object(y, a));
+    *y = 0;
+  }
+}
+
+void main()
+{
+  bar();
+}

regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/test.desc

@@ -0,0 +1,32 @@
+CORE dfcc-only
+main.c
+--dfcc main --replace-call-with-contract foo
+^\[bar.assertion.\d+\] line 33 assertion 0: FAILURE$
+^\[bar.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)x\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$
+^\[bar.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: SUCCESS$
+^\[bar.assertion.\d+\] line 39 assertion 0: FAILURE$
+^\[bar.assertion.\d+\] line \d+ assertion x == \(\(.*\)NULL\): SUCCESS$
+^\[bar.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)y\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$
+^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Illustrates the behaviour of `__CPROVER_pointer_equals` under disjunctions in assume contexts.
+The postcondition of `foo` describes a disjunction of cases: either `x` equals `a` and `y` is null,
+or `x` is null and `y` equals `a`. The function `bar` branches on `y == NULL`.
+The test succeeds if the two `assert(0)` are falsifiable, which which shows that
+both cases of the disjunction expressed in the ensures clause of `foo` are reachable.

src/ansi-c/c_typecheck_expr.cpp

@@ -2591,7 +2591,19 @@ exprt c_typecheck_baset::do_special_functions(
 
   const irep_idt &identifier=to_symbol_expr(f_op).get_identifier();
 
-  if(identifier == CPROVER_PREFIX "is_fresh")
+  if(identifier == CPROVER_PREFIX "pointer_equals")
+  {
+    if(expr.arguments().size() != 2)
+    {
+      error().source_location = f_op.source_location();
+      error() << CPROVER_PREFIX "pointer_equals expects two operands; "
+              << expr.arguments().size() << "provided." << eom;
+      throw 0;
+    }
+    typecheck_function_call_arguments(expr);
+    return nil_exprt();
+  }
+  else if(identifier == CPROVER_PREFIX "is_fresh")
   {
     if(expr.arguments().size() != 2)
     {

src/ansi-c/cprover_builtin_headers.h

@@ -44,6 +44,7 @@ void __CPROVER_fence(const char *kind, ...);
 // contract-related functions
 __CPROVER_bool __CPROVER_is_freeable(const void *mem);
 __CPROVER_bool __CPROVER_was_freed(const void *mem);
+__CPROVER_bool __CPROVER_pointer_equals(void *p, void *q);
 __CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size);
 __CPROVER_bool __CPROVER_obeys_contract(void (*)(void), void (*)(void));
 // same as pointer_in_range with experimental support in contracts

src/ansi-c/library/cprover_contracts.c

@@ -1162,6 +1162,62 @@ void __CPROVER_contracts_make_invalid_pointer(void **ptr)
 #endif
 }
 
+/// \brief Implementation of the `pointer_equals` front-end predicate.
+///
+/// \param ptr1 First argument of the `pointer_equals` predicate
+/// \param ptr2 Second argument of the `pointer_equals` predicate
+/// \param write_set Write set which conveys the invocation context
+///   (requires/ensures clause, assert/assume context);
+///
+/// \details The behaviour is as follows:
+/// When \p set->assume_requires_ctx or \p set->assume_ensures_ctx is `true`,
+/// the predicate nondeterministically invalidates `*ptr1` and returns `false`,
+/// or checks that `ptr2` is either NULL or valid, and assigns `*ptr1` to `ptr2`.
+/// When \p set->assert_requires_ctx or \p set->assert_ensures_ctx is `true`,
+/// the predicate checks that both `*ptr1` and `ptr2` are either NULL or valid,
+/// and returns the value of (*ptr1 == ptr2).
+__CPROVER_bool __CPROVER_contracts_pointer_equals(
+  void **ptr1,
+  void *ptr2,
+  __CPROVER_contracts_write_set_ptr_t write_set)
+{
+__CPROVER_HIDE:;
+  __CPROVER_assert(
+    (write_set != 0) & ((write_set->assume_requires_ctx == 1) |
+                        (write_set->assert_requires_ctx == 1) |
+                        (write_set->assume_ensures_ctx == 1) |
+                        (write_set->assert_ensures_ctx == 1)),
+    "__CPROVER_is_fresh is used only in requires or ensures clauses");
+#ifdef __CPROVER_DFCC_DEBUG_LIB
+  __CPROVER_assert(
+    __CPROVER_rw_ok(write_set, sizeof(__CPROVER_contracts_write_set_t)),
+    "set readable");
+#endif
+  if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx)
+  {
+    if(__VERIFIER_nondet___CPROVER_bool())
+    {
+      __CPROVER_contracts_make_invalid_pointer(ptr1);
+      return 0;
+    }
+    __CPROVER_assert(
+      (ptr2 == 0) || __CPROVER_r_ok(ptr2, 0),
+      "pointer_equals is only called with valid pointers");
+    *ptr1 = ptr2;
+    return 1;
+  }
+  else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */
+  {
+    void *derefd = *ptr1;
+    __CPROVER_assert(
+      (derefd == 0) || __CPROVER_r_ok(derefd, 0),
+      "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;
+  }
+}
 
 /// \brief Implementation of the `is_fresh` front-end predicate.
 ///

src/goto-instrument/Makefile

@@ -29,6 +29,7 @@ SRC = accelerate/accelerate.cpp \
       contracts/dynamic-frames/dfcc_instrument_loop.cpp \
       contracts/dynamic-frames/dfcc_library.cpp \
       contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp \
+      contracts/dynamic-frames/dfcc_pointer_equals.cpp \
       contracts/dynamic-frames/dfcc_is_fresh.cpp \
       contracts/dynamic-frames/dfcc_pointer_in_range.cpp \
       contracts/dynamic-frames/dfcc_is_freeable.cpp \

src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md

@@ -29,6 +29,7 @@ Each of these translation passes is implemented in a specific class:
  @ref dfcc_instrumentt           | Implements @ref contracts-dev-spec-dfcc for @ref goto_functiont, @ref goto_programt, or subsequences of instructions of @ref goto_programt
  @ref dfcc_is_fresht             | Implements @ref contracts-dev-spec-is-fresh
  @ref dfcc_pointer_in_ranget     | Implements @ref contracts-dev-spec-pointer-in-range
+ @ref dfcc_pointer_equalst       | Implements @ref contracts-dev-spec-pointer-equals
  @ref dfcc_lift_memory_predicatest | Implements @ref contracts-dev-spec-memory-predicates-rewriting
  @ref dfcc_is_freeablet          | Implements @ref contracts-dev-spec-is-freeable
  @ref dfcc_obeys_contractt       | Implements @ref contracts-dev-spec-obeys-contract

src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md

@@ -174,6 +174,9 @@ Calls to `__CPROVER_obeys_contract` are rewritten as described in
 Calls to `__CPROVER_pointer_in_range_dfcc` are rewritten as described in
 @subpage contracts-dev-spec-pointer-in-range
 
+Calls to `__CPROVER_pointer_equals` are rewritten as described in
+@subpage contracts-dev-spec-pointer-equals
+
 For all other function or function pointer calls, we proceed as follows.
 
 If the function call has an LHS (i.e. its result is assigned to a return value

src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md

@@ -8,6 +8,9 @@ The C extensions for contract specification provide three pointer-related memory
 predicates:
 
 ```c
+// Holds iff ptr1 and ptr2 are both either null or valid and are equal.
+__CPROVER_bool __CPROVER_pointer_equals(void *ptr1, void* ptr2);
+
 // Holds iff ptr is pointing to an object distinct to all objects pointed to by
 // other __CPROVER_is_fresh occurrences in the contract's pre and post conditions
 __CPROVER_bool __CPROVER_is_fresh(void *ptr, size_t size);

src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-equals.md

@@ -0,0 +1,25 @@
+# Rewriting Calls to the __CPROVER_pointer_equals Predicate {#contracts-dev-spec-pointer-equals}
+
+Back to top @ref contracts-dev-spec
+
+@tableofcontents
+
+In goto programs encoding pre or post conditions (generated from the contract
+clauses) and in all user-defined functions, we simply replace calls to
+`__CPROVER_pointer_equals` with calls to the library implementation.
+
+```c
+__CPROVER_contracts_pointer_equals(
+    void **ptr1,
+    void *ptr2,
+    __CPROVER_contracts_write_set_ptr_t write_set);
+```
+
+This function implements the `__CPROVER_pointer_equals` behaviour in all
+possible contexts (contract checking vs replacement, requires vs ensures clause
+context, as described by the flags carried by the write set parameter).
+
+---
+ Prev | Next
+:-----|:------
+ @ref contracts-dev | @ref contracts-dev-spec-reminder

src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md

@@ -23,4 +23,4 @@ context, as described by the flags carried by the write set parameter).
 ---
  Prev | Next
 :-----|:------
- @ref contracts-dev | @ref contracts-dev-spec-reminder
+ @ref contracts-dev | @ref contracts-dev-spec-pointer-equals