### Profile

« Previous | Next »

## Revision 9094307a

Working on algebraic loop diagnostic and resolution

View differences:

src/algebraicLoop.ml
1
```(* We try to solve all algebraic loops (AL) from prog:
```
2
```each node is mapped to its own cycles
```
3
```each cycle is tentatively solved by inlining one of its component
```
4

5
```When done, a report is generated
```
6

7
```- for each initial AL, the cycle is presented
```
8
```   - either it is solvable and we provide the set of inlines that solves it
```
9
```   - or it is not and we write the AL as unsolvable by inlining
```
10

11
```   If the option solve_al is activated, the resulting partially inlined prog is
```
12
```   propagated fur future processing
```
13
```   Otherwise the program stops
```
14
```*)
```
15
```open LustreSpec
```
16
```open Corelang
```
17
```open Utils
```
18
```open Format
```
19

20
```(* An single algebraic loop is defined (partition, node calls, inlined, status)
```
21
```   ie the list of variables in the loop, ident list
```
22
```      the possible functions identifier to inline, and whether they have been inlined yet (ident * tag * bool) list
```
23
```   and a status whether the inlining is enough  bool
```
24
```*)
```
25
```type algebraic_loop = (ident list * (ident * expr * bool) list * bool)
```
26
```
```
27
```exception Error of (node_desc * (algebraic_loop list)) list
```
28

29
```(* Module that extract from the DataCycle the set of node that could be inlined
```
30
```   to solve the problem. *)
```
31
```module CycleResolution =
```
32
```struct
```
33

34
```  (* We iter over calls in node defs. If the call defined on of the variable in
```
35
```     the cycle, we store it for future possible inline. *)
```
36
```  let resolve node partition =
```
37
```    let partition = ISet.of_list partition in
```
38
```    (* Preprocessing calls: associate to each of them the eq.lhs associated *)
```
39
```    let eqs = get_node_eqs node in
```
40
```    let calls_expr = Causality.NodeDep.get_calls (fun _ -> true) eqs in
```
41
```    let calls = List.map (
```
42
```      fun expr ->
```
43
```	let eq = List.find (fun eq ->
```
44
```	  Corelang.expr_contains_expr expr.expr_tag eq.eq_rhs
```
45
```	) eqs in
```
46
```	let fun_name = match expr.expr_desc with
```
47
```	  | Expr_appl(fun_id, _, _) -> fun_id
```
48
```	  | _ -> assert false
```
49
```	in
```
50
```	eq, expr, fun_name
```
51
```    ) calls_expr in
```
52
```    List.fold_left (
```
53
```      fun accu ((eq, _, _) as call) ->
```
54
```	let shared_vars = ISet.inter (ISet.of_list eq.eq_lhs) partition in
```
55
```	if not (ISet.is_empty shared_vars) then
```
56
```	  (* We have a match: keep the eq and the expr to inline *)
```
57
```	  call::accu
```
58
```	else
```
59
```	  accu
```
60
```    ) [] calls
```
61
```end
```
62

63

64
```(* Format.fprintf fmt "@[<v 2>Possible resolution:@ %a@]" pp_resolution resolution*)
```
65

66
```
```
67
```let pp_resolution fmt resolution =
```
68
```  fprintf_list ~sep:"@ " (fun fmt (eq, tag) ->
```
69
```    Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq
```
70
```  ) fmt resolution
```
71
```
```
72
```let al_is_solved al = true
```
73

74
```(********************)
```
75

76
```let inline_annotation loc =
```
77
```  Inliner.keyword,
```
78
```  Corelang.mkeexpr loc
```
79
```    (Corelang.mkexpr loc
```
80
```       (Expr_const (Const_tag tag_true) ))
```
81

