From c4bf1ccbeb23c2f8248fa755a8f4949efbe328e9 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 26 Sep 2023 15:16:51 +0300
Subject: [PATCH 01/18] 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 <simmo.saan@gmail.com>
Date: Thu, 5 Oct 2023 12:02:14 +0300
Subject: [PATCH 02/18] 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 8468a5a676fae48a82e0284ea13170d0cefa935c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 12:12:58 +0300
Subject: [PATCH 03/18] Fix too broad try block in BaseInvariant

Caused Invalid_argument("Cilfacade.get_fkind: non-float type int ") before,
even though integer case is checked first,
but something else in it raises.
---
 src/analyses/baseInvariant.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 70c6ed9101..72e00efbb1 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -805,15 +805,15 @@ struct
         | BinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _, _) -> true
         | _ -> false
       in
-      try
-        let ik = Cilfacade.get_ikind_exp exp in
+      match Cilfacade.get_ikind_exp exp with
+      | ik ->
         let itv = if not tv || is_cmp exp then (* false is 0, but true can be anything that is not 0, except for comparisons which yield 1 *)
             ID.of_bool ik tv (* this will give 1 for true which is only ok for comparisons *)
           else
             ID.of_excl_list ik [BI.zero] (* Lvals, Casts, arithmetic operations etc. should work with true = non_zero *)
         in
         inv_exp (Int itv) exp st
-      with Invalid_argument _ ->
+      | exception Invalid_argument _ ->
         let fk = Cilfacade.get_fkind_exp exp in
         let ftv = if not tv then (* false is 0, but true can be anything that is not 0, except for comparisons which yield 1 *)
             FD.of_const fk 0.

From c6f7180617d67f5e00845cfc80b2a6f7e78e9dda Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 15:37:37 +0300
Subject: [PATCH 04/18] 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 <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 15:43:04 +0300
Subject: [PATCH 05/18] 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 <simmo.saan@gmail.com>
Date: Mon, 9 Oct 2023 15:53:34 +0300
Subject: [PATCH 06/18] 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 <michael.schwarz93@gmail.com>
Date: Mon, 9 Oct 2023 16:20:50 +0200
Subject: [PATCH 07/18] Some ~15 more library functions (#1203)

* More socket

* `recvfrom`

* `writev` / `readv`

* `popen`

* `stat` / `fstat`

* `statfs`

* `mount` / `umount`

* Fix `select`

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>

* Rm duplicate `fstat`

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>

* Rm duplicates

---------

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
---
 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 <simmo.saan@gmail.com>
Date: Tue, 10 Oct 2023 17:36:58 +0300
Subject: [PATCH 08/18] 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;

From 5cc481148d4e079327e6f395c02e28e99cdaa414 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 10 Oct 2023 17:47:36 +0300
Subject: [PATCH 09/18] Fix library function duplicate check indentation (PR
 #1213)

---
 src/analyses/libraryFunctions.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index dd9360d7b7..0f9c34f957 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -1047,11 +1047,11 @@ let all_library_descs: (string, LibraryDesc.t) Hashtbl.t =
 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
-    )
+        match desc1, desc2 with
+        | (Some _ as desc), None
+        | None, (Some _ as desc) -> desc
+        | _, _ -> assert false
+      )
   in
   ResettableLazy.from_fun (fun () ->
       GobConfig.get_string_list "lib.activated"

From 7ddd47167395781152fe85efa66f57ca74caa477 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 11 Oct 2023 14:12:21 +0300
Subject: [PATCH 10/18] Improve MCP.D pretty

---
 src/analyses/mCPRegistry.ml | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml
index d1311e0427..8560e5122d 100644
--- a/src/analyses/mCPRegistry.ml
+++ b/src/analyses/mCPRegistry.ml
@@ -149,20 +149,21 @@ struct
   let unop_map f x =
     List.rev @@ unop_fold (fun a n s d -> (n, f s d) :: a) [] x
 
-  let pretty () x =
-    let f a n (module S : Printable.S) x = Pretty.dprintf "%s:%a" (S.name ()) S.pretty (obj x) :: a in
-    let xs = unop_fold f [] x in
-    match xs with
-    | [] -> text "[]"
-    | x :: [] -> x
-    | x :: y ->
-      let rest  = List.fold_left (fun p n->p ++ text "," ++ break ++ n) nil y in
-      text "[" ++ align ++ x ++ rest ++ unalign ++ text "]"
+  let pretty () xs =
+    let pretty_one a n (module S: Printable.S) x =
+      let doc = Pretty.dprintf "%s:%a" (find_spec_name n) S.pretty (obj x) in
+      match a with
+      | None -> Some doc
+      | Some a -> Some (a ++ text "," ++ line ++ doc)
+    in
+    let doc = Option.default Pretty.nil (unop_fold pretty_one None xs) in
+    Pretty.dprintf "[@[%a@]]" Pretty.insert doc
 
   let show x =
     let xs = unop_fold (fun a n (module S : Printable.S) x ->
         let analysis_name = find_spec_name n in
-        (analysis_name ^ ":(" ^ S.show (obj x) ^ ")") :: a) [] x
+        (analysis_name ^ ":(" ^ S.show (obj x) ^ ")") :: a
+      ) [] x
     in
     IO.to_string (List.print ~first:"[" ~last:"]" ~sep:", " String.print) (rev xs)
 

