Project

General

Profile

Download (32.6 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
  module GhostProto: MODIFIERS_GHOST_PROTO
21
  val pp_predicates: formatter -> machine_t list -> unit
22
  val pp_set_reset_spec: formatter -> ident -> ident -> machine_t -> unit
23
  val pp_clear_reset_spec: formatter -> ident -> ident -> machine_t -> unit
24
  val pp_step_spec: formatter -> machine_t list -> ident -> ident -> machine_t -> unit
25
  val pp_step_instr_spec: machine_t -> ident -> ident -> formatter -> instr_t -> unit
26
  val pp_ghost_parameter: ident -> formatter -> ident option -> unit
27
end
28

    
29
module EmptyMod = struct
30
  module GhostProto = EmptyGhostProto
31
  let pp_predicates _ _ = ()
32
  let pp_set_reset_spec _ _ _ _ = ()
33
  let pp_clear_reset_spec _ _ _ _ = ()
34
  let pp_step_spec _ _ _ _ _ = ()
35
  let pp_step_instr_spec _ _ _ _ _ = ()
36
  let pp_ghost_parameter _ _ _ = ()
37
end
38

    
39
module Main = functor (Mod: MODIFIERS_SRC) -> struct
40

    
41
  module Protos = Protos(Mod.GhostProto)
42

    
43
  (********************************************************************************************)
44
  (*                    Instruction Printing functions                                        *)
45
  (********************************************************************************************)
46

    
47

    
48
  let rec merge_static_loop_profiles lp1 lp2 =
49
    match lp1, lp2 with
50
    | []      , _        -> lp2
51
    | _       , []       -> lp1
52
    | p1 :: q1, p2 :: q2 -> (p1 || p2) :: merge_static_loop_profiles q1 q2
53

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

    
76

    
77
  (* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
78
     which may yield constant arrays in expressions.
79
     Type is needed to correctly print constant arrays.
80
  *)
81
  let pp_c_val m self pp_var fmt v =
82
    pp_value_suffix m self v.value_type [] pp_var fmt v
83

    
84
  let pp_machine_ pp_machine_name fn_name m fmt ?inst self mem =
85
    let name, is_arrow, static =
86
      match inst with
87
      | Some inst ->
88
        let node, static = try List.assoc inst m.minstances with Not_found ->
89
          eprintf "internal error: %s %s %s %s:@."
90
            fn_name m.mname.node_id self inst;
91
          raise Not_found
92
        in
93
        node_name node, Arrow.td_is_arrow node, static
94
      | None ->
95
        m.mname.node_id, false, []
96
    in
97
    let is_arrow_reset = is_arrow && fn_name = "pp_machine_set_reset" in
98
    fprintf fmt "%a(%a%s%a)%a;"
99
      (if is_arrow_reset then
100
         (fun fmt -> fprintf fmt "%s_reset")
101
       else
102
         pp_machine_name) name
103
      (pp_comma_list ~pp_eol:pp_print_comma Dimension.pp_dimension) static
104
      self
105
      (pp_print_option (fun fmt -> fprintf fmt "->%s")) inst
106
      (if is_arrow_reset then pp_print_nothing else Mod.pp_ghost_parameter mem)
107
      inst
108

    
109
  let pp_machine_set_reset m self mem fmt inst =
110
    pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst
111
      self mem
112

    
113
  let pp_machine_clear_reset m self mem fmt =
114
    pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt
115
      self mem
116

    
117
  let pp_machine_init m self mem fmt inst =
118
    pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self mem
119

    
120
  let pp_machine_clear m self mem fmt inst =
121
    pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self mem
122

    
123
  let pp_call m self mem pp_read pp_write fmt i inputs outputs =
124
    try (* stateful node instance *)
125
      let n, _ = List.assoc i m.minstances in
126
      fprintf fmt "%a(%a%a%s->%s)%a;"
127
        pp_machine_step_name (node_name n)
128
        (pp_comma_list ~pp_eol:pp_print_comma
129
           (pp_c_val m self pp_read)) inputs
130
        (pp_comma_list ~pp_eol:pp_print_comma
131
           pp_write) outputs
132
        self
133
        i
134
        (Mod.pp_ghost_parameter mem) (Some i)
135
    with Not_found -> (* stateless node instance *)
136
      let n, _ = List.assoc i m.mcalls in
137
      fprintf fmt "%a(%a%a);"
138
        pp_machine_step_name (node_name n)
139
        (pp_comma_list ~pp_eol:pp_print_comma
140
           (pp_c_val m self pp_read)) inputs
141
        (pp_comma_list pp_write) outputs
142

    
143
  let pp_basic_instance_call m self mem =
144
    pp_call m self mem (pp_c_var_read m) (pp_c_var_write m)
145

    
146
  let pp_arrow_call m self mem fmt i outputs =
147
    match outputs with
148
    | [x] ->
149
      fprintf fmt "%a = %a(%s->%s)%a;"
150
        (pp_c_var_read m) x
151
        pp_machine_step_name Arrow.arrow_id
152
        self
153
        i
154
        (Mod.pp_ghost_parameter mem) (Some i)
155
    | _ -> assert false
156

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

    
180
  let rec pp_conditional dependencies m self mem fmt c tl el =
181
    let pp_machine_instrs =
182
      pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
183
        (pp_machine_instr dependencies m self mem) in
184
    let pp_cond = pp_c_val m self (pp_c_var_read m) in
185
    match tl, el with
186
    | [], _ :: _ ->
187
      fprintf fmt "@[<v 2>if (!%a) {%a@]@,}"
188
        pp_cond c
189
        pp_machine_instrs el
190
    | _, [] ->
191
      fprintf fmt "@[<v 2>if (%a) {%a@]@,}"
192
        pp_cond c
193
        pp_machine_instrs tl
194
    | _, _ ->
195
      fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
196
        pp_cond c
197
        pp_machine_instrs tl
198
        pp_machine_instrs el
199

    
200
  and pp_machine_instr dependencies m self mem fmt instr =
201
    let pp_instr fmt instr = match get_instr_desc instr with
202
      | MNoReset _ -> ()
203
      | MSetReset inst ->
204
        pp_machine_set_reset m self mem fmt inst
205
      | MClearReset ->
206
        fprintf fmt "%t@,%a"
207
          (pp_machine_clear_reset m self mem) pp_label reset_label
208
      | MResetAssign b ->
209
        pp_reset_assign self fmt b
210
      | MLocalAssign (i, v) ->
211
        pp_assign m self (pp_c_var_read m) fmt (i, v)
212
      | MStateAssign (i, v) ->
213
        pp_assign m self (pp_c_var_read m) fmt (i, v)
214
      | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->
215
        pp_machine_instr dependencies m self mem fmt
216
          (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
217
      | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
218
        pp_instance_call m self mem fmt i vl il
219
      | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
220
        fprintf fmt "%a = %s%a;"
221
          (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
222
          i
223
          (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
224
      | MStep (il, i, vl) ->
225
        let td, _ = List.assoc i m.minstances in
226
        if Arrow.td_is_arrow td then
227
          pp_arrow_call m self mem fmt i il
228
        else
229
          pp_basic_instance_call m self mem fmt i vl il
230
      | MBranch (_, []) ->
231
        eprintf "internal error: C_backend_src.pp_machine_instr %a@."
232
          (pp_instr m) instr;
233
        assert false
234
      | MBranch (g, hl) ->
235
        if let t = fst (List.hd hl) in t = tag_true || t = tag_false
236
        then (* boolean case, needs special treatment in C because truth value is not unique *)
237
          (* may disappear if we optimize code by replacing last branch test with default *)
238
          let tl = try List.assoc tag_true  hl with Not_found -> [] in
239
          let el = try List.assoc tag_false hl with Not_found -> [] in
240
          let no_noreset = List.filter (fun i -> match i.instr_desc with
241
              | MNoReset _ -> false
242
              | _ -> true)
243
          in
244
          pp_conditional dependencies m self mem fmt g
245
            (no_noreset tl) (no_noreset el)
246
        else (* enum type case *)
247
          (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
248
          fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
249
            (pp_c_val m self (pp_c_var_read m)) g
250
            (pp_print_list ~pp_open_box:pp_open_vbox0
251
               (pp_machine_branch dependencies m self mem)) hl
252
      | MSpec s ->
253
        fprintf fmt "@[/*@@ %s */@]@ " s
254
      | MComment s  ->
255
        fprintf fmt "/*%s*/@ " s
256
    in
257
    fprintf fmt "%a%a" pp_instr instr (Mod.pp_step_instr_spec m self mem) instr
258

    
259
  and pp_machine_branch dependencies m self mem fmt (t, h) =
260
    fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
261
      pp_c_tag t
262
      (pp_print_list ~pp_open_box:pp_open_vbox0
263
         (pp_machine_instr dependencies m self mem)) h
264

    
265
  (* let pp_machine_nospec_instr dependencies m self fmt instr =
266
   *   pp_machine_instr dependencies m self fmt instr
267
   *
268
   * let pp_machine_step_instr dependencies m self mem fmt instr =
269
   *   fprintf fmt "%a%a"
270
   *     (pp_machine_instr dependencies m self) instr
271
   *     (Mod.pp_step_instr_spec m self mem) instr *)
272

    
273
  (********************************************************************************************)
274
  (*                         C file Printing functions                                        *)
275
  (********************************************************************************************)
276

    
277
  let print_const_def fmt tdecl =
278
    let cdecl = const_of_top tdecl in
279
    if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
280
    then
281
      fprintf fmt "%a;"
282
        (pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type)
283
    else
284
      fprintf fmt "%a = %a;"
285
        (pp_c_type cdecl.const_id) cdecl.const_type
286
        pp_c_const cdecl.const_value
287

    
288
  let print_alloc_instance fmt (i, (m, static)) =
289
    fprintf fmt "_alloc->%s = %a %a;"
290
      i
291
      pp_machine_alloc_name (node_name m)
292
      (pp_print_parenthesized Dimension.pp_dimension) static
293

    
294
  let print_dealloc_instance fmt (i, (m, _)) =
295
    fprintf fmt "%a (_alloc->%s);"
296
      pp_machine_dealloc_name (node_name m)
297
      i
298

    
299
  let const_locals m =
300
    List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals
301

    
302
  let pp_c_decl_array_mem self fmt id =
303
    fprintf fmt "%a = (%a) (%s->_reg.%s)"
304
      (pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type
305
      (pp_c_type "(*)") id.var_type
306
      self
307
      id.var_id
308

    
309
  let print_alloc_const fmt m =
310
    pp_print_list
311
      ~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";")
312
      (pp_c_decl_local_var m) fmt (const_locals m)
313

    
314
  let print_alloc_array fmt vdecl =
315
    let base_type = Types.array_base_type vdecl.var_type in
316
    let size_types = Types.array_type_multi_dimension vdecl.var_type in
317
    let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in
318
    fprintf fmt
319
      "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,\
320
       assert(_alloc->%s);"
321
      vdecl.var_id
322
      (pp_c_type "") base_type
323
      Dimension.pp_dimension size_type
324
      (pp_c_type "") base_type
325
      vdecl.var_id
326

    
327
  let print_dealloc_array fmt vdecl =
328
    fprintf fmt "free (_alloc->_reg.%s);"
329
      vdecl.var_id
330

    
331
  let array_mems m =
332
    List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
333

    
334
  let print_alloc_code fmt m =
335
    fprintf fmt
336
      "%a *_alloc;@,\
337
       _alloc = (%a *) malloc(sizeof(%a));@,\
338
       assert(_alloc);@,\
339
       %a%areturn _alloc;"
340
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
341
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
342
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
343
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m)
344
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances
345

    
346
  let print_dealloc_code fmt m =
347
    fprintf fmt
348
      "%a%afree (_alloc);@,\
349
       return;"
350
      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array) (array_mems m)
351
      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance) m.minstances
352

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

    
383
  let pp_c_check m self fmt (loc, check) =
384
    fprintf fmt "@[<v>%a@,assert (%a);@]"
385
      Location.pp_c_loc loc
386
      (pp_c_val m self (pp_c_var_read m)) check
387

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

    
439
  let node_of_machine m = {
440
    top_decl_desc = Node m.mname;
441
    top_decl_loc = Location.dummy_loc;
442
    top_decl_owner = "";
443
    top_decl_itf = false
444
  }
445

    
446
  let print_stateless_code machines dependencies fmt m =
447
    let self = "__ERROR__" in
448
    if not (!Options.ansi && is_generic_node (node_of_machine m))
449
    then
450
      (* C99 code *)
451
      pp_print_function
452
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self self m)
453
        ~pp_prototype:Protos.print_stateless_prototype
454
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
455
        ~pp_local:(pp_c_decl_local_var m)
456
        ~base_locals:m.mstep.step_locals
457
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
458
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
459
        ~mpfr_locals:m.mstep.step_locals
460
        ~pp_check:(pp_c_check m self)
461
        ~checks:m.mstep.step_checks
462
        ~pp_instr:(pp_machine_instr dependencies m self self)
463
        ~instrs:m.mstep.step_instrs
464
        fmt
465
    else
466
      (* C90 code *)
467
      let gen_locals, base_locals = List.partition (fun v ->
468
          Types.is_generic_type v.var_type) m.mstep.step_locals in
469
      let gen_calls = List.map (fun e ->
470
          let (id, _, _) = call_of_expr e
471
          in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
472
      pp_print_function
473
        ~pp_prototype:Protos.print_stateless_prototype
474
        ~prototype:(m.mname.node_id,
475
                    m.mstep.step_inputs @ gen_locals @ gen_calls,
476
                    m.mstep.step_outputs)
477
        ~pp_local:(pp_c_decl_local_var m)
478
        ~base_locals
479
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
480
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
481
        ~mpfr_locals:m.mstep.step_locals
482
        ~pp_check:(pp_c_check m self)
483
        ~checks:m.mstep.step_checks
484
        ~pp_instr:(pp_machine_instr dependencies m self self)
485
        ~instrs:m.mstep.step_instrs
486
        fmt
487

    
488
  let print_clear_reset_code dependencies self mem fmt m =
489
    pp_print_function
490
      ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt self mem m)
491
      ~pp_prototype:(Protos.print_clear_reset_prototype self mem)
492
      ~prototype:(m.mname.node_id, m.mstatic)
493
      ~pp_local:(pp_c_decl_local_var m)
494
      ~base_locals:(const_locals m)
495
      ~pp_instr:(pp_machine_instr dependencies m self mem)
496
      ~instrs:[mk_branch
497
                 (mk_val ResetFlag Type_predef.type_bool)
498
                 ["true", mkinstr (MResetAssign false) :: m.minit]]
499
      fmt
500

    
501
  let print_set_reset_code dependencies self mem fmt m =
502
    pp_print_function
503
      ~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m)
