1

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

2

(* *)

3

(* The LustreC compiler toolset / The LustreC Development Team *)

4

(* Copyright 2012   ONERA  CNRS  INPT  LIFL *)

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

(* This file was originally from the Prelude compiler *)

11

(* *)

12

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

13


14


15

(** Simple modular syntactic causality analysis. Can reject correct

16

programs, especially if the program is not flattened first. *)

17

open Utils

18

open Lustre_types

19

open Corelang

20

open Graph

21


22


23

type identified_call = eq * tag

24

type error =

25

 DataCycle of ident list list (* multiple failed partitions at once *)

26

 NodeCycle of ident list

27


28

exception Error of error

29


30


31


32

(* Dependency of mem variables on mem variables is cut off

33

by duplication of some mem vars into local node vars.

34

Thus, cylic dependency errors may only arise between nomem vars.

35

nonmem variables are:

36

 constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars

37

 read mems (fake vars): same remark as above.

38

 outputs: decoupled from mems, if necessary

39

 locals

40

 instance vars (fake vars): simplify causality analysis

41


42

global constants are not part of the dependency graph.

43


44

no_mem' = combinational(no_mem, mem);

45

=> (mem > no_mem' > no_mem)

46


47

mem' = pre(no_mem, mem);

48

=> (mem' > no_mem), (mem > mem')

49


50

Global roadmap:

51

 compute two dep graphs g (nonmem/nonmem&mem) and g' (mem/mem)

52

 check cycles in g (a cycle means a dependency error)

53

 break cycles in g' (it's legal !):

54

 check cycles in g'

55

 if any, introduce aux var to break cycle, then start afresh

56

 insert g' into g

57

 return g

58

*)

59


60

(* Tests whether [v] is a root of graph [g], i.e. a source *)

61

let is_graph_root v g =

62

IdentDepGraph.in_degree g v = 0

63


64

(* Computes the set of graph roots, i.e. the sources of acyclic graph [g] *)

65

let graph_roots g =

66

IdentDepGraph.fold_vertex

67

(fun v roots > if is_graph_root v g then v::roots else roots)

68

g []

69


70

let add_edges src tgt g =

71

(*List.iter (fun s > List.iter (fun t > Format.eprintf "add %s > %s@." s t) tgt) src;*)

72

List.iter

73

(fun s >

74

List.iter

75

(fun t > IdentDepGraph.add_edge g s t)

76

tgt)

77

src;

78

g

79


80

let add_vertices vtc g =

81

(*List.iter (fun t > Format.eprintf "add %s@." t) vtc;*)

82

List.iter (fun v > IdentDepGraph.add_vertex g v) vtc;

83

g

84


85

let new_graph () =

86

IdentDepGraph.create ()

87


88


89

module ExprDep = struct

90

let get_node_eqs nd =

91

let eqs, auts = get_node_eqs nd in

92

if auts != [] then assert false (* No call on causality on a Lustre model

93

with automaton. They should be expanded by now. *);

94

eqs

95


96

let instance_var_cpt = ref 0

97


98

(* read vars represent input/mem readonly vars,

99

they are not part of the program/schedule,

100

as they are not assigned,

101

but used to compute useless inputs/mems.

102

a mem read var represents a mem at the beginning of a cycle *)

103

let mk_read_var id =

104

Format.sprintf "#%s" id

105


106

(* instance vars represent node instance calls,

107

they are not part of the program/schedule,

108

but used to simplify causality analysis

109

*)

110

let mk_instance_var id =

111

incr instance_var_cpt; Format.sprintf "!%s_%d" id !instance_var_cpt

112


113

let is_read_var v = v.[0] = '#'

114


115

let is_instance_var v = v.[0] = '!'

116


117

let is_ghost_var v = is_instance_var v  is_read_var v

118


119

let undo_read_var id =

120

assert (is_read_var id);

121

String.sub id 1 (String.length id  1)

122


123

let undo_instance_var id =

124

assert (is_instance_var id);

125

String.sub id 1 (String.length id  1)

126


127

let eq_memory_variables mems eq =

128

let rec match_mem lhs rhs mems =

129

match rhs.expr_desc with

130

 Expr_fby _

131

 Expr_pre _ > List.fold_right ISet.add lhs mems

132

 Expr_tuple tl >

133

let lhs' = (transpose_list [lhs]) in

134

List.fold_right2 match_mem lhs' tl mems

135

 _ > mems in

136

match_mem eq.eq_lhs eq.eq_rhs mems

137


