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 LustreSpec

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

module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule)

32

(*module DotGraph = Graphviz.Dot (IdentDepGraph)*)

33

module Bfs = Traverse.Bfs (IdentDepGraph)

34


35

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

36

by duplication of some mem vars into local node vars.

37

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

38

nonmem variables are:

39

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

40

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

41

 outputs: decoupled from mems, if necessary

42

 locals

43

 instance vars (fake vars): simplify causality analysis

44


45

global constants are not part of the dependency graph.

46


47

no_mem' = combinational(no_mem, mem);

48

=> (mem > no_mem' > no_mem)

49


50

mem' = pre(no_mem, mem);

51

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

52


53

Global roadmap:

54

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

55

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

56

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

57

 check cycles in g'

58

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

59

 insert g' into g

60

 return g

61

*)

62


63

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

64

let is_graph_root v g =

65

IdentDepGraph.in_degree g v = 0

66


67

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

68

let graph_roots g =

69

IdentDepGraph.fold_vertex

70

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

71

g []

72


73

let add_edges src tgt g =

74

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

75

List.iter

76

(fun s >

77

List.iter

78

(fun t > IdentDepGraph.add_edge g s t)

79

tgt)

80

src;

81

g

82


83

let add_vertices vtc g =

84

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

85

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

86

g

87


88

let new_graph () =

89

IdentDepGraph.create ()

90


91

module ExprDep = struct

92


93

let instance_var_cpt = ref 0

94


95

(* read vars represent input/mem readonly vars,

96

they are not part of the program/schedule,

97

as they are not assigned,

98

but used to compute useless inputs/mems.

99

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

100

let mk_read_var id =

101

Format.sprintf "#%s" id

102


103

(* instance vars represent node instance calls,

104

they are not part of the program/schedule,

105

but used to simplify causality analysis

106

*)

107

let mk_instance_var id =

108

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

109


110

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

111


112

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

113


114

let is_ghost_var v = is_instance_var v  is_read_var v

115


116

let undo_read_var id =

117

assert (is_read_var id);

118

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

119


120

let undo_instance_var id =

121

assert (is_instance_var id);

122

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

123


124

let eq_memory_variables mems eq =

125

let rec match_mem lhs rhs mems =

126

match rhs.expr_desc with

127

 Expr_fby _

128

 Expr_pre _ > List.fold_right ISet.add lhs mems

129

 Expr_tuple tl >

130

let lhs' = (transpose_list [lhs]) in

131

List.fold_right2 match_mem lhs' tl mems

132

 _ > mems in

133

match_mem eq.eq_lhs eq.eq_rhs mems

134


135

let node_memory_variables nd =

136

List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)

137


138

let node_input_variables nd =

139

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

140


141

let node_local_variables nd =

142

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

143


144

let node_constant_variables nd =

145

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

146


147

let node_output_variables nd =

148

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

149


150

let node_auxiliary_variables nd =

151

ISet.diff (node_local_variables nd) (node_memory_variables nd)

152


153

let node_variables nd =

154

let inputs = node_input_variables nd in

155

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

156

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

157


158

(* computes the equivalence relation relating variables

159

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

160

of class representatives *)

161

let node_eq_equiv nd =

162

let eq_equiv = Hashtbl.create 23 in

163

List.iter (fun eq >

164

let first = List.hd eq.eq_lhs in

165

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

166

)

167

(get_node_eqs nd);

168

eq_equiv

169


170

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

171

(* filled with variable [v] *)

172

let adjust_tuple v expr =

173

match expr.expr_type.Types.tdesc with

174

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

175

 _ > [v]

176


177


178

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

179

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

180

