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


21


22

type identified_call = eq * tag

23

type error =

24

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

25

 NodeCycle of ident list

26


27

exception Error of error

28


29


30


31

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

32

by duplication of some mem vars into local node vars.

33

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

34

nonmem variables are:

35

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

36

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

37

 outputs: decoupled from mems, if necessary

38

 locals

39

 instance vars (fake vars): simplify causality analysis

40


41

global constants are not part of the dependency graph.

42


43

no_mem' = combinational(no_mem, mem);

44

=> (mem > no_mem' > no_mem)

45


46

mem' = pre(no_mem, mem);

47

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

48


49

Global roadmap:

50

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

51

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

52

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

53

 check cycles in g'

54

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

55

 insert g' into g

56

 return g

57

*)

58


59

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

60

let is_graph_root v g =

61

IdentDepGraph.in_degree g v = 0

62


63

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

64

let graph_roots g =

65

IdentDepGraph.fold_vertex

66

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

67

g []

68


69

let add_edges src tgt g =

70

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

71

List.iter

72

(fun s > List.iter (IdentDepGraph.add_edge g s) tgt)

73

src;

74

g

75


76

let add_vertices vtc g =

77

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

78

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

79

g

80


81

let new_graph () =

82

IdentDepGraph.create ()

83


84

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

85

let slice_graph gr v =

86

begin

87

let gr' = new_graph () in

88

IdentDepGraph.add_vertex gr' v;

89

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;

90

gr'

91

end

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

148

(if nd.node_iscontract then

149

nd.node_inputs@nd.node_outputs

150

else

151

nd.node_inputs)

152


153

let node_output_variables nd =

154

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

155

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

156


157

let node_local_variables nd =

158

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

159


160

let node_constant_variables nd =

161

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

162


163

let node_auxiliary_variables nd =

164

ISet.diff (node_local_variables nd) (node_memory_variables nd)

165


166

let node_variables nd =

167

let inputs = node_input_variables nd in

168

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

169

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

170


171

(* computes the equivalence relation relating variables

172

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

173

of class representatives *)

174

let eqs_eq_equiv eqs =

175

let eq_equiv = Hashtbl.create 23 in

176

List.iter (fun eq >

177

let first = List.hd eq.eq_lhs in

178

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

179

)

180

eqs;

181

eq_equiv

182


183

let node_eq_equiv nd = eqs_eq_equiv (get_node_eqs nd)

184


185

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

186

(* filled with variable [v] *)

187

let adjust_tuple v expr =

188

match expr.expr_type.Types.tdesc with

189

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

190

 _ > [v]

191


192


193

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

194

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

195

