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

type param_t =

33

{

34

unfold_arrow_active: bool;

35

force_alias_ite: bool;

36

force_alias_internal_fun: bool;

37

}

38


39

let params = ref

40

{

41

unfold_arrow_active = false;

42

force_alias_ite = false;

43

force_alias_internal_fun =false;

44

}

45


46

type norm_ctx_t =

47

{

48

parentid: ident;

49

vars: var_decl list;

50

is_output: ident > bool;

51

}

52


53


54

let expr_true loc ck =

55

{ expr_tag = Utils.new_tag ();

56

expr_desc = Expr_const (Const_tag tag_true);

57

expr_type = Type_predef.type_bool;

58

expr_clock = ck;

59

expr_delay = Delay.new_var ();

60

expr_annot = None;

61

expr_loc = loc }

62


63

let expr_false loc ck =

64

{ expr_tag = Utils.new_tag ();

65

expr_desc = Expr_const (Const_tag tag_false);

66

expr_type = Type_predef.type_bool;

67

expr_clock = ck;

68

expr_delay = Delay.new_var ();

69

expr_annot = None;

70

expr_loc = loc }

71


72

let expr_once loc ck =

73

{ expr_tag = Utils.new_tag ();

74

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

75

expr_type = Type_predef.type_bool;

76

expr_clock = ck;

77

expr_delay = Delay.new_var ();

78

expr_annot = None;

79

expr_loc = loc }

80


81

let is_expr_once =

82

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

83

fun expr > Corelang.is_eq_expr expr dummy_expr_once

84


85

let unfold_arrow expr =

86

match expr.expr_desc with

87

 Expr_arrow (e1, e2) >

88

let loc = expr.expr_loc in

89

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

90

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

91

 _ > assert false

92


93


94


95

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

96

let get_expr_alias defs expr =

97

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)

98

with

99

 Not_found > None

100


101

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

102

let replace_expr locals expr =

103

match locals with

104

 [] > assert false

105

 [v] > { expr with

106

expr_tag = Utils.new_tag ();

107

expr_desc = Expr_ident v.var_id }

108

 _ > { expr with

109

expr_tag = Utils.new_tag ();

110

expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }

111


112

let unfold_offsets e offsets =

113

let add_offset e d =

114

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

115

let res = *)

116

{ e with

117

expr_tag = Utils.new_tag ();

118

expr_loc = d.Dimension.dim_loc;

119

expr_type = Types.array_element_type e.expr_type;

120

expr_desc = Expr_access (e, d) }

121

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

122

in

123

List.fold_left add_offset e offsets

124


125

(* IS IT USED ? TODO

126

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

127

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

128

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

129

match get_expr_alias defs expr with

130

 Some eq >

131

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

132

(defs, vars), replace_expr aliases expr

133

 None >

134

let new_aliases =

135

List.map2

136

(mk_fresh_var (parentid, vars) expr.expr_loc)

137

(Types.type_list_of_type expr.expr_type)

138

(Clocks.clock_list_of_clock expr.expr_clock) in

139

let new_def =

140

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

141

in

142

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

143

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

144

*)

145


146

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

147

and [opt] is true *)

148

let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =

149

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

150

match expr.expr_desc with

151

 Expr_ident alias >

152

(defs, vars), expr

153

 _ >

154

match get_expr_alias defs expr with

155

 Some eq >

156

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

157

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

158

(defs, vars), replace_expr aliases expr

159

 None >

160

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

161

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

162

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

163

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

164

* Clocks.print_ck eq.eq_rhs.expr_clock

165

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

166

* (is_eq_expr eq.eq_rhs expr)

167

* Printers.pp_node_eq eq))

168

* defs; *)

169

if opt

170

then

171

let new_aliases =

172

List.map2

173

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

174

(Types.type_list_of_type expr.expr_type)

175

(Clocks.clock_list_of_clock expr.expr_clock) in

176

let new_def =

177

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

178

in

179

(* Typing and Registering machine type *)

180

let _ = if Machine_types.is_active then

181

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

182

in

183

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

184

else

185

(defs, vars), expr

186


187

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

188

replacing description with [norm_d],

189

taking propagated [offsets] into account

190

in order to change expression type *)

191

let mk_norm_expr offsets ref_e norm_d =

192

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

193

let drop_array_type ty =

194

Types.map_tuple_type Types.array_element_type ty in

195

