Skip to content

Fix memOutOfBounds handling of negative pointer offsets #2017

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sim642 merged 7 commits into from
May 7, 2026
Merged

Fix memOutOfBounds handling of negative pointer offsets #2017

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
321fe15
Add regressions for negative-offset memOutOfBounds checks
karoliineh May 5, 2026
f57838e
memOutOfBounds: warn on before-start pointer offsets
karoliineh May 5, 2026
8ad5fb3
Catch IntDomain.ArithmeticOnIntegerBot symmetrically for all ptr_size…
karoliineh May 5, 2026
5447075
Refactor: deduplicate offset bound functions
karoliineh May 5, 2026
8400643
Replace roundabout less-equal computation with less-equal call
karoliineh May 7, 2026
08f01ee
Refactor ptr_size_lt_offs to ptr_size_le_offs to avoid confusion
karoliineh May 7, 2026
9c3cf67
Add regtests to distinguish between ptr value and deref bounds
karoliineh May 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
57 changes: 36 additions & 21 deletions src/analyses/memOutOfBounds.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,27 @@ struct
let size_of_type_in_bytes typ =
intdom_of_int (Cilfacade.bytesSizeOf typ)

let offs_lt_zero offs =
try ID.lt offs (intdom_of_int 0)
with IntDomain.ArithmeticOnIntegerBot _ -> None

let check_deref_offset_bounds ptr_size offs =
let ptr_size_lt_offs =
try
let one = intdom_of_int 1 in
let max_valid_offs = ID.sub ptr_size one in
ID.lt max_valid_offs offs
Comment thread
karoliineh marked this conversation as resolved.
Outdated
with IntDomain.ArithmeticOnIntegerBot _ -> None
in
offs_lt_zero offs, ptr_size_lt_offs

let check_ptr_offset_bounds ptr_size offs =
let ptr_size_lt_offs =
try ID.lt ptr_size offs
with IntDomain.ArithmeticOnIntegerBot _ -> None
in
offs_lt_zero offs, ptr_size_lt_offs
Comment on lines +48 to +53
Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz May 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Copy Markdown
Member Author

@karoliineh karoliineh May 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz May 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for checking!

Copy link
Copy Markdown
Member

@sim642 sim642 May 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Copy link
Copy Markdown
Member

@sim642 sim642 May 7, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


let rec exp_contains_a_ptr (exp:exp) =
match exp with
| Const _
Expand Down Expand Up @@ -290,23 +311,17 @@ struct
| `Lifted es ->
let casted_es = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) es in (* TODO: proper castkind *)
let casted_offs = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) offs_intdom in (* TODO: proper castkind *)
let ptr_size_lt_offs =
let one = intdom_of_int 1 in
let casted_es = ID.sub casted_es one in
begin try ID.lt casted_es casted_offs
with IntDomain.ArithmeticOnIntegerBot _ -> None
end
in
let behavior = Undefined MemoryOutOfBoundsAccess in
let cwe_number = 823 in
begin match ptr_size_lt_offs with
| Some true ->
begin match check_deref_offset_bounds casted_es casted_offs with
| Some true, _
| _, Some true ->
(set_mem_safety_flag InvalidDeref;
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of lval dereference expression is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" ID.pretty casted_es ID.pretty casted_offs);
Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" ID.pretty casted_es ID.pretty casted_offs
| Some false ->
| Some false, Some false ->
Checks.safe Checks.Category.InvalidMemoryAccess
| None ->
| _ ->
(set_mem_safety_flag InvalidDeref;
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of lval dereference expression (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_es ID.pretty casted_offs);
Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare size of lval dereference expression (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_es ID.pretty casted_offs
Expand Down Expand Up @@ -343,15 +358,15 @@ struct
| `Lifted ps, ao ->
let casted_ps = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *)
let casted_ao = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ao in (* TODO: proper castkind *)
let ptr_size_lt_offs = ID.lt casted_ps casted_ao in
begin match ptr_size_lt_offs with
| Some true ->
begin match check_ptr_offset_bounds casted_ps casted_ao with
| Some true, _
| _, Some true ->
set_mem_safety_flag InvalidDeref;
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" ID.pretty casted_ps ID.pretty casted_ao;
Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" ID.pretty casted_ps ID.pretty casted_ao
| Some false ->
| Some false, Some false ->
Checks.safe Checks.Category.InvalidMemoryAccess
| None ->
| _ ->
set_mem_safety_flag InvalidDeref;
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of pointer (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_ps ID.pretty casted_ao;
Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare size of pointer (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_ps ID.pretty casted_ao
Expand Down Expand Up @@ -431,15 +446,15 @@ struct
| `Lifted ps, `Lifted o ->
let casted_ps = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *)
let casted_o = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) o in (* TODO: proper castkind *)
let ptr_size_lt_offs = ID.lt casted_ps casted_o in
begin match ptr_size_lt_offs with
| Some true ->
begin match check_ptr_offset_bounds casted_ps casted_o with
| Some true, _
| _, Some true ->
set_mem_safety_flag InvalidDeref;
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o;
Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o
| Some false ->
| Some false, Some false ->
Checks.safe Checks.Category.InvalidMemoryAccess
| None ->
| _ ->
set_mem_safety_flag InvalidDeref;
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o;
Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o
Expand Down
14 changes: 14 additions & 0 deletions tests/regression/74-invalid_deref/34-negative-index-after-ptr-increment.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
#include <stdlib.h>

int main() {
int *b = malloc(2 * sizeof(int));
int x;

*b++ = 0; //NOWARN

x = *(b - 2); //WARN

free(b - 1);
return x;
}
14 changes: 14 additions & 0 deletions tests/regression/74-invalid_deref/35-negative-index-after-ptr-increment-index-syntax.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval
#include <stdlib.h>

int main() {
int *b = malloc(2 * sizeof(int));

*b++ = 0; //NOWARN

if (b[-2]) //WARN
return 1;

free(b - 1);
return 0;
}
Loading