From 321fe158c6159bf3e9c29d0366799aa73b49c3d3 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Tue, 5 May 2026 15:16:22 +0300 Subject: [PATCH 1/7] Add regressions for negative-offset memOutOfBounds checks --- .../34-negative-index-after-ptr-increment.c | 14 ++++++++++++++ ...gative-index-after-ptr-increment-index-syntax.c | 14 ++++++++++++++ 2 files changed, 28 insertions(+) create mode 100644 tests/regression/74-invalid_deref/34-negative-index-after-ptr-increment.c create mode 100644 tests/regression/74-invalid_deref/35-negative-index-after-ptr-increment-index-syntax.c diff --git a/tests/regression/74-invalid_deref/34-negative-index-after-ptr-increment.c b/tests/regression/74-invalid_deref/34-negative-index-after-ptr-increment.c new file mode 100644 index 0000000000..12eb084dfc --- /dev/null +++ b/tests/regression/74-invalid_deref/34-negative-index-after-ptr-increment.c @@ -0,0 +1,14 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include + +int main() { + int *b = malloc(2 * sizeof(int)); + int x; + + *b++ = 0; //NOWARN + + x = *(b - 2); //WARN + + free(b - 1); + return x; +} diff --git a/tests/regression/74-invalid_deref/35-negative-index-after-ptr-increment-index-syntax.c b/tests/regression/74-invalid_deref/35-negative-index-after-ptr-increment-index-syntax.c new file mode 100644 index 0000000000..ad4dd65b03 --- /dev/null +++ b/tests/regression/74-invalid_deref/35-negative-index-after-ptr-increment-index-syntax.c @@ -0,0 +1,14 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include + +int main() { + int *b = malloc(2 * sizeof(int)); + + *b++ = 0; //NOWARN + + if (b[-2]) //WARN + return 1; + + free(b - 1); + return 0; +} From f57838ef7beab0ee3fa80ad40267383f6e2b6327 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Tue, 5 May 2026 15:16:49 +0300 Subject: [PATCH 2/7] memOutOfBounds: warn on before-start pointer offsets --- src/analyses/memOutOfBounds.ml | 40 ++++++++++++++++++++++++---------- 1 file changed, 28 insertions(+), 12 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 8d5ea86299..fd929ca850 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -297,16 +297,22 @@ struct with IntDomain.ArithmeticOnIntegerBot _ -> None end in + let offs_lt_zero = + let zero = intdom_of_int 0 in + try ID.lt casted_offs zero + with IntDomain.ArithmeticOnIntegerBot _ -> None + in let behavior = Undefined MemoryOutOfBoundsAccess in let cwe_number = 823 in - begin match ptr_size_lt_offs with - | Some true -> + begin match offs_lt_zero, ptr_size_lt_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 @@ -343,15 +349,20 @@ 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 offs_lt_zero = + try ID.lt casted_ao (intdom_of_int 0) + with IntDomain.ArithmeticOnIntegerBot _ -> None + in let ptr_size_lt_offs = ID.lt casted_ps casted_ao in - begin match ptr_size_lt_offs with - | Some true -> + begin match offs_lt_zero, ptr_size_lt_offs 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 @@ -431,15 +442,20 @@ 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 offs_lt_zero = + try ID.lt casted_o (intdom_of_int 0) + with IntDomain.ArithmeticOnIntegerBot _ -> None + in let ptr_size_lt_offs = ID.lt casted_ps casted_o in - begin match ptr_size_lt_offs with - | Some true -> + begin match offs_lt_zero, ptr_size_lt_offs 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 From 8ad5fb3edf3c22a8fbc720fd7a6aae9e101764f7 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Tue, 5 May 2026 15:21:34 +0300 Subject: [PATCH 3/7] Catch IntDomain.ArithmeticOnIntegerBot symmetrically for all ptr_size_lt_offs sites --- src/analyses/memOutOfBounds.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index fd929ca850..cae39fc44d 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -353,7 +353,10 @@ struct try ID.lt casted_ao (intdom_of_int 0) with IntDomain.ArithmeticOnIntegerBot _ -> None in - let ptr_size_lt_offs = ID.lt casted_ps casted_ao in + let ptr_size_lt_offs = + try ID.lt casted_ps casted_ao + with IntDomain.ArithmeticOnIntegerBot _ -> None + in begin match offs_lt_zero, ptr_size_lt_offs with | Some true, _ | _, Some true -> @@ -446,7 +449,10 @@ struct try ID.lt casted_o (intdom_of_int 0) with IntDomain.ArithmeticOnIntegerBot _ -> None in - let ptr_size_lt_offs = ID.lt casted_ps casted_o in + let ptr_size_lt_offs = + try ID.lt casted_ps casted_o + with IntDomain.ArithmeticOnIntegerBot _ -> None + in begin match offs_lt_zero, ptr_size_lt_offs with | Some true, _ | _, Some true -> From 5447075fe2ea23c505c82bfae5dd408868da582a Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Tue, 5 May 2026 15:31:37 +0300 Subject: [PATCH 4/7] Refactor: deduplicate offset bound functions --- src/analyses/memOutOfBounds.ml | 55 +++++++++++++++------------------- 1 file changed, 24 insertions(+), 31 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index cae39fc44d..1b9911ae62 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -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 + 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 + let rec exp_contains_a_ptr (exp:exp) = match exp with | Const _ @@ -290,21 +311,9 @@ 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 offs_lt_zero = - let zero = intdom_of_int 0 in - try ID.lt casted_offs zero - with IntDomain.ArithmeticOnIntegerBot _ -> None - in let behavior = Undefined MemoryOutOfBoundsAccess in let cwe_number = 823 in - begin match offs_lt_zero, ptr_size_lt_offs with + begin match check_deref_offset_bounds casted_es casted_offs with | Some true, _ | _, Some true -> (set_mem_safety_flag InvalidDeref; @@ -349,15 +358,7 @@ 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 offs_lt_zero = - try ID.lt casted_ao (intdom_of_int 0) - with IntDomain.ArithmeticOnIntegerBot _ -> None - in - let ptr_size_lt_offs = - try ID.lt casted_ps casted_ao - with IntDomain.ArithmeticOnIntegerBot _ -> None - in - begin match offs_lt_zero, ptr_size_lt_offs with + begin match check_ptr_offset_bounds casted_ps casted_ao with | Some true, _ | _, Some true -> set_mem_safety_flag InvalidDeref; @@ -445,15 +446,7 @@ 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 offs_lt_zero = - try ID.lt casted_o (intdom_of_int 0) - with IntDomain.ArithmeticOnIntegerBot _ -> None - in - let ptr_size_lt_offs = - try ID.lt casted_ps casted_o - with IntDomain.ArithmeticOnIntegerBot _ -> None - in - begin match offs_lt_zero, ptr_size_lt_offs with + begin match check_ptr_offset_bounds casted_ps casted_o with | Some true, _ | _, Some true -> set_mem_safety_flag InvalidDeref; From 84006439cbaf87797738559cd5f691a2df176493 Mon Sep 17 00:00:00 2001 From: Karoliine Holter <44437975+karoliineh@users.noreply.github.com> Date: Thu, 7 May 2026 12:24:34 +0300 Subject: [PATCH 5/7] Replace roundabout less-equal computation with less-equal call Co-authored-by: Simmo Saan --- src/analyses/memOutOfBounds.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 1b9911ae62..66ffee906f 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -41,9 +41,7 @@ struct 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 + ID.le ptr_size offs with IntDomain.ArithmeticOnIntegerBot _ -> None in offs_lt_zero offs, ptr_size_lt_offs From 08f01ee55456dd5b49ed290d2c4ea1c1ae245ac5 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 7 May 2026 12:25:38 +0300 Subject: [PATCH 6/7] Refactor ptr_size_lt_offs to ptr_size_le_offs to avoid confusion --- src/analyses/memOutOfBounds.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 66ffee906f..4546fda32e 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -39,12 +39,11 @@ struct with IntDomain.ArithmeticOnIntegerBot _ -> None let check_deref_offset_bounds ptr_size offs = - let ptr_size_lt_offs = - try - ID.le ptr_size offs + let ptr_size_le_offs = + try ID.le ptr_size offs with IntDomain.ArithmeticOnIntegerBot _ -> None in - offs_lt_zero offs, ptr_size_lt_offs + offs_lt_zero offs, ptr_size_le_offs let check_ptr_offset_bounds ptr_size offs = let ptr_size_lt_offs = From 9c3cf67842744ac0c42b937bf59696a184074e32 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 7 May 2026 13:02:39 +0300 Subject: [PATCH 7/7] Add regtests to distinguish between ptr value and deref bounds --- .../74-invalid_deref/36-one-past-pointer.c | 12 ++++++++++++ .../74-invalid_deref/37-one-past-deref-offset.c | 16 ++++++++++++++++ 2 files changed, 28 insertions(+) create mode 100644 tests/regression/74-invalid_deref/36-one-past-pointer.c create mode 100644 tests/regression/74-invalid_deref/37-one-past-deref-offset.c diff --git a/tests/regression/74-invalid_deref/36-one-past-pointer.c b/tests/regression/74-invalid_deref/36-one-past-pointer.c new file mode 100644 index 0000000000..b4ceb506d7 --- /dev/null +++ b/tests/regression/74-invalid_deref/36-one-past-pointer.c @@ -0,0 +1,12 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include +#include + +int main(void) { + char *buf = malloc(4); + char *end; + end = buf + 4; //NOWARN + printf("%p", (void *) end); //NOWARN + free(buf); + return 0; +} diff --git a/tests/regression/74-invalid_deref/37-one-past-deref-offset.c b/tests/regression/74-invalid_deref/37-one-past-deref-offset.c new file mode 100644 index 0000000000..8c441d4793 --- /dev/null +++ b/tests/regression/74-invalid_deref/37-one-past-deref-offset.c @@ -0,0 +1,16 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include + +struct S { + unsigned char a; + unsigned char b:2; + unsigned char c:2; + unsigned char d; +} __attribute__((packed)); + +int main(void) { + struct S *p = malloc(2); + p->d = 1; //WARN + free(p); + return 0; +}