CristalCaveGem » LustreC

(* Header Printing functions *)

  module GhostProto : MODIFIERS_GHOST_PROTO

  val print_machine_decl_prefix : Format.formatter -> machine_t -> unit

  val pp_import_arrow : formatter -> unit -> unit

  let print_machine_decl_prefix _ _ = ()

module Main =

functor

  (Mod : MODIFIERS_HDR)

  ->

  struct

    module Protos = Protos (Mod.GhostProto)

    let print_import_standard fmt () =

      (* if Machine_types.has_machine_type () then *)

      fprintf fmt "#include <stdint.h>@,%a%a"

        (if !Options.mpfr then pp_print_endcut "#include <mpfr.h>"

        else pp_print_nothing)

        () Mod.pp_import_arrow ()

    let rec print_static_val pp_var fmt v =

      match v.value_desc with

      | Cst c ->

        pp_c_const fmt c

      | Var v ->

        pp_var fmt v

      | Fun (n, vl) ->

        pp_basic_lib_fun

          (Types.is_int_type v.value_type)

          n (print_static_val pp_var) fmt vl

      | _ ->

        eprintf "Internal error: C_backend_header.print_static_val";

    let print_constant_decl (m, attr, inst) pp_var fmt v =

      fprintf fmt "%s %a = %a" attr

        (pp_c_type (sprintf "%s ## %s" inst v.var_id))

        v.var_type (print_static_val pp_var) (get_const_assign m v)

    let pp_var inst const_locals fmt v =

      if List.mem v const_locals then fprintf fmt "%s ## %s" inst v.var_id

      else fprintf fmt "%s" v.var_id

    let print_static_constant_decl ((_, _, inst) as macro) fmt const_locals =

      pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:(pp_print_endcut ";\\")

        ~pp_eol:(pp_print_endcut ";\\")

        (print_constant_decl macro (pp_var inst const_locals))

        fmt const_locals

    let print_static_declare_instance (m, attr, inst) const_locals fmt

        (i, (n, static)) =

      let values = List.map (value_of_dimension m) static in

      fprintf fmt "%a(%s, %a%s)" pp_machine_static_declare_name (node_name n)

        attr

        (pp_print_list ~pp_open_box:pp_open_hbox ~pp_sep:pp_print_comma

           ~pp_eol:pp_print_comma

           (print_static_val (pp_var inst const_locals)))

        values i

    let print_static_declare_macro fmt ((m, attr, inst) as macro) =

      let const_locals =

        List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals

      in

      let array_mem =

        List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory

      in

      fprintf fmt "@[<v 2>#define %a(%s, %a%s)\\@,%a%s %a %s;\\@,%a%a;@]"

        pp_machine_static_declare_name m.mname.node_id attr

        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma

           (pp_c_var_read m))

        m.mstatic inst

        (* constants *)

        (print_static_constant_decl macro)

        const_locals attr

        (pp_machine_memtype_name ~ghost:false)

        m.mname.node_id inst

        (pp_print_list ~pp_open_box:pp_open_vbox0

           ~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\")

           (pp_c_decl_local_var m))

        array_mem

        (pp_print_list ~pp_open_box:pp_open_vbox0

           ~pp_sep:(pp_print_endcut ";\\") (fun fmt (i', m') ->

             let path = sprintf "%s ## _%s" inst i' in

             fprintf fmt "%a"

               (print_static_declare_instance macro const_locals)

               (path, m')))

        m.minstances

    let print_static_link_instance fmt (i, (m, _)) =

      fprintf fmt "%a(%s)" pp_machine_static_link_name (node_name m) i

    (* Allocation of a node struct: - if node memory is an array/matrix/etc, we

       cast it to a pointer (see pp_registers_struct) *)

    let print_static_link_macro fmt (m, _, inst) =

      let array_mem =

        List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory

      in

      fprintf fmt "@[<v>@[<v 2>#define %a(%s) do {\\@,%a%a;\\@]@,} while (0)@]"

        pp_machine_static_link_name m.mname.node_id inst

        (pp_print_list ~pp_open_box:pp_open_vbox0

           ~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\")

           (fun fmt v ->

             fprintf fmt "%s._reg.%s = (%a*) &%s" inst v.var_id

               (fun fmt v ->

                 pp_c_type "" fmt (Types.array_base_type v.var_type))

               v v.var_id))

        array_mem

        (pp_print_list ~pp_open_box:pp_open_vbox0

           ~pp_sep:(pp_print_endcut ";\\") (fun fmt (i', m') ->

             let path = sprintf "%s ## _%s" inst i' in

             fprintf fmt "%a;\\@,%s.%s = &%s" print_static_link_instance

               (path, m') inst i' path))

        m.minstances

    let print_static_alloc_macro fmt (m, attr, inst) =

      fprintf fmt

        "@[<v>@[<v 2>#define %a(%s, %a%s)\\@,%a(%s, %a%s);\\@,%a(%s);@]@]"

        pp_machine_static_alloc_name m.mname.node_id attr

        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma

           (pp_c_var_read m))

        m.mstatic inst pp_machine_static_declare_name m.mname.node_id attr

        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma

           (pp_c_var_read m))

        m.mstatic inst pp_machine_static_link_name m.mname.node_id inst

    (* TODO: ACSL we do multiple things: - provide the semantics of the node as

       a predicate: function step and reset are associated to ACSL predicate -

       the node is associated to a refinement contract, wrt its ACSL sem - if

       the node is a regular node associated to a contract, print the contract

       as function contract. - do not print anything if this is a contract node *)

    let print_machine_alloc_decl fmt m =

      Mod.print_machine_decl_prefix fmt m;

      if not (fst (get_stateless_status m)) then

        if !Options.static_mem then

          (* Static allocation *)

          let macro = m, mk_attribute m, mk_instance m in

          fprintf fmt "%a@,%a@,%a" print_static_declare_macro macro

            print_static_link_macro macro print_static_alloc_macro macro

        else

          (* Dynamic allocation *)

          fprintf fmt "extern %a;@,extern %a" print_alloc_prototype

            (m.mname.node_id, m.mstatic)

            print_dealloc_prototype m.mname.node_id

    let print_machine_struct_top_decl_from_header fmt tdecl =

      let inode = imported_node_of_top tdecl in

      if not inode.nodei_stateless then

        (* Declare struct *)

        fprintf fmt "%a;" (pp_machine_memtype_name ~ghost:false) inode.nodei_id

    let print_stateless_C_prototype fmt (name, inputs, outputs) =

      let output = match outputs with [ hd ] -> hd | _ -> assert false in

      fprintf fmt "%a %s %a"

        (pp_basic_c_type ~pp_c_basic_type_desc ~var_opt:None)

        output.var_type name

        (pp_print_parenthesized pp_c_decl_input_var)

        inputs

    let print_machine_decl_top_decl_from_header fmt tdecl =

      let inode = imported_node_of_top tdecl in

      (*Mod.print_machine_decl_prefix fmt m;*)

      let prototype = inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs in

      if inode.nodei_prototype = Some "C" then

        if inode.nodei_stateless then

          fprintf fmt "extern %a;" print_stateless_C_prototype prototype

        else (

          (* TODO: raise proper error *)

          Format.eprintf

            "internal error: print_machine_decl_top_decl_from_header";

          assert false)

      else if inode.nodei_stateless then

        fprintf fmt "extern %a;" Protos.print_stateless_prototype prototype

      else

        let static_inputs =

          List.filter (fun v -> v.var_dec_const) inode.nodei_inputs

        in

        let used name =

          List.exists

            (fun v -> v.var_id = name)

            (inode.nodei_inputs @ inode.nodei_outputs)

        in

        let self = mk_new_name used "self" in

        let mem = mk_new_name used "mem" in

        let static_prototype = inode.nodei_id, static_inputs in

        fprintf fmt "extern %a;@,extern %a;@,extern %a;@,extern %a;@,extern %a;"

          (Protos.print_set_reset_prototype self mem)

          static_prototype

          (Protos.print_clear_reset_prototype self mem)

          static_prototype

          (Protos.print_init_prototype self)

          static_prototype

          (Protos.print_clear_prototype self)

          static_prototype

          (Protos.print_step_prototype self mem)

          prototype

    let print_const_top_decl fmt tdecl =

      let cdecl = const_of_top tdecl in

      fprintf fmt "extern %a;" (pp_c_type cdecl.const_id)

        (if

         !Options.mpfr

         && Types.(is_real_type (array_base_type cdecl.const_type))

        then Types.dynamic_type cdecl.const_type

        else cdecl.const_type)

    let rec pp_c_type_decl filename cpt var fmt tdecl =

      match tdecl with

      | Tydec_any ->

        assert false

      | Tydec_int ->

        fprintf fmt "int %s" var

      | Tydec_real when !Options.mpfr ->

        fprintf fmt "%s %s" Mpfr.mpfr_t var

      | Tydec_real ->

        fprintf fmt "double %s" var

      (* | Tydec_float -> fprintf fmt "float %s" var *)

      | Tydec_bool ->

        fprintf fmt "_Bool %s" var

      | Tydec_clock ty ->

        pp_c_type_decl filename cpt var fmt ty

      | Tydec_const c ->

        fprintf fmt "%s %s" c var

      | Tydec_array (d, ty) ->

        fprintf fmt "%a[%a]"

          (pp_c_type_decl filename cpt var)

          ty pp_c_dimension d

      | Tydec_enum tl ->

        incr cpt;

        fprintf fmt "enum _enum_%s_%d %a %s"

          (protect_filename filename)

          !cpt

          (pp_print_braced pp_print_string)

          tl var

      | Tydec_struct fl ->

        incr cpt;

        fprintf fmt "struct _struct_%s_%d %a %s"

          (protect_filename filename)

          !cpt

          (pp_print_braced ~pp_sep:pp_print_semicolon (fun fmt (label, tdesc) ->

               pp_c_type_decl filename cpt label fmt tdesc))

          fl var

    (* let print_type_definitions fmt filename =

     *   let cpt_type = ref 0 in

     *   Hashtbl.iter (fun typ decl ->

     *       match typ with

     *       | Tydec_const var ->

     *         begin match decl.top_decl_desc with

     *           | TypeDef tdef ->

     *             fprintf fmt "typedef %a;@.@."

     *               (pp_c_type_decl filename cpt_type var) tdef.tydef_desc

     *           | _ -> assert false

     *         end

     *       | _ -> ()) type_table *)

    let reset_type_definitions, print_type_definition_top_decl_from_header =

      let cpt_type = ref 0 in

      ( (fun () -> cpt_type := 0),

        fun filename fmt tdecl ->

          let typ = typedef_of_top tdecl in

          fprintf fmt "typedef %a;"

            (pp_c_type_decl filename cpt_type typ.tydef_id)

            typ.tydef_desc )

    (********************************************************************************************)

    (* MAIN Header Printing functions *)

    (********************************************************************************************)

    let print_alloc_header header_fmt basename _prog machines dependencies spec

        =

      (* Include once: start *)

      let baseNAME = file_to_module_name basename in

      fprintf header_fmt

        "@[<v>%a@,\

         #ifndef _%s_alloc@,\

         #define _%s_alloc@,\

         @,\

         /* Import header from %s */@,\

         %a@,\

         @,\

         %a%a%a#endif@]"

        (* Print the svn version number and the supported C standard (C90 or

           C99) *)

        pp_print_version () baseNAME baseNAME (* Import the header *) basename

        print_import_prototype

        {

          local = true;

          name = basename;

          content = [];

          is_stateful = true (* assuming it is staful *);

        }

        (* Print dependencies *)

        (pp_print_list ~pp_open_box:pp_open_vbox0

           ~pp_prologue:(pp_print_endcut "/* Import dependencies */")

           print_import_alloc_prototype ~pp_epilogue:pp_print_cutcut)

        dependencies

        (* Print the struct definitions of all machines. *)

        (pp_print_list ~pp_open_box:pp_open_vbox0

           ~pp_prologue:(pp_print_endcut "/* Struct definitions */")

           ~pp_sep:pp_print_cutcut print_machine_struct

           ~pp_epilogue:pp_print_cutcut)

        machines

        (* Print the prototypes of all machines *)

        (pp_print_list ~pp_open_box:pp_open_vbox0

           ~pp_prologue:

             (pp_print_endcut "/* Node allocation function/macro prototypes */")

           ~pp_sep:pp_print_cutcut print_machine_alloc_decl

           ~pp_epilogue:pp_print_cutcut)

        machines

    (* Include once: end *)

    (* Function called when compiling a lusi file and generating the associated

       C header. *)

    let print_header_from_header header_fmt basename header =

      (* Include once: start *)

      let baseNAME = file_to_module_name basename in

      let types = get_typedefs header in

      let consts = get_consts header in

      let nodes = get_imported_nodes header in

      let dependencies = get_dependencies header in

      reset_type_definitions ();

      fprintf header_fmt

        "@[<v>%a@,\

         #ifndef _%s@,\

         #define _%s@,\

         @,\

         /* Import standard library */@,\

         %a@,\

         @,\

         %a%a%a%a%a%a#endif@]@."

        (* Print the version number and the supported C standard (C90 or C99) *)

        pp_print_version () baseNAME baseNAME

        (* imports standard library definitions (arrow) *)

        print_import_standard ()

        (* imports dependencies *)

        (pp_print_list ~pp_open_box:pp_open_vbox0

           ~pp_prologue:(pp_print_endcut "/* Import dependencies */")

           (fun fmt dep ->

             let local, name = dependency_of_top dep in

             print_import_prototype fmt

               {

                 local;

                 name;

                 content = [];

                 is_stateful = true (* assuming it is stateful *);

               })

           ~pp_epilogue:pp_print_cutcut)

        dependencies

        (* Print the type definitions from the type table *)

        (pp_print_list ~pp_open_box:pp_open_vbox0

           ~pp_prologue:(pp_print_endcut "/* Types definitions */")

           (print_type_definition_top_decl_from_header basename)

           ~pp_epilogue:pp_print_cutcut)

        types

        (* Print the global constant declarations. *)

        (pp_print_list ~pp_open_box:pp_open_vbox0

           ~pp_prologue:

             (pp_print_endcut

                "/* Global constants (declarations, definitions are in C file) \

                 */")

           print_const_top_decl ~pp_epilogue:pp_print_cutcut)

        consts

        (* MPFR *)

        (if !Options.mpfr then fun fmt () ->

         fprintf fmt

           "/* Global initialization declaration */@,\

            extern %a;@,\

            @,\

            /* Global clear declaration */@,\

            extern %a;@,\

            @,"

           print_global_init_prototype baseNAME print_global_clear_prototype

           baseNAME

        else pp_print_nothing)

        ()

        (* Print the struct declarations of all machines. *)

        (pp_print_list ~pp_open_box:pp_open_vbox0

           ~pp_prologue:(pp_print_endcut "/* Struct declarations */")

           print_machine_struct_top_decl_from_header

           ~pp_epilogue:pp_print_cutcut)

        nodes

        (* Print the prototypes of all machines *)

        (pp_print_list ~pp_open_box:pp_open_vbox0

           ~pp_prologue:(pp_print_endcut "/* Nodes declarations */")

           ~pp_sep:pp_print_cutcut print_machine_decl_top_decl_from_header

           ~pp_epilogue:pp_print_cutcut)

        nodes

  end