138

let node_memory_variables nd =

139

List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)

140


141

let node_input_variables nd =

142

List.fold_left (fun inputs v > ISet.add v.var_id inputs) ISet.empty nd.node_inputs

143


144

let node_local_variables nd =

145

List.fold_left (fun locals v > ISet.add v.var_id locals) ISet.empty nd.node_locals

146


147

let node_constant_variables nd =

148

List.fold_left (fun locals v > if v.var_dec_const then ISet.add v.var_id locals else locals) ISet.empty nd.node_locals

149


150

let node_output_variables nd =

151

List.fold_left (fun outputs v > ISet.add v.var_id outputs) ISet.empty nd.node_outputs

152


153

let node_auxiliary_variables nd =

154

ISet.diff (node_local_variables nd) (node_memory_variables nd)

155


156

let node_variables nd =

157

let inputs = node_input_variables nd in

158

let inoutputs = List.fold_left (fun inoutputs v > ISet.add v.var_id inoutputs) inputs nd.node_outputs in

159

List.fold_left (fun vars v > ISet.add v.var_id vars) inoutputs nd.node_locals

160


161

(* computes the equivalence relation relating variables

162

in the same equation lhs, under the form of a table

163

of class representatives *)

164

let node_eq_equiv nd =

165

let eq_equiv = Hashtbl.create 23 in

166

List.iter (fun eq >

167

let first = List.hd eq.eq_lhs in

168

List.iter (fun v > Hashtbl.add eq_equiv v first) eq.eq_lhs

169

)

170

(get_node_eqs nd);

171

eq_equiv

172


173

(* Create a tuple of right dimension, according to [expr] type, *)

174

(* filled with variable [v] *)

175

let adjust_tuple v expr =

176

match expr.expr_type.Types.tdesc with

177

 Types.Ttuple tl > duplicate v (List.length tl)

178

 _ > [v]

179


180


181

