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

open Utils

15

(** Simple modular syntactic causality analysis. Can reject correct programs,

16

especially if the program is not flattened first. *)

17


18

open Lustre_types

19

open Corelang

20


21

type identified_call = eq * tag

22


23

type error =

24

 DataCycle of ident list list

25

(* multiple failed partitions at once *)

26

 NodeCycle of ident list

27


28

exception Error of error

29


30

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

31

some mem vars into local node vars. Thus, cylic dependency errors may only

32

arise between nomem vars. nonmem variables are:  constants/inputs: not

33

needed for causality/scheduling, needed only for detecting useless vars 

34

read mems (fake vars): same remark as above.  outputs: decoupled from mems,

35

if necessary  locals  instance vars (fake vars): simplify causality

36

analysis

37


38

global constants are not part of the dependency graph.

39


40

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

41


42

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

43


44

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

45

(mem/mem)  check cycles in g (a cycle means a dependency error)  break

46

cycles in g' (it's legal !):  check cycles in g'  if any, introduce aux var

47

to break cycle, then start afresh  insert g' into g  return g *)

48


49

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

50

let is_graph_root v g = IdentDepGraph.in_degree g v = 0

51


52

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

53

let graph_roots g =

54

IdentDepGraph.fold_vertex

55

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

56

g []

57


58

let add_edges src tgt g =

59

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

60

tgt) src;*)

61

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

62

g

63


64

let add_vertices vtc g =

65

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

66

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

67

g

68


69

let new_graph () = IdentDepGraph.create ()

70


71

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

72

let slice_graph gr v =

73

let gr' = new_graph () in

74

IdentDepGraph.add_vertex gr' v;

75

Bfs.iter_component

76

(fun v >

77

IdentDepGraph.iter_succ

78

(fun s >

79

IdentDepGraph.add_vertex gr' s;

80

IdentDepGraph.add_edge gr' v s)

81

gr v)

82

gr v;

83

gr'

84


85

module ExprDep = struct

86

let get_node_eqs nd =

87

let eqs, auts = get_node_eqs nd in

88

if auts != [] then assert false

89

(* No call on causality on a Lustre model with automaton. They should be

90

expanded by now. *);

91

eqs

92


93

let instance_var_cpt = ref 0

94


95

(* read vars represent input/mem readonly vars, they are not part of the

96

program/schedule, as they are not assigned, but used to compute useless

97

inputs/mems. a mem read var represents a mem at the beginning of a cycle *)

98

let mk_read_var id = Format.sprintf "#%s" id

99


100

(* instance vars represent node instance calls, they are not part of the

101

program/schedule, but used to simplify causality analysis *)

102

let mk_instance_var id =

103

incr instance_var_cpt;

104

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

105


106

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

107


108

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

109


110

let is_ghost_var v = is_instance_var v  is_read_var v

111


112

let undo_read_var id =

113

assert (is_read_var id);

114

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

115


116

let undo_instance_var id =

117

assert (is_instance_var id);

118

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

119


120

let eq_memory_variables mems eq =

121

let rec match_mem lhs rhs mems =

122

match rhs.expr_desc with

123

 Expr_fby _  Expr_pre _ >

124

List.fold_right ISet.add lhs mems

125

 Expr_tuple tl >

126

let lhs' = transpose_list [ lhs ] in

127

List.fold_right2 match_mem lhs' tl mems

128

 _ >

129

mems

130

in

131

match_mem eq.eq_lhs eq.eq_rhs mems

132


133

let node_memory_variables nd =

134

List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)

135


136

let node_input_variables nd =

137

List.fold_left

138

(fun inputs v > ISet.add v.var_id inputs)

139

ISet.empty

140

(if nd.node_iscontract then nd.node_inputs @ nd.node_outputs

141

else nd.node_inputs)

142


143

let node_output_variables nd =

144

List.fold_left

145

(fun outputs v > ISet.add v.var_id outputs)

146

ISet.empty

147

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

148


149

let node_local_variables nd =

150

List.fold_left

151

(fun locals v > ISet.add v.var_id locals)

152

ISet.empty nd.node_locals

153


154

let node_constant_variables nd =

155

List.fold_left

156

(fun locals v >

157

if v.var_dec_const then ISet.add v.var_id locals else locals)

158

ISet.empty nd.node_locals

159


160

let node_auxiliary_variables nd =

161

ISet.diff (node_local_variables nd) (node_memory_variables nd)

162


163

let node_variables nd =

164

let inputs = node_input_variables nd in

165

let inoutputs =

166

List.fold_left

167

(fun inoutputs v > ISet.add v.var_id inoutputs)

