Project

General

Profile

Download (16.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 Corelang
15
open Machine_code_types
16
open Machine_code_common
17
open C_backend_common
18

    
19
(********************************************************************************************)
20
(*                         Header Printing functions                                        *)
21
(********************************************************************************************)
22

    
23

    
24
module type MODIFIERS_HDR = sig
25
  module GhostProto: MODIFIERS_GHOST_PROTO
26
  val print_machine_decl_prefix: Format.formatter -> machine_t -> unit
27
  val pp_import_standard_spec: formatter -> unit -> unit
28
end
29

    
30
module EmptyMod = struct
31
  module GhostProto = EmptyGhostProto
32
  let print_machine_decl_prefix = fun _ _ -> ()
33
  let pp_import_standard_spec _ _ = ()
34
end
35

    
36
module Main = functor (Mod: MODIFIERS_HDR) -> struct
37

    
38
  module Protos = Protos(Mod.GhostProto)
39

    
40
  let print_import_standard fmt () =
41
    (* if Machine_types.has_machine_type () then *)
42
    fprintf fmt
43
      "#include <stdint.h>@,\
44
       %a\
45
       #include \"%s/arrow.h%s\"\
46
       %a"
47
      (if !Options.mpfr then
48
         pp_print_endcut "#include <mpfr.h>"
49
       else pp_print_nothing) ()
50
      (Arrow.arrow_top_decl ()).top_decl_owner
51
      (if !Options.cpp then "pp" else "")
52
      Mod.pp_import_standard_spec ()
53

    
54
  let rec print_static_val pp_var fmt v =
55
    match v.value_desc with
56
    | Cst c ->
57
      pp_c_const fmt c
58
    | Var v ->
59
      pp_var fmt v
60
    | Fun (n, vl) ->
61
      pp_basic_lib_fun (Types.is_int_type v.value_type) n
62
        (print_static_val pp_var) fmt vl
63
    | _ ->
64
      (* TODO: raise proper error *)
65
      eprintf "Internal error: C_backend_header.print_static_val";
66
      assert false
67

    
68
  let print_constant_decl (m, attr, inst) pp_var fmt v =
69
    fprintf fmt "%s %a = %a"
70
      attr
71
      (pp_c_type (sprintf "%s ## %s" inst v.var_id)) v.var_type
72
      (print_static_val pp_var) (get_const_assign m v)
73

    
74
  let pp_var inst const_locals fmt v =
75
    if List.mem v const_locals then
76
      fprintf fmt "%s ## %s" inst v.var_id
77
    else fprintf fmt "%s" v.var_id
78

    
79
  let print_static_constant_decl (_, _, inst as macro) fmt const_locals =
80
    pp_print_list ~pp_open_box:pp_open_vbox0
81
      ~pp_sep:(pp_print_endcut ";\\")  ~pp_eol:(pp_print_endcut ";\\")
82
      (print_constant_decl macro (pp_var inst const_locals))
83
      fmt
84
      const_locals
85

    
86
  let print_static_declare_instance
87
      (m, attr, inst) const_locals fmt (i, (n, static)) =
88
    let values = List.map (value_of_dimension m) static in
89
    fprintf fmt "%a(%s, %a%s)"
90
      pp_machine_static_declare_name (node_name n)
91
      attr
92
      (pp_print_list ~pp_open_box:pp_open_hbox ~pp_sep:pp_print_comma
93
         ~pp_eol:pp_print_comma (print_static_val (pp_var inst const_locals)))
94
      values
95
      i
96

    
97
  let print_static_declare_macro fmt (m, attr, inst as macro) =
98
    let const_locals =
99
      List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
100
    let array_mem =
101
      List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
102
    fprintf fmt
103
      "@[<v 2>\
104
       #define %a(%s, %a%s)\\@,\
105
       %a%s %a %s;\\@,\
106
       %a%a;\
107
       @]"
108
      pp_machine_static_declare_name m.mname.node_id
109
      attr
110
      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
111
         (pp_c_var_read m)) m.mstatic
112
      inst
113
      (* constants *)
114
      (print_static_constant_decl macro) const_locals
115
      attr
116
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
117
      inst
118
      (pp_print_list ~pp_open_box:pp_open_vbox0
119
         ~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\")
120
         (pp_c_decl_local_var m)) array_mem
