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

{

37

unfold_arrow_active: bool;

38

force_alias_ite: bool;

39

force_alias_internal_fun: bool;

40

}

41


42

let params = 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

{

51

parentid: ident;

52

vars: var_decl list;

53

is_output: ident > bool;

54

}

55


56


57

let expr_true loc ck =

58

{ expr_tag = Utils.new_tag ();

59

expr_desc = Expr_const (Const_tag tag_true);

60

expr_type = Type_predef.type_bool;

61

expr_clock = ck;

62

expr_delay = Delay.new_var ();

63

expr_annot = None;

64

expr_loc = loc }

65


66

let expr_false loc ck =

67

{ expr_tag = Utils.new_tag ();

68

expr_desc = Expr_const (Const_tag tag_false);

69

expr_type = Type_predef.type_bool;

70

expr_clock = ck;

71

expr_delay = Delay.new_var ();

72

expr_annot = None;

73

expr_loc = loc }

74


75

let expr_once loc ck =

76

{ expr_tag = Utils.new_tag ();

77

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

78

expr_type = Type_predef.type_bool;

79

expr_clock = ck;

80

expr_delay = Delay.new_var ();

81

expr_annot = None;

82

expr_loc = loc }

83


84

let is_expr_once =

85

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

86

fun expr > Corelang.is_eq_expr expr dummy_expr_once

87


88

let unfold_arrow expr =

89

match expr.expr_desc with

90

 Expr_arrow (e1, e2) >

91

let loc = expr.expr_loc in

92

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

93

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

94

 _ > assert false

95


96


97


98

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

99

let get_expr_alias defs expr =

100

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)

101

with

102

 Not_found > None

103


104

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

105

let replace_expr locals expr =

106

match locals with

107

 [] > assert false

108

 [v] > { expr with

109

expr_tag = Utils.new_tag ();

110

expr_desc = Expr_ident v.var_id }

111

 _ > { expr with

112

expr_tag = Utils.new_tag ();

113

expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }

114


115


116

(* IS IT USED ? TODO

117

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

118

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

119

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

120

match get_expr_alias defs expr with

121

 Some eq >

122

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

123

(defs, vars), replace_expr aliases expr

124

 None >

125

let new_aliases =

126

List.map2

127

(mk_fresh_var (parentid, vars) expr.expr_loc)

128

(Types.type_list_of_type expr.expr_type)

129

(Clocks.clock_list_of_clock expr.expr_clock) in

130

let new_def =

131

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

132

in

133

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

134

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

135

*)

136


137

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

138

and [opt] is true

139


140


141

*)

142

let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =

143

if !debug then

144

Log.report ~plugin:"normalization" ~level:2

145

(fun fmt > Format.fprintf fmt "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);

146

match expr.expr_desc with

147

 Expr_ident alias >

148

(defs, vars), expr

149

 _ >

150

match get_expr_alias defs expr with

151

 Some eq >

152

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

153

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

154

(defs, vars), replace_expr aliases expr

155

 None >

156

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

157

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

158

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

159

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

160

* Clocks.print_ck eq.eq_rhs.expr_clock

161

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

162

* (is_eq_expr eq.eq_rhs expr)

163

* Printers.pp_node_eq eq))

164

* defs; *)

165

if opt

166

then

167

let new_aliases =

168

List.map2

169

(mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc)

170

(Types.type_list_of_type expr.expr_type)

171

(Clocks.clock_list_of_clock expr.expr_clock) in

172

let new_def =

173

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

174

in

175

(* Typing and Registering machine type *)

176

let _ = if Machine_types.is_active then

177

Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr

178

in

179

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

180

else

181

(defs, vars), expr

182


183

(* Similar fonctions for dimensions *)

184

let mk_dim_alias opt norm_ctx (defs, vars) dim =

185

match dim.Dimension.dim_desc with

186

 Dimension.Dbool _  Dint _

187

 Dident _ > (defs, vars), dim (* Keep the same *)