504
      ~pp_prototype:(Protos.print_set_reset_prototype self mem)
505
      ~prototype:(m.mname.node_id, m.mstatic)
506
      ~pp_instr:(pp_machine_instr dependencies m self mem)
507
      ~instrs:[mkinstr (MResetAssign true)]
508
      fmt
509

    
510
  let print_init_code self fmt m =
511
    let minit = List.map (fun i ->
512
        match get_instr_desc i with
513
        | MSetReset i -> i
514
        | _ -> assert false)
515
        m.minit in
516
    pp_print_function
517
      ~pp_prototype:(Protos.print_init_prototype self)
518
      ~prototype:(m.mname.node_id, m.mstatic)
519
      ~pp_array_mem:(pp_c_decl_array_mem self)
520
      ~array_mems:(array_mems m)
521
      ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
522
      ~mpfr_locals:m.mmemory
523
      ~pp_extra:(fun fmt () ->
524
          pp_print_list
525
            ~pp_open_box:pp_open_vbox0
526
            ~pp_epilogue:pp_print_cut
527
            (pp_machine_init m self self)
528
            fmt minit)
529
      fmt
530

    
531
  let print_clear_code self fmt m =
532
    let minit = List.map (fun i ->
533
        match get_instr_desc i with
534
        | MSetReset i -> i
535
        | _ -> assert false) m.minit in
