1

(********************************************************************)

2

(* *)

3

(* The LustreC compiler toolset / The LustreC Development Team *)

4

(* Copyright 2012   ONERA  CNRS  INPT *)

5

(* *)

6

(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)

7

(* under the terms of the GNU Lesser General Public License *)

8

(* version 2.1. *)

9

(* *)

10

(********************************************************************)

11


12

open Utils

13

open LustreSpec

14

open Corelang

15

open Format

16

open Normalization_common

17


18

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

19

replacing description with [norm_d],

20

taking propagated [offsets] into account

21

in order to change expression type *)

22

let mk_norm_expr offsets ref_e norm_d =

23

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

24

let drop_array_type ty =

25

Types.map_tuple_type Types.array_element_type ty in

26

{ ref_e with

27

expr_desc = norm_d;

28

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

29


30

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

31

let rec normalize_list alias node offsets norm_element defvars elist =

32

List.fold_right

33

(fun t (defvars, qlist) >

34

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

35

(defvars, norm_t :: qlist)

36

) elist (defvars, [])

37


38

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

39

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

40

match expr.expr_desc with

41

 Expr_const _

42

 Expr_ident _ > defvars, unfold_offsets expr offsets

43

 Expr_array elist >

44

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

45

let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in

46

mk_expr_alias_opt alias node defvars norm_expr

47

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

48

let defvars, norm_e1 = normalize_expr node offsets defvars e1 in

49

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

50

mk_expr_alias_opt alias node defvars norm_expr

51

 Expr_power (e1, d) >

52

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

53

 Expr_access (e1, d) >

54

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

55

 Expr_tuple elist >

56

let defvars, norm_elist =

57

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

58

defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)

59

 Expr_appl (id, args, None)

60

when Basic_library.is_homomorphic_fun id

61

&& Types.is_array_type expr.expr_type >

62

let defvars, norm_args =

63

normalize_list

64

alias

65

node

66

offsets

67

(fun _ > normalize_array_expr ~alias:true)

68

defvars

69

(expr_list_of_expr args)

70

in

71

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

72

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

73

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

74

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

75

 Expr_appl (id, args, r) >

76

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

77

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

78

if offsets <> []

79

then

80

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

81

normalize_expr ~alias:alias node offsets defvars norm_expr

82

else

83

mk_expr_alias_opt (alias && not (Basic_library.is_expr_internal_fun expr)) node defvars norm_expr

84

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

85

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

86

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

87

 Expr_arrow (e1,e2) >

88

let defvars, norm_e1 = normalize_expr node offsets defvars e1 in

89

let defvars, norm_e2 = normalize_expr node offsets defvars e2 in

90

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

91

mk_expr_alias_opt alias node defvars norm_expr

92

 Expr_pre e >

93

let defvars, norm_e = normalize_expr node offsets defvars e in

94

let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in

95

mk_expr_alias_opt alias node defvars norm_expr

96

 Expr_fby (e1, e2) >

97

let defvars, norm_e1 = normalize_expr node offsets defvars e1 in

98

let defvars, norm_e2 = normalize_expr node offsets defvars e2 in

99

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

100

mk_expr_alias_opt alias node defvars norm_expr

101

 Expr_when (e, c, l) >

102

let defvars, norm_e = normalize_expr node offsets defvars e in

103

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

104

 Expr_ite (c, t, e) >

105

let defvars, norm_c = normalize_guard node defvars c in

106

let defvars, norm_t = normalize_cond_expr node offsets defvars t in

107

let defvars, norm_e = normalize_cond_expr node offsets defvars e in

108

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

109

mk_expr_alias_opt alias node defvars norm_expr

110

 Expr_merge (c, hl) >

111

let defvars, norm_hl = normalize_branches node offsets defvars hl in

112

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

113

mk_expr_alias_opt alias node defvars norm_expr

114


115

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

116

(*

117

let norm_conditional_as_merge alias node norm_expr offsets defvars expr =

118

match expr.expr_desc with

119

 Expr_ite (c, t, e) >

120

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

121

 _ > assert false

122

*)

123

and normalize_branches node offsets defvars hl =

124