82
```let is_expr_inlined expr =
```
83
```  match expr.expr_annot with
```
84
```    None -> false
```
85
```  | Some anns -> if List.mem_assoc Inliner.keyword anns.annots then
```
86
```      let status = List.assoc Inliner.keyword anns.annots in
```
87
```      match status.eexpr_qfexpr.expr_desc with
```
88
```      | Expr_const (Const_tag tag) when tag = tag_true ->
```
89
```	 true
```
90
```      | Expr_const (Const_tag tag) when tag = tag_false ->
```
91
```	 false
```
92
```      | _ -> assert false (* expecting true or false value *)
```
93
```    else false
```
94
```
```
95
```(* Inline the provided expression *)
```
96
```let inline_expr expr =
```
97
```  let ann = inline_annotation expr.expr_loc in
```
98
```    match expr.expr_annot with
```
99
```    | None -> expr.expr_annot = Some {annots = [ann]; annot_loc = expr.expr_loc}
```
100
```    | Some anns -> expr.expr_annot = Some {anns with annots = ann::anns.annots}
```
101
```
```
102
```(* Inline the call tagged tag in expr: should not be used anymore, thanks to a direct call to inline_expr *)
```
103
```let rec inline_call tag expr =
```
104
```  if expr.expr_tag = tag then
```
105
```    inline_expr expr
```
106
```  else
```
107
```    let _in = inline_call tag in
```
108
```    let _ins = List.exists _in
```
109
```    in
```
110
```    match expr.expr_desc with
```
111
```    | Expr_const _
```
112
```    | Expr_ident _ -> false
```
113
```    | Expr_tuple el -> _ins el
```
114
```    | Expr_ite (g,t,e) -> _ins [g;t;e]
```
115
```    | Expr_arrow (e1, e2)
```
116
```    | Expr_fby (e1, e2) -> _ins [e1; e2]
```
117
```    | Expr_array el -> _ins el
```
118
```    | Expr_access (e, _)
```
119
```    | Expr_power (e, _)
```
120
```    | Expr_pre e
```
121
```    | Expr_when (e, _, _) -> _in e
```
122
```    | Expr_merge (_, hl) -> _ins (List.map snd hl)
```
123
```    | Expr_appl (_, arg, Some r) -> _ins [arg; r]
```
124
```    | Expr_appl (_, arg, None) -> _in arg
```
125

126

127
```(**********************)
```
128
```(* Returns a modified node, if possible, and an algebraic_loop report *)
```
129
```let rec solving_node nd existing_al partitions =
```
130
```  (* For each partition, we identify the original one *)
```
131
```  let rerun, al = List.fold_left (fun (rerun, al) part ->
```
132
```    let part_vars = ISet.of_list part in
```
133
```    let match_al (vars, calls, status) =
```
134
```      not (ISet.is_empty (ISet.inter (ISet.of_list vars) part_vars))  in
```
135
```    let matched, non_matched = List.partition match_al existing_al in
```
136
```    match matched, non_matched with
```
137
```    | [], _ -> ((* A new conflict partition *)
```
138
```      let calls = CycleResolution.resolve nd part in
```
139
```      (* Filter out already inlined calls *)
```
140
```      let already_inlined, possible_resolution =
```
141
```	List.partition (fun (_, expr, _) -> is_expr_inlined expr) calls in
```
142
```      (* Inlining the first uninlined call *)
```
143
```      match possible_resolution with
```
144
```      | (eq, expr, fun_id)::_ -> ((* One could inline expr *)
```
145
```	(* Forcing the expr to be inlined *)
```
146
```	let _ = inline_expr expr in
```
147
```	true, (* we have to rerun to see if the inlined expression solves the issue *)
```
148
```	(
```
149
```	  part,
```
150
```	  List.map (fun (eq, expr2, fcn_name) ->  fcn_name, expr2, (expr2.expr_tag = expr.expr_tag)) calls,
```
151
```	  false (* Status is nok, LA is unsolved yet *)
```
152
```
```
153
```	)::non_matched
```
154
```      )
```
155
```      | [] -> (* No more calls to inline: algebraic loop is not solvable *)
```
156
```	 rerun, (* we don't force rerun since the current node is not solvable *)
```
157
```	(
```
158
```	  part, (* initial list of troublesome variables *)
```
159
```	  List.map (fun (eq, expr, fcn_name) ->  fcn_name, expr, false) calls,
```
160
```	  false (* Status is nok, LA is unsolved *)
```
161
```	)::non_matched
```
162
```
```
163
```    )
```
164
```    | [vars, calls, status], _ ->
```
165
```       assert false (* Existing partitions were already addressed:
```
166
```		       on peut regarder si la partition courante concerne xxx
```
167
```		       else (* New cycle ??? *)
```
168
```
```
169
```
```
170

