lustrec / src / tools / seal / seal_extract.ml @ 6517aa0e
History  View  Annotate  Download (12.3 KB)
1 
open Lustre_types 

2 
open Utils 
3 
open Seal_utils 
4  
5 
(* Switched system extraction *) 
6 
type element = IsInit  Expr of expr 
7 
type guard = (element * bool) list 
8 
type guarded_expr = guard * element 
9 
type mdef_t = guarded_expr list 
10  
11 
let pp_elem fmt e = 
12 
match e with 
13 
 IsInit > Format.fprintf fmt "init" 
14 
 Expr e > Printers.pp_expr fmt e 
15  
16 
let pp_guard_expr fmt (gl,e) = 
17 
Format.fprintf fmt "%a > %a" 
18 
(fprintf_list ~sep:"; " 
19 
(fun fmt (e,b) > if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) gl 
20 
pp_elem e 
21  
22 
let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel 
23  
24 

25 
let add_init defs vid = 
26 
Hashtbl.add defs vid [[], IsInit] 
27  
28 
let deelem e = match e with 
29 
Expr e > e 
30 
 IsInit > assert false (* Wasn't expecting isinit here: we are building values! *) 
31  
32 
let is_eq_elem elem elem' = 
33 
match elem, elem' with 
34 
 IsInit, IsInit > true 
35 
 Expr e, Expr e' > 
36 
Corelang.is_eq_expr e e' 
37 
 _ > false 
38  
39 
let select_elem elem (gelem, _) = 
40 
is_eq_elem elem gelem 
41  
42 

43 
let combine_guards ?(fresh=None) gl1 gl2 = 
44 
(* Filtering out trivial cases. More semantics ones would have to be 
45 
addressed later *) 
46 
let check (gexpr, posneg) l = 
47 
(* Check if gepxr is part of l *) 
48 
let sel_fun = select_elem gexpr in 
49 
if List.exists sel_fun l then 
50 
(* Checking the guard value posneg *) 
51 
let _, status = List.find sel_fun l in 
52 
status=posneg, l 
53 
else 
54 
(* Valid: no overlap *) 
55 
true, (gexpr, posneg)::l 
56 
in 
57 
let ok, gl = 
58 
List.fold_left ( 
59 
fun (ok, l) g > 
60 
(* Bypass for negative output *) 
61 
if not ok then false, [] 
62 
else 
63 
check g l 
64 
) (true, gl2) gl1 
65 
in 
66 
if ok then 
67 
match fresh with 
68 
None > true, gl 
69 
 Some fresh_g > ( 
70 
(* Checking the fresh element *) 
71 
check fresh_g gl 
72 
) 
73 
else 
74 
ok, [] 
75  
76 
(* Encode "If gel1=posneg then gel2": 
77 
 Compute the combination of guarded exprs in gel1 and gel2: 
78 
 Each guarded_expr in gel1 is transformed as a guard: the 
79 
expression is associated to posneg. 
80 
 Existing guards in gel2 are concatenated to that list of guards 
81 
 We keep expr in the ge of gel2 as the legitimate expression 
82 
*) 
83 
let concatenate_ge gel1 posneg gel2 = 
84 
List.fold_left ( 
85 
fun accu (g2,e2) > 
86 
List.fold_left ( 
87 
fun accu (g1,e1) > 
88 
let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in 
89 
if ok then 
90 
(gl, e2)::accu 
91 
else 
92 
accu 
93 
) accu gel1 
94 
) [] gel2 
95  
96 
let rec rewrite defs expr : guarded_expr list = 
97 
let rewrite = rewrite defs in 
98 
match expr.expr_desc with 
99 
 Expr_appl (id, args, None) > 
100 
let args = rewrite args in 
101 
List.map (fun (guards, e) > 
102 
guards, 
103 
Expr {expr with expr_desc = Expr_appl(id, deelem e, None)} 
104 
) args 
105 
 Expr_const _ > [[], Expr expr] 
106 
 Expr_ident id > 
107 
if Hashtbl.mem defs id then 
108 
Hashtbl.find defs id 
109 
else 
110 
(* id should be an input *) 
111 
[[], Expr expr] 
112 
 Expr_ite (g, e1, e2) > 
113 
let g = rewrite g and 
114 
e1 = rewrite e1 and 
115 
e2 = rewrite e2 in 
116 
(concatenate_ge g true e1)@ 
117 
(concatenate_ge g false e2) 
118 
 Expr_merge (g, branches) > 
119 
assert false (* TODO: deal with merges *) 
120 

121 
 Expr_when (e, _, _) > rewrite e 
122 
 Expr_arrow _ > [[], IsInit] (* At this point the only arrow should be true > false *) 
123 
 Expr_tuple el > 
124 
(* Each expr is associated to its flatten guarded expr list *) 
125 
let gell = List.map rewrite el in 
126 
(* Computing all combinations: we obtain a list of guarded tuple *) 
127 
let rec aux gell : (guard * expr list) list = 
128 
match gell with 
129 
 [] > assert false (* Not happening *) 
130 
 [gel] > List.map (fun (g,e) > g, [deelem e]) gel 
131 
 gel::getl > 
132 
let getl = aux getl in 
133 
List.fold_left ( 
134 
fun accu (g,e) > 
135 
List.fold_left ( 
136 
fun accu (gl, minituple) > 
137 
let is_compat, guard_comb = combine_guards g gl in 
138 
if is_compat then 
139 
let new_gt : guard * expr list = (guard_comb, (deelem e)::minituple) in 
140 
new_gt::accu 
141 
else 
142 
accu 
143 

144 
) accu getl 
145 
) [] gel 
146 
in 
147 
let gtuples = aux gell in 
148 
(* Rebuilding the valid type: guarded expr list (with tuple exprs) *) 
149 
List.map (fun (g,tuple) > g, Expr {expr with expr_desc = Expr_tuple tuple}) gtuples 
150 
 Expr_fby _ 
151 
 Expr_appl _ 
152 
(* Should be removed by mormalization and inlining *) 
153 
> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false 
154 
 Expr_array _  Expr_access _  Expr_power _ 
155 
(* Arrays not handled here yet *) 
156 
> assert false 
157 
 Expr_pre _ > (* Not rewriting mem assign *) 
158 
assert false 
159 
and add_def defs vid expr = 
160 
Hashtbl.add defs vid (rewrite defs expr) 
161  
162 
(* Takes a list of guarded exprs (ge) and a guard 
163 
returns the same list of ge splited into the ones where the guard is true and the ones where it is false. In both lists the associated ge do not mention that guard anymore. 
164  
165 
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *) 
166 
let split_mdefs elem (mdefs: guarded_expr list) = 
167 
List.fold_left ( 
168 
fun (selected, left_out) 
169 
((guards, expr) as ge) > 
170 
(* select the element of guards that match the argument elem *) 
171 
let sel, others_guards = List.partition (select_elem elem) guards in 
172 
match sel with 
173 
(* we extract the element from the list and add it to the 
174 
appropriate list *) 
175 
 [_, sel_status] > 
176 
if sel_status then 
177 
(others_guards,expr)::selected, left_out 
178 
else selected, (others_guards,expr)::left_out 
179 
 [] > (* no such guard exists, we have to duplicate the 
180 
guard_expr in both lists *) 
181 
ge::selected, ge::left_out 
182 
 _ > ( 
183 
Format.eprintf "@.Spliting list on elem %a.@.List:%a@." 
184 
pp_elem elem 
185 
pp_mdefs mdefs; 
186 
assert false (* more then one element selected. Should 
187 
not happen , or trival dead code like if 
188 
x then if not x then dead code *) 
189 
) 
190 
) ([],[]) mdefs 
191 

192 
let split_mem_defs 
193 
(elem: element) 
194 
(mem_defs: (ident * guarded_expr list) list) : 
195 
((ident * mdef_t) list) * ((ident * mdef_t) list) 
196 
= 
197 
List.fold_right (fun (m,mdefs) 
198 
(accu_pos, accu_neg) > 
199 
let pos, neg = 
200 
split_mdefs elem mdefs 
201 
in 
202 
(m, pos)::accu_pos, 
203 
(m, neg)::accu_neg 
204 
) mem_defs ([],[]) 
205  
206  
207 
(* Split a list of mem_defs into init and step lists of guarded 
208 
expressions per memory. *) 
209 
let split_init mem_defs = 
210 
split_mem_defs IsInit mem_defs 
211  
212 
let pick_guard mem_defs : expr = 
213 
let gel = List.flatten (List.map snd mem_defs) in 
214 
let gl = List.flatten (List.map fst gel) in 
215 
let all_guards = 
216 
List.map ( 
217 
(* selecting guards and getting rid of boolean *) 
218 
fun (e,b) > 
219 
match e with 
220 
 Expr e > e 
221 
 _ > assert false 
222 
(* should have been filtered out 
223 
yet *) 
224 
) gl 
225 
in 
226 
(* TODO , one could sort by occurence and provided the most common 
227 
one *) 
228 
List.hd all_guards 
229 

230 
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions) 
231 
*) 
232 
let rec build_switch_sys 
233 
(mem_defs : (Utils.ident * guarded_expr list) list ) 
234 
prefix 
235 
: 
236 
((expr * bool) list * (ident * expr) list ) list = 
237 
(* if all mem_defs have empty guards, we are done, return prefix, 
238 
mem_defs expr. 
239  
240 
otherwise pick a guard in one of the mem, eg (g, b) then for each 
241 
other mem, one need to select the same guard g with the same status b, *) 
242 
if List.for_all (fun (m,mdefs) > 
243 
(* All defs are unguarded *) 
244 
match mdefs with 
245 
 [[], _] > true 
246 
 _ > false) mem_defs 
