Project

General

Profile

Revision 0d79d0f3

View differences:

src/main_lustre_verifier.ml
45 45
  let source_name = dirname ^ "/" ^ basename ^ extension in
46 46

  
47 47
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
48
  decr Options.verbose_level;
48 49

  
49 50
  (* Parsing source *)
50 51
  let prog = parse_source source_name in
51 52

  
52 53
  (* Checking which solver is active *)
54
  incr Options.verbose_level;
53 55
  let verifier = Verifiers.get_active () in
54 56
  let module Verifier = (val verifier : VerifierType.S) in
55 57

  
56
  
58
  decr Options.verbose_level;
57 59
  (* Normalizing it *)
58 60
  let prog, dependencies = 
59 61
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
60 62
    try
63
      incr Options.verbose_level;
61 64
      let params = Verifier.get_normalization_params () in
65
      decr Options.verbose_level;
62 66
      Compiler_stages.stage1 params prog dirname basename
63 67
    with Compiler_stages.StopPhase1 prog -> (
64 68
        assert false
......
75 79

  
76 80
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
77 81
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ "Machine_code_common.pp_machines machine_code);
78

  
82
  
79 83
  if Scopes.Plugin.show_scopes () then
80 84
    begin
81 85
      let all_scopes = Scopes.compute_scopes prog !Options.main_node in
......
90 94
  let machine_code = Plugins.refine_machine_code prog machine_code in
91 95

  
92 96
  assert (dependencies = []); (* Do not handle deps yet *)
97
  incr Options.verbose_level;
93 98
  Verifier.run basename prog machine_code;
94 99
  begin
95
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
100
    decr Options.verbose_level;
101
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ ");
102
    incr Options.verbose_level;
103
    Log.report ~level:1 (fun fmt -> fprintf fmt "@]@.");
96 104
    (* We stop the process here *)
97 105
    exit 0
98 106
  end
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 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
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 sorted_eqs = Scheduling.sort_equations_from_schedule nd msch.Scheduling_type.schedule in
132

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

  
135
  let stmts =
136
    List.filter (
137
        fun (* stmt ->
138
         * match stmt with
139
         * | Aut _ -> assert false
140
         * | Eq *) eq -> (
141
          match eq.eq_lhs with
142
            [vid] -> List.mem vid coi_vars
143
          | _ -> Format.eprintf "Faulty statement: %a@.@?" Printers.pp_node_eq eq; assert false
144
        (* should not happen after inlining and normalization *)
145
        )
146
      ) sorted_eqs
147
  in
148
  { nd
149
  with
150
    node_outputs = outputs;
151
    node_locals = locals;
152
    node_stmts = List.map (fun e -> Eq e) stmts 
153
  } 
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
src/tools/seal_verifier.ml
1
open Seal_slice
2
open Seal_extract
1 3
open Seal_utils
2 4

  
3 5
let active = ref false
......
7 9
let seal_run basename prog machines =
8 10
  let node_name =
9 11
    match !Options.main_node with
10
    | "" -> assert false
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
    )
11 23
    | s -> s
12 24
  in
13 25
  let m = Machine_code_common.get_machine machines node_name in
......
19 31
  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)
20 32
  let sliced_nd = slice_node mems msch nd in
21 33
  (* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *)
34
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
22 35
  let sw_init, sw_sys = node_as_switched_sys mems sliced_nd in
23 36
  let pp_res =
24 37
    (Utils.fprintf_list ~sep:"@ "
25 38
       (fun fmt (gel, up) ->
26
         Format.fprintf fmt "@[<v 2>%a:@ %a@]"
39
         Format.fprintf fmt "@[<v 2>[%a]:@ %a@]"
27 40
           (Utils.fprintf_list ~sep:"; "
28 41
              (fun fmt (e,b) ->
29 42
                if b then Printers.pp_expr fmt e
30 43
                else Format.fprintf fmt "not(%a)"
31 44
                       Printers.pp_expr e)) gel
32
           (Utils.fprintf_list ~sep:"; "
45
           (Utils.fprintf_list ~sep:";@ "
33 46
              (fun fmt (id, e) ->
34
                Format.fprintf fmt "%s = %a"
47
                Format.fprintf fmt "%s = @[<hov 0>%a@]"
35 48
                  id
36 49
                  Printers.pp_expr e)) up
37 50
    ))
38 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
    );
39 60
  report ~level:1 (fun fmt ->
40 61
      Format.fprintf fmt "@[<v 0>@[<v 3>Init:@ %a@]@ "
41 62
        pp_res sw_init;

Also available in: Unified diff