`offset` intrinsic doesn't check that pointers stay within bounds

[adpaco-aws]

The documentation for the offset method mentions in the safety conditions that:

Both the starting and resulting pointer must be either in bounds or one byte past the end of the same allocated object.

At present, the standard library prevents us from adding this check because otherwise we run into spurious failures (i.e., offsets that go out-of-bounds, are frequently used).

[adpaco-aws]

Removing the soundness label since this is not strictly a soundness issue.

Adding this check would introduce many failures that aren't part of the user code, because offset operations often go out-of-bounds (in the standard library and other projects), but that's not an issue unless the pointer gets used. Let me illustrate with an example in C:

int *p = malloc(10);
p = p + 50; // pointer has been offset 50 units (out of bounds) - not an error since the pointer is not used
int x = *p // this is an error, the index points to somewhere out of the bounds for the object

Rust allows manipulations as in line (2), so there's no soundness concerns about that. On the other hand, de-referencing the pointer in line (3) should raise an error, which Kani does.

[giltho]

i.e., offsets that go out-of-bounds, are frequently used

Do you have an example of that? The stdlib is tested with MIRI I believe, and MIRI detects creating OOB pointers as UB.

de-referencing the pointer in line (3) should raise an error, which Kani does

Not always, see #1665