{ ref_e with

196

expr_desc = norm_d;

197

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

198


199

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

200

let rec normalize_list alias norm_ctx offsets norm_element defvars elist =

201

List.fold_right

202

(fun t (defvars, qlist) >

203

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

204

(defvars, norm_t :: qlist)

205

) elist (defvars, [])

206


207

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

208

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

209

match expr.expr_desc with

210

 Expr_const _

211

 Expr_ident _ > defvars, unfold_offsets expr offsets

212

 Expr_array elist >

213

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

214

let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in

215

mk_expr_alias_opt alias norm_ctx defvars norm_expr

216

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

217

let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

218

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

219

mk_expr_alias_opt alias norm_ctx defvars norm_expr

220

 Expr_power (e1, d) >

221

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

222

 Expr_access (e1, d) >

223

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

224

 Expr_tuple elist >

225

let defvars, norm_elist =

226

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

227

defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)

228

 Expr_appl (id, args, None)

229

when Basic_library.is_homomorphic_fun id

230

&& Types.is_array_type expr.expr_type >

231

let defvars, norm_args =

232

normalize_list

233

alias

234

norm_ctx

235

offsets

236

(fun _ > normalize_array_expr ~alias:true)

237

defvars

238

(expr_list_of_expr args)

239

in

240

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

241

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

242

&& not (!params.force_alias_internal_fun  alias_basic) >

243

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

244

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

245

 Expr_appl (id, args, r) >

246

let defvars, r =

247

match r with

248

 None > defvars, None

249

 Some r >

250

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

251

defvars, Some norm_r

252

in

253

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

254

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

255

if offsets <> []

256

then

257

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

258

normalize_expr ~alias:alias norm_ctx offsets defvars norm_expr

259

else

260

mk_expr_alias_opt (alias && (!params.force_alias_internal_fun  alias_basic

261

 not (Basic_library.is_expr_internal_fun expr)))

262

norm_ctx defvars norm_expr

263

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

264

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

265

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

266

 Expr_arrow (e1,e2) >

267

let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

268

let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in

269

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

270

mk_expr_alias_opt alias norm_ctx defvars norm_expr

271

 Expr_pre e >

272

let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in

273

let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in

274

mk_expr_alias_opt alias norm_ctx defvars norm_expr

275

 Expr_fby (e1, e2) >

276

let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

277

let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in

278

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

279

mk_expr_alias_opt alias norm_ctx defvars norm_expr

280

 Expr_when (e, c, l) >

281

let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in

282

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

283

 Expr_ite (c, t, e) >

284

let defvars, norm_c = normalize_guard norm_ctx defvars c in

285

let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in

286

let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in

287

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

288

mk_expr_alias_opt alias norm_ctx defvars norm_expr

289

 Expr_merge (c, hl) >

290

let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in

291

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

292

mk_expr_alias_opt alias norm_ctx defvars norm_expr

293


294

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

295

(*

296

let norm_conditional_as_merge alias node norm_expr offsets defvars expr =

297

match expr.expr_desc with

298

 Expr_ite (c, t, e) >

299

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

300

 _ > assert false

301

*)

302

and normalize_branches norm_ctx offsets defvars hl =

303

List.fold_right

304

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

305

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

306

defvars, (t, norm_h) :: norm_q

307

)

308

hl (defvars, [])

309


310

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

311

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

312

match expr.expr_desc with

313

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

314

let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in

315

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

316

 Expr_power (e1, d) >

317

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

318

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

319

 Expr_array elist when offsets = [] >

320

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

321

defvars, mk_norm_expr offsets expr (Expr_array norm_elist)

322

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

323

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

324

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

325

 _ > normalize_expr ~alias:alias norm_ctx offsets defvars expr

326


327

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

328

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

329

match expr.expr_desc with

330

 Expr_access (e1, d) >

331

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

332

 Expr_ite (c, t, e) >

333

let defvars, norm_c = normalize_guard norm_ctx defvars c in

334

let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in

335

let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in

336

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

337

 Expr_merge (c, hl) >

338

let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in

339

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

340

 _ when !params.force_alias_ite >

341

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

342

let defvars, norm_expr =

343

normalize_expr ~alias:alias norm_ctx offsets defvars expr

344

in

345

mk_expr_alias_opt true norm_ctx defvars norm_expr

346

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

347

normalize_expr ~alias:alias norm_ctx offsets defvars expr

348


349

and normalize_guard norm_ctx defvars expr =

350

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

351

mk_expr_alias_opt true norm_ctx defvars norm_expr

352


353

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

354

*)

355

let decouple_outputs norm_ctx defvars eq =

356

let rec fold_lhs defvars lhs tys cks =

357

match lhs, tys, cks with

358

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

359

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

360

if norm_ctx.is_output v

361

then

362

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

363

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

364

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

365

else

366

(defs_q, vars_q), v::lhs_q

367

 _ > assert false in

368

let defvars', lhs' =

369

fold_lhs

370

defvars

371

eq.eq_lhs

