diff --git a/.semgrep/fold.yml b/.semgrep/fold.yml new file mode 100644 index 0000000000..8e4739791f --- /dev/null +++ b/.semgrep/fold.yml @@ -0,0 +1,26 @@ +rules: + - id: fold-exists + patterns: + - pattern-either: + - pattern: $D.fold ... false + - pattern: $D.fold_left ... false + - pattern: $D.fold_right ... false + - pattern: fold ... false + - pattern: fold_left ... false + - pattern: fold_right ... false + message: consider replacing fold with exists + languages: [ocaml] + severity: WARNING + + - id: fold-for_all + patterns: + - pattern-either: + - pattern: $D.fold ... true + - pattern: $D.fold_left ... true + - pattern: $D.fold_right ... true + - pattern: fold ... true + - pattern: fold_left ... true + - pattern: fold_right ... true + message: consider replacing fold with for_all + languages: [ocaml] + severity: WARNING diff --git a/.semgrep/tracing.yml b/.semgrep/tracing.yml index 061b3efa0d..9c7813a7e8 100644 --- a/.semgrep/tracing.yml +++ b/.semgrep/tracing.yml @@ -8,8 +8,16 @@ rules: - pattern: Messages.tracec - pattern: Messages.traceu - pattern: Messages.traceli + - pattern: M.trace + - pattern: M.tracel + - pattern: M.tracei + - pattern: M.tracec + - pattern: M.traceu + - pattern: M.traceli - pattern-not-inside: if Messages.tracing then ... - pattern-not-inside: if Messages.tracing && ... then ... + - pattern-not-inside: if M.tracing then ... + - pattern-not-inside: if M.tracing && ... then ... message: trace functions should only be called if tracing is enabled at compile time languages: [ocaml] severity: WARNING diff --git a/src/analyses/base.ml b/src/analyses/base.ml index e429155e4d..e5bcbfede5 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2172,11 +2172,7 @@ struct in List.filter_map (create_thread ~multiple (Some (Mem id, NoOffset)) (Some ptc_arg)) start_funvars_with_unknown end - | _, _ when get_bool "sem.unknown_function.spawn" -> - (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions. - But here we consider all non-ThreadCreate functions also unknown, so old-style LibraryFunctions access - definitions using `Write would still spawn because they are not truly unknown functions (missing from LibraryFunctions). - Need this to not have memmove spawn in SV-COMP. *) + | _, _ -> 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 let shallow_flist = collect_invalidate ~deep:false ~ctx ctx.local shallow_args in @@ -2185,7 +2181,6 @@ struct let addrs = List.concat_map AD.to_var_may flist in if addrs <> [] then M.debug ~category:Analyzer "Spawning non-unique functions from unknown function: %a" (d_list ", " CilType.Varinfo.pretty) addrs; List.filter_map (create_thread ~multiple:true None None) addrs - | _, _ -> [] let assert_fn ctx e refine = (* make the state meet the assertion in the rest of the code *) @@ -2656,6 +2651,15 @@ struct | Unknown, "__goblint_assume_join" -> let id = List.hd args in Priv.thread_join ~force:true (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) id st + | ThreadSelf, _ -> + begin match lv, ThreadId.get_current (Analyses.ask_of_ctx ctx) with + | Some lv, `Lifted tid -> + set ~ctx st (eval_lv ~ctx st lv) (Cilfacade.typeOfLval lv) (Thread (ValueDomain.Threads.singleton tid)) + | Some lv, _ -> + invalidate_ret_lv st + | None, _ -> + st + end | Alloca size, _ -> begin match lv with | Some lv -> diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 946b8f8cc5..e69757c7a8 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -1040,11 +1040,11 @@ struct let s = MustLockset.remove m (current_lockset ask) in let t = current_thread ask in let side_cpa = CPA.filter (fun x _ -> - GWeak.fold (fun s' tm acc -> + GWeak.exists (fun s' tm -> (* TODO: swap 2^M and T partitioning for lookup by t here first? *) let v = ThreadMap.find t tm in - (MustLockset.mem m s' && not (VD.is_bot v)) || acc - ) (G.weak (getg (V.global x))) false + (MustLockset.mem m s' && not (VD.is_bot v)) + ) (G.weak (getg (V.global x))) ) st.cpa in sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa)); @@ -1098,9 +1098,9 @@ struct let unlock ask getg sideg (st: BaseComponents (D).t) m = let s = MustLockset.remove m (current_lockset ask) in let side_cpa = CPA.filter (fun x _ -> - GWeak.fold (fun s' v acc -> - (MustLockset.mem m s' && not (VD.is_bot v)) || acc - ) (G.weak (getg (V.global x))) false + GWeak.exists (fun s' v -> + (MustLockset.mem m s' && not (VD.is_bot v)) + ) (G.weak (getg (V.global x))) ) st.cpa in sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa)); diff --git a/src/autoTune.ml b/src/autoTune.ml index 0def6021fa..f59a10ee8a 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -157,7 +157,7 @@ let hasFunction pred = Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) @@ fun () -> if LibraryFunctions.is_special var then let desc = LibraryFunctions.find var in - GobOption.exists (fun args -> pred (desc.special args)) (functionArgs var) + GobOption.exists (fun args -> pred desc args) (functionArgs var) else false in @@ -169,7 +169,7 @@ let hasFunction pred = match unrollType var.vtype with | TFun (_, args, _, _) -> let args = BatOption.map_default (List.map (fun (x,_,_) -> MyCFG.unknown_exp)) [] args in - pred (desc.special args) + pred desc args | _ -> false else false @@ -191,9 +191,10 @@ let enableAnalyses anas = let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"] let reduceThreadAnalyses () = - let isThreadCreate = function + let isThreadCreate (desc: LibraryDesc.t) args = + match desc.special args with | LibraryDesc.ThreadCreate _ -> true - | _ -> false + | _ -> LibraryDesc.Accesses.find_kind desc.accs Spawn args <> [] in let hasThreadCreate = hasFunction isThreadCreate in if not @@ hasThreadCreate then ( @@ -446,7 +447,8 @@ let wideningOption factors file = } let activateTmpSpecialAnalysis () = - let isMathFun = function + let isMathFun (desc: LibraryDesc.t) args = + match desc.special args with | LibraryDesc.Math _ -> true | _ -> false in diff --git a/src/cdomain/value/cdomains/stringDomain.ml b/src/cdomain/value/cdomains/stringDomain.ml index 2b968b0321..35054590f9 100644 --- a/src/cdomain/value/cdomains/stringDomain.ml +++ b/src/cdomain/value/cdomains/stringDomain.ml @@ -20,12 +20,12 @@ let reset_lazy () = type t = string option [@@deriving eq, ord, hash] +(** [None] means top. *) let hash x = - if get_string_domain () = Disjoint then - hash x - else - 13859 + match get_string_domain () with + | Disjoint | Flat -> hash x + | Unit -> 13859 let show = function | Some x -> "\"" ^ x ^ "\"" @@ -39,10 +39,9 @@ include Printable.SimpleShow ( ) let of_string x = - if get_string_domain () = Unit then - None - else - Some x + match get_string_domain () with + | Unit -> None + | Disjoint | Flat -> Some x let to_string x = x (* only keep part before first null byte *) @@ -91,10 +90,10 @@ let join x y = | _, None -> None | Some a, Some b when a = b -> Some a | Some a, Some b (* when a <> b *) -> - if get_string_domain () = Disjoint then - raise Lattice.Uncomparable - else - None + match get_string_domain () with + | Disjoint -> raise Lattice.Uncomparable + | Flat -> None + | Unit -> assert false let meet x y = match x, y with @@ -102,13 +101,14 @@ let meet x y = | a, None -> a | Some a, Some b when a = b -> Some a | Some a, Some b (* when a <> b *) -> - if get_string_domain () = Disjoint then - raise Lattice.Uncomparable - else - raise Lattice.BotValue + match get_string_domain () with + | Disjoint -> raise Lattice.Uncomparable + | Flat -> raise Lattice.BotValue + | Unit -> assert false let repr x = - if get_string_domain () = Disjoint then + match get_string_domain () with + | Disjoint -> x (* everything else is kept separate, including strings if not limited *) - else + | Flat | Unit -> None (* all strings together if limited *) diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml index fff6734f27..226905ed6f 100644 --- a/src/cdomain/value/cdomains/threadIdDomain.ml +++ b/src/cdomain/value/cdomains/threadIdDomain.ml @@ -83,10 +83,10 @@ struct (v, None) let is_main = function - | ({vname; _}, None) -> List.mem vname @@ GobConfig.get_string_list "mainfun" + | ({vname; _}, None) -> GobConfig.get_bool "ana.thread.include-node" && List.mem vname @@ GobConfig.get_string_list "mainfun" | _ -> false - let is_unique _ = false (* TODO: should this consider main unique? *) + let is_unique = is_main let may_create _ _ = true let is_must_parent _ _ = false end diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 447290b44d..5d87eb51f6 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1544,6 +1544,19 @@ } }, "additionalProperties": false + }, + "atexit": { + "title": "sem.atexit", + "type": "object", + "properties": { + "ignore": { + "title": "sem.atexit.ignore", + "description": "Ignore atexit callbacks (unsound).", + "type": "boolean", + "default": false + } + }, + "additionalProperties": false } }, "additionalProperties": false diff --git a/src/domain/partitionDomain.ml b/src/domain/partitionDomain.ml index 9675e9bfce..316f4fb705 100644 --- a/src/domain/partitionDomain.ml +++ b/src/domain/partitionDomain.ml @@ -31,10 +31,10 @@ struct let meet _ _ = failwith "PartitonDomain.Set.meet: unsound" let collapse (s1:t) (s2:t): bool = - let f vf2 res = - res || exists (fun vf1 -> S.collapse vf1 vf2) s1 + let f vf2 = + exists (fun vf1 -> S.collapse vf1 vf2) s1 in - fold f s2 false + exists f s2 let add e s = join s (singleton e) diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml index 6c314ef7c9..a663b80833 100644 --- a/src/incremental/compareCFG.ml +++ b/src/incremental/compareCFG.ml @@ -131,7 +131,7 @@ let reexamine f1 f2 (same : biDirectionNodeMap) (diffNodes1 : unit NH.t) (module false end in let cond n2 = Node.equal n2 (FunctionEntry f2) || check_all_nodes_in_same (List.map snd (CfgNew.prev n2)) n2 in - let forall = NH.fold (fun n2 n1 acc -> acc && cond n2) same.node2to1 true in + let forall = NH.fold (fun n2 n1 acc -> acc && cond n2) same.node2to1 true in (* nosemgrep: fold-for_all *) (* cond does side effects *) if not forall then repeat () in repeat (); NH.to_seq same.node1to2, NH.to_seq_keys diffNodes1 diff --git a/src/solver/td3.ml b/src/solver/td3.ml index c7bec621e3..3cab3cf7f7 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -49,7 +49,7 @@ module Base = open SolverBox.Warrow (S.Dom) include Generic.SolverStats (S) (HM) module VS = Set.Make (S.Var) - let exists_key f hm = HM.fold (fun k _ a -> a || f k) hm false + let exists_key f hm = HM.exists (fun k _ -> f k) hm type solver_data = { st: (S.Var.t * S.Dom.t) list; (* needed to destabilize start functions if their start state changed because of some changed global initializer *) @@ -289,7 +289,7 @@ module Base = destabilize_vs y || b || was_stable && List.mem_cmp S.Var.compare y vs else true - ) w false + ) w false (* nosemgrep: fold-exists *) (* does side effects *) and solve ?reuse_eq x phase = if tracing then trace "sol2" "solve %a, phase: %s, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (show_phase phase) (HM.mem called x) (HM.mem stable x) (HM.mem wpoint x); init x; diff --git a/src/util/autoSoundConfig.ml b/src/util/autoSoundConfig.ml index 7a30bdf5ce..0bb67e768e 100644 --- a/src/util/autoSoundConfig.ml +++ b/src/util/autoSoundConfig.ml @@ -12,8 +12,8 @@ let enableSpecAnalyses spec analyses = Logs.info "Specification: %s -> enabling soundness analyses \"%s\"" (Svcomp.Specification.to_string [spec]) (String.concat ", " analyses); enableAnalyses analyses -let enableOptions options = - let enableOpt option = +let enableOptions options = + let enableOpt option = Logs.info "Setting \"%s\" to true" option; set_bool option true in @@ -60,7 +60,8 @@ let enableAnalysesForSpecification () = let longjmpAnalyses = ["activeLongjmp"; "activeSetjmp"; "taintPartialContexts"; "modifiedSinceSetjmp"; "poisonVariables"; "expsplit"; "vla"] let activateLongjmpAnalysesWhenRequired () = - let isLongjmp = function + let isLongjmp (desc: LibraryDesc.t) args = + match desc.special args with | LibraryDesc.Longjmp _ -> true | _ -> false in diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml index 80cf86b1e2..6f34de1864 100644 --- a/src/util/library/libraryDesc.ml +++ b/src/util/library/libraryDesc.ml @@ -56,6 +56,7 @@ type special = | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; multiple: bool } | ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; } | ThreadExit of { ret_val: Cil.exp; } + | ThreadSelf | Globalize of Cil.exp | Signal of Cil.exp | Broadcast of Cil.exp diff --git a/src/util/library/libraryDsl.ml b/src/util/library/libraryDsl.ml index 64684fb1ce..a380714dc0 100644 --- a/src/util/library/libraryDsl.ml +++ b/src/util/library/libraryDsl.ml @@ -30,8 +30,20 @@ struct | [] -> fail "^::" end +type access = + | Access of LibraryDesc.Access.t + | If of (unit -> bool) * access + +let rec eval_access = function + | Access acc -> Some acc + | If (p, access) -> + if p () then + eval_access access + else + None + type ('k, 'l, 'r) arg_desc = { - accesses: Access.t list; + accesses: access list; match_arg: (Cil.exp, 'k, 'r) Pattern.t; match_var_args: (Cil.exp list, 'l, 'r) Pattern.t; } @@ -51,15 +63,21 @@ let rec accs: type k r. (k, r) args_desc -> Accesses.t = fun args_desc args -> match args_desc, args with | [], [] -> [] | VarArgs arg_desc, args -> - List.map (fun acc -> - (acc, args) + List.filter_map (fun access -> + match eval_access access with + | Some acc -> Some (acc, args) + | None -> None ) arg_desc.accesses | arg_desc :: args_desc, arg :: args -> let accs'' = accs args_desc args in - List.fold_left (fun (accs'': (Access.t * Cil.exp list) list) (acc: Access.t) -> - match List.assoc_opt acc accs'' with - | Some args -> (acc, arg :: args) :: List.remove_assoc acc accs'' - | None -> (acc, [arg]) :: accs'' + List.fold_left (fun (accs'': (Access.t * Cil.exp list) list) (access: access) -> + match eval_access access with + | Some acc -> + begin match List.assoc_opt acc accs'' with + | Some args -> (acc, arg :: args) :: List.remove_assoc acc accs'' + | None -> (acc, [arg]) :: accs'' + end + | None -> accs'' ) accs'' arg_desc.accesses | _, _ -> invalid_arg "accs" @@ -94,13 +112,15 @@ let drop (_name: string) accesses = { empty_drop_desc with accesses; } let drop' accesses = { empty_drop_desc with accesses; } -let r = Access.{ kind = Read; deep = false; } -let r_deep = Access.{ kind = Read; deep = true; } -let w = Access.{ kind = Write; deep = false; } -let w_deep = Access.{ kind = Write; deep = true; } -let f = Access.{ kind = Free; deep = false; } -let f_deep = Access.{ kind = Free; deep = true; } -let s = Access.{ kind = Spawn; deep = false; } -let s_deep = Access.{ kind = Spawn; deep = true; } -let c = Access.{ kind = Spawn; deep = false; } (* TODO: Sound, but very imprecise hack for calls to function pointers given as arguments. *) -let c_deep = Access.{ kind = Spawn; deep = true; } +let r = Access { kind = Read; deep = false; } +let r_deep = Access { kind = Read; deep = true; } +let w = Access { kind = Write; deep = false; } +let w_deep = Access { kind = Write; deep = true; } +let f = Access { kind = Free; deep = false; } +let f_deep = Access { kind = Free; deep = true; } +let s = Access { kind = Spawn; deep = false; } +let s_deep = Access { kind = Spawn; deep = true; } +let c = Access { kind = Spawn; deep = false; } (* TODO: Sound, but very imprecise hack for calls to function pointers given as arguments. *) +let c_deep = Access { kind = Spawn; deep = true; } + +let if_ p access = If (p, access) diff --git a/src/util/library/libraryDsl.mli b/src/util/library/libraryDsl.mli index 052f92c593..42c300af8e 100644 --- a/src/util/library/libraryDsl.mli +++ b/src/util/library/libraryDsl.mli @@ -28,52 +28,57 @@ val special': ?attrs:LibraryDesc.attr list -> (LibraryDesc.special, LibraryDesc. (** Create unknown library function descriptor from arguments descriptor, which must {!drop} all arguments. *) val unknown: ?attrs:LibraryDesc.attr list -> (LibraryDesc.special, LibraryDesc.special) args_desc -> LibraryDesc.t +(** Argument access descriptor. *) +type access (** Argument descriptor, which captures the named argument with accesses for continuation function of {!special}. *) -val __: string -> LibraryDesc.Access.t list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc +val __: string -> access list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc (** Argument descriptor, which captures an unnamed argument with accesses for continuation function of {!special}. *) -val __': LibraryDesc.Access.t list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc +val __': access list -> (Cil.exp -> 'r, Cil.exp list -> 'r, 'r) arg_desc (** Argument descriptor, which drops (does not capture) the named argument with accesses. *) -val drop: string -> LibraryDesc.Access.t list -> ('r, 'r, 'r) arg_desc +val drop: string -> access list -> ('r, 'r, 'r) arg_desc (** Argument descriptor, which drops (does not capture) an unnamed argument with accesses. *) -val drop': LibraryDesc.Access.t list -> ('r, 'r, 'r) arg_desc +val drop': access list -> ('r, 'r, 'r) arg_desc (** Shallow {!AccessKind.Read} access. All immediate arguments of function calls are always read, this specifies the reading of pointed-to values. *) -val r: LibraryDesc.Access.t +val r: access (** Deep {!AccessKind.Read} access. All immediate arguments of function calls are always read, this specifies the reading of pointed-to values. Rarely needed. *) -val r_deep: LibraryDesc.Access.t +val r_deep: access (** Shallow {!AccessKind.Write} access. *) -val w: LibraryDesc.Access.t +val w: access (** Deep {!AccessKind.Write} access. Rarely needed. *) -val w_deep: LibraryDesc.Access.t +val w_deep: access (** Shallow {!AccessKind.Free} access. *) -val f: LibraryDesc.Access.t +val f: access (** Deep {!AccessKind.Free} access. Rarely needed. *) -val f_deep: LibraryDesc.Access.t +val f_deep: access (** Shallow {!AccessKind.Spawn} access. *) -val s: LibraryDesc.Access.t +val s: access (** Deep {!AccessKind.Spawn} access. Rarely needed. *) -val s_deep: LibraryDesc.Access.t +val s_deep: access (** Shallow {!AccessKind.Spawn} access, substituting function pointer calls for now (TODO). *) -val c: LibraryDesc.Access.t +val c: access (** Deep {!AccessKind.Spawn} access, substituting deep function pointer calls for now (TODO) *) -val c_deep: LibraryDesc.Access.t \ No newline at end of file +val c_deep: access + +(** Conditional access, e.g. on an option. *) +val if_: (unit -> bool) -> access -> access diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 25a90da2d3..fbcaa4fe60 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -145,7 +145,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *) ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value }); - ("atexit", unknown [drop "function" [s]]); + ("atexit", unknown [drop "function" [if_ (fun () -> not (get_bool "sem.atexit.ignore")) s]]); ("atoi", unknown [drop "nptr" [r]]); ("atol", unknown [drop "nptr" [r]]); ("atoll", unknown [drop "nptr" [r]]); @@ -504,7 +504,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_attr_setstacksize", unknown [drop "attr" [w]; drop "stacksize" []]); ("pthread_attr_getscope", unknown [drop "attr" [r]; drop "scope" [w]]); ("pthread_attr_setscope", unknown [drop "attr" [w]; drop "scope" []]); - ("pthread_self", unknown []); + ("pthread_self", special [] ThreadSelf); ("pthread_sigmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]); ("pthread_setspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []; drop "value" [w_deep]]); ("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]); diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 5da46a1011..bb70c3319f 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -342,14 +342,14 @@ struct | UnreachCall _ -> (* error function name is globally known through Svcomp.task *) let is_unreach_call = - LHT.fold (fun (n, c) v acc -> + LHT.for_all (fun (n, c) v -> match n with (* FunctionEntry isn't used for extern __VERIFIER_error... *) | FunctionEntry f when Svcomp.is_error_function f.svar -> let is_dead = Spec.D.is_bot v in - acc && is_dead - | _ -> acc - ) lh true + is_dead + | _ -> true + ) lh in if is_unreach_call then ( diff --git a/tests/regression/41-stdlib/08-atexit-no-spawn.c b/tests/regression/41-stdlib/08-atexit-no-spawn.c index 7f25f42183..3bbba82634 100644 --- a/tests/regression/41-stdlib/08-atexit-no-spawn.c +++ b/tests/regression/41-stdlib/08-atexit-no-spawn.c @@ -1,4 +1,4 @@ -// PARAM: --disable sem.unknown_function.spawn +// PARAM: --enable sem.atexit.ignore #include #include diff --git a/tests/regression/51-threadjoins/09-join-main.c b/tests/regression/51-threadjoins/09-join-main.c new file mode 100644 index 0000000000..196ef8bc00 --- /dev/null +++ b/tests/regression/51-threadjoins/09-join-main.c @@ -0,0 +1,29 @@ +//PARAM: --set ana.activated[+] threadJoins +#include +#include + +pthread_t mainid; + +int g = 10; + +void *t_fun(void *arg) { + int r = pthread_join(mainid, NULL); // TSan doesn't like this... + printf("j: %d\n", r); + g++; // NORACE + printf("t_fun: %d\n", g); + return NULL; +} + + +int main(void) { + mainid = pthread_self(); + + pthread_t id2; + pthread_create(&id2, NULL, t_fun, NULL); + + g++; // NORACE + printf("main: %d\n", g); + + pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2 + return 0; +} diff --git a/tests/regression/51-threadjoins/10-join-main-plain.c b/tests/regression/51-threadjoins/10-join-main-plain.c new file mode 100644 index 0000000000..5b2c188bf5 --- /dev/null +++ b/tests/regression/51-threadjoins/10-join-main-plain.c @@ -0,0 +1,29 @@ +//PARAM: --set ana.activated[+] threadJoins --set ana.thread.domain plain +#include +#include + +pthread_t mainid; + +int g = 10; + +void *t_fun(void *arg) { + int r = pthread_join(mainid, NULL); // TSan doesn't like this... + printf("j: %d\n", r); + g++; // RACE (imprecise by plain thread IDs) + printf("t_fun: %d\n", g); + return NULL; +} + + +int main(void) { + mainid = pthread_self(); + + pthread_t id2; + pthread_create(&id2, NULL, t_fun, NULL); + + g++; // NORACE + printf("main: %d\n", g); + + pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2 + return 0; +} diff --git a/tests/regression/51-threadjoins/11-join-main-plain-no-node.c b/tests/regression/51-threadjoins/11-join-main-plain-no-node.c new file mode 100644 index 0000000000..7f235fd1d8 --- /dev/null +++ b/tests/regression/51-threadjoins/11-join-main-plain-no-node.c @@ -0,0 +1,29 @@ +//PARAM: --set ana.activated[+] threadJoins --set ana.thread.domain plain --disable ana.thread.include-node +#include +#include + +pthread_t mainid; + +int g = 10; + +void *t_fun(void *arg) { + int r = pthread_join(mainid, NULL); // TSan doesn't like this... + printf("j: %d\n", r); + g++; // RACE (imprecise by plain thread IDs) + printf("t_fun: %d\n", g); + return NULL; +} + + +int main(void) { + mainid = pthread_self(); + + pthread_t id2; + pthread_create(&id2, NULL, t_fun, NULL); + + g++; // RACE (imprecise by plain thread IDs not knowing if main is actual main or spawned by program) + printf("main: %d\n", g); + + pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2 + return 0; +}