## lustrec / src / inliner.ml @ 566dbf49

History | View | Annotate | Download (12.5 KB)

1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|

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 | b09a175c | ploc | open LustreSpec |

13 | open Corelang |
||

14 | 566dbf49 | ploc | open Utils |

15 | |||

16 | (* Local annotations are declared with the following key /inlining/: true *) |
||

17 | let keyword = ["inlining"] |
||

18 | |||

19 | let is_inline_expr expr = |
||

20 | match expr.expr_annot with |
||

21 | | Some ann -> |
||

22 | List.exists (fun (key, value) -> key = keyword) ann.annots |
||

23 | | None -> false |
||

24 | b09a175c | ploc | |

25 | let check_node_name id = (fun t -> |
||

26 | match t.top_decl_desc with |
||

27 | | Node nd -> nd.node_id = id |
||

28 | | _ -> false) |
||

29 | |||

30 | |||

31 | af5af1e8 | ploc | let rename_expr rename expr = expr_replace_var rename expr |

32 | let rename_eq rename eq = |
||

33 | { eq with |
||

34 | eq_lhs = List.map rename eq.eq_lhs; |
||

35 | eq_rhs = rename_expr rename eq.eq_rhs |
||

36 | } |
||

37 | |||

38 | b09a175c | ploc | (* |

39 | expr, locals', eqs = inline_call id args' reset locals nodes |
||

40 | |||

41 | We select the called node equations and variables. |
||

42 | renamed_inputs = args |
||

43 | renamed_eqs |
||

44 | |||

45 | the resulting expression is tuple_of_renamed_outputs |
||

46 | |||

47 | TODO: convert the specification/annotation/assert and inject them |
||

48 | TODO: deal with reset |
||

49 | *) |
||

50 | let inline_call orig_expr args reset locals node = |
||

51 | let loc = orig_expr.expr_loc in |
||

52 | let uid = orig_expr.expr_tag in |
||

53 | 9603460e | xthirioux | let rename v = |

54 | if v = tag_true || v = tag_false then v else |
||

55 | (Format.fprintf Format.str_formatter "%s_%i_%s" |
||

56 | b09a175c | ploc | node.node_id uid v; |

57 | 9603460e | xthirioux | Format.flush_str_formatter ()) |

58 | b09a175c | ploc | in |

59 | b08ffca7 | xthirioux | let eqs' = List.map (rename_eq rename) (get_node_eqs node) |

60 | b09a175c | ploc | in |

61 | let rename_var v = { v with var_id = rename v.var_id } in |
||

62 | let inputs' = List.map rename_var node.node_inputs in |
||

63 | let outputs' = List.map rename_var node.node_outputs in |
||

64 | let locals' = List.map rename_var node.node_locals in |
||

65 | |||

66 | (* checking we are at the appropriate (early) step: node_checks and |
||

67 | node_gencalls should be empty (not yet assigned) *) |
||

68 | assert (node.node_checks = []); |
||

69 | assert (node.node_gencalls = []); |
||

70 | |||

71 | (* Bug included: todo deal with reset *) |
||

72 | assert (reset = None); |
||

73 | |||

74 | let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in |
||

75 | let expr = expr_of_expr_list |
||

76 | loc |
||

