### Profile

Statistics
| Branch: | Tag: | Revision:

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

1 2 3 0d79d0f3 ploc ```open Seal_slice ``` ```open Seal_extract ``` a703ed0c ploc ```open Seal_utils ``` ad4774b0 ploc ```let active = ref false ``` d5ec9f63 ploc ```(* TODO ``` ``` - build the output function: for the moment we slice the node with ``` ``` its memories, building the function updating the memory. We will ``` ``` need later the output function, using inputs and memories to ``` ``` compute the output. A way to do this would be to declared memories ``` ``` as input, remove their definitions, and slice the node with its ``` ``` outputs. This should clean up unnecessary internal variables and ``` ``` give us the output function. ``` ``` - compute the dimension of the node (nb of memories) ``` ``` - if the updates are all linear or affine, provide the update as a ``` ``` matrix rather then a polynomial. Check if this is simpler to do ``` ``` here or in matlab. ``` ``` - analyzes require bounds on inputs or sometimes target property ``` ``` over states. These could be specified as node annotations: eg ``` ``` - /seal/bounds/inputs/semialg/: (in1^4 + in2^3, 1) ``` ``` to specify that the inputs are constrained by a semialgebraic ``` ``` set (p,b) such as p(inputs) <= b ``` ``` - /seal/bounds/inputs/LMI/: (todo_describe_a_matrix) .... and so on. ``` ``` To be defined depending on needs. ``` ``` - /seal/prop/semialg/: (x3 - x5, 2) -- if x3 - x5 <= 2 is ``` ``` the property to prove ``` ``` ``` ``` *) ``` ``` ``` a703ed0c ploc ```(* Select the appropriate node, should have been inlined already and ``` ``` extract update/output functions. *) ``` ```let seal_run basename prog machines = ``` ``` let node_name = ``` ``` match !Options.main_node with ``` 0d79d0f3 ploc ``` | "" -> ( ``` ``` Format.eprintf "SEAL verifier requires a main node.@."; ``` ``` Format.eprintf "@[Available ones are:@ %a@]@.@?" ``` ``` (Utils.fprintf_list ~sep:"@ " ``` ``` (fun fmt m -> ``` ``` Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id ``` ``` ) ``` ``` ) ``` ``` machines; ``` ``` exit 1 ``` ``` ) ``` a703ed0c ploc ``` | s -> s ``` ``` in ``` ``` let m = Machine_code_common.get_machine machines node_name in ``` ``` let nd = m.mname in ``` a742719e ploc ``` (* Format.eprintf "Node %a@." Printers.pp_node nd; *) ``` a703ed0c ploc ``` let mems = m.mmemory in ``` a742719e ploc ``` (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *) ``` a703ed0c ploc ``` let msch = Utils.desome m.msch in ``` a742719e ploc ``` (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *) ``` ``` let sliced_nd = slice_node mems msch nd in ``` ``` (* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *) ``` 0d79d0f3 ploc ``` report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@."); ``` 8c934ccd ploc ``` let consts = Corelang.(List.map const_of_top (get_consts prog)) in ``` d75eb6f1 ploc ``` let sw_init, sw_sys, init_out, update_out = node_as_switched_sys consts mems sliced_nd in ``` 81229f63 ploc ``` let pp_res pp_expr = ``` a742719e ploc ``` (Utils.fprintf_list ~sep:"@ " ``` 81229f63 ploc ``` (fun fmt (g, up) -> ``` ``` Format.fprintf fmt "@[[%t]:@ %a@]" ``` ``` (fun fmt -> match g with None -> () | Some g -> pp_expr fmt g) ``` ``` ``` ``` (* (Utils.fprintf_list ~sep:"; " ``` ``` * (fun fmt (e,b) -> ``` ``` * if b then pp_expr fmt e ``` ``` * else Format.fprintf fmt "not(%a)" ``` ``` * pp_expr e)) gel *) ``` 0d79d0f3 ploc ``` (Utils.fprintf_list ~sep:";@ " ``` a742719e ploc ``` (fun fmt (id, e) -> ``` 0d79d0f3 ploc ``` Format.fprintf fmt "%s = @[%a@]" ``` a742719e ploc ``` id ``` 81229f63 ploc ``` pp_expr e)) up ``` a742719e ploc ``` )) ``` ``` in ``` 0d79d0f3 ploc ``` report ~level:1 ( ``` ``` fun fmt -> Format.fprintf fmt ``` ``` "%i memories, %i init, %i step switch cases@." ``` ``` (List.length mems) ``` ``` (List.length sw_init) ``` ``` (List.length sw_sys) ``` ``` ``` ``` ); ``` a742719e ploc ``` report ~level:1 (fun fmt -> ``` 81229f63 ploc ``` (*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag) in*) ``` ``` let pp_res = pp_res Printers.pp_expr in ``` a742719e ploc ``` Format.fprintf fmt "@[@[Init:@ %a@]@ " ``` 81229f63 ploc ``` pp_res sw_init; ``` a742719e ploc ``` Format.fprintf fmt "@[Step:@ %a@]@]@ " ``` 81229f63 ploc ``` pp_res sw_sys ``` a742719e ploc ``` ); ``` d75eb6f1 ploc ``` let new_node = Seal_export.to_lustre m sw_init sw_sys init_out update_out in ``` ``` Format.eprintf "%a@." Printers.pp_node new_node; ``` a703ed0c ploc ``` () ``` ``` ``` ad4774b0 ploc ```module Verifier = ``` ``` (struct ``` ``` include VerifierType.Default ``` ``` let name = "seal" ``` ``` let options = [] ``` a703ed0c ploc ``` let activate () = ``` ``` active := true; ``` ``` Options.global_inline := true ``` ``` ``` ad4774b0 ploc ``` let is_active () = !active ``` a703ed0c ploc ``` let run = seal_run ``` ``` ``` ad4774b0 ploc ``` ``` ``` end: VerifierType.S) ``` ` `