### Profile

« Previous | Next »

## Revision ca7ff3f7

reformatting

View differences:

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