Merge pull request #1089 from goblint/access-distr

Use TrieDomain to distribute accesses to contained fields

src/analyses/raceAnalysis.ml

@@ -12,25 +12,61 @@ struct
   let name () = "race"
 
   (* Two global invariants:
-     1. (lval, type) -> accesses  --  used for warnings
-     2. varinfo -> set of (lval, type)  --  used for IterSysVars Global *)
+     1. memoroot -> (offset -> accesses)  --  used for warnings
+     2. varinfo -> set of memo  --  used for IterSysVars Global *)
 
   module V =
   struct
-    include Printable.Either (Access.Memo) (CilType.Varinfo)
+    include Printable.Either (Access.MemoRoot) (CilType.Varinfo)
     let name () = "race"
     let access x = `Left x
     let vars x = `Right x
     let is_write_only _ = true
   end
 
   module MemoSet = SetDomain.Make (Access.Memo)
+
+  module OneOffset =
+  struct
+    include Printable.StdLeaf
+    type t =
+      | Field of CilType.Fieldinfo.t
+      | Index
+    [@@deriving eq, ord, hash, to_yojson]
+
+    let name () = "oneoffset"
+
+    let show = function
+      | Field f -> CilType.Fieldinfo.show f
+      | Index -> "?"
+
+    include Printable.SimpleShow (struct
+        type nonrec t = t
+        let show = show
+      end)
+
+    let to_offset : t -> Offset.Unit.t = function
+      | Field f -> `Field (f, `NoOffset)
+      | Index -> `Index ((), `NoOffset)
+  end
+
+  module OffsetTrie =
+  struct
+    include TrieDomain.Make (OneOffset) (Access.AS)
+
+    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))
+  end
+
   module G =
   struct
-    include Lattice.Lift2 (Access.AS) (MemoSet) (Printable.DefaultNames)
+    include Lattice.Lift2 (OffsetTrie) (MemoSet) (Printable.DefaultNames)
 
     let access = function
-      | `Bot -> Access.AS.bot ()
+      | `Bot -> OffsetTrie.bot ()
       | `Lifted1 x -> x
       | _ -> failwith "Race.access"
     let vars = function
@@ -58,21 +94,32 @@ struct
     | _ ->
       ()
 
-  let side_access ctx (conf, w, loc, e, a) memo =
+  let side_access ctx (conf, w, loc, e, a) ((memoroot, offset) as memo) =
     if !AnalysisState.should_warn then
-      ctx.sideg (V.access memo) (G.create_access (Access.AS.singleton (conf, w, loc, e, a)));
+      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (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 memo -> (* accesses *)
+        | `Left g' -> (* accesses *)
           (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *)
-          let accs = G.access (ctx.global g) 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 memo) accs
+          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 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
+            )
+          in
+          distribute_inner `NoOffset trie (Access.AS.empty ())
         | `Right _ -> (* vars *)
           ()
       end
@@ -99,7 +146,7 @@ struct
       in
       let add_access_struct conf ci =
         let a = part_access None in
