CristalCaveGem » LustreC

    "/* @[<v>\

     C code generated by %s@,\

    (Filename.basename Sys.executable_name) 

    Version.number 

    (if !Options.mpfr then "MPFR multi-precision" else "(double) floating-point")

let protect_filename s =

  Str.global_replace (Str.regexp "\\.\\|\\ ") "_" s

let pp_ptr fmt =

  fprintf fmt "*%s"

let pp_label fmt =

  fprintf fmt "%s:"

let var_is name v =

  v.var_id = name

    || exists (var_is name) m.mmemory in

(* Generation of a non-clashing name for the self memory variable (for step and reset functions) *)

(* Generation of a non-clashing name for the instance variable of static allocation macro *)

    exists (var_is name) m.mstep.step_inputs

    || exists (var_is name) m.mmemory in

(* Generation of a non-clashing name for the attribute variable of static allocation macro *)

    exists (var_is name) m.mstep.step_inputs

    || exists (var_is name) m.mmemory in

  { var_id = id;

    var_loc = loc }

let reset_loop_counter () =

 loop_cpt := -1

  let vars = m.mstep.step_inputs

             @ m.mstep.step_outputs

             @ m.mstep.step_locals

             @ m.mmemory in

  in aux ()

(*

let addr_cpt = ref (-1)

let reset_addr_counter () =

 addr_cpt := -1

let mk_addr_var m var =

  let vars = m.mmemory in

  let rec aux () =

    incr addr_cpt;

    let s = Printf.sprintf "%s_%s_%d" var "addr" !addr_cpt in

    if List.exists (fun v -> v.var_id = s) vars then aux () else s

  in aux ()

*)

let pp_machine_memtype_name ?(ghost=false) fmt id =

let pp_machine_decl ?(ghost=false) pp_var fmt (id, var) =

let pp_machine_decl' ?(ghost=false) fmt =

    fprintf fmt "((%a %% %a) + ((%a %% %a) < 0?(abs(%a)):0))"

      pp_val v1 pp_val v2

      pp_val v1 pp_val v2

      pp_val v2

  else (* Regular behavior: printing a % *)

    fprintf fmt "(%a - %t) / %a"

      pp_val v1

      (pp_mod pp_val v1 v2)

      pp_val v2

  else (* Regular behavior: printing a / *)

  (*  | "ite", [v1; v2; v3] -> fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)

  | "uminus", [v] ->

  | "not", [v] ->

  | "impl", [v1; v2] ->

  | "=", [v1; v2] ->

  | "mod", [v1; v2] ->

     if is_int then

       pp_mod pp_val v1 v2 fmt 

     else

       fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2

  | "equi", [v1; v2] ->

  | "xor", [v1; v2] ->

  | "/", [v1; v2] ->

     if is_int then

       pp_div pp_val v1 v2 fmt

     else

       fprintf fmt "(%a / %a)" pp_val v1 pp_val v2

  | _, [v1; v2] ->

    fprintf fmt "((%a)?%a:%a)"

      pp_c_dimension i pp_c_dimension t pp_c_dimension e

  if Types.is_bool_type t_desc then

    if !Options.cpp then "bool" else "_Bool"

  else

    assert false (* Not a basic C type. Do not handle arrays or pointers *)