77 | (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs') |
||

78 | in |
||

79 | af5af1e8 | ploc | let asserts' = (* We rename variables in assert expressions *) |

80 | List.map |
||

81 | (fun a -> |
||

82 | {a with assert_expr = |
||

83 | let expr = a.assert_expr in |
||

84 | rename_expr rename expr |
||

85 | }) |
||

86 | node.node_asserts |
||

87 | in |
||

88 | expr, |
||

89 | inputs'@outputs'@locals'@locals, |
||

90 | 04d15b97 | xthirioux | assign_inputs::eqs', |

91 | af5af1e8 | ploc | asserts' |

92 | b09a175c | ploc | |

93 | |||

94 | |||

95 | |||

96 | (* |
||

97 | new_expr, new_locals, new_eqs = inline_expr expr locals nodes |
||

98 | |||

99 | Each occurence of a node in nodes in the expr should be replaced by fresh |
||

100 | variables and the code of called node instance added to new_eqs |
||

101 | |||

102 | *) |
||

103 | 566dbf49 | ploc | let rec inline_expr ?(selection_on_annotation=false) expr locals nodes = |

104 | let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |
||

105 | let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in |
||

106 | b09a175c | ploc | let inline_tuple el = |

107 | af5af1e8 | ploc | List.fold_right (fun e (el_tail, locals, eqs, asserts) -> |

108 | let e', locals', eqs', asserts' = inline_expr e locals nodes in |
||

109 | e'::el_tail, locals', eqs'@eqs, asserts@asserts' |
||

110 | ) el ([], locals, [], []) |
||

111 | b09a175c | ploc | in |

112 | let inline_pair e1 e2 = |
||

113 | af5af1e8 | ploc | let el', l', eqs', asserts' = inline_tuple [e1;e2] in |

114 | b09a175c | ploc | match el' with |

115 | af5af1e8 | ploc | | [e1'; e2'] -> e1', e2', l', eqs', asserts' |

116 | b09a175c | ploc | | _ -> assert false |

117 | in |
||

118 | let inline_triple e1 e2 e3 = |
||

119 | af5af1e8 | ploc | let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in |

120 | b09a175c | ploc | match el' with |

121 | af5af1e8 | ploc | | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts' |

122 | b09a175c | ploc | | _ -> assert false |

123 | in |
||

124 | 566dbf49 | ploc | |

125 | b09a175c | ploc | match expr.expr_desc with |

126 | | Expr_appl (id, args, reset) -> |
||

127 | af5af1e8 | ploc | let args', locals', eqs', asserts' = inline_expr args locals nodes in |

128 | 566dbf49 | ploc | if List.exists (check_node_name id) nodes && (* the current node call is provided |

129 | as arguments nodes *) |
||

130 | (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated, |
||

131 | it is explicitely inlined here *) |
||

132 | then |
||

133 | b09a175c | ploc | (* The node should be inlined *) |

134 | 566dbf49 | ploc | let _ = Format.eprintf "Inlining call to %s@." id in |

135 | af5af1e8 | ploc | let node = try List.find (check_node_name id) nodes |

136 | b09a175c | ploc | with Not_found -> (assert false) in |

137 | 70df2f87 | xthirioux | let node = node_of_top node in |

138 | b09a175c | ploc | let node = inline_node node nodes in |

139 | af5af1e8 | ploc | let expr, locals', eqs'', asserts'' = |

140 | b09a175c | ploc | inline_call expr args' reset locals' node in |

141 | af5af1e8 | ploc | expr, locals', eqs'@eqs'', asserts'@asserts'' |

142 | b09a175c | ploc | else |

143 | (* let _ = Format.eprintf "Not inlining call to %s@." id in *) |
||

144 | af5af1e8 | ploc | { expr with expr_desc = Expr_appl(id, args', reset)}, |

145 | locals', |
||

146 | eqs', |
||

147 | asserts' |
||

148 | b09a175c | ploc | |

149 | (* For other cases, we just keep the structure, but convert sub-expressions *) |
||

150 | | Expr_const _ |
||

151 | af5af1e8 | ploc | | Expr_ident _ -> expr, locals, [], [] |

152 | b09a175c | ploc | | Expr_tuple el -> |

153 | af5af1e8 | ploc | let el', l', eqs', asserts' = inline_tuple el in |

154 | { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts' |
||

155 | b09a175c | ploc | | Expr_ite (g, t, e) -> |

156 | af5af1e8 | ploc | let g', t', e', l', eqs', asserts' = inline_triple g t e in |

157 | { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts' |
||

158 | b09a175c | ploc | | Expr_arrow (e1, e2) -> |

159 | af5af1e8 | ploc | let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in |

160 | { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts' |
||

161 | b09a175c | ploc | | Expr_fby (e1, e2) -> |

162 | af5af1e8 | ploc | let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in |

163 | { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts' |
||

164 | b09a175c | ploc | | Expr_array el -> |

165 | af5af1e8 | ploc | let el', l', eqs', asserts' = inline_tuple el in |

166 | { expr with expr_desc = Expr_array el' }, l', eqs', asserts' |
||

167 | b09a175c | ploc | | Expr_access (e, dim) -> |

168 | af5af1e8 | ploc | let e', l', eqs', asserts' = inline_expr e locals nodes in |

169 | { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts' |
||

170 | b09a175c | ploc | | Expr_power (e, dim) -> |

171 | af5af1e8 | ploc | let e', l', eqs', asserts' = inline_expr e locals nodes in |

172 | { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts' |
||

173 | b09a175c | ploc | | Expr_pre e -> |

174 | af5af1e8 | ploc | let e', l', eqs', asserts' = inline_expr e locals nodes in |

175 | { expr with expr_desc = Expr_pre e' }, l', eqs', asserts' |
||

176 | b09a175c | ploc | | Expr_when (e, id, label) -> |

177 | af5af1e8 | ploc | let e', l', eqs', asserts' = inline_expr e locals nodes in |

178 | { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts' |
||

179 | b09a175c | ploc | | Expr_merge (id, branches) -> |

180 | af5af1e8 | ploc | let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in |

181 | b09a175c | ploc | let branches' = List.map2 (fun (label, _) v -> label, v) branches el in |

182 | af5af1e8 | ploc | { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts' |

183 | 566dbf49 | ploc | and inline_node ?(selection_on_annotation=false) nd nodes = |

184 | let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |
||

185 | af5af1e8 | ploc | let new_locals, eqs, asserts = |

186 | List.fold_left (fun (locals, eqs, asserts) eq -> |
||

187 | let eq_rhs', locals', new_eqs', asserts' = |
||

188 | b09a175c | ploc | inline_expr eq.eq_rhs locals nodes |

189 | in |
||

190 | af5af1e8 | ploc | locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts |

191 | b08ffca7 | xthirioux | ) (nd.node_locals, [], nd.node_asserts) (get_node_eqs nd) |

192 | b09a175c | ploc | in |

193 | { nd with |
||

194 | node_locals = new_locals; |
||

195 | b08ffca7 | xthirioux | node_stmts = List.map (fun eq -> Eq eq) eqs; |

196 | af5af1e8 | ploc | node_asserts = asserts; |

197 | b09a175c | ploc | } |

198 | |||

199 | let inline_all_calls node nodes = |
||

200 | let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in |
||

201 | { node with top_decl_desc = Node (inline_node nd nodes) } |
||

202 | |||

203 | |||

204 | |||

205 | |||

206 | |||

207 | 592f508c | ploc | let witness filename main_name orig inlined type_env clock_env = |

208 | b09a175c | ploc | let loc = Location.dummy_loc in |

209 | let rename_local_node nodes prefix id = |
||

210 | if List.exists (check_node_name id) nodes then |
||

211 | prefix ^ id |
||

212 | else |
||

213 | id |
||

214 | in |
||

215 | let main_orig_node = match (List.find (check_node_name main_name) orig).top_decl_desc with |
||

216 | Node nd -> nd | _ -> assert false in |
||

217 | |||

218 | let orig_rename = rename_local_node orig "orig_" in |
||

219 | let inlined_rename = rename_local_node inlined "inlined_" in |
||

220 | let identity = (fun x -> x) in |
||

221 | let is_node top = match top.top_decl_desc with Node _ -> true | _ -> false in |
||

222 | let orig = rename_prog orig_rename identity identity orig in |
||

223 | let inlined = rename_prog inlined_rename identity identity inlined in |
||

224 | let nodes_origs, others = List.partition is_node orig in |
||

225 | let nodes_inlined, _ = List.partition is_node inlined in |
||

226 | |||

227 | b50c665d | ploc | (* One ok_i boolean variable per output var *) |

228 | let nb_outputs = List.length main_orig_node.node_outputs in |
||

229 | let ok_i = List.map (fun id -> |
||

230 | mkvar_decl |
||

231 | loc |
||

232 | ("OK" ^ string_of_int id, |
||

233 | {ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, |
||

234 | {ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, |
||

235 | false) |
||

236 | ) (Utils.enumerate nb_outputs) |
||

237 | in |
||

238 | |||

239 | (* OK = ok_1 and ok_2 and ... ok_n-1 *) |
||

240 | b09a175c | ploc | let ok_ident = "OK" in |

241 | let ok_output = mkvar_decl |
||

242 | loc |
||

243 | (ok_ident, |
||

244 | {ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, |
||

245 | {ck_dec_desc=Ckdec_any; ck_dec_loc=loc}, |
||

246 | false) |
||

247 | in |
||

248 | b50c665d | ploc | let main_ok_expr = |

249 | let mkv x = mkexpr loc (Expr_ident x) in |
||

250 | match ok_i with |
||

251 | | [] -> assert false |
||

252 | | [x] -> mkv x.var_id |
||

253 | | hd::tl -> |
||

254 | List.fold_left (fun accu elem -> |
||

255 | mkpredef_call loc "&&" [mkv elem.var_id; accu] |
||

256 | ) (mkv hd.var_id) tl |
||

257 | in |
||

258 | |||

259 | (* Building main node *) |
||

260 | |||

261 | b08ffca7 | xthirioux | let ok_i_eq = |

262 | { eq_loc = loc; |
||

263 | eq_lhs = List.map (fun v -> v.var_id) ok_i; |
||

264 | eq_rhs = |
||

265 | let inputs = expr_of_expr_list loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in |
||

266 | let call_orig = |
||

267 | mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in |
||

268 | let call_inlined = |
||

269 | mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in |
||

270 | let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in |
||

271 | mkexpr loc (Expr_appl ("=", args, None)) |
||

272 | } in |
||

273 | let ok_eq = |
||

274 | { eq_loc = loc; |
||

275 | eq_lhs = [ok_ident]; |
||

276 | eq_rhs = main_ok_expr; |
||

277 | } in |
||

278 | b09a175c | ploc | let main_node = { |

279 | node_id = "check"; |
||

280 | node_type = Types.new_var (); |
||

281 | node_clock = Clocks.new_var true; |
||

282 | node_inputs = main_orig_node.node_inputs; |
||

283 | node_outputs = [ok_output]; |
||

284 | 9603460e | xthirioux | node_locals = ok_i; |

285 | b09a175c | ploc | node_gencalls = []; |

286 | node_checks = []; |
||

287 | node_asserts = []; |
||

288 | b08ffca7 | xthirioux | node_stmts = [Eq ok_i_eq; Eq ok_eq]; |

289 | 3ab5748b | ploc | node_dec_stateless = false; |

290 | 52cfee34 | xthirioux | node_stateless = None; |

291 | b09a175c | ploc | node_spec = Some |

292 | {requires = []; |
||

293 | 01c7d5e1 | ploc | ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))]; |

294 | behaviors = []; |
||

295 | spec_loc = loc |
||

296 | b09a175c | ploc | }; |

297 | 01c7d5e1 | ploc | node_annot = []; |

298 | b09a175c | ploc | } |

299 | in |
||

300 | ef34b4ae | xthirioux | let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in |

301 | b09a175c | ploc | let new_prog = others@nodes_origs@nodes_inlined@main in |

302 | let _ = Typing.type_prog type_env new_prog in |
||

303 | let _ = Clock_calculus.clock_prog clock_env new_prog in |
||

304 | |||

305 | 592f508c | ploc | |

306 | let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in |
||

307 | b09a175c | ploc | let witness_out = open_out witness_file in |

308 | let witness_fmt = Format.formatter_of_out_channel witness_out in |
||

309 | Format.fprintf witness_fmt |
||

310 | "(* Generated lustre file to check validity of inlining process *)@."; |
||

311 | Printers.pp_prog witness_fmt new_prog; |
||

312 | Format.fprintf witness_fmt "@."; |
||

313 | () (* xx *) |
||

314 | |||

315 | 592f508c | ploc | let global_inline basename prog type_env clock_env = |

316 | b09a175c | ploc | (* We select the main node desc *) |

317 | let main_node, other_nodes, other_tops = |
||

318 | List.fold_left |
||

319 | (fun (main_opt, nodes, others) top -> |
||

320 | match top.top_decl_desc with |
||

321 | | Node nd when nd.node_id = !Options.main_node -> |
||

322 | Some top, nodes, others |
||

323 | | Node _ -> main_opt, top::nodes, others |
||

324 | | _ -> main_opt, nodes, top::others) |
||

325 | (None, [], []) prog |
||

326 | in |
||

327 | (* Recursively each call of a node in the top node is replaced *) |
||

328 | let main_node = Utils.desome main_node in |
||

329 | let main_node' = inline_all_calls main_node other_nodes in |
||

330 | let res = main_node'::other_tops in |
||

331 | 592f508c | ploc | if !Options.witnesses then ( |

332 | witness |
||

333 | basename |
||

334 | (match main_node.top_decl_desc with Node nd -> nd.node_id | _ -> assert false) |
||

335 | prog res type_env clock_env |
||

336 | ); |
||

337 | b09a175c | ploc | res |

338 | b50c665d | ploc | |

339 | 566dbf49 | ploc | let local_inline basename prog type_env clock_env = |

340 | let local_anns = Annotations.get_expr_annotations keyword in |
||

341 | if local_anns != [] then ( |
||

342 | let nodes_with_anns = List.fold_left (fun accu (k, _) -> ISet.add k accu) ISet.empty local_anns in |
||

343 | ISet.iter (fun node_id -> Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns; |
||

344 | List.fold_right (fun top accu -> |
||

345 | ( match top.top_decl_desc with |
||

346 | | Node nd when ISet.mem nd.node_id nodes_with_anns -> |
||

347 | { top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) } |
||

348 | | _ -> top |
||

349 | )::accu) prog [] |
||

350 | |||

351 | ) |
||

352 | else |
||

353 | prog |
||

354 | |||

355 | |||

356 | b50c665d | ploc | (* Local Variables: *) |

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

358 | (* End: *) |