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


22

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

23

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

24

(* si : initialization instructions *)

25

(* j : node aka machine instances *)

26

(* d : local variables *)

27

(* s : step instructions *)

28

let translate_ident node (m, si, j, d, s) id =

29

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

30

try (* id is a node var *)

31

let var_id = get_node_var id node in

32

if VSet.exists (fun v > v.var_id = id) m

33

then (

34

(* Format.eprintf "a STATE VAR@."; *)

35

mk_val (StateVar var_id) var_id.var_type

36

)

37

else (

38

(* Format.eprintf "a LOCAL VAR@."; *)

39

mk_val (LocalVar var_id) var_id.var_type

40

)

41

with Not_found >

42

try (* id is a constant *)

43

let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in

44

mk_val (LocalVar vdecl) vdecl.var_type

45

with Not_found >

46

(* id is a tag *)

47

(* DONE construire une liste des enum declarés et alors chercher dedans la liste

48

qui contient id *)

49

try

50

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

51

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

52

with Not_found > (Format.eprintf "internal error: Machine_code.translate_ident %s" id;

53

assert false)

54


55

let rec control_on_clock node ((m, si, j, d, s) as args) ck inst =

56

match (Clocks.repr ck).cdesc with

57

 Con (ck1, cr, l) >

58

let id = Clocks.const_of_carrier cr in

59

control_on_clock node args ck1 (mkinstr

60

(* TODO il faudrait prendre le lustre

61

associé à instr et rajouter print_ck_suffix

62

ck) de clocks.ml *)

63

(MBranch (translate_ident node args id,

64

[l, [inst]] )))

65

 _ > inst

66


67


68

(* specialize predefined (polymorphic) operators

69

wrt their instances, so that the C semantics

70

is preserved *)

71

let specialize_to_c expr =

72

match expr.expr_desc with

73

 Expr_appl (id, e, r) >

74

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

75

then let id =

76

match id with

77

 "=" > "equi"

78

 "!=" > "xor"

79

 _ > id in

80

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

81

else expr

82

 _ > expr

83


84

let specialize_op expr =

85

match !Options.output with

86

 "C" > specialize_to_c expr

87

 _ > expr

88


89

let rec translate_expr node ((m, si, j, d, s) as args) expr =

90

let expr = specialize_op expr in

91

let value_desc =

92

match expr.expr_desc with

93

 Expr_const v > Cst v

94

 Expr_ident x > (translate_ident node args x).value_desc

95

 Expr_array el > Array (List.map (translate_expr node args) el)

96

 Expr_access (t, i) > Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))

97

 Expr_power (e, n) > Power (translate_expr node args e, translate_expr node args (expr_of_dimension n))

98

 Expr_tuple _

99

 Expr_arrow _

100

 Expr_fby _

101

 Expr_pre _ > (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)

102

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

103

 Expr_merge (x, _) > raise NormalizationError

104

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

105

let nd = node_from_name id in

106

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

107

 Expr_ite (g,t,e) > (

108

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

109

are preserved in expression. While they are removed for C or Java

110

backends. *)

111

match !Options.output with

112

 "horn" >

113

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

114

 "C"  "java"  _ >

115

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

116

!Options.output

117

Printers.pp_expr expr;

118

raise NormalizationError)

119

)

120

 _ > raise NormalizationError

121

in

122

mk_val value_desc expr.expr_type

123


124

let translate_guard node args expr =

125

match expr.expr_desc with

126

 Expr_ident x > translate_ident node args x

127

 _ > (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false)

128


129

let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =

130

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

131

match expr.expr_desc with

132

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

133

mk_conditional ?lustre_eq:(Some eq) g

134

[translate_act node args (y, t)]

135

[translate_act node args (y, e)]

