Skip to content

Commit 2f05849

Browse files
authored
provides the new liveness analysis (#1446)
* provides the new liveness analysis The new liveness analysis works with functions in the SSA and non-SSA form and provides the extended interface that gives an easy access to live-ins, liveouts, live and dead blocks. The phi-nodes semantics is clearly specified and the `Blk.free_vars` function is updated to be in line with the semantics of the SSA nodes. The printing function of the phi-nodes is also updated. To reflect that the phi-node is not an assignment but a selection, we use the `<-` symbol instead of `:=` to separate the asignment operand from the right-hand side. * refines the definition of live-out
1 parent 0f32782 commit 2f05849

File tree

6 files changed

+311
-70
lines changed

6 files changed

+311
-70
lines changed

lib/bap/bap.mli

Lines changed: 147 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -7682,7 +7682,6 @@ module Std : sig
76827682
val is_barrier : jump -> bool
76837683
end
76847684

7685-
76867685
(** A set of subroutines.
76877686
76887687
A partition of a whole program control-flow graph into a
@@ -8040,6 +8039,151 @@ module Std : sig
80408039
include Regular.S with type t := t
80418040
end
80428041

8042+
(** Live Variables.
8043+
8044+
Computes the set of live variables for each block in a
8045+
subroutine, taking into account subroutine arguments.
8046+
8047+
A variable [v] is {i live} at a program point [x] if there exists a
8048+
path from [x] to a use of [v] that doesn't go through a
8049+
definition of [v].
8050+
8051+
This module computes liveness on the block granularity, which
8052+
gives rise to the following notions.
8053+
8054+
A variable is {i live-in} at a basic block [x] if it is live at the
8055+
begining of the block [x].
8056+
8057+
A variable is {i live-out} at a basic block [x] if it is live on
8058+
any of the outcoming edges of [x].
8059+
8060+
A variable is {i live-through} at a basic block [x] if it is
8061+
both live-in and live-out at it.
8062+
8063+
{3 Liveness in the SSA form}
8064+
8065+
The algorithm works with the SSA form. From the perspective of
8066+
liveness, the phi-nodes define their right-hand sides on the
8067+
edges incoming from the corresponding blocks. More formally, for
8068+
a phi-node at block [b0], [x0 := phi([b1,x1; b2,x2;...;bN,xN])],
8069+
the defined variable [x0] is considered to be defined at blocks
8070+
[bi] and the variable [xi] live-out of basic block [bi], for
8071+
[0 < i <= N].
8072+
8073+
Intuitively, this can be visualized as if the following program,
8074+
8075+
{v
8076+
8077+
b1:
8078+
x.1 := 1
8079+
goto b3
8080+
8081+
b2:
8082+
x.2 := 2
8083+
goto b3
8084+
8085+
b3:
8086+
x.3 <- phi([b1,x1]; [b2, x2])
8087+
...
8088+
v}
8089+
8090+
is rewritten to an equivalent (but not in SSA) program,
8091+
8092+
{v
8093+
8094+
b1:
8095+
x.1 := 1
8096+
x.3 := x1
8097+
goto b3
8098+
8099+
b2:
8100+
x.2 := 2
8101+
x.3 := x2
8102+
goto b3
8103+
8104+
b3:
8105+
...
8106+
v}
8107+
8108+
That means that a variable defined by a phi-node in a block [x]
8109+
could be live-in at the block [x].
8110+
8111+
The {!Live.defs} and {!Live.uses} includes the variables from
8112+
the corresponding phi-nodes, e.g., [Live.defs b1] will is
8113+
[{x1,x3}] and [Live.uses b1] is [{x1}].
8114+
8115+
@since 2.5.0
8116+
@before 2.5.0 see {!Sub.compute_liveness} *)
8117+
module Live : sig
8118+
type t
8119+
8120+
(** [compute sub] computes the subroutine liveness information.
8121+
8122+
Variables specified by [keep] will be kept live at the exit
8123+
from the function. In addition to the variables in [keep],
8124+
all free variables used by in and in/out arguments of the
8125+
subroutine will be kept alive at the exit.*)
8126+
val compute : ?keep:Var.Set.t -> sub term -> t
8127+
8128+
(** [vars live] the variables that are live in the subroutine.
8129+
8130+
The set of variables that are live-in on the entry block of
8131+
the subroutine that was used to compute [live]. The live
8132+
variables of the subroutine also called free variables or
8133+
upper-exposed variables. They may be used in the subroutine
8134+
before they are assigned. *)
8135+
val vars : t -> Var.Set.t
8136+
8137+
(** [ins live blk] the set of live-in variables at [blk].
8138+
8139+
The set of variables that are live at the entry to the basic
8140+
block [blk].
8141+
8142+
Returns an empty set if [blk] doesn't belong to the [sub] graph.
8143+
*)
8144+
val ins : t -> tid -> Var.Set.t
8145+
8146+
(** [outs live blk] the set of live-outs variables at [blk].
8147+
8148+
The set of variables that are live at the exist from the basic
8149+
block [blk].
8150+
8151+
Returns an empty set if [blk] doesn't belong to the [sub] graph.*)
8152+
val outs : t -> tid -> Var.Set.t
8153+
8154+
(** [blks live var] the set of blks where [var] is live-in. *)
8155+
val blks : t -> var -> Set.M(Tid).t
8156+
8157+
(** [defs live blk] the set of variables defined by [blk].
8158+
8159+
Aka the {i KILL} set, i.e., the set of variables whose
8160+
liveness is killed in the block [blk]. *)
8161+
val defs : t -> tid -> Var.Set.t
8162+
8163+
(** [uses live blk] the set of variables used by [blk].
8164+
8165+
Aka the {i GEN} set, i.e., the set of variables generated by
8166+
the block [blk]. *)
8167+
val uses : t -> tid -> Var.Set.t
8168+
8169+
(** [fold live ~init ~f] folds over live-ins of blocks.
8170+
8171+
Applies [f] to live-in set of variables of each block of the
8172+
subroutine.
8173+
8174+
Note, pseudo start and exit nodes are not folded over. *)
8175+
val fold : t -> init:'a -> f:('a -> tid -> Var.Set.t -> 'a) -> 'a
8176+
8177+
(** [solution live] returns the fixed point solution.
8178+
8179+
The solution is the mapping from blocks to their live-outs.*)
8180+
val solution : t -> (tid, Var.Set.t) Solution.t
8181+
8182+
8183+
(** [pp ppf live] prints the live-in sets of each basic block. *)
8184+
val pp : Format.formatter -> t -> unit
8185+
end
8186+
80438187
(** IR language term.
80448188
80458189
Term is a building block of the
@@ -8530,22 +8674,17 @@ module Std : sig
85308674
[Graphs.Tid.start] node.
85318675
85328676
When the subroutine is in the SSA form then the phi-nodes have
8533-
the following semantics. For a phi-node at block [b0],
8534-
[x0 := phi([b1,x1; b2,x2;...;bN,xN])], the defined variable
8535-
[x0] is considered to be at the entry of [b0], i.e., [x0] is
8536-
live-in of [b0], and the variable [xi] is live-out of basic
8537-
block [bi], for [i > 0].
8677+
the following semantics.
85388678
85398679
Informally, a phi-node defines the values on the corresponding
85408680
edges of the predecessors.
85418681
8542-
85438682
@since 2.1
85448683
@since 2.5.0 supports SSA
85458684
@before 2.5.0 the subroutine must not be in the SSA form
85468685
*)
85478686
val compute_liveness : t -> (tid, Var.Set.t) Solution.t
8548-
8687+
[@@deprecated "[since 2022-03] use Live.compute"]
85498688

85508689
(** [flatten sub] returns [sub] in flattened form in which all
85518690
operands are trivial.

lib/bap_sema/bap_sema.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,7 @@ module Std = struct
4141
let flatten = Flatten.flatten_sub
4242
end
4343

44+
module Live = FV.Live
4445
module Taint = Bap_sema_taint
4546

4647
module Graphs = struct

lib/bap_sema/bap_sema_free_vars.ml

Lines changed: 108 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -7,64 +7,123 @@ module Ssa = Bap_sema_ssa
77
module G = Bap_tid_graph
88

99
let (++) = Set.union and (--) = Set.diff
10-
let blk = G.Node.label
1110

1211
let ssa_free_vars sub =
1312
let is_undefined v = Var.index v = 0 in
1413
Term.enum blk_t sub |> Seq.fold ~init:Var.Set.empty ~f:(fun vars blk ->
1514
vars ++ Set.filter (Ir_blk.free_vars blk) ~f:is_undefined)
1615

17-
let defined_by_blk b =
18-
Ir_blk.elts b |> Seq.fold ~init:Var.Set.empty ~f:(fun kill -> function
19-
| `Phi phi -> Set.add kill @@ Ir_phi.lhs phi
20-
| `Def def -> Set.add kill @@ Ir_def.lhs def
21-
| `Jmp _ -> kill)
22-
23-
type blk_transfer = {
24-
defs : Var.Set.t;
25-
uses : Var.Set.t;
26-
}
27-
28-
let blk_defs blk =
29-
Term.enum def_t blk |>
30-
Seq.fold ~init:Var.Set.empty ~f:(fun defs def ->
31-
Set.add defs (Ir_def.lhs def))
32-
33-
let update blk defs uses trans = Map.update trans blk ~f:(function
34-
| None -> {defs; uses}
35-
| Some had -> {
36-
defs = Set.union had.defs defs;
37-
uses = Set.union had.uses uses
38-
})
39-
40-
let block_transitions sub =
41-
Term.enum blk_t sub |>
42-
Seq.fold ~init:Tid.Map.empty ~f:(fun fs blk ->
43-
let init = update
44-
(Term.tid blk)
45-
(blk_defs blk)
46-
(Ir_blk.free_vars blk) fs in
47-
Term.enum phi_t blk |>
48-
Seq.fold ~init ~f:(fun init phi ->
49-
let defs = Var.Set.singleton @@ Ir_phi.lhs phi in
50-
Ir_phi.values phi |>
51-
Seq.fold ~init ~f:(fun fs (src,exp) ->
52-
update src defs (Exp.free_vars exp) fs)))
16+
module Live = struct
17+
type tran = {
18+
defs : Var.Set.t;
19+
uses : Var.Set.t;
20+
}
21+
22+
type t = {
23+
blks : tran Tid.Map.t;
24+
outs : (tid, Var.Set.t) Solution.t
25+
}
26+
27+
let pp_vars ppf vars =
28+
Format.pp_print_list
29+
~pp_sep:Format.pp_print_space
30+
Var.pp
31+
ppf (Set.to_list vars)
32+
33+
let pp_transfer ppf {uses; defs} =
34+
Format.fprintf ppf "(%a) / (%a)"
35+
pp_vars uses pp_vars defs
36+
37+
let blk_defs blk =
38+
Term.enum def_t blk |>
39+
Seq.fold ~init:Var.Set.empty ~f:(fun defs def ->
40+
Set.add defs (Ir_def.lhs def))
41+
42+
let update blk trans ~f = Map.update trans blk ~f:(function
43+
| None -> f {defs=Var.Set.empty; uses=Var.Set.empty}
44+
| Some had -> f had)
45+
46+
let block_transitions sub =
47+
Term.enum blk_t sub |>
48+
Seq.fold ~init:Tid.Map.empty ~f:(fun fs blk ->
49+
Map.add_exn fs (Term.tid blk) {
50+
defs = blk_defs blk;
51+
uses = Ir_blk.free_vars blk;
52+
}) |> fun trans ->
53+
Term.enum blk_t sub |>
54+
Seq.fold ~init:trans ~f:(fun init blk ->
55+
Term.enum phi_t blk |>
56+
Seq.fold ~init ~f:(fun init phi ->
57+
Ir_phi.values phi |>
58+
Seq.fold ~init ~f:(fun fs (src,exp) ->
59+
update src fs ~f:(fun {defs; uses} -> {
60+
defs = Set.add defs (Ir_phi.lhs phi);
61+
uses = uses ++ (Exp.free_vars exp -- defs)
62+
}))))
63+
64+
let lookup blks n = match Map.find blks n with
65+
| None -> {defs = Var.Set.empty; uses = Var.Set.empty}
66+
| Some t -> t
67+
68+
let is_pseudo n = Tid.equal n G.exit || Tid.equal n G.start
69+
let apply {defs;uses} vars = vars -- defs ++ uses
70+
let transfer blks n vars =
71+
if is_pseudo n then vars
72+
else apply (lookup blks n) vars
73+
74+
let initialize ?(init=Var.Set.empty) sub =
75+
Tid.Map.singleton G.exit @@
76+
Seq.fold (Term.enum arg_t sub) ~init ~f:(fun vars arg ->
77+
match Ir_arg.intent arg with
78+
| None | Some In -> vars
79+
| Some (Out | Both) ->
80+
vars ++ Exp.free_vars (Ir_arg.rhs arg))
81+
82+
let compute ?keep:init sub =
83+
let g = G.create sub in
84+
let init = Solution.create (initialize ?init sub) Var.Set.empty in
85+
let blks = block_transitions sub in {
86+
blks;
87+
outs = Graphlib.fixpoint (module G) ~init ~start:G.exit ~rev:true g
88+
~merge:Set.union
89+
~equal:Var.Set.equal
90+
~f:(transfer blks)
91+
}
92+
93+
let outs {outs} blk = Solution.get outs blk
94+
let ins {outs; blks} blk =
95+
transfer blks blk (Solution.get outs blk)
96+
97+
let defs {blks} blk = (lookup blks blk).defs
98+
let uses {blks} blk = (lookup blks blk).uses
99+
100+
let fold live ~init ~f =
101+
Map.fold live.blks ~init ~f:(fun ~key:blk ~data:trans init ->
102+
let outs = Solution.get live.outs blk in
103+
f init blk (apply trans outs))
104+
105+
let blks live var =
106+
fold live ~init:Tid.Set.empty ~f:(fun blks blk ins ->
107+
if Set.mem ins var
108+
then Set.add blks blk
109+
else blks)
110+
111+
let vars live = outs live G.start
112+
113+
let solution {outs=x} = x
114+
115+
let pp ppf live =
116+
Format.pp_open_vbox ppf 0;
117+
fold live ~init:() ~f:(fun () blk live ->
118+
Format.fprintf ppf "@[<h>%a: @[<hov 2>(%a)@]@]@;"
119+
Tid.pp blk pp_vars live);
120+
Format.pp_close_box ppf ()
121+
end
53122

54123
let compute_liveness sub =
55-
let g = G.create sub in
56-
let init = Solution.create Tid.Map.empty Var.Set.empty in
57-
let tran = block_transitions sub in
58-
Graphlib.fixpoint (module G) ~init ~start:G.exit ~rev:true g
59-
~merge:Set.union
60-
~equal:Var.Set.equal
61-
~f:(fun n vars ->
62-
if Tid.equal n G.exit || Tid.equal n G.start then vars
63-
else
64-
let {defs; uses} = Map.find_exn tran n in
65-
vars -- defs ++ uses)
124+
Live.(solution@@compute sub)
66125

67126
let free_vars_of_sub sub =
68127
if Ssa.is_transformed sub
69128
then ssa_free_vars sub
70-
else Solution.get (compute_liveness sub) G.start
129+
else Live.(vars@@compute sub)

lib/bap_sema/bap_sema_free_vars.mli

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,19 @@ open Bap_types.Std
22
open Graphlib.Std
33
open Bap_ir
44

5+
module Live : sig
6+
type t
7+
val compute : ?keep:Var.Set.t -> sub term -> t
8+
val ins : t -> tid -> Var.Set.t
9+
val vars : t -> Var.Set.t
10+
val outs : t -> tid -> Var.Set.t
11+
val defs : t -> tid -> Var.Set.t
12+
val uses : t -> tid -> Var.Set.t
13+
val fold : t -> init:'a -> f:('a -> tid -> Var.Set.t -> 'a) -> 'a
14+
val blks : t -> var -> Tid.Set.t
15+
val solution : t -> (tid, Var.Set.t) Solution.t
16+
val pp : Format.formatter -> t -> unit
17+
end
18+
519
val compute_liveness : sub term -> (tid, Var.Set.t) Solution.t
620
val free_vars_of_sub : sub term -> Var.Set.t

0 commit comments

Comments
 (0)