Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal / seal_verifier.ml @ 8c934ccd

History | View | Annotate | Download (3.74 KB)

1
open Seal_slice
2
open Seal_extract
3
open Seal_utils
4

    
5
let active = ref false
6

    
7
(* 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
(* 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
    | "" -> (
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
    | s -> s
52
  in
53
  let m = Machine_code_common.get_machine machines node_name in
54
  let nd = m.mname in
55
  (* Format.eprintf "Node %a@." Printers.pp_node nd; *)
56
  let mems = m.mmemory in
57
  (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *)
58
  let msch = Utils.desome m.msch in
59
  (* 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
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
63

    
64
  let consts = Corelang.(List.map const_of_top (get_consts prog)) in
65
  let sw_init, sw_sys = node_as_switched_sys consts mems sliced_nd in
66
  let pp_res =
67
    (Utils.fprintf_list ~sep:"@ "
68
       (fun fmt (gel, up) ->
69
         Format.fprintf fmt "@[<v 2>[%a]:@ %a@]"
70
           (Utils.fprintf_list ~sep:"; "
71
              (fun fmt (e,b) ->
72
                if b then Printers.pp_expr fmt e
73
                else Format.fprintf fmt "not(%a)"
74
                       Printers.pp_expr e)) gel
75
           (Utils.fprintf_list ~sep:";@ "
76
              (fun fmt (id, e) ->
77
                Format.fprintf fmt "%s = @[<hov 0>%a@]"
78
                  id
79
                  Printers.pp_expr e)) up
80
    ))
81
  in
82
  report ~level:1 (
83
      fun fmt -> Format.fprintf fmt
84
                   "%i memories, %i init, %i step switch cases@."
85
                   (List.length mems)
86
                   (List.length sw_init)
87
                   (List.length sw_sys)
88
               
89
    );
90
  report ~level:1 (fun fmt ->
91
      Format.fprintf fmt "@[<v 0>@[<v 3>Init:@ %a@]@ "
92
        pp_res sw_init;
93
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "
94
        pp_res sw_sys
95
    );
96
  
97

    
98
  ()
99
  
100
module Verifier =
101
  (struct
102
    include VerifierType.Default
103
    let name = "seal"
104
    let options = []
105
    let activate () =
106
      active := true;
107
      Options.global_inline := true
108
      
109
    let is_active () = !active
110
    let run = seal_run
111
      
112
                    
113
  end: VerifierType.S)
114