diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 970895e971..74a98af6be 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -3,6 +3,128 @@ open GoblintCil open Analyses +(** Data race analysis with tries for offsets and type-based memory locations for open code. + + Accesses are to memory locations ({{!Access.Memo} memos}) which consist of a root and offset. + {{!Access.MemoRoot} Root} can be: + + variable, if access is to known global variable or alloc-variable; + + type, if access is to unknown pointer. + + Accesses are (now) collected to sets for each corresponding memo, + after points-to sets are resolved, during postsolving. + + Race checking is performed per-memo, + except must additionally account for accesses to other memos (see diagram below): + + access to [s.f] can race with access to a prefix like [s], which writes an entire struct at once; + + access to [s.f] can race with type-based access like [(struct S).f]; + + access to [(struct S).f] can race with type-based access to a suffix like [(int)]. + + access to [(struct T).s.f] can race with type-based access like [(struct S)], which is a combination of the above. + + These are accounted for lazily (unlike in the past). + + Prefixes (a.k.a. inner distribution) are handled using a trie data structure enriched with lattice properties. + Race checking starts at the root and passes accesses to ancestor nodes down to children. + + Type suffixes (a.k.a. outer distribution) are handled by computing successive immediate type suffixes transitively + and accessing corresponding offsets from corresponding root tries in the global invariant. + + Type suffix prefixes (for the combination of the two) are handled by passing type suffix accesses down when traversing the prefix trie. + + Race checking happens at each trie node with the above three access sets at hand using {!Access.group_may_race}. + All necessary combinations between the four classes are handled, but unnecessary repeated work is carefully avoided. + E.g. accesses which are pairwise checked at some prefix are not re-checked pairwise at a node. + Thus, races (with prefixes or type suffixes) are reported for most precise memos with actual accesses: + at the longest prefix and longest type suffix. + + Additionally, accesses between prefix and type suffix intersecting at a node are checked. + These races are reported at the unique memo at the intersection of the prefix and the type suffix. + This requires an implementation hack to still eagerly do outer distribution, but only of empty access sets. + It ensures that corresponding trie nodes exist for traversal later. *) + +(** Given C declarations: + {@c[ + struct S { + int f; + }; + + struct T { + struct S s; + }; + + struct T t; + ]} + + Example structure of related memos for race checking: + {v + (int) (S) (T) + \ / \ / \ + f s t + \ / \ / + f s + \ / + f + v} + where: + - [(int)] is a type-based memo root for the primitive [int] type; + - [(S)] and [(T)] are short for [(struct S)] and [(struct T)], which are type-based memo roots; + - prefix relations are indicated by [/], so access paths run diagonally from top-right to bottom-left; + - type suffix relations are indicated by [\ ]. + + All same-node races: + - Race between [t.s.f] and [t.s.f] is checked/reported at [t.s.f]. + - Race between [t.s] and [t.s] is checked/reported at [t.s]. + - Race between [t] and [t] is checked/reported at [t]. + - Race between [(T).s.f] and [(T).s.f] is checked/reported at [(T).s.f]. + - Race between [(T).s] and [(T).s] is checked/reported at [(T).s]. + - Race between [(T)] and [(T)] is checked/reported at [(T)]. + - Race between [(S).f] and [(S).f] is checked/reported at [(S).f]. + - Race between [(S)] and [(S)] is checked/reported at [(S)]. + - Race between [(int)] and [(int)] is checked/reported at [(int)]. + + All prefix races: + - Race between [t.s.f] and [t.s] is checked/reported at [t.s.f]. + - Race between [t.s.f] and [t] is checked/reported at [t.s.f]. + - Race between [t.s] and [t] is checked/reported at [t.s]. + - Race between [(T).s.f] and [(T).s] is checked/reported at [(T).s.f]. + - Race between [(T).s.f] and [(T)] is checked/reported at [(T).s.f]. + - Race between [(T).s] and [(T)] is checked/reported at [(T).s]. + - Race between [(S).f] and [(S)] is checked/reported at [(S).f]. + + All type suffix races: + - Race between [t.s.f] and [(T).s.f] is checked/reported at [t.s.f]. + - Race between [t.s.f] and [(S).f] is checked/reported at [t.s.f]. + - Race between [t.s.f] and [(int)] is checked/reported at [t.s.f]. + - Race between [(T).s.f] and [(S).f] is checked/reported at [(T).s.f]. + - Race between [(T).s.f] and [(int)] is checked/reported at [(T).s.f]. + - Race between [(S).f] and [(int)] is checked/reported at [(S).f]. + - Race between [t.s] and [(T).s] is checked/reported at [t.s]. + - Race between [t.s] and [(S)] is checked/reported at [t.s]. + - Race between [(T).s] and [(S)] is checked/reported at [(T).s]. + - Race between [t] and [(T)] is checked/reported at [t]. + + All type suffix prefix races: + - Race between [t.s.f] and [(T).s] is checked/reported at [t.s.f]. + - Race between [t.s.f] and [(T)] is checked/reported at [t.s.f]. + - Race between [t.s.f] and [(S)] is checked/reported at [t.s.f]. + - Race between [(T).s.f] and [(S)] is checked/reported at [(T).s.f]. + - Race between [t.s] and [(T)] is checked/reported at [t.s]. + + All prefix-type suffix races: + - Race between [t.s] and [(T).s.f] is checked/reported at [t.s.f]. + - Race between [t.s] and [(S).f] is checked/reported at [t.s.f]. + - Race between [t.s] and [(int)] is checked/reported at [t.s.f]. + - Race between [t] and [(T).s.f] is checked/reported at [t.s.f]. + - Race between [t] and [(S).f] is checked/reported at [t.s.f]. + - Race between [t] and [(int)] is checked/reported at [t.s.f]. + - Race between [t] and [(T).s] is checked/reported at [t.s]. + - Race between [t] and [(S)] is checked/reported at [t.s]. + - Race between [(T).s] and [(S).f] is checked/reported at [(T).s.f]. + - Race between [(T).s] and [(int)] is checked/reported at [(T).s.f]. + - Race between [(T)] and [(S).f] is checked/reported at [(T).s.f]. + - Race between [(T)] and [(int)] is checked/reported at [(T).s.f]. + - Race between [(T)] and [(S)] is checked/reported at [(T).s]. + - Race between [(S)] and [(int)] is checked/reported at [(S).f]. *) + (** Data race analyzer without base --- this is the new standard *) module Spec = @@ -12,7 +134,7 @@ struct let name () = "race" (* Two global invariants: - 1. memoroot -> (offset -> accesses) -- used for warnings + 1. memoroot -> (offset --trie--> accesses) -- used for warnings 2. varinfo -> set of memo -- used for IterSysVars Global *) module V = @@ -52,13 +174,22 @@ struct module OffsetTrie = struct - include TrieDomain.Make (OneOffset) (Access.AS) + (* LiftBot such that add_distribute_outer can side-effect empty set to indicate + all offsets that exist for prefix-type_suffix race checking. + Otherwise, there are no trie nodes to traverse to where this check must happen. *) + include TrieDomain.Make (OneOffset) (Lattice.LiftBot (Access.AS)) + + let rec find (offset : Offset.Unit.t) ((accs, children) : t) : value = + match offset with + | `NoOffset -> accs + | `Field (f, offset') -> find offset' (ChildMap.find (Field f) children) + | `Index ((), offset') -> find offset' (ChildMap.find Index children) let rec singleton (offset : Offset.Unit.t) (value : value) : t = match offset with | `NoOffset -> (value, ChildMap.empty ()) - | `Field (f, offset') -> (Access.AS.empty (), ChildMap.singleton (Field f) (singleton offset' value)) - | `Index ((), offset') -> (Access.AS.empty (), ChildMap.singleton Index (singleton offset' value)) + | `Field (f, offset') -> (`Bot, ChildMap.singleton (Field f) (singleton offset' value)) + | `Index ((), offset') -> (`Bot, ChildMap.singleton Index (singleton offset' value)) end module G = @@ -96,9 +227,42 @@ struct let side_access ctx (conf, w, loc, e, a) ((memoroot, offset) as memo) = if !AnalysisState.should_warn then - ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (Access.AS.singleton (conf, w, loc, e, a)))); + ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton (conf, w, loc, e, a))))); + side_vars ctx memo + + (** Side-effect empty access set for prefix-type_suffix race checking. *) + let side_access_empty ctx ((memoroot, offset) as memo) = + if !AnalysisState.should_warn then + ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.empty ())))); side_vars ctx memo + (** Get immediate type_suffix memo. *) + let type_suffix_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option = + (* No need to make ana.race.direct-arithmetic return None here, + because (int) is empty anyway since Access.add_distribute_outer isn't called. *) + match root, offset with + | `Var v, _ -> Some (`Type (Cil.typeSig v.vtype), offset) (* global.foo.bar -> (struct S).foo.bar *) (* TODO: Alloc variables void type *) + | _, `NoOffset -> None (* primitive type *) + | _, `Field (f, offset') -> Some (`Type (Cil.typeSig f.ftype), offset') (* (struct S).foo.bar -> (struct T).bar *) + | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') (* (int[])[*] -> int *) + | _, `Index ((), offset') -> None (* TODO: why indexing on non-array? *) + + let rec find_type_suffix' ctx ((root, offset) as memo : Access.Memo.t) : Access.AS.t = + let trie = G.access (ctx.global (V.access root)) in + let accs = + match OffsetTrie.find offset trie with + | `Lifted accs -> accs + | `Bot -> Access.AS.empty () + in + let type_suffix = find_type_suffix ctx memo in + Access.AS.union accs type_suffix + + (** Find accesses from all type_suffixes transitively. *) + and find_type_suffix ctx (memo : Access.Memo.t) : Access.AS.t = + match type_suffix_memo memo with + | Some type_suffix_memo -> find_type_suffix' ctx type_suffix_memo + | None -> Access.AS.empty () + let query ctx (type a) (q: a Queries.t): a Queries.result = match q with | WarnGlobal g -> @@ -108,18 +272,27 @@ struct (* ignore (Pretty.printf "WarnGlobal %a\n" Access.MemoRoot.pretty g'); *) let trie = G.access (ctx.global g) in (** Distribute access to contained fields. *) - let rec distribute_inner offset (accs, children) ancestor_accs = - let ancestor_accs' = Access.AS.union ancestor_accs accs in - OffsetTrie.ChildMap.iter (fun child_key child_trie -> - distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ancestor_accs' - ) children; - if not (Access.AS.is_empty accs) then ( + let rec distribute_inner offset (accs, children) ~prefix ~type_suffix_prefix = + let accs = + match accs with + | `Lifted accs -> accs + | `Bot -> Access.AS.empty () + in + let type_suffix = find_type_suffix ctx (g', offset) in + if not (Access.AS.is_empty accs) || (not (Access.AS.is_empty prefix) && not (Access.AS.is_empty type_suffix)) then ( let memo = (g', offset) in let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in - Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs memo) accs - ) + Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe {node=accs; prefix; type_suffix; type_suffix_prefix}) memo + ); + + (* Recurse to children. *) + let prefix' = Access.AS.union prefix accs in + let type_suffix_prefix' = Access.AS.union type_suffix_prefix type_suffix in + OffsetTrie.ChildMap.iter (fun child_key child_trie -> + distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ~prefix:prefix' ~type_suffix_prefix:type_suffix_prefix' + ) children; in - distribute_inner `NoOffset trie (Access.AS.empty ()) + distribute_inner `NoOffset trie ~prefix:(Access.AS.empty ()) ~type_suffix_prefix:(Access.AS.empty ()) | `Right _ -> (* vars *) () end @@ -142,11 +315,11 @@ struct let loc = Option.get !Node.current_node in let add_access conf voffs = let a = part_access (Option.map fst voffs) in - Access.add (side_access octx (conf, kind, loc, e, a)) e voffs; + Access.add ~side:(side_access octx (conf, kind, loc, e, a)) ~side_empty:(side_access_empty octx) e voffs; in let add_access_struct conf ci = let a = part_access None in - Access.add_one (side_access octx (conf, kind, loc, e, a)) (`Type (TComp (ci, [])), `NoOffset) + Access.add_one ~side:(side_access octx (conf, kind, loc, e, a)) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset) in let has_escaped g = octx.ask (Queries.MayEscape g) in (* The following function adds accesses to the lval-set ls diff --git a/src/domains/access.ml b/src/domains/access.ml index a183a32633..675d1c2e72 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -84,8 +84,7 @@ type acc_typ = [ `Type of CilType.Typ.t | `Struct of CilType.Compinfo.t * Offset module MemoRoot = struct include Printable.StdLeaf - type t = [`Var of CilType.Varinfo.t | `Type of CilType.Typ.t] [@@deriving eq, ord, hash] - (* Can't use typsig for `Type because there's no function to follow offsets on typsig. *) + type t = [`Var of CilType.Varinfo.t | `Type of CilType.Typsig.t] [@@deriving eq, ord, hash] let name () = "memoroot" @@ -93,8 +92,8 @@ struct (* Imitate old printing for now *) match vt with | `Var v -> CilType.Varinfo.pretty () v - | `Type (TComp (c, _)) -> Pretty.dprintf "(struct %s)" c.cname - | `Type t -> Pretty.dprintf "(%a)" CilType.Typ.pretty t + | `Type (TSComp (_, name, _)) -> Pretty.dprintf "(struct %s)" name + | `Type t -> Pretty.dprintf "(%a)" Cilfacade.pretty_typsig_like_typ t include Printable.SimplePretty ( struct @@ -109,7 +108,6 @@ module Memo = struct include Printable.StdLeaf type t = MemoRoot.t * Offset.Unit.t [@@deriving eq, ord, hash] - (* Can't use typsig for `Type because there's no function to follow offsets on typsig. *) let name () = "memo" @@ -117,8 +115,8 @@ struct (* Imitate old printing for now *) match vt with | `Var v -> Pretty.dprintf "%a%a" CilType.Varinfo.pretty v Offset.Unit.pretty o - | `Type (TComp (c, _)) -> Pretty.dprintf "(struct %s)%a" c.cname Offset.Unit.pretty o - | `Type t -> Pretty.dprintf "(%a)%a" CilType.Typ.pretty t Offset.Unit.pretty o + | `Type (TSComp (_, name, _)) -> Pretty.dprintf "(struct %s)%a" name Offset.Unit.pretty o + | `Type t -> Pretty.dprintf "(%a)%a" Cilfacade.pretty_typsig_like_typ t Offset.Unit.pretty o include Printable.SimplePretty ( struct @@ -129,23 +127,14 @@ struct let of_ty (ty: acc_typ): t = match ty with - | `Struct (c, o) -> (`Type (TComp (c, [])), o) - | `Type t -> (`Type t, `NoOffset) + | `Struct (c, o) -> (`Type (TSComp (c.cstruct, c.cname, [])), o) + | `Type t -> (`Type (Cil.typeSig t), `NoOffset) let to_mval: t -> Mval.Unit.t option = function | (`Var v, o) -> Some (v, o) | (`Type _, _) -> None let add_offset ((vt, o): t) o2: t = (vt, Offset.Unit.add_offset o o2) - - let type_of_base ((vt, _): t): typ = - match vt with - | `Var v -> v.vtype - | `Type t -> t - - (** @raise Offset.Type_of_error *) - let type_of ((vt, o) as memo: t): typ = - Offset.Unit.type_of ~base:(type_of_base memo) o end (* TODO: What is the logic for get_type? *) @@ -205,42 +194,43 @@ let get_val_type e: acc_typ = (** Add access to {!Memo} after distributing. *) -let add_one side memo: unit = +let add_one ~side memo: unit = let mv = Memo.to_mval memo in let ignorable = is_ignorable mv in if M.tracing then M.trace "access" "add_one %a (ignorable = %B)\n" Memo.pretty memo ignorable; if not ignorable then side memo -(** Distribute type-based access to variables and containing fields. *) -let rec add_distribute_outer side (t: typ) (o: Offset.Unit.t) = - let memo = (`Type t, o) in +(** Distribute empty access set for type-based access to variables and containing fields. + Empty access sets are needed for prefix-type_suffix race checking. *) +let rec add_distribute_outer ~side ~side_empty (ts: typsig) (o: Offset.Unit.t) = + let memo = (`Type ts, o) in if M.tracing then M.tracei "access" "add_distribute_outer %a\n" Memo.pretty memo; - add_one side memo; + add_one ~side memo; (* Add actual access for non-recursive call, or empty access for recursive call when side is side_empty. *) (* distribute to variables of the type *) - let ts = typeSig t in let vars = TSH.find_all typeVar ts in List.iter (fun v -> - add_one side (`Var v, o) (* same offset, but on variable *) + (* same offset, but on variable *) + add_one ~side:side_empty (`Var v, o) (* Switch to side_empty. *) ) vars; (* recursively distribute to fields containing the type *) let fields = TSH.find_all typeIncl ts in List.iter (fun f -> (* prepend field and distribute to outer struct *) - add_distribute_outer side (TComp (f.fcomp, [])) (`Field (f, o)) + add_distribute_outer ~side:side_empty ~side_empty (TSComp (f.fcomp.cstruct, f.fcomp.cname, [])) (`Field (f, o)) (* Switch to side_empty. *) ) fields; if M.tracing then M.traceu "access" "add_distribute_outer\n" (** Add access to known variable with offsets or unknown variable from expression. *) -let add side e voffs = +let add ~side ~side_empty e voffs = begin match voffs with | Some (v, o) -> (* known variable *) if M.tracing then M.traceli "access" "add var %a%a\n" CilType.Varinfo.pretty v CilType.Offset.pretty o; let memo = (`Var v, Offset.Unit.of_cil o) in - add_one side memo + add_one ~side memo | None -> (* unknown variable *) if M.tracing then M.traceli "access" "add type %a\n" CilType.Exp.pretty e; let ty = get_val_type e in (* extract old acc_typ from expression *) @@ -250,7 +240,7 @@ let add side e voffs = in match o with | `NoOffset when not !collect_direct_arithmetic && isArithmeticType t -> () - | _ -> add_distribute_outer side t o (* distribute to variables and outer offsets *) + | _ -> add_distribute_outer ~side ~side_empty (Cil.typeSig t) o (* distribute to variables and outer offsets *) end; if M.tracing then M.traceu "access" "add\n" @@ -379,10 +369,48 @@ let may_race (conf,(kind: AccessKind.t),loc,e,a) (conf2,(kind2: AccessKind.t),lo else true -let group_may_race ~ancestor_accs accs = +(** Access sets for race detection and warnings. *) +module WarnAccs = +struct + type t = { + node: AS.t; (** Accesses for current memo. From accesses at trie node corresponding to memo offset. *) + prefix: AS.t; (** Accesses for all prefixes. From accesses to trie node ancestors. *) + type_suffix: AS.t; (** Accesses for all type suffixes. From offset suffixes in other tries. *) + type_suffix_prefix: AS.t; (** Accesses to all prefixes of all type suffixes. *) + } + + let diff w1 w2 = { + node = AS.diff w1.node w2.node; + prefix = AS.diff w1.prefix w2.prefix; + type_suffix = AS.diff w1.type_suffix w2.type_suffix; + type_suffix_prefix = AS.diff w1.type_suffix_prefix w2.type_suffix_prefix; + } + + let union_all w = + AS.union + (AS.union w.node w.prefix) + (AS.union w.type_suffix w.type_suffix_prefix) + + let is_empty w = + AS.is_empty w.node && AS.is_empty w.prefix && AS.is_empty w.type_suffix && AS.is_empty w.type_suffix_prefix + + let empty () = + {node=AS.empty (); prefix=AS.empty (); type_suffix=AS.empty (); type_suffix_prefix=AS.empty ()} + + let pretty () w = + Pretty.dprintf "{node = %a; prefix = %a; type_suffix = %a; type_suffix_prefix = %a}" + AS.pretty w.node AS.pretty w.prefix AS.pretty w.type_suffix AS.pretty w.type_suffix_prefix +end + +let group_may_race (warn_accs:WarnAccs.t) = + if M.tracing then M.tracei "access" "group_may_race %a\n" WarnAccs.pretty warn_accs; (* BFS to traverse one component with may_race edges *) - let rec bfs' ~ancestor_accs ~accs ~todo ~visited = - let may_race_accs ~accs ~todo = + let rec bfs' warn_accs ~todo ~visited = + let todo_all = WarnAccs.union_all todo in + let visited' = AS.union visited todo_all in (* Add all todo accesses to component. *) + let warn_accs' = WarnAccs.diff warn_accs todo in (* Todo accesses don't need to be considered as step targets, because they're already in the component. *) + + let step_may_race ~todo ~accs = (* step from todo to accs if may_race *) AS.fold (fun acc todo' -> AS.fold (fun acc' todo' -> if may_race acc acc' then @@ -392,30 +420,67 @@ let group_may_race ~ancestor_accs accs = ) accs todo' ) todo (AS.empty ()) in - let accs' = AS.diff accs todo in - let ancestor_accs' = AS.diff ancestor_accs todo in - let todo_accs = may_race_accs ~accs:accs' ~todo in - let todo_ancestor_accs = may_race_accs ~accs:ancestor_accs' ~todo:(AS.diff todo ancestor_accs') in - let todo' = AS.union todo_accs todo_ancestor_accs in - let visited' = AS.union visited todo in - if AS.is_empty todo' then - (accs', visited') + (* Undirected graph of may_race checks: + + type_suffix_prefix + | + | + type_suffix --+-- prefix + \ | / + \ | / + node + / \ + \_/ + + Each undirected edge is handled by two opposite step_may_race-s. + All missing edges are checked at other nodes by other group_may_race calls. *) + let todo' : WarnAccs.t = { + node = step_may_race ~todo:todo_all ~accs:warn_accs'.node; + prefix = step_may_race ~todo:(AS.union todo.node todo.type_suffix) ~accs:warn_accs'.prefix; + type_suffix = step_may_race ~todo:(AS.union todo.node todo.prefix) ~accs:warn_accs'.type_suffix; + type_suffix_prefix = step_may_race ~todo:todo.node ~accs:warn_accs'.type_suffix_prefix + } + in + + if WarnAccs.is_empty todo' then + (warn_accs', visited') else - (bfs' [@tailcall]) ~ancestor_accs:ancestor_accs' ~accs:accs' ~todo:todo' ~visited:visited' + (bfs' [@tailcall]) warn_accs' ~todo:todo' ~visited:visited' in - let bfs accs acc = bfs' ~ancestor_accs ~accs ~todo:(AS.singleton acc) ~visited:(AS.empty ()) in - (* repeat BFS to find all components *) - let rec components comps accs = - if AS.is_empty accs then - comps + let bfs warn_accs todo = bfs' warn_accs ~todo ~visited:(AS.empty ()) in + (* repeat BFS to find all components starting from node accesses *) + let rec components comps (warn_accs:WarnAccs.t) = + if AS.is_empty warn_accs.node then + (comps, warn_accs) else ( - let acc = AS.choose accs in - let (accs', comp) = bfs accs acc in + let acc = AS.choose warn_accs.node in + let (warn_accs', comp) = bfs warn_accs {(WarnAccs.empty ()) with node=AS.singleton acc} in let comps' = comp :: comps in - components comps' accs' + components comps' warn_accs' + ) + in + let (comps, warn_accs) = components [] warn_accs in + if M.tracing then M.trace "access" "components %a\n" WarnAccs.pretty warn_accs; + (* repeat BFS to find all prefix-type_suffix-only components starting from prefix accesses (symmetric) *) + let rec components_cross comps ~prefix ~type_suffix = + if AS.is_empty prefix then + comps + else ( + let prefix_acc = AS.choose prefix in + let (warn_accs', comp) = bfs {(WarnAccs.empty ()) with prefix; type_suffix} {(WarnAccs.empty ()) with prefix=AS.singleton prefix_acc} in + if M.tracing then M.trace "access" "components_cross %a\n" WarnAccs.pretty warn_accs'; + let comps' = + if AS.cardinal comp > 1 then + comp :: comps + else + comps (* ignore self-race prefix_acc component, self-race checked at prefix's level *) + in + components_cross comps' ~prefix:warn_accs'.prefix ~type_suffix:warn_accs'.type_suffix ) in - components [] accs + let components_cross = components_cross comps ~prefix:warn_accs.prefix ~type_suffix:warn_accs.type_suffix in + if M.tracing then M.traceu "access" "group_may_race\n"; + components_cross let race_conf accs = assert (not (AS.is_empty accs)); (* group_may_race should only construct non-empty components *) @@ -483,7 +548,7 @@ let print_accesses memo grouped_accs = M.msg_group Success ?loc:group_loc ~category:Race "Memory location %a (safe)" Memo.pretty memo (msgs safe_accs) ) -let warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs memo accs = - let grouped_accs = group_may_race ~ancestor_accs accs in (* do expensive component finding only once *) +let warn_global ~safe ~vulnerable ~unsafe warn_accs memo = + let grouped_accs = group_may_race warn_accs in (* do expensive component finding only once *) incr_summary ~safe ~vulnerable ~unsafe grouped_accs; print_accesses memo grouped_accs diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml index d0dcc428ad..c77d2cd738 100644 --- a/src/util/cilfacade.ml +++ b/src/util/cilfacade.ml @@ -359,6 +359,101 @@ let split_anoncomp_name name = else invalid_arg "Cilfacade.split_anoncomp_name" +(** Pretty-print typsig like typ, because + {!d_typsig} prints with CIL constructors. *) +let rec pretty_typsig_like_typ (nameOpt: Pretty.doc option) () ts = + (* Copied & modified from Cil.defaultCilPrinterClass#pType. *) + let open Pretty in + let name = match nameOpt with None -> nil | Some d -> d in + let printAttributes (a: attributes) = + let pa = d_attrlist () a in + match nameOpt with + | None when not !print_CIL_Input -> + (* Cannot print the attributes in this case because gcc does not + like them here, except if we are printing for CIL. *) + if pa = nil then nil else + text "/*" ++ pa ++ text "*/" + | _ -> pa + in + match ts with + | TSBase t -> dn_type () t + | TSComp (cstruct, cname, a) -> + let su = if cstruct then "struct" else "union" in + text (su ^ " " ^ cname ^ " ") + ++ d_attrlist () a + ++ name + | TSEnum (ename, a) -> + text ("enum " ^ ename ^ " ") + ++ d_attrlist () a + ++ name + | TSPtr (bt, a) -> + (* Parenthesize the ( * attr name) if a pointer to a function or an + array. *) + let (paren: doc option), (bt': typsig) = + match bt with + | TSFun _ | TSArray _ -> Some (text "("), bt + | _ -> None, bt + in + let name' = text "*" ++ printAttributes a ++ name in + let name'' = (* Put the parenthesis *) + match paren with + Some p -> p ++ name' ++ text ")" + | _ -> name' + in + pretty_typsig_like_typ + (Some name'') + () + bt' + + | TSArray (elemt, lo, a) -> + (* ignore the const attribute for arrays *) + let a' = dropAttributes [ "pconst" ] a in + let name' = + if a' == [] then name else + if nameOpt == None then printAttributes a' else + text "(" ++ printAttributes a' ++ name ++ text ")" + in + pretty_typsig_like_typ + (Some (name' + ++ text "[" + ++ (match lo with None -> nil | Some e -> text (Z.to_string e)) + ++ text "]")) + () + elemt + + | TSFun (restyp, args, isvararg, a) -> + let name' = + if a == [] then name else + if nameOpt == None then printAttributes a else + text "(" ++ printAttributes a ++ name ++ text ")" + in + pretty_typsig_like_typ + (Some + (name' + ++ text "(" + ++ (align + ++ + (if args = Some [] && isvararg then + text "..." + else + (if args = None then nil + else if args = Some [] then text "void" + else + let pArg atype = + (pretty_typsig_like_typ None () atype) + in + (docList ~sep:(chr ',' ++ break) pArg) () + (match args with None -> [] | Some args -> args)) + ++ (if isvararg then break ++ text ", ..." else nil)) + ++ unalign) + ++ text ")")) + () + restyp + +(** Pretty-print typsig like typ, because + {!d_typsig} prints with CIL constructors. *) +let pretty_typsig_like_typ = pretty_typsig_like_typ None + (** HashSet of line numbers *) let locs = Hashtbl.create 200 diff --git a/tests/regression/04-mutex/49-type-invariants.c b/tests/regression/04-mutex/49-type-invariants.c index 4f69986478..e6ac17dcd9 100644 --- a/tests/regression/04-mutex/49-type-invariants.c +++ b/tests/regression/04-mutex/49-type-invariants.c @@ -1,4 +1,3 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include diff --git a/tests/regression/04-mutex/49-type-invariants.t b/tests/regression/04-mutex/49-type-invariants.t index 3d3f7442ef..3ddd8f237d 100644 --- a/tests/regression/04-mutex/49-type-invariants.t +++ b/tests/regression/04-mutex/49-type-invariants.t @@ -1,47 +1,47 @@ $ goblint --enable warn.deterministic --enable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:22:3-22:21) - [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:9:10-9:11) - write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:22:3-22:21) - read with [mhp:{tid=[main, t_fun@49-type-invariants.c:21:3-21:40#top]}, thread:[main, t_fun@49-type-invariants.c:21:3-21:40#top]] (conf. 110) (exp: & s.field) (49-type-invariants.c:12:3-12:23) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21) + [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11) + write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#top]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#top]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:22:3-22:21) + write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:22:3-22:21) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:22:3-22:21) - [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:22:3-22:21) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:22:3-22:21) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:22:3-22:21) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:22:3-22:21) - [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:22:3-22:21) + [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:21:3-21:21) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:21:3-21:21) + [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:21:3-21:21) + [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21) $ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:22:3-22:21) - [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:9:10-9:11) - write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:22:3-22:21) - read with [mhp:{tid=[main, t_fun@49-type-invariants.c:21:3-21:40#top]}, thread:[main, t_fun@49-type-invariants.c:21:3-21:40#top]] (conf. 110) (exp: & s.field) (49-type-invariants.c:12:3-12:23) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21) + [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11) + write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#top]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#top]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:22:3-22:21) + write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:22:3-22:21) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:22:3-22:21) - [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:22:3-22:21) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:22:3-22:21) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:22:3-22:21) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:22:3-22:21) - [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:22:3-22:21) + [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:21:3-21:21) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:21:3-21:21) + [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:21:3-21:21) + [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21) diff --git a/tests/regression/04-mutex/77-type-nested-fields.c b/tests/regression/04-mutex/77-type-nested-fields.c index 6f173d6fec..00b21e3fcf 100644 --- a/tests/regression/04-mutex/77-type-nested-fields.c +++ b/tests/regression/04-mutex/77-type-nested-fields.c @@ -1,7 +1,14 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include +// (int) (S) (T) (U) +// \ / \ / \ / +// >f< s t +// \ / \ / +// >f< s +// \ / +// f + struct S { int field; }; diff --git a/tests/regression/04-mutex/77-type-nested-fields.t b/tests/regression/04-mutex/77-type-nested-fields.t new file mode 100644 index 0000000000..738784f5d5 --- /dev/null +++ b/tests/regression/04-mutex/77-type-nested-fields.t @@ -0,0 +1,29 @@ + $ goblint --enable warn.deterministic --enable allglobs 77-type-nested-fields.c + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:31:3-31:20) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:38:3-38:22) + [Warning][Race] Memory location (struct T).s.field (race with conf. 100): + write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) + write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22) + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 1 + total memory locations: 2 + [Success][Race] Memory location (struct S).field (safe): + write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:31:3-31:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:31:3-31:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:31:3-31:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:38:3-38:22) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:38:3-38:22) + [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:38:3-38:22) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:31:3-31:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:31:3-31:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:38:3-38:22) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:38:3-38:22) + [Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:31:3-31:20) + [Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:38:3-38:22) diff --git a/tests/regression/04-mutex/78-type-array.c b/tests/regression/04-mutex/78-type-array.c index cdffe244b9..835f6163a3 100644 --- a/tests/regression/04-mutex/78-type-array.c +++ b/tests/regression/04-mutex/78-type-array.c @@ -1,4 +1,3 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.c b/tests/regression/04-mutex/79-type-nested-fields-deep1.c index ee99c40973..e100404960 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.c +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.c @@ -1,7 +1,14 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include +// (int) (S) (T) (U) +// \ / \ / \ / +// >f< s t +// \ / \ / +// f s +// \ / +// >f< + struct S { int field; }; diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t new file mode 100644 index 0000000000..2e15f83c39 --- /dev/null +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t @@ -0,0 +1,29 @@ + $ goblint --enable warn.deterministic --enable allglobs 79-type-nested-fields-deep1.c + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:36:3-36:20) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:43:3-43:24) + [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): + write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24) + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 1 + total memory locations: 2 + [Success][Race] Memory location (struct S).field (safe): + write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:36:3-36:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:36:3-36:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:36:3-36:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:43:3-43:24) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:43:3-43:24) + [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:43:3-43:24) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:36:3-36:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:36:3-36:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:43:3-43:24) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:43:3-43:24) + [Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:36:3-36:20) + [Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:43:3-43:24) diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.c b/tests/regression/04-mutex/80-type-nested-fields-deep2.c index 646acd9147..4ddd4684f7 100644 --- a/tests/regression/04-mutex/80-type-nested-fields-deep2.c +++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.c @@ -1,7 +1,14 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include +// (int) (S) (T) (U) +// \ / \ / \ / +// f s t +// \ / \ / +// >f< s +// \ / +// >f< + struct S { int field; }; diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.t b/tests/regression/04-mutex/80-type-nested-fields-deep2.t new file mode 100644 index 0000000000..48e726f623 --- /dev/null +++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.t @@ -0,0 +1,29 @@ + $ goblint --enable warn.deterministic --enable allglobs 80-type-nested-fields-deep2.c + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:36:3-36:22) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:43:3-43:24) + [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): + write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + write with [mhp:{tid=[main]; created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24) + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 1 + total memory locations: 2 + [Success][Race] Memory location (struct T).s.field (safe): + write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:36:3-36:22) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:36:3-36:22) + [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:36:3-36:22) + [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:43:3-43:24) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:43:3-43:24) + [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:43:3-43:24) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:36:3-36:22) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:36:3-36:22) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:43:3-43:24) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:43:3-43:24) + [Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:36:3-36:22) + [Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:43:3-43:24) diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.c b/tests/regression/04-mutex/90-distribute-fields-type-1.c new file mode 100644 index 0000000000..062b7421e6 --- /dev/null +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.c @@ -0,0 +1,41 @@ +#include +#include + +// (int) (S) (T) (U) +// \ / \ / \ / +// >f< >s< t +// \ / \ / +// f s +// \ / +// f + +struct S { + int field; +}; + +struct T { + struct S s; +}; + +// struct S s; +// struct T t; + +extern struct S* getS(); +extern struct T* getT(); + +// getS could return the same struct as is contained in getT + +void *t_fun(void *arg) { + // should write to (struct T).s.field in addition to (struct S).field + // but easier to implement the other way around? + getS()->field = 1; // RACE! + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + struct S s1; + getT()->s = s1; // RACE! + return 0; +} diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.t b/tests/regression/04-mutex/90-distribute-fields-type-1.t new file mode 100644 index 0000000000..ba3e3da0ed --- /dev/null +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.t @@ -0,0 +1,31 @@ + $ goblint --enable warn.deterministic --enable allglobs 90-distribute-fields-type-1.c + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:31:3-31:20) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:39:3-39:17) + [Warning][Race] Memory location (struct T).s.field (race with conf. 100): + write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 1 + total memory locations: 3 + [Success][Race] Memory location (struct S).field (safe): + write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + [Success][Race] Memory location (struct T).s (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:31:3-31:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:31:3-31:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:31:3-31:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:39:3-39:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:39:3-39:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:39:3-39:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:31:3-31:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:31:3-31:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:39:3-39:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:39:3-39:17) + [Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:31:3-31:20) + [Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:39:3-39:17) diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.c b/tests/regression/04-mutex/91-distribute-fields-type-2.c new file mode 100644 index 0000000000..01c945f730 --- /dev/null +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.c @@ -0,0 +1,42 @@ +#include +#include + +// (int) >(S)< >(T)< (U) +// \ / \ / \ / +// f s t +// \ / \ / +// f s +// \ / +// f + +struct S { + int field; +}; + +struct T { + struct S s; +}; + +// struct S s; +// struct T t; + +extern struct S* getS(); +extern struct T* getT(); + +// getS could return the same struct as is contained in getT + +void *t_fun(void *arg) { + // should write to (struct T).s.field in addition to (struct S).field + // but easier to implement the other way around? + struct S s1; + *(getS()) = s1; // RACE! + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + struct T t1; + *(getT()) = t1; // RACE! + return 0; +} diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.t b/tests/regression/04-mutex/91-distribute-fields-type-2.t new file mode 100644 index 0000000000..fd544b0b0b --- /dev/null +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.t @@ -0,0 +1,31 @@ + $ goblint --enable warn.deterministic --enable allglobs 91-distribute-fields-type-2.c + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:32:3-32:17) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:40:3-40:17) + [Warning][Race] Memory location (struct T).s (race with conf. 100): + write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 1 + total memory locations: 3 + [Success][Race] Memory location (struct S) (safe): + write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + [Success][Race] Memory location (struct T) (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:32:3-32:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:32:3-32:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:32:3-32:17) + [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:40:3-40:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:40:3-40:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:40:3-40:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:32:3-32:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:32:3-32:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:40:3-40:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:40:3-40:17) + [Error][Imprecise][Unsound] Function definition missing for getS (91-distribute-fields-type-2.c:32:3-32:17) + [Error][Imprecise][Unsound] Function definition missing for getT (91-distribute-fields-type-2.c:40:3-40:17) diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.c b/tests/regression/04-mutex/92-distribute-fields-type-deep.c new file mode 100644 index 0000000000..59fb09a605 --- /dev/null +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.c @@ -0,0 +1,46 @@ +#include +#include + +// (int) (S) (T) (U) +// \ / \ / \ / +// >f< s >t< +// \ / \ / +// f s +// \ / +// f + +struct S { + int field; +}; + +struct T { + struct S s; +}; + +struct U { + struct T t; +}; + +// struct S s; +// struct T t; + +extern struct S* getS(); +extern struct T* getT(); +extern struct U* getU(); + +// getS could return the same struct as is contained in getT + +void *t_fun(void *arg) { + // should write to (struct U).t.s.field in addition to (struct T).s.field + // but easier to implement the other way around? + getS()->field = 1; // RACE! + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + struct T t1; + getU()->t = t1; // RACE! + return 0; +} diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t new file mode 100644 index 0000000000..aefc1520d1 --- /dev/null +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t @@ -0,0 +1,31 @@ + $ goblint --enable warn.deterministic --enable allglobs 92-distribute-fields-type-deep.c + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:36:3-36:20) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:44:3-44:17) + [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): + write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 1 + total memory locations: 3 + [Success][Race] Memory location (struct S).field (safe): + write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + [Success][Race] Memory location (struct U).t (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:36:3-36:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:36:3-36:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:36:3-36:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:44:3-44:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:44:3-44:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:44:3-44:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:36:3-36:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:36:3-36:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:44:3-44:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:44:3-44:17) + [Error][Imprecise][Unsound] Function definition missing for getS (92-distribute-fields-type-deep.c:36:3-36:20) + [Error][Imprecise][Unsound] Function definition missing for getU (92-distribute-fields-type-deep.c:44:3-44:17) diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.c b/tests/regression/04-mutex/93-distribute-fields-type-global.c new file mode 100644 index 0000000000..466d47e7fc --- /dev/null +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.c @@ -0,0 +1,25 @@ +#include +#include + +struct S { + int field; +}; + +struct S s; + +extern struct S* getS(); + +void *t_fun(void *arg) { + printf("%d",getS()->field); // RACE! + + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + struct S s1; + s = s1; // RACE! + return 0; +} + diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t new file mode 100644 index 0000000000..2199c689b1 --- /dev/null +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.t @@ -0,0 +1,25 @@ + $ goblint --enable warn.deterministic --enable allglobs 93-distribute-fields-type-global.c + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (93-distribute-fields-type-global.c:13:3-13:29) + [Warning][Race] Memory location s.field (race with conf. 110): (93-distribute-fields-type-global.c:8:10-8:11) + read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 1 + total memory locations: 3 + [Success][Race] Memory location (struct S).field (safe): + read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + [Success][Race] Memory location s (safe): (93-distribute-fields-type-global.c:8:10-8:11) + write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (93-distribute-fields-type-global.c:13:3-13:29) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (93-distribute-fields-type-global.c:13:3-13:29) + [Info][Unsound] Write to unknown address: privatization is unsound. (93-distribute-fields-type-global.c:13:3-13:29) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (93-distribute-fields-type-global.c:13:3-13:29) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (93-distribute-fields-type-global.c:13:3-13:29) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (93-distribute-fields-type-global.c:13:3-13:29) + [Error][Imprecise][Unsound] Function definition missing for getS (93-distribute-fields-type-global.c:13:3-13:29) diff --git a/tests/regression/04-mutex/90-thread-unsafe_fun_rc.c b/tests/regression/04-mutex/94-thread-unsafe_fun_rc.c similarity index 100% rename from tests/regression/04-mutex/90-thread-unsafe_fun_rc.c rename to tests/regression/04-mutex/94-thread-unsafe_fun_rc.c diff --git a/tests/regression/04-mutex/91-thread-unsafe_fun_nr.c b/tests/regression/04-mutex/95-thread-unsafe_fun_nr.c similarity index 100% rename from tests/regression/04-mutex/91-thread-unsafe_fun_nr.c rename to tests/regression/04-mutex/95-thread-unsafe_fun_nr.c diff --git a/tests/regression/06-symbeq/16-type_rc.c b/tests/regression/06-symbeq/16-type_rc.c index efeb6c768b..e9e7c7972b 100644 --- a/tests/regression/06-symbeq/16-type_rc.c +++ b/tests/regression/06-symbeq/16-type_rc.c @@ -1,6 +1,14 @@ // PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" #include +//>(int)< (S) (T) (U) +// \ / \ / \ / +// >f< s t +// \ / \ / +// f s +// \ / +// f + struct s { int datum; pthread_mutex_t mutex; diff --git a/tests/regression/06-symbeq/16-type_rc.t b/tests/regression/06-symbeq/16-type_rc.t index 78c293b7ef..06a3b314a4 100644 --- a/tests/regression/06-symbeq/16-type_rc.t +++ b/tests/regression/06-symbeq/16-type_rc.t @@ -1,22 +1,22 @@ Disable info messages because race summary contains (safe) memory location count, which is different on Linux and OSX. $ goblint --enable warn.deterministic --disable warn.info --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" 16-type_rc.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:13:3-13:15) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:24:3-24:16) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:25:3-25:16) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:28:3-28:9) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:21:3-21:15) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:32:3-32:16) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:33:3-33:16) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:36:3-36:9) [Warning][Race] Memory location (struct s).datum (race with conf. 100): - write with [mhp:{tid=[main, t_fun@16-type_rc.c:27:3-27:37#top]}, thread:[main, t_fun@16-type_rc.c:27:3-27:37#top]] (conf. 100) (exp: & s->datum) (16-type_rc.c:13:3-13:15) - write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:27:3-27:37#top]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:28:3-28:9) - [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:12:12-12:24) - [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:23:3-23:14) + write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#top]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#top]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:35:3-35:37#top]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) + [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24) + [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14) $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs 16-type_rc.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:13:3-13:15) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:24:3-24:16) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:25:3-25:16) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:28:3-28:9) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:21:3-21:15) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:32:3-32:16) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:33:3-33:16) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:36:3-36:9) [Success][Race] Memory location (struct s).datum (safe): - write with [mhp:{tid=[main, t_fun@16-type_rc.c:27:3-27:37#top]}, thread:[main, t_fun@16-type_rc.c:27:3-27:37#top]] (conf. 100) (exp: & s->datum) (16-type_rc.c:13:3-13:15) - [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:12:12-12:24) - [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:23:3-23:14) + write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#top]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#top]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24) + [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14)