Revision a0c92fa8
Added by Pierre-Loïc Garoche over 2 years ago
| 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
printing nodes + more progress on seal export