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 VSet = 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

(* Returns the node/machine associated to id in m calls *)

105

let get_node_def id m =

106

try

107

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

108

Corelang.node_of_top decl

109

with Not_found > (

110

(* Format.eprintf "Unable to find node %s in list [%a]@.@?" *)

111

(* id *)

112

(* (Utils.fprintf_list ~sep:", " (fun fmt (n,_) > Format.fprintf fmt "%s" n)) m.mcalls *)

113

(* ; *)

114

raise Not_found

115

)

116


117

(* merge log: machine_vars was in 44686 *)

118

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

119


120

let pp_step fmt s =

121

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

122

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

123

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

124

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

125

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

126

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

127

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

128


129


130

let pp_static_call fmt (node, args) =

131

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

132

(node_name node)

133

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

134


135

let pp_machine fmt m =

136

Format.fprintf fmt

137

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

138

m.mname.node_id

139

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

140

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

141

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

142

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

143

pp_step m.mstep

144

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

145

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

146


147

let pp_machines fmt ml =

148

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

149


150


151

let rec is_const_value v =

152

match v.value_desc with

153

 Cst _ > true

154

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

155

 _ > false

156


157

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

158

let get_stateless_status m =

159

(m.mname.node_dec_stateless, try Utils.desome m.mname.node_stateless with _ > failwith ("stateless status of machine " ^ m.mname.node_id ^ " not computed"))

160


161

let is_input m id =

162

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

163


164

let is_output m id =

165

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

166


167

let is_memory m id =

168

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

169


170

let conditional ?lustre_eq c t e =

171

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

172


173

let dummy_var_decl name typ =

174

{

175

var_id = name;

176

var_orig = false;

177

var_dec_type = dummy_type_dec;

178

var_dec_clock = dummy_clock_dec;

179

var_dec_const = false;

180

var_dec_value = None;

181

var_type = typ;

182

var_clock = Clocks.new_ck Clocks.Cvar true;

183

var_loc = Location.dummy_loc

184

}

185


186

let arrow_id = "_arrow"

187


188

let arrow_typ = Types.new_ty Types.Tunivar

189


190

let arrow_desc =

191

{

192

node_id = arrow_id;

193

node_type = Type_predef.type_bin_poly_op;

194

node_clock = Clock_predef.ck_bin_univ;

195

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

196

node_outputs= [dummy_var_decl "_out" arrow_typ];

197

node_locals= [];

198

node_gencalls = [];

199

node_checks = [];

200

node_asserts = [];

201

node_stmts= [];

202

node_dec_stateless = false;

203

node_stateless = Some false;

204

node_spec = None;

205

node_annot = []; }

206


207

let arrow_top_decl =

208

{

209

top_decl_desc = Node arrow_desc;

210

top_decl_owner = (Options_management.core_dependency "arrow");

211

top_decl_itf = false;

212

top_decl_loc = Location.dummy_loc

213

}

214


215

let mk_val v t = { value_desc = v;

216

value_type = t;

217

value_annot = None }

218


219

let arrow_machine =

220

let state = "_first" in

221

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

222

let var_input1 = List.nth arrow_desc.node_inputs 0 in

223

let var_input2 = List.nth arrow_desc.node_inputs 1 in

224

let var_output = List.nth arrow_desc.node_outputs 0 in

225

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

226

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

227