372

(Types.type_list_of_type eq.eq_rhs.expr_type)

373

(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in

374

defvars', {eq with eq_lhs = lhs' }

375


376

let rec normalize_eq norm_ctx defvars eq =

377

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

378

match eq.eq_rhs.expr_desc with

379

 Expr_pre _

380

 Expr_fby _ >

381

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

382

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

383

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

384

(norm_eq::defs', vars')

385

 Expr_array _ >

386

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

387

let norm_eq = { eq with eq_rhs = norm_rhs } in

388

(norm_eq::defs', vars')

389

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

390

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

391

let norm_eq = { eq with eq_rhs = norm_rhs } in

392

(norm_eq::defs', vars')

393

 Expr_appl _ >

394

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

395

let norm_eq = { eq with eq_rhs = norm_rhs } in

396

(norm_eq::defs', vars')

397

 _ >

398

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

399

let norm_eq = { eq with eq_rhs = norm_rhs } in

400

norm_eq::defs', vars'

401


402

let normalize_eq_split norm_ctx defvars eq =

403

try

404

let defs, vars = normalize_eq norm_ctx defvars eq in

405

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

406

let eq_defs = Splitting.tuple_split_eq eq in

407

if eq_defs = [eq] then

408

eq::def, vars

409

else

410

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

411

) defs ([], vars)

412


413

with ex > (

414

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

415

raise ex

416

)

417


418

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

419

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

420

associated statement *)

421

let normalize_pred_eexpr decls norm_ctx (def,vars) ee =

422

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

423

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

424

let skip =

425

match ee.eexpr_qfexpr.expr_desc with

426

 Expr_ident _  Expr_const _ > true

427

 _ > false

428

in

429

if skip then

430

ee, (def, vars)

431

else (

432

(* New output variable *)

433

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

434

let output_var =

435

mkvar_decl

436

ee.eexpr_loc

437

(output_id,

438

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

439

mkclock ee.eexpr_loc Ckdec_any,

440

false (* not a constant *),

441

None,

442

None

443

)

444

in

445

let output_expr = expr_of_vdecl output_var in

446

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

447

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

448


449

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

450

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

451

result. *)

452

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

453


454


455

(* (\* Inlining any calls *\)

456

* let nodes = get_nodes decls in

457

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

458

* let vars, eqs =

459

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

460

* vars, [eq]

461

* else

462

* assert false (\* TODO *\)

463

* in *)

464


465

(* Normalizing expr and eqs *)

466

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

467

let vars = output_var :: vars in

468

(* let todefine =

469

List.fold_left

470

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

471

(ISet.add output_id ISet.empty) vars in

472

*)

473


474

(* Typing / Clocking *)

475

try

476

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

477

(*

478

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

479

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

480

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

481

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

482

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

483

(* check that table is empty *)

484

if (not (ISet.is_empty undefined_vars)) then

485

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

486


487

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

488

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

489

*)

490


491

ee', (defs, vars)

492


493

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

494

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

495

Printers.pp_eexpr ee

496

Types.pp_error err

497

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

498

Location.pp_loc loc

499


500


501

;

502

raise exc

503


504

)

505


506

(*

507


508

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

509

(* Calls are first inlined *)

510


511

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

512

let (new_locals, eqs) =

513

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

514

(locals, [eq])

515

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

516

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

517

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

518

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

519

(new_locals, eqs)

520

*)

521

(locals, [eq])

522


523

) in

524

(* Normalizing expr and eqs *)

525

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

526

let todefine = List.fold_left

527

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

528

(ISet.add output_id ISet.empty) vars in

529


530

try

531

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

532

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

533

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

534

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

535

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

536

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

537

(* check that table is empty *)

538

if (not (ISet.is_empty undefined_vars)) then

539

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

540


541

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

542

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

543

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

544


545

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

546

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

547

Printers.pp_eexpr ee

548

Types.pp_error err

549

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

550

Location.pp_loc loc

551


552


553

;

554

raise exc

555

*)

556


557


558

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

559

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

560

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

561

spec locals (no node locals) *)

562

let orig_vars = in_vars @ out_vars @ s.locals in

563

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

564

let not_is_orig_var v =

565

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

566

let norm_ctx = {

567

parentid = parentid;

568

vars = in_vars @ out_vars @ l_vars;

569

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

570

}

571

in

572

(* Normalizing existing stmts *)

573

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

574

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

575

let defsvars =

576

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

577

in

578

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

579

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

580

let process_predicates l defvars =

581

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

582

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

583

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

584

ee'::accu, defvars

585

) l ([], defvars)

586

in

587

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

588

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

589

res

590

in

591


592


593

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

594

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

595

let modes', (defs, vars) =

