## lustrec/src/inliner.ml @ 820616b1

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 | 8446bf03 | ploc | open Lustre_types |

13 | b09a175c | ploc | 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 | fc886259 | xthirioux | let is_node_var node v = |

31 | ```
try
``` |
||

32 | ignore (Corelang.get_node_var v node); true |
||

33 | with Not_found -> false |
||

34 | b09a175c | ploc | |

35 | 333e3a25 | ploc | ```
(* let rename_expr rename expr = expr_replace_var rename expr *)
``` |

36 | ```
(*
``` |
||

37 | af5af1e8 | ploc | ```
let rename_eq rename eq =
``` |

38 | ```
{ eq with
``` |
||

39 | ```
eq_lhs = List.map rename eq.eq_lhs;
``` |
||

40 | ```
eq_rhs = rename_expr rename eq.eq_rhs
``` |
||

41 | ```
}
``` |
||

42 | 333e3a25 | ploc | ```
*)
``` |

43 | |||

44 | 45f0f48d | xthirioux | let rec add_expr_reset_cond cond expr = |

45 | let aux = add_expr_reset_cond cond in |
||

46 | let new_desc = |
||

47 | match expr.expr_desc with |
||

48 | | Expr_const _ |
||

49 | | Expr_ident _ -> expr.expr_desc |
||

50 | | Expr_tuple el -> Expr_tuple (List.map aux el) |
||

51 | | Expr_ite (c, t, e) -> Expr_ite (aux c, aux t, aux e) |
||

52 | |||

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

54 | ```
(* we replace the expression e1 -> e2 by e1 -> (if cond then e1 else e2) *)
``` |
||

55 | let e1 = aux e1 and e2 = aux e2 in |
||

56 | ```
(* inlining is performed before typing. we can leave the fields free *)
``` |
||

57 | let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in |
||

58 | Expr_arrow (e1, new_e2) |
||

59 | |||

60 | | Expr_fby _ -> assert false (* TODO: deal with fby. This hasn't been much handled yet *) |
||

61 | |||

62 | | Expr_array el -> Expr_array (List.map aux el) |
||

63 | | Expr_access (e, dim) -> Expr_access (aux e, dim) |
||

64 | | Expr_power (e, dim) -> Expr_power (aux e, dim) |
||

65 | | Expr_pre e -> Expr_pre (aux e) |
||

66 | | Expr_when (e, id, l) -> Expr_when (aux e, id, l) |
||

67 | | Expr_merge (id, cases) -> Expr_merge (id, List.map (fun (l,e) -> l, aux e) cases) |
||

68 | |||

69 | | Expr_appl (id, args, reset_opt) -> |
||

70 | ```
(* we "add" cond to the reset field. *)
``` |
||

71 | let new_reset = match reset_opt with |
||

72 | None -> cond |
||

73 | | Some cond' -> mkpredef_call cond'.expr_loc "||" [cond; cond'] |
||

74 | ```
in
``` |
||

75 | Expr_appl (id, args, Some new_reset) |
||

76 | |||

77 | |||

78 | ```
in
``` |
||

79 | { expr with expr_desc = new_desc } |
||

80 | |||

81 | let add_eq_reset_cond cond eq = |
||

82 | { eq with eq_rhs = add_expr_reset_cond cond eq.eq_rhs } |
||

83 | ec433d69 | xthirioux | ```
(*
``` |

84 | ```
let get_static_inputs input_arg_list =
``` |
||

85 | ```
List.fold_right (fun (vdecl, arg) res ->
``` |
||

86 | ```
if vdecl.var_dec_const
``` |
||

87 | ```
then (vdecl.var_id, Corelang.dimension_of_expr arg) :: res
``` |
||

88 | ```
else res)
``` |
||

89 | ```
input_arg_list []
``` |
||

90 | |||

91 | ```
let get_carrier_inputs input_arg_list =
``` |
||

92 | ```
List.fold_right (fun (vdecl, arg) res ->
``` |
||

93 | ```
if Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc
``` |
||

94 | ```
then (vdecl.var_id, ident_of_expr arg) :: res
``` |
||

95 | ```
else res)
``` |
||

96 | ```
input_arg_list []
``` |
||

97 | ```
*)
``` |
||

98 | b09a175c | ploc | ```
(*
``` |

99 | fc886259 | xthirioux | ```
expr, locals', eqs = inline_call id args' reset locals node nodes
``` |

100 | b09a175c | ploc | |

101 | ```
We select the called node equations and variables.
``` |
||

102 | ```
renamed_inputs = args
``` |
||

103 | ```
renamed_eqs
``` |
||

104 | |||

105 | ```
the resulting expression is tuple_of_renamed_outputs
``` |
||

106 | ```
``` |
||

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

108 | ```
*)
``` |
||

109 | 45f0f48d | xthirioux | ```
(** [inline_call node loc uid args reset locals caller] returns a tuple (expr,
``` |

110 | ```
locals, eqs, asserts)
``` |
||

111 | ```
*)
``` |
||

112 | let inline_call node loc uid args reset locals caller = |
||

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

114 | fc886259 | xthirioux | if v = tag_true || v = tag_false || not (is_node_var node v) then v else |

115 | Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v) |
||

116 | b09a175c | ploc | ```
in
``` |

117 | 333e3a25 | ploc | let eqs, auts = get_node_eqs node in |

118 | let eqs' = List.map (rename_eq (fun x -> x) rename) eqs in |
||

119 | let auts' = List.map (rename_aut (fun x -> x) rename) auts in |
||

120 | ec433d69 | xthirioux | let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in |

121 | let static_inputs, dynamic_inputs = List.partition (fun (vdecl, arg) -> vdecl.var_dec_const) input_arg_list in |
||

122 | let static_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) static_inputs in |
||

