Project

General

Profile

Revision 0d79d0f3 src/tools/seal_utils.ml

View differences:

src/tools/seal_utils.ml
3 3
   
4 4
let report = Log.report ~plugin:"seal"
5 5

  
6
			
7
			
8
(******************************************************************************)
9
(* Computing a slice of a node, selecting only some variables, based on       *)
10
(* their COI (cone of influence)                                              *)
11
(******************************************************************************)
12 6

  
13
(* Basic functions to search into nodes. Could be moved to corelang eventually *)
14
let is_variable nd vid = 
15
  List.exists
16
    (fun v -> v.var_id = vid)
17
    nd.node_locals
18
  
19
let find_variable nd vid = 
20
  List.find
21
    (fun v -> v.var_id = vid)
22
    nd.node_locals
23

  
24
(* Returns the vars required to compute v. 
25
   Memories are specifically identified. *)
26
let coi_var deps nd v =
27
  let vname = v.var_id in
28
  let sliced_deps =
29
    Causality.slice_graph deps vname
30
  in
31
  (* Format.eprintf "sliced graph for %a: %a@."
32
   *   Printers.pp_var v
33
   *   Causality.pp_dep_graph sliced_deps; *)
34
  let vset, memset =
35
    IdentDepGraph.fold_vertex
36
      (fun vname (vset,memset)  ->
37
       if Causality.ExprDep.is_read_var vname
38
       then
39
         let vname' = String.sub vname 1 (-1 + String.length vname) in
40
         if is_variable nd vname' then
41
           ISet.add vname' vset,
42
           ISet.add vname' memset
43
         else
44
           vset, memset
45
       else
46
         ISet.add vname vset, memset
47
      )
48
      sliced_deps
49
      (ISet.singleton vname, ISet.empty)
50
  in
51
  report ~level:3 (fun fmt -> Format.fprintf fmt "COI of var %s: (%a // %a)@."
52
					     v.var_id
53
					     (fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements vset)
54
					     (fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements memset)
55
		  )  ;
56
  vset, memset
57

  
58
	  
59
(* Computes the variables required to compute vl. Variables /seen/ do not need
60
     to be computed *)
61
let rec coi_vars deps nd vl seen =
62
  let coi_vars = coi_vars deps nd in
63
  List.fold_left