let pp_basic_c_type ?(pp_c_basic_type_desc=pp_c_basic_type_desc) ?(var_opt=None) fmt t =

     Machine_types.pp_c_var_type fmt v

     fprintf fmt "%s" (pp_c_basic_type_desc t)

    if is_basic_c_type  t then

       fprintf fmt "%a %s%a"

         (pp_basic_c_type ?pp_c_basic_type_desc ~var_opt) t

         var_id

         pp_suffix ()

      | Tarray (d, t')  ->

          fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in

        fprintf fmt "const "; aux t' pp_suffix

  in aux t (fun _ () -> ())

(*

let rec pp_c_initialize fmt t = 

  match (Types.repr t).Types.tdesc with

  | Types.Tint -> pp_print_string fmt "0"

  | Types.Tclock t' -> pp_c_initialize fmt t'

  | Types.Tbool -> pp_print_string fmt "0" 

  | Types.Treal when not !Options.mpfr -> pp_print_string fmt "0."

  | Types.Tarray (d, t') when Dimension.is_dimension_const d ->

    fprintf fmt "{%a}"

      (Utils.fprintf_list ~sep:"," (fun fmt _ -> pp_c_initialize fmt t'))

      (Utils.duplicate 0 (Dimension.size_const_dimension d))

  | _ -> assert false

 *)

  (* | Const_float r   -> pp_print_float fmt r *)

  | Const_string _

  | Const_modeid _ -> assert false (* string occurs in annotations not in C *)

let pp_reset_flag ?(indirect=true) pp_stru fmt stru =

  fprintf fmt "%a%s%s"

    pp_stru stru

let pp_reset_flag' ?indirect fmt =

  pp_reset_flag ?indirect pp_print_string fmt

    (pp_reset_flag' ~indirect:true) self (if b then 1 else 0)

(* Prints a value expression [v], with internal function calls only.

   [pp_var] is a printer for variables (typically [pp_c_var_read]),

   but an offset suffix may be added for array variables

*)

      (Machine_code_common.pp_val m) v;

     if Machine_code_common.is_memory m v then

       (* array memory vars are represented by an indirection to a local var

        *  with the right type, in order to avoid casting everywhere. *)

       if Types.is_array_type v.var_type

       && not (Types.is_real_type v.var_type && !Options.mpfr)

       then fprintf fmt "%a" pp_var v

       else fprintf fmt "%s->_reg.%a" self pp_var v

     else

       pp_var fmt v

(* Access to the value of a variable:

   - if it's not a scalar output, then its name is enough

   - otherwise, dereference it (it has been declared as a pointer,

     despite its scalar Lustre type)

   - moreover, dereference memory array variables.

*)

let pp_c_var_read ?(test_output=true) m fmt id =

  if Types.is_address_type id.var_type

  then

    if Machine_code_common.is_memory m id

    && not (Types.is_real_type id.var_type && !Options.mpfr)

  else

    if test_output && Machine_code_common.is_output m id

    then fprintf fmt "*%s" id.var_id

    else fprintf fmt "%s" id.var_id

(* Addressable value of a variable, the one that is passed around in calls:

   - if it's not a scalar non-output, then its name is enough

   - otherwise, reference it (it must be passed as a pointer,

     despite its scalar Lustre type)

*)

  if Types.is_address_type id.var_type

  then

    fprintf fmt "%s" id.var_id

  else

    if Machine_code_common.is_output m id

    then

      fprintf fmt "%s" id.var_id

    else

      fprintf fmt "&%s" id.var_id

(* Declaration of an input variable:

   - if its type is array/matrix/etc, then declare it as a mere pointer,

     in order to cope with unknown/parametric array dimensions, 

     as it is the case for generics

*)

  if !Options.ansi && Types.is_address_type id.var_type

  then

    pp_c_type ~var_opt:id (sprintf "(*%s)" id.var_id) fmt

  else

    pp_c_type ~var_opt:id id.var_id fmt id.var_type

(* Declaration of an output variable:

   - if its type is scalar, then pass its address

   - if its type is array/matrix/struct/etc, then declare it as a mere pointer,

     in order to cope with unknown/parametric array dimensions, 

     as it is the case for generics

*)

  if (not !Options.ansi) && Types.is_address_type id.var_type

  then

    pp_c_type ~var_opt:id (sprintf "(*%s)" id.var_id) fmt

(* Declaration of a local/mem variable:

   - if it's an array/matrix/etc, its size(s) should be

     known in order to statically allocate memory, 

     so we print the full type

*)

  if id.var_dec_const

  then

      (pp_c_type ?pp_c_basic_type_desc ~var_opt:id id.var_id) id.var_type

(* Declaration of a struct variable:

   - if it's an array/matrix/etc, we declare it as a pointer

*)

  if Types.is_array_type id.var_type

  then

    pp_c_type (sprintf "(*%s)" id.var_id) fmt

  else

    pp_c_type id.var_id  fmt id.var_type

let pp_c_decl_instance_var ?(ghost=false) fmt (name, (node, _)) =

    (pp_machine_memtype_name ~ghost) (node_name node)

  (* We select the last imported node with the name funname.

     The order of evaluation of dependencies should be

     compatible with overloading. (Not checked yet) *)

         match res with

         | Some _ -> res

         | None ->

           let decls = dep.content in

           let matched = fun t -> match t.top_decl_desc with

             | ImportedNode nd -> nd.nodei_id = funname

             | _ -> false

           in

           if List.exists matched decls then

             match (List.find matched decls).top_decl_desc with

             | ImportedNode nd -> Some nd

             | _ -> assert false

           else

             None) None dependencies in

  | None -> false

  | Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false)

(* Computes the depth to which multi-dimension array assignments should be expanded.

   It equals the maximum number of nested static array constructions accessible from root [v].

*)

  | Cst cst -> expansion_depth_cst cst

  | Var _ -> 0

  | Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0

  | Array vl    -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0

  | Access (v, _) -> max 0 (expansion_depth v - 1)

  | Power _  -> 0 (*1 + expansion_depth v*)

  | ResetFlag -> 0

  | _ -> 0

(*

let rec value_offsets v offsets =

 match v, offsets with

 | _                        , []          -> v

 | Power (v, n)             , _ :: q      -> value_offsets v q

 | Array vl                 , LInt r :: q -> value_offsets (List.nth vl !r) q

 | Cst (Const_array cl)     , LInt r :: q -> value_offsets (Cst (List.nth cl !r)) q

 | Fun (f, vl)              , _           -> Fun (f, List.map (fun v -> value_offsets v offsets) vl)

 | _                        , LInt r :: q -> value_offsets (Access (v, Cst (Const_int !r))) q

 | _                        , LVar i :: q -> value_offsets (Access (v, Var i)) q

*)

(* Computes the list of nested loop variables together with their dimension bounds.

   - LInt r stands for loop expansion (no loop variable, but int loop index)

   - LVar v stands for loop variable v

*)

  | _, 0 -> []

  | _ -> assert false

  let (int_loops, var_loops) =

    List.partition (function (_, LInt _) -> true | _ -> false) loop_vars

  | LVar v -> fprintf fmt "[%s]" v

  | LInt r -> fprintf fmt "[%d]" !r

  | LAcc i -> fprintf fmt "[%a]" pp_val i

  | Cst (Const_int _) -> true

  | Fun (_, vl)       -> List.for_all is_const_index vl

  | _                 -> false

(* Prints a value expression [v], with internal function calls only.

   [pp_var] is a printer for variables (typically [pp_c_var_read]),

   but an offset suffix may be added for array variables

*)

    fprintf fmt "(%a[])%a"

      (pp_c_type "") var_type

      (pp_print_braced (pp_c_const_suffix var_type)) ca

         (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)

  | Const_string _

  | Const_modeid _ -> assert false (* string occurs in annotations not in C *)

let rec pp_value_suffix ?(indirect=true) m self var_type loop_vars pp_var fmt value =

  (*eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)

  let pp_suffix = pp_suffix (pp_value_suffix ~indirect m self var_type [] pp_var) in

    pp_value_suffix ~indirect m self var_type ((x, LInt r)::q) pp_var fmt value

  | loop_var :: q, Array vl      ->

    fprintf fmt "(%a[])%a%a"

      (pp_c_type "") var_type

      (pp_print_braced (pp_value_suffix ~indirect m self var_type q pp_var)) vl

      pp_suffix [loop_var]

  | [], Array vl      ->

    fprintf fmt "(%a[])%a"

      (pp_c_type "") var_type

      (pp_print_braced (pp_value_suffix ~indirect m self var_type [] pp_var)) vl

  | _ :: q, Power (v, _)  ->

  | _, Fun (n, vl)   ->

    pp_basic_lib_fun (Types.is_int_type value.value_type) n

      (pp_value_suffix ~indirect m self var_type loop_vars pp_var) fmt vl

      ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_var fmt v

      (* array memory vars are represented by an indirection to a local var with the right type,

         in order to avoid casting everywhere. *)

      if Types.is_array_type v.var_type

      then fprintf fmt "%a%a" pp_var v pp_suffix loop_vars

      else fprintf fmt "%s%s_reg.%a%a"

          self (if indirect then "->" else ".") pp_var v pp_suffix loop_vars

      fprintf fmt "%s%s%a%a"

          self (if indirect then "->" else ".") pp_var v pp_suffix loop_vars

    else

      fprintf fmt "%a%a" pp_var v pp_suffix loop_vars

(*                       Struct Printing functions                                          *)

let print_machine_struct ?(ghost=false) fmt m =

      (pp_machine_memtype_name ~ghost) m.mname.node_id

         (fun fmt -> function

            | [] -> pp_print_nothing fmt ()

            | _ -> fprintf fmt "@,%a _reg;"

                     pp_machine_regtype_name m.mname.node_id)

       else

         pp_print_list

           ~pp_open_box:pp_open_vbox0

           ~pp_prologue:(fun fmt () ->

               fprintf fmt "@,@[%a {" pp_machine_regtype_name m.mname.node_id)

           ~pp_sep:pp_print_semicolon

           ~pp_eol:pp_print_semicolon'

           ~pp_epilogue:(fun fmt () -> fprintf fmt "}@] _reg;")

           pp_c_decl_struct_var)

      (pp_print_list

         ~pp_open_box:pp_open_vbox0

         ~pp_prologue:pp_print_cut

         ~pp_sep:pp_print_semicolon

         ~pp_eol:pp_print_semicolon'

(*                      Prototype Printing functions                                        *)

  fprintf fmt "void %a ()"

    pp_global_init_name baseNAME

  fprintf fmt "void %a ()"

    pp_global_clear_name baseNAME

    (pp_machine_memtype_name ~ghost:false) name

    pp_machine_alloc_name name

    (pp_print_parenthesized pp_c_decl_input_var) static

  fprintf fmt "void %a (%a * _alloc)"

    pp_machine_dealloc_name name

    (pp_machine_memtype_name ~ghost:false) name

  val pp_ghost_parameters: ?cut:bool -> formatter -> (string * (formatter -> string -> unit)) list -> unit

module EmptyGhostProto: MODIFIERS_GHOST_PROTO = struct

module Protos (Mod: MODIFIERS_GHOST_PROTO) = struct

      (fun fmt mem -> fprintf fmt "\\ghost %a" pp_ptr mem) fmt

      (name, mem)

    fprintf fmt "@[<v>void %a (%a%a *%s)%a@]"

      pp_machine_clear_reset_name name

      (pp_comma_list ~pp_eol:pp_print_comma

         pp_c_decl_input_var) static

      (pp_machine_memtype_name ~ghost:false) name

      self

      (Mod.pp_ghost_parameters ~cut:true) [mem, pp_mem_ghost name]

    fprintf fmt "@[<v>void %a (%a%a *%s)%a@]"

      pp_machine_set_reset_name name

      (pp_comma_list ~pp_eol:pp_print_comma

         pp_c_decl_input_var) static

      (pp_machine_memtype_name ~ghost:false) name

      self

      (Mod.pp_ghost_parameters ~cut:true) [mem, pp_mem_ghost name]

    fprintf fmt "@[<v>void %a (@[<v>%a%a%a *%s@])%a@]"

      pp_machine_step_name name

      (pp_comma_list ~pp_eol:pp_print_comma

         ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs

      (pp_comma_list ~pp_eol:pp_print_comma

         ~pp_epilogue:pp_print_cut pp_c_decl_output_var) outputs

      (pp_machine_memtype_name ~ghost:false) name

      self

      (Mod.pp_ghost_parameters ~cut:true) [mem, pp_mem_ghost name]

    fprintf fmt "void %a (%a%a *%s)"

      pp_machine_init_name name

      (pp_comma_list ~pp_eol:pp_print_comma

         pp_c_decl_input_var) static

      (pp_machine_memtype_name ~ghost:false) name

      self

    fprintf fmt "void %a (%a%a *%s)"

      pp_machine_clear_name name

      (pp_comma_list ~pp_eol:pp_print_comma

         pp_c_decl_input_var) static

      (pp_machine_memtype_name ~ghost:false) name

      self

    fprintf fmt "void %a (@[<v>%a%a@])"

      pp_machine_step_name name

      (pp_comma_list ~pp_eol:pp_print_comma

         ~pp_epilogue:pp_print_cut pp_c_decl_input_var) inputs

      (pp_comma_list pp_c_decl_output_var) outputs

let print_import_prototype fmt dep =

  fprintf fmt "#include \"%s.h\"" dep.name

  if dep.is_stateful then

    fprintf fmt "#include \"%s_alloc.h\"" dep.name

    pp_c_val m self pp_var fmt (Machine_code_common.mk_val (Var var) var.var_type)

    List.filter (fun v -> Types.(is_real_type (array_base_type v.var_type))) vars

    List.filter (fun c -> Types.(is_real_type (array_base_type c.const_type))) consts

   except for MPFR injection, where values are dynamically allocated

*)

    if Types.is_array_type typ

    then

      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"

        idx idx idx pp_c_dimension dim idx

        (aux (idx::indices)) (Types.array_element_type typ)

        fprintf fmt "%a%a" (pp_c_var m self pp_var) var pp_array_suffix indices in

(* type directed clear: useless wrt the lustre compilation model,

   except for MPFR injection, where values are dynamically allocated

*)

    if Types.is_array_type typ

    then

      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"

        idx idx idx pp_c_dimension dim idx

        (aux (idx::indices)) (Types.array_element_type typ)

        fprintf fmt "%a%a" (pp_c_var m self pp_var) var pp_array_suffix indices in

  (*** Common functions for main ***)

    "@[<v 2>if (traces) {@,\

     fprintf(f_%s, \"%%%s\\n\", %s);@,\

     fflush(f_%s);@]@,\

     }"

    file_suffix typ arg

    file_suffix

       if Types.is_int_type unclocked_t then

         fprintf fmt "_put_int(\"%s\", %s);@,%a"

           name var_id

           pp_file ("d", var_id)

       else if Types.is_bool_type unclocked_t then

         fprintf fmt "_put_bool(\"%s\", %s);@,%a"

           name var_id

           pp_file ("i", var_id)

       else if Types.is_real_type unclocked_t then

         if !Options.mpfr then

           fprintf fmt "_put_double(\"%s\", mpfr_get_d(%s, %s), %i);@,%a"

             name var_id (Mpfr.mpfr_rnd ()) !Options.print_prec_double

             pp_file (".*f",

                      string_of_int !Options.print_prec_double

                      ^ ", mpfr_get_d(" ^ var_id ^ ", MPFR_RNDN)")

         else

           fprintf fmt "_put_double(\"%s\", %s, %i);@,%a"

             name var_id !Options.print_prec_double

             pp_file (".*f",

                      string_of_int !Options.print_prec_double ^ ", " ^ var_id)

       else begin

         eprintf "Impossible to print the _put_xx for type %a@.@?"

           Types.print_ty var_type;

         assert false

       end) ()

  let idx = idx + 1 in (* we start from 1: in1, in2, ... *)

  let idx = idx + 1 in (* we start from 1: in1, in2, ... *)

     size_t l%s%i = strlen(dir) + strlen(prefix) + strlen(cst_char_suffix_%s%i);@,\

     free(f_%s%i_name);\

     @]"

    inout idx inout idx

    inout idx inout idx

    inout idx inout idx

    inout idx

    inout idx

    inout idx

    inout idx inout idx

    inout idx inout idx

    inout idx;

  if Types.is_real_type typ && !Options.mpfr

  then

  else

    fprintf fmt "%a = %a;"

      pp_var var_name

      pp_var value

(* type_directed assignment: array vs. statically sized type

   - [var_type]: type of variable to be assigned

   - [var_name]: name of variable to be assigned

   - [value]: assigned value

   - [pp_var]: printer for variables

*)

  (*eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)

      pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var)

      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"

        i i i pp_c_dimension d i

        (aux typ') q

        (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl

    | _ -> assert false

  begin

    reset_loop_counter ();

    (*reset_addr_counter ();*)

    aux var_type fmt reordered_loop_vars;

    (*eprintf "end pp_assign@.";*)

  end