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 Lustre_types

13

open Machine_code_types

14

open Machine_code_common

15

open Spec_types

16

open Spec_common

17

open Corelang

18

open Clocks

19

open Causality

20

open Utils

21


22

exception NormalizationError

23


24

(* Questions:

25


26

 where are used the mconst. They contain initialization of

27

constant in nodes. But they do not seem to be used by c_backend *)

28


29


30

(* translate_<foo> : vars > context > <foo> > machine code/expression *)

31

(* the context contains m : state aka memory variables *)

32

(* si : initialization instructions *)

33

(* j : node aka machine instances *)

34

(* d : local variables *)

35

(* s : step instructions *)

36


37

(* Machine processing requires knowledge about variables and local

38

variables. Local could be memories while other could not. *)

39

type machine_env = {

40

is_local: string > bool;

41

get_var: string > var_decl

42

}

43


44


45

let build_env inputs locals outputs =

46

let all = List.sort_uniq VDeclModule.compare (locals @ inputs @ outputs) in

47

{ is_local = (fun id > List.exists (fun v > v.var_id = id) locals);

48

get_var = (fun id > try List.find (fun v > v.var_id = id) all with Not_found >

49

(* Format.eprintf "Impossible to find variable %s in set %a@.@?"

50

* id

51

* VSet.pp all; *)

52

raise Not_found)

53

}

54


55


56


57

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

58

(* Basic functions to translate to machine values, instructions *)

59

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

60


61

let translate_ident env id =

62

(* Format.eprintf "trnaslating ident: %s@." id; *)

63

(* id is a var that shall be visible here , ie. in vars *)

64

try

65

let var_id = env.get_var id in

66

vdecl_to_val var_id

67

with Not_found >

68


69

(* id is a constant *)

70

try

71

let vdecl = (Corelang.var_decl_of_const

72

(const_of_top (Hashtbl.find Corelang.consts_table id)))

73

in

74

vdecl_to_val vdecl

75

with Not_found >

76


77

(* id is a tag, getting its type in the list of declared enums *)

78

try

79

id_to_tag id

80

with Not_found >

81

Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;

82

assert false

83


84


85

(* specialize predefined (polymorphic) operators wrt their instances,

86

so that the C semantics is preserved *)

87

let specialize_to_c expr =

88

match expr.expr_desc with

89

 Expr_appl (id, e, r) >

90

if List.exists (fun e > Types.is_bool_type e.expr_type) (expr_list_of_expr e)

91

then let id =

92

match id with

93

 "=" > "equi"

94

 "!=" > "xor"

95

 _ > id in

96

{ expr with expr_desc = Expr_appl (id, e, r) }

97

else expr

98

 _ > expr

99


100

let specialize_op expr =

101

match !Options.output with

102

 "C" > specialize_to_c expr

103

 _ > expr

104


105

let rec translate_expr env expr =

106

let expr = specialize_op expr in

107

let translate_expr = translate_expr env in

108

let value_desc =

109

match expr.expr_desc with

110

 Expr_const v >

111

Cst v

112

 Expr_ident x >

113

(translate_ident env x).value_desc

114

 Expr_array el >

115

Array (List.map translate_expr el)

116

 Expr_access (t, i) >

117

Access (translate_expr t, translate_expr (expr_of_dimension i))

118

 Expr_power (e, n) >

119

Power (translate_expr e, translate_expr (expr_of_dimension n))

120

 Expr_when (e1, _, _) >

121

(translate_expr e1).value_desc

122

 Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr >

123

let nd = node_from_name id in

124

Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))

125

 Expr_ite (g,t,e) when Backends.is_functional () >

126

(* special treatment depending on the active backend. For

127

functional ones, like horn backend, ite are preserved in

128

expression. While they are removed for C or Java backends. *)

129

Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])

130

 _ >

131

Format.eprintf "Normalization error for backend %s: %a@."

132

!Options.output

133

Printers.pp_expr expr;

134

raise NormalizationError

135

in

136

mk_val value_desc expr.expr_type

137


138

let translate_guard env expr =

139

match expr.expr_desc with

140

 Expr_ident x > translate_ident env x

141

 _ >

142

Format.eprintf "internal error: translate_guard %a@." Printers.pp_expr expr;

