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

(* To update thank to some command line options *)

18

let debug = ref false

19


20

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

21

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

22

the function mk_expr_alias_opt when the alias argument is on.

23


24

Initial expressions, ie expressions attached a variable in an equation

25

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

26

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

27

cases of arrows.

28


29

Two global variables may impact the normalization process:

30

 unfold_arrow_active

31

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

32

definitions.

33

*)

34


35

type param_t = {

36

unfold_arrow_active : bool;

37

force_alias_ite : bool;

38

force_alias_internal_fun : bool;

39

}

40


41

let params =

42

ref

43

{

44

unfold_arrow_active = false;

45

force_alias_ite = false;

46

force_alias_internal_fun = false;

47

}

48


49

type norm_ctx_t = {

50

parentid : ident;

51

vars : var_decl list;

52

is_output : ident > bool;

53

}

54


55

let expr_true loc ck =

56

{

57

expr_tag = Utils.new_tag ();

58

expr_desc = Expr_const (Const_tag tag_true);

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


66

let expr_false loc ck =

67

{

68

expr_tag = Utils.new_tag ();

69

expr_desc = Expr_const (Const_tag tag_false);

70

expr_type = Type_predef.type_bool;

71

expr_clock = ck;

72

expr_delay = Delay.new_var ();

73

expr_annot = None;

74

expr_loc = loc;

75

}

76


77

let expr_once loc ck =

78

{

79

expr_tag = Utils.new_tag ();

80

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

81

expr_type = Type_predef.type_bool;

82

expr_clock = ck;

83

expr_delay = Delay.new_var ();

84

expr_annot = None;

85

expr_loc = loc;

86

}

87


88

let is_expr_once =

89

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

90

fun expr > Corelang.is_eq_expr expr dummy_expr_once

91


92

let unfold_arrow expr =

93

match expr.expr_desc with

94

 Expr_arrow (e1, e2) >

95

let loc = expr.expr_loc in

96

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

97

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

98

 _ > assert false

99


100

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

101

let get_expr_alias defs expr =

102

try

103

Some

104

(List.find

105

(fun eq >

106

Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock

107

&& is_eq_expr eq.eq_rhs expr)

108

defs)

109

with Not_found > None

110


111

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

112

let replace_expr locals expr =

113

match locals with

114

 [] > assert false

115

 [ v ] >

116

{ expr with expr_tag = Utils.new_tag (); expr_desc = Expr_ident v.var_id }

117

 _ >

118

{

119

expr with

120

expr_tag = Utils.new_tag ();

121

expr_desc = Expr_tuple (List.map expr_of_vdecl locals);

122

}

123


124

(* IS IT USED ? TODO

125

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

126

let mk_expr_alias (parentid, vars) (defs, vars) expr =

127

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

128

match get_expr_alias defs expr with

129

 Some eq >

130

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

131

(defs, vars), replace_expr aliases expr

132

 None >

133

let new_aliases =

134

List.map2

135

(mk_fresh_var (parentid, vars) expr.expr_loc)

136

(Types.type_list_of_type expr.expr_type)

137

(Clocks.clock_list_of_clock expr.expr_clock) in

138

let new_def =

139

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

140

in

141

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

142

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

143

*)

144


145

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

146

and [opt] is true

147


148


149

*)

150

let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =

151

if !debug then

152

Log.report ~plugin:"normalization" ~level:2 (fun fmt >

153

Format.fprintf fmt "mk_expr_alias_opt %B %a %a %a@." opt

154

Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck

155

expr.expr_clock);

156

match expr.expr_desc with

157

 Expr_ident _ > (defs, vars), expr

