Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_verifier.ml @ a0c92fa8

History | View | Annotate | Download (5.18 KB)

1 d5ec9f63 ploc
(* TODO
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.
10
11
   - compute the dimension of the node (nb of memories)
12
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
 *)
28 a0c92fa8 ploc
29
30
open Seal_slice
31
open Seal_extract
32
open Seal_utils
33
34
let active = ref false
35
let seal_export = ref None
36
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 d5ec9f63 ploc
           
41 a703ed0c ploc
(* Select the appropriate node, should have been inlined already and
42
   extract update/output functions. *)
43 7a4fd94d ploc
let seal_run ~basename prog machines =
44 a703ed0c ploc
  let node_name =
45
    match !Options.main_node with
46 0d79d0f3 ploc
    | "" -> (
47
      Format.eprintf "SEAL verifier requires a main node.@.";
48
      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; 
55
      exit 1
56
    )
57 efc2cd2f ploc
    | s -> ( (* should have been addessed before *)
58
      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 04a188ec ploc
          raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
63 efc2cd2f ploc
        end
64
      | Some _ -> s
65
    )
66 a703ed0c ploc
  in
67
  let m = Machine_code_common.get_machine machines node_name in
68
  let nd = m.mname in
69
  let mems = m.mmemory in
70 a0c92fa8 ploc
71 04a188ec ploc
  report ~level:1 (fun fmt -> Format.fprintf fmt "Node %s compiled: %i memories@." nd.node_id (List.length mems));
72 a0c92fa8 ploc
73
  (* Slicing node *)
74 a703ed0c ploc
  let msch = Utils.desome m.msch in
75 25320f03 ploc
  let sliced_nd = slice_node (mems@nd.node_outputs) msch nd in
76 0d79d0f3 ploc
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
77 a0c92fa8 ploc
  report ~level:10 (fun fmt -> Format.fprintf fmt "Sliced Node %a@." Printers.pp_node sliced_nd);
78 8c934ccd ploc
79
  let consts = Corelang.(List.map const_of_top (get_consts prog)) in
80 a0c92fa8 ploc
81
  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
103
  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 a703ed0c ploc
  
137 ad4774b0 ploc
module Verifier =
138
  (struct
139
    include VerifierType.Default
140
    let name = "seal"
141 03c767b1 ploc
    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 a703ed0c ploc
    let activate () =
148
      active := true;
149 efc2cd2f ploc
      Options.global_inline := true;
150
      Options.optimization := 0;
151
      Options.const_unfold := true;
152
      ()
153 a703ed0c ploc
      
154 ad4774b0 ploc
    let is_active () = !active
155 a703ed0c ploc
    let run = seal_run
156 a0c92fa8 ploc
            
157
            
158 ad4774b0 ploc
  end: VerifierType.S)
159