Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_verifier.ml @ 03c767b1

History | View | Annotate | Download (4.57 KB)

1 0d79d0f3 ploc
open Seal_slice
2
open Seal_extract
3 a703ed0c ploc
open Seal_utils
4
5 ad4774b0 ploc
let active = ref false
6 518951ed ploc
let seal_export = ref None
7 ad4774b0 ploc
8 518951ed ploc
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 d5ec9f63 ploc
(* 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 a703ed0c ploc
(* Select the appropriate node, should have been inlined already and
40
   extract update/output functions. *)
41 7a4fd94d ploc
let seal_run ~basename prog machines =
42 a703ed0c ploc
  let node_name =
43
    match !Options.main_node with
44 0d79d0f3 ploc
    | "" -> (
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 a703ed0c ploc
    | s -> s
56
  in
57
  let m = Machine_code_common.get_machine machines node_name in
58
  let nd = m.mname in
59 a742719e ploc
  (* Format.eprintf "Node %a@." Printers.pp_node nd; *)
60 a703ed0c ploc
  let mems = m.mmemory in
61 a742719e ploc
  (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *)
62 a703ed0c ploc
  let msch = Utils.desome m.msch in
63 a742719e ploc
  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)
64
  let sliced_nd = slice_node mems msch nd in
65
  (* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *)
66 0d79d0f3 ploc
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
67 8c934ccd ploc
68
  let consts = Corelang.(List.map const_of_top (get_consts prog)) in
69 d75eb6f1 ploc
  let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in
70 81229f63 ploc
  let pp_res pp_expr =
71 a742719e ploc
    (Utils.fprintf_list ~sep:"@ "
72 81229f63 ploc
       (fun fmt (g, up) ->
73
         Format.fprintf fmt "@[<v 2>[%t]:@ %a@]"
74
           (fun fmt -> match g with None -> () | Some g -> pp_expr fmt g)
75
           
76
           (* (Utils.fprintf_list ~sep:"; "
77
            *    (fun fmt (e,b) ->
78
            *      if b then pp_expr fmt e
79
            *      else Format.fprintf fmt "not(%a)"
80
            *             pp_expr e)) gel *)
81 0d79d0f3 ploc
           (Utils.fprintf_list ~sep:";@ "
82 a742719e ploc
              (fun fmt (id, e) ->
83 0d79d0f3 ploc
                Format.fprintf fmt "%s = @[<hov 0>%a@]"
84 a742719e ploc
                  id
85 81229f63 ploc
                  pp_expr e)) up
86 a742719e ploc
    ))
87
  in
88 0d79d0f3 ploc
  report ~level:1 (
89
      fun fmt -> Format.fprintf fmt
90
                   "%i memories, %i init, %i step switch cases@."
91
                   (List.length mems)
92
                   (List.length sw_init)
93
                   (List.length sw_sys)
94
               
95
    );
96 a742719e ploc
  report ~level:1 (fun fmt ->
97 81229f63 ploc
      (*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag)  in*)
98
       let pp_res = pp_res Printers.pp_expr in
99 a742719e ploc
      Format.fprintf fmt "@[<v 0>@[<v 3>Init:@ %a@]@ "
100 81229f63 ploc
        pp_res  sw_init;
101 a742719e ploc
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "
102 81229f63 ploc
        pp_res  sw_sys
103 a742719e ploc
    );
104 518951ed ploc
  let _ = match !seal_export with
105
    | Some "lustre" | Some "lus" ->
106
       Seal_export.to_lustre basename prog m sw_init sw_sys init_out update_out  
107
    | Some "matlab" | Some "m" -> assert false (* TODO *)
108
    | Some _ -> assert false 
109
    | None -> ()
110
  in
111 a703ed0c ploc
  ()
112
  
113 ad4774b0 ploc
module Verifier =
114
  (struct
115
    include VerifierType.Default
116
    let name = "seal"
117 03c767b1 ploc
    let options =
118
      [
119
        "-export", Arg.String set_export, "seal export option (lustre, matlab)";
120
        "-debug", Arg.Set seal_debug, "seal debug"
121
122
      ]
123 a703ed0c ploc
    let activate () =
124
      active := true;
125
      Options.global_inline := true
126
      
127 ad4774b0 ploc
    let is_active () = !active
128 a703ed0c ploc
    let run = seal_run
129
      
130 ad4774b0 ploc
                    
131
  end: VerifierType.S)
132