136

 Expr_merge (x, hl) > mkinstr ?lustre_eq:(Some eq) (MBranch (translate_ident node args x,

137

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

138

 _ > mkinstr ?lustre_eq:(Some eq) (MLocalAssign (y, translate_expr node args expr))

139


140

let reset_instance node args i r c =

141

match r with

142

 None > []

143

 Some r > let g = translate_guard node args r in

144

[control_on_clock node args c (mk_conditional g [mkinstr (MReset i)] [mkinstr (MNoReset i)])]

145


146

let translate_eq node ((m, si, j, d, s) as args) eq =

147

(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)

148

match eq.eq_lhs, eq.eq_rhs.expr_desc with

149

 [x], Expr_arrow (e1, e2) >

150

let var_x = get_node_var x node in

151

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

152

let c1 = translate_expr node args e1 in

153

let c2 = translate_expr node args e2 in

154

(m,

155

mkinstr (MReset o) :: si,

156

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

157

d,

158

(control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s)

159

 [x], Expr_pre e1 when VSet.mem (get_node_var x node) d >

160

let var_x = get_node_var x node in

161

(VSet.add var_x m,

162

si,

163

j,

164

d,

165

control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1))) :: s)

166

 [x], Expr_fby (e1, e2) when VSet.mem (get_node_var x node) d >

167

let var_x = get_node_var x node in

168

(VSet.add var_x m,

169

mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1)) :: si,

170

j,

171

d,

172

control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e2))) :: s)

173


174

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

175

let var_p = List.map (fun v > get_node_var v node) p in

176

let el = expr_list_of_expr arg in

177

let vl = List.map (translate_expr node args) el in

178

let node_f = node_from_name f in

179

let call_f =

180

node_f,

181

NodeDep.filter_static_inputs (node_inputs node_f) el in

182

let o = new_instance node node_f eq.eq_rhs.expr_tag in

183

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

184

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

185

(*Clocks.new_var true in

186

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

187

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

188

(m,

189

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

190

Utils.IMap.add o call_f j,

191

d,

192

(if Stateless.check_node node_f

193

then []

194

else reset_instance node args o r call_ck) @

195

(control_on_clock node args call_ck (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl)))) :: s)

196

(*

197

(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)

198

are preserved. While they are replaced as if g then x = t else x = e in C or Java

199

backends. *)

200

 [x], Expr_ite (c, t, e)

201

when (match !Options.output with  "horn" > true  "C"  "java"  _ > false)

202

>

203

let var_x = get_node_var x node in

204

(m,

205

si,

206

j,

207

d,

208

(control_on_clock node args eq.eq_rhs.expr_clock

209

(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)

210

)

211


212

*)

213

 [x], _ > (

214

let var_x = get_node_var x node in

215

(m, si, j, d,

216

control_on_clock

217

node

218

args

219

eq.eq_rhs.expr_clock

220

(translate_act node args (var_x, eq.eq_rhs)) :: s

221

)

222

)

223

 _ >

224

begin

225

Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq;

226

assert false

227

end

228


229

let find_eq xl eqs =

230

let rec aux accu eqs =

231

match eqs with

232

 [] >

233

begin

234

Format.eprintf "Looking for variables %a in the following equations@.%a@."

235

(Utils.fprintf_list ~sep:" , " (fun fmt v > Format.fprintf fmt "%s" v)) xl

236

Printers.pp_node_eqs eqs;

237

assert false

238

end

239

 hd::tl >

240

