make pointer_offset_exprt unsigned

regression/cbmc-incr-smt2/pointers-conversions/byte_update.desc

@@ -10,7 +10,7 @@ Assumption:
   file byte_update\.c line \d+ function main
   offset >= 0u && offset < 4u
 State \d+ file byte_update\.c function main line \d+ thread \d+
-  byte_extract_little_endian\(x, \(signed long( long)? int\)offset, uint8_t\)=1 \(00000001\)
+  byte_extract_little_endian\(x, \(.*\)offset, uint8_t\)=1 \(00000001\)
 Violated property:
   file byte_update.c function main line \d+ thread \d+
   assertion x != 256u

regression/cbmc-library/free-01/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --pointer-check --bounds-check --stop-on-fail
-free argument must be (NULL or valid pointer|dynamic object)
+free argument (must be (NULL or valid pointer|dynamic object)|has offset zero)
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-library/strlen-02/test-c-with-string-abstraction.desc

@@ -1,7 +1,7 @@
 CORE
 test.c
 --string-abstraction --show-goto-functions
-ASSIGN strlen#return_value := cast\(cast\(\*strlen::s::s#str\.length, signedbv\[.*\]\) - pointer_offset\(strlen::s\), unsignedbv\[.*\]\)
+ASSIGN strlen#return_value := \*strlen::s::s#str\.length - pointer_offset\(strlen::s\)
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc

@@ -3,11 +3,11 @@ main.c
 --no-simplify --no-propagation
 ^EXIT=10$
 ^SIGNAL=0$
-\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: FAILURE
+\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: SUCCESS
 \[main.assertion.2\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) < 0: FAILURE
 --
 ^warning: ignoring
 --
-Check that both positive and negative offsets can be chosen for uninitialized
-pointers. We use --no-simplify and --no-propagation to ensure that the case is
-not solved by the constant propagation and thus tests the constraint encoding.
+Check that positive offsets can be chosen for uninitialized pointers.  We
+use --no-simplify and --no-propagation to ensure that the case is not solved
+by the constant propagation and thus tests the constraint encoding.

regression/cbmc-primitives/pointer-offset-01/test.desc

@@ -3,15 +3,13 @@ main.c
 
 ^EXIT=10$
 ^SIGNAL=0$
-\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: FAILURE
+\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: SUCCESS
 \[main.assertion.2\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) < 0: FAILURE
 --
 ^warning: ignoring
 --
-For uninitialised pointers, CBMC chooses a nondeterministic value (though no memory
-is allocated). Since the offset of pointers is signed, negative offsets should be
-able to be chosen (along with positive ones) non-deterministically.
-`__CPROVER_POINTER_OFFSET` is the CBMC primitive that gets the pointer offset
-from the base address of the object. This test guards this, and especially
-against the case where we could only observe some cases where offsets were only
-positive (in some CI configurations, for instance).
+For uninitialised pointers, CBMC chooses a nondeterministic value (though no
+memory is allocated).  Since the offset of pointers is unsigned, negative
+offsets cannot be chosen.  `__CPROVER_POINTER_OFFSET` is the CBMC primitive
+that gets the pointer offset from the base address of the object.  This test
+guards this.

regression/cbmc/address_space_size_limit3/test.desc

@@ -1,6 +1,6 @@
 CORE thorough-smt-backend
 main.i
---32 --little-endian --object-bits 25 --pointer-check
+--32 --little-endian --object-bits 26 --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc/memory_allocation2/test.desc

@@ -3,9 +3,9 @@ main.c
 --bounds-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$
-^\[main\.array_bounds\.[67]\] line 38 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$
-^\*\* 1 of 6 failed
+^\[main\.array_bounds\.[1-2]\] .*: SUCCESS$
+^\[main\.array_bounds\.3\] line 38 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$
+^\*\* 1 of 3 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/pointer-offset-01/main.c