536
    pp_print_function
537
      ~pp_prototype:(Protos.print_clear_prototype self)
538
      ~prototype:(m.mname.node_id, m.mstatic)
539
      ~pp_array_mem:(pp_c_decl_array_mem self)
540
      ~array_mems:(array_mems m)
541
      ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
542
      ~mpfr_locals:m.mmemory
543
      ~pp_extra:(fun fmt () ->
544
          pp_print_list
545
            ~pp_open_box:pp_open_vbox0
546
            ~pp_epilogue:pp_print_cut
547
            (pp_machine_clear m self self)
548
            fmt minit)
549
      fmt
550

    
551
  let print_step_code machines dependencies self mem fmt m =
552
    if not (!Options.ansi && is_generic_node (node_of_machine m))
553
    then
554
      (* C99 code *)
555
      pp_print_function
556
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
557
        ~pp_prototype:(Protos.print_step_prototype self mem)
558
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
559
        ~pp_local:(pp_c_decl_local_var m)
560
        ~base_locals:m.mstep.step_locals
561
        ~pp_array_mem:(pp_c_decl_array_mem self)
562
        ~array_mems:(array_mems m)
563
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
564
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
565
        ~mpfr_locals:m.mstep.step_locals
566
        ~pp_check:(pp_c_check m self)