143

assert false

144


145

let rec translate_act env (y, expr) =

146

let translate_act = translate_act env in

147

let translate_guard = translate_guard env in

148

(* let translate_ident = translate_ident env in *)

149

let translate_expr = translate_expr env in

150

let lustre_eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in

151

match expr.expr_desc with

152

 Expr_ite (c, t, e) >

153

let c = translate_guard c in

154

let t, spec_t = translate_act (y, t) in

155

let e, spec_e = translate_act (y, e) in

156

mk_conditional ~lustre_eq c [t] [e],

157

mk_conditional_tr c spec_t spec_e

158

 Expr_merge (x, hl) >

159

let var_x = env.get_var x in

160

let hl, spec_hl = List.(split (map (fun (t, h) >

161

let h, spec_h = translate_act (y, h) in

162

(t, [h]), (t, spec_h))

163

hl)) in

164

mk_branch' ~lustre_eq var_x hl,

165

mk_branch_tr var_x spec_hl

166

 _ >

167

let e = translate_expr expr in

168

mk_assign ~lustre_eq y e,

169

mk_assign_tr y e

170


171

let get_memory env mems eq = match eq.eq_lhs, eq.eq_rhs.expr_desc with

172

 ([x], Expr_pre _  [x], Expr_fby _) when env.is_local x >

173

let var_x = env.get_var x in

174

VSet.add var_x mems

175

 _ > mems

176


177

let get_memories env =

178

List.fold_left (get_memory env) VSet.empty

179


180

(* Datastructure updated while visiting equations *)

181

type machine_ctx = {

182

(* Reset instructions *)

183

si: instr_t list;

184

(* Instances *)

185

j: (Lustre_types.top_decl * Dimension.dim_expr list) IMap.t;

186

(* Step instructions *)

187

s: instr_t list;

188

(* Memory pack spec *)

189

mp: mc_formula_t list;

190

(* Transition spec *)

191

t: (var_decl list * var_decl list * var_decl list * mc_formula_t) list;

192

}

193


194

let ctx_init = {

195

si = [];

196

j = IMap.empty;

197

s = [];

198

mp = [];

199

t = []

200

}

201


202

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

203

(* Main function to translate equations into this machine context we

204

are building *)

205

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

206


207

let mk_control v l inst =

208

mkinstr

209

(MBranch (vdecl_to_val v, [l, [inst]]))

210


211

let control_on_clock env ck inst =

212

let rec aux (fspec, inst as acc) ck =

213

match (Clocks.repr ck).cdesc with

214

 Con (ck, cr, l) >

215

let id = Clocks.const_of_carrier cr in

216

let v = env.get_var id in

217

aux ((fun spec > Imply (Equal (Var v, Tag l), fspec spec)),

218

mk_control v l inst)

219

ck

220

 _ > acc

221

in

222

let fspec, inst = aux ((fun spec > spec), inst) ck in

223

fspec, inst

224


225

let reset_instance env i r c =

226

match r with

227

 Some r >

228

let _, inst = control_on_clock env c

229

(mk_conditional

230

(translate_guard env r)

231

[mkinstr (MSetReset i)]

232

[mkinstr (MNoReset i)]) in

233

[ inst ]

234

 None > []

235


236

let translate_eq env ctx id inputs locals outputs i eq =

237

let translate_expr = translate_expr env in

238

let translate_act = translate_act env in

239

let locals_pi = Lustre_live.inter_live_i_with id (i1) locals in

240

let outputs_pi = Lustre_live.inter_live_i_with id (i1) outputs in

241

let locals_i = Lustre_live.inter_live_i_with id i locals in

242

let outputs_i = Lustre_live.inter_live_i_with id i outputs in

243

let pred_mp ctx a =

244

And [mk_memory_pack ~i:(i1) id; a] :: ctx.mp in

245

let pred_t ctx a =

246

(inputs, locals_i, outputs_i,

247

Exists

248

(Lustre_live.existential_vars id i eq (locals @ outputs),

249

And [

250

mk_transition ~i:(i1) id

251

(vdecls_to_vals inputs)

252

(vdecls_to_vals locals_pi)

253

(vdecls_to_vals outputs_pi);

254

a

255

]))

