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 Corelang

16

open Clocks

17

open Causality

18


19

exception NormalizationError

20


21

(* Questions:

22


23

 where are used the mconst. They contain initialization of

24

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

25


26


27

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

28

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

29

(* si : initialization instructions *)

30

(* j : node aka machine instances *)

31

(* d : local variables *)

32

(* s : step instructions *)

33


34

(* Machine processing requires knowledge about variables and local

35

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

36

type machine_env = {

37

is_local: string > bool;

38

get_var: string > var_decl

39

}

40


41


42

let build_env locals non_locals =

43

let all = VSet.union locals non_locals in

44

{

45

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

46

get_var = (fun id > try

47

VSet.get id all

48

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


59

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

60

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

61

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

62


63

let translate_ident env id =

64

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

65

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

66

let var_id = env.get_var id in

67

mk_val (Var var_id) var_id.var_type

68

with Not_found >

69

try (* id is a constant *)

70

let vdecl = (Corelang.var_decl_of_const

71

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

72

in

73

mk_val (Var vdecl) vdecl.var_type

74

with Not_found >

75

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

76

try

77

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

78

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

79

with Not_found > (Format.eprintf

80

"internal error: Machine_code.translate_ident %s"

81

id;

82

assert false)

83


84

let rec control_on_clock env ck inst =

85

match (Clocks.repr ck).cdesc with

86

 Con (ck1, cr, l) >

87

let id = Clocks.const_of_carrier cr in

88

control_on_clock env ck1

89

(mkinstr

90

(MBranch (translate_ident env id,

91

[l, [inst]] )))

92

 _ > inst

93


94


95

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

96

so that the C semantics is preserved *)

97

let specialize_to_c expr =

98

match expr.expr_desc with

99

 Expr_appl (id, e, r) >

100

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

101

then let id =

102

match id with

103

 "=" > "equi"

104

 "!=" > "xor"

105

 _ > id in

106

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

107

else expr

108

 _ > expr

109


110

let specialize_op expr =

111

match !Options.output with

112

 "C" > specialize_to_c expr

113

 _ > expr

114


115

let rec translate_expr env expr =

116

let expr = specialize_op expr in

117

let translate_expr = translate_expr env in

118

let value_desc =

119

match expr.expr_desc with

120

 Expr_const v > Cst v

121

 Expr_ident x > (translate_ident env x).value_desc

122

 Expr_array el > Array (List.map translate_expr el)

123

 Expr_access (t, i) > Access (translate_expr t,

124

translate_expr

125

(expr_of_dimension i))

126

 Expr_power (e, n) > Power (translate_expr e,

127

translate_expr

128

(expr_of_dimension n))

129

 Expr_tuple _

130

 Expr_arrow _

131

 Expr_fby _

132

 Expr_pre _ > (Printers.pp_expr

133

Format.err_formatter expr;

134

Format.pp_print_flush

135

Format.err_formatter ();

136

raise NormalizationError)

137


138

 Expr_when (e1, _, _) > (translate_expr e1).value_desc

139

 Expr_merge (x, _) > raise NormalizationError

140

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

141

let nd = node_from_name id in

142

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

143

 Expr_ite (g,t,e) > (

144

(* special treatment depending on the active backend. For

145

functional ones, like horn backend, ite are preserved in

146

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

147

if Backends.is_functional () then

148

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

149

else

150

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

151

!Options.output

152

Printers.pp_expr expr;

153

raise NormalizationError)

154

)

155

 _ > raise NormalizationError

156

in

157

mk_val value_desc expr.expr_type

158


159

let translate_guard env expr =

160

match expr.expr_desc with

161

 Expr_ident x > translate_ident env x

162

 _ > (Format.eprintf "internal error: translate_guard %a@."

163

Printers.pp_expr expr;

164

assert false)

165


166

let rec translate_act env (y, expr) =

167

let translate_act = translate_act env in

168

let translate_guard = translate_guard env in

169

let translate_ident = translate_ident env in

170

let translate_expr = translate_expr env in

171

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

172

match expr.expr_desc with

173

 Expr_ite (c, t, e) > let g = translate_guard c in

174

mk_conditional ?lustre_eq:(Some eq) g

175

[translate_act (y, t)]

176

[translate_act (y, e)]

177

 Expr_merge (x, hl) > mkinstr ?lustre_eq:(Some eq)

178

(MBranch (translate_ident x,

179

List.map (fun (t, h) >

180

t, [translate_act (y, h)])

181

hl))

182

 _ > mkinstr ?lustre_eq:(Some eq)

183

(MLocalAssign (y, translate_expr expr))

184


185

let reset_instance env i r c =

186

match r with

187

 None > []

188

 Some r > let g = translate_guard env r in

189

[control_on_clock

190

env

191

c

192

(mk_conditional

193

g

194

[mkinstr (MReset i)]

195

[mkinstr (MNoReset i)])

196

]

197


198


199

(* Datastructure updated while visiting equations *)

200

type machine_ctx = {

201

m: VSet.t; (* Memories *)

202

si: instr_t list;

203

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

204

s: instr_t list;

205

}

206


207

let ctx_init = { m = VSet.empty; (* memories *)

208

si = []; (* init instr *)

209

j = Utils.IMap.empty;

210

s = [] }

211


212

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

213

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

214

are building *)

215

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

216


217


218


219

let translate_eq env ctx eq =

220

let translate_expr = translate_expr env in

221

let translate_act = translate_act env in

222

let control_on_clock = control_on_clock env in

223

let reset_instance = reset_instance env in

224


225

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

226

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

227

match eq.eq_lhs, eq.eq_rhs.expr_desc with

228

 [x], Expr_arrow (e1, e2) >

229

let var_x = env.get_var x in

230

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

231

let c1 = translate_expr e1 in

232

let c2 = translate_expr e2 in

233

{ ctx with

234

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

235

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

236

s = (control_on_clock

237

eq.eq_rhs.expr_clock

238

(mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))

239

) :: ctx.s

240

}

241

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

242

let var_x = env.get_var x in

243


244

{ ctx with

245

m = VSet.add var_x ctx.m;

246

s = control_on_clock

247

eq.eq_rhs.expr_clock

248

(mkinstr ?lustre_eq:(Some eq)

249

(MStateAssign (var_x, translate_expr e1)))

250

:: ctx.s

251

}

252

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

253

let var_x = env.get_var x in

254

{ ctx with

255

m = VSet.add var_x ctx.m;

256

si = mkinstr ?lustre_eq:(Some eq)

257

(MStateAssign (var_x, translate_expr e1))

258

:: ctx.si;

259

s = control_on_clock

260

eq.eq_rhs.expr_clock

261

(mkinstr ?lustre_eq:(Some eq)

262

(MStateAssign (var_x, translate_expr e2)))

263

:: ctx.s

264

}

265


266

 p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) >

267

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

268

let el = expr_list_of_expr arg in

269

let vl = List.map translate_expr el in

270

let node_f = node_from_name f in

271

let call_f =

272

node_f,

273

NodeDep.filter_static_inputs (node_inputs node_f) el in

274

let o = new_instance node_f eq.eq_rhs.expr_tag in

275

let env_cks = List.fold_right (fun arg cks > arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in

276

let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in

277

(*Clocks.new_var true in

278

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

279

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

280

{ ctx with

281

si =

282

(if Stateless.check_node node_f then ctx.si else mkinstr (MReset o) :: ctx.si);

283

j = Utils.IMap.add o call_f ctx.j;

284

s = (if Stateless.check_node node_f

285

then []

286

else reset_instance o r call_ck) @

287

(control_on_clock call_ck

288

(mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl))))

289

:: ctx.s

290

}

291


292

 [x], _ > (

293

let var_x = env.get_var x in

294

{ ctx with

295

s =

296

control_on_clock

297

eq.eq_rhs.expr_clock

298

(translate_act (var_x, eq.eq_rhs)) :: ctx.s

299

}

300

)

301

 _ >

302

begin

303

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

304

Printers.pp_node_eq eq;

305

assert false

306

end

307


308


309


310

let constant_equations locals =

311

VSet.fold (fun vdecl eqs >

312

if vdecl.var_dec_const

313

then

314

{ eq_lhs = [vdecl.var_id];

315

eq_rhs = Utils.desome vdecl.var_dec_value;

316

eq_loc = vdecl.var_loc

317

} :: eqs

318

else eqs)

319

locals []

320


321

let translate_eqs env ctx eqs =

322

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

323


324


325

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

326

(* Processing nodes *)

327

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

328


329

let process_asserts nd =

330


331

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

332

if Backends.is_functional () then

333

[], [], exprl

334

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

335

v=e; assert (v); *)

