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 constant in

27

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

28


29

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

30

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

31

(* si : initialization instructions *)

32

(* j : node aka machine instances *)

33

(* d : local variables *)

34

(* s : step instructions *)

35


36

(* Machine processing requires knowledge about variables and local variables.

37

Local could be memories while other could not. *)

38

type machine_env = { is_local : string > bool; get_var : string > var_decl }

39


40

let build_env inputs locals outputs =

41

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

42

{

43

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

44

get_var =

45

(fun id >

46

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

47

with Not_found >

48

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

49

* VSet.pp all; *)

50

raise Not_found);

51

}

52


53

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

54

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

55

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

56


57

let translate_ident env id =

58

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

59

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

60

try

61

let var_id = env.get_var id in

62

vdecl_to_val var_id

63

with Not_found > (

64

(* id is a constant *)

65

try

66

let vdecl =

67

Corelang.var_decl_of_const

68

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

69

in

70

vdecl_to_val vdecl

71

with Not_found > (

72

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

73

try id_to_tag id

74

with Not_found >

75

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

76

assert false))

77


78

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

79

the C semantics is preserved *)

80

let specialize_to_c expr =

81

match expr.expr_desc with

82

 Expr_appl (id, e, r) >

83

if

84

List.exists

85

(fun e > Types.is_bool_type e.expr_type)

86

(expr_list_of_expr e)

87

then

88

let id = match id with "=" > "equi"  "!=" > "xor"  _ > id in

89

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

90

else expr

91

 _ >

92

expr

93


94

let specialize_op expr =

95

match !Options.output with "C" > specialize_to_c expr  _ > expr

96


97

let rec translate_expr env expr =

98

let expr = specialize_op expr in

99

let translate_expr = translate_expr env in

100

let value_desc =

101

match expr.expr_desc with

102

 Expr_const v >

103

Cst v

104

 Expr_ident x >

105

(translate_ident env x).value_desc

106

 Expr_array el >

107

Array (List.map translate_expr el)

108

 Expr_access (t, i) >

109

Access (translate_expr t, translate_expr (expr_of_dimension i))

110

 Expr_power (e, n) >

111

Power (translate_expr e, translate_expr (expr_of_dimension n))

112

 Expr_when (e1, _, _) >

113

(translate_expr e1).value_desc

114

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

115

let nd = node_from_name id in

116

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

117

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

118

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

119

like horn backend, ite are preserved in expression. While they are

120

removed for C or Java backends. *)

121

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

122

 _ >

123

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

124

Printers.pp_expr expr;

125

raise NormalizationError

126

in

127

mk_val value_desc expr.expr_type

128


129

let translate_guard env expr =

130

match expr.expr_desc with

131

 Expr_ident x >

132

translate_ident env x

133

 _ >

134

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

135

assert false

136


137

let rec translate_act env (y, expr) =

138

let translate_act = translate_act env in

139

let translate_guard = translate_guard env in

140

let translate_expr = translate_expr env in

141

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

142

match expr.expr_desc with

143

 Expr_ite (c, t, e) >

144

let c = translate_guard c in

145

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

146

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

147

mk_conditional ~lustre_eq c [ t ] [ e ], mk_conditional_tr c spec_t spec_e

148

 Expr_merge (x, hl) >

149

let var_x = env.get_var x in

150

let hl, spec_hl =

151

List.(

152

split

153

(map

154

(fun (t, h) >

155

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

156

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

157

hl))

158

in

159

mk_branch' ~lustre_eq var_x hl, mk_branch_tr var_x spec_hl

160

 _ >

161

let e = translate_expr expr in

162

mk_assign ~lustre_eq y e, mk_assign_tr y e

163


164

let get_memory env mems eq =

165

match eq.eq_lhs, eq.eq_rhs.expr_desc with

166

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

167

let var_x = env.get_var x in

168

VSet.add var_x mems

169

 _ >

170

mems

171


172

let get_memories env = List.fold_left (get_memory env) VSet.empty

173


174

(* Datastructure updated while visiting equations *)

175

type machine_ctx = {

176

(* memories *)

177

m : ISet.t;

178

(* Reset instructions *)

179

si : instr_t list;

180

(* Instances *)

181

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

182

(* Step instructions *)

183

s : instr_t list;

184

(* Memory pack spec *)

185

mp : mc_formula_t list;

186

(* Transition spec *)

187

t :

188

(var_decl list

189

(* inputs *)

190

* var_decl list

191

(* locals *)

192

* var_decl list

193

(* outputs *)

194

* ISet.t (* memory footprint *)

195

* ident IMap.t

196

(* memory instances footprint *)

197

* mc_formula_t)

198

(* formula *)

199

list;

200

}

201


202

let ctx_init =

203

{ m = ISet.empty; si = []; j = IMap.empty; s = []; mp = []; t = [] }

204


205

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

206

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

207

building *)

