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

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

89

let slice_graph gr v =

90

begin

91

let gr' = new_graph () in

92

IdentDepGraph.add_vertex gr' v;

93

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;

94

gr'

95

end

96


97


98

module ExprDep = struct

99

let get_node_eqs nd =

100

let eqs, auts = get_node_eqs nd in

101

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

102

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

103

eqs

104


105

let instance_var_cpt = ref 0

106


107

(* read vars represent input/mem readonly vars,

108

they are not part of the program/schedule,

109

as they are not assigned,

110

but used to compute useless inputs/mems.

111

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

112

let mk_read_var id =

113

Format.sprintf "#%s" id

114


115

(* instance vars represent node instance calls,

116

they are not part of the program/schedule,

117

but used to simplify causality analysis

118

*)

119

let mk_instance_var id =

120

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

121


122

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

123


124

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

125


126

let is_ghost_var v = is_instance_var v  is_read_var v

127


128

let undo_read_var id =

129

assert (is_read_var id);

130

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

131


132

let undo_instance_var id =

133

assert (is_instance_var id);

134

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

135


136

let eq_memory_variables mems eq =

137

let rec match_mem lhs rhs mems =

138

match rhs.expr_desc with

139

 Expr_fby _

140

 Expr_pre _ > List.fold_right ISet.add lhs mems

141

 Expr_tuple tl >

142

let lhs' = (transpose_list [lhs]) in

143

List.fold_right2 match_mem lhs' tl mems

144

 _ > mems in

145

match_mem eq.eq_lhs eq.eq_rhs mems

146


147

let node_memory_variables nd =

148

List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)

149


150

let node_input_variables nd =

151

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

152

(if nd.node_iscontract then

153

nd.node_inputs@nd.node_outputs

154

else

155

nd.node_inputs)

156


157

let node_output_variables nd =

158

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

159

(if nd.node_iscontract then [] else nd.node_outputs)

160


161

let node_local_variables nd =

162

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

163


164

let node_constant_variables nd =

165

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

166


167

let node_auxiliary_variables nd =

168

ISet.diff (node_local_variables nd) (node_memory_variables nd)

169


170

let node_variables nd =

171

let inputs = node_input_variables nd in

172

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

173

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

174


175

(* computes the equivalence relation relating variables

176

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

177

of class representatives *)

178

let eqs_eq_equiv eqs =

179

let eq_equiv = Hashtbl.create 23 in

180

List.iter (fun eq >

181

let first = List.hd eq.eq_lhs in

182

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

183

)

184

eqs;

185

eq_equiv

186


187

let node_eq_equiv nd = eqs_eq_equiv (get_node_eqs nd)

188


189

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

190

(* filled with variable [v] *)

191

let adjust_tuple v expr =

192

match expr.expr_type.Types.tdesc with

193

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

194

 _ > [v]

195


196


197

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

198

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

199

