Support for pthread_once

conf/bench-yaml-validate.json

@@ -71,7 +71,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]

conf/bench-yaml.json

@@ -67,7 +67,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]

conf/ldv-races.json

@@ -1,7 +1,6 @@
 {
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]

conf/traces-rel.json

@@ -83,7 +83,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]

scripts/sv-comp/archive.sh

@@ -37,7 +37,6 @@ zip goblint/scripts/sv-comp/goblint.zip \
     goblint/lib/libc/stub/include/assert.h \
     goblint/lib/goblint/runtime/include/goblint.h \
     goblint/lib/libc/stub/src/stdlib.c \
-    goblint/lib/libc/stub/src/pthread.c \
     goblint/lib/sv-comp/stub/src/sv-comp.c \
     goblint/README.md \
     goblint/LICENSE

src/analyses/pthreadOnce.ml

@@ -0,0 +1,109 @@
+(** Must active and have passed pthreadOnce calls ([pthreadOnce]). *)
+
+open GoblintCil
+open Analyses
+module LF = LibraryFunctions
+
+module Spec =
+struct
+  module Onces = struct
+    include SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All onces" end)
+    let name () = "mayOnces"
+  end
+
+  module ActiveOnces = struct
+    include Lattice.Reverse (Onces)
+    let name () = "active"
+  end
+
+  module SeenOnces = struct
+    include Lattice.Reverse (Onces)
+    let name () = "seen"
+  end
+
+  include Analyses.DefaultSpec
+
+  let name () = "pthreadOnce"
+  module D = Lattice.Prod (ActiveOnces) (SeenOnces)
+  include Analyses.ValueContexts(D)
+
+  (* transfer functions *)
+  let assign man (lval:lval) (rval:exp) : D.t =
+    man.local
+
+  let branch man (exp:exp) (tv:bool) : D.t =
+    man.local
+
+  let body man (f:fundec) : D.t =
+    man.local
+
+  let return man (exp:exp option) (f:fundec) : D.t =
+    man.local
+
+  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+    [man.local, man.local]
+
+  let combine_env man lval fexp f args fc au f_ask =
+    au
+
+  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+    man.local
+
+  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    man.local
+
+  let startstate v = (Onces.empty (), Onces.empty ())
+
+  let possible_vinfos (a: Queries.ask) barrier =
+    Queries.AD.to_var_may (a.f (Queries.MayPointTo barrier))
+
+  let event man (e: Events.t) oman : D.t =
+    match e with
+    | Events.EnterOnce { once_control; tf } when tf ->
+      (let (active, seen) = man.local in
+       let ask = Analyses.ask_of_man man in
+       let possible_vinfos = possible_vinfos ask once_control in
+       let unseen = List.filter (fun v -> not (Onces.mem v seen) && not (Onces.mem v active)) possible_vinfos in
+       match unseen with
+       | [] -> raise Deadcode
+       | [v] -> (Onces.add v active, seen)
+       | _ :: _ -> man.local)
+    | Events.EnterOnce { once_control; tf } ->
+      (let (active, seen) = man.local in
+       let ask = Analyses.ask_of_man man in
+       match possible_vinfos ask once_control with
+       | [v] -> (Onces.add v active, seen)
+       | _ -> man.local)
+    | Events.LeaveOnce { once_control } ->
+      (let (active, seen) = man.local in
+       let ask = Analyses.ask_of_man man in
+       let active' = Onces.diff active (Onces.of_list (possible_vinfos ask once_control)) in
+       let seen' = match possible_vinfos ask once_control with
+         | [v] -> Onces.add v seen
+         | _ -> seen
+       in
+       (active', seen'))
+    | _ -> man.local
+
+  let access man _ = man.local
+
+  module A =
+  struct
+    include D
+    let name () = "onces"
+    let may_race (a1, s1) (a2, s2) =
+      (Onces.is_empty (Onces.inter a1 (Onces.union a2 s2))) && (Onces.is_empty (Onces.inter a2 (Onces.union a1 s1)))
+    let should_print (a1, s1) = not (Onces.is_empty a1) || not (Onces.is_empty s1)
+  end
+
+
+  let threadenter man ~multiple lval f args =
+    let (_, seen) = man.local in
+    [Onces.empty (), seen]
+
+  let threadspawn man ~multiple lval f args fman = man.local
+  let exitstate  v = D.top ()
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)

src/domains/events.ml

@@ -16,6 +16,8 @@ type t =
   | Assert of exp
   | Unassume of {exp: CilType.Exp.t; tokens: WideningToken.t list}
   | Longjmped of {lval: CilType.Lval.t option}