@@ -0,0 +1,38 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main(void)
+{
+  size_t size;
+  size_t max_malloc_size = __CPROVER_max_malloc_size;
+  __CPROVER_assume(0 <= size && size <= max_malloc_size);
+  char *lb = malloc(size);
+  size_t offset_lb = __CPROVER_POINTER_OFFSET(lb);
+  size_t object_lb = __CPROVER_POINTER_OBJECT(lb);
+
+  char *ub = lb + size;
+  size_t offset_ub = __CPROVER_POINTER_OFFSET(ub);
+  size_t object_ub = __CPROVER_POINTER_OBJECT(ub);
+
+  char *ubp1 = lb + size + 1;
+  size_t offset_ubp1 = __CPROVER_POINTER_OFFSET(ubp1);
+  size_t object_ubp1 = __CPROVER_POINTER_OBJECT(ubp1);
+
+  assert(object_ub == object_lb);       // proved
+  assert(object_ubp1 == object_lb);     // proved
+  assert(ubp1 > ub);                    // proved
+  assert(offset_ubp1 > offset_ub);      // proved
+  assert(offset_ubp1 == offset_ub + 1); // falsified
+
+  size_t idx;
+  if(idx < size)
+  {
+    char *lb_idx = lb + idx;
+    void *dummy_ub = ub;
+    assert(lb <= lb_idx); // proved
+    assert(lb_idx <= ub); // proved
+  }
+
+  // to produce a trace so that we can observe some intermittent values
+  assert(size < max_malloc_size);
+}

regression/cbmc/pointer-offset-01/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--trace
+^\s*ub.*=\(char \*\)&dynamic_object \+ \d+
+^\s*offset_ubp1=\d+ul* \(00000000 1[0 ]+1\)$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+^\s*ub.*=\(char \*\)&dynamic_object \+ -\d+
+^\s*offset_ubp1=\d+ul* \(11111111 1
+--
+Verifies that all offsets use unsigned arithmetic.

regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/main.c

@@ -7,8 +7,8 @@ __CPROVER_assigns(__CPROVER_object_from(arr))
 // clang-format on
 {
   __CPROVER_assert(arr != NULL, "arr is not NULL");
-  __CPROVER_assert(size < __CPROVER_max_malloc_size, "size is capped");
-  if(size > 0)
+  __CPROVER_assert(size <= __CPROVER_max_malloc_size, "size is capped");
+  if(size > 0 && size <= __CPROVER_max_malloc_size)
   {
     arr[0] = 0;
     arr[size - 1] = 0;

regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc

@@ -2,14 +2,8 @@ CORE
 main.c
 --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
 ^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: FAILURE$
-^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
-^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
 ^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$
-^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: FAILURE$
-^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: FAILURE$
-^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): FAILURE$
-^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): FAILURE$
-^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: FAILURE$
+^\*\* 2 of \d+ failed
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

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

@@ -4,13 +4,13 @@
 void foo(char *arr, size_t size, char *cur)
   // clang-format off
 __CPROVER_requires(0 < 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))
+    __CPROVER_pointer_in_range_dfcc(arr, cur, arr + (size - 1)))
+__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(arr, cur, arr + (size - 1)))
 // clang-format on
 {
   assert(__CPROVER_r_ok(arr, size));
   assert(__CPROVER_same_object(arr, cur));
-  assert(arr <= cur && cur <= arr + size);
+  assert(arr <= cur && cur <= arr + (size - 1));
 }
 
 int main()

regression/contracts/no_redudant_checks/test.desc

@@ -23,7 +23,8 @@ main.c
 ^\[main.pointer_arithmetic.15\].*: SUCCESS
 ^\[main.pointer_arithmetic.16\].*: SUCCESS
 ^\[main.pointer_arithmetic.17\].*: SUCCESS
-^\*\* 0 of 20 failed \(1 iterations\)
+^\[main.pointer_arithmetic.18\].*: SUCCESS
+^\*\* 0 of 21 failed \(1 iterations\)
 ^VERIFICATION SUCCESSFUL$
 --
 ^\[main.overflow.\d+\].*: FAILURE