188

 _ when opt > (* Cast to expression, normalizing *)

189

let e = expr_of_dimension dim in

190

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

191

defvars, dimension_of_expr e

192


193

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

194


195


196

let unfold_offsets norm_ctx defvars e offsets =

197

let add_offset (defvars, e) d =

198

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

199

let defvars, d = mk_dim_alias !params.force_alias_internal_fun norm_ctx defvars d in

200

let new_e =

201

{ e with

202

expr_tag = Utils.new_tag ();

203

expr_loc = d.Dimension.dim_loc;

204

expr_type = Types.array_element_type e.expr_type;

205

expr_desc = Expr_access (e, d) }

206

in

207

defvars, new_e

208

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

209

in

210

List.fold_left add_offset (defvars, e) offsets

211


212


213

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

214

replacing description with [norm_d],

215

taking propagated [offsets] into account

216

in order to change expression type *)

217

let mk_norm_expr offsets ref_e norm_d =

218

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

219

let drop_array_type ty =

220

Types.map_tuple_type Types.array_element_type ty in

221

{ ref_e with

222

expr_desc = norm_d;

223

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

224


225

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

226

let rec normalize_list alias norm_ctx offsets norm_element defvars elist =

227

List.fold_right

228

(fun t (defvars, qlist) >

229

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

230

(defvars, norm_t :: qlist)

231

) elist (defvars, [])

232


233

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

234

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

235

match expr.expr_desc with

236

 Expr_const _

237

 Expr_ident _ >

238

unfold_offsets norm_ctx defvars expr offsets

239

 Expr_array elist >

240

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

241

let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in

242

mk_expr_alias_opt alias norm_ctx defvars norm_expr

243

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

244

let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

245

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

246

mk_expr_alias_opt alias norm_ctx defvars norm_expr

247

 Expr_power (e1, d) >

248

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

249

 Expr_access (e1, d) >

250

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

251


252

 Expr_tuple elist >

253

let defvars, norm_elist =

254

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

255

defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)

256

 Expr_appl (id, args, None)

257

when Basic_library.is_homomorphic_fun id

258

&& Types.is_array_type expr.expr_type >

259

let defvars, norm_args =

260

normalize_list

261

alias

262

norm_ctx

263

offsets

264

(fun _ > normalize_array_expr ~alias:true)

265

defvars

266

(expr_list_of_expr args)

267

in

268

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

269

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

270

&& not (!params.force_alias_internal_fun  alias_basic) >

271

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

272

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

273

 Expr_appl (id, args, r) >

274

let defvars, r =

275

match r with

276

 None > defvars, None

277

 Some r >

278

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

279

defvars, Some norm_r

280

in

281

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

282

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

283

if offsets <> []

284

then

285

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

286

normalize_expr ~alias:alias norm_ctx offsets defvars norm_expr

287

else

288

mk_expr_alias_opt (alias && (!params.force_alias_internal_fun  alias_basic

289

 not (Basic_library.is_expr_internal_fun expr)))

290

norm_ctx defvars norm_expr

291

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

292

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

293

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

294

 Expr_arrow (e1,e2) >

295

let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

296

let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in

297

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

298

mk_expr_alias_opt alias norm_ctx defvars norm_expr

299

 Expr_pre e >

300

let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in

301

let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in

302

mk_expr_alias_opt alias norm_ctx defvars norm_expr

303

 Expr_fby (e1, e2) >

304

let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

305

let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in

306

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

307

mk_expr_alias_opt alias norm_ctx defvars norm_expr

308

 Expr_when (e, c, l) >

309

let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in

310

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

311

 Expr_ite (c, t, e) >

312

let defvars, norm_c = normalize_guard norm_ctx defvars c in

313

let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in

314

let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in

315

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

316

mk_expr_alias_opt alias norm_ctx defvars norm_expr

317

 Expr_merge (c, hl) >

318

let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in

319

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

320

mk_expr_alias_opt alias norm_ctx defvars norm_expr

321


322

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

323

