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

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

32

module TopologicalDepGraph = Topological.Make(IdentDepGraph)

33


34

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

35

module Bfs = Traverse.Bfs (IdentDepGraph)

36


37

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

38

by duplication of some mem vars into local node vars.

39

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

40

nonmem variables are:

41

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

42

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

43

 outputs: decoupled from mems, if necessary

44

 locals

45

 instance vars (fake vars): simplify causality analysis

46


47

global constants are not part of the dependency graph.

48


49

no_mem' = combinational(no_mem, mem);

50

=> (mem > no_mem' > no_mem)

51


52

mem' = pre(no_mem, mem);

53

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

54


55

Global roadmap:

56

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

57

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

58

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

59

 check cycles in g'

60

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

61

 insert g' into g

62

 return g

63

*)

64


65

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

66

let is_graph_root v g =

67

IdentDepGraph.in_degree g v = 0

68


69

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

70

let graph_roots g =

71

IdentDepGraph.fold_vertex

72

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

73

g []

74


75

let add_edges src tgt g =

76

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

77

List.iter

78

(fun s >

79

List.iter

80

(fun t > IdentDepGraph.add_edge g s t)

81

tgt)

82

src;

83

g

84


85

let add_vertices vtc g =

86

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

87

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

88

g

89


90

let new_graph () =

91

IdentDepGraph.create ()

92


93


94

module ExprDep = struct

95

let get_node_eqs nd =

96

let eqs, auts = get_node_eqs nd in

97

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

98

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

99

eqs

100


101

let instance_var_cpt = ref 0

102


103

(* read vars represent input/mem readonly vars,

104

they are not part of the program/schedule,

105

as they are not assigned,

106

but used to compute useless inputs/mems.

107

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

108

let mk_read_var id =

109

Format.sprintf "#%s" id

110


111

(* instance vars represent node instance calls,

112

they are not part of the program/schedule,

113

but used to simplify causality analysis

114

*)

115

let mk_instance_var id =

116

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

117


118

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

119


120

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

121


122

let is_ghost_var v = is_instance_var v  is_read_var v

123


124

let undo_read_var id =

125

assert (is_read_var id);

126

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

127


128

let undo_instance_var id =

129

assert (is_instance_var id);

130

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

131


132

let eq_memory_variables mems eq =

133

let rec match_mem lhs rhs mems =

134

match rhs.expr_desc with

135

 Expr_fby _

136

 Expr_pre _ > List.fold_right ISet.add lhs mems

137

 Expr_tuple tl >

138

let lhs' = (transpose_list [lhs]) in

139

List.fold_right2 match_mem lhs' tl mems

140

 _ > mems in

141

match_mem eq.eq_lhs eq.eq_rhs mems

142


143

let node_memory_variables nd =

144

List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)

145


146

let node_input_variables nd =

147

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

148


149

let node_local_variables nd =

150

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

151


152

let node_constant_variables nd =

153

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

154


155

let node_output_variables nd =

156

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

157


158

let node_auxiliary_variables nd =

159

ISet.diff (node_local_variables nd) (node_memory_variables nd)

160


161

let node_variables nd =

162

let inputs = node_input_variables nd in

163

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

164

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

165


166

(* computes the equivalence relation relating variables

167

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

168

of class representatives *)

169

let node_eq_equiv nd =

170

let eq_equiv = Hashtbl.create 23 in

171

List.iter (fun eq >

172

let first = List.hd eq.eq_lhs in

173

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

174

)

175

(get_node_eqs nd);

176

eq_equiv

177


178

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

179

(* filled with variable [v] *)

180

let adjust_tuple v expr =

181

match expr.expr_type.Types.tdesc with

182

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

183

 _ > [v]

184


185


186

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

187

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

188