567
        ~checks:m.mstep.step_checks
568
        ~pp_instr:(pp_machine_instr dependencies m self mem)
569
        ~instrs:m.mstep.step_instrs
570
        fmt
571
    else
572
      (* C90 code *)
573
      let gen_locals, base_locals = List.partition (fun v ->
574
          Types.is_generic_type v.var_type) m.mstep.step_locals in
575
      let gen_calls = List.map (fun e ->
576
          let id, _, _ = call_of_expr e in
577
          mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
578
      pp_print_function
579
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
580
        ~pp_prototype:(Protos.print_step_prototype self mem)
581
        ~prototype:(m.mname.node_id,
582
                    m.mstep.step_inputs @ gen_locals @ gen_calls,
583
                    m.mstep.step_outputs)
584
        ~pp_local:(pp_c_decl_local_var m)
585
        ~base_locals
586
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
587
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
588
        ~mpfr_locals:m.mstep.step_locals
589
        ~pp_check:(pp_c_check m self)
590
        ~checks:m.mstep.step_checks
591
        ~pp_instr:(pp_machine_instr dependencies m self mem)
592
        ~instrs:m.mstep.step_instrs
593
        fmt
594

    
595
  (********************************************************************************************)
596
  (*                     MAIN C file Printing functions                                       *)
597
  (********************************************************************************************)
598

    
599
  let pp_const_initialize m pp_var fmt const =
600
    let var = Machine_code_common.mk_val
601
        (Var (Corelang.var_decl_of_const const)) const.const_type in
602
    let rec aux indices value fmt typ =
603
      if Types.is_array_type typ
604
      then
605
        let dim = Types.array_type_dimension typ in
606
        let szl = Utils.enumerate (Dimension.size_const_dimension dim) in
607
        let typ' = Types.array_element_type typ in
608
        let value = match value with
609
          | Const_array ca -> List.nth ca
610
          | _ -> assert false in
611
        pp_print_list
612
          (fun fmt i -> aux (string_of_int i :: indices) (value i) fmt typ') fmt szl
613
      else
614
        let indices = List.rev indices in
615
        let pp_var_suffix fmt var =
616
          fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix indices in
617
        fprintf fmt "%a@,%a"
618
          (Mpfr.pp_inject_init pp_var_suffix) var
619
          (Mpfr.pp_inject_real pp_var_suffix pp_c_const) (var, value)
620
    in
621
    reset_loop_counter ();
622
    aux [] const.const_value fmt const.const_type
623

    
624
  let pp_const_clear pp_var fmt const =
625
    let m = Machine_code_common.empty_machine in
626
    let var = Corelang.var_decl_of_const const in
627
    let rec aux indices fmt typ =
628
      if Types.is_array_type typ
629
      then
630
        let dim = Types.array_type_dimension typ in
631
        let idx = mk_loop_var m () in
632
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
633
          idx idx idx pp_c_dimension dim idx
634
          (aux (idx::indices)) (Types.array_element_type typ)
635
      else
636
        let indices = List.rev indices in
637
        let pp_var_suffix fmt var =
638
          fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix indices in
639
        Mpfr.pp_inject_clear pp_var_suffix fmt var
640
    in
641
    reset_loop_counter ();
642
    aux [] fmt var.var_type
643

    
644
  let print_import_init fmt dep =
645
    let baseNAME = file_to_module_name dep.name in
646
    fprintf fmt "%a();" pp_global_init_name baseNAME
647

    
648
  let print_import_clear fmt dep =
649
    let baseNAME = file_to_module_name dep.name in
650
    fprintf fmt "%a();" pp_global_clear_name baseNAME
651

    
652
  let print_global_init_code fmt (basename, prog, dependencies) =
653
    let baseNAME = file_to_module_name basename in
654
    let constants = List.map const_of_top (get_consts prog) in
655
    fprintf fmt
656
      "@[<v 2>%a {@,\
657
       static %s init = 0;@,\
658
       @[<v 2>if (!init) { @,\
659
       init = 1;%a%a@]@,\
660
       }@,\
661
       return;@]@,\
662
       }"