(*

324

let norm_conditional_as_merge alias node norm_expr offsets defvars expr =

325

match expr.expr_desc with

326

 Expr_ite (c, t, e) >

327

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

328

 _ > assert false

329

*)

330

and normalize_branches norm_ctx offsets defvars hl =

331

List.fold_right

332

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

333

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

334

defvars, (t, norm_h) :: norm_q

335

)

336

hl (defvars, [])

337


338

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

339

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

340

match expr.expr_desc with

341

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

342

let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

343

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

344

 Expr_power (e1, d) >

345

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

346

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

347

 Expr_array elist when offsets = [] >

348

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

349

defvars, mk_norm_expr offsets expr (Expr_array norm_elist)

350

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

351

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

352

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

353

 _ > normalize_expr ~alias:alias norm_ctx offsets defvars expr

354


355

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

356

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

357

match expr.expr_desc with

358

 Expr_access (e1, d) >

359

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

360

 Expr_ite (c, t, e) >

361

let defvars, norm_c = normalize_guard norm_ctx defvars c in

362

let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in

363

let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in

364

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

365

 Expr_merge (c, hl) >

366

let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in

367

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

368

 _ when !params.force_alias_ite >

369

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

370

let defvars, norm_expr =

371

normalize_expr ~alias:alias norm_ctx offsets defvars expr

372

in

373

mk_expr_alias_opt true norm_ctx defvars norm_expr

374

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

375

normalize_expr ~alias:alias norm_ctx offsets defvars expr

376


377

and normalize_guard norm_ctx defvars expr =

378

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

379

mk_expr_alias_opt true norm_ctx defvars norm_expr

380


381

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

382

*)

383

let decouple_outputs norm_ctx defvars eq =

384

let rec fold_lhs defvars lhs tys cks =

385

match lhs, tys, cks with

386

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

387

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

388

if norm_ctx.is_output v

389

then

390

let newvar = mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c in

391

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

392

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

393

else

394

(defs_q, vars_q), v::lhs_q

395

 _ > assert false in

396

let defvars', lhs' =

397

fold_lhs

398

defvars

399

eq.eq_lhs

400

(Types.type_list_of_type eq.eq_rhs.expr_type)

401

(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in

402

defvars', {eq with eq_lhs = lhs' }

403


404

let rec normalize_eq norm_ctx defvars eq =

405

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

406

match eq.eq_rhs.expr_desc with

407

 Expr_pre _

408

 Expr_fby _ >

409

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

410

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

411

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

412

(norm_eq::defs', vars')

413

 Expr_array _ >

414

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

415

let norm_eq = { eq with eq_rhs = norm_rhs } in

416

(norm_eq::defs', vars')

417

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

418

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

419

let norm_eq = { eq with eq_rhs = norm_rhs } in

420

(norm_eq::defs', vars')

421

 Expr_appl _ >

422

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

423

let norm_eq = { eq with eq_rhs = norm_rhs } in

424

(norm_eq::defs', vars')

425

 _ >

426

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

427

let norm_eq = { eq with eq_rhs = norm_rhs } in

428

norm_eq::defs', vars'

429


430

let normalize_eq_split norm_ctx defvars eq =

431

try

432

let defs, vars = normalize_eq norm_ctx defvars eq in

433

List.fold_right (fun eq (def, vars) >

434

let eq_defs = Splitting.tuple_split_eq eq in

435

if eq_defs = [eq] then

436

eq::def, vars

437

else

438

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

439

) defs ([], vars)

440


441

with ex > (

442

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

443

raise ex

444

)

445


446

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

447

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

448

associated statement *)

449

let normalize_pred_eexpr decls norm_ctx (def,vars) ee =

450

assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *)

451

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

452

let skip =

453

match ee.eexpr_qfexpr.expr_desc with

454

 Expr_ident _  Expr_const _ > true

455

 _ > false

456

in

457

if skip then

458

ee, (def, vars)

459

