## lustrec / src / inliner.ml @ 01c7d5e1

History | View | Annotate | Download (9.54 KB)

1 | b09a175c | ploc | open LustreSpec |
---|---|---|---|

2 | open Corelang |
||

3 | |||

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

5 | match t.top_decl_desc with |
||

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

7 | | _ -> false) |
||

8 | |||

9 | |||

10 | (* |
||

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

12 | |||

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

14 | renamed_inputs = args |
||

15 | renamed_eqs |
||

16 | |||

17 | the resulting expression is tuple_of_renamed_outputs |
||

18 | |||

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

20 | TODO: deal with reset |
||

21 | *) |
||

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

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

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

25 | let rename v = |
||

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

27 | node.node_id uid v; |
||

28 | Format.flush_str_formatter () |
||

29 | in |
||

30 | let eqs' = List.map |
||

31 | (fun eq -> { eq with |
||

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

33 | eq_rhs = expr_replace_var rename eq.eq_rhs |
||

34 | } ) node.node_eqs |
||

35 | in |
||

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

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

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

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

40 | |||

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

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

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

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

45 | |||

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

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

48 | |||

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

50 | let expr = expr_of_expr_list |
||

51 | loc |
||

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

53 | in |
||

54 | expr , inputs'@outputs'@locals'@locals, assign_inputs::eqs' |
||

55 | |||

56 | |||

57 | |||

58 | |||

59 | (* |
||

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

61 | |||

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

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

64 | |||

65 | *) |
||

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

67 | let inline_tuple el = |
||

