Project

General

Profile

« Previous | Next » 

Revision 1daf7bf0

Added by Lélio Brun 8 months ago

systematically add dependencies to clock variables in rhs

View differences:

src/causality.ml
69 69
let add_edges src tgt g =
70 70
 (*List.iter (fun s -> List.iter (fun t -> Format.eprintf "add %s -> %s@." s t) tgt) src;*)
71 71
  List.iter
72
    (fun s ->
73
      List.iter
74
	(fun t -> IdentDepGraph.add_edge g s t)
75
	tgt)
72
    (fun s -> List.iter (IdentDepGraph.add_edge g s) tgt)
76 73
    src;
77 74
  g
78 75

  
......
209 206
  let add_eq_dependencies mems inputs node_vars eq (g, g') =
210 207
    let add_var lhs_is_mem lhs x (g, g') =
211 208
      if is_instance_var x || ISet.mem x node_vars then
212
	if ISet.mem x mems
213
	then
214
	  let g = add_edges lhs [mk_read_var x] g in
215
	  if lhs_is_mem
216
	  then
217
	    (g, add_edges [x] lhs g')
218
	  else
219
	    (add_edges [x] lhs g, g')
220
	else
221
	  let x = if ISet.mem x inputs then mk_read_var x else x in
222
	  (add_edges lhs [x] g, g')
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')
223 220
      else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *)
224 221
    in
225
  (* Add dependencies from [lhs] to rhs clock [ck]. *)
222
    (* Add dependencies from [lhs] to rhs clock [ck]. *)
226 223
    let rec add_clock lhs_is_mem lhs ck g =
227
    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
224
      (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
228 225
      match (Clocks.repr ck).Clocks.cdesc with
229
      | Clocks.Con (ck', cr, _)   -> add_var lhs_is_mem lhs (Clocks.const_of_carrier cr) (add_clock lhs_is_mem lhs ck' g)
230
      | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g
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 231
      | _                         -> g 
232 232
    in
233 233
    let rec add_dep lhs_is_mem lhs rhs g =
234
    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
235
    (* i.e every input is connected to every output, through a ghost var *)
234
      (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)
235
      (* i.e every input is connected to every output, through a ghost var *)
236 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) 
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 240
      in
241
      let g = add_clock lhs_is_mem lhs rhs.expr_clock g in
241 242
      match rhs.expr_desc with
242 243
      | Expr_const _    -> g
243 244
      | Expr_fby (e1, e2)  -> add_dep true lhs e2 (add_dep false lhs e1 g)
244 245
      | Expr_pre e      -> add_dep true lhs e g
245
      | Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)
246
      | Expr_ident x -> add_var lhs_is_mem lhs x g
246 247
      | Expr_access (e1, d)
247 248
      | Expr_power (e1, d) -> add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g)
248 249
      | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g
......
252 253
      | Expr_arrow (e1, e2)  -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
253 254
      | Expr_when  (e, c, _)  -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
254 255
      | Expr_appl (f, e, None) ->
255
	 if Basic_library.is_expr_internal_fun rhs
256
      (* tuple component-wise dependency for internal operators *)
257
	 then
258
	   List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
259
      (* mashed up dependency for user-defined operators *)
260
	 else
261
	   mashup_appl_dependencies f e g
256
        if Basic_library.is_expr_internal_fun rhs
257
        (* tuple component-wise 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 user-defined operators *)
261
        else
262
          mashup_appl_dependencies f e g
262 263
      | Expr_appl (f, e, Some c) ->
263
	 mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
264
        mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
264 265
    in
265
    let g =
266
      List.fold_left
267
	(fun g lhs ->
268
	  if ISet.mem lhs mems then
269
	    add_vertices [lhs; mk_read_var lhs] g
270
	  else
271
	    add_vertices [lhs] g
272
	)
273
	g eq.eq_lhs
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
274 272
    in
275 273
    add_dep false eq.eq_lhs eq.eq_rhs (g, g')
276
      
274

  
277 275

  
278 276
  (* Returns the dependence graph for node [n] *)
279 277
  let dependence_graph mems inputs node_vars n =
280 278
    instance_var_cpt := 0;
281 279
    let g = new_graph (), new_graph () in
282 280
    (* Basic dependencies *)
283
    let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in
281
    let g = List.fold_right (add_eq_dependencies mems inputs node_vars)
282
        (get_node_eqs n) g in
284 283
    (* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il
285 284
       faut imposer que les outputs dépendent des asserts pour identifier que les
286 285
       fcn calls des asserts sont évalués avant le noeuds *)
......
665 664
    begin
666 665
      merge_with g_non_mems g_mems';
667 666
      add_external_dependency outputs mems g_non_mems;
668
      { node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals }, 
667
      { node with
668
        node_stmts = List.map (fun eq -> Eq eq) eqs';
669
        node_locals = vdecls' @ node.node_locals },
669 670
      g_non_mems
670 671
    end
671
  with Error (DataCycle _ as exc) -> (
672
      raise (Error (exc))
673
  )
672
  with Error (DataCycle _ as exc) ->
673
    raise (Error (exc))
674 674

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

Also available in: Unified diff