Project

General

Profile

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

    
12
open Utils.Format
13
open Lustre_types
14
open 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
module type MODIFIERS_HDR = sig
24
  module GhostProto : MODIFIERS_GHOST_PROTO
25

    
26
  val print_machine_decl_prefix : Format.formatter -> machine_t -> unit
27

    
28
  val pp_import_arrow : formatter -> unit -> unit
29
end
30

    
31
module EmptyMod = struct
32
  module GhostProto = EmptyGhostProto
33

    
34
  let print_machine_decl_prefix _ _ = ()
35

    
36
  let pp_import_arrow fmt () =
37
    fprintf fmt "#include \"%s/arrow.h%s\""
38
      (Arrow.arrow_top_decl ()).top_decl_owner
39
      (if !Options.cpp then "pp" else "")
40
end
41

    
42
module Main =
43
functor
44
  (Mod : MODIFIERS_HDR)
45
  ->
46
  struct
47
    module Protos = Protos (Mod.GhostProto)
48

    
49
    let print_import_standard fmt () =
50
      (* if Machine_types.has_machine_type () then *)
51
      fprintf fmt "#include <stdint.h>@,%a%a"
52
        (if !Options.mpfr then pp_print_endcut "#include <mpfr.h>"
53
        else pp_print_nothing)
54
        () Mod.pp_import_arrow ()
55

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

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

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

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

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

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

    
125
    let print_static_link_instance fmt (i, (m, _)) =
126
      fprintf fmt "%a(%s)" pp_machine_static_link_name (node_name m) i
127

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

    
151
    let print_static_alloc_macro fmt (m, attr, inst) =
152
      fprintf fmt
153
        "@[<v>@[<v 2>#define %a(%s, %a%s)\\@,%a(%s, %a%s);\\@,%a(%s);@]@]"
154
        pp_machine_static_alloc_name m.mname.node_id attr
155
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
156
           (pp_c_var_read m))
157
        m.mstatic inst pp_machine_static_declare_name m.mname.node_id attr
158
        (pp_print_list ~pp_sep:pp_print_comma ~pp_eol:pp_print_comma
159
           (pp_c_var_read m))
160
        m.mstatic inst pp_machine_static_link_name m.mname.node_id inst
161

    
162
    (* TODO: ACSL we do multiple things: - provide the semantics of the node as
163
       a predicate: function step and reset are associated to ACSL predicate -
164
       the node is associated to a refinement contract, wrt its ACSL sem - if
165
       the node is a regular node associated to a contract, print the contract
166
       as function contract. - do not print anything if this is a contract node *)
167
    let print_machine_alloc_decl fmt m =
168
      Mod.print_machine_decl_prefix fmt m;
169
      if not (fst (get_stateless_status m)) then
170
        if !Options.static_mem then
171
          (* Static allocation *)
172
          let macro = m, mk_attribute m, mk_instance m in
173
          fprintf fmt "%a@,%a@,%a" print_static_declare_macro macro
174
            print_static_link_macro macro print_static_alloc_macro macro
175
        else
176
          (* Dynamic allocation *)
177
          fprintf fmt "extern %a;@,extern %a" print_alloc_prototype
178
            (m.mname.node_id, m.mstatic)
179
            print_dealloc_prototype m.mname.node_id
180

    
181
    let print_machine_struct_top_decl_from_header fmt tdecl =
182
      let inode = imported_node_of_top tdecl in
183
      if not inode.nodei_stateless then
184
        (* Declare struct *)
185
        fprintf fmt "%a;" (pp_machine_memtype_name ~ghost:false) inode.nodei_id
186

    
187
    let print_stateless_C_prototype fmt (name, inputs, outputs) =
188
      let output = match outputs with [ hd ] -> hd | _ -> assert false in
189
      fprintf fmt "%a %s %a"
190
        (pp_basic_c_type ~pp_c_basic_type_desc ~var_opt:None)
191
        output.var_type name
192
        (pp_print_parenthesized pp_c_decl_input_var)
193
        inputs
194

    
195
    let print_machine_decl_top_decl_from_header fmt tdecl =
196
      let inode = imported_node_of_top tdecl in
197
      (*Mod.print_machine_decl_prefix fmt m;*)
198
      let prototype = inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs in
199
      if inode.nodei_prototype = Some "C" then
200
        if inode.nodei_stateless then
201
          fprintf fmt "extern %a;" print_stateless_C_prototype prototype
202
        else (
203
          (* TODO: raise proper error *)
204
          Format.eprintf
205
            "internal error: print_machine_decl_top_decl_from_header";
206
          assert false)
207
      else if inode.nodei_stateless then