(* mem/mem in g' *)

200

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

201

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

202

g')

203

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

204

g')

205

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

206

g')

207

 (true , true ) > (g,

208

add_edges [x] lhs g')

209

*)

210

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

211

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

212

if is_instance_var x  ISet.mem x node_vars then

213

if ISet.mem x mems

214

then

215

let g = add_edges lhs [mk_read_var x] g in

216

if lhs_is_mem

217

then

218

(g, add_edges [x] lhs g')

219

else

220

(add_edges [x] lhs g, g')

221

else

222

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

223

(add_edges lhs [x] g, g')

224

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

225

in

226

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

227

let rec add_clock lhs_is_mem lhs ck g =

228

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

229

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

230

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

231

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

232

 _ > g

233

in

234

let rec add_dep lhs_is_mem lhs rhs g =

235

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

236

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

237

let mashup_appl_dependencies f e g =

238

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

239

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

240

(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g)

241

in

242

match rhs.expr_desc with

243

 Expr_const _ > g

244

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

245

 Expr_pre e > add_dep true lhs e g

246

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

247

 Expr_access (e1, d)

248

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

249

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

250

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

251

 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)

252

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

253

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

254

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

255

 Expr_appl (f, e, None) >

256

if Basic_library.is_expr_internal_fun rhs

257

(* tuple componentwise dependency for internal operators *)

258

then

259

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

260

(* mashed up dependency for userdefined operators *)

261

else

262

mashup_appl_dependencies f e g

263

 Expr_appl (f, e, Some c) >

264

mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)

265

in

266

let g =

267

List.fold_left

268

(fun g lhs >

269

if ISet.mem lhs mems then

270

add_vertices [lhs; mk_read_var lhs] g

271

else

272

add_vertices [lhs] g

273

)

274

g eq.eq_lhs

275

in

276

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

277


278


279

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

280

let dependence_graph mems inputs node_vars n =

281

instance_var_cpt := 0;

282

let g = new_graph (), new_graph () in

283

(* Basic dependencies *)

284

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

285

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

286

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

287

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

288


289

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

290

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

291

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

292

(* function add_eq_dependencies *\) *)

293

(* let g = *)

294

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

295

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

296

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

297

(* add_eq_dependencies mems inputs node_vars fake_eq g *)

298

(* ) g n.node_asserts in *)

299

g

300


301

end

302


303

module NodeDep = struct

304


305

module ExprModule =

306

struct

307

type t = expr

308

let compare = compare

309

let hash n = Hashtbl.hash n

310

let equal n1 n2 = n1 = n2

311

end

312


313

module ESet = Set.Make(ExprModule)

314


315

let rec get_expr_calls prednode expr =

316

match expr.expr_desc with

317

 Expr_const _

318

 Expr_ident _ > ESet.empty

319

 Expr_access (e, _)

320

 Expr_power (e, _) > get_expr_calls prednode e

321

 Expr_array t

322

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

323

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

324

 Expr_fby (e1,e2)

325

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

326

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

327

 Expr_pre e

328

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

329

 Expr_appl (id,e, _) >

330

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

331

then ESet.add expr (get_expr_calls prednode e)

332

else (get_expr_calls prednode e)

333


334

let get_eexpr_calls prednode ee =

335

get_expr_calls prednode ee.eexpr_qfexpr

336


337

let get_callee expr =

338

match expr.expr_desc with

339

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

340

 _ > None

341


342

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

343


344

let get_eq_calls prednode eq = get_expr_calls prednode eq.eq_rhs

345


346

let rec get_stmt_calls prednode s =

347

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

348

and get_aut_calls prednode aut =

349

let get_handler_calls prednode h =

350

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

351

let until = get_cond_calls h.hand_until in

352

let unless = get_cond_calls h.hand_unless in

353

let calls = ESet.union until unless in

354

let calls = accu (get_stmt_calls prednode) calls h.hand_stmts in

355

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

356

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

357

calls

358

in

359

accu (get_handler_calls prednode) ESet.empty aut.aut_handlers

360


361

let get_calls prednode nd =

362

let eqs, auts = get_node_eqs nd in

363

let deps = accu (get_eq_calls prednode) ESet.empty eqs in

364

let deps = accu (get_aut_calls prednode) deps auts in

365

ESet.elements deps

366


367

let get_contract_calls prednode c =

368

let deps = accu (get_stmt_calls prednode) ESet.empty c.stmts in

369

let deps = accu (get_eexpr_calls prednode) deps ( c.assume @ c.guarantees @ (List.fold_left (fun accu m > accu @ m.require @ m.ensure ) [] c.modes)) in

370

let id_deps = List.map (fun e > fst (desome (get_callee e))) (ESet.elements deps) in

371

let id_deps = (List.fold_left (fun accu imp > imp.import_nodeid::accu) [] c.imports) @ id_deps in

372

id_deps

373


374

let dependence_graph prog =

375

let g = new_graph () in

376

let g = List.fold_right

377

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

378

match td.top_decl_desc with

379

 Node nd >

380

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

381

