diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 74a98af6be..d1d608ae06 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -225,9 +225,9 @@ struct | _ -> () - let side_access ctx (conf, w, loc, e, a) ((memoroot, offset) as memo) = + let side_access ctx acc ((memoroot, offset) as memo) = if !AnalysisState.should_warn then - ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton (conf, w, loc, e, a))))); + ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton acc)))); side_vars ctx memo (** Side-effect empty access set for prefix-type_suffix race checking. *) @@ -302,24 +302,24 @@ struct ) (G.vars (ctx.global (V.vars g))) | _ -> Queries.Result.top q - let event ctx e octx = - match e with - | Events.Access {exp=e; lvals; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *) + let event ctx exp octx = + match exp with + | Events.Access {exp; lvals; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *) (* must use original (pre-assign, etc) ctx queries *) let conf = 110 in let module LS = Queries.LS in let part_access (vo:varinfo option): MCPAccess.A.t = (*partitions & locks*) - Obj.obj (octx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind}))) + Obj.obj (octx.ask (PartAccess (Memory {exp; var_opt=vo; kind}))) in - let loc = Option.get !Node.current_node in + let node = Option.get !Node.current_node in let add_access conf voffs = - let a = part_access (Option.map fst voffs) in - Access.add ~side:(side_access octx (conf, kind, loc, e, a)) ~side_empty:(side_access_empty octx) e voffs; + let acc = part_access (Option.map fst voffs) in + Access.add ~side:(side_access octx {conf; kind; node; exp; acc}) ~side_empty:(side_access_empty octx) exp voffs; in let add_access_struct conf ci = - let a = part_access None in - Access.add_one ~side:(side_access octx (conf, kind, loc, e, a)) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset) + let acc = part_access None in + Access.add_one ~side:(side_access octx {conf; kind; node; exp; acc}) (`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 @@ -345,7 +345,7 @@ struct (* the case where the points-to set is non top and contains unknown values *) let includes_uk = ref false in (* now we need to access all fields that might be pointed to: is this correct? *) - begin match octx.ask (ReachableUkTypes e) with + begin match octx.ask (ReachableUkTypes exp) with | ts when Queries.TS.is_top ts -> includes_uk := true | ts -> @@ -370,12 +370,13 @@ struct (* perform shallow and deep invalidate according to Library descriptors *) let desc = LibraryFunctions.find f in if List.mem LibraryDesc.ThreadUnsafe desc.attrs then ( - let e = Lval (Var f, NoOffset) in + let exp = Lval (Var f, NoOffset) in let conf = 110 in - let loc = Option.get !Node.current_node in + let kind = AccessKind.Call in + let node = Option.get !Node.current_node in let vo = Some f in - let a = Obj.obj (ctx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind=Call}))) in - side_access ctx (conf, Call, loc, e, a) ((`Var f), `NoOffset) ; + let acc = Obj.obj (ctx.ask (PartAccess (Memory {exp; var_opt=vo; kind}))) in + side_access ctx {conf; kind; node; exp; acc} ((`Var f), `NoOffset) ; ); ctx.local diff --git a/src/domains/access.ml b/src/domains/access.ml index 675d1c2e72..83903ba355 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -329,12 +329,18 @@ and distribute_access_type f = function module A = struct include Printable.Std - type t = int * AccessKind.t * Node.t * CilType.Exp.t * MCPAccess.A.t [@@deriving eq, ord, hash] + type t = { + conf : int; + kind : AccessKind.t; + node : Node.t; + exp : CilType.Exp.t; + acc : MCPAccess.A.t; + } [@@deriving eq, ord, hash] let name () = "access" - let pretty () (conf, kind, node, e, lp) = - Pretty.dprintf "%d, %a, %a, %a, %a" conf AccessKind.pretty kind CilType.Location.pretty (Node.location node) CilType.Exp.pretty e MCPAccess.A.pretty lp + let pretty () {conf; kind; node; exp; acc} = + Pretty.dprintf "%d, %a, %a, %a, %a" conf AccessKind.pretty kind CilType.Location.pretty (Node.location node) CilType.Exp.pretty exp MCPAccess.A.pretty acc include Printable.SimplePretty ( struct @@ -343,10 +349,8 @@ struct end ) - let conf (conf, _, _, _, _) = conf - - let relift (conf, kind, node, e, a) = - (conf, kind, node, e, MCPAccess.A.relift a) + let relift {conf; kind; node; exp; acc} = + {conf; kind; node; exp; acc = MCPAccess.A.relift acc} end module AS = @@ -354,17 +358,17 @@ struct include SetDomain.Make (A) let max_conf accs = - accs |> elements |> List.map A.conf |> (List.max ~cmp:Int.compare) + accs |> elements |> List.map (fun {A.conf; _} -> conf) |> (List.max ~cmp:Int.compare) end (* Check if two accesses may race and if yes with which confidence *) -let may_race (conf,(kind: AccessKind.t),loc,e,a) (conf2,(kind2: AccessKind.t),loc2,e2,a2) = +let may_race A.{kind; acc; _} A.{kind=kind2; acc=acc2; _} = if kind = Read && kind2 = Read then false (* two read/read accesses do not race *) else if not (get_bool "ana.race.free") && (kind = Free || kind2 = Free) then false - else if not (MCPAccess.A.may_race a a2) then + else if not (MCPAccess.A.may_race acc acc2) then false (* analysis-specific information excludes race *) else true @@ -487,7 +491,7 @@ let race_conf accs = if AS.cardinal accs = 1 then ( (* singleton component *) let acc = AS.choose accs in if may_race acc acc then (* self-race *) - Some (A.conf acc) + Some (acc.conf) else None ) @@ -516,9 +520,8 @@ let print_accesses memo grouped_accs = let allglobs = get_bool "allglobs" in let race_threshold = get_int "warn.race-threshold" in let msgs race_accs = - let h (conf,kind,node,e,a) = - let d_msg () = dprintf "%a with %a (conf. %d)" AccessKind.pretty kind MCPAccess.A.pretty a conf in - let doc = dprintf "%t (exp: %a)" d_msg d_exp e in + let h A.{conf; kind; node; exp; acc} = + let doc = dprintf "%a with %a (conf. %d) (exp: %a)" AccessKind.pretty kind MCPAccess.A.pretty acc conf d_exp exp in (doc, Some (Messages.Location.Node node)) in AS.elements race_accs