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 Utils

13

open Lustre_types

14

open Corelang

15

open Format

16


17

(** Normalisation iters through the AST of expressions and bind fresh definition

18

when some criteria are met. This creation of fresh definition is performed by

19

the function mk_expr_alias_opt when the alias argument is on.

20


21

Initial expressions, ie expressions attached a variable in an equation

22

definition are not aliased. This nonalias feature is propagated in the

23

expression AST for array access and power construct, tuple, and some special

24

cases of arrows.

25


26

Two global variables may impact the normalization process:

27

 unfold_arrow_active

28

 force_alias_ite: when set, bind a fresh alias for then and else

29

definitions.

30

*)

31


32

(* Two global variables *)

33

let unfold_arrow_active = ref true

34

let force_alias_ite = ref false

35

let force_alias_internal_fun = ref false

36


37


38

let expr_true loc ck =

39

{ expr_tag = Utils.new_tag ();

40

expr_desc = Expr_const (Const_tag tag_true);

41

expr_type = Type_predef.type_bool;

42

expr_clock = ck;

43

expr_delay = Delay.new_var ();

44

expr_annot = None;

45

expr_loc = loc }

46


47

let expr_false loc ck =

48

{ expr_tag = Utils.new_tag ();

49

expr_desc = Expr_const (Const_tag tag_false);

50

expr_type = Type_predef.type_bool;

51

expr_clock = ck;

52

expr_delay = Delay.new_var ();

53

expr_annot = None;

54

expr_loc = loc }

55


56

let expr_once loc ck =

57

{ expr_tag = Utils.new_tag ();

58

expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);

59

expr_type = Type_predef.type_bool;

60

expr_clock = ck;

61

expr_delay = Delay.new_var ();

62

expr_annot = None;

63

expr_loc = loc }

64


65

let is_expr_once =

66

let dummy_expr_once = expr_once Location.dummy_loc (Clocks.new_var true) in

67

fun expr > Corelang.is_eq_expr expr dummy_expr_once

68


69

let unfold_arrow expr =

70

match expr.expr_desc with

71

 Expr_arrow (e1, e2) >

72

let loc = expr.expr_loc in

73

let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in

74

{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }

75

 _ > assert false

76


77


78


79

(* Get the equation in [defs] with [expr] as rhs, if any *)

80

let get_expr_alias defs expr =

81

try Some (List.find (fun eq > Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock && is_eq_expr eq.eq_rhs expr) defs)

82

with

83

 Not_found > None

84


85

(* Replace [expr] with (tuple of) [locals] *)

86

let replace_expr locals expr =

87

match locals with

88

 [] > assert false

89

 [v] > { expr with

90

expr_tag = Utils.new_tag ();

91

expr_desc = Expr_ident v.var_id }

92

 _ > { expr with

93

expr_tag = Utils.new_tag ();

94

expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }

95


96

let unfold_offsets e offsets =

97

let add_offset e d =

98

(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;

99

let res = *)

100

{ e with

101

expr_tag = Utils.new_tag ();

102

expr_loc = d.Dimension.dim_loc;

103

expr_type = Types.array_element_type e.expr_type;

104

expr_desc = Expr_access (e, d) }

105

(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)

106

in

107

List.fold_left add_offset e offsets

108


109

(* Create an alias for [expr], if none exists yet *)

110

let mk_expr_alias node (defs, vars) expr =

111

(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)

112

match get_expr_alias defs expr with

113

 Some eq >

114

let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in

115

(defs, vars), replace_expr aliases expr

116

 None >

117

let new_aliases =

118

List.map2

119

(mk_fresh_var node expr.expr_loc)

120

(Types.type_list_of_type expr.expr_type)

121

(Clocks.clock_list_of_clock expr.expr_clock) in

122

let new_def =

123

mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr)

124

in

125

