Fix memOutOfBounds handling of negative pointer offsets

[karoliineh]

This PR fixes a bug in memOutOfBounds where before-start accesses were classified as safe when the offset was negative and precise enough under ana.int.interval, i.e., the bug only manifested when interval domain was turned on. With ana.int.interval, Goblint can compute offsets precisely enough that negative-offset accesses no longer stay at top. This issue was found using the dashboard comparison between Goblint and Mopsa and was exposed by the SV-COMP task list-ext-properties/960521-1_1-1.i.

• Added regressions for negative-offset memOutOfBounds cases in tests/regression/74-invalid_deref.
• Fixed memOutOfBounds to warn when the computed byte offset is negative, in addition to the existing past-the-end check.
• Made the ptr_size_lt_offs comparison sites handle IntDomain.ArithmeticOnIntegerBot consistently by falling back to the existing conservative “could not compare” behavior.
• Refactored the duplicated offset-bound comparison logic into top-level helpers, while preserving the original distinction between:
  • dereference-offset checks using (size - 1) < offset
  • pointer-offset checks using size < offset

[michael-schwarz]

Could you elaborate on why this needs to be handled differently from the things above?

[karoliineh]

First I didn't give it much thought, I just refactored out the parts that were in the original code, but with the help of Codex, I now know the difference and we also added regtests that would catch a change in these in both directions:

This follows directly from the C standard distinction between pointer values and dereferenceable positions. Per C11 §6.5.6, pointer arithmetic may produce a pointer one past the end of an object (this is well-defined), but such a pointer must not be dereferenced. So:

For dereferencing, the valid range is [0, size), hence ID.le ptr_size offs (reject offs == size).
For pointer values, the valid range is [0, size], hence ID.lt ptr_size offs (allow offs == size, reject only offs > size).

and changing either side breaks soundness/precision, I added two regression tests to make this concrete:

74/36: valid one-past pointer (buf + 4) → fails if we switch to le in the pointer case (false positive)
74/37: dereference at end → missed if we switch to lt in the deref case (unsound)

So the difference encodes the standard’s [0, size] vs [0, size) distinction and is intentional.

The unsoundness by changing the deref case to lt is also caught by an existing test 74/13, but the other way around was not detectable by the current tests.

[michael-schwarz]

Thanks for checking!

[sim642]

But this is still strange. The memOutOfBounds analysis should only consider dereferencing. If a pointer points one or more past the end should make no difference if it's never dereferenced. It would only matter for the valid-memtrack subproperty which is handled by memLeak (which has many other problems).

[sim642]

I'll merge this so we can see if it makes any difference in the knightly.
This strangeness already existed before and could be fixed separately.

[michael-schwarz]

Other than the suggestion, LGTM!

[michael-schwarz]

Suggested change

	printf("%p", (void *) end); //NOWARN
	printf("%p", (void *) end); //NOWARN
	printf("%c", *end); //WARN

So we also see that we do indeed warn if this pointer is dereferenced.

[karoliineh]

ha! it seems you just uncovered an unrelated unsoundness with this ;) I suggest we merge this as is and I will add this suggestion on another PR with an appropriate fix.

[michael-schwarz]

Yeah, sounds good!