247 
then 
248 
[prefix , 
249 
List.map (fun (m,gel) > 
250 
match gel with 
251 
 [_,e] > 
252 
let e = 
253 
match e with 
254 
 Expr e > e 
255 
 _ > assert false (* No IsInit expression *) 
256 
in 
257 
m,e 
258 
 _ > assert false 
259 
) mem_defs] 
260 
else 
261 
(* Picking a guard *) 
262 
let elem : expr = pick_guard mem_defs in 
263 
let pos, neg = 
264 
split_mem_defs 
265 
(Expr elem) 
266 
mem_defs 
267 
in 
268 
(* Special cases to avoid useless computations: true, false conditions *) 
269 
match elem.expr_desc with 
270 
 Expr_ident "true" > build_switch_sys pos prefix 
271 
 Expr_const (Const_tag tag) when tag = Corelang.tag_true 
272 
> build_switch_sys pos prefix 
273 
 Expr_ident "false" > build_switch_sys neg prefix 
274 
 Expr_const (Const_tag tag) when tag = Corelang.tag_false 
275 
> build_switch_sys neg prefix 
276 
 _ > (* Regular case *) 
277 
(* let _ = ( 
278 
* Format.eprintf "Expr is %a@." Printers.pp_expr elem; 
279 
* match elem.expr_desc with 
280 
*  Expr_const _ > Format.eprintf "a const@." 
281 
* 
282 
*  Expr_ident _ > Format.eprintf "an ident@." 
283 
*  _ > Format.eprintf "something else@." 
284 
* ) 
285 
* in *) 
286 
(build_switch_sys pos ((elem, true)::prefix)) 
287 
@ 
288 
(build_switch_sys neg ((elem, false)::prefix)) 
289 