(* mem/mem in g' *)

189

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

190

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

191

g')

192

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

193

g')

194

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

195

g')

196

 (true , true ) > (g,

197

add_edges [x] lhs g')

198

*)

199

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

200

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

201

if is_instance_var x  ISet.mem x node_vars then

202

if ISet.mem x mems

203

then

204

let g = add_edges lhs [mk_read_var x] g in

205

if lhs_is_mem

206

then

207

(g, add_edges [x] lhs g')

208

else

209

(add_edges [x] lhs g, g')

210

else

211

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

212

(add_edges lhs [x] g, g')

213

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

214

in

215

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

216

let rec add_clock lhs_is_mem lhs ck g =

217

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

218

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

219

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

220

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

221

 _ > g

222

in

223

let rec add_dep lhs_is_mem lhs rhs g =

224

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

225

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

226

let mashup_appl_dependencies f e g =

227

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

228

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

229

(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g)

230

in

231

match rhs.expr_desc with

232

 Expr_const _ > g

233

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

234

 Expr_pre e > add_dep true lhs e g

235

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

236

 Expr_access (e1, d)

237

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

238

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

239

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

240

 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)

241

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

242

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

243

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

244

 Expr_appl (f, e, None) >

245

if Basic_library.is_expr_internal_fun rhs

246

(* tuple componentwise dependency for internal operators *)

247

then

248

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

249

(* mashed up dependency for userdefined operators *)

250

else

251

mashup_appl_dependencies f e g

252

 Expr_appl (f, e, Some c) >

253

mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)

254

in

255

let g =

256

List.fold_left

257

(fun g lhs >

258

if ISet.mem lhs mems then

259

add_vertices [lhs; mk_read_var lhs] g

260

else

261

add_vertices [lhs] g

262

)

263

g eq.eq_lhs

264

in

265

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

266


267


268

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

269

let dependence_graph mems inputs node_vars n =

270

instance_var_cpt := 0;

271

let g = new_graph (), new_graph () in

272

(* Basic dependencies *)

273

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

274

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

275

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

276

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

277


278

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

279

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

280

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

281

(* function add_eq_dependencies *\) *)

282

(* let g = *)

283

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

284

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

285

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

286

(* add_eq_dependencies mems inputs node_vars fake_eq g *)

287

(* ) g n.node_asserts in *)

288

g

289


290

end

291


292

module NodeDep = struct

293


294

module ExprModule =

295

struct

296

type t = expr

297

let compare = compare

298

let hash n = Hashtbl.hash n

299

let equal n1 n2 = n1 = n2

300

end

301


302

module ESet = Set.Make(ExprModule)

303


304

let rec get_expr_calls prednode expr =

305

match expr.expr_desc with

306

 Expr_const _

307

 Expr_ident _ > ESet.empty

308

 Expr_access (e, _)

309

 Expr_power (e, _) > get_expr_calls prednode e

310

 Expr_array t

311

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

312

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

313

 Expr_fby (e1,e2)

314

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

315

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

316

 Expr_pre e

317

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

318

 Expr_appl (id,e, _) >

319

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

320

then ESet.add expr (get_expr_calls prednode e)

321

else (get_expr_calls prednode e)

322


323

let get_callee expr =

324

match expr.expr_desc with

325

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

326

 _ > None

327


328

let get_calls prednode nd =

329

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

330

let get_eq_calls eq = get_expr_calls prednode eq.eq_rhs in

331

let rec get_stmt_calls s =

332

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

333

and get_aut_calls aut =

334

let get_handler_calls h =

335

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

336

let until = get_cond_calls h.hand_until in

337

let unless = get_cond_calls h.hand_unless in

338

let calls = ESet.union until unless in

339

let calls = accu get_stmt_calls calls h.hand_stmts in

340

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

341

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

342

calls

343

in

344

accu get_handler_calls ESet.empty aut.aut_handlers

345

in

346

let eqs, auts = get_node_eqs nd in

347

let deps = accu get_eq_calls ESet.empty eqs in

348

let deps = accu get_aut_calls deps auts in

349

ESet.elements deps

350


351

let dependence_graph prog =

352

