1

(********************************************************************)

2

(* *)

3

(* The LustreC compiler toolset / The LustreC Development Team *)

4

(* Copyright 2012   ONERA  CNRS  INPT  LIFL *)

5

(* *)

6

(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)

7

(* under the terms of the GNU Lesser General Public License *)

8

(* version 2.1. *)

9

(* *)

10

(* This file was originally from the Prelude compiler *)

11

(* *)

12

(********************************************************************)

13


14


15

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

16

programs, especially if the program is not flattened first. *)

17

open Utils

18

open LustreSpec

19

open Corelang

20

open Graph

21

open Format

22


23

exception Cycle of ident list

24


25

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

26


27

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

28

by duplication of some mem vars into local node vars.

29

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

30

nonmem variables are:

31

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

32

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

33

 outputs: decoupled from mems, if necessary

34

 locals

35

 instance vars (fake vars): simplify causality analysis

36


37

global constants are not part of the dependency graph.

38


39

no_mem' = combinational(no_mem, mem);

40

=> (mem > no_mem' > no_mem)

41


42

mem' = pre(no_mem, mem);

43

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

44


45

Global roadmap:

46

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

47

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

48

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

49

 check cycles in g'

50

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

51

 insert g' into g

52

 return g

53

*)

54


55

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

56

let is_graph_root v g =

57

IdentDepGraph.in_degree g v = 0

58


59

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

60

let graph_roots g =

61

IdentDepGraph.fold_vertex

62

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

63

g []

64


65

let add_edges src tgt g =

66

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

67

List.iter

68

(fun s >

69

List.iter

70

(fun t > IdentDepGraph.add_edge g s t)

71

tgt)

72

src;

73

g

74


75

let add_vertices vtc g =

76

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

77

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

78

g

79


80

let new_graph () =

81

IdentDepGraph.create ()

82


83

module ExprDep = struct

84


85

let instance_var_cpt = ref 0

86


87

(* read vars represent input/mem readonly vars,

88

they are not part of the program/schedule,

89

as they are not assigned,

90

but used to compute useless inputs/mems.

91

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

92

let mk_read_var id =

93

sprintf "#%s" id

94


95

(* instance vars represent node instance calls,

96

they are not part of the program/schedule,

97

but used to simplify causality analysis

98

*)

99

let mk_instance_var id =

100

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

101


102

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

103


104

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

105


106

let is_ghost_var v = is_instance_var v  is_read_var v

107


108

let undo_read_var id =

109

assert (is_read_var id);

110

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

111


112

let undo_instance_var id =

113

assert (is_instance_var id);

114

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

115


116

let eq_memory_variables mems eq =

117

let rec match_mem lhs rhs mems =

118

match rhs.expr_desc with

119

 Expr_fby _

120

 Expr_pre _ > List.fold_right ISet.add lhs mems

121

 Expr_tuple tl >

122

let lhs' = (transpose_list [lhs]) in

123

List.fold_right2 match_mem lhs' tl mems

124

 _ > mems in

125

match_mem eq.eq_lhs eq.eq_rhs mems

126


127

let node_memory_variables nd =

128

List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)

129


130

let node_input_variables nd =

131

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

132


133

let node_local_variables nd =

134

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

135


136

let node_constant_variables nd =

137

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

138


139

let node_output_variables nd =

140

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

141


142

let node_auxiliary_variables nd =

143

ISet.diff (node_local_variables nd) (node_memory_variables nd)

144


145

let node_variables nd =

146

let inputs = node_input_variables nd in

147

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

148

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

149


150

(* computes the equivalence relation relating variables

151

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

152

of class representatives *)

153

let node_eq_equiv nd =

154

let eq_equiv = Hashtbl.create 23 in

155

List.iter (fun eq >

156

let first = List.hd eq.eq_lhs in

157

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

158

)

159

(get_node_eqs nd);

160

eq_equiv

161


162

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

163

(* filled with variable [v] *)

164

let adjust_tuple v expr =

165

match expr.expr_type.Types.tdesc with

166

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

167

 _ > [v]

168


169


170

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

171

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

172