From e2a585999e3f46642f4474aa339cd6567e429448 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 11 Oct 2023 14:12:45 +0300
Subject: [PATCH 11/18] Improve MCP.D pretty_diff

---
 src/analyses/mCPRegistry.ml | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml
index 8560e5122d..32847bb3ed 100644
--- a/src/analyses/mCPRegistry.ml
+++ b/src/analyses/mCPRegistry.ml
@@ -370,12 +370,19 @@ struct
   let top () = map (fun (n,(module S : Lattice.S)) -> (n,repr @@ S.top ())) @@ domain_list ()
   let bot () = map (fun (n,(module S : Lattice.S)) -> (n,repr @@ S.bot ())) @@ domain_list ()
 
-  let pretty_diff () (x,y) =
-    let f a n (module S : Lattice.S) x y =
-      if S.leq (obj x) (obj y) then a
-      else a ++ S.pretty_diff () (obj x, obj y) ++ text ". "
+  let pretty_diff () (xs, ys) =
+    let pretty_one a n (module S: Lattice.S) x y =
+      if S.leq (obj x) (obj y) then
+        a
+      else (
+        let doc = Pretty.dprintf "%s:%a" (find_spec_name n) S.pretty_diff (obj x, obj y) in
+        match a with
+        | None -> Some doc
+        | Some a -> Some (a ++ text "," ++ line ++ doc)
+      )
     in
-    binop_fold f nil x y
+    let doc = Option.default Pretty.nil (binop_fold pretty_one None xs ys) in
+    Pretty.dprintf "[@[%a@]]" Pretty.insert doc
 end
 
 module DomVariantLattice0 (DLSpec : DomainListLatticeSpec)

From 44f775942ce6d82736fe2150ff7af219dc0c1532 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 11 Oct 2023 14:35:44 +0300
Subject: [PATCH 12/18] Improve empty MapDomain pretty

---
 src/domains/mapDomain.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/domains/mapDomain.ml b/src/domains/mapDomain.ml
index 6c40ab9792..76dec6f0d2 100644
--- a/src/domains/mapDomain.ml
+++ b/src/domains/mapDomain.ml
@@ -68,11 +68,14 @@ end
 module Print (D: Printable.S) (R: Printable.S) (M: Bindings with type key = D.t and type value = R.t) =
 struct
   let pretty () map =
