make pointer_offset_exprt unsigned

This commit changes the type of __CPROVER_POINTER_OFFSET from ssize_t to
size_t.  To match, relational operators on pointers are now unsigned, to
enable p+PTRDIFF_MAX+1 > p.

The rationale is subtle.  The ISO C 11 standard 6.5.8 par 5 suggests that a
pair of pointers can be compared if either the pointers point into the
object, or one beyond the end of the sequence.  The behavior in the case of
a pointer that points before the sequence is undefined.  There is a similar
narrative for pointer arithmetic.  A pointer with an offset that has a set
most significant bit should thus compare "less than" a pointer with an
offset that has a zero MSB.  This suggests an unsigned encoding.

Author: kroening

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/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/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

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/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

src/solvers/flattening/bv_pointers.cpp

@@ -194,13 +194,14 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
       if(same_object_lit.is_false())
         return same_object_lit;
 
+      // The comparison is UNSIGNED, to match the type of pointer_offsett
       return prop.land(
         same_object_lit,
         bv_utils.rel(
           offset_bv0,
           expr.id(),
           offset_bv1,
-          bv_utilst::representationt::SIGNED));
+          bv_utilst::representationt::UNSIGNED));
     }
   }
 

src/util/pointer_predicates.cpp

@@ -37,7 +37,7 @@ exprt object_size(const exprt &pointer)
 
 exprt pointer_offset(const exprt &pointer)
 {
-  return pointer_offset_exprt(pointer, signed_size_type());
+  return pointer_offset_exprt(pointer, size_type());
 }
 
 exprt deallocated(const exprt &pointer, const namespacet &ns)
@@ -73,30 +73,45 @@ exprt object_upper_bound(
   const exprt &pointer,
   const exprt &access_size)
 {
-  // this is
-  // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer)
+  exprt object_offset = pointer_offset(pointer);
 
   exprt object_size_expr=object_size(pointer);
 
-  exprt object_offset=pointer_offset(pointer);
-
-  // need to add size
-  irep_idt op=ID_ge;
-  exprt sum=object_offset;
+  std::size_t max_width = std::max(
+    to_bitvector_type(object_offset.type()).get_width(),
+    to_bitvector_type(object_size_expr.type()).get_width());
 
+  // We add the size to the offset, if given.
   if(access_size.is_not_nil())
   {
-    op=ID_gt;
+    // This is
+    // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer)
+    // We enlarge all bit-vectors to avoid an overflow on the addition.
+
+    max_width =
+      std::max(max_width, to_bitvector_type(access_size.type()).get_width());
+
+    auto type = unsignedbv_typet(max_width + 1);
+
+    auto sum = plus_exprt(
+      typecast_exprt::conditional_cast(object_offset, type),
+      typecast_exprt::conditional_cast(access_size, type));
 
-    sum = plus_exprt(
-      typecast_exprt::conditional_cast(object_offset, access_size.type()),
-      access_size);
+    return binary_relation_exprt(
+      sum, ID_gt, typecast_exprt::conditional_cast(object_size_expr, type));
   }
+  else
+  {
+    // This is
+    // POINTER_OFFSET(p)>=OBJECT_SIZE(pointer)
+
+    auto type = unsignedbv_typet(max_width);
 
-  return binary_relation_exprt(
-    typecast_exprt::conditional_cast(sum, object_size_expr.type()),
-    op,
-    object_size_expr);
+    return binary_relation_exprt(
+      typecast_exprt::conditional_cast(object_offset, type),
+      ID_ge,
+      typecast_exprt::conditional_cast(object_size_expr, type));
+  }
 }
 
 exprt object_lower_bound(

unit/util/pointer_expr.cpp

@@ -10,14 +10,14 @@
 TEST_CASE("pointer_offset_exprt", "[core][util]")
 {
   const exprt pointer = symbol_exprt{"foo", pointer_type(void_type())};
-  const pointer_offset_exprt pointer_offset{pointer, signed_size_type()};
+  const pointer_offset_exprt pointer_offset{pointer, size_type()};
   SECTION("Is equivalent to free function.")
   {
     CHECK(::pointer_offset(pointer) == pointer_offset);
   }
   SECTION("Result type")
   {
-    CHECK(pointer_offset.type() == signed_size_type());
+    CHECK(pointer_offset.type() == size_type());
   }
   SECTION("Pointer operand accessor")
   {