Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (4.11 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
7 d5ec9f63 ploc
(* TODO
8
9
   - build the output function: for the moment we slice the node with
10
   its memories, building the function updating the memory. We will
11
   need later the output function, using inputs and memories to
12
   compute the output. A way to do this would be to declared memories
13
   as input, remove their definitions, and slice the node with its
14
   outputs. This should clean up unnecessary internal variables and
15
   give us the output function.
16
17
   - compute the dimension of the node (nb of memories)
18
19
   - if the updates are all linear or affine, provide the update as a
20
   matrix rather then a polynomial. Check if this is simpler to do
21
   here or in matlab.
22
23
   - analyzes require bounds on inputs or sometimes target property 
24
   over states. These could be specified as node annotations: eg     
25
     - /seal/bounds/inputs/semialg/: (in1^4 + in2^3, 1) 
26
       to specify that the inputs are constrained by a semialgebraic 
27
       set (p,b) such as p(inputs) <= b
28
     - /seal/bounds/inputs/LMI/: (todo_describe_a_matrix) .... and so on. 
29
       To be defined depending on needs.
30
     - /seal/prop/semialg/: (x3 - x5, 2) -- if x3 - x5 <= 2 is 
31
       the property to prove
32
     
33
 *)
34
           
35 a703ed0c ploc
(* Select the appropriate node, should have been inlined already and
36
   extract update/output functions. *)
37
let seal_run basename prog machines =
38
  let node_name =
39
    match !Options.main_node with
40 0d79d0f3 ploc
    | "" -> (
41
      Format.eprintf "SEAL verifier requires a main node.@.";
42
      Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
43
        (Utils.fprintf_list ~sep:"@ "
44
           (fun fmt m ->
45
             Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id
46
           )
47
        )
48
        machines; 
49
      exit 1
50
    )
51 a703ed0c ploc
    | s -> s
52
  in
53
  let m = Machine_code_common.get_machine machines node_name in
54
  let nd = m.mname in
55 a742719e ploc
  (* Format.eprintf "Node %a@." Printers.pp_node nd; *)
56 a703ed0c ploc
  let mems = m.mmemory in
57 a742719e ploc
  (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *)
58 a703ed0c ploc
  let msch = Utils.desome m.msch in
59 a742719e ploc
  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)
60
  let sliced_nd = slice_node mems msch nd in
61
  (* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *)
62 0d79d0f3 ploc
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
63 8c934ccd ploc
64
  let consts = Corelang.(List.map const_of_top (get_consts prog)) in
65 d75eb6f1 ploc
  let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in
66 81229f63 ploc
  let pp_res pp_expr =
67 a742719e ploc
    (Utils.fprintf_list ~sep:"@ "
68 81229f63 ploc
       (fun fmt (g, up) ->
69
         Format.fprintf fmt "@[<v 2>[%t]:@ %a@]"
70
           (fun fmt -> match g with None -> () | Some g -> pp_expr fmt g)
71
           
72
           (* (Utils.fprintf_list ~sep:"; "
73
            *    (fun fmt (e,b) ->
74
            *      if b then pp_expr fmt e
75
            *      else Format.fprintf fmt "not(%a)"
76
            *             pp_expr e)) gel *)
77 0d79d0f3 ploc
           (Utils.fprintf_list ~sep:";@ "
78 a742719e ploc
              (fun fmt (id, e) ->
79 0d79d0f3 ploc
                Format.fprintf fmt "%s = @[<hov 0>%a@]"
80 a742719e ploc
                  id
81 81229f63 ploc
                  pp_expr e)) up
82 a742719e ploc
    ))
83
  in
84 0d79d0f3 ploc
  report ~level:1 (
85
      fun fmt -> Format.fprintf fmt
86
                   "%i memories, %i init, %i step switch cases@."
87
                   (List.length mems)
88
                   (List.length sw_init)
89
                   (List.length sw_sys)
90
               
91
    );
92 a742719e ploc
  report ~level:1 (fun fmt ->
93 81229f63 ploc
      (*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag)  in*)
94
       let pp_res = pp_res Printers.pp_expr in
95 a742719e ploc
      Format.fprintf fmt "@[<v 0>@[<v 3>Init:@ %a@]@ "
96 81229f63 ploc
        pp_res  sw_init;
97 a742719e ploc
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "
98 81229f63 ploc
        pp_res  sw_sys
99 a742719e ploc
    );
100 d75eb6f1 ploc
  let new_node = Seal_export.to_lustre m sw_init sw_sys init_out update_out in  
101
  Format.eprintf "%a@." Printers.pp_node new_node;
102 a703ed0c ploc
  ()
103
  
104 ad4774b0 ploc
module Verifier =
105
  (struct
106
    include VerifierType.Default
107
    let name = "seal"
108
    let options = []
109 a703ed0c ploc
    let activate () =
110
      active := true;
111
      Options.global_inline := true
112
      
113 ad4774b0 ploc
    let is_active () = !active
114 a703ed0c ploc
    let run = seal_run
115
      
116 ad4774b0 ploc
                    
117
  end: VerifierType.S)
118