336

let _, vars, eql, assertl =

337

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

338

let loc = expr.expr_loc in

339

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

340

let assert_var =

341

mkvar_decl

342

loc

343

~orig:false (* fresh var *)

344

(var_id,

345

mktyp loc Tydec_bool,

346

mkclock loc Ckdec_any,

347

false, (* not a constant *)

348

None, (* no default value *)

349

Some nd.node_id

350

)

351

in

352

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

353

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

354

(i+1,

355

assert_var::vars,

356

eq::eqlist,

357

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

358

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

359

in

360

vars, eql, assertl

361


362

let translate_core sorted_eqs locals other_vars =

363

let constant_eqs = constant_equations locals in

364


365

let env = build_env locals other_vars in

366


367

(* Compute constants' instructions *)

368

let ctx0 = translate_eqs env ctx_init constant_eqs in

369

assert (VSet.is_empty ctx0.m);

370

assert (ctx0.si = []);

371

assert (Utils.IMap.is_empty ctx0.j);

372


373

(* Compute ctx for all eqs *)

374

let ctx = translate_eqs env ctx_init sorted_eqs in

375


376

ctx, ctx0.s

377


378


379

let translate_decl nd sch =

380

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

381

(* Extracting eqs, variables .. *)

382

let eqs, auts = get_node_eqs nd in

383

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

384


385

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

386

to be declared for each assert *)

387

let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in

388


389

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

390

let locals_list = nd.node_locals @ new_locals in

391

let locals = VSet.of_list locals_list in

392

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

393

let env = build_env locals inout_vars in

394


395

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

396


397

(* Computing main content *)

398

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

399

let schedule = sch.Scheduling_type.schedule in

400

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

401

let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in

402

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

403

* VSet.pp locals

404

* VSet.pp inout_vars

405

* ; *)