663
      print_global_init_prototype baseNAME
664
      (pp_c_basic_type_desc Type_predef.type_bool)
665
      (* constants *)
666
      (pp_print_list
667
         ~pp_prologue:pp_print_cut
668
         (pp_const_initialize empty_machine (pp_c_var_read empty_machine)))
669
      (mpfr_consts constants)
670
      (* dependencies initialization *)
671
      (pp_print_list
672
         ~pp_prologue:pp_print_cut
673
         print_import_init) (List.filter (fun dep -> dep.local) dependencies)
674

    
675
  let print_global_clear_code fmt (basename, prog, dependencies) =
676
    let baseNAME = file_to_module_name basename in
677
    let constants = List.map const_of_top (get_consts prog) in
678
    fprintf fmt
679
      "@[<v 2>%a {@,\
680
       static %s clear = 0;@,\
681
       @[<v 2>if (!clear) { @,\
682
       clear = 1;%a%a@]@,\
683
       }@,\
684
       return;@]@,\
685
       }"
686
      print_global_clear_prototype baseNAME
687
      (pp_c_basic_type_desc Type_predef.type_bool)
688
      (* constants *)
689
      (pp_print_list
690
         ~pp_prologue:pp_print_cut
691
         (pp_const_clear (pp_c_var_read empty_machine))) (mpfr_consts constants)
