Project

General

Profile

Download (33.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
  module GhostProto : MODIFIERS_GHOST_PROTO
21

    
22
  val pp_predicates : formatter -> machine_t list -> unit
23

    
24
  val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
25

    
26
  val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit
27

    
28
  val pp_step_spec :
29
    formatter -> machine_t list -> ident -> ident -> machine_t -> unit
30

    
31
  val pp_step_instr_spec :
32
    machine_t -> ident -> ident -> formatter -> instr_t -> unit
33

    
34
  val pp_ghost_parameter : ident -> formatter -> ident option -> unit
35
end
36

    
37
module EmptyMod = struct
38
  module GhostProto = EmptyGhostProto
39

    
40
  let pp_predicates _ _ = ()
41

    
42
  let pp_set_reset_spec _ _ _ _ = ()
43

    
44
  let pp_clear_reset_spec _ _ _ _ = ()
45

    
46
  let pp_step_spec _ _ _ _ _ = ()
47

    
48
  let pp_step_instr_spec _ _ _ _ _ = ()
49

    
50
  let pp_ghost_parameter _ _ _ = ()
51
end
52

    
53
module Main =
54
functor
55
  (Mod : MODIFIERS_SRC)
56
  ->
57
  struct
58
    module Protos = Protos (Mod.GhostProto)
59

    
60
    (********************************************************************************************)
61
    (* Instruction Printing functions *)
62
    (********************************************************************************************)
63

    
64
    let rec merge_static_loop_profiles lp1 lp2 =
65
      match lp1, lp2 with
66
      | [], _ ->
67
        lp2
68
      | _, [] ->
69
        lp1
70
      | p1 :: q1, p2 :: q2 ->
71
        (p1 || p2) :: merge_static_loop_profiles q1 q2
72

    
73
    (* Returns a list of bool values, indicating whether the indices must be
74
       static or not *)
75
    let rec static_loop_profile v =
76
      match v.value_desc with
77
      | Cst cst ->
78
        static_loop_profile_cst cst
79
      | Var _ | ResetFlag ->
80
        []
81
      | Fun (_, vl) ->
82
        List.fold_right
83
          (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v))
84
          vl []
85
      | Array vl ->
86
        true
87
        ::
88
        List.fold_right
89
          (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v))
90
          vl []
91
      | Access (v, _) -> (
92
        match static_loop_profile v with [] -> [] | _ :: q -> q)
93
      | Power (v, _) ->
94
        false :: static_loop_profile v
95

    
96
    and static_loop_profile_cst cst =
97
      match cst with
98
      | Const_array cl ->
99
        List.fold_right
100
          (fun c lp ->
101
            merge_static_loop_profiles lp (static_loop_profile_cst c))
102
          cl []
103
      | _ ->
104
        []
105

    
106
    (* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
107
       which may yield constant arrays in expressions. Type is needed to
108
       correctly print constant arrays. *)
109
    let pp_c_val m self pp_var fmt v =
110
      pp_value_suffix m self v.value_type [] pp_var fmt v
111

    
112
    let pp_machine_ pp_machine_name fn_name m fmt ?inst self mem =
113
      let name, is_arrow, static =
114
        match inst with
115
        | Some inst ->
116
          let node, static =
117
            try List.assoc inst m.minstances
118
            with Not_found ->
119
              eprintf "internal error: %s %s %s %s:@." fn_name m.mname.node_id
120
                self inst;
121
              raise Not_found
122
          in
123
          node_name node, Arrow.td_is_arrow node, static
124
        | None ->
125
          m.mname.node_id, false, []
126
      in
127
      let is_arrow_reset = is_arrow && fn_name = "pp_machine_set_reset" in
128
      fprintf fmt "%a(%a%s%a)%a;"
129
        (if is_arrow_reset then fun fmt -> fprintf fmt "%s_reset"
130
        else pp_machine_name)
131
        name
132
        (pp_comma_list ~pp_eol:pp_print_comma Dimension.pp_dimension)
133
        static self
134
        (pp_print_option (fun fmt -> fprintf fmt "->%s"))
135
        inst
136
        (if is_arrow_reset then pp_print_nothing
137
        else Mod.pp_ghost_parameter mem)
138
        inst
139

    
140
    let pp_machine_set_reset m self mem fmt inst =
141
      pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst
142
        self mem
