Skip to content

Check duplicate library functions #1213

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
merged 3 commits into from
Oct 10, 2023
Merged

Check duplicate library functions #1213

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c6f7180
Add more duplicate library function checks
sim642 Oct 9, 2023
44e01f5
Remove duplicate library functions
sim642 Oct 9, 2023
599bbb5
Refactor invalidate actions table
sim642 Oct 9, 2023
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
80 changes: 46 additions & 34 deletions src/analyses/libraryFunctions.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -244,7 +244,6 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("symlink" , unknown [drop "oldpath" [r]; drop "newpath" [r];]);
("ftruncate", unknown [drop "fd" []; drop "length" []]);
("mkfifo", unknown [drop "pathname" [r]; drop "mode" []]);
("ntohs", unknown [drop "netshort" []]);
("alarm", unknown [drop "seconds" []]);
("pwrite", unknown [drop "fd" []; drop "buf" [r]; drop "count" []; drop "offset" []]);
("hstrerror", unknown [drop "err" []]);
Expand Down Expand Up @@ -275,7 +274,6 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("lstat", unknown [drop "pathname" [r]; drop "statbuf" [w]]);
("fstat", unknown [drop "fd" []; drop "buf" [w]]);
("fstatat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "buf" [w]; drop "flags" []]);
("getpwnam", unknown [drop "name" [r]]);
("chdir", unknown [drop "path" [r]]);
("closedir", unknown [drop "dirp" [r]]);
("mkdir", unknown [drop "pathname" [r]; drop "mode" []]);
Expand All @@ -295,7 +293,6 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("freeaddrinfo", unknown [drop "res" [f_deep]]);
("getgid", unknown []);
("pselect", unknown [drop "nfds" []; drop "readdfs" [r]; drop "writedfs" [r]; drop "exceptfds" [r]; drop "timeout" [r]; drop "sigmask" [r]]);
("strncasecmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]);
("getnameinfo", unknown [drop "addr" [r_deep]; drop "addrlen" []; drop "host" [w]; drop "hostlen" []; drop "serv" [w]; drop "servlen" []; drop "flags" []]);
("strtok_r", unknown [drop "str" [r; w]; drop "delim" [r]; drop "saveptr" [r_deep; w_deep]]); (* deep accesses through saveptr if str is NULL: https://github.com/lattera/glibc/blob/895ef79e04a953cac1493863bcae29ad85657ee1/string/strtok_r.c#L31-L40 *)
("kill", unknown [drop "pid" []; drop "sig" []]);
Expand Down Expand Up @@ -437,7 +434,6 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("pthread_attr_setschedpolicy", unknown [drop "attr" [r; w]; drop "policy" []]);
("pthread_condattr_init", unknown [drop "attr" [w]]);
("pthread_condattr_setclock", unknown [drop "attr" [w]; drop "clock_id" []]);
("pthread_mutexattr_destroy", unknown [drop "attr" [f]]);
("pthread_attr_setschedparam", unknown [drop "attr" [r; w]; drop "param" [r]]);
("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]);
("pthread_getaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [w]]);
Expand Down Expand Up @@ -994,11 +990,43 @@ let libraries = Hashtbl.of_list [
("liblzma", liblzma_descs_list);
]

let libraries =
Hashtbl.map (fun library descs_list ->
let descs_tbl = Hashtbl.create 113 in
List.iter (fun (name, desc) ->
Hashtbl.modify_opt name (function
| None -> Some desc
| Some _ -> failwith (Format.sprintf "Library function %s specified multiple times in library %s" name library)
) descs_tbl
) descs_list;
descs_tbl
) libraries

let all_library_descs: (string, LibraryDesc.t) Hashtbl.t =
Hashtbl.fold (fun _ descs_tbl acc ->
Hashtbl.merge (fun name desc1 desc2 ->
match desc1, desc2 with
| Some _, Some _ -> failwith (Format.sprintf "Library function %s specified in multiple libraries" name)
| (Some _ as desc), None
| None, (Some _ as desc) -> desc
| None, None -> assert false
) acc descs_tbl
) libraries (Hashtbl.create 0)

let activated_library_descs: (string, LibraryDesc.t) Hashtbl.t ResettableLazy.t =
let union =
Hashtbl.merge (fun _ desc1 desc2 ->
match desc1, desc2 with
| (Some _ as desc), None
| None, (Some _ as desc) -> desc
| _, _ -> assert false
)
in
ResettableLazy.from_fun (fun () ->
let activated = List.unique (GobConfig.get_string_list "lib.activated") in
let desc_list = List.concat_map (Hashtbl.find libraries) activated in
Hashtbl.of_list desc_list
GobConfig.get_string_list "lib.activated"
|> List.unique
|> List.map (Hashtbl.find libraries)
|> List.fold_left union (Hashtbl.create 0)
)

let reset_lazy () =
Expand Down Expand Up @@ -1200,32 +1228,16 @@ let invalidate_actions = [
"__goblint_assume_join", readsAll;
]

let () = List.iter (fun (x, _) ->
if Hashtbl.exists (fun _ b -> List.mem_assoc x b) libraries then
failwith ("You have added a function to invalidate_actions that already exists in libraries. Please undo this for function: " ^ x);
) invalidate_actions

(* used by get_invalidate_action to make sure
* that hash of invalidates is built only once
*
* Hashtable from strings to functions of type (exp list -> exp list)
*)
let processed_table = ref None

let get_invalidate_action name =
let tbl = match !processed_table with
| None -> begin
let hash = Hashtbl.create 113 in
let f (k, v) = Hashtbl.add hash k v in
List.iter f invalidate_actions;
processed_table := (Some hash);
hash
end
| Some x -> x
in
if Hashtbl.mem tbl name
then Some (Hashtbl.find tbl name)
else None
let invalidate_actions =
let tbl = Hashtbl.create 113 in
List.iter (fun (name, old_accesses) ->
Hashtbl.modify_opt name (function
| None when Hashtbl.mem all_library_descs name -> failwith (Format.sprintf "Library function %s specified both in libraries and invalidate actions" name)
| None -> Some old_accesses
| Some _ -> failwith (Format.sprintf "Library function %s specified multiple times in invalidate actions" name)
) tbl
) invalidate_actions;
tbl


let lib_funs = ref (Set.String.of_list ["__raw_read_unlock"; "__raw_write_unlock"; "spin_trylock"])
Expand Down Expand Up @@ -1269,7 +1281,7 @@ let find f =
match Hashtbl.find_option (ResettableLazy.force activated_library_descs) name with
| Some desc -> desc
| None ->
match get_invalidate_action name with
match Hashtbl.find_option invalidate_actions name with
| Some old_accesses ->
LibraryDesc.of_old old_accesses
| None ->
Expand Down