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

(* Memories *)

169

m: VSet.t;

170

(* Reset instructions *)

171

si: instr_t list;

172

(* Instances *)

173

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

174

(* Step instructions *)

175

s: instr_t list;

176

(* Memory pack spec *)

177

mp: mc_formula_t list;

178

(* Clocked spec *)

179

c: mc_formula_t IMap.t;

180

(* Transition spec *)

181

t: mc_formula_t list;

182

}

183


184

let ctx_init = {

185

m = VSet.empty;

186

si = [];

187

j = IMap.empty;

188

s = [];

189

mp = [];

190

c = IMap.empty;

191

t = []

192

}

193


194

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

195

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

196

are building *)

197

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

198


199

let mk_control id vs v l inst =

200

mkinstr

201

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

202

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

203


204

let control_on_clock env ctx ck inst =

205

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

206

match (Clocks.repr ck).cdesc with

207

 Con (ck, cr, l) >

208

let id = Clocks.const_of_carrier cr in

209

let v = translate_ident env id in

210

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

211

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

212

let ck_spec = mk_condition v l in

213

aux (id :: ck_ids,

214

v :: vs,

215

{ ctx

216

with c = IMap.add id ck_spec

217

(IMap.add id'

218

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

219

},

220

mk_control id' (v :: vs) v l inst) ck

221

 _ > acc

222

in

223

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

224

ctx, inst

225


226

let reset_instance env i r c =

227

match r with

228

 Some r >

229

[snd (control_on_clock env ctx_init c

230

(mk_conditional

231

(translate_guard env r)

232

[mkinstr True (MReset i)]

233

[mkinstr True (MNoReset i)]))]

234

 None > []

235


236


237

let translate_eq env ctx eq =

238

let translate_expr = translate_expr env in

239

let translate_act = translate_act env in

240

let control_on_clock ck inst =

241

let ctx, ins = control_on_clock env ctx ck inst in

242

{ ctx with s = ins :: ctx.s }

243

in

244

let reset_instance = reset_instance env in

245

let mkinstr' = mkinstr ~lustre_eq:eq True in

246

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

247

control_on_clock ck (mkinstr' instr) in

248


249

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

250

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

251

match eq.eq_lhs, eq.eq_rhs.expr_desc with

252

 [x], Expr_arrow (e1, e2) >

253

let var_x = env.get_var x in

254

let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in

255

let c1 = translate_expr e1 in

256

let c2 = translate_expr e2 in

257

let ctx = ctl (MStep ([var_x], o, [c1;c2])) in

258

{ ctx with

259

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

260

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

261

}

262

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

263

let var_x = env.get_var x in

264

let ctx = ctl (MStateAssign (var_x, translate_expr e1)) in

265

{ ctx with

266

m = VSet.add var_x ctx.m;

267

}

268

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

269

let var_x = env.get_var x in

270

let ctx = ctl (MStateAssign (var_x, translate_expr e2)) in

271

{ ctx with

272

m = VSet.add var_x ctx.m;

273

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

274

}

275

 p, Expr_appl (f, arg, r)

276

when not (Basic_library.is_expr_internal_fun eq.eq_rhs) >

277

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

278

let el = expr_list_of_expr arg in

279

let vl = List.map translate_expr el in

280

let node_f = node_from_name f in

281

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

282

let o = new_instance node_f eq.eq_rhs.expr_tag in

283

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

284

el [eq.eq_rhs.expr_clock] in

285

let call_ck = Clock_calculus.compute_root_clock

286

(Clock_predef.ck_tuple env_cks) in

287

let ctx = ctl ~ck:call_ck (MStep (var_p, o, vl)) in

288

(*Clocks.new_var true in

289

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

290

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

291

{ ctx with

292

si = if Stateless.check_node node_f

293

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

294

j = IMap.add o call_f ctx.j;

295

s = (if Stateless.check_node node_f

296

then []

297

else reset_instance o r call_ck)

298

@ ctx.s

299

}

300

 [x], _ >

301

let var_x = env.get_var x in

302

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

303

 _ >

304

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

305

Printers.pp_node_eq eq;

306

assert false

307


308

let constant_equations locals =

309

VSet.fold (fun vdecl eqs >

310

if vdecl.var_dec_const

311

then

312

{ eq_lhs = [vdecl.var_id];

313

eq_rhs = desome vdecl.var_dec_value;

314

eq_loc = vdecl.var_loc

315

} :: eqs

316

else eqs)

317

locals []

318


319

let translate_eqs env ctx eqs =

320

List.fold_right (fun eq ctx > translate_eq env ctx eq) eqs ctx

321


322


323

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

324

(* Processing nodes *)

325

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

326


327

let process_asserts nd =

328


329

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

330

if Backends.is_functional () then

331

[], [], exprl

332

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

333

v=e; assert (v); *)

334

let _, vars, eql, assertl =

335

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

336

let loc = expr.expr_loc in

337

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

338

let assert_var =

339

mkvar_decl

340

loc

341

~orig:false (* fresh var *)

342

(var_id,

343

mktyp loc Tydec_bool,

344

mkclock loc Ckdec_any,

345

false, (* not a constant *)

346

None, (* no default value *)

347

Some nd.node_id

348

)

349

in

350

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

351

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

352

(i+1,

353

assert_var::vars,

354

eq::eqlist,

355

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

356

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

357

in

358

vars, eql, assertl

359


360

let translate_core sorted_eqs locals other_vars =

361

let constant_eqs = constant_equations locals in

362


363

let env = build_env locals other_vars in

364


365

(* Compute constants' instructions *)

366

let ctx0 = translate_eqs env ctx_init constant_eqs in

367

assert (VSet.is_empty ctx0.m);

368

assert (ctx0.si = []);

369

assert (IMap.is_empty ctx0.j);

370


371

(* Compute ctx for all eqs *)

372

let ctx = translate_eqs env ctx_init sorted_eqs in

373


374

ctx, ctx0.s

375


376


377

let translate_decl nd sch =

378

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

379

(* Extracting eqs, variables .. *)

380

let eqs, auts = get_node_eqs nd in

381

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

382


383

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

384

to be declared for each assert *)

385

let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in

386


387

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

388

let locals_list = nd.node_locals @ new_locals in

389

let locals = VSet.of_list locals_list in

390

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

391

let env = build_env locals inout_vars in

392


393

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

394


395

(* Computing main content *)

396

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

397

let schedule = sch.Scheduling_type.schedule in

398

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

399

let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in

400

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

401

* VSet.pp locals

402

* VSet.pp inout_vars

403

* ; *)

404


405

let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in

406


407

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

408


409

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

410

let updated_locals =

411

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

412

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

413

in

414

let mmap = IMap.bindings ctx.j in

415

{

416

mname = nd;

417

mmemory = VSet.elements ctx.m;

418

mcalls = mmap;

419

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

420

minit = ctx.si;

421

mconst = ctx0_s;

422

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

423

mstep = {

424

step_inputs = nd.node_inputs;

425

step_outputs = nd.node_outputs;

426

step_locals = updated_locals;

427

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

428

translate_expr env

429

(expr_of_dimension d))

430

nd.node_checks;

431

step_instrs = (

432

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

433

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

434

backends. *)

435

if !Backends.join_guards then

436

join_guards_list ctx.s

437

else

438

ctx.s

439

);

440

step_asserts = List.map (translate_expr env) nd_node_asserts;

441

};

442


443

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

444

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

445

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

446

not contain any statement or import. *)

447


448

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

449

mannot = nd.node_annot;

450

msch = Some sch;

451

}

452


453

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

454

let translate_prog decls node_schs =

455

let nodes = get_nodes decls in

456

let machines =

457

List.map

458

(fun decl >

459

let node = node_of_top decl in

460

let sch = IMap.find node.node_id node_schs in

461

translate_decl node sch

462

) nodes

463

in

464

machines

465


466

(* Local Variables: *)

467

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

468

(* End: *)
