lustrec / src / tools / seal / seal_verifier.ml @ d75eb6f1
History | View | Annotate | Download (4.11 KB)
1 |
open Seal_slice |
---|---|
2 |
open Seal_extract |
3 |
open Seal_utils |
4 |
|
5 |
let active = ref false |
6 |
|
7 |
(* TODO |
8 |
|
9 |
- build the output function: for the moment we slice the node with |
10 |
its memories, building the function updating the memory. We will |
11 |
need later the output function, using inputs and memories to |
12 |
compute the output. A way to do this would be to declared memories |
13 |
as input, remove their definitions, and slice the node with its |
14 |
outputs. This should clean up unnecessary internal variables and |
15 |
give us the output function. |
16 |
|
17 |
- compute the dimension of the node (nb of memories) |
18 |
|
19 |
- if the updates are all linear or affine, provide the update as a |
20 |
matrix rather then a polynomial. Check if this is simpler to do |
21 |
here or in matlab. |
22 |
|
23 |
- analyzes require bounds on inputs or sometimes target property |
24 |
over states. These could be specified as node annotations: eg |
25 |
- /seal/bounds/inputs/semialg/: (in1^4 + in2^3, 1) |
26 |
to specify that the inputs are constrained by a semialgebraic |
27 |
set (p,b) such as p(inputs) <= b |
28 |
- /seal/bounds/inputs/LMI/: (todo_describe_a_matrix) .... and so on. |
29 |
To be defined depending on needs. |
30 |
- /seal/prop/semialg/: (x3 - x5, 2) -- if x3 - x5 <= 2 is |
31 |
the property to prove |
32 |
|
33 |
*) |
34 |
|
35 |
(* Select the appropriate node, should have been inlined already and |
36 |
extract update/output functions. *) |
37 |
let seal_run basename prog machines = |
38 |
let node_name = |
39 |
match !Options.main_node with |
40 |
| "" -> ( |
41 |
Format.eprintf "SEAL verifier requires a main node.@."; |
42 |
Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?" |
43 |
(Utils.fprintf_list ~sep:"@ " |
44 |
(fun fmt m -> |
45 |
Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id |
46 |
) |
47 |
) |
48 |
machines; |
49 |
exit 1 |
50 |
) |
51 |
| s -> s |
52 |
in |
53 |
let m = Machine_code_common.get_machine machines node_name in |
54 |
let nd = m.mname in |
55 |
(* Format.eprintf "Node %a@." Printers.pp_node nd; *) |
56 |
let mems = m.mmemory in |
57 |
(* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *) |
58 |
let msch = Utils.desome m.msch in |
59 |
(* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *) |
60 |
let sliced_nd = slice_node mems msch nd in |
61 |
(* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *) |
62 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@."); |
63 |
|
64 |
let consts = Corelang.(List.map const_of_top (get_consts prog)) in |
65 |
let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in |
66 |
let pp_res pp_expr = |
67 |
(Utils.fprintf_list ~sep:"@ " |
68 |
(fun fmt (g, up) -> |
69 |
Format.fprintf fmt "@[<v 2>[%t]:@ %a@]" |
70 |
(fun fmt -> match g with None -> () | Some g -> pp_expr fmt g) |
71 |
|
72 |
(* (Utils.fprintf_list ~sep:"; " |
73 |
* (fun fmt (e,b) -> |
74 |
* if b then pp_expr fmt e |
75 |
* else Format.fprintf fmt "not(%a)" |
76 |
* pp_expr e)) gel *) |
77 |
(Utils.fprintf_list ~sep:";@ " |
78 |
(fun fmt (id, e) -> |
79 |
Format.fprintf fmt "%s = @[<hov 0>%a@]" |
80 |
id |
81 |
pp_expr e)) up |
82 |
)) |
83 |
in |
84 |
report ~level:1 ( |
85 |
fun fmt -> Format.fprintf fmt |
86 |
"%i memories, %i init, %i step switch cases@." |
87 |
(List.length mems) |
88 |
(List.length sw_init) |
89 |
(List.length sw_sys) |
90 |
|
91 |
); |
92 |
report ~level:1 (fun fmt -> |
93 |
(*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) in*) |
94 |
let pp_res = pp_res Printers.pp_expr in |
95 |
Format.fprintf fmt "@[<v 0>@[<v 3>Init:@ %a@]@ " |
96 |
pp_res sw_init; |
97 |
Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ " |
98 |
pp_res sw_sys |
99 |
); |
100 |
let new_node = Seal_export.to_lustre m sw_init sw_sys init_out update_out in |
101 |
Format.eprintf "%a@." Printers.pp_node new_node; |
102 |
() |
103 |
|
104 |
module Verifier = |
105 |
(struct |
106 |
include VerifierType.Default |
107 |
let name = "seal" |
108 |
let options = [] |
109 |
let activate () = |
110 |
active := true; |
111 |
Options.global_inline := true |
112 |
|
113 |
let is_active () = !active |
114 |
let run = seal_run |
115 |
|
116 |
|
117 |
end: VerifierType.S) |
118 |
|