Project

General

Profile

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

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

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

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

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

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

    
39

    
40
  (* Computes the depth to which multi-dimension array assignments should be expanded.
41
     It equals the maximum number of nested static array constructions accessible from root [v].
42
  *)
43
  let rec expansion_depth v =
44
    match v.value_desc with
45
    | Cst cst -> expansion_depth_cst cst
46
    | Var _ -> 0
47
    | Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0
48
    | Array vl    -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0
49
    | Access (v, _) -> max 0 (expansion_depth v - 1)
50
    | Power _  -> 0 (*1 + expansion_depth v*)
51
  and expansion_depth_cst c = 
52
    match c with
53
    | Const_array cl ->
54
      1 + List.fold_right (fun c -> max (expansion_depth_cst c)) cl 0
55
    | _ -> 0
56

    
57
  let rec merge_static_loop_profiles lp1 lp2 =
58
    match lp1, lp2 with
59
    | []      , _        -> lp2
60
    | _       , []       -> lp1
61
    | p1 :: q1, p2 :: q2 -> (p1 || p2) :: merge_static_loop_profiles q1 q2
62

    
63
  (* Returns a list of bool values, indicating whether the indices must be static or not *)
64
  let rec static_loop_profile v =
65
    match v.value_desc with
66
    | Cst cst  -> static_loop_profile_cst cst
67
    | Var _  -> []
68
    | Fun (_, vl) ->
69
      List.fold_right
