Merge pull request #1170 from goblint/acc-record

Use record as `Access.A` type instead of a quintuple

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
 

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,28 +349,26 @@ 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 =
 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