208

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

209


210

let mk_control v l inst = mkinstr (MBranch (vdecl_to_val v, [ l, [ inst ] ]))

211


212

let control_on_clock env ck inst =

213

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

214

match (Clocks.repr ck).cdesc with

215

 Con (ck, cr, l) >

216

let id = Clocks.const_of_carrier cr in

217

let v = env.get_var id in

218

aux

219

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

220

mk_control v l inst )

221

ck

222

 _ >

223

acc

224

in

225

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

226

fspec, inst

227


228

let reset_instance env i r c =

229

match r with

230

 Some r >

231

let r = translate_guard env r in

232

let _, inst =

233

control_on_clock env c

234

(mk_conditional r [ mkinstr (MSetReset i) ] [ mkinstr (MNoReset i) ])

235

in

236

Some r, [ inst ]

237

 None >

238

None, []

239


240

let translate_eq env ctx nd inputs locals outputs i eq =

241

let id = nd.node_id in

242

let translate_expr = translate_expr env in

243

let translate_act = translate_act env in

244

let locals_pi = Lustre_live.inter_live_i_with id (i  1) locals in

245

let outputs_pi = Lustre_live.inter_live_i_with id (i  1) outputs in

246

let locals_i = Lustre_live.inter_live_i_with id i locals in

247

let outputs_i = Lustre_live.inter_live_i_with id i outputs in

248

let pred_mp ctx a = And [ mk_memory_pack ~i:(i  1) id; a ] :: ctx.mp in

249

let pred_t ctx a =

250

( inputs,

251

locals_i,

252

outputs_i,

253

ctx.m,

254

IMap.map (fun (td, _) > node_name td) ctx.j,

255

Exists

256

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

257

And

258

[

259

mk_transition ~i:(i  1) id (vdecls_to_vals inputs)

260

(vdecls_to_vals locals_pi)

261

(vdecls_to_vals outputs_pi);

262

a;

263

] ) )

264

:: ctx.t

265

in

266

let control_on_clock ck inst spec_mp spec_t ctx =

267

let fspec, inst = control_on_clock env ck inst in

268

{

269

ctx with

270

s =

271

{

272

inst with

273

instr_spec =

274

(if fst (get_stateless_status_node nd) then []

275

else [ mk_memory_pack ~i id ])

276

@ [

277

mk_transition ~i id (vdecls_to_vals inputs)

278

(vdecls_to_vals locals_i) (vdecls_to_vals outputs_i);

279

];

280

}

281

:: ctx.s;

282

mp = pred_mp ctx spec_mp;

283

t = pred_t ctx (fspec spec_t);

284

}

285

in

286

let reset_instance = reset_instance env in

287

let mkinstr' = mkinstr ~lustre_eq:eq in

288

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

289

control_on_clock ck (mkinstr' instr)

290

in

291


292

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

293

Clocks.print_ck eq.eq_rhs.expr_clock; *)

294

match eq.eq_lhs, eq.eq_rhs.expr_desc with

295

 [ x ], Expr_arrow (e1, e2) >

296

let var_x = env.get_var x in

297

let td = Arrow.arrow_top_decl () in

298

let inst = new_instance td eq.eq_rhs.expr_tag in

299

let c1 = translate_expr e1 in

300

let c2 = translate_expr e2 in

301

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

302

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

303

let ctx =

304

ctl

305

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

306

(mk_memory_pack ~inst (node_name td))

307

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

308

{ ctx with j = IMap.add inst (td, []) ctx.j }

309

in

310

{ ctx with si = mkinstr (MSetReset inst) :: ctx.si }

311

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

312

let var_x = env.get_var x in

313

let e = translate_expr e in

314

ctl

315

(MStateAssign (var_x, e))

316

(mk_state_variable_pack var_x)

317

(mk_state_assign_tr var_x e)

318

{ ctx with m = ISet.add x ctx.m }

319

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

320

let var_x = env.get_var x in

