Project

General

Profile

Download (33 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 -> machine_t list -> 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 -> formatter -> instr_t -> unit
26
  val pp_ghost_set_reset_spec: formatter -> ident -> 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_set_reset_spec _ _ = ()
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 _  -> []
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_basic_assign pp_var fmt typ var_name value =
85
    if Types.is_real_type typ && !Options.mpfr
86
    then
87
      Mpfr.pp_inject_assign pp_var fmt (var_name, value)
88
    else
89
      fprintf fmt "%a = %a;"
90
        pp_var var_name
91
        pp_var value
92

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

    
130
  let pp_machine_ pp_machine_name fn_name m fmt ?inst self =
131
    let name, static =
132
      match inst with
133
      | Some inst ->
134
        let node, static = try List.assoc inst m.minstances with Not_found ->
135
          eprintf "internal error: %s %s %s %s:@."
136
            fn_name m.mname.node_id self inst;
137
          raise Not_found
138
        in
139
        node_name node, static
140
      | None ->
141
        m.mname.node_id, []
142
    in
143
    fprintf fmt "%a(%a%s%a);"
144
      pp_machine_name name
145
      (pp_comma_list ~pp_eol:pp_print_comma Dimension.pp_dimension) static
146
      self
147
      (pp_print_option (fun fmt -> fprintf fmt "->%s")) inst
148

    
149
  let pp_machine_set_reset m self fmt inst =
150
    pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst self
151

    
152
  let pp_machine_clear_reset m self fmt =
153
    pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt self
154

    
155
  let pp_machine_init m self fmt inst =
156
    pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self
157

    
158
  let pp_machine_clear m self fmt inst =
159
    pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self
160

    
161
  let pp_call m self pp_read pp_write fmt i inputs outputs =
162
    try (* stateful node instance *)
163
      let n, _ = List.assoc i m.minstances in
164
      fprintf fmt "%a(%a%a%s->%s);"
165
        pp_machine_step_name (node_name n)
166
        (pp_comma_list ~pp_eol:pp_print_comma
167
           (pp_c_val m self pp_read)) inputs
168
        (pp_comma_list ~pp_eol:pp_print_comma
169
           pp_write) outputs
170
        self
171
        i
172
    with Not_found -> (* stateless node instance *)
173
      let n, _ = List.assoc i m.mcalls in
174
      fprintf fmt "%a(%a%a);"
175
        pp_machine_step_name (node_name n)
176
        (pp_comma_list ~pp_eol:pp_print_comma
177
           (pp_c_val m self pp_read)) inputs
178
        (pp_comma_list pp_write) outputs
179

    
180
  let pp_basic_instance_call m self =
181
    pp_call m self (pp_c_var_read m) (pp_c_var_write m)
182

    
183
  let pp_arrow_call m self fmt i outputs =
184
    match outputs with
185
    | [x] ->
186
      fprintf fmt "%a = %a(%s->%s);"
187
        (pp_c_var_read m) x
188
        pp_machine_step_name Arrow.arrow_id
189
        self
190
        i
191
    | _ -> assert false
192

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

    
216
  let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
217
    fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
218
      (pp_c_val m self (pp_c_var_read m)) c
219
      (pp_print_list ~pp_prologue:pp_print_cut
220
         (pp_machine_instr dependencies m self)) tl
221
      (pp_print_list ~pp_prologue:pp_print_cut
222
         (pp_machine_instr dependencies m self)) el
223

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

    
278
  and pp_machine_branch dependencies m self fmt (t, h) =
279
    fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
280
      pp_c_tag t
281
      (pp_print_list ~pp_open_box:pp_open_vbox0
282
         (pp_machine_instr dependencies m self)) h
283

    
284
  let pp_machine_nospec_instr dependencies m self fmt _i instr =
285
    pp_machine_instr dependencies m self fmt instr
286

    
287
  let pp_machine_step_instr dependencies m self fmt _i instr =
288
    fprintf fmt "%a%a"
289
      (pp_machine_instr dependencies m self) instr
290
      (Mod.pp_step_instr_spec m self) instr
291

    
292
  (********************************************************************************************)
293
  (*                         C file Printing functions                                        *)
294
  (********************************************************************************************)
295

    
296
  let print_const_def fmt tdecl =
297
    let cdecl = const_of_top tdecl in
298
    if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
299
    then
300
      fprintf fmt "%a;"
301
        (pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type)
302
    else
303
      fprintf fmt "%a = %a;"
304
        (pp_c_type cdecl.const_id) cdecl.const_type
305
        pp_c_const cdecl.const_value
306

    
307
  let print_alloc_instance fmt (i, (m, static)) =
308
    fprintf fmt "_alloc->%s = %a %a;"
309
      i
310
      pp_machine_alloc_name (node_name m)
311
      (pp_print_parenthesized Dimension.pp_dimension) static
312

    
313
  let print_dealloc_instance fmt (i, (m, _)) =
314
    fprintf fmt "%a (_alloc->%s);"
315
      pp_machine_dealloc_name (node_name m)
316
      i
317

    
318
  let const_locals m =
319
    List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals
320

    
321
  let pp_c_decl_array_mem self fmt id =
322
    fprintf fmt "%a = (%a) (%s->_reg.%s)"
323
      (pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type
324
      (pp_c_type "(*)") id.var_type
325
      self
326
      id.var_id
327

    
328
  let print_alloc_const fmt m =
329
    pp_print_list
330
      ~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";")
331
      (pp_c_decl_local_var m) fmt (const_locals m)
332

    
333
  let print_alloc_array fmt vdecl =
334
    let base_type = Types.array_base_type vdecl.var_type in
335
    let size_types = Types.array_type_multi_dimension vdecl.var_type in
336
    let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in
337
    fprintf fmt
338
      "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,\
339
       assert(_alloc->%s);"
340
      vdecl.var_id
341
      (pp_c_type "") base_type
342
      Dimension.pp_dimension size_type
343
      (pp_c_type "") base_type
344
      vdecl.var_id
345

    
346
  let print_dealloc_array fmt vdecl =
347
    fprintf fmt "free (_alloc->_reg.%s);"
348
      vdecl.var_id
349

    
350
  let array_mems m =
351
    List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
352

    
353
  let print_alloc_code fmt m =
354
    fprintf fmt
355
      "%a *_alloc;@,\
356
       _alloc = (%a *) malloc(sizeof(%a));@,\
357
       assert(_alloc);@,\
358
       %a%areturn _alloc;"
359
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
360
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
361
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
362
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m)
363
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances
364

    
365
  let print_dealloc_code fmt m =
