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

open Format

22


23

type error =

24

 DataCycle of ident list

25

 NodeCycle of ident list

26


27

exception Error of error

28


29


30

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

31

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

32

module Bfs = Traverse.Bfs (IdentDepGraph)

33


34

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

35

by duplication of some mem vars into local node vars.

36

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

37

nonmem variables are:

38

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

39

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

40

 outputs: decoupled from mems, if necessary

41

 locals

42

 instance vars (fake vars): simplify causality analysis

43


44

global constants are not part of the dependency graph.

45


46

no_mem' = combinational(no_mem, mem);

47

=> (mem > no_mem' > no_mem)

48


49

mem' = pre(no_mem, mem);

50

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

51


52

Global roadmap:

53

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

54

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

55

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

56

 check cycles in g'

57

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

58

 insert g' into g

59

 return g

60

*)

61


62

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

63

let is_graph_root v g =

64

IdentDepGraph.in_degree g v = 0

65


66

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

67

let graph_roots g =

68

IdentDepGraph.fold_vertex

69

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

70

g []

71


72

let add_edges src tgt g =

73

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

74

List.iter

75

(fun s >

76

List.iter

77

(fun t > IdentDepGraph.add_edge g s t)

78

tgt)

79

src;

80

g

81


82

let add_vertices vtc g =

83

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

84

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

85

g

86


87

let new_graph () =

88

IdentDepGraph.create ()

89


90

module ExprDep = struct

91


92

let instance_var_cpt = ref 0

93


94

(* read vars represent input/mem readonly vars,

95

they are not part of the program/schedule,

96

as they are not assigned,

97

but used to compute useless inputs/mems.

98

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

99

let mk_read_var id =

100

sprintf "#%s" id

101


102

(* instance vars represent node instance calls,

103

they are not part of the program/schedule,

104

but used to simplify causality analysis

105

*)

106

let mk_instance_var id =

107

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

108


109

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

110


111

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

112


113

let is_ghost_var v = is_instance_var v  is_read_var v

114


115

let undo_read_var id =

116

assert (is_read_var id);

117

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

118


119

let undo_instance_var id =

120

assert (is_instance_var id);

121

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

122


123

let eq_memory_variables mems eq =

124

let rec match_mem lhs rhs mems =

125

match rhs.expr_desc with

126

 Expr_fby _

127

 Expr_pre _ > List.fold_right ISet.add lhs mems

128

 Expr_tuple tl >

129

let lhs' = (transpose_list [lhs]) in

130

List.fold_right2 match_mem lhs' tl mems

131

 _ > mems in

132

match_mem eq.eq_lhs eq.eq_rhs mems

133


134

let node_memory_variables nd =

135

List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)

136


137

let node_input_variables nd =

138

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

139


140

let node_local_variables nd =

141

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

142


143

let node_constant_variables nd =

144

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

145


146

let node_output_variables nd =

147

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

148


149

let node_auxiliary_variables nd =

150

ISet.diff (node_local_variables nd) (node_memory_variables nd)

151


152

let node_variables nd =

153

let inputs = node_input_variables nd in

154

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

155

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

156


157

(* computes the equivalence relation relating variables

158

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

159

of class representatives *)

160

let node_eq_equiv nd =

161

let eq_equiv = Hashtbl.create 23 in

162

List.iter (fun eq >

163

let first = List.hd eq.eq_lhs in

164

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

165

)

166

(get_node_eqs nd);

167

eq_equiv

168


169

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

170

(* filled with variable [v] *)

171

let adjust_tuple v expr =

172

match expr.expr_type.Types.tdesc with

173

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

174

 _ > [v]

175


176


177

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

178

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

179