64
    (fun accu v ->
65
     let vset, memset = coi_var deps nd v in
66
     (* We handle the new mems discovered in the coi *)
67
     let memset =
68
       ISet.filter (
69
           fun vid ->
70
           not
71
             (List.exists
72
                (fun v -> v.var_id = vid)
73
                vl
74
             ) 
75
         ) memset
76
     in
77
     let memset_vars = 
78
       ISet.fold (
79
           fun vid accu ->
80
           (find_variable nd vid)::accu
81
         ) memset [] 
82
     in
83
     let vset' =
84
       coi_vars memset_vars (vl@seen)
85
     in
86
     ISet.union accu (ISet.union vset vset')
87
    )
88
    ISet.empty
89
    (List.filter
90
       (fun v -> not (List.mem v seen))
91
       vl
92
    )
93
    
94
    
95
(* compute the coi of vars_to_keeps in node nd *)
96
let compute_sliced_vars vars_to_keep deps nd =
97
  ISet.elements (coi_vars deps nd vars_to_keep []) 
98

  
99

  
100

  
101

  
102

  
103
  (* If existing outputs are included in vars_to_keep, just slice the content.
104
   Otherwise outputs are replaced by vars_to_keep *)
105
let slice_node vars_to_keep msch nd =
106
  let coi_vars =
107
    compute_sliced_vars vars_to_keep msch.Scheduling_type.dep_graph nd
108
  in
109
  report ~level:3 (fun fmt -> Format.fprintf fmt
110
                                  "COI Vars: %a@."
111
    (Utils.fprintf_list ~sep:"," Format.pp_print_string)
112
     coi_vars);
113
  let outputs =
114
    List.filter
115
      (
116
        fun v -> List.mem v.var_id coi_vars 
117
      ) nd.node_outputs
118
  in
119
  let outputs = match outputs with
120
      [] -> (
121
      report ~level:1 (fun fmt -> Format.fprintf fmt "No visible output variable, subtituting with provided vars@ ");
122
      vars_to_keep
123
    )
124
    | l -> l
125
  in
126
  let locals =
127
    List.filter (fun v -> List.mem v.var_id coi_vars) nd.node_locals
128
  in
129

  
130
  (* Split tuples while sorting eqs *)
131
  let sorted_eqs = Scheduling.sort_equations_from_schedule nd msch.Scheduling_type.schedule in
132

  
133
  let stmts =
134
    List.filter (
135
        fun (* stmt ->
136
         * match stmt with
137
         * | Aut _ -> assert false
138
         * | Eq *) eq -> (
139
          match eq.eq_lhs with
140
            [vid] -> List.mem vid coi_vars
141
          | _ -> Format.eprintf "Faulty statement: %a@.@?" Printers.pp_node_eq eq; assert false
142
        (* should not happen after inlining and normalization *)
143
        )
144
      ) sorted_eqs
145
  in
146
  { nd
147
  with
148
    node_outputs = outputs;
149
    node_locals = locals;
150
    node_stmts = List.map (fun e -> Eq e) stmts 
151
  } 
152

  
153
(* Switched system extraction *)
154
type element = IsInit | Expr of expr
155
type guarded_expr = (element * bool) list * element
156
type mdef_t = guarded_expr list
157
            
158
let pp_guard_expr fmt (gl,e) =
159
  let pp_elem fmt e =
160
    match e with
161
    | IsInit -> Format.fprintf fmt "init"
162
    | Expr e -> Printers.pp_expr fmt e
163
  in 
164
       Format.fprintf fmt "%a -> %a"
165
         (fprintf_list ~sep:"; "
166
            (fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) gl
167
         pp_elem e
168
  
169
let concatenate_ge gel1 posneg gel2 =
170
  List.fold_left (
171
      fun accu (g2,e2) ->
172
      List.fold_left (
173
          fun accu (g1,e1) ->
174
          ((e1, posneg)::g1@g2, e2)::accu
175
        ) accu gel1
176
    ) [] gel2
177
  
178
let add_init defs vid =
179
  Hashtbl.add defs vid [[], IsInit]
180
  
181
let rec rewrite defs expr : guarded_expr list =
182
    match expr.expr_desc with
183
    | Expr_const _ | Expr_appl _ -> [[], Expr expr]
184
    | Expr_ident id ->
185
       if Hashtbl.mem defs id then
186
         Hashtbl.find defs id
187
       else
188
         (* id should be an input *)
189
         [[], Expr expr]
190
    | Expr_ite (g, e1, e2) ->
191
       let g = rewrite defs g and
192
           e1 = rewrite defs e1 and
193
           e2 = rewrite defs e2 in
194
       (concatenate_ge g true e1)@
195
         (concatenate_ge g false e2)
196
    | Expr_merge (g, branches) ->
197
       assert false (* TODO *)
198
      
199
    | Expr_when (e, _, _) -> rewrite defs e
200
    | Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *)
201
    | Expr_tuple _  | Expr_fby _ 
202
                                                           (* Should be removed by mormalization and inlining *)
203
      -> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false
204
    | Expr_array _ | Expr_access _ | Expr_power _
205
                                                (* Arrays not handled here yet *)
206
      -> assert false
207
    | Expr_pre _ -> (* Not rewriting mem assign *)
208
       assert false
209
and add_def defs vid expr =
210
  Hashtbl.add defs vid (rewrite defs expr)
211

  
212
(* Takes a list of guarded exprs (ge) and a guard
213
returns the same list of ge splited into the ones where the guard is true and the ones where it is false. In both lists the associated ge do not mention that guard anymore.
214

  
215
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *)
216
let split_mdefs elem (mdefs: guarded_expr list) =
217
  List.fold_left (
218
      fun (selected, left_out)
219
          ((guards, expr) as ge) ->
220
      (* select the element of guards that match the argument elem *)
221
      let select_fun (elem',_) =
222
        match elem, elem' with
223
        | IsInit, IsInit -> true
224
        | Expr e, Expr e' ->
225
           Corelang.is_eq_expr e e'
226
        | _ -> false
227
      in
228
      let sel, others_guards = List.partition select_fun guards in
229
      match sel with
230
      (* we extract the element from the list and add it to the
231
         appropriate list *)
232
      | [_, sel_status] ->
233
         if sel_status then
234
           (others_guards,expr)::selected, left_out
235
         else selected, (others_guards,expr)::left_out
236
      | [] -> (* no such guard exists, we have to duplicate the
237
              guard_expr in both lists *)
238
         ge::selected, ge::left_out
239
      | _ -> assert false (* more then one element selected. Should
240
                             not happen , or trival dead code like if
241
                             x then if not x then dead code *)
242
    ) ([],[]) mdefs
243
    
244
let split_mem_defs
245
      (elem: element)
246
      (mem_defs: (ident * guarded_expr list) list) :
247
      ((ident * mdef_t) list) * ((ident * mdef_t) list)
248
  =
249
  List.fold_right (fun (m,mdefs)
250
                       (accu_pos, accu_neg) ->
251
      let pos, neg =
252
        split_mdefs elem mdefs
253
      in
254
      (m, pos)::accu_pos,
255
      (m, neg)::accu_neg
256
    ) mem_defs ([],[])
257

  
258

  
259
(* Split a list of mem_defs into init and step lists of guarded
260
   expressions per memory. *)
261
let split_init mem_defs =
262
  split_mem_defs IsInit mem_defs
263

  
264
let pick_guard mem_defs : expr =
265
  let gel = List.flatten (List.map snd mem_defs) in
266
  let gl = List.flatten (List.map fst gel) in
267
  let all_guards =
268
    List.map (
269
        (* selecting guards and getting rid of boolean *)
270
        fun (e,b) ->
271
        match e with
272
        | Expr e -> e
273
        | _ -> assert false
274
      (* should have been filtered out
275
                                      yet *)
276
      ) gl
277
  in
278
  (* TODO , one could sort by occurence and provided the most common
279
     one *)
280
  List.hd all_guards  
281
  
282
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions)
283
*)
284
let rec build_switch_sys
285
          (mem_defs : (Utils.ident * guarded_expr list) list )