143

    
144
    let pp_machine_clear_reset m self mem fmt =
145
      pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt
146
        self mem
147

    
148
    let pp_machine_init m self mem fmt inst =
149
      pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self mem
150

    
151
    let pp_machine_clear m self mem fmt inst =
152
      pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self mem
153

    
154
    let pp_call m self mem pp_read pp_write fmt i inputs outputs =
155
      try
156
        (* stateful node instance *)
157
        let n, _ = List.assoc i m.minstances in
158
        fprintf fmt "%a(%a%a%s->%s)%a;" pp_machine_step_name (node_name n)
159
          (pp_comma_list ~pp_eol:pp_print_comma (pp_c_val m self pp_read))
160
          inputs
161
          (pp_comma_list ~pp_eol:pp_print_comma pp_write)
162
          outputs self i
163
          (Mod.pp_ghost_parameter mem)
164
          (Some i)
165
      with Not_found ->
166
        (* stateless node instance *)
167
        let n, _ = List.assoc i m.mcalls in
168
        fprintf fmt "%a(%a%a);" pp_machine_step_name (node_name n)
169
          (pp_comma_list ~pp_eol:pp_print_comma (pp_c_val m self pp_read))
170
          inputs (pp_comma_list pp_write) outputs
171

    
172
    let pp_basic_instance_call m self mem =
173
      pp_call m self mem (pp_c_var_read m) (pp_c_var_write m)
174

    
175
    let pp_arrow_call m self mem fmt i outputs =
176
      match outputs with
177
      | [ x ] ->
178
        fprintf fmt "%a = %a(%s->%s)%a;" (pp_c_var_read m) x
179
          pp_machine_step_name Arrow.arrow_id self i
180
          (Mod.pp_ghost_parameter mem)
181
          (Some i)
182
      | _ ->
183
        assert false
184

    
185
    let pp_instance_call m self mem fmt i inputs outputs =
186
      let pp_offset pp_var indices fmt var =
187
        fprintf fmt "%a%a" pp_var var
188
          (pp_print_list ~pp_sep:pp_print_nothing (fun fmt ->
189
               fprintf fmt "[%s]"))
190
          indices
191
      in
192
      let rec aux indices fmt typ =
193
        if Types.is_array_type typ then
194
          let dim = Types.array_type_dimension typ in
195
          let idx = mk_loop_var m () in
196
          fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}" idx
197
            idx idx pp_c_dimension dim idx
198
            (aux (idx :: indices))
199
            (Types.array_element_type typ)
200
        else
201
          let pp_read = pp_offset (pp_c_var_read m) indices in
202
          let pp_write = pp_offset (pp_c_var_write m) indices in
203
          pp_call m self mem pp_read pp_write fmt i inputs outputs
204
      in
205
      reset_loop_counter ();
206
      aux [] fmt (List.hd inputs).Machine_code_types.value_type
207

    
208
    let rec pp_conditional dependencies m self mem fmt c tl el =
209
      let pp_machine_instrs =
210
        pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
211
          (pp_machine_instr dependencies m self mem)
212
      in
213
      let pp_cond = pp_c_val m self (pp_c_var_read m) in
214
      match tl, el with
215
      | [], _ :: _ ->
216
        fprintf fmt "@[<v 2>if (!%a) {%a@]@,}" pp_cond c pp_machine_instrs el
217
      | _, [] ->
218
        fprintf fmt "@[<v 2>if (%a) {%a@]@,}" pp_cond c pp_machine_instrs tl
219
      | _, _ ->
220
        fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}" pp_cond c
221
          pp_machine_instrs tl pp_machine_instrs el
222

    
223
    and pp_machine_instr dependencies m self mem fmt instr =
224
      let pp_instr fmt instr =
225
        match get_instr_desc instr with
226
        | MNoReset _ ->
227
          ()
228
        | MSetReset inst ->
229
          pp_machine_set_reset m self mem fmt inst
230
        | MClearReset ->
231
          if not (fst (get_stateless_status m)) then
232
            fprintf fmt "%t@,%a"
233
              (pp_machine_clear_reset m self mem)
234
              pp_label reset_label
235
        | MResetAssign b ->
236
          pp_reset_assign self fmt b
237
        | MLocalAssign (i, v) ->
238
          pp_assign m self (pp_c_var_read m) fmt (i, v)
239
        | MStateAssign (i, v) ->
