## lustrec / src / tools / seal_slice.ml @ 0d79d0f3

History | View | Annotate | Download (4.3 KB)

1 | 0d79d0f3 | ploc | 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 | } |