Skip to content

Improve memOutOfBounds precision for points-to sets which mix allocs with others #2030

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
sim642 merged 3 commits into from
May 29, 2026
+107 −108
Merged

Improve memOutOfBounds precision for points-to sets which mix allocs with others #2030

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8a5aed1
Add test 74-invalid_deref/38-oob-alloc-array-mix
sim642 May 13, 2026
8323565
Improve memOutOfBounds precision for points-to sets which mix allocs …
sim642 May 13, 2026
9b1af19
Add TODOs about BlobSize and EvalLength queries
sim642 May 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
94 changes: 42 additions & 52 deletions src/analyses/base.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1532,7 +1532,7 @@ struct
| _ -> MutexAttrDomain.top ()
end
| Q.EvalLength e -> begin
match eval_rv_address ~man man.local e with
match eval_rv_address ~man man.local e with (* TODO: why doesn't this use length from ArrayDomain? *)
| Address a ->
let slen = Seq.map String.length (List.to_seq (AD.to_string a)) in
let lenOf t =
Expand Down Expand Up @@ -2345,64 +2345,54 @@ struct
M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Pointer %a in function %s doesn't evaluate to a valid address. Invalid memory deallocation may occur" d_exp ptr special_fn.vname;
Checks.warn Checks.Category.InvalidMemoryAccess "Pointer %a in function %s doesn't evaluate to a valid address. Invalid memory deallocation may occur" d_exp ptr special_fn.vname

let points_to_heap_only man ptr =
match man.ask (Queries.MayPointTo ptr) with
| a when not (Queries.AD.is_top a)->
Queries.AD.for_all (function
| Addr (v, _) -> man.ask (Queries.IsHeapVar v)
| _ -> false
) a
| _ -> false

let get_size_of_ptr_target man ptr = (* TODO: deduplicate with memOutOfBounds *)
let get_size_of_ptr_target man ptr = (* TODO: deduplicate with memOutOfBounds (this uses IsHeapVar) *)
let intdom_of_int x =
ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x)
in
let size_of_type_in_bytes typ =
intdom_of_int (Cilfacade.bytesSizeOf typ)
in
if points_to_heap_only man ptr then
(* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *)
man.ask (Queries.BlobSize {exp = ptr; base_address = true})
else
match man.ask (Queries.MayPointTo ptr) with
| a when not (Queries.AD.is_top a) ->
let pts_list = Queries.AD.elements a in
let pts_elems_to_sizes (addr: Queries.AD.elt) =
begin match addr with
| Addr (v, _) ->
begin match Cil.unrollType v.vtype with
| TArray (item_typ, _, _) ->
let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
begin match man.ask (Queries.EvalLength ptr) with
| `Lifted arr_len ->
let arr_len_casted = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) arr_len in (* TODO: proper castkind *)
begin
try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted)
with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
end
| `Bot -> `Bot
| `Top -> `Top
end
| _ ->
let type_size_in_bytes = size_of_type_in_bytes v.vtype in
`Lifted type_size_in_bytes
end
| _ -> `Top
end
in
(* Map each points-to-set element to its size *)
let pts_sizes = List.map pts_elems_to_sizes pts_list in
(* Take the smallest of all sizes that ptr's contents may have *)
begin match pts_sizes with
| [] -> `Bot
| [x] -> x
| x::xs -> List.fold_left ValueDomainQueries.ID.join x xs
match man.ask (Queries.MayPointTo ptr) with
| a when not (Queries.AD.is_top a) ->
let pts_list = Queries.AD.elements a in
let pts_elems_to_sizes (addr: Queries.AD.elt) =
begin match addr with
| Addr (v, _) when man.ask (Queries.IsHeapVar v) ->
(* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *)
man.ask (Queries.BlobSize {exp = ptr; base_address = true}) (* TODO: only query for addr/v *)
| Addr (v, _) ->
begin match Cil.unrollType v.vtype with
| TArray (item_typ, _, _) ->
let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
begin match man.ask (Queries.EvalLength ptr) with (* TODO: only query for addr/v *)
| `Lifted arr_len ->
let arr_len_casted = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) arr_len in (* TODO: proper castkind *)
begin
try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted)
with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
end
| `Bot -> `Bot
| `Top -> `Top
end
| _ ->
let type_size_in_bytes = size_of_type_in_bytes v.vtype in
`Lifted type_size_in_bytes
end
| _ -> `Top
end
| _ ->
(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)
in
(* Map each points-to-set element to its size *)
let pts_sizes = List.map pts_elems_to_sizes pts_list in
(* Take the smallest of all sizes that ptr's contents may have *)
begin match pts_sizes with
| [] -> `Bot
| [x] -> x
| x::xs -> List.fold_left ValueDomainQueries.ID.join x xs
end
| _ ->
(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)