(* mem/mem in g' *)

196

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

197

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

198

g')

199

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

200

g')

201

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

202

g')

203

 (true , true ) > (g,

204

add_edges [x] lhs g')

205

*)

206

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

207

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

208

if is_instance_var x  ISet.mem x node_vars then

209

if ISet.mem x mems

210

then

211

let g = add_edges lhs [mk_read_var x] g in

212

if lhs_is_mem

213

then

214

(g, add_edges [x] lhs g')

215

else

216

(add_edges [x] lhs g, g')

217

else

218

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

219

(add_edges lhs [x] g, g')

220

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

221

in

222

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

223

let rec add_clock lhs_is_mem lhs ck g =

224

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

225

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

226

 Clocks.Con (ck', cr, _) >

227

add_var lhs_is_mem lhs (Clocks.const_of_carrier cr)

228

(add_clock lhs_is_mem lhs ck' g)

229

 Clocks.Ccarrying (_, ck') >

230

add_clock lhs_is_mem lhs ck' g

231

 _ > g

232

in

233

let rec add_dep lhs_is_mem lhs rhs g =

234

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

235

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

236

let mashup_appl_dependencies f e g =

237

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

238

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

239

(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g)

240

in

241

let g = add_clock lhs_is_mem lhs rhs.expr_clock g 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 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 = List.fold_left (fun g lhs >

267

if ISet.mem lhs mems then

268

add_vertices [lhs; mk_read_var lhs] g

269

else

270

add_vertices [lhs] g)

271

g eq.eq_lhs

272

in

273

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

274


275


276

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

277

let dependence_graph mems inputs node_vars n =

278

instance_var_cpt := 0;

279

let g = new_graph (), new_graph () in

280

(* Basic dependencies *)

281

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

282

(get_node_eqs n) g in

283

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

284

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

285

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

286


287

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

288

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

289

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

290

(* function add_eq_dependencies *\) *)

291

(* let g = *)

292

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

293

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

294

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

295

(* add_eq_dependencies mems inputs node_vars fake_eq g *)

296

(* ) g n.node_asserts in *)

297

g

298


299

end

300


301

module NodeDep = struct

302


303

module ExprModule =

304

struct

305

type t = expr

306

let compare = compare

307

let hash n = Hashtbl.hash n

308

let equal n1 n2 = n1 = n2

309

end

310


311

module ESet = Set.Make(ExprModule)

312


313

let rec get_expr_calls prednode expr =

314

match expr.expr_desc with

315

 Expr_const _

316

 Expr_ident _ > ESet.empty

317

 Expr_access (e, _)

318

 Expr_power (e, _) > get_expr_calls prednode e

319

 Expr_array t

320

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

321

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

322

 Expr_fby (e1,e2)

323

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

324

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

325

 Expr_pre e

326

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

327

 Expr_appl (id,e, _) >

328

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

329

then ESet.add expr (get_expr_calls prednode e)

330

else (get_expr_calls prednode e)

331


332

let get_eexpr_calls prednode ee =

333

get_expr_calls prednode ee.eexpr_qfexpr

334


335

let get_callee expr =

336

match expr.expr_desc with

337

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

338

 _ > None

339


340

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

341


342

let get_eq_calls prednode eq = get_expr_calls prednode eq.eq_rhs

343


344

let rec get_stmt_calls prednode s =

345

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

346

and get_aut_calls prednode aut =

347

let get_handler_calls prednode h =

348

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

349

let until = get_cond_calls h.hand_until in

350

let unless = get_cond_calls h.hand_unless in

351

let calls = ESet.union until unless in

352

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

353

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

354

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

355

calls

356

in

357

accu (get_handler_calls prednode) ESet.empty aut.aut_handlers

358


359

let get_calls prednode nd =

360

let eqs, auts = get_node_eqs nd in

361

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

362

let deps = accu (get_aut_calls prednode) deps auts in

363

ESet.elements deps

364


365

let get_contract_calls prednode c =

366

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

367

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

368

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

369

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

370

id_deps

371


372

let dependence_graph prog =

373

let g = new_graph () in

374

let g = List.fold_right

375

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

376

match td.top_decl_desc with

377

 Node nd >

378

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

379

let accu = add_vertices [nd.node_id] accu in

380

let deps = List.map

381

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

382

(get_calls (fun _ > true) nd)

383

in

384

(* Adding assert expressions deps *)

385

let deps_asserts =

386

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

387

List.map

388

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

389

(ESet.elements

390

(List.fold_left

391

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

392

ESet.empty

393

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

394

)

395

)

396

in

397

let deps_spec = match nd.node_spec with

398

 None > []

399

 Some (NodeSpec id) > [id]

400

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

401


402

in

403

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

404

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

405

 _ > assert false (* should not happen *)

406


407

) prog g in

408

g

409


410

let rec filter_static_inputs inputs args =

411

match inputs, args with

412

 [] , [] > []

413

 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

414

 _ > assert false

415


416

let compute_generic_calls prog =

417

List.iter

418

(fun td >

419

match td.top_decl_desc with

420

 Node nd >

421

let prednode n = is_generic_node (node_from_name n) in

422

nd.node_gencalls < get_calls prednode nd

423

 _ > ()

424


425

) prog

426


427

end

428


429


430

module CycleDetection = struct

431


432

(*  Look for cycles in a dependency graph *)

433

module Cycles = Graph.Components.Make (IdentDepGraph)

434


435

let mk_copy_var n id =

436

let used name =

437

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

438

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

439

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

440

in mk_new_name used id

441


442

let mk_copy_eq n var =

443

let var_decl = get_node_var var n in

444

let cp_var = mk_copy_var n var in

445

let expr =

446

{ expr_tag = Utils.new_tag ();

447

expr_desc = Expr_ident var;

448

expr_type = var_decl.var_type;

449

expr_clock = var_decl.var_clock;

450

expr_delay = Delay.new_var ();

451

expr_annot = None;

452

expr_loc = var_decl.var_loc } in

453

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

454

mkeq var_decl.var_loc ([cp_var], expr)

455


456

let wrong_partition g partition =

457

match partition with

458

 [id] > IdentDepGraph.mem_edge g id id

459

 _::_::_ > true

460

 [] > assert false

461


462

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

463

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

464

let check_cycles g =

465

let scc_l = Cycles.scc_list g in

466

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

467

if List.length algebraic_loops > 0 then

468

raise (Error (DataCycle algebraic_loops))

469

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

470

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

471

its specific id *)

472


473

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

474

let copy_partition g partition =

475

let copy_g = IdentDepGraph.create () in

476

IdentDepGraph.iter_edges

477

(fun src tgt >

478

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

479

then IdentDepGraph.add_edge copy_g src tgt)

480

g

481


482


483

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

484

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

485

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

486

let break_cycle head cp_head g =

487

let succs = IdentDepGraph.succ g head in

488

IdentDepGraph.add_edge g head cp_head;

489

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

490

List.iter

491

(fun s >

492

IdentDepGraph.remove_edge g head s;

493

IdentDepGraph.add_edge g s cp_head)

494

succs

495


496

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

497

belonging in node [node]. Returns:

498

 a list of new auxiliary variable declarations

499

 a list of new equations

500

 a modified acyclic version of [g]

501

*)

502

let break_cycles node mems g =

503

let eqs , auts = get_node_eqs node in

504

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

505

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

506

let rec break vdecls mem_eqs g =

507

let scc_l = Cycles.scc_list g in

508

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

509

match wrong with

510

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

511

 [head]::_ >

512

begin

513

IdentDepGraph.remove_edge g head head;

514

break vdecls mem_eqs g

515

end

516

 (head::part)::_ >

517

begin

518

let vdecl_cp_head, cp_eq = mk_copy_eq node head in

519

let pvar v = List.mem v part in

520

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

521

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

522

break_cycle head vdecl_cp_head.var_id g;

523

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

524

end

525

 _ > assert false

526

in break [] mem_eqs g

527


528

end

529


530

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

531

module Disjunction =

532

struct

533

module ClockedIdentModule =

534

struct

535

type t = var_decl

536

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

537

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

538

end

539


540

module CISet = Set.Make(ClockedIdentModule)

541


542

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

543

maybe removing shorter branches *)

544

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

545


546

let pp_ciset fmt t = let open Format in

547

pp_print_braced' ~pp_sep:pp_print_space Printers.pp_var_name fmt

548

(CISet.elements t)

549


550

let clock_disjoint_map vdecls =

551

let map = Hashtbl.create 23 in

552

begin

553

List.iter

554

(fun v1 > let disj_v1 =

555

List.fold_left

556

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

557

CISet.empty

558

vdecls in

559

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

560

Hashtbl.add map v1.var_id disj_v1)

561

vdecls;

562

(map : disjoint_map)

563

end

564


565

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

566

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

567

 the mapping v > ... then disappears

568

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

569

*)

