From c4bf1ccbeb23c2f8248fa755a8f4949efbe328e9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 26 Sep 2023 15:16:51 +0300 Subject: [PATCH 1/7] Add some library functions for zstd --- src/analyses/libraryFunctions.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 137a3103a5..9ee9dc8c9d 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -209,6 +209,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strnlen", unknown [drop "s" [r]; drop "maxlen" []]); ("chmod", unknown [drop "pathname" [r]; drop "mode" []]); ("fchmod", unknown [drop "fd" []; drop "mode" []]); + ("chown", unknown [drop "pathname" [r]; drop "owner" []; drop "group" []]); ("fchown", unknown [drop "fd" []; drop "owner" []; drop "group" []]); ("lchown", unknown [drop "pathname" [r]; drop "owner" []; drop "group" []]); ("clock_gettime", unknown [drop "clockid" []; drop "tp" [w]]); @@ -245,6 +246,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("timer_settime", unknown [drop "timerid" []; drop "flags" []; drop "new_value" [r_deep]; drop "old_value" [w_deep]]); ("timer_gettime", unknown [drop "timerid" []; drop "curr_value" [w_deep]]); ("timer_getoverrun", unknown [drop "timerid" []]); + ("fstat", unknown [drop "fd" []; drop "statbuf" [w]]); ("lstat", unknown [drop "pathname" [r]; drop "statbuf" [w]]); ("getpwnam", unknown [drop "name" [r]]); ("chdir", unknown [drop "path" [r]]); @@ -833,12 +835,23 @@ let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("inflateInit2", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []]); ("inflateInit2_", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []; drop "version" [r]; drop "stream_size" []]); ("inflateEnd", unknown [drop "strm" [f_deep]]); + ("deflate", unknown [drop "strm" [r_deep; w_deep]; drop "flush" []]); + ("deflateInit2", unknown [drop "strm" [r_deep; w_deep]; drop "level" []; drop "method" []; drop "windowBits" []; drop "memLevel" []; drop "strategy" []]); + ("deflateInit2_", unknown [drop "strm" [r_deep; w_deep]; drop "level" []; drop "method" []; drop "windowBits" []; drop "memLevel" []; drop "strategy" []; drop "version" [r]; drop "stream_size" []]); + ("deflateEnd", unknown [drop "strm" [f_deep]]); + ("zlibVersion", unknown []); ] let liblzma_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("lzma_code", unknown [drop "strm" [r_deep; w_deep]; drop "action" []]); ("lzma_auto_decoder", unknown [drop "strm" [r_deep; w_deep]; drop "memlimit" []; drop "flags" []]); + ("lzma_alone_decoder", unknown [drop "strm" [r_deep; w_deep]; drop "memlimit" []]); + ("lzma_stream_decoder", unknown [drop "strm" [r_deep; w_deep]; drop "memlimit" []; drop "flags" []]); + ("lzma_alone_encoder", unknown [drop "strm" [r_deep; w_deep]; drop "options" [r_deep]]); + ("lzma_easy_encoder", unknown [drop "strm" [r_deep; w_deep]; drop "preset" []; drop "check" []]); ("lzma_end", unknown [drop "strm" [r_deep; w_deep; f_deep]]); + ("lzma_version_string", unknown []); + ("lzma_lzma_preset", unknown [drop "options" [w_deep]; drop "preset" []]); ] let libraries = Hashtbl.of_list [ From 0776dbe5423c38aa74acfbdc1cdd88c148e2051d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 5 Oct 2023 12:02:14 +0300 Subject: [PATCH 2/7] Add __builtin_clzll to library functions --- src/analyses/libraryFunctions.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 9ee9dc8c9d..7695844dd0 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -374,6 +374,8 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin_ctzl", unknown [drop "x" []]); ("__builtin_ctzll", unknown [drop "x" []]); ("__builtin_clz", unknown [drop "x" []]); + ("__builtin_clzl", unknown [drop "x" []]); + ("__builtin_clzll", unknown [drop "x" []]); ("__builtin_object_size", unknown [drop "ptr" [r]; drop' []]); ("__builtin_prefetch", unknown (drop "addr" [] :: VarArgs (drop' []))); ("__builtin_expect", special [__ "exp" []; drop' []] @@ fun exp -> Identity exp); (* Identity, because just compiler optimization annotation. *) From c6f7180617d67f5e00845cfc80b2a6f7e78e9dda Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 9 Oct 2023 15:37:37 +0300 Subject: [PATCH 3/7] Add more duplicate library function checks --- src/analyses/libraryFunctions.ml | 40 ++++++++++++++++++++++++++++---- 1 file changed, 36 insertions(+), 4 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 1c509e7660..f30f40cbdf 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -994,11 +994,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 () = @@ -1201,7 +1233,7 @@ let invalidate_actions = [ ] let () = List.iter (fun (x, _) -> - if Hashtbl.exists (fun _ b -> List.mem_assoc x b) libraries then + if Hashtbl.mem all_library_descs x then failwith ("You have added a function to invalidate_actions that already exists in libraries. Please undo this for function: " ^ x); ) invalidate_actions From 44e01f563bc6cf74399af4e4251456c54325a34e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 9 Oct 2023 15:43:04 +0300 Subject: [PATCH 4/7] Remove duplicate library functions --- src/analyses/libraryFunctions.ml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index f30f40cbdf..0360617171 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -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" []]); @@ -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" []]); @@ -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" []]); @@ -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]]); From 599bbb5ed55a7a8ab509271193e4c2df05dadbbe Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 9 Oct 2023 15:53:34 +0300 Subject: [PATCH 5/7] Refactor invalidate actions table --- src/analyses/libraryFunctions.ml | 38 +++++++++----------------------- 1 file changed, 11 insertions(+), 27 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 0360617171..aa279ff324 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -1228,32 +1228,16 @@ let invalidate_actions = [ "__goblint_assume_join", readsAll; ] -let () = List.iter (fun (x, _) -> - if Hashtbl.mem all_library_descs x 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"]) @@ -1297,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 -> From 5aa420441c248a582b4484df170666b75fee5377 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 9 Oct 2023 16:20:50 +0200 Subject: [PATCH 6/7] Some ~15 more library functions (#1203) * More socket * `recvfrom` * `writev` / `readv` * `popen` * `stat` / `fstat` * `statfs` * `mount` / `umount` * Fix `select` Co-authored-by: Simmo Saan * Rm duplicate `fstat` Co-authored-by: Simmo Saan * Rm duplicates --------- Co-authored-by: Simmo Saan --- src/analyses/libraryFunctions.ml | 33 ++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 1c509e7660..c4d1acf76a 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -285,7 +285,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("read", unknown [drop "fd" []; drop "buf" [w]; drop "count" []]); ("write", unknown [drop "fd" []; drop "buf" [r]; drop "count" []]); ("recv", unknown [drop "sockfd" []; drop "buf" [w]; drop "len" []; drop "flags" []]); + ("recvfrom", unknown [drop "sockfd" []; drop "buf" [w]; drop "len" []; drop "flags" []; drop "src_addr" [w_deep]; drop "addrlen" [r; w]]); ("send", unknown [drop "sockfd" []; drop "buf" [r]; drop "len" []; drop "flags" []]); + ("sendto", unknown [drop "sockfd" []; drop "buf" [r]; drop "len" []; drop "flags" []; drop "dest_addr" [r_deep]; drop "addrlen" []]); ("strdup", unknown [drop "s" [r]]); ("strndup", unknown [drop "s" [r]; drop "n" []]); ("syscall", unknown (drop "number" [] :: VarArgs (drop' [r; w]))); @@ -373,6 +375,18 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("uname", unknown [drop "buf" [w_deep]]); ("strcasecmp", unknown [drop "s1" [r]; drop "s2" [r]]); ("strncasecmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]); + ("connect", unknown [drop "sockfd" []; drop "sockaddr" [r_deep]; drop "addrlen" []]); + ("bind", unknown [drop "sockfd" []; drop "sockaddr" [r_deep]; drop "addrlen" []]); + ("listen", unknown [drop "sockfd" []; drop "backlog" []]); + ("select", unknown [drop "nfds" []; drop "readfds" [r; w]; drop "writefds" [r; w]; drop "exceptfds" [r; w]; drop "timeout" [r; w]]); + ("accept", unknown [drop "sockfd" []; drop "addr" [w_deep]; drop "addrlen" [r; w]]); + ("close", unknown [drop "fd" []]); + ("writev", unknown [drop "fd" []; drop "iov" [r_deep]; drop "iovcnt" []]); + ("readv", unknown [drop "fd" []; drop "iov" [w_deep]; drop "iovcnt" []]); + ("unlink", unknown [drop "pathname" [r]]); + ("popen", unknown [drop "command" [r]; drop "type" [r]]); + ("stat", unknown [drop "pathname" [r]; drop "statbuf" [w]]); + ("statfs", unknown [drop "path" [r]; drop "buf" [w]]); ] (** Pthread functions. *) @@ -588,6 +602,9 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("fts_open", unknown [drop "path_argv" [r_deep]; drop "options" []; drop "compar" [s]]); (* TODO: use Call instead of Spawn *) ("fts_read", unknown [drop "ftsp" [r_deep; w_deep]]); ("fts_close", unknown [drop "ftsp" [f_deep]]); + ("mount", unknown [drop "source" [r]; drop "target" [r]; drop "filesystemtype" [r]; drop "mountflags" []; drop "data" [r]]); + ("umount", unknown [drop "target" [r]]); + ("umount2", unknown [drop "target" [r]; drop "flags" []]); ] let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType))) @@ -1100,7 +1117,6 @@ open Invalidate * We assume that no known functions that are reachable are executed/spawned. For that we use ThreadCreate above. *) (* WTF: why are argument numbers 1-indexed (in partition)? *) let invalidate_actions = [ - "connect", readsAll; (*safe*) "__printf_chk", readsAll;(*safe*) "printk", readsAll;(*safe*) "__mutex_init", readsAll;(*safe*) @@ -1118,23 +1134,17 @@ let invalidate_actions = [ "atoi__extinline", readsAll;(*safe*) "_IO_getc", writesAll;(*unsafe*) "pipe", writesAll;(*unsafe*) - "close", writesAll;(*unsafe*) "strerror_r", writesAll;(*unsafe*) "raise", writesAll;(*unsafe*) "_strlen", readsAll;(*safe*) "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) - "umount2", readsAll;(*safe*) "waitpid", readsAll;(*safe*) - "statfs", writes [1;3;4];(*keep [1;3;4]*) - "mount", readsAll;(*safe*) "__open_alias", readsAll;(*safe*) "__open_2", readsAll;(*safe*) "ioctl", writesAll;(*unsafe*) "fstat__extinline", writesAll;(*unsafe*) - "umount", readsAll;(*safe*) "scandir", writes [1;3;4];(*keep [1;3;4]*) - "unlink", readsAll;(*safe*) "sigwait", writesAllButFirst 1 readsAll;(*drop 1*) "bindtextdomain", readsAll;(*safe*) "textdomain", readsAll;(*safe*) @@ -1149,11 +1159,9 @@ let invalidate_actions = [ "svctcp_create", readsAll;(*safe*) "clntudp_bufcreate", writesAll;(*unsafe*) "authunix_create_default", readsAll;(*safe*) - "writev", readsAll;(*safe*) "clnt_broadcast", writesAll;(*unsafe*) "clnt_sperrno", readsAll;(*safe*) "pmap_unset", writesAll;(*unsafe*) - "bind", readsAll;(*safe*) "svcudp_create", readsAll;(*safe*) "svc_register", writesAll;(*unsafe*) "svc_run", writesAll;(*unsafe*) @@ -1162,18 +1170,13 @@ let invalidate_actions = [ "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) "__error", readsAll; (*safe*) "__maskrune", writesAll; (*unsafe*) - "listen", readsAll; (*safe*) - "select", writes [1;5]; (*keep [1;5]*) - "accept", writesAll; (*keep [1]*) "times", writesAll; (*unsafe*) "timespec_get", writes [1]; "__tolower", readsAll; (*safe*) "signal", writesAll; (*unsafe*) - "popen", readsAll; (*safe*) "BF_cfb64_encrypt", writes [1;3;4;5]; (*keep [1;3;4,5]*) "BZ2_bzBuffToBuffDecompress", writes [3;4]; (*keep [3;4]*) "uncompress", writes [3;4]; (*keep [3;4]*) - "stat", writes [2]; (*keep [1]*) "__xstat", writes [3]; (*keep [1]*) "__lxstat", writes [3]; (*keep [1]*) "remove", readsAll; @@ -1181,8 +1184,6 @@ let invalidate_actions = [ "compress2", writes [3]; (*keep [3]*) "__toupper", readsAll; (*safe*) "BF_set_key", writes [3]; (*keep [3]*) - "sendto", writes [2;4]; (*keep [2;4]*) - "recvfrom", writes [4;5]; (*keep [4;5]*) "PL_NewHashTable", readsAll; (*safe*) "assert_failed", readsAll; (*safe*) "munmap", readsAll;(*safe*) From b96c010fb5c86b5b238b91668feeb0156f2cba8c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 10 Oct 2023 17:36:58 +0300 Subject: [PATCH 7/7] Fix memOutOfBounds indentation --- src/analyses/memOutOfBounds.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 7015e6f143..c715a1d2e7 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -397,8 +397,7 @@ struct match desc.special arglist with | Memset { dest; ch; count; } -> check_count ctx f.vname dest count; | Memcpy { dest; src; n = count; } -> check_count ctx f.vname dest count; - | _ -> (); - ctx.local + | _ -> ctx.local let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = List.iter (fun arg -> check_exp_for_oob_access ctx arg) args;