123 | let carrier_inputs, other_inputs = List.partition (fun (vdecl, arg) -> Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc) dynamic_inputs in |
||

124 | let carrier_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg) carrier_inputs in |
||

125 | fc886259 | xthirioux | let rename_static v = |

126 | ```
try
``` |
||

127 | ec433d69 | xthirioux | snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) static_inputs) |

128 | with Not_found -> Dimension.mkdim_ident loc v in |
||

129 | fc886259 | xthirioux | let rename_carrier v = |

130 | ```
try
``` |
||

131 | ec433d69 | xthirioux | snd (List.find (fun (vdecl, _) -> v = vdecl.var_id) carrier_inputs) |

132 | fc886259 | xthirioux | with Not_found -> v in |

133 | let rename_var v = |
||

134 | ec433d69 | xthirioux | let vdecl = |

135 | Corelang.mkvar_decl v.var_loc |
||

136 | (rename v.var_id, |
||

137 | { v.var_dec_type with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc }, |
||

138 | { v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc }, |
||

139 | v.var_dec_const, |
||

140 | 66359a5e | ploc | Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value, |

141 | v.var_parent_nodeid (* we keep the original parent name *) |
||

142 | ) in |
||

143 | ec433d69 | xthirioux | ```
begin
``` |

144 | 45f0f48d | xthirioux | ```
(*
``` |

145 | ```
(try
``` |
||

146 | ```
Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
``` |
||

147 | ```
Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
``` |
||

148 | ```
with Not_found -> ());
``` |
||

149 | ```
(try
``` |
||

150 | ```
Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
``` |
||

151 | ```
with Not_found -> ());
``` |
||

152 | ```
(*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
``` |
||

153 | ```
*)
``` |
||

154 | ec433d69 | xthirioux | ```
vdecl
``` |

155 | ```
end
``` |
||

156 | 01d48bb0 | xthirioux | ```
(*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
``` |

157 | ec433d69 | xthirioux | ```
in
``` |

158 | let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in |
||

159 | b09a175c | ploc | let outputs' = List.map rename_var node.node_outputs in |

160 | ec433d69 | xthirioux | let locals' = |

161 | 01d48bb0 | xthirioux | (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs) |

162 | ec433d69 | xthirioux | @ (List.map rename_var node.node_locals) |

163 | 01d48bb0 | xthirioux | ```
in
``` |