168

inputs nd.node_outputs

169

in

170

List.fold_left

171

(fun vars v > ISet.add v.var_id vars)

172

inoutputs nd.node_locals

173


174

(* computes the equivalence relation relating variables in the same equation

175

lhs, under the form of a table of class representatives *)

176

let eqs_eq_equiv eqs =

177

let eq_equiv = Hashtbl.create 23 in

178

List.iter

179

(fun eq >

180

let first = List.hd eq.eq_lhs in

181

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

182

eqs;

183

eq_equiv

184


185

let node_eq_equiv nd = eqs_eq_equiv (get_node_eqs nd)

186


187

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

188

(* filled with variable [v] *)

189

let adjust_tuple v expr =

190

match expr.expr_type.Types.tdesc with

191

 Types.Ttuple tl >

192

duplicate v (List.length tl)

193

 _ >

194

[ v ]

195


196

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

197

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

198

(* mem/mem in g' *)

199

(* match (lhs_is_mem, ISet.mem x mems) with  (false, true ) > (add_edges [x]

200

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

201

> (add_edges lhs [x] g, g')  (true , true ) > (g, add_edges [x] lhs g') *)

202

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

203

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

204

if is_instance_var x  ISet.mem x node_vars then

205

if ISet.mem x mems then

206

let g = add_edges lhs [ mk_read_var x ] g in

207

if lhs_is_mem then g, add_edges [ x ] lhs g'

208

else add_edges [ x ] lhs g, g'

209

else

210

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

211

add_edges lhs [ x ] g, g'

212

else add_edges lhs [ mk_read_var x ] g, g'

213

(* 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, _) >

220

add_var lhs_is_mem lhs

221

(Clocks.const_of_carrier cr)

222

(add_clock lhs_is_mem lhs ck' g)

223

 Clocks.Ccarrying (_, ck') >

224

add_clock lhs_is_mem lhs ck' g

225

 _ >

226

g

227

in

228

let rec add_dep lhs_is_mem lhs rhs g =

229

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

230

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

231

let mashup_appl_dependencies f e g =

232

let f_var =

233

mk_instance_var

234

(Format.sprintf "%s_%d" f (fst eq.eq_loc).Lexing.pos_lnum)

235

in

236

List.fold_right

237

(fun rhs > add_dep lhs_is_mem (adjust_tuple f_var rhs) rhs)

238

(expr_list_of_expr e)

239

(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 _ >

244

g

245

 Expr_fby (e1, e2) >

246

add_dep true lhs e2 (add_dep false lhs e1 g)

247

 Expr_pre e >

248

add_dep true lhs e g

249

 Expr_ident x >

250

add_var lhs_is_mem lhs x g

251

 Expr_access (e1, d)  Expr_power (e1, d) >

252

add_dep lhs_is_mem lhs e1

253

(add_dep lhs_is_mem lhs (expr_of_dimension d) g)

254

 Expr_array a >

255

List.fold_right (add_dep lhs_is_mem lhs) a g

256

 Expr_tuple t >

257

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

258

 Expr_merge (c, hl) >

259

add_var lhs_is_mem lhs c

260

(List.fold_right (fun (_, h) > add_dep lhs_is_mem lhs h) hl g)

261

 Expr_ite (c, t, e) >

262

add_dep lhs_is_mem lhs c

263

(add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g))

264

 Expr_arrow (e1, e2) >

265

add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)

266

 Expr_when (e, c, _) >

267

add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)

268

 Expr_appl (f, e, None) >

269

if

270

Basic_library.is_expr_internal_fun rhs

271

(* tuple componentwise dependency for internal operators *)

272

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

273

(* mashed up dependency for userdefined operators *)

274

else mashup_appl_dependencies f e g

275

 Expr_appl (f, e, Some c) >

276

mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)

277

in

278

let g =

279

List.fold_left

280

(fun g lhs >

281

if ISet.mem lhs mems then add_vertices [ lhs; mk_read_var lhs ] g

282

else add_vertices [ lhs ] g)

283

g eq.eq_lhs

284

in

285

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

286


287

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

288

let dependence_graph mems inputs node_vars n =

289

instance_var_cpt := 0;

290

let g = new_graph (), new_graph () in

291

(* Basic dependencies *)

292

let g =

293

List.fold_right

294

(add_eq_dependencies mems inputs node_vars)

295

(get_node_eqs n) g

296

in

297


298

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

299

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

300

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

301


302

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

303

node, *)

304

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

305

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

306

in *)

307

(* function add_eq_dependencies *\) *)

308

(* let g = *)

309

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

310

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