208
        fprintf fmt "extern %a;" Protos.print_stateless_prototype prototype
209
      else
210
        let static_inputs =
211
          List.filter (fun v -> v.var_dec_const) inode.nodei_inputs
212
        in
213
        let used name =
214
          List.exists
215
            (fun v -> v.var_id = name)
216
            (inode.nodei_inputs @ inode.nodei_outputs)
217
        in
218
        let self = mk_new_name used "self" in
219
        let mem = mk_new_name used "mem" in
220
        let static_prototype = inode.nodei_id, static_inputs in
221
        fprintf fmt "extern %a;@,extern %a;@,extern %a;@,extern %a;@,extern %a;"
222
          (Protos.print_set_reset_prototype self mem)
223
          static_prototype
224
          (Protos.print_clear_reset_prototype self mem)
225
          static_prototype
226
          (Protos.print_init_prototype self)
227
          static_prototype
228
          (Protos.print_clear_prototype self)
229
          static_prototype
230
          (Protos.print_step_prototype self mem)
231
          prototype
232

    
233
    let print_const_top_decl fmt tdecl =
234
      let cdecl = const_of_top tdecl in
235
      fprintf fmt "extern %a;" (pp_c_type cdecl.const_id)
236
        (if
237
         !Options.mpfr
238
         && Types.(is_real_type (array_base_type cdecl.const_type))
239
        then Types.dynamic_type cdecl.const_type
240
        else cdecl.const_type)
241

    
242
    let rec pp_c_type_decl filename cpt var fmt tdecl =
243
      match tdecl with
244
      | Tydec_any ->
245
        assert false
246
      | Tydec_int ->
247
        fprintf fmt "int %s" var
248
      | Tydec_real when !Options.mpfr ->
249
        fprintf fmt "%s %s" Mpfr.mpfr_t var
250
      | Tydec_real ->
251
        fprintf fmt "double %s" var
252
      (* | Tydec_float -> fprintf fmt "float %s" var *)
253
      | Tydec_bool ->
254
        fprintf fmt "_Bool %s" var
255
      | Tydec_clock ty ->
256
        pp_c_type_decl filename cpt var fmt ty
257
      | Tydec_const c ->
258
        fprintf fmt "%s %s" c var
259
      | Tydec_array (d, ty) ->
260
        fprintf fmt "%a[%a]"
261
          (pp_c_type_decl filename cpt var)
262
          ty pp_c_dimension d
263
      | Tydec_enum tl ->
264
        incr cpt;
265
        fprintf fmt "enum _enum_%s_%d %a %s"
266
          (protect_filename filename)
267
          !cpt
268
          (pp_print_braced pp_print_string)
269
          tl var
270
      | Tydec_struct fl ->
271
        incr cpt;
272
        fprintf fmt "struct _struct_%s_%d %a %s"
273
          (protect_filename filename)
274
          !cpt
275
          (pp_print_braced ~pp_sep:pp_print_semicolon (fun fmt (label, tdesc) ->
276
               pp_c_type_decl filename cpt label fmt tdesc))
277
          fl var
278

    
279
    (* let print_type_definitions fmt filename =
280
     *   let cpt_type = ref 0 in
281
     *   Hashtbl.iter (fun typ decl ->
282
     *       match typ with
283
     *       | Tydec_const var ->
284
     *         begin match decl.top_decl_desc with
285
     *           | TypeDef tdef ->
286
     *             fprintf fmt "typedef %a;@.@."
287
     *               (pp_c_type_decl filename cpt_type var) tdef.tydef_desc
288
     *           | _ -> assert false
289
     *         end
290
     *       | _ -> ()) type_table *)
291

    
292
    let reset_type_definitions, print_type_definition_top_decl_from_header =
293
      let cpt_type = ref 0 in
294
      ( (fun () -> cpt_type := 0),
295
        fun filename fmt tdecl ->
296
          let typ = typedef_of_top tdecl in
297
          fprintf fmt "typedef %a;"
298
            (pp_c_type_decl filename cpt_type typ.tydef_id)
299
            typ.tydef_desc )
300

    
301
    (********************************************************************************************)
302
    (* MAIN Header Printing functions *)
303
    (********************************************************************************************)
304

    
305
    let print_alloc_header header_fmt basename machines dependencies =
306
      (* Include once: start *)
307
      let baseNAME = file_to_module_name basename in
308
      fprintf header_fmt
309
        "@[<v>%a@,\
310
         #ifndef _%s_alloc@,\
311
         #define _%s_alloc@,\
312
         @,\
313
         /* Import header from %s */@,\
314
         %a@,\
315
         @,\
316
         %a%a%a#endif@]"
