Revision b09a175c
src/inliner.ml  

1 
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 
let _ = Format.eprintf "Inlining call to %s@." id in 

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

93 
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 subexpressions *) 

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 
Also available in: Unified diff