570

let merge_in_disjoint_map map v v' =

571

begin

572

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

573

Hashtbl.remove map v.var_id;

574

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;

575

end

576


577

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

578

[v'] is a dead variable. Then:

579

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

580

 the mapping v > ... then disappears

581

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

582

*)

583

let replace_in_disjoint_map map v v' =

584

begin

585

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

586

Hashtbl.remove map v.var_id;

587

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;

588

end

589


590

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

591

 the mapping v > ... then disappears

592

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

593

*)

594

let remove_in_disjoint_map map v =

595

begin

596

Hashtbl.remove map v.var_id;

597

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

598

end

599


600

let pp_disjoint_map fmt map =

601

Format.(fprintf fmt "@[<v 2>{ /* disjoint map */%t@] }"

602

(fun fmt >

603

Hashtbl.iter (fun k v >

604

fprintf fmt "@,%s # %a"

605

k (pp_print_braced' Printers.pp_var_name)

606

(CISet.elements v)) map))

607

end

608


609


610

let pp_dep_graph fmt g =

611

Format.fprintf fmt "@[<v 0>@[<v 2>{ /* graph */%t@]@ }@]"

612

(fun fmt >

613

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

614


615

let pp_error fmt err =

616

match err with

617

 NodeCycle trace >

618

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

619

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

620

 DataCycle traces > (

621

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

622

(fprintf_list ~sep:";@ "

623

(fun fmt trace >

624

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

625

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

626

trace

627

)) traces

628

)

629


630

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

631

let merge_with g1 g2 =

632

begin

633

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

634

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

635

end

636


637

let world = "!!_world"

638


639

let add_external_dependency outputs mems g =

640

begin

641

IdentDepGraph.add_vertex g world;

642

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

643

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

644

end

645


646

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

647

rebuilt with the equations enriched with new ones introduced to

648

"break cycles" *)

649

let global_dependency node =

650

let mems = ExprDep.node_memory_variables node in

651

let inputs =

652

ISet.union

653

(ExprDep.node_input_variables node)

654

(ExprDep.node_constant_variables node) in

655

let outputs = ExprDep.node_output_variables node in

656

let node_vars = ExprDep.node_variables node in

657

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

658

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

659

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

660

try

661

CycleDetection.check_cycles g_non_mems;

662

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

663

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

664

begin

665

merge_with g_non_mems g_mems';

666

add_external_dependency outputs mems g_non_mems;

667

{ node with

668

node_stmts = List.map (fun eq > Eq eq) eqs';

669

node_locals = vdecls' @ node.node_locals },

670

g_non_mems

671

end

672

with Error (DataCycle _ as exc) >

673

raise (Error (exc))

674


675

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

676

module VarClockDep =

677

struct

678

let rec get_clock_dep ck =

679

match ck.Clocks.cdesc with

680

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

681

 Clocks.Clink ck'

682

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

683

 _ > []

684


685

let sort locals =

686

let g = new_graph () in

687

let g = List.fold_left (

688

fun g var_decl >

689

let deps = get_clock_dep var_decl.var_clock in

690

add_edges [var_decl.var_id] deps g

691

) g locals

692

in

693

let sorted, no_deps =

694

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

695

let select v = v.var_id = vid in

696

let selected, not_selected = List.partition select remaining in

697

selected@accu, not_selected

698

)) g ([],locals)

699

in

700

no_deps @ sorted

701


702

end

703


704

(* Local Variables: *)

705

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

706

(* End: *)
