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 LustreSpec

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

let cpt_fresh = ref 0

78


79

(* Generate a new local [node] variable *)

80

let mk_fresh_var node loc ty ck =

81

let vars = get_node_vars node in

82

let rec aux () =

83

incr cpt_fresh;

84

let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in

85

if List.exists (fun v > v.var_id = s) vars then aux () else

86

{

87

var_id = s;

88

var_orig = false;

89

var_dec_type = dummy_type_dec;

90

var_dec_clock = dummy_clock_dec;

91

var_dec_const = false;

92

var_dec_value = None;

93

var_type = ty;

94

var_clock = ck;

95

var_loc = loc

96

}

97

in aux ()

98


99

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

100

let get_expr_alias defs expr =

101

try Some (List.find (fun eq > is_eq_expr eq.eq_rhs expr) defs)

102

with

103

 Not_found > None

104


105

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

106

let replace_expr locals expr =

107

match locals with

108

 [] > assert false

109

 [v] > { expr with

110

expr_tag = Utils.new_tag ();

111

expr_desc = Expr_ident v.var_id }

112

 _ > { expr with

113

expr_tag = Utils.new_tag ();

114

expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }

115


116

let unfold_offsets e offsets =

117

let add_offset e d =

118

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

119

let res = *)

120

{ e with

121

expr_tag = Utils.new_tag ();

122

expr_loc = d.Dimension.dim_loc;

123

expr_type = Types.array_element_type e.expr_type;

124

expr_desc = Expr_access (e, d) }

125

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

126

in

127

List.fold_left add_offset e offsets

128


129

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

130

let mk_expr_alias node (defs, vars) expr =

131

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

132

match get_expr_alias defs expr with

133

 Some eq >

134

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

135

(defs, vars), replace_expr aliases expr

136

 None >

137

let new_aliases =

138

List.map2

139

(mk_fresh_var node expr.expr_loc)

140

(Types.type_list_of_type expr.expr_type)

141

(Clocks.clock_list_of_clock expr.expr_clock) in

142

let new_def =

143

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

144

in

145

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

146

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

147


148

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

149

and [opt] is true *)

150

let mk_expr_alias_opt opt node (defs, vars) expr =

151

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

152

match expr.expr_desc with

153

 Expr_ident alias >

154

(defs, vars), expr

155

 _ >

156

match get_expr_alias defs expr with

157

 Some eq >

158

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

159

(defs, vars), replace_expr aliases expr

160

 None >

161

if opt

162

then

163

let new_aliases =

164

List.map2

165

(mk_fresh_var node expr.expr_loc)

166

(Types.type_list_of_type expr.expr_type)

167

(Clocks.clock_list_of_clock expr.expr_clock) in

168

let new_def =

169

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

170

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

171

else

172

(defs, vars), expr

173


174

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

175

replacing description with [norm_d],

176

taking propagated [offsets] into account

177

in order to change expression type *)

178

let mk_norm_expr offsets ref_e norm_d =

179

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

180

let drop_array_type ty =

181

Types.map_tuple_type Types.array_element_type ty in

182

{ ref_e with

183

expr_desc = norm_d;

184

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

185


186

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

187

let rec normalize_list alias node offsets norm_element defvars elist =

188

List.fold_right

189

(fun t (defvars, qlist) >

190

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

191

(defvars, norm_t :: qlist)

192

) elist (defvars, [])

193


194

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

195

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

196

match expr.expr_desc with

197

 Expr_const _

198

 Expr_ident _ > defvars, unfold_offsets expr offsets

199

 Expr_array elist >

200

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

201

let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in

202

mk_expr_alias_opt alias node defvars norm_expr

203

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

204

let defvars, norm_e1 = normalize_expr node offsets defvars e1 in

205

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

206

mk_expr_alias_opt alias node defvars norm_expr

207

 Expr_power (e1, d) >

208

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

209

 Expr_access (e1, d) >

210

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

211

 Expr_tuple elist >

212

let defvars, norm_elist =

213

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

214

defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)

215

 Expr_appl (id, args, None)

216

when Basic_library.is_homomorphic_fun id

217

&& Types.is_array_type expr.expr_type >

218

let defvars, norm_args =