-    let pretty_bindings () = M.fold (fun k v acc ->
-        acc ++ dprintf "%a ->@?  @[%a@]\n" D.pretty k R.pretty v
+    let doc = M.fold (fun k v acc ->
+        acc ++ dprintf "%a ->@?@[%a@]\n" D.pretty k R.pretty v
       ) map nil
     in
-    dprintf "@[{\n  @[%t@]}@]" pretty_bindings
+    if doc = Pretty.nil then
+      text "{}"
+    else
+      dprintf "@[{\n  @[%a@]}@]" Pretty.insert doc
 
   let show map = GobPretty.sprint pretty map
 

From 00b7e623a7a2ddaa36a91cfd21546de33008e10e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 11 Oct 2023 15:00:49 +0300
Subject: [PATCH 13/18] Add module names to Prod and Prod3

---
 src/domains/printable.ml | 32 ++++++++++++++++++++++++++------
 1 file changed, 26 insertions(+), 6 deletions(-)

diff --git a/src/domains/printable.ml b/src/domains/printable.ml
index 1207d35db2..b0755fb730 100644
--- a/src/domains/printable.ml
+++ b/src/domains/printable.ml
@@ -366,9 +366,17 @@ struct
   let pretty () (x,y) =
     if expand_fst || expand_snd then
       text "("
+      ++ text (Base1.name ())
+      ++ text ":"
+      ++ align
       ++ (if expand_fst then Base1.pretty () x else text (Base1.show x))
+      ++ unalign
       ++ text ", "
+      ++ text (Base2.name ())
+      ++ text ":"
+      ++ align
       ++ (if expand_snd then Base2.pretty () y else text (Base2.show y))
+      ++ unalign
       ++ text ")"
     else
       text (show (x,y))
@@ -403,12 +411,24 @@ struct
     "(" ^ !first ^ ", " ^ !second ^ ", " ^ !third ^ ")"
 
   let pretty () (x,y,z) =
-    text "(" ++
-    Base1.pretty () x
-    ++ text ", " ++
-    Base2.pretty () y
-    ++ text ", " ++
-    Base3.pretty () z
+    text "("
+    ++ text (Base1.name ())
+    ++ text ":"
+    ++ align
+    ++ Base1.pretty () x
+    ++ unalign
+    ++ text ", "
+    ++ text (Base2.name ())
+    ++ text ":"
+    ++ align
+    ++ Base2.pretty () y
+    ++ unalign
+    ++ text ", "
+    ++ text (Base3.name ())
+    ++ text ":"
+    ++ align
+    ++ Base3.pretty () z
+    ++ unalign
     ++ text ")"
 
   let printXml f (x,y,z) =

From 83fef2cd47fb15d937192392684c4e39d9d136bb Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 11 Oct 2023 15:01:03 +0300
Subject: [PATCH 14/18] Add names to mutex analysis domains

---
 src/analyses/mutexAnalysis.ml | 2 ++
 src/cdomains/lockDomain.ml    | 1 +
 2 files changed, 3 insertions(+)

diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 5a61976ef5..ee050f55ca 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -30,6 +30,8 @@ struct
 
       include MapDomain.MapTop_LiftBot (ValueDomain.Addr) (Count)
 
+      let name () = "multiplicity"
+
       let increment v x =
         let current = find v x in
         if current = max_count () then
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index 4bc97b34ab..107c1c0692 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -37,6 +37,7 @@ struct
   end
 
   include SetDomain.Reverse(SetDomain.ToppedSet (Lock) (struct let topname = "All mutexes" end))
+  let name () = "lockset"
 
   let may_be_same_offset of1 of2 =
     (* Only reached with definite of2 and indefinite of1. *)

From 151ccb15068bb262a0134ec818fe7ad307615379 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 11 Oct 2023 15:01:17 +0300
Subject: [PATCH 15/18] Add names to mallocWrapper analysis domains

---
 src/analyses/wrapperFunctionAnalysis.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml
index 5c0176df48..e98597a66a 100644
--- a/src/analyses/wrapperFunctionAnalysis.ml
+++ b/src/analyses/wrapperFunctionAnalysis.ml
@@ -33,11 +33,20 @@ struct
      Introduce a function for this to keep things consistent. *)
   let node_for_ctx ctx = ctx.prev_node
 
+  module NodeFlatLattice =
+  struct
+    include NodeFlatLattice
+    let name () = "wrapper call"
+  end
+
   module UniqueCount = UniqueCount
 
   (* Map for counting function call node visits up to n (of the current thread). *)
   module UniqueCallCounter =