171

172
```		       Que faut il faire?
```
173

174
```		       dans un premiertemps on peut ramasser les contraintes et s'arreter là.
```
175
```		       pas d'appel recursif donc on a toujours des nouvelles partitions
```
176
```		       on calcule les apples, on les associe à faux (on a pas inliné encore)
```
177
```		       et le statue global est à faux (on a rien resolu)
```
178

179
```		       comment resoud-on ?
```
180
```		       on ne doit se focaliser que sur les partitions courantes. C'est elle qui sont en conflit
```
181
```		       pour chaque, on pick un call et on l'inlinee
```
182
```		       apres on appel stage1/stage2 pour faire le scheudling du node
```
183

184

185
```		    *)
```
186

187
```
```
188
```  ) (false, existing_al) partitions
```
189
```  in
```
190
```  (* if partition an already identified al ? *)
```
191
```  (* if ISet.of_list partition *)
```
192

193
```  (* if rerun then *)
```
194
```  (*   assert false (\* the missing part, redo stage 1, ... with the updated inline flags *\) *)
```
195
```  (* ; *)
```
196
```  (* TODO xxx il faut ici ajouter le inline sur le 1er appel,
```
197
```     puis reafaire le stage1 et scheduling du noeud *)
```
198
```  Some(nd, al)
```
199

200
```(** This function takes a prog and returns (prog', status, alarms)
```
201
```    where prog' is a modified prog with some locally inlined calls
```
202
```    status is true is the final prog' is schedulable, ie no algebraic loop
```
203
```    In case of failure, ie. inlining does not solve the problem; the status is false.
```
204
```    Alarms contain the list of inlining performed or advised for each node.
```
205
```    This could be provided as a feedback to the user.
```
206
```*)
```
207
```let clean_al prog =
```
208
```(* We iterate over each node *)
```
209
```  let prog, al_list =
```
210
```    List.fold_right (
```
211
```      fun top (prog_accu, al_list) ->
```
212
```	match top.top_decl_desc with
```
213
```	| Node nd -> (
```
214
```	  let error =
```
215
```	    try (* without exception the node is schedulable; nothing to declare *)
```
216
```	      let _ = Scheduling.schedule_node nd in
```
217
```	      None
```
218
```	    with Causality.Error (Causality.DataCycle partitions) -> solving_node nd [] partitions
```
219
```	  in
```
220
```	  match error with
```
221
```	  | None -> top::prog_accu, al_list (* keep it as is *)
```
222
```	  | Some (nd, al) ->
```
223
```	     (* returning the updated node, possible solved, as well as the
```
224
```		generated alarms *)
```
225
```	     {top with top_decl_desc = Node nd}::prog_accu, (nd, al)::al_list
```
226
```	)
```
227
```	| _ -> top::prog_accu, al_list
```
228
```    ) prog ([], [])
```
229
```  in
```
230
```  prog, List.for_all al_is_solved al_list, al_list
```
231

232

233
```(* (ident list * (ident * expr* bool) list * bool) *)
```
234
```let pp_al fmt (partition, calls, status) =
```
235
```  fprintf fmt "@[<v 0>";
```
236
```  fprintf fmt "variables in the alg. loop: @[<hov 0>%a@]@ "
```
237
```    (fprintf_list ~sep:",@ " pp_print_string) partition;
```
238
```  fprintf fmt "@ involved node calls: @[<v 0>%a@]@ "
```
239
```    (fprintf_list ~sep:",@ "
```
240
```       (fun fmt (funid, expr, status) ->
```
241
```	 fprintf fmt "%s" funid;
```
242
```	 if status && is_expr_inlined expr then fprintf fmt " (inlining it solves the alg. loop)";
```
243
```       )
```
244
```    ) calls;
```
245
```  fprintf fmt "@]"
```
246
```     (* TODO ploc:
```
247
```	First analyse the cycle and identify a list of nodes to be inlined, or node instances
```
248
```	Then two behaviors:
```
249
```	- print that list instead of the unreadable cyclic dependency comment
```
250
```	- modify the node by adding the inline information
```
251
```	- recall the subset of stage1 but restricted to a single node:
```
252
```	- inline locally, typing, clocking (may have to reset the tables first), normalization of the node, mpfr injection
```
253
```        - recall stage2
```
254
```     *)
```
255
```
```
256
```
```
257
```let pp_report fmt report =
```
258
```  fprintf fmt "@.Algebraic loops in nodes@.";
```
259
```  fprintf_list ~sep:"@."
```
260
```    (fun fmt (nd, als) ->
```
261
```      let top = Corelang.node_from_name (nd.node_id) in
```
262
```      Error.pp_error top.top_decl_loc
```
263
```	(fun fmt ->
```
264
```	  fprintf fmt "node %s: {@[<v 0>%a@]}"
```
265
```	    nd.node_id
```
266
```	    (fprintf_list ~sep:"@ " pp_al) als
```
267
```	)
```
268
```    ) fmt report;
```
269
```  fprintf fmt "@."
```
270
```
```
271