(* mem/mem in g' *)

181

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

182

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

183

g')

184

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

185

g')

186

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

187

g')

188

 (true , true ) > (g,

189

add_edges [x] lhs g')

190

*)

191

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

192

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

193

if is_instance_var x  ISet.mem x node_vars then

194

if ISet.mem x mems

195

then

196

let g = add_edges lhs [mk_read_var x] g in

197

if lhs_is_mem

198

then

199

(g, add_edges [x] lhs g')

200

else

201

(add_edges [x] lhs g, g')

202

else

203

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

204

(add_edges lhs [x] g, g')

205

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

206

in

207

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

208

let rec add_clock lhs_is_mem lhs ck g =

209

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

210

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

211

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

212

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

213

 _ > g

214

in

215

let rec add_dep lhs_is_mem lhs rhs g =

216

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

217

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

218

let mashup_appl_dependencies f e g =

219

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

220

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

221

(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g)

222

in

223

match rhs.expr_desc with

224

 Expr_const _ > g

225

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

226

 Expr_pre e > add_dep true lhs e g

227

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

228

 Expr_access (e1, d)

229

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

230

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

231

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

232

 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)

233

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

234

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

235

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

236

 Expr_appl (f, e, None) >

237

if Basic_library.is_expr_internal_fun rhs

238

(* tuple componentwise dependency for internal operators *)

239

then

240

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

241

(* mashed up dependency for userdefined operators *)

242

else

243

mashup_appl_dependencies f e g

244

 Expr_appl (f, e, Some c) >

245

mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)

246

in

247

let g =

248

List.fold_left

249

(fun g lhs >

250

if ISet.mem lhs mems then

251

add_vertices [lhs; mk_read_var lhs] g

252

else

253

add_vertices [lhs] g

254

)

255

g eq.eq_lhs

256

in

257

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

258


259


260

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

261

let dependence_graph mems inputs node_vars n =

262

instance_var_cpt := 0;

263

let g = new_graph (), new_graph () in

264

(* Basic dependencies *)

265

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

266

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

267

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

268

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

269


270

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

271

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

272

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

273

(* function add_eq_dependencies *\) *)

274

(* let g = *)

275

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

276

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

277

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

278

(* add_eq_dependencies mems inputs node_vars fake_eq g *)

279

(* ) g n.node_asserts in *)

280

g

281


282

end

283


284

module NodeDep = struct

285


286

module ExprModule =

287

struct

288

type t = expr

289

let compare = compare

290

let hash n = Hashtbl.hash n

291

let equal n1 n2 = n1 = n2

292

end

293


294

module ESet = Set.Make(ExprModule)

295


296

let rec get_expr_calls prednode expr =

297

match expr.expr_desc with

298

 Expr_const _

299

 Expr_ident _ > ESet.empty

300

 Expr_access (e, _)

301

 Expr_power (e, _) > get_expr_calls prednode e

302

 Expr_array t

303

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

304

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

305

 Expr_fby (e1,e2)

306

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

307

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

308

 Expr_pre e

309

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

310

 Expr_appl (id,e, _) >

311

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

312

then ESet.add expr (get_expr_calls prednode e)

313

else (get_expr_calls prednode e)

314


315

let get_callee expr =

316

match expr.expr_desc with

317

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

318

 _ > None

319


320

let get_calls prednode eqs =

321

let deps =

322

List.fold_left

323

(fun accu eq > ESet.union accu (get_expr_calls prednode eq.eq_rhs))

324

ESet.empty

325

eqs in

326

ESet.elements deps

327


328

let dependence_graph prog =

329

let g = new_graph () in

330

let g = List.fold_right

331

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

332

match td.top_decl_desc with

333

 Node nd >

334

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

335

let accu = add_vertices [nd.node_id] accu in

336

let deps = List.map

337

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

338

(get_calls (fun _ > true) (get_node_eqs nd))

339

in

340

(* Adding assert expressions deps *)

341

let deps_asserts =

342

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

343

List.map

344

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

345

(ESet.elements

346

(List.fold_left

347

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

348

ESet.empty

349

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

350

)

351

)

352

in

353

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

354

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

355

 _ > assert false (* should not happen *)

356


357

) prog g in

358

g

359


360

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

361

let slice_graph gr v =

362

begin

363

let gr' = new_graph () in

364

IdentDepGraph.add_vertex gr' v;

365

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;

366

gr'

367

end

368


369

let rec filter_static_inputs inputs args =

370

match inputs, args with

371

 [] , [] > []

372

 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

373

 _ > assert false

374


375

let compute_generic_calls prog =

376

List.iter

377

(fun td >

378

match td.top_decl_desc with

379

 Node nd >

380

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

381

nd.node_gencalls < get_calls prednode (get_node_eqs nd)

382

 _ > ()

383


384

) prog

385


386

end

387


388


389

module CycleDetection = struct

390


391

(*  Look for cycles in a dependency graph *)

392

module Cycles = Graph.Components.Make (IdentDepGraph)

393


394

let mk_copy_var n id =

395

let used name =

396

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

397

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

398

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

399

in mk_new_name used id

400


401

let mk_copy_eq n var =

402

let var_decl = get_node_var var n in

403

let cp_var = mk_copy_var n var in

404

let expr =

405

{ expr_tag = Utils.new_tag ();

406

expr_desc = Expr_ident var;

407

expr_type = var_decl.var_type;

408

expr_clock = var_decl.var_clock;

409

expr_delay = Delay.new_var ();

410

expr_annot = None;

411

expr_loc = var_decl.var_loc } in

412

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

413

mkeq var_decl.var_loc ([cp_var], expr)

414


415

let wrong_partition g partition =

416

match partition with

417

 [id] > IdentDepGraph.mem_edge g id id

418

 _::_::_ > true

419

 [] > assert false

420


421

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

422

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

423

let check_cycles g =

424

let scc_l = Cycles.scc_list g in

