CONTRACTS: support pointer_in_range_dfcc predicate

Adds support for pointer_in_range_dfcc in ensures and
requires clauses and user-defined predicates. This is a
temporary workaround to the fact that pointer_in_range
is lowered by the front-end.

Author: Remi Delmas

Diff for: regression/contracts-dfcc/memory-predicates-pointer-in-range-nondet/main.c

@@ -0,0 +1,42 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+// A vtable is a struct containing function pointers
+typedef struct vtable_s
+{
+  int (*f)(void);
+} vtable_t;
+
+int return_0()
+{
+  return 0;
+}
+
+int return_1()
+{
+  return 1;
+}
+
+// we have two possible vtables
+vtable_t vtable_0 = {.f = &return_0};
+vtable_t vtable_1 = {.f = &return_1};
+
+// foo takes a vtable and calls f
+int foo(vtable_t *vtable)
+  // clang-format off
+__CPROVER_requires(
+  // vtable is nondeterministic pointer to one of two objects
+    __CPROVER_pointer_in_range_dfcc(&vtable_0, vtable, &vtable_0) ||
+    __CPROVER_pointer_in_range_dfcc(&vtable_1, vtable, &vtable_1))
+__CPROVER_ensures(__CPROVER_return_value == 0 || __CPROVER_return_value == 1)
+// clang-format on
+{
+CALL:
+  return vtable->f();
+}
+
+int main()
+{
+  vtable_t *vtable;
+  foo(vtable);
+}

Diff for: regression/contracts-dfcc/memory-predicates-pointer-in-range-nondet/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--restrict-function-pointer foo.CALL/return_0,return_1 --nondet-static-exclude vtable_0 --nondet-static-exclude vtable_1 --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Demonstrates the use of __CPROVER_pointer_in_range_dfcc to define nondeterministic
+pointers to one or more targets.

Diff for: regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void foo(char *arr, size_t size, char *cur)
+  // clang-format off
+__CPROVER_requires(
+    (0 < size && size < __CPROVER_max_malloc_size) &&
+    __CPROVER_is_fresh(arr, size) &&
+    __CPROVER_pointer_in_range_dfcc(arr, cur, arr + size))
+__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(arr, cur, arr + size))
+// clang-format on
+{
+  assert(__CPROVER_r_ok(arr, size));
+  assert(__CPROVER_same_object(arr, cur));
+  assert(arr <= cur && cur <= arr + size);
+}
+
+int main()
+{
+  char *arr;
+  size_t size;
+  char *cur;
+  foo(arr, size, cur);
+}

Diff for: regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks that assuming pointer-in-range as preconditions establishes a state
+in which the definition of the predicate holds.

Diff for: regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void foo(char *arr, size_t size, char *cur)
+  // clang-format off
+__CPROVER_requires(
+    (0 < size && size < __CPROVER_max_malloc_size) &&
+    __CPROVER_is_fresh(arr, size) &&
+    __CPROVER_pointer_in_range_dfcc(arr, cur, arr + size))
+__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(
+  arr, cur /*, arr + size missing arg */))
+// clang-format on
+{
+  assert(__CPROVER_r_ok(arr, size));
+  assert(__CPROVER_same_object(arr, cur));
+  assert(arr <= cur && cur <= arr + size);
+}
+
+int main()
+{
+  char *arr;
+  size_t size;
+  char *cur;
+  foo(arr, size, cur);
+}

Diff for: regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
+^.*error: __CPROVER_pointer_in_range_dfcc expects three arguments$
+^EXIT=(1|64)$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+--
+Checks that badly typed occurrences of __CPROVER_pointer_in_range_dfcc are detected.

Diff for: regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void foo(char *arr, size_t size, char *cur)
+  // clang-format off
+__CPROVER_requires(
+    (0 < size && size < __CPROVER_max_malloc_size) &&
+    __CPROVER_is_fresh(arr, size) &&
+    __CPROVER_pointer_in_range_dfcc(arr, cur, arr + size))
+__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(
+  arr, cur, 2 /* wrong type arg */))
+// clang-format on
+{
+  assert(__CPROVER_r_ok(arr, size));
+  assert(__CPROVER_same_object(arr, cur));
+  assert(arr <= cur && cur <= arr + size);
+}
+
+int main()
+{
+  char *arr;
+  size_t size;
+  char *cur;
+  foo(arr, size, cur);
+}

Diff for: regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
+^.*error: __CPROVER_pointer_in_range_dfcc expects pointer-typed arguments$
+^EXIT=(1|64)$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+--
+Checks that badly typed occurrences of __CPROVER_pointer_in_range_dfcc are detected.

Diff for: src/ansi-c/c_typecheck_expr.cpp

@@ -2334,6 +2334,29 @@ exprt c_typecheck_baset::do_special_functions(
     // returning nil leaves the call expression in place
     return nil_exprt();
   }