240
          pp_assign m self (pp_c_var_read m) fmt (i, v)
241
        | MStep ([ i0 ], i, vl)
242
          when Basic_library.is_value_internal_fun
243
                 (mk_val (Fun (i, vl)) i0.var_type) ->
244
          pp_machine_instr dependencies m self mem fmt
245
            (update_instr_desc instr
246
               (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
247
        | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
248
          pp_instance_call m self mem fmt i vl il
249
        | MStep ([ i0 ], i, vl) when has_c_prototype i dependencies ->
250
          fprintf fmt "%a = %s%a;"
251
            (pp_c_val m self (pp_c_var_read m))
252
            (mk_val (Var i0) i0.var_type)
253
            i
254
            (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m)))
255
            vl
256
        | MStep (il, i, vl) ->
257
          let td, _ = List.assoc i m.minstances in
258
          if Arrow.td_is_arrow td then pp_arrow_call m self mem fmt i il
259
          else pp_basic_instance_call m self mem fmt i vl il
260
        | MBranch (_, []) ->
261
          eprintf "internal error: C_backend_src.pp_machine_instr %a@."
262
            (pp_instr m) instr;
263
          assert false
264
        | MBranch (g, hl) ->
265
          if
266
            let t = fst (List.hd hl) in
267
            t = tag_true || t = tag_false
268
          then
269
            (* boolean case, needs special treatment in C because truth value is
270
               not unique *)
271
            (* may disappear if we optimize code by replacing last branch test
272
               with default *)
273
            let tl = try List.assoc tag_true hl with Not_found -> [] in
274
            let el = try List.assoc tag_false hl with Not_found -> [] in
275
            let no_noreset =
276
              List.filter (fun i ->
277
                  match i.instr_desc with MNoReset _ -> false | _ -> true)
278
            in
279
            pp_conditional dependencies m self mem fmt g (no_noreset tl)
280
              (no_noreset el)
281
          else
282
            (* enum type case *)
283
            (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst
284
              (List.hd hl))) in*)
285
            fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
286
              (pp_c_val m self (pp_c_var_read m))
287
              g
288
              (pp_print_list ~pp_open_box:pp_open_vbox0
289
                 (pp_machine_branch dependencies m self mem))
290
              hl
291
        | MSpec s ->
292
          fprintf fmt "@[/*@@ %s */@]@ " s
293
        | MComment s ->
294
          fprintf fmt "/*%s*/@ " s
295
      in
296
      fprintf fmt "%a%a" pp_instr instr
297
        (Mod.pp_step_instr_spec m self mem)
298
        instr
299

    
300
    and pp_machine_branch dependencies m self mem fmt (t, h) =
301
      fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" pp_c_tag t
302
        (pp_print_list ~pp_open_box:pp_open_vbox0
303
           (pp_machine_instr dependencies m self mem))
304
        h
305

    
306
    (* let pp_machine_nospec_instr dependencies m self fmt instr =
307
     *   pp_machine_instr dependencies m self fmt instr
308
     *
309
     * let pp_machine_step_instr dependencies m self mem fmt instr =
310
     *   fprintf fmt "%a%a"
311
     *     (pp_machine_instr dependencies m self) instr
312
     *     (Mod.pp_step_instr_spec m self mem) instr *)
313

    
314
    (********************************************************************************************)
315
    (* C file Printing functions *)
316
    (********************************************************************************************)
317

    
318
    let print_const_def fmt tdecl =
319
      let cdecl = const_of_top tdecl in
320
      if
321
        !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
322
      then
323
        fprintf fmt "%a;" (pp_c_type cdecl.const_id)
324
          (Types.dynamic_type cdecl.const_type)
325
      else
326
        fprintf fmt "%a = %a;" (pp_c_type cdecl.const_id) cdecl.const_type
327
          pp_c_const cdecl.const_value
328

    
329
    let print_alloc_instance fmt (i, (m, static)) =
330
      fprintf fmt "_alloc->%s = %a %a;" i pp_machine_alloc_name (node_name m)
331
        (pp_print_parenthesized Dimension.pp_dimension)
332
        static
333

    
334
    let print_dealloc_instance fmt (i, (m, _)) =
335
      fprintf fmt "%a (_alloc->%s);" pp_machine_dealloc_name (node_name m) i
336

    
337
    let const_locals m =
338
      List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals
339

    
340
    let pp_c_decl_array_mem self fmt id =
341
      fprintf fmt "%a = (%a) (%s->_reg.%s)"
342
        (pp_c_type (sprintf "(*%s)" id.var_id))
343
        id.var_type (pp_c_type "(*)") id.var_type self id.var_id
344

    
345
    let print_alloc_const fmt m =
346
      pp_print_list ~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";")
347
        (pp_c_decl_local_var m) fmt (const_locals m)
348

    
349
    let print_alloc_array fmt vdecl =
350
      let base_type = Types.array_base_type vdecl.var_type in
351
      let size_types = Types.array_type_multi_dimension vdecl.var_type in
352
      let size_type =
353
        Dimension.multi_dimension_product vdecl.var_loc size_types
354
      in
355
      fprintf fmt
356
        "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,assert(_alloc->%s);"
357
        vdecl.var_id (pp_c_type "") base_type Dimension.pp_dimension size_type
358
        (pp_c_type "") base_type vdecl.var_id
359

    
360
    let print_dealloc_array fmt vdecl =
361
      fprintf fmt "free (_alloc->_reg.%s);" vdecl.var_id
362

    
363
    let array_mems m =
364
      List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
365

    
366
    let print_alloc_code fmt m =
367
      fprintf fmt
368
        "%a *_alloc;@,\
369
         _alloc = (%a *) malloc(sizeof(%a));@,\
370
         assert(_alloc);@,\
371
         %a%areturn _alloc;"
372
        (pp_machine_memtype_name ~ghost:false)
373
        m.mname.node_id
374
        (pp_machine_memtype_name ~ghost:false)
375
        m.mname.node_id
376
        (pp_machine_memtype_name ~ghost:false)
377
        m.mname.node_id
378
        (pp_print_list ~pp_sep:pp_print_nothing print_alloc_array)
379
        (array_mems m)
380
        (pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance)
381
        m.minstances
382

    
383
    let print_dealloc_code fmt m =
384
      fprintf fmt "%a%afree (_alloc);@,return;"
385
        (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array)
386
        (array_mems m)
387
        (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance)
388
        m.minstances
