From c1149dfa90c0284431e354023dc370f7d79f3e9c Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 7 May 2026 15:21:26 +0300 Subject: [PATCH 1/4] 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 2/4] 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 3/4] 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 4/4] 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 =