{

228

mname = arrow_desc;

229

mmemory = [var_state];

230

mcalls = [];

231

minstances = [];

232

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

233

mstatic = [];

234

mconst = [];

235

mstep = {

236

step_inputs = arrow_desc.node_inputs;

237

step_outputs = arrow_desc.node_outputs;

238

step_locals = [];

239

step_checks = [];

240

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

241

(List.map mkinstr

242

[MStateAssign(var_state, cst false);

243

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

244

(List.map mkinstr

245

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

246

step_asserts = [];

247

};

248

mspec = None;

249

mannot = [];

250

}

251


252

let empty_desc =

253

{

254

node_id = arrow_id;

255

node_type = Types.bottom;

256

node_clock = Clocks.bottom;

257

node_inputs= [];

258

node_outputs= [];

259

node_locals= [];

260

node_gencalls = [];

261

node_checks = [];

262

node_asserts = [];

263

node_stmts= [];

264

node_dec_stateless = true;

265

node_stateless = Some true;

266

node_spec = None;

267

node_annot = []; }

268


269

let empty_machine =

270

{

271

mname = empty_desc;

272

mmemory = [];

273

mcalls = [];

274

minstances = [];

275

minit = [];

276

mstatic = [];

277

mconst = [];

278

mstep = {

279

step_inputs = [];

280

step_outputs = [];

281

step_locals = [];

282

step_checks = [];

283

step_instrs = [];

284

step_asserts = [];

285

};

286

mspec = None;

287

mannot = [];

288

}

289


290

let new_instance =

291

let cpt = ref (1) in

292

fun caller callee tag >

293

begin

294

let o =

295

if Stateless.check_node callee then

296

node_name callee

297

else

298

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

299

let o =

300

if !Options.ansi && is_generic_node callee

301

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

302

else o in

303

o

304

end

305


306


307

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

308

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

309

(* si : initialization instructions *)

310

(* j : node aka machine instances *)

311

(* d : local variables *)

312

(* s : step instructions *)

313

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

314

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

315

try (* id is a node var *)

316

let var_id = get_node_var id node in

317

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

318

then (

319

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

320

mk_val (StateVar var_id) var_id.var_type

321

)

322

else (

323

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

324

mk_val (LocalVar var_id) var_id.var_type

325

)

326

with Not_found >

327

try (* id is a constant *)

328

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

329

mk_val (LocalVar vdecl) vdecl.var_type

330

with Not_found >

331

(* id is a tag *)

332

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

333

qui contient id *)

334

try

335

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

336

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

337

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

338

assert false)

339


340

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

341

match (Clocks.repr ck).cdesc with

342

 Con (ck1, cr, l) >

343

let id = Clocks.const_of_carrier cr in

344

control_on_clock node args ck1 (mkinstr

345

(* TODO il faudrait prendre le lustre

346

associé à instr et rajouter print_ck_suffix

347

ck) de clocks.ml *)

348

(MBranch (translate_ident node args id,

349

[l, [inst]] )))

350

 _ > inst

351


352

let rec join_branches hl1 hl2 =

353

match hl1, hl2 with

354

 [] , _ > hl2

355

 _ , [] > hl1

356

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

357

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

358

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

359

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

360


361

and join_guards inst1 insts2 =

362

match get_instr_desc inst1, List.map get_instr_desc insts2 with

363

 _ , [] >

364

[inst1]

365

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

366

mkinstr

367

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

368

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

369

:: (List.tl insts2)

370

 _ > inst1 :: insts2

371


372

let join_guards_list insts =

373

List.fold_right join_guards insts []

374


375

(* specialize predefined (polymorphic) operators

376

wrt their instances, so that the C semantics

377

is preserved *)

378

let specialize_to_c expr =

379

match expr.expr_desc with

380

 Expr_appl (id, e, r) >

381

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

382

then let id =

383

match id with

384

 "=" > "equi"

385

 "!=" > "xor"

386

 _ > id in

387

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

388

else expr

389

 _ > expr

390


391

let specialize_op expr =

392

match !Options.output with

393

 "C" > specialize_to_c expr

394

 _ > expr

395


396

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

397

let expr = specialize_op expr in

398

let value_desc =

399

match expr.expr_desc with

400

 Expr_const v > Cst v

401

 Expr_ident x > (translate_ident node args x).value_desc

402

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

403

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

404

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

405

 Expr_tuple _

406

 Expr_arrow _

407

 Expr_fby _

408

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

409

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

410

 Expr_merge (x, _) > raise NormalizationError

411

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

412

let nd = node_from_name id in

413

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

414

 Expr_ite (g,t,e) > (

415

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

416

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

417

backends. *)

418

match !Options.output with

419

 "horn" >

420

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

421

 "C"  "java"  _ >

422

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

