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
module Mpfr = Lustrec_mpfr
20

    
21
(********************************************************************************************)
22
(* Header Printing functions *)
23
(********************************************************************************************)
24

    
25
module type MODIFIERS_HDR = sig
26
  module GhostProto : MODIFIERS_GHOST_PROTO
27

    
28
  val print_machine_decl_prefix : formatter -> machine_t -> unit
29

    
30
  val pp_import_arrow : formatter -> unit -> unit
31
end
32

    
33
module EmptyMod = struct
34
  module GhostProto = EmptyGhostProto
35

    
36
  let print_machine_decl_prefix _ _ = ()
37

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
303
    (********************************************************************************************)
304
    (* MAIN Header Printing functions *)
305
    (********************************************************************************************)
306

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

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