596

List.fold_right (

597

fun m (accu_m, defsvars) >

598

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

599

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

600

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

601

) s.modes ([], defsvars)

602

in

603


604

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

605

new_locals, defs,

606

{s with

607

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

608

stmts = [];

609

assume = assume';

610

guarantees = guarantees';

611

modes = modes'

612

}

613

(* let nee _ = () in

614

* (\*normalize_eexpr decls iovars in *\)

615

* List.iter nee s.assume;

616

* List.iter nee s.guarantees;

617

* List.iter (fun m >

618

* List.iter nee m.require;

619

* List.iter nee m.ensure

620

* ) s.modes; *)

621


622


623


624


625


626


627

(* The normalization phase introduces new local variables

628

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

629

memories are introduced.

630

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

631

access

632

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

633


634

Concerning specification, a similar process is applied, replacing an

635

expression by a list of local variables and definitions

636

*)

637


638

(** normalize_node node returns a normalized node,

639

ie.

640

 updated locals

641

 new equations

642



643

*)

644

let normalize_node decls node =

645

reset_cpt_fresh ();

646

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

647

let not_is_orig_var v =

648

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

649

let norm_ctx = {

650

parentid = node.node_id;

651

vars = get_node_vars node;

652

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

653

}

654

in

655


656

let eqs, auts = get_node_eqs node in

657

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

658

let spec, new_vars, eqs =

659

begin

660

(* Update mutable fields of eexpr to perform normalization of

661

specification.

662


663

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

664

x = (a, b, c) *)

665

match node.node_spec with

666

 None

667

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

668

 Some (Contract s) >

669

let new_locals, new_stmts, s' = normalize_spec

670

decls

671

node.node_id

672

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

673

s

674

in

675

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

676

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

677

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

678

end

679

in

680

let defs, vars =

681

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

682

(* Normalize the asserts *)

683

let vars, assert_defs, asserts =

684

List.fold_left (

685

fun (vars, def_accu, assert_accu) assert_ >

686

let assert_expr = assert_.assert_expr in

687

let (defs, vars'), expr =

688

normalize_expr

689

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

690

norm_ctx

691

[] (* empty offset for arrays *)

692

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

693

assert_expr

694

in

695

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

696

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

697

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

698

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

699

vars and initial locals ones *)

700


701

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

702

beginning of the list the

703

local declared ones *)

704

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

705


706


707

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

708


709

(* Compute traceability info:

710

 gather newly bound variables

711

 compute the associated expression without aliases

712

*)

713

let new_annots =

714

if !Options.traces then

715

begin

716

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

717

let norm_traceability = {

718

annots = List.map (fun v >

719

let eq =

720

try

721

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

722

with Not_found >

723

(

724

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

725

assert false

726

)

727

in

728

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

729

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

730

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

731

(["traceability"], pair)

732

) diff_vars;

733

annot_loc = Location.dummy_loc

734

}

735

in

736

norm_traceability::node.node_annot

737

end

738

else

739

node.node_annot

740

in

741


742

let new_annots =

743

List.fold_left (fun annots v >

744

if Machine_types.is_active && Machine_types.is_exportable v then

745

let typ = Machine_types.get_specified_type v in

746

let typ_name = Machine_types.type_name typ in

747


748

let loc = v.var_loc in

749

let typ_as_string =

750

mkexpr

751

loc

752

(Expr_const

753

(Const_string typ_name))

754

in

755

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

756

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

757

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

758

else

759

annots

760

) new_annots new_locals

761

in

762


763


764

let node =

765

{ node with

766

node_locals = all_locals;

767

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

768

node_asserts = asserts;

769

node_annot = new_annots;

770

node_spec = spec;

771

}

772

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

773

node

774

)

775


776

let normalize_inode decls nd =

777

reset_cpt_fresh ();

778

match nd.nodei_spec with

779

None  Some (NodeSpec _) > nd

780

 Some (Contract _) > assert false

781


782

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

783

match decl.top_decl_desc with

784

 Node nd >

785

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

786

update_node nd.node_id decl';

787

decl'

788

 ImportedNode nd >

789

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

790

update_node nd.nodei_id decl';

791

decl'

792


793

 Include _ Open _  Const _  TypeDef _ > decl

794


795

let normalize_prog p decls =

796

(* Backend specific configurations for normalization *)

797

params := p;

798


799

(* Main algorithm: iterates over nodes *)

800

List.map (normalize_decl decls) decls

801


802


803

(* Fake interface for outside uses *)

804

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

805

mk_expr_alias_opt

806

opt

807

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

808

(defs, vars)

809

expr

810


811


812

(* Local Variables: *)

813

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

814

(* End: *)

815

