Project

General

Profile

Download (31.5 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
open Utils.Format
13
open Lustre_types
14
open Machine_code_types
15
open Corelang
16
open Machine_code_common
17
open C_backend_common
18

    
19
module type MODIFIERS_SRC = sig
20
  val pp_predicates: dep_t list -> formatter -> machine_t list -> unit
21
  val pp_reset_spec: formatter -> machine_t list -> ident -> machine_t -> unit
22
  val pp_step_spec: formatter -> machine_t list -> ident -> machine_t -> unit
23
  val pp_step_instr_spec: machine_t -> ident -> formatter -> (int * instr_t) -> unit
24
end
25

    
26
module EmptyMod = struct
27
  let pp_predicates _ _ _ = ()
28
  let pp_reset_spec _ _ _ _ = ()
29
  let pp_step_spec _ _ _ _ = ()
30
  let pp_step_instr_spec _ _ _ _ = ()
31
end
32

    
33
module Main = functor (Mod: MODIFIERS_SRC) -> struct
34

    
35
  (********************************************************************************************)
36
  (*                    Instruction Printing functions                                        *)
37
  (********************************************************************************************)
38

    
39

    
40
  let rec merge_static_loop_profiles lp1 lp2 =
41
    match lp1, lp2 with
42
    | []      , _        -> lp2
43
    | _       , []       -> lp1
44
    | p1 :: q1, p2 :: q2 -> (p1 || p2) :: merge_static_loop_profiles q1 q2
45

    
46
  (* Returns a list of bool values, indicating whether the indices must be static or not *)
47
  let rec static_loop_profile v =
48
    match v.value_desc with
49
    | Cst cst  -> static_loop_profile_cst cst
50
    | Var _  -> []
51
    | Fun (_, vl) ->
52
      List.fold_right
53
        (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
54
    | Array vl    ->
55
      true :: List.fold_right
56
        (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
57
    | Access (v, _) ->
58
      begin match static_loop_profile v with [] -> [] | _ :: q -> q end
59
    | Power (v, _) -> false :: static_loop_profile v
60
  and static_loop_profile_cst cst =
61
    match cst with
62
      Const_array cl ->
63
      List.fold_right
64
        (fun c lp -> merge_static_loop_profiles lp (static_loop_profile_cst c))
65
        cl []
66
    | _ -> [] 
67

    
68

    
69
  (* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
70
     which may yield constant arrays in expressions.
71
     Type is needed to correctly print constant arrays.
72
  *)
73
  let pp_c_val m self pp_var fmt v =
74
    pp_value_suffix m self v.value_type [] pp_var fmt v
75

    
76
  let pp_basic_assign pp_var fmt typ var_name value =
77
    if Types.is_real_type typ && !Options.mpfr
78
    then
79
      Mpfr.pp_inject_assign pp_var fmt (var_name, value)
80
    else
81
      fprintf fmt "%a = %a;"
82
        pp_var var_name
83
        pp_var value
84

    
85
  (* type_directed assignment: array vs. statically sized type
86
     - [var_type]: type of variable to be assigned
87
     - [var_name]: name of variable to be assigned
88
     - [value]: assigned value
89
     - [pp_var]: printer for variables
90
  *)
91
  let pp_assign m self pp_var fmt var_type var_name value =
92
    let depth = expansion_depth value in
93
    (*eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
94
    let loop_vars = mk_loop_variables m var_type depth in
95
    let reordered_loop_vars = reorder_loop_variables loop_vars in
96
    let rec aux typ fmt vars =
97
      match vars with
98
      | [] ->
99
        pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var)
100
          fmt typ var_name value
101
      | (d, LVar i) :: q ->
102
        let typ' = Types.array_element_type typ in
103
        (*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
104
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
105
          i i i pp_c_dimension d i
106
          (aux typ') q
107
      | (d, LInt r) :: q ->
108
        (*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
109
        let typ' = Types.array_element_type typ in
110
        let szl = Utils.enumerate (Dimension.size_const_dimension d) in
111
        fprintf fmt "@[<v 2>{@,%a@]@,}"
112
          (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl
113
      | _ -> assert false
114
    in
115
    begin
116
      reset_loop_counter ();
117
      (*reset_addr_counter ();*)
118
      aux var_type fmt reordered_loop_vars;
119
      (*eprintf "end pp_assign@.";*)
120
    end
121

    
122
  let pp_machine_ pp_machine_name fn_name m self fmt inst =
123
    let (node, static) = try List.assoc inst m.minstances with Not_found ->
124
      eprintf "internal error: %s %s %s %s:@." fn_name m.mname.node_id self inst;
125
      raise Not_found
126
    in
127
    fprintf fmt "%a(%a%s->%s);"
128
      pp_machine_name (node_name node)
129
      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
130
         Dimension.pp_dimension) static
131
      self inst
132

    
133
  let pp_machine_reset =
134
    pp_machine_ pp_machine_reset_name "pp_machine_reset"
135

    
136
  let pp_machine_init =
137
    pp_machine_ pp_machine_init_name "pp_machine_init"
138

    
139
  let pp_machine_clear =
140
    pp_machine_ pp_machine_clear_name "pp_machine_clear"
141

    
142
  let pp_call m self pp_read pp_write fmt i
143
      (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
144
    try (* stateful node instance *)
145
      let n, _ = List.assoc i m.minstances in
146
      fprintf fmt "%a (%a%a%s->%s);"
147
        pp_machine_step_name (node_name n)
148
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
149
           (pp_c_val m self pp_read)) inputs
150
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
151
           pp_write) outputs
152
        self
153
        i
154
    with Not_found -> (* stateless node instance *)
155
      let n, _ = List.assoc i m.mcalls in
156
      fprintf fmt "%a (%a%a);"
157
        pp_machine_step_name (node_name n)
158
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
159
           (pp_c_val m self pp_read)) inputs
160
        (pp_print_list ~pp_sep:pp_print_comma pp_write) outputs
161

    
162
  let pp_basic_instance_call m self =
163
    pp_call m self (pp_c_var_read m) (pp_c_var_write m)
164

    
165
  let pp_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
166
    let pp_offset pp_var indices fmt var =
167
      fprintf fmt "%a%a"
168
        pp_var var
169
        (pp_print_list ~pp_sep:pp_print_nothing (fun fmt -> fprintf fmt "[%s]"))
170
        indices
171
    in
172
    let rec aux indices fmt typ =
173
      if Types.is_array_type typ
174
      then
175
        let dim = Types.array_type_dimension typ in
176
        let idx = mk_loop_var m () in
177
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
178
          idx idx idx pp_c_dimension dim idx
179
          (aux (idx::indices)) (Types.array_element_type typ)
180
      else
181
        let pp_read  = pp_offset (pp_c_var_read  m) indices in
182
        let pp_write = pp_offset (pp_c_var_write m) indices in
183
        pp_call m self pp_read pp_write fmt i inputs outputs
184
    in
185
    reset_loop_counter ();
186
    aux [] fmt (List.hd inputs).Machine_code_types.value_type
187

    
188
  let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
189
    fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
190
      (pp_c_val m self (pp_c_var_read m)) c
191
      (pp_print_list ~pp_prologue:pp_print_cut
192
         (pp_machine_instr dependencies m self)) tl
193
      (pp_print_list ~pp_prologue:pp_print_cut
194
         (pp_machine_instr dependencies m self)) el
195

    
196
  and pp_machine_instr dependencies (m: machine_t) self fmt instr =
197
    match get_instr_desc instr with
198
    | MNoReset _ -> ()
199
    | MReset i ->
200
      pp_machine_reset m self fmt i
201
    | MLocalAssign (i,v) ->
202
      pp_assign
203
        m self (pp_c_var_read m) fmt
204
        i.var_type (mk_val (Var i) i.var_type) v
205
    | MStateAssign (i,v) ->
206
      pp_assign
207
        m self (pp_c_var_read m) fmt
208
        i.var_type (mk_val (Var i) i.var_type) v
209
    | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->
210
      pp_machine_instr dependencies m self fmt
211
        (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
212
    | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
213
      pp_instance_call m self fmt i vl il
214
    | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
215
      fprintf fmt "%a = %s%a;"
216
        (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
217
        i
218
        (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
219
    | MStep (il, i, vl) ->
220
      pp_basic_instance_call m self fmt i vl il
221
    | MBranch (_, []) ->
222
      eprintf "internal error: C_backend_src.pp_machine_instr %a@."
223
        (pp_instr m) instr;
224
      assert false
225
    | MBranch (g, hl) ->
226
      if let t = fst (List.hd hl) in t = tag_true || t = tag_false
227
      then (* boolean case, needs special treatment in C because truth value is not unique *)
228
        (* may disappear if we optimize code by replacing last branch test with default *)
229
        let tl = try List.assoc tag_true  hl with Not_found -> [] in
230
        let el = try List.assoc tag_false hl with Not_found -> [] in
231
        pp_conditional dependencies m self fmt g tl el
232
      else (* enum type case *)
233
        (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
234
        fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
235
          (pp_c_val m self (pp_c_var_read m)) g
236
          (pp_print_list ~pp_open_box:pp_open_vbox0
237
             (pp_machine_branch dependencies m self)) hl
238
    | MSpec s ->
239
      fprintf fmt "@[/*@@ %s */@]@ " s
240
    | MComment s  ->
241
      fprintf fmt "/*%s*/@ " s
242

    
243
  and pp_machine_branch dependencies m self fmt (t, h) =
244
    fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
245
      pp_c_tag t
246
      (pp_print_list ~pp_open_box:pp_open_vbox0
247
         (pp_machine_instr dependencies m self)) h
248

    
249
  let pp_machine_nospec_instr dependencies m self fmt _i instr =
250
    pp_machine_instr dependencies m self fmt instr
251

    
252
  let pp_machine_step_instr dependencies m self fmt i instr =
253
    fprintf fmt "%a%a%a"
254
      (if i = 0 then
255
         (fun fmt () -> fprintf fmt "%a@,"
256
             (Mod.pp_step_instr_spec m self) (i, instr))
257
       else
258
         pp_print_nothing) ()
259
      (pp_machine_instr dependencies m self) instr
260
      (Mod.pp_step_instr_spec m self) (i+1, instr)
261

    
262
  (********************************************************************************************)
263
  (*                         C file Printing functions                                        *)
264
  (********************************************************************************************)
265

    
266
  let print_const_def fmt tdecl =
267
    let cdecl = const_of_top tdecl in
268
    if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
269
    then
270
      fprintf fmt "%a;"
271
        (pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type)
272
    else
273
      fprintf fmt "%a = %a;"
274
        (pp_c_type cdecl.const_id) cdecl.const_type
275
        pp_c_const cdecl.const_value
276

    
277
  let print_alloc_instance fmt (i, (m, static)) =
278
    fprintf fmt "_alloc->%s = %a %a;"
279
      i
280
      pp_machine_alloc_name (node_name m)
281
      (pp_print_parenthesized Dimension.pp_dimension) static
282

    
283
  let print_dealloc_instance fmt (i, (m, _)) =
284
    fprintf fmt "%a (_alloc->%s);"
285
      pp_machine_dealloc_name (node_name m)
286
      i
287

    
288
  let const_locals m =
289
    List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals
290

    
291
  let pp_c_decl_array_mem self fmt id =
292
    fprintf fmt "%a = (%a) (%s->_reg.%s)"
293
      (pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type
294
      (pp_c_type "(*)") id.var_type
295
      self
296
      id.var_id
297

    
298
  let print_alloc_const fmt m =
299
    pp_print_list
300
      ~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";")
301
      (pp_c_decl_local_var m) fmt (const_locals m)
302

    
303
  let print_alloc_array fmt vdecl =
304
    let base_type = Types.array_base_type vdecl.var_type in
305
    let size_types = Types.array_type_multi_dimension vdecl.var_type in
306
    let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in
307
    fprintf fmt
308
      "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,\
309
       assert(_alloc->%s);"
310
      vdecl.var_id
311
      (pp_c_type "") base_type
312
      Dimension.pp_dimension size_type
313
      (pp_c_type "") base_type
314
      vdecl.var_id
315

    
316
  let print_dealloc_array fmt vdecl =
317
    fprintf fmt "free (_alloc->_reg.%s);"
318
      vdecl.var_id
319

    
320
  let array_mems m =
321
    List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
322

    
323
  let print_alloc_code fmt m =
324
    fprintf fmt
325
      "%a *_alloc;@,\
326
       _alloc = (%a *) malloc(sizeof(%a));@,\
327
       assert(_alloc);@,\
328
       %a%areturn _alloc;"
329
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
330
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
331
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
332
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m)
333
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances
334

    
335
  let print_dealloc_code fmt m =
336
    fprintf fmt
337
      "%a%afree (_alloc);@,\
338
       return;"
339
      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array) (array_mems m)
340
      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance) m.minstances
341

    
342
  (* let print_stateless_init_code fmt m self =
343
   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
344
   *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
345
   *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
346
   *     (print_init_prototype self) (m.mname.node_id, m.mstatic)
347
   *     (\* array mems *\)
348
   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
349
   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
350
   *     (\* memory initialization *\)
351
   *     (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
352
   *     (Utils.pp_newline_if_non_empty m.mmemory)
353
   *     (\* sub-machines initialization *\)
354
   *     (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
355
   *     (Utils.pp_newline_if_non_empty m.minit)
356
   *
357
   * let print_stateless_clear_code fmt m self =
358
   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
359
   *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
360
   *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
361
   *     (print_clear_prototype self) (m.mname.node_id, m.mstatic)
362
   *     (\* array mems *\)
363
   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
364
   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
365
   *     (\* memory clear *\)
366
   *     (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
367
   *     (Utils.pp_newline_if_non_empty m.mmemory)
368
   *     (\* sub-machines clear*\)
369
   *     (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
370
   *     (Utils.pp_newline_if_non_empty m.minit) *)
371

    
372
  let pp_c_check m self fmt (loc, check) =
373
    fprintf fmt "@[<v>%a@,assert (%a);@]"
374
      Location.pp_c_loc loc
375
      (pp_c_val m self (pp_c_var_read m)) check
376

    
377
  let pp_print_function
378
      ~pp_prototype ~prototype
379
      ?(pp_spec=pp_print_nothing)
380
      ?(pp_local=pp_print_nothing) ?(base_locals=[])
381
      ?(pp_array_mem=pp_print_nothing) ?(array_mems=[])
382
      ?(pp_init_mpfr_local=pp_print_nothing)
383
      ?(pp_clear_mpfr_local=pp_print_nothing)
384
      ?(mpfr_locals=[])
385
      ?(pp_check=pp_print_nothing) ?(checks=[])
386
      ?(pp_extra=pp_print_nothing)
387
      ?(pp_instr=fun fmt _ _ -> pp_print_nothing fmt ()) ?(instrs=[])
388
      fmt =
389
    fprintf fmt
390
      "%a@[<v 2>%a {@,\
391
       %a%a\
392
       %a%a%a%a%areturn;@]@,\
393
       }"
394
      pp_spec ()
395
      pp_prototype prototype
396
      (* locals *)
397
      (pp_print_list
398
         ~pp_open_box:pp_open_vbox0
399
         ~pp_sep:pp_print_semicolon
400
         ~pp_eol:pp_print_semicolon
401
         pp_local)
402
      base_locals
403
      (* array mems *)
404
      (pp_print_list
405
         ~pp_open_box:pp_open_vbox0
406
         ~pp_sep:pp_print_semicolon
407
         ~pp_eol:pp_print_semicolon
408
         pp_array_mem)
409
      array_mems
410
      (* locals initialization *)
411
      (pp_print_list
412
         ~pp_epilogue:pp_print_cut
413
         pp_init_mpfr_local) (mpfr_vars mpfr_locals)
414
      (* check assertions *)
415
      (pp_print_list pp_check) checks
416
      (* instrs *)
417
      (pp_print_list_i
418
         ~pp_open_box:pp_open_vbox0
419
         ~pp_epilogue:pp_print_cut
420
         pp_instr) instrs
421
      (* locals clear *)
422
      (pp_print_list
423
         ~pp_epilogue:pp_print_cut
424
         pp_clear_mpfr_local) (mpfr_vars mpfr_locals)
425
      (* extra *)
426
      pp_extra ()
427

    
428
  let node_of_machine m = {
429
    top_decl_desc = Node m.mname;
430
    top_decl_loc = Location.dummy_loc;
431
    top_decl_owner = "";
432
    top_decl_itf = false
433
  }
434

    
435
  let print_stateless_code dependencies fmt m =
436
    let self = "__ERROR__" in
437
    if not (!Options.ansi && is_generic_node (node_of_machine m))
438
    then
439
      (* C99 code *)
440
      pp_print_function
441
        ~pp_prototype:print_stateless_prototype
442
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
443
        ~pp_local:(pp_c_decl_local_var m)
444
        ~base_locals:m.mstep.step_locals
445
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
446
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
447
        ~mpfr_locals:m.mstep.step_locals
448
        ~pp_check:(pp_c_check m self)
449
        ~checks:m.mstep.step_checks
450
        ~pp_instr:(pp_machine_nospec_instr dependencies m self)
451
        ~instrs:m.mstep.step_instrs
452
        fmt
453
    else
454
      (* C90 code *)
455
      let gen_locals, base_locals = List.partition (fun v ->
456
          Types.is_generic_type v.var_type) m.mstep.step_locals in
457
      let gen_calls = List.map (fun e ->
458
          let (id, _, _) = call_of_expr e
459
          in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
460
      pp_print_function
461
        ~pp_prototype:print_stateless_prototype
462
        ~prototype:(m.mname.node_id,
463
                    m.mstep.step_inputs @ gen_locals @ gen_calls,
464
                    m.mstep.step_outputs)
465
        ~pp_local:(pp_c_decl_local_var m)
466
        ~base_locals
467
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
468
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
469
        ~mpfr_locals:m.mstep.step_locals
470
        ~pp_check:(pp_c_check m self)
471
        ~checks:m.mstep.step_checks
472
        ~pp_instr:(pp_machine_nospec_instr dependencies m self)
473
        ~instrs:m.mstep.step_instrs
474
        fmt
475

    
476
  let print_reset_code machines dependencies self fmt m =
477
    pp_print_function
478
      ~pp_spec:(fun fmt () -> Mod.pp_reset_spec fmt machines self m)
479
      ~pp_prototype:(print_reset_prototype self)
480
      ~prototype:(m.mname.node_id, m.mstatic)
481
      ~pp_local:(pp_c_decl_local_var m)
482
      ~base_locals:(const_locals m)
483
      ~pp_instr:(pp_machine_nospec_instr dependencies m self)
484
      ~instrs:m.minit
485
      fmt
486

    
487
  let print_init_code self fmt m =
488
    let minit = List.map (fun i ->
489
        match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
490
    pp_print_function
491
      ~pp_prototype:(print_init_prototype self)
492
      ~prototype:(m.mname.node_id, m.mstatic)
493
      ~pp_array_mem:(pp_c_decl_array_mem self)
494
      ~array_mems:(array_mems m)
495
      ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
496
      ~mpfr_locals:m.mmemory
497
      ~pp_extra:(fun fmt () ->
498
          pp_print_list
499
            ~pp_open_box:pp_open_vbox0
500
            ~pp_epilogue:pp_print_cut
501
            (pp_machine_init m self)
502
            fmt minit)
503
      fmt
504

    
505
  let print_clear_code self fmt m =
506
    let minit = List.map (fun i ->
507
        match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
508
    pp_print_function
509
      ~pp_prototype:(print_clear_prototype self)
510
      ~prototype:(m.mname.node_id, m.mstatic)
511
      ~pp_array_mem:(pp_c_decl_array_mem self)
512
      ~array_mems:(array_mems m)
513
      ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
514
      ~mpfr_locals:m.mmemory
515
      ~pp_extra:(fun fmt () ->
516
          pp_print_list
517
            ~pp_open_box:pp_open_vbox0
518
            ~pp_epilogue:pp_print_cut
519
            (pp_machine_clear m self)
520
            fmt minit)
521
      fmt
522

    
523
  let print_step_code machines dependencies self fmt m =
524
    if not (!Options.ansi && is_generic_node (node_of_machine m))
525
    then
526
      (* C99 code *)
527
      pp_print_function
528
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self m)
529
        ~pp_prototype:(print_step_prototype self)
530
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
531
        ~pp_local:(pp_c_decl_local_var m)
532
        ~base_locals:m.mstep.step_locals
533
        ~pp_array_mem:(pp_c_decl_array_mem self)
534
        ~array_mems:(array_mems m)
535
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
536
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
537
        ~mpfr_locals:m.mstep.step_locals
538
        ~pp_check:(pp_c_check m self)
539
        ~checks:m.mstep.step_checks
540
        ~pp_instr:(pp_machine_step_instr dependencies m self)
541
        ~instrs:m.mstep.step_instrs
542
        fmt
543
    else
544
      (* C90 code *)
545
      let gen_locals, base_locals = List.partition (fun v ->
546
          Types.is_generic_type v.var_type) m.mstep.step_locals in
547
      let gen_calls = List.map (fun e ->
548
          let id, _, _ = call_of_expr e in
549
          mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
550
      pp_print_function
551
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self m)
552
        ~pp_prototype:(print_step_prototype self)
553
        ~prototype:(m.mname.node_id,
554
                    m.mstep.step_inputs @ gen_locals @ gen_calls,
555
                    m.mstep.step_outputs)
556
        ~pp_local:(pp_c_decl_local_var m)
557
        ~base_locals
558
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
559
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
560
        ~mpfr_locals:m.mstep.step_locals
561
        ~pp_check:(pp_c_check m self)
562
        ~checks:m.mstep.step_checks
563
        ~pp_instr:(pp_machine_step_instr dependencies m self)
564
        ~instrs:m.mstep.step_instrs
565
        fmt
566

    
567
  (********************************************************************************************)
568
  (*                     MAIN C file Printing functions                                       *)
569
  (********************************************************************************************)
570

    
571
  let pp_const_initialize m pp_var fmt const =
572
    let var = Machine_code_common.mk_val
573
        (Var (Corelang.var_decl_of_const const)) const.const_type in
574
    let rec aux indices value fmt typ =
575
      if Types.is_array_type typ
576
      then
577
        let dim = Types.array_type_dimension typ in
578
        let szl = Utils.enumerate (Dimension.size_const_dimension dim) in
579
        let typ' = Types.array_element_type typ in
580
        let value = match value with
581
          | Const_array ca -> List.nth ca
582
          | _ -> assert false in
583
        pp_print_list
584
          (fun fmt i -> aux (string_of_int i :: indices) (value i) fmt typ') fmt szl
585
      else
586
        let indices = List.rev indices in
587
        let pp_var_suffix fmt var =
588
          fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix indices in
589
        fprintf fmt "%a@,%a"
590
          (Mpfr.pp_inject_init pp_var_suffix) var
591
          (Mpfr.pp_inject_real pp_var_suffix pp_c_const) (var, value)
592
    in
593
    reset_loop_counter ();
594
    aux [] const.const_value fmt const.const_type
595

    
596
  let pp_const_clear pp_var fmt const =
597
    let m = Machine_code_common.empty_machine in
598
    let var = Corelang.var_decl_of_const const in
599
    let rec aux indices fmt typ =
600
      if Types.is_array_type typ
601
      then
602
        let dim = Types.array_type_dimension typ in
603
        let idx = mk_loop_var m () in
604
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
605
          idx idx idx pp_c_dimension dim idx
606
          (aux (idx::indices)) (Types.array_element_type typ)
607
      else
608
        let indices = List.rev indices in
609
        let pp_var_suffix fmt var =
610
          fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix indices in
611
        Mpfr.pp_inject_clear pp_var_suffix fmt var
612
    in
613
    reset_loop_counter ();
614
    aux [] fmt var.var_type
615

    
616
  let print_import_init fmt dep =
617
    let baseNAME = file_to_module_name dep.name in
618
    fprintf fmt "%a();" pp_global_init_name baseNAME
619

    
620
  let print_import_clear fmt dep =
621
    let baseNAME = file_to_module_name dep.name in
622
    fprintf fmt "%a();" pp_global_clear_name baseNAME
623

    
624
  let print_global_init_code fmt (basename, prog, dependencies) =
625
    let baseNAME = file_to_module_name basename in
626
    let constants = List.map const_of_top (get_consts prog) in
627
    fprintf fmt
628
      "@[<v 2>%a {@,\
629
       static %s init = 0;@,\
630
       @[<v 2>if (!init) { @,\
631
       init = 1;%a%a@]@,\
632
       }@,\
633
       return;@]@,\
634
       }"
635
      print_global_init_prototype baseNAME
636
      (pp_c_basic_type_desc Type_predef.type_bool)
637
      (* constants *)
638
      (pp_print_list
639
         ~pp_prologue:pp_print_cut
640
         (pp_const_initialize empty_machine (pp_c_var_read empty_machine)))
641
      (mpfr_consts constants)
642
      (* dependencies initialization *)
643
      (pp_print_list
644
         ~pp_prologue:pp_print_cut
645
         print_import_init) (List.filter (fun dep -> dep.local) dependencies)
646

    
647
  let print_global_clear_code fmt (basename, prog, dependencies) =
648
    let baseNAME = file_to_module_name basename in
649
    let constants = List.map const_of_top (get_consts prog) in
650
    fprintf fmt
651
      "@[<v 2>%a {@,\
652
       static %s clear = 0;@,\
653
       @[<v 2>if (!clear) { @,\
654
       clear = 1;%a%a@]@,\
655
       }@,\
656
       return;@]@,\
657
       }"
658
      print_global_clear_prototype baseNAME
659
      (pp_c_basic_type_desc Type_predef.type_bool)
660
      (* constants *)
661
      (pp_print_list
662
         ~pp_prologue:pp_print_cut
663
         (pp_const_clear (pp_c_var_read empty_machine))) (mpfr_consts constants)
664
      (* dependencies initialization *)
665
      (pp_print_list
666
         ~pp_prologue:pp_print_cut
667
         print_import_clear) (List.filter (fun dep -> dep.local) dependencies)
668

    
669
  let print_alloc_function fmt m =
670
    if (not !Options.static_mem) then
671
      (* Alloc functions, only if non static mode *)
672
      fprintf fmt
673
        "@[<v 2>%a {@,\
674
         %a%a@]@,\
675
         }@,\
676
         @[<v 2>%a {@,\
677
         %a%a@]@,\
678
         @,"
679
        print_alloc_prototype (m.mname.node_id, m.mstatic)
680
        print_alloc_const m
681
        print_alloc_code m
682
        print_dealloc_prototype m.mname.node_id
683
        print_alloc_const m
684
        print_dealloc_code m
685

    
686
  let print_mpfr_code self fmt m =
687
    if !Options.mpfr then
688
      fprintf fmt "@,@[<v>%a@,%a@]"
689
        (* Init function *)
690
        (print_init_code self) m
691
        (* Clear function *)
692
        (print_clear_code self) m
693

    
694
  (* TODO: ACSL
695
     - a contract machine shall not be directly printed in the C source
696
     - but a regular machine associated to a contract machine shall integrate
697
       the associated statements, updating its memories, at the end of the
698
       function body.
699
     - last one may print intermediate comment/acsl if/when they are present in
700
       the sequence of instruction
701
  *)
702
  let print_machine machines dependencies fmt m =
703
    if fst (get_stateless_status m) then
704
      (* Step function *)
705
      print_stateless_code dependencies fmt m
706
    else
707
      let self = mk_self m in
708
      fprintf fmt "@[<v>%a%a@,@,%a%a@]"
709
        print_alloc_function m
710
        (* Reset function *)
711
        (print_reset_code machines dependencies self) m
712
        (* Step function *)
713
        (print_step_code machines dependencies self) m
714
        (print_mpfr_code self) m
715

    
716
  let print_import_standard source_fmt () =
717
    fprintf source_fmt
718
      "@[<v>#include <assert.h>@,%a%a%a@]"
719
      (if Machine_types.has_machine_type ()
720
       then pp_print_endcut "#include <stdint.h>"
721
       else pp_print_nothing) ()
722
      (if not !Options.static_mem
723
       then pp_print_endcut "#include <stdlib.h>"
724
       else pp_print_nothing) ()
725
      (if !Options.mpfr
726
       then pp_print_endcut "#include <mpfr.h>"
727
       else pp_print_nothing) ()
728

    
729
  let print_extern_alloc_prototype fmt ind =
730
    let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs in
731
    fprintf fmt "extern %a;@,extern %a;"
732
      print_alloc_prototype (ind.nodei_id, static)
733
      print_dealloc_prototype ind.nodei_id
734

    
735
  let print_lib_c source_fmt basename prog machines dependencies =
736
    fprintf source_fmt
737
      "@[<v>\
738
       %a\
739
       %a@,\
740
       @,\
741
       %a@,\
742
       %a\
743
       %a\
744
       %a\
745
       %a\
746
       %a\
747
       %a\
748
       %a\
749
       @]@."
750
      print_import_standard ()
751
      print_import_prototype
752
      {
753
        local = true;
754
        name = basename;
755
        content = [];
756
        is_stateful=true (* assuming it is stateful *);
757
      }
758

    
759
      (* Print the svn version number and the supported C standard (C90 or C99) *)
760
      pp_print_version ()
761

    
762
      (* Print dependencies *)
763
      (pp_print_list
764
         ~pp_open_box:pp_open_vbox0
765
         ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
766
         print_import_prototype
767
         ~pp_epilogue:pp_print_cutcut) dependencies
768

    
769
      (* Print consts *)
770
      (pp_print_list
771
         ~pp_open_box:pp_open_vbox0
772
         ~pp_prologue:(pp_print_endcut "/* Global constants (definitions) */")
773
         print_const_def
774
         ~pp_epilogue:pp_print_cutcut) (get_consts prog)
775

    
776
      (* MPFR *)
777
      (if !Options.mpfr then
778
         fun fmt () ->
779
           fprintf fmt
780
             "@[<v>/* Global constants initialization */@,\
781
              %a@,\
782
              @,\
783
              /* Global constants clearing */@,\
784
              %a@]@,@,"
785
             print_global_init_code (basename, prog, dependencies)
786
             print_global_clear_code (basename, prog, dependencies)
787
       else pp_print_nothing) ()
788

    
789
      (if not !Options.static_mem then
790
         fun fmt () ->
791
           fprintf fmt
792
             "@[<v>%a%a@]@,@,"
793
             (pp_print_list
794
                ~pp_open_box:pp_open_vbox0
795
                ~pp_epilogue:pp_print_cut
796
                ~pp_prologue:(pp_print_endcut
797
                                "/* External allocation function prototypes */")
798
                (fun fmt dep ->
799
                   pp_print_list
800
                     ~pp_open_box:pp_open_vbox0
801
                     ~pp_epilogue:pp_print_cut
802
                     print_extern_alloc_prototype
803
                     fmt
804
                     (List.filter_map (fun decl -> match decl.top_decl_desc with
805
                          | ImportedNode ind when not ind.nodei_stateless ->
806
                            Some ind
807
                          | _ -> None) dep.content))) dependencies
808
             (pp_print_list
809
                ~pp_open_box:pp_open_vbox0
810
                ~pp_prologue:(pp_print_endcut
811
                                "/* Node allocation function prototypes */")
812
                ~pp_sep:pp_print_cutcut
813
                (fun fmt m ->
814
                   fprintf fmt "%a;@,%a;"
815
                     print_alloc_prototype (m.mname.node_id, m.mstatic)
816
                     print_dealloc_prototype m.mname.node_id)) machines
817
       else pp_print_nothing) ()
818

    
819
      (* Print the struct definitions of all machines. *)
820
      (pp_print_list
821
         ~pp_open_box:pp_open_vbox0
822
         ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
823
         ~pp_sep:pp_print_cutcut
824
         print_machine_struct
825
         ~pp_epilogue:pp_print_cutcut) machines
826

    
827
      (* Print the spec predicates *)
828
      (Mod.pp_predicates dependencies) machines
829

    
830
      (* Print nodes one by one (in the previous order) *)
831
      (pp_print_list
832
         ~pp_open_box:pp_open_vbox0
833
         ~pp_sep:pp_print_cutcut
834
         (print_machine machines dependencies)) machines
835

    
836
end
837

    
838
(* Local Variables: *)
839
(* compile-command:"make -C ../../.." *)
840
(* End: *)
(9-9/9)