lustrec / src / tools / seal_verifier.ml @ 0d79d0f3
History | View | Annotate | Download (2.49 KB)
1 | 0d79d0f3 | ploc | open Seal_slice |
---|---|---|---|
2 | open Seal_extract |
||
3 | a703ed0c | ploc | open Seal_utils |
4 | |||
5 | ad4774b0 | ploc | let active = ref false |
6 | |||
7 | a703ed0c | ploc | (* Select the appropriate node, should have been inlined already and |
8 | extract update/output functions. *) |
||
9 | let seal_run basename prog machines = |
||
10 | let node_name = |
||
11 | match !Options.main_node with |
||
12 | 0d79d0f3 | ploc | | "" -> ( |
13 | Format.eprintf "SEAL verifier requires a main node.@."; |
||
14 | Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?" |
||
15 | (Utils.fprintf_list ~sep:"@ " |
||
16 | (fun fmt m -> |
||
17 | Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id |
||
18 | ) |
||
19 | ) |
||
20 | machines; |
||
21 | exit 1 |
||
22 | ) |
||
23 | a703ed0c | ploc | | s -> s |
24 | in |
||
25 | let m = Machine_code_common.get_machine machines node_name in |
||
26 | let nd = m.mname in |
||
27 | a742719e | ploc | (* Format.eprintf "Node %a@." Printers.pp_node nd; *) |
28 | a703ed0c | ploc | let mems = m.mmemory in |
29 | a742719e | ploc | (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *) |
30 | a703ed0c | ploc | let msch = Utils.desome m.msch in |
31 | a742719e | ploc | (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *) |
32 | let sliced_nd = slice_node mems msch nd in |
||
33 | (* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *) |
||
34 | 0d79d0f3 | ploc | report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@."); |
35 | a742719e | ploc | let sw_init, sw_sys = node_as_switched_sys mems sliced_nd in |
36 | let pp_res = |
||
37 | (Utils.fprintf_list ~sep:"@ " |
||
38 | (fun fmt (gel, up) -> |
||
39 | 0d79d0f3 | ploc | Format.fprintf fmt "@[<v 2>[%a]:@ %a@]" |
40 | a742719e | ploc | (Utils.fprintf_list ~sep:"; " |
41 | (fun fmt (e,b) -> |
||
42 | if b then Printers.pp_expr fmt e |
||
43 | else Format.fprintf fmt "not(%a)" |
||
44 | Printers.pp_expr e)) gel |
||
45 | 0d79d0f3 | ploc | (Utils.fprintf_list ~sep:";@ " |
46 | a742719e | ploc | (fun fmt (id, e) -> |
47 | 0d79d0f3 | ploc | Format.fprintf fmt "%s = @[<hov 0>%a@]" |
48 | a742719e | ploc | id |
49 | Printers.pp_expr e)) up |
||
50 | )) |
||
51 | in |
||
52 | 0d79d0f3 | ploc | report ~level:1 ( |
53 | fun fmt -> Format.fprintf fmt |
||
54 | "%i memories, %i init, %i step switch cases@." |
||
55 | (List.length mems) |
||
56 | (List.length sw_init) |
||
57 | (List.length sw_sys) |
||
58 | |||
59 | ); |
||
60 | a742719e | ploc | report ~level:1 (fun fmt -> |
61 | Format.fprintf fmt "@[<v 0>@[<v 3>Init:@ %a@]@ " |
||
62 | pp_res sw_init; |
||
63 | Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ " |
||
64 | pp_res sw_sys |
||
65 | ); |
||
66 | |||
67 | |||
68 | a703ed0c | ploc | () |
69 | |||
70 | ad4774b0 | ploc | module Verifier = |
71 | (struct |
||
72 | include VerifierType.Default |
||
73 | let name = "seal" |
||
74 | let options = [] |
||
75 | a703ed0c | ploc | let activate () = |
76 | active := true; |
||
77 | Options.global_inline := true |
||
78 | |||
79 | ad4774b0 | ploc | let is_active () = !active |
80 | a703ed0c | ploc | let run = seal_run |
81 | |||
82 | ad4774b0 | ploc | |
83 | end: VerifierType.S) |
||
84 |