256

:: ctx.t in

257

let control_on_clock ck inst spec_mp spec_t =

258

let fspec, inst = control_on_clock env ck inst in

259

{ ctx with

260

s = { inst with

261

instr_spec = [

262

mk_memory_pack ~i id;

263

mk_transition ~i id

264

(vdecls_to_vals inputs)

265

(vdecls_to_vals locals_i)

266

(vdecls_to_vals outputs_i)

267

] }

268

:: ctx.s;

269

mp = pred_mp ctx spec_mp;

270

t = pred_t ctx (fspec spec_t);

271

}

272

in

273

let reset_instance = reset_instance env in

274

let mkinstr' = mkinstr ~lustre_eq:eq in

275

let ctl ?(ck=eq.eq_rhs.expr_clock) instr spec_mp spec_t =

276

control_on_clock ck (mkinstr' instr) spec_mp spec_t in

277


278

(* Format.eprintf "translate_eq %a with clock %a@."

279

Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)

280

match eq.eq_lhs, eq.eq_rhs.expr_desc with

281

 [x], Expr_arrow (e1, e2) >

282

let var_x = env.get_var x in

283

let td = Arrow.arrow_top_decl () in

284

let inst = new_instance td eq.eq_rhs.expr_tag in

285

let c1 = translate_expr e1 in

286

let c2 = translate_expr e2 in

287

assert (c1.value_desc = Cst (Const_tag "true"));

288

assert (c2.value_desc = Cst (Const_tag "false"));

289

let ctx = ctl

290

(MStep ([var_x], inst, [c1; c2]))

291

(mk_memory_pack ~inst (node_name td))

292

(mk_transition ~inst (node_name td) [] [] [vdecl_to_val var_x])

293

in

294

{ ctx with

295

si = mkinstr (MSetReset inst) :: ctx.si;

296

j = IMap.add inst (td, []) ctx.j;

297

}

298


299

 [x], Expr_pre e when env.is_local x >

300

let var_x = env.get_var x in

301

let e = translate_expr e in

302

ctl

303

(MStateAssign (var_x, e))

304

(mk_state_variable_pack var_x)

305

(mk_state_assign_tr var_x e)

306


307

 [x], Expr_fby (e1, e2) when env.is_local x >

308

let var_x = env.get_var x in

309

let e2 = translate_expr e2 in

310

let ctx = ctl

311

(MStateAssign (var_x, e2))

312

(mk_state_variable_pack var_x)

313

(mk_state_assign_tr var_x e2)

314

in

315

{ ctx with

316

si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;

317

}

318


319

 p, Expr_appl (f, arg, r)

320

when not (Basic_library.is_expr_internal_fun eq.eq_rhs) >

321

let var_p = List.map (fun v > env.get_var v) p in

322

let el = expr_list_of_expr arg in

323

let vl = List.map translate_expr el in

324

let node_f = node_from_name f in

325

let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in

326

let inst = new_instance node_f eq.eq_rhs.expr_tag in

327

let env_cks = List.fold_right (fun arg cks > arg.expr_clock :: cks)

328

el [eq.eq_rhs.expr_clock] in

329

let call_ck = Clock_calculus.compute_root_clock

330

(Clock_predef.ck_tuple env_cks) in

331

let ctx = ctl

332

~ck:call_ck

333

(MStep (var_p, inst, vl))

334

(mk_memory_pack ~inst (node_name node_f))

335

(mk_transition ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))

336

in

337

(*Clocks.new_var true in

338

Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;

339

Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)

340

{ ctx with

341

si = if Stateless.check_node node_f

342

then ctx.si else mkinstr (MSetReset inst) :: ctx.si;

343

j = IMap.add inst call_f ctx.j;

344

s = (if Stateless.check_node node_f

345

then []

346

else reset_instance inst r call_ck)

347

@ ctx.s;

348

}

349


350

 [x], _ >

351

let var_x = env.get_var x in

352

let instr, spec = translate_act (var_x, eq.eq_rhs) in

353

control_on_clock eq.eq_rhs.expr_clock instr True spec

354


355

 _ >

356

Format.eprintf "internal error: Machine_code.translate_eq %a@?"

357

Printers.pp_node_eq eq;

358