321

let e2 = translate_expr e2 in

322

let ctx =

323

ctl

324

(MStateAssign (var_x, e2))

325

(mk_state_variable_pack var_x)

326

(mk_state_assign_tr var_x e2)

327

{ ctx with m = ISet.add x ctx.m }

328

in

329

{

330

ctx with

331

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

332

}

333

 p, Expr_appl (f, arg, r)

334

when not (Basic_library.is_expr_internal_fun eq.eq_rhs) >

335

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

336

let el = expr_list_of_expr arg in

337

let vl = List.map translate_expr el in

338

let node_f = node_from_name f in

339

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

340

let inst = new_instance node_f eq.eq_rhs.expr_tag in

341

let env_cks =

342

List.fold_right

343

(fun arg cks > arg.expr_clock :: cks)

344

el [ eq.eq_rhs.expr_clock ]

345

in

346

let call_ck =

347

Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks)

348

in

349

let r, reset_inst = reset_instance inst r call_ck in

350

let ctx =

351

ctl ~ck:call_ck

352

(MStep (var_p, inst, vl))

353

(mk_memory_pack ~inst (node_name node_f))

354

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

355

{

356

ctx with

357

j = IMap.add inst call_f ctx.j;

358

s = (if Stateless.check_node node_f then [] else reset_inst) @ ctx.s;

359

}

360

in

361

(*Clocks.new_var true in Clock_calculus.unify_imported_clock (Some call_ck)

362

eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; Format.eprintf "call %a: %a:

363

%a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple

364

env_cks) Clocks.print_ck call_ck;*)

365

{

366

ctx with

367

si =

368

(if Stateless.check_node node_f then ctx.si

369

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

370

}

371

 [ x ], _ >

372

let var_x = env.get_var x in

373

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

374

control_on_clock eq.eq_rhs.expr_clock instr True spec ctx

375

 _ >

376

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

377

Printers.pp_node_eq eq;

378

assert false

379


380

let constant_equations locals =

381

List.fold_left

382

(fun eqs vdecl >

383

if vdecl.var_dec_const then

384

{

385

eq_lhs = [ vdecl.var_id ];

386

eq_rhs = desome vdecl.var_dec_value;

387

eq_loc = vdecl.var_loc;

388

}

389

:: eqs

390

else eqs)

391

[] locals

392


393

let translate_eqs env ctx nd inputs locals outputs eqs =

394

List.fold_left

395

(fun (ctx, i) eq >

396

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

397

ctx, i + 1)

398

(ctx, 1) eqs

399

> fst

400


401

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

402

(* Processing nodes *)

403

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

404


405

let process_asserts nd =

406

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

407

if Backends.is_functional () then [], [], exprl

408

else

409

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

410

assert (v); *)

411

let _, vars, eql, assertl =

412

List.fold_left

413

(fun (i, vars, eqlist, assertlist) expr >

414

let loc = expr.expr_loc in

415

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

416

let assert_var =

417

mkvar_decl loc ~orig:false

418

(* fresh var *)

419

( var_id,

420

mktyp loc Tydec_bool,

421

mkclock loc Ckdec_any,

422

false,

423

(* not a constant *)

424

None,

425

(* no default value *)

426

Some nd.node_id )

427

in

428

assert_var.var_type < Type_predef.type_bool

429

(* Types.new_ty (Types.Tbool) *);

430

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

431

( i + 1,

432

assert_var :: vars,

433

eq :: eqlist,

434

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

435

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

436

in

437

vars, eql, assertl

438


439

let translate_core env nd sorted_eqs inputs locals outputs =

440

let constant_eqs = constant_equations locals in

441


442

(* Compute constants' instructions *)

443

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

444

assert (ctx0.si = []);

445

assert (IMap.is_empty ctx0.j);

446


447

(* Compute ctx for all eqs *)

448

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

449


450

ctx, ctx0.s

451


452

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

453


454

let memory_pack_0 nd =

455

{

456

mpname = nd;

457

mpindex = Some 0;

458

mpformula =

459

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

460

}

461


462

let memory_pack_toplevel nd i =

463

{

464

mpname = nd;

465

mpindex = None;

466

mpformula =

467

Ternary

468

(Memory ResetFlag, StateVarPack ResetFlag, mk_memory_pack ~i nd.node_id);

469

}

470


471

let transition_0 nd =

472

{

473

tname = nd;

474

tindex = Some 0;

475

tinputs = nd.node_inputs;

476

tlocals = [];

477

toutputs = [];

478

tformula = True;

479

tmem_footprint = ISet.empty;

480

tinst_footprint = IMap.empty;

481

}

482


483

let transition_toplevel nd i =

484

let tr =

485

mk_transition nd.node_id ~i

486

(vdecls_to_vals nd.node_inputs)

487

[]

488

(vdecls_to_vals nd.node_outputs)

489

in

490

{

491

tname = nd;

492

tindex = None;

493

tinputs = nd.node_inputs;

494

tlocals = [];

495

toutputs = nd.node_outputs;

496

tformula =

497

(if fst (get_stateless_status_node nd) then tr

498

else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));

499

tmem_footprint = ISet.empty;

500

tinst_footprint = IMap.empty;

501

}

502


503

let translate_decl nd sch =

504

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

505

(* Extracting eqs, variables .. *)

506

let eqs, auts = get_node_eqs nd in

507

assert (auts = []);

508


509

(* Automata should be expanded by now *)

510


511

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

512

to be declared for each assert *)

513

let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in

514


515

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

516

let locals = nd.node_locals @ new_locals in

517

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

518

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

519

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

520


521

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

522


523

(* Computing main content *)

524

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

525

let schedule = sch.Scheduling_type.schedule in

526

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

527

let sorted_eqs, unused =

528

Scheduling.sort_equations_from_schedule eqs schedule

529

in

530


531

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

532

* VSet.pp locals

533

* VSet.pp inout_vars

534

* ; *)