272
```let analyze prog =
```
273
```  let prog, status_ok, report = clean_al prog in
```
274
```  if !Options.solve_al && status_ok then
```
275
```    Scheduling.schedule_prog prog
```
276
```  else (
```
277
```    (* TODO create a report *)
```
278
```    Format.eprintf "%a" pp_report report;
```
279
```    raise (Corelang.Error (Location.dummy_loc, Error.AlgebraicLoop))
```
280
```  )
```
src/error.ml
1
```open Format
```
2

3
```type ident = LustreSpec.ident
```
4
```type error_kind =
```
5
```    Main_not_found
```
6
```  | Main_wrong_kind
```
7
```  | No_main_specified
```
8
```  | Unbound_symbol of ident
```
9
```  | Already_bound_symbol of ident
```
10
```  | Unknown_library of ident
```
11
```  | Wrong_number of ident
```
12
```  | AlgebraicLoop
```
13

14
```let return_code kind =
```
15
```  match kind with
```
16
```  | Main_not_found -> 2
```
17
```  | Main_wrong_kind -> 3
```
18
```  | No_main_specified -> 4
```
19
```  | Unbound_symbol _ -> 5
```
20
```  | Already_bound_symbol _ -> 6
```
21
```  | Unknown_library _ -> 7
```
22
```  | Wrong_number _ -> 8
```
23
```  | AlgebraicLoop -> 9
```
24

25

26
```  let pp_error_msg fmt = function
```
27
```  | Main_not_found ->
```
28
```      fprintf fmt "Could not find the definition of main node %s.@."
```
29
```	!Global.main_node
```
30
```  | Main_wrong_kind ->
```
31
```    fprintf fmt
```
32
```      "Node %s does not correspond to a valid main node definition.@."
```
33
```      !Global.main_node
```
34
```  | No_main_specified ->
```
35
```    fprintf fmt "No main node specified (use -node option)@."
```
36
```  | Unbound_symbol sym ->
```
37
```    fprintf fmt
```
38
```      "%s is undefined.@."
```
39
```      sym
```
40
```  | Already_bound_symbol sym ->
```
41
```    fprintf fmt
```
42
```      "%s is already defined.@."
```
43
```      sym
```
44
```  | Unknown_library sym ->
```
45
```    fprintf fmt
```
46
```      "impossible to load library %s.lusic.@.Please compile the corresponding interface or source file.@."
```
47
```      sym
```
48
```  | Wrong_number sym ->
```
49
```    fprintf fmt
```
50
```      "library %s.lusic has a different version number and may crash compiler.@.Please recompile the corresponding interface or source file.@."
```
51
```      sym
```
52

53
```let pp_warning loc warning_code pp_msg =
```
54
```  Format.eprintf "%a@.Warning %i: %t@."
```
55
```    Location.pp_loc loc
```
56
```    warning_code
```
57
```    pp_msg
```
58

59
```let pp_error loc pp_msg =
```
60
```  Format.eprintf "@.%a@.Error: @[<v 0>%t@]@."
```
61
```    Location.pp_loc loc
```
62
```    pp_msg
```
63

64
```
```

Also available in: Unified diff