@@ -35,7 +36,7 @@ Checks that assertions generated by the first --pointer-overflow-check:
 We expect 20 assertions to be generated:
 In the goto-instrument run:
 - 2 for using malloc
-- 17 caused by --pointer-overflow-check
+- 18 caused by --pointer-overflow-check
 
 In the final cbmc run:
 - 0 caused by --pointer-overflow-check

regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \"sources"\: \[ \"main\.c\" \]
-\"main\"\: \[ \"loop 1 invariant i \>\= 80u \|\| \_\_CPROVER\_POINTER\_OFFSET\(array\)
+\"main\"\: \[ \"loop 1 invariant i \>\= 80u \|\|
 --
 This test case checks if synthesized contracts are correctly dumped.

src/ansi-c/cprover_builtin_headers.h

@@ -59,7 +59,7 @@ void __CPROVER_loop_entry(const void *);
 __CPROVER_bool __CPROVER_LIVE_OBJECT(const void *);
 __CPROVER_bool __CPROVER_WRITEABLE_OBJECT(const void *);
 __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
-__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
+__CPROVER_size_t __CPROVER_POINTER_OFFSET(const void *);
 __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
 __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *);
 __CPROVER_bool __CPROVER_pointer_in_range(const void *, const void *, const void *);

src/ansi-c/goto_check_c.cpp

@@ -1571,7 +1571,7 @@ void goto_check_ct::bounds_check_index(
               effective_offset, p_offset.type())};
         }
 
-        exprt zero = from_integer(0, ode.offset().type());
+        exprt zero = from_integer(0, effective_offset.type());
 
         // the final offset must not be negative
         binary_relation_exprt inequality(

src/ansi-c/library/cprover_contracts.c

@@ -114,12 +114,11 @@ __CPROVER_HIDE:;
     ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
     "ptr NULL or writable up to size");
   __CPROVER_assert(
-    size < __CPROVER_max_malloc_size,
+    size <= __CPROVER_max_malloc_size,
     "CAR size is less than __CPROVER_max_malloc_size");
-  __CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(ptr);
+  __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr);
   __CPROVER_assert(
-    !(offset > 0) |
-      ((__CPROVER_size_t)offset + size < __CPROVER_max_malloc_size),
+    !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
     "no offset bits overflow on CAR upper bound computation");
   return (__CPROVER_contracts_car_t){
     .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size};
@@ -163,12 +162,11 @@ __CPROVER_HIDE:;
     ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
     "ptr NULL or writable up to size");
   __CPROVER_assert(
-    size < __CPROVER_max_malloc_size,
+    size <= __CPROVER_max_malloc_size,
     "CAR size is less than __CPROVER_max_malloc_size");
-  __CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(ptr);
+  __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr);
   __CPROVER_assert(
-    !(offset > 0) |
-      ((__CPROVER_size_t)offset + size < __CPROVER_max_malloc_size),
+    !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
     "no offset bits overflow on CAR upper bound computation");
   __CPROVER_contracts_car_t *elem = set->elems + idx;
   *elem = (__CPROVER_contracts_car_t){
@@ -783,14 +781,13 @@ __CPROVER_HIDE:;
 
   // Compute the upper bound, perform inclusion check against contract-assigns
   __CPROVER_assert(
-    size < __CPROVER_max_malloc_size,
+    size <= __CPROVER_max_malloc_size,
     "CAR size is less than __CPROVER_max_malloc_size");
 
-  __CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(ptr);
+  __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr);
 
   __CPROVER_assert(
-    !(offset > 0) |
-      ((__CPROVER_size_t)offset + size < __CPROVER_max_malloc_size),
+    !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
     "no offset bits overflow on CAR upper bound computation");
   void *ub = (void *)((char *)ptr + size);
   __CPROVER_contracts_car_t *elem = set->contract_assigns.elems;
