Project

General

Profile

Revision 9094307a

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