-    MapDomain.MapBot_LiftTop(NodeFlatLattice)(UniqueCount)
+  struct
+    include MapDomain.MapBot_LiftTop(NodeFlatLattice)(UniqueCount)
+    let name () = "unique calls"
+  end
 
   (* Increase counter for given node. If it does not exist yet, create it. *)
   let add_unique_call counter node =

From b0ce3691ec8525711f57889ddb29b44670090d76 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 11 Oct 2023 15:01:24 +0300
Subject: [PATCH 16/18] Add names to threadid analysis domains

---
 src/analyses/threadId.ml | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index 4acf88a7ef..8144aea507 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -29,11 +29,30 @@ module Spec =
 struct
   include Analyses.IdentitySpec
 
-  module N = Lattice.Flat (VNI) (struct let bot_name = "unknown node" let top_name = "unknown node" end)
+  module N =
+  struct
+    include Lattice.Flat (VNI) (struct let bot_name = "unknown node" let top_name = "unknown node" end)
+    let name () = "wrapper call"
+  end
   module TD = Thread.D
+  module Created =
+  struct
+    module Current =
+    struct
+      include TD
+      let name () = "current function"
+    end
+    module Callees =
+    struct
+      include TD
+      let name () = "callees"
+    end
+    include Lattice.Prod (Current) (Callees)
+    let name () = "created"
+  end
 
   (** Uniqueness Counter * TID * (All thread creates of current thread * All thread creates of the current function and its callees) *)
-  module D = Lattice.Prod3 (N) (ThreadLifted) (Lattice.Prod(TD)(TD))
+  module D = Lattice.Prod3 (N) (ThreadLifted) (Created)
   module C = D
   module P = IdentityP (D)
 

From 0f70e17d5d13404b83d1caed8b4219471c32776f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 11 Oct 2023 15:09:09 +0300
Subject: [PATCH 17/18] Fix MCP module names

---
 src/analyses/mCPRegistry.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml
index 32847bb3ed..810da827ff 100644
--- a/src/analyses/mCPRegistry.ml
+++ b/src/analyses/mCPRegistry.ml
@@ -318,6 +318,7 @@ struct
   open Obj
 
   include DomListPrintable (PrintableOfRepresentativeSpec (DLSpec))
+  let name () = "MCP.P"
 
   type elt = (int * unknown) list
 
@@ -344,6 +345,7 @@ struct
   open Obj
 
   include DomListPrintable (PrintableOfLatticeSpec (DLSpec))
+  let name () = "MCP.D"
 
   let binop_fold f a (x:t) (y:t) =
     GobList.fold_left3 (fun a (n,d) (n',d') (n'',s) -> assert (n = n' && n = n''); f a n s d d') a x y (domain_list ())

From d9afd55a63514ff47f163c34ff07a41ffd48a30c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 11 Oct 2023 15:09:17 +0300
Subject: [PATCH 18/18] Add names to region analysis domains

---
 src/cdomains/regionDomain.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/cdomains/regionDomain.ml b/src/cdomains/regionDomain.ml
index 143ba086a6..b577e3499f 100644
--- a/src/cdomains/regionDomain.ml
+++ b/src/cdomains/regionDomain.ml
@@ -9,6 +9,15 @@ module B = Printable.UnitConf (struct let name = "•" end)
 module VFB =
 struct
   include Printable.Either (VF) (B)
+  let name () = "region"
+
+  let pretty () = function
+    | `Right () -> Pretty.text "•"
+    | `Left x -> VF.pretty () x
+
+  let show = function
+    | `Right () -> "•"
+    | `Left x -> VF.show x
 
   let printXml f = function
     | `Right () ->
@@ -51,6 +60,7 @@ end
 
 module RS = struct
   include PartitionDomain.Set (VFB)
+  let name () = "regions"
   let single_vf vf = singleton (VFB.of_vf vf)
   let single_bullet = singleton (VFB.bullet)
   let remove_bullet x = remove VFB.bullet x