311

(* let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs,

312

ae.assert_expr) in *)

313

(* add_eq_dependencies mems inputs node_vars fake_eq g *)

314

(* ) g n.node_asserts in *)

315

g

316

end

317


318

module NodeDep = struct

319

module ExprModule = struct

320

type t = expr

321


322

let compare = compare

323


324

let hash n = Hashtbl.hash n

325


326

let equal n1 n2 = n1 = n2

327

end

328


329

module ESet = Set.Make (ExprModule)

330


331

let rec get_expr_calls prednode expr =

332

match expr.expr_desc with

333

 Expr_const _  Expr_ident _ >

334

ESet.empty

335

 Expr_access (e, _)  Expr_power (e, _) >

336

get_expr_calls prednode e

337

 Expr_array t  Expr_tuple t >

338

List.fold_right

339

(fun x set > ESet.union (get_expr_calls prednode x) set)

340

t ESet.empty

341

 Expr_merge (_, hl) >

342

List.fold_right

343

(fun (_, h) set > ESet.union (get_expr_calls prednode h) set)

344

hl ESet.empty

345

 Expr_fby (e1, e2)  Expr_arrow (e1, e2) >

346

ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)

347

 Expr_ite (c, t, e) >

348

ESet.union

349

(get_expr_calls prednode c)

350

(ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))

351

 Expr_pre e  Expr_when (e, _, _) >

352

get_expr_calls prednode e

353

 Expr_appl (id, e, _) >

354

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

355

ESet.add expr (get_expr_calls prednode e)

356

else get_expr_calls prednode e

357


358

let get_eexpr_calls prednode ee = get_expr_calls prednode ee.eexpr_qfexpr

359


360

let get_callee expr =

361

match expr.expr_desc with

362

 Expr_appl (id, args, _) >

363

Some (id, expr_list_of_expr args)

364

 _ >

365

None

366


367

let accu f init objl =

368

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

369


370

let get_eq_calls prednode eq = get_expr_calls prednode eq.eq_rhs

371


372

let rec get_stmt_calls prednode s =

373

match s with

374

 Eq eq >

375

get_eq_calls prednode eq

376

 Aut aut >

377

get_aut_calls prednode aut

378


379

and get_aut_calls prednode aut =

380

let get_handler_calls prednode h =

381

let get_cond_calls c =

382

accu (fun (_, e, _, _) > get_expr_calls prednode e) ESet.empty c

383

in

384

let until = get_cond_calls h.hand_until in

385

let unless = get_cond_calls h.hand_unless in

386

let calls = ESet.union until unless in

387

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

388

let calls =

389

accu

390

(fun a > get_expr_calls prednode a.assert_expr)

391

calls h.hand_asserts

392

in

393

(* let calls = accu xx calls h.hand_annots in *)

394

(* TODO: search for calls in eexpr *)

395

calls

396

in

397

accu (get_handler_calls prednode) ESet.empty aut.aut_handlers

398


399

let get_calls prednode nd =

400

let eqs, auts = get_node_eqs nd in

401

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

402

let deps = accu (get_aut_calls prednode) deps auts in

403

ESet.elements deps

404


405

let get_contract_calls prednode c =

406

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

407

let deps =

408

accu (get_eexpr_calls prednode) deps

409

(c.assume @ c.guarantees

410

@ List.fold_left (fun accu m > accu @ m.require @ m.ensure) [] c.modes

411

)

412

in

413

let id_deps =

414

List.map (fun e > fst (desome (get_callee e))) (ESet.elements deps)

415

in

416

let id_deps =

417

List.fold_left (fun accu imp > imp.import_nodeid :: accu) [] c.imports

418

@ id_deps

419

in

420

id_deps

421


422

let dependence_graph prog =

423

let g = new_graph () in

424

let g =

425

List.fold_right

426

(fun td accu >

427

(* for each node we add its dependencies *)

428

match td.top_decl_desc with

429

 Node nd >

430

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

431

let accu = add_vertices [ nd.node_id ] accu in

432

let deps =

433

List.map

434

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

435

(get_calls (fun _ > true) nd)

436

in

437

(* Adding assert expressions deps *)

438

let deps_asserts =

439

let prednode _ = true in

440

(* what is this about? *)

441

List.map

442

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

443

(ESet.elements

444

(List.fold_left

445

(fun accu assert_expr >

446

ESet.union accu (get_expr_calls prednode assert_expr))

447

ESet.empty

448

(List.map

449

(fun _assert > _assert.assert_expr)

450

nd.node_asserts)))

451

in

452

let deps_spec =

453

match nd.node_spec with

454

 None >

455

[]

456

 Some (NodeSpec id) >

457

[ id ]

458

 Some (Contract c) >

459

get_contract_calls (fun _ > true) c

460

in

461


462

(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@."

463

Format.pp_print_string) deps; *)

