Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal_extract.ml @ 0d79d0f3

History | View | Annotate | Download (12.2 KB)

1
open Lustre_types
2
open Utils
3
open Seal_utils			
4

    
5
(* Switched system extraction *)
6
type element = IsInit | Expr of expr
7
type guard = (element * bool) list
8
type guarded_expr = guard * element
9
type mdef_t = guarded_expr list
10

    
11
let pp_elem fmt e =
12
  match e with
13
  | IsInit -> Format.fprintf fmt "init"
14
  | Expr e -> Printers.pp_expr fmt e
15

    
16
let pp_guard_expr fmt (gl,e) =
17
  Format.fprintf fmt "%a -> %a"
18
    (fprintf_list ~sep:"; "
19
       (fun fmt (e,b) -> if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) gl
20
    pp_elem e
21

    
22
let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel
23

    
24
  
25
let add_init defs vid =
26
  Hashtbl.add defs vid [[], IsInit]
27

    
28
let deelem e =  match e with
29
    Expr e -> e
30
  | IsInit -> assert false (* Wasn't expecting isinit here: we are building values! *)
31

    
32
let is_eq_elem elem elem' =
33
  match elem, elem' with
34
  | IsInit, IsInit -> true
35
  | Expr e, Expr e' ->
36
     Corelang.is_eq_expr e e'
37
  | _ -> false
38

    
39
let select_elem elem (gelem, _) =
40
  is_eq_elem elem gelem
41

    
42
  
43
let combine_guards ?(fresh=None) gl1 gl2 =
44
  (* Filtering out trivial cases. More semantics ones would have to be
45
     addressed later *)
46
  let check (gexpr, posneg) l =
47
    (* Check if gepxr is part of l *)
48
    let sel_fun = select_elem gexpr in
49
    if List.exists sel_fun l then
50
      (* Checking the guard value posneg *)
51
      let _, status = List.find sel_fun l in
52
      status=posneg, l
53
    else
54
      (* Valid: no overlap *)
55
      true, (gexpr, posneg)::l
56
  in
57
  let ok, gl =
58
    List.fold_left (
59
        fun (ok, l) g ->
60
        (* Bypass for negative output *)
61
        if not ok then false, []
62
        else
63
          check g l 
64
      ) (true, gl2) gl1
65
  in
66
  if ok then
67
    match fresh with
68
      None -> true, gl
69
    | Some fresh_g -> (
70
    (* Checking the fresh element *)
71
      check fresh_g gl
72
    )
73
  else
74
    ok, []
75

    
76
(* Encode "If gel1=posneg then gel2":
77
   - Compute the combination of guarded exprs in gel1 and gel2:
78
     - Each guarded_expr in gel1 is transformed as a guard: the
79
       expression is associated to posneg.
80
     - Existing guards in gel2 are concatenated to that list of guards
81
     - We keep expr in the ge of gel2 as the legitimate expression 
82
 *)
83
let concatenate_ge gel1 posneg gel2 =
84
  List.fold_left (
85
      fun accu (g2,e2) ->
86
      List.fold_left (
87
          fun accu (g1,e1) ->
88
          let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in
89
          if ok then
90
            (gl, e2)::accu
91
          else
92
            accu
93
        ) accu gel1
94
    ) [] gel2
95

    
96
let rec rewrite defs expr : guarded_expr list =
97
  let rewrite = rewrite defs in
98
  match expr.expr_desc with
99
  | Expr_appl (id, args, None) ->
100
     let args = rewrite args in
101
     List.map (fun (guards, e) ->
102
           guards,
103
           Expr {expr with expr_desc = Expr_appl(id, deelem e, None)}
104
       ) args 
105
  | Expr_const _  -> [[], Expr expr]
106
  | Expr_ident id ->
107
     if Hashtbl.mem defs id then
108
       Hashtbl.find defs id
109
     else
110
       (* id should be an input *)
111
       [[], Expr expr]
112
  | Expr_ite (g, e1, e2) ->
113
     let g = rewrite g and
114
         e1 = rewrite e1 and
115
         e2 = rewrite e2 in
116
     (concatenate_ge g true e1)@
117
       (concatenate_ge g false e2)
118
  | Expr_merge (g, branches) ->
119
     assert false (* TODO: deal with merges *)
120
    
121
  | Expr_when (e, _, _) -> rewrite e
122
  | Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *)
123
  | Expr_tuple el ->
124
     (* Each expr is associated to its flatten guarded expr list *)
125
     let gell = List.map rewrite el in
126
     (* Computing all combinations: we obtain a list of guarded tuple *)
127
     let rec aux gell : (guard * expr list) list =
128
       match gell with
129
       | [] -> assert false (* Not happening *)
130
       | [gel] -> List.map (fun (g,e) -> g, [deelem e]) gel
131
       | gel::getl ->
132
          let getl = aux getl in
133
          List.fold_left (
134
              fun accu (g,e) ->
135
              List.fold_left (
136
                    fun accu (gl, minituple) ->
137
                    let is_compat, guard_comb = combine_guards g gl in
138
                    if is_compat then
139
                      let new_gt : guard * expr list = (guard_comb, (deelem e)::minituple) in
140
                      new_gt::accu
141
                    else
142
                      accu
143
                  
144
                  ) accu getl
145
            ) [] gel
146
     in
147
     let gtuples = aux gell in
148
     (* Rebuilding the valid type: guarded expr list (with tuple exprs) *)
149
     List.map (fun (g,tuple) -> g, Expr {expr with expr_desc = Expr_tuple tuple}) gtuples
150
  | Expr_fby _
151
    | Expr_appl _
152
                (* Should be removed by mormalization and inlining *)
153
    -> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false
154
  | Expr_array _ | Expr_access _ | Expr_power _
155
                                              (* Arrays not handled here yet *)
156
    -> assert false
157
  | Expr_pre _ -> (* Not rewriting mem assign *)
158
     assert false
159
and add_def defs vid expr =
160
  Hashtbl.add defs vid (rewrite defs expr)
161

    
162
(* Takes a list of guarded exprs (ge) and a guard
163
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.
164

    
165
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *)
166
let split_mdefs elem (mdefs: guarded_expr list) =
167
  List.fold_left (
168
      fun (selected, left_out)
169
          ((guards, expr) as ge) ->
170
      (* select the element of guards that match the argument elem *)
171
      let sel, others_guards = List.partition (select_elem elem) guards in
172
      match sel with
173
      (* we extract the element from the list and add it to the
174
         appropriate list *)
175
      | [_, sel_status] ->
176
         if sel_status then
177
           (others_guards,expr)::selected, left_out
178
         else selected, (others_guards,expr)::left_out
179
      | [] -> (* no such guard exists, we have to duplicate the
180
              guard_expr in both lists *)
181
         ge::selected, ge::left_out
182
      | _ -> (
183
        Format.eprintf "@.Spliting list on elem %a.@.List:%a@."
184
          pp_elem elem
185
          pp_mdefs mdefs;
186
        assert false (* more then one element selected. Should
187
                          not happen , or trival dead code like if
188
                              x then if not x then dead code *)
189
      )
190
    ) ([],[]) mdefs
191
    
192
let split_mem_defs
193
      (elem: element)
194
      (mem_defs: (ident * guarded_expr list) list) :
195
      ((ident * mdef_t) list) * ((ident * mdef_t) list)
196
  =
197
  List.fold_right (fun (m,mdefs)
198
                       (accu_pos, accu_neg) ->
199
      let pos, neg =
200
        split_mdefs elem mdefs
201
      in
202
      (m, pos)::accu_pos,
203
      (m, neg)::accu_neg
204
    ) mem_defs ([],[])
205

    
206

    
207
(* Split a list of mem_defs into init and step lists of guarded
208
   expressions per memory. *)
209
let split_init mem_defs =
210
  split_mem_defs IsInit mem_defs
211

    
212
let pick_guard mem_defs : expr =
213
  let gel = List.flatten (List.map snd mem_defs) in
214
  let gl = List.flatten (List.map fst gel) in
215
  let all_guards =
216
    List.map (
217
        (* selecting guards and getting rid of boolean *)
218
        fun (e,b) ->
219
        match e with
220
        | Expr e -> e
221
        | _ -> assert false
222
      (* should have been filtered out
223
                                      yet *)
224
      ) gl
225
  in
226
  (* TODO , one could sort by occurence and provided the most common
227
     one *)
228
  List.hd all_guards  
229
  
230
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions)
231
*)
232
let rec build_switch_sys
233
          (mem_defs : (Utils.ident * guarded_expr list) list )
