lustrec / src / normalization.ml @ 7231d0e4
History  View  Annotate  Download (16.8 KB)
1 
(*  

2 
* SchedMCore  A MultiCore Scheduling Framework 
3 
* Copyright (C) 20092013, ONERA, Toulouse, FRANCE  LIFL, Lille, FRANCE 
4 
* Copyright (C) 20122013, INPT, Toulouse, FRANCE 
5 
* 
6 
* This file is part of Prelude 
7 
* 
8 
* Prelude is free software; you can redistribute it and/or 
9 
* modify it under the terms of the GNU Lesser General Public License 
10 
* as published by the Free Software Foundation ; either version 2 of 
11 
* the License, or (at your option) any later version. 
12 
* 
13 
* Prelude is distributed in the hope that it will be useful, but 
14 
* WITHOUT ANY WARRANTY ; without even the implied warranty of 
15 
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 
16 
* Lesser General Public License for more details. 
17 
* 
18 
* You should have received a copy of the GNU Lesser General Public 
19 
* License along with this program ; if not, write to the Free Software 
20 
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 021111307 
21 
* USA 
22 
* *) 
23  
24 
(* This module is used for the lustre to C compiler *) 
25  
26  
27 
open Utils 
28 
open Corelang 
29 
(* open Clocks *) 
30 
open Format 
31  
32 
let cpt_fresh = ref 0 
33  
34 
(* Generate a new local [node] variable *) 
35 
let mk_fresh_var node loc ty ck = 
36 
let vars = node_vars node in 
37 
let rec aux () = 
38 
incr cpt_fresh; 
39 
let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in 
40 
if List.exists (fun v > v.var_id = s) vars then aux () else 
41 
{ 
42 
var_id = s; 
43 
var_dec_type = dummy_type_dec; 
44 
var_dec_clock = dummy_clock_dec; 
45 
var_dec_const = false; 
46 
var_type = ty; 
47 
var_clock = ck; 
48 
var_loc = loc 
49 
} 
50 
in aux () 
51  
52 
(* Generate a new ident expression from a declared variable *) 
53 
let mk_ident_expr v = 
54 
{ expr_tag = new_tag (); 
55 
expr_desc = Expr_ident v.var_id; 
56 
expr_type = v.var_type; 
57 
expr_clock = v.var_clock; 
58 
expr_delay = Delay.new_var (); 
59 
expr_annot = None; 
60 
expr_loc = v.var_loc } 
61  
62 
(* Get the equation in [defs] with [expr] as rhs, if any *) 
63 
let get_expr_alias defs expr = 
64 
try Some (List.find (fun eq > is_eq_expr eq.eq_rhs expr) defs) 
65 
with 
66 
Not_found > None 
67  
68 
(* Replace [expr] with (tuple of) [locals] *) 
69 
let replace_expr locals expr = 
70 
match locals with 
71 
 [] > assert false 
72 
 [v] > { expr with 
73 
expr_tag = Utils.new_tag (); 
74 
expr_desc = Expr_ident v.var_id } 
75 
 _ > { expr with 
76 
expr_tag = Utils.new_tag (); 
77 
expr_desc = Expr_tuple (List.map mk_ident_expr locals) } 
78  
79 
let unfold_offsets e offsets = 
80 
let add_offset e d = 
81 
(*Format.eprintf "add_offset %a %a@." Dimension.pp_dimension (Types.array_type_dimension e.expr_type) Dimension.pp_dimension d;*) 
82 
{ e with 
83 
expr_tag = Utils.new_tag (); 
84 
expr_loc = d.Dimension.dim_loc; 
85 
expr_type = Types.array_element_type e.expr_type; 
86 
expr_desc = Expr_access (e, d) } in 
87 
List.fold_left add_offset e offsets 
88  
89 
(* Create an alias for [expr], if none exists yet *) 
90 
let mk_expr_alias node (defs, vars) expr = 
91 
match get_expr_alias defs expr with 
92 
 Some eq > 
93 
let aliases = List.map (fun id > List.find (fun v > v.var_id = id) vars) eq.eq_lhs in 
94 
(defs, vars), replace_expr aliases expr 
95 
 None > 