assert false

359


360

let constant_equations locals =

361

List.fold_left (fun eqs vdecl >

362

if vdecl.var_dec_const

363

then

364

{ eq_lhs = [vdecl.var_id];

365

eq_rhs = desome vdecl.var_dec_value;

366

eq_loc = vdecl.var_loc

367

} :: eqs

368

else eqs)

369

[] locals

370


371

let translate_eqs env ctx id inputs locals outputs eqs =

372

List.fold_right (fun eq (ctx, i) >

373

let ctx = translate_eq env ctx id inputs locals outputs i eq in

374

ctx, i  1)

375

eqs (ctx, List.length eqs)

376

> fst

377


378


379

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

380

(* Processing nodes *)

381

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

382


383

let process_asserts nd =

384


385

let exprl = List.map (fun assert_ > assert_.assert_expr ) nd.node_asserts in

386

if Backends.is_functional () then

387

[], [], exprl

388

else (* Each assert(e) is associated to a fresh variable v and declared as

389

v=e; assert (v); *)

390

let _, vars, eql, assertl =

391

List.fold_left (fun (i, vars, eqlist, assertlist) expr >

392

let loc = expr.expr_loc in

393

let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in

394

let assert_var =

395

mkvar_decl

396

loc

397

~orig:false (* fresh var *)

398

(var_id,

399

mktyp loc Tydec_bool,

400

mkclock loc Ckdec_any,

401

false, (* not a constant *)

402

None, (* no default value *)

403

Some nd.node_id

404

)

405

in

406

assert_var.var_type < Type_predef.type_bool (* Types.new_ty (Types.Tbool) *);

407

let eq = mkeq loc ([var_id], expr) in

408

(i+1,

409

assert_var::vars,

410

eq::eqlist,

411

{expr with expr_desc = Expr_ident var_id}::assertlist)

412

) (1, [], [], []) exprl

413

in

414

vars, eql, assertl

415


416

let translate_core env nid sorted_eqs inputs locals outputs =

417

let constant_eqs = constant_equations locals in

418


419

