## lustrec / src / inliner.ml @ ef34b4ae

History | View | Annotate | Download (11 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 | |||

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

16 | match t.top_decl_desc with |
||

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

18 | | _ -> false) |
||

19 | |||

20 | |||

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

22 | let rename_eq rename eq = |
||

23 | { eq with |
||

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

25 | eq_rhs = rename_expr rename eq.eq_rhs |
||

26 | } |
||

27 | |||

28 | b09a175c | ploc | (* |

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

30 | |||

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

32 | renamed_inputs = args |
||

33 | renamed_eqs |
||

34 | |||

35 | the resulting expression is tuple_of_renamed_outputs |
||

36 | |||

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

38 | TODO: deal with reset |
||

39 | *) |
||

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

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

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

43 | let rename v = |
||

44 | Format.fprintf Format.str_formatter "%s_%i_%s" |
||

45 | node.node_id uid v; |
||

46 | Format.flush_str_formatter () |
||

47 | in |
||

48 | af5af1e8 | ploc | let eqs' = List.map (rename_eq rename) node.node_eqs |

49 | b09a175c | ploc | in |

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

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

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

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

54 | |||

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

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

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

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

59 | |||

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

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

62 | |||

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

64 | let expr = expr_of_expr_list |
||

65 | loc |
||

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

67 | in |
||

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

69 | List.map |
||

70 | (fun a -> |
||

71 | {a with assert_expr = |
||

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

73 | rename_expr rename expr |
||

74 | }) |
||

75 | node.node_asserts |
||

76 | in |
||

77 | expr, |
||

78 | inputs'@outputs'@locals'@locals, |
||

79 | assign_inputs::eqs', |
||

80 | asserts' |
||

81 | b09a175c | ploc | |

82 | |||

83 | |||

84 | |||

85 | (* |
||

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

87 | |||

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

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

90 | |||

91 | *) |
||

92 | let rec inline_expr expr locals nodes = |
||

93 | let inline_tuple el = |
||

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

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

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

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

98 | b09a175c | ploc | in |

99 | let inline_pair e1 e2 = |
||

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

101 | b09a175c | ploc | match el' with |

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

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

104 | in |
||

105 | let inline_triple e1 e2 e3 = |
||

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

107 | b09a175c | ploc | match el' with |

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

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

110 | in |
||

111 | |||

112 | match expr.expr_desc with |
||

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

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

115 | b09a175c | ploc | if List.exists (check_node_name id) nodes then |

116 | (* The node should be inlined *) |
||

117 | af5af1e8 | ploc | (* let _ = Format.eprintf "Inlining call to %s@." id in *) |

118 | let node = try List.find (check_node_name id) nodes |
||

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

120 | af5af1e8 | ploc | let node = |

121 | match node.top_decl_desc with Node nd -> nd | _ -> assert false in |
||

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

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

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

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

126 | b09a175c | ploc | else |

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

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

129 | locals', |
||

130 | eqs', |
||

131 | asserts' |
||

132 | b09a175c | ploc | |

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

134 | | Expr_const _ |
||

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

136 | b09a175c | ploc | | Expr_tuple el -> |

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

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

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

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

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

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

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

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

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

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

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

148 | b09a175c | ploc | | Expr_array el -> |

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

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

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

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

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

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

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

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

157 | b09a175c | ploc | | Expr_pre e -> |

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

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

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

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

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

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

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

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

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

167 | b09a175c | ploc | and inline_node nd nodes = |

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

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

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

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

172 | in |
||

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

174 | ) (nd.node_locals, [], nd.node_asserts) nd.node_eqs |
||

175 | b09a175c | ploc | in |

176 | { nd with |
||

177 | node_locals = new_locals; |
||

178 | af5af1e8 | ploc | node_eqs = eqs; |

179 | node_asserts = asserts; |
||

180 | b09a175c | ploc | } |

181 | |||

182 | let inline_all_calls node nodes = |
||

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

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

185 | |||

186 | |||

187 | |||

188 | |||

189 | |||

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

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

192 | let rename_local_node nodes prefix id = |
||

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

194 | prefix ^ id |
||

195 | else |
||

196 | id |
||

197 | in |
||

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

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

200 | |||

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

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

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

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

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

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

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

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

209 | |||

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

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

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

213 | mkvar_decl |
||

214 | loc |
||

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

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

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

218 | false) |
||

219 | ) (Utils.enumerate nb_outputs) |
||

220 | in |
||

221 | |||

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

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

224 | let ok_output = mkvar_decl |
||

225 | loc |
||

226 | (ok_ident, |
||

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

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

229 | false) |
||

230 | in |
||

231 | b50c665d | ploc | let main_ok_expr = |

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

233 | match ok_i with |
||

234 | | [] -> assert false |
||

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

236 | | hd::tl -> |
||

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

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

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

240 | in |
||

241 | |||

242 | (* Building main node *) |
||

243 | |||

244 | b09a175c | ploc | let main_node = { |

245 | node_id = "check"; |
||

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

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

248 | node_inputs = main_orig_node.node_inputs; |
||

249 | node_outputs = [ok_output]; |
||

250 | node_locals = []; |
||

251 | node_gencalls = []; |
||

252 | node_checks = []; |
||

253 | node_asserts = []; |
||

254 | node_eqs = [ |
||

255 | { eq_loc = loc; |
||

256 | b50c665d | ploc | eq_lhs = List.map (fun v -> v.var_id) ok_i; |

257 | b09a175c | ploc | eq_rhs = |

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

259 | let call_orig = |
||

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

261 | let call_inlined = |
||

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

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

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

265 | b50c665d | ploc | }; |

266 | { eq_loc = loc; |
||

267 | eq_lhs = [ok_ident]; |
||

268 | eq_rhs = main_ok_expr; |
||

269 | } |
||

270 | ]; |
||

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

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

273 | b09a175c | ploc | node_spec = Some |

274 | {requires = []; |
||

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

276 | behaviors = []; |
||

277 | spec_loc = loc |
||

278 | b09a175c | ploc | }; |

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

280 | b09a175c | ploc | } |

281 | in |
||

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

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

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

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

286 | |||

287 | 592f508c | ploc | |

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

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

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

291 | Format.fprintf witness_fmt |
||

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

293 | Printers.pp_prog witness_fmt new_prog; |
||

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

295 | () (* xx *) |
||

296 | |||

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

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

299 | let main_node, other_nodes, other_tops = |
||

300 | List.fold_left |
||

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

302 | match top.top_decl_desc with |
||

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

304 | Some top, nodes, others |
||

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

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

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

308 | in |
||

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

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

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

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

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

314 | witness |
||

315 | basename |
||

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

317 | prog res type_env clock_env |
||

318 | ); |
||

319 | b09a175c | ploc | res |

320 | b50c665d | ploc | |

321 | (* Local Variables: *) |
||

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

323 | (* End: *) |