Revision 7aaacbc9 src/tools/seal/seal_extract.ml
src/tools/seal/seal_extract.ml  

15  15 
 IsInit > Format.fprintf fmt "init" 
16  16 
 Expr e > Printers.pp_expr fmt e 
17  17  
18 
let pp_guard_list fmt gl = 

19 
(fprintf_list ~sep:"; " 

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

21 


18  22 
let pp_guard_expr fmt (gl,e) = 
19  23 
Format.fprintf fmt "%a > %a" 
20 
(fprintf_list ~sep:"; " 

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

24 
pp_guard_list gl 

22  25 
pp_elem e 
23  26  
24  27 
let pp_mdefs fmt gel = fprintf_list ~sep:"@ " pp_guard_expr fmt gel 
...  ...  
222  225 
let check_sat, clean_guard = 
223  226 
( 
224  227 
fun l > 
228 
(* Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " pp_guard_list l; *) 

225  229 
let solver = Z3.Solver.mk_simple_solver !ctx in 
226  230 
try ( 
227  231 
let zl = 
...  ...  
237  241 
neg_ze ze 
238  242 
) l 
239  243 
in 
244 
(* Format.eprintf "Z3 exprs: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; *) 

240  245 
let status_res = Z3.Solver.check solver zl in 
246 
(* Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); *) 

241  247 
let sat = match status_res with 
242  248 
 Z3.Solver.UNSATISFIABLE > false 
243  249 
 _ > true in 
...  ...  
268  274 
Z3.Goal.add goal zl; 
269  275 
let goal' = Z3.Goal.simplify goal None in 
270  276 

271 
Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@." 

272 
(Z3.Goal.to_string goal) 

273 
(Z3.Goal.to_string goal') 

274 
(Z3.Solver.string_of_status status_res) 

275 
;


277 
(* Format.eprintf "Goal before: %s@.Goal after : %s@.Sat? %s@."


278 
* (Z3.Goal.to_string goal)


279 
* (Z3.Goal.to_string goal')


280 
* (Z3.Solver.string_of_status status_res)


281 
* ; *)


276  282 
let ze = Z3.Goal.as_expr goal' in 
277 
Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); 

278 
(* let l = 

279 
match zexpr_to_expr ze with 

283 
(* Format.eprintf "as an expr: %s@." (Z3.Expr.to_string ze); *) 

284 
let l = 

285 
(* zexpr_to_expr function returns a pair (is_init option, expr 

286 
option). Since we are simplifying /pure/ expression, there 

287 
should be not init subexpressions here. *) 

288 
match zexpr_to_expr ze with 

280  289 
 None, None > [] 
281  290 
 None, Some e > [e, true] 
282  291 
 _ > assert false 
283 
(*  Some init, None > [IsInit, init] 

284 
 Some init, Some e > [IsInit, init; Expr e, true] 

285 
*) in 

286 
*) 

292 
in 

287  293 
l 
294 


295 


288  296 
) 
289  297 
with Zustre_common.UnknownFunction(id, msg) > ( 
290  298 
report ~level:1 msg; 
...  ...  
317  325 
(* Filtering out trivial cases. More semantics ones would have to be 
318  326 
addressed later *) 
319  327 
let check (gexpr, posneg) l = 
328 
(* Format.eprintf "Checking %a=%b in %a@ " 

329 
* pp_elem gexpr 

330 
* posneg 

331 
* pp_guard_list l 

332 
* ; *) 

320  333 
(* Check if gepxr is part of l *) 
321 
let sel_fun = select_elem gexpr in 

322 
if List.exists sel_fun l then 

334 
let sel_fun = select_elem gexpr in 

335 
let ok, res = 

336 
if List.exists sel_fun l then ( 

323  337 
(* Checking the guard value posneg *) 
324  338 
let _, status = List.find sel_fun l in 
339 
(* Format.eprintf "Found %a in %a. @ Checking status (%b).@ " 

340 
* pp_elem gexpr 

341 
* pp_guard_list l 

342 
* (status=posneg) 

343 
* ; *) 

325  344 
status=posneg, l 
326 
else 

345 
) 

346 
else ( 

347 
(* Format.eprintf "Not found.@ "; *) 

327  348 
(* Valid: no overlap *) 
328  349 
(* Individual checkat *) 
329  350 
let ok, e = check_sat [gexpr, posneg] in 
351 
(* let ok, e = true, [gexpr, posneg] in (* TODO solve the issue with check_sat *) *) 

352 
(* Format.eprintf "Check_sat? %b@ " ok; *) 

330  353 
if ok then 
331  354 
let l = e@l in 
332  355 
let ok, l = check_sat l in 
356 
(* let ok, l = true, l in (* TODO solve the issue with check_sat *) *) 

333  357 
ok, l 
334  358 
else 
335 
true, l 

359 
false, [] 

360 
) 

361 
in 

362 
(* Format.eprintf "Check sat res: %a@ " 

363 
* pp_guard_list res; *) 

364 
ok, res 

336  365 
in 
337  366 
let ok, gl = 
338  367 
List.fold_left ( 
...  ...  
351  380 
check fresh_g gl 
352  381 
) 
353  382 
else 
354 
ok, []


383 
false, []


355  384  
385 
(* DEBUG 

386 
let combine_guards ?(fresh=None) gl1 gl2 = 

387 
true, 

388 
(match fresh with None > []  Some (gexpr, posneg) > [gexpr, posneg])@gl1@gl2 

389 
*) 

356  390 
(* Encode "If gel1=posneg then gel2": 
357  391 
 Compute the combination of guarded exprs in gel1 and gel2: 
358  392 
 Each guarded_expr in gel1 is transformed as a guard: the 
...  ...  
365  399 
fun accu (g2,e2) > 
366  400 
List.fold_left ( 
367  401 
fun accu (g1,e1) > 
402 
(* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ " 

403 
* pp_elem e1 

404 
* posneg 

405 
* pp_guard_list g1 

406 
* pp_guard_list g2; *) 

407 


368  408 
let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in 
409 
(* Format.eprintf "@]@ Result is [%a]@ " 

410 
* pp_guard_list gl; *) 

411 


369  412 
if ok then 
370  413 
(gl, e2)::accu 
371 
else 

414 
else ( 

415 


372  416 
accu 
417 
) 

373  418 
) accu gel1 
374  419 
) [] gel2 
375  420  
376  421 
let rec rewrite defs expr : guarded_expr list = 
377  422 
let rewrite = rewrite defs in 
378 
match expr.expr_desc with 

379 
 Expr_appl (id, args, None) > 

380 
let args = rewrite args in 

381 
List.map (fun (guards, e) > 

423 
let res = 

424 
match expr.expr_desc with 

425 
 Expr_appl (id, args, None) > 

426 
let args = rewrite args in 

427 
List.map (fun (guards, e) > 

382  428 
guards, 
383  429 
Expr {expr with expr_desc = Expr_appl(id, deelem e, None)} 
384 
) args 

385 
 Expr_const _ > [[], Expr expr] 

386 
 Expr_ident id > 

387 
if Hashtbl.mem defs id then 

388 
Hashtbl.find defs id 

389 
else 

390 
(* id should be an input *) 

391 
[[], Expr expr] 

392 
 Expr_ite (g, e1, e2) > 

393 
let g = rewrite g and 

394 
e1 = rewrite e1 and 

395 
e2 = rewrite e2 in 

396 
(concatenate_ge g true e1)@ 

397 
(concatenate_ge g false e2) 

398 
 Expr_merge (g, branches) > 

399 
assert false (* TODO: deal with merges *) 

400 


401 
 Expr_when (e, _, _) > rewrite e 

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

403 
 Expr_tuple el > 

404 
(* Each expr is associated to its flatten guarded expr list *) 

405 
let gell = List.map rewrite el in 

406 
(* Computing all combinations: we obtain a list of guarded tuple *) 

407 
let rec aux gell : (guard * expr list) list = 

408 
match gell with 

409 
 [] > assert false (* Not happening *) 

410 
 [gel] > List.map (fun (g,e) > g, [deelem e]) gel 

411 
 gel::getl > 

412 
let getl = aux getl in 

413 
List.fold_left ( 

414 
fun accu (g,e) > 

415 
List.fold_left ( 

430 
) args


431 
 Expr_const _ > [[], Expr expr]


432 
 Expr_ident id >


433 
if Hashtbl.mem defs id then


434 
Hashtbl.find defs id


435 
else


436 
(* id should be an input *)


437 
[[], Expr expr]


438 
 Expr_ite (g, e1, e2) >


439 
let g = rewrite g and


440 
e1 = rewrite e1 and


441 
e2 = rewrite e2 in


442 
(concatenate_ge g true e1)@


443 
(concatenate_ge g false e2)


444 
 Expr_merge (g, branches) >


445 
assert false (* TODO: deal with merges *)


446 


447 
 Expr_when (e, _, _) > rewrite e


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


449 
 Expr_tuple el >


450 
(* Each expr is associated to its flatten guarded expr list *)


451 
let gell = List.map rewrite el in


452 
(* Computing all combinations: we obtain a list of guarded tuple *)


453 
let rec aux gell : (guard * expr list) list =


454 
match gell with


455 
 [] > assert false (* Not happening *)


456 
 [gel] > List.map (fun (g,e) > g, [deelem e]) gel


457 
 gel::getl >


458 
let getl = aux getl in


459 
List.fold_left (


460 
fun accu (g,e) >


461 
List.fold_left (


416  462 
fun accu (gl, minituple) > 
417  463 
let is_compat, guard_comb = combine_guards g gl in 
418  464 
if is_compat then 
...  ...  
420  466 
new_gt::accu 
421  467 
else 
422  468 
accu 
423 


469 


424  470 
) accu getl 
425 
) [] gel 

426 
in 

427 
let gtuples = aux gell in 

428 
(* Rebuilding the valid type: guarded expr list (with tuple exprs) *) 

429 
List.map (fun (g,tuple) > g, Expr {expr with expr_desc = Expr_tuple tuple}) gtuples 

430 
 Expr_fby _ 

431 
 Expr_appl _ 

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

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

434 
 Expr_array _  Expr_access _  Expr_power _ 

435 
(* Arrays not handled here yet *) 

436 
> assert false 

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

438 
assert false 

471 
) [] gel 

472 
in 

473 
let gtuples = aux gell in 

474 
(* Rebuilding the valid type: guarded expr list (with tuple exprs) *) 

475 
List.map (fun (g,tuple) > g, Expr {expr with expr_desc = Expr_tuple tuple}) gtuples 

476 
 Expr_fby _ 

477 
 Expr_appl _ 

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

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

480 
 Expr_array _  Expr_access _  Expr_power _ 

481 
(* Arrays not handled here yet *) 

482 
> assert false 

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

484 
assert false 

485 
in 

486 
(* Format.eprintf "Rewriting %a as [@[<v 0>%a@]]@ " 

487 
* Printers.pp_expr expr 

488 
* (Utils.fprintf_list ~sep:"@ " 

489 
* pp_guard_expr) res; *) 

490 
res 

439  491 
and add_def defs vid expr = 
440 
Hashtbl.add defs vid (rewrite defs expr) 

492 
let vid_defs = rewrite defs expr in 

493 
(* Format.eprintf "Add_def: %s = %a@. > @[<v 0>%a@]@." 

494 
* vid 

495 
* Printers.pp_expr expr 

496 
* ( 

497 
* (Utils.fprintf_list ~sep:"@ " 

498 
* pp_guard_expr)) vid_defs; *) 

499 
Hashtbl.add defs vid vid_defs 

441  500  
442  501 
(* Takes a list of guarded exprs (ge) and a guard 
443  502 
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. 
...  ...  
608  667 
let _ = 
609  668 
List.iter (fun c > Hashtbl.add const_defs c.const_id c.const_value) consts 
610  669 
in 
670  
611  671 

612  672 
(* Registering node equations: identifying mem definitions and 
613  673 
storing others in the "defs" hashtbl. *) 
...  ...  
685  745 
build_switch_sys update_defs [] 
686  746 
in 
687  747 
clean_sys sw_init, clean_sys sw_sys 
748 

Also available in: Unified diff