389

    
390
    (* let print_stateless_init_code fmt m self =
391
     *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
392
     *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
393
     *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
394
     *     (print_init_prototype self) (m.mname.node_id, m.mstatic)
395
     *     (\* array mems *\)
396
     *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
397
     *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
398
     *     (\* memory initialization *\)
399
     *     (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
400
     *     (Utils.pp_newline_if_non_empty m.mmemory)
401
     *     (\* sub-machines initialization *\)
402
     *     (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
403
     *     (Utils.pp_newline_if_non_empty m.minit)
404
     *
405
     * let print_stateless_clear_code fmt m self =
406
     *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
407
     *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
408
     *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
409
     *     (print_clear_prototype self) (m.mname.node_id, m.mstatic)
410
     *     (\* array mems *\)
411
     *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
412
     *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
413
     *     (\* memory clear *\)
414
     *     (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
415
     *     (Utils.pp_newline_if_non_empty m.mmemory)
416
     *     (\* sub-machines clear*\)
417
     *     (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
418
     *     (Utils.pp_newline_if_non_empty m.minit) *)
419

    
420
    let pp_c_check m self fmt (loc, check) =
421
      fprintf fmt "@[<v>%a@,assert (%a);@]" Location.pp_c_loc loc
422
        (pp_c_val m self (pp_c_var_read m))
423
        check
424

    
425
    let pp_print_function ~pp_prototype ~prototype ?(pp_spec = pp_print_nothing)
426
        ?(pp_local = pp_print_nothing) ?(base_locals = [])
427
        ?(pp_array_mem = pp_print_nothing) ?(array_mems = [])
428
        ?(pp_init_mpfr_local = pp_print_nothing)
429
        ?(pp_clear_mpfr_local = pp_print_nothing) ?(mpfr_locals = [])
430
        ?(pp_check = pp_print_nothing) ?(checks = [])
431
        ?(pp_extra = pp_print_nothing)
432
        ?(pp_instr = fun fmt _ -> pp_print_nothing fmt ()) ?(instrs = []) fmt =
433
      fprintf fmt "%a@[<v 2>%a {@,%a%a%a%a%a%a%areturn;@]@,}" pp_spec ()
434
        pp_prototype prototype
435
        (* locals *)
436
        (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon
437
           ~pp_eol:pp_print_semicolon pp_local)
438
        base_locals
439
        (* array mems *)
440
        (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon
441
           ~pp_eol:pp_print_semicolon pp_array_mem)
442
        array_mems
443
        (* locals initialization *)
444
        (pp_print_list ~pp_epilogue:pp_print_cut pp_init_mpfr_local)
445
        (mpfr_vars mpfr_locals)
446
        (* check assertions *)
447
        (pp_print_list pp_check)
448
        checks
449
        (* instrs *)
450
        (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_epilogue:pp_print_cut
451
           pp_instr)
452
        instrs
453
        (* locals clear *)
454
        (pp_print_list ~pp_epilogue:pp_print_cut pp_clear_mpfr_local)
455
        (mpfr_vars mpfr_locals) (* extra *)
456
        pp_extra ()
457

    
458
    let node_of_machine m =
459
      {
460
        top_decl_desc = Node m.mname;
461
        top_decl_loc = Location.dummy_loc;
462
        top_decl_owner = "";
463
        top_decl_itf = false;
464
      }
465

    
466
    let print_stateless_code machines dependencies fmt m =
467
      let self = "__ERROR__" in
468
      if not (!Options.ansi && is_generic_node (node_of_machine m)) then
469
        (* C99 code *)
470
        pp_print_function
471
          ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self self m)
472
          ~pp_prototype:Protos.print_stateless_prototype
473
          ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
474
          ~pp_local:(pp_c_decl_local_var m) ~base_locals:m.mstep.step_locals
475
          ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
476
          ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
477
          ~mpfr_locals:m.mstep.step_locals ~pp_check:(pp_c_check m self)
478
          ~checks:m.mstep.step_checks
479
          ~pp_instr:(pp_machine_instr dependencies m self self)
480
          ~instrs:m.mstep.step_instrs fmt
481
      else
482
        (* C90 code *)
483
        let gen_locals, base_locals =
484
          List.partition
485
            (fun v -> Types.is_generic_type v.var_type)
486
            m.mstep.step_locals
487
        in
488
        let gen_calls =
489
          List.map
490
            (fun e ->
491
              let id, _, _ = call_of_expr e in
492
              mk_call_var_decl e.expr_loc id)
493
            m.mname.node_gencalls
494
        in
495
        pp_print_function ~pp_prototype:Protos.print_stateless_prototype
496
          ~prototype:
497
            ( m.mname.node_id,
498
              m.mstep.step_inputs @ gen_locals @ gen_calls,
499
              m.mstep.step_outputs )
500
          ~pp_local:(pp_c_decl_local_var m) ~base_locals
501
          ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
502
          ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
503
          ~mpfr_locals:m.mstep.step_locals ~pp_check:(pp_c_check m self)
504
          ~checks:m.mstep.step_checks
505
          ~pp_instr:(pp_machine_instr dependencies m self self)
506
          ~instrs:m.mstep.step_instrs fmt
507

    
508
    let print_clear_reset_code dependencies self mem fmt m =
509
      pp_print_function
510
        ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt self mem m)
511
        ~pp_prototype:(Protos.print_clear_reset_prototype self mem)
512
        ~prototype:(m.mname.node_id, m.mstatic)
513
        ~pp_local:(pp_c_decl_local_var m) ~base_locals:(const_locals m)
514
        ~pp_instr:(pp_machine_instr dependencies m self mem)
515
        ~instrs:
516
          [
517
            mk_branch
518
              (mk_val ResetFlag Type_predef.type_bool)
519
              [ "true", mkinstr (MResetAssign false) :: m.minit ];
520
          ]
521
        fmt
522

    
523
    let print_set_reset_code dependencies self mem fmt m =
524
      pp_print_function
525
        ~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m)
526
        ~pp_prototype:(Protos.print_set_reset_prototype self mem)
527
        ~prototype:(m.mname.node_id, m.mstatic)
528
        ~pp_instr:(pp_machine_instr dependencies m self mem)
529
        ~instrs:[ mkinstr (MResetAssign true) ]
530
        fmt
531

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

    
551
    let print_clear_code self fmt m =
552
      let minit =
553
        List.map
554
          (fun i ->
555
            match get_instr_desc i with MSetReset i -> i | _ -> assert false)
556
          m.minit
557
      in
558
      pp_print_function
559
        ~pp_prototype:(Protos.print_clear_prototype self)
560
        ~prototype:(m.mname.node_id, m.mstatic)
561
        ~pp_array_mem:(pp_c_decl_array_mem self) ~array_mems:(array_mems m)
562
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
563
        ~mpfr_locals:m.mmemory
564
        ~pp_extra:(fun fmt () ->
565
          pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_epilogue:pp_print_cut
566
            (pp_machine_clear m self self)
567
            fmt minit)
568
        fmt
569

    
570
    let print_step_code machines dependencies self mem fmt m =
571
      if not (!Options.ansi && is_generic_node (node_of_machine m)) then
572
        (* C99 code *)
573
        pp_print_function
574
          ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
575
          ~pp_prototype:(Protos.print_step_prototype self mem)
576
          ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
577
          ~pp_local:(pp_c_decl_local_var m) ~base_locals:m.mstep.step_locals
578
          ~pp_array_mem:(pp_c_decl_array_mem self) ~array_mems:(array_mems m)
579
          ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
580
          ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
581
          ~mpfr_locals:m.mstep.step_locals ~pp_check:(pp_c_check m self)
582
          ~checks:m.mstep.step_checks
583
          ~pp_instr:(pp_machine_instr dependencies m self mem)
584
          ~instrs:m.mstep.step_instrs fmt
585
      else
586
        (* C90 code *)
587
        let gen_locals, base_locals =
588
          List.partition
589
            (fun v -> Types.is_generic_type v.var_type)
590
            m.mstep.step_locals
591
        in
592
        let gen_calls =
593
          List.map
594
            (fun e ->
595
              let id, _, _ = call_of_expr e in
596
              mk_call_var_decl e.expr_loc id)
597
            m.mname.node_gencalls
598
        in
599
        pp_print_function
600
          ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
601
          ~pp_prototype:(Protos.print_step_prototype self mem)
602
          ~prototype:
603
            ( m.mname.node_id,
604
              m.mstep.step_inputs @ gen_locals @ gen_calls,
605
              m.mstep.step_outputs )
606
          ~pp_local:(pp_c_decl_local_var m) ~base_locals
607
          ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
608
          ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
609
          ~mpfr_locals:m.mstep.step_locals ~pp_check:(pp_c_check m self)
610
          ~checks:m.mstep.step_checks
611
          ~pp_instr:(pp_machine_instr dependencies m self mem)
612
          ~instrs:m.mstep.step_instrs fmt
613

    
614
    (********************************************************************************************)
615
    (* MAIN C file Printing functions *)
616
    (********************************************************************************************)
617

    
618
    let pp_const_initialize m pp_var fmt const =
619
      let var =
620
        Machine_code_common.mk_val
621
          (Var (Corelang.var_decl_of_const const))
622
          const.const_type
623
      in
624
      let rec aux indices value fmt typ =
625
        if Types.is_array_type typ then
626
          let dim = Types.array_type_dimension typ in
627
          let szl = Utils.enumerate (Dimension.size_const_dimension dim) in
628
          let typ' = Types.array_element_type typ in
629
          let value =
630
            match value with Const_array ca -> List.nth ca | _ -> assert false
631
          in
632
          pp_print_list
633
            (fun fmt i -> aux (string_of_int i :: indices) (value i) fmt typ')
634
            fmt szl
635
        else
636
          let indices = List.rev indices in
637
          let pp_var_suffix fmt var =
638
            fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix
639
              indices
640
          in
641
          fprintf fmt "%a@,%a"
642
            (Mpfr.pp_inject_init pp_var_suffix)
643
            var
644
            (Mpfr.pp_inject_real pp_var_suffix pp_c_const)
645
            (var, value)
646
      in
647
      reset_loop_counter ();
648
      aux [] const.const_value fmt const.const_type
649

    
650
    let pp_const_clear pp_var fmt const =
651
      let m = Machine_code_common.empty_machine in
652
      let var = Corelang.var_decl_of_const const in
653
      let rec aux indices fmt typ =
654
        if Types.is_array_type typ then
655
          let dim = Types.array_type_dimension typ in
656
          let idx = mk_loop_var m () in
657
          fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}" idx
658
            idx idx pp_c_dimension dim idx
659
            (aux (idx :: indices))
660
            (Types.array_element_type typ)
661
        else
662
          let indices = List.rev indices in
663
          let pp_var_suffix fmt var =
664
            fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix
665
              indices
666
          in
667
          Mpfr.pp_inject_clear pp_var_suffix fmt var
668
      in
669
      reset_loop_counter ();
670
      aux [] fmt var.var_type
671

    
672
    let print_import_init fmt dep =
673
      let baseNAME = file_to_module_name dep.name in
674
      fprintf fmt "%a();" pp_global_init_name baseNAME
675

    
676
    let print_import_clear fmt dep =
677
      let baseNAME = file_to_module_name dep.name in
678
      fprintf fmt "%a();" pp_global_clear_name baseNAME
679

    
680
    let print_global_init_code fmt (basename, prog, dependencies) =
681
      let baseNAME = file_to_module_name basename in
682
      let constants = List.map const_of_top (get_consts prog) in
683
      fprintf fmt
684
        "@[<v 2>%a {@,\
685
         static %s init = 0;@,\
686
         @[<v 2>if (!init) { @,\
687
         init = 1;%a%a@]@,\
688
         }@,\
689
         return;@]@,\