425

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

426

if List.length algebraic_loops > 0 then

427

raise (Error (DataCycle algebraic_loops))

428

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

429

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

430

its specific id *)

431


432

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

433

let copy_partition g partition =

434

let copy_g = IdentDepGraph.create () in

435

IdentDepGraph.iter_edges

436

(fun src tgt >

437

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

438

then IdentDepGraph.add_edge copy_g src tgt)

439

g

440


441


442

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

443

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

444

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

445

let break_cycle head cp_head g =

446

let succs = IdentDepGraph.succ g head in

447

IdentDepGraph.add_edge g head cp_head;

448

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

449

List.iter

450

(fun s >

451

IdentDepGraph.remove_edge g head s;

452

IdentDepGraph.add_edge g s cp_head)

453

succs

454


455

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

456

belonging in node [node]. Returns:

457

 a list of new auxiliary variable declarations

458

 a list of new equations

459

 a modified acyclic version of [g]

460

*)

461

let break_cycles node mems g =

462

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

463

let rec break vdecls mem_eqs g =

464

let scc_l = Cycles.scc_list g in

465

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

466

match wrong with

467

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

468

 [head]::_ >

469

begin

470

IdentDepGraph.remove_edge g head head;

471

break vdecls mem_eqs g

472

end

473

 (head::part)::_ >

474

begin

475

let vdecl_cp_head, cp_eq = mk_copy_eq node head in

476

let pvar v = List.mem v part in

477

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

478

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

479

break_cycle head vdecl_cp_head.var_id g;

480

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

481

end

482

 _ > assert false

483

in break [] mem_eqs g

484


485

end

486


487

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

488

module Disjunction =

489

struct

490

module ClockedIdentModule =

491

struct

492

type t = var_decl

493

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

494

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

495

end

496


497

module CISet = Set.Make(ClockedIdentModule)

498


499

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

500

maybe removing shorter branches *)

501

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

502


503

let pp_ciset fmt t =

504

begin

505

Format.fprintf fmt "{@ ";

506

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

507

Format.fprintf fmt "}@."

508

end

509


510

let clock_disjoint_map vdecls =

511

let map = Hashtbl.create 23 in

512

begin

513

List.iter

514

(fun v1 > let disj_v1 =

515

List.fold_left

516

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

517

CISet.empty

518

vdecls in

519

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

520

Hashtbl.add map v1.var_id disj_v1)

521

vdecls;

522

(map : disjoint_map)

523

end

524


525

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

526

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

527

 the mapping v > ... then disappears

528

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

529

*)

530

let merge_in_disjoint_map map v v' =

531

begin

532

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

533

Hashtbl.remove map v.var_id;

534

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;

535

end

536


537

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

538

[v'] is a dead variable. Then:

539

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

540

 the mapping v > ... then disappears

541

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

542

*)

543

let replace_in_disjoint_map map v v' =

544

begin

545

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

546

Hashtbl.remove map v.var_id;

547

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;

548

end

549


550

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

551

 the mapping v > ... then disappears

552

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

553

*)

554

let remove_in_disjoint_map map v =

555

begin

556

Hashtbl.remove map v.var_id;

557

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

558

end

559


560

let pp_disjoint_map fmt map =

561

begin

562

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

563

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

564

Format.fprintf fmt "}@."

565

end

566

end

567


568


569

let pp_dep_graph fmt g =

570

begin

571

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

572

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

573

Format.fprintf fmt "}@."

574

end

575


576

let pp_error fmt err =

577

match err with

578

 NodeCycle trace >

579

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

580

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

581

 DataCycle traces > (

582

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

583

(fprintf_list ~sep:";@ "

584

(fun fmt trace >

585

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

586

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

587

trace

588

)) traces

589

)

590


591

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

592

let merge_with g1 g2 =

593

begin

594

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

595

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

596

end

597


598

let world = "!!_world"

599


600

let add_external_dependency outputs mems g =

601

begin

602

IdentDepGraph.add_vertex g world;

603

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

604

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

605

end

606


607

let global_dependency node =

608

let mems = ExprDep.node_memory_variables node in

609

let inputs =

610

ISet.union

611

(ExprDep.node_input_variables node)

612

(ExprDep.node_constant_variables node) in

613

let outputs = ExprDep.node_output_variables node in

614

let node_vars = ExprDep.node_variables node in

615

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

616

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

617

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

618

try

619

CycleDetection.check_cycles g_non_mems;

620

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

621

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

622

begin

623

merge_with g_non_mems g_mems';

624

add_external_dependency outputs mems g_non_mems;

625

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

626

g_non_mems

627

end

628

with Error (DataCycle _ as exc) > (

629

raise (Error (exc))

630

)

631


632

(* Local Variables: *)

633

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

634

(* End: *)