423

!Options.output

424

Printers.pp_expr expr;

425

raise NormalizationError)

426

)

427

 _ > raise NormalizationError

428

in

429

mk_val value_desc expr.expr_type

430


431

let translate_guard node args expr =

432

match expr.expr_desc with

433

 Expr_ident x > translate_ident node args x

434

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

435


436

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

437

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

438

match expr.expr_desc with

439

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

440

conditional ?lustre_eq:(Some eq) g

441

[translate_act node args (y, t)]

442

[translate_act node args (y, e)]

443

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

444

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

445

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

446


447

let reset_instance node args i r c =

448

match r with

449

 None > []

450

 Some r > let g = translate_guard node args r in

451

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

452


453

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

454

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

455

match eq.eq_lhs, eq.eq_rhs.expr_desc with

456

 [x], Expr_arrow (e1, e2) >

457

let var_x = get_node_var x node in

458

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

459

let c1 = translate_expr node args e1 in

460

let c2 = translate_expr node args e2 in

461

(m,

462

mkinstr (MReset o) :: si,

463

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

464

d,

465

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

466

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

467

let var_x = get_node_var x node in

468

(VSet.add var_x m,

469

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 e1))) :: s)

473

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

474

let var_x = get_node_var x node in

475

(VSet.add var_x m,

476

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

477

j,

478

d,

479

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

480


481

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

482

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

483

let el = expr_list_of_expr arg in

484

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

485

let node_f = node_from_name f in

486

let call_f =

487

node_f,

488

NodeDep.filter_static_inputs (node_inputs node_f) el in

489

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

490

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

491

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

492

(*Clocks.new_var true in

493

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

494

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

495

(m,

496

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

497

Utils.IMap.add o call_f j,

498

d,

499

(if Stateless.check_node node_f

500

then []

501

else reset_instance node args o r call_ck) @

502

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

503

(*

504

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

505

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

506

backends. *)

507

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

508

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

509

>

510

let var_x = get_node_var x node in

511

(m,

512

si,

513

j,

514

d,

515

(control_on_clock node args eq.eq_rhs.expr_clock

516

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

517

)

518


519

*)

520

 [x], _ > (

521

let var_x = get_node_var x node in

522

(m, si, j, d,

523

control_on_clock

524

node

525

args

526

eq.eq_rhs.expr_clock

527

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

528

)

529

)

530

 _ >

531

begin

532

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

533

assert false

534

end

535


536

let find_eq xl eqs =

537

let rec aux accu eqs =

538

match eqs with

539

 [] >

540

begin

541

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

542

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

543

Printers.pp_node_eqs eqs;

544

assert false

545

end

546

 hd::tl >

547

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

548

in

549

aux [] eqs

550


551

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

552

to the computed schedule [sch]

553

*)

554

let sort_equations_from_schedule nd sch =

555

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

556

(* nd.node_id *)

557

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

558

let eqs, auts = get_node_eqs nd in

559

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

560

let split_eqs = Splitting.tuple_split_eq_list eqs in

561

let eqs_rev, remainder =

562

List.fold_left

563

(fun (accu, node_eqs_remainder) vl >

564

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

565

then

566

(accu, node_eqs_remainder)

567

else

568

let eq_v, remainder = find_eq vl node_eqs_remainder in

569

eq_v::accu, remainder

570

)

571

([], split_eqs)

572

sch

573

in

574

begin

575

if List.length remainder > 0 then (

576

let eqs, auts = get_node_eqs nd in

577

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

578

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

579

Printers.pp_node_eqs remainder

580

Printers.pp_node_eqs eqs;

581

assert false);

582

List.rev eqs_rev

583

end

584


585

let constant_equations nd =

586

List.fold_right (fun vdecl eqs >

587

if vdecl.var_dec_const

588

then

589

{ eq_lhs = [vdecl.var_id];

590

eq_rhs = Utils.desome vdecl.var_dec_value;

591

eq_loc = vdecl.var_loc

592

} :: eqs

593

else eqs)

594

nd.node_locals []

595


596

let translate_eqs node args eqs =

597

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

598


599

let translate_decl nd sch =

600

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

601


602

let sorted_eqs = sort_equations_from_schedule nd sch in

603

let constant_eqs = constant_equations nd in

604


605

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

606

to be declared for each assert *)

607

let new_locals, assert_instrs, nd_node_asserts =

608

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

609

if Backends.is_functional () then

610

[], [], exprl

611

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

612

v=e; assert (v); *)