121
      (pp_print_list ~pp_open_box:pp_open_vbox0
122
         ~pp_sep:(pp_print_endcut ";\\")
123
         (fun fmt (i', m') ->
124
            let path = sprintf "%s ## _%s" inst i' in
125
            fprintf fmt "%a"
126
              (print_static_declare_instance macro const_locals)
127
              (path, m'))) m.minstances
128

    
129
  let print_static_link_instance fmt (i, (m, _)) =
130
    fprintf fmt "%a(%s)" pp_machine_static_link_name (node_name m) i
131

    
132
  (* Allocation of a node struct:
133
     - if node memory is an array/matrix/etc, we cast it to a pointer (see pp_registers_struct)
134
  *)
135
  let print_static_link_macro fmt (m, _, inst) =
136
    let array_mem = List.filter (fun v -> Types.is_array_type v.var_type)
137
        m.mmemory in
138
    fprintf fmt
139
      "@[<v>@[<v 2>\
140
       #define %a(%s) do {\\@,\
141
       %a%a;\\@]@,\
142
       } while (0)\
143
       @]"
144
      pp_machine_static_link_name m.mname.node_id
145
      inst
146
      (pp_print_list ~pp_open_box:pp_open_vbox0
147
         ~pp_sep:(pp_print_endcut ";\\") ~pp_eol:(pp_print_endcut ";\\")
148
         (fun fmt v ->
149
            fprintf fmt "%s._reg.%s = (%a*) &%s"
150
              inst
151
              v.var_id
152
              (fun fmt v -> pp_c_type "" fmt (Types.array_base_type v.var_type)) v
153
              v.var_id)) array_mem
154
      (pp_print_list ~pp_open_box:pp_open_vbox0
155
         ~pp_sep:(pp_print_endcut ";\\")
156
         (fun fmt (i',m') ->
157
            let path = sprintf "%s ## _%s" inst i' in
158
            fprintf fmt "%a;\\@,%s.%s = &%s"
159
              print_static_link_instance (path,m')
160
              inst
161
              i'
162
              path)) m.minstances
163

    
164
  let print_static_alloc_macro fmt (m, attr, inst) =
165
    fprintf fmt
166
      "@[<v>@[<v 2>\
167
       #define %a(%s, %a%s)\\@,\
168
       %a(%s, %a%s);\\@,\
169
       %a(%s);\
170
       @]@]"
171
      pp_machine_static_alloc_name m.mname.node_id
172
      attr
173
      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
174
         (pp_c_var_read m)) m.mstatic
175
      inst
176
      pp_machine_static_declare_name m.mname.node_id
177
      attr
178
      (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
179
         (pp_c_var_read m)) m.mstatic
180
      inst
181
      pp_machine_static_link_name m.mname.node_id
182
      inst
183

    
184
  (* TODO: ACSL
185
     we do multiple things:
186
     - provide the semantics of the node as a predicate: function step and reset are associated to ACSL predicate
187
     - the node is associated to a refinement contract, wrt its ACSL sem
188
     - if the node is a regular node associated to a contract, print the contract as function contract.
189
     - do not print anything if this is a contract node
190
  *)
191
  let print_machine_alloc_decl fmt m =
192
    Mod.print_machine_decl_prefix fmt m;
193
    if not (fst (get_stateless_status m)) then
194
      if !Options.static_mem then
195
        (* Static allocation *)
196
        let macro = (m, mk_attribute m, mk_instance m) in
197
        fprintf fmt "%a@,%a@,%a"
198
          print_static_declare_macro macro
199
          print_static_link_macro macro
200
          print_static_alloc_macro macro
201
      else
202
        (* Dynamic allocation *)
203
        fprintf fmt "extern %a;@,extern %a"
204
          print_alloc_prototype (m.mname.node_id, m.mstatic)
205
          print_dealloc_prototype m.mname.node_id
206

    
207
  let print_machine_struct_top_decl_from_header fmt tdecl =
208
    let inode = imported_node_of_top tdecl in
209
    if not inode.nodei_stateless then
210
      (* Declare struct *)
211
      fprintf fmt "%a;"
212
        (pp_machine_memtype_name ~ghost:false) inode.nodei_id
213

    
214
  let print_stateless_C_prototype fmt (name, inputs, outputs) =
215
    let output =
216
      match outputs with
217
      | [hd] -> hd
218
      | _ -> assert false
219
    in
220
    fprintf fmt "%a %s %a"
221
      (pp_basic_c_type ~pp_c_basic_type_desc ~var_opt:None) output.var_type
222
      name
223
      (pp_print_parenthesized pp_c_decl_input_var) inputs
224

    
225
  let print_machine_decl_top_decl_from_header fmt tdecl =
226
    let inode = imported_node_of_top tdecl in
227
    (*Mod.print_machine_decl_prefix fmt m;*)
228
    let prototype = (inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs) in
229
    if inode.nodei_prototype = Some "C" then
230
      if inode.nodei_stateless then
231
        fprintf fmt "extern %a;" print_stateless_C_prototype prototype
232
      else begin
233
        (* TODO: raise proper error *)
234
        Format.eprintf "internal error: print_machine_decl_top_decl_from_header";
235
        assert false
236
      end
237
    else if inode.nodei_stateless then