let g = new_graph () in

353

let g = List.fold_right

354

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

355

match td.top_decl_desc with

356

 Node nd >

357

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

358

let accu = add_vertices [nd.node_id] accu in

359

let deps = List.map

360

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

361

(get_calls (fun _ > true) nd)

362

in

363

(* Adding assert expressions deps *)

364

let deps_asserts =

365

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

366

List.map

367

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

368

(ESet.elements

369

(List.fold_left

370

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

371

ESet.empty

372

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

373

)

374

)

375

in

376

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

377

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

378

 _ > assert false (* should not happen *)

379


380

) prog g in

381

g

382


383

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

384

let slice_graph gr v =

385

begin

386

let gr' = new_graph () in

387

IdentDepGraph.add_vertex gr' v;

388

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;

389

gr'

390

end

391


392

let rec filter_static_inputs inputs args =

393

match inputs, args with

394

 [] , [] > []

395

 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

396

 _ > assert false

397


398

let compute_generic_calls prog =

399

List.iter

400

(fun td >

401

match td.top_decl_desc with

402

 Node nd >

403

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

404

nd.node_gencalls < get_calls prednode nd

405

 _ > ()

406


407

) prog

408


409

end

410


411


412

module CycleDetection = struct

413


414

(*  Look for cycles in a dependency graph *)

415

module Cycles = Graph.Components.Make (IdentDepGraph)

416


417

let mk_copy_var n id =

418

let used name =

419

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

420

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

421

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

422

in mk_new_name used id

423


424

let mk_copy_eq n var =

425

let var_decl = get_node_var var n in

426

let cp_var = mk_copy_var n var in

427

let expr =

428

{ expr_tag = Utils.new_tag ();

429

expr_desc = Expr_ident var;

430

expr_type = var_decl.var_type;

431

expr_clock = var_decl.var_clock;

432

expr_delay = Delay.new_var ();

433

expr_annot = None;

434

expr_loc = var_decl.var_loc } in

435

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

436

mkeq var_decl.var_loc ([cp_var], expr)

437


438

let wrong_partition g partition =

439

match partition with

440

 [id] > IdentDepGraph.mem_edge g id id

441

 _::_::_ > true

442

 [] > assert false

443


444

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

445

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

446

let check_cycles g =

447

let scc_l = Cycles.scc_list g in

448

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

449

if List.length algebraic_loops > 0 then

450

raise (Error (DataCycle algebraic_loops))

451

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

452

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

453

its specific id *)

454


455

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

456

let copy_partition g partition =

457

let copy_g = IdentDepGraph.create () in

458

IdentDepGraph.iter_edges

459

(fun src tgt >

460

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

461

then IdentDepGraph.add_edge copy_g src tgt)

462

g

463


464


465

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

466

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

467

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

468

let break_cycle head cp_head g =

469

let succs = IdentDepGraph.succ g head in

470

IdentDepGraph.add_edge g head cp_head;

471

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

472

List.iter

473

(fun s >

474

IdentDepGraph.remove_edge g head s;

475

IdentDepGraph.add_edge g s cp_head)

476

succs

477


478

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

479

belonging in node [node]. Returns:

480

 a list of new auxiliary variable declarations

481

 a list of new equations

482

 a modified acyclic version of [g]

483

*)

484

let break_cycles node mems g =

485

let eqs , auts = get_node_eqs node in

486

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

487

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

488

let rec break vdecls mem_eqs g =

489

let scc_l = Cycles.scc_list g in

490

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

491

match wrong with

492

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

493

 [head]::_ >

494

begin

495

IdentDepGraph.remove_edge g head head;

496

break vdecls mem_eqs g

497

end

498

 (head::part)::_ >

499

begin

500

let vdecl_cp_head, cp_eq = mk_copy_eq node head in

501

let pvar v = List.mem v part in

502

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

503

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

504

break_cycle head vdecl_cp_head.var_id g;

505

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

506

end

507

 _ > assert false

