Project

General

Profile

« Previous | Next » 

Revision c9043042

Added by Pierre-Loïc Garoche about 5 years ago

Issues with Causality and asserts

View differences:

src/causality.ml
201 201
      else
202 202
	let x = if ISet.mem x inputs then mk_read_var x else x in
203 203
	(add_edges lhs [x] g, g')
204
    else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *) in
205
(* Add dependencies from [lhs] to rhs clock [ck]. *)
204
    else (add_edges lhs [mk_read_var x] g, g') (* x is a global constant, treated as a read var *)
205
  in
206
  (* Add dependencies from [lhs] to rhs clock [ck]. *)
206 207
  let rec add_clock lhs_is_mem lhs ck g =
207 208
    (*Format.eprintf "add_clock %a@." Clocks.print_ck ck;*)
208 209
    match (Clocks.repr ck).Clocks.cdesc with
......
244 245
  in
245 246
  let g =
246 247
    List.fold_left
247
      (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
248
      (fun g lhs ->
249
	if ISet.mem lhs mems then
250
	  add_vertices [lhs; mk_read_var lhs] g
251
	else
252
	  add_vertices [lhs] g
253
      )
254
      g eq.eq_lhs
255
  in
248 256
  add_dep false eq.eq_lhs eq.eq_rhs (g, g')
249 257
  
250 258

  
......
254 262
  let g = new_graph (), new_graph () in
255 263
  (* Basic dependencies *)
256 264
  let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in
265
  (* TODO Xavier: un essai ci dessous. Ca n'a pas l'air de résoudre le pb. Il
266
     faut imposer que les outputs dépendent des asserts pour identifier que les
267
     fcn calls des asserts sont évalués avant le noeuds *)
268

  
269
  (* (\* In order to introduce dependencies between assert expressions and the node, *)
270
  (*    we build an artificial dependency between node output and each assert *)
271
  (*    expr. While these are not valid equations, they should properly propage in *)
272
  (*    function add_eq_dependencies *\) *)
273
  (* let g = *)
274
  (*   let output_vars_as_lhs = ISet.elements (node_output_variables n) in *)
275
  (*   List.fold_left (fun g ae -> *)
276
  (*     let fake_eq = mkeq Location.dummy_loc (output_vars_as_lhs, ae.assert_expr) in *)
277
  (*   add_eq_dependencies mems inputs node_vars fake_eq g *)
278
  (* ) g n.node_asserts in  *)
257 279
  g
258 280

  
259
end
260

  
261
module NodeDep = struct
262

  
263
  module ExprModule =
264
  struct
265
    type t = expr
266
    let compare = compare
267
    let hash n = Hashtbl.hash n
268
    let equal n1 n2 = n1 = n2
269
  end
270

  
271
  module ESet = Set.Make(ExprModule)
272

  
273
  let rec get_expr_calls prednode expr = 
274
    match expr.expr_desc with
275
      | Expr_const _ 
276
      | Expr_ident _ -> ESet.empty
277
      | Expr_access (e, _)
278
      | Expr_power (e, _) -> get_expr_calls prednode e
279
      | Expr_array t
280
      | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
281
      | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
282
      | Expr_fby (e1,e2)
283
      | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
284
      | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
285
      | Expr_pre e 
286
      | Expr_when (e,_,_) -> get_expr_calls prednode e
287
      | Expr_appl (id,e, _) ->
288
	if not (Basic_library.is_expr_internal_fun expr) && prednode id
289
	then ESet.add expr (get_expr_calls prednode e)
290
	else (get_expr_calls prednode e)
291

  
292
  let get_callee expr =
293
    match expr.expr_desc with
294
    | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
295
    | _ -> None
296

  
297
  let get_calls prednode eqs =
298
    let deps =
299
      List.fold_left 
300
	(fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
301
	ESet.empty
302
	eqs in
303
    ESet.elements deps
304

  
305
  let dependence_graph prog =
306
  let g = new_graph () in
307
  let g = List.fold_right 
308
    (fun td accu -> (* for each node we add its dependencies *)
281
   end
282

  
283
   module NodeDep = struct
284

  
285
   module ExprModule =
286
   struct
287
   type t = expr
288
   let compare = compare
289
   let hash n = Hashtbl.hash n
290
   let equal n1 n2 = n1 = n2
291
   end
292

  
293
   module ESet = Set.Make(ExprModule)
294

  
295
   let rec get_expr_calls prednode expr = 
296
   match expr.expr_desc with
297
   | Expr_const _ 
298
   | Expr_ident _ -> ESet.empty
299
   | Expr_access (e, _)
300
   | Expr_power (e, _) -> get_expr_calls prednode e
301
   | Expr_array t
302
   | Expr_tuple t -> List.fold_right (fun x set -> ESet.union (get_expr_calls prednode x) set) t ESet.empty
303
   | Expr_merge (_,hl) -> List.fold_right (fun (_,h) set -> ESet.union (get_expr_calls prednode h) set) hl ESet.empty
304
   | Expr_fby (e1,e2)
305
   | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
306
   | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
307
   | Expr_pre e 
308
   | Expr_when (e,_,_) -> get_expr_calls prednode e
309
   | Expr_appl (id,e, _) ->
310
   if not (Basic_library.is_expr_internal_fun expr) && prednode id
311
   then ESet.add expr (get_expr_calls prednode e)
312
   else (get_expr_calls prednode e)
313

  
314
   let get_callee expr =
315
   match expr.expr_desc with
316
   | Expr_appl (id, args, _) -> Some (id, expr_list_of_expr args)
317
   | _ -> None
318

  
319
   let get_calls prednode eqs =
320
   let deps =
321
   List.fold_left 
322
   (fun accu eq -> ESet.union accu (get_expr_calls prednode eq.eq_rhs))
323
   ESet.empty
324
   eqs in
325
   ESet.elements deps
326

  
327
   let dependence_graph prog =
328
   let g = new_graph () in
329
   let g = List.fold_right 
330
   (fun td accu -> (* for each node we add its dependencies *)
309 331
      match td.top_decl_desc with 
310 332
	| Node nd ->
311 333
	  (*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *)

Also available in: Unified diff