(* Format.eprintf "Checking def of alias: %a > %a@." (fprintf_list ~sep:", " (fun fmt v > Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)

126

(new_def::defs, new_aliases@vars), replace_expr new_aliases expr

127


128

(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)

129

and [opt] is true *)

130

let mk_expr_alias_opt opt node (defs, vars) expr =

131

(*Format.eprintf "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)

132

match expr.expr_desc with

133

 Expr_ident alias >

134

(defs, vars), expr

135

 _ >

136

match get_expr_alias defs expr with

137

 Some eq >

138

let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in

139

(defs, vars), replace_expr aliases expr

140

 None >

141

if opt

142

then

143

let new_aliases =

144

List.map2

145

(mk_fresh_var node expr.expr_loc)

146

(Types.type_list_of_type expr.expr_type)

147

(Clocks.clock_list_of_clock expr.expr_clock) in

148

let new_def =

149

mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr)

150

in

151

(* Typing and Registering machine type *)

152

let _ = if Machine_types.is_active then Machine_types.type_def node new_aliases expr in

153

(new_def::defs, new_aliases@vars), replace_expr new_aliases expr

154

else

155

(defs, vars), expr

156


157

(* Create a (normalized) expression from [ref_e],

158

replacing description with [norm_d],

159

taking propagated [offsets] into account

160

in order to change expression type *)

161

let mk_norm_expr offsets ref_e norm_d =

162

(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)

163

let drop_array_type ty =

164

Types.map_tuple_type Types.array_element_type ty in

165

{ ref_e with

166

expr_desc = norm_d;

167

expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }

168


169

(* normalize_<foo> : defs * used vars > <foo> > (updated defs * updated vars) * normalized <foo> *)

170

let rec normalize_list alias node offsets norm_element defvars elist =

171

List.fold_right

172

(fun t (defvars, qlist) >

173

let defvars, norm_t = norm_element alias node offsets defvars t in

174

(defvars, norm_t :: qlist)

175

) elist (defvars, [])

176


177

let rec normalize_expr ?(alias=true) ?(alias_basic=false) node offsets defvars expr =

178

(*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)

179

match expr.expr_desc with

180

 Expr_const _

181

 Expr_ident _ > defvars, unfold_offsets expr offsets

182

 Expr_array elist >

183

let defvars, norm_elist = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in

184

let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in

185

mk_expr_alias_opt alias node defvars norm_expr

186

 Expr_power (e1, d) when offsets = [] >

187

let defvars, norm_e1 = normalize_expr node offsets defvars e1 in

188

let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in

189

mk_expr_alias_opt alias node defvars norm_expr

190

 Expr_power (e1, d) >

191

normalize_expr ~alias:alias node (List.tl offsets) defvars e1

192

 Expr_access (e1, d) >

193

normalize_expr ~alias:alias node (d::offsets) defvars e1

194

 Expr_tuple elist >

195

let defvars, norm_elist =

196

normalize_list alias node offsets (fun alias > normalize_expr ~alias:alias ~alias_basic:false) defvars elist in

197

defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)

198

 Expr_appl (id, args, None)

199

when Basic_library.is_homomorphic_fun id

200

&& Types.is_array_type expr.expr_type >

201

let defvars, norm_args =

202

normalize_list

203

alias

204

node

205

offsets

206

(fun _ > normalize_array_expr ~alias:true)

207

defvars

208

(expr_list_of_expr args)

209

in

210

defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))

211

 Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr

212

&& not (!force_alias_internal_fun  alias_basic) >

213

let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in

214

defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))

215

 Expr_appl (id, args, r) >

216

let defvars, r =

217

match r with

218

 None > defvars, None

219

 Some r >

220

let defvars, norm_r = normalize_expr ~alias_basic:true node [] defvars r in

221

defvars, Some norm_r

222

in

223

let defvars, norm_args = normalize_expr node [] defvars args in

224

let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in

225

if offsets <> []

226

then

227

let defvars, norm_expr = normalize_expr node [] defvars norm_expr in

228

normalize_expr ~alias:alias node offsets defvars norm_expr

229

else

230

mk_expr_alias_opt (alias && (!force_alias_internal_fun  alias_basic

231

 not (Basic_library.is_expr_internal_fun expr)))

232

node defvars norm_expr

233

 Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) >

234

(* Here we differ from Colaco paper: arrows are pushed to the top *)

235

normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)

236

 Expr_arrow (e1,e2) >

237

let defvars, norm_e1 = normalize_expr node offsets defvars e1 in

238

let defvars, norm_e2 = normalize_expr node offsets defvars e2 in

239

let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in

240

mk_expr_alias_opt alias node defvars norm_expr

241

 Expr_pre e >

242

let defvars, norm_e = normalize_expr node offsets defvars e in

243

let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in

244

mk_expr_alias_opt alias node defvars norm_expr

245

 Expr_fby (e1, e2) >

246

let defvars, norm_e1 = normalize_expr node offsets defvars e1 in

247

let defvars, norm_e2 = normalize_expr node offsets defvars e2 in

248

let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in

249

mk_expr_alias_opt alias node defvars norm_expr

250

 Expr_when (e, c, l) >

251

let defvars, norm_e = normalize_expr node offsets defvars e in

252

defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))

253

 Expr_ite (c, t, e) >

254

let defvars, norm_c = normalize_guard node defvars c in

255

let defvars, norm_t = normalize_cond_expr node offsets defvars t in

256

let defvars, norm_e = normalize_cond_expr node offsets defvars e in