let accu = add_vertices [nd.node_id] accu in

382

let deps = List.map

383

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

384

(get_calls (fun _ > true) nd)

385

in

386

(* Adding assert expressions deps *)

387

let deps_asserts =

388

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

389

List.map

390

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

391

(ESet.elements

392

(List.fold_left

393

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

394

ESet.empty

395

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

396

)

397

)

398

in

399

let deps_spec = match nd.node_spec with

400

 None > []

401

 Some (NodeSpec id) > [id]

402

 Some (Contract c) > get_contract_calls (fun _ > true) c

403


404

in

405

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

406

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

407

 _ > assert false (* should not happen *)

408


409

) prog g in

410

g

411


412

let rec filter_static_inputs inputs args =

413

match inputs, args with

414

 [] , [] > []

415

 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

416

 _ > assert false

417


418

let compute_generic_calls prog =

419

List.iter

420

(fun td >

421

match td.top_decl_desc with

422

 Node nd >

423

let prednode n = is_generic_node (node_from_name n) in

424

nd.node_gencalls < get_calls prednode nd

425

 _ > ()

426


427

) prog

428


429

end

430


431


432

module CycleDetection = struct

433


434

(*  Look for cycles in a dependency graph *)

435

module Cycles = Graph.Components.Make (IdentDepGraph)

436


437

let mk_copy_var n id =

438

let used name =

439

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

440

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

441

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

442

in mk_new_name used id

443


444

let mk_copy_eq n var =

445

let var_decl = get_node_var var n in

446

let cp_var = mk_copy_var n var in

447

let expr =

448

{ expr_tag = Utils.new_tag ();

449

expr_desc = Expr_ident var;

450

expr_type = var_decl.var_type;

451

expr_clock = var_decl.var_clock;

452

expr_delay = Delay.new_var ();

453

expr_annot = None;

454

expr_loc = var_decl.var_loc } in

455

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

456

mkeq var_decl.var_loc ([cp_var], expr)

457


458

let wrong_partition g partition =

459

match partition with

460

 [id] > IdentDepGraph.mem_edge g id id

461

 _::_::_ > true

462

 [] > assert false

463


464

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

465

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

466

let check_cycles g =

467

let scc_l = Cycles.scc_list g in

468

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

469

if List.length algebraic_loops > 0 then

470

raise (Error (DataCycle algebraic_loops))

471

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

472

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

473

its specific id *)

474


475

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

476

let copy_partition g partition =

477

let copy_g = IdentDepGraph.create () in

478

IdentDepGraph.iter_edges

479

(fun src tgt >

480

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

481

then IdentDepGraph.add_edge copy_g src tgt)

482

g

483


484


485

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

486

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

487

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

488

let break_cycle head cp_head g =

489

let succs = IdentDepGraph.succ g head in

490

IdentDepGraph.add_edge g head cp_head;

491

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

492

List.iter

493

(fun s >

494

IdentDepGraph.remove_edge g head s;

495

IdentDepGraph.add_edge g s cp_head)

496

succs

497


498

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

499

belonging in node [node]. Returns:

500

 a list of new auxiliary variable declarations

501

 a list of new equations

502

 a modified acyclic version of [g]

503

*)

504

let break_cycles node mems g =

505

let eqs , auts = get_node_eqs node in

506

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

507

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

508

let rec break vdecls mem_eqs g =

509

let scc_l = Cycles.scc_list g in

510

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

511

match wrong with

512

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

513

 [head]::_ >

514

begin

515

IdentDepGraph.remove_edge g head head;

516

break vdecls mem_eqs g

517

end

518

 (head::part)::_ >

519

begin

520

let vdecl_cp_head, cp_eq = mk_copy_eq node head in

521

let pvar v = List.mem v part in

522

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

523

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

524

break_cycle head vdecl_cp_head.var_id g;

525

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

526

end

527

 _ > assert false

528

in break [] mem_eqs g

529


530

end

531


532

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

533

module Disjunction =

534

struct

535

