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

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


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


31

let rename_expr rename expr = expr_replace_var rename expr

32

let rename_eq rename eq =

33

{ eq with

34

eq_lhs = List.map rename eq.eq_lhs;

35

eq_rhs = rename_expr rename eq.eq_rhs

36

}

37


38

(*

39

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

40


41

We select the called node equations and variables.

42

renamed_inputs = args

43

renamed_eqs

44


45

the resulting expression is tuple_of_renamed_outputs

46


47

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

48

TODO: deal with reset

49

*)

50

let inline_call orig_expr args reset locals node =

51

let loc = orig_expr.expr_loc in

52

let uid = orig_expr.expr_tag in

53

let rename v =

54

if v = tag_true  v = tag_false then v else

55

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

56

node.node_id uid v;

57

Format.flush_str_formatter ())

58

in

59

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

60

in

61

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

62

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

63

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

64

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

65


66

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

67

node_gencalls should be empty (not yet assigned) *)

68

assert (node.node_checks = []);

69

assert (node.node_gencalls = []);

70


71

(* Bug included: todo deal with reset *)

72

assert (reset = None);

73


74

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

75

let expr = expr_of_expr_list

76

loc

77

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

78

in

79

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

80

List.map

81

(fun a >

82

{a with assert_expr =

83

let expr = a.assert_expr in

84

rename_expr rename expr

85

})

86

node.node_asserts

87

in

88

expr,

89

inputs'@outputs'@locals'@locals,

90

assign_inputs::eqs',

91

asserts'

92


93


94


95


96

(*

97

new_expr, new_locals, new_eqs = inline_expr expr locals nodes

98


99

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

100

variables and the code of called node instance added to new_eqs

101


102

*)

103

let rec inline_expr ?(selection_on_annotation=false) expr locals nodes =

104

let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in

105

let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in

106

let inline_tuple el =

107

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

108

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

109

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

110

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

111

in

112

let inline_pair e1 e2 =

113

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

114

match el' with

115

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

116

 _ > assert false

117

in

118

let inline_triple e1 e2 e3 =

119

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

120

match el' with

121

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

122

 _ > assert false

123

in

124


125

match expr.expr_desc with

126

 Expr_appl (id, args, reset) >

127

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

128

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

129

as arguments nodes *)

130

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

131

it is explicitely inlined here *)

132

then

133

(* The node should be inlined *)

134

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

135

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

136

with Not_found > (assert false) in

137

let node = node_of_top node in

138

let node = inline_node node nodes in

139

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

140

inline_call expr args' reset locals' node in

141

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

142

else

143

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

144

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

145

locals',

146

eqs',

147

asserts'

148


149

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

150

 Expr_const _

151

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

152

 Expr_tuple el >

153

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

154

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

155

 Expr_ite (g, t, e) >

156

let g', t', e', l', eqs', asserts' = inline_triple g t e in

157

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

158

 Expr_arrow (e1, e2) >

159

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

160

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

161

 Expr_fby (e1, e2) >

162

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

163

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

164

 Expr_array el >

165

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

166

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

167

 Expr_access (e, dim) >

168

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

169

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

170

 Expr_power (e, dim) >

171

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

172

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

173

 Expr_pre e >

174

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

175

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

176

 Expr_when (e, id, label) >

177

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

178

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

179

 Expr_merge (id, branches) >

180

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

181

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

182

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

183

and inline_node ?(selection_on_annotation=false) nd nodes =

184

let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in

185

let new_locals, eqs, asserts =

186

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

187

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

188

inline_expr eq.eq_rhs locals nodes

189

in

190

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

191

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

192

in

193

{ nd with

194

node_locals = new_locals;

195

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

196

node_asserts = asserts;

197

}

198


199

let inline_all_calls node nodes =

200

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

201

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

202


203


204


205


206


207

let witness filename main_name orig inlined type_env clock_env =

208

let loc = Location.dummy_loc in

209

let rename_local_node nodes prefix id =

210

if List.exists (check_node_name id) nodes then

211

prefix ^ id

212

else

213

id

214

in

215

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

216

Node nd > nd  _ > assert false in

217


218

let orig_rename = rename_local_node orig "orig_" in

219

let inlined_rename = rename_local_node inlined "inlined_" in