68 | List.fold_right (fun e (el_tail, locals, eqs) -> |
||

69 | let e', locals', eqs' = inline_expr e locals nodes in |
||

70 | e'::el_tail, locals', eqs'@eqs |
||

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

72 | in |
||

73 | let inline_pair e1 e2 = |
||

74 | let el', l', eqs' = inline_tuple [e1;e2] in |
||

75 | match el' with |
||

76 | | [e1'; e2'] -> e1', e2', l', eqs' |
||

77 | | _ -> assert false |
||

78 | in |
||

79 | let inline_triple e1 e2 e3 = |
||

80 | let el', l', eqs' = inline_tuple [e1;e2;e3] in |
||

81 | match el' with |
||

82 | | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs' |
||

83 | | _ -> assert false |
||

84 | in |
||

85 | |||

86 | match expr.expr_desc with |
||

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

88 | let args', locals', eqs' = inline_expr args locals nodes in |
||

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

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

91 | 867595f2 | ploc | (* let _ = Format.eprintf "Inlining call to %s@." id in |

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

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

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

95 | let node = inline_node node nodes in |
||

96 | let expr, locals', eqs'' = |
||

97 | inline_call expr args' reset locals' node in |
||

98 | expr, locals', eqs'@eqs'' |
||

99 | else |
||

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

101 | { expr with expr_desc = Expr_appl(id, args', reset)}, locals', eqs' |
||

102 | |||

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

104 | | Expr_const _ |
||

105 | | Expr_ident _ -> expr, locals, [] |
||

106 | | Expr_tuple el -> |
||

107 | let el', l', eqs' = inline_tuple el in |
||

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

109 | | Expr_ite (g, t, e) -> |
||

110 | let g', t', e', l', eqs' = inline_triple g t e in |
||

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

112 | | Expr_arrow (e1, e2) -> |
||

113 | let e1', e2', l', eqs' = inline_pair e1 e2 in |
||

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

115 | | Expr_fby (e1, e2) -> |
||

116 | let e1', e2', l', eqs' = inline_pair e1 e2 in |
||

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

118 | | Expr_array el -> |
||

119 | let el', l', eqs' = inline_tuple el in |
||

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

121 | | Expr_access (e, dim) -> |
||

122 | let e', l', eqs' = inline_expr e locals nodes in |
||

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

124 | | Expr_power (e, dim) -> |
||

125 | let e', l', eqs' = inline_expr e locals nodes in |
||

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

127 | | Expr_pre e -> |
||

128 | let e', l', eqs' = inline_expr e locals nodes in |
||

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

130 | | Expr_when (e, id, label) -> |
||

131 | let e', l', eqs' = inline_expr e locals nodes in |
||

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

133 | | Expr_merge (id, branches) -> |
||

134 | let el, l', eqs' = inline_tuple (List.map snd branches) in |
||

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

136 | { expr with expr_desc = Expr_merge (id, branches') }, l', eqs' |
||

137 | and inline_node nd nodes = |
||

138 | let new_locals, eqs = |
||

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

140 | let eq_rhs', locals', new_eqs' = |
||

141 | inline_expr eq.eq_rhs locals nodes |
||

142 | in |
||

143 | locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs |
||

144 | ) (nd.node_locals, []) nd.node_eqs |
||

145 | in |
||

146 | { nd with |
||

147 | node_locals = new_locals; |
||

148 | node_eqs = eqs |
||

149 | } |
||

150 | |||

151 | let inline_all_calls node nodes = |
||

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

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

154 | |||

155 | |||

156 | |||

157 | |||

158 | |||

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

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

161 | let rename_local_node nodes prefix id = |
||

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

163 | prefix ^ id |
||

164 | else |
||

165 | id |
||

166 | in |
||

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

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

169 | |||

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

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

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

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

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

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

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

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

178 | |||

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

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

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

182 | mkvar_decl |
||

183 | loc |
||

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

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

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

187 | false) |
||

188 | ) (Utils.enumerate nb_outputs) |
||

189 | in |
||

190 | |||

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

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

193 | let ok_output = mkvar_decl |
||

194 | loc |
||

195 | (ok_ident, |
||

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

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

198 | false) |
||

199 | in |
||

200 | b50c665d | ploc | let main_ok_expr = |

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

202 | match ok_i with |
||

203 | | [] -> assert false |
||

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

205 | | hd::tl -> |
||

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

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

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

209 | in |
||

210 | |||

211 | (* Building main node *) |
||

212 | |||

213 | b09a175c | ploc | let main_node = { |

214 | node_id = "check"; |
||

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

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

217 | node_inputs = main_orig_node.node_inputs; |
||

218 | node_outputs = [ok_output]; |
||

219 | node_locals = []; |
||

220 | node_gencalls = []; |
||

221 | node_checks = []; |
||

222 | node_asserts = []; |
||

223 | node_eqs = [ |
||

224 | { eq_loc = loc; |
||

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

226 | b09a175c | ploc | eq_rhs = |

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

228 | let call_orig = |
||

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

230 | let call_inlined = |
||

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

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

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

234 | b50c665d | ploc | }; |

235 | { eq_loc = loc; |
||

236 | eq_lhs = [ok_ident]; |
||

237 | eq_rhs = main_ok_expr; |
||

238 | } |
||

239 | ]; |
||

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

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

242 | b09a175c | ploc | node_spec = Some |

243 | {requires = []; |
||

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

245 | behaviors = []; |
||

246 | spec_loc = loc |
||

247 | b09a175c | ploc | }; |

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

249 | b09a175c | ploc | } |

250 | in |
||

251 | let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc }] in |
||

252 | let new_prog = others@nodes_origs@nodes_inlined@main in |
||

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

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

255 | |||

256 | 592f508c | ploc | |

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

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

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

260 | Format.fprintf witness_fmt |
||

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

262 | Printers.pp_prog witness_fmt new_prog; |
||

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

264 | () (* xx *) |
||

265 | |||

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

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

268 | let main_node, other_nodes, other_tops = |
||

269 | List.fold_left |
||

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

271 | match top.top_decl_desc with |
||

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

273 | Some top, nodes, others |
||

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

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

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

277 | in |
||

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

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

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

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

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

283 | witness |
||

284 | basename |
||

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

286 | prog res type_env clock_env |
||

287 | ); |
||

288 | b09a175c | ploc | res |

289 | b50c665d | ploc | |

290 | (* Local Variables: *) |
||

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

292 | (* End: *) |