let special man (lv:lval option) (f: varinfo) (args: exp list) =
let invalidate_ret_lv st =
Expand Down
102 changes: 46 additions & 56 deletions src/analyses/memOutOfBounds.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,64 +79,54 @@ struct
in
host_contains_a_ptr host || offset_contains_a_ptr offset

let points_to_alloc_only man ptr =
let get_size_of_ptr_target man ptr = (* TODO: deduplicate with base (this uses IsAllocVar) *)
match man.ask (Queries.MayPointTo ptr) with
| a when not (Queries.AD.is_top a)->
Queries.AD.for_all (function
| Addr (v, o) -> man.ask (Queries.IsAllocVar v)
| _ -> false
) a
| _ -> false

let get_size_of_ptr_target man ptr = (* TODO: deduplicate with base *)
if points_to_alloc_only man ptr then
(* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *)
man.ask (Queries.BlobSize {exp = ptr; base_address = true})
else
match man.ask (Queries.MayPointTo ptr) with
| a when not (Queries.AD.is_top a) ->
let pts_list = Queries.AD.elements a in
let pts_elems_to_sizes (addr: Queries.AD.elt) =
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
);
begin match Cil.unrollType v.vtype with
| TArray (item_typ, _, _) ->
let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
begin match man.ask (Queries.EvalLength ptr) with
| `Lifted arr_len ->
let arr_len_casted = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) arr_len in (* TODO: proper castkind *)
begin
try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted)
with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
end
| `Bot -> `Bot
| `Top -> `Top
end
| _ ->
let type_size_in_bytes = size_of_type_in_bytes v.vtype in
`Lifted type_size_in_bytes
end
| _ -> `Top
end
in
(* Map each points-to-set element to its size *)
let pts_sizes = List.map pts_elems_to_sizes pts_list in
(* Take the smallest of all sizes that ptr's contents may have *)
begin match pts_sizes with
| [] -> `Bot
| [x] -> x
| x::xs -> List.fold_left VDQ.ID.join x xs
| a when not (Queries.AD.is_top a) ->
let pts_list = Queries.AD.elements a in
let pts_elems_to_sizes (addr: Queries.AD.elt) =
begin match addr with
| Addr (v, _) when man.ask (Queries.IsAllocVar v) ->
(* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *)
man.ask (Queries.BlobSize {exp = ptr; base_address = true}) (* TODO: only query for addr/v *)
| 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
);
begin match Cil.unrollType v.vtype with
| TArray (item_typ, _, _) ->
let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
begin match man.ask (Queries.EvalLength ptr) with (* TODO: only query for addr/v *)
| `Lifted arr_len ->
let arr_len_casted = ID.cast_to ~kind:Internal (Cilfacade.ptrdiff_ikind ()) arr_len in (* TODO: proper castkind *)
begin
try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted)
with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
end
| `Bot -> `Bot
| `Top -> `Top
end
| _ ->
let type_size_in_bytes = size_of_type_in_bytes v.vtype in
`Lifted type_size_in_bytes
end
| _ -> `Top
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)
in
(* Map each points-to-set element to its size *)
let pts_sizes = List.map pts_elems_to_sizes pts_list in
(* Take the smallest of all sizes that ptr's contents may have *)
begin match pts_sizes with
| [] -> `Bot
| [x] -> x
| 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)

let get_ptr_deref_type ptr_typ =
match Cil.unrollType ptr_typ with
Expand Down
19 changes: 19 additions & 0 deletions tests/regression/74-invalid_deref/38-oob-alloc-array-mix.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] memOutOfBounds --enable ana.int.interval
#include <stdlib.h>
#include <stdio.h>

extern _Bool __VERIFIER_nondet_bool();

int main(void) {
int foo[4];
int *bar = malloc(4 * sizeof(int));

int *p;
if (__VERIFIER_nondet_bool())
p = &foo[3];
else
p = &bar[3];

*p = 42; // NOWARN
return 0;
}
Loading