1
|
(* TODO
|
2
|
|
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.
|
9
|
|
10
|
- compute the dimension of the node (nb of memories)
|
11
|
|
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.
|
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 *)
|
22
|
|
23
|
open Seal_slice
|
24
|
open Seal_extract
|
25
|
open Seal_utils
|
26
|
|
27
|
let active = ref false
|
28
|
|
29
|
let seal_export = ref None
|
30
|
|
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. *)
|
41
|
let seal_run ~basename prog machines =
|
42
|
let node_name =
|
43
|
match !Options.main_node with
|
44
|
| "" ->
|
45
|
Format.eprintf "SEAL verifier requires a main node.@.";
|
46
|
Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
|
47
|
(Utils.fprintf_list ~sep:"@ " (fun fmt m ->
|
48
|
Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id))
|
49
|
machines;
|
50
|
exit 1
|
51
|
| s -> (
|
52
|
(* should have been addessed before *)
|
53
|
match Machine_code_common.get_machine_opt machines s with
|
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)
|
61
|
in
|
62
|
let m = Machine_code_common.get_machine machines node_name in
|
63
|
let nd = m.mname in
|
64
|
let mems = m.mmemory in
|
65
|
|
66
|
report ~level:1 (fun fmt ->
|
67
|
Format.fprintf fmt "Node %s compiled: %i memories@." nd.node_id
|
68
|
(List.length mems));
|
69
|
|
70
|
(* Slicing node *)
|
71
|
let msch = Utils.desome m.msch in
|
72
|
let sliced_nd = slice_node (mems @ nd.node_outputs) msch nd in
|
73
|
report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
|
74
|
report ~level:10 (fun fmt ->
|
75
|
Format.fprintf fmt "Sliced Node %a@." Printers.pp_node sliced_nd);
|
76
|
|
77
|
let consts = Corelang.(List.map const_of_top (get_consts prog)) in
|
78
|
|
79
|
let pp_sys = pp_sys Printers.pp_expr in
|
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
|
())
|
100
|
else
|
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
|
|
157
|
let () =
|
158
|
VerifierList.registered :=
|
159
|
(module Verifier : VerifierType.S) :: !VerifierList.registered
|