Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/tools/seal/seal_slice.ml
1 1
open Lustre_types
2 2
open Utils
3
open Seal_utils			
4
			
3
open Seal_utils
4

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

  
10 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
11
let is_variable nd vid = List.exists (fun v -> v.var_id = vid) nd.node_locals
12

  
13
let find_variable nd vid = List.find (fun v -> v.var_id = vid) nd.node_locals
20 14

  
21
(* Returns the vars required to compute v. 
22
   Memories are specifically identified. *)
15
(* Returns the vars required to compute v. Memories are specifically identified. *)
23 16
let coi_var deps nd v =
24 17
  let vname = v.var_id in
25
  let sliced_deps =
26
    Causality.slice_graph deps vname
27
  in
18
  let sliced_deps = Causality.slice_graph deps vname in
28 19
  (* Format.eprintf "sliced graph for %a: %a@."
29 20
   *   Printers.pp_var v
30 21
   *   Causality.pp_dep_graph sliced_deps; *)
31 22
  let vset, memset =
32 23
    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
      )
24
      (fun vname (vset, memset) ->
25
        if Causality.ExprDep.is_read_var vname then
26
          let vname' = String.sub vname 1 (-1 + String.length vname) in
27
          if is_variable nd vname' then
28
            ISet.add vname' vset, ISet.add vname' memset
29
          else vset, memset
30
        else ISet.add vname vset, memset)
45 31
      sliced_deps
46 32
      (ISet.singleton vname, ISet.empty)
47 33
  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
    )  ;
34
  report ~level:3 (fun fmt ->
35
      Format.fprintf fmt "COI of var %s: (%a // %a)@." v.var_id
36
        (fprintf_list ~sep:"," Format.pp_print_string)
37
        (ISet.elements vset)
38
        (fprintf_list ~sep:"," Format.pp_print_string)
39
        (ISet.elements memset));
54 40
  vset, memset
55
  
56
	  
41

  
57 42
(* Computes the variables required to compute vl. Variables /seen/ do not need
58
     to be computed *)
43
   to be computed *)
59 44
let rec coi_vars deps nd vl seen =
60 45
  let coi_vars = coi_vars deps nd in
61 46
  List.fold_left
62 47
    (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
    )
48
      let vset, memset = coi_var deps nd v in
49
      (* We handle the new mems discovered in the coi *)
50
      let memset =
51
        ISet.filter
52
          (fun vid -> not (List.exists (fun v -> v.var_id = vid) vl))
53
          memset
54
      in
55
      let memset_vars =
56
        ISet.fold (fun vid accu -> find_variable nd vid :: accu) memset []
57
      in
58
      let vset' = coi_vars memset_vars (vl @ seen) in
59
      ISet.union accu (ISet.union vset vset'))
86 60
    ISet.empty
87
    (List.filter
88
       (fun v -> not (List.mem v seen))
89
       vl
90
    )
91
    
92
    
61
    (List.filter (fun v -> not (List.mem v seen)) vl)
62

  
93 63
(* compute the coi of vars_to_keeps in node nd *)
94 64
let compute_sliced_vars vars_to_keep deps nd =
95
  ISet.elements (coi_vars deps nd vars_to_keep []) 
96

  
97

  
65
  ISet.elements (coi_vars deps nd vars_to_keep [])
98 66

  
99

  
100

  
101
  (* If existing outputs are included in vars_to_keep, just slice the content.
67
(* If existing outputs are included in vars_to_keep, just slice the content.
102 68
   Otherwise outputs are replaced by vars_to_keep *)
103 69
let slice_node vars_to_keep msch nd =
104 70
  let coi_vars =
105 71
    compute_sliced_vars vars_to_keep msch.Scheduling_type.dep_graph nd
106 72
  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);
73
  report ~level:3 (fun fmt ->
74
      Format.fprintf fmt "COI Vars: %a@."
75
        (Utils.fprintf_list ~sep:"," Format.pp_print_string)
76
        coi_vars);
111 77
  let outputs =
112
    List.filter
113
      (
114
        fun v -> List.mem v.var_id coi_vars 
115
      ) nd.node_outputs
78
    List.filter (fun v -> List.mem v.var_id coi_vars) nd.node_outputs
116 79
  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@ ");
80
  let outputs =
81
    match outputs with
82
    | [] ->
83
      report ~level:2 (fun fmt ->
84
          Format.fprintf fmt
85
            "No visible output variable, subtituting with provided vars@ ");
120 86
      vars_to_keep
121
    )
122
    | l -> l
87
    | l ->
88
      l
123 89
  in
124 90
  let locals =
125 91
    List.filter (fun v -> List.mem v.var_id coi_vars) nd.node_locals
126 92
  in
127 93

  
128 94
  report ~level:3 (fun fmt -> Format.fprintf fmt "Scheduling node@.");
129
  
95

  
130 96
  (* Split tuples while sorting eqs *)
131 97
  let eqs, auts = Corelang.get_node_eqs nd in
132
  assert (auts = []); (* Automata should be expanded by now *)
133
  let sorted_eqs, unused = Scheduling.sort_equations_from_schedule
134
                     eqs
135
                     msch.Scheduling_type.schedule 
98
  assert (auts = []);
99
  (* Automata should be expanded by now *)
100
  let sorted_eqs, unused =
101
    Scheduling.sort_equations_from_schedule eqs msch.Scheduling_type.schedule
136 102
  in
137 103
  let locals = List.filter (fun v -> not (List.mem v.var_id unused)) locals in
138 104
  report ~level:3 (fun fmt -> Format.fprintf fmt "Scheduled node@.");
139 105

  
140 106
  let stmts =
141
    List.filter (
142
        fun (* stmt ->
143
         * match stmt with
144
         * | Aut _ -> assert false
145
         * | Eq *) eq -> (
146
          match eq.eq_lhs with
147
            [vid] -> List.mem vid coi_vars
148
          | _ -> Format.eprintf "Faulty statement: %a@.@?" Printers.pp_node_eq eq; assert false
149
        (* should not happen after inlining and normalization *)
150
        )
151
      ) sorted_eqs
107
    List.filter
108
      (fun (* stmt -> * match stmt with * | Aut _ -> assert false * | Eq *)
109
             eq ->
110
        match eq.eq_lhs with
111
        | [ vid ] ->
112
          List.mem vid coi_vars
113
        | _ ->
114
          Format.eprintf "Faulty statement: %a@.@?" Printers.pp_node_eq eq;
115
          assert false
116
        (* should not happen after inlining and normalization *))
117
      sorted_eqs
152 118
  in
153
  { nd
154
  with
119
  {
120
    nd with
155 121
    node_outputs = outputs;
156 122
    node_locals = locals;
157
    node_stmts = List.map (fun e -> Eq e) stmts 
158
  } 
123
    node_stmts = List.map (fun e -> Eq e) stmts;
124
  }

Also available in: Unified diff