219

normalize_list

220

alias

221

node

222

offsets

223

(fun _ > normalize_array_expr ~alias:true)

224

defvars

225

(expr_list_of_expr args)

226

in

227

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

228

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

229

&& not (!force_alias_internal_fun  alias_basic) >

230

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

231

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

232

 Expr_appl (id, args, r) >

233

let defvars, r =

234

match r with

235

 None > defvars, None

236

 Some r >

237

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

238

defvars, Some norm_r

239

in

240

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

241

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

242

if offsets <> []

243

then

244

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

245

normalize_expr ~alias:alias node offsets defvars norm_expr

246

else

247

mk_expr_alias_opt (alias && (!force_alias_internal_fun  alias_basic

248

 not (Basic_library.is_expr_internal_fun expr)))

249

node defvars norm_expr

250

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

251

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

252

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

253

 Expr_arrow (e1,e2) >

254

let defvars, norm_e1 = normalize_expr node offsets defvars e1 in

255

let defvars, norm_e2 = normalize_expr node offsets defvars e2 in

256

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

257

mk_expr_alias_opt alias node defvars norm_expr

258

 Expr_pre e >

259

let defvars, norm_e = normalize_expr node offsets defvars e in

260

let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in

261

mk_expr_alias_opt alias node defvars norm_expr

262

 Expr_fby (e1, e2) >

263

let defvars, norm_e1 = normalize_expr node offsets defvars e1 in

264

let defvars, norm_e2 = normalize_expr node offsets defvars e2 in

265

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

266

mk_expr_alias_opt alias node defvars norm_expr

267

 Expr_when (e, c, l) >

268

let defvars, norm_e = normalize_expr node offsets defvars e in

269

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

270

 Expr_ite (c, t, e) >

271

let defvars, norm_c = normalize_guard node defvars c in

272

let defvars, norm_t = normalize_cond_expr node offsets defvars t in

273

let defvars, norm_e = normalize_cond_expr node offsets defvars e in

274

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

275

mk_expr_alias_opt alias node defvars norm_expr

276

 Expr_merge (c, hl) >

277

let defvars, norm_hl = normalize_branches node offsets defvars hl in

278

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

279

mk_expr_alias_opt alias node defvars norm_expr

280


281

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

282

(*

283

let norm_conditional_as_merge alias node norm_expr offsets defvars expr =

284

match expr.expr_desc with

285

 Expr_ite (c, t, e) >

286

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

287

 _ > assert false

288

*)

289

and normalize_branches node offsets defvars hl =

290

List.fold_right

291

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

292

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

293

defvars, (t, norm_h) :: norm_q

294

)

295

hl (defvars, [])

296


297

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

298

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

299

match expr.expr_desc with

300

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

301

let defvars, norm_e1 = normalize_expr node offsets defvars e1 in

302

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

303

 Expr_power (e1, d) >

304

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

305

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

306

 Expr_array elist when offsets = [] >

307

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

308

defvars, mk_norm_expr offsets expr (Expr_array norm_elist)

309

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

310

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

311

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

312

 _ > normalize_expr ~alias:alias node offsets defvars expr

313


314

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

315

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

316

match expr.expr_desc with

317

 Expr_access (e1, d) >

318

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

319

 Expr_ite (c, t, e) >

320

let defvars, norm_c = normalize_guard node defvars c in

321

let defvars, norm_t = normalize_cond_expr node offsets defvars t in

322

let defvars, norm_e = normalize_cond_expr node offsets defvars e in

323

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

324

 Expr_merge (c, hl) >

325

let defvars, norm_hl = normalize_branches node offsets defvars hl in

326

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

327

 _ when !force_alias_ite >

328

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

329

let defvars, norm_expr =

330

normalize_expr ~alias:alias node offsets defvars expr

331

in

332

mk_expr_alias_opt true node defvars norm_expr

333

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

334

normalize_expr ~alias:alias node offsets defvars expr

335


336

and normalize_guard node defvars expr =

337

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

338

mk_expr_alias_opt true node defvars norm_expr

339


340

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

341

*)

342

let decouple_outputs node defvars eq =

343

let rec fold_lhs defvars lhs tys cks =

344

match lhs, tys, cks with