464

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

465

 _ >

466

assert false

467

(* should not happen *))

468

prog g

469

in

470

g

471


472

let rec filter_static_inputs inputs args =

473

match inputs, args with

474

 [], [] >

475

[]

476

 v :: vq, a :: aq >

477

if v.var_dec_const && Types.is_dimension_type v.var_type then

478

dimension_of_expr a :: filter_static_inputs vq aq

479

else filter_static_inputs vq aq

480

 _ >

481

assert false

482


483

let compute_generic_calls prog =

484

List.iter

485

(fun td >

486

match td.top_decl_desc with

487

 Node nd >

488

let prednode n = is_generic_node (node_from_name n) in

489

nd.node_gencalls < get_calls prednode nd

490

 _ >

491

())

492

prog

493

end

494


495

module CycleDetection = struct

496

(*  Look for cycles in a dependency graph *)

497

module Cycles = Graph.Components.Make (IdentDepGraph)

498


499

let mk_copy_var n id =

500

let used name =

501

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

502

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

503

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

504

in

505

mk_new_name used id

506


507

let mk_copy_eq n var =

508

let var_decl = get_node_var var n in

509

let cp_var = mk_copy_var n var in

510

let expr =

511

{

512

expr_tag = Utils.new_tag ();

513

expr_desc = Expr_ident var;

514

expr_type = var_decl.var_type;

515

expr_clock = var_decl.var_clock;

516

expr_delay = Delay.new_var ();

517

expr_annot = None;

518

expr_loc = var_decl.var_loc;

519

}

520

in

521

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

522

mkeq var_decl.var_loc ([ cp_var ], expr) )

523


524

let wrong_partition g partition =

525

match partition with

526

 [ id ] >

527

IdentDepGraph.mem_edge g id id

528

 _ :: _ :: _ >

529

true

530

 [] >

531

assert false

532


533

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

534

[Cycle partition] if the succession of dependencies [partition] forms a

535

cycle *)

536

let check_cycles g =

537

let scc_l = Cycles.scc_list g in

538

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

539

if List.length algebraic_loops > 0 then

540

raise (Error (DataCycle algebraic_loops))

541

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

542

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

543

specific id *)

544


545

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

546

let copy_partition g partition =

547

let copy_g = IdentDepGraph.create () in

548

IdentDepGraph.iter_edges

549

(fun src tgt >

550

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

551

IdentDepGraph.add_edge copy_g src tgt)

552

g

553


554

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

555

is a head of a nontrivial scc of [g]. In Lustre, this is legal only for

556

mem/mem cycles *)

557

let break_cycle head cp_head g =

558

let succs = IdentDepGraph.succ g head in

559

IdentDepGraph.add_edge g head cp_head;

560

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

561

List.iter

562

(fun s >

563

IdentDepGraph.remove_edge g head s;

564

IdentDepGraph.add_edge g s cp_head)

565

succs

566


567

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

568

belonging in node [node]. Returns:  a list of new auxiliary variable

569

declarations  a list of new equations  a modified acyclic version of [g] *)

570

let break_cycles node mems g =

571

let eqs, auts = get_node_eqs node in

572

assert (auts = []);

573

(* TODO: check: For the moment we assume that auts are expanded by now *)

574

let mem_eqs, non_mem_eqs =

575

List.partition

576

(fun eq > List.exists (fun v > ISet.mem v mems) eq.eq_lhs)

577

eqs

578

in

579

let rec break vdecls mem_eqs g =

580

let scc_l = Cycles.scc_list g in

581

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

582

match wrong with

583

 [] >

584

vdecls, non_mem_eqs @ mem_eqs, g

585

 [ head ] :: _ >

586

IdentDepGraph.remove_edge g head head;

587

break vdecls mem_eqs g

588

 (head :: part) :: _ >

589

let vdecl_cp_head, cp_eq = mk_copy_eq node head in

590

let pvar v = List.mem v part in

591

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

592

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

593

break_cycle head vdecl_cp_head.var_id g;

594

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

595

 _ >

596

assert false

597

in

598

break [] mem_eqs g

599

end

600


601

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

602

clocks. *)

603

module Disjunction = struct

604

module ClockedIdentModule = struct

605

type t = var_decl

606


607

let root_branch vdecl =

608

Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock

609


610

let compare v1 v2 =

611

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

612

end

613


614

