Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal_verifier.ml @ 0d79d0f3

History | View | Annotate | Download (2.49 KB)

1
open Seal_slice
2
open Seal_extract
3
open Seal_utils
4

    
5
let active = ref false
6

    
7
(* Select the appropriate node, should have been inlined already and
8
   extract update/output functions. *)
9
let seal_run basename prog machines =
10
  let node_name =
11
    match !Options.main_node with
12
    | "" -> (
13
      Format.eprintf "SEAL verifier requires a main node.@.";
14
      Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
15
        (Utils.fprintf_list ~sep:"@ "
16
           (fun fmt m ->
17
             Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id
18
           )
19
        )
20
        machines; 
21
      exit 1
22
    )
23
    | s -> s
24
  in
25
  let m = Machine_code_common.get_machine machines node_name in
26
  let nd = m.mname in
27
  (* Format.eprintf "Node %a@." Printers.pp_node nd; *)
28
  let mems = m.mmemory in
29
  (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *)
30
  let msch = Utils.desome m.msch in
31
  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)
32
  let sliced_nd = slice_node mems msch nd in
33
  (* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *)
34
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
35
  let sw_init, sw_sys = node_as_switched_sys mems sliced_nd in
36
  let pp_res =
37
    (Utils.fprintf_list ~sep:"@ "
38
       (fun fmt (gel, up) ->
39
         Format.fprintf fmt "@[<v 2>[%a]:@ %a@]"
40
           (Utils.fprintf_list ~sep:"; "
41
              (fun fmt (e,b) ->
42
                if b then Printers.pp_expr fmt e
43
                else Format.fprintf fmt "not(%a)"
44
                       Printers.pp_expr e)) gel
45
           (Utils.fprintf_list ~sep:";@ "
46
              (fun fmt (id, e) ->
47
                Format.fprintf fmt "%s = @[<hov 0>%a@]"
48
                  id
49
                  Printers.pp_expr e)) up
50
    ))
51
  in
52
  report ~level:1 (
53
      fun fmt -> Format.fprintf fmt
54
                   "%i memories, %i init, %i step switch cases@."
55
                   (List.length mems)
56
                   (List.length sw_init)
57
                   (List.length sw_sys)
58
               
59
    );
60
  report ~level:1 (fun fmt ->
61
      Format.fprintf fmt "@[<v 0>@[<v 3>Init:@ %a@]@ "
62
        pp_res sw_init;
63
      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "
64
        pp_res sw_sys
65
    );
66
  
67

    
68
  ()
69
  
70
module Verifier =
71
  (struct
72
    include VerifierType.Default
73
    let name = "seal"
74
    let options = []
75
    let activate () =
76
      active := true;
77
      Options.global_inline := true
78
      
79
    let is_active () = !active
80
    let run = seal_run
81
      
82
                    
83
  end: VerifierType.S)
84