257

let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in

258

mk_expr_alias_opt alias node defvars norm_expr

259

 Expr_merge (c, hl) >

260

let defvars, norm_hl = normalize_branches node offsets defvars hl in

261

let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in

262

mk_expr_alias_opt alias node defvars norm_expr

263


264

(* Creates a conditional with a merge construct, which is more lazy *)

265

(*

266

let norm_conditional_as_merge alias node norm_expr offsets defvars expr =

267

match expr.expr_desc with

268

 Expr_ite (c, t, e) >

269

let defvars, norm_t = norm_expr (alias node offsets defvars t in

270

 _ > assert false

271

*)

272

and normalize_branches node offsets defvars hl =

273

List.fold_right

274

(fun (t, h) (defvars, norm_q) >

275

let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in

276

defvars, (t, norm_h) :: norm_q

277

)

278

hl (defvars, [])

279


280

and normalize_array_expr ?(alias=true) node offsets defvars expr =

281

(*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)

282

match expr.expr_desc with

283

 Expr_power (e1, d) when offsets = [] >

284

let defvars, norm_e1 = normalize_expr node offsets defvars e1 in

285

defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))

286

 Expr_power (e1, d) >

287

normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1

288

 Expr_access (e1, d) > normalize_array_expr ~alias:alias node (d::offsets) defvars e1

289

 Expr_array elist when offsets = [] >

290

let defvars, norm_elist = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in

291

defvars, mk_norm_expr offsets expr (Expr_array norm_elist)

292

 Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr >

293

let defvars, norm_args = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in

294

defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))

295

 _ > normalize_expr ~alias:alias node offsets defvars expr

296


297

and normalize_cond_expr ?(alias=true) node offsets defvars expr =

298

(*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)

299

match expr.expr_desc with

300

 Expr_access (e1, d) >

301

normalize_cond_expr ~alias:alias node (d::offsets) defvars e1

302

 Expr_ite (c, t, e) >

303

let defvars, norm_c = normalize_guard node defvars c in

304

let defvars, norm_t = normalize_cond_expr node offsets defvars t in

305

let defvars, norm_e = normalize_cond_expr node offsets defvars e in

306

defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))

307

 Expr_merge (c, hl) >

308

let defvars, norm_hl = normalize_branches node offsets defvars hl in

309

defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))

310

 _ when !force_alias_ite >

311

(* Forcing alias creation for then/else expressions *)

312

let defvars, norm_expr =

313

normalize_expr ~alias:alias node offsets defvars expr

314

in

315

mk_expr_alias_opt true node defvars norm_expr

316

 _ > (* default case without the force_alias_ite option *)

317

normalize_expr ~alias:alias node offsets defvars expr

318


319

and normalize_guard node defvars expr =

320

let defvars, norm_expr = normalize_expr ~alias_basic:true node [] defvars expr in

321

mk_expr_alias_opt true node defvars norm_expr

322


323

(* outputs cannot be memories as well. If so, introduce new local variable.

324

*)

325

let decouple_outputs node defvars eq =

326

let rec fold_lhs defvars lhs tys cks =

327

match lhs, tys, cks with

328

 [], [], [] > defvars, []

329

 v::qv, t::qt, c::qc > let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in

330

if List.exists (fun o > o.var_id = v) node.node_outputs

331

then

332

let newvar = mk_fresh_var node eq.eq_loc t c in

333

let neweq = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in

334

(neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q

335

else

336

(defs_q, vars_q), v::lhs_q

337

 _ > assert false in

338

let defvars', lhs' =

339

fold_lhs

340

defvars

341

eq.eq_lhs

342

(Types.type_list_of_type eq.eq_rhs.expr_type)

343

(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in

344

defvars', {eq with eq_lhs = lhs' }

345


346

let rec normalize_eq node defvars eq =

347

(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)

348

match eq.eq_rhs.expr_desc with

349

 Expr_pre _

350

 Expr_fby _ >

351

let (defvars', eq') = decouple_outputs node defvars eq in

352

let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in

353

let norm_eq = { eq' with eq_rhs = norm_rhs } in

354

(norm_eq::defs', vars')

355

 Expr_array _ >

356

let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in

357

let norm_eq = { eq with eq_rhs = norm_rhs } in

358

(norm_eq::defs', vars')

359

 Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type >

360

let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in

361

let norm_eq = { eq with eq_rhs = norm_rhs } in

362

(norm_eq::defs', vars')

363

 Expr_appl _ >

364

let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in

365

let norm_eq = { eq with eq_rhs = norm_rhs } in

366

(norm_eq::defs', vars')

367

 _ >

368

let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in

369

let norm_eq = { eq with eq_rhs = norm_rhs } in

370

norm_eq::defs', vars'

371


372

(** normalize_node node returns a normalized node,

373

ie.

374

 updated locals

375

 new equations

376



377

*)

378

let normalize_node node =

379

reset_cpt_fresh ();

380

let inputs_outputs = node.node_inputs@node.node_outputs in

381

let orig_vars = inputs_outputs@node.node_locals in

382

let not_is_orig_var v =

383

List.for_all ((!=) v) orig_vars in

384

let defs, vars =

385

let eqs, auts = get_node_eqs node in

386

if auts != [] then assert false; (* Automata should be expanded by now. *)

387

List.fold_left (normalize_eq node) ([], orig_vars) eqs in

388

(* Normalize the asserts *)

389

let vars, assert_defs, asserts =

390

List.fold_left (

391

fun (vars, def_accu, assert_accu) assert_ >

392

let assert_expr = assert_.assert_expr in

393

let (defs, vars'), expr =

394

normalize_expr

395

~alias:true (* forcing introduction of new equations for fcn calls *)

396

node

397

[] (* empty offset for arrays *)

398

([], vars) (* defvar only contains vars *)

399

assert_expr

400

in

401

(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)

402

vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu

403

) (vars, [], []) node.node_asserts in

404

let new_locals = List.filter not_is_orig_var vars in (* we filter out inout

405

vars and initial locals ones *)

406


407

let all_locals = node.node_locals @ new_locals in (* we add again, at the

408

beginning of the list the

409

local declared ones *)

410

(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)

411


412


413

(* Updating annotations: traceability and machine types for fresh variables *)

414


415

(* Compute traceability info:

416

 gather newly bound variables

417

 compute the associated expression without aliases

418

*)

419

let new_annots =

420

if !Options.traces then

421

begin

422

let diff_vars = List.filter (fun v > not (List.mem v node.node_locals) ) all_locals in

423

let norm_traceability = {

424

annots = List.map (fun v >

425

let eq =

426

try

427

List.find (fun eq > List.exists (fun v' > v' = v.var_id ) eq.eq_lhs) (defs@assert_defs)

428

with Not_found >

429

(

430

Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id;

431

assert false

432

)

433

in

434

let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in

435

let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in

436

Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];

437

(["traceability"], pair)

438

) diff_vars;

439

annot_loc = Location.dummy_loc

440

}

441

in

442

norm_traceability::node.node_annot

443

end

444

else

445

node.node_annot

446

in

447


448

let new_annots =

449

List.fold_left (fun annots v >

450

if Machine_types.is_active && Machine_types.is_exportable v then

451

let typ = Machine_types.get_specified_type v in

452

let typ_name = Machine_types.type_name typ in

453


454

let loc = v.var_loc in

455

let typ_as_string =

456

mkexpr

457

loc

458

(Expr_const

459

(Const_string typ_name))

460

in

461

let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in

462

Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;

463

{annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots

464

else

465

annots

466

) new_annots new_locals

467

in

468

let node =

469

{ node with

470

node_locals = all_locals;

471

node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs);

472

node_asserts = asserts;

473

node_annot = new_annots;

474

}

475

in ((*Printers.pp_node Format.err_formatter node;*)

476

node

477

)

478


479


480

let normalize_decl decl =

481

match decl.top_decl_desc with

482

 Node nd >

483

let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in

484

Hashtbl.replace Corelang.node_table nd.node_id decl';

485

decl'

486

 Open _  ImportedNode _  Const _  TypeDef _ > decl

487


488

let normalize_prog ?(backend="C") decls =

489

let old_unfold_arrow_active = !unfold_arrow_active in

490

let old_force_alias_ite = !force_alias_ite in

491

let old_force_alias_internal_fun = !force_alias_internal_fun in

492


493

(* Backend specific configurations for normalization *)

494

let _ =

495

match backend with

496

 "lustre" >

497

(* Special treatment of arrows in lustre backend. We want to keep them *)

498

unfold_arrow_active := false;

499

 "emf" > (

500

(* Forcing ite normalization *)

501

force_alias_ite := true;

502

force_alias_internal_fun := true;

503

)

504

 _ > () (* No fancy options for other backends *)

505

in

506


507

(* Main algorithm: iterates over nodes *)

508

let res = List.map normalize_decl decls in

509


510

(* Restoring previous settings *)

511

unfold_arrow_active := old_unfold_arrow_active;

512

force_alias_ite := old_force_alias_ite;

513

force_alias_internal_fun := old_force_alias_internal_fun;

514

res

515


516

(* Local Variables: *)

517

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

518

(* End: *)