else (

460

(* New output variable *)

461

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

462

let output_var =

463

mkvar_decl

464

ee.eexpr_loc

465

(output_id,

466

mktyp ee.eexpr_loc Tydec_bool, (* It is a predicate, hence a bool *)

467

mkclock ee.eexpr_loc Ckdec_any,

468

false (* not a constant *),

469

None,

470

None

471

)

472

in

473

let output_expr = expr_of_vdecl output_var in

474

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

475

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

476


477

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

478

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

479

result. *)

480

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

481


482


483

(* (\* Inlining any calls *\)

484

* let nodes = get_nodes decls in

485

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

486

* let vars, eqs =

487

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

488

* vars, [eq]

489

* else

490

* assert false (\* TODO *\)

491

* in *)

492


493

(* Normalizing expr and eqs *)

494

let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) [eq] in

495

let vars = output_var :: vars in

496

(* let todefine =

497

List.fold_left

498

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

499

(ISet.add output_id ISet.empty) vars in

500

*)

501


502

(* Typing / Clocking *)

503

try

504

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

505

(*

506

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

507

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

508

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

509

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

510

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

511

(* check that table is empty *)

512

if (not (ISet.is_empty undefined_vars)) then

513

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

514


515

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

516

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

517

*)

518


519

ee', (defs, vars)

520


521

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

522

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

523

Printers.pp_eexpr ee

524

Types.pp_error err

525

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

526

Location.pp_loc loc

527


528


529

;

530

raise exc

531


532

)

533


534

(*

535


536

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

537

(* Calls are first inlined *)

538


539

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

540

let (new_locals, eqs) =

541

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

542

(locals, [eq])

543

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

544

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

545

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

546

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

547

(new_locals, eqs)

548

*)

549

(locals, [eq])

550


551

) in

552

(* Normalizing expr and eqs *)

553

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

554

let todefine = List.fold_left

555

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

556

(ISet.add output_id ISet.empty) vars in

557


558

try

559

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

560

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

561

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

562

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

563

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

564

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

565

(* check that table is empty *)

566

if (not (ISet.is_empty undefined_vars)) then

567

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

568


569

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

570

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

571

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

572


573

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

574

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

575

Printers.pp_eexpr ee

576

Types.pp_error err

577

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

578

Location.pp_loc loc

579


580


581

;

582

raise exc

583

*)

584


585


586

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

587

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

588

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

589

spec locals (no node locals) *)

590

let orig_vars = in_vars @ out_vars @ s.locals in

591

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

592

let not_is_orig_var v =

593

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

594

let norm_ctx = {

595

parentid = parentid;

596

vars = in_vars @ out_vars @ l_vars;

597

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

598

}

599

in

600

(* Normalizing existing stmts *)

601

let eqs, auts = List.fold_right (fun s (el,al) > match s with Eq e > e::el, al  Aut a > el, a::al) s.stmts ([], []) in

602

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

603

let defsvars =

604

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

605

in

606

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

607

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

608

let process_predicates l defvars =

609

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

610

let res = List.fold_right (fun ee (accu, defvars) >

611

let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in

612

ee'::accu, defvars

613

) l ([], defvars)

614

in

615

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

616

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

617

res

618

in

619


620


621

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

622

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

623

let modes', (defs, vars) =

624

List.fold_right (

625

fun m (accu_m, defsvars) >

626

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

627

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

628

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

629

) s.modes ([], defsvars)

630

in

631


632

let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)

633

new_locals, defs,

634

{s with

635

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

636

stmts = [];

637

assume = assume';

638

guarantees = guarantees';

639

modes = modes'

640

}

641

(* let nee _ = () in

642

* (\*normalize_eexpr decls iovars in *\)

643

* List.iter nee s.assume;

644

* List.iter nee s.guarantees;

645

* List.iter (fun m >

646

* List.iter nee m.require;

647

* List.iter nee m.ensure

648

* ) s.modes; *)

649


650


651


652


653


654


655