@@ -1198,7 +1195,7 @@ __CPROVER_HIDE:;
     {
       // When --malloc-may-fail --malloc-fail-null
       // add implicit assumption that the size is capped
-      __CPROVER_assume(size < __CPROVER_max_malloc_size);
+      __CPROVER_assume(size <= __CPROVER_max_malloc_size);
     }
     else if(
       __CPROVER_malloc_failure_mode ==
@@ -1208,9 +1205,9 @@ __CPROVER_HIDE:;
       // check if max allocation size is exceeded and
       // add implicit assumption that the size is capped
       __CPROVER_assert(
-        size < __CPROVER_max_malloc_size,
+        size <= __CPROVER_max_malloc_size,
         "__CPROVER_is_fresh max allocation size exceeded");
-      __CPROVER_assume(size < __CPROVER_max_malloc_size);
+      __CPROVER_assume(size <= __CPROVER_max_malloc_size);
     }
 
     void *ptr = __CPROVER_allocate(size, 0);
@@ -1255,16 +1252,16 @@ __CPROVER_HIDE:;
       __CPROVER_malloc_failure_mode ==
       __CPROVER_malloc_failure_mode_return_null)
     {
-      __CPROVER_assume(size < __CPROVER_max_malloc_size);
+      __CPROVER_assume(size <= __CPROVER_max_malloc_size);
     }
     else if(
       __CPROVER_malloc_failure_mode ==
       __CPROVER_malloc_failure_mode_assert_then_assume)
     {
       __CPROVER_assert(
-        size < __CPROVER_max_malloc_size,
-        "__CPROVER_is_fresh requires size < __CPROVER_max_malloc_size");
-      __CPROVER_assume(size < __CPROVER_max_malloc_size);
+        size <= __CPROVER_max_malloc_size,
+        "__CPROVER_is_fresh requires size <= __CPROVER_max_malloc_size");
+      __CPROVER_assume(size <= __CPROVER_max_malloc_size);
     }
 
     void *ptr = __CPROVER_allocate(size, 0);
@@ -1360,8 +1357,8 @@ __CPROVER_HIDE:;
   __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_size_t lb_offset = __CPROVER_POINTER_OFFSET(lb);
+  __CPROVER_size_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)
@@ -1373,14 +1370,14 @@ __CPROVER_HIDE:;
     __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_size_t max_offset = 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);
+    __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(*ptr);
     return __CPROVER_same_object(lb, *ptr) && lb_offset <= offset &&
            offset <= ub_offset;
   }

src/cprover/bv_pointers_wide.cpp

@@ -769,7 +769,7 @@ exprt bv_pointers_widet::bv_get_rec(
 
   pointer_logict::pointert pointer{
     numeric_cast_v<std::size_t>(binary2integer(value_addr, false)),
-    binary2integer(value_offset, true)};
+    binary2integer(value_offset, false)};
 
   return annotated_pointer_constant_exprt{
     bvrep, pointer_logic.pointer_expr(pointer, pt)};

src/pointer-analysis/value_set_dereference.cpp

@@ -517,7 +517,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 
       const index_exprt index_expr(
         symbol_expr,
-        pointer_offset(pointer_expr),
+        typecast_exprt::conditional_cast(
+          pointer_offset(pointer_expr),
+          to_array_type(memory_symbol.type).index_type()),
         to_array_type(memory_symbol.type).element_type());
 
       valuet result;
@@ -532,7 +534,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     {
       const index_exprt index_expr(
         symbol_expr,
-        pointer_offset(pointer_expr),
+        typecast_exprt::conditional_cast(
+          pointer_offset(pointer_expr),
+          to_array_type(memory_symbol.type).index_type()),
         to_array_type(memory_symbol.type).element_type());
 
       valuet result;
@@ -768,7 +772,11 @@ bool value_set_dereferencet::memory_model_bytes(
   {
     // yes, can use 'index', but possibly need to convert
     result = typecast_exprt::conditional_cast(
-      index_exprt(value, offset, to_array_type(from_type).element_type()),
+      index_exprt(
+        value,
+        typecast_exprt::conditional_cast(
+          offset, to_array_type(from_type).index_type()),
+        to_array_type(from_type).element_type()),
       to_type);
   }
   else