613

let _, vars, eql, assertl =

614

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

615

let loc = expr.expr_loc in

616

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

617

let assert_var =

618

mkvar_decl

619

loc

620

~orig:false (* fresh var *)

621

(var_id,

622

mktyp loc Tydec_bool,

623

mkclock loc Ckdec_any,

624

false, (* not a constant *)

625

None (* no default value *)

626

)

627

in

628

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

629

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

630

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

631

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

632

in

633

vars, eql, assertl

634

in

635

let locals_list = nd.node_locals @ new_locals in

636


637

let nd = { nd with node_locals = locals_list } in

638

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

639

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

640

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

641

assert (VSet.is_empty m0);

642

assert (init0 = []);

643

assert (Utils.IMap.is_empty j0);

644

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

645

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

646

{

647

mname = nd;

648

mmemory = VSet.elements m;

649

mcalls = mmap;

650

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

651

minit = init;

652

mconst = s0;

653

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

654

mstep = {

655

step_inputs = nd.node_inputs;

656

step_outputs = nd.node_outputs;

657

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

658

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

659

step_instrs = (

660

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

661

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

662

backends. *)

663

(*match !Options.output with

664

 "horn" > s

665

 "C"  "java"  _ >*)

666

if !Backends.join_guards then

667

join_guards_list s

668

else

669

s

670

);

671

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

672

};

673

mspec = nd.node_spec;

674

mannot = nd.node_annot;

675

}

676


677

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

678

let translate_prog decls node_schs =

679

let nodes = get_nodes decls in

680

List.map

681

(fun decl >

682

let node = node_of_top decl in

683

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

684

translate_decl node sch

685

) nodes

686


687

let get_machine_opt name machines =

688

List.fold_left

689

(fun res m >

690

match res with

691

 Some _ > res

692

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

693

None machines

694


695

let get_const_assign m id =

696

try

697

match get_instr_desc (List.find

698

(fun instr > match get_instr_desc instr with

699

 MLocalAssign (v, _) > v == id

700

 _ > false)

701

m.mconst

702

) with

703

 MLocalAssign (_, e) > e

704

 _ > assert false

705

with Not_found > assert false

706


707


708

let value_of_ident loc m id =

709

(* is is a state var *)

710

try

711

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

712

in mk_val (StateVar v) v.var_type

713

with Not_found >

714

try (* id is a node var *)

715

let v = get_node_var id m.mname

716

in mk_val (LocalVar v) v.var_type

717

with Not_found >

718

try (* id is a constant *)

719

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

720

in mk_val (LocalVar c) c.var_type

721

with Not_found >

722

(* id is a tag *)

723

let t = Const_tag id

724

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

725


726

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

727

let type_of_value_appl f args =

728

if List.mem f Basic_library.arith_funs

729

then (List.hd args).value_type

730

else Type_predef.type_bool

731


732

let rec value_of_dimension m dim =

733

match dim.Dimension.dim_desc with

734

 Dimension.Dbool b >

735

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

736

 Dimension.Dint i >

737

mk_val (Cst (Const_int i)) Type_predef.type_int

738

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

739

 Dimension.Dappl (f, args) >

740

let vargs = List.map (value_of_dimension m) args

741

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

742

 Dimension.Dite (i, t, e) >

743

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

744

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

745

 _ > assert false)

746

 Dimension.Dlink dim' > value_of_dimension m dim'

747

 _ > assert false

748


749

let rec dimension_of_value value =

750

match value.value_desc with

751

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

752

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

753

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

754

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

755

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

756

 _ > assert false

757


758

(* Local Variables: *)

759

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

760

(* End: *)
