From af1e6a1f95b340e874a3a0a64d4eca8e087c623e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 25 Jun 2026 16:50:34 +0300 Subject: [PATCH 1/3] Remove duplicate binop handling from memOutOfBounds --- src/analyses/memOutOfBounds.ml | 88 +------------------ .../74-invalid_deref/01-oob-heap-simple.t | 12 +-- 2 files changed, 7 insertions(+), 93 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 27096d2b61..5f577fcf11 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -116,19 +116,6 @@ struct | TPtr (t, _) -> Some t | _ -> None - let eval_ptr_offset_in_binop man exp ptr_contents_typ = - let eval_offset = man.ask (Queries.EvalInt exp) in - match eval_offset with - | `Lifted eo -> - let ptr_contents_typ_size_in_bytes = size_of_type_in_bytes ptr_contents_typ in - let casted_eo = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) eo in (* TODO: proper castkind *) - begin - try `Lifted (ID.mul casted_eo ptr_contents_typ_size_in_bytes) - with IntDomain.ArithmeticOnIntegerBot _ -> `Bot - end - | `Top -> `Top - | `Bot -> `Bot - let rec offs_to_idx typ offs = match offs with | `NoOffset -> intdom_of_int 0 @@ -222,14 +209,7 @@ struct 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 end end; - begin match e with - | Lval (Var v, _) as lval_exp -> check_no_binop_deref man lval_exp - | BinOp (binop, e1, e2, t) when binop = PlusPI || binop = MinusPI || binop = IndexPI -> - check_binop_exp man binop e1 e2 t; - check_exp_for_oob_access man ~is_implicitly_derefed e1; - check_exp_for_oob_access man ~is_implicitly_derefed e2 - | _ -> check_exp_for_oob_access man ~is_implicitly_derefed e - end + check_no_binop_deref man e and check_no_binop_deref man lval_exp = let behavior = Undefined MemoryOutOfBoundsAccess in @@ -293,72 +273,6 @@ struct | StartOf lval | AddrOf lval -> check_lval_for_oob_access man ~is_implicitly_derefed lval - and check_binop_exp man binop e1 e2 t = - let binopexp = BinOp (binop, e1, e2, t) in - let behavior = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in - match binop with - | PlusPI - | IndexPI - | MinusPI -> - let ptr_type = typeOf e1 in - let ptr_contents_type = get_ptr_deref_type ptr_type in - begin match ptr_contents_type with - | Some t -> - let offset_size = eval_ptr_offset_in_binop man e2 t in - let* addr = man.ask (Queries.MayPointTo e1) in - let ptr_size = get_addr_size man addr in - let addr_offs = get_addr_offset t addr in - (* Make sure to add the address offset to the binop offset *) - let offset_size_with_addr_size = match offset_size with - | `Lifted os -> - let casted_os = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) os in (* TODO: proper castkind *) - let casted_ao = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) addr_offs in (* TODO: proper castkind *) - begin - try `Lifted (ID.add casted_os casted_ao) - with IntDomain.ArithmeticOnIntegerBot _ -> `Bot - end - | `Top -> `Top - | `Bot -> `Bot - in - begin match ptr_size, offset_size_with_addr_size with - | `Top, _ -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is top. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a in expression %a is top. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp - | _, `Top -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is top. Memory out-of-bounds access might occur" d_exp binopexp; - Checks.warn Checks.Category.InvalidMemoryAccess "Operand value for pointer arithmetic in expression %a is top. Memory out-of-bounds access might occur" d_exp binopexp - | `Bot, _ -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is bottom. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a in expression %a is bottom. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp - | _, `Bot -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is bottom. Memory out-of-bounds access might occur" d_exp binopexp; - Checks.warn Checks.Category.InvalidMemoryAccess "Operand value for pointer arithmetic in expression %a is bottom. Memory out-of-bounds access might occur" d_exp binopexp - | `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 *) - begin match check_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 -> - Checks.safe Checks.Category.InvalidMemoryAccess - | _ -> - 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 - end - end - | _ -> M.error "Binary expression %a doesn't have a pointer" d_exp binopexp - end - | _ -> () - (* For memset() and memcpy() *) let check_count man fun_name ptr n = let (behavior:MessageCategory.behavior) = Undefined MemoryOutOfBoundsAccess in diff --git a/tests/regression/74-invalid_deref/01-oob-heap-simple.t b/tests/regression/74-invalid_deref/01-oob-heap-simple.t index ac3ec99fa8..6528f82bd5 100644 --- a/tests/regression/74-invalid_deref/01-oob-heap-simple.t +++ b/tests/regression/74-invalid_deref/01-oob-heap-simple.t @@ -1,7 +1,7 @@ $ goblint --set ana.activated[+] memOutOfBounds --enable ana.int.interval 01-oob-heap-simple.c 2>&1 | tee default-output.txt [Warning] The memOutOfBounds analysis enables cil.addNestedScopeAttr. - [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer in expression ptr + 10 is 5 (in bytes). It is offset by 10 (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) - [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (5) with offset (⊤). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) + [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 5 (in bytes). It is offset by 10 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) + [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (5) (in bytes) with offset by (⊤) (in bytes). Memory out-of-bounds access might occur (01-oob-heap-simple.c:11:5-11:21) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 8 dead: 0 @@ -11,9 +11,9 @@ $ diff default-output.txt full-output.txt 2,3c2,3 - < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer in expression ptr + 10 is 5 (in bytes). It is offset by 10 (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) - < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size (5) with offset (⊤). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) + < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is 5 (in bytes). It is offset by 10 (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) + < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (5) (in bytes) with offset by (⊤) (in bytes). Memory out-of-bounds access might occur (01-oob-heap-simple.c:11:5-11:21) --- - > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer in expression ptr + 10 is (5,[5,5]) (in bytes). It is offset by (10,[10,10]) (in bytes). Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) - > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare pointer size ((5,[5,5])) with offset ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) + > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer is (5,[5,5]) (in bytes). It is offset by (10,[10,10]) (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur (01-oob-heap-simple.c:10:5-10:22) + > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer ((5,[5,5])) (in bytes) with offset by ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])) (in bytes). Memory out-of-bounds access might occur (01-oob-heap-simple.c:11:5-11:21) [1] From 4e9fa40c9e58c310ce4127699ea6c3a0508ff743 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 26 Jun 2026 16:55:47 +0300 Subject: [PATCH 2/3] Add test 74-invalid_deref/40-oob-deref-cast --- tests/regression/74-invalid_deref/40-oob-deref-cast.c | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 tests/regression/74-invalid_deref/40-oob-deref-cast.c diff --git a/tests/regression/74-invalid_deref/40-oob-deref-cast.c b/tests/regression/74-invalid_deref/40-oob-deref-cast.c new file mode 100644 index 0000000000..721d426d6b --- /dev/null +++ b/tests/regression/74-invalid_deref/40-oob-deref-cast.c @@ -0,0 +1,9 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include + +int main() { + char* s = malloc(10); + s += 10; // NOWARN + unsigned char ch = (*(unsigned char *) s); // TODO WARN! + return 0; +} From 63e9e3680d1d239937ca9062b6be517fb8ff1d0b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 26 Jun 2026 17:35:07 +0300 Subject: [PATCH 3/3] Add test 74-invalid_deref/41-oob-coreutils-seq-incr --- .../41-oob-coreutils-seq-incr.c | 37 +++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 tests/regression/74-invalid_deref/41-oob-coreutils-seq-incr.c diff --git a/tests/regression/74-invalid_deref/41-oob-coreutils-seq-incr.c b/tests/regression/74-invalid_deref/41-oob-coreutils-seq-incr.c new file mode 100644 index 0000000000..2a3af3b2e5 --- /dev/null +++ b/tests/regression/74-invalid_deref/41-oob-coreutils-seq-incr.c @@ -0,0 +1,37 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +#include +#include + +// This is some wild C code from coreutils seq. +static void +incr (char **s0, size_t *s_len) +{ + char *s = *s0; // NOWARN + char *endp = s + *s_len - 1; // NOWARN + do + { + if ((*endp)++ < '9') // TODO NOWARN + return; + *endp-- = '0'; // TODO NOWARN + } + while (endp >= s); + *--(*s0) = '1'; // TODO WARN! + ++*s_len; // NOWARN +} + +int main() { + char* s = malloc(10); + memset(s, '0', 10); // NOWARN + + char* s2 = s + 9; + size_t len = 1; + incr(&s2, &len); // everything in this should be in bounds + + memset(s, '9', 10); // NOWARN + + s2 = s; + len = 10; + incr(&s2, &len); // something in this could be out of bounds + + return 0; +}