List.fold_right

125

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

126

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

127

defvars, (t, norm_h) :: norm_q

128

)

129

hl (defvars, [])

130


131

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

132

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

133

match expr.expr_desc with

134

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

135

let defvars, norm_e1 = normalize_expr node offsets defvars e1 in

136

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

137

 Expr_power (e1, d) >

138

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

139

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

140

 Expr_array elist when offsets = [] >

141

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

142

defvars, mk_norm_expr offsets expr (Expr_array norm_elist)

143

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

144

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

145

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

146

 _ > normalize_expr ~alias:alias node offsets defvars expr

147


148

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

149

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

150

match expr.expr_desc with

151

 Expr_access (e1, d) >

152

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

153

 Expr_ite (c, t, e) >

154

let defvars, norm_c = normalize_guard node defvars c in

155

let defvars, norm_t = normalize_cond_expr node offsets defvars t in

156

let defvars, norm_e = normalize_cond_expr node offsets defvars e in

157

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

158

 Expr_merge (c, hl) >

159

let defvars, norm_hl = normalize_branches node offsets defvars hl in

160

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

161

 _ > normalize_expr ~alias:alias node offsets defvars expr

162


163

and normalize_guard node defvars expr =

164

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

165

mk_expr_alias_opt true node defvars norm_expr

166


167

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

168

*)

169

let decouple_outputs node defvars eq =

170

let rec fold_lhs defvars lhs tys cks =

171

match lhs, tys, cks with

172

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

173

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

174

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

175

then

176

let newvar = mk_fresh_var node eq.eq_loc t c in

177

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

178

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

179

else

180

(defs_q, vars_q), v::lhs_q

181

 _ > assert false in

182

let defvars', lhs' =

183

fold_lhs

184

defvars

185

eq.eq_lhs

186

(Types.type_list_of_type eq.eq_rhs.expr_type)

187

(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in

188

defvars', {eq with eq_lhs = lhs' }

189


190

let rec normalize_eq node defvars eq =

191

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

192

match eq.eq_rhs.expr_desc with

193

 Expr_pre _

194

 Expr_fby _ >

195

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

196

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

197

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

198

(norm_eq::defs', vars')

199

 Expr_array _ >

200

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

201

let norm_eq = { eq with eq_rhs = norm_rhs } in

202

(norm_eq::defs', vars')

203

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

204

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

205

let norm_eq = { eq with eq_rhs = norm_rhs } in

206

(norm_eq::defs', vars')

207

 Expr_appl _ >

208

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

209

let norm_eq = { eq with eq_rhs = norm_rhs } in

210

(norm_eq::defs', vars')

211

 _ >

212

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

213

let norm_eq = { eq with eq_rhs = norm_rhs } in

214

norm_eq::defs', vars'

215


216

let normalize_eq_split node defvars eq =

217


218

let defs, vars = normalize_eq node defvars eq in

219

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

220

let eq_defs = Splitting.tuple_split_eq eq in

221

if eq_defs = [eq] then

222

eq::def, vars

223

else

224

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

225

) defs ([], vars)

226


227

let normalize_eexpr decls node vars ee =

228

(* New output variable *)

229

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

230

let output_var =

231

mkvar_decl

232

ee.eexpr_loc

233

(output_id,

234

mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)

235

mkclock ee.eexpr_loc Ckdec_any,

236

false (* not a constant *),

237

None)

238

in

239

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

240

(* Calls are first inlined *)

241

(* let nodes = get_registered_nodes () in *)

242

Format.eprintf "Reg nodes #####@.";

243

List.iter (fun nd > Format.eprintf "node %s@." (node_name nd)) decls;

244

Format.eprintf "Reg nodes #####@.";

245

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

246

let calls = List.map

247

(fun called_nd > try

248

(List.find (fun nd > node_name nd = called_nd) decls)

249

with _ > Format.eprintf "looking for node %s@." called_nd; assert false

250

) calls

251


252

in

253

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

254

let locals = node.node_locals @ (List.fold_left (fun accu (_, q) > q@accu) [] ee.eexpr_quantifiers) in

255

let (new_locals, eqs) =