164 | b09a175c | ploc | ```
(* checking we are at the appropriate (early) step: node_checks and
``` |

165 | ```
node_gencalls should be empty (not yet assigned) *)
``` |
||

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

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

168 | |||

169 | 45f0f48d | xthirioux | ```
(* Expressing reset locally in equations *)
``` |

170 | 333e3a25 | ploc | let eqs_r' = |

171 | let all_eqs = (List.map (fun eq -> Eq eq) eqs') @ (List.map (fun aut -> Aut aut) auts') in |
||

172 | 45f0f48d | xthirioux | match reset with |

173 | 333e3a25 | ploc | None -> all_eqs |

174 | | Some cond -> ( |
||

175 | assert (auts' = []); (* TODO: we do not handle properly automaton in case of reset call *) |
||

176 | List.map (fun eq -> Eq (add_eq_reset_cond cond eq)) eqs' |
||

177 | ```
)
``` |
||

178 | 45f0f48d | xthirioux | ```
in
``` |

179 | 333e3a25 | ploc | let assign_inputs = Eq (mkeq loc (List.map (fun v -> v.var_id) inputs', |

180 | expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs))) in |
||

181 | fc886259 | xthirioux | let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs') |

182 | b09a175c | ploc | ```
in
``` |

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

184 | List.map |
||

185 | (fun a -> |
||

186 | {a with assert_expr = |
||

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

188 | 333e3a25 | ploc | rename_expr (fun x -> x) rename expr |

189 | 45f0f48d | xthirioux | ```
})
``` |

190 | af5af1e8 | ploc | node.node_asserts |

191 | ```
in
``` |
||

192 | 04a63d25 | xthirioux | let annots' = |

193 | Plugins.inline_annots rename node.node_annot |
||

194 | ```
in
``` |
||

195 | af5af1e8 | ploc | expr, |

196 | inputs'@outputs'@locals'@locals, |
||

197 | 45f0f48d | xthirioux | assign_inputs::eqs_r', |

198 | 04a63d25 | xthirioux | asserts', |

199 | ```
annots'
``` |
||

200 | b09a175c | ploc | |

201 | |||

202 | |||

203 | fc886259 | xthirioux | let inline_table = Hashtbl.create 23 |

204 | b09a175c | ploc | |

205 | ```
(*
``` |
||

206 | fc886259 | xthirioux | ```
new_expr, new_locals, new_eqs = inline_expr expr locals node nodes
``` |

207 | b09a175c | ploc | ```
``` |

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

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

210 | |||

211 | ```
*)
``` |
||

212 | fc886259 | xthirioux | let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes = |

213 | 566dbf49 | ploc | let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |

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

215 | b09a175c | ploc | let inline_tuple el = |

216 | 04a63d25 | xthirioux | List.fold_right (fun e (el_tail, locals, eqs, asserts, annots) -> |

217 | let e', locals', eqs', asserts', annots' = inline_expr e locals node nodes in |
||

218 | e'::el_tail, locals', eqs'@eqs, asserts@asserts', annots@annots' |
||

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

220 | b09a175c | ploc | ```
in
``` |

221 | let inline_pair e1 e2 = |
||

222 | 04a63d25 | xthirioux | let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in |

223 | b09a175c | ploc | match el' with |

224 | d2d9d4cb | ploc | | [e1'; e2'] -> e1', e2', l', eqs', asserts', annots' |

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

226 | ```
in
``` |
||

227 | let inline_triple e1 e2 e3 = |
||

228 | 04a63d25 | xthirioux | let el', l', eqs', asserts', annots' = inline_tuple [e1;e2;e3] in |

229 | b09a175c | ploc | match el' with |

230 | 04a63d25 | xthirioux | | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts', annots' |

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

232 | ```
in
``` |
||

233 | 566dbf49 | ploc | |

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

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

236 | 333e3a25 | ploc | let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in |

237 | if List.exists (check_node_name id) nodes && (* the current node call is provided |
||

238 | ```
as arguments nodes *)
``` |
||

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

240 | ```
it is explicitely inlined here *)
``` |
||

241 | then ( |
||

242 | ```
(* Format.eprintf "Inlining call to %s in expression %a@." id Printers.pp_expr expr; *)
``` |
||

243 | ```
(* The node should be inlined *)
``` |
||

244 | ```
(* let _ = Format.eprintf "Inlining call to %s@." id in *)
``` |
||

245 | let called = try List.find (check_node_name id) nodes |
||

246 | with Not_found -> (assert false) in |
||

247 | let called = node_of_top called in |
||

248 | let called' = inline_node called nodes in |
||

249 | let expr, locals', eqs'', asserts'', annots'' = |
||

250 | inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in |
||

251 | expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots'' |
||

252 | ```
)
``` |
||

253 | ```
else
``` |
||

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

255 | { expr with expr_desc = Expr_appl(id, args', reset)}, |
||

256 | locals', |
||

257 | eqs', |
||

258 | asserts', |
||

259 | ```
annots'
``` |
||

260 | b09a175c | ploc | |

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

262 | | Expr_const _ |
||

263 | 04a63d25 | xthirioux | | Expr_ident _ -> expr, locals, [], [], [] |

264 | b09a175c | ploc | | Expr_tuple el -> |

265 | 333e3a25 | ploc | let el', l', eqs', asserts', annots' = inline_tuple el in |

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

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

268 | 333e3a25 | ploc | let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in |

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

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

271 | 333e3a25 | ploc | let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in |

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

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

274 | 333e3a25 | ploc | let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in |

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

276 | b09a175c | ploc | | Expr_array el -> |

277 | 333e3a25 | ploc | let el', l', eqs', asserts', annots' = inline_tuple el in |

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

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

280 | 333e3a25 | ploc | let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |

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

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

283 | 333e3a25 | ploc | let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |

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

285 | b09a175c | ploc | | Expr_pre e -> |

286 | 333e3a25 | ploc | let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |

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

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

289 | 333e3a25 | ploc | let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in |

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

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

292 | 333e3a25 | ploc | let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in |

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

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

295 | fc886259 | xthirioux | |

296 | and inline_node ?(selection_on_annotation=false) node nodes = |
||

297 | ec433d69 | xthirioux | try copy_node (Hashtbl.find inline_table node.node_id) |

298 | fc886259 | xthirioux | with Not_found -> |

299 | 333e3a25 | ploc | let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in |

300 | let eqs, auts = get_node_eqs node in |
||

301 | assert (auts = []); (* No inlining of automaton yet. One should visit each |
||

302 | ```
handler eqs and perform similar computation *)
``` |
||

303 | let new_locals, stmts, asserts, annots = |
||

304 | List.fold_left (fun (locals, stmts, asserts, annots) eq -> |
||

305 | let eq_rhs', locals', new_stmts', asserts', annots' = |
||

306 | inline_expr eq.eq_rhs locals node nodes |
||

307 | ```
in
``` |
||

308 | locals', Eq { eq with eq_rhs = eq_rhs' }::new_stmts'@stmts, asserts'@asserts, annots'@annots |
||

309 | ) (node.node_locals, [], node.node_asserts, node.node_annot) eqs |
||

310 | ```
in
``` |
||

311 | let inlined = |
||

312 | { node with |
||

313 | node_locals = new_locals; |
||

314 | node_stmts = stmts; |
||

315 | node_asserts = asserts; |
||

316 | node_annot = annots; |
||

317 | ```
}
``` |
||

318 | ```
in
``` |
||

319 | ```
begin
``` |
||

320 | ```
(*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
``` |
||

321 | Hashtbl.add inline_table node.node_id inlined; |
||

322 | ```
inlined
``` |
||

323 | ```
end
``` |
||

324 | b09a175c | ploc | |

325 | let inline_all_calls node nodes = |
||

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

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

328 | |||

329 | |||

330 | |||

331 | |||

332 | |||

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

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

335 | let rename_local_node nodes prefix id = |
||

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

337 | prefix ^ id |
||

338 | ```
else
``` |
||

339 | ```
id
``` |
||

340 | ```
in
``` |
||

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

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

343 | |||

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

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

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

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

348 | 333e3a25 | ploc | let orig = rename_prog orig_rename (* f_node *) identity (* f_var *) identity (* f_const *) orig in |

349 | b09a175c | ploc | let inlined = rename_prog inlined_rename identity identity inlined in |

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

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

352 | |||

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

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

355 | ec433d69 | xthirioux | let ok_ident = "OK" in |

356 | b50c665d | ploc | let ok_i = List.map (fun id -> |

357 | ```
mkvar_decl
``` |
||

358 | ```
loc
``` |
||

359 | ec433d69 | xthirioux | (Format.sprintf "%s_%i" ok_ident id, |

360 | b50c665d | ploc | {ty_dec_desc=Tydec_bool; ty_dec_loc=loc}, |

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

362 | ec433d69 | xthirioux | false, |

363 | 66359a5e | ploc | None, |

364 | ```
None
``` |
||

365 | ```
)
``` |
||

366 | b50c665d | ploc | ) (Utils.enumerate nb_outputs) |

367 | ```
in
``` |
||

368 | |||

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

370 | b09a175c | ploc | let ok_output = mkvar_decl |

371 | ```
loc
``` |
||

372 | (ok_ident, |
||

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

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

375 | ec433d69 | xthirioux | false, |

376 | 66359a5e | ploc | None, |

377 | ```
None
``` |
||

378 | ```
)
``` |
||

379 | b09a175c | ploc | ```
in
``` |

380 | b50c665d | ploc | let main_ok_expr = |

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

382 | match ok_i with |
||

383 | | [] -> assert false |
||

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

385 | | hd::tl -> |
||

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

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

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

389 | ```
in
``` |
||

390 | |||

391 | ```
(* Building main node *)
``` |
||

392 | |||

393 | b08ffca7 | xthirioux | let ok_i_eq = |

394 | { eq_loc = loc; |
||

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

396 | eq_rhs = |
||

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

398 | let call_orig = |
||

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

400 | let call_inlined = |
||

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

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

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

404 | } in |
||

405 | let ok_eq = |
||

406 | { eq_loc = loc; |
||

407 | eq_lhs = [ok_ident]; |
||

408 | eq_rhs = main_ok_expr; |
||

409 | } in |
||

410 | b09a175c | ploc | let main_node = { |

411 | node_id = "check"; |
||

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

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

414 | node_inputs = main_orig_node.node_inputs; |
||

415 | node_outputs = [ok_output]; |
||

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

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

418 | node_checks = []; |
||

419 | node_asserts = []; |
||

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

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

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

423 | b09a175c | ploc | node_spec = Some |

424 | f4cba4b8 | ploc | (Contract |

425 | (mk_contract_guarantees |
||

426 | (mkeexpr loc (mkexpr loc (Expr_ident ok_ident))) |
||

427 | ```
)
``` |
||

428 | ```
);
``` |
||

429 | node_annot = []; |
||

430 | node_iscontract = true; |
||

431 | ```
}
``` |
||

432 | b09a175c | ploc | ```
in
``` |

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

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

435 | 04a63d25 | xthirioux | ```
(*
``` |

436 | ```
let _ = Typing.type_prog type_env new_prog in
``` |
||

437 | ```
let _ = Clock_calculus.clock_prog clock_env new_prog in
``` |
||

438 | ```
*)
``` |
||

439 | |||

440 | 1bff14ac | ploc | let witness_file = (Options_management.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in |

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

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

443 | ec433d69 | xthirioux | ```
begin
``` |

444 | List.iter (fun vdecl -> Typing.try_unify Type_predef.type_bool vdecl.var_type vdecl.var_loc) (ok_output::ok_i); |
||

445 | Format.fprintf witness_fmt |
||

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

447 | Printers.pp_prog witness_fmt new_prog; |
||

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

449 | ```
()
``` |
||

450 | end (* xx *) |
||

451 | b09a175c | ploc | |

452 | 2d27eedd | ploc | let global_inline basename prog (*type_env clock_env*) = |

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

454 | let main_node, other_nodes, other_tops = |
||

455 | ec433d69 | xthirioux | List.fold_right |

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

457 | b09a175c | ploc | match top.top_decl_desc with |

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

459 | Some top, nodes, others |
||

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

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

462 | ec433d69 | xthirioux | prog (None, [], []) |

463 | b09a175c | ploc | ```
in
``` |

464 | 85da3a4b | ploc | |

465 | b09a175c | ploc | ```
(* Recursively each call of a node in the top node is replaced *)
``` |

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

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

468 | ec433d69 | xthirioux | let res = List.map (fun top -> if check_node_name !Options.main_node top then main_node' else top) prog in |

469 | 85da3a4b | ploc | ```
(* Code snippet from unstable branch. May be used when reactivating witnesses.
``` |

470 | ```
let res = main_node'::other_tops in
``` |
||

471 | 53206908 | xthirioux | ```
if !Options.witnesses then (
``` |

472 | ```
witness
``` |
||

473 | ```
basename
``` |
||

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

475 | ```
prog res type_env clock_env
``` |
||

476 | ```
);
``` |
||

477 | 85da3a4b | ploc | ```
*)
``` |

478 | b09a175c | ploc | ```
res
``` |

479 | b50c665d | ploc | |

480 | 264a4844 | ploc | let pp_inline_calls fmt prog = |

481 | 566dbf49 | ploc | let local_anns = Annotations.get_expr_annotations keyword in |

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

483 | Format.fprintf fmt "@[<v 0>Inlined expresssions in node (by tags):@ %a@]" |
||

484 | (fprintf_list ~sep:"" |
||

485 | (fun fmt top -> |
||

486 | match top.top_decl_desc with |
||

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

488 | Format.fprintf fmt "%s: {@[<v 0>%a}@]@ " |
||

489 | nd.node_id |
||

490 | (fprintf_list ~sep:"@ " (fun fmt tag -> Format.fprintf fmt "%i" tag)) |
||

491 | (List.fold_left |
||

492 | (fun accu (id, tag) -> if id = nd.node_id then tag::accu else accu) |
||

493 | ```
[]
``` |
||

494 | ```
local_anns
``` |
||

495 | ```
)
``` |
||

496 | ```
(* | Node nd -> Format.fprintf fmt "%s: no inline annotations" nd.node_id *)
``` |
||

497 | | _ -> () |
||

498 | ```
))
``` |
||

499 | ```
prog
``` |
||

500 | |||

501 | |||

502 | let local_inline prog (* type_env clock_env *) = |
||

503 | Log.report ~level:2 (fun fmt -> Format.fprintf fmt ".. @[<v 2>Inlining@,"); |
||

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

505 | let prog = |
||

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

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

508 | ISet.iter (fun node_id -> Log.report ~level:2 (fun fmt -> Format.fprintf fmt "Node %s has local expression annotations@ " node_id)) |
||

509 | nodes_with_anns; |
||

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

511 | ( match top.top_decl_desc with |
||

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

513 | Log.report ~level:2 (fun fmt -> Format.fprintf fmt "[local inline] Processing node %s@ " nd.node_id); |
||

514 | let inlined_node = inline_node ~selection_on_annotation:true nd prog in |
||

515 | ```
(* Format.eprintf "Before inline@.%a@.After:@.%a@." *)
``` |
||

516 | ```
(* Printers.pp_node nd *)
``` |
||

517 | ```
(* Printers.pp_node inlined_node; *)
``` |
||

518 | { top with top_decl_desc = Node inlined_node } |
||

519 | |||

520 | | _ -> top |
||

521 | )::accu) prog [] |
||

522 | |||

523 | ```
)
``` |
||

524 | else ( |
||

525 | Log.report ~level:2 (fun fmt -> Format.fprintf fmt "No local inline information!@ "); |
||

526 | ```
prog
``` |
||

527 | ```
)
``` |
||

528 | ```
in
``` |
||

529 | Log.report ~level:2 (fun fmt -> Format.fprintf fmt "@]@,"); |
||

530 | 566dbf49 | ploc | ```
prog
``` |

531 | |||

532 | b50c665d | ploc | ```
(* Local Variables: *)
``` |

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

534 | ```
(* End: *)
``` |