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 LustreSpec

13

open Corelang

14

open Clocks

15

open Causality

16


17

let print_statelocaltag = true

18


19

exception NormalizationError

20


21

module OrdVarDecl:Map.OrderedType with type t=var_decl =

22

struct type t = var_decl;; let compare = compare end

23


24

module ISet = Set.Make(OrdVarDecl)

25


26

let rec pp_val fmt v =

27

match v.value_desc with

28

 Cst c > Printers.pp_const fmt c

29

 LocalVar v >

30

if print_statelocaltag then

31

Format.fprintf fmt "%s(L)" v.var_id

32

else

33

Format.pp_print_string fmt v.var_id

34


35

 StateVar v >

36

if print_statelocaltag then

37

Format.fprintf fmt "%s(S)" v.var_id

38

else

39

Format.pp_print_string fmt v.var_id

40

 Array vl > Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl

41

 Access (t, i) > Format.fprintf fmt "%a[%a]" pp_val t pp_val i

42

 Power (v, n) > Format.fprintf fmt "(%a^%a)" pp_val v pp_val n

43

 Fun (n, vl) > Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl

44


45

let rec pp_instr fmt i =

46

let _ =

47

match i.instr_desc with

48

 MLocalAssign (i,v) > Format.fprintf fmt "%s<l %a" i.var_id pp_val v

49

 MStateAssign (i,v) > Format.fprintf fmt "%s<s %a" i.var_id pp_val v

50

 MReset i > Format.fprintf fmt "reset %s" i

51

 MNoReset i > Format.fprintf fmt "noreset %s" i

52

 MStep (il, i, vl) >

53

Format.fprintf fmt "%a = %s (%a)"

54

(Utils.fprintf_list ~sep:", " (fun fmt v > Format.pp_print_string fmt v.var_id)) il

55

i

56

(Utils.fprintf_list ~sep:", " pp_val) vl

57

 MBranch (g,hl) >

58

Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"

59

pp_val g

60

(Utils.fprintf_list ~sep:"@," pp_branch) hl

61

 MComment s > Format.pp_print_string fmt s

62


63

in

64

(* Annotation *)

65

(* let _ = *)

66

(* match i.lustre_expr with None > ()  Some e > Format.fprintf fmt "  original expr: %a" Printers.pp_expr e *)

67

(* in *)

68

let _ =

69

match i.lustre_eq with None > ()  Some eq > Format.fprintf fmt "  original eq: %a" Printers.pp_node_eq eq

70

in

71

()

72


73

and pp_branch fmt (t, h) =

74

Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h

75


76

and pp_instrs fmt il =

77

Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," pp_instr) il

78


79

type step_t = {

80

step_checks: (Location.t * value_t) list;

81

step_inputs: var_decl list;

82

step_outputs: var_decl list;

83

step_locals: var_decl list;

84

step_instrs: instr_t list;

85

step_asserts: value_t list;

86

}

87


88

type static_call = top_decl * (Dimension.dim_expr list)

89


90

type machine_t = {

91

mname: node_desc;

92

mmemory: var_decl list;

93

mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *)

94

minstances: (ident * static_call) list; (* submap of mcalls, from stateful instance to node *)

95

minit: instr_t list;

96

mstatic: var_decl list; (* static inputs only *)

97

mconst: instr_t list; (* assignments of node constant locals *)

98

mstep: step_t;

99

mspec: node_annot option;

100

mannot: expr_annot list;

101

}

102


103

(* merge log: get_node_def was in c0f8 *)

104

let get_node_def id m =

105

try

106

let (decl, _) = List.assoc id m.minstances in

107

Corelang.node_of_top decl

108

with Not_found > raise Not_found

109


110

(* merge log: machine_vars was in 44686 *)

111

let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory

112


113

let pp_step fmt s =

114

Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "

115