286
          prefix
287
        :
288
          ((expr * bool) list * (ident * expr) list ) list =
289
  (* if all mem_defs have empty guards, we are done, return prefix,
290
     mem_defs expr.
291

  
292
     otherwise pick a guard in one of the mem, eg (g, b) then for each
293
     other mem, one need to select the same guard g with the same status b, *)
294
  if List.for_all (fun (m,mdefs) ->
295
         (* All defs are unguarded *)
296
         match mdefs with
297
         | [[], _] -> true
298
         | _ -> false) mem_defs
299
  then
300
    [prefix ,
301
     List.map (fun (m,gel) ->
302
         match gel with
303
         | [_,e] ->
304
            let e =
305
              match e with
306
              | Expr e -> e
307
              | _ -> assert false (* No IsInit expression *)
308
            in
309
            m,e
310
         | _ -> assert false
311
       ) mem_defs]
312
  else
313
    (* Picking a guard *)
314
    let elem : expr = pick_guard mem_defs in
315
    let pos, neg =
316
      split_mem_defs
317
        (Expr elem)
318
        mem_defs
319
    in
320
    (* Special cases to avoid useless computations: true, false conditions *)
321
    match elem.expr_desc with
322
    | Expr_ident "true"  ->   build_switch_sys pos prefix
