Make signal handler threads unique

src/analyses/base.ml

@@ -2226,6 +2226,20 @@ struct
         in
         List.filter_map (create_thread ~multiple (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown
       end
+    | SignalHandler { signal; handler }, _ -> begin
+        (* extra sync so that we do not analyze new threads with bottom global invariant *)
+        publish_all man `Thread;
+        (* Collect the threads. *)
+        let start_addr = eval_tv ~man man.local handler in
+        let start_funvars = AD.to_var_may start_addr in
+        let start_funvars_with_unknown =
+          if AD.mem Addr.UnknownPtr start_addr then
+            dummyFunDec.svar :: start_funvars
+          else
+            start_funvars
+        in
+        List.filter_map (create_thread ~multiple:false None (Some signal)) start_funvars_with_unknown
+      end
     | _, _ ->
       let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in
       let deep_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = true } args in

src/util/library/libraryDesc.ml

@@ -87,6 +87,7 @@ type special =
   | Bounded of { exp: Cil.exp}  (** Used to check for bounds for termination analysis. *)
   | Rand
   | Once of { once_control: Cil.exp; init_routine: Cil.exp; }
+  | SignalHandler of { signal: Cil.exp; handler: Cil.exp; }
   | Unknown (** Anything not belonging to other types. *) (* TODO: rename to Other? *)
 
 

src/util/library/libraryFunctions.ml

@@ -180,7 +180,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("remove", unknown [drop "pathname" [r]]);
     ("raise", unknown [drop "sig" []]); (* safe-ish, we don't handle signal handlers for now *)
     ("timespec_get", unknown [drop "ts" [w]; drop "base" []]);
-    ("signal", unknown [drop "signum" []; drop "handler" [s]]);
+    ("signal", special [__ "signum" []; __ "handler" [s]] @@ fun signal handler -> SignalHandler {signal; handler});
     ("va_arg", unknown [drop "ap" [r]; drop "T" []]);
     ("va_start", unknown [drop "ap" [r_deep]; drop "parmN" []]);
     ("va_end", unknown [drop "ap" [r_deep]]);
@@ -301,7 +301,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("gethostname", unknown [drop "name" [w]; drop "len" []]);
     ("getpeername", unknown [drop "sockfd" []; drop "addr" [w_deep]; drop "addrlen" [r; w]]);
     ("socket", unknown [drop "domain" []; drop "type" []; drop "protocol" []]);
-    ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]);
+    ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); (* TODO: SignalHandler special *)
     ("tcgetattr", unknown [drop "fd" []; drop "termios_p" [w_deep]]);
     ("tcsetattr", unknown [drop "fd" []; drop "optional_actions" []; drop "termios_p" [r_deep]]);
     ("access", unknown [drop "pathname" [r]; drop "mode" []]);

tests/regression/03-practical/37-signal-sound.c

@@ -0,0 +1,15 @@
+#include <signal.h>
+#include <goblint.h>
+
+int g = 0;
+
+void handler(int sig) {
+  g = 1;
+}
+
+int main() {
+  __goblint_check(g == 0);
+  signal(SIGTERM, handler);
+  __goblint_check(g == 0); // UNKNOWN!
+  return 0;
+}

tests/regression/03-practical/38-signal-unique.c

@@ -0,0 +1,13 @@
+#include <signal.h>
+
+int g = 0;
+
+void handler(int sig) {
+  g = 1; // NORACE
+  g = 2; // NORACE
+}
+
+int main() {
+  signal(SIGTERM, handler);
+  return 0;
+}

tests/regression/03-practical/39-signal-arg.c

@@ -0,0 +1,11 @@
+#include <signal.h>
+#include <goblint.h>
+
+void handler(int sig) {
+  __goblint_check(sig == SIGTERM);
+}
+
+int main() {
+  signal(SIGTERM, handler);
+  return 0;
+}