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 locals non_locals =

46

let all = VSet.union locals non_locals in

47

{

48

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

49

get_var = (fun id > try VSet.get id all with Not_found >

50

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

51

* id

52

* VSet.pp all; *)

53

raise Not_found)

54

}

55


56


57


58

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

59

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

60

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

61


62

let translate_ident env id =

63

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

64

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

65

try

66

let var_id = env.get_var id in

67

mk_val (Var var_id) var_id.var_type

68

with Not_found >

69


70

(* id is a constant *)

71

try

72

let vdecl = (Corelang.var_decl_of_const

73

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

74

in

75

mk_val (Var vdecl) vdecl.var_type

76

with Not_found >

77


78

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

79

try

80

let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in

81

mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)

82

with Not_found >

83

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

84

assert false

85


86


87

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

88

so that the C semantics is preserved *)

89

let specialize_to_c expr =

90

match expr.expr_desc with

91

 Expr_appl (id, e, r) >

92

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

93

then let id =

94

match id with

95

 "=" > "equi"

96

 "!=" > "xor"

97

 _ > id in

98

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

99

else expr

100

 _ > expr

101


102

let specialize_op expr =

103

match !Options.output with

104

 "C" > specialize_to_c expr

105

 _ > expr

106


107

let rec translate_expr env expr =

108

let expr = specialize_op expr in

109

let translate_expr = translate_expr env in

110

let value_desc =

111

match expr.expr_desc with

112

 Expr_const v >

113

Cst v

114

 Expr_ident x >

115

(translate_ident env x).value_desc

116

 Expr_array el >

117

Array (List.map translate_expr el)

118

 Expr_access (t, i) >

119

Access (translate_expr t, translate_expr (expr_of_dimension i))

120

 Expr_power (e, n) >

121

Power (translate_expr e, translate_expr (expr_of_dimension n))

122

 Expr_when (e1, _, _) >

123

(translate_expr e1).value_desc

124

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

125

let nd = node_from_name id in

126

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

127

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

128

(* special treatment depending on the active backend. For

129

functional ones, like horn backend, ite are preserved in

130

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

131

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

132

 _ >

133

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

134

!Options.output

135

Printers.pp_expr expr;

136

raise NormalizationError

137

in

138

mk_val value_desc expr.expr_type

139


140

let translate_guard env expr =

141

match expr.expr_desc with

142

 Expr_ident x > translate_ident env x

143

 _ >

144

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

145

assert false

146


147

let rec translate_act env (y, expr) =

148

let translate_act = translate_act env in

149

let translate_guard = translate_guard env in

150

let translate_ident = translate_ident env in

151

let translate_expr = translate_expr env in

152

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

153

match expr.expr_desc with

154

 Expr_ite (c, t, e) >

155

mk_conditional ~lustre_eq

156

(translate_guard c)

157

[translate_act (y, t)]

158

[translate_act (y, e)]

159

 Expr_merge (x, hl) >

160

mk_branch ~lustre_eq

161

(translate_ident x)

162

(List.map (fun (t, h) > t, [translate_act (y, h)]) hl)

163

 _ >

164

mk_assign ~lustre_eq y (translate_expr expr)

165


166

(* Datastructure updated while visiting equations *)

167

type machine_ctx = {

168

(* machine name *)

169

id: ident;

170

(* Memories *)

171

m: VSet.t;

172

(* Reset instructions *)

173

si: instr_t list;

174

(* Instances *)

175

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

176

(* Step instructions *)

177

s: instr_t list;

178

(* Memory pack spec *)

179

mp: mc_formula_t list;

180

(* Clocked spec *)

181

c: mc_formula_t IMap.t;

182

(* Transition spec *)

183

t: mc_formula_t list;

184

}

185


186

let ctx_init id = {

187

id;

188

m = VSet.empty;

189

si = [];

190

j = IMap.empty;

191

s = [];

192

mp = [];

193

c = IMap.empty;

194

t = []

195

}

196


197

let ctx_dummy = ctx_init ""

198


199

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

200

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

201

are building *)

202

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

203


204

let mk_control v l inst =

205

mkinstr

206

True

207

(* (Imply (mk_clocked_on id vs, inst.instr_spec)) *)

208

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

209


210

let control_on_clock env ctx ck spec inst =

211

