Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_verifier.ml @ 04a188ec

History | View | Annotate | Download (5.62 KB)

1
open Seal_slice
2
open Seal_extract
3
open Seal_utils
4

    
5
let active = ref false
6
let seal_export = ref None
7

    
8
let set_export s = match s with
9
  | "lustre" | "lus" | "m" | "matlab" -> seal_export := Some s
10
  | _ -> (Format.eprintf "Unrecognized seal export: %s@.@?" s; exit 1)
11
(* TODO
12

    
13
   - build the output function: for the moment we slice the node with
14
   its memories, building the function updating the memory. We will
15
   need later the output function, using inputs and memories to
16
   compute the output. A way to do this would be to declared memories
17
   as input, remove their definitions, and slice the node with its
18
   outputs. This should clean up unnecessary internal variables and
19
   give us the output function.
20

    
21
   - compute the dimension of the node (nb of memories)
22

    
23
   - if the updates are all linear or affine, provide the update as a
24
   matrix rather then a polynomial. Check if this is simpler to do
25
   here or in matlab.
26

    
27
   - analyzes require bounds on inputs or sometimes target property 
28
   over states. These could be specified as node annotations: eg     
29
     - /seal/bounds/inputs/semialg/: (in1^4 + in2^3, 1) 
30
       to specify that the inputs are constrained by a semialgebraic 
31
       set (p,b) such as p(inputs) <= b
32
     - /seal/bounds/inputs/LMI/: (todo_describe_a_matrix) .... and so on. 
33
       To be defined depending on needs.
34
     - /seal/prop/semialg/: (x3 - x5, 2) -- if x3 - x5 <= 2 is 
35
       the property to prove
36
     
37
 *)
38
           
39
(* Select the appropriate node, should have been inlined already and
40
   extract 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:"@ "
48
           (fun fmt m ->
49
             Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id
50
           )
51
        )
52
        machines; 
53
      exit 1
54
    )
55
    | s -> ( (* should have been addessed before *)
56
      match Machine_code_common.get_machine_opt machines s with
57
      | None -> begin
58
          Global.main_node := s;
59
          Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
60
          raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
61
        end
62
      | Some _ -> s
63
    )
64
  in
65
  let m = Machine_code_common.get_machine machines node_name in
66
  let nd = m.mname in
67
  (* Format.eprintf "Node %a@." Printers.pp_node nd; *)
68
  let mems = m.mmemory in
69
  report ~level:1 (fun fmt -> Format.fprintf fmt "Node %s compiled: %i memories@." nd.node_id (List.length mems));
70
  (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *)
71
  let msch = Utils.desome m.msch in
72
  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)
73
  let sliced_nd = slice_node (mems@nd.node_outputs) msch nd in
74
  if false then Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd;
75
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
76

    
77
  let consts = Corelang.(List.map const_of_top (get_consts prog)) in
78
  let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in
79
  let pp_res pp_expr =
80
    (Utils.fprintf_list ~sep:"@ "
81
       (fun fmt (g, up) ->
82
         Format.fprintf fmt "@[<v 2>[%t]:@ %a@]"
83
           (fun fmt -> match g with None -> () | Some g -> pp_expr fmt g)
84
           
85
           (* (Utils.fprintf_list ~sep:"; "
86
            *    (fun fmt (e,b) ->
87
            *      if b then pp_expr fmt e
88
            *      else Format.fprintf fmt "not(%a)"
89
            *             pp_expr e)) gel *)
90
           (Utils.fprintf_list ~sep:";@ "
91
              (fun fmt (id, e) ->
92
                Format.fprintf fmt "%s = @[<hov 0>%a@]"
93
                  id
94
                  pp_expr e)) up
95
    ))
96
  in
97
  report ~level:1 (
98
      fun fmt -> Format.fprintf fmt
99
                   "%i memories, %i init, %i step switch cases@."
100
                   (List.length mems)
101
                   (List.length sw_init)
102
                   (List.length sw_sys)
103
               
104
    );
105
  report ~level:1 (fun fmt ->
106
      (*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag)  in*)
107
       let pp_res = pp_res Printers.pp_expr in
108
      Format.fprintf fmt "DynSys:@ @[<v 0>@[<v 3>Init:@ %a@]@ "
109
        pp_res  sw_init;
110
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@."
111
        pp_res  sw_sys
112
    );
113

    
114

    
115
                
116
 report ~level:1 (fun fmt ->
117
      (*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag)  in*)
118
       let pp_res = pp_res Printers.pp_expr in
119
      Format.fprintf fmt "Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ "
120
             (List.length init_out)
121
                   (List.length update_out)
122
                   pp_res  init_out;
123
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@."
124
        pp_res  update_out
125
    );
126
  let _ = match !seal_export with
127
    | Some "lustre" | Some "lus" ->
128
       Seal_export.to_lustre basename prog m sw_init sw_sys init_out update_out  
129
    | Some "matlab" | Some "m" -> assert false (* TODO *)
130
    | Some _ -> assert false 
131
    | None -> ()
132
  in
133
  ()
134
  
135
module Verifier =
136
  (struct
137
    include VerifierType.Default
138
    let name = "seal"
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
    let run = seal_run
154
      
155
                    
156
  end: VerifierType.S)
157