220

let identity = (fun x > x) in

221

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

222

let orig = rename_prog orig_rename identity identity orig in

223

let inlined = rename_prog inlined_rename identity identity inlined in

224

let nodes_origs, others = List.partition is_node orig in

225

let nodes_inlined, _ = List.partition is_node inlined in

226


227

(* One ok_i boolean variable per output var *)

228

let nb_outputs = List.length main_orig_node.node_outputs in

229

let ok_i = List.map (fun id >

230

mkvar_decl

231

loc

232

("OK" ^ string_of_int id,

233

{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},

234

{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},

235

false)

236

) (Utils.enumerate nb_outputs)

237

in

238


239

(* OK = ok_1 and ok_2 and ... ok_n1 *)

240

let ok_ident = "OK" in

241

let ok_output = mkvar_decl

242

loc

243

(ok_ident,

244

{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},

245

{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},

246

false)

247

in

248

let main_ok_expr =

249

let mkv x = mkexpr loc (Expr_ident x) in

250

match ok_i with

251

 [] > assert false

252

 [x] > mkv x.var_id

253

 hd::tl >

254

List.fold_left (fun accu elem >

255

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

256

) (mkv hd.var_id) tl

257

in

258


259

(* Building main node *)

260


261

let ok_i_eq =

262

{ eq_loc = loc;

263

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

264

eq_rhs =

265

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

266

let call_orig =

267

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

268

let call_inlined =

269

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

270

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

271

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

272

} in

273

let ok_eq =

274

{ eq_loc = loc;

275

eq_lhs = [ok_ident];

276

eq_rhs = main_ok_expr;

277

} in

278

let main_node = {

279

node_id = "check";

280

node_type = Types.new_var ();

281

node_clock = Clocks.new_var true;

282

node_inputs = main_orig_node.node_inputs;

283

node_outputs = [ok_output];

284

node_locals = ok_i;

285

node_gencalls = [];

286

node_checks = [];

287

node_asserts = [];

288

node_stmts = [Eq ok_i_eq; Eq ok_eq];

289

node_dec_stateless = false;

290

node_stateless = None;

291

node_spec = Some

292

{requires = [];

293

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

294

behaviors = [];

295

spec_loc = loc

296

};

297

node_annot = [];

298

}

299

in

300

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

301

let new_prog = others@nodes_origs@nodes_inlined@main in

302

let _ = Typing.type_prog type_env new_prog in

303

let _ = Clock_calculus.clock_prog clock_env new_prog in

304


305


306

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

307

let witness_out = open_out witness_file in

308

let witness_fmt = Format.formatter_of_out_channel witness_out in

309

Format.fprintf witness_fmt

310

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

311

Printers.pp_prog witness_fmt new_prog;

312

Format.fprintf witness_fmt "@.";

313

() (* xx *)

314


315

let global_inline basename prog type_env clock_env =

316

(* We select the main node desc *)

317

let main_node, other_nodes, other_tops =

318

List.fold_left

319

(fun (main_opt, nodes, others) top >

320

match top.top_decl_desc with

321

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

322

Some top, nodes, others

323

 Node _ > main_opt, top::nodes, others

324

 _ > main_opt, nodes, top::others)

325

(None, [], []) prog

326

in

327

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

328

let main_node = Utils.desome main_node in

329

let main_node' = inline_all_calls main_node other_nodes in

330

let res = main_node'::other_tops in

331

if !Options.witnesses then (

332

witness

333

basename

334

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

335

prog res type_env clock_env

336

);

337

res

338


339

let local_inline basename prog type_env clock_env =

340

let local_anns = Annotations.get_expr_annotations keyword in

341

if local_anns != [] then (

342

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

343

ISet.iter (fun node_id > Format.eprintf "Node %s has local expression annotations@." node_id) nodes_with_anns;

344

List.fold_right (fun top accu >

345

( match top.top_decl_desc with

346

 Node nd when ISet.mem nd.node_id nodes_with_anns >

347

{ top with top_decl_desc = Node (inline_node ~selection_on_annotation:true nd prog) }

348

 _ > top

349

)::accu) prog []

350


351

)

352

else

353

prog

354


355


356

(* Local Variables: *)

357

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

358

(* End: *)