-        Access.add_distribute_inner (side_access octx (conf, kind, loc, e, a)) (`Type (TComp (ci, [])), `NoOffset)
+        Access.add_one (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

src/domains/access.ml

@@ -81,11 +81,34 @@ let reset () =
 type acc_typ = [ `Type of CilType.Typ.t | `Struct of CilType.Compinfo.t * Offset.Unit.t ] [@@deriving eq, ord, hash]
 (** Old access type inferred from an expression. *)
 
+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. *)
+
+  let name () = "memoroot"
+
+  let pretty () vt =
+    (* Imitate old printing for now *)
+    match vt with
+    | `Var v -> Pretty.dprintf "%a@@%a" CilType.Varinfo.pretty v CilType.Location.pretty v.vdecl
+    | `Type (TComp (c, _)) -> Pretty.dprintf "(struct %s)" c.cname
+    | `Type t -> Pretty.dprintf "(%a)" CilType.Typ.pretty t
+
+  include Printable.SimplePretty (
+    struct
+      type nonrec t = t
+      let pretty = pretty
+    end
+    )
+end
+
 (** Memory location of an access. *)
 module Memo =
 struct
   include Printable.StdLeaf
-  type t = [`Var of CilType.Varinfo.t | `Type of CilType.Typ.t] * Offset.Unit.t [@@deriving eq, ord, hash]
+  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"
@@ -189,48 +212,17 @@ let add_one side memo: unit =
   if not ignorable then
     side memo
 
-(** Find all nested offsets in type. *)
-let rec nested_offsets ty: Offset.Unit.t list =
-  (* TODO: is_ignorable_type outside of TComp if ty itself is ignorable? *)
-  match unrollType ty with
-  | TComp (ci,_)   ->
-    let one_field fld =
-      if is_ignorable_type fld.ftype then
-        []
-      else
-        List.map (fun x -> `Field (fld,x)) (nested_offsets fld.ftype)
-    in
-    List.concat_map one_field ci.cfields
-  | TArray (t,_,_) ->
-    List.map (fun x -> `Index ((), x)) (nested_offsets t)
-  | _ -> [`NoOffset]
-
-(** Distribute access to contained fields. *)
-let add_distribute_inner side memo: unit =
-  if M.tracing then M.tracei "access" "add_distribute_inner %a\n" Memo.pretty memo;
-  begin match Memo.type_of memo with
-    | t ->
-      let oss = nested_offsets t in
-      List.iter (fun os ->
-          add_one side (Memo.add_offset memo os) (* distribute to all nested offsets *)
-        ) oss
-    | exception Offset.Type_of_error _ -> (* `Var has alloc variable with void type *)
-      if M.tracing then M.trace "access" "Offset.Type_of_error\n";
-      add_one side memo
-  end;
-  if M.tracing then M.traceu "access" "add_distribute_inner\n"
-
 (** 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
   if M.tracing then M.tracei "access" "add_distribute_outer %a\n" Memo.pretty memo;
-  add_distribute_inner side memo; (* distribute to inner offsets of type *)
+  add_one side memo;
 
-  (* distribute to inner offsets of variables of the type *)
+  (* distribute to variables of the type *)
   let ts = typeSig t in
   let vars = TSH.find_all typeVar ts in
   List.iter (fun v ->
-      add_distribute_inner side (`Var v, o) (* same offset, but on variable *)
+      add_one side (`Var v, o) (* same offset, but on variable *)
     ) vars;
 
   (* recursively distribute to fields containing the type *)
@@ -248,7 +240,7 @@ let add side e voffs =
     | 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_distribute_inner side memo (* distribute to inner offsets *)
+      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 *)
@@ -387,26 +379,31 @@ let may_race (conf,(kind: AccessKind.t),loc,e,a) (conf2,(kind2: AccessKind.t),lo
   else
     true
 
-let group_may_race accs =
+let group_may_race ~ancestor_accs accs =
   (* BFS to traverse one component with may_race edges *)
-  let rec bfs' accs visited todo =
-    let accs' = AS.diff accs todo in
-    let todo' = AS.fold (fun acc todo' ->
-        AS.fold (fun acc' todo' ->
-            if may_race acc acc' then
-              AS.add acc' todo'
-            else
-              todo'
-          ) accs' todo'
-      ) todo (AS.empty ())
+  let rec bfs' ~ancestor_accs ~accs ~todo ~visited =
+    let may_race_accs ~accs ~todo =
+      AS.fold (fun acc todo' ->
+          AS.fold (fun acc' todo' ->
+              if may_race acc acc' then
+                AS.add acc' todo'
+              else
+                todo'
+            ) 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')
     else
-      (bfs' [@tailcall]) accs' visited' todo'
+      (bfs' [@tailcall]) ~ancestor_accs:ancestor_accs' ~accs:accs' ~todo:todo' ~visited:visited'
   in
-  let bfs accs acc = bfs' accs (AS.empty ()) (AS.singleton acc) 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
@@ -435,7 +432,7 @@ let race_conf accs =
 let is_all_safe = ref true
 
 (* Commenting your code is for the WEAK! *)
-let incr_summary safe vulnerable unsafe grouped_accs =
+let incr_summary ~safe ~vulnerable ~unsafe grouped_accs =
   (* ignore(printf "Checking safety of %a:\n" d_memo (ty,lv)); *)
   let safety =
     grouped_accs
@@ -482,7 +479,7 @@ let print_accesses memo grouped_accs =
         M.msg_group Success ~category:Race "Memory location %a (safe)" Memo.pretty memo (msgs safe_accs)
     )
 
-let warn_global safe vulnerable unsafe memo accs =
-  let grouped_accs = group_may_race accs in (* do expensive component finding only once *)
-  incr_summary safe vulnerable unsafe grouped_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 *)
+  incr_summary ~safe ~vulnerable ~unsafe grouped_accs;
   print_accesses memo grouped_accs

src/domains/trieDomain.ml

@@ -0,0 +1,19 @@
+(** Trie domains. *)
+
+module Make (Key: MapDomain.Groupable) (Value: Lattice.S) =
+struct
+  module rec Trie:
+  sig
+    type key = Key.t
+    type value = Value.t
+    include Lattice.S with type t = value * ChildMap.t
+  end =
+  struct
+    type key = Key.t
+    type value = Value.t
+    include Lattice.Prod (Value) (ChildMap)
+  end
+  and ChildMap: MapDomain.S with type key = Key.t and type value = Trie.t = MapDomain.MapBot (Key) (Trie)
+
+  include Trie
+end

src/goblint_lib.ml

@@ -177,6 +177,7 @@ module Lattice = Lattice
 module BoolDomain = BoolDomain
 module SetDomain = SetDomain
 module MapDomain = MapDomain
+module TrieDomain = TrieDomain
 module DisjointDomain = DisjointDomain
 module HoareDomain = HoareDomain
 module PartitionDomain = PartitionDomain

tests/regression/04-mutex/84-distribute-fields-1.c

@@ -0,0 +1,23 @@
+#include <pthread.h>
+#include <stdlib.h>
+
+struct S {
+  int data;
+  int data2;
+};
+
+struct S s;
+
+void *t_fun(void *arg) {
+  s.data = 1; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  struct S s2;
+  s = s2; // RACE!
+  pthread_join (id, NULL);
+  return 0;
+}

tests/regression/04-mutex/84-distribute-fields-1.t

@@ -0,0 +1,15 @@
+  $ goblint --enable warn.deterministic --enable allglobs 84-distribute-fields-1.c
+  [Warning][Race] Memory location s.data@84-distribute-fields-1.c:9:10-9:11 (race with conf. 110):
+    write with [mhp:{tid=[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}, thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]] (conf. 110)  (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13)
+    write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}}, thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 2
+  [Success][Race] Memory location s@84-distribute-fields-1.c:9:10-9:11 (safe):
+    write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}}, thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 8
+    dead: 0
+    total lines: 8

tests/regression/04-mutex/85-distribute-fields-2.c

@@ -0,0 +1,29 @@
+#include <pthread.h>
+#include <stdlib.h>
+
+struct S {
+  int data;
+  int data2;
+};
+
+struct T {
+  struct S s;
+  struct S s2;
+  int data3;
+};
+
+struct T t;
+
+void *t_fun(void *arg) {
+  t.s.data = 1; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  struct S s2;
+  t.s = s2; // RACE!
+  pthread_join (id, NULL);
+  return 0;
+}

tests/regression/04-mutex/85-distribute-fields-2.t

@@ -0,0 +1,15 @@
+  $ goblint --enable warn.deterministic --enable allglobs 85-distribute-fields-2.c
+  [Warning][Race] Memory location t.s.data@85-distribute-fields-2.c:15:10-15:11 (race with conf. 110):
+    write with [mhp:{tid=[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}, thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]] (conf. 110)  (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15)
+    write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}}, thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 2
+  [Success][Race] Memory location t.s@85-distribute-fields-2.c:15:10-15:11 (safe):
+    write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}}, thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 8
+    dead: 0
+    total lines: 8