Project

General

Profile

Revision a0c92fa8 src/tools/seal/seal_verifier.ml

View differences:

src/tools/seal/seal_verifier.ml
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 1
(* TODO
12 2

  
13 3
   - build the output function: for the moment we slice the node with
......
35 25
       the property to prove
36 26
     
37 27
 *)
28

  
29

  
30
open Seal_slice
31
open Seal_extract
32
open Seal_utils
33

  
34
let active = ref false
35
let seal_export = ref None
36

  
37
let set_export s = match s with
38
  | "lustre" | "lus" | "m" | "matlab" -> seal_export := Some s
39
  | _ -> (Format.eprintf "Unrecognized seal export: %s@.@?" s; exit 1)
38 40
           
39 41
(* Select the appropriate node, should have been inlined already and
40 42
   extract update/output functions. *)
......
64 66
  in
65 67
  let m = Machine_code_common.get_machine machines node_name in
66 68
  let nd = m.mname in
67
  (* Format.eprintf "Node %a@." Printers.pp_node nd; *)
68 69
  let mems = m.mmemory in
70

  
69 71
  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; *)
72

  
73
  (* Slicing node *)
71 74
  let msch = Utils.desome m.msch in
72
  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)
73 75
  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 76
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
77
  report ~level:10 (fun fmt -> Format.fprintf fmt "Sliced Node %a@." Printers.pp_node sliced_nd);
76 78

  
77 79
  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
  ()
80

  
81
  let pp_sys = pp_sys Printers.pp_expr in
82
  if List.length mems = 0 then
83
    begin (* A stateless node = a function ! *)
84
      
85
      let update_out = fun_as_switched_sys consts sliced_nd in
86

  
87
      report ~level:1 (fun fmt ->
88
          Format.fprintf fmt
89
            "Output (%i step switch cases):@ @[<v 0>%a@]@."
90
            (List.length update_out)
91
            pp_sys update_out
92
        );
93
      
94
      let _ = match !seal_export with
95
        | Some "lustre" | Some "lus" ->
96
           Seal_export.fun_to_lustre basename prog m update_out  
97
        | Some "matlab" | Some "m" -> assert false (* TODO *)
98
        | Some _ -> assert false 
99
        | None -> ()
100
      in
101
      ()
102
    end
103
  else
104
    begin (* A stateful node *)
105

  
106
      let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in
107

  
108
      report ~level:1 (fun fmt ->
109
          Format.fprintf fmt
110
            "DynSys: (%i memories, %i init, %i step switch cases)@ @[<v 0>@[<v 3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@."
111
            (List.length mems)
112
            (List.length sw_init)
113
            (List.length sw_sys)
114
            pp_sys  sw_init
115
            pp_sys  sw_sys
116
        );
117
      
118
      report ~level:1 (fun fmt ->
119
          Format.fprintf fmt
120
            "Output (%i init, %i step switch cases):@ @[<v 0>@[<v 3>Init:@ %a@]@ @[<v 3>Step:@ %a@]@]@."
121
            (List.length init_out)
122
            (List.length update_out)
123
            pp_sys  init_out
124
            pp_sys  update_out
125
        );
126
      
127
      let _ = match !seal_export with
128
        | Some "lustre" | Some "lus" ->
129
           Seal_export.node_to_lustre basename prog m sw_init sw_sys init_out update_out  
130
        | Some "matlab" | Some "m" -> assert false (* TODO *)
131
        | Some _ -> assert false 
132
        | None -> ()
133
      in
134
      ()
135
    end
134 136
  
135 137
module Verifier =
136 138
  (struct
......
151 153
      
152 154
    let is_active () = !active
153 155
    let run = seal_run
154
      
155
                    
156
            
157
            
156 158
  end: VerifierType.S)
157 159
    

Also available in: Unified diff