let rec aux (ck_ids, vs, ctx, spec, inst as acc) ck =

212

match (Clocks.repr ck).cdesc with

213

 Con (ck, cr, l) >

214

let id = Clocks.const_of_carrier cr in

215

let v = translate_ident env id in

216

let ck_ids' = String.concat "_" ck_ids in

217

let id' = id ^ "_" ^ ck_ids' in

218

let ck_spec = mk_condition v l in

219

aux (id :: ck_ids,

220

v :: vs,

221

{ ctx with

222

c = IMap.add id ck_spec

223

(IMap.add id' (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)

224

},

225

Imply (mk_clocked_on id' (v :: vs), spec),

226

mk_control v l inst) ck

227

 _ > acc

228

in

229

let _, _, ctx, spec, inst = aux ([], [], ctx, spec, inst) ck in

230

ctx, spec, inst

231


232

let reset_instance env i r c =

233

match r with

234

 Some r >

235

let _, _, inst = control_on_clock env ctx_dummy c True

236

(mk_conditional

237

(translate_guard env r)

238

[mkinstr True (MReset i)]

239

[mkinstr True (MNoReset i)]) in

240

[ inst ]

241

 None > []

242


243


244

let translate_eq env ctx i eq =

245

let translate_expr = translate_expr env in

246

let translate_act = translate_act env in

247

let control_on_clock ck spec inst =

248

let ctx, _spec, inst = control_on_clock env ctx ck spec inst in

249

{ ctx with

250

s = { inst with

251

instr_spec = mk_transition ~i ctx.id [] } :: ctx.s }

252

in

253

let reset_instance = reset_instance env in

254

let mkinstr' = mkinstr ~lustre_eq:eq True in

255

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

256

control_on_clock ck spec (mkinstr' instr) in

257


258

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

259

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

260

match eq.eq_lhs, eq.eq_rhs.expr_desc with

261

 [x], Expr_arrow (e1, e2) >

262

let var_x = env.get_var x in

263

let td = Arrow.arrow_top_decl () in

264

let o = new_instance td eq.eq_rhs.expr_tag in

265

let c1 = translate_expr e1 in

266

let c2 = translate_expr e2 in

267

let ctx = ctl

268

(mk_transition (node_name td) [])

269

(MStep ([var_x], o, [c1;c2])) in

270

{ ctx with

271

si = mkinstr True (MReset o) :: ctx.si;

272

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

273

}

274


275

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

276

let var_x = env.get_var x in

277

let ctx = ctl

278

True

279

(MStateAssign (var_x, translate_expr e1)) in

280

{ ctx with

281

m = VSet.add var_x ctx.m;

282

}

283


284

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

285

let var_x = env.get_var x in

286

let ctx = ctl

287

True

288

(MStateAssign (var_x, translate_expr e2)) in

289

{ ctx with

290

m = VSet.add var_x ctx.m;

291

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

292

}

293


294

 p, Expr_appl (f, arg, r)

295

when not (Basic_library.is_expr_internal_fun eq.eq_rhs) >

296

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

297

let el = expr_list_of_expr arg in

298

let vl = List.map translate_expr el in

299

let node_f = node_from_name f in

300

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

301

let o = new_instance node_f eq.eq_rhs.expr_tag in

302

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

303

el [eq.eq_rhs.expr_clock] in

304

let call_ck = Clock_calculus.compute_root_clock

305

(Clock_predef.ck_tuple env_cks) in

306

let ctx = ctl

307

~ck:call_ck

308

True

309

(MStep (var_p, o, vl)) in

310

(*Clocks.new_var true in

311

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

312

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

313

{ ctx with

314

si = if Stateless.check_node node_f

315

then ctx.si else mkinstr True (MReset o) :: ctx.si;

316

j = IMap.add o call_f ctx.j;

317

s = (if Stateless.check_node node_f

318

then []

319

else reset_instance o r call_ck)

320

@ ctx.s

321

}

322


323

 [x], _ >

324

let var_x = env.get_var x in

325

control_on_clock eq.eq_rhs.expr_clock True (translate_act (var_x, eq.eq_rhs))

326


327

 _ >

328

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

329

Printers.pp_node_eq eq;

330

assert false

331


332

let constant_equations locals =

333

VSet.fold (fun vdecl eqs >

334

if vdecl.var_dec_const

335

then

336

{ eq_lhs = [vdecl.var_id];

337

eq_rhs = desome vdecl.var_dec_value;

338

eq_loc = vdecl.var_loc

339

} :: eqs

340

else eqs)

341

locals []

342


343

let translate_eqs env ctx eqs =

344

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

345

let ctx = translate_eq env ctx i eq in

346

ctx, i  1)

347

eqs (ctx, List.length eqs)

348

> fst

349


350


351

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

352

(* Processing nodes *)

353

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

354


355

let process_asserts nd =

356


357

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

358

if Backends.is_functional () then

359

[], [], exprl

360

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

361

v=e; assert (v); *)

362

let _, vars, eql, assertl =

363

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

364

let loc = expr.expr_loc in

365

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

366

let assert_var =

367

mkvar_decl

368

loc

369

~orig:false (* fresh var *)

370

(var_id,

371

mktyp loc Tydec_bool,

372

mkclock loc Ckdec_any,

373

false, (* not a constant *)

374

None, (* no default value *)

375

Some nd.node_id

376

)

377

in

378

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

379

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

380

(i+1,

381

assert_var::vars,

382

eq::eqlist,

383

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

384

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

385

in

386

vars, eql, assertl

387


388

let translate_core nid sorted_eqs locals other_vars =

389

let constant_eqs = constant_equations locals in

390


391

let env = build_env locals other_vars in

392


393

(* Compute constants' instructions *)

394

let ctx0 = translate_eqs env (ctx_init nid) constant_eqs in

395

assert (VSet.is_empty ctx0.m);

396

assert (ctx0.si = []);

397

assert (IMap.is_empty ctx0.j);

398


399

(* Compute ctx for all eqs *)

400

let ctx = translate_eqs env (ctx_init nid) sorted_eqs in

401


402

ctx, ctx0.s

403


404


405

let translate_decl nd sch =

406

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

407

(* Extracting eqs, variables .. *)

408

let eqs, auts = get_node_eqs nd in

409

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

410


411

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

412

to be declared for each assert *)

413

let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in

414


415

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

416

let locals_list = nd.node_locals @ new_locals in

417

let locals = VSet.of_list locals_list in

418

let inout_vars = (VSet.of_list (nd.node_inputs @ nd.node_outputs)) in

419

let env = build_env locals inout_vars in

420


421

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

422


423

(* Computing main content *)

424

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

425

let schedule = sch.Scheduling_type.schedule in

426

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

427

let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in

428

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

429

* VSet.pp locals

430

* VSet.pp inout_vars

431

* ; *)

432


433

let ctx, ctx0_s = translate_core

434

nd.node_id (assert_instrs@sorted_eqs) locals inout_vars in

435


436

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

437


438

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

439

let updated_locals =

440

let l = VSet.elements (VSet.diff locals ctx.m) in

441

List.fold_left (fun res v > if List.mem v.var_id unused then res else v::res) [] l

442

in

443

let mmap = IMap.bindings ctx.j in

444

{

445

mname = nd;

446

mmemory = VSet.elements ctx.m;

447

mcalls = mmap;

448

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

449

minit = ctx.si;

450

mconst = ctx0_s;

451

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

452

mstep = {

453

step_inputs = nd.node_inputs;

454

step_outputs = nd.node_outputs;

455

step_locals = updated_locals;

456

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

457

translate_expr env

458

(expr_of_dimension d))

459

nd.node_checks;

460

step_instrs = (

461

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

462

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

463

backends. *)

464

if !Backends.join_guards then

465

join_guards_list ctx.s

466

else

467

ctx.s

468

);

469

step_asserts = List.map (translate_expr env) nd_node_asserts;

470

};

471


472

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

473

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

474

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

475

not contain any statement or import. *)

476


477

mspec = { mnode_spec = nd.node_spec; mtransitions = [] };

478

mannot = nd.node_annot;

479

msch = Some sch;

480

}

481


482

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

483

let translate_prog decls node_schs =

484

let nodes = get_nodes decls in

485

let machines =

486

List.map

487

(fun decl >

488

let node = node_of_top decl in

489

let sch = IMap.find node.node_id node_schs in

490

translate_decl node sch

491

) nodes

492

in

493

machines

494


495

(* Local Variables: *)

496

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

497

(* End: *)
