make pointer_offset_exprt unsigned

[kroening]

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.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[tautschnig]

I'm unconvinced the required change is as small as the current PR suggests: there are several uses of bv_utils.sign_extension in bv_pointers.cpp, and I believe these need to be changed.

[codecov]

Codecov Report

Base: 78.48% // Head: 78.48% // Decreases project coverage by -0.01% ⚠️

Coverage data is based on head (7cb83c1) compared to base (fb65095).
Patch coverage: 93.18% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #6893      +/-   ##
===========================================
- Coverage    78.48%   78.48%   -0.01%     
===========================================
  Files         1663     1663              
  Lines       191189   191232      +43     
===========================================
+ Hits        150055   150082      +27     
- Misses       41134    41150      +16     

Impacted Files	Coverage Δ
src/util/pointer_predicates.cpp	87.23% <76.47%> (-7.89%)	⬇️
src/util/lower_byte_operators.cpp	92.85% <95.91%> (+0.08%)	⬆️
src/ansi-c/goto_check_c.cpp	91.60% <100.00%> (ø)
src/cprover/bv_pointers_wide.cpp	58.28% <100.00%> (ø)
src/pointer-analysis/value_set_dereference.cpp	99.38% <100.00%> (+0.01%)	⬆️
src/solvers/flattening/bv_pointers.cpp	86.28% <100.00%> (ø)
src/util/replace_expr.cpp	100.00% <100.00%> (ø)
unit/util/pointer_expr.cpp	100.00% <100.00%> (ø)
src/solvers/smt2/smt2_format.cpp	85.39% <0.00%> (-1.13%)	⬇️
src/goto-programs/string_abstraction.cpp	90.93% <0.00%> (-0.78%)	⬇️
... and 2 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

[tautschnig]

I'm unconvinced the required change is as small as the current PR suggests: there are several uses of bv_utils.sign_extension in bv_pointers.cpp, and I believe these need to be changed.

Slightly amending my concern as discussed out of band: we likely make a mess at the moment when converting the result of pointer (offset) arithmetic back to the bit-limited offset representation where we may or may not end up producing a negative number in case of overflow/underflow. This needs looking into, or perhaps we should just invest our energy in the alternative pointer encodings.

[tautschnig]

I believe the only missing piece for this one is adjusting pointer_offset in pointer_predicates.cpp.

[tautschnig]

I believe the only missing piece for this one is adjusting pointer_offset in pointer_predicates.cpp.

We now have a bunch of failing regression tests with warning: ignoring >= as that comparison now mixes signed/unsigned types. Looks like we are hardcoding the signed offset in a bunch of places?

[tautschnig]

Adding a temporary blocker: I am now expecting all tests to pass, but @remi-delmas-3000 is taking a look at all pointer arithmetic done contracts code to make sure no further updates are required.

[remi-delmas-3000]

I wrote a test to check that I can perform inclusion checks using pointers that are one past the end of the object, it seems to work except for one thing I don’t understand:

#include <stdio.h>
#include <assert.h>
#include <stdbool.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);

    void *ub = lb + size;
    size_t offset_ub = __CPROVER_POINTER_OFFSET(ub);
    size_t object_ub = __CPROVER_POINTER_OBJECT(ub);

    void *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) {
      void *lb_idx = lb + idx;
      void *dummy_ub = ub;
      assert(lb <= lb_idx); // proved
      assert(lb_idx <= ub); // proved
    }
}

the third assertion is falsified with

max_malloc_size=36028797018963968ul (00000000 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
size=36028797018963967ul (00000000 01111111 11111111 11111111 11111111 11111111 11111111 11111111)
ub=(const void *)((char *)&dynamic_object + 36028797018963967l) (00000010 01111111 11111111 11111111 11111111 11111111 11111111 11111111)
offset_ub=36028797018963967ul (00000000 01111111 11111111 11111111 11111111 11111111 11111111 11111111)
ubp1=(const void *)((char *)&dynamic_object + -36028797018963968l) (00000010 10000000 00000000 00000000 00000000 00000000 00000000 00000000)
offset_ubp1=18410715276690587648ul (11111111 10000000 00000000 00000000 00000000 00000000 00000000 00000000)

In the trace size is taken to be max_malloc_size-1 so that the offset of ubp1 = lb + size + 1 lands exactly at max_malloc_size in the pointer representation but becomes something else when extracted using __CPROVER_POINTER_OFFSET, with leading ones added offset_ubp1. The trace prints the offset as a negative number when printing the pointer.

The counter example goes away if we restrict the allocation size to be strictly less than __CPROVER_max_malloc_size
So it seems like offsets strictly below max_malloc_size get translated without leading ones, offsets greater or equal to max_malloc_size get leading ones. Seems like a remnant of signed conversion for overflowing pointers.

I wasn't expecting unsigned offsets to use the full width, rather N-object-bits at most.

max_malloc_size is still defined as 2^(offset_bits-1) so technically we could still add (max_malloc_size-1) to max_malloc_size before having to overflow into object bits in the pointer representation.

[tautschnig]

I have now included the test posted by @remi-delmas-3000 together with further fixes (ensuring that we always interpret the offset as unsigned).