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


23

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

24

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

25

(* si : initialization instructions *)

26

(* j : node aka machine instances *)

27

(* d : local variables *)

28

(* s : step instructions *)

29

let translate_ident vars _ (* (m, si, j, d, s) *) id =

30

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

31

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

32

let var_id = get_var id vars in

33

mk_val (Var var_id) var_id.var_type

34

with Not_found >

35

try (* id is a constant *)

36

let vdecl = (Corelang.var_decl_of_const

37

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

38

in

39

mk_val (Var vdecl) vdecl.var_type

40

with Not_found >

41

(* id is a tag *)

42

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

43

dedans la liste qui contient id *)

44

try

45

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

46

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

47

with Not_found > (Format.eprintf

48

"internal error: Machine_code.translate_ident %s"

49

id;

50

assert false)

51


52

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

53

match (Clocks.repr ck).cdesc with

54

 Con (ck1, cr, l) >

55

let id = Clocks.const_of_carrier cr in

56

control_on_clock vars args ck1 (mkinstr

57

(* TODO il faudrait prendre le lustre

58

associé à instr et rajouter print_ck_suffix

59

ck) de clocks.ml *)

60

(MBranch (translate_ident vars args id,

61

[l, [inst]] )))

62

 _ > inst

63


64


65

(* specialize predefined (polymorphic) operators

66

wrt their instances, so that the C semantics

67

is preserved *)

68

let specialize_to_c expr =

69

match expr.expr_desc with

70

 Expr_appl (id, e, r) >

71

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

72

then let id =

73

match id with

74

 "=" > "equi"

75

 "!=" > "xor"

76

 _ > id in

77

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

78

else expr

79

 _ > expr

80


81

let specialize_op expr =

82

match !Options.output with

83

 "C" > specialize_to_c expr

84

 _ > expr

85


86

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

87

let expr = specialize_op expr in

88

(* all calls are using the same arguments (vars for the variable

89

enviroment and args for computed memories). No fold constructs

90

here. We can do partial evaluation of translate_expr *)

91

let translate_expr = translate_expr vars args in

92

let value_desc =

93

match expr.expr_desc with

94

 Expr_const v > Cst v

95

 Expr_ident x > (translate_ident vars args x).value_desc

96

 Expr_array el > Array (List.map translate_expr el)

97

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

98

translate_expr

99

(expr_of_dimension i))

100

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

101

translate_expr

102

(expr_of_dimension n))

103

 Expr_tuple _

104

 Expr_arrow _

105

 Expr_fby _

106

 Expr_pre _ > (Printers.pp_expr

107

Format.err_formatter expr;

108

Format.pp_print_flush

109

Format.err_formatter ();

110

raise NormalizationError)

111


112

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

113

 Expr_merge (x, _) > raise NormalizationError

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) > (

118

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

119

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

120

backends. *)

121

match !Options.output with

122

 "horn" >

123

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

124

 "C"  "java"  _ >

125

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

126

!Options.output

127

Printers.pp_expr expr;

128

raise NormalizationError)

129

)

130

 _ > raise NormalizationError

131

in

132

mk_val value_desc expr.expr_type

133


134

let translate_guard vars args expr =

135

match expr.expr_desc with

136

 Expr_ident x > translate_ident vars args x

137

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

138

Printers.pp_expr expr;

139

assert false)

140


141

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

142

let translate_act = translate_act vars args in

143

let translate_guard = translate_guard vars args in

144

let translate_ident = translate_ident vars args in

145

let translate_expr = translate_expr vars args in

146

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

147

match expr.expr_desc with

148

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

149

mk_conditional ?lustre_eq:(Some eq) g

150

[translate_act (y, t)]

151

[translate_act (y, e)]

152

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

153

(MBranch (translate_ident x,

154

List.map (fun (t, h) >

155

t, [translate_act (y, h)])

156

hl))

157

 _ > mkinstr ?lustre_eq:(Some eq)

158

(MLocalAssign (y, translate_expr expr))

159


160

let reset_instance vars args i r c =

161

match r with

162

 None > []

163

 Some r > let g = translate_guard vars args r in

164

[control_on_clock

165

vars

166

args

167

c

168

(mk_conditional

169

g

170

[mkinstr (MReset i)]

171

[mkinstr (MNoReset i)])

172

]

173


174

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

175

let translate_expr = translate_expr vars args in

176

let translate_act = translate_act vars args in

177

let control_on_clock = control_on_clock vars args in

178

let reset_instance = reset_instance vars args in

179


180

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

181

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

182

match eq.eq_lhs, eq.eq_rhs.expr_desc with

183

 [x], Expr_arrow (e1, e2) >

184

let var_x = get_var x vars in

185

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

186

let c1 = translate_expr e1 in