+  | EnterOnce of {once_control: CilType.Exp.t; tf:bool}
+  | LeaveOnce of {once_control: CilType.Exp.t}
 
 (** Should event be emitted after transfer function raises [Deadcode]? *)
 let emit_on_deadcode = function
@@ -31,7 +33,9 @@ let emit_on_deadcode = function
   | UpdateExpSplit _ (* Pointless to split on dead. *)
   | Unassume _ (* Avoid spurious writes. *)
   | Assert _ (* Pointless to refine dead. *)
-  | Longjmped _ ->
+  | Longjmped _
+  | EnterOnce _
+  | LeaveOnce _ ->
     false
 
 let pretty () = function
@@ -47,3 +51,5 @@ let pretty () = function
   | Assert exp -> dprintf "Assert %a" d_exp exp
   | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningToken.pretty) tokens
   | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval
+  | EnterOnce {once_control; tf} -> dprintf "todo"
+  | LeaveOnce {once_control} -> dprintf "todo"

src/framework/constraints.ml

@@ -245,7 +245,7 @@ struct
 
   let tf_special_call man lv f args = S.special man lv f args
 
-  let tf_proc var edge prev_node lv e args getl sidel getg sideg d =
+  let rec tf_proc var edge prev_node lv e args getl sidel getg sideg d =
     let man, r, spawns = common_man var edge prev_node d getl sidel getg sideg in
     let functions =
       match e with
@@ -258,6 +258,34 @@ struct
         let ad = man.ask (Queries.EvalFunvar e) in
         Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *)
     in