+  else if(identifier == CPROVER_PREFIX "pointer_in_range_dfcc")
+  {
+    // same as pointer_in_range with experimental support for DFCC contracts
+    // -- do not use
+    if(expr.arguments().size() != 3)
+    {
+      throw invalid_source_file_exceptiont{
+        CPROVER_PREFIX "pointer_in_range_dfcc expects three arguments",
+        expr.source_location()};
+    }
+
+    for(const auto &arg : expr.arguments())
+    {
+      if(arg.type().id() != ID_pointer)
+      {
+        throw invalid_source_file_exceptiont{
+          CPROVER_PREFIX
+          "pointer_in_range_dfcc expects pointer-typed arguments",
+          arg.source_location()};
+      }
+    }
+    return nil_exprt();
+  }
   else if(identifier == CPROVER_PREFIX "same_object")
   {
     if(expr.arguments().size()!=2)

Diff for: src/ansi-c/cprover_builtin_headers.h

@@ -50,6 +50,8 @@ __CPROVER_bool __CPROVER_is_freeable(const void *mem);
 __CPROVER_bool __CPROVER_was_freed(const void *mem);
 __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
+__CPROVER_bool __CPROVER_pointer_in_range_dfcc(void *lb, void *ptr, void *ub);
 void __CPROVER_old(const void *);
 void __CPROVER_loop_entry(const void *);
 

Diff for: src/ansi-c/library/cprover_contracts.c

@@ -1292,6 +1292,51 @@ __CPROVER_HIDE:;
   }
 }
 
+__CPROVER_bool __CPROVER_contracts_pointer_in_range_dfcc(
+  void *lb,
+  void **ptr,
+  void *ub,
+  __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_pointer_in_range_dfcc is used only in requires or ensures "
+    "clauses");
+  __CPROVER_assert(__CPROVER_r_ok(lb, 0), "lb pointer must be valid");
+  __CPROVER_assert(__CPROVER_r_ok(ub, 0), "ub pointer must be valid");
+  __CPROVER_assert(
+    __CPROVER_same_object(lb, ub),
+    "lb and ub pointers must have the same object");
+  __CPROVER_ssize_t lb_offset = __CPROVER_POINTER_OFFSET(lb);
+  __CPROVER_ssize_t ub_offset = __CPROVER_POINTER_OFFSET(ub);
+  __CPROVER_assert(
+    lb_offset <= ub_offset, "lb and ub pointers must be ordered");
+  if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx)
+  {
+    if(__VERIFIER_nondet___CPROVER_bool())
+      return 0;
+
+    // add nondet offset
+    __CPROVER_size_t offset = __VERIFIER_nondet_size();
+
+    // this cast is safe because we prove that ub and lb are ordered
+    __CPROVER_size_t max_offset = (__CPROVER_size_t)(ub_offset - lb_offset);
+    __CPROVER_assume(offset <= max_offset);
+    *ptr = (char *)lb + offset;
+    return 1;
+  }
+  else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */
+  {
+    __CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(*ptr);
+    return __CPROVER_same_object(lb, *ptr) && lb_offset <= offset &&
+           offset <= ub_offset;
+  }
+}
+
 /// \brief Returns the start address of the conditional address range found at
 /// index \p idx in  \p set->contract_assigns.
 void *__CPROVER_contracts_write_set_havoc_get_assignable_target(

Diff for: src/goto-instrument/Makefile

@@ -20,6 +20,7 @@ SRC = accelerate/accelerate.cpp \
       contracts/dynamic-frames/dfcc_utils.cpp \
       contracts/dynamic-frames/dfcc_library.cpp \
       contracts/dynamic-frames/dfcc_is_fresh.cpp \
+      contracts/dynamic-frames/dfcc_pointer_in_range.cpp \
       contracts/dynamic-frames/dfcc_is_freeable.cpp \
       contracts/dynamic-frames/dfcc_obeys_contract.cpp \
       contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp \

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

@@ -28,6 +28,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_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

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

@@ -171,7 +171,8 @@ Calls to `__CPROVER_is_fresh` are rewritten as described in
 Calls to `__CPROVER_obeys_contract` are rewritten as described in
 @subpage contracts-dev-spec-obeys-contract
 
-Calls to `__CPROVER_obeys_contract` are rewritten as described in @subpage contracts-dev-spec-obeys-contract
+Calls to `__CPROVER_pointer_in_range_dfcc` are rewritten as described in
+@subpage contracts-dev-spec-pointer-in-range
 
 For all other function or function pointer calls, we proceed as follows.
 

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

@@ -12,6 +12,10 @@ predicates:
 // other __CPROVER_is_fresh occurrences in the contract's pre and post conditions
 __CPROVER_bool __CPROVER_is_fresh(void *ptr, size_t size);
 
+// Holds iff ptr is a valid pointer pointing between lb and ub pointers.
+// \pre lb and ub must be valid pointers pointing in the same object.
+__CPROVER_bool __CPROVER_pointer_in_range_dfcc(void *lb, void *ptr, void *ub);
+
 // Holds iff the function pointer \p fptr points to a function satisfying
 // \p contract.
 __CPROVER_bool __CPROVER_obeys_contract(void (*fptr)(void), void (*contract)(void));

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

@@ -0,0 +1,26 @@
+# Rewriting Calls to the __CPROVER_pointer_in_range_dfcc Predicate {#contracts-dev-spec-pointer-in-range}
+
+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_in_range_dfcc` with calls to the library implementation.
+
+```c
+__CPROVER_pointer_in_range_dfcc(
+    void *lb,
+    void **ptr,
+    void *ub,
+    __CPROVER_contracts_write_set_ptr_t write_set);
+```
+
+This function implements the `__CPROVER_pointer_in_range_dfcc` 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