Project

General

Profile

Download (37.1 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
end
21

    
22
module EmptyMod = struct
23
end
24

    
25
module Main = functor (Mod: MODIFIERS_SRC) -> struct
26

    
27
  (********************************************************************************************)
28
  (*                    Instruction Printing functions                                        *)
29
  (********************************************************************************************)
30

    
31

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

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

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

    
77
  let rec is_const_index v =
78
    match v.value_desc with
79
    | Cst (Const_int _) -> true
80
    | Fun (_, vl)       -> List.for_all is_const_index vl
81
    | _                 -> false
82

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

    
110
  let reorder_loop_variables loop_vars =
111
    let (int_loops, var_loops) =
112
      List.partition (function (_, LInt _) -> true | _ -> false) loop_vars
113
    in
114
    var_loops @ int_loops
115

    
116
  (* Prints a one loop variable suffix for arrays *)
117
  let pp_loop_var pp_val fmt lv =
118
    match snd lv with
119
    | LVar v -> fprintf fmt "[%s]" v
120
    | LInt r -> fprintf fmt "[%d]" !r
121
    | LAcc i -> fprintf fmt "[%a]" pp_val i
122

    
123
  (* Prints a suffix of loop variables for arrays *)
124
  let pp_suffix pp_val =
125
    pp_print_list ~pp_sep:pp_print_nothing (pp_loop_var pp_val)
126

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

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

    
204
  (* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
205
     which may yield constant arrays in expressions.
206
     Type is needed to correctly print constant arrays.
207
  *)
208
  let pp_c_val m self pp_var fmt v =
209
    pp_value_suffix m self v.value_type [] pp_var fmt v
210

    
211
  let pp_basic_assign pp_var fmt typ var_name value =
212
    if Types.is_real_type typ && !Options.mpfr
213
    then
214
      Mpfr.pp_inject_assign pp_var fmt (var_name, value)
215
    else
216
      fprintf fmt "%a = %a;"
217
        pp_var var_name
218
        pp_var value
219

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

    
257
  let pp_machine_ pp_machine_name fn_name m self fmt inst =
258
    let (node, static) = try List.assoc inst m.minstances with Not_found ->
259
      eprintf "internal error: %s %s %s %s:@." fn_name m.mname.node_id self inst;
260
      raise Not_found
261
    in
262
    fprintf fmt "%a(%a%s->%s);"
263
      pp_machine_name (node_name node)
264
      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
265
         Dimension.pp_dimension) static
266
      self inst
267

    
268
  let pp_machine_reset =
269
    pp_machine_ pp_machine_reset_name "pp_machine_reset"
270

    
271
  let pp_machine_init =
272
    pp_machine_ pp_machine_init_name "pp_machine_init"
273

    
274
  let pp_machine_clear =
275
    pp_machine_ pp_machine_clear_name "pp_machine_clear"
276

    
277
  let has_c_prototype funname dependencies =
278
    (* We select the last imported node with the name funname.
279
       The order of evaluation of dependencies should be
280
       compatible with overloading. (Not checked yet) *)
281
    let imported_node_opt =
282
      List.fold_left
283
        (fun res dep ->
284
           match res with
285
           | Some _ -> res
286
           | None ->
287
             let decls = dep.content in
288
             let matched = fun t -> match t.top_decl_desc with
289
               | ImportedNode nd -> nd.nodei_id = funname
290
               | _ -> false
291
             in
292
             if List.exists matched decls then
293
               match (List.find matched decls).top_decl_desc with
294
               | ImportedNode nd -> Some nd
295
               | _ -> assert false
296
             else
297
               None) None dependencies in
298
    match imported_node_opt with
299
    | None -> false
300
    | Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false)
301

    
302
  let pp_call m self pp_read pp_write fmt i
303
      (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
304
    try (* stateful node instance *)
305
      let n, _ = List.assoc i m.minstances in
306
      fprintf fmt "%a (%a%a%s->%s);"
307
        pp_machine_step_name (node_name n)
308
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
309
           (pp_c_val m self pp_read)) inputs
310
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
311
           pp_write) outputs
312
        self
313
        i
314
    with Not_found -> (* stateless node instance *)
315
      let n, _ = List.assoc i m.mcalls in
316
      fprintf fmt "%a (%a%a);"
317
        pp_machine_step_name (node_name n)
318
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
319
           (pp_c_val m self pp_read)) inputs
320
        (pp_print_list ~pp_sep:pp_print_comma pp_write) outputs
321

    
322
  let pp_basic_instance_call m self =
323
    pp_call m self (pp_c_var_read m) (pp_c_var_write m)
324

    
325
  let pp_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
326
    let pp_offset pp_var indices fmt var =
327
      fprintf fmt "%a%a"
328
        pp_var var
329
        (pp_print_list ~pp_sep:pp_print_nothing (fun fmt -> fprintf fmt "[%s]"))
330
        indices
331
    in
332
    let rec aux indices fmt typ =
333
      if Types.is_array_type typ
334
      then
335
        let dim = Types.array_type_dimension typ in
336
        let idx = mk_loop_var m () in