(* mem/mem in g' *)

180

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

181

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

182

g')

183

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

184

g')

185

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

186

g')

187

 (true , true ) > (g,

188

add_edges [x] lhs g')

189

*)

190

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

191

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

192

if is_instance_var x  ISet.mem x node_vars then

193

if ISet.mem x mems

194

then

195

let g = add_edges lhs [mk_read_var x] g in

196

if lhs_is_mem

197

then

198

(g, add_edges [x] lhs g')

199

else

200

(add_edges [x] lhs g, g')

201

else

202

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

203

(add_edges lhs [x] g, g')

204

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

205

in

206

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

207

let rec add_clock lhs_is_mem lhs ck g =

208

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

209

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

210

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

211

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

212

 _ > g

213

in

214

let rec add_dep lhs_is_mem lhs rhs g =

215

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

216

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

217

let mashup_appl_dependencies f e g =

218

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

219

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

220

(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g)

221

in

222

match rhs.expr_desc with

223

 Expr_const _ > g

224

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

225

 Expr_pre e > add_dep true lhs e g

226

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

227

 Expr_access (e1, d)

228

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

229

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

230

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

231

 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)

232

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

233

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

234

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

235

 Expr_appl (f, e, None) >

236

if Basic_library.is_expr_internal_fun rhs

237

(* tuple componentwise dependency for internal operators *)

238

then

239

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

240

(* mashed up dependency for userdefined operators *)

241

else

242

mashup_appl_dependencies f e g

243

 Expr_appl (f, e, Some c) >

244

mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)

245

in

246

let g =

247

List.fold_left

248

(fun g lhs >

249

if ISet.mem lhs mems then

250

add_vertices [lhs; mk_read_var lhs] g

251

else

252

add_vertices [lhs] g

253

)

254

g eq.eq_lhs

255

in

256

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

257


258


259

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

260

let dependence_graph mems inputs node_vars n =

261

instance_var_cpt := 0;

262

let g = new_graph (), new_graph () in

263

(* Basic dependencies *)

264

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

265

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

266

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

267

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

268


269

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

270

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

271

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

272

(* function add_eq_dependencies *\) *)

273

(* let g = *)

274

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

275

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

276

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

277

(* add_eq_dependencies mems inputs node_vars fake_eq g *)

278

(* ) g n.node_asserts in *)

279

g

280


281

end

282


283

module NodeDep = struct

284


285

module ExprModule =

286

struct

287

type t = expr

288

let compare = compare

289

let hash n = Hashtbl.hash n

290

let equal n1 n2 = n1 = n2

291

end

292


293

module ESet = Set.Make(ExprModule)

294


295

let rec get_expr_calls prednode expr =

296

match expr.expr_desc with

297

 Expr_const _

298

 Expr_ident _ > ESet.empty

299

 Expr_access (e, _)

300

 Expr_power (e, _) > get_expr_calls prednode e

301

 Expr_array t

302

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

303

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

304

 Expr_fby (e1,e2)

305

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

306

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

307

 Expr_pre e

308

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

309

 Expr_appl (id,e, _) >

310

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

311

then ESet.add expr (get_expr_calls prednode e)

312

else (get_expr_calls prednode e)

313


314

let get_callee expr =

315

match expr.expr_desc with

316

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

317

 _ > None

318


319

let get_calls prednode eqs =

320

let deps =

321

List.fold_left

322

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

323

ESet.empty

324

eqs in

325

ESet.elements deps

326


327

let dependence_graph prog =

328

let g = new_graph () in

329

let g = List.fold_right

330

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

331

match td.top_decl_desc with

332

 Node nd >

333

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

334

let accu = add_vertices [nd.node_id] accu in

335

let deps = List.map

336

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

337

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

338

in

339

(* Adding assert expressions deps *)

340

let deps_asserts =

341

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

342

List.map

343

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

344

(ESet.elements

345

(List.fold_left

346

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

347

ESet.empty

348

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

349

)

350

)

351

in

352

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

353

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

354

 _ > assert false (* should not happen *)

355


356

) prog g in

357

g

358


359

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

360

let slice_graph gr v =

361

begin

362

let gr' = new_graph () in

363

IdentDepGraph.add_vertex gr' v;

364

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;

365

gr'

366

end

367


368

let rec filter_static_inputs inputs args =

369

match inputs, args with

370

 [] , [] > []

371

 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

372

 _ > assert false

373


374

let compute_generic_calls prog =

375

List.iter

376

(fun td >

377

match td.top_decl_desc with

378

 Node nd >

379

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

380

nd.node_gencalls < get_calls prednode (get_node_eqs nd)

381

 _ > ()

382


383

) prog

384


385

end

386


387

module CycleDetection = struct

388


389

(*  Look for cycles in a dependency graph *)

390

module Cycles = Graph.Components.Make (IdentDepGraph)

391


392

let mk_copy_var n id =

393

let used name =

394

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

395

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

396

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

397

in mk_new_name used id

398


399

let mk_copy_eq n var =

400

let var_decl = get_node_var var n in

401

let cp_var = mk_copy_var n var in

402

let expr =

403

{ expr_tag = Utils.new_tag ();

404

expr_desc = Expr_ident var;

405

expr_type = var_decl.var_type;

406

expr_clock = var_decl.var_clock;

407

expr_delay = Delay.new_var ();

408

expr_annot = None;

409

expr_loc = var_decl.var_loc } in

410

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

411

mkeq var_decl.var_loc ([cp_var], expr)

412


413

let wrong_partition g partition =

414

match partition with

415

 [id] > IdentDepGraph.mem_edge g id id

416

 _::_::_ > true

417

 [] > assert false

418


419

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

420

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

421

let check_cycles g =

422

let scc_l = Cycles.scc_list g in

423

