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 Lustre_types

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

let is_node_var node v =

31

try

32

ignore (Corelang.get_node_var v node); true

33

with Not_found > false

34


35

(* let rename_expr rename expr = expr_replace_var rename expr *)

36

(*

37

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

*)

43


44

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

(*

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

(*

99

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

100


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

(** [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

let rename v =

114

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

in

117

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

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

let rename_static v =

126

try

127

snd (List.find (fun (vdecl, _) > v = vdecl.var_id) static_inputs)

128

with Not_found > Dimension.mkdim_ident loc v in

129

let rename_carrier v =

130

try

131

snd (List.find (fun (vdecl, _) > v = vdecl.var_id) carrier_inputs)

132

with Not_found > v in

133

let rename_var v =

134

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

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

begin

144

(*

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

vdecl

155

end

156

(*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)

157

in

158

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

159

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

160

let locals' =

161

(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

@ (List.map rename_var node.node_locals)

163

in

164

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

(* Expressing reset locally in equations *)

170

let eqs_r' =

171

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

172

match reset with

173

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

in

179

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

let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')

182

in

183

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

rename_expr (fun x > x) rename expr

189

})

190

node.node_asserts

191

in

192

let annots' =

193

Plugins.inline_annots rename node.node_annot

194

in

195

expr,

196

inputs'@outputs'@locals'@locals,

197

assign_inputs::eqs_r',

198

asserts',

199

annots'

200


201


202


203

let inline_table = Hashtbl.create 23

204


205

(*

206

new_expr, new_locals, new_eqs = inline_expr expr locals node nodes

207


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

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

213

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

let inline_tuple el =

216

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

in

221

let inline_pair e1 e2 =

222

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

223

match el' with

224

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

225

 _ > assert false

226

in

227

let inline_triple e1 e2 e3 =

228

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

229

match el' with

230

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

231

 _ > assert false

232

in

233


234

match expr.expr_desc with

235

 Expr_appl (id, args, reset) >

236

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


261

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

262

 Expr_const _

263

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

264

 Expr_tuple el >

265

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

266

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

267

 Expr_ite (g, t, e) >

268

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

 Expr_arrow (e1, e2) >

271

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

 Expr_fby (e1, e2) >

274

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

 Expr_array el >

277

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

278

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

279

 Expr_access (e, dim) >

280

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

 Expr_power (e, dim) >

283

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

 Expr_pre e >

286

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

 Expr_when (e, id, label) >

289

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

 Expr_merge (id, branches) >

292

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


296

and inline_node ?(selection_on_annotation=false) node nodes =

297

try copy_node (Hashtbl.find inline_table node.node_id)

298

with Not_found >

299

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


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

let witness filename main_name orig inlined type_env clock_env =

334

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

let orig = rename_prog orig_rename (* f_node *) identity (* f_var *) identity (* f_const *) orig in

349

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

(* One ok_i boolean variable per output var *)

354

let nb_outputs = List.length main_orig_node.node_outputs in

355

let ok_ident = "OK" in

356

let ok_i = List.map (fun id >

357

mkvar_decl

358

loc

359

(Format.sprintf "%s_%i" ok_ident id,

360

{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},

361

{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},

362

false,

363

None,

364

None

365

)

366

) (Utils.enumerate nb_outputs)

367

in

368


369

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

370

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

false,

376

None,

377

None

378

)

379

in

380

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

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

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

node_locals = ok_i;

417

node_gencalls = [];

418

node_checks = [];

419

node_asserts = [];

420

node_stmts = [Eq ok_i_eq; Eq ok_eq];

421

node_dec_stateless = false;

422

node_stateless = None;

423

node_spec = Some

424

(mk_contract_guarantees (mkeexpr loc (mkexpr loc (Expr_ident ok_ident))));

425

node_annot = [];

426

}

427

in

428

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

429

let new_prog = others@nodes_origs@nodes_inlined@main in

430

(*

431

let _ = Typing.type_prog type_env new_prog in

432

let _ = Clock_calculus.clock_prog clock_env new_prog in

433

*)

434


435

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

436

let witness_out = open_out witness_file in

437

let witness_fmt = Format.formatter_of_out_channel witness_out in

438

begin

439

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

440

Format.fprintf witness_fmt

441

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

442

Printers.pp_prog witness_fmt new_prog;

443

Format.fprintf witness_fmt "@.";

444

()

445

end (* xx *)

446


447

let global_inline basename prog (*type_env clock_env*) =

448

(* We select the main node desc *)

449

let main_node, other_nodes, other_tops =

450

List.fold_right

451

(fun top (main_opt, nodes, others) >

452

match top.top_decl_desc with

453

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

454

Some top, nodes, others

455

 Node _ > main_opt, top::nodes, others

456

 _ > main_opt, nodes, top::others)

457

prog (None, [], [])

458

in

459


460

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

461

let main_node = Utils.desome main_node in

462

let main_node' = inline_all_calls main_node other_nodes in

463

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

464

(* Code snippet from unstable branch. May be used when reactivating witnesses.

465

let res = main_node'::other_tops in

466

if !Options.witnesses then (

467

witness

468

basename

469

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

470

prog res type_env clock_env

471

);

472

*)

473

res

474


475

let pp_inline_calls fmt prog =

476

let local_anns = Annotations.get_expr_annotations keyword in

477

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

478

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

479

(fprintf_list ~sep:""

480

(fun fmt top >

481

match top.top_decl_desc with

482

 Node nd when ISet.mem nd.node_id nodes_with_anns >

483

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

484

nd.node_id

485

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

486

(List.fold_left

487

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

488

[]

489

local_anns

490

)

491

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

492

 _ > ()

493

))

494

prog

495


496


497

let local_inline prog (* type_env clock_env *) =

498

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

499

let local_anns = Annotations.get_expr_annotations keyword in

500

let prog =

501

if local_anns != [] then (

502

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

503

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

504

nodes_with_anns;

505

List.fold_right (fun top accu >

506

( match top.top_decl_desc with

507

 Node nd when ISet.mem nd.node_id nodes_with_anns >

508

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

509

let inlined_node = inline_node ~selection_on_annotation:true nd prog in

510

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

511

(* Printers.pp_node nd *)

512

(* Printers.pp_node inlined_node; *)

513

{ top with top_decl_desc = Node inlined_node }

514


515

 _ > top

516

)::accu) prog []

517


518

)

519

else (

520

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

521

prog

522

)

523

in

524

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

525

prog

526


527

(* Local Variables: *)

528

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

529

(* End: *)