234
          prefix
235
        :
236
          ((expr * bool) list * (ident * expr) list ) list =
237
  (* if all mem_defs have empty guards, we are done, return prefix,
238
     mem_defs expr.
239

    
240
     otherwise pick a guard in one of the mem, eg (g, b) then for each
241
     other mem, one need to select the same guard g with the same status b, *)
242
  if List.for_all (fun (m,mdefs) ->
243
         (* All defs are unguarded *)
244
         match mdefs with
245
         | [[], _] -> true
246
         | _ -> false) mem_defs
247
  then
248
    [prefix ,
249
     List.map (fun (m,gel) ->
250
         match gel with
251
         | [_,e] ->
252
            let e =
253
              match e with
254
              | Expr e -> e
255
              | _ -> assert false (* No IsInit expression *)
256
            in
257
            m,e
258
         | _ -> assert false
259
       ) mem_defs]
260
  else
261
    (* Picking a guard *)
262
    let elem : expr = pick_guard mem_defs in
263
    let pos, neg =
264
      split_mem_defs
265
        (Expr elem)
266
        mem_defs
267
    in
268
    (* Special cases to avoid useless computations: true, false conditions *)
269
    match elem.expr_desc with
270
    | Expr_ident "true"  ->   build_switch_sys pos prefix