337
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
338
          idx idx idx pp_c_dimension dim idx
339
          (aux (idx::indices)) (Types.array_element_type typ)
340
      else
341
        let pp_read  = pp_offset (pp_c_var_read  m) indices in
342
        let pp_write = pp_offset (pp_c_var_write m) indices in
343
        pp_call m self pp_read pp_write fmt i inputs outputs
344
    in
345
    reset_loop_counter ();
346
    aux [] fmt (List.hd inputs).Machine_code_types.value_type
347

    
348
  let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
349
    fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
350
      (pp_c_val m self (pp_c_var_read m)) c
351
      (pp_print_list ~pp_prologue:pp_print_cut
352
         (pp_machine_instr dependencies m self)) tl
353
      (pp_print_list ~pp_prologue:pp_print_cut
354
         (pp_machine_instr dependencies m self)) el
355

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

    
403
  and pp_machine_branch dependencies m self fmt (t, h) =
404
    fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
405
      pp_c_tag t
406
      (pp_print_list ~pp_open_box:pp_open_vbox0
407
         (pp_machine_instr dependencies m self)) h
408

    
409

    
410
  (********************************************************************************************)
411
  (*                         C file Printing functions                                        *)
412
  (********************************************************************************************)
413

    
414
  let print_const_def fmt tdecl =
415
    let cdecl = const_of_top tdecl in
416
    if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
417
    then
418
      fprintf fmt "%a;"
419
        (pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type)
420
    else
421
      fprintf fmt "%a = %a;"
422
        (pp_c_type cdecl.const_id) cdecl.const_type
423
        pp_c_const cdecl.const_value
424

    
425
  let print_alloc_instance fmt (i, (m, static)) =
426
    fprintf fmt "_alloc->%s = %a %a;"
427
      i
428
      pp_machine_alloc_name (node_name m)
429
      (pp_print_parenthesized Dimension.pp_dimension) static
430

    
431
  let print_dealloc_instance fmt (i, (m, _)) =
432
    fprintf fmt "%a (_alloc->%s);"
433
      pp_machine_dealloc_name (node_name m)
434
      i
435

    
436
  let const_locals m =
437
    List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals
438

    
439
  let pp_c_decl_array_mem self fmt id =
440
    fprintf fmt "%a = (%a) (%s->_reg.%s)"
441
      (pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type
442
      (pp_c_type "(*)") id.var_type
443
      self
444
      id.var_id
445

    
446
  let print_alloc_const fmt m =
447
    pp_print_list
448
      ~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";")
449
      (pp_c_decl_local_var m) fmt (const_locals m)
450

    
451
  let print_alloc_array fmt vdecl =
452
    let base_type = Types.array_base_type vdecl.var_type in
453
    let size_types = Types.array_type_multi_dimension vdecl.var_type in
454
    let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in
455
    fprintf fmt
456
      "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,\
457
       assert(_alloc->%s);"
458
      vdecl.var_id
459
      (pp_c_type "") base_type
460
      Dimension.pp_dimension size_type
461
      (pp_c_type "") base_type
462
      vdecl.var_id
463

    
464
  let print_dealloc_array fmt vdecl =
465
    fprintf fmt "free (_alloc->_reg.%s);"
466
      vdecl.var_id
467

    
468
  let array_mems m =
469
    List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
470

    
471
  let print_alloc_code fmt m =
472
    fprintf fmt
473
      "%a *_alloc;@,\
474
       _alloc = (%a *) malloc(sizeof(%a));@,\
475
       assert(_alloc);@,\
476
       %a%areturn _alloc;"
477
      pp_machine_memtype_name m.mname.node_id
478
      pp_machine_memtype_name m.mname.node_id
479
      pp_machine_memtype_name m.mname.node_id
480
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m)
481
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances
482

    
483
  let print_dealloc_code fmt m =
484
    fprintf fmt
485
      "%a%afree (_alloc);@,\
486
       return;"
487
      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array) (array_mems m)
488
      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance) m.minstances
489

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

    
520
  let pp_c_check m self fmt (loc, check) =
521
    fprintf fmt "@[<v>%a@,assert (%a);@]"
522
      Location.pp_c_loc loc
523
      (pp_c_val m self (pp_c_var_read m)) check
524

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

    
574
  let node_of_machine m = {
575
    top_decl_desc = Node m.mname;
576
    top_decl_loc = Location.dummy_loc;
577
    top_decl_owner = "";
578
    top_decl_itf = false
579
  }
580

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

    
622
  let print_reset_code dependencies self fmt m =
623
    pp_print_function
624
      ~pp_prototype:(print_reset_prototype self)
625
      ~prototype:(m.mname.node_id, m.mstatic)
626
      ~pp_local:(pp_c_decl_local_var m)
627
      ~base_locals:(const_locals m)
628
      ~pp_instr:(pp_machine_instr dependencies m self)
629
      ~instrs:m.minit
630
      fmt
631

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

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

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

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

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

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

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

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

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

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

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

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

    
837

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

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

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

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

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

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

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

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

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

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

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

    
976
end
977

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