238
      fprintf fmt "extern %a;" Protos.print_stateless_prototype prototype
239
    else
240
      let static_inputs = List.filter (fun v -> v.var_dec_const)
241
          inode.nodei_inputs in
242
      let used name =
243
        List.exists (fun v -> v.var_id = name)
244
          (inode.nodei_inputs @ inode.nodei_outputs) in
245
      let self = mk_new_name used "self" in
246
      let mem = mk_new_name used "mem" in
247
      let static_prototype = (inode.nodei_id, static_inputs) in
248
      fprintf fmt
249
        "extern %a;@,\
250
         extern %a;@,\
251
         extern %a;@,\
252
         extern %a;@,\
253
         extern %a;"
254
        (Protos.print_set_reset_prototype self mem) static_prototype
255
        (Protos.print_clear_reset_prototype self mem) static_prototype
256
        (Protos.print_init_prototype self) static_prototype
257
        (Protos.print_clear_prototype self) static_prototype
258
        (Protos.print_step_prototype self mem) prototype
259

    
260
  let print_const_top_decl fmt tdecl =
261
    let cdecl = const_of_top tdecl in
262
    fprintf fmt "extern %a;"
263
      (pp_c_type cdecl.const_id)
264
      (if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
265
       then Types.dynamic_type cdecl.const_type
266
       else cdecl.const_type)
267

    
268
  let rec pp_c_type_decl filename cpt var fmt tdecl =
269
    match tdecl with
270
    | Tydec_any ->
271
      assert false
272
    | Tydec_int ->
273
      fprintf fmt "int %s" var
274
    | Tydec_real when !Options.mpfr ->
275
      fprintf fmt "%s %s" Mpfr.mpfr_t var
276
    | Tydec_real ->
277
      fprintf fmt "double %s" var
278
    (* | Tydec_float         -> fprintf fmt "float %s" var *)
279
    | Tydec_bool ->
280
      fprintf fmt "_Bool %s" var
281
    | Tydec_clock ty ->
282
      pp_c_type_decl filename cpt var fmt ty
283
    | Tydec_const c ->
284
      fprintf fmt "%s %s" c var
285
    | Tydec_array (d, ty) ->
286
      fprintf fmt "%a[%a]" (pp_c_type_decl filename cpt var) ty pp_c_dimension d
287
    | Tydec_enum tl ->
288
      incr cpt;
289
      fprintf fmt "enum _enum_%s_%d %a %s" (protect_filename filename) !cpt
290
        (pp_print_braced pp_print_string) tl var
291
    | Tydec_struct fl ->
292
      incr cpt;
293
      fprintf fmt "struct _struct_%s_%d %a %s" (protect_filename filename) !cpt
294
        (pp_print_braced ~pp_sep:pp_print_semicolon
295
           (fun fmt (label, tdesc) -> pp_c_type_decl filename cpt label fmt tdesc))
296
        fl var
297

    
298
  (* let print_type_definitions fmt filename =
299
   *   let cpt_type = ref 0 in
300
   *   Hashtbl.iter (fun typ decl ->
301
   *       match typ with
302
   *       | Tydec_const var ->
303
   *         begin match decl.top_decl_desc with
304
   *           | TypeDef tdef ->
305
   *             fprintf fmt "typedef %a;@.@."
306
   *               (pp_c_type_decl filename cpt_type var) tdef.tydef_desc
307
   *           | _ -> assert false
308
   *         end
309
   *       | _ -> ()) type_table *)
310

    
311
  let reset_type_definitions, print_type_definition_top_decl_from_header =
312
    let cpt_type = ref 0 in
313
    (fun () -> cpt_type := 0),
314
    (fun filename fmt tdecl ->
315
       let typ = typedef_of_top tdecl in
316
       fprintf fmt "typedef %a;"
317
         (pp_c_type_decl filename cpt_type typ.tydef_id) typ.tydef_desc)
318

    
319
  (********************************************************************************************)
320
  (*                         MAIN Header Printing functions                                   *)
321
  (********************************************************************************************)
322

    
323
  let print_alloc_header header_fmt basename _prog machines dependencies spec =
324
    (* Include once: start *)
325
    let baseNAME = file_to_module_name basename in
326
    fprintf header_fmt
327
      "@[<v>\
328
       %a@,\
329
       #ifndef _%s_alloc@,\
330
       #define _%s_alloc@,\
331
       @,\
332
       /* Import header from %s */@,\
333
       %a@,\
334
       @,\
335
       %a\
336
       %a\
337
       %a\
338
       #endif\
339
       @]"
340

    
341
      (* Print the svn version number and the supported C standard (C90 or C99) *)
342
      pp_print_version ()
343

    
344
      baseNAME baseNAME
345

    
346
      (* Import the header *)
347
      basename