690
         }"
691
        print_global_init_prototype baseNAME
692
        (pp_c_basic_type_desc Type_predef.type_bool)
693
        (* constants *)
694
        (pp_print_list ~pp_prologue:pp_print_cut
695
           (pp_const_initialize empty_machine (pp_c_var_read empty_machine)))
696
        (mpfr_consts constants)
697
        (* dependencies initialization *)
698
        (pp_print_list ~pp_prologue:pp_print_cut print_import_init)
699
        (List.filter (fun dep -> dep.local) dependencies)
700

    
701
    let print_global_clear_code fmt (basename, prog, dependencies) =
702
      let baseNAME = file_to_module_name basename in
703
      let constants = List.map const_of_top (get_consts prog) in
704
      fprintf fmt
705
        "@[<v 2>%a {@,\
706
         static %s clear = 0;@,\
707
         @[<v 2>if (!clear) { @,\
708
         clear = 1;%a%a@]@,\
709
         }@,\
710
         return;@]@,\
711
         }"
712
        print_global_clear_prototype baseNAME
713
        (pp_c_basic_type_desc Type_predef.type_bool)
714
        (* constants *)
715
        (pp_print_list ~pp_prologue:pp_print_cut
716
           (pp_const_clear (pp_c_var_read empty_machine)))