module CISet = Set.Make (ClockedIdentModule)

615


616

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

617

order, maybe removing shorter branches *)

618

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

619


620

let pp_ciset fmt t =

621

let open Format in

622

pp_print_braced' ~pp_sep:pp_print_space Printers.pp_var_name fmt

623

(CISet.elements t)

624


625

let clock_disjoint_map vdecls =

626

let map = Hashtbl.create 23 in

627

List.iter

628

(fun v1 >

629

let disj_v1 =

630

List.fold_left

631

(fun res v2 >

632

if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res

633

else res)

634

CISet.empty vdecls

635

in

636

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

637

Hashtbl.add map v1.var_id disj_v1)

638

vdecls;

639

(map : disjoint_map)

640


641

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

642

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

643

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

644

v') *)

645

let merge_in_disjoint_map map v v' =

646

Hashtbl.replace map v'.var_id

647

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

648

Hashtbl.remove map v.var_id;

649

Hashtbl.iter

650

(fun x map_x >

651

Hashtbl.replace map x

652

(CISet.remove (if CISet.mem v map_x then v else v') map_x))

653

map

654


655

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

656

Then:  the mapping v' becomes v' > (map v)  the mapping v > ... then

657

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

658

map x) *)

659

let replace_in_disjoint_map map v v' =

660

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

661

Hashtbl.remove map v.var_id;

662

Hashtbl.iter

663

(fun x mapx >

664

Hashtbl.replace map x

665

(if CISet.mem v mapx then CISet.add v' (CISet.remove v mapx)

666

else CISet.remove v' mapx))

667

map

668


669

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

670

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

671

let remove_in_disjoint_map map v =

672

Hashtbl.remove map v.var_id;

673

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

674


675

let pp_disjoint_map fmt map =

676

Format.(

677

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

678

Hashtbl.iter

679

(fun k v >

680

fprintf fmt "@,%s # %a" k

681

(pp_print_braced' Printers.pp_var_name)

682

(CISet.elements v))

683

map))

684

end

685


686

let pp_dep_graph fmt g =

687

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

688

IdentDepGraph.iter_edges

689

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

690

g)

691


692

let pp_error fmt err =

693

match err with

694

 NodeCycle trace >

695

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

696

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

697

trace

698

 DataCycle traces >

699

Format.fprintf fmt

700

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

701

(fprintf_list ~sep:";@ " (fun fmt trace >

702

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

703

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

704

trace))

705

traces

706


707

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

708

let merge_with g1 g2 =

709

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

710

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

711


712

let world = "!!_world"

713


714

let add_external_dependency outputs mems g =

715

IdentDepGraph.add_vertex g world;

716

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

717

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

718


719

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

720

with the equations enriched with new ones introduced to "break cycles" *)

721

let global_dependency node =

722

let mems = ExprDep.node_memory_variables node in

723

let inputs =

724

ISet.union

725

(ExprDep.node_input_variables node)

726

(ExprDep.node_constant_variables node)

727

in

728

let outputs = ExprDep.node_output_variables node in

729

let node_vars = ExprDep.node_variables node in

730

let g_non_mems, g_mems =

731

ExprDep.dependence_graph mems inputs node_vars node

732

in

733

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

734

"g_mems: %a" pp_dep_graph g_mems;*)

735

try

736

CycleDetection.check_cycles g_non_mems;

737

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

738

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

739

merge_with g_non_mems g_mems';

740

add_external_dependency outputs mems g_non_mems;

741

( {

742

node with

743

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

744

node_locals = vdecls' @ node.node_locals;

745

},

746

g_non_mems )

747

with Error (DataCycle _ as exc) > raise (Error exc)

748


749

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

750

declarations *)

751

module VarClockDep = struct

752

let rec get_clock_dep ck =

753

match ck.Clocks.cdesc with

754

 Clocks.Con (ck, _, l) >

755

l :: get_clock_dep ck

756

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

757

get_clock_dep ck'

758

 _ >

759

[]

760


761

let sort locals =

762

let g = new_graph () in

763

let g =

764

List.fold_left

765

(fun g var_decl >

766

let deps = get_clock_dep var_decl.var_clock in

767

add_edges [ var_decl.var_id ] deps g)

768

g locals

769

in

770

let sorted, no_deps =

771

TopologicalDepGraph.fold

772

(fun vid (accu, remaining) >

773

let select v = v.var_id = vid in

774

let selected, not_selected = List.partition select remaining in

775

selected @ accu, not_selected)

776

g ([], locals)

777

in

778

no_deps @ sorted

779

end

780


781

(* Local Variables: *)

782

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

783

(* End: *)