508

in break [] mem_eqs g

509


510

end

511


512

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

513

module Disjunction =

514

struct

515

module ClockedIdentModule =

516

struct

517

type t = var_decl

518

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

519

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

520

end

521


522

module CISet = Set.Make(ClockedIdentModule)

523


524

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

525

maybe removing shorter branches *)

526

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

527


528

let pp_ciset fmt t =

529

begin

530

Format.fprintf fmt "{@ ";

531

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

532

Format.fprintf fmt "}@."

533

end

534


535

let clock_disjoint_map vdecls =

536

let map = Hashtbl.create 23 in

537

begin

538

List.iter

539

(fun v1 > let disj_v1 =

540

List.fold_left

541

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

542

CISet.empty

543

vdecls in

544

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

545

Hashtbl.add map v1.var_id disj_v1)

546

vdecls;

547

(map : disjoint_map)

548

end

549


550

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

551

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

552

 the mapping v > ... then disappears

553

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

554

*)

555

let merge_in_disjoint_map map v v' =

556

begin

557

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

558

Hashtbl.remove map v.var_id;

559

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;

560

end

561


562

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

563

[v'] is a dead variable. Then:

564

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

565

 the mapping v > ... then disappears

566

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

567

*)

568

let replace_in_disjoint_map map v v' =

569

begin

570

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

571

Hashtbl.remove map v.var_id;

572

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;

573

end

574


575

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

576

 the mapping v > ... then disappears

577

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

578

*)

579

let remove_in_disjoint_map map v =

580

begin

581

Hashtbl.remove map v.var_id;

582

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

583

end

584


585

let pp_disjoint_map fmt map =

586

begin

587

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

588

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

589

Format.fprintf fmt "}@."

590

end

591

end

592


593


594

let pp_dep_graph fmt g =

595

begin

596

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

597

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

598

Format.fprintf fmt "}@."

599

end

600


601

let pp_error fmt err =

602

match err with

603

 NodeCycle trace >

604

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

605

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

606

 DataCycle traces > (

607

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

608

(fprintf_list ~sep:";@ "

609

(fun fmt trace >

610

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

611

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

612

trace

613

)) traces

614

)

615


616

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

617

let merge_with g1 g2 =

618

begin

619

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

620

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

621

end

622


623

let world = "!!_world"

624


625

let add_external_dependency outputs mems g =

626

begin

627

IdentDepGraph.add_vertex g world;

628

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

629

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

630

end

631


632

let global_dependency node =

633

let mems = ExprDep.node_memory_variables node in

634

let inputs =

635

ISet.union

636

(ExprDep.node_input_variables node)

637

(ExprDep.node_constant_variables node) in

638

let outputs = ExprDep.node_output_variables node in

639

let node_vars = ExprDep.node_variables node in

640

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

641

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

642

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

643

try

644

CycleDetection.check_cycles g_non_mems;

645

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

646

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

647

begin

648

merge_with g_non_mems g_mems';

649

add_external_dependency outputs mems g_non_mems;

650

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

651

g_non_mems

652

end

653

with Error (DataCycle _ as exc) > (

654

raise (Error (exc))

655

)

656


657

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

658

module VarClockDep =

659

struct

660

let rec get_clock_dep ck =

661

match ck.Clocks.cdesc with

662

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

663

 Clocks.Clink ck'

664

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

665

 _ > []

666


667

let sort locals =

668

let g = new_graph () in

669

let g = List.fold_left (

670

fun g var_decl >

671

let deps = get_clock_dep var_decl.var_clock in

672

add_edges [var_decl.var_id] deps g

673

) g locals

674

in

675

let sorted, no_deps =

676

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

677

let select v = v.var_id = vid in

678

let selected, not_selected = List.partition select remaining in

679

selected@accu, not_selected

680

)) g ([],locals)

681

in

682

no_deps @ sorted

683


684

end

685


686

(* Local Variables: *)

687

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

688

(* End: *)
