From c1149dfa90c0284431e354023dc370f7d79f3e9c Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 7 May 2026 15:21:26 +0300 Subject: [PATCH 01/15] Check for warn if pointer is dereferenced past end Co-authored-by: Michael Schwarz --- tests/regression/74-invalid_deref/36-one-past-pointer.c | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/regression/74-invalid_deref/36-one-past-pointer.c b/tests/regression/74-invalid_deref/36-one-past-pointer.c index b4ceb506d7..41cc4b54c9 100644 --- a/tests/regression/74-invalid_deref/36-one-past-pointer.c +++ b/tests/regression/74-invalid_deref/36-one-past-pointer.c @@ -7,6 +7,7 @@ int main(void) { char *end; end = buf + 4; //NOWARN printf("%p", (void *) end); //NOWARN + printf("%c", *end); //WARN free(buf); return 0; } From e14c553beea398301c9c637bbd4da195aab693ac Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 7 May 2026 15:25:08 +0300 Subject: [PATCH 02/15] Account for stored pointer offsets in deref checks --- src/analyses/memOutOfBounds.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 4546fda32e..d376ea8e81 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -52,6 +52,10 @@ struct in offs_lt_zero offs, ptr_size_lt_offs + let add_offsets x y = + try ID.add x y + with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + let rec exp_contains_a_ptr (exp:exp) = match exp with | Const _ @@ -295,6 +299,15 @@ struct | Some t -> cil_offs_to_idx man t o | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () end in + let offs_intdom = + match e with + | BinOp (binop, _, _, _) when binop = PlusPI || binop = MinusPI || binop = IndexPI -> + offs_intdom + | _ -> + let addr_offs = get_addr_offs man e in + let casted_addr_offs = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) addr_offs in (* TODO: proper castkind *) + add_offsets casted_addr_offs offs_intdom + in let e_size = get_size_of_ptr_target man e in begin match e_size with | `Top -> From 1948593d37b436ab741e63ddb2804700af33dacb Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 7 May 2026 16:07:05 +0300 Subject: [PATCH 03/15] Refactor: extract pointer arithmetic offset helpers --- src/analyses/memOutOfBounds.ml | 38 ++++++++++++++++++++++------------ 1 file changed, 25 insertions(+), 13 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index d376ea8e81..afc008a1e8 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -56,6 +56,14 @@ struct try ID.add x y with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + let is_ptr_arith_binop = function + | PlusPI | MinusPI | IndexPI -> true + | _ -> false + + let exp_is_explicit_ptr_arith = function + | BinOp (binop, _, _, _) -> is_ptr_arith_binop binop + | _ -> false + let rec exp_contains_a_ptr (exp:exp) = match exp with | Const _ @@ -204,7 +212,6 @@ struct in PreValueDomain.Offs.to_index (convert_offset offs) - let check_unknown_addr_deref man ptr = let may_contain_unknown_addr = match man.ask (Queries.EvalValue ptr) with @@ -294,20 +301,25 @@ struct | (Var _, _), false -> () | (Var v, _), true -> check_no_binop_deref man (Lval lval) | (Mem e, o), _ -> - let ptr_deref_type = get_ptr_deref_type @@ typeOf e in - let offs_intdom = begin match ptr_deref_type with - | Some t -> cil_offs_to_idx man t o + let get_lval_offset ptr_deref_type offs = + match ptr_deref_type with + | Some t -> cil_offs_to_idx man t offs | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - end in - let offs_intdom = - match e with - | BinOp (binop, _, _, _) when binop = PlusPI || binop = MinusPI || binop = IndexPI -> - offs_intdom - | _ -> - let addr_offs = get_addr_offs man e in - let casted_addr_offs = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) addr_offs in (* TODO: proper castkind *) - add_offsets casted_addr_offs offs_intdom in + let get_stored_addr_offset e = + let addr_offs = get_addr_offs man e in + ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) addr_offs (* TODO: proper castkind *) + in + let get_deref_offset ptr_deref_type e offs = + let lval_offs = get_lval_offset ptr_deref_type offs in + match exp_is_explicit_ptr_arith e with + | true -> (* Explicit pointer arithmetic is checked separately by check_binop_exp; do not add it here again. *) + lval_offs + | false -> + add_offsets (get_stored_addr_offset e) lval_offs + in + let ptr_deref_type = get_ptr_deref_type @@ typeOf e in + let offs_intdom = get_deref_offset ptr_deref_type e o in let e_size = get_size_of_ptr_target man e in begin match e_size with | `Top -> From 2132d736fed77b13e56c01f892d3c698b93558b8 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 7 May 2026 16:19:35 +0300 Subject: [PATCH 04/15] Refactor: inline pointer-arithmetic checks and simplify binop handling --- src/analyses/memOutOfBounds.ml | 37 +++++++++++++--------------------- 1 file changed, 14 insertions(+), 23 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index afc008a1e8..b19573bcf9 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -56,14 +56,6 @@ struct try ID.add x y with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - let is_ptr_arith_binop = function - | PlusPI | MinusPI | IndexPI -> true - | _ -> false - - let exp_is_explicit_ptr_arith = function - | BinOp (binop, _, _, _) -> is_ptr_arith_binop binop - | _ -> false - let rec exp_contains_a_ptr (exp:exp) = match exp with | Const _ @@ -312,10 +304,11 @@ struct in let get_deref_offset ptr_deref_type e offs = let lval_offs = get_lval_offset ptr_deref_type offs in - match exp_is_explicit_ptr_arith e with - | true -> (* Explicit pointer arithmetic is checked separately by check_binop_exp; do not add it here again. *) + match e with + | BinOp ((PlusPI | MinusPI | IndexPI), _, _, _) -> + (* Explicit pointer arithmetic is checked separately by check_binop_exp; do not add it here again. *) lval_offs - | false -> + | _ -> add_offsets (get_stored_addr_offset e) lval_offs in let ptr_deref_type = get_ptr_deref_type @@ typeOf e in @@ -351,8 +344,8 @@ struct 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; + | BinOp ((PlusPI | MinusPI | IndexPI), e1, e2, _) as binopexp -> + check_binop_exp man binopexp; 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 @@ -420,15 +413,12 @@ struct | StartOf lval | AddrOf lval -> check_lval_for_oob_access man ~is_implicitly_derefed lval - and check_binop_exp man binop e1 e2 t = - check_unknown_addr_deref man e1; - let binopexp = BinOp (binop, e1, e2, t) in - let behavior = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in - match binop with - | PlusPI - | IndexPI - | MinusPI -> + and check_binop_exp man binopexp = + match binopexp with + | BinOp ((PlusPI | MinusPI | IndexPI), e1, e2, _) -> + check_unknown_addr_deref man e1; + let behavior = Undefined MemoryOutOfBoundsAccess in + let cwe_number = 823 in let ptr_size = get_size_of_ptr_target man e1 in let addr_offs = get_addr_offs man e1 in let ptr_type = typeOf e1 in @@ -484,7 +474,8 @@ struct end | _ -> M.error "Binary expression %a doesn't have a pointer" d_exp binopexp end - | _ -> () + | _ -> + M.error "check_binop_exp called with non-pointer-arithmetic expression %a" d_exp binopexp (* For memset() and memcpy() *) let check_count man fun_name ptr n = From 7921e08413b69a60d2f48ed3f3f2df8fa9245040 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 7 May 2026 22:35:24 +0300 Subject: [PATCH 05/15] MemOutOfBounds: check accesses from access events Use access events instead of recursively traversing expressions in memOutOfBounds. This follows the same direction as the useAfterFree refactoring #1864: accessAnalysis determines what is accessed, while memOutOfBounds only checks the reported access. This avoids duplicating access traversal logic and removes the need to distinguish implicit from explicit dereferences in the analysis itself. Keep the initial refactor close to the previous implementation to make the behavioral diff easier to review. Further cleanup of now-obsolete helpers is left for a follow-up commit. --- src/analyses/accessAnalysis.ml | 2 +- src/analyses/memOutOfBounds.ml | 263 +++++++++++---------------------- 2 files changed, 88 insertions(+), 177 deletions(-) diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index 64c61a8d93..c67eee6cac 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -29,7 +29,7 @@ struct let init _ = collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed"; let activated = get_string_list "ana.activated" in - emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated (* TODO: some of these don't have access as dependency *) + emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated || List.mem (MemOutOfBounds.Spec.name ()) activated (* TODO: some of these don't have access as dependency *) let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) = if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach; diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index b19573bcf9..3aebe809a6 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -56,40 +56,6 @@ struct try ID.add x y with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - let rec exp_contains_a_ptr (exp:exp) = - match exp with - | Const _ - | SizeOf _ - | SizeOfStr _ - | AlignOf _ - | AddrOfLabel _ -> false - | Real e - | Imag e - | SizeOfE e - | AlignOfE e - | UnOp (_, e, _) - | CastE (_, _, e) -> exp_contains_a_ptr e - | BinOp (_, e1, e2, _) -> - exp_contains_a_ptr e1 || exp_contains_a_ptr e2 - | Question (e1, e2, e3, _) -> - exp_contains_a_ptr e1 || exp_contains_a_ptr e2 || exp_contains_a_ptr e3 - | Lval lval - | AddrOf lval - | StartOf lval -> lval_contains_a_ptr lval - - and lval_contains_a_ptr (lval:lval) = - let (host, offset) = lval in - let host_contains_a_ptr = function - | Var v -> isPointerType v.vtype - | Mem e -> exp_contains_a_ptr e - in - let rec offset_contains_a_ptr = function - | NoOffset -> false - | Index (e, o) -> exp_contains_a_ptr e || offset_contains_a_ptr o - | Field (f, o) -> isPointerType f.ftype || offset_contains_a_ptr o - in - host_contains_a_ptr host || offset_contains_a_ptr offset - let points_to_alloc_only man ptr = match man.ask (Queries.MayPointTo ptr) with | a when not (Queries.AD.is_top a)-> @@ -154,38 +120,24 @@ 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 - let ptr_contents_typ_size_in_bytes = size_of_type_in_bytes ptr_contents_typ in - match eval_offset with - | `Lifted eo -> - 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 eight = Z.of_int 8 + (* TODO: investigate why using PreValueDomain.Offs.to_index instead is too imprecise (to do with the Index case) *) let rec offs_to_idx typ offs = match offs with | `NoOffset -> intdom_of_int 0 | `Field (field, o) -> - let bytes_offset = Cilfacade.fieldBytesOffsetOnly field in - let bytes_offset = intdom_of_int bytes_offset in + let bits_offset = Cilfacade.fieldBitsOffsetOnly field in + let bits_offset = Z.of_int bits_offset in + (* Interval of floor and ceil division in case bitfield offset. *) + let bytes_offset = ID.of_interval (Cilfacade.ptrdiff_ikind ()) Z.(fdiv bits_offset eight, cdiv bits_offset eight) in let remaining_offset = offs_to_idx field.ftype o in - begin - try ID.add bytes_offset remaining_offset - with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - end + add_offsets bytes_offset remaining_offset | `Index (x, o) -> - begin try - let typ_size_in_bytes = size_of_type_in_bytes typ in - let bytes_offset = ID.mul typ_size_in_bytes x in - let remaining_offset = offs_to_idx typ o in - ID.add bytes_offset remaining_offset - with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - end + let typ_size_in_bytes = size_of_type_in_bytes typ in + let bytes_offset = ID.mul typ_size_in_bytes x in + let remaining_offset = offs_to_idx typ o in + add_offsets bytes_offset remaining_offset let cil_offs_to_idx man typ offs = (* TODO: Some duplication with convert_offset in base.ml, unclear how to immediately get more reuse *) @@ -232,8 +184,8 @@ struct (* Intuition: if ptr evaluates to top, it could all sorts of things and not only string addresses *) | _ -> false - let rec get_addr_offs man ptr = - match man.ask (Queries.MayPointTo ptr) with + let get_addr_offs_from_ad man ptr a = + match a with | a when not (VDQ.AD.is_top a) -> let ptr_deref_type = get_ptr_deref_type @@ typeOf ptr in begin match ptr_deref_type with @@ -283,7 +235,8 @@ struct Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; ID.top_of @@ Cilfacade.ptrdiff_ikind () - and check_lval_for_oob_access man ?(is_implicitly_derefed = false) lval = + (* let check_lval_for_oob_access man ?(is_implicitly_derefed = false) lval = + (* this fun is unused anyways, kept only to make initial diff more readable *) (* If the lval does not contain a pointer or if it does contain a pointer, but only points to string addresses, then no need to WARN *) if (not @@ lval_contains_a_ptr lval) || ptr_only_has_str_addr man (Lval lval) then () else @@ -349,9 +302,12 @@ struct 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 + end *) + + let get_addr_offs man ptr = + get_addr_offs_from_ad man ptr (man.ask (Queries.MayPointTo ptr)) - and check_no_binop_deref man lval_exp = + let check_ptr_access man lval_exp addr_offs = check_unknown_addr_deref man lval_exp; let behavior = Undefined MemoryOutOfBoundsAccess in let cwe_number = 823 in @@ -389,93 +345,55 @@ struct end | _ -> M.error "Expression %a is not a pointer" d_exp lval_exp - and check_exp_for_oob_access man ?(is_implicitly_derefed = false) exp = + let check_access_for_oob man exp ad = + let exp = Cil.stripCasts exp in match exp with - | Const _ - | SizeOf _ - | SizeOfStr _ - | AlignOf _ - | AddrOfLabel _ -> () - | Real e - | Imag e - | SizeOfE e - | AlignOfE e - | UnOp (_, e, _) - | CastE (_, _, e) -> check_exp_for_oob_access man ~is_implicitly_derefed e - | BinOp (bop, e1, e2, t) -> - check_exp_for_oob_access man ~is_implicitly_derefed e1; - check_exp_for_oob_access man ~is_implicitly_derefed e2 - | Question (e1, e2, e3, _) -> - 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 e3 - | Lval lval - | StartOf lval - | AddrOf lval -> check_lval_for_oob_access man ~is_implicitly_derefed lval - - and check_binop_exp man binopexp = - match binopexp with - | BinOp ((PlusPI | MinusPI | IndexPI), e1, e2, _) -> - check_unknown_addr_deref man e1; - let behavior = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in - let ptr_size = get_size_of_ptr_target man e1 in - let addr_offs = get_addr_offs man e1 in - 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 - (* 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_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 -> - 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 + | AddrOf (Mem e, o) when not (ptr_only_has_str_addr man e) -> + check_unknown_addr_deref man e; + let e_size = get_size_of_ptr_target man e in + let get_lval_offset ptr_deref_type offs = + match ptr_deref_type with + | Some t -> cil_offs_to_idx man t offs + | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + in + let ptr_deref_type = get_ptr_deref_type @@ typeOf e in + let stored_addr_offs = get_addr_offs man e in + let lval_offs = get_lval_offset ptr_deref_type o in + let offs_intdom = add_offsets stored_addr_offs lval_offs in + begin match e_size with + | `Top -> + (set_mem_safety_flag InvalidDeref; + M.warn "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e); + Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e + | `Bot -> + (set_mem_safety_flag InvalidDeref; + M.warn "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e); + Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e + | `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 behavior = Undefined MemoryOutOfBoundsAccess in + let cwe_number = 823 in + 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 -> + Checks.safe Checks.Category.InvalidMemoryAccess + | _ -> + (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 end - | _ -> M.error "Binary expression %a doesn't have a pointer" d_exp binopexp end + | AddrOf _ -> + () + | _ when isPointerType (typeOf exp) && not (ptr_only_has_str_addr man exp) -> + check_ptr_access man exp (get_addr_offs_from_ad man exp ad) | _ -> - M.error "check_binop_exp called with non-pointer-arithmetic expression %a" d_exp binopexp + () (* For memset() and memcpy() *) let check_count man fun_name ptr n = @@ -518,34 +436,26 @@ struct M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name; Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name end - - - (* TRANSFER FUNCTIONS *) - - let assign man (lval:lval) (rval:exp) : D.t = - check_lval_for_oob_access man lval; - check_exp_for_oob_access man rval; - man.local - - let branch man (exp:exp) (tv:bool) : D.t = - check_exp_for_oob_access man exp; - man.local - - let return man (exp:exp option) (f:fundec) : D.t = - Option.iter (fun x -> check_exp_for_oob_access man x) exp; - man.local - let special man (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = let desc = LibraryFunctions.find f in - let is_arg_implicitly_derefed arg = + let is_arg_accessed_through_pointer arg = let read_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = false } arglist in let read_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = true } arglist in let write_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } arglist in let write_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } arglist in List.mem arg read_shallow_args || List.mem arg read_deep_args || List.mem arg write_shallow_args || List.mem arg write_deep_args in - Option.iter (fun x -> check_lval_for_oob_access man x) lval; - List.iter (fun arg -> check_exp_for_oob_access man ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) arg) arglist; + (* Access events don't preserve whether AddrOf/StartOf arguments were dereferenced by a special access. *) + List.iter (fun arg -> + if is_arg_accessed_through_pointer arg then + match Cil.stripCasts arg with + | AddrOf lval + | StartOf lval -> + let ptr_exp = Lval lval in + check_ptr_access man ptr_exp (get_addr_offs man ptr_exp) + | _ -> + () + ) arglist; (* Check calls to memset and memcpy for out-of-bounds-accesses *) match desc.special arglist with | Memset { dest; ch; count; } -> check_count man f.vname dest count; @@ -554,17 +464,18 @@ struct check_count man f.vname dest count;) | _ -> man.local - let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = - List.iter (fun arg -> check_exp_for_oob_access man arg) args; - [man.local, man.local] - - let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = - Option.iter (fun x -> check_lval_for_oob_access man x) lval; - man.local - let startstate v = () let exitstate v = () + + let event man e oman = + match e with + | Events.Access {exp; ad; _} -> + (* must use original (pre-assign, etc) man queries *) + check_access_for_oob oman exp ad; + man.local + | _ -> + man.local end let _ = - MCP.register_analysis (module Spec : MCPSpec) + MCP.register_analysis ~dep:["access"] (module Spec : MCPSpec) From 502ef63909a8ab9ef978f4a5c4fbfa30237bebdd Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 7 May 2026 23:05:51 +0300 Subject: [PATCH 06/15] Remove unused function --- src/analyses/memOutOfBounds.ml | 69 ---------------------------------- 1 file changed, 69 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 3aebe809a6..c31836327e 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -235,75 +235,6 @@ struct Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; ID.top_of @@ Cilfacade.ptrdiff_ikind () - (* let check_lval_for_oob_access man ?(is_implicitly_derefed = false) lval = - (* this fun is unused anyways, kept only to make initial diff more readable *) - (* If the lval does not contain a pointer or if it does contain a pointer, but only points to string addresses, then no need to WARN *) - if (not @@ lval_contains_a_ptr lval) || ptr_only_has_str_addr man (Lval lval) then () - else - (* If the lval doesn't indicate an explicit dereference, we still need to check for an implicit dereference *) - (* An implicit dereference is, e.g., printf("%p", ptr), where ptr is a pointer *) - match lval, is_implicitly_derefed with - | (Var _, _), false -> () - | (Var v, _), true -> check_no_binop_deref man (Lval lval) - | (Mem e, o), _ -> - let get_lval_offset ptr_deref_type offs = - match ptr_deref_type with - | Some t -> cil_offs_to_idx man t offs - | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - in - let get_stored_addr_offset e = - let addr_offs = get_addr_offs man e in - ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) addr_offs (* TODO: proper castkind *) - in - let get_deref_offset ptr_deref_type e offs = - let lval_offs = get_lval_offset ptr_deref_type offs in - match e with - | BinOp ((PlusPI | MinusPI | IndexPI), _, _, _) -> - (* Explicit pointer arithmetic is checked separately by check_binop_exp; do not add it here again. *) - lval_offs - | _ -> - add_offsets (get_stored_addr_offset e) lval_offs - in - let ptr_deref_type = get_ptr_deref_type @@ typeOf e in - let offs_intdom = get_deref_offset ptr_deref_type e o in - let e_size = get_size_of_ptr_target man e in - begin match e_size with - | `Top -> - (set_mem_safety_flag InvalidDeref; - M.warn "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e); - Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e - | `Bot -> - (set_mem_safety_flag InvalidDeref; - M.warn "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e); - Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e - | `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 behavior = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in - 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 -> - Checks.safe Checks.Category.InvalidMemoryAccess - | _ -> - (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 - end - end; - begin match e with - | Lval (Var v, _) as lval_exp -> check_no_binop_deref man lval_exp - | BinOp ((PlusPI | MinusPI | IndexPI), e1, e2, _) as binopexp -> - check_binop_exp man binopexp; - 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 *) - let get_addr_offs man ptr = get_addr_offs_from_ad man ptr (man.ask (Queries.MayPointTo ptr)) From d685a429fb12632b87f63a89e74837fa9fe6f6a0 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 7 May 2026 23:11:05 +0300 Subject: [PATCH 07/15] Extract ptr deref part into own fun to make `check_access_for_oob`cases symmetrical --- src/analyses/memOutOfBounds.ml | 115 +++++++++++++++++---------------- 1 file changed, 59 insertions(+), 56 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index c31836327e..0fece5dac2 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -238,25 +238,63 @@ struct let get_addr_offs man ptr = get_addr_offs_from_ad man ptr (man.ask (Queries.MayPointTo ptr)) - let check_ptr_access man lval_exp addr_offs = - check_unknown_addr_deref man lval_exp; - let behavior = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in - let ptr_size = get_size_of_ptr_target man lval_exp in - let addr_offs = get_addr_offs man lval_exp in - let ptr_type = typeOf lval_exp in - let ptr_contents_type = get_ptr_deref_type ptr_type in - match ptr_contents_type with - | Some t -> + let check_ptr_deref_access man ptr_exp offs = + check_unknown_addr_deref man ptr_exp; + let get_lval_offset ptr_deref_type offs = + match ptr_deref_type with + | Some t -> cil_offs_to_idx man t offs + | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + in + let ptr_deref_type = get_ptr_deref_type @@ typeOf ptr_exp in + let stored_addr_offs = get_addr_offs man ptr_exp in + let lval_offs = get_lval_offset ptr_deref_type offs in + let offs_intdom = add_offsets stored_addr_offs lval_offs in + begin match get_size_of_ptr_target man ptr_exp with + | `Top -> + (set_mem_safety_flag InvalidDeref; + M.warn "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp ptr_exp); + Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp ptr_exp + | `Bot -> + (set_mem_safety_flag InvalidDeref; + M.warn "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp ptr_exp); + Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp ptr_exp + | `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 behavior = Undefined MemoryOutOfBoundsAccess in + let cwe_number = 823 in + 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 -> + Checks.safe Checks.Category.InvalidMemoryAccess + | _ -> + (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 + end + end + + let check_ptr_value_access man ptr_exp = + match get_ptr_deref_type @@ typeOf ptr_exp with + | Some _ -> + check_unknown_addr_deref man ptr_exp; + let behavior = Undefined MemoryOutOfBoundsAccess in + let cwe_number = 823 in + let ptr_size = get_size_of_ptr_target man ptr_exp in + let addr_offs = get_addr_offs man ptr_exp in begin match ptr_size, addr_offs with | `Top, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp | `Bot, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp | `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 *) @@ -274,55 +312,20 @@ struct 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 end end - | _ -> M.error "Expression %a is not a pointer" d_exp lval_exp + | _ -> M.error "Expression %a is not a pointer" d_exp ptr_exp let check_access_for_oob man exp ad = let exp = Cil.stripCasts exp in match exp with + (* Actual dereference/access through a pointer. *) | AddrOf (Mem e, o) when not (ptr_only_has_str_addr man e) -> - check_unknown_addr_deref man e; - let e_size = get_size_of_ptr_target man e in - let get_lval_offset ptr_deref_type offs = - match ptr_deref_type with - | Some t -> cil_offs_to_idx man t offs - | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - in - let ptr_deref_type = get_ptr_deref_type @@ typeOf e in - let stored_addr_offs = get_addr_offs man e in - let lval_offs = get_lval_offset ptr_deref_type o in - let offs_intdom = add_offsets stored_addr_offs lval_offs in - begin match e_size with - | `Top -> - (set_mem_safety_flag InvalidDeref; - M.warn "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e); - Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e - | `Bot -> - (set_mem_safety_flag InvalidDeref; - M.warn "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e); - Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e - | `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 behavior = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in - 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 -> - Checks.safe Checks.Category.InvalidMemoryAccess - | _ -> - (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 - end - end + check_ptr_deref_access man e o + (* Taking the address of something is not an access itself. *) | AddrOf _ -> () + (* Pointer arithmetic / pointer value access. *) | _ when isPointerType (typeOf exp) && not (ptr_only_has_str_addr man exp) -> - check_ptr_access man exp (get_addr_offs_from_ad man exp ad) + check_ptr_value_access man exp | _ -> () @@ -383,7 +386,7 @@ struct | AddrOf lval | StartOf lval -> let ptr_exp = Lval lval in - check_ptr_access man ptr_exp (get_addr_offs man ptr_exp) + check_ptr_value_access man ptr_exp | _ -> () ) arglist; From 71a7cd36ef07c0a10831833318470a18bcd63110 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 7 May 2026 23:15:00 +0300 Subject: [PATCH 08/15] Extract common category and tags to top level and move computations into cases that use them --- src/analyses/memOutOfBounds.ml | 61 ++++++++++++++++------------------ 1 file changed, 28 insertions(+), 33 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 0fece5dac2..4dbe556de5 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -28,6 +28,9 @@ struct (* HELPER FUNCTIONS *) + let mem_oob_behavior = Undefined MemoryOutOfBoundsAccess + let mem_oob_cwe = 823 + let intdom_of_int x = ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) @@ -240,40 +243,36 @@ struct let check_ptr_deref_access man ptr_exp offs = check_unknown_addr_deref man ptr_exp; - let get_lval_offset ptr_deref_type offs = - match ptr_deref_type with - | Some t -> cil_offs_to_idx man t offs - | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () - in - let ptr_deref_type = get_ptr_deref_type @@ typeOf ptr_exp in - let stored_addr_offs = get_addr_offs man ptr_exp in - let lval_offs = get_lval_offset ptr_deref_type offs in - let offs_intdom = add_offsets stored_addr_offs lval_offs in begin match get_size_of_ptr_target man ptr_exp with | `Top -> - (set_mem_safety_flag InvalidDeref; - M.warn "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp ptr_exp); + set_mem_safety_flag InvalidDeref; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp ptr_exp; Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp ptr_exp | `Bot -> - (set_mem_safety_flag InvalidDeref; - M.warn "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp ptr_exp); + set_mem_safety_flag InvalidDeref; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp ptr_exp; Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp ptr_exp | `Lifted es -> + let stored_addr_offs = get_addr_offs man ptr_exp in + let lval_offs = + match get_ptr_deref_type @@ typeOf ptr_exp with + | Some t -> cil_offs_to_idx man t offs + | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + in + let offs_intdom = add_offsets stored_addr_offs lval_offs in 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 behavior = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in 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); + set_mem_safety_flag InvalidDeref; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "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 -> Checks.safe Checks.Category.InvalidMemoryAccess | _ -> - (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); + set_mem_safety_flag InvalidDeref; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "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 end end @@ -282,18 +281,16 @@ struct match get_ptr_deref_type @@ typeOf ptr_exp with | Some _ -> check_unknown_addr_deref man ptr_exp; - let behavior = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in let ptr_size = get_size_of_ptr_target man ptr_exp in let addr_offs = get_addr_offs man ptr_exp in begin match ptr_size, addr_offs with | `Top, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp; Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp | `Bot, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp; Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp | `Lifted ps, ao -> let casted_ps = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *) @@ -302,13 +299,13 @@ struct | 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; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "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 -> Checks.safe Checks.Category.InvalidMemoryAccess | _ -> 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; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "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 end end @@ -331,27 +328,25 @@ struct (* For memset() and memcpy() *) let check_count man fun_name ptr n = - let (behavior:MessageCategory.behavior) = Undefined MemoryOutOfBoundsAccess in - let cwe_number = 823 in let ptr_size = get_size_of_ptr_target man ptr in let eval_n = man.ask (Queries.EvalInt n) in let addr_offs = get_addr_offs man ptr in match ptr_size, eval_n with | `Top, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp ptr fun_name; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp ptr fun_name; Checks.warn Checks.Category.InvalidMemoryAccess "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp ptr fun_name | _, `Top -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name; Checks.warn Checks.Category.InvalidMemoryAccess "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name | `Bot, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp ptr fun_name; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp ptr fun_name; Checks.warn Checks.Category.InvalidMemoryAccess "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp ptr fun_name | _, `Bot -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Count parameter, passed to function %s is bottom" fun_name; Checks.warn Checks.Category.InvalidMemoryAccess "Count parameter, passed to function %s is bottom" fun_name | `Lifted ds, `Lifted en -> let casted_ds = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ds in (* TODO: proper castkind *) @@ -361,13 +356,13 @@ struct begin match dest_size_lt_count with | Some true -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of %a in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of %a in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en; Checks.warn Checks.Category.InvalidMemoryAccess "Size of %a in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en | 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 dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name; + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name; Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name end let special man (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = From 2c2fa2a5a2fe9597a066a8b5b34b38accfe64197 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 7 May 2026 23:50:06 +0300 Subject: [PATCH 09/15] Actually use the addr from event in `check_ptr_value_access` --- 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 4dbe556de5..e642f755b8 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -277,12 +277,11 @@ struct end end - let check_ptr_value_access man ptr_exp = + let check_ptr_value_access man ptr_exp addr_offs = match get_ptr_deref_type @@ typeOf ptr_exp with | Some _ -> check_unknown_addr_deref man ptr_exp; let ptr_size = get_size_of_ptr_target man ptr_exp in - let addr_offs = get_addr_offs man ptr_exp in begin match ptr_size, addr_offs with | `Top, _ -> set_mem_safety_flag InvalidDeref; @@ -322,7 +321,7 @@ struct () (* Pointer arithmetic / pointer value access. *) | _ when isPointerType (typeOf exp) && not (ptr_only_has_str_addr man exp) -> - check_ptr_value_access man exp + check_ptr_value_access man exp (get_addr_offs_from_ad man exp ad) | _ -> () @@ -381,7 +380,7 @@ struct | AddrOf lval | StartOf lval -> let ptr_exp = Lval lval in - check_ptr_value_access man ptr_exp + check_ptr_value_access man ptr_exp (get_addr_offs man ptr_exp) | _ -> () ) arglist; From c5eadfa46f69fde07d7f103fc2ed4e6f9fbf4dfb Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 8 May 2026 00:11:03 +0300 Subject: [PATCH 10/15] Remove redundant warnings from offset calculations --- src/analyses/memOutOfBounds.ml | 50 ++++++++++------------------------ 1 file changed, 15 insertions(+), 35 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index e642f755b8..6c0e0533b1 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -190,52 +190,32 @@ struct let get_addr_offs_from_ad man ptr a = match a with | a when not (VDQ.AD.is_top a) -> - let ptr_deref_type = get_ptr_deref_type @@ typeOf ptr in - begin match ptr_deref_type with + begin match get_ptr_deref_type @@ typeOf ptr with | Some t -> - begin match VDQ.AD.is_empty a with - | true -> - M.warn "Pointer %a has an empty points-to-set" d_exp ptr; - Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has an empty points-to-set" d_exp ptr; + if VDQ.AD.is_empty a then + ID.top_of @@ Cilfacade.ptrdiff_ikind () + else + (* Get the address offsets of all points-to set elements *) + let addr_offsets = + VDQ.AD.filter (function Addr _ -> true | _ -> false) a + |> VDQ.AD.to_mval + |> List.map (fun (_, o) -> offs_to_idx t o) + in + if List.exists ID.is_bot addr_offsets then + ID.bot_of @@ Cilfacade.ptrdiff_ikind () + else if List.exists (ID.is_top_of (Cilfacade.ptrdiff_ikind ())) addr_offsets then ID.top_of @@ Cilfacade.ptrdiff_ikind () - | false -> - if VDQ.AD.exists (function - | Addr (_, o) -> ID.is_bot @@ offs_to_idx t o - | _ -> false - ) a then ( - set_mem_safety_flag InvalidDeref; - M.warn "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr; - Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr - ) else if VDQ.AD.exists (function - | Addr (_, o) -> ID.is_top_of (Cilfacade.ptrdiff_ikind ()) (offs_to_idx t o) - | _ -> false - ) a then ( - set_mem_safety_flag InvalidDeref; - M.warn "Pointer %a has a top address offset. An invalid memory access may occur" d_exp ptr; - Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has a top address offset. An invalid memory access may occur" d_exp ptr - ) else ( - Checks.safe Checks.Category.InvalidMemoryAccess - ); - (* Get the address offsets of all points-to set elements *) - let addr_offsets = - VDQ.AD.filter (function Addr (v, o) -> true | _ -> false) a - |> VDQ.AD.to_mval - |> List.map (fun (_, o) -> offs_to_idx t o) - in + else begin match addr_offsets with | [] -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () | [x] -> x - | x::xs -> List.fold_left ID.join x xs + | x :: xs -> List.fold_left ID.join x xs end - end | None -> M.error "Expression %a doesn't have pointer type" d_exp ptr; ID.top_of @@ Cilfacade.ptrdiff_ikind () end | _ -> - set_mem_safety_flag InvalidDeref; - M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; - Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; ID.top_of @@ Cilfacade.ptrdiff_ikind () let get_addr_offs man ptr = From 83e65c2b637c4021c2b835691f50de04f4918d6f Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 8 May 2026 00:19:19 +0300 Subject: [PATCH 11/15] Change warning messages and promote --- src/analyses/memOutOfBounds.ml | 48 ++++++++++++------- .../74-invalid_deref/01-oob-heap-simple.t | 12 ++--- 2 files changed, 38 insertions(+), 22 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 6c0e0533b1..ba839ddeb6 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -226,12 +226,12 @@ struct begin match get_size_of_ptr_target man ptr_exp with | `Top -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp ptr_exp; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp ptr_exp + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of object accessed through %a is top. Out-of-bounds memory access may occur" d_exp ptr_exp; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of object accessed through %a is top. Out-of-bounds memory access may occur" d_exp ptr_exp | `Bot -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp ptr_exp; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp ptr_exp + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of object accessed through %a is bot. Out-of-bounds memory access may occur" d_exp ptr_exp; + Checks.warn Checks.Category.InvalidMemoryAccess "Size of object accessed through %a is bot. Out-of-bounds memory access may occur" d_exp ptr_exp | `Lifted es -> let stored_addr_offs = get_addr_offs man ptr_exp in let lval_offs = @@ -246,14 +246,22 @@ struct | Some true, _ | _, Some true -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "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 + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] + "Size of object accessed through %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" + d_exp ptr_exp ID.pretty casted_es ID.pretty casted_offs; + Checks.warn Checks.Category.InvalidMemoryAccess + "Size of object accessed through %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" + d_exp ptr_exp ID.pretty casted_es ID.pretty casted_offs | Some false, Some false -> Checks.safe Checks.Category.InvalidMemoryAccess | _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "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 + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] + "Could not compare size of object accessed through %a (%a) (in bytes) with offset (%a) (in bytes). Memory out-of-bounds access might occur" + d_exp ptr_exp ID.pretty casted_es ID.pretty casted_offs; + Checks.warn Checks.Category.InvalidMemoryAccess + "Could not compare size of object accessed through %a (%a) (in bytes) with offset (%a) (in bytes). Memory out-of-bounds access might occur" + d_exp ptr_exp ID.pretty casted_es ID.pretty casted_offs end end @@ -265,12 +273,16 @@ struct begin match ptr_size, addr_offs with | `Top, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] + "Size of object pointed to by %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp; + Checks.warn Checks.Category.InvalidMemoryAccess + "Size of object pointed to by %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp | `Bot, _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] + "Size of object pointed to by %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp; + Checks.warn Checks.Category.InvalidMemoryAccess + "Size of object pointed to by %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp | `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 *) @@ -278,14 +290,18 @@ struct | Some true, _ | _, Some true -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "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 + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] + "Size of object pointed to by %a is %a (in bytes). Pointer offset is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr_exp ID.pretty casted_ps ID.pretty casted_ao; + Checks.warn Checks.Category.InvalidMemoryAccess + "Size of object pointed to by %a is %a (in bytes). Pointer offset is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr_exp ID.pretty casted_ps ID.pretty casted_ao | Some false, Some false -> Checks.safe Checks.Category.InvalidMemoryAccess | _ -> set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "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 + M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] + "Could not compare size of object pointed to by %a (%a) (in bytes) with pointer offset (%a) (in bytes). Memory out-of-bounds access might occur" d_exp ptr_exp ID.pretty casted_ps ID.pretty casted_ao; + Checks.warn Checks.Category.InvalidMemoryAccess + "Could not compare size of object pointed to by %a (%a) (in bytes) with pointer offset (%a) (in bytes). Memory out-of-bounds access might occur" d_exp ptr_exp ID.pretty casted_ps ID.pretty casted_ao end end | _ -> M.error "Expression %a is not a pointer" d_exp ptr_exp 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..0046fa7963 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 object accessed through 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 size of object accessed through ptr + r (5) (in bytes) with offset (⊤) (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 object accessed through 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 size of object accessed through ptr + r (5) (in bytes) with offset (⊤) (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 object accessed through 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 size of object accessed through ptr + r ((5,[5,5])) (in bytes) with offset ((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 074e4d7db486eea10b8427dfc1e2150150ee3b5e Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 8 May 2026 00:50:08 +0300 Subject: [PATCH 12/15] Refactor excessive warn msg duplication into helper functions --- src/analyses/memOutOfBounds.ml | 103 +++++++++++---------------------- 1 file changed, 33 insertions(+), 70 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index ba839ddeb6..fb80fbbbed 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -28,8 +28,12 @@ struct (* HELPER FUNCTIONS *) - let mem_oob_behavior = Undefined MemoryOutOfBoundsAccess - let mem_oob_cwe = 823 + let report_oob fmt = + set_mem_safety_flag InvalidDeref; + Pretty.gprintf (fun doc -> + M.warn ~category:(Behavior (Undefined MemoryOutOfBoundsAccess)) ~tags:[CWE 823] "%a" Pretty.insert doc; + Checks.warn Checks.Category.InvalidMemoryAccess "%a" Pretty.insert doc; + ) fmt let intdom_of_int x = ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) @@ -80,9 +84,7 @@ struct begin match addr with | Addr (v, _) -> if hasAttribute "goblint_cil_nested" v.vattr then ( - set_mem_safety_flag InvalidDeref; - M.warn "Var %a is potentially accessed out-of-scope. Invalid memory access may occur" CilType.Varinfo.pretty v; - Checks.warn Checks.Category.InvalidMemoryAccess "Var %a is potentially accessed out-of-scope. Invalid memory access may occur" CilType.Varinfo.pretty v + report_oob "Var %a is potentially accessed out-of-scope. Invalid memory access may occur" CilType.Varinfo.pretty v ); begin match Cil.unrollType v.vtype with | TArray (item_typ, _, _) -> @@ -113,10 +115,8 @@ struct | x::xs -> List.fold_left VDQ.ID.join x xs end | _ -> - (set_mem_safety_flag InvalidDeref; - M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; - Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; - `Top) + report_oob "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; + `Top let get_ptr_deref_type ptr_typ = match Cil.unrollType ptr_typ with @@ -171,9 +171,7 @@ struct | _ -> true in if may_contain_unknown_addr then begin - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior (Undefined Other)) "Pointer %a contains an unknown address. Invalid dereference may occur" d_exp ptr; - Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a contains an unknown address. Invalid dereference may occur" d_exp ptr + report_oob "Pointer %a contains an unknown address. Invalid dereference may occur" d_exp ptr end else Checks.safe Checks.Category.InvalidMemoryAccess @@ -221,17 +219,22 @@ struct let get_addr_offs man ptr = get_addr_offs_from_ad man ptr (man.ask (Queries.MayPointTo ptr)) + let report_unknown_object_size access_desc d_exp ptr_exp size_desc = + report_oob "Size of object %s %a is %s. Memory out-of-bounds access might occur" access_desc d_exp ptr_exp size_desc + + let report_must_offset_oob access_desc d_exp ptr_exp object_size offset = + report_oob "Size of object %s %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" access_desc d_exp ptr_exp ID.pretty object_size ID.pretty offset + + let report_may_offset_oob access_desc d_exp ptr_exp object_size offset = + report_oob "Could not compare size of object %s %a (%a) (in bytes) with offset (%a) (in bytes). Memory out-of-bounds access might occur" access_desc d_exp ptr_exp ID.pretty object_size ID.pretty offset + let check_ptr_deref_access man ptr_exp offs = check_unknown_addr_deref man ptr_exp; begin match get_size_of_ptr_target man ptr_exp with | `Top -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of object accessed through %a is top. Out-of-bounds memory access may occur" d_exp ptr_exp; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of object accessed through %a is top. Out-of-bounds memory access may occur" d_exp ptr_exp + report_unknown_object_size "accessed through" d_exp ptr_exp "top" | `Bot -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of object accessed through %a is bot. Out-of-bounds memory access may occur" d_exp ptr_exp; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of object accessed through %a is bot. Out-of-bounds memory access may occur" d_exp ptr_exp + report_unknown_object_size "accessed through" d_exp ptr_exp "bot" | `Lifted es -> let stored_addr_offs = get_addr_offs man ptr_exp in let lval_offs = @@ -245,23 +248,11 @@ struct begin match check_deref_offset_bounds casted_es casted_offs with | Some true, _ | _, Some true -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] - "Size of object accessed through %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" - d_exp ptr_exp ID.pretty casted_es ID.pretty casted_offs; - Checks.warn Checks.Category.InvalidMemoryAccess - "Size of object accessed through %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" - d_exp ptr_exp ID.pretty casted_es ID.pretty casted_offs + report_must_offset_oob "accessed through" d_exp ptr_exp casted_es casted_offs; | Some false, Some false -> Checks.safe Checks.Category.InvalidMemoryAccess | _ -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] - "Could not compare size of object accessed through %a (%a) (in bytes) with offset (%a) (in bytes). Memory out-of-bounds access might occur" - d_exp ptr_exp ID.pretty casted_es ID.pretty casted_offs; - Checks.warn Checks.Category.InvalidMemoryAccess - "Could not compare size of object accessed through %a (%a) (in bytes) with offset (%a) (in bytes). Memory out-of-bounds access might occur" - d_exp ptr_exp ID.pretty casted_es ID.pretty casted_offs + report_may_offset_oob "accessed through" d_exp ptr_exp casted_es casted_offs; end end @@ -272,36 +263,20 @@ struct let ptr_size = get_size_of_ptr_target man ptr_exp in begin match ptr_size, addr_offs with | `Top, _ -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] - "Size of object pointed to by %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp; - Checks.warn Checks.Category.InvalidMemoryAccess - "Size of object pointed to by %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp + report_unknown_object_size "pointed to by" d_exp ptr_exp "top" | `Bot, _ -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] - "Size of object pointed to by %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp; - Checks.warn Checks.Category.InvalidMemoryAccess - "Size of object pointed to by %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp ptr_exp + report_unknown_object_size "pointed to by" d_exp ptr_exp "bot" | `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 *) begin match check_ptr_offset_bounds casted_ps casted_ao with | Some true, _ | _, Some true -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] - "Size of object pointed to by %a is %a (in bytes). Pointer offset is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr_exp ID.pretty casted_ps ID.pretty casted_ao; - Checks.warn Checks.Category.InvalidMemoryAccess - "Size of object pointed to by %a is %a (in bytes). Pointer offset is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr_exp ID.pretty casted_ps ID.pretty casted_ao + report_must_offset_oob "pointed to by" d_exp ptr_exp casted_ps casted_ao | Some false, Some false -> Checks.safe Checks.Category.InvalidMemoryAccess | _ -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] - "Could not compare size of object pointed to by %a (%a) (in bytes) with pointer offset (%a) (in bytes). Memory out-of-bounds access might occur" d_exp ptr_exp ID.pretty casted_ps ID.pretty casted_ao; - Checks.warn Checks.Category.InvalidMemoryAccess - "Could not compare size of object pointed to by %a (%a) (in bytes) with pointer offset (%a) (in bytes). Memory out-of-bounds access might occur" d_exp ptr_exp ID.pretty casted_ps ID.pretty casted_ao + report_may_offset_oob "pointed to by" d_exp ptr_exp casted_ps casted_ao end end | _ -> M.error "Expression %a is not a pointer" d_exp ptr_exp @@ -328,21 +303,13 @@ struct let addr_offs = get_addr_offs man ptr in match ptr_size, eval_n with | `Top, _ -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp ptr fun_name; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp ptr fun_name + report_oob "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp ptr fun_name; | _, `Top -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name; - Checks.warn Checks.Category.InvalidMemoryAccess "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name + report_oob "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name | `Bot, _ -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp ptr fun_name; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp ptr fun_name + report_oob "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp ptr fun_name | _, `Bot -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Count parameter, passed to function %s is bottom" fun_name; - Checks.warn Checks.Category.InvalidMemoryAccess "Count parameter, passed to function %s is bottom" fun_name + report_oob "Count parameter, passed to function %s is bottom" fun_name | `Lifted ds, `Lifted en -> let casted_ds = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) ds in (* TODO: proper castkind *) let casted_en = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) en in (* TODO: proper castkind *) @@ -350,15 +317,11 @@ struct let dest_size_lt_count = ID.lt casted_ds (ID.add casted_en casted_ao) in begin match dest_size_lt_count with | Some true -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Size of %a in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en; - Checks.warn Checks.Category.InvalidMemoryAccess "Size of %a in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en + report_oob "Size of %a in function %s is %a (in bytes) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" d_exp ptr fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en | Some false -> Checks.safe Checks.Category.InvalidMemoryAccess | None -> - set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior mem_oob_behavior) ~tags:[CWE mem_oob_cwe] "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name; - Checks.warn Checks.Category.InvalidMemoryAccess "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name + report_oob "Could not compare size of dest (%a) with address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name end let special man (lval:lval option) (f:varinfo) (arglist:exp list) : D.t = let desc = LibraryFunctions.find f in From 2ad23f6384c86e94f64e872f2bcd1a54999f3048 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 8 May 2026 12:36:37 +0300 Subject: [PATCH 13/15] Refactor: extract duplicate code into helper function --- src/analyses/memOutOfBounds.ml | 44 +++++++------------ .../74-invalid_deref/01-oob-heap-simple.t | 6 +-- 2 files changed, 20 insertions(+), 30 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index fb80fbbbed..146f4323e8 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -222,11 +222,21 @@ struct let report_unknown_object_size access_desc d_exp ptr_exp size_desc = report_oob "Size of object %s %a is %s. Memory out-of-bounds access might occur" access_desc d_exp ptr_exp size_desc - let report_must_offset_oob access_desc d_exp ptr_exp object_size offset = - report_oob "Size of object %s %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" access_desc d_exp ptr_exp ID.pretty object_size ID.pretty offset - - let report_may_offset_oob access_desc d_exp ptr_exp object_size offset = - report_oob "Could not compare size of object %s %a (%a) (in bytes) with offset (%a) (in bytes). Memory out-of-bounds access might occur" access_desc d_exp ptr_exp ID.pretty object_size ID.pretty offset + let check_offset_against_object_size access_desc bounds_check man ptr_exp object_size offset = + let ptrdiff_ikind = Cilfacade.ptrdiff_ikind () in + let casted_object_size = ID.cast_to ~kind:Internal ptrdiff_ikind object_size in (* TODO: proper castkind *) + let casted_offset = ID.cast_to ~kind:Internal ptrdiff_ikind offset in (* TODO: proper castkind *) + begin match bounds_check casted_object_size casted_offset with + | Some true, _ + | _, Some true -> + report_oob "Size of object %s %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" + access_desc d_exp ptr_exp ID.pretty casted_object_size ID.pretty casted_offset + | Some false, Some false -> + Checks.safe Checks.Category.InvalidMemoryAccess + | _ -> + report_oob "Could not compare size of object %s %a (%a) (in bytes) with offset (%a) (in bytes). Memory out-of-bounds access may occur" + access_desc d_exp ptr_exp ID.pretty casted_object_size ID.pretty casted_offset + end let check_ptr_deref_access man ptr_exp offs = check_unknown_addr_deref man ptr_exp; @@ -243,17 +253,7 @@ struct | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () in let offs_intdom = add_offsets stored_addr_offs lval_offs in - 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 *) - begin match check_deref_offset_bounds casted_es casted_offs with - | Some true, _ - | _, Some true -> - report_must_offset_oob "accessed through" d_exp ptr_exp casted_es casted_offs; - | Some false, Some false -> - Checks.safe Checks.Category.InvalidMemoryAccess - | _ -> - report_may_offset_oob "accessed through" d_exp ptr_exp casted_es casted_offs; - end + check_offset_against_object_size "accessed through" check_deref_offset_bounds man ptr_exp es offs_intdom end let check_ptr_value_access man ptr_exp addr_offs = @@ -267,17 +267,7 @@ struct | `Bot, _ -> report_unknown_object_size "pointed to by" d_exp ptr_exp "bot" | `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 *) - begin match check_ptr_offset_bounds casted_ps casted_ao with - | Some true, _ - | _, Some true -> - report_must_offset_oob "pointed to by" d_exp ptr_exp casted_ps casted_ao - | Some false, Some false -> - Checks.safe Checks.Category.InvalidMemoryAccess - | _ -> - report_may_offset_oob "pointed to by" d_exp ptr_exp casted_ps casted_ao - end + check_offset_against_object_size "pointed to by" check_ptr_offset_bounds man ptr_exp ps ao end | _ -> M.error "Expression %a is not a pointer" d_exp ptr_exp 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 0046fa7963..0458eaa476 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 object accessed through 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 size of object accessed through ptr + r (5) (in bytes) with offset (⊤) (in bytes). Memory out-of-bounds access might occur (01-oob-heap-simple.c:11:5-11:21) + [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of object accessed through ptr + r (5) (in bytes) with offset (⊤) (in bytes). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 8 dead: 0 @@ -12,8 +12,8 @@ $ diff default-output.txt full-output.txt 2,3c2,3 < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of object accessed through 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 size of object accessed through ptr + r (5) (in bytes) with offset (⊤) (in bytes). Memory out-of-bounds access might occur (01-oob-heap-simple.c:11:5-11:21) + < [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of object accessed through ptr + r (5) (in bytes) with offset (⊤) (in bytes). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) --- > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of object accessed through 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 size of object accessed through ptr + r ((5,[5,5])) (in bytes) with offset ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])) (in bytes). Memory out-of-bounds access might occur (01-oob-heap-simple.c:11:5-11:21) + > [Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of object accessed through ptr + r ((5,[5,5])) (in bytes) with offset ((Unknown int([-63,63]),[-9223372036854775808,9223372036854775807])) (in bytes). Memory out-of-bounds access may occur (01-oob-heap-simple.c:11:5-11:21) [1] From 29da285d7faa1a82d4a3552a69bbf0a0a2a41e87 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 8 May 2026 13:25:43 +0300 Subject: [PATCH 14/15] Move and simplify `ptr_only_has_str_addr` Co-authored-by: Simmo Saan --- src/analyses/memOutOfBounds.ml | 17 +++++------------ 1 file changed, 5 insertions(+), 12 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 146f4323e8..750ea9a9e3 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -175,16 +175,6 @@ struct end else Checks.safe Checks.Category.InvalidMemoryAccess - let ptr_only_has_str_addr man ptr = - match man.ask (Queries.EvalValue ptr) with - | a when not (Queries.VD.is_top a) -> - begin match a with - | Address a -> ValueDomain.AD.for_all (fun addr -> match addr with | StrPtr _ -> true | _ -> false) a - | _ -> false - end - (* Intuition: if ptr evaluates to top, it could all sorts of things and not only string addresses *) - | _ -> false - let get_addr_offs_from_ad man ptr a = match a with | a when not (VDQ.AD.is_top a) -> @@ -272,16 +262,19 @@ struct | _ -> M.error "Expression %a is not a pointer" d_exp ptr_exp let check_access_for_oob man exp ad = + let ptr_only_has_str_addr ptr = + ValueDomain.AD.for_all (function StrPtr _ -> true | _ -> false) (man.ask (Queries.MayPointTo ptr)) + in let exp = Cil.stripCasts exp in match exp with (* Actual dereference/access through a pointer. *) - | AddrOf (Mem e, o) when not (ptr_only_has_str_addr man e) -> + | AddrOf (Mem e, o) when not (ptr_only_has_str_addr e) -> check_ptr_deref_access man e o (* Taking the address of something is not an access itself. *) | AddrOf _ -> () (* Pointer arithmetic / pointer value access. *) - | _ when isPointerType (typeOf exp) && not (ptr_only_has_str_addr man exp) -> + | _ when isPointerType (typeOf exp) && not (ptr_only_has_str_addr exp) -> check_ptr_value_access man exp (get_addr_offs_from_ad man exp ad) | _ -> () From bf7daffd9e9977db9c26c9a92d4e67a97c37cb07 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 8 May 2026 13:30:01 +0300 Subject: [PATCH 15/15] Simplify `may_contain_unknown_addr` --- src/analyses/memOutOfBounds.ml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 750ea9a9e3..8dd6fb5aa2 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -161,14 +161,7 @@ struct let check_unknown_addr_deref man ptr = let may_contain_unknown_addr = - match man.ask (Queries.EvalValue ptr) with - | a when not (Queries.VD.is_top a) -> - begin match a with - | Address a -> ValueDomain.AD.may_be_unknown a - | _ -> false - end - (* Intuition: if ptr evaluates to top, it could potentially evaluate to the unknown address *) - | _ -> true + ValueDomain.AD.may_be_unknown (man.ask (Queries.MayPointTo ptr)) in if may_contain_unknown_addr then begin report_oob "Pointer %a contains an unknown address. Invalid dereference may occur" d_exp ptr