(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs

116

(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs

117

(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals

118

(Utils.fprintf_list ~sep:", " (fun fmt (_, c) > pp_val fmt c)) s.step_checks

119

(Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs

120

(Utils.fprintf_list ~sep:", " pp_val) s.step_asserts

121


122


123

let pp_static_call fmt (node, args) =

124

Format.fprintf fmt "%s<%a>"

125

(node_name node)

126

(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args

127


128

let pp_machine fmt m =

129

Format.fprintf fmt

130

"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ const : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ "

131

m.mname.node_id

132

(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory

133

(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) > Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances

134

(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit

135

(Utils.fprintf_list ~sep:"@ " pp_instr) m.mconst

136

pp_step m.mstep

137

(fun fmt > match m.mspec with  None > ()  Some spec > Printers.pp_spec fmt spec)

138

(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot

139


140

let pp_machines fmt ml =

141

Format.fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml

142


143


144

let rec is_const_value v =

145

match v.value_desc with

146

 Cst _ > true

147

 Fun (id, args) > Basic_library.is_value_internal_fun v && List.for_all is_const_value args

148

 _ > false

149


150

(* Returns the declared stateless status and the computed one. *)

151

let get_stateless_status m =

152

(m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless)

153


154

let is_input m id =

155

List.exists (fun o > o.var_id = id.var_id) m.mstep.step_inputs

156


157

let is_output m id =

158

List.exists (fun o > o.var_id = id.var_id) m.mstep.step_outputs

159


160

let is_memory m id =

161

List.exists (fun o > o.var_id = id.var_id) m.mmemory

162


163

let conditional ?lustre_eq c t e =

164

mkinstr ?lustre_eq:lustre_eq (MBranch(c, [ (tag_true, t); (tag_false, e) ]))

165


166

let dummy_var_decl name typ =

167

{

168

var_id = name;

169

var_orig = false;

170

var_dec_type = dummy_type_dec;

171

var_dec_clock = dummy_clock_dec;

172

var_dec_const = false;

173

var_dec_value = None;

174

var_type = typ;

175

var_clock = Clocks.new_ck Clocks.Cvar true;

176

var_loc = Location.dummy_loc

177

}

178


179

let arrow_id = "_arrow"

180


181

let arrow_typ = Types.new_ty Types.Tunivar

182


183

let arrow_desc =

184

{

185

node_id = arrow_id;

186

node_type = Type_predef.type_bin_poly_op;

187

node_clock = Clock_predef.ck_bin_univ;

188

node_inputs= [dummy_var_decl "_in1" arrow_typ; dummy_var_decl "_in2" arrow_typ];

189

node_outputs= [dummy_var_decl "_out" arrow_typ];

190

node_locals= [];

191

node_gencalls = [];

192

node_checks = [];

193

node_asserts = [];

194

node_stmts= [];

195

node_dec_stateless = false;

196

node_stateless = Some false;

197

node_spec = None;

198

node_annot = []; }

199


200

let arrow_top_decl =

201

{

202

top_decl_desc = Node arrow_desc;

203

top_decl_owner = (Options_management.core_dependency "arrow");

204

top_decl_itf = false;

205

top_decl_loc = Location.dummy_loc

206

}

207


208

let mk_val v t = { value_desc = v;

209

value_type = t;

210

value_annot = None }

211


212

let arrow_machine =

213

let state = "_first" in

214

let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in

215

let var_input1 = List.nth arrow_desc.node_inputs 0 in

216

let var_input2 = List.nth arrow_desc.node_inputs 1 in

217

let var_output = List.nth arrow_desc.node_outputs 0 in

218

let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in

219

let t_arg = Types.new_univar () in (* TODO Xavier: c'est bien la bonne def ? *)

220

{

221

mname = arrow_desc;

222

mmemory = [var_state];

223

mcalls = [];

224

minstances = [];

225

minit = [mkinstr (MStateAssign(var_state, cst true))];

226

mstatic = [];

227

mconst = [];

228

mstep = {

229

step_inputs = arrow_desc.node_inputs;

230

step_outputs = arrow_desc.node_outputs;

231

step_locals = [];

232

step_checks = [];

233

step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool)

234

(List.map mkinstr

235

[MStateAssign(var_state, cst false);

236

MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)])

237

(List.map mkinstr

238

[MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)]) ];

239

step_asserts = [];

240

};

241

mspec = None;

242

mannot = [];

243

}

244


245

let empty_desc =

246

{

247

node_id = arrow_id;

248

node_type = Types.bottom;

249

node_clock = Clocks.bottom;

250

node_inputs= [];

251

node_outputs= [];

252

node_locals= [];

253

node_gencalls = [];

254

node_checks = [];

255

node_asserts = [];

256

node_stmts= [];

257

node_dec_stateless = true;

258

node_stateless = Some true;

259

node_spec = None;

260

node_annot = []; }

261


262

let empty_machine =

263

{

264

mname = empty_desc;

265

mmemory = [];

266

mcalls = [];

267

minstances = [];

268

minit = [];

269

mstatic = [];

270

mconst = [];

271

mstep = {

272

step_inputs = [];

273

step_outputs = [];

274

step_locals = [];

275

step_checks = [];

276

step_instrs = [];

277

step_asserts = [];

278

};

279

mspec = None;

280

mannot = [];

281

}

282


283

let new_instance =

284

let cpt = ref (1) in

285

fun caller callee tag >

286

begin

287

let o =

288

if Stateless.check_node callee then

289

node_name callee

290

else

291

Printf.sprintf "ni_%d" (incr cpt; !cpt) in

292

let o =

293

if !Options.ansi && is_generic_node callee

294

then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e > e.expr_tag = tag) caller.node_gencalls)

295

else o in

296

o

297

end

298


299


300

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

301

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

302

(* si : initialization instructions *)

303

(* j : node aka machine instances *)

304

(* d : local variables *)

305

(* s : step instructions *)

306

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

307

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

308

try (* id is a node var *)

309

let var_id = get_node_var id node in

310

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

311

then (

312

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

313

mk_val (StateVar var_id) var_id.var_type

314

)

315

else (

316

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

317

mk_val (LocalVar var_id) var_id.var_type

318

)

319

with Not_found >

320

try (* id is a constant *)

321

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

322

mk_val (LocalVar vdecl) vdecl.var_type

323

with Not_found >

324

(* id is a tag *)

325

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

326

qui contient id *)

327

try

328

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

329

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

330

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

331

assert false)

332


333

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

334

match (Clocks.repr ck).cdesc with

335

 Con (ck1, cr, l) >

336

let id = Clocks.const_of_carrier cr in

337

control_on_clock node args ck1 (mkinstr

338

(* TODO il faudrait prendre le lustre

339

associé à instr et rajouter print_ck_suffix

340

ck) de clocks.ml *)

341

(MBranch (translate_ident node args id,

342

[l, [inst]] )))

