Skip to content

Commit

Permalink
Merge pull request #1136 from goblint/access-distr-outer
Browse files Browse the repository at this point in the history 
Make access outer distribution lazy
  • Loading branch information
@sim642
sim642 authored Sep 12, 2023
2 parents 70cd4e8 + 4e1cf15 commit 8c8fd28
Show file tree
Hide file tree
Showing 24 changed files with 831 additions and 112 deletions.
205 changes: 189 additions & 16 deletions src/analyses/raceAnalysis.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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 =
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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 ->
Expand All @@ -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
Expand All @@ -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
Expand Down
Loading

0 comments on commit 8c8fd28

Please sign in to comment.