158

 _ > (

159

match get_expr_alias defs expr with

160

 Some eq >

161

(* Format.eprintf "Found a preexisting definition@."; *)

162

let aliases =

163

List.map

164

(fun id > List.find (fun v > v.var_id = id) vars)

165

eq.eq_lhs

166

in

167

(defs, vars), replace_expr aliases expr

168

 None >

169

(*

170

Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt;

171

* Format.eprintf "existing defs are: @[[%a@]]@."

172

* (fprintf_list ~sep:"@ "(fun fmt eq >

173

* Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a"

174

* Clocks.print_ck eq.eq_rhs.expr_clock

175

* (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock)

176

* (is_eq_expr eq.eq_rhs expr)

177

* Printers.pp_node_eq eq))

178

* defs; *)

179

if opt then

180

let new_aliases =

181

List.map2

182

(mk_fresh_var

183

(norm_ctx.parentid, norm_ctx.vars @ vars)

184

expr.expr_loc)

185

(Types.type_list_of_type expr.expr_type)

186

(Clocks.clock_list_of_clock expr.expr_clock)

187

in

188

let new_def =

189

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

190

in

191

(* Typing and Registering machine type *)

192

let _ =

193

if Machine_types.is_active then

194

Machine_types.type_def

195

(norm_ctx.parentid, norm_ctx.vars)

196

new_aliases expr

197

in

198

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

199

else (defs, vars), expr)

200


201

(* Similar fonctions for dimensions *)

202

let mk_dim_alias opt norm_ctx (defs, vars) dim =

203

match dim.Dimension.dim_desc with

204

 Dimension.Dbool _  Dint _  Dident _ >

205

(defs, vars), dim (* Keep the same *)

206

 _ when opt >

207

(* Cast to expression, normalizing *)

208

let e = expr_of_dimension dim in

209

let defvars, e = mk_expr_alias_opt true norm_ctx (defs, vars) e in

210

defvars, dimension_of_expr e

211

 _ > (defs, vars), dim

212

(* Keep the same *)

213


214

let unfold_offsets norm_ctx defvars e offsets =

215

let add_offset (defvars, e) d =

216

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

217

let defvars, d =

218

mk_dim_alias !params.force_alias_internal_fun norm_ctx defvars d

219

in

220

let new_e =

221

{

222

e with

223

expr_tag = Utils.new_tag ();

224

expr_loc = d.Dimension.dim_loc;

225

expr_type = Types.array_element_type e.expr_type;

226

expr_desc = Expr_access (e, d);

227

}

228

in

229

defvars, new_e

230

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

231

in

232

List.fold_left add_offset (defvars, e) offsets

233


234

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

235

replacing description with [norm_d],

236

taking propagated [offsets] into account

237

in order to change expression type *)

238

let mk_norm_expr offsets ref_e norm_d =

239

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

240

let drop_array_type ty = Types.map_tuple_type Types.array_element_type ty in

241

{

242

ref_e with

243

expr_desc = norm_d;

244

expr_type =

245

Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type;

246

}

247


248

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

249

let normalize_list alias norm_ctx offsets norm_element defvars elist =

250

List.fold_right

251

(fun t (defvars, qlist) >

252

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

253

defvars, norm_t :: qlist)

254

elist (defvars, [])

255


256

let rec normalize_expr ?(alias = true) ?(alias_basic = false) norm_ctx offsets

257

defvars expr =

258

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

259

match expr.expr_desc with

260

 Expr_const _  Expr_ident _ > unfold_offsets norm_ctx defvars expr offsets

261

 Expr_array elist >

262

let defvars, norm_elist =

263

normalize_list alias norm_ctx offsets

264

(fun _ > normalize_array_expr ~alias:true)

265

defvars elist

266

in

267

let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in

268

mk_expr_alias_opt alias norm_ctx defvars norm_expr

269

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

270

let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

271

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

272

mk_expr_alias_opt alias norm_ctx defvars norm_expr

273

 Expr_power (e1, _) >

274

normalize_expr ~alias norm_ctx (List.tl offsets) defvars e1

275

 Expr_access (e1, d) >

276

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

277

 Expr_tuple elist >

278

let defvars, norm_elist =

279

normalize_list alias norm_ctx offsets

280

(fun alias > normalize_expr ~alias ~alias_basic:false)

281

defvars elist

282

in

283

defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)

284

 Expr_appl (id, args, None)

285

when Basic_library.is_homomorphic_fun id

286

&& Types.is_array_type expr.expr_type >

287

let defvars, norm_args =

288

normalize_list alias norm_ctx offsets

289

(fun _ > normalize_array_expr ~alias:true)

290

defvars (expr_list_of_expr args)