96 
let new_aliases = 
97 
List.map2 
98 
(mk_fresh_var node expr.expr_loc) 
99 
(Types.type_list_of_type expr.expr_type) 
100 
(Clocks.clock_list_of_clock expr.expr_clock) in 
101 
let new_def = 
102 
mkeq expr.expr_loc (List.map (fun v > v.var_id) new_aliases, expr) 
103 
in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr 
104  
105 
(* Create an alias for [expr], if [opt] *) 
106 
let mk_expr_alias_opt opt node defvars expr = 
107 
if opt 
108 
then 
109 
mk_expr_alias node defvars expr 
110 
else 
111 
defvars, expr 
112  
113 
(* Create a (normalized) expression from [ref_e], 
114 
replacing description with [norm_d], 
115 
taking propagated [offsets] into account 
116 
in order to change expression type *) 
117 
let mk_norm_expr offsets ref_e norm_d = 
118 
let drop_array_type ty = 
119 
Types.map_tuple_type Types.array_element_type ty in 
120 
{ ref_e with 
121 
expr_desc = norm_d; 
122 
expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type } 
123  
124 
(* normalize_<foo> : defs * used vars > <foo> > (updated defs * updated vars) * normalized <foo> *) 
125 
let rec normalize_list alias node offsets norm_element defvars elist = 
126 
List.fold_right 
127 
(fun t (defvars, qlist) > 
128 
let defvars, norm_t = norm_element alias node offsets defvars t in 
129 
(defvars, norm_t :: qlist) 
130 
) elist (defvars, []) 
131  
132 
let rec normalize_expr ?(alias=true) node offsets defvars expr = 
133 
(* Format.eprintf "normalize %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) 
134 
match expr.expr_desc with 
135 
 Expr_const _ 
136 
 Expr_ident _ > defvars, unfold_offsets expr offsets 
137 
 Expr_array elist > 
138 
let defvars, norm_elist = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in 
139 
let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in 
140 
mk_expr_alias_opt alias node defvars norm_expr 
141 
 Expr_power (e1, d) when offsets = [] > 
142 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in 
143 
let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in 
144 
mk_expr_alias_opt alias node defvars norm_expr 
145 
 Expr_power (e1, d) > 
146 
normalize_expr ~alias:alias node (List.tl offsets) defvars e1 
147 
 Expr_access (e1, d) > 
148 
normalize_expr ~alias:alias node (d::offsets) defvars e1 
149 
 Expr_tuple elist > 
150 
let defvars, norm_elist = 
151 
normalize_list alias node offsets (fun alias > normalize_expr ~alias:alias) defvars elist in 
152 
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) 
153 
 Expr_appl (id, args, None) when Basic_library.is_internal_fun id && Types.is_array_type expr.expr_type > 
154 
let defvars, norm_args = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in 
155 
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) 
156 
 Expr_appl (id, args, None) when Basic_library.is_internal_fun id > 
157 
let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in 
158 
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None)) 
159 
 Expr_appl (id, args, r) > 
160 
let defvars, norm_args = normalize_expr node [] defvars args in 
161 
let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in 
162 
if offsets <> [] 
163 
then 
164 
let defvars, norm_expr = normalize_expr node [] defvars norm_expr in 
165 
normalize_expr ~alias:alias node offsets defvars norm_expr 
166 
else 
167 
mk_expr_alias_opt (alias && not (Basic_library.is_internal_fun id)) node defvars norm_expr 
168 
 Expr_arrow (e1,e2) > (* Here we differ from Colaco paper: arrows are pushed to the top *) 
169 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in 
170 
let defvars, norm_e2 = normalize_expr node offsets defvars e2 in 
171 
let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in 
172 
mk_expr_alias_opt alias node defvars norm_expr 
173 
 Expr_pre e > 
174 
let defvars, norm_e = normalize_expr node offsets defvars e in 
175 
let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in 
176 
mk_expr_alias_opt alias node defvars norm_expr 
177 
 Expr_fby (e1, e2) > 
178 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in 
179 
let defvars, norm_e2 = normalize_expr node offsets defvars e2 in 
180 
let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in 
181 
mk_expr_alias_opt alias node defvars norm_expr 
182 
 Expr_when (e, c, l) > 
183 
let defvars, norm_e = normalize_expr node offsets defvars e in 
184 
defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l)) 
185 
 Expr_ite (c, t, e) > 
186 
let defvars, norm_c = normalize_guard node defvars c in 
187 
let defvars, norm_t = normalize_cond_expr node offsets defvars t in 
188 
let defvars, norm_e = normalize_cond_expr node offsets defvars e in 
189 
let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in 
190 
mk_expr_alias_opt alias node defvars norm_expr 
191 
 Expr_merge (c, hl) > 
192 
let defvars, norm_hl = normalize_branches node offsets defvars hl in 
193 
let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in 
194 
mk_expr_alias_opt alias node defvars norm_expr 
195 
 Expr_uclock _ 
196 
 Expr_dclock _ 
197 
 Expr_phclock _ > assert false (* Not handled yet *) 
