## lustrec / src / tools / seal_extract.ml @ 0d79d0f3

History | View | Annotate | Download (12.2 KB)

1 | 0d79d0f3 | ploc | 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 sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in |
||

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

303 | let add_def = add_def defs in |
||

304 | (* Registering node equations *) |
||

305 | let mem_defs = |
||

306 | List.fold_left (fun accu eq -> |
||

307 | match eq.eq_lhs with |
||

308 | | [vid] -> |
||

309 | (* Only focus on non memory definitions *) |
||

310 | if not (List.exists (fun v -> v.var_id = vid) mems) then ( |
||

311 | report ~level:3 (fun fmt -> Format.fprintf fmt "Registering variable %s@." vid); |
||

312 | add_def vid eq.eq_rhs; |
||

313 | accu |
||

314 | ) |
||

315 | else |
||

316 | ( |
||

317 | match eq.eq_rhs.expr_desc with |
||

318 | | Expr_pre def_m -> |
||

319 | report ~level:3 (fun fmt -> Format.fprintf fmt "Preparing mem %s@." vid); |
||

320 | |||

321 | (vid, rewrite defs def_m)::accu |
||

322 | | _ -> assert false |
||

323 | ) |
||

324 | | _ -> assert false (* should have been removed by normalization *) |
||

325 | ) [] sorted_eqs |
||

326 | in |
||

327 | report ~level:2 (fun fmt -> Format.fprintf fmt "Printing out memories definitions (may takes time)@."); |
||

328 | (* Printing memories definitions *) |
||

329 | report ~level:3 |
||

330 | (fun fmt -> |
||

331 | Format.fprintf fmt |
||

332 | "%a" |
||

333 | (Utils.fprintf_list ~sep:"@." |
||

334 | (fun fmt (m,mdefs) -> |
||

335 | Format.fprintf fmt |
||

336 | "%s -> @[<v 0>[%a@] ]@." |
||

337 | m |
||

338 | (Utils.fprintf_list ~sep:"@ " |
||

339 | pp_guard_expr) mdefs |
||

340 | )) |
||

341 | mem_defs); |
||

342 | let init_defs, update_defs = |
||

343 | split_init mem_defs |
||

344 | in |
||

345 | report ~level:3 |
||

346 | (fun fmt -> |
||

347 | Format.fprintf fmt |
||

348 | "Init:@.%a@.Step@.%a" |
||

349 | (Utils.fprintf_list ~sep:"@." |
||

350 | (fun fmt (m,mdefs) -> |
||

351 | Format.fprintf fmt |
||

352 | "%s -> @[<v 0>[%a@] ]@." |
||

353 | m |
||

354 | (Utils.fprintf_list ~sep:"@ " |
||

355 | pp_guard_expr) mdefs |
||

356 | )) |
||

357 | init_defs |
||

358 | (Utils.fprintf_list ~sep:"@." |
||

359 | (fun fmt (m,mdefs) -> |
||

360 | Format.fprintf fmt |
||

361 | "%s -> @[<v 0>[%a@] ]@." |
||

362 | m |
||

363 | (Utils.fprintf_list ~sep:"@ " |
||

364 | pp_guard_expr) mdefs |
||

365 | )) |
||

366 | update_defs); |
||

367 | let sw_init= |
||

368 | build_switch_sys init_defs [] |
||

369 | in |
||

370 | let sw_sys = |
||

371 | build_switch_sys update_defs [] |
||

372 | in |
||

373 | sw_init, sw_sys |