343

 _ > inst

344


345

let rec join_branches hl1 hl2 =

346

match hl1, hl2 with

347

 [] , _ > hl2

348

 _ , [] > hl1

349

 (t1, h1)::q1, (t2, h2)::q2 >

350

if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else

351

if t1 > t2 then (t2, h2) :: join_branches hl1 q2

352

else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2

353


354

and join_guards inst1 insts2 =

355

match get_instr_desc inst1, List.map get_instr_desc insts2 with

356

 _ , [] >

357

[inst1]

358

 MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 >

359

mkinstr

360

(* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)

361

(MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))

362

:: (List.tl insts2)

363

 _ > inst1 :: insts2

364


365

let join_guards_list insts =

366

List.fold_right join_guards insts []

367


368

(* specialize predefined (polymorphic) operators

369

wrt their instances, so that the C semantics

370

is preserved *)

371

let specialize_to_c expr =

372

match expr.expr_desc with

373

 Expr_appl (id, e, r) >

374

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

375

then let id =

376

match id with

377

 "=" > "equi"

378

 "!=" > "xor"

379

 _ > id in

380

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

381

else expr

382

 _ > expr

383


384

let specialize_op expr =

385

match !Options.output with

386

 "C" > specialize_to_c expr

387

 _ > expr

388


389

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

390

let expr = specialize_op expr in

391

let value_desc =

392

match expr.expr_desc with

393

 Expr_const v > Cst v

394

 Expr_ident x > (translate_ident node args x).value_desc

395

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

396

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

397

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

398

 Expr_tuple _

399

 Expr_arrow _

400

 Expr_fby _

401

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

402

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

403

 Expr_merge (x, _) > raise NormalizationError

404

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

405

let nd = node_from_name id in

406

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

407

 Expr_ite (g,t,e) > (

408

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

409

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

410

backends. *)

411

match !Options.output with

412

 "horn" >

413

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

414

 "C"  "java"  _ >

415

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

416

!Options.output

417

Printers.pp_expr expr;

418

raise NormalizationError)

419

)

420

 _ > raise NormalizationError

421

in

422

mk_val value_desc expr.expr_type

423


424

let translate_guard node args expr =