291

in

292

( defvars,

293

mk_norm_expr offsets expr

294

(Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) )

295

 Expr_appl (id, args, None)

296

when Basic_library.is_expr_internal_fun expr

297

&& not (!params.force_alias_internal_fun  alias_basic) >

298

let defvars, norm_args =

299

normalize_expr ~alias:true norm_ctx offsets defvars args

300

in

301

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

302

 Expr_appl (id, args, r) >

303

let defvars, r =

304

match r with

305

 None > defvars, None

306

 Some r >

307

let defvars, norm_r =

308

normalize_expr ~alias_basic:true norm_ctx [] defvars r

309

in

310

defvars, Some norm_r

311

in

312

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

313

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

314

if offsets <> [] then

315

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

316

normalize_expr ~alias norm_ctx offsets defvars norm_expr

317

else

318

mk_expr_alias_opt

319

(alias

320

&& (!params.force_alias_internal_fun  alias_basic

321

 not (Basic_library.is_expr_internal_fun expr)))

322

norm_ctx defvars norm_expr

323

 Expr_arrow _ when !params.unfold_arrow_active && not (is_expr_once expr) >

324

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

325

normalize_expr ~alias norm_ctx offsets defvars (unfold_arrow expr)

326

 Expr_arrow (e1, e2) >

327

let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

328

let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in

329

let norm_expr =

330

mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2))

331

in

332

mk_expr_alias_opt alias norm_ctx defvars norm_expr

333

 Expr_pre e >

334

let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in

335

let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in

336

mk_expr_alias_opt alias norm_ctx defvars norm_expr

337

 Expr_fby (e1, e2) >

338

let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

339

let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in

340

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

341

mk_expr_alias_opt alias norm_ctx defvars norm_expr

342

 Expr_when (e, c, l) >

343

let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in

344

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

345

 Expr_ite (c, t, e) >

346

let defvars, norm_c = normalize_guard norm_ctx defvars c in

347

let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in

348

let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in

349

let norm_expr =

350

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

351

in

352

mk_expr_alias_opt alias norm_ctx defvars norm_expr

353

 Expr_merge (c, hl) >

354

let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in

355

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

356

mk_expr_alias_opt alias norm_ctx defvars norm_expr

357


358

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

359

(*

360

let norm_conditional_as_merge alias node norm_expr offsets defvars expr =

361

match expr.expr_desc with

362

 Expr_ite (c, t, e) >

363

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

364

 _ > assert false

365

*)

366

and normalize_branches norm_ctx offsets defvars hl =

367

List.fold_right

368

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

369

let defvars, norm_h = normalize_cond_expr norm_ctx offsets defvars h in

370

defvars, (t, norm_h) :: norm_q)

371

hl (defvars, [])

372


373

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

374

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

375

match expr.expr_desc with

376

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

377

let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

378

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

379

 Expr_power (e1, _) >

380

normalize_array_expr ~alias norm_ctx (List.tl offsets) defvars e1

381

 Expr_access (e1, d) >

382

normalize_array_expr ~alias norm_ctx (d :: offsets) defvars e1

383

 Expr_array elist when offsets = [] >

384

let defvars, norm_elist =

385

normalize_list alias norm_ctx offsets

386

(fun _ > normalize_array_expr ~alias:true)

387

defvars elist

388

in

389

defvars, mk_norm_expr offsets expr (Expr_array norm_elist)

390

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

391

let defvars, norm_args =

392

normalize_list alias norm_ctx offsets

393

(fun _ > normalize_array_expr ~alias:true)

394

defvars (expr_list_of_expr args)

395

in

396

( defvars,

397

mk_norm_expr offsets expr

398

(Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) )

399

 _ > normalize_expr ~alias norm_ctx offsets defvars expr

400


401

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

402

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

403

match expr.expr_desc with

404

 Expr_access (e1, d) >

405

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

406

 Expr_ite (c, t, e) >

407

let defvars, norm_c = normalize_guard norm_ctx defvars c in

408

let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in

409

let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in

410

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

411

 Expr_merge (c, hl) >

412

let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in

413

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

414

 _ when !params.force_alias_ite >