366
    fprintf fmt
367
      "%a%afree (_alloc);@,\
368
       return;"
369
      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array) (array_mems m)
370
      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance) m.minstances
371

    
372
  (* let print_stateless_init_code fmt m self =
373
   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
374
   *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
375
   *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
376
   *     (print_init_prototype self) (m.mname.node_id, m.mstatic)
377
   *     (\* array mems *\)
378
   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
379
   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
380
   *     (\* memory initialization *\)
381
   *     (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
382
   *     (Utils.pp_newline_if_non_empty m.mmemory)
383
   *     (\* sub-machines initialization *\)
384
   *     (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
385
   *     (Utils.pp_newline_if_non_empty m.minit)
386
   *
387
   * let print_stateless_clear_code fmt m self =
388
   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
389
   *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
390
   *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
391
   *     (print_clear_prototype self) (m.mname.node_id, m.mstatic)
392
   *     (\* array mems *\)
393
   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
394
   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
395
   *     (\* memory clear *\)
396
   *     (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
397
   *     (Utils.pp_newline_if_non_empty m.mmemory)
398
   *     (\* sub-machines clear*\)
399
   *     (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
400
   *     (Utils.pp_newline_if_non_empty m.minit) *)
401

    
402
  let pp_c_check m self fmt (loc, check) =
403
    fprintf fmt "@[<v>%a@,assert (%a);@]"
404
      Location.pp_c_loc loc
405
      (pp_c_val m self (pp_c_var_read m)) check
406

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

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

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

    
507
  let print_clear_reset_code machines dependencies self mem fmt m =
508
    pp_print_function
509
      ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt machines self mem m)
510
      ~pp_prototype:(Protos.print_clear_reset_prototype self mem)
511
      ~prototype:(m.mname.node_id, m.mstatic)
512
      ~pp_local:(pp_c_decl_local_var m)
513
      ~base_locals:(const_locals m)
514
      ~pp_instr:(pp_machine_nospec_instr dependencies m self)
515
      ~instrs:m.minit
516
      fmt
517

    
518
  let print_set_reset_code self mem fmt m =
519
    pp_print_function
520
      ~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m)
521
      ~pp_prototype:(Protos.print_set_reset_prototype self mem)
522
      ~prototype:(m.mname.node_id, m.mstatic)
523
      ~pp_extra:(fun fmt () -> fprintf fmt "self->_reset = 1;%a"
524
                    Mod.pp_ghost_set_reset_spec mem)
525
      fmt
526

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

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

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

    
612
  (********************************************************************************************)
613
  (*                     MAIN C file Printing functions                                       *)
614
  (********************************************************************************************)
615

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

    
641
  let pp_const_clear pp_var fmt const =
642
    let m = Machine_code_common.empty_machine in
643
    let var = Corelang.var_decl_of_const const in
644
    let rec aux indices fmt typ =
645
      if Types.is_array_type typ
646
      then
647
        let dim = Types.array_type_dimension typ in
648
        let idx = mk_loop_var m () in
649
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
650
          idx idx idx pp_c_dimension dim idx
651
          (aux (idx::indices)) (Types.array_element_type typ)
652
      else
653
        let indices = List.rev indices in
654
        let pp_var_suffix fmt var =
655
          fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix indices in
656
        Mpfr.pp_inject_clear pp_var_suffix fmt var
657
    in
658
    reset_loop_counter ();
659
    aux [] fmt var.var_type
660

    
661
  let print_import_init fmt dep =
662
    let baseNAME = file_to_module_name dep.name in
663
    fprintf fmt "%a();" pp_global_init_name baseNAME
664

    
665
  let print_import_clear fmt dep =
666
    let baseNAME = file_to_module_name dep.name in
667
    fprintf fmt "%a();" pp_global_clear_name baseNAME
668

    
669
  let print_global_init_code fmt (basename, prog, dependencies) =
670
    let baseNAME = file_to_module_name basename in
671
    let constants = List.map const_of_top (get_consts prog) in
672
    fprintf fmt
673
      "@[<v 2>%a {@,\
674
       static %s init = 0;@,\
675
       @[<v 2>if (!init) { @,\
676
       init = 1;%a%a@]@,\
677
       }@,\
678
       return;@]@,\
679
       }"