425

match expr.expr_desc with

426

 Expr_ident x > translate_ident node args x

427

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

428


429

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

430

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

431

match expr.expr_desc with

432

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

433

conditional ?lustre_eq:(Some eq) g

434

[translate_act node args (y, t)]

435

[translate_act node args (y, e)]

436

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

437

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

438

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

439


440

let reset_instance node args i r c =

441

match r with

442

 None > []

443

 Some r > let g = translate_guard node args r in

444

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

445


446

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

447

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

448

match eq.eq_lhs, eq.eq_rhs.expr_desc with

449

 [x], Expr_arrow (e1, e2) >

450

let var_x = get_node_var x node in

451

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

452

let c1 = translate_expr node args e1 in

453

let c2 = translate_expr node args e2 in

454

(m,

455

mkinstr (MReset o) :: si,

456

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

457

d,

458

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

459

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

460

let var_x = get_node_var x node in

461

(ISet.add var_x m,

462

si,

463

j,

464

d,

465

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

466

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

467

let var_x = get_node_var x node in

468

(ISet.add var_x m,

469

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

470

j,

471

d,

472

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

473


474

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

475

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

476

let el = expr_list_of_expr arg in

477

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

478

let node_f = node_from_name f in

479

let call_f =

480

node_f,

481

NodeDep.filter_static_inputs (node_inputs node_f) el in

482

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

483

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

484

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

485

(*Clocks.new_var true in

486

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

487

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

488

(m,

489

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

490

Utils.IMap.add o call_f j,

491

d,

492

(if Stateless.check_node node_f

493

then []

494

else reset_instance node args o r call_ck) @

495

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

496

(*

497

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

498

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

499

backends. *)

500

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

501

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

502

>

503

let var_x = get_node_var x node in

504

(m,

505

si,

506

j,

507

d,

508

(control_on_clock node args eq.eq_rhs.expr_clock

509

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

510

)

511


512

*)

513

 [x], _ > (

514

let var_x = get_node_var x node in

515

(m, si, j, d,

516

control_on_clock

517

node

518

args

519

eq.eq_rhs.expr_clock

520

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

521

)

522

)

523

 _ >

524

begin

525

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

526

assert false

527

end

528


529

let find_eq xl eqs =

530

let rec aux accu eqs =

531

match eqs with

532

 [] >

533

begin

534

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

535

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

536

Printers.pp_node_eqs eqs;

537

assert false

538

end

539

 hd::tl >

540

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

541

in

542

aux [] eqs

543


544

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

545

to the computed schedule [sch]

546

*)

547

let sort_equations_from_schedule nd sch =

548

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

549

(* nd.node_id *)

550

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

551

let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in

552

let eqs_rev, remainder =

553

List.fold_left

554

(fun (accu, node_eqs_remainder) vl >

555

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

556

then

557

(accu, node_eqs_remainder)

558

else

559

let eq_v, remainder = find_eq vl node_eqs_remainder in

560

eq_v::accu, remainder

561

)

562

([], split_eqs)

563

sch

564

in

565

begin

566

if List.length remainder > 0 then (

567

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

568

Printers.pp_node_eqs remainder

569

Printers.pp_node_eqs (get_node_eqs nd);

570

assert false);

571

List.rev eqs_rev

572

end

573


574

let constant_equations nd =

575

List.fold_right (fun vdecl eqs >

576

if vdecl.var_dec_const

577

then

578

{ eq_lhs = [vdecl.var_id];

579

eq_rhs = Utils.desome vdecl.var_dec_value;

580

eq_loc = vdecl.var_loc

581

} :: eqs

582

else eqs)

583

nd.node_locals []

584


585

let translate_eqs node args eqs =

586

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

587


588

let translate_decl nd sch =

589

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

590


591

let sorted_eqs = sort_equations_from_schedule nd sch in

592

let constant_eqs = constant_equations nd in

593


594

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

595

to be declared for each assert *)

596

let new_locals, assert_instrs, nd_node_asserts =

597

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

598

if Corelang.functional_backend () then

599

[], [], exprl

600

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

601

v=e; assert (v); *)

602

let _, vars, eql, assertl =

603

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

604

let loc = expr.expr_loc in

605

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

606

let assert_var =

607

mkvar_decl

608

loc

609

~orig:false (* fresh var *)

610

(var_id,

611

mktyp loc Tydec_bool,

612

mkclock loc Ckdec_any,

613

false, (* not a constant *)

614

None (* no default value *)

615

)

616

in

617

assert_var.var_type < Types.new_ty (Types.Tbool);

618

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

619

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

620

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

621

in

622

vars, eql, assertl

623

in

624

let locals_list = nd.node_locals @ new_locals in

625


626

let nd = { nd with node_locals = locals_list } in

627

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

628

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

629

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

630

assert (ISet.is_empty m0);

631

assert (init0 = []);

632

assert (Utils.IMap.is_empty j0);

633

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

634

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

635

{

636

mname = nd;

637

mmemory = ISet.elements m;

638

mcalls = mmap;

639

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

640

minit = init;

641

mconst = s0;

642

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

643

mstep = {

644

step_inputs = nd.node_inputs;

645

step_outputs = nd.node_outputs;

646

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

647

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

648

step_instrs = (

649

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

650

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

651

backends. *)

652

(*match !Options.output with

653

 "horn" > s

654

 "C"  "java"  _ >*)

655

if !Backends.join_guards then

656

join_guards_list s

657

else

658

s

659

);

660

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

661

};

662

mspec = nd.node_spec;

663

mannot = nd.node_annot;

664

}

665


666

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

667

let translate_prog decls node_schs =

668

let nodes = get_nodes decls in

669

List.map

670

(fun decl >

671

let node = node_of_top decl in

672

let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in

673

translate_decl node sch

674

) nodes

675


676

let get_machine_opt name machines =

677

List.fold_left

678

(fun res m >

679

match res with

680

 Some _ > res

681

 None > if m.mname.node_id = name then Some m else None)

682

None machines

683


684

let get_const_assign m id =

685

try

686

match get_instr_desc (List.find

687

(fun instr > match get_instr_desc instr with

688

 MLocalAssign (v, _) > v == id

689

 _ > false)

690

m.mconst

691

) with

692

 MLocalAssign (_, e) > e

693

 _ > assert false

694

with Not_found > assert false

695


696


697

let value_of_ident loc m id =

698

(* is is a state var *)

699

try

700

let v = List.find (fun v > v.var_id = id) m.mmemory

701

in mk_val (StateVar v) v.var_type

702

with Not_found >

703

try (* id is a node var *)

704

let v = get_node_var id m.mname

705

in mk_val (LocalVar v) v.var_type

706

with Not_found >

707

try (* id is a constant *)

708

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

709

in mk_val (LocalVar c) c.var_type

710

with Not_found >

711

(* id is a tag *)

712

let t = Const_tag id

713

in mk_val (Cst t) (Typing.type_const loc t)

714


715

(* type of internal fun used in dimension expression *)

716

let type_of_value_appl f args =

717

if List.mem f Basic_library.arith_funs

718

then (List.hd args).value_type

719

else Type_predef.type_bool

720


721

let rec value_of_dimension m dim =

722

match dim.Dimension.dim_desc with

723

 Dimension.Dbool b >

724

mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool

725

 Dimension.Dint i >

726

mk_val (Cst (Const_int i)) Type_predef.type_int

727

 Dimension.Dident v > value_of_ident dim.Dimension.dim_loc m v

728

 Dimension.Dappl (f, args) >

729

let vargs = List.map (value_of_dimension m) args

730

in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs)

731

 Dimension.Dite (i, t, e) >

732

(match List.map (value_of_dimension m) [i; t; e] with

733

 [vi; vt; ve] > mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type

734

 _ > assert false)

735

 Dimension.Dlink dim' > value_of_dimension m dim'

736

 _ > assert false

737


738

let rec dimension_of_value value =

739

match value.value_desc with

740

 Cst (Const_tag t) when t = Corelang.tag_true > Dimension.mkdim_bool Location.dummy_loc true

741

 Cst (Const_tag t) when t = Corelang.tag_false > Dimension.mkdim_bool Location.dummy_loc false

742

 Cst (Const_int i) > Dimension.mkdim_int Location.dummy_loc i

743

 LocalVar v > Dimension.mkdim_ident Location.dummy_loc v.var_id

744

 Fun (f, args) > Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args)

745

 _ > assert false

746


747

(* Local Variables: *)

748

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

749

(* End: *)