List.iter (fun partition >

424

if wrong_partition g partition then

425

raise (Error (DataCycle partition))

426

else ()

427

) scc_l

428


429

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

430

let copy_partition g partition =

431

let copy_g = IdentDepGraph.create () in

432

IdentDepGraph.iter_edges

433

(fun src tgt >

434

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

435

then IdentDepGraph.add_edge copy_g src tgt)

436

g

437


438


439

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

440

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

441

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

442

let break_cycle head cp_head g =

443

let succs = IdentDepGraph.succ g head in

444

IdentDepGraph.add_edge g head cp_head;

445

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

446

List.iter

447

(fun s >

448

IdentDepGraph.remove_edge g head s;

449

IdentDepGraph.add_edge g s cp_head)

450

succs

451


452

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

453

belonging in node [node]. Returns:

454

 a list of new auxiliary variable declarations

455

 a list of new equations

456

 a modified acyclic version of [g]

457

*)

458

let break_cycles node mems g =

459

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

460

let rec break vdecls mem_eqs g =

461

let scc_l = Cycles.scc_list g in

462

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

463

match wrong with

464

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

465

 [head]::_ >

466

begin

467

IdentDepGraph.remove_edge g head head;

468

break vdecls mem_eqs g

469

end

470

 (head::part)::_ >

471

begin

472

let vdecl_cp_head, cp_eq = mk_copy_eq node head in

473

let pvar v = List.mem v part in

474

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

475

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

476

break_cycle head vdecl_cp_head.var_id g;

477

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

478

end

479

 _ > assert false

480

in break [] mem_eqs g

481


482

end

483


484

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

485

module Disjunction =

486

struct

487

module ClockedIdentModule =

488

struct

489

type t = var_decl

490

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

491

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

492

end

493


494

module CISet = Set.Make(ClockedIdentModule)

495


496

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

497

maybe removing shorter branches *)

498

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

499


500

let pp_ciset fmt t =

501

begin

502

Format.fprintf fmt "{@ ";

503

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

504

Format.fprintf fmt "}@."

505

end

506


507

let clock_disjoint_map vdecls =

508

let map = Hashtbl.create 23 in

509

begin

510

List.iter

511

(fun v1 > let disj_v1 =

512

List.fold_left

513

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

514

CISet.empty

515

vdecls in

516

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

517

Hashtbl.add map v1.var_id disj_v1)

518

vdecls;

519

(map : disjoint_map)

520

end

521


522

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

523

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

524

 the mapping v > ... then disappears

525

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

526

*)

527

let merge_in_disjoint_map map v v' =

528

begin

529

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

530

Hashtbl.remove map v.var_id;

531

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;

532

end

533


534

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

535

[v'] is a dead variable. Then:

536

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

537

 the mapping v > ... then disappears

538

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

539

*)

540

let replace_in_disjoint_map map v v' =

541

begin

542

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

543

Hashtbl.remove map v.var_id;

544

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;

545

end

546


547

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

548

 the mapping v > ... then disappears

549

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

550

*)

551

let remove_in_disjoint_map map v =

552

begin

553

Hashtbl.remove map v.var_id;

554

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

555

end

556


557

let pp_disjoint_map fmt map =

558

begin

559

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

560

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

561

Format.fprintf fmt "}@."

562

end

563

end

564


565

let pp_dep_graph fmt g =

566

begin

567

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

568

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

569

Format.fprintf fmt "}@."

570

end

571


572

let pp_error fmt err =

573

match err with

574

 DataCycle trace >

575

fprintf fmt "@.Causality error, cyclic data dependencies: %a@."

576

(fprintf_list ~sep:", " pp_print_string) trace

577

 NodeCycle trace >

578

fprintf fmt "@.Causality error, cyclic node calls: %a@."

579

(fprintf_list ~sep:", " pp_print_string) trace

580


581

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

582

let merge_with g1 g2 =

583

begin

584

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

585

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

586

end

587


588

let world = "!!_world"

589


590

let add_external_dependency outputs mems g =

591

begin

592

IdentDepGraph.add_vertex g world;

593

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

594

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

595

end

596


597

let global_dependency node =

598

let mems = ExprDep.node_memory_variables node in

599

let inputs =

600

ISet.union

601

(ExprDep.node_input_variables node)

602

(ExprDep.node_constant_variables node) in

603

let outputs = ExprDep.node_output_variables node in

604

let node_vars = ExprDep.node_variables node in

605

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

606

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

607

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

608

CycleDetection.check_cycles g_non_mems;

609

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

610

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

611

begin

612

merge_with g_non_mems g_mems';

613

add_external_dependency outputs mems g_non_mems;

614

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

615

g_non_mems

616

end

617


618

(* Local Variables: *)

619

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

620

(* End: *)
