1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
(** The algorithm in this module locates a suitable location for declaring each
variable.
The instructions of a function, represented by their location, are gathered
in a tree that represents the nesting structure of the lexical scopes: a
variable declared in a node is visible from all of its children, unless a
variable with the same name is declared in between. Therefore a variable can
be declared at the least common ancestor to all of its occurrences.
The tree data structure that is used remembers the depth of each node to
support the computation of least common ancestors. *)
open Utils
open Prog
type node = Location.i_loc
type nodeset = Siloc.t
module Tree : sig
type t = private { parent : t option; depth : int; data : node }
val root : node -> t
val make : node -> t -> t
end = struct
type t = { parent : t option; depth : int; data : node }
let root ii = { parent = None; depth = 0; data = ii }
let make ii t = { parent = Some t; data = ii; depth = 1 + t.depth }
end
let make ii = function None -> Tree.root ii | Some t -> Tree.make ii t
type tree = Tree.t Miloc.t
let parent_at_depth (d : int) (t : tree) (n : node) : node =
assert (0 <= d);
let open Tree in
let rec loop n =
if Stdlib.Int.equal d n.depth then n.data else loop (Option.get n.parent)
in
loop (Miloc.find n t)
let find_common_ancestor (t : tree) (nodes : nodeset) : node =
assert (not (Siloc.is_empty nodes));
let depth =
Siloc.fold (fun n -> min (Miloc.find n t).depth) nodes Stdlib.Int.max_int
in
let nodes = Siloc.map (parent_at_depth depth t) nodes in
let rec loop nodes =
if Siloc.is_singleton nodes then Siloc.any nodes
else
nodes
|> Siloc.map (fun n -> (Option.get (Miloc.find n t).parent).data)
|> loop
in
loop nodes
let variables_in_gvar x (acc : Spv.t) : Spv.t =
if x.v_kind <> Const then Spv.add x acc else acc
let variables_in_pexpr = rvars_e variables_in_gvar
let variables_in_pexprs = rvars_es variables_in_gvar
let variables_in_plval = rvars_lv variables_in_gvar
let variables_in_plvals = rvars_lvs variables_in_gvar
let variables_in_instr_r : _ pinstr_r -> Spv.t = function
| Cassgn (x, _, _, e) -> variables_in_pexpr (variables_in_plval Spv.empty x) e
| Copn (xs, _, _, es) | Csyscall (xs, _, es) | Ccall (xs, _, es) ->
variables_in_pexprs (variables_in_plvals Spv.empty xs) es
| Cfor (x, (_, e1, e2), _) ->
variables_in_pexprs (Spv.singleton (L.unloc x)) [ e1; e2 ]
| Cif (e, _, _) | Cwhile (_, _, e, _, _) | Cassert (_, e) -> variables_in_pexpr Spv.empty e
(** Maps each variable to the set of nodes at which it occurs *)
let variable_occurrences (c : _ pstmt) : nodeset Mpv.t =
let tbl = ref Mpv.empty in
let insert (n : node) (x : pvar) =
tbl := Mpv.modify_def Siloc.empty x (Siloc.add n) !tbl
in
iter_instr
(fun i -> i.i_desc |> variables_in_instr_r |> Spv.iter (insert i.i_loc))
c;
!tbl
let rec tree_of_instr ((acc : tree), (t : Tree.t option)) (i : _ ginstr) :
tree * Tree.t option =
let t = make i.i_loc t in
let acc = Miloc.add i.i_loc t acc in
(tree_of_instr_r acc t i.i_desc, Some t)
and tree_of_instr_r (acc : tree) (t : Tree.t) : _ ginstr_r -> tree = function
| Cassgn _ | Copn _ | Csyscall _ | Ccall _ | Cassert _ -> acc
| Cfor (_, _, c) -> tree_of_stmt acc (Some t) c |> fst
| Cif (_, c1, c2) | Cwhile (_, c1, _, _, c2) ->
let acc, _ = tree_of_stmt acc (Some t) c1 in
let acc, _ = tree_of_stmt acc (Some t) c2 in
acc
and tree_of_stmt (acc : tree) (t : Tree.t option) (c : _ gstmt) :
tree * Tree.t option =
List.fold_left tree_of_instr (acc, t) c
(** Reverse a map from variable to nodes into the corresponding map from nodes
to sets of variables *)
let reverse (m : node Mpv.t) : Spv.t Miloc.t =
Mpv.fold (fun x n -> Miloc.modify_def Spv.empty n (Spv.add x)) m Miloc.empty
let get_declaration_sites (fd : _ pfunc) : Spv.t Miloc.t =
let t, last = tree_of_stmt Miloc.empty None fd.f_body in
let occ = variable_occurrences fd.f_body in
let occ =
match last with
| None -> occ
| Some t ->
List.fold_left
(fun occ x ->
Mpv.modify_def Siloc.empty (L.unloc x) (Siloc.add t.data) occ)
occ fd.f_ret
in
let occ = List.fold_left (fun occ x -> Mpv.remove x occ) occ fd.f_args in
Mpv.map (find_common_ancestor t) occ |> reverse