if List.exists (fun x > List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl

241

in

242

aux [] eqs

243


244

(* Sort the set of equations of node [nd] according

245

to the computed schedule [sch]

246

*)

247

let sort_equations_from_schedule nd sch =

248

(* Format.eprintf "%s schedule: %a@." *)

249

(* nd.node_id *)

250

(* (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch; *)

251

let eqs, auts = get_node_eqs nd in

252

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

253

let split_eqs = Splitting.tuple_split_eq_list eqs in

254

let eqs_rev, remainder =

255

List.fold_left

256

(fun (accu, node_eqs_remainder) vl >

257

if List.exists (fun eq > List.exists (fun v > List.mem v eq.eq_lhs) vl) accu

258

then

259

(accu, node_eqs_remainder)

260

else

261

let eq_v, remainder = find_eq vl node_eqs_remainder in

262

eq_v::accu, remainder

263

)

264

([], split_eqs)

265

sch

266

in

267

begin

268

if List.length remainder > 0 then (

269

let eqs, auts = get_node_eqs nd in

270

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

271

Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?"

272

Printers.pp_node_eqs remainder

273

Printers.pp_node_eqs eqs;

274

assert false);

275

List.rev eqs_rev

276

end

277


278

let constant_equations nd =

279

List.fold_right (fun vdecl eqs >

280

if vdecl.var_dec_const

281

then

282

{ eq_lhs = [vdecl.var_id];

283

eq_rhs = Utils.desome vdecl.var_dec_value;

284

eq_loc = vdecl.var_loc

285

} :: eqs

286

else eqs)

287

nd.node_locals []

288


289

let translate_eqs node args eqs =

290

List.fold_right (fun eq args > translate_eq node args eq) eqs args;;

291


292

let translate_decl nd sch =

293

(*Log.report ~level:1 (fun fmt > Printers.pp_node fmt nd);*)

294

let schedule = sch.Scheduling_type.schedule in

295

let sorted_eqs = sort_equations_from_schedule nd schedule in

296

let constant_eqs = constant_equations nd in

297


298

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

299

to be declared for each assert *)

300

let new_locals, assert_instrs, nd_node_asserts =

301

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

302

if Backends.is_functional () then

303

[], [], exprl

304

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

305

v=e; assert (v); *)

306

let _, vars, eql, assertl =

307

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

308

let loc = expr.expr_loc in

309

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

310

let assert_var =

311

mkvar_decl

312

loc

313

~orig:false (* fresh var *)

314

(var_id,

315

mktyp loc Tydec_bool,

316

mkclock loc Ckdec_any,

317

false, (* not a constant *)

318

None, (* no default value *)

319

Some nd.node_id

320

)

321

in

322

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

323

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

324

(i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist)

325

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

326

in

327

vars, eql, assertl

328

in

329

let locals_list = nd.node_locals @ new_locals in

330


331

let nd = { nd with node_locals = locals_list } in

332

let init_args = VSet.empty, [], Utils.IMap.empty, List.fold_right (fun l > VSet.add l) locals_list VSet.empty, [] in

333

(* memories, init instructions, node calls, local variables (including memories), step instrs *)

334

let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in

335

assert (VSet.is_empty m0);

336

assert (init0 = []);

337

assert (Utils.IMap.is_empty j0);

338

let m, init, j, locals, s as context_with_asserts = translate_eqs nd (m0, init0, j0, locals0, []) (assert_instrs@sorted_eqs) in

339

let mmap = Utils.IMap.fold (fun i n res > (i, n)::res) j [] in

340

{

341

mname = nd;

342

mmemory = VSet.elements m;

343

mcalls = mmap;

344

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

345

minit = init;

346

mconst = s0;

347

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

348

mstep = {

349

step_inputs = nd.node_inputs;

350

step_outputs = nd.node_outputs;

351

step_locals = VSet.elements (VSet.diff locals m);

352

step_checks = List.map (fun d > d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks;

353

step_instrs = (

354

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

355

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

356

backends. *)

357

(*match !Options.output with

358

 "horn" > s

359

 "C"  "java"  _ >*)

360

if !Backends.join_guards then

361

join_guards_list s

362

else

363

s

364

);

365

step_asserts = List.map (translate_expr nd context_with_asserts) nd_node_asserts;

366

};

367

mspec = nd.node_spec;

368

mannot = nd.node_annot;

369

msch = Some sch;

370

}

371


372

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

373

let translate_prog decls node_schs =

374

let nodes = get_nodes decls in

375

List.map

376

(fun decl >

377

let node = node_of_top decl in

378

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

379

translate_decl node sch

380

) nodes

381


382


383

(* Local Variables: *)

384

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

385

(* End: *)