345

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

346

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

347

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

348

then

349

let newvar = mk_fresh_var node eq.eq_loc t c in

350

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

351

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

352

else

353

(defs_q, vars_q), v::lhs_q

354

 _ > assert false in

355

let defvars', lhs' =

356

fold_lhs

357

defvars

358

eq.eq_lhs

359

(Types.type_list_of_type eq.eq_rhs.expr_type)

360

(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in

361

defvars', {eq with eq_lhs = lhs' }

362


363

let rec normalize_eq node defvars eq =

364

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

365

match eq.eq_rhs.expr_desc with

366

 Expr_pre _

367

 Expr_fby _ >

368

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

369

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

370

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

371

(norm_eq::defs', vars')

372

 Expr_array _ >

373

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

374

let norm_eq = { eq with eq_rhs = norm_rhs } in

375

(norm_eq::defs', vars')

376

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

377

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

378

let norm_eq = { eq with eq_rhs = norm_rhs } in

379

(norm_eq::defs', vars')

380

 Expr_appl _ >

381

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

382

let norm_eq = { eq with eq_rhs = norm_rhs } in

383

(norm_eq::defs', vars')

384

 _ >

385

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

386

let norm_eq = { eq with eq_rhs = norm_rhs } in

387

norm_eq::defs', vars'

388


389

(** normalize_node node returns a normalized node,

390

ie.

391

 updated locals

392

 new equations

393



394

*)

395

let normalize_node node =

396

cpt_fresh := 0;

397

let inputs_outputs = node.node_inputs@node.node_outputs in

398

let is_local v =

399

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

400

let orig_vars = inputs_outputs@node.node_locals in

401

let defs, vars =

402

let eqs, auts = get_node_eqs node in

403

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

404

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

405

(* Normalize the asserts *)

406

let vars, assert_defs, asserts =

407

List.fold_left (

408

fun (vars, def_accu, assert_accu) assert_ >

409

let assert_expr = assert_.assert_expr in

410

let (defs, vars'), expr =

411

normalize_expr

412

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

413

node

414

[] (* empty offset for arrays *)

415

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

416

assert_expr

417

in

418

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

419

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

420

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

421

let new_locals = List.filter is_local vars in

422

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

423


424

let new_annots =

425

if !Options.traces then

426

begin

427

(* Compute traceability info:

428

 gather newly bound variables

429

 compute the associated expression without aliases

430

*)

431

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

432

let norm_traceability = {

433

annots = List.map (fun v >

434

let eq =

435

try

436

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

437

with Not_found >

438

(

439

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

440

assert false

441

)

442

in

443

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

444

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

445

(["traceability"], pair)

446

) diff_vars;

447

annot_loc = Location.dummy_loc

448

}

449

in

450

norm_traceability::node.node_annot

451

end

452

else

453

node.node_annot

454

in

455


456

let node =

457

{ node with

458

node_locals = new_locals;

459

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

460

node_asserts = asserts;

461

node_annot = new_annots;

462

}

463

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

464

node

465

)

466


467


468

let normalize_decl decl =

469

match decl.top_decl_desc with

470

 Node nd >

471

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

472

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

473

decl'

474

 Open _  ImportedNode _  Const _  TypeDef _ > decl

475


476

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

477

let old_unfold_arrow_active = !unfold_arrow_active in

478

let old_force_alias_ite = !force_alias_ite in

479

let old_force_alias_internal_fun = !force_alias_internal_fun in

480


481

(* Backend specific configurations for normalization *)

482

let _ =

483

match backend with

484

 "lustre" >

485

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

486

unfold_arrow_active := false;

487

 "emf" > (

488

(* Forcing ite normalization *)

489

force_alias_ite := true;

490

force_alias_internal_fun := true;

491

)

492

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

493

in

494


495

(* Main algorithm: iterates over nodes *)

496

let res = List.map normalize_decl decls in

497


498

(* Restoring previous settings *)

499

unfold_arrow_active := old_unfold_arrow_active;

500

force_alias_ite := old_force_alias_ite;

501

force_alias_internal_fun := old_force_alias_internal_fun;

502

res

503


504

(* Local Variables: *)

505

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

506

(* End: *)