680
      print_global_init_prototype baseNAME
681
      (pp_c_basic_type_desc Type_predef.type_bool)
682
      (* constants *)
683
      (pp_print_list
684
         ~pp_prologue:pp_print_cut
685
         (pp_const_initialize empty_machine (pp_c_var_read empty_machine)))
686
      (mpfr_consts constants)
687
      (* dependencies initialization *)
688
      (pp_print_list
689
         ~pp_prologue:pp_print_cut
690
         print_import_init) (List.filter (fun dep -> dep.local) dependencies)
691

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

    
714
  let print_alloc_function fmt m =
715
    if (not !Options.static_mem) then
716
      (* Alloc functions, only if non static mode *)
717
      fprintf fmt
718
        "@[<v 2>%a {@,\
719
         %a%a@]@,\
720
         }@,\
721
         @[<v 2>%a {@,\
722
         %a%a@]@,\
723
         @,"
724
        print_alloc_prototype (m.mname.node_id, m.mstatic)
725
        print_alloc_const m
726
        print_alloc_code m
727
        print_dealloc_prototype m.mname.node_id
728
        print_alloc_const m
729
        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) m
736
        (* Clear function *)
737
        (print_clear_code self) m
738

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

    
763
  let print_import_standard source_fmt () =
764
    fprintf source_fmt
765
      "@[<v>#include <assert.h>@,%a%a%a@]"
766
      (if Machine_types.has_machine_type ()
767
       then pp_print_endcut "#include <stdint.h>"
768
       else pp_print_nothing) ()
769
      (if not !Options.static_mem
770
       then pp_print_endcut "#include <stdlib.h>"
771
       else pp_print_nothing) ()