692
      (* dependencies initialization *)
693
      (pp_print_list
694
         ~pp_prologue:pp_print_cut
695
         print_import_clear) (List.filter (fun dep -> dep.local) dependencies)
696

    
697
  let print_alloc_function fmt m =
698
    if (not !Options.static_mem) then
699
      (* Alloc functions, only if non static mode *)
700
      fprintf fmt
701
        "@[<v 2>%a {@,\
702
         %a%a@]@,\
703
         }@,\
704
         @[<v 2>%a {@,\
705
         %a%a@]@,\
706
         @,"
707
        print_alloc_prototype (m.mname.node_id, m.mstatic)
708
        print_alloc_const m
709
        print_alloc_code m
710
        print_dealloc_prototype m.mname.node_id
711
        print_alloc_const m
712
        print_dealloc_code m
713

    
714
  let print_mpfr_code self fmt m =
715
    if !Options.mpfr then
716
      fprintf fmt "@,@[<v>%a@,%a@]"
717
        (* Init function *)
718
        (print_init_code self) m
719
        (* Clear function *)
720
        (print_clear_code self) m
721

    
722
  (* TODO: ACSL
723
     - a contract machine shall not be directly printed in the C source
724
     - but a regular machine associated to a contract machine shall integrate
725
       the associated statements, updating its memories, at the end of the
726
       function body.
727
     - last one may print intermediate comment/acsl if/when they are present in
728
       the sequence of instruction
729
  *)
730
  let print_machine machines dependencies fmt m =
731
    if fst (get_stateless_status m) then
732
      (* Step function *)
733
      print_stateless_code machines dependencies fmt m
734
    else
735
      let self = mk_self m in
736
      let mem = mk_mem m in
737
      fprintf fmt "@[<v>%a%a@,@,%a@,@,%a%a@]"
738
        print_alloc_function m
739
        (* Reset functions *)
740
        (print_clear_reset_code dependencies self mem) m
741
        (print_set_reset_code dependencies self mem) m
742
        (* Step function *)
743
        (print_step_code machines dependencies self mem) m
744
        (print_mpfr_code self) m
745

    
746
  let print_import_standard source_fmt () =
747
    fprintf source_fmt
748
      "@[<v>#include <assert.h>@,%a%a%a@]"
749
      (if Machine_types.has_machine_type ()
750
       then pp_print_endcut "#include <stdint.h>"
751
       else pp_print_nothing) ()
752
      (if not !Options.static_mem
753
       then pp_print_endcut "#include <stdlib.h>"
754
       else pp_print_nothing) ()
755
      (if !Options.mpfr
756
       then pp_print_endcut "#include <mpfr.h>"
757
       else pp_print_nothing) ()
758

    
759
  let print_extern_alloc_prototype fmt ind =
760
    let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs in
761
    fprintf fmt "extern %a;@,extern %a;"
762
      print_alloc_prototype (ind.nodei_id, static)
763
      print_dealloc_prototype ind.nodei_id
764

    
765
  let print_lib_c source_fmt basename prog machines dependencies =
766
    fprintf source_fmt
767
      "@[<v>\
768
       %a\
769
       %a@,\
770
       @,\
771
       %a@,\
772
       %a\
773
       %a\
774
       %a\
775
       %a\
776
       %a\
777
       %a\
778
       %a\
779
       @]@."
