Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

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