348
      print_import_prototype
349
      {
350
        local = true;
351
        name = basename;
352
        content = [];
353
        is_stateful = true  (* assuming it is staful *);
354
      }
355

    
356
      (* Print dependencies *)
357
      (pp_print_list
358
         ~pp_open_box:pp_open_vbox0
359
         ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
360
         print_import_alloc_prototype
361
         ~pp_epilogue:pp_print_cutcut) dependencies
362

    
363
      (* Print the struct definitions of all machines. *)
364
      (pp_print_list
365
         ~pp_open_box:pp_open_vbox0
366
         ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
367
         ~pp_sep:pp_print_cutcut
368
         print_machine_struct
369
         ~pp_epilogue:pp_print_cutcut) machines
370

    
371
      (* Print the prototypes of all machines *)
372
      (pp_print_list
373
         ~pp_open_box:pp_open_vbox0
374
         ~pp_prologue:(pp_print_endcut
375
                         "/* Node allocation function/macro prototypes */")
376
         ~pp_sep:pp_print_cutcut
377
         print_machine_alloc_decl
378
         ~pp_epilogue:pp_print_cutcut) machines
379
  (* Include once: end *)
380

    
381
  (* Function called when compiling a lusi file and generating the associated C
382
     header. *)
383
  let print_header_from_header header_fmt basename header =
384
    (* Include once: start *)
385
    let baseNAME = file_to_module_name basename in
386
    let types = get_typedefs header in
387
    let consts = get_consts header in
388
    let nodes = get_imported_nodes header in
389
    let dependencies = get_dependencies header in
390
    reset_type_definitions ();
391
    fprintf header_fmt
392
      "@[<v>\
393
       %a@,\
394
       #ifndef _%s@,\
395
       #define _%s@,\
396
       @,\
397
       /* Import standard library */@,\
398
       %a@,\
399
       @,\
400
       %a\
401
       %a\
402
       %a\
403
       %a\
404
       %a\
405
       %a\
406
       #endif\
407
       @]@."
408

    
409
      (* Print the version number and the supported C standard (C90 or C99) *)
410
      pp_print_version ()
411

    
412
      baseNAME baseNAME
413

    
414
      (* imports standard library definitions (arrow) *)
415
      print_import_standard ()
416

    
417
      (* imports dependencies *)
418
      (pp_print_list
419
         ~pp_open_box:pp_open_vbox0
420
         ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
421
         (fun fmt dep ->
422
            let local, name = dependency_of_top dep in
423
            print_import_prototype fmt
424
              {
425
                local;
426
                name;
427
                content = [];
428
                is_stateful = true (* assuming it is stateful *)
429
              })
430
         ~pp_epilogue:pp_print_cutcut)
431
      dependencies
432

    
433
      (* Print the type definitions from the type table *)
434
      (pp_print_list
435
         ~pp_open_box:pp_open_vbox0
436
         ~pp_prologue:(pp_print_endcut "/* Types definitions */")
437
         (print_type_definition_top_decl_from_header basename)
438
         ~pp_epilogue:pp_print_cutcut)
439
      types
440

    
441
      (* Print the global constant declarations. *)
442
      (pp_print_list
443
         ~pp_open_box:pp_open_vbox0
444
         ~pp_prologue:
445
           (pp_print_endcut
446
              "/* Global constants (declarations, definitions are in C file) */")
447
         print_const_top_decl
448
         ~pp_epilogue:pp_print_cutcut)
449
      consts
450

    
451
      (* MPFR *)
452
      (if !Options.mpfr then
453
         fun fmt () -> fprintf fmt
454
             "/* Global initialization declaration */@,\
455
              extern %a;@,@,\
456
              /* Global clear declaration */@,\
457
              extern %a;@,@,"
458
             print_global_init_prototype baseNAME
459
             print_global_clear_prototype baseNAME
460
       else pp_print_nothing) ()
461

    
462
      (* Print the struct declarations of all machines. *)
463
      (pp_print_list
464
         ~pp_open_box:pp_open_vbox0
465
         ~pp_prologue:(pp_print_endcut "/* Struct declarations */")
466
         print_machine_struct_top_decl_from_header
467
         ~pp_epilogue:pp_print_cutcut)
468
      nodes
469

    
470
      (* Print the prototypes of all machines *)
471
      (pp_print_list
472
         ~pp_open_box:pp_open_vbox0
473
         ~pp_prologue:(pp_print_endcut "/* Nodes declarations */")
474
         ~pp_sep:pp_print_cutcut
475
         print_machine_decl_top_decl_from_header
476
         ~pp_epilogue:pp_print_cutcut)
477
      nodes
478

    
479
end
480
(* Local Variables: *)
481
(* compile-command:"make -C ../../.." *)
482
(* End: *)
(4-4/9)