70
        (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
71
    | Array vl    ->
72
      true :: List.fold_right
73
        (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
74
    | Access (v, _) ->
75
      begin match static_loop_profile v with [] -> [] | _ :: q -> q end
76
    | Power (v, _) -> false :: static_loop_profile v
77
  and static_loop_profile_cst cst =
78
    match cst with
79
      Const_array cl ->
80
      List.fold_right
81
        (fun c lp -> merge_static_loop_profiles lp (static_loop_profile_cst c))
82
        cl []
83
    | _ -> [] 
84

    
85
  let rec is_const_index v =
86
    match v.value_desc with
87
    | Cst (Const_int _) -> true
88
    | Fun (_, vl)       -> List.for_all is_const_index vl
89
    | _                 -> false
90

    
91
  type loop_index = LVar of ident | LInt of int ref | LAcc of value_t
92
(*
93
let rec value_offsets v offsets =
94
 match v, offsets with
95
 | _                        , []          -> v
96
 | Power (v, n)             , _ :: q      -> value_offsets v q
97
 | Array vl                 , LInt r :: q -> value_offsets (List.nth vl !r) q
98
 | Cst (Const_array cl)     , LInt r :: q -> value_offsets (Cst (List.nth cl !r)) q
99
 | Fun (f, vl)              , _           -> Fun (f, List.map (fun v -> value_offsets v offsets) vl)
100
 | _                        , LInt r :: q -> value_offsets (Access (v, Cst (Const_int !r))) q
101
 | _                        , LVar i :: q -> value_offsets (Access (v, Var i)) q
102
*)
103
  (* Computes the list of nested loop variables together with their dimension bounds.
104
     - LInt r stands for loop expansion (no loop variable, but int loop index)
105
     - LVar v stands for loop variable v
106
  *)
107
  let rec mk_loop_variables m ty depth =
108
    match (Types.repr ty).Types.tdesc, depth with
109
    | Types.Tarray (d, ty'), 0 ->
110
      let v = mk_loop_var m () in
111
      (d, LVar v) :: mk_loop_variables m ty' 0
112
    | Types.Tarray (d, ty'), _ ->
113
      let r = ref (-1) in
114
      (d, LInt r) :: mk_loop_variables m ty' (depth - 1)
115
    | _, 0 -> []
116
    | _ -> assert false
117

    
118
  let reorder_loop_variables loop_vars =
119
    let (int_loops, var_loops) =
120
      List.partition (function (_, LInt _) -> true | _ -> false) loop_vars
121
    in
122
    var_loops @ int_loops
123

    
124
  (* Prints a one loop variable suffix for arrays *)
125
  let pp_loop_var pp_val fmt lv =
126
    match snd lv with
127
    | LVar v -> fprintf fmt "[%s]" v
128
    | LInt r -> fprintf fmt "[%d]" !r
129
    | LAcc i -> fprintf fmt "[%a]" pp_val i
130

    
131
  (* Prints a suffix of loop variables for arrays *)
132
  let pp_suffix pp_val =
133
    pp_print_list ~pp_sep:pp_print_nothing (pp_loop_var pp_val)
134

    
135
  (* Prints a value expression [v], with internal function calls only.
136
     [pp_var] is a printer for variables (typically [pp_c_var_read]),
137
     but an offset suffix may be added for array variables
138
  *)
139
  (* Prints a constant value before a suffix (needs casting) *)
140
  let rec pp_c_const_suffix var_type fmt c =
141
    match c with
142
    | Const_int i ->
143
      pp_print_int fmt i
144
    | Const_real r ->
145
      Real.pp fmt r
146
    | Const_tag t ->
147
      pp_c_tag fmt t
148
    | Const_array ca ->
149
      let var_type = Types.array_element_type var_type in
150
      fprintf fmt "(%a[])%a"
151
        (pp_c_type "") var_type
152
        (pp_print_braced (pp_c_const_suffix var_type)) ca
153
    | Const_struct fl ->
154
      pp_print_braced
155
        (fun fmt (f, c) ->
156
           (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)
157
        fmt fl
158
    | Const_string _
159
    | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
160

    
161
  (* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
162
  let rec pp_value_suffix m self var_type loop_vars pp_var fmt value =
163
    (*eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)
164
    let pp_suffix = pp_suffix (pp_value_suffix m self var_type [] pp_var) in
165
    match loop_vars, value.value_desc with
166
    | (x, LAcc i) :: q, _ when is_const_index i ->
167
      let r = ref (Dimension.size_const_dimension (dimension_of_value i)) in
168
      pp_value_suffix m self var_type ((x, LInt r)::q) pp_var fmt value
169
    | (_, LInt r) :: q, Cst (Const_array cl) ->
170
      let var_type = Types.array_element_type var_type in
171
      pp_value_suffix m self var_type q pp_var fmt
172
        (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)
173
    | (_, LInt r) :: q, Array vl ->
174
      let var_type = Types.array_element_type var_type in
175
      pp_value_suffix m self var_type q pp_var fmt (List.nth vl !r)
176
    | loop_var :: q, Array vl      ->
177
      let var_type = Types.array_element_type var_type in
178
      fprintf fmt "(%a[])%a%a"
179
        (pp_c_type "") var_type
180
        (pp_print_braced (pp_value_suffix m self var_type q pp_var)) vl
181
        pp_suffix [loop_var]
182
    | [], Array vl      ->
183
      let var_type = Types.array_element_type var_type in
184
      fprintf fmt "(%a[])%a"
185
        (pp_c_type "") var_type
186
        (pp_print_braced (pp_value_suffix m self var_type [] pp_var)) vl
187
    | _ :: q, Power (v, _)  ->
188
      pp_value_suffix m self var_type q pp_var fmt v
189
    | _, Fun (n, vl)   ->
190
      pp_basic_lib_fun (Types.is_int_type value.value_type) n
191
        (pp_value_suffix m self var_type loop_vars pp_var) fmt vl
192
    | _, Access (v, i) ->
193
      let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
194
      pp_value_suffix m self var_type
195
        ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_var fmt v
196
    | _, Var v ->
197
      if is_memory m v then
198
        (* array memory vars are represented by an indirection to a local var with the right type,
199
           in order to avoid casting everywhere. *)
200
        if Types.is_array_type v.var_type
201
        then fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
202
        else fprintf fmt "%s->_reg.%a%a" self pp_var v pp_suffix loop_vars
203
      else
204
        fprintf fmt "%a%a" pp_var v pp_suffix loop_vars
205
    | _, Cst cst ->
206
      pp_c_const_suffix var_type fmt cst
207
    | _, _ ->
208
      eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@."
209
        Types.print_ty var_type (pp_val m) value pp_suffix loop_vars;
210
      assert false
211

    
212
  (* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
213
     which may yield constant arrays in expressions.
214
     Type is needed to correctly print constant arrays.
215
  *)
216
  let pp_c_val m self pp_var fmt v =
217
    pp_value_suffix m self v.value_type [] pp_var fmt v
218

    
219
  let pp_basic_assign pp_var fmt typ var_name value =
220
    if Types.is_real_type typ && !Options.mpfr
221
    then
222
      Mpfr.pp_inject_assign pp_var fmt (var_name, value)
223
    else
224
      fprintf fmt "%a = %a;"
225
        pp_var var_name
226
        pp_var value
227

    
228
  (* type_directed assignment: array vs. statically sized type
229
     - [var_type]: type of variable to be assigned
230
     - [var_name]: name of variable to be assigned
231
     - [value]: assigned value
232
     - [pp_var]: printer for variables
233
  *)
234
  let pp_assign m self pp_var fmt var_type var_name value =
235
    let depth = expansion_depth value in
236
    (*eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
237
    let loop_vars = mk_loop_variables m var_type depth in
238
    let reordered_loop_vars = reorder_loop_variables loop_vars in
239
    let rec aux typ fmt vars =
240
      match vars with
241
      | [] ->
242
        pp_basic_assign (pp_value_suffix m self var_type loop_vars pp_var)
243
          fmt typ var_name value
244
      | (d, LVar i) :: q ->
245
        let typ' = Types.array_element_type typ in
246
        (*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
247
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
248
          i i i pp_c_dimension d i
249
          (aux typ') q
250
      | (d, LInt r) :: q ->
251
        (*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
252
        let typ' = Types.array_element_type typ in
253
        let szl = Utils.enumerate (Dimension.size_const_dimension d) in
254
        fprintf fmt "@[<v 2>{@,%a@]@,}"
255
          (pp_print_list (fun fmt i -> r := i; aux typ' fmt q)) szl
256
      | _ -> assert false
257
    in
258
    begin
259
      reset_loop_counter ();
260
      (*reset_addr_counter ();*)
261
      aux var_type fmt reordered_loop_vars;
262
      (*eprintf "end pp_assign@.";*)
263
    end
264

    
265
  let pp_machine_ pp_machine_name fn_name m self fmt inst =
266
    let (node, static) = try List.assoc inst m.minstances with Not_found ->
267
      eprintf "internal error: %s %s %s %s:@." fn_name m.mname.node_id self inst;
268
      raise Not_found
269
    in
270
    fprintf fmt "%a(%a%s->%s);"
271
      pp_machine_name (node_name node)
272
      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
273
         Dimension.pp_dimension) static
274
      self inst
275

    
276
  let pp_machine_reset =
277
    pp_machine_ pp_machine_reset_name "pp_machine_reset"
278

    
279
  let pp_machine_init =
280
    pp_machine_ pp_machine_init_name "pp_machine_init"
281

    
282
  let pp_machine_clear =
283
    pp_machine_ pp_machine_clear_name "pp_machine_clear"
284

    
285
  let pp_call m self pp_read pp_write fmt i
286
      (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
287
    try (* stateful node instance *)
288
      let n, _ = List.assoc i m.minstances in
289
      fprintf fmt "%a (%a%a%s->%s);"
290
        pp_machine_step_name (node_name n)
291
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
292
           (pp_c_val m self pp_read)) inputs
293
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
294
           pp_write) outputs
295
        self
296
        i
297
    with Not_found -> (* stateless node instance *)
298
      let n, _ = List.assoc i m.mcalls in
299
      fprintf fmt "%a (%a%a);"
300
        pp_machine_step_name (node_name n)
301
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
302
           (pp_c_val m self pp_read)) inputs
303
        (pp_print_list ~pp_sep:pp_print_comma pp_write) outputs
304

    
305
  let pp_basic_instance_call m self =
306
    pp_call m self (pp_c_var_read m) (pp_c_var_write m)
307

    
308
  let pp_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
309
    let pp_offset pp_var indices fmt var =
310
      fprintf fmt "%a%a"
311
        pp_var var
312
        (pp_print_list ~pp_sep:pp_print_nothing (fun fmt -> fprintf fmt "[%s]"))
313
        indices
314
    in
315
    let rec aux indices fmt typ =
316
      if Types.is_array_type typ
317
      then
318
        let dim = Types.array_type_dimension typ in
319
        let idx = mk_loop_var m () in
320
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
321
          idx idx idx pp_c_dimension dim idx
322
          (aux (idx::indices)) (Types.array_element_type typ)
323
      else
324
        let pp_read  = pp_offset (pp_c_var_read  m) indices in
325
        let pp_write = pp_offset (pp_c_var_write m) indices in
326
        pp_call m self pp_read pp_write fmt i inputs outputs
327
    in
328
    reset_loop_counter ();
329
    aux [] fmt (List.hd inputs).Machine_code_types.value_type
330

    
331
  let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
332
    fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
333
      (pp_c_val m self (pp_c_var_read m)) c
334
      (pp_print_list ~pp_prologue:pp_print_cut
335
         (pp_machine_instr dependencies m self)) tl
336
      (pp_print_list ~pp_prologue:pp_print_cut
337
         (pp_machine_instr dependencies m self)) el
338

    
339
  and pp_machine_instr dependencies (m: machine_t) self fmt instr =
340
    match get_instr_desc instr with
341
    | MNoReset _ -> ()
342
    | MReset i ->
343
      pp_machine_reset m self fmt i
344
    | MLocalAssign (i,v) ->
345
      pp_assign
346
        m self (pp_c_var_read m) fmt
347
        i.var_type (mk_val (Var i) i.var_type) v
348
    | MStateAssign (i,v) ->
349
      pp_assign
350
        m self (pp_c_var_read m) fmt
351
        i.var_type (mk_val (Var i) i.var_type) v
352
    | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->
353
      pp_machine_instr dependencies m self fmt
354
        (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
355
    | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
356
      pp_instance_call m self fmt i vl il
357
    | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
358
      fprintf fmt "%a = %s%a;"
359
        (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
360
        i
361
        (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
362
    | MStep (il, i, vl) ->
363
      pp_basic_instance_call m self fmt i vl il
364
    | MBranch (_, []) ->
365
      eprintf "internal error: C_backend_src.pp_machine_instr %a@."
366
        (pp_instr m) instr;
367
      assert false
368
    | MBranch (g, hl) ->
369
      if let t = fst (List.hd hl) in t = tag_true || t = tag_false
370
      then (* boolean case, needs special treatment in C because truth value is not unique *)
371
        (* may disappear if we optimize code by replacing last branch test with default *)
372
        let tl = try List.assoc tag_true  hl with Not_found -> [] in
373
        let el = try List.assoc tag_false hl with Not_found -> [] in
374
        pp_conditional dependencies m self fmt g tl el
375
      else (* enum type case *)
376
        (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
377
        fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
378
          (pp_c_val m self (pp_c_var_read m)) g
379
          (pp_print_list ~pp_open_box:pp_open_vbox0
380
             (pp_machine_branch dependencies m self)) hl
381
    | MSpec s ->
382
      fprintf fmt "@[/*@@ %s */@]@ " s
383
    | MComment s  ->
384
      fprintf fmt "/*%s*/@ " s
385

    
386
  and pp_machine_branch dependencies m self fmt (t, h) =
387
    fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
388
      pp_c_tag t
389
      (pp_print_list ~pp_open_box:pp_open_vbox0
390
         (pp_machine_instr dependencies m self)) h
391

    
392
  let pp_machine_nospec_instr dependencies m self fmt _i instr =
393
    pp_machine_instr dependencies m self fmt instr
394

    
395
  let pp_machine_step_instr dependencies m self fmt i instr =
396
    fprintf fmt "%a%a%a"
397
      (if i = 0 then
398
         (fun fmt () -> Mod.pp_step_instr_spec m self fmt (i-1, instr))
399
       else
400
         pp_print_nothing) ()
401
      (pp_machine_instr dependencies m self) instr
402
      (Mod.pp_step_instr_spec m self) (i, instr)
403

    
404
  (********************************************************************************************)
405
  (*                         C file Printing functions                                        *)
406
  (********************************************************************************************)
407

    
408
  let print_const_def fmt tdecl =
409
    let cdecl = const_of_top tdecl in
410
    if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
411
    then
412
      fprintf fmt "%a;"
413
        (pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type)
414
    else
415
      fprintf fmt "%a = %a;"
416
        (pp_c_type cdecl.const_id) cdecl.const_type
417
        pp_c_const cdecl.const_value
418

    
419
  let print_alloc_instance fmt (i, (m, static)) =
420
    fprintf fmt "_alloc->%s = %a %a;"
421
      i
422
      pp_machine_alloc_name (node_name m)
423
      (pp_print_parenthesized Dimension.pp_dimension) static
424

    
425
  let print_dealloc_instance fmt (i, (m, _)) =
426
    fprintf fmt "%a (_alloc->%s);"
427
      pp_machine_dealloc_name (node_name m)
428
      i
429

    
430
  let const_locals m =
431
    List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals
432

    
433
  let pp_c_decl_array_mem self fmt id =
434
    fprintf fmt "%a = (%a) (%s->_reg.%s)"
435
      (pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type
436
      (pp_c_type "(*)") id.var_type
437
      self
438
      id.var_id
439

    
440
  let print_alloc_const fmt m =
441
    pp_print_list
442
      ~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";")
443
      (pp_c_decl_local_var m) fmt (const_locals m)
444

    
445
  let print_alloc_array fmt vdecl =
446
    let base_type = Types.array_base_type vdecl.var_type in
447
    let size_types = Types.array_type_multi_dimension vdecl.var_type in
448
    let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in
449
    fprintf fmt
450
      "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,\
451
       assert(_alloc->%s);"
452
      vdecl.var_id
453
      (pp_c_type "") base_type
454
      Dimension.pp_dimension size_type
455
      (pp_c_type "") base_type
456
      vdecl.var_id
457

    
458
  let print_dealloc_array fmt vdecl =
459
    fprintf fmt "free (_alloc->_reg.%s);"
460
      vdecl.var_id
461

    
462
  let array_mems m =
463
    List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
464

    
465
  let print_alloc_code fmt m =
466
    fprintf fmt
467
      "%a *_alloc;@,\
468
       _alloc = (%a *) malloc(sizeof(%a));@,\
469
       assert(_alloc);@,\
470
       %a%areturn _alloc;"
471
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
472
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
473
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
474
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m)
475
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances
476

    
477
  let print_dealloc_code fmt m =
478
    fprintf fmt
479
      "%a%afree (_alloc);@,\
480
       return;"
481
      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array) (array_mems m)
482
      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance) m.minstances
483

    
484
  (* let print_stateless_init_code fmt m self =
485
   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
486
   *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
487
   *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
488
   *     (print_init_prototype self) (m.mname.node_id, m.mstatic)
489
   *     (\* array mems *\)
490
   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
491
   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
492
   *     (\* memory initialization *\)
493
   *     (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
494
   *     (Utils.pp_newline_if_non_empty m.mmemory)
495
   *     (\* sub-machines initialization *\)
496
   *     (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
497
   *     (Utils.pp_newline_if_non_empty m.minit)
498
   *
499
   * let print_stateless_clear_code fmt m self =
500
   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
501
   *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
502
   *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
503
   *     (print_clear_prototype self) (m.mname.node_id, m.mstatic)
504
   *     (\* array mems *\)
505
   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
506
   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
507
   *     (\* memory clear *\)
508
   *     (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
509
   *     (Utils.pp_newline_if_non_empty m.mmemory)
510
   *     (\* sub-machines clear*\)
511
   *     (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
512
   *     (Utils.pp_newline_if_non_empty m.minit) *)
513

    
514
  let pp_c_check m self fmt (loc, check) =
515
    fprintf fmt "@[<v>%a@,assert (%a);@]"
516
      Location.pp_c_loc loc
517
      (pp_c_val m self (pp_c_var_read m)) check
518

    
519
  let pp_print_function
520
      ~pp_prototype ~prototype
521
      ?(pp_spec=pp_print_nothing)
522
      ?(pp_local=pp_print_nothing) ?(base_locals=[])
523
      ?(pp_array_mem=pp_print_nothing) ?(array_mems=[])
524
      ?(pp_init_mpfr_local=pp_print_nothing)
525
      ?(pp_clear_mpfr_local=pp_print_nothing)
526
      ?(mpfr_locals=[])
527
      ?(pp_check=pp_print_nothing) ?(checks=[])
528
      ?(pp_extra=pp_print_nothing)
529
      ?(pp_instr=fun fmt _ _ -> pp_print_nothing fmt ()) ?(instrs=[])
530
      fmt =
531
    fprintf fmt
532
      "%a@[<v 2>%a {@,\
533
       %a%a\
534
       %a%a%a%a%areturn;@]@,\
535
       }"
536
      pp_spec ()
537
      pp_prototype prototype
538
      (* locals *)
539
      (pp_print_list
540
         ~pp_open_box:pp_open_vbox0
541
         ~pp_sep:pp_print_semicolon
542
         ~pp_eol:pp_print_semicolon
543
         pp_local)
544
      base_locals
545
      (* array mems *)
546
      (pp_print_list
547
         ~pp_open_box:pp_open_vbox0
548
         ~pp_sep:pp_print_semicolon
549
         ~pp_eol:pp_print_semicolon
550
         pp_array_mem)
551
      array_mems
552
      (* locals initialization *)
553
      (pp_print_list
554
         ~pp_epilogue:pp_print_cut
555
         pp_init_mpfr_local) (mpfr_vars mpfr_locals)
556
      (* check assertions *)
557
      (pp_print_list pp_check) checks
558
      (* instrs *)
559
      (pp_print_list_i
560
         ~pp_open_box:pp_open_vbox0
561
         ~pp_epilogue:pp_print_cut
562
         pp_instr) instrs
563
      (* locals clear *)
564
      (pp_print_list
565
         ~pp_epilogue:pp_print_cut
566
         pp_clear_mpfr_local) (mpfr_vars mpfr_locals)
567
      (* extra *)
568
      pp_extra ()
569

    
570
  let node_of_machine m = {
571
    top_decl_desc = Node m.mname;
572
    top_decl_loc = Location.dummy_loc;
573
    top_decl_owner = "";
574
    top_decl_itf = false
575
  }
576

    
577
  let print_stateless_code dependencies fmt m =
578
    let self = "__ERROR__" in
579
    if not (!Options.ansi && is_generic_node (node_of_machine m))
580
    then
581
      (* C99 code *)
582
      pp_print_function
583
        ~pp_prototype:print_stateless_prototype
584
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
585
        ~pp_local:(pp_c_decl_local_var m)
586
        ~base_locals:m.mstep.step_locals
587
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
588
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
589
        ~mpfr_locals:m.mstep.step_locals
590
        ~pp_check:(pp_c_check m self)
591
        ~checks:m.mstep.step_checks
592
        ~pp_instr:(pp_machine_nospec_instr dependencies m self)
593
        ~instrs:m.mstep.step_instrs
594
        fmt
595
    else
596
      (* C90 code *)
597
      let gen_locals, base_locals = List.partition (fun v ->
598
          Types.is_generic_type v.var_type) m.mstep.step_locals in
599
      let gen_calls = List.map (fun e ->
600
          let (id, _, _) = call_of_expr e
601
          in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
602
      pp_print_function
603
        ~pp_prototype:print_stateless_prototype
604
        ~prototype:(m.mname.node_id,
605
                    m.mstep.step_inputs @ gen_locals @ gen_calls,
606
                    m.mstep.step_outputs)
607
        ~pp_local:(pp_c_decl_local_var m)
608
        ~base_locals
609
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
610
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
611
        ~mpfr_locals:m.mstep.step_locals
612
        ~pp_check:(pp_c_check m self)
613
        ~checks:m.mstep.step_checks
614
        ~pp_instr:(pp_machine_nospec_instr dependencies m self)
615
        ~instrs:m.mstep.step_instrs
616
        fmt
617

    
618
  let print_reset_code dependencies self fmt m =
619
    pp_print_function
620
      ~pp_spec:(fun fmt () -> Mod.pp_reset_spec fmt self m)
621
      ~pp_prototype:(print_reset_prototype self)
622
      ~prototype:(m.mname.node_id, m.mstatic)
623
      ~pp_local:(pp_c_decl_local_var m)
624
      ~base_locals:(const_locals m)
625
      ~pp_instr:(pp_machine_nospec_instr dependencies m self)
626
      ~instrs:m.minit
627
      fmt
628

    
629
  let print_init_code self fmt m =
630
    let minit = List.map (fun i ->
631
        match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
632
    pp_print_function
633
      ~pp_prototype:(print_init_prototype self)
634
      ~prototype:(m.mname.node_id, m.mstatic)
635
      ~pp_array_mem:(pp_c_decl_array_mem self)
636
      ~array_mems:(array_mems m)
637
      ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
638
      ~mpfr_locals:m.mmemory
639
      ~pp_extra:(fun fmt () ->
640
          pp_print_list
641
            ~pp_open_box:pp_open_vbox0
642
            ~pp_epilogue:pp_print_cut
643
            (pp_machine_init m self)
644
            fmt minit)
645
      fmt
646

    
647
  let print_clear_code self fmt m =
648
    let minit = List.map (fun i ->
649
        match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
650
    pp_print_function
651
      ~pp_prototype:(print_clear_prototype self)
652
      ~prototype:(m.mname.node_id, m.mstatic)
653
      ~pp_array_mem:(pp_c_decl_array_mem self)
654
      ~array_mems:(array_mems m)
655
      ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
656
      ~mpfr_locals:m.mmemory
657
      ~pp_extra:(fun fmt () ->
658
          pp_print_list
659
            ~pp_open_box:pp_open_vbox0
660
            ~pp_epilogue:pp_print_cut
661
            (pp_machine_clear m self)
662
            fmt minit)
663
      fmt
664

    
665
  let print_step_code dependencies self fmt m =
666
    if not (!Options.ansi && is_generic_node (node_of_machine m))
667
    then
668
      (* C99 code *)
669
      pp_print_function
670
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt self m)
671
        ~pp_prototype:(print_step_prototype self)
672
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
673
        ~pp_local:(pp_c_decl_local_var m)
674
        ~base_locals:m.mstep.step_locals
675
        ~pp_array_mem:(pp_c_decl_array_mem self)
676
        ~array_mems:(array_mems m)
677
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
678
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
679
        ~mpfr_locals:m.mstep.step_locals
680
        ~pp_check:(pp_c_check m self)
681
        ~checks:m.mstep.step_checks
682
        ~pp_instr:(pp_machine_step_instr dependencies m self)
683
        ~instrs:m.mstep.step_instrs
684
        fmt
685
    else
686
      (* C90 code *)
687
      let gen_locals, base_locals = List.partition (fun v ->
688
          Types.is_generic_type v.var_type) m.mstep.step_locals in
689
      let gen_calls = List.map (fun e ->
690
          let id, _, _ = call_of_expr e in
691
          mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
692
      pp_print_function
693
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt self m)
694
        ~pp_prototype:(print_step_prototype self)
695
        ~prototype:(m.mname.node_id,
696
                    m.mstep.step_inputs @ gen_locals @ gen_calls,
697
                    m.mstep.step_outputs)
698
        ~pp_local:(pp_c_decl_local_var m)
699
        ~base_locals
700
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
701
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
702
        ~mpfr_locals:m.mstep.step_locals
703
        ~pp_check:(pp_c_check m self)
704
        ~checks:m.mstep.step_checks
705
        ~pp_instr:(pp_machine_step_instr dependencies m self)
706
        ~instrs:m.mstep.step_instrs
707
        fmt
708

    
709
  (********************************************************************************************)
710
  (*                     MAIN C file Printing functions                                       *)
711
  (********************************************************************************************)
712

    
713
  let pp_const_initialize m pp_var fmt const =
714
    let var = Machine_code_common.mk_val
715
        (Var (Corelang.var_decl_of_const const)) const.const_type in
716
    let rec aux indices value fmt typ =
717
      if Types.is_array_type typ
718
      then
719
        let dim = Types.array_type_dimension typ in
720
        let szl = Utils.enumerate (Dimension.size_const_dimension dim) in
721
        let typ' = Types.array_element_type typ in
722
        let value = match value with
723
          | Const_array ca -> List.nth ca
724
          | _ -> assert false in
725
        pp_print_list
726
          (fun fmt i -> aux (string_of_int i :: indices) (value i) fmt typ') fmt szl
727
      else
728
        let indices = List.rev indices in
729
        let pp_var_suffix fmt var =
730
          fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix indices in
731
        fprintf fmt "%a@,%a"
732
          (Mpfr.pp_inject_init pp_var_suffix) var
733
          (Mpfr.pp_inject_real pp_var_suffix pp_c_const) (var, value)
734
    in
735
    reset_loop_counter ();
736
    aux [] const.const_value fmt const.const_type
737

    
738
  let pp_const_clear pp_var fmt const =
739
    let m = Machine_code_common.empty_machine in
740
    let var = Corelang.var_decl_of_const const in
741
    let rec aux indices fmt typ =
742
      if Types.is_array_type typ
743
      then
744
        let dim = Types.array_type_dimension typ in
745
        let idx = mk_loop_var m () in
746
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
747
          idx idx idx pp_c_dimension dim idx
748
          (aux (idx::indices)) (Types.array_element_type typ)
749
      else
750
        let indices = List.rev indices in
751
        let pp_var_suffix fmt var =
752
          fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix indices in
753
        Mpfr.pp_inject_clear pp_var_suffix fmt var
754
    in
755
    reset_loop_counter ();
756
    aux [] fmt var.var_type
757

    
758
  let print_import_init fmt dep =
759
    let baseNAME = file_to_module_name dep.name in
760
    fprintf fmt "%a();" pp_global_init_name baseNAME
761

    
762
  let print_import_clear fmt dep =
763
    let baseNAME = file_to_module_name dep.name in
764
    fprintf fmt "%a();" pp_global_clear_name baseNAME
765

    
766
  let print_global_init_code fmt (basename, prog, dependencies) =
767
    let baseNAME = file_to_module_name basename in
768
    let constants = List.map const_of_top (get_consts prog) in
769
    fprintf fmt
770
      "@[<v 2>%a {@,\
771
       static %s init = 0;@,\
772
       @[<v 2>if (!init) { @,\
773
       init = 1;%a%a@]@,\
774
       }@,\
775
       return;@]@,\
776
       }"
777
      print_global_init_prototype baseNAME
778
      (pp_c_basic_type_desc Type_predef.type_bool)
779
      (* constants *)
780
      (pp_print_list
781
         ~pp_prologue:pp_print_cut
782
         (pp_const_initialize empty_machine (pp_c_var_read empty_machine)))
783
      (mpfr_consts constants)
784
      (* dependencies initialization *)
785
      (pp_print_list
786
         ~pp_prologue:pp_print_cut
787
         print_import_init) (List.filter (fun dep -> dep.local) dependencies)
788

    
789
  let print_global_clear_code fmt (basename, prog, dependencies) =
790
    let baseNAME = file_to_module_name basename in
791
    let constants = List.map const_of_top (get_consts prog) in
792
    fprintf fmt
793
      "@[<v 2>%a {@,\
794
       static %s clear = 0;@,\
795
       @[<v 2>if (!clear) { @,\
796
       clear = 1;%a%a@]@,\
797
       }@,\
798
       return;@]@,\
799
       }"
800
      print_global_clear_prototype baseNAME
801
      (pp_c_basic_type_desc Type_predef.type_bool)
802
      (* constants *)
803
      (pp_print_list
804
         ~pp_prologue:pp_print_cut
805
         (pp_const_clear (pp_c_var_read empty_machine))) (mpfr_consts constants)
806
      (* dependencies initialization *)
807
      (pp_print_list
808
         ~pp_prologue:pp_print_cut
809
         print_import_clear) (List.filter (fun dep -> dep.local) dependencies)
810

    
811
  let print_alloc_function fmt m =
812
    if (not !Options.static_mem) then
813
      (* Alloc functions, only if non static mode *)
814
      fprintf fmt
815
        "@[<v 2>%a {@,\
816
         %a%a@]@,\
817
         }@,\
818
         @[<v 2>%a {@,\
819
         %a%a@]@,\
820
         @,"
821
        print_alloc_prototype (m.mname.node_id, m.mstatic)
822
        print_alloc_const m
823
        print_alloc_code m
824
        print_dealloc_prototype m.mname.node_id
825
        print_alloc_const m
826
        print_dealloc_code m
827

    
828
  let print_mpfr_code self fmt m =
829
    if !Options.mpfr then
830
      fprintf fmt "@,@[<v>%a@,%a@]"
831
        (* Init function *)
832
        (print_init_code self) m
833
        (* Clear function *)
834
        (print_clear_code self) m
835

    
836
  (* TODO: ACSL
837
     - a contract machine shall not be directly printed in the C source
838
     - but a regular machine associated to a contract machine shall integrate
839
       the associated statements, updating its memories, at the end of the
840
       function body.
841
     - last one may print intermediate comment/acsl if/when they are present in
842
       the sequence of instruction
843
  *)
844
  let print_machine dependencies fmt m =
845
    if fst (get_stateless_status m) then
846
      (* Step function *)
847
      print_stateless_code dependencies fmt m
848
    else
849
      let self = mk_self m in
850
      fprintf fmt "@[<v>%a%a@,@,%a%a@]"
851
        print_alloc_function m
852
        (* Reset function *)
853
        (print_reset_code dependencies self) m
854
        (* Step function *)
855
        (print_step_code dependencies self) m
856
        (print_mpfr_code self) m
857

    
858
  let print_import_standard source_fmt () =
859
    fprintf source_fmt
860
      "@[<v>#include <assert.h>@,%a%a%a@]"
861
      (if Machine_types.has_machine_type ()
862
       then pp_print_endcut "#include <stdint.h>"
863
       else pp_print_nothing) ()
864
      (if not !Options.static_mem
865
       then pp_print_endcut "#include <stdlib.h>"
866
       else pp_print_nothing) ()
867
      (if !Options.mpfr
868
       then pp_print_endcut "#include <mpfr.h>"
869
       else pp_print_nothing) ()
870

    
871
  let print_extern_alloc_prototype fmt ind =
872
    let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs in
873
    fprintf fmt "extern %a;@,extern %a;"
874
      print_alloc_prototype (ind.nodei_id, static)
875
      print_dealloc_prototype ind.nodei_id
876

    
877
  let print_lib_c source_fmt basename prog machines dependencies =
878
    fprintf source_fmt
879
      "@[<v>\
880
       %a\
881
       %a@,\
882
       @,\
883
       %a@,\
884
       %a\
885
       %a\
886
       %a\
887
       %a\
888
       %a\
889
       %a\
890
       %a\
891
       @]@."
892
      print_import_standard ()
893
      print_import_prototype
894
      {
895
        local = true;
896
        name = basename;
897
        content = [];
898
        is_stateful=true (* assuming it is stateful *);
899
      }
900

    
901
      (* Print the svn version number and the supported C standard (C90 or C99) *)
902
      pp_print_version ()
903

    
904
      (* Print dependencies *)
905
      (pp_print_list
906
         ~pp_open_box:pp_open_vbox0
907
         ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
908
         print_import_prototype
909
         ~pp_epilogue:pp_print_cutcut) dependencies
910

    
911
      (* Print consts *)
912
      (pp_print_list
913
         ~pp_open_box:pp_open_vbox0
914
         ~pp_prologue:(pp_print_endcut "/* Global constants (definitions) */")
915
         print_const_def
916
         ~pp_epilogue:pp_print_cutcut) (get_consts prog)
917

    
918
      (* MPFR *)
919
      (if !Options.mpfr then
920
         fun fmt () ->
921
           fprintf fmt
922
             "@[<v>/* Global constants initialization */@,\
923
              %a@,\
924
              @,\
925
              /* Global constants clearing */@,\
926
              %a@]@,@,"
927
             print_global_init_code (basename, prog, dependencies)
928
             print_global_clear_code (basename, prog, dependencies)
929
       else pp_print_nothing) ()
930

    
931
      (if not !Options.static_mem then
932
         fun fmt () ->
933
           fprintf fmt
934
             "@[<v>%a%a@]@,@,"
935
             (pp_print_list
936
                ~pp_open_box:pp_open_vbox0
937
                ~pp_epilogue:pp_print_cut
938
                ~pp_prologue:(pp_print_endcut
939
                                "/* External allocation function prototypes */")
940
                (fun fmt dep ->
941
                   pp_print_list
942
                     ~pp_open_box:pp_open_vbox0
943
                     ~pp_epilogue:pp_print_cut
944
                     print_extern_alloc_prototype
945
                     fmt
946
                     (List.filter_map (fun decl -> match decl.top_decl_desc with
947
                          | ImportedNode ind when not ind.nodei_stateless ->
948
                            Some ind
949
                          | _ -> None) dep.content))) dependencies
950
             (pp_print_list
951
                ~pp_open_box:pp_open_vbox0
952
                ~pp_prologue:(pp_print_endcut
953
                                "/* Node allocation function prototypes */")
954
                ~pp_sep:pp_print_cutcut
955
                (fun fmt m ->
956
                   fprintf fmt "%a;@,%a;"
957
                     print_alloc_prototype (m.mname.node_id, m.mstatic)
958
                     print_dealloc_prototype m.mname.node_id)) machines
959
       else pp_print_nothing) ()
960

    
961
      (* Print the struct definitions of all machines. *)
962
      (pp_print_list
963
         ~pp_open_box:pp_open_vbox0
964
         ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
965
         ~pp_sep:pp_print_cutcut
966
         print_machine_struct
967
         ~pp_epilogue:pp_print_cutcut) machines
968

    
969
      (* Print the spec predicates *)
970
      (Mod.pp_predicates dependencies) machines
971

    
972
      (* Print nodes one by one (in the previous order) *)
973
      (pp_print_list
974
         ~pp_open_box:pp_open_vbox0
975
         ~pp_sep:pp_print_cutcut
976
         (print_machine dependencies)) machines
977

    
978
end
979

    
980
(* Local Variables: *)
981
(* compile-command:"make -C ../../.." *)
982
(* End: *)
(10-10/10)