+    let once once_control init_routine =
+      let enter =
+        let d' = S.event man (Events.EnterOnce { once_control;  tf = true }) man in
+        let proc = tf_proc var edge prev_node None init_routine [] getl sidel getg sideg d' in
+        if not (S.D.is_bot proc) then
+          let rec proc_man =
+            { man with
+              ask = (fun (type a) (q: a Queries.t) -> S.query proc_man q);
+              local = proc;
+            }
+          in
+          S.event proc_man (Events.LeaveOnce { once_control }) proc_man
+        else
+          S.D.bot ()
+      in
+      let not_enter =
+        (* Always possible, will never yield `Bot *)
+        let d' = S.event man (Events.EnterOnce { once_control;  tf = false }) man in
+        let rec d'_man =
+          { man with
+            ask = (fun (type a) (q: a Queries.t) -> S.query d'_man q);
+            local = d';
+          }
+        in
+        S.event d'_man (Events.LeaveOnce { once_control }) d'_man
+      in
+      D.join enter not_enter
+    in
     let one_function f =
       match f.vtype with
       | TFun (_, params, var_arg, _)  ->
@@ -266,14 +294,21 @@ struct
         (* Check whether number of arguments fits. *)
         (* If params is None, the function or its parameters are not declared, so we still analyze the unknown function call. *)
         if Option.is_none params || p_length = arg_length || (var_arg && arg_length >= p_length) then
-          begin Some (match Cilfacade.find_varinfo_fundec f with
-              | fd when LibraryFunctions.use_special f.vname ->
-                M.info ~category:Analyzer "Using special for defined function %s" f.vname;
-                tf_special_call man lv f args
-              | fd ->
-                tf_normal_call man lv e fd args getl sidel getg sideg
-              | exception Not_found ->
-                tf_special_call man lv f args)
+          begin
+            let is_once = LibraryFunctions.find ~nowarn:true f in
+            match is_once.special args with
+            | Once { once_control; init_routine } ->
+              Some (once once_control init_routine)
+            | _
+            | exception LibraryDsl.Expected _-> (* propagate weirdness inside *)
+              Some (match Cilfacade.find_varinfo_fundec f with
+                  | fd when LibraryFunctions.use_special f.vname ->
+                    M.info ~category:Analyzer "Using special for defined function %s" f.vname;
+                    tf_special_call man lv f args
+                  | fd ->
+                    tf_normal_call man lv e fd args getl sidel getg sideg
+                  | exception Not_found ->
+                    tf_special_call man lv f args)
           end
         else begin
           let geq = if var_arg then ">=" else "" in

src/goblint_lib.ml

@@ -130,6 +130,7 @@ module RelationPriv = RelationPriv
 module ThreadEscape = ThreadEscape
 module PthreadSignals = PthreadSignals
 module ExtractPthread = ExtractPthread
+module PthreadOnce = PthreadOnce
 
 (** {2 Longjmp}
 

src/maingoblint.ml

@@ -418,9 +418,6 @@ let preprocess_files () =
   if List.mem "c" (get_string_list "lib.activated") then
     extra_files := find_custom_include (Fpath.v "stdlib.c") :: !extra_files;
 
-  if List.mem "pthread" (get_string_list "lib.activated") then
-    extra_files := find_custom_include (Fpath.v "pthread.c") :: !extra_files;
-
   if List.mem "sv-comp" (get_string_list "lib.activated") then
     extra_files := find_custom_include (Fpath.v "sv-comp.c") :: !extra_files;
 

src/util/library/libraryDesc.ml

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

src/util/library/libraryDsl.ml

@@ -30,6 +30,8 @@ struct
     | [] -> fail "^::"
 end
 
+exception Expected = Pattern.Expected
+
 type access =
   | Access of LibraryDesc.Access.t
   | If of (unit -> bool) * access

src/util/library/libraryDsl.mli

@@ -82,3 +82,5 @@ val c_deep: access
 
 (** Conditional access, e.g. on an option. *)
 val if_: (unit -> bool) -> access -> access
+
+exception Expected of string

src/util/library/libraryFunctions.ml

@@ -464,6 +464,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg; multiple = false }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *)
     ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *)
     ("pthread_join", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
+    ("pthread_once", special [__ "once_control" []; __ "init_routine" []] @@ fun once_control init_routine -> Once {once_control; init_routine});
     ("pthread_kill", unknown [drop "thread" []; drop "sig" []]);
     ("pthread_equal", unknown [drop "t1" []; drop "t2" []]);
     ("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]);
@@ -1298,7 +1299,7 @@ let is_safe_uncalled fn_name =
   List.exists (fun r -> Str.string_match r fn_name 0) kernel_safe_uncalled_regex
 
 
-let unknown_desc f : LibraryDesc.t =
+let unknown_desc f ~nowarn : LibraryDesc.t =
   let accs args : (LibraryDesc.Access.t * 'a list) list = [
     ({ kind = Read; deep = true; }, if GobConfig.get_bool "sem.unknown_function.read.args" then args else []);
     ({ kind = Write; deep = true; }, if GobConfig.get_bool "sem.unknown_function.invalidate.args" then args else []);
@@ -1314,7 +1315,7 @@ let unknown_desc f : LibraryDesc.t =
       []
   in
   (* TODO: remove hack when all classify are migrated *)
-  if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then (
+  if not nowarn && not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then (
     M.msg_final Error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing";
     M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname
   );
@@ -1324,12 +1325,11 @@ let unknown_desc f : LibraryDesc.t =
     special = fun _ -> Unknown;
   }
 
-let find f =
+let find ?(nowarn=false) f =
   let name = f.vname in
   match Hashtbl.find_option (ResettableLazy.force activated_library_descs) name with
   | Some desc -> desc
-  | None -> unknown_desc f
-
+  | None -> unknown_desc ~nowarn f
 
 let is_special fv =
   if use_special fv.vname then

src/util/library/libraryFunctions.mli

@@ -11,7 +11,7 @@ val use_special : string -> bool
 val is_safe_uncalled : string -> bool
 
 (** Find library function descriptor for {e special} function (as per {!is_special}). *)
-val find: Cil.varinfo -> LibraryDesc.t
+val find: ?nowarn:bool -> Cil.varinfo -> LibraryDesc.t
 
 val is_special: Cil.varinfo -> bool
 (** Check if function is treated specially. *)

tests/regression/03-practical/35-base-mutex-macos.t

@@ -1,4 +1,4 @@
-  $ goblint --enable witness.yaml.enabled --disable witness.invariant.accessed --set pre.cppflags[+] -DGOBLINT_NO_PTHREAD_ONCE 35-base-mutex-macos.c
+  $ goblint --enable witness.yaml.enabled --disable witness.invariant.accessed 35-base-mutex-macos.c
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0

tests/regression/71-doublelocking/07-rec-dyn-osx.c

@@ -1,6 +1,5 @@
-// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
 // Here, we do not include pthread.h, so MutexAttr.recursive_int remains at `2`, emulating the behavior of OS X.
-#define GOBLINT_NO_PTHREAD_ONCE 1
 typedef signed char __int8_t;
 typedef unsigned char __uint8_t;
 typedef short __int16_t;

tests/regression/71-doublelocking/20-default-init-osx.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
 // Here, we do not include pthread.h, to emulate the behavior of OS X.
 #define NULL ((void *)0)
 typedef signed char __int8_t;