Revision ae08b9fc
Added by Pierre-Loïc Garoche about 5 years ago
| src/tools/seal/seal_extract.ml | ||
|---|---|---|
| 549 | 549 |
) ([], true) gel2 |
| 550 | 550 |
in |
| 551 | 551 |
not all_invalid, l |
| 552 |
|
|
| 553 |
(* Rewrite the expression expr, replacing any occurence of a variable |
|
| 552 |
|
|
| 553 |
(* Transform the guard expressions ge = [gl1, e1; gl2, e2;...] as |
|
| 554 |
[gl1, e1=id; gl2, e2=id; ...] *) |
|
| 555 |
let mk_ge_eq_id ge id = |
|
| 556 |
List.map |
|
| 557 |
(fun (gl, g_e) -> |
|
| 558 |
gl, |
|
| 559 |
if id = "true" then |
|
| 560 |
g_e |
|
| 561 |
else |
|
| 562 |
match g_e with |
|
| 563 |
| Expr g_e -> |
|
| 564 |
if id = "false" then |
|
| 565 |
Expr (Corelang.push_negations ~neg:true g_e) |
|
| 566 |
else |
|
| 567 |
let loc = g_e.expr_loc in |
|
| 568 |
Expr(Corelang.mk_eq loc |
|
| 569 |
g_e |
|
| 570 |
(Corelang.expr_of_ident id loc)) |
|
| 571 |
| _ -> assert false |
|
| 572 |
) ge |
|
| 573 |
|
|
| 574 |
(* Rewrite the expression expr, replacing any occurence of a variable |
|
| 554 | 575 |
by its definition. |
| 555 |
*) |
|
| 576 |
*)
|
|
| 556 | 577 |
let rec rewrite defs expr : elem_guarded_expr list = |
| 557 | 578 |
let rewrite = rewrite defs in |
| 558 | 579 |
let res = |
| ... | ... | |
| 578 | 599 |
let ok_else, g_else = concatenate_ge g false e2 in |
| 579 | 600 |
(if ok_then then g_then else [])@ |
| 580 | 601 |
(if ok_else then g_else else []) |
| 581 |
| Expr_merge (g, branches) -> |
|
| 582 |
assert false (* TODO: deal with merges *) |
|
| 583 |
|
|
| 584 |
| Expr_when (e, _, _) -> rewrite e |
|
| 602 |
| Expr_merge (g_id, branches) -> |
|
| 603 |
if Hashtbl.mem defs g_id then |
|
| 604 |
let g = Hashtbl.find defs g_id in |
|
| 605 |
(* Format.eprintf "Expr_merge %s = %a@." g_id (pp_mdefs pp_elem) g ; *) |
|
| 606 |
List.fold_left (fun accu (id, e) -> |
|
| 607 |
let g = mk_ge_eq_id g id in |
|
| 608 |
let e = rewrite e in |
|
| 609 |
let ok, g_eq_id = concatenate_ge g true e in |
|
| 610 |
if ok then g_eq_id@accu else accu |
|
| 611 |
) [] branches |
|
| 612 |
else |
|
| 613 |
assert false (* g should be defined already *) |
|
| 614 |
| Expr_when (e, id, l) -> |
|
| 615 |
let e = rewrite e in |
|
| 616 |
let id_def = Hashtbl.find defs id in |
|
| 617 |
let clock = mk_ge_eq_id id_def l in |
|
| 618 |
let ok, new_ge = concatenate_ge clock true e in |
|
| 619 |
if ok then new_ge else [] |
|
| 585 | 620 |
| Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *) |
| 586 | 621 |
| Expr_tuple el -> |
| 587 | 622 |
(* Each expr is associated to its flatten guarded expr list *) |
| ... | ... | |
| 628 | 663 |
* pp_guard_expr) res; *) |
| 629 | 664 |
res |
| 630 | 665 |
and add_def defs vid expr = |
| 666 |
(* Format.eprintf "Add_def: %s = %a@." |
|
| 667 |
* vid |
|
| 668 |
* Printers.pp_expr expr; *) |
|
| 631 | 669 |
let vid_defs = rewrite defs expr in |
| 670 |
(* Format.eprintf "-> @[<v 0>%a@]@." |
|
| 671 |
* (Utils.fprintf_list ~sep:"@ " |
|
| 672 |
* (pp_guard_expr pp_elem)) vid_defs; *) |
|
| 632 | 673 |
(* Format.eprintf "Add_def: %s = %a@. -> @[<v 0>%a@]@." |
| 633 | 674 |
* vid |
| 634 | 675 |
* Printers.pp_expr expr |
| ... | ... | |
| 740 | 781 |
((expr * bool) list * (ident * expr) list ) list = |
| 741 | 782 |
if !seal_debug then |
| 742 | 783 |
report ~level:4 (fun fmt -> Format.fprintf fmt "@[<v 2>Build_switch with@ %a@]@." |
| 743 |
(Utils.fprintf_list ~sep:",@ " |
|
| 744 |
(fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]" |
|
| 745 |
id |
|
| 746 |
(pp_mdefs pp_elem) gel)) |
|
| 747 |
mem_defs); |
|
| 784 |
pp_all_defs |
|
| 785 |
mem_defs); |
|
| 748 | 786 |
(* if all mem_defs have empty guards, we are done, return prefix, |
| 749 | 787 |
mem_defs expr. |
| 750 | 788 |
|
| ... | ... | |
| 755 | 793 |
if List.for_all (fun (m,mdefs) -> |
| 756 | 794 |
(* All defs are unguarded *) |
| 757 | 795 |
match mdefs with |
| 758 |
| [[], _] -> true |
|
| 796 |
| [[], _] -> true (* Regular unguarded expression *) |
|
| 797 |
| [] -> true (* A unbalanced definition of the memory. Here |
|
| 798 |
we have m_{k+1} -> m_k *)
|
|
| 759 | 799 |
| _ -> false |
| 760 | 800 |
) mem_defs |
| 761 | 801 |
then |
| ... | ... | |
| 769 | 809 |
| _ -> assert false (* No IsInit expression *) |
| 770 | 810 |
in |
| 771 | 811 |
m,e |
| 812 |
| [] -> m, Corelang.expr_of_ident m Location.dummy_loc |
|
| 772 | 813 |
| _ -> assert false |
| 773 | 814 |
) mem_defs] |
| 774 | 815 |
else |
| 775 | 816 |
(* Picking a guard *) |
| 776 | 817 |
let elem_opt : expr option = pick_guard mem_defs in |
| 777 | 818 |
match elem_opt with |
| 778 |
None -> assert false (* Otherwise the first case should have matched *) |
|
| 819 |
None -> ( |
|
| 820 |
Format.eprintf "Issues picking guard in mem_defs: %a@." pp_all_defs mem_defs; |
|
| 821 |
assert false (* Otherwise the first case should have matched *) |
|
| 822 |
) |
|
| 779 | 823 |
| Some elem -> ( |
| 780 | 824 |
report ~level:4 (fun fmt -> Format.fprintf fmt "selecting guard %a@." Printers.pp_expr elem); |
| 781 | 825 |
let pos, neg = |
Also available in: Unified diff
[seal] delt with Merge and when
[printer] more kind2 syntax