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 = 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
|
14
|
|
15
|
(* Returns the vars required to compute v. Memories are specifically identified. *)
|
16
|
let coi_var deps nd v =
|
17
|
let vname = v.var_id in
|
18
|
let sliced_deps = Causality.slice_graph deps vname in
|
19
|
(* Format.eprintf "sliced graph for %a: %a@."
|
20
|
* Printers.pp_var v
|
21
|
* Causality.pp_dep_graph sliced_deps; *)
|
22
|
let vset, memset =
|
23
|
IdentDepGraph.fold_vertex
|
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)
|
31
|
sliced_deps
|
32
|
(ISet.singleton vname, ISet.empty)
|
33
|
in
|
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));
|
40
|
vset, memset
|
41
|
|
42
|
(* Computes the variables required to compute vl. Variables /seen/ do not need
|
43
|
to be computed *)
|
44
|
let rec coi_vars deps nd vl seen =
|
45
|
let coi_vars = coi_vars deps nd in
|
46
|
List.fold_left
|
47
|
(fun accu v ->
|
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'))
|
60
|
ISet.empty
|
61
|
(List.filter (fun v -> not (List.mem v seen)) vl)
|
62
|
|
63
|
(* compute the coi of vars_to_keeps in node nd *)
|
64
|
let compute_sliced_vars vars_to_keep deps nd =
|
65
|
ISet.elements (coi_vars deps nd vars_to_keep [])
|
66
|
|
67
|
(* If existing outputs are included in vars_to_keep, just slice the content.
|
68
|
Otherwise outputs are replaced by vars_to_keep *)
|
69
|
let slice_node vars_to_keep msch nd =
|
70
|
let coi_vars =
|
71
|
compute_sliced_vars vars_to_keep msch.Scheduling_type.dep_graph nd
|
72
|
in
|
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);
|
77
|
let outputs =
|
78
|
List.filter (fun v -> List.mem v.var_id coi_vars) nd.node_outputs
|
79
|
in
|
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@ ");
|
86
|
vars_to_keep
|
87
|
| l ->
|
88
|
l
|
89
|
in
|
90
|
let locals =
|
91
|
List.filter (fun v -> List.mem v.var_id coi_vars) nd.node_locals
|
92
|
in
|
93
|
|
94
|
report ~level:3 (fun fmt -> Format.fprintf fmt "Scheduling node@.");
|
95
|
|
96
|
(* Split tuples while sorting eqs *)
|
97
|
let eqs, auts = Corelang.get_node_eqs nd in
|
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
|
102
|
in
|
103
|
let locals = List.filter (fun v -> not (List.mem v.var_id unused)) locals in
|
104
|
report ~level:3 (fun fmt -> Format.fprintf fmt "Scheduled node@.");
|
105
|
|
106
|
let stmts =
|
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
|
118
|
in
|
119
|
{
|
120
|
nd with
|
121
|
node_outputs = outputs;
|
122
|
node_locals = locals;
|
123
|
node_stmts = List.map (fun e -> Eq e) stmts;
|
124
|
}
|