### Profile

 1 ```(* 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 *) ``` ```open Seal_slice ``` ```open Seal_extract ``` ```open Seal_utils ``` ```let active = ref false ``` ```let seal_export = ref None ``` ```let set_export s = ``` ``` match s with ``` ``` | "lustre" | "lus" | "m" | "matlab" -> ``` ``` seal_export := Some s ``` ``` | _ -> ``` ``` Format.eprintf "Unrecognized seal export: %s@.@?" s; ``` ``` exit 1 ``` ```(* 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 ``` ``` | "" -> ``` ``` 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 ``` ``` | s -> ( ``` ``` (* should have been addessed before *) ``` ``` match Machine_code_common.get_machine_opt machines s with ``` ``` | None -> ``` ``` Global.main_node := s; ``` ``` Format.eprintf "Code generation error: %a@." Error.pp_error_msg ``` ``` Error.Main_not_found; ``` ``` raise (Error.Error (Location.dummy_loc, Error.Main_not_found)) ``` ``` | Some _ -> ``` ``` s) ``` ``` in ``` ``` let m = Machine_code_common.get_machine machines node_name in ``` ``` let nd = m.mname in ``` ``` let mems = m.mmemory in ``` ``` report ~level:1 (fun fmt -> ``` ``` Format.fprintf fmt "Node %s compiled: %i memories@." nd.node_id ``` ``` (List.length mems)); ``` ``` (* Slicing node *) ``` ``` let msch = Utils.desome m.msch in ``` ``` let sliced_nd = slice_node (mems @ nd.node_outputs) msch nd in ``` ``` report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@."); ``` ``` report ~level:10 (fun fmt -> ``` ``` Format.fprintf fmt "Sliced Node %a@." Printers.pp_node sliced_nd); ``` ``` let consts = Corelang.(List.map const_of_top (get_consts prog)) in ``` ``` let pp_sys = pp_sys Printers.pp_expr in ``` ``` if List.length mems = 0 then ( ``` ``` (* A stateless node = a function ! *) ``` ``` let update_out = fun_as_switched_sys consts sliced_nd in ``` ``` report ~level:1 (fun fmt -> ``` ``` Format.fprintf fmt "Output (%i step switch cases):@ @[%a@]@." ``` ``` (List.length update_out) pp_sys update_out); ``` ``` let _ = ``` ``` match !seal_export with ``` ``` | Some "lustre" | Some "lus" -> ``` ``` Seal_export.fun_to_lustre basename prog m update_out ``` ``` | Some "matlab" | Some "m" -> ``` ``` assert false (* TODO *) ``` ``` | Some _ -> ``` ``` assert false ``` ``` | None -> ``` ``` () ``` ``` in ``` ``` ()) ``` ``` else ``` ``` (* A stateful node *) ``` ``` let sw_init, sw_sys, init_out, update_out = ``` ``` node_as_switched_sys consts mems sliced_nd ``` ``` in ``` ``` report ~level:1 (fun fmt -> ``` ``` Format.fprintf fmt ``` ``` "DynSys: (%i memories, %i init, %i step switch cases)@ @[@[Init:@ %a@]@ @[Step:@ %a@]@]@." ``` ``` (List.length mems) (List.length sw_init) (List.length sw_sys) pp_sys ``` ``` sw_init pp_sys sw_sys); ``` ``` report ~level:1 (fun fmt -> ``` ``` Format.fprintf fmt ``` ``` "Output (%i init, %i step switch cases):@ @[@[Init:@ %a@]@ \ ``` ``` @[Step:@ %a@]@]@." ``` ``` (List.length init_out) (List.length update_out) pp_sys init_out pp_sys ``` ``` update_out); ``` ``` let _ = ``` ``` match !seal_export with ``` ``` | Some "lustre" | Some "lus" -> ``` ``` Seal_export.node_to_lustre basename prog m sw_init sw_sys init_out ``` ``` update_out ``` ``` | Some "matlab" | Some "m" -> ``` ``` assert false (* TODO *) ``` ``` | Some _ -> ``` ``` assert false ``` ``` | None -> ``` ``` () ``` ``` in ``` ``` () ``` ```module Verifier : VerifierType.S = struct ``` ``` include VerifierType.Default ``` ``` let name = "seal" ``` ``` let options = ``` ``` [ ``` ``` "-export", Arg.String set_export, "seal export option (lustre, matlab)"; ``` ``` "-debug", Arg.Set seal_debug, "seal debug"; ``` ``` ] ``` ``` let activate () = ``` ``` active := true; ``` ``` Options.global_inline := true; ``` ``` Options.optimization := 0; ``` ``` Options.const_unfold := true; ``` ``` () ``` ``` let is_active () = !active ``` ``` let run = seal_run ``` ```end ``` ```let () = ``` ``` VerifierList.registered := ``` ``` (module Verifier : VerifierType.S) :: !VerifierList.registered ```