Merge pull request #6893 from diffblue/unsigned_pointer_offset

make pointer_offset_exprt unsigned

Author: tautschnig

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;