soc2c.ml

(* Time-stamp: <modified the 10/07/2017 (at 13:12) by Erwan Jahier> *)


(* let put (os: out_channel) (fmt:('a, unit, string, unit) format4) : 'a = *)
(* 	Printf.kprintf (fun t -> output_string os t) fmt *)

open Printf
open Soc2cIdent
open Data


let rec (type_to_string2 : Data.t -> string) = 
  fun v -> 
    let str =
      match v with
        | Bool -> "bool"
        | Int  -> "int"
        | Real -> "real"
        | Extern s -> id2s s
        | Enum  (s, sl) -> id2s s
        | Struct (sid,_) -> (id2s sid)
        | Array (ty, sz) -> Printf.sprintf "%s_%d" (type_to_string2 ty) sz 
        | Alpha nb -> "alpha_"^(string_of_int nb) 
        | Alias(n,_) -> n
    in
    str

let inlined_soc = Soc2cDep.inlined_soc

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

(* Soc printer *)
type 'a soc_pp = {
  hfmt:  ('a, unit, string, unit) format4 -> 'a;
  cfmt:  ('a, unit, string, unit) format4 -> 'a;
  cput : string -> unit;
  hput : string -> unit;
  soc: Soc.t
}


let (string_of_soc_key : Soc.key -> string) = Soc2cIdent.get_soc_name


let string_of_var_expr = Soc2cDep.string_of_var_expr
open Soc

(* when an error occur, remove the generated c file (for the nonreg tests) *)
exception Delete_C_files

let var_expr_is_not_a_slice = function Slice _ -> false | _ -> true

let (gao2c : Soc.tbl -> 'a soc_pp -> Soc.gao -> unit) =
  fun stbl sp gao -> 
    let rec gao2str gao = 
      match gao with
        | Case(id, id_gao_l,_) -> ( 
          let to_case_str (v,gaol) =
            let gaol_str = (List.map gao2str gaol) in
            let gaol_block = String.concat "" gaol_str in
            (id2s v), gaol_block
          in
          let cases = List.map to_case_str id_gao_l in
          let ctx_opt = 
            let il,ol = sp.soc.profile in
            if List.mem_assoc id il || List.mem_assoc id ol then
              (if SocUtils.ctx_is_global sp.soc 
               then Soc2cUtil.ML_IO sp.soc.key 
               else Soc2cUtil.M_IO)
            else Soc2cUtil.Local 
          in
          let str = Soc2cUtil.gen_c_switch (Soc2cDep.ctx_var ctx_opt sp.soc id) cases in
          str
        )
        | Call(vel_out, Assign, vel_in,_) -> (
          let l = List.map2 (Soc2cDep.gen_assign_var_expr sp.soc) vel_out vel_in in
          String.concat "" l 
        )
        | Call(vel_out, Method((inst_name,sk),sname), vel_in,lxm) -> ( 
          let called_soc = SocUtils.find lxm sk stbl in
          let _, get_index = Soc2cInstances.to_array (sp.soc).instances in
          let index = get_index (inst_name,sk) in
          let step_arg = Printf.sprintf "ctx->%s_tab[%d]" (get_ctx_name sk) index in
          let ctx = step_arg in
          let step_arg = "&"^step_arg in
          List.iter (fun ve  -> assert(var_expr_is_not_a_slice ve)) vel_in;
          List.iter (fun ve  -> assert(var_expr_is_not_a_slice ve)) vel_out;
          Soc2cDep.gen_step_call sp.soc called_soc vel_out vel_in ctx sname step_arg
        )
        | Call(vel_out, Procedure sk, vel_in, lxm) -> (
          let called_soc = SocUtils.find lxm sk stbl in
          let ctx = get_ctx_name called_soc.key in
          (try
            List.iter (fun ve  -> assert(var_expr_is_not_a_slice ve)) vel_in;
            List.iter (fun ve  -> assert(var_expr_is_not_a_slice ve)) vel_out;
          with _ -> 
            print_string
              "*** Error. Slices in left part not yet supported in the C code generator, sorry\n";
            flush stdout;
            raise Delete_C_files
          ); 
          Soc2cDep.gen_step_call sp.soc called_soc vel_out vel_in ctx "step" ""
        )
    in
    sp.cput (gao2str gao)

let (step2c : Soc.tbl -> 'a soc_pp -> Soc.step_method -> unit) =
  fun stbl sp sm -> 
    if inlined_soc sp.soc.key then () (* don't generate code if inlined *) else
    (*     let sname = Soc2cDep.step_name sp.soc.key sm.name in *)
      let sname = Soc2cDep.step_name sp.soc.key sm.name in
      if sm.impl<>Extern then (
        let decl, def, ctype = Soc2cDep.get_step_prototype sm sp.soc in
        sp.hput (Printf.sprintf "%s\n" decl);
        sp.cput (Printf.sprintf "%s" def);
        (match sm.impl with
          | Extern -> ()
          | Predef ->
             (match sp.soc.key with
              | ("Lustre::eq",(Array _)::_,_) ->  
                 let str = Printf.sprintf
             "  *out = memcmp((const void *) i1, (const void *) i2, %s)==0;\n" ctype in
                 sp.cput str  
              | ("Lustre::eq",(Struct _)::_,_) -> 
                 let str = Printf.sprintf
             "  *out = memcmp((const void *) &i1, (const void *) &i2, %s)==0;\n" ctype in
                 sp.cput str  
              | ("Lustre::neq",(Array _)::_,_)  ->
                 let str = Printf.sprintf
             "  *out = !memcmp((const void *) i1, (const void *) i2, %s)==0;\n" ctype in
                 sp.cput str  
              | ("Lustre::neq",(Struct _)::_,_)  ->
                 let str = Printf.sprintf
             "  *out = !memcmp((const void *) &i1, (const void *) &i2, %s)==0;\n" ctype in
                 sp.cput str  
              | n -> sp.cput (Soc2cDep.get_predef_op n)
             )
          | Gaol(vl, gaol) -> (
            if Lv6MainArgs.global_opt.Lv6MainArgs.gen_wcet then 
              List.iter
                (fun v -> sp.cput (Soc2cUtil.string_of_flow_decl_w7annot gaol v))
                vl
            else
              List.iter (fun v -> sp.cput (Soc2cUtil.string_of_flow_decl v)) vl;
            sp.cput "\n"; 
            List.iter (gao2c stbl sp) gaol
          )
          | Iterator(it,it_soc_key,s) ->     
            let it_soc = SocUtils.find sm.lxm it_soc_key stbl in
            sp.cput (Soc2cDep.get_iterator sp.soc it it_soc s)
          | Boolred(i,j,k) -> 
            sp.cput (Soc2cDep.get_boolred sp.soc i j k)
          | Condact(k,el) -> 
            sp.cput (Soc2cDep.get_condact sp.soc (SocUtils.find sm.lxm k stbl) el)
        );
        sp.cput (sprintf "\n} // End of %s\n\n" sname)
      )
let (gen_instance_init_call : 'a soc_pp -> Soc.key * int -> unit) =
  fun sp (key,i) -> 
    let ctx_name = get_ctx_name key in
    if Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_inline_loops || i<4 then
      for k=0 to i-1 do
        sp.cfmt "\n    %s_reset(&ctx->%s_tab[%d]);" ctx_name ctx_name k
      done
    else (
      sp.cput (Printf.sprintf "  for (_i=0 ; _i<%d ; _i+=1){" i);
      sp.cput (Printf.sprintf "\n    %s_reset(&ctx->%s_tab[_i]);" ctx_name ctx_name);
      sp.cput "\n }"
    )

module KeySet = Set.Make(struct type t = Soc.key let compare = compare end)
           
let (get_used_soc : Soc.t -> KeySet.t) =
  fun soc -> (* dig into the soc for the list of socs it uses *)
  let rec get_soc_of_gao acc = function
    | Case(_,l,_) ->
       List.fold_left
         (fun acc (_,gaol) -> List.fold_left get_soc_of_gao acc gaol) acc l         
    | Call(_,Assign,_,_) -> acc
    | Call(_,Method((_,sk),_),_,_) 
    | Call(_,Procedure sk,_,_) -> KeySet.add sk acc
  in
  let get_soc_of_step acc sm =
    match sm.impl with
    | Gaol(_, gaol) -> List.fold_left get_soc_of_gao acc gaol
    | Iterator(_,sk,_)
    | Condact(sk,_) -> KeySet.add sk acc
    | _ -> acc
  in
  List.fold_left get_soc_of_step KeySet.empty soc.step
           
let one_file() = Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_one_file

(* soc2c
- creates c and h file(s) 
- updates/returns the list of created C files *)
let (soc2c : int -> out_channel -> out_channel -> Soc.tbl -> Soc.key ->
             string list -> Soc.t -> string list) = 
  fun pass hfile cfile stbl msoc_key cfiles_acc soc -> 
  if inlined_soc soc.key then cfiles_acc (* don't generate code if inlined *) else
    let ctx_name = get_ctx_name soc.key in
    let ctx_name_type = ctx_name^"_type" in
    if pass=1 then (
      (* Only for ctx of memoryless nodes + main node *)
      if SocUtils.ctx_is_global soc then
        Printf.kprintf (fun t -> output_string cfile t) "%s %s;\n" ctx_name_type ctx_name;
        cfiles_acc
    ) else (
      let base = string_of_soc_key soc.key  in
      let cfile,hfile,cfiles_acc =
        if one_file() || msoc_key = soc.key then cfile, hfile, cfiles_acc else
          let cfile =  (base^".c") in
          let hfile =  (base^".h") in
          let cfile_oc = open_out cfile in
          let hfile_oc = open_out hfile in
          (*open_out (base^".h"), *)
          Lv6util.entete cfile_oc "/*" "*/" ;
          Lv6util.entete hfile_oc "/*" "*/" ;
          Printf.fprintf cfile_oc "#include \"%s\"\n" hfile;
          Printf.fprintf hfile_oc "#include \"lustre_types.h\"\n";
          Printf.fprintf hfile_oc "#include \"lustre_consts.h\"\n";
          Printf.fprintf hfile_oc "#ifndef _%s_H_FILE \n" base;
          Printf.fprintf hfile_oc "#define _%s_H_FILE \n" base;
          flush cfile_oc;
          flush hfile_oc;
          cfile_oc, hfile_oc,
          (if List.mem cfile cfiles_acc then cfiles_acc else cfile::cfiles_acc)
      in
      let hfmt fmt = Printf.kprintf (fun t -> output_string hfile t) fmt in
      let cfmt fmt = Printf.kprintf (fun t -> output_string cfile t) fmt in
      let hput str = output_string hfile str in
      let cput str = output_string cfile str in
      let sp = { hfmt = hfmt; cfmt=cfmt; hput = hput; cput = cput; soc = soc } in
      (* include the header files that define the step functions used by the soc *)
      if (one_file()) then () else (
        let (used_soc:Soc.key list) = KeySet.elements (get_used_soc soc) in
        List.iter
          (fun sk -> if inlined_soc sk then () else
                       hfmt "#include \"%s.h\"\n" (string_of_soc_key sk)
          )
          used_soc;
        if msoc_key <> soc.key then hfmt "%s\n" (Soc2cDep.typedef_of_soc soc);
      );
      
      if SocUtils.is_memory_less soc then () else (
        cfmt "// Memory initialisation for %s\n" ctx_name;
        hfmt "void %s_reset(%s_type* ctx);\n" ctx_name ctx_name;
        cfmt "void %s_reset(%s_type* ctx){" ctx_name ctx_name;
        (* Call the reset_ctx functions of the soc instances *)
        if Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_inline_loops then () else
          sp.cput "\n  int _i;\n";
        List.iter (gen_instance_init_call sp)
                  (fst (Soc2cInstances.to_array soc.instances));
        (match soc.key with
         (* set the parameter fields that have a default value (arrow,fby) *)
         | (_,_,MemInit (ve)) ->
            assert(var_expr_is_not_a_slice ve);
            cfmt "  ctx->_memory = %s;" (string_of_var_expr soc ve)
         | _ -> ()
        );
        cfmt "\n}\n";
        if
          SocUtils.is_memory_less soc
        then () (*no ctx at all in this case ! *) 
        else if
          Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_global_ctx
        then
          (
            cfmt "\n// Initialisation of the  internal structure of %s\n" ctx_name;
            hfmt "void %s_init(%s_type* ctx);\n" ctx_name ctx_name;
            cfmt "void %s_init(%s_type* ctx){" ctx_name ctx_name;
            cfmt "
  // ctx->client_data = cdata;
  %s_reset(ctx);
 }
" ctx_name 
          )   
        else
          (
            cfmt "// Memory allocation for %s\n" ctx_name;
            hfmt "%s_type* %s_new_ctx();\n" ctx_name ctx_name;
            cfmt "%s_type* %s_new_ctx(){" ctx_name ctx_name;
            cfmt "

   %s_type* ctx = (%s_type*)calloc(1, sizeof(%s_type));
   // ctx->client_data = cdata;
   %s_reset(ctx);
  return ctx;
}
" ctx_name ctx_name ctx_name ctx_name) 
      );
      cfmt "// Step function(s) for %s\n" ctx_name;
      List.iter (step2c stbl sp) soc.step;
      ();
      if not (one_file() || msoc_key = soc.key) then (
        hfmt "#endif /* _%s_H_FILE */" base;
        close_out hfile;
        close_out cfile;
        Printf.printf "%s.h has been generated.\n" base;
        Printf.printf "%s.c has been generated.\n" base;
        flush stdout
      );
      cfiles_acc
      )

(****************************************************************************)
let (type_to_format_string : Data.t -> string) =
  function
    | Bool -> "%d"
    | Int -> "%d"
    | Real-> "%f"
    | Extern s -> "%d"
    | Enum  (s, sl) -> "%d" 
    | Struct (sid,_) -> "%s"
    | Array (ty, sz) -> "%s"
    | Alpha nb -> assert false 
    | Alias _ -> assert false 


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


module ItemKeySet = Set.Make(struct type t = Lic.item_key let compare = compare end)

(* To perform the topological sort of typedef. nf stands for "no
   fixpoint", that should be done by the caller. it is recursive just
   to deal with array of arrays *)
let  (find_typedep_nf : Lic.type_ -> Lic.item_key list) =
  fun t -> 
    let rec aux top = function
      | Lic.Bool_type_eff | Lic.Int_type_eff | Lic.Real_type_eff
      | Lic.External_type_eff _   | Lic.TypeVar _  
        ->  []
      | Lic.Abstract_type_eff(name,_) 
      | Lic.Enum_type_eff(name,_) -> if top then [] (* avoid self dep *) else [name] 
      | Lic.Array_type_eff(t,_) -> aux false t
      | Lic.Struct_type_eff(name, fl) -> 
        if not top then [name] else List.flatten(List.map (fun (_,(t,_)) -> aux false t) fl)
    in
    aux true t

let (is_extern_type: Lic.type_ -> bool) =
  function 
    | Lic.External_type_eff _ -> true
    | _  -> false


(* returns the typedef *)
let user_typedef licprg = 
  let to_c k t =
    Printf.sprintf "typedef %s;\n" (Soc2cUtil.lic_type_to_c t (long2s k))
  in
  let rec (typedef_to_string : Lic.item_key -> Lic.type_ -> string * ItemKeySet.t -> 
                               string * ItemKeySet.t) =
    fun k t acc ->
    (* topological sort according to type dep *)
    if is_extern_type t then acc else
      if ItemKeySet.mem k (snd acc) then acc else
        let type_list = find_typedep_nf t in
        let acc = List.fold_left 
                    (fun acc k -> 
                     match LicPrg.find_type licprg k with
                     | Some t -> typedef_to_string k t acc
                     | None -> acc (* occurs ? *)
                    ) 
                    acc type_list 
        in
        ((fst acc)^(to_c k t), ItemKeySet.add k (snd acc))
  in
  fst (LicPrg.fold_types typedef_to_string licprg ("",ItemKeySet.empty))
    
let (typedef_all : LicPrg.t -> Soc.tbl -> Soc.t -> string) =
  fun licprg soc_tbl main_soc ->
  (* We need to print the ctx typedef in a good order
       (w.r.t. typedef dependencies).  To do that, we traverse
       the tree of soc instances which root is the main soc. 
   *)

  (* Soc with memory can be used several times; hence we mark via this
       set the ones that have already been visited. *)
  let visited = KeySet.empty in
  let rec (soc_with_mem : string * KeySet.t -> Soc.t -> string * KeySet.t) =
    (* recursively traverse the soc dependancies to define the typedef
       in the good order (i.e., define before use) *)
    fun (acc,visited) soc ->
    if KeySet.mem soc.key visited then (acc,visited) else
      let visited = KeySet.add soc.key visited in
      let acc,visited =
        List.fold_left
          (fun (acc,visited) (iname, sk) ->
           let soc = SocUtils.find_no_exc sk soc_tbl in
           soc_with_mem (acc,visited) soc
          )
          (acc,visited) soc.instances
      in
      let acc = acc ^ (
          if one_file() || soc.key = main_soc.key then
            Soc2cDep.typedef_of_soc soc
          else
            (Printf.sprintf "#include \"%s.h\"\n" (string_of_soc_key soc.key))
        )
      in
      acc,visited
  in
  let soc_ctx_typedef_with_mem = 
    if SocUtils.ctx_is_global main_soc then "" else
      fst (soc_with_mem ("",visited) main_soc)
  in
  (* Then we still have to print memoryless soc that can not appear
       as a soc instance *)
  let soc_ctx_typedef_without_mem =
    let socs = Soc.SocMap.bindings soc_tbl in
    let socs = snd (List.split socs) in
    let memless_soc_to_string acc soc =
      if SocUtils.is_memory_less soc then acc^(Soc2cDep.typedef_of_soc soc) else acc
    in 
    List.fold_left  memless_soc_to_string "" socs
  in 
"// Memoryless soc ctx typedef \n"^soc_ctx_typedef_without_mem
  ^"// Memoryfull soc ctx typedef \n"^soc_ctx_typedef_with_mem
    



(****************************************************************************)
let rec (const_to_c: Lic.const -> string) =
  function
    | Lic.Bool_const_eff true -> "1"
    | Lic.Bool_const_eff false -> "0"
    | Lic.Int_const_eff i -> (sprintf "%s" i)
    | Lic.Real_const_eff r -> r
    | Lic.Extern_const_eff (s,t) -> (long2s s)
    | Lic.Abstract_const_eff (s,t,v,_) -> const_to_c v
    | Lic.Enum_const_eff   (s,Lic.Enum_type_eff(_,ll)) -> Lic.enum_to_string s ll
    | Lic.Enum_const_eff   _ -> assert false (* SNO *)
    | Lic.Struct_const_eff (fl, t) -> (
      let string_of_field = 
        function (id, veff) -> 
          (Lv6Id.to_string id)^" = "^ (const_to_c veff) 
      in
      let flst = List.map string_of_field fl in
(*       (string_of_type_eff t)^ *)
        "{"^(String.concat "; " flst)^"}"
    )
    | Lic.Array_const_eff (ctab, t) -> (
      let vl = List.map const_to_c ctab in
      "{"^(String.concat ", " vl)^"}"
    )
    | Lic.Tuple_const_eff   cl -> assert false

(* returns a pair: the lhs for the .h, the rhs for the .c
Indeed, arrays constant need to be defined in a .c
*)
let (constdef : LicPrg.t -> string*string) = 
  fun licprg -> 
    let to_c k = function
      | Lic.Extern_const_eff _ -> "",""
      (*       | Lic.Array_const_eff (ctab, Array_type_eff(_t,s)) -> ( *)
      | Lic.Array_const_eff (ctab, t) -> (
        let vl = List.map const_to_c ctab in
        let s = List.length vl in
        let tab_exp = "{"^(String.concat ", " vl)^"}" in
         Printf.sprintf "const %s [%i];\n" (long2s k) s, 
         Printf.sprintf "const %s [%i] = %s;\n" (long2s k) s tab_exp 
      )       
      | c  -> 
      Printf.sprintf "#define %s %s\n"
        (long2s k)
        (const_to_c c),""
    in
    let strh,strc = LicPrg.fold_consts
                (fun k t (acc_h,acc_c) ->
                 let h,c = to_c k t in
                 (acc_h^h,acc_c^c)) licprg  ("","")
    in
    (if strh = "" then "" else
       "\n// Constant definitions \n" ^ strh),
    (if strc = "" then "" else
       "\n// Constant definitions \n" ^ strc)

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

let (gen_memoryless_ctx : Soc.tbl -> string) =
  fun stbl -> 
    let do_soc sk soc acc =
      if (SocUtils.ctx_is_global soc) && not (inlined_soc soc.key) then 
        let ctx_name = get_ctx_name soc.key in
        let ctx_name_type = ctx_name^"_type" in    
        Printf.sprintf "%sextern %s %s;\n" acc ctx_name_type ctx_name 
      else
        acc
    in
    let acc = Soc.SocMap.fold do_soc stbl "" in
    if acc = "" then "" else 
      Printf.sprintf "\n// Allocation of memoryless ctx\n%s" acc

(* a shortcut *)
let io_transmit_mode () = Lv6MainArgs.global_opt.Lv6MainArgs.io_transmit_mode

(****************************************************************************)
let gen_main_loop_body inputs outputs soc ctx =
  if not Lv6MainArgs.global_opt.Lv6MainArgs.soc2c_global_ctx then
    (match io_transmit_mode () with
     | Lv6MainArgs.Stack ->
        let to_c_decl (n,t) = ((Soc2cUtil.data_type_to_c t n)^ ";\n  ") in
        let inputs_t  = List.map to_c_decl inputs in
        let outputs_t = List.map to_c_decl outputs in
        let inputs_decl = Printf.sprintf "\n  %s" (String.concat "" inputs_t) in
        let outputs_decl = Printf.sprintf "%s" (String.concat "" outputs_t) in
        let ctx_decl = if SocUtils.is_memory_less soc then "" else 
                         "  "^ctx^"_type* ctx = "^ ctx^"_new_ctx(NULL);\n"
        in
        inputs_decl ^ outputs_decl ^ ctx_decl
     | Lv6MainArgs.Heap -> ("
/* Context allocation */
" ^ (if SocUtils.is_memory_less soc then ctx^"_type* ctx = &"^ctx^";\n"
     else ctx^"_type* ctx = "^ ctx^"_new_ctx(NULL);")
                              )
        | Lv6MainArgs.HeapStack -> ("
/* Context allocation */
" ^ (if SocUtils.is_memory_less soc then ctx^""
     else ctx^"_type* ctx ;\n"^ ctx^"_reset(ctx);")
                                   )
    ) 
  else
    (match io_transmit_mode () with
     | Lv6MainArgs.Stack ->
        let to_c_decl (n,t) = ((Soc2cUtil.data_type_to_c t n)^ ";\n  ") in
        let inputs_t  = List.map to_c_decl inputs in
        let outputs_t = List.map to_c_decl outputs in
        let inputs_decl = Printf.sprintf "\n  %s" (String.concat "" inputs_t) in
        let outputs_decl = Printf.sprintf "%s" (String.concat "" outputs_t) in
        let ctx_decl = if SocUtils.is_memory_less soc then "" else 
                         ctx^"_type ctx_struct;\n  "^
                           ctx^"_type* ctx = &ctx_struct;\n  "^
                             ctx^"_init(ctx);"
        in
        inputs_decl ^ outputs_decl ^ ctx_decl
     | Lv6MainArgs.Heap -> ("
/* Context allocation */
" ^ (if SocUtils.is_memory_less soc then 
       ctx^"_type* ctx = &"^ctx^";\n"
     else (
       ctx^"_type ctx_struct;
    "^ctx^"_type* ctx = & ctx_struct;
    "^ctx^"_init(ctx);    
")
    )
                           )
     | Lv6MainArgs.HeapStack -> ("
/* Context allocation */
" ^ (if SocUtils.is_memory_less soc then ctx^""
     else ctx^"_type* ctx ;\n"^ ctx^"_reset(ctx);")
                                )
    )
      
(****************************************************************************)
let (gen_main_wcet_file : Soc.t -> string -> Soc.tbl -> unit) =
  fun soc base stbl -> 
    let mainfile = base^"_main.c" in
    let oc = open_out mainfile in

    let putc s = output_string oc s in
    let ctx = get_ctx_name soc.key in
    let step = Soc2cDep.step_name soc.key "step" in
    let inputs,outputs = soc.profile in
    Lv6util.entete oc "/*" "*/";
    putc  ("
#include <stdlib.h>
#include \""^base ^".h\" 
int main(){" ^ (gen_main_loop_body inputs outputs soc ctx));
    (match io_transmit_mode () with
      | Lv6MainArgs.Stack ->
        let i =  fst (List.split inputs) in
        let o = List.map (fun (n,t) -> match t with Data.Array(_,_) -> n | _ ->"&"^n) outputs in
        let io = String.concat "," (i@o) in
        let io = if SocUtils.is_memory_less soc then io else if io = "" then "ctx" else io^",ctx" in
        putc ("  " ^ step^"("^io^");
  return 0; 
}
"
        );
      | Lv6MainArgs.HeapStack -> assert false
      | Lv6MainArgs.Heap ->
        let io = if SocUtils.is_memory_less soc then  "" else "ctx"  in
        putc ("  " ^ step^"("^io^");
  return 0; 
}
"
        );
    );
    Printf.printf "%s has been generated.\n" mainfile; flush stdout;
    close_out oc


let (gen_loop_file : LicPrg.t -> Soc.t -> string -> out_channel -> Soc.tbl -> unit) =
  fun licprg soc base oc stbl -> 
    let putc s = output_string oc s in
    let ctx = get_ctx_name soc.key in
    let step = Soc2cDep.step_name soc.key "step" in
    let (n,_,_) = soc.key in
    let n = id2s n in
    let inputs,outputs = soc.profile in
    let inputs_io  = SocVar.expand_profile true false inputs  in
    let outputs_io = SocVar.expand_profile true false outputs in
    let inputs_exp = SocVar.expand_profile true true  inputs  in
    let outputs_exp= SocVar.expand_profile true true  outputs in
    Lv6util.entete oc "/*" "*/";
    putc  ("
#include <stdlib.h>
#include <stdio.h>
#include <unistd.h>
#include \""^base ^".h\" 
/* Print a promt ? ************************/
static int ISATTY;
/* MACROS DEFINITIONS ****************/
#ifndef TT
#define TT \"1\"
#endif
#ifndef FF
#define FF \"0\"
#endif
#ifndef BB
#define BB \"bottom\"
#endif
#ifdef CKCHECK
/* set this macro for testing output clocks */
#endif

/* Standard Input procedures **************/
_boolean _get_bool(char* n){
   char b[512];
   _boolean r = 0;
   int s = 1;
   char c;
   do {
      if(ISATTY) {
         if((s != 1)||(r == -1)) printf(\"\\a\");
         // printf(\"%s (1,t,T/0,f,F) ? \", n);
      }
      if(scanf(\"%s\", b)==EOF) exit(0);
      if (*b == 'q') exit(0);
      s = sscanf(b, \"%c\", &c);
      r = -1;
      if((c == '0') || (c == 'f') || (c == 'F')) r = 0;
      if((c == '1') || (c == 't') || (c == 'T')) r = 1;
   } while((s != 1) || (r == -1));
   return r;
}
_integer _get_int(char* n){
   char b[512];
   _integer r;
   int s = 1;
   do {
      if(ISATTY) {
         if(s != 1) printf(\"\\a\");
         //printf(\"%s (integer) ? \", n);
      }
      if(scanf(\"%s\", b)==EOF) exit(0);
      if (*b == 'q') exit(0);
      s = sscanf(b, \"%d\", &r);
   } while(s != 1);
   return r;
}
#define REALFORMAT ((sizeof(_real)==8)?\"%lf\":\"%f\")
_real _get_real(char* n){
   char b[512];
   _real r;
   int s = 1;
   do {
      if(ISATTY) {
         if(s != 1) printf(\"\\a\");
         //printf(\"%s (real) ? \", n);
      }
      if(scanf(\"%s\", b)==EOF) exit(0);
      if (*b == 'q') exit(0);
      s = sscanf(b, REALFORMAT, &r);
   } while(s != 1);
   return r;
}
/* Standard Output procedures **************/
void _put_bottom(char* n){
   if(ISATTY) printf(\"%s = \", n);
   printf(\"%s \", BB);
   if(ISATTY) printf(\"\\n\");
}
void _put_bool(char* n, _boolean _V){
   if(ISATTY) printf(\"%s = \", n);
   printf(\"%s \", (_V)? TT : FF);
   if(ISATTY) printf(\"\\n\");
}
void _put_int(char* n, _integer _V){
   if(ISATTY) printf(\"%s = \", n);
   printf(\"%d \", _V);
   if(ISATTY) printf(\"\\n\");
}
void _put_real(char* n, _real _V){
   if(ISATTY) printf(\"%s = \", n);
   printf(\"%f \", _V);
   if(ISATTY) printf(\"\\n\");
}"^(Soc2cExtern.gen_getters licprg)^"
/* Output procedures **********************/
#ifdef CKCHECK
void %s_BOT_n(void* cdata){
   _put_bottom(\"n\");
}
#endif
/* Output procedures **********************/
void "^n^"_O_n(void* cdata, _integer _V) {
   _put_int(\"n\", _V);
}"^ (gen_memoryless_ctx stbl) ^
"
/* Main procedure *************************/
int main(){
  int _s = 0;" ^ (
  (gen_main_loop_body inputs outputs soc ctx)
           )
    );
    let to_rif_decl (n,t) = ("\\\""^n^"\\\":" ^(type_to_string t)) in
    let inputs_t  = List.map to_rif_decl inputs_io in
    let outputs_t = List.map to_rif_decl outputs_io in
    let inputs_decl = Printf.sprintf "#inputs %s" (String.concat " " inputs_t) in
    let outputs_decl = Printf.sprintf "#outputs %s" (String.concat " " outputs_t) in
    
    putc  ("
  printf(\""^inputs_decl^"\\n\");
  printf(\""^outputs_decl^"\\n\");

  /* Main loop */
  ISATTY = isatty(0);
  while(1){
    if (ISATTY) printf(\"#step %d \\n\", _s+1);
    else if(_s) printf(\"\\n\");
    fflush(stdout);
    ++_s;
");
    List.iter (fun (id,t) -> 
      let t = type_to_string2 t in
      let str = 
        if io_transmit_mode () = Lv6MainArgs.Stack 
        then Printf.sprintf "    %s = _get_%s(\"%s\");\n" id t id 
        else Printf.sprintf "    ctx->%s = _get_%s(\"%s\");\n" id t id 
      in
      putc str
    ) 
      inputs_exp;
    let inputs_fmt  = List.map (fun (_,t) -> type_to_format_string t) inputs_io in
    let outputs_fmt = List.map (fun (_,t) -> type_to_format_string t) outputs_io in
    if io_transmit_mode () = Lv6MainArgs.Stack 
    then
      let i =  fst (List.split inputs) in
      let o = List.map
                (fun (n,t) -> match t with Data.Array(_,_) -> n | _ ->"&"^n)
                outputs
      in
      let io = String.concat "," (i@o) in
      let io = if SocUtils.is_memory_less soc then io
               else if io = "" then "ctx" else io^",ctx"
      in
      putc ("    " ^ step^"("^io^");
    // printf(\"" ^ (String.concat " " inputs_fmt)^ " #outs " ^ 
               (String.concat " " outputs_fmt)^ "\\n\"," ^
                 (String.concat "," (List.map (fun (id,_) -> ""^id )
                                              (inputs_exp@outputs_exp)))^ 
               ");
    printf(\"" ^ 
               (String.concat " " outputs_fmt)^ "\\n\"," ^
               (String.concat "," (List.map (fun (id,_) -> ""^id ) (outputs_exp)))^ 
               ");
  }"
    ) else (
      putc ("    " ^ step^"(ctx);
    // printf(\"" ^ (String.concat " " inputs_fmt)^ " #outs " ^ 
               (String.concat " " outputs_fmt)^ "\\n\"," ^
                 (String.concat "," (List.map (fun (id,_) -> "ctx->"^id )
                                              (inputs_exp@outputs_exp)))^ 
               ");
    printf(\"" ^ 
               (String.concat " " outputs_fmt)^ "\\n\"," ^
             (String.concat "," (List.map (fun (id,_) -> "ctx->"^id ) (outputs_exp)))^ 
             ");
  }"));
    putc "\n  return 1;
   
}
"


let (gen_loop_file4ogensim : Soc.t -> string -> out_channel -> Soc.tbl -> unit) =
  fun soc base oc stbl -> 
  let putc s = output_string oc s in
  let ctx = get_ctx_name soc.key in
  let step = Soc2cDep.step_name soc.key "step" in
  let inputs,outputs = soc.profile in
  let inputs_io  = SocVar.expand_profile true false inputs  in
  let outputs_io = SocVar.expand_profile true false outputs in
  let inputs_exp = SocVar.expand_profile true true  inputs  in
  let outputs_exp= SocVar.expand_profile true true  outputs in
  let define_define i (var_name,_) =
    putc (Printf.sprintf "#define _%s\t 0xe%07X\n" var_name ((i+1)*8));
  in
  Lv6util.entete oc "/*" "*/";
  
  putc  ("#include \""^base ^".h\"
                              
                              #define tickBegin  0xe0000000
                              ");
  List.iteri define_define (inputs_io@ outputs_io);
  
  putc ("\n int main(){\n" ^ gen_main_loop_body inputs outputs soc ctx);
  putc  ("
          /* Main loop */
          while(1){
          // notify the simulator that it is time to load the inputs from Lurette
          // to the specified address
          *((unsigned int*)tickBegin) = 0;
          // load inputs from the memory locations
          ");
  List.iter2 
    (fun (id,t)  (id_flat,_) -> 
     let t = Soc2cUtil.data_type_to_c t "" in
     let str = 
       Printf.sprintf "    %s = *((%s*)_%s);\n" id t id_flat
     in
     putc str
    ) 
    inputs_exp inputs_io;

  assert (io_transmit_mode () = Lv6MainArgs.Stack);

  let i =  fst (List.split inputs) in
  let o = List.map (fun (n,t) -> match t with Data.Array(_,_) -> n | _ ->"&"^n) outputs in
  let io = String.concat "," (i@o) in
  let io = if SocUtils.is_memory_less soc then io else if io = "" then "ctx" else io^",ctx" in
  putc ("    " ^ step^"("^io^");

// now write the output to the memory which will be output to Lurette
");
  List.iter2
    (fun (id,t) (id_flat,_) -> 
     let t = Soc2cUtil.data_type_to_c t "" in
     let str = Printf.sprintf "	 *((%s*)_%s) = %s;\n" t id id_flat in
     putc str
    ) 
    outputs_io outputs_exp;

  putc "}\n  return 1;       
        }        
        "

(****************************************************************************)
(* The entry point for lus2lic --to-c *)
let (f : Lv6MainArgs.t -> Soc.key -> Soc.tbl -> LicPrg.t -> unit) =
  fun args msoc stbl licprg -> 
  let socs = Soc.SocMap.bindings stbl in
  let socs = snd (List.split socs) in 
  (* XXX que fait-on pour les soc predef ? *)
  (*     let _, socs = List.partition is_predef socs in *)
  let base = 
    if args.Lv6MainArgs.outfile = "" then
      string_of_soc_key msoc 
    else
      Filename.basename (
          try Filename.chop_extension args.Lv6MainArgs.outfile
          with Invalid_argument _ -> args.Lv6MainArgs.outfile)
  in
  let hfile = base ^ ".h" in
  let cfile = base ^ ".c" in
  let ext_cfile = Printf.sprintf "%s_ext.c" base in
  let ext_hfile = Printf.sprintf "%s_ext.h" base in
  let loopfile = base^"_loop.c" in
  let occ = open_out cfile in
  let och = open_out hfile in
  let ocl = open_out loopfile in
  let types_h_oc = open_out "lustre_types.h" in
  let consts_h_oc = open_out "lustre_consts.h" in
  let consts_c_oc = open_out "lustre_consts.c" in
  let cfiles_acc = ["lustre_consts.c"; cfile] in
  let const_def_h, const_def_c = constdef licprg in
  let assign_ext_types_list = (Soc2cGenAssign.gen_used_types socs) in
  let main_soc = SocUtils.find_no_exc msoc stbl in
    (* Generate ext files if necessary  *)
  let needs_cfile, needs_hfile = 
    Soc2cExtern.gen_files main_soc stbl licprg ext_cfile ext_hfile hfile
  in
  Lv6util.entete consts_h_oc "/*" "*/" ;
  output_string consts_h_oc const_def_h;
  Lv6util.entete consts_c_oc "/*" "*/" ;
  output_string consts_c_oc "#include \"lustre_consts.h\"";
  output_string consts_c_oc const_def_c;
  Lv6util.entete types_h_oc "/*" "*/" ;
  output_string types_h_oc ("
#ifndef _SOC2C_PREDEF_TYPES
#define _SOC2C_PREDEF_TYPES
typedef int _boolean;
typedef int _integer;
typedef char* _string;
typedef double _real;
typedef double _double;
typedef float _float;
#define _false 0
#define _true 1
#endif
// end of _SOC2C_PREDEF_TYPES
// User typedef 
#ifndef _"^base^"_TYPES
#define _"^base^"_TYPES\n");
    output_string types_h_oc (user_typedef licprg);
    output_string types_h_oc ("#endif // enf of  _"^base^"_TYPES
"
  ^ (typedef_all licprg stbl main_soc )
  ^ (if needs_hfile then "#include \""^ base ^"_ext.h\"" else ""));
   
    try
    let putc s = output_string occ s in
    let puth s = output_string och s in
    Lv6util.entete occ "/*" "*/" ;
    Lv6util.entete och "/*" "*/";
    if Lv6MainArgs.global_opt.Lv6MainArgs.gen_wcet then (
      gen_loop_file4ogensim main_soc base ocl stbl;
      gen_main_wcet_file main_soc base stbl
    )
    else
      gen_loop_file licprg main_soc base ocl stbl;
    
    output_string och "
#include <stdlib.h>
#include <string.h>

#include \"lustre_types.h\"
#include \"lustre_consts.h\"

";

    if needs_hfile then puth (Printf.sprintf "#include \"%s\"\n" ext_hfile);
    puth (Printf.sprintf "#ifndef _%s_H_FILE\n" base);
    puth (Printf.sprintf "#define _%s_H_FILE\n" base);

    putc (Printf.sprintf "#include \"%s\"\n" hfile);
(*     putc (Soc2cExtern.cpy_declaration licprg); *)
    putc (Soc2cExtern.const_declaration licprg);
    let cfiles_acc = 
    if io_transmit_mode () = Lv6MainArgs.Heap then (
      puth "/////////////////////////////////////////////////\n";
      puth "//// Static allocation of memoryless soc ctx\n";
      let cfiles_acc = List.fold_left (soc2c 1 och occ stbl msoc) cfiles_acc socs in
      puth "/////////////////////////////////////////////////\n";
      cfiles_acc
    ) else cfiles_acc
    in
    putc "//// Defining step functions\n";
    let cfiles_acc = List.fold_left (soc2c 2 och occ stbl msoc) cfiles_acc socs in
    
    puth "/////////////////////////////////////////////////\n";
    if assign_ext_types_list <> [] then (
      output_string types_h_oc "// Defining array and extern types assignments \n";
      if Lv6MainArgs.global_opt.Lv6MainArgs.gen_wcet then 
        List.iter (fun t -> output_string types_h_oc (Soc2cGenAssign.f_forloop t))
                  assign_ext_types_list
      else
        List.iter (fun t -> output_string types_h_oc (Soc2cGenAssign.f t))
                  assign_ext_types_list
    );
    puth "#endif\n";
    flush occ; close_out occ;
    flush och; close_out och;
    flush ocl; close_out ocl;
    flush consts_h_oc; close_out consts_h_oc;
    flush consts_c_oc; close_out consts_c_oc;
    Printf.printf "%s has been generated.\n" loopfile;
    Printf.printf "%s has been generated.\n" hfile;
    Printf.printf "%s has been generated.\n" cfile;
    flush stdout;
    let node = args.Lv6MainArgs.main_node in
    let execfile = if args.Lv6MainArgs.outfile = "" then (node^".exec")
      else args.Lv6MainArgs.outfile 
    in
    let cflags = try Sys.getenv "CFLAGS" with Not_found -> "" in
    let ocsh = open_out (node ^".sh") in
    let main_file, ogensim_main_file, gcc = 
      if Lv6MainArgs.global_opt.Lv6MainArgs.gen_wcet then 
        base^"_main.c",base^"_loop.c","$gcc --specs=linux.specs -g" 
      else 
        loopfile, "I am a dead string...", "gcc"
    in
    let ogensim_exe = node^"4ogensim.exec" in
    let cfiles_acc = if needs_cfile then ext_cfile::cfiles_acc else cfiles_acc in
    let cfiles = String.concat " " cfiles_acc in
    let gcc, gcc_ogensim =
        Printf.sprintf "%s -o %s \\\n\t%s %s %s"
                       gcc execfile cfiles cflags main_file,
        Printf.sprintf "%s -o %s \\\n\t%s %s %s"
                       gcc ogensim_exe cfiles cflags ogensim_main_file
    in
    let main_step = (string_of_soc_key msoc)^"_step" in
    let gcc = if Lv6MainArgs.global_opt.Lv6MainArgs.gen_wcet then
        ("#!/bin/bash
set -x

otawa=\"true\"