1

(********************************************************************)

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

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

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

(*

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

if v = tag_true  v = tag_false then v else

45

(Format.fprintf Format.str_formatter "%s_%i_%s"

46

node.node_id uid v;

47

Format.flush_str_formatter ())

48

in

49

let eqs' = List.map (rename_eq rename) (get_node_eqs node)

50

in

51

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

52

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

53

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

54

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

55


56

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

57

node_gencalls should be empty (not yet assigned) *)

58

assert (node.node_checks = []);

59

assert (node.node_gencalls = []);

60


61

(* Bug included: todo deal with reset *)

62

assert (reset = None);

63


64

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

65

let expr = expr_of_expr_list

66

loc

67

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

68

in

69

let asserts' = (* We rename variables in assert expressions *)

70

List.map

71

(fun a >

72

{a with assert_expr =

73

let expr = a.assert_expr in

74

rename_expr rename expr

75

})

76

node.node_asserts

77

in

78

expr,

79

inputs'@outputs'@locals'@locals,

80

assign_inputs::eqs',

81

asserts'

82


83


84


85


86

(*

87

new_expr, new_locals, new_eqs = inline_expr expr locals nodes

88


89

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

90

variables and the code of called node instance added to new_eqs

91


92

*)

93

let rec inline_expr expr locals nodes =

94

let inline_tuple el =

95

List.fold_right (fun e (el_tail, locals, eqs, asserts) >

96

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

97

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

98

) el ([], locals, [], [])

99

in

100

let inline_pair e1 e2 =

101

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

102

match el' with

103

 [e1'; e2'] > e1', e2', l', eqs', asserts'

104

 _ > assert false

105

in

106

let inline_triple e1 e2 e3 =

107

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

108

match el' with

109

 [e1'; e2'; e3'] > e1', e2', e3', l', eqs', asserts'

110

 _ > assert false

111

in

112


113

match expr.expr_desc with

114

 Expr_appl (id, args, reset) >

115

let args', locals', eqs', asserts' = inline_expr args locals nodes in

116

if List.exists (check_node_name id) nodes then

117

(* The node should be inlined *)

118

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

119

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

120

with Not_found > (assert false) in

121

let node = node_of_top node in

122

let node = inline_node node nodes in

123

let expr, locals', eqs'', asserts'' =

124

inline_call expr args' reset locals' node in

125

expr, locals', eqs'@eqs'', asserts'@asserts''

126

else

127

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

128

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

129

locals',

130

eqs',

131

asserts'

132


133

(* For other cases, we just keep the structure, but convert subexpressions *)

134

 Expr_const _

135

 Expr_ident _ > expr, locals, [], []

136

 Expr_tuple el >

137

let el', l', eqs', asserts' = inline_tuple el in

138

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

139

 Expr_ite (g, t, e) >

140

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

 Expr_arrow (e1, e2) >

143

let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in

144

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

145

 Expr_fby (e1, e2) >

146

let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in

147

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

148

 Expr_array el >

149

let el', l', eqs', asserts' = inline_tuple el in

150

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

151

 Expr_access (e, dim) >

152

let e', l', eqs', asserts' = inline_expr e locals nodes in

153

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

154

 Expr_power (e, dim) >

155

let e', l', eqs', asserts' = inline_expr e locals nodes in

156

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

157

 Expr_pre e >

158

let e', l', eqs', asserts' = inline_expr e locals nodes in

159

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

160

 Expr_when (e, id, label) >

161

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

 Expr_merge (id, branches) >

164

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

165

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

166

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

167

and inline_node nd nodes =

168

let new_locals, eqs, asserts =

169

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

170

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

171

inline_expr eq.eq_rhs locals nodes

172

in

173

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

174

) (nd.node_locals, [], nd.node_asserts) (get_node_eqs nd)

175

in

176

{ nd with

177

node_locals = new_locals;

178

node_stmts = List.map (fun eq > Eq eq) eqs;

179

node_asserts = asserts;

180

}

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

let witness filename main_name orig inlined type_env clock_env =

191

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

(* 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_n1 *)

223

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

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

let ok_i_eq =

245

{ eq_loc = loc;

246

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

247

eq_rhs =

248

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

249

let call_orig =

250

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

251

let call_inlined =

252

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

253

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

254

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

255

} in

256

let ok_eq =

257

{ eq_loc = loc;

258

eq_lhs = [ok_ident];

259

eq_rhs = main_ok_expr;

260

} in

261

let main_node = {

262

node_id = "check";

263

node_type = Types.new_var ();

264

node_clock = Clocks.new_var true;

265

node_inputs = main_orig_node.node_inputs;

266

node_outputs = [ok_output];

267

node_locals = ok_i;

268

node_gencalls = [];

269

node_checks = [];

270

node_asserts = [];

271

node_stmts = [Eq ok_i_eq; Eq ok_eq];

272

node_dec_stateless = false;

273

node_stateless = None;

274

node_spec = Some

275

{requires = [];

276

ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))];

277

behaviors = [];

278

spec_loc = loc

279

};

280

node_annot = [];

281

}

282

in

283

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

284

let new_prog = others@nodes_origs@nodes_inlined@main in

285

let _ = Typing.type_prog type_env new_prog in

286

let _ = Clock_calculus.clock_prog clock_env new_prog in

287


288


289

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

290

let witness_out = open_out witness_file in

291

let witness_fmt = Format.formatter_of_out_channel witness_out in

292

Format.fprintf witness_fmt

293

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

294

Printers.pp_prog witness_fmt new_prog;

295

Format.fprintf witness_fmt "@.";

296

() (* xx *)

297


298

let global_inline basename prog type_env clock_env =

299

(* We select the main node desc *)

300

let main_node, other_nodes, other_tops =

301

List.fold_left

302

(fun (main_opt, nodes, others) top >

303

match top.top_decl_desc with

304

 Node nd when nd.node_id = !Options.main_node >

305

Some top, nodes, others

306

 Node _ > main_opt, top::nodes, others

307

 _ > main_opt, nodes, top::others)

308

(None, [], []) prog

309

in

310

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

311

let main_node = Utils.desome main_node in

312

let main_node' = inline_all_calls main_node other_nodes in

313

let res = main_node'::other_tops in

314

if !Options.witnesses then (

315

witness

316

basename

317

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

318

prog res type_env clock_env

319

);

320

res

321


322

(* Local Variables: *)

323

(* compilecommand:"make C .." *)

324

(* End: *)