(* mem/mem in g' *)

173

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

174

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

175

g')

176

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

177

g')

178

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

179

g')

180

 (true , true ) > (g,

181

add_edges [x] lhs g')

182

*)

183

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

184

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

185

if is_instance_var x  ISet.mem x node_vars then

186

if ISet.mem x mems

187

then

188

let g = add_edges lhs [mk_read_var x] g in

189

if lhs_is_mem

190

then

191

(g, add_edges [x] lhs g')

192

else

193

(add_edges [x] lhs g, g')

194

else

195

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

196

(add_edges lhs [x] g, g')

197

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

198

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

199

let rec add_clock lhs_is_mem lhs ck g =

200

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

201

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

202

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

203

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

204

 _ > g

205

in

206

let rec add_dep lhs_is_mem lhs rhs g =

207

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

208

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

209

let mashup_appl_dependencies f e g =

210

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

211

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

212

(expr_list_of_expr e) (add_var lhs_is_mem lhs f_var g)

213

in

214

match rhs.expr_desc with

215

 Expr_const _ > g

216

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

217

 Expr_pre e > add_dep true lhs e g

218

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

219

 Expr_access (e1, _)

220

 Expr_power (e1, _) > add_dep lhs_is_mem lhs e1 g

221

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

222

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

223

 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)

224

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

225

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

226

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

227

 Expr_appl (f, e, None) >

228

if Basic_library.is_internal_fun f

229

(* tuple componentwise dependency for internal operators *)

230

then

231

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

232

(* mashed up dependency for userdefined operators *)

233

else

234

mashup_appl_dependencies f e g

235

 Expr_appl (f, e, Some c) >

236

mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)

237

in

238

let g =

239

List.fold_left

240

(fun g lhs > if ISet.mem lhs mems then add_vertices [lhs; mk_read_var lhs] g else add_vertices [lhs] g) g eq.eq_lhs in

241

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

242


243


244

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

245

let dependence_graph mems inputs node_vars n =

246

instance_var_cpt := 0;

247

let g = new_graph (), new_graph () in

248

(* Basic dependencies *)

249

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

250

g

251


252

end

253


254

module NodeDep = struct

255


256

module ExprModule =

257

struct

258

type t = expr

259

let compare = compare

260

let hash n = Hashtbl.hash n

261

let equal n1 n2 = n1 = n2

262

end

263


264

module ESet = Set.Make(ExprModule)

265


266

let rec get_expr_calls prednode expr =

267

match expr.expr_desc with

268

 Expr_const _

269

 Expr_ident _ > ESet.empty

270

 Expr_access (e, _)

271

 Expr_power (e, _) > get_expr_calls prednode e

272

 Expr_array t

273

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

274

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

275

 Expr_fby (e1,e2)

276

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

277

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

278

 Expr_pre e

279

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

280

 Expr_appl (id,e, _) >

281

if not (Basic_library.is_internal_fun id) && prednode id

282

then ESet.add expr (get_expr_calls prednode e)

283

else (get_expr_calls prednode e)

284


285

let get_callee expr =

286

match expr.expr_desc with

287

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

288

 _ > None

289


290

let get_calls prednode eqs =

291

let deps =

292

List.fold_left

293

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

294

ESet.empty

295

eqs in

296

ESet.elements deps

297


298

let dependence_graph prog =

299

let g = new_graph () in

300

let g = List.fold_right

301

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

302

match td.top_decl_desc with

303

 Node nd >

304

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

305

let accu = add_vertices [nd.node_id] accu in

306

let deps = List.map (fun e > fst (desome (get_callee e))) (get_calls (fun _ > true) (get_node_eqs nd)) in

307

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

308

add_edges [nd.node_id] deps accu

309

 _ > assert false (* should not happen *)

310


311

) prog g in

312

g

313


314

let rec filter_static_inputs inputs args =

315

match inputs, args with

316

 [] , [] > []

317

 v::vq, a::aq > if v.var_dec_const then (dimension_of_expr a) :: filter_static_inputs vq aq else filter_static_inputs vq aq

318

 _ > assert false

319


320

let compute_generic_calls prog =

321

List.iter

322

(fun td >

323

match td.top_decl_desc with

324

 Node nd >

325

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

326

nd.node_gencalls < get_calls prednode (get_node_eqs nd)

327

 _ > ()

328


329

) prog

330


331

end

332


333

module CycleDetection = struct

334


335

(*  Look for cycles in a dependency graph *)

336

module Cycles = Graph.Components.Make (IdentDepGraph)

337


338

let mk_copy_var n id =

339

let used name =

340

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

341

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

342

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

343

in mk_new_name used id

344


345

let mk_copy_eq n var =

346

let var_decl = get_node_var var n in

347

let cp_var = mk_copy_var n var in

348

let expr =

349

{ expr_tag = Utils.new_tag ();

350

expr_desc = Expr_ident var;

351

expr_type = var_decl.var_type;

352

expr_clock = var_decl.var_clock;

353

expr_delay = Delay.new_var ();

354

expr_annot = None;

355

expr_loc = var_decl.var_loc } in

356

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

357

mkeq var_decl.var_loc ([cp_var], expr)

358


359

let wrong_partition g partition =

360

match partition with

361

 [id] > IdentDepGraph.mem_edge g id id

362

 _::_::_ > true

363

 [] > assert false

364


365

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

366

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

367

let check_cycles g =

368

let scc_l = Cycles.scc_list g in

369

List.iter (fun partition >

370

if wrong_partition g partition then

371

raise (Cycle partition)

372

else ()

373

) scc_l

374


375

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

376

let copy_partition g partition =

377

let copy_g = IdentDepGraph.create () in

378

IdentDepGraph.iter_edges

379

(fun src tgt >

380

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

381

then IdentDepGraph.add_edge copy_g src tgt)

382

g

383


384


385

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

386

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

387

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

388

let break_cycle head cp_head g =

389

let succs = IdentDepGraph.succ g head in

390

IdentDepGraph.add_edge g head cp_head;

391

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

392

List.iter

393

(fun s >

394

IdentDepGraph.remove_edge g head s;

395

IdentDepGraph.add_edge g s cp_head)

396

succs

397


398

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

399

belonging in node [node]. Returns:

400

 a list of new auxiliary variable declarations

401

 a list of new equations

402

 a modified acyclic version of [g]

403

*)

