Refactor and fix race access distribution

src/analyses/accessAnalysis.ml

@@ -42,13 +42,15 @@ struct
       + [deref=true], [reach=false] - Access [exp] by dereferencing once (may-point-to), used for lval writes and shallow special accesses.
       + [deref=true], [reach=true] - Access [exp] by dereferencing transitively (reachable), used for deep special accesses. *)
   let access_one_top ?(force=false) ?(deref=false) ctx (kind: AccessKind.t) reach exp =
-    if M.tracing then M.traceli "access" "access_one_top %a %b %a:\n" AccessKind.pretty kind reach d_exp exp;
+    if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)\n" CilType.Exp.pretty exp AccessKind.pretty kind reach deref;
     if force || !collect_local || !emit_single_threaded || ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) then (
       if deref then
         do_access ctx kind reach exp;
-      Access.distribute_access_exp (do_access ctx Read false) exp
+      if M.tracing then M.tracei "access" "distribute_access_exp\n";
+      Access.distribute_access_exp (do_access ctx Read false) exp;
+      if M.tracing then M.traceu "access" "distribute_access_exp\n";
     );
-    if M.tracing then M.traceu "access" "access_one_top %a %b %a\n" AccessKind.pretty kind reach d_exp exp
+    if M.tracing then M.traceu "access" "access_one_top\n"
 
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()

src/analyses/raceAnalysis.ml

@@ -15,27 +15,26 @@ struct
      1. (lval, type) -> accesses  --  used for warnings
      2. varinfo -> set of (lval, type)  --  used for IterSysVars Global *)
 
-  module V0 = Printable.Prod (Access.LVOpt) (Access.T)
   module V =
   struct
-    include Printable.Either (V0) (CilType.Varinfo)
+    include Printable.Either (Access.Memo) (CilType.Varinfo)
     let name () = "race"
     let access x = `Left x
     let vars x = `Right x
     let is_write_only _ = true
   end
 
-  module V0Set = SetDomain.Make (V0)
+  module MemoSet = SetDomain.Make (Access.Memo)
   module G =
   struct
-    include Lattice.Lift2 (Access.AS) (V0Set) (Printable.DefaultNames)
+    include Lattice.Lift2 (Access.AS) (MemoSet) (Printable.DefaultNames)
 
     let access = function
       | `Bot -> Access.AS.bot ()
       | `Lifted1 x -> x
       | _ -> failwith "Race.access"
     let vars = function
-      | `Bot -> V0Set.bot ()
+      | `Bot -> MemoSet.bot ()
       | `Lifted2 x -> x
       | _ -> failwith "Race.vars"
     let create_access access = `Lifted1 access
@@ -51,41 +50,34 @@ struct
     vulnerable := 0;
     unsafe := 0
 
-  let side_vars ctx lv_opt ty =
-    match lv_opt with
-    | Some (v, _) ->
+  let side_vars ctx memo =
+    match memo with
+    | (`Var v, _) ->
       if !AnalysisState.should_warn then
-        ctx.sideg (V.vars v) (G.create_vars (V0Set.singleton (lv_opt, ty)))
-    | None ->
+        ctx.sideg (V.vars v) (G.create_vars (MemoSet.singleton memo))
+    | _ ->
       ()
 
-  let side_access ctx ty lv_opt (conf, w, loc, e, a) =
-    let ty =
-      if Option.is_some lv_opt then
-        `Type Cil.voidType (* avoid unsound type split for alloc variables *)
-      else
-        ty
-    in
+  let side_access ctx (conf, w, loc, e, a) memo =
     if !AnalysisState.should_warn then
-      ctx.sideg (V.access (lv_opt, ty)) (G.create_access (Access.AS.singleton (conf, w, loc, e, a)));
-    side_vars ctx lv_opt ty
+      ctx.sideg (V.access memo) (G.create_access (Access.AS.singleton (conf, w, loc, e, a)));
+    side_vars ctx memo
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
     | WarnGlobal g ->
       let g: V.t = Obj.obj g in
       begin match g with
-        | `Left g' -> (* accesses *)
+        | `Left memo -> (* accesses *)
           (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *)
           let accs = G.access (ctx.global g) in
-          let (lv, ty) = g' in
-          let mem_loc_str = GobPretty.sprint Access.d_memo (ty, lv) in
-          Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global safe vulnerable unsafe g') accs
+          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 memo) accs
         | `Right _ -> (* vars *)
           ()
       end
     | IterSysVars (Global g, vf) ->
-      V0Set.iter (fun v ->
+      MemoSet.iter (fun v ->
           vf (Obj.repr (V.access v))
         ) (G.vars (ctx.global (V.vars g)))
     | _ -> Queries.Result.top q
@@ -96,17 +88,18 @@ struct
       (* must use original (pre-assign, etc) ctx queries *)
       let conf = 110 in
       let module LS = Queries.LS in
-      let part_access (vo:varinfo option) (oo: offset option): MCPAccess.A.t =
+      let part_access (vo:varinfo option): MCPAccess.A.t =
         (*partitions & locks*)
         Obj.obj (octx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind})))
       in
-      let add_access conf vo oo =
-        let a = part_access vo oo in
-        Access.add (side_access octx) e kind conf vo oo a;
+      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;
       in
       let add_access_struct conf ci =
-        let a = part_access None None in
-        Access.add_struct (side_access octx) e kind conf (`Struct (ci,`NoOffset)) None a
+        let a = part_access None in
+        Access.add_distribute_inner (side_access octx (conf, kind, loc, e, a)) (`Type (TComp (ci, [])), `NoOffset)
       in
       let has_escaped g = octx.ask (Queries.MayEscape g) in
       (* The following function adds accesses to the lval-set ls
@@ -118,9 +111,9 @@ struct
         let f (var, offs) =
           let coffs = Offset.Exp.to_cil offs in
           if CilType.Varinfo.equal var dummyFunDec.svar then
-            add_access conf None (Some coffs)
+            add_access conf None
           else
-            add_access conf (Some var) (Some coffs)
+            add_access conf (Some (var, coffs))
         in
         LS.iter f ls
       in
@@ -147,7 +140,7 @@ struct
           end;
           on_lvals ls !includes_uk
         | _ ->
-          add_access (conf - 60) None None
+          add_access (conf - 60) None
       end;
       ctx.local
     | _ ->

src/cdomains/offset.ml

@@ -146,7 +146,8 @@ struct
           let s = GobPretty.sprintf "Addr.type_offset: field %s not found in type %a" f.fname d_plaintype t in
           raise (Type_of_error (t, s))
       in type_of ~base:fi.ftype o
-    | TComp _, `Index (_,o) -> type_of ~base:t o (* this happens (hmmer, perlbench). safe? *)
+    (* TODO: Why? Imprecise on zstd-thread-pool regression tests. *)
+    (* | TComp _, `Index (_,o) -> type_of ~base:t o (* this happens (hmmer, perlbench). safe? *) *)
     | t,o ->
       let s = GobPretty.sprintf "Addr.type_offset: could not follow offset in type. type: %a, offset: %a" d_plaintype t pretty o in
       raise (Type_of_error (t, s))