317
        (* Print the svn version number and the supported C standard (C90 or
318
           C99) *)
319
        pp_print_version () baseNAME baseNAME (* Import the header *) basename
320
        print_import_prototype
321
        {
322
          local = true;
323
          name = basename;
324
          content = [];
325
          is_stateful = true (* assuming it is staful *);
326
        }
327
        (* Print dependencies *)
328
        (pp_print_list ~pp_open_box:pp_open_vbox0
329
           ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
330
           print_import_alloc_prototype ~pp_epilogue:pp_print_cutcut)
331
        dependencies
332
        (* Print the struct definitions of all machines. *)
333
        (pp_print_list ~pp_open_box:pp_open_vbox0
334
           ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
335
           ~pp_sep:pp_print_cutcut print_machine_struct
336
           ~pp_epilogue:pp_print_cutcut)
337
        machines
338
        (* Print the prototypes of all machines *)
339
        (pp_print_list ~pp_open_box:pp_open_vbox0
340
           ~pp_prologue:
341
             (pp_print_endcut "/* Node allocation function/macro prototypes */")
342
           ~pp_sep:pp_print_cutcut print_machine_alloc_decl
343
           ~pp_epilogue:pp_print_cutcut)
344
        machines
345
    (* Include once: end *)
346

    
347
    (* Function called when compiling a lusi file and generating the associated
348
       C header. *)
349
    let print_header_from_header header_fmt basename header =
350
      (* Include once: start *)
351
      let baseNAME = file_to_module_name basename in
352
      let types = get_typedefs header in
353
      let consts = get_consts header in
354
      let nodes = get_imported_nodes header in
355
      let dependencies = get_dependencies header in
356
      reset_type_definitions ();
357
      fprintf header_fmt
358
        "@[<v>%a@,\
359
         #ifndef _%s@,\
360
         #define _%s@,\
361
         @,\
362
         /* Import standard library */@,\
363
         %a@,\
364
         @,\
365
         %a%a%a%a%a%a#endif@]@."
366
        (* Print the version number and the supported C standard (C90 or C99) *)
367
        pp_print_version () baseNAME baseNAME
368
        (* imports standard library definitions (arrow) *)
369
        print_import_standard ()
370
        (* imports dependencies *)
371
        (pp_print_list ~pp_open_box:pp_open_vbox0
372
           ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
373
           (fun fmt dep ->
374
             let local, name = dependency_of_top dep in
375
             print_import_prototype fmt
376
               {
377
                 local;
378
                 name;
379
                 content = [];
380
                 is_stateful = true (* assuming it is stateful *);
381
               })
382
           ~pp_epilogue:pp_print_cutcut)
383
        dependencies
384
        (* Print the type definitions from the type table *)
385
        (pp_print_list ~pp_open_box:pp_open_vbox0
386
           ~pp_prologue:(pp_print_endcut "/* Types definitions */")
387
           (print_type_definition_top_decl_from_header basename)
388
           ~pp_epilogue:pp_print_cutcut)
389
        types
390
        (* Print the global constant declarations. *)
391
        (pp_print_list ~pp_open_box:pp_open_vbox0
392
           ~pp_prologue:
393
             (pp_print_endcut
394
                "/* Global constants (declarations, definitions are in C file) \
395
                 */")
396
           print_const_top_decl ~pp_epilogue:pp_print_cutcut)
397
        consts
398
        (* MPFR *)
399
        (if !Options.mpfr then fun fmt () ->
400
         fprintf fmt
401
           "/* Global initialization declaration */@,\
402
            extern %a;@,\
403
            @,\
404
            /* Global clear declaration */@,\
405
            extern %a;@,\
406
            @,"
407
           print_global_init_prototype baseNAME print_global_clear_prototype
408
           baseNAME
409
        else pp_print_nothing)
410
        ()
411
        (* Print the struct declarations of all machines. *)
412
        (pp_print_list ~pp_open_box:pp_open_vbox0
413
           ~pp_prologue:(pp_print_endcut "/* Struct declarations */")
414
           print_machine_struct_top_decl_from_header
415
           ~pp_epilogue:pp_print_cutcut)
416
        nodes
417
        (* Print the prototypes of all machines *)
418
        (pp_print_list ~pp_open_box:pp_open_vbox0
419
           ~pp_prologue:(pp_print_endcut "/* Nodes declarations */")
420
           ~pp_sep:pp_print_cutcut print_machine_decl_top_decl_from_header
421
           ~pp_epilogue:pp_print_cutcut)
422
        nodes
423
  end
424
(* Local Variables: *)
425
(* compile-command:"make -C ../../.." *)
426
(* End: *)
(4-4/9)