415

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

416

let defvars, norm_expr =

417

normalize_expr ~alias norm_ctx offsets defvars expr

418

in

419

mk_expr_alias_opt true norm_ctx defvars norm_expr

420

 _ >

421

(* default case without the force_alias_ite option *)

422

normalize_expr ~alias norm_ctx offsets defvars expr

423


424

and normalize_guard norm_ctx defvars expr =

425

let defvars, norm_expr =

426

normalize_expr ~alias_basic:true norm_ctx [] defvars expr

427

in

428

mk_expr_alias_opt true norm_ctx defvars norm_expr

429


430

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

431

*)

432

let decouple_outputs norm_ctx defvars eq =

433

let rec fold_lhs defvars lhs tys cks =

434

match lhs, tys, cks with

435

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

436

 v :: qv, t :: qt, c :: qc >

437

let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in

438

if norm_ctx.is_output v then

439

let newvar =

440

mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c

441

in

442

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

443

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

444

else (defs_q, vars_q), v :: lhs_q

445

 _ > assert false

446

in

447

let defvars', lhs' =

448

fold_lhs defvars eq.eq_lhs

449

(Types.type_list_of_type eq.eq_rhs.expr_type)

450

(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock)

451

in

452

defvars', { eq with eq_lhs = lhs' }

453


454

let normalize_eq norm_ctx defvars eq =

455

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

456

match eq.eq_rhs.expr_desc with

457

 Expr_pre _  Expr_fby _ >

458

let defvars', eq' = decouple_outputs norm_ctx defvars eq in

459

let (defs', vars'), norm_rhs =

460

normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs

461

in

462

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

463

norm_eq :: defs', vars'

464

 Expr_array _ >

465

let (defs', vars'), norm_rhs =

466

normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs

467

in

468

let norm_eq = { eq with eq_rhs = norm_rhs } in

469

norm_eq :: defs', vars'

470

 Expr_appl (id, _, None)

471

when Basic_library.is_homomorphic_fun id

472

&& Types.is_array_type eq.eq_rhs.expr_type >

473

let (defs', vars'), norm_rhs =

474

normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs

475

in

476

let norm_eq = { eq with eq_rhs = norm_rhs } in

477

norm_eq :: defs', vars'

478

 Expr_appl _ >

479

let (defs', vars'), norm_rhs =

480

normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs

481

in

482

let norm_eq = { eq with eq_rhs = norm_rhs } in

483

norm_eq :: defs', vars'

484

 _ >

485

let (defs', vars'), norm_rhs =

486

normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs

487

in

488

let norm_eq = { eq with eq_rhs = norm_rhs } in

489

norm_eq :: defs', vars'

490


491

let normalize_eq_split norm_ctx defvars eq =

492

try

493

let defs, vars = normalize_eq norm_ctx defvars eq in

494

List.fold_right

495

(fun eq (def, vars) >

496

let eq_defs = Splitting.tuple_split_eq eq in

497

if eq_defs = [ eq ] then eq :: def, vars

498

else List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs)

499

defs ([], vars)

500

with ex >

501

Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;

502

raise ex

503


504

(* Projecting an eexpr to an eexpr associated to a single

505

variable. Returns the updated ee, the bounded variable and the

506

associated statement *)

507

let normalize_pred_eexpr norm_ctx (def, vars) ee =

508

assert (ee.eexpr_quantifiers = []);

509

(* We do not normalize quantifiers yet. This is for very far future. *)

510