(* The normalization phase introduces new local variables

656

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

657

memories are introduced.

658

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

659

access

660

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

661


662

Concerning specification, a similar process is applied, replacing an

663

expression by a list of local variables and definitions

664

*)

665


666

(** normalize_node node returns a normalized node,

667

ie.

668

 updated locals

669

 new equations

670



671

*)

672

let normalize_node decls node =

673

reset_cpt_fresh ();

674

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

675

let not_is_orig_var v =

676

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

677

let norm_ctx = {

678

parentid = node.node_id;

679

vars = get_node_vars node;

680

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

681

}

682

in

683


684

let eqs, auts = get_node_eqs node in

685

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

686

let spec, new_vars, eqs =

687

begin

688

(* Update mutable fields of eexpr to perform normalization of

689

specification.

690


691

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

692

x = (a, b, c) *)

693

match node.node_spec with

694

 None

695

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

696

 Some (Contract s) >

697

let new_locals, new_stmts, s' = normalize_spec

698

decls

699

node.node_id

700

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

701

s

702

in

703

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

704

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

705

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

706

end

707

in

708

let defs, vars =

709

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

710

(* Normalize the asserts *)

711

let vars, assert_defs, asserts =

712

List.fold_left (

713

fun (vars, def_accu, assert_accu) assert_ >

714

let assert_expr = assert_.assert_expr in

715

let (defs, vars'), expr =

716

normalize_expr

717

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

718

norm_ctx

719

[] (* empty offset for arrays *)

720

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

721

assert_expr

722

in

723

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

724

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

725

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

726

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

727

vars and initial locals ones *)

728


729

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

730

beginning of the list the

731

local declared ones *)

732

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

733


734


735

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

736


737

(* Compute traceability info:

738

 gather newly bound variables

739

 compute the associated expression without aliases

740

*)

741

let new_annots =

742

if !Options.traces then

743

begin

744

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

745

let norm_traceability = {

746

annots = List.map (fun v >

747

let eq =

748

try

749

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

750

with Not_found >

751

(

752

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

753

assert false

754

)

755

in

756

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

757

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

758

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

759

(["traceability"], pair)

760

) diff_vars;

761

annot_loc = Location.dummy_loc

762

}

763

in

764

norm_traceability::node.node_annot

765

end

766

else

767

node.node_annot

768

in

769


770

let new_annots =

771

List.fold_left (fun annots v >

772

if Machine_types.is_active && Machine_types.is_exportable v then

773

let typ = Machine_types.get_specified_type v in

774

let typ_name = Machine_types.type_name typ in

775


776

let loc = v.var_loc in

777

let typ_as_string =

778

mkexpr

779

loc

780

(Expr_const

781

(Const_string typ_name))

782

in

783

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

784

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

785

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

786

else

787

annots

788

) new_annots new_locals

789

in

790


791


792

let node =

793

{ node with

794

node_locals = all_locals;

795

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

796

node_asserts = asserts;

797

node_annot = new_annots;

798

node_spec = spec;

799

}

800

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

801

node

802

)

803


804

let normalize_inode decls nd =

805

reset_cpt_fresh ();

806

match nd.nodei_spec with

807

None  Some (NodeSpec _) > nd

808

 Some (Contract _) > assert false

809


810

let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =

811

match decl.top_decl_desc with

812

 Node nd >

813

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

814

update_node nd.node_id decl';

815

decl'

816

 ImportedNode nd >

817

let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode decls nd)} in

818

update_node nd.nodei_id decl';

819

decl'

820


821

 Include _ Open _  Const _  TypeDef _ > decl

822


823

let normalize_prog p decls =

824

(* Backend specific configurations for normalization *)

825

params := p;

826


827

(* Main algorithm: iterates over nodes *)

828

List.map (normalize_decl decls) decls

829


830


831

(* Fake interface for outside uses *)

832

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

833

mk_expr_alias_opt

834

opt

835

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

836

(defs, vars)

837

expr

838


839


840

(* Local Variables: *)

841

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

842

(* End: *)

843