(* Add dependencies from lhs to rhs in [g, g'], *)

182

(* nomem/nomem and mem/nomem in g *)

183

(* mem/mem in g' *)

184

(* match (lhs_is_mem, ISet.mem x mems) with

185

 (false, true ) > (add_edges [x] lhs g,

186

g')

187

 (false, false) > (add_edges lhs [x] g,

188

g')

189

 (true , false) > (add_edges lhs [x] g,

190

g')

191

 (true , true ) > (g,

192

add_edges [x] lhs g')

193

*)

194

let add_eq_dependencies mems inputs node_vars eq (g, g') =

195

let add_var lhs_is_mem lhs x (g, g') =

196

if is_instance_var x  ISet.mem x node_vars then

197

if ISet.mem x mems

198

then

199

let g = add_edges lhs [mk_read_var x] g in

200

if lhs_is_mem

201

then

202

(g, add_edges [x] lhs g')

203

else

204

(add_edges [x] lhs g, g')

205

else

206

let x = if ISet.mem x inputs then mk_read_var x else x in

207

(add_edges lhs [x] g, g')

208

else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *)

209

in

210

(* Add dependencies from [lhs] to rhs clock [ck]. *)

211

let rec add_clock lhs_is_mem lhs ck g =

212

(*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)

213

match (Clocks.repr ck).Clocks.cdesc with

214

 Clocks.Con (ck', cr, _) > add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)

215

 Clocks.Ccarrying (_, ck') > add_clock lhs_is_mem lhs ck' g

216

 _ > g

217

in

218

let rec add_dep lhs_is_mem lhs rhs g =

219

(* Add mashup dependencies for a userdefined node instance [lhs] = [f]([e]) *)

220

(* i.e every input is connected to every output, through a ghost var *)

221

let mashup_appl_dependencies f e g =

222

let f_var = mk_instance_var (Format.sprintf "%s_%d" f eq.eq_loc.Location.loc_start.Lexing.pos_lnum) in

223

List.fold_right (fun rhs > add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)

224

(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g)

225

in

226

match rhs.expr_desc with

227

 Expr_const _ > g

228

 Expr_fby (e1, e2) > add_dep true lhs e2 (add_dep false lhs e1 g)

229

 Expr_pre e > add_dep true lhs e g

230

 Expr_ident x > add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)

231

 Expr_access (e1, d)

232

 Expr_power (e1, d) > add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g)

233

 Expr_array a > List.fold_right (add_dep lhs_is_mem lhs) a g

234

 Expr_tuple t > List.fold_right2 (fun l r > add_dep lhs_is_mem [l] r) lhs t g

235

 Expr_merge (c, hl) > add_var lhs_is_mem lhs c (List.fold_right (fun (_, h) > add_dep lhs_is_mem lhs h) hl g)

236

 Expr_ite (c, t, e) > add_dep lhs_is_mem lhs c (add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g))

237

 Expr_arrow (e1, e2) > add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)

238

 Expr_when (e, c, _) > add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)

239

 Expr_appl (f, e, None) >

240

if Basic_library.is_expr_internal_fun rhs

241

(* tuple componentwise dependency for internal operators *)

242

then

243

List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g

244

(* mashed up dependency for userdefined operators *)

245

else

246

mashup_appl_dependencies f e g

247

 Expr_appl (f, e, Some c) >

248

mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)

249

in

250

let g =

251

List.fold_left

252

(fun g lhs >

253

if ISet.mem lhs mems then

254

add_vertices [lhs; mk_read_var lhs] g

255

else

256

add_vertices [lhs] g

257

)

258

g eq.eq_lhs

259

in

260

add_dep false eq.eq_lhs eq.eq_rhs (g, g')

261


262


263

(* Returns the dependence graph for node [n] *)

264

let dependence_graph mems inputs node_vars n =

265

instance_var_cpt := 0;

266

let g = new_graph (), new_graph () in

267

(* Basic dependencies *)

268

let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in

269

(* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il

270

faut imposer que les outputs dépendent des asserts pour identifier que les

271

fcn calls des asserts sont évalués avant le noeuds *)

272


273

(* (\* In order to introduce dependencies between assert expressions and the node, *)

274

(* we build an artificial dependency between node output and each assert *)

275

(* expr. While these are not valid equations, they should properly propage in *)

276

(* function add_eq_dependencies *\) *)

277

(* let g = *)

278

(* let output_vars_as_lhs = ISet.elements (node_output_variables n) in *)

279

(* List.fold_left (fun g ae > *)

280

(* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *)

281

(* add_eq_dependencies mems inputs node_vars fake_eq g *)

282

(* ) g n.node_asserts in *)

283

g

284


285

end

286


287

module NodeDep = struct

288


289

module ExprModule =

290

struct

291

type t = expr

292

let compare = compare

293

let hash n = Hashtbl.hash n

294

let equal n1 n2 = n1 = n2

295

end

296


297

module ESet = Set.Make(ExprModule)

298


299

let rec get_expr_calls prednode expr =

300

match expr.expr_desc with

301

 Expr_const _

302

 Expr_ident _ > ESet.empty

303

 Expr_access (e, _)

304

 Expr_power (e, _) > get_expr_calls prednode e

305

 Expr_array t

306

 Expr_tuple t > List.fold_right (fun x set > ESet.union (get_expr_calls prednode x) set) t ESet.empty

307

 Expr_merge (_,hl) > List.fold_right (fun (_,h) set > ESet.union (get_expr_calls prednode h) set) hl ESet.empty

308

 Expr_fby (e1,e2)

309

 Expr_arrow (e1,e2) > ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)

310

 Expr_ite (c, t, e) > ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))

311

 Expr_pre e

312

 Expr_when (e,_,_) > get_expr_calls prednode e

313

 Expr_appl (id,e, _) >

314

if not (Basic_library.is_expr_internal_fun expr) && prednode id

315

then ESet.add expr (get_expr_calls prednode e)

316

else (get_expr_calls prednode e)

317


318

let get_callee expr =

319

match expr.expr_desc with

320

 Expr_appl (id, args, _) > Some (id, expr_list_of_expr args)

321

 _ > None

322


323

let get_calls prednode nd =

324

let accu f init objl = List.fold_left (fun accu o > ESet.union accu (f o)) init objl in

325

let get_eq_calls eq = get_expr_calls prednode eq.eq_rhs in

326

let rec get_stmt_calls s =

327

match s with Eq eq > get_eq_calls eq  Aut aut > get_aut_calls aut

328

and get_aut_calls aut =

329

let get_handler_calls h =

330

let get_cond_calls c = accu (fun (_,e,_,_) > get_expr_calls prednode e) ESet.empty c in

331

let until = get_cond_calls h.hand_until in

332

let unless = get_cond_calls h.hand_unless in

333

let calls = ESet.union until unless in

334

let calls = accu get_stmt_calls calls h.hand_stmts in

335

let calls = accu (fun a > get_expr_calls prednode a.assert_expr) calls h.hand_asserts in

336

(* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *)

337

calls

338

in

339

accu get_handler_calls ESet.empty aut.aut_handlers

340

in

341

let eqs, auts = get_node_eqs nd in

342

let deps = accu get_eq_calls ESet.empty eqs in

343

let deps = accu get_aut_calls deps auts in

344

ESet.elements deps

345


346

let dependence_graph prog =

347

let g = new_graph () in

348

let g = List.fold_right

349

(fun td accu > (* for each node we add its dependencies *)

350

match td.top_decl_desc with

351

 Node nd >

352

(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)

353

let accu = add_vertices [nd.node_id] accu in

354

let deps = List.map

355

(fun e > fst (desome (get_callee e)))

356

(get_calls (fun _ > true) nd)

357

in

358

(* Adding assert expressions deps *)

359

let deps_asserts =

360

let prednode = (fun _ > true) in (* what is this about? *)

361

List.map

362

(fun e > fst (desome (get_callee e)))

363

(ESet.elements

364

(List.fold_left

365

(fun accu assert_expr > ESet.union accu (get_expr_calls prednode assert_expr))

366

ESet.empty

367

(List.map (fun _assert > _assert.assert_expr) nd.node_asserts)

368

)

369

)

370

in

371

(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *)

372

add_edges [nd.node_id] (deps@deps_asserts) accu

373

 _ > assert false (* should not happen *)

374


375

) prog g in

376

g

377


378

(* keep subgraph of [gr] consisting of nodes accessible from node [v] *)

379

let slice_graph gr v =

380

begin

381

let gr' = new_graph () in

382

IdentDepGraph.add_vertex gr' v;

383

Bfs.iter_component (fun v > IdentDepGraph.iter_succ (fun s > IdentDepGraph.add_vertex gr' s; IdentDepGraph.add_edge gr' v s) gr v) gr v;

384

gr'

385

end

386


387

let rec filter_static_inputs inputs args =

388

match inputs, args with

389

 [] , [] > []

390

 v::vq, a::aq > if v.var_dec_const && Types.is_dimension_type v.var_type then (dimension_of_expr a) :: filter_static_inputs vq aq else filter_static_inputs vq aq

391

 _ > assert false

392


393

let compute_generic_calls prog =

394

List.iter

395

(fun td >

396

match td.top_decl_desc with

397

 Node nd >

398

let prednode n = is_generic_node (Hashtbl.find node_table n) in

399

nd.node_gencalls < get_calls prednode nd

400

 _ > ()

401


402

) prog

403


404

end

405


406


407

module CycleDetection = struct

408


409

(*  Look for cycles in a dependency graph *)

410

module Cycles = Graph.Components.Make (IdentDepGraph)

411


412

let mk_copy_var n id =

413

let used name =

414

(List.exists (fun v > v.var_id = name) n.node_locals)

415

 (List.exists (fun v > v.var_id = name) n.node_inputs)

416

 (List.exists (fun v > v.var_id = name) n.node_outputs)

417

in mk_new_name used id

418


419

let mk_copy_eq n var =

420

let var_decl = get_node_var var n in

421

let cp_var = mk_copy_var n var in

422

let expr =

423

{ expr_tag = Utils.new_tag ();

424

expr_desc = Expr_ident var;

425

expr_type = var_decl.var_type;

426

expr_clock = var_decl.var_clock;

427

expr_delay = Delay.new_var ();

428

expr_annot = None;

429

expr_loc = var_decl.var_loc } in

430

{ var_decl with var_id = cp_var; var_orig = false },

431

mkeq var_decl.var_loc ([cp_var], expr)

432


433

let wrong_partition g partition =

434

match partition with

435

 [id] > IdentDepGraph.mem_edge g id id

436

 _::_::_ > true

437

 [] > assert false

438


439

(* Checks that the dependency graph [g] does not contain a cycle. Raises

440

[Cycle partition] if the succession of dependencies [partition] forms a cycle *)

441

let check_cycles g =

442

let scc_l = Cycles.scc_list g in

443

let algebraic_loops = List.filter (wrong_partition g) scc_l in

444

if List.length algebraic_loops > 0 then

445

raise (Error (DataCycle algebraic_loops))

446

(* We extract a hint to resolve the cycle: for each variable in the cycle

447

which is defined by a call, we return the name of the node call and

448

its specific id *)

449


450

(* Creates the subgraph of [g] restricted to vertices and edges in partition *)

451

let copy_partition g partition =

452

let copy_g = IdentDepGraph.create () in

453

IdentDepGraph.iter_edges

454

(fun src tgt >

455

if List.mem src partition && List.mem tgt partition

456

then IdentDepGraph.add_edge copy_g src tgt)

457

g

458


459


460

(* Breaks dependency cycles in a graph [g] by inserting aux variables.

461

[head] is a head of a nontrivial scc of [g].

462

In Lustre, this is legal only for mem/mem cycles *)

463

let break_cycle head cp_head g =

464

let succs = IdentDepGraph.succ g head in

465

IdentDepGraph.add_edge g head cp_head;

466

IdentDepGraph.add_edge g cp_head (ExprDep.mk_read_var head);

467

List.iter

468

(fun s >

469

IdentDepGraph.remove_edge g head s;

470

IdentDepGraph.add_edge g s cp_head)

471

succs

472


473

(* Breaks cycles of the dependency graph [g] of memory variables [mems]

474

belonging in node [node]. Returns:

475

 a list of new auxiliary variable declarations

476

 a list of new equations

477

 a modified acyclic version of [g]

478

*)

479

let break_cycles node mems g =

480

let eqs , auts = get_node_eqs node in

481

assert (auts = []); (* TODO: check: For the moment we assume that auts are expanded by now *)

482

let (mem_eqs, non_mem_eqs) = List.partition (fun eq > List.exists (fun v > ISet.mem v mems) eq.eq_lhs) eqs in

483

let rec break vdecls mem_eqs g =

484

let scc_l = Cycles.scc_list g in

485

let wrong = List.filter (wrong_partition g) scc_l in

486

match wrong with

487

 [] > (vdecls, non_mem_eqs@mem_eqs, g)

488

 [head]::_ >

489

begin

490

IdentDepGraph.remove_edge g head head;

491

break vdecls mem_eqs g

492

end

493

 (head::part)::_ >

494

begin

495

let vdecl_cp_head, cp_eq = mk_copy_eq node head in

496

let pvar v = List.mem v part in

497

let fvar v = if v = head then vdecl_cp_head.var_id else v in

498

let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in

499

break_cycle head vdecl_cp_head.var_id g;

500

break (vdecl_cp_head::vdecls) (cp_eq::mem_eqs') g

501

end

502

 _ > assert false

503

in break [] mem_eqs g

504


505

end

506


507

(* Module used to compute static disjunction of variables based upon their clocks. *)

508

module Disjunction =

509

struct

510

module ClockedIdentModule =

511

struct

512

type t = var_decl

513

let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock

514

let compare v1 v2 = compare (root_branch v2, v2.var_id) (root_branch v1, v1.var_id)

515

end

516


517

module CISet = Set.Make(ClockedIdentModule)

518


519

(* map: var > list of disjoint vars, sorted in increasing branch length order,

520

maybe removing shorter branches *)

521

type disjoint_map = (ident, CISet.t) Hashtbl.t

522


523

let pp_ciset fmt t =

524

begin

525

Format.fprintf fmt "{@ ";

526

CISet.iter (fun s > Format.fprintf fmt "%a@ " Printers.pp_var_name s) t;

527

Format.fprintf fmt "}@."

528

end

529


530

let clock_disjoint_map vdecls =

531

let map = Hashtbl.create 23 in

532

begin

533

List.iter

534

(fun v1 > let disj_v1 =

535

List.fold_left

536

(fun res v2 > if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res)

537

CISet.empty

538

vdecls in

539

(* disjoint vdecls are stored in increasing branch length order *)

540

Hashtbl.add map v1.var_id disj_v1)

541

vdecls;

542

(map : disjoint_map)

543

end

544


545

(* merge variables [v] and [v'] in disjunction [map]. Then:

546

 the mapping v' becomes v' > (map v) inter (map v')

547

 the mapping v > ... then disappears

548

 other mappings become x > (map x) \ (if v in x then v else v')

549

*)

550

let merge_in_disjoint_map map v v' =

551

begin

552

Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id));

553

Hashtbl.remove map v.var_id;

554

Hashtbl.iter (fun x map_x > Hashtbl.replace map x (CISet.remove (if CISet.mem v map_x then v else v') map_x)) map;

555

end

556


557

(* replace variable [v] by [v'] in disjunction [map].

558

[v'] is a dead variable. Then:

559

 the mapping v' becomes v' > (map v)

560

 the mapping v > ... then disappears

561

 all mappings become x > ((map x) \ { v}) union ({v'} if v in map x)

562

*)

563

let replace_in_disjoint_map map v v' =

564

begin

565

Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id);

566

Hashtbl.remove map v.var_id;

567

Hashtbl.iter (fun x mapx > Hashtbl.replace map x (if CISet.mem v mapx then CISet.add v' (CISet.remove v mapx) else CISet.remove v' mapx)) map;

568

end

569


570

(* remove variable [v] in disjunction [map]. Then:

571

 the mapping v > ... then disappears

572

 all mappings become x > (map x) \ { v}

573

*)

574

let remove_in_disjoint_map map v =

575

begin

576

Hashtbl.remove map v.var_id;

577

Hashtbl.iter (fun x mapx > Hashtbl.replace map x (CISet.remove v mapx)) map;

578

end

579


580

let pp_disjoint_map fmt map =

581

begin

582

Format.fprintf fmt "{ /* disjoint map */@.";

583

Hashtbl.iter (fun k v > Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;

584

Format.fprintf fmt "}@."

585

end

586

end

587


588


589

let pp_dep_graph fmt g =

590

begin

591

Format.fprintf fmt "{ /* graph */@.";

592

IdentDepGraph.iter_edges (fun s t > Format.fprintf fmt "%s > %s@." s t) g;

593

Format.fprintf fmt "}@."

594

end

595


596

let pp_error fmt err =

597

match err with

598

 NodeCycle trace >

599

Format.fprintf fmt "Causality error, cyclic node calls:@ @[<v 0>%a@]@ "

600

(fprintf_list ~sep:",@ " Format.pp_print_string) trace

601

 DataCycle traces > (

602

Format.fprintf fmt "Causality error, cyclic data dependencies:@ @[<v 0>%a@]@ "

603

(fprintf_list ~sep:";@ "

604

(fun fmt trace >

605

Format.fprintf fmt "@[<v 0>{%a}@]"

606

(fprintf_list ~sep:",@ " Format.pp_print_string)

607

trace

608

)) traces

609

)

610


611

(* Merges elements of graph [g2] into graph [g1] *)

612

let merge_with g1 g2 =

613

begin

614

IdentDepGraph.iter_vertex (fun v > IdentDepGraph.add_vertex g1 v) g2;

615

IdentDepGraph.iter_edges (fun s t > IdentDepGraph.add_edge g1 s t) g2

616

end

617


618

let world = "!!_world"

619


620

let add_external_dependency outputs mems g =

621

begin

622

IdentDepGraph.add_vertex g world;

623

ISet.iter (fun o > IdentDepGraph.add_edge g world o) outputs;

624

ISet.iter (fun m > IdentDepGraph.add_edge g world m) mems;

625

end

626


627

let global_dependency node =

628

let mems = ExprDep.node_memory_variables node in

629

let inputs =

630

ISet.union

631

(ExprDep.node_input_variables node)

632

(ExprDep.node_constant_variables node) in

633

let outputs = ExprDep.node_output_variables node in

634

let node_vars = ExprDep.node_variables node in

635

let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in

636

(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;

637

Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)

638

try

639

CycleDetection.check_cycles g_non_mems;

640

let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in

641

(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*)

642

begin

643

merge_with g_non_mems g_mems';

644

add_external_dependency outputs mems g_non_mems;

645

{ node with node_stmts = List.map (fun eq > Eq eq) eqs'; node_locals = vdecls'@node.node_locals },

646

g_non_mems

647

end

648

with Error (DataCycle _ as exc) > (

649

raise (Error (exc))

650

)

651


652

(* A module to sort dependencies among local variables when relying on clocked declarations *)

653

module VarClockDep =

654

struct

655

let rec get_clock_dep ck =

656

match ck.Clocks.cdesc with

657

 Clocks.Con (ck ,c ,l) > l::(get_clock_dep ck)

658

 Clocks.Clink ck'

659

 Clocks.Ccarrying (_, ck') > get_clock_dep ck'

660

 _ > []

661


662

let sort locals =

663

let g = new_graph () in

664

let g = List.fold_left (

665

fun g var_decl >

666

let deps = get_clock_dep var_decl.var_clock in

667

add_edges [var_decl.var_id] deps g

668

) g locals

669

in

670

let sorted, no_deps =

671

TopologicalDepGraph.fold (fun vid (accu, remaining) > (

672

let select v = v.var_id = vid in

673

let selected, not_selected = List.partition select remaining in

674

selected@accu, not_selected

675

)) g ([],locals)

676

in

677

no_deps @ sorted

678


679

end

680


681

(* Local Variables: *)

682

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

683

(* End: *)