290  
291  
292 

293 
(* Take a normalized node and extract a list of switches: (cond, 
294 
update) meaning "if cond then update" where update shall define all 
295 
node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *) 
296 
let node_as_switched_sys (mems:var_decl list) nd = 
297 
(* rescheduling node: has been scheduled already, no need to protect 
298 
the call to schedule_node *) 
299 
let nd_report = Scheduling.schedule_node nd in 
300 
let schedule = nd_report.Scheduling_type.schedule in 
301 
let eqs, auts = Corelang.get_node_eqs nd in 
302 
assert (auts = []); (* Automata should be expanded by now *) 
303 
let sorted_eqs = Scheduling.sort_equations_from_schedule eqs schedule in 
304 
let defs : (ident, guarded_expr list) Hashtbl.t = Hashtbl.create 13 in 
305 
let add_def = add_def defs in 
306 
(* Registering node equations *) 
307 
let mem_defs = 
308 
List.fold_left (fun accu eq > 
309 
match eq.eq_lhs with 
310 
 [vid] > 
311 
(* Only focus on non memory definitions *) 
312 
if not (List.exists (fun v > v.var_id = vid) mems) then ( 
313 
report ~level:3 (fun fmt > Format.fprintf fmt "Registering variable %s@." vid); 
314 
add_def vid eq.eq_rhs; 
315 
accu 
316 
) 
317 
else 
318 
( 
319 
match eq.eq_rhs.expr_desc with 
320 
 Expr_pre def_m > 
321 
report ~level:3 (fun fmt > Format.fprintf fmt "Preparing mem %s@." vid); 
322  
323 
(vid, rewrite defs def_m)::accu 
324 
 _ > assert false 
325 
) 
326 
 _ > assert false (* should have been removed by normalization *) 
327 
) [] sorted_eqs 
328 
in 
329 
report ~level:2 (fun fmt > Format.fprintf fmt "Printing out memories definitions (may takes time)@."); 
330 
(* Printing memories definitions *) 
331 
report ~level:3 
332 
(fun fmt > 
333 
Format.fprintf fmt 
334 
"%a" 
335 
(Utils.fprintf_list ~sep:"@." 
336 
(fun fmt (m,mdefs) > 
337 
Format.fprintf fmt 
338 
"%s > @[<v 0>[%a@] ]@." 
339 
m 
340 
(Utils.fprintf_list ~sep:"@ " 
341 
pp_guard_expr) mdefs 
342 
)) 
343 
mem_defs); 
344 
let init_defs, update_defs = 
345 
split_init mem_defs 
346 
in 
347 
report ~level:3 
348 
(fun fmt > 
349 
Format.fprintf fmt 
350 
"Init:@.%a@.Step@.%a" 
351 
(Utils.fprintf_list ~sep:"@." 
352 
(fun fmt (m,mdefs) > 
353 
Format.fprintf fmt 
354 
"%s > @[<v 0>[%a@] ]@." 
355 
m 
356 
(Utils.fprintf_list ~sep:"@ " 
357 
pp_guard_expr) mdefs 
358 
)) 
359 
init_defs 
360 
(Utils.fprintf_list ~sep:"@." 
361 
(fun fmt (m,mdefs) > 
362 
Format.fprintf fmt 
363 
"%s > @[<v 0>[%a@] ]@." 
364 
m 
365 
(Utils.fprintf_list ~sep:"@ " 
366 
pp_guard_expr) mdefs 
367 
)) 
368 
update_defs); 
369 
let sw_init= 
370 
build_switch_sys init_defs [] 
371 
in 
372 
let sw_sys = 
373 
build_switch_sys update_defs [] 
374 
in 
375 
sw_init, sw_sys 