772
      (if !Options.mpfr
773
       then pp_print_endcut "#include <mpfr.h>"
774
       else pp_print_nothing) ()
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;"
779
      print_alloc_prototype (ind.nodei_id, static)
780
      print_dealloc_prototype ind.nodei_id
781

    
782
  let print_lib_c source_fmt basename prog machines dependencies =
783
    fprintf source_fmt
784
      "@[<v>\
785
       %a\
786
       %a@,\
787
       @,\
788
       %a@,\
789
       %a\
790
       %a\
791
       %a\
792
       %a\
793
       %a\
794
       %a\
795
       %a\
796
       @]@."
797
      print_import_standard ()
798
      print_import_prototype
799
      {
800
        local = true;
801
        name = basename;
802
        content = [];
803
        is_stateful=true (* assuming it is stateful *);
804
      }
805

    
806
      (* Print the svn version number and the supported C standard (C90 or C99) *)
807
      pp_print_version ()
808

    
809
      (* Print dependencies *)
810
      (pp_print_list
811
         ~pp_open_box:pp_open_vbox0
812
         ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
813
         print_import_prototype
814
         ~pp_epilogue:pp_print_cutcut) dependencies
815

    
816
      (* Print consts *)
817
      (pp_print_list
818
         ~pp_open_box:pp_open_vbox0
819
         ~pp_prologue:(pp_print_endcut "/* Global constants (definitions) */")
820
         print_const_def
821
         ~pp_epilogue:pp_print_cutcut) (get_consts prog)
822

    
823
      (* MPFR *)
824
      (if !Options.mpfr then
825
         fun fmt () ->
826
           fprintf fmt
827
             "@[<v>/* Global constants initialization */@,\
828
              %a@,\
829
              @,\
830
              /* Global constants clearing */@,\
831
              %a@]@,@,"
832
             print_global_init_code (basename, prog, dependencies)
833
             print_global_clear_code (basename, prog, dependencies)
834
       else pp_print_nothing) ()
835

    
836
      (if not !Options.static_mem then
837
         fun fmt () ->
838
           fprintf fmt
839
             "@[<v>%a%a@]@,@,"
840
             (pp_print_list
841
                ~pp_open_box:pp_open_vbox0
842
                ~pp_epilogue:pp_print_cut
843
                ~pp_prologue:(pp_print_endcut
844
                                "/* External allocation function prototypes */")
845
                (fun fmt dep ->
846
                   pp_print_list
847
                     ~pp_open_box:pp_open_vbox0
848
                     ~pp_epilogue:pp_print_cut
849
                     print_extern_alloc_prototype
850
                     fmt
851
                     (List.filter_map (fun decl -> match decl.top_decl_desc with
852
                          | ImportedNode ind when not ind.nodei_stateless ->
853
                            Some ind
854
                          | _ -> None) dep.content))) dependencies
855
             (pp_print_list
856
                ~pp_open_box:pp_open_vbox0
857
                ~pp_prologue:(pp_print_endcut
858
                                "/* Node allocation function prototypes */")
859
                ~pp_sep:pp_print_cutcut
860
                (fun fmt m ->
861
                   fprintf fmt "%a;@,%a;"
862
                     print_alloc_prototype (m.mname.node_id, m.mstatic)
863
                     print_dealloc_prototype m.mname.node_id)) machines
864
       else pp_print_nothing) ()
865

    
866
      (* Print the struct definitions of all machines. *)
867
      (pp_print_list
868
         ~pp_open_box:pp_open_vbox0
869
         ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
870
         ~pp_sep:pp_print_cutcut
871
         print_machine_struct
872
         ~pp_epilogue:pp_print_cutcut) machines
873

    
874
      (* Print the spec predicates *)
875
      Mod.pp_predicates machines
876

    
877
      (* Print nodes one by one (in the previous order) *)
878
      (pp_print_list
879
         ~pp_open_box:pp_open_vbox0
880
         ~pp_sep:pp_print_cutcut
881
         (print_machine machines dependencies)) machines
882

    
883
end
884

    
885
(* Local Variables: *)
886
(* compile-command:"make -C ../../.." *)
887
(* End: *)
(9-9/9)