187

let c2 = translate_expr e2 in

188

(m,

189

mkinstr (MReset o) :: si,

190

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

191

d,

192

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

193

 [x], Expr_pre e1 when VSet.mem (get_var x vars) d >

194

let var_x = get_var x vars in

195

(VSet.add var_x m,

196

si,

197

j,

198

d,

199

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

200

 [x], Expr_fby (e1, e2) when VSet.mem (get_var x vars) d >

201

let var_x = get_var x vars in

202

(VSet.add var_x m,

203

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

204

j,

205

d,

206

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

207


208

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

209

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

210

let el = expr_list_of_expr arg in

211

let vl = List.map translate_expr el in

212

let node_f = node_from_name f in

213

let call_f =

214

node_f,

215

NodeDep.filter_static_inputs (node_inputs node_f) el in

216

let o = new_instance node_f eq.eq_rhs.expr_tag in

217

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

218

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

219

(*Clocks.new_var true in

220

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

221

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

222

(m,

223

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

224

Utils.IMap.add o call_f j,

225

d,

226

(if Stateless.check_node node_f

227

then []

228

else reset_instance o r call_ck) @

229

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

230

(*

231

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

232

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

233

backends. *)

234

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

235

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

236

>

237

let var_x = get_node_var x node in

238

(m,

239

si,

240

j,

241

d,

242

(control_on_clock node args eq.eq_rhs.expr_clock

243

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

244

)

245


246

*)

247

 [x], _ > (

248

let var_x = get_var x vars in

249

(m, si, j, d,

250

control_on_clock

251

eq.eq_rhs.expr_clock

252

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

253

)

254

)

255

 _ >

256

begin

257

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

258

assert false

259

end

260


261


262


263

let constant_equations nd =

264

List.fold_right (fun vdecl eqs >

265

if vdecl.var_dec_const

266

then

267

{ eq_lhs = [vdecl.var_id];

268

eq_rhs = Utils.desome vdecl.var_dec_value;

269

eq_loc = vdecl.var_loc

270

} :: eqs

271

else eqs)

272

nd.node_locals []

273


274

let translate_eqs node args eqs =

275

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

276


277

let process_asserts nd =

278


279

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

280

if Backends.is_functional () then

281

[], [], exprl

282

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

283

v=e; assert (v); *)

284

let _, vars, eql, assertl =

285

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

286

let loc = expr.expr_loc in

287

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

288

let assert_var =

289

mkvar_decl

290

loc

291

~orig:false (* fresh var *)

292

(var_id,

293

mktyp loc Tydec_bool,

294

mkclock loc Ckdec_any,

295

false, (* not a constant *)

296

None, (* no default value *)

297

Some nd.node_id

298

)

299

in

300

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

301

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

302

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

303

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

304

in

305

vars, eql, assertl

306


307

let translate_decl nd sch =

308

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

309

let schedule = sch.Scheduling_type.schedule in

310

let sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in

311

let constant_eqs = constant_equations nd in

312


313

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

314

to be declared for each assert *)

315

let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in

316

let locals_list = nd.node_locals @ new_locals in

317

let nd = { nd with node_locals = locals_list } in

318

let vars = get_node_vars nd in

319


320

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

321

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

322


323

let m0, init0, j0, locals0, s0 =

324

translate_eqs vars init_args constant_eqs

325

in

326


327

assert (VSet.is_empty m0);

328

assert (init0 = []);

329

assert (Utils.IMap.is_empty j0);

330


331

let m, init, j, locals, s as context_with_asserts =

332

translate_eqs

333

vars

334

(m0, init0, j0, locals0, [])

335

(assert_instrs@sorted_eqs)

336

in

337

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

338

{

339

mname = nd;

340

mmemory = VSet.elements m;

341

mcalls = mmap;

342

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

343

minit = init;

344

mconst = s0;

345

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

346

mstep = {

347

step_inputs = nd.node_inputs;

348

step_outputs = nd.node_outputs;

349

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

350

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

351

translate_expr vars init_args

352

(expr_of_dimension d))

353

nd.node_checks;

354

step_instrs = (

355

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

356

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

357

backends. *)

358

(*match !Options.output with

359

 "horn" > s

360

 "C"  "java"  _ >*)

361

if !Backends.join_guards then

362

join_guards_list s

363

else

364

s

365

);

366

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

367

};

368

mspec = nd.node_spec;

369

mannot = nd.node_annot;

370

msch = Some sch;

371

}

372


373

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

374

let translate_prog decls node_schs =

375

let nodes = get_nodes decls in

376

List.map

377

(fun decl >

378

let node = node_of_top decl in

379

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

380

translate_decl node sch

381

) nodes

382


383


384

(* Local Variables: *)

385

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

386

(* End: *)