271
    | Expr_const (Const_tag tag) when tag = Corelang.tag_true
272
                         ->   build_switch_sys pos prefix
273
    | Expr_ident "false" ->   build_switch_sys neg prefix
274
    | Expr_const (Const_tag tag) when tag = Corelang.tag_false 
275
                         ->   build_switch_sys neg prefix
276
    | _ -> (* Regular case *)
277
       (* let _ = (
278
        *     Format.eprintf "Expr is %a@." Printers.pp_expr elem;
279
        *     match elem.expr_desc with
280
        *     | Expr_const _ -> Format.eprintf "a const@."
281
        *                     
282
        *     | Expr_ident _ -> Format.eprintf "an ident@."
283
        *     | _ -> Format.eprintf "something else@."
284
        *   )
285
        * in *)
286
       (build_switch_sys pos ((elem, true)::prefix))
287
       @
288
         (build_switch_sys neg ((elem, false)::prefix))
289
      
290

    
291

    
292
      
293
(* Take a normalized node and extract a list of switches: (cond,
294
   update) meaning "if cond then update" where update shall define all
295
   node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *)
296
let node_as_switched_sys (mems:var_decl list) nd =
297
  (* rescheduling node: has been scheduled already, no need to protect
298
     the call to schedule_node *)
299
  let nd_report = Scheduling.schedule_node nd in
300
  let schedule = nd_report.Scheduling_type.schedule in
301
  let sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in
302
  let defs : (ident,  guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
303
  let add_def = add_def defs in
304
  (* Registering node equations *)
305
  let mem_defs =
306
    List.fold_left (fun accu eq ->
307
        match eq.eq_lhs with
308
        | [vid] ->
309
           (* Only focus on non memory definitions *)
310
           if not (List.exists (fun v -> v.var_id = vid) mems) then (
311
             report ~level:3 (fun fmt -> Format.fprintf fmt "Registering variable %s@." vid);
312
             add_def vid eq.eq_rhs;
313
             accu
314
           )
315
           else
316
             (
317
               match eq.eq_rhs.expr_desc with
318
               | Expr_pre def_m ->
319
                  report ~level:3 (fun fmt -> Format.fprintf fmt "Preparing mem %s@." vid);
320

    
321
                  (vid, rewrite defs def_m)::accu
322
               | _ -> assert false
323
             )
324
        | _ -> assert false (* should have been removed by normalization *)
325
      ) [] sorted_eqs
326
  in
327
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out memories definitions (may takes time)@.");
328
  (* Printing memories definitions *)
329
  report ~level:3
330
    (fun fmt ->
331
      Format.fprintf fmt
332
        "%a"
333
        (Utils.fprintf_list ~sep:"@."
334
           (fun fmt (m,mdefs) ->
335
             Format.fprintf fmt
336
               "%s -> @[<v 0>[%a@] ]@."
337
               m
338
               (Utils.fprintf_list ~sep:"@ "
339
                  pp_guard_expr) mdefs
340
        ))
341
        mem_defs);
342
  let init_defs, update_defs =
343
    split_init mem_defs
344
  in
345
  report ~level:3
346
    (fun fmt ->
347
      Format.fprintf fmt
348
        "Init:@.%a@.Step@.%a"
349
        (Utils.fprintf_list ~sep:"@."
350
           (fun fmt (m,mdefs) ->
351
             Format.fprintf fmt
352
               "%s -> @[<v 0>[%a@] ]@."
353
               m
354
               (Utils.fprintf_list ~sep:"@ "
355
                  pp_guard_expr) mdefs
356
        ))
357
        init_defs
358
        (Utils.fprintf_list ~sep:"@."
359
           (fun fmt (m,mdefs) ->
360
             Format.fprintf fmt
361
               "%s -> @[<v 0>[%a@] ]@."
362
               m
363
               (Utils.fprintf_list ~sep:"@ "
364
                  pp_guard_expr) mdefs
365
        ))
366
        update_defs);
367
  let sw_init= 
368
    build_switch_sys init_defs []
369
  in
370
  let sw_sys =
371
    build_switch_sys update_defs []
372
  in
373
  sw_init, sw_sys