323
    | Expr_const (Const_tag tag) when tag = Corelang.tag_true
324
                         ->   build_switch_sys pos prefix
325
    | Expr_ident "false" ->   build_switch_sys neg prefix
326
    | Expr_const (Const_tag tag) when tag = Corelang.tag_false 
327
                         ->   build_switch_sys neg prefix
328
    | _ -> (* Regular case *)
329
       let _ = (
330
           Format.eprintf "Expr is %a@." Printers.pp_expr elem;
331
           match elem.expr_desc with
332
           | Expr_const _ -> Format.eprintf "a const@."
333
                           
334
           | Expr_ident _ -> Format.eprintf "an ident@."
335
           | _ -> Format.eprintf "something else@."
336
         )
337
       in
338
       (build_switch_sys pos ((elem, true)::prefix))
339
       @
340
         (build_switch_sys neg ((elem, false)::prefix))
341
      
342

  
343

  
344
      
345
(* Take a normalized node and extract a list of switches: (cond,
346
   update) meaning "if cond then update" where update shall define all
347
   node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *)
348
let node_as_switched_sys (mems:var_decl list) nd =
349
  (* rescheduling node: has been scheduled already, no need to protect
350
     the call to schedule_node *)
351
  let nd_report = Scheduling.schedule_node nd in
352
  let schedule = nd_report.Scheduling_type.schedule in
353
  let sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in
354
  let defs : (ident,  guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
355
  let add_def = add_def defs in
356
  (* Registering node equations *)
357
  let mem_defs =
358
    List.fold_left (fun accu eq ->
359
        match eq.eq_lhs with
360
        | [vid] ->
361
           (* Only focus on non memory definitions *)
362
           if not (List.exists (fun v -> v.var_id = vid) mems) then (
363
             add_def vid eq.eq_rhs;
364
             accu
365
           )
366
           else
367
             (
368
               match eq.eq_rhs.expr_desc with
369
               | Expr_pre def_m ->
370
                  (vid, rewrite defs def_m)::accu
371
               | _ -> assert false
372
             )
373
        | _ -> assert false (* should have been removed by normalization *)
374
      ) [] sorted_eqs
375
  in
376
  (* Printing memories definitions *)
377
  report ~level:3
378
    (fun fmt ->
379
      Format.fprintf fmt
380
        "%a"
381
        (Utils.fprintf_list ~sep:"@."
382
           (fun fmt (m,mdefs) ->
383
             Format.fprintf fmt
384
               "%s -> @[<v 0>[%a@] ]@."
385
               m
386
               (Utils.fprintf_list ~sep:"@ "
387
                  pp_guard_expr) mdefs
388
        ))
389
        mem_defs);
390
  let init_defs, update_defs =
391
    split_init mem_defs
392
  in
393
  report ~level:3
394
    (fun fmt ->
395
      Format.fprintf fmt
396
        "Init:@.%a@.Step@.%a"
397
        (Utils.fprintf_list ~sep:"@."
398
           (fun fmt (m,mdefs) ->
399
             Format.fprintf fmt
400
               "%s -> @[<v 0>[%a@] ]@."
401
               m
402
               (Utils.fprintf_list ~sep:"@ "
403
                  pp_guard_expr) mdefs
404
        ))
405
        init_defs
406
        (Utils.fprintf_list ~sep:"@."
407
           (fun fmt (m,mdefs) ->
408
             Format.fprintf fmt
409
               "%s -> @[<v 0>[%a@] ]@."
410
               m
411
               (Utils.fprintf_list ~sep:"@ "
412
                  pp_guard_expr) mdefs
413
        ))
414
        update_defs);
415
  let sw_init= 
416
    build_switch_sys init_defs []
417
  in
418
  let sw_sys =
419
    build_switch_sys update_defs []
420
  in
421
  sw_init, sw_sys

Also available in: Unified diff