Revision 0d79d0f3 src/tools/seal_utils.ml
src/tools/seal_utils.ml  

3  3 

4  4 
let report = Log.report ~plugin:"seal" 
5  5  
6 


7 


8 
(******************************************************************************) 

9 
(* Computing a slice of a node, selecting only some variables, based on *) 

10 
(* their COI (cone of influence) *) 

11 
(******************************************************************************) 

12  6  
13 
(* Basic functions to search into nodes. Could be moved to corelang eventually *) 

14 
let is_variable nd vid = 

15 
List.exists 

16 
(fun v > v.var_id = vid) 

17 
nd.node_locals 

18 


19 
let find_variable nd vid = 

20 
List.find 

21 
(fun v > v.var_id = vid) 

22 
nd.node_locals 

23  
24 
(* Returns the vars required to compute v. 

25 
Memories are specifically identified. *) 

26 
let coi_var deps nd v = 

27 
let vname = v.var_id in 

28 
let sliced_deps = 

29 
Causality.slice_graph deps vname 

30 
in 

31 
(* Format.eprintf "sliced graph for %a: %a@." 

32 
* Printers.pp_var v 

33 
* Causality.pp_dep_graph sliced_deps; *) 

34 
let vset, memset = 

35 
IdentDepGraph.fold_vertex 

36 
(fun vname (vset,memset) > 

37 
if Causality.ExprDep.is_read_var vname 

38 
then 

39 
let vname' = String.sub vname 1 (1 + String.length vname) in 

40 
if is_variable nd vname' then 

41 
ISet.add vname' vset, 

42 
ISet.add vname' memset 

43 
else 

44 
vset, memset 

45 
else 

46 
ISet.add vname vset, memset 

47 
) 

48 
sliced_deps 

49 
(ISet.singleton vname, ISet.empty) 

50 
in 

51 
report ~level:3 (fun fmt > Format.fprintf fmt "COI of var %s: (%a // %a)@." 

52 
v.var_id 

53 
(fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements vset) 

54 
(fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements memset) 

55 
) ; 

56 
vset, memset 

57  
58 


59 
(* Computes the variables required to compute vl. Variables /seen/ do not need 

60 
to be computed *) 

61 
let rec coi_vars deps nd vl seen = 

62 
let coi_vars = coi_vars deps nd in 

63 
List.fold_left 