535

let equations = assert_instrs @ sorted_eqs in

536

let mems = get_memories env equations in

537

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

538

let locals =

539

List.filter

540

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

541

locals

542

in

543

(* Compute live sets for spec *)

544

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

545


546

(* Translate equations *)

547

let ctx, ctx0_s =

548

translate_core env nd equations nd.node_inputs locals nd.node_outputs

549

in

550


551

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

552


553

(* Build the machine *)

554

let mmap = IMap.bindings ctx.j in

555

let mmemory_packs =

556

memory_pack_0 nd

557

::

558

List.mapi

559

(fun i f > { mpname = nd; mpindex = Some (i + 1); mpformula = red f })

560

(List.rev ctx.mp)

561

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

562

in

563

let mtransitions =

564

transition_0 nd

565

::

566

List.mapi

567

(fun i (tinputs, tlocals, toutputs, tmem_footprint, tinst_footprint, f) >

568

{

569

tname = nd;

570

tindex = Some (i + 1);

571

tinputs;

572

tlocals;

573

toutputs;

574

tformula = red f;

575

tmem_footprint;

576

tinst_footprint;

577

})

578

(List.rev ctx.t)

579

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

580

in

581

let clear_reset =

582

mkinstr

583

~instr_spec:

584

((if fst (get_stateless_status_node nd) then []

585

else [ mk_memory_pack ~i:0 nd.node_id ])

586

@ [

587

mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] [];

588

])

589

MClearReset

590

in

591

{

592

mname = nd;

593

mmemory = VSet.elements mems;

594

mcalls = mmap;

595

minstances =

596

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

597

minit = List.rev ctx.si;

598

mconst = List.rev ctx0_s;

599

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

600

mstep =

601

{

602

step_inputs = nd.node_inputs;

603

step_outputs = nd.node_outputs;

604

step_locals = locals;

605

step_checks =

606

List.map

607

(fun d >

608

d.Dimension.dim_loc, translate_expr env (expr_of_dimension d))

609

nd.node_checks;

610

step_instrs =

611

clear_reset

612

::

613

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

614

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

615

backends. *)

616

(if !Backends.join_guards then join_guards_list (List.rev ctx.s)

617

else List.rev ctx.s);

618

step_asserts = List.map (translate_expr env) nd_node_asserts;

619

};

620

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

621

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

622

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

623

statement or import. *)

624

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

625

mannot = nd.node_annot;

626

msch = Some sch;

627

}

628


629

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

630

let translate_prog decls node_schs =

631

let nodes = get_nodes decls in

632

let machines =

633

List.map

634

(fun decl >

635

let node = node_of_top decl in

636

let sch = IMap.find node.node_id node_schs in

637

translate_decl node sch)

638

nodes

639

in

640

machines

641


642

(* Local Variables: *)

643

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

644

(* End: *)
