Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/seal/seal_verifier.ml | ||
---|---|---|
1 | 1 |
(* TODO |
2 | 2 |
|
3 |
- build the output function: for the moment we slice the node with |
|
4 |
its memories, building the function updating the memory. We will |
|
5 |
need later the output function, using inputs and memories to |
|
6 |
compute the output. A way to do this would be to declared memories |
|
7 |
as input, remove their definitions, and slice the node with its |
|
8 |
outputs. This should clean up unnecessary internal variables and |
|
9 |
give us the output function. |
|
3 |
- build the output function: for the moment we slice the node with its |
|
4 |
memories, building the function updating the memory. We will need later the |
|
5 |
output function, using inputs and memories to compute the output. A way to do |
|
6 |
this would be to declared memories as input, remove their definitions, and |
|
7 |
slice the node with its outputs. This should clean up unnecessary internal |
|
8 |
variables and give us the output function. |
|
10 | 9 |
|
11 | 10 |
- compute the dimension of the node (nb of memories) |
12 | 11 |
|
13 |
- if the updates are all linear or affine, provide the update as a |
|
14 |
matrix rather then a polynomial. Check if this is simpler to do |
|
15 |
here or in matlab. |
|
16 |
|
|
17 |
- analyzes require bounds on inputs or sometimes target property |
|
18 |
over states. These could be specified as node annotations: eg |
|
19 |
- /seal/bounds/inputs/semialg/: (in1^4 + in2^3, 1) |
|
20 |
to specify that the inputs are constrained by a semialgebraic |
|
21 |
set (p,b) such as p(inputs) <= b |
|
22 |
- /seal/bounds/inputs/LMI/: (todo_describe_a_matrix) .... and so on. |
|
23 |
To be defined depending on needs. |
|
24 |
- /seal/prop/semialg/: (x3 - x5, 2) -- if x3 - x5 <= 2 is |
|
25 |
the property to prove |
|
26 |
|
|
27 |
*) |
|
12 |
- if the updates are all linear or affine, provide the update as a matrix |
|
13 |
rather then a polynomial. Check if this is simpler to do here or in matlab. |
|
28 | 14 |
|
15 |
- analyzes require bounds on inputs or sometimes target property over states. |
|
16 |
These could be specified as node annotations: eg - |
|
17 |
/seal/bounds/inputs/semialg/: (in1^4 + in2^3, 1) to specify that the inputs |
|
18 |
are constrained by a semialgebraic set (p,b) such as p(inputs) <= b - |
|
19 |
/seal/bounds/inputs/LMI/: (todo_describe_a_matrix) .... and so on. To be |
|
20 |
defined depending on needs. - /seal/prop/semialg/: (x3 - x5, 2) -- if x3 - x5 |
|
21 |
<= 2 is the property to prove *) |
|
29 | 22 |
|
30 | 23 |
open Seal_slice |
31 | 24 |
open Seal_extract |
32 | 25 |
open Seal_utils |
33 | 26 |
|
34 | 27 |
let active = ref false |
28 |
|
|
35 | 29 |
let seal_export = ref None |
36 | 30 |
|
37 |
let set_export s = match s with |
|
38 |
| "lustre" | "lus" | "m" | "matlab" -> seal_export := Some s |
|
39 |
| _ -> (Format.eprintf "Unrecognized seal export: %s@.@?" s; exit 1) |
|
40 |
|
|
41 |
(* Select the appropriate node, should have been inlined already and |
|
42 |
extract update/output functions. *) |
|
31 |
let set_export s = |
|
32 |
match s with |
|
33 |
| "lustre" | "lus" | "m" | "matlab" -> |
|
34 |
seal_export := Some s |
|
35 |
| _ -> |
|
36 |
Format.eprintf "Unrecognized seal export: %s@.@?" s; |
|
37 |
exit 1 |
|
38 |
|
|
39 |
(* Select the appropriate node, should have been inlined already and extract |
|
40 |
update/output functions. *) |
|
43 | 41 |
let seal_run ~basename prog machines = |
44 | 42 |
let node_name = |
45 | 43 |
match !Options.main_node with |
46 |
| "" -> (
|
|
44 |
| "" -> |
|
47 | 45 |
Format.eprintf "SEAL verifier requires a main node.@."; |
48 | 46 |
Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?" |
49 |
(Utils.fprintf_list ~sep:"@ " |
|
50 |
(fun fmt m -> |
|
51 |
Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id |
|
52 |
) |
|
53 |
) |
|
54 |
machines; |
|
47 |
(Utils.fprintf_list ~sep:"@ " (fun fmt m -> |
|
48 |
Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id)) |
|
49 |
machines; |
|
55 | 50 |
exit 1 |
56 |
)
|
|
57 |
| s -> ( (* should have been addessed before *)
|
|
51 |
| s -> (
|
|
52 |
(* should have been addessed before *)
|
|
58 | 53 |
match Machine_code_common.get_machine_opt machines s with |
59 |
| None -> begin
|
|
60 |
Global.main_node := s;
|
|
61 |
Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
|
|
62 |
raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
|
|
63 |
end
|
|
64 |
| Some _ -> s
|
|
65 |
) |
|
54 |
| None -> |
|
55 |
Global.main_node := s; |
|
56 |
Format.eprintf "Code generation error: %a@." Error.pp_error_msg
|
|
57 |
Error.Main_not_found;
|
|
58 |
raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
|
|
59 |
| Some _ -> |
|
60 |
s)
|
|
66 | 61 |
in |
67 | 62 |
let m = Machine_code_common.get_machine machines node_name in |
68 | 63 |
let nd = m.mname in |
69 | 64 |
let mems = m.mmemory in |
70 | 65 |
|
71 |
report ~level:1 (fun fmt -> Format.fprintf fmt "Node %s compiled: %i memories@." nd.node_id (List.length mems)); |
|
66 |
report ~level:1 (fun fmt -> |
|
67 |
Format.fprintf fmt "Node %s compiled: %i memories@." nd.node_id |
|
68 |
(List.length mems)); |
|
72 | 69 |
|
73 | 70 |
(* Slicing node *) |
74 | 71 |
let msch = Utils.desome m.msch in |
75 |
let sliced_nd = slice_node (mems@nd.node_outputs) msch nd in
|
|
72 |
let sliced_nd = slice_node (mems @ nd.node_outputs) msch nd in
|
|
76 | 73 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@."); |
77 |
report ~level:10 (fun fmt -> Format.fprintf fmt "Sliced Node %a@." Printers.pp_node sliced_nd); |
|
74 |
report ~level:10 (fun fmt -> |
|
75 |
Format.fprintf fmt "Sliced Node %a@." Printers.pp_node sliced_nd); |
|
78 | 76 |
|
79 | 77 |
let consts = Corelang.(List.map const_of_top (get_consts prog)) in |
80 | 78 |
|
81 | 79 |
let pp_sys = pp_sys Printers.pp_expr in |
82 |
if List.length mems = 0 then |
|
83 |
begin (* A stateless node = a function ! *) |
|
84 |
|
|
85 |
let update_out = fun_as_switched_sys consts sliced_nd in |
|
86 |
|
|
87 |
report ~level:1 (fun fmt -> |
|
88 |
Format.fprintf fmt |
|
89 |
"Output (%i step switch cases):@ @[<v 0>%a@]@." |
|
90 |
(List.length update_out) |
|
91 |
pp_sys update_out |
|
92 |
); |
|
93 |
|
|
94 |
let _ = match !seal_export with |
|
95 |
| Some "lustre" | Some "lus" -> |
|
96 |
Seal_export.fun_to_lustre basename prog m update_out |
|
97 |
| Some "matlab" | Some "m" -> assert false (* TODO *) |
|
98 |
| Some _ -> assert false |
|
99 |
| None -> () |
|
100 |
in |
|
101 |
() |
|
102 |
end |
|
80 |
if List.length mems = 0 then ( |
|
81 |
(* A stateless node = a function ! *) |
|
82 |
let update_out = fun_as_switched_sys consts sliced_nd in |
|
83 |
|
|
84 |
report ~level:1 (fun fmt -> |
|
85 |
Format.fprintf fmt "Output (%i step switch cases):@ @[<v 0>%a@]@." |
|
86 |
(List.length update_out) pp_sys update_out); |
|
87 |
|
|
88 |
let _ = |
|
89 |
match !seal_export with |
|
90 |
| Some "lustre" | Some "lus" -> |
|
91 |
Seal_export.fun_to_lustre basename prog m update_out |
|
92 |
| Some "matlab" | Some "m" -> |
|
93 |
assert false (* TODO *) |
|
94 |
| Some _ -> |
|
95 |
assert false |
|
96 |
| None -> |
|
97 |
() |
|
98 |
in |
|
99 |
()) |
|
103 | 100 |
else |
104 |
begin (* A stateful node *)
|
|
105 |
|
|
106 |
let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in
|
|
107 |
|
|
108 |
report ~level:1 (fun fmt -> |
|
109 |
Format.fprintf fmt
|
|
110 |
"DynSys: (%i memories, %i init, %i step switch cases)@ @[<v 0>@[<v 3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@."
|
|
111 |
(List.length mems)
|
|
112 |
(List.length sw_init)
|
|
113 |
(List.length sw_sys)
|
|
114 |
pp_sys sw_init
|
|
115 |
pp_sys sw_sys |
|
116 |
);
|
|
117 |
|
|
118 |
report ~level:1 (fun fmt ->
|
|
119 |
Format.fprintf fmt
|
|
120 |
"Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@."
|
|
121 |
(List.length init_out)
|
|
122 |
(List.length update_out) |
|
123 |
pp_sys init_out
|
|
124 |
pp_sys update_out
|
|
125 |
);
|
|
126 |
|
|
127 |
let _ = match !seal_export with
|
|
128 |
| Some "lustre" | Some "lus" ->
|
|
129 |
Seal_export.node_to_lustre basename prog m sw_init sw_sys init_out update_out
|
|
130 |
| Some "matlab" | Some "m" -> assert false (* TODO *)
|
|
131 |
| Some _ -> assert false
|
|
132 |
| None -> ()
|
|
133 |
in
|
|
134 |
()
|
|
135 |
end
|
|
136 |
|
|
137 |
module Verifier =
|
|
138 |
(struct
|
|
139 |
include VerifierType.Default |
|
140 |
let name = "seal"
|
|
141 |
let options = |
|
142 |
[
|
|
143 |
"-export", Arg.String set_export, "seal export option (lustre, matlab)";
|
|
144 |
"-debug", Arg.Set seal_debug, "seal debug"
|
|
145 |
|
|
146 |
]
|
|
147 |
let activate () = |
|
148 |
active := true;
|
|
149 |
Options.global_inline := true;
|
|
150 |
Options.optimization := 0;
|
|
151 |
Options.const_unfold := true;
|
|
152 |
()
|
|
153 |
|
|
154 |
let is_active () = !active |
|
155 |
let run = seal_run
|
|
156 |
|
|
157 |
|
|
158 |
end: VerifierType.S)
|
|
159 |
|
|
101 |
(* A stateful node *) |
|
102 |
let sw_init, sw_sys, init_out, update_out = |
|
103 |
node_as_switched_sys consts mems sliced_nd
|
|
104 |
in |
|
105 |
|
|
106 |
report ~level:1 (fun fmt ->
|
|
107 |
Format.fprintf fmt
|
|
108 |
"DynSys: (%i memories, %i init, %i step switch cases)@ @[<v 0>@[<v \
|
|
109 |
3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@."
|
|
110 |
(List.length mems) (List.length sw_init) (List.length sw_sys) pp_sys
|
|
111 |
sw_init pp_sys sw_sys);
|
|
112 |
|
|
113 |
report ~level:1 (fun fmt ->
|
|
114 |
Format.fprintf fmt |
|
115 |
"Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ \
|
|
116 |
@[<v 3>Step:@ %a@]@]@."
|
|
117 |
(List.length init_out) (List.length update_out) pp_sys init_out pp_sys
|
|
118 |
update_out);
|
|
119 |
|
|
120 |
let _ =
|
|
121 |
match !seal_export with
|
|
122 |
| Some "lustre" | Some "lus" ->
|
|
123 |
Seal_export.node_to_lustre basename prog m sw_init sw_sys init_out |
|
124 |
update_out
|
|
125 |
| Some "matlab" | Some "m" ->
|
|
126 |
assert false (* TODO *)
|
|
127 |
| Some _ ->
|
|
128 |
assert false
|
|
129 |
| None ->
|
|
130 |
()
|
|
131 |
in
|
|
132 |
()
|
|
133 |
|
|
134 |
module Verifier : VerifierType.S = struct
|
|
135 |
include VerifierType.Default
|
|
136 |
|
|
137 |
let name = "seal" |
|
138 |
|
|
139 |
let options =
|
|
140 |
[
|
|
141 |
"-export", Arg.String set_export, "seal export option (lustre, matlab)";
|
|
142 |
"-debug", Arg.Set seal_debug, "seal debug"; |
|
143 |
] |
|
144 |
|
|
145 |
let activate () =
|
|
146 |
active := true;
|
|
147 |
Options.global_inline := true;
|
|
148 |
Options.optimization := 0;
|
|
149 |
Options.const_unfold := true;
|
|
150 |
() |
|
151 |
|
|
152 |
let is_active () = !active
|
|
153 |
|
|
154 |
let run = seal_run |
|
155 |
end
|
|
156 |
|
|
160 | 157 |
let () = |
161 |
VerifierList.registered := (module Verifier : VerifierType.S) :: |
|
162 |
!VerifierList.registered |
|
158 |
VerifierList.registered := |
|
159 |
(module Verifier : VerifierType.S) :: !VerifierList.registered |
Also available in: Unified diff
reformatting