(* don't do anything is eexpr is just a variable *)

511

let skip =

512

match ee.eexpr_qfexpr.expr_desc with

513

 Expr_ident _  Expr_const _ > true

514

 _ > false

515

in

516

if skip then ee, (def, vars)

517

else

518

(* New output variable *)

519

let output_id = "spec" ^ string_of_int ee.eexpr_tag in

520

let output_var =

521

mkvar_decl ee.eexpr_loc

522

( output_id,

523

mktyp ee.eexpr_loc Tydec_bool,

524

(* It is a predicate, hence a bool *)

525

mkclock ee.eexpr_loc Ckdec_any,

526

false (* not a constant *),

527

None,

528

None )

529

in

530

let output_expr = expr_of_vdecl output_var in

531

(* Rebuilding an eexpr with a silly expression, just a variable *)

532

let ee' = { ee with eexpr_qfexpr = output_expr } in

533


534

(* Now processing a fresh equation output_id = eexpr_qfexpr. We

535

inline possible calls within, normalize it and type/clock the

536

result. *)

537

let eq = mkeq ee.eexpr_loc ([ output_id ], ee.eexpr_qfexpr) in

538


539

(* (\* Inlining any calls *\)

540

* let nodes = get_nodes decls in

541

* let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in

542

* let vars, eqs =

543

* if calls = [] && not (eq_has_arrows eq) then

544

* vars, [eq]

545

* else

546

* assert false (\* TODO *\)

547

* in *)

548


549

(* Normalizing expr and eqs *)

550

let defs, vars =

551

List.fold_left (normalize_eq_split norm_ctx) (def, vars) [ eq ]

552

in

553

let vars = output_var :: vars in

554


555

(* let todefine =

556

List.fold_left

557

(fun m x> if List.exists (fun y> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)

558

(ISet.add output_id ISet.empty) vars in

559

*)

560


561

(* Typing / Clocking *)

562

try

563

ignore (Typing.type_var_decl_list vars !Global.type_env vars);

564


565

(*

566

let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *)

567

(* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)

568

let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in

569

(*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)

570

let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in

571

(* check that table is empty *)

572

if (not (ISet.is_empty undefined_vars)) then

573

raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));

574


575

(*Format.eprintf "normalized eqs %a@.@?"

576

(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *)

577

*)

578

ee', (defs, vars)

579

with Types.Error (loc, err) as exc >

580

eprintf "Typing error for eexpr %a: %a%a%a@." Printers.pp_eexpr ee

581

Types.pp_error err

582

(Utils.fprintf_list ~sep:", " Printers.pp_node_eq)

583

defs Location.pp_loc loc;

584


585

raise exc

586


587

(*

588


589

let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in

590

(* Calls are first inlined *)

591


592

(*Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd > pp_print_string fmt nd.node_id)) calls; *)

593

let (new_locals, eqs) =

594

if calls = [] && not (eq_has_arrows eq) then

595

(locals, [eq])

596

else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)

597

(* let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in

598

(*Format.eprintf "eqs %a@.@?"

599

(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs; *)

600

(new_locals, eqs)

601

*)

602

(locals, [eq])

603


604

) in

605

(* Normalizing expr and eqs *)

606

let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in

607

let todefine = List.fold_left

608

(fun m x> if List.exists (fun y> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)

609

(ISet.add output_id ISet.empty) vars in

610


611

try

612

let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in

613

let env = Typing.type_var_decl [] env output_var in (* typing the variable *)

614

(* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)

615

let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in

616

(*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)

617

let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in

618

(* check that table is empty *)

619

if (not (ISet.is_empty undefined_vars)) then

620

raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));

621


622

(*Format.eprintf "normalized eqs %a@.@?"

623

(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *)

624

ee.eexpr_normalized < Some (output_var, defs, vars)

625


626

with (Types.Error (loc,err)) as exc >

627

eprintf "Typing error for eexpr %a: %a%a%a@."

628

Printers.pp_eexpr ee

629

Types.pp_error err

630

(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs

631

Location.pp_loc loc

632


633


634

;

635

raise exc

636

*)

637


638

(* We use node local vars to make sure we are creating fresh variables *)

639

let normalize_spec parentid (in_vars, out_vars, l_vars) s =

640

(* Original set of variables actually visible from here: in/out and

641

spec locals (no node locals) *)

642

let orig_vars = in_vars @ out_vars @ s.locals in

643

(* Format.eprintf "NormSpec: init locals: %a@." Printers.pp_vars s.locals; *)

644

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

645

let norm_ctx =

646

{

647

parentid;

648

vars = in_vars @ out_vars @ l_vars;

649

is_output =

650

(fun _ > false) (* no need to introduce fresh variables for outputs *);

651

}

652

in

653

(* Normalizing existing stmts *)

654

let eqs, auts =

655

List.fold_right

656

(fun s (el, al) >

657

match s with Eq e > e :: el, al  Aut a > el, a :: al)

658

s.stmts ([], [])

659

in

660

if auts != [] then assert false;

661

(* Automata should be expanded by now. *)

662

let defsvars = List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in

663

(* Iterate through predicates and normalize them on the go, creating

664

fresh variables for any guarantees/assumes/require/ensure *)

665

let process_predicates l defvars =

666

(* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd defvars); *)