717
        (mpfr_consts constants)
718
        (* dependencies initialization *)
719
        (pp_print_list ~pp_prologue:pp_print_cut print_import_clear)
720
        (List.filter (fun dep -> dep.local) dependencies)
721

    
722
    let print_alloc_function fmt m =
723
      if not !Options.static_mem then
724
        (* Alloc functions, only if non static mode *)
725
        fprintf fmt "@[<v 2>%a {@,%a%a@]@,}@,@[<v 2>%a {@,%a%a@]@,@,"
726
          print_alloc_prototype
727
          (m.mname.node_id, m.mstatic)
728
          print_alloc_const m print_alloc_code m print_dealloc_prototype
729
          m.mname.node_id print_alloc_const m print_dealloc_code m
730

    
731
    let print_mpfr_code self fmt m =
732
      if !Options.mpfr then
733
        fprintf fmt "@,@[<v>%a@,%a@]"
734
          (* Init function *)
735
          (print_init_code self)
736
          m
737
          (* Clear function *)
738
          (print_clear_code self)
739
          m
740

    
741
    (* TODO: ACSL - a contract machine shall not be directly printed in the C
742
       source - but a regular machine associated to a contract machine shall
743
       integrate the associated statements, updating its memories, at the end of
744
       the function body. - last one may print intermediate comment/acsl if/when
745
       they are present in the sequence of instruction *)
746
    let print_machine machines dependencies fmt m =
747
      if fst (get_stateless_status m) then
748
        (* Step function *)
749
        print_stateless_code machines dependencies fmt m
750
      else
751
        let self = mk_self m in
752
        let mem = mk_mem m in
753
        fprintf fmt "@[<v>%a%a@,@,%a@,@,%a%a@]" print_alloc_function m
754
          (* Reset functions *)
755
          (print_clear_reset_code dependencies self mem)
756
          m
757
          (print_set_reset_code dependencies self mem)
758
          m
759
          (* Step function *)
