Skip to content

Commit f8ad4ab

Browse files
committed
Extend memset zeroing support bzero and friends (PR #696)
Should fix 01-cpa/24-library_functions on MacOS CI.
1 parent 217d62c commit f8ad4ab

File tree

3 files changed

+18
-1
lines changed

3 files changed

+18
-1
lines changed

src/analyses/accessAnalysis.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -182,6 +182,7 @@ struct
182182
let reach =
183183
match f.vname with
184184
| "memset" | "__builtin_memset" | "__builtin___memset_chk" -> false
185+
| "bzero" | "__builtin_bzero" | "explicit_bzero" | "__explicit_bzero_chk" -> false
185186
| "__builtin_object_size" -> false
186187
| _ -> true
187188
in

src/analyses/base.ml

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2134,6 +2134,20 @@ struct
21342134
set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
21352135
| _, _ -> failwith "strange memset arguments"
21362136
end
2137+
| `Unknown (("bzero" | "__builtin_bzero" | "explicit_bzero" | "__explicit_bzero_chk") as name) ->
2138+
(* TODO: share something with memset special case? *)
2139+
begin match name, args with
2140+
| "__explicit_bzero_chk", [dest; count; _ (* dest_size *)]
2141+
| ("bzero" | "__builtin_bzero" | "explicit_bzero"), [dest; count] ->
2142+
(* TODO: check count *)
2143+
let dest_lval = mkMem ~addr:(Cil.stripCasts dest) ~off:NoOffset in
2144+
let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st dest_lval in
2145+
(* let dest_typ = Cilfacade.typeOfLval dest_lval in *)
2146+
let dest_typ = AD.get_type dest_a in (* TODO: what is the right way? *)
2147+
let value = VD.zero_init_value dest_typ in
2148+
set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
2149+
| _, _ -> failwith "strange bzero arguments"
2150+
end
21372151
| `Unknown "F59" (* strcpy *)
21382152
| `Unknown "F60" (* strncpy *)
21392153
| `Unknown "F63" (* memcpy *)

src/analyses/libraryFunctions.ml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -185,6 +185,9 @@ let invalidate_actions = [
185185
"__builtin_ctzll", readsAll;
186186
"__builtin_clz", readsAll;
187187
"bzero", writes [1]; (*keep 1*)
188+
"__builtin_bzero", writes [1]; (*keep [1]*)
189+
"explicit_bzero", writes [1];
190+
"__explicit_bzero_chk", writes [1];
188191
"connect", readsAll; (*safe*)
189192
"fclose", readsAll; (*safe*)
190193
"fflush", writesAll; (*unsafe*)
@@ -398,7 +401,6 @@ let invalidate_actions = [
398401
"__maskrune", writesAll; (*unsafe*)
399402
"inet_addr", readsAll; (*safe*)
400403
"gethostbyname", readsAll; (*safe*)
401-
"__builtin_bzero", writes [1]; (*keep [1]*)
402404
"setsockopt", readsAll; (*safe*)
403405
"listen", readsAll; (*safe*)
404406
"getsockname", writes [1;3]; (*keep [1;3]*)

0 commit comments

Comments
 (0)