(* Compute constants' instructions *)

420

let ctx0 = translate_eqs env ctx_init nid inputs locals outputs constant_eqs in

421

assert (ctx0.si = []);

422

assert (IMap.is_empty ctx0.j);

423


424

(* Compute ctx for all eqs *)

425

let ctx = translate_eqs env ctx_init nid inputs locals outputs sorted_eqs in

426


427

ctx, ctx0.s

428


429

let zero = mk_val (Cst (Const_int 0)) Type_predef.type_int

430


431

let memory_pack_0 nd =

432

{

433

mpname = nd;

434

mpindex = Some 0;

435

mpformula = And [StateVarPack ResetFlag; Equal (Memory ResetFlag, Val zero)]

436

}

437


438

let memory_pack_toplevel nd i =

439

{

440

mpname = nd;

441

mpindex = None;

442

mpformula = Ternary (Memory ResetFlag,

443

StateVarPack ResetFlag,

444

mk_memory_pack ~i nd.node_id)

445

}

446


447

let transition_0 nd =

448

{

449

tname = nd;

450

tindex = Some 0;

451

tinputs = nd.node_inputs;

452

tlocals = [];

453

toutputs = [];

454

tformula = True;

455

}

456


457

let transition_toplevel nd i =

458

{

459

tname = nd;

460

tindex = None;

461

tinputs = nd.node_inputs;

462

tlocals = [];

463

toutputs = nd.node_outputs;

464

tformula = ExistsMem (Predicate (ResetCleared nd.node_id),

465

mk_transition nd.node_id ~i

466

(vdecls_to_vals (nd.node_inputs))

467

[]

468

(vdecls_to_vals nd.node_outputs));

469

}

470


471

let translate_decl nd sch =

472

(* Format.eprintf "Translating node %s@." nd.node_id; *)

473

(* Extracting eqs, variables .. *)

474

let eqs, auts = get_node_eqs nd in

475

assert (auts = []); (* Automata should be expanded by now *)

476


477

(* In case of non functional backend (eg. C), additional local variables have

478

to be declared for each assert *)

479

let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in

480


481

(* Build the env: variables visible in the current scope *)

482

let locals = nd.node_locals @ new_locals in

483

(* let locals = VSet.of_list locals_list in *)

484

(* let inout_vars = nd.node_inputs @ nd.node_outputs in *)

485

let env = build_env nd.node_inputs locals nd.node_outputs in

486


487

(* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)

488


489

(* Computing main content *)

490

(* Format.eprintf "ok1@.@?"; *)

491

let schedule = sch.Scheduling_type.schedule in

492

(* Format.eprintf "ok2@.@?"; *)

493

let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in

494

(* Format.eprintf "ok3@.locals=%a@.inout:%a@?"

495

* VSet.pp locals

496

* VSet.pp inout_vars

497

* ; *)

498


499

let equations = assert_instrs @ sorted_eqs in

500

let mems = get_memories env equations in

501

(* Removing computed memories from locals. We also removed unused variables. *)

502

let locals = List.filter

503

(fun v > not (VSet.mem v mems) && not (List.mem v.var_id unused)) locals in

504

(* Compute live sets for spec *)

505

Lustre_live.set_live_of nd.node_id nd.node_outputs locals equations;

506


507

(* Translate equations *)

508

let ctx, ctx0_s = translate_core env nd.node_id equations

509

nd.node_inputs locals nd.node_outputs in

510


511

(* Format.eprintf "ok4@.@?"; *)

512


513

(* Build the machine *)

514

let mmap = IMap.bindings ctx.j in

515

let mmemory_packs =

516

memory_pack_0 nd

517

:: List.mapi (fun i f >

518

{

519

mpname = nd;

520

mpindex = Some (i + 1);

521

mpformula = red f

522

}) ctx.mp

523

@ [memory_pack_toplevel nd (List.length ctx.mp)]

524

in

525

let mtransitions =

526

transition_0 nd

527

:: List.mapi (fun i (tinputs, tlocals, toutputs, f) >

528

{

529

tname = nd;

530

tindex = Some (i + 1);

531

tinputs;

532

tlocals;

533

toutputs;

534

tformula = red f;

535

}) ctx.t

536

@ [transition_toplevel nd (List.length ctx.t)]

537

in

538

let clear_reset = mkinstr ~instr_spec:[

539

mk_memory_pack ~i:0 nd.node_id;

540

mk_transition ~i:0 nd.node_id

541

(vdecls_to_vals nd.node_inputs)

542

[]

543

[]] MClearReset in

544

{

545

mname = nd;

546

mmemory = VSet.elements mems;

547

mcalls = mmap;

548

minstances = List.filter (fun (_, (n,_)) > not (Stateless.check_node n)) mmap;

549

minit = ctx.si;

550

mconst = ctx0_s;

551

mstatic = List.filter (fun v > v.var_dec_const) nd.node_inputs;

552

mstep = {

553

step_inputs = nd.node_inputs;

554

step_outputs = nd.node_outputs;

555

step_locals = locals;

556

step_checks = List.map (fun d > d.Dimension.dim_loc,

557

translate_expr env

558

(expr_of_dimension d))

559

nd.node_checks;

560

step_instrs = clear_reset ::

561

(* special treatment depending on the active backend. For horn backend,

562

common branches are not merged while they are in C or Java

563

backends. *)

564

(if !Backends.join_guards then

565

join_guards_list ctx.s

566

else

567

ctx.s);

568

step_asserts = List.map (translate_expr env) nd_node_asserts;

569

};

570


571

(* Processing spec: there is no processing performed here. Contract

572

have been processed already. Either one of the other machine is a

573

cocospec node, or the current one is a cocospec node. Contract do

574

not contain any statement or import. *)

575


576

mspec = { mnode_spec = nd.node_spec; mtransitions; mmemory_packs };

577

mannot = nd.node_annot;

578

msch = Some sch;

579

}

580


581

(** takes the global declarations and the scheduling associated to each node *)

582

let translate_prog decls node_schs =

583

let nodes = get_nodes decls in

584

let machines =

585

List.map

586

(fun decl >

587

let node = node_of_top decl in

588

let sch = IMap.find node.node_id node_schs in

589

translate_decl node sch

590

) nodes

591

in

592

machines

593


594

(* Local Variables: *)

595

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

596

(* End: *)