667

let res =

668

List.fold_right

669

(fun ee (accu, defvars) >

670

let ee', defvars = normalize_pred_eexpr norm_ctx defvars ee in

671

ee' :: accu, defvars)

672

l ([], defvars)

673

in

674

(* Format.eprintf "ProcStmt: %a@." Printers.pp_node_eqs (fst (snd res));

675

* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd (snd res)); *)

676

res

677

in

678


679

let assume', defsvars = process_predicates s.assume defsvars in

680

let guarantees', defsvars = process_predicates s.guarantees defsvars in

681

let modes', (defs, vars) =

682

List.fold_right

683

(fun m (accu_m, defsvars) >

684

let require', defsvars = process_predicates m.require defsvars in

685

let ensure', defsvars = process_predicates m.ensure defsvars in

686

{ m with require = require'; ensure = ensure' } :: accu_m, defsvars)

687

s.modes ([], defsvars)

688

in

689


690

let new_locals = List.filter not_is_orig_var vars in

691

(* removing inouts and initial locals ones *)

692

( new_locals,

693

defs,

694

{

695

s with

696

(* locals = s.locals @ new_locals; *)

697

stmts = [];

698

assume = assume';

699

guarantees = guarantees';

700

modes = modes';

701

} )

702

(* let nee _ = () in

703

* (\*normalize_eexpr decls iovars in *\)

704

* List.iter nee s.assume;

705

* List.iter nee s.guarantees;

706

* List.iter (fun m >

707

* List.iter nee m.require;

708

* List.iter nee m.ensure

709

* ) s.modes; *)

710


711

(* The normalization phase introduces new local variables

712

 output cannot be memories. If this happen, new local variables acting as

713

memories are introduced.

714

 array constants, pre, arrow, fby, ite, merge, calls to node with index

715

access

716

Thoses values are shared, ie. no duplicate expressions are introduced.

717


718

Concerning specification, a similar process is applied, replacing an

719

expression by a list of local variables and definitions

720

*)

721


722

(** normalize_node node returns a normalized node,

723

ie.

724

 updated locals

725

 new equations

726



727

*)

728

let normalize_node node =

729

reset_cpt_fresh ();

730

let orig_vars = node.node_inputs @ node.node_outputs @ node.node_locals in

731

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

732

let norm_ctx =

733

{

734

parentid = node.node_id;

735

vars = get_node_vars node;

736

is_output =

737

(fun vid > List.exists (fun v > v.var_id = vid) node.node_outputs);

738

}

739

in

740


741

let eqs, auts = get_node_eqs node in

742

if auts != [] then assert false;

743

(* Automata should be expanded by now. *)

744

let spec, new_vars, eqs =

745

(* Update mutable fields of eexpr to perform normalization of

746

specification.

747


748

Careful: we do not normalize annotations, since they can have the form

749

x = (a, b, c) *)

750

match node.node_spec with

751

 None  Some (NodeSpec _) > node.node_spec, [], eqs

752

 Some (Contract s) >

753

let new_locals, new_stmts, s' =

754

normalize_spec node.node_id

755

(node.node_inputs, node.node_outputs, node.node_locals)

756

s

757

in

758

(* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals;

759

* Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *)

760