404

let break_cycles node mems g =

405

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

406

let rec break vdecls mem_eqs g =

407

let scc_l = Cycles.scc_list g in

408

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

409

match wrong with

410

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

411

 [head]::_ >

412

begin

413

IdentDepGraph.remove_edge g head head;

414

break vdecls mem_eqs g

415

end

416

 (head::part)::_ >

417

begin

418

let vdecl_cp_head, cp_eq = mk_copy_eq node head in

419

let pvar v = List.mem v part in

420

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

421

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

422

break_cycle head vdecl_cp_head.var_id g;

423

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

424

end

425

 _ > assert false

426

in break [] mem_eqs g

427


428

end

429


430

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

431

module Disjunction =

432

struct

433

module ClockedIdentModule =

434

struct

435

type t = var_decl

436

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

437

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

438

end

439


440

module CISet = Set.Make(ClockedIdentModule)

441


442

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

443

maybe removing shorter branches *)

444

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

445


446

let pp_ciset fmt t =

447

begin

448

Format.fprintf fmt "{@ ";

449

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

450

Format.fprintf fmt "}@."

451

end

452


453

let clock_disjoint_map vdecls =

454

let map = Hashtbl.create 23 in

455

begin

456

List.iter

457

(fun v1 > let disj_v1 =

458

List.fold_left

459

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

460

CISet.empty

461

vdecls in

462

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

463

Hashtbl.add map v1.var_id disj_v1)

464

vdecls;

465

(map : disjoint_map)

466

end

467


468

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

469

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

470

 the mapping v > ... then disappears

471

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

472

*)

473

let merge_in_disjoint_map map v v' =

474

begin

475

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

476

Hashtbl.remove map v.var_id;

477

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;

478

end

479


480

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

481

[v'] is a dead variable. Then:

482

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

483

 the mapping v > ... then disappears

484

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

485

*)

486

let replace_in_disjoint_map map v v' =

487

begin

488

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

489

Hashtbl.remove map v.var_id;

490

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;

491

end

492


493

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

494

 the mapping v > ... then disappears

495

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

496

*)

497

let remove_in_disjoint_map map v =

498

begin

499

Hashtbl.remove map v.var_id;

500

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

501

end

502


503

let pp_disjoint_map fmt map =

504

begin

505

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

506

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

507

Format.fprintf fmt "}@."

508

end

509

end

510


511

let pp_dep_graph fmt g =

512

begin

513

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

514

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

515

Format.fprintf fmt "}@."

516

end

517


518

let pp_error fmt trace =

519

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

520

(fprintf_list ~sep:", " pp_print_string) trace

521


522

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

523

let merge_with g1 g2 =

524

begin

525

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

526

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

527

end

528


529

let add_external_dependency outputs mems g =

530

let caller ="!!_world" in

531

begin

532

IdentDepGraph.add_vertex g caller;

533

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

534

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

535

end

536


537

let global_dependency node =

538

let mems = ExprDep.node_memory_variables node in

539

let inputs =

540

ISet.union

541

(ExprDep.node_input_variables node)

542

(ExprDep.node_constant_variables node) in

543

let outputs = ExprDep.node_output_variables node in

544

let node_vars = ExprDep.node_variables node in

545

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

546

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

547

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

548

CycleDetection.check_cycles g_non_mems;

549

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

550

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

551

begin

552

merge_with g_non_mems g_mems';

553

add_external_dependency outputs mems g_non_mems;

554

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

555

g_non_mems

556

end

557


558

(* Local Variables: *)

559

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

560

(* End: *)
