Project

General

Profile

Revision 6517aa0e

View differences:

src/tools/seal/seal_extract.ml
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 eqs, auts = Corelang.get_node_eqs nd in
302
  assert (auts = []); (* Automata should be expanded by now *)
303
  let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
304
  let defs : (ident,  guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
305
  let add_def = add_def defs in
306
  (* Registering node equations *)
307
  let mem_defs =
308
    List.fold_left (fun accu eq ->
309
        match eq.eq_lhs with
310
        | [vid] ->
311
           (* Only focus on non memory definitions *)
312
           if not (List.exists (fun v -> v.var_id = vid) mems) then (
313
             report ~level:3 (fun fmt -> Format.fprintf fmt "Registering variable %s@." vid);
314
             add_def vid eq.eq_rhs;
315
             accu
316
           )
317
           else
318
             (
319
               match eq.eq_rhs.expr_desc with
320
               | Expr_pre def_m ->
321
                  report ~level:3 (fun fmt -> Format.fprintf fmt "Preparing mem %s@." vid);
322

  
323
                  (vid, rewrite defs def_m)::accu
324
               | _ -> assert false
325
             )
326
        | _ -> assert false (* should have been removed by normalization *)
327
      ) [] sorted_eqs
328
  in
329
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out memories definitions (may takes time)@.");
330
  (* Printing memories definitions *)
331
  report ~level:3
332
    (fun fmt ->
333
      Format.fprintf fmt
334
        "%a"
335
        (Utils.fprintf_list ~sep:"@."
336
           (fun fmt (m,mdefs) ->
337
             Format.fprintf fmt
338
               "%s -> @[<v 0>[%a@] ]@."
339
               m
340
               (Utils.fprintf_list ~sep:"@ "
341
                  pp_guard_expr) mdefs
342
        ))
343
        mem_defs);
344
  let init_defs, update_defs =
345
    split_init mem_defs
346
  in
347
  report ~level:3
348
    (fun fmt ->
349
      Format.fprintf fmt
350
        "Init:@.%a@.Step@.%a"
351
        (Utils.fprintf_list ~sep:"@."
352
           (fun fmt (m,mdefs) ->
353
             Format.fprintf fmt
354
               "%s -> @[<v 0>[%a@] ]@."
355
               m
356
               (Utils.fprintf_list ~sep:"@ "
357
                  pp_guard_expr) mdefs
358
        ))
359
        init_defs
360
        (Utils.fprintf_list ~sep:"@."
361
           (fun fmt (m,mdefs) ->
362
             Format.fprintf fmt
363
               "%s -> @[<v 0>[%a@] ]@."
364
               m
365
               (Utils.fprintf_list ~sep:"@ "
366
                  pp_guard_expr) mdefs
367
        ))
368
        update_defs);
369
  let sw_init= 
370
    build_switch_sys init_defs []
371
  in
372
  let sw_sys =
373
    build_switch_sys update_defs []
374
  in
375
  sw_init, sw_sys
src/tools/seal/seal_slice.ml
1
open Lustre_types
2
open Utils
3
open Seal_utils			
4
			
5
(******************************************************************************)
6
(* Computing a slice of a node, selecting only some variables, based on       *)
7
(* their COI (cone of influence)                                              *)
8
(******************************************************************************)
9

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

  
21
(* Returns the vars required to compute v. 
22
   Memories are specifically identified. *)
23
let coi_var deps nd v =
24
  let vname = v.var_id in
25
  let sliced_deps =
26
    Causality.slice_graph deps vname
27
  in
28
  (* Format.eprintf "sliced graph for %a: %a@."
29
   *   Printers.pp_var v
30
   *   Causality.pp_dep_graph sliced_deps; *)
31
  let vset, memset =
32
    IdentDepGraph.fold_vertex
33
      (fun vname (vset,memset)  ->
34
       if Causality.ExprDep.is_read_var vname
35
       then
36
         let vname' = String.sub vname 1 (-1 + String.length vname) in
37
         if is_variable nd vname' then
38
           ISet.add vname' vset,
39
           ISet.add vname' memset
40
         else
41
           vset, memset
42
       else
43
         ISet.add vname vset, memset
44
      )
45
      sliced_deps
46
      (ISet.singleton vname, ISet.empty)
47
  in
48
  report ~level:3
49
    (fun fmt -> Format.fprintf fmt "COI of var %s: (%a // %a)@."
50
		  v.var_id
51
		  (fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements vset)
52
		  (fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements memset)
53
    )  ;
54
  vset, memset
55
  
56
	  
57
(* Computes the variables required to compute vl. Variables /seen/ do not need
58
     to be computed *)
59
let rec coi_vars deps nd vl seen =
60
  let coi_vars = coi_vars deps nd in
61
  List.fold_left
62
    (fun accu v ->
63
     let vset, memset = coi_var deps nd v in
64
     (* We handle the new mems discovered in the coi *)
65
     let memset =
66
       ISet.filter (
67
           fun vid ->
68
           not
69
             (List.exists
70
                (fun v -> v.var_id = vid)
71
                vl
72
             ) 
73
         ) memset
74
     in
75
     let memset_vars = 
76
       ISet.fold (
77
           fun vid accu ->
78
           (find_variable nd vid)::accu
79
         ) memset [] 
80
     in
81
     let vset' =
82
       coi_vars memset_vars (vl@seen)
83
     in
84
     ISet.union accu (ISet.union vset vset')
85
    )
86
    ISet.empty
87
    (List.filter
88
       (fun v -> not (List.mem v seen))
89
       vl
90
    )
91
    
92
    
93
(* compute the coi of vars_to_keeps in node nd *)
94
let compute_sliced_vars vars_to_keep deps nd =
95
  ISet.elements (coi_vars deps nd vars_to_keep []) 
96

  
97

  
98

  
99

  
100

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

  
128
  report ~level:3 (fun fmt -> Format.fprintf fmt "Scheduling node@.");
129
  
130
  (* Split tuples while sorting eqs *)
131
  let eqs, auts = Corelang.get_node_eqs nd in
132
  assert (auts = []); (* Automata should be expanded by now *)
133
  let sorted_eqs = Scheduling.sort_equations_from_schedule
134
                     eqs
135
                     msch.Scheduling_type.schedule in
136

  
137
  report ~level:3 (fun fmt -> Format.fprintf fmt "Scheduled node@.");
138

  
139
  let stmts =
140
    List.filter (
141
        fun (* stmt ->
142
         * match stmt with
143
         * | Aut _ -> assert false
144
         * | Eq *) eq -> (
145
          match eq.eq_lhs with
146
            [vid] -> List.mem vid coi_vars
147
          | _ -> Format.eprintf "Faulty statement: %a@.@?" Printers.pp_node_eq eq; assert false
148
        (* should not happen after inlining and normalization *)
149
        )
150
      ) sorted_eqs
151
  in
152
  { nd
153
  with
154
    node_outputs = outputs;
155
    node_locals = locals;
156
    node_stmts = List.map (fun e -> Eq e) stmts 
157
  } 
src/tools/seal/seal_utils.ml
1
open Lustre_types
2
open Utils
3
   
4
let report = Log.report ~plugin:"seal"
5

  
6

  
src/tools/seal/seal_verifier.ml
1
open Seal_slice
2
open Seal_extract
3
open Seal_utils
4

  
5
let active = ref false
6

  
7
(* Select the appropriate node, should have been inlined already and
8
   extract update/output functions. *)
9
let seal_run basename prog machines =
10
  let node_name =
11
    match !Options.main_node with
12
    | "" -> (
13
      Format.eprintf "SEAL verifier requires a main node.@.";
14
      Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
15
        (Utils.fprintf_list ~sep:"@ "
16
           (fun fmt m ->
17
             Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id
18
           )
19
        )
20
        machines; 
21
      exit 1
22
    )
23
    | s -> s
24
  in
25
  let m = Machine_code_common.get_machine machines node_name in
26
  let nd = m.mname in
27
  (* Format.eprintf "Node %a@." Printers.pp_node nd; *)
28
  let mems = m.mmemory in
29
  (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *)
30
  let msch = Utils.desome m.msch in
31
  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)
32
  let sliced_nd = slice_node mems msch nd in
33
  (* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *)
34
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
35
  let sw_init, sw_sys = node_as_switched_sys mems sliced_nd in
36
  let pp_res =
37
    (Utils.fprintf_list ~sep:"@ "
38
       (fun fmt (gel, up) ->
39
         Format.fprintf fmt "@[<v 2>[%a]:@ %a@]"
40
           (Utils.fprintf_list ~sep:"; "
41
              (fun fmt (e,b) ->
42
                if b then Printers.pp_expr fmt e
43
                else Format.fprintf fmt "not(%a)"
44
                       Printers.pp_expr e)) gel
45
           (Utils.fprintf_list ~sep:";@ "
46
              (fun fmt (id, e) ->
47
                Format.fprintf fmt "%s = @[<hov 0>%a@]"
48
                  id
49
                  Printers.pp_expr e)) up
50
    ))
51
  in
52
  report ~level:1 (
53
      fun fmt -> Format.fprintf fmt
54
                   "%i memories, %i init, %i step switch cases@."
55
                   (List.length mems)
56
                   (List.length sw_init)
57
                   (List.length sw_sys)
58
               
59
    );
60
  report ~level:1 (fun fmt ->
61
      Format.fprintf fmt "@[<v 0>@[<v 3>Init:@ %a@]@ "
62
        pp_res sw_init;
63
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "
64
        pp_res sw_sys
65
    );
66
  
67

  
68
  ()
69
  
70
module Verifier =
71
  (struct
72
    include VerifierType.Default
73
    let name = "seal"
74
    let options = []
75
    let activate () =
76
      active := true;
77
      Options.global_inline := true
78
      
79
    let is_active () = !active
80
    let run = seal_run
81
      
82
                    
83
  end: VerifierType.S)
84
    
src/tools/seal_extract.ml
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 eqs, auts = Corelang.get_node_eqs nd in
302
  assert (auts = []); (* Automata should be expanded by now *)
303
  let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in
304
  let defs : (ident,  guarded_expr list) Hashtbl.t = Hashtbl.create 13 in
305
  let add_def = add_def defs in
306
  (* Registering node equations *)
307
  let mem_defs =
308
    List.fold_left (fun accu eq ->
309
        match eq.eq_lhs with
310
        | [vid] ->
311
           (* Only focus on non memory definitions *)
312
           if not (List.exists (fun v -> v.var_id = vid) mems) then (
313
             report ~level:3 (fun fmt -> Format.fprintf fmt "Registering variable %s@." vid);
314
             add_def vid eq.eq_rhs;
315
             accu
316
           )
317
           else
318
             (
319
               match eq.eq_rhs.expr_desc with
320
               | Expr_pre def_m ->
321
                  report ~level:3 (fun fmt -> Format.fprintf fmt "Preparing mem %s@." vid);
322

  
323
                  (vid, rewrite defs def_m)::accu
324
               | _ -> assert false
325
             )
326
        | _ -> assert false (* should have been removed by normalization *)
327
      ) [] sorted_eqs
328
  in
329
  report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out memories definitions (may takes time)@.");
330
  (* Printing memories definitions *)
331
  report ~level:3
332
    (fun fmt ->
333
      Format.fprintf fmt
334
        "%a"
335
        (Utils.fprintf_list ~sep:"@."
336
           (fun fmt (m,mdefs) ->
337
             Format.fprintf fmt
338
               "%s -> @[<v 0>[%a@] ]@."
339
               m
340
               (Utils.fprintf_list ~sep:"@ "
341
                  pp_guard_expr) mdefs
342
        ))
343
        mem_defs);
344
  let init_defs, update_defs =
345
    split_init mem_defs
346
  in
347
  report ~level:3
348
    (fun fmt ->
349
      Format.fprintf fmt
350
        "Init:@.%a@.Step@.%a"
351
        (Utils.fprintf_list ~sep:"@."
352
           (fun fmt (m,mdefs) ->
353
             Format.fprintf fmt
354
               "%s -> @[<v 0>[%a@] ]@."
355
               m
356
               (Utils.fprintf_list ~sep:"@ "
357
                  pp_guard_expr) mdefs
358
        ))
359
        init_defs
360
        (Utils.fprintf_list ~sep:"@."
361
           (fun fmt (m,mdefs) ->
362
             Format.fprintf fmt
363
               "%s -> @[<v 0>[%a@] ]@."
364
               m
365
               (Utils.fprintf_list ~sep:"@ "
366
                  pp_guard_expr) mdefs
367
        ))
368
        update_defs);
369
  let sw_init= 
370
    build_switch_sys init_defs []
371
  in
372
  let sw_sys =
373
    build_switch_sys update_defs []
374
  in
375
  sw_init, sw_sys
src/tools/seal_slice.ml
1
open Lustre_types
2
open Utils
3
open Seal_utils			
4
			
5
(******************************************************************************)
6
(* Computing a slice of a node, selecting only some variables, based on       *)
7
(* their COI (cone of influence)                                              *)
8
(******************************************************************************)
9

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

  
21
(* Returns the vars required to compute v. 
22
   Memories are specifically identified. *)
23
let coi_var deps nd v =
24
  let vname = v.var_id in
25
  let sliced_deps =
26
    Causality.slice_graph deps vname
27
  in
28
  (* Format.eprintf "sliced graph for %a: %a@."
29
   *   Printers.pp_var v
30
   *   Causality.pp_dep_graph sliced_deps; *)
31
  let vset, memset =
32
    IdentDepGraph.fold_vertex
33
      (fun vname (vset,memset)  ->
34
       if Causality.ExprDep.is_read_var vname
35
       then
36
         let vname' = String.sub vname 1 (-1 + String.length vname) in
37
         if is_variable nd vname' then
38
           ISet.add vname' vset,
39
           ISet.add vname' memset
40
         else
41
           vset, memset
42
       else
43
         ISet.add vname vset, memset
44
      )
45
      sliced_deps
46
      (ISet.singleton vname, ISet.empty)
47
  in
48
  report ~level:3
49
    (fun fmt -> Format.fprintf fmt "COI of var %s: (%a // %a)@."
50
		  v.var_id
51
		  (fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements vset)
52
		  (fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements memset)
53
    )  ;
54
  vset, memset
55
  
56
	  
57
(* Computes the variables required to compute vl. Variables /seen/ do not need
58
     to be computed *)
59
let rec coi_vars deps nd vl seen =
60
  let coi_vars = coi_vars deps nd in
61
  List.fold_left
62
    (fun accu v ->
63
     let vset, memset = coi_var deps nd v in
64
     (* We handle the new mems discovered in the coi *)
65
     let memset =
66
       ISet.filter (
67
           fun vid ->
68
           not
69
             (List.exists
70
                (fun v -> v.var_id = vid)
71
                vl
72
             ) 
73
         ) memset
74
     in
75
     let memset_vars = 
76
       ISet.fold (
77
           fun vid accu ->
78
           (find_variable nd vid)::accu
79
         ) memset [] 
80
     in
81
     let vset' =
82
       coi_vars memset_vars (vl@seen)
83
     in
84
     ISet.union accu (ISet.union vset vset')
85
    )
86
    ISet.empty
87
    (List.filter
88
       (fun v -> not (List.mem v seen))
89
       vl
90
    )
91
    
92
    
93
(* compute the coi of vars_to_keeps in node nd *)
94
let compute_sliced_vars vars_to_keep deps nd =
95
  ISet.elements (coi_vars deps nd vars_to_keep []) 
96

  
97

  
98

  
99

  
100

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

  
128
  report ~level:3 (fun fmt -> Format.fprintf fmt "Scheduling node@.");
129
  
130
  (* Split tuples while sorting eqs *)
131
  let eqs, auts = Corelang.get_node_eqs nd in
132
  assert (auts = []); (* Automata should be expanded by now *)
133
  let sorted_eqs = Scheduling.sort_equations_from_schedule
134
                     eqs
135
                     msch.Scheduling_type.schedule in
136

  
137
  report ~level:3 (fun fmt -> Format.fprintf fmt "Scheduled node@.");
138

  
139
  let stmts =
140
    List.filter (
141
        fun (* stmt ->
142
         * match stmt with
143
         * | Aut _ -> assert false
144
         * | Eq *) eq -> (
145
          match eq.eq_lhs with
146
            [vid] -> List.mem vid coi_vars
147
          | _ -> Format.eprintf "Faulty statement: %a@.@?" Printers.pp_node_eq eq; assert false
148
        (* should not happen after inlining and normalization *)
149
        )
150
      ) sorted_eqs
151
  in
152
  { nd
153
  with
154
    node_outputs = outputs;
155
    node_locals = locals;
156
    node_stmts = List.map (fun e -> Eq e) stmts 
157
  } 
src/tools/seal_utils.ml
1
open Lustre_types
2
open Utils
3
   
4
let report = Log.report ~plugin:"seal"
5

  
6

  
src/tools/seal_verifier.ml
1
open Seal_slice
2
open Seal_extract
3
open Seal_utils
4

  
5
let active = ref false
6

  
7
(* Select the appropriate node, should have been inlined already and
8
   extract update/output functions. *)
9
let seal_run basename prog machines =
10
  let node_name =
11
    match !Options.main_node with
12
    | "" -> (
13
      Format.eprintf "SEAL verifier requires a main node.@.";
14
      Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
15
        (Utils.fprintf_list ~sep:"@ "
16
           (fun fmt m ->
17
             Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id
18
           )
19
        )
20
        machines; 
21
      exit 1
22
    )
23
    | s -> s
24
  in
25
  let m = Machine_code_common.get_machine machines node_name in
26
  let nd = m.mname in
27
  (* Format.eprintf "Node %a@." Printers.pp_node nd; *)
28
  let mems = m.mmemory in
29
  (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *)
30
  let msch = Utils.desome m.msch in
31
  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)
32
  let sliced_nd = slice_node mems msch nd in
33
  (* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *)
34
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
35
  let sw_init, sw_sys = node_as_switched_sys mems sliced_nd in
36
  let pp_res =
37
    (Utils.fprintf_list ~sep:"@ "
38
       (fun fmt (gel, up) ->
39
         Format.fprintf fmt "@[<v 2>[%a]:@ %a@]"
40
           (Utils.fprintf_list ~sep:"; "
41
              (fun fmt (e,b) ->
42
                if b then Printers.pp_expr fmt e
43
                else Format.fprintf fmt "not(%a)"
44
                       Printers.pp_expr e)) gel
45
           (Utils.fprintf_list ~sep:";@ "
46
              (fun fmt (id, e) ->
47
                Format.fprintf fmt "%s = @[<hov 0>%a@]"
48
                  id
49
                  Printers.pp_expr e)) up
50
    ))
51
  in
52
  report ~level:1 (
53
      fun fmt -> Format.fprintf fmt
54
                   "%i memories, %i init, %i step switch cases@."
55
                   (List.length mems)
56
                   (List.length sw_init)
57
                   (List.length sw_sys)
58
               
59
    );
60
  report ~level:1 (fun fmt ->
61
      Format.fprintf fmt "@[<v 0>@[<v 3>Init:@ %a@]@ "
62
        pp_res sw_init;
63
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "
64
        pp_res sw_sys
65
    );
66
  
67

  
68
  ()
69
  
70
module Verifier =
71
  (struct
72
    include VerifierType.Default
73
    let name = "seal"
74
    let options = []
75
    let activate () =
76
      active := true;
77
      Options.global_inline := true
78
      
79
    let is_active () = !active
80
    let run = seal_run
81
      
82
                    
83
  end: VerifierType.S)
84
    

Also available in: Unified diff