Some (Contract s'), new_locals, new_stmts @ eqs

761

in

762

let defs, vars =

763

List.fold_left (normalize_eq norm_ctx) ([], new_vars @ orig_vars) eqs

764

in

765

(* Normalize the asserts *)

766

let vars, assert_defs, asserts =

767

List.fold_left

768

(fun (vars, def_accu, assert_accu) assert_ >

769

let assert_expr = assert_.assert_expr in

770

let (defs, vars'), expr =

771

normalize_expr ~alias:true

772

(* forcing introduction of new equations for fcn calls *)

773

norm_ctx []

774

(* empty offset for arrays *)

775

([], vars)

776

(* defvar only contains vars *)

777

assert_expr

778

in

779

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

780

( vars',

781

defs @ def_accu,

782

{ assert_ with assert_expr = expr } :: assert_accu ))

783

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

784

in

785

let new_locals = List.filter not_is_orig_var vars in

786


787

(* we filter out inout

788

vars and initial locals ones *)

789

let all_locals = node.node_locals @ new_locals in

790


791

(* we add again, at the

792

beginning of the list the

793

local declared ones *)

794

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

795


796

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

797


798

(* Compute traceability info:

799

 gather newly bound variables

800

 compute the associated expression without aliases

801

*)

802

let new_annots =

803

if !Options.traces then

804

let diff_vars =

805

List.filter (fun v > not (List.mem v node.node_locals)) all_locals

806

in

807

let norm_traceability =

808

{

809

annots =

810

List.map

811

(fun v >

812

let eq =

813

try

814

List.find

815

(fun eq >

816

List.exists (fun v' > v' = v.var_id) eq.eq_lhs)

817

(defs @ assert_defs)

818

with Not_found >

819

Format.eprintf

820

"Traceability annotation generation: var %s not found@."

821

v.var_id;

822

assert false

823

in

824

let expr =

825

substitute_expr diff_vars (defs @ assert_defs) eq.eq_rhs

826

in

827

let pair =

828

mkeexpr expr.expr_loc

829

(mkexpr expr.expr_loc

830

(Expr_tuple

831

[ expr_of_ident v.var_id expr.expr_loc; expr ]))

832

in

833

Annotations.add_expr_ann node.node_id pair.eexpr_tag

834

[ "traceability" ];

835

[ "traceability" ], pair)

836

diff_vars;

837

annot_loc = Location.dummy_loc;

838

}

839

in

840

norm_traceability :: node.node_annot

841

else node.node_annot

842

in

843


844

let new_annots =

845

List.fold_left

846

(fun annots v >

847

if Machine_types.is_active && Machine_types.is_exportable v then (

848

let typ = Machine_types.get_specified_type v in

849

let typ_name = Machine_types.type_name typ in

850


851

let loc = v.var_loc in

852

let typ_as_string = mkexpr loc (Expr_const (Const_string typ_name)) in

853

let pair =

854

expr_to_eexpr

855

(expr_of_expr_list loc [ expr_of_vdecl v; typ_as_string ])

856

in

857

Annotations.add_expr_ann node.node_id pair.eexpr_tag

858

Machine_types.keyword;

859

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

860

:: annots)

861

else annots)

862

new_annots new_locals

863

in

864


865

let node =

866

{

867

node with

868

node_locals = all_locals;

869

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

870

node_asserts = asserts;

871

node_annot = new_annots;

872

node_spec = spec;

873

}

874

in

875

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

876

node

877


878

let normalize_inode nd =

879

reset_cpt_fresh ();

880

match nd.nodei_spec with

881

 None  Some (NodeSpec _) > nd

882

 Some (Contract _) > assert false

883


884

let normalize_decl (decl : top_decl) : top_decl =

885

match decl.top_decl_desc with

886

 Node nd >

887

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

888

update_node nd.node_id decl';

889

decl'

890

 ImportedNode nd >

891

let decl' =

892

{ decl with top_decl_desc = ImportedNode (normalize_inode nd) }

893

in

894

update_node nd.nodei_id decl';

895

decl'

896

 Include _  Open _  Const _  TypeDef _ > decl

897


898

let normalize_prog p decls =

899

(* Backend specific configurations for normalization *)

900

params := p;

901


902

(* Main algorithm: iterates over nodes *)

903

List.map normalize_decl decls

904


905

(* Fake interface for outside uses *)

906

let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr =

907

mk_expr_alias_opt opt

908

{ parentid; vars = ctx_vars; is_output = (fun _ > false) }

909

(defs, vars) expr

910


911

(* Local Variables: *)

912

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

913

(* End: *)