198  
199 
and normalize_branches node offsets defvars hl = 
200 
List.fold_right 
201 
(fun (t, h) (defvars, norm_q) > 
202 
let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in 
203 
defvars, (t, norm_h) :: norm_q 
204 
) 
205 
hl (defvars, []) 
206  
207 
and normalize_array_expr ?(alias=true) node offsets defvars expr = 
208 
(* Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) 
209 
match expr.expr_desc with 
210 
 Expr_power (e1, d) when offsets = [] > 
211 
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in 
212 
defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d)) 
213 
 Expr_power (e1, d) > 
214 
normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1 
215 
 Expr_access (e1, d) > normalize_array_expr ~alias:alias node (d::offsets) defvars e1 
216 
 Expr_array elist when offsets = [] > 
217 
let defvars, norm_elist = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars elist in 
218 
defvars, mk_norm_expr offsets expr (Expr_array norm_elist) 
219 
 Expr_appl (id, args, None) when Basic_library.is_internal_fun id > 
220 
let defvars, norm_args = normalize_list alias node offsets (fun _ > normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in 
221 
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) 
222 
 _ > normalize_expr ~alias:alias node offsets defvars expr 
223  
224 
and normalize_cond_expr ?(alias=true) node offsets defvars expr = 
225 
(*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*) 
226 
match expr.expr_desc with 
227 
 Expr_access (e1, d) > 
228 
normalize_cond_expr ~alias:alias node (d::offsets) defvars e1 
229 
 Expr_ite (c, t, e) > 
230 
let defvars, norm_c = normalize_guard node defvars c in 
231 
let defvars, norm_t = normalize_cond_expr node offsets defvars t in 
232 
let defvars, norm_e = normalize_cond_expr node offsets defvars e in 
233 
defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) 
234 
 Expr_merge (c, hl) > 
235 
let defvars, norm_hl = normalize_branches node offsets defvars hl in 
236 
defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) 
237 
 _ > normalize_expr ~alias:alias node offsets defvars expr 
238  
239 
and normalize_guard node defvars expr = 
240 
match expr.expr_desc with 
241 
 Expr_ident _ > defvars, expr 
242 
 _ > 
243 
let defvars, norm_expr = normalize_expr node [] defvars expr in 
244 
mk_expr_alias_opt true node defvars norm_expr 
245  
246 
(* outputs cannot be memories as well. If so, introduce new local variable. 
247 
*) 
248 
let decouple_outputs node defvars eq = 
249 
let rec fold_lhs defvars lhs tys cks = 
250 
match lhs, tys, cks with 
251 
 [], [], [] > defvars, [] 
252 
 v::qv, t::qt, c::qc > let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in 