406


407

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

408


409

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

410


411


412

let mmap = Utils.IMap.elements ctx.j in

413

{

414

mname = nd;

415

mmemory = VSet.elements ctx.m;

416

mcalls = mmap;

417

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

418

minit = ctx.si;

419

mconst = ctx0_s;

420

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

421

mstep = {

422

step_inputs = nd.node_inputs;

423

step_outputs = nd.node_outputs;

424

step_locals = (* Removing computed memories from locals *)

425

VSet.elements (VSet.diff locals ctx.m);

426

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

427

translate_expr env

428

(expr_of_dimension d))

429

nd.node_checks;

430

step_instrs = (

431

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

432

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

433

backends. *)

434

if !Backends.join_guards then

435

join_guards_list ctx.s

436

else

437

ctx.s

438

);

439

step_asserts = List.map (translate_expr env) nd_node_asserts;

440

};

441


442

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

443

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

444

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

445

not contain any statement or import. *)

446


447

mspec = nd.node_spec;

448

mannot = nd.node_annot;

449

msch = Some sch;

450

}

451


452

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

453

let translate_prog decls node_schs =

454

let nodes = get_nodes decls in

455

let machines =

456

List.map

457

(fun decl >

458

let node = node_of_top decl in

459

let sch = Utils.IMap.find node.node_id node_schs in

460

translate_decl node sch

461

) nodes

462

in

463

machines

464


465


466

(* Local Variables: *)

467

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

468

(* End: *)