780
      print_import_standard ()
781
      print_import_prototype
782
      {
783
        local = true;
784
        name = basename;
785
        content = [];
786
        is_stateful=true (* assuming it is stateful *);
787
      }
788

    
789
      (* Print the svn version number and the supported C standard (C90 or C99) *)
790
      pp_print_version ()
791

    
792
      (* Print dependencies *)
793
      (pp_print_list
794
         ~pp_open_box:pp_open_vbox0
795
         ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
796
         print_import_prototype
797
         ~pp_epilogue:pp_print_cutcut) dependencies
798

    
799
      (* Print consts *)
800
      (pp_print_list
801
         ~pp_open_box:pp_open_vbox0
802
         ~pp_prologue:(pp_print_endcut "/* Global constants (definitions) */")
803
         print_const_def
804
         ~pp_epilogue:pp_print_cutcut) (get_consts prog)
805

    
806
      (* MPFR *)
807
      (if !Options.mpfr then
808
         fun fmt () ->
809
           fprintf fmt
810
             "@[<v>/* Global constants initialization */@,\
811
              %a@,\
812
              @,\
813
              /* Global constants clearing */@,\
814
              %a@]@,@,"
815
             print_global_init_code (basename, prog, dependencies)
816
             print_global_clear_code (basename, prog, dependencies)
817
       else pp_print_nothing) ()
818

    
819
      (if not !Options.static_mem then
820
         fun fmt () ->
821
           fprintf fmt
822
             "@[<v>%a%a@]@,@,"
823
             (pp_print_list
824
                ~pp_open_box:pp_open_vbox0
825
                ~pp_epilogue:pp_print_cut
826
                ~pp_prologue:(pp_print_endcut
827
                                "/* External allocation function prototypes */")
828
                (fun fmt dep ->
829
                   pp_print_list
830
                     ~pp_open_box:pp_open_vbox0
831
                     ~pp_epilogue:pp_print_cut
832
                     print_extern_alloc_prototype
833
                     fmt
834
                     (List.filter_map (fun decl -> match decl.top_decl_desc with
835
                          | ImportedNode ind when not ind.nodei_stateless ->
836
                            Some ind
837
                          | _ -> None) dep.content))) dependencies
838
             (pp_print_list
839
                ~pp_open_box:pp_open_vbox0
840
                ~pp_prologue:(pp_print_endcut
841
                                "/* Node allocation function prototypes */")
842
                ~pp_sep:pp_print_cutcut
843
                (fun fmt m ->
844
                   fprintf fmt "%a;@,%a;"
845
                     print_alloc_prototype (m.mname.node_id, m.mstatic)
846
                     print_dealloc_prototype m.mname.node_id)) machines
847
       else pp_print_nothing) ()
848

    
849
      (* Print the struct definitions of all machines. *)
850
      (pp_print_list
851
         ~pp_open_box:pp_open_vbox0
852
         ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
853
         ~pp_sep:pp_print_cutcut
854
         print_machine_struct
855
         ~pp_epilogue:pp_print_cutcut) machines
856

    
857
      (* Print the spec predicates *)
858
      Mod.pp_predicates machines
859

    
860
      (* Print nodes one by one (in the previous order) *)
861
      (pp_print_list
862
         ~pp_open_box:pp_open_vbox0
863
         ~pp_sep:pp_print_cutcut
864
         (print_machine machines dependencies)) machines
865

    
866
end
867

    
868
(* Local Variables: *)
869
(* compile-command:"make -C ../../.." *)
870
(* End: *)
(9-9/9)