760
          (print_step_code machines dependencies self mem)
761
          m (print_mpfr_code self) m
762

    
763
    let print_import_standard source_fmt () =
764
      fprintf source_fmt "@[<v>#include <assert.h>@,%a%a%a@]"
765
        (if Machine_types.has_machine_type () then
766
         pp_print_endcut "#include <stdint.h>"
767
        else pp_print_nothing)
768
        ()
769
        (if not !Options.static_mem then pp_print_endcut "#include <stdlib.h>"
770
        else pp_print_nothing)
771
        ()
772
        (if !Options.mpfr then pp_print_endcut "#include <mpfr.h>"
773
        else pp_print_nothing)
774
        ()
775

    
776
    let print_extern_alloc_prototype fmt ind =
777
      let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs in
778
      fprintf fmt "extern %a;@,extern %a;" print_alloc_prototype
779
        (ind.nodei_id, static) print_dealloc_prototype ind.nodei_id
780

    
781
    let print_lib_c source_fmt basename prog machines dependencies =
782
      fprintf source_fmt "@[<v>%a%a@,@,%a@,%a%a%a%a%a%a%a@]@."
783
        print_import_standard () print_import_prototype
784
        {
785
          local = true;
786
          name = basename;
787
          content = [];
788
          is_stateful = true (* assuming it is stateful *);
789
        }
790
        (* Print the svn version number and the supported C standard (C90 or
791
           C99) *)
792
        pp_print_version ()
793
        (* Print dependencies *)
794
        (pp_print_list ~pp_open_box:pp_open_vbox0
795
           ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
796
           print_import_prototype ~pp_epilogue:pp_print_cutcut)
797
        dependencies
798
        (* Print consts *)
799
        (pp_print_list ~pp_open_box:pp_open_vbox0
800
           ~pp_prologue:(pp_print_endcut "/* Global constants (definitions) */")
801
           print_const_def ~pp_epilogue:pp_print_cutcut)
802
        (get_consts prog)
803
        (* MPFR *)
804
        (if !Options.mpfr then fun fmt () ->
805
         fprintf fmt
806
           "@[<v>/* Global constants initialization */@,\
807
            %a@,\
808
            @,\
809
            /* Global constants clearing */@,\
810
            %a@]@,\
811
            @,"
812
           print_global_init_code
813
           (basename, prog, dependencies)
814
           print_global_clear_code
815
           (basename, prog, dependencies)
816
        else pp_print_nothing)
817
        ()
818
        (if not !Options.static_mem then fun fmt () ->
819
         fprintf fmt "@[<v>%a%a@]@,@,"
820
           (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_epilogue:pp_print_cut
821
              ~pp_prologue:
822
                (pp_print_endcut "/* External allocation function prototypes */")
823
              (fun fmt dep ->
824
                pp_print_list ~pp_open_box:pp_open_vbox0
825
                  ~pp_epilogue:pp_print_cut print_extern_alloc_prototype fmt
826
                  (List.filter_map
827
                     (fun decl ->
828
                       match decl.top_decl_desc with
829
                       | ImportedNode ind when not ind.nodei_stateless ->
830
                         Some ind
831
                       | _ ->
832
                         None)
833
                     dep.content)))
834
           dependencies
835
           (pp_print_list ~pp_open_box:pp_open_vbox0
836
              ~pp_prologue:
837
                (pp_print_endcut "/* Node allocation function prototypes */")
838
              ~pp_sep:pp_print_cutcut (fun fmt m ->
839
                fprintf fmt "%a;@,%a;" print_alloc_prototype
840
                  (m.mname.node_id, m.mstatic)
841
                  print_dealloc_prototype m.mname.node_id))
842
           machines
843
        else pp_print_nothing)
844
        ()
845
        (* Print the struct definitions of all machines. *)
846
        (pp_print_list ~pp_open_box:pp_open_vbox0
847
           ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
848
           ~pp_sep:pp_print_cutcut print_machine_struct
849
           ~pp_epilogue:pp_print_cutcut)
850
        machines (* Print the spec predicates *) Mod.pp_predicates machines
851
        (* Print nodes one by one (in the previous order) *)
852
        (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut
853
           (print_machine machines dependencies))
854
        machines
855
  end
856

    
857
(* Local Variables: *)
858
(* compile-command:"make -C ../../.." *)
859
(* End: *)
(9-9/9)