256

if calls = [] && not (expr_has_arrows ee.eexpr_qfexpr) then

257

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

258

(locals, [eq])

259

else (

260

Format.eprintf "Ici@.";

261

let e, new_locals, eqs, _ (* asserts *), _ (* annots *) =

262

Inliner.inline_expr ee.eexpr_qfexpr locals node calls

263

in

264

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

265

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

266

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

267

(new_locals, eq::eqs)

268

) in

269

(* Normalizing expr and eqs *)

270

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

271

let todefine = List.fold_left

272

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

273

(ISet.add output_id ISet.empty) vars in

274

try

275

let env = Typing.type_var_decl_list quant_vars Basic_library.type_env quant_vars in

276

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

277

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

278

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

279

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

280

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

281

(* check that table is empty *)

282

if (not (ISet.is_empty undefined_vars)) then

283

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

284


285

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

286

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

287

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

288

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

289

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

290

Printers.pp_eexpr ee

291

Types.pp_error err

292

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

293

Location.pp_loc loc

294


295

;

296

raise exc

297


298

let normalize_spec decls node vars s =

299

let nee = normalize_eexpr decls node vars in

300

List.iter nee s.requires;

301

List.iter nee s.ensures;

302

List.iter (fun (_, assumes, ensures, _) >

303

List.iter nee assumes;

304

List.iter nee ensures

305

) s.behaviors

306


307


308

(* The normalization phase introduces new local variables

309

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

310

memories are introduced.

311

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

312

access

313

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

314


315

Concerning specification, a similar process is applied, replacing an

316

expression by a list of local variables and definitions

317

*)

318


319

(** normalize_node prog node returns a normalized node,

320

ie.

321

 updated locals

322

 new equations

323



324

*)

325

let normalize_node decls node =

326

cpt_fresh := 0;

327

let inputs_outputs = node.node_inputs@node.node_outputs in

328

let is_local v =

329

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

330

let orig_vars = inputs_outputs@node.node_locals in

331

let defs, vars =

332

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

333

(* Normalize the asserts *)

334

let vars, assert_defs, asserts =

335

List.fold_left (

336

fun (vars, def_accu, assert_accu) assert_ >

337

let assert_expr = assert_.assert_expr in

338

let (defs, vars'), expr =

339

normalize_expr

340

~alias:false

341

node

342

[] (* empty offset for arrays *)

343

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

344

assert_expr

345

in

346

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

347

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

348

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

349

let new_locals = List.filter is_local vars in

350

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

351


352

let new_annots =

353

if !Options.traces then

354

begin

355

(* Compute traceability info:

356

 gather newly bound variables

357

 compute the associated expression without aliases

358

*)

359

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

360

let norm_traceability = {

361

annots = List.map (fun v >

362

let eq =

363

try

364

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

365

with Not_found >

366

(

367

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

368

assert false

369

)

370

in

371

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

372

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

373

(["traceability"], pair)

374

) diff_vars;

375

annot_loc = Location.dummy_loc

376

}

377

in

378

norm_traceability::node.node_annot

379

end

380

else

381

node.node_annot

382

in

383

if !Options.spec <> "no" then

384

begin

385

(* Update mutable fields of eexpr to perform normalization of specification/annotations *)

386

List.iter

387

(fun a >

388

List.iter

389

(fun (_, ann) > normalize_eexpr decls node inputs_outputs ann)

390

a.annots

391

)

392

node.node_annot;

393

match node.node_spec with None > ()  Some s > normalize_spec decls node [] s

394

end;

395


396


397

let new_locals = List.filter is_local vars in

398

let node =

399

{ node with

400

node_locals = new_locals;

401

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

402

node_asserts = asserts;

403

node_annot = new_annots;

404

}

405

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

406

node

407

)

408


409

let normalize_decl decls decl =

410

match decl.top_decl_desc with

411

 Node nd >

412

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

413

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

414

decl'

415

 Open _  ImportedNode _  Const _  TypeDef _ > decl

416


417

let normalize_prog decls =

418

List.map (normalize_decl decls) decls

419


420

(* Local Variables: *)

421

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

422

(* End: *)