64 
(fun accu v > 

65 
let vset, memset = coi_var deps nd v in 

66 
(* We handle the new mems discovered in the coi *) 

67 
let memset = 

68 
ISet.filter ( 

69 
fun vid > 

70 
not 

71 
(List.exists 

72 
(fun v > v.var_id = vid) 

73 
vl 

74 
) 

75 
) memset 

76 
in 

77 
let memset_vars = 

78 
ISet.fold ( 

79 
fun vid accu > 

80 
(find_variable nd vid)::accu 

81 
) memset [] 

82 
in 

83 
let vset' = 

84 
coi_vars memset_vars (vl@seen) 

85 
in 

86 
ISet.union accu (ISet.union vset vset') 

87 
) 

88 
ISet.empty 

89 
(List.filter 

90 
(fun v > not (List.mem v seen)) 

91 
vl 

92 
) 

93 


94 


95 
(* compute the coi of vars_to_keeps in node nd *) 

96 
let compute_sliced_vars vars_to_keep deps nd = 

97 
ISet.elements (coi_vars deps nd vars_to_keep []) 

98  
99  
100  
101  
102  
103 
(* If existing outputs are included in vars_to_keep, just slice the content. 

104 
Otherwise outputs are replaced by vars_to_keep *) 

105 
let slice_node vars_to_keep msch nd = 

106 
let coi_vars = 

107 
compute_sliced_vars vars_to_keep msch.Scheduling_type.dep_graph nd 

108 
in 

109 
report ~level:3 (fun fmt > Format.fprintf fmt 

110 
"COI Vars: %a@." 

111 
(Utils.fprintf_list ~sep:"," Format.pp_print_string) 

112 
coi_vars); 

113 
let outputs = 

114 
List.filter 

115 
( 

116 
fun v > List.mem v.var_id coi_vars 

117 
) nd.node_outputs 

118 
in 

119 
let outputs = match outputs with 

120 
[] > ( 

121 
report ~level:1 (fun fmt > Format.fprintf fmt "No visible output variable, subtituting with provided vars@ "); 

122 
vars_to_keep 

123 
) 

124 
 l > l 

125 
in 

126 
let locals = 

127 
List.filter (fun v > List.mem v.var_id coi_vars) nd.node_locals 

128 
in 

129  
130 
(* Split tuples while sorting eqs *) 

131 
let sorted_eqs = Scheduling.sort_equations_from_schedule nd msch.Scheduling_type.schedule in 

132  
133 
let stmts = 

134 
List.filter ( 

135 
fun (* stmt > 

136 
* match stmt with 

137 
*  Aut _ > assert false 

138 
*  Eq *) eq > ( 

139 
match eq.eq_lhs with 

140 
[vid] > List.mem vid coi_vars 

141 
 _ > Format.eprintf "Faulty statement: %a@.@?" Printers.pp_node_eq eq; assert false 

142 
(* should not happen after inlining and normalization *) 

143 
) 

144 
) sorted_eqs 

145 
in 

146 
{ nd 

147 
with 

148 
node_outputs = outputs; 

149 
node_locals = locals; 

150 
node_stmts = List.map (fun e > Eq e) stmts 

151 
} 

152  
153 
(* Switched system extraction *) 

154 
type element = IsInit  Expr of expr 

155 
type guarded_expr = (element * bool) list * element 

156 
type mdef_t = guarded_expr list 

157 


158 
let pp_guard_expr fmt (gl,e) = 

159 
let pp_elem fmt e = 

160 
match e with 

161 
 IsInit > Format.fprintf fmt "init" 

162 
 Expr e > Printers.pp_expr fmt e 

163 
in 

164 
Format.fprintf fmt "%a > %a" 

165 
(fprintf_list ~sep:"; " 

166 
(fun fmt (e,b) > if b then pp_elem fmt e else Format.fprintf fmt "not(%a)" pp_elem e)) gl 

167 
pp_elem e 

168 


169 
let concatenate_ge gel1 posneg gel2 = 

170 
List.fold_left ( 

171 
fun accu (g2,e2) > 

172 
List.fold_left ( 

173 
fun accu (g1,e1) > 

174 
((e1, posneg)::g1@g2, e2)::accu 

175 
) accu gel1 

176 
) [] gel2 

177 


178 
let add_init defs vid = 

179 
Hashtbl.add defs vid [[], IsInit] 

180 


181 
let rec rewrite defs expr : guarded_expr list = 

182 
match expr.expr_desc with 

183 
 Expr_const _  Expr_appl _ > [[], Expr expr] 

184 
 Expr_ident id > 

185 
if Hashtbl.mem defs id then 

186 
Hashtbl.find defs id 

187 
else 

188 
(* id should be an input *) 

189 
[[], Expr expr] 

190 
 Expr_ite (g, e1, e2) > 

191 
let g = rewrite defs g and 

192 
e1 = rewrite defs e1 and 

193 
e2 = rewrite defs e2 in 

194 
(concatenate_ge g true e1)@ 

195 
(concatenate_ge g false e2) 

196 
 Expr_merge (g, branches) > 

197 
assert false (* TODO *) 

198 


199 
 Expr_when (e, _, _) > rewrite defs e 

200 
 Expr_arrow _ > [[], IsInit] (* At this point the only arrow should be true > false *) 

201 
 Expr_tuple _  Expr_fby _ 

202 
(* Should be removed by mormalization and inlining *) 

203 
> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false 

204 
 Expr_array _  Expr_access _  Expr_power _ 

205 
(* Arrays not handled here yet *) 

206 
> assert false 

207 
 Expr_pre _ > (* Not rewriting mem assign *) 

208 
assert false 

209 
and add_def defs vid expr = 

210 
Hashtbl.add defs vid (rewrite defs expr) 

211  
212 
(* Takes a list of guarded exprs (ge) and a guard 

213 
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. 

214  
215 
When a given ge doesn't mention positively or negatively such guards, it is duplicated in both lists *) 

216 
let split_mdefs elem (mdefs: guarded_expr list) = 

217 
List.fold_left ( 

218 
fun (selected, left_out) 

219 
((guards, expr) as ge) > 

220 
(* select the element of guards that match the argument elem *) 

221 
let select_fun (elem',_) = 

222 
match elem, elem' with 

223 
 IsInit, IsInit > true 

224 
 Expr e, Expr e' > 

225 
Corelang.is_eq_expr e e' 

226 
 _ > false 

227 
in 

228 
let sel, others_guards = List.partition select_fun guards in 

229 
match sel with 

230 
(* we extract the element from the list and add it to the 

231 
appropriate list *) 

232 
 [_, sel_status] > 

233 
if sel_status then 

234 
(others_guards,expr)::selected, left_out 

235 
else selected, (others_guards,expr)::left_out 

236 
 [] > (* no such guard exists, we have to duplicate the 

237 
guard_expr in both lists *) 

238 
ge::selected, ge::left_out 

239 
 _ > assert false (* more then one element selected. Should 

240 
not happen , or trival dead code like if 

241 
x then if not x then dead code *) 

242 
) ([],[]) mdefs 

243 


244 
let split_mem_defs 

245 
(elem: element) 

246 
(mem_defs: (ident * guarded_expr list) list) : 

247 
((ident * mdef_t) list) * ((ident * mdef_t) list) 

248 
= 

249 
List.fold_right (fun (m,mdefs) 

250 
(accu_pos, accu_neg) > 

251 
let pos, neg = 

252 
split_mdefs elem mdefs 

253 
in 

254 
(m, pos)::accu_pos, 

255 
(m, neg)::accu_neg 

256 
) mem_defs ([],[]) 

257  
258  
259 
(* Split a list of mem_defs into init and step lists of guarded 

260 
expressions per memory. *) 

261 
let split_init mem_defs = 

262 
split_mem_defs IsInit mem_defs 

263  
264 
let pick_guard mem_defs : expr = 

265 
let gel = List.flatten (List.map snd mem_defs) in 

266 
let gl = List.flatten (List.map fst gel) in 

267 
let all_guards = 

268 
List.map ( 

269 
(* selecting guards and getting rid of boolean *) 

270 
fun (e,b) > 

271 
match e with 

272 
 Expr e > e 

273 
 _ > assert false 

274 
(* should have been filtered out 

275 
yet *) 

276 
) gl 

277 
in 

278 
(* TODO , one could sort by occurence and provided the most common 

279 
one *) 

280 
List.hd all_guards 

281 


282 
(* Transform a list of variable * guarded exprs into a list of guarded pairs (variable, expressions) 

283 
*) 

284 
let rec build_switch_sys 

285 
(mem_defs : (Utils.ident * guarded_expr list) list ) 

286 
prefix 

287 
: 

288 
((expr * bool) list * (ident * expr) list ) list = 

289 
(* if all mem_defs have empty guards, we are done, return prefix, 

290 
mem_defs expr. 

291  
292 
otherwise pick a guard in one of the mem, eg (g, b) then for each 

293 
other mem, one need to select the same guard g with the same status b, *) 

294 
if List.for_all (fun (m,mdefs) > 

295 
(* All defs are unguarded *) 

296 
match mdefs with 

297 
 [[], _] > true 

298 
 _ > false) mem_defs 

299 
then 

300 
[prefix , 

301 
List.map (fun (m,gel) > 

302 
match gel with 

303 
 [_,e] > 

304 
let e = 

305 
match e with 

306 
 Expr e > e 

307 
 _ > assert false (* No IsInit expression *) 

308 
in 

309 
m,e 

310 
 _ > assert false 

311 
) mem_defs] 

312 
else 

313 
(* Picking a guard *) 

314 
let elem : expr = pick_guard mem_defs in 

315 
let pos, neg = 

316 
split_mem_defs 

317 
(Expr elem) 

318 
mem_defs 

319 
in 

320 
(* Special cases to avoid useless computations: true, false conditions *) 

321 
match elem.expr_desc with 

322 
 Expr_ident "true" > build_switch_sys pos prefix 

323 
 Expr_const (Const_tag tag) when tag = Corelang.tag_true 

324 
> build_switch_sys pos prefix 

325 
 Expr_ident "false" > build_switch_sys neg prefix 

326 
 Expr_const (Const_tag tag) when tag = Corelang.tag_false 

327 
> build_switch_sys neg prefix 

328 
 _ > (* Regular case *) 

329 
let _ = ( 

330 
Format.eprintf "Expr is %a@." Printers.pp_expr elem; 

331 
match elem.expr_desc with 

332 
 Expr_const _ > Format.eprintf "a const@." 

333 


334 
 Expr_ident _ > Format.eprintf "an ident@." 

335 
 _ > Format.eprintf "something else@." 

336 
) 

337 
in 

338 
(build_switch_sys pos ((elem, true)::prefix)) 

339 
@ 

340 
(build_switch_sys neg ((elem, false)::prefix)) 

341 


342  
343  
344 


345 
(* Take a normalized node and extract a list of switches: (cond, 

346 
update) meaning "if cond then update" where update shall define all 

347 
node memories. Everything as to be expressed over inputs or memories, intermediate variables are removed through inlining *) 

348 
let node_as_switched_sys (mems:var_decl list) nd = 

349 
(* rescheduling node: has been scheduled already, no need to protect 

350 
the call to schedule_node *) 

351 
let nd_report = Scheduling.schedule_node nd in 

352 
let schedule = nd_report.Scheduling_type.schedule in 

353 
let sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in 

354 
let defs : (ident, guarded_expr list) Hashtbl.t = Hashtbl.create 13 in 

355 
let add_def = add_def defs in 

356 
(* Registering node equations *) 

357 
let mem_defs = 

358 
List.fold_left (fun accu eq > 

359 
match eq.eq_lhs with 

360 
 [vid] > 

361 
(* Only focus on non memory definitions *) 

362 
if not (List.exists (fun v > v.var_id = vid) mems) then ( 

363 
add_def vid eq.eq_rhs; 

364 
accu 

365 
) 

366 
else 

367 
( 

368 
match eq.eq_rhs.expr_desc with 

369 
 Expr_pre def_m > 

370 
(vid, rewrite defs def_m)::accu 

371 
 _ > assert false 

372 
) 

373 
 _ > assert false (* should have been removed by normalization *) 

374 
) [] sorted_eqs 

375 
in 

376 
(* Printing memories definitions *) 

377 
report ~level:3 

378 
(fun fmt > 

379 
Format.fprintf fmt 

380 
"%a" 

381 
(Utils.fprintf_list ~sep:"@." 

382 
(fun fmt (m,mdefs) > 

383 
Format.fprintf fmt 

384 
"%s > @[<v 0>[%a@] ]@." 

385 
m 

386 
(Utils.fprintf_list ~sep:"@ " 

387 
pp_guard_expr) mdefs 

388 
)) 

389 
mem_defs); 

390 
let init_defs, update_defs = 

391 
split_init mem_defs 

392 
in 

393 
report ~level:3 

394 
(fun fmt > 

395 
Format.fprintf fmt 

396 
"Init:@.%a@.Step@.%a" 

397 
(Utils.fprintf_list ~sep:"@." 

398 
(fun fmt (m,mdefs) > 

399 
Format.fprintf fmt 

400 
"%s > @[<v 0>[%a@] ]@." 

401 
m 

402 
(Utils.fprintf_list ~sep:"@ " 

403 
pp_guard_expr) mdefs 

404 
)) 

405 
init_defs 

406 
(Utils.fprintf_list ~sep:"@." 

407 
(fun fmt (m,mdefs) > 

408 
Format.fprintf fmt 

409 
"%s > @[<v 0>[%a@] ]@." 

410 
m 

411 
(Utils.fprintf_list ~sep:"@ " 

412 
pp_guard_expr) mdefs 

413 
)) 

414 
update_defs); 

415 
let sw_init= 

416 
build_switch_sys init_defs [] 

417 
in 

418 
let sw_sys = 

419 
build_switch_sys update_defs [] 

420 
in 

421 
sw_init, sw_sys 
Also available in: Unified diff