### Profile

Statistics
| Branch: | Tag: | Revision:

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

1 2 3 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 ``` ``` ``` ``` *) ``` a0c92fa8 ploc ```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) ``` d5ec9f63 ploc ``` ``` a703ed0c ploc ```(* Select the appropriate node, should have been inlined already and ``` ``` extract update/output functions. *) ``` 7a4fd94d ploc ```let seal_run ~basename prog machines = ``` a703ed0c ploc ``` 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 ``` ``` ) ``` efc2cd2f ploc ``` | s -> ( (* should have been addessed before *) ``` ``` match Machine_code_common.get_machine_opt machines s with ``` ``` | None -> begin ``` ``` Global.main_node := s; ``` ``` Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found; ``` 04a188ec ploc ``` raise (Error.Error (Location.dummy_loc, Error.Main_not_found)) ``` efc2cd2f ploc ``` end ``` ``` | Some _ -> s ``` ``` ) ``` a703ed0c ploc ``` in ``` ``` let m = Machine_code_common.get_machine machines node_name in ``` ``` let nd = m.mname in ``` ``` let mems = m.mmemory in ``` a0c92fa8 ploc 04a188ec ploc ``` report ~level:1 (fun fmt -> Format.fprintf fmt "Node %s compiled: %i memories@." nd.node_id (List.length mems)); ``` a0c92fa8 ploc ``` (* Slicing node *) ``` a703ed0c ploc ``` let msch = Utils.desome m.msch in ``` 25320f03 ploc ``` let sliced_nd = slice_node (mems@nd.node_outputs) msch nd in ``` 0d79d0f3 ploc ``` report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@."); ``` a0c92fa8 ploc ``` report ~level:10 (fun fmt -> Format.fprintf fmt "Sliced Node %a@." Printers.pp_node sliced_nd); ``` 8c934ccd ploc ``` let consts = Corelang.(List.map const_of_top (get_consts prog)) in ``` a0c92fa8 ploc ``` let pp_sys = pp_sys Printers.pp_expr in ``` ``` if List.length mems = 0 then ``` ``` begin (* 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 ``` ``` () ``` ``` end ``` ``` else ``` ``` begin (* 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 ``` ``` () ``` ``` end ``` a703ed0c ploc ``` ``` ad4774b0 ploc ```module Verifier = ``` ``` (struct ``` ``` include VerifierType.Default ``` ``` let name = "seal" ``` 03c767b1 ploc ``` let options = ``` ``` [ ``` ``` "-export", Arg.String set_export, "seal export option (lustre, matlab)"; ``` ``` "-debug", Arg.Set seal_debug, "seal debug" ``` ``` ] ``` a703ed0c ploc ``` let activate () = ``` ``` active := true; ``` efc2cd2f ploc ``` Options.global_inline := true; ``` ``` Options.optimization := 0; ``` ``` Options.const_unfold := true; ``` ``` () ``` a703ed0c ploc ``` ``` ad4774b0 ploc ``` let is_active () = !active ``` a703ed0c ploc ``` let run = seal_run ``` a0c92fa8 ploc ``` ``` ``` ``` ad4774b0 ploc ``` end: VerifierType.S) ``` ` `