## lustrec/src/checks/liveness.ml @ ca7ff3f7

1 | ca7ff3f7 | LĂ©lio Brun | ```
(********************************************************************)
``` |
---|---|---|---|

2 | ```
(* *)
``` |
||

3 | ```
(* The LustreC compiler toolset / The LustreC Development Team *)
``` |
||

4 | ```
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
``` |
||

5 | ```
(* *)
``` |
||

6 | ```
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
``` |
||

7 | ```
(* under the terms of the GNU Lesser General Public License *)
``` |
||

8 | ```
(* version 2.1. *)
``` |
||

9 | ```
(* *)
``` |
||

10 | ```
(********************************************************************)
``` |
||

11 | |||

12 | open Utils |
||

13 | open Lustre_types |
||

14 | open Corelang |
||

15 | open Causality |
||

16 | |||

17 | type context = { |
||

18 | mutable evaluated : Disjunction.CISet.t; |
||

19 | dep_graph : IdentDepGraph.t; |
||

20 | disjoint : (ident, Disjunction.CISet.t) Hashtbl.t; |
||

21 | policy : (ident, var_decl) Hashtbl.t; |
||

22 | ```
}
``` |
||

23 | |||

24 | ```
(* computes the in-degree for each local variable of node [n], according to dep
``` |
||

25 | ```
graph [g]. *)
``` |
||

26 | let compute_fanin n g = |
||

27 | let locals = |
||

28 | ISet.diff (ExprDep.node_local_variables n) (ExprDep.node_memory_variables n) |
||

29 | ```
in
``` |
||

30 | let inputs = ExprDep.node_input_variables n in |
||

31 | let fanin = Hashtbl.create 23 in |
||

32 | IdentDepGraph.iter_vertex |
||

33 | (fun v -> |
||

34 | if ISet.mem v locals then |
||

35 | Hashtbl.add fanin v (IdentDepGraph.in_degree g v) |
||

36 | else if ExprDep.is_read_var v && not (ISet.mem v inputs) then |
||

37 | Hashtbl.add fanin (ExprDep.undo_read_var v) |
||

38 | (IdentDepGraph.in_degree g v)) |
||

39 | g; |
||

40 | ```
fanin
``` |
||

41 | |||

42 | let pp_fanin fmt fanin = |
||

43 | Format.fprintf fmt "@[<v 0>@[<v 2>{ /* locals fanin: */"; |
||

44 | Hashtbl.iter (fun s t -> Format.fprintf fmt "@ %s -> %d" s t) fanin; |
||

45 | Format.fprintf fmt "@]@ }@]" |
||

46 | |||

47 | ```
(* computes the cone of influence of a given [var] wrt a dependency graph [g]. *)
``` |
||

48 | let cone_of_influence g var = |
||

49 | ```
(*Format.printf "DEBUG coi: %s@." var;*)
``` |
||

50 | let frontier = ref (ISet.add var ISet.empty) in |
||

51 | let explored = ref ISet.empty in |
||

52 | let coi = ref ISet.empty in |
||

53 | while not (ISet.is_empty !frontier) do |
||

54 | let head = ISet.min_elt !frontier in |
||

55 | ```
(*Format.printf "DEBUG head: %s@." head;*)
``` |
||

56 | frontier := ISet.remove head !frontier; |
||

57 | explored := ISet.add head !explored; |
||

58 | if ExprDep.is_read_var head then |
||

59 | coi := ISet.add (ExprDep.undo_read_var head) !coi; |
||

60 | List.iter |
||

61 | (fun s -> |
||

62 | if not (ISet.mem s !explored) then frontier := ISet.add s !frontier) |
||

63 | (IdentDepGraph.succ g head) |
||

64 | done; |
||

65 | !coi |
||

66 | |||

67 | let compute_unused_variables n g = |
||

68 | let inputs = ExprDep.node_input_variables n in |
||

69 | let mems = ExprDep.node_memory_variables n in |
||

70 | let outputs = ExprDep.node_output_variables n in |
||

71 | ISet.fold |
||

72 | (fun var unused -> ISet.diff unused (cone_of_influence g var)) |
||

73 | (ISet.union outputs mems) (ISet.union inputs mems) |
||

74 | |||

75 | ```
(* computes the set of potentially reusable variables. We don't reuse input
``` |
||

76 | ```
variables, due to possible aliasing *)
``` |
||

77 | let node_reusable_variables node = |
||

78 | let mems = ExprDep.node_memory_variables node in |
||

79 | List.fold_left |
||

80 | (fun acc l -> |
||

81 | if ISet.mem l.var_id mems then acc else Disjunction.CISet.add l acc) |
||

82 | Disjunction.CISet.empty node.node_locals |
||

83 | |||

84 | let kill_instance_variables ctx inst = |
||

85 | IdentDepGraph.remove_vertex ctx.dep_graph inst |
||

86 | |||

87 | let kill_root ctx head = |
||

88 | IdentDepGraph.iter_succ |
||

89 | (IdentDepGraph.remove_edge ctx.dep_graph head.var_id) |
||

90 | ctx.dep_graph head.var_id |
||

91 | |||

92 | ```
(* Recursively removes useless variables, i.e. [ctx.evaluated] variables that
``` |
||

93 | ```
are current roots of the dep graph [ctx.dep_graph] - [evaluated] is the set
``` |
||

94 | ```
of already evaluated variables, wrt the scheduling - does only remove edges,
``` |
||

95 | ```
not variables themselves - yet, instance variables are removed *)
``` |
||

96 | let remove_roots ctx = |
||

97 | let rem = ref true in |
||

98 | let remaining = ref ctx.evaluated in |
||

99 | while !rem do |
||

100 | rem := false; |
||

101 | let all_roots = graph_roots ctx.dep_graph in |
||

102 | let inst_roots, var_roots = |
||

103 | List.partition |
||

104 | (fun v -> ExprDep.is_instance_var v && v <> Causality.world) |
||

105 | ```
all_roots
``` |
||

106 | ```
in
``` |
||

107 | let frontier_roots = |
||

108 | Disjunction.CISet.filter (fun v -> List.mem v.var_id var_roots) !remaining |
||

109 | ```
in
``` |
||

110 | if not (Disjunction.CISet.is_empty frontier_roots && inst_roots = []) then ( |
||

111 | rem := true; |
||

112 | List.iter (kill_instance_variables ctx) inst_roots; |
||

113 | Disjunction.CISet.iter (kill_root ctx) frontier_roots; |
||

114 | remaining := Disjunction.CISet.diff !remaining frontier_roots) |
||

115 | ```
done
``` |
||

116 | |||

117 | ```
(* checks whether a variable is aliasable, depending on its (address) type *)
``` |
||

118 | let is_aliasable var = |
||

119 | (not (!Options.mpfr && Types.is_real_type var.var_type)) |
||

120 | && Types.is_address_type var.var_type |
||

121 | |||

122 | ```
(* checks whether a variable [v] is an input of the [var] equation, with an
``` |
||

123 | ```
address type. if so, [var] could not safely reuse/alias [v], should [v] be
``` |
||

124 | ```
dead in the caller node, because [v] may not be dead in the callee node when
``` |
||

125 | ```
[var] is assigned *)
``` |
||

126 | let is_aliasable_input node var = |
||

127 | let eq_var = get_node_eq var node in |
||

128 | let inputs_var = |
||

129 | match NodeDep.get_callee eq_var.eq_rhs with |
||

130 | | None -> |
||

131 | ```
[]
``` |
||

132 | | Some (_, args) -> |
||

133 | List.fold_right |
||

134 | (fun e r -> match e.expr_desc with Expr_ident id -> id :: r | _ -> r) |
||

135 | args [] |
||

136 | ```
in
``` |
||

137 | fun v -> is_aliasable v && List.mem v.var_id inputs_var |
||

138 | |||

139 | ```
(* replace variable [v] by [v'] in graph [g]. [v'] is a dead variable *)
``` |
||

140 | let replace_in_dep_graph v v' g = |
||

141 | IdentDepGraph.add_vertex g v'; |
||

142 | IdentDepGraph.iter_succ (fun s -> IdentDepGraph.add_edge g v' s) g v; |
||

143 | IdentDepGraph.iter_pred (fun p -> IdentDepGraph.add_edge g p v') g v; |
||

144 | IdentDepGraph.remove_vertex g v |
||

145 | |||

146 | let pp_reuse_policy fmt policy = |
||

147 | Format.( |
||

148 | fprintf fmt "@[<v 2>{ /* reuse policy */%t@] }" (fun fmt -> |
||

149 | Hashtbl.iter (fun s t -> fprintf fmt "@,%s -> %s" s t.var_id) policy)) |
||

150 | |||

151 | let pp_context fmt ctx = |
||

152 | Format.fprintf fmt |
||

153 | ```
"@[<v 2>{ /*BEGIN context */@,\
``` |
||

154 | ```
eval = %a;@,\
``` |
||

155 | ```
graph = %a;@,\
``` |
||

156 | ```
disjoint = %a;@,\
``` |
||

157 | ```
policy = %a;@,\
``` |
||

158 | /* END context */ }@]" Disjunction.pp_ciset ctx.evaluated pp_dep_graph |
||

159 | ctx.dep_graph Disjunction.pp_disjoint_map ctx.disjoint pp_reuse_policy |
||

160 | ctx.policy |
||

161 | |||

162 | ```
(* computes the reusable dependencies of variable [var] in graph [g], once [var]
``` |
||

163 | ```
has been evaluated - [locals] is the set of potentially reusable variables -
``` |
||

164 | ```
[evaluated] is the set of evaluated variables - [quasi] is the set of
``` |
||

165 | ```
quasi-reusable variables - [reusable] is the set of dead/reusable
``` |
||

166 | ```
dependencies of [var] in graph [g] - [policy] is the reuse map (which domain
``` |
||

167 | ```
is [evaluated]) *)
``` |
||

168 | let compute_dependencies heads ctx = |
||

169 | ```
(*Log.report ~level:6 (fun fmt -> Format.fprintf fmt
``` |
||

170 | ```
"compute_reusable_dependencies %a %a %a@." Disjunction.pp_ciset locals
``` |
||

171 | ```
Printers.pp_var_name var pp_context ctx);*)
``` |
||

172 | List.iter (kill_root ctx) heads; |
||

173 | remove_roots ctx |
||

174 | |||

175 | let compute_evaluated heads ctx = |
||

176 | List.iter |
||

177 | (fun head -> ctx.evaluated <- Disjunction.CISet.add head ctx.evaluated) |
||

178 | ```
heads
``` |
||

179 | |||

180 | ```
(* tests whether a variable [v] may be (re)used instead of [var]. The conditions
``` |
||

181 | ```
are: - [v] has been really used ([v] is its own representative) - same type -
``` |
||

182 | ```
[v] is not an aliasable input of the equation defining [var] - [v] is not one
``` |
||

183 | ```
of the current heads (which contain [var]) - [v] is not currently in use *)
``` |
||

184 | let eligible node ctx heads var v = |
||

185 | Hashtbl.find ctx.policy v.var_id == v |
||

186 | && Typing.eq_ground |
||

187 | (Types.unclock_type var.var_type) |
||

188 | (Types.unclock_type v.var_type) |
||

189 | && (not (is_aliasable_input node var.var_id v)) |
||

190 | && (not (List.exists (fun h -> h.var_id = v.var_id) heads)) |
||

191 | && (*let repr_v = Hashtbl.find ctx.policy v.var_id*) |
||

192 | ```
not
``` |
||

193 | (Disjunction.CISet.exists |
||

194 | (fun p -> IdentDepGraph.mem_edge ctx.dep_graph p.var_id v.var_id) |
||

195 | ctx.evaluated) |
||

196 | |||

197 | let compute_reuse node ctx heads var = |
||

198 | let disjoint = Hashtbl.find ctx.disjoint var.var_id in |
||

199 | let locally_reusable v = |
||

200 | IdentDepGraph.fold_pred |
||

201 | (fun p r -> |
||

202 | r && Disjunction.CISet.exists (fun d -> p = d.var_id) disjoint) |
||

203 | ctx.dep_graph v.var_id true |
||

204 | ```
in
``` |
||

205 | let eligibles = |
||

206 | if ISet.mem var.var_id (ExprDep.node_memory_variables node) then |
||

207 | Disjunction.CISet.empty |
||

208 | else Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated |
||

209 | ```
in
``` |
||

210 | let quasi_dead, live = |
||

211 | Disjunction.CISet.partition locally_reusable eligibles |
||

212 | ```
in
``` |
||

213 | let disjoint_live = Disjunction.CISet.inter disjoint live in |
||

214 | let dead = |
||

215 | Disjunction.CISet.filter |
||

216 | (fun v -> is_graph_root v.var_id ctx.dep_graph) |
||

217 | ```
quasi_dead
``` |
||

218 | ```
in
``` |
||

219 | Log.report ~level:7 (fun fmt -> |
||

220 | Format.fprintf fmt |
||

221 | ```
"@[<v>eligibles : %a@,\
``` |
||

222 | ```
live : %a@,\
``` |
||

223 | ```
disjoint live: %a@,\
``` |
||

224 | ```
dead : %a@,\
``` |
||

225 | ```
@]"
``` |
||

226 | Disjunction.pp_ciset eligibles Disjunction.pp_ciset live |
||

227 | Disjunction.pp_ciset disjoint_live Disjunction.pp_ciset dead); |
||

228 | (try |
||

229 | let reuse = |
||

230 | match Disjunction.CISet.max_elt_opt disjoint_live with |
||

231 | | Some reuse -> |
||

232 | ```
reuse
``` |
||

233 | | None -> |
||

234 | Disjunction.CISet.choose dead |
||

235 | ```
in
``` |
||

236 | IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id; |
||

237 | Hashtbl.add ctx.policy var.var_id reuse |
||

238 | with Not_found -> Hashtbl.add ctx.policy var.var_id var); |
||

239 | ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated |
||

240 | |||

241 | let compute_reuse_policy node schedule disjoint g = |
||

242 | let ctx = |
||

243 | ```
{
``` |
||

244 | evaluated = Disjunction.CISet.empty; |
||

245 | dep_graph = g; |
||

246 | disjoint; |
||

247 | policy = Hashtbl.create 23; |
||

248 | ```
}
``` |
||

249 | ```
in
``` |
||

250 | List.iter |
||

251 | (fun heads -> |
||

252 | let heads = List.map (fun v -> get_node_var v node) heads in |
||

253 | Log.report ~level:6 (fun fmt -> |
||

254 | Format.( |
||

255 | fprintf fmt |
||

256 | ```
"@[<v>@[<v 2>new context:@,\
``` |
||

257 | ```
%a@]@,\
``` |
||

258 | ```
NEW HEADS:%a@,\
``` |
||

259 | ```
COMPUTE_DEPENDENCIES@,\
``` |
||

260 | ```
@]"
``` |
||

261 | pp_context ctx |
||

262 | (pp_print_list ~pp_open_box:pp_open_hbox ~pp_sep:pp_print_space |
||

263 | (fun fmt head -> |
||

264 | fprintf fmt "%s (%a)" head.var_id Printers.pp_node_eq |
||

265 | (get_node_eq head.var_id node))) |
||

266 | heads)); |
||

267 | compute_dependencies heads ctx; |
||

268 | Log.report ~level:6 (fun fmt -> |
||

269 | Format.fprintf fmt "@[<v>@[<v 2>new context:@,%a@]@,COMPUTE_REUSE@,@]" |
||

270 | pp_context ctx); |
||

271 | List.iter (compute_reuse node ctx heads) heads; |
||

272 | ```
(*compute_evaluated heads ctx;*)
``` |
||

273 | Log.report ~level:6 (fun fmt -> |
||

274 | Format.( |
||

275 | fprintf fmt "@[<v>%a@,@]" |
||

276 | (pp_print_list ~pp_open_box:pp_open_vbox0 (fun fmt head -> |
||

277 | fprintf fmt "reuse %s instead of %s" |
||

278 | (Hashtbl.find ctx.policy head.var_id).var_id head.var_id)) |
||

279 | heads))) |
||

280 | schedule; |
||

281 | IdentDepGraph.clear ctx.dep_graph; |
||

282 | ctx.policy |
||

283 | |||

284 | ```
(* Reuse policy: - could reuse variables with the same type exactly only
``` |
||

285 | ```
(simple). - reusing variables with different types would involve: - either
``` |
||

286 | ```
dirty castings - or complex inclusion expression (for instance: array <->
``` |
||

287 | ```
array cell, struct <-> struct field) to be able to reuse only some parts of
``` |
||

288 | ```
structured data. ... it seems too complex and potentially unsafe - for node
``` |
||

289 | ```
instance calls: output variables could NOT reuse aliasable input variables,
``` |
||

290 | ```
even if inputs become dead, because the correctness would depend on the
``` |
||

291 | ```
scheduling of the callee (so, the compiling strategy could NOT be modular
``` |
||

292 | ```
anymore). - once a policy is set, we need to: - replace each variable by its
``` |
||

293 | ```
reuse alias. - simplify resulting equations, as we may now have: x = x; --> ;
``` |
||

294 | ```
for scalar vars or: x = &{ f1 = x->f1; f2 = t; } --> x->f2 = t; for struct
``` |
||

295 | ```
vars *)
``` |
||

296 | |||

297 | ```
(* the reuse policy seeks to use less local variables by replacing local
``` |
||

298 | ```
variables, applying the rules in the following order: 1) use another clock
``` |
||

299 | ```
disjoint still live variable, with the greatest possible disjoint clock 2)
``` |
||

300 | ```
reuse a dead variable For the sake of safety, we replace variables by others:
``` |
||

301 | ```
- with the same type - not aliasable (i.e. address type) *)
``` |
||

302 | |||

303 | ```
(* Local Variables: *)
``` |
||

304 | ```
(* compile-command:"make -C .." *)
``` |
||

305 | ```
(* End: *)
``` |