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/string-abstraction/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/Pointer_Arithmetic19/test.desc

@@ -1,7 +1,7 @@
 CORE new-smt-backend
 main.c
 --program-only
-ASSERT\(\{ 42, 43 \}\[POINTER_OFFSET\(p!0@1#2\) / \d+l*\] == 43\)$
+ASSERT\(\{ 42, 43 \}\[\(signed (long )?int\)POINTER_OFFSET\(p!0@1#2\) / \d+l*\] == 43\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

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

@@ -56,7 +56,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

@@ -1574,7 +1574,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

@@ -503,29 +503,30 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 
     const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");
     const symbol_exprt symbol_expr(memory_symbol.name, memory_symbol.type);
+    const auto &memory_array_type = to_array_type(memory_symbol.type);
 
-    if(to_array_type(memory_symbol.type).element_type() == dereference_type)
+    if(memory_array_type.element_type() == dereference_type)
     {
       // Types match already, what a coincidence!
       // We can use an index expression.
 
       const index_exprt index_expr(
         symbol_expr,
-        pointer_offset(pointer_expr),
-        to_array_type(memory_symbol.type).element_type());
+        typecast_exprt::conditional_cast(
+          pointer_offset(pointer_expr), memory_array_type.index_type()),
+        memory_array_type.element_type());
 
       result.value=index_expr;
       result.pointer = address_of_exprt{index_expr};
     }
     else if(dereference_type_compare(
-              to_array_type(memory_symbol.type).element_type(),
-              dereference_type,
-              ns))
+              memory_array_type.element_type(), dereference_type, ns))
     {
       const index_exprt index_expr(
         symbol_expr,
-        pointer_offset(pointer_expr),
-        to_array_type(memory_symbol.type).element_type());
+        typecast_exprt::conditional_cast(
+          pointer_offset(pointer_expr), memory_array_type.index_type()),
+        memory_array_type.element_type());
       result.value=typecast_exprt(index_expr, dereference_type);
       result.pointer =
         typecast_exprt{address_of_exprt{index_expr}, pointer_type};
@@ -585,6 +586,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       pointer_offset_bits(to_array_type(root_object_type).element_type(), ns) ==
         pointer_offset_bits(dereference_type, ns))
     {
+      const auto &array_type = to_array_type(root_object_type);
+
       // We have an array with a subtype that matches
       // the dereferencing type.
       exprt offset;
@@ -593,11 +596,13 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       if(o.offset().is_constant())
         offset=o.offset();
       else
-        offset=pointer_offset(pointer_expr);
+      {
+        offset = typecast_exprt::conditional_cast(
+          pointer_offset(pointer_expr), array_type.index_type());
+      }
 
       // are we doing a byte?
-      auto element_size =
-        pointer_offset_size(to_array_type(root_object_type).element_type(), ns);
+      auto element_size = pointer_offset_size(array_type.element_type(), ns);
 
       if(!element_size.has_value() || *element_size == 0)
       {
@@ -644,7 +649,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       // this is relative to the root object
       exprt offset;
       if(o.offset().id()==ID_unknown)
+      {
         offset=pointer_offset(pointer_expr);
+      }
       else
         offset=o.offset();
 
@@ -765,8 +772,12 @@ bool value_set_dereferencet::memory_model_bytes(
     is_a_bv_type(to_type))
   {
     // yes, can use 'index', but possibly need to convert
+    const auto &from_array_type = to_array_type(from_type);
     result = typecast_exprt::conditional_cast(
-      index_exprt(value, offset, to_array_type(from_type).element_type()),
+      index_exprt(
+        value,
+        typecast_exprt::conditional_cast(offset, from_array_type.index_type()),
+        from_array_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));
     }
   }