CristalCaveGem » LustreC

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)

(* 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

 *)

(* 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 "@[<v 2>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 -> begin

          Global.main_node := s;

          Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;

          raise (Corelang.Error (Location.dummy_loc, Error.Main_not_found))

        end

      | Some _ -> s

    )

  in

  let m = Machine_code_common.get_machine machines node_name in

  let nd = m.mname in

  (* Format.eprintf "Node %a@." Printers.pp_node nd; *)

  let mems = m.mmemory in

  (* Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems; *)

  let msch = Utils.desome m.msch in

  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)

  let sliced_nd = slice_node (mems@nd.node_outputs) msch nd in

  if false then Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd;

  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");

  let consts = Corelang.(List.map const_of_top (get_consts prog)) in

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

  let pp_res pp_expr =

    (Utils.fprintf_list ~sep:"@ "

       (fun fmt (g, up) ->

         Format.fprintf fmt "@[<v 2>[%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 *)

           (Utils.fprintf_list ~sep:";@ "

              (fun fmt (id, e) ->

                Format.fprintf fmt "%s = @[<hov 0>%a@]"

                  id

                  pp_expr e)) up

    ))

  in

  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)

    );

  report ~level:1 (fun fmt ->

      (*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

      Format.fprintf fmt "DynSys:@ @[<v 0>@[<v 3>Init:@ %a@]@ "

        pp_res  sw_init;

      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "

        pp_res  sw_sys

    );

  report ~level:1 (fun fmt ->

      (*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

      Format.fprintf fmt "Output:@ @[<v 0>@[<v 3>Init:@ %a@]@ "

        pp_res  init_out;

      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "

        pp_res  update_out

    );

  let _ = match !seal_export with

    | Some "lustre" | Some "lus" ->

       Seal_export.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 =

  (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: VerifierType.S)