Do not check array bounds when invalidating or collecting reachable addresses

[jerhard]

[Opus 5.5]:

Goblint produces spurious "May access array out of bounds" warnings when a value containing an array is invalidated or traversed for reachable addresses. For example, this happens when an unknown function, or a library function with a deep write, gets a pointer to a struct with an array member. These warnings also set the InvalidDeref flag, so valid-deref/valid-memsafety cannot be proven.

struct s { int a[2]; int *p; };
extern void unknown(struct s *x);

struct s x = {{0, 0}, &y};
unknown(&x); // master: "May access array out of bounds"

This was because ValueDomain.invalidate_value and base's reachable_from_value read the array contents at an unknown index via CArrays.get, which runs the out-of-bounds check by default. These reads are internal to the analysis and not accesses by the program.

We fix this by passing ~checkBounds:false to these reads, as the conversions between array domains in ArrayDomain already do. Real array accesses by the program are still checked.

Tests

New regression test 26-undefined_behavior/16-invalidate-array-no-oob.c. On master it fails with the spurious warning at the call. An actual out-of-bounds write afterwards is still reported.

Context

This is needed for an upcoming PR that tracks stdin/stdout/stderr as pointers to actual FILE objects. Libc's FILE contains arrays, so calls like fgets(buf, n, stdin), which deep-write the stream, would otherwise trigger this warning.

🤖 Generated with Claude Code

[sim642]

This gave me deja vu because #2022 put the whole reachability calculation under speculation, which should suppress these checks/warnings.
I wonder why that wasn't enough. Is it actually just the invalidation aspect where we should assume unknown functions don't access OOB?

[michael-schwarz]

This one should be unnecessary, this function is only called from the reachable_from_value below.

[sim642]

It also wouldn't hurt to be more explicit about it, rather than relying so heavily on global speculation state. But either way is fine by me.

[michael-schwarz]

Probably the check should be in invalidate setting the speculative flag. But the problem is that invalidate is also used for lvals in a bunch of transfer functions, and there we need to check.

[sim642]

But the problem is that invalidate is also used for lvals in a bunch of transfer functions, and there we need to check.

Perhaps we shouldn't abuse invalidate for just setting things to top and only use it for the invalidations via unknown function arguments.
Because if we have the assumption that unknown functions don't do OOB accesses, then that assumption shouldn't apply to lvalues explicitly assigned by special function calls (where we're using invalidate to top-ify the left-hand side), because writing to that explicit lvalue can be OOB, etc.