## lustrec / src / inliner.ml @ 7291cb80

History | View | Annotate | Download (8.58 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 | | Expr_uclock _ |
||

138 | | Expr_dclock _ |
||

139 | | Expr_phclock _ -> assert false |
||

140 | and inline_node nd nodes = |
||

141 | let new_locals, eqs = |
||

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

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

144 | inline_expr eq.eq_rhs locals nodes |
||

145 | in |
||

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

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

148 | in |
||

149 | { nd with |
||

150 | node_locals = new_locals; |
||

151 | node_eqs = eqs |
||

152 | } |
||

153 | |||

154 | let inline_all_calls node nodes = |
||

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

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

157 | |||

158 | |||

159 | |||

160 | |||

161 | |||

162 | let witness main_name orig inlined type_env clock_env = |
||

163 | let loc = Location.dummy_loc in |
||

164 | let rename_local_node nodes prefix id = |
||

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

166 | prefix ^ id |
||

167 | else |
||

168 | id |
||

169 | in |
||

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

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

172 | |||

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

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

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

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

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

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

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

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

181 | |||

182 | let ok_ident = "OK" in |
||

183 | let ok_output = mkvar_decl |
||

184 | loc |
||

185 | (ok_ident, |
||

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

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

188 | false) |
||

189 | in |
||

190 | let main_node = { |
||

191 | node_id = "check"; |
||

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

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

194 | node_inputs = main_orig_node.node_inputs; |
||

195 | node_outputs = [ok_output]; |
||

196 | node_locals = []; |
||

197 | node_gencalls = []; |
||

198 | node_checks = []; |
||

199 | node_asserts = []; |
||

200 | node_eqs = [ |
||

201 | { eq_loc = loc; |
||

202 | eq_lhs = [ok_ident]; |
||

203 | eq_rhs = |
||

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

205 | let call_orig = |
||

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

207 | let call_inlined = |
||

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

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

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

211 | }]; |
||

212 | node_spec = Some |
||

213 | {requires = []; |
||

214 | ensures = [EnsuresExpr (mkeexpr loc (EExpr_ident ok_ident))]; |
||

215 | behaviors = [] |
||

216 | }; |
||

217 | node_annot = None; |
||

218 | } |
||

219 | in |
||

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

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

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

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

224 | |||

225 | let witness_file = "witness.lus" in |
||

226 | let witness_out = open_out witness_file in |
||

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

228 | Format.fprintf witness_fmt |
||

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

230 | Printers.pp_prog witness_fmt new_prog; |
||

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

232 | () (* xx *) |
||

233 | |||

234 | let global_inline prog type_env clock_env = |
||

235 | (* We select the main node desc *) |
||

236 | let main_node, other_nodes, other_tops = |
||

237 | List.fold_left |
||

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

239 | match top.top_decl_desc with |
||

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

241 | Some top, nodes, others |
||

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

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

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

245 | in |
||

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

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

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

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

250 | if !Options.witnesses then |
||

251 | witness (match main_node.top_decl_desc with Node nd -> nd.node_id | _ -> assert false) prog res type_env clock_env; |
||

252 | res |