253 
if List.exists (fun o > o.var_id = v) node.node_outputs 
254 
then 
255 
let newvar = mk_fresh_var node eq.eq_loc t c in 
256 
let neweq = mkeq eq.eq_loc ([v], mk_ident_expr newvar) in 
257 
(neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q 
258 
else 
259 
(defs_q, vars_q), v::lhs_q 
260 
 _ > assert false in 
261 
let defvars', lhs' = 
262 
fold_lhs 
263 
defvars 
264 
eq.eq_lhs 
265 
(Types.type_list_of_type eq.eq_rhs.expr_type) 
266 
(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in 
267 
defvars', {eq with eq_lhs = lhs' } 
268  
269 
let rec normalize_eq spec node defvars eq = 
270 
match eq.eq_rhs.expr_desc with 
271 
 Expr_pre _ > 
272 
let (defvars', eq') = decouple_outputs node defvars eq in 
273 
let eq_rhs = if spec then 
274 
let expr = Corelang.mkexpr eq'.eq_rhs.expr_loc (Expr_pre eq'.eq_rhs) in 
275 
expr.expr_type < eq'.eq_rhs.expr_type; expr 
276 
else eq'.eq_rhs in 
277 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq_rhs in 
278 
let norm_eq = { eq' with eq_rhs = norm_rhs } in 
279 
(norm_eq::defs', vars') 
280 
 Expr_fby _ > 
281 
let (defvars', eq') = decouple_outputs node defvars eq in 
282 
let eq_rhs = eq'.eq_rhs in (*TODO: Must be like in pre ??? *) 
283 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq_rhs in 
284 
let norm_eq = { eq' with eq_rhs = norm_rhs } in 
285 
(norm_eq::defs', vars') 
286 
 Expr_array _ > 
287 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in 
288 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
289 
(norm_eq::defs', vars') 
290 
 Expr_appl (id, _, None) when Basic_library.is_internal_fun id && Types.is_array_type eq.eq_rhs.expr_type > 
291 
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in 
292 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
293 
(norm_eq::defs', vars') 
294 
 Expr_appl _ > 
295 
let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in 
296 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
297 
(norm_eq::defs', vars') 
298 
 _ > 
299 
let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in 
300 
let norm_eq = { eq with eq_rhs = norm_rhs } in 
301 
norm_eq::defs', vars' 
302  
303 
let normalize_eq_split spec node defvars eq = 
304 
let defs, vars = normalize_eq spec node defvars eq in 
305 
List.fold_right (fun eq (def, vars) > 
306 
let eq_defs = Splitting.tuple_split_eq eq in 
307 
if eq_defs = [eq] then 
308 
eq::def, vars 
309 
else 
310 
List.fold_left (normalize_eq spec node) (def, vars) eq_defs 
311 
) defs ([], vars) 
312  
313 
let normalize_eexpr decls node vars ee = 
314 
(* New output variable *) 
315 
let output_id = "spec" ^ string_of_int ee.eexpr_tag in 
316 
let output_var = 
317 
mkvar_decl 
318 
ee.eexpr_loc 
319 
(output_id, 
320 
mktyp ee.eexpr_loc Tydec_bool, 
321 
mkclock ee.eexpr_loc Ckdec_any, 
322 
false (* not a constant *)) 
323 
in 
324 
let _ = Typing.type_var_decl [] Env.initial output_var in (* typing the variable *) 
325 

326 
(* Calls are first inlined *) 
327 
let nodes = get_nodes decls in 
328 
let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in 
329 
let calls = List.map 
330 
(fun called_nd > List.find (fun nd2 > node_name nd2 = called_nd) nodes) calls 
331 
in 
332 
(* Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd > pp_print_string fmt (node_name nd))) calls; *) 
333 
let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in 
334 
let defs, vars = 
335 
if calls = [] && not (eq_has_arrows eq) then 
336 
normalize_eq_split true node ([], vars) eq 
337 
else ( 
338 
let locals = 
339 
node.node_locals @ (List.fold_left (fun accu (_, q) > q@accu) [] ee.eexpr_quantifiers) in 
340 
let new_locals, eqs = Inliner.inline_eq ~arrows:true eq locals calls in 
341 

342 
(* Normalizing expr and eqs *) 
343 
List.fold_left (normalize_eq_split true node) ([], vars@new_locals) eqs 
344 
) 
345 
in 
346 

347 
ee.eexpr_normalized < Some (output_var, defs, vars) 
348  
349 
let normalize_spec decls node vars s = 
350 
let nee = normalize_eexpr decls node vars in 
351 
List.iter nee s.requires; 
352 
List.iter nee s.ensures; 
353 
List.iter (fun (_, assumes, ensures, _) > 
354 
List.iter nee assumes; 
355 
List.iter nee ensures 
356 
) s.behaviors 
357 

358 

359 
(* The normalization phase introduces new local variables 
360 
 output cannot be memories. If this happen, new local variables acting as 
361 
memories are introduced. 
362 
 array constants, pre, arrow, fby, ite, merge, calls to node with index 
363 
access 
364 
Thoses values are shared, ie. no duplicate expressions are introduced. 
365  
366 
Concerning specification, a similar process is applied, replacing an 
367 
expression by a list of local variables and definitions 
368 
*) 
369 
let normalize_node decls node = 
370 
cpt_fresh := 0; 
371 
let inputs_outputs = node.node_inputs@node.node_outputs in 
372 
let is_local v = 
373 
List.for_all ((<>) v) inputs_outputs in 
374 
let defs, vars = 
375 
List.fold_left (normalize_eq_split false node) ([], inputs_outputs@node.node_locals) node.node_eqs in 
376  
377 
(* Update mutable fields of eexpr to perform normalization of specification/annotations *) 
378 
List.iter (fun a > List.iter (fun (_, ann) > normalize_eexpr decls node inputs_outputs ann) a.annots) 
379 
node.node_annot; 
380 
let _ = match node.node_spec with None > ()  Some s > normalize_spec decls node [] s in 
381 

382 
let new_locals = List.filter is_local vars in 
383 
let node = 
384 
{ node with node_locals = new_locals; 
385 
node_eqs = defs; 
386 
} 
387 
in ((*Printers.pp_node Format.err_formatter node;*) node) 
388  
389 
let normalize_decl decls decl = 
390 
match decl.top_decl_desc with 
391 
 Node nd > 
392 
{decl with top_decl_desc = Node (normalize_node decls nd)} 
393 
 Open _  ImportedNode _  ImportedFun _  Consts _ > decl 
394 

395 
let normalize_prog decls = 
396 
List.map (normalize_decl decls) decls 
397  
398 
(* Local Variables: *) 
399 
(* compilecommand:"make C .." *) 
400 
(* End: *) 