module ClockedIdentModule =

536

struct

537

type t = var_decl

538

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

539

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

540

end

541


542

module CISet = Set.Make(ClockedIdentModule)

543


544

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

545

maybe removing shorter branches *)

546

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

547


548

let pp_ciset fmt t =

549

begin

550

Format.fprintf fmt "{@ ";

551

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

552

Format.fprintf fmt "}@."

553

end

554


555

let clock_disjoint_map vdecls =

556

let map = Hashtbl.create 23 in

557

begin

558

List.iter

559

(fun v1 > let disj_v1 =

560

List.fold_left

561

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

562

CISet.empty

563

vdecls in

564

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

565

Hashtbl.add map v1.var_id disj_v1)

566

vdecls;

567

(map : disjoint_map)

568

end

569


570

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

571

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

572

 the mapping v > ... then disappears

573

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

574

*)

575

let merge_in_disjoint_map map v v' =

576

begin

577

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

578

Hashtbl.remove map v.var_id;

579

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;

580

end

581


582

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

583

[v'] is a dead variable. Then:

584

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

585

 the mapping v > ... then disappears

586

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

587

*)

588

let replace_in_disjoint_map map v v' =

589

begin

590

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

591

Hashtbl.remove map v.var_id;

592

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;

593

end

594


595

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

596

 the mapping v > ... then disappears

597

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

598

*)

599

let remove_in_disjoint_map map v =

600

begin

601

Hashtbl.remove map v.var_id;

602

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

603

end

604


605

let pp_disjoint_map fmt map =

606

begin

607

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

608

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

609

Format.fprintf fmt "}@."

610

end

611

end

612


613


614

let pp_dep_graph fmt g =

615

begin

616

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

617

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

618

Format.fprintf fmt "}@."

619

end

620


621

let pp_error fmt err =

622

match err with

623

 NodeCycle trace >

624

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

625

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

626

 DataCycle traces > (

627

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

628

(fprintf_list ~sep:";@ "

629

(fun fmt trace >

630

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

631

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

632

trace

633

)) traces

634

)

635


636

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

637

let merge_with g1 g2 =

638

begin

639

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

640

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

641

end

642


643

let world = "!!_world"

644


645

let add_external_dependency outputs mems g =

646

begin

647

IdentDepGraph.add_vertex g world;

648

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

649

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

650

end

651


652

(* Takes a node and return a pair (node', graph) where node' is node

653

rebuilt with the equations enriched with new ones introduced to

654

"break cycles" *)

655

let global_dependency node =

656

let mems = ExprDep.node_memory_variables node in

657

let inputs =

658

ISet.union

659

(ExprDep.node_input_variables node)

660

(ExprDep.node_constant_variables node) in

661

let outputs = ExprDep.node_output_variables node in

662

let node_vars = ExprDep.node_variables node in

663

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

664

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

665

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

666

try

667

CycleDetection.check_cycles g_non_mems;

668

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

669

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

670

begin

671

merge_with g_non_mems g_mems';

672

add_external_dependency outputs mems g_non_mems;

673

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

674

g_non_mems

675

end

676

with Error (DataCycle _ as exc) > (

677

raise (Error (exc))

678

)

679


680

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

681

module VarClockDep =

682

struct

683

let rec get_clock_dep ck =

684

match ck.Clocks.cdesc with

685

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

686

 Clocks.Clink ck'

687

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

688

 _ > []

689


690

let sort locals =

691

let g = new_graph () in

692

let g = List.fold_left (

693

fun g var_decl >

694

let deps = get_clock_dep var_decl.var_clock in

695

add_edges [var_decl.var_id] deps g

696

) g locals

697

in

698

let sorted, no_deps =

699

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

700

let select v = v.var_id = vid in

701

let selected, not_selected = List.partition select remaining in

702

selected@accu, not_selected

703

)) g ([],locals)

704

in

705

no_deps @ sorted

706


707

end

708


709

(* Local Variables: *)

710

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

711

(* End: *)
