Project

General

Profile

Download (13.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
module Mpfr = Lustrec_mpfr
19

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

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

    
27
  val pp_machine_decl_prefix : formatter -> machine_t -> unit
28

    
29
  val pp_predicates : formatter -> machine_t list -> unit
30

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

    
33
  val pp_machine_alloc_decl : formatter -> machine_t -> unit
34
end
35

    
36
module EmptyMod = struct
37
  module GhostProto = EmptyGhostProto
38

    
39
  let pp_machine_decl_prefix _ _ = ()
40

    
41
  let pp_predicates _ _ = ()
42

    
43
  let pp_import_arrow fmt () =
44
    fprintf
45
      fmt
46
      "#include \"%s/arrow.h%s\""
47
      (Arrow.arrow_top_decl ()).top_decl_owner
48
      (if !Options.cpp then "pp" else "")
49

    
50
  let pp_machine_alloc_decl _ _ = ()
51
end
52

    
53
module Main =
54
functor
55
  (Mod : MODIFIERS_HDR)
56
  ->
57
  struct
58
    module Protos = Protos (Mod.GhostProto)
59

    
60
    let pp_import_standard fmt () =
61
      (* if Machine_types.has_machine_type () then *)
62
      fprintf
63
        fmt
64
        "#include <stdint.h>@,%a%a"
65
        (if !Options.mpfr then pp_print_endcut "#include <mpfr.h>"
66
        else pp_print_nothing)
67
        ()
68
        Mod.pp_import_arrow
69
        ()
70

    
71
    (* TODO: ACSL we do multiple things: - provide the semantics of the node as
72
       a predicate: function step and reset are associated to ACSL predicate -
73
       the node is associated to a refinement contract, wrt its ACSL sem - if
74
       the node is a regular node associated to a contract, print the contract
75
       as function contract. - do not print anything if this is a contract node *)
76
    let pp_machine_alloc_decl fmt m =
77
      Mod.pp_machine_decl_prefix fmt m;
78
      if not (fst (get_stateless_status m)) then
79
        if !Options.static_mem then
80
          (* Static allocation *)
81
          let macro = m, mk_attribute m, mk_instance m in
82
          fprintf
83
            fmt
84
            "%a@,%a@,%a"
85
            (fun x -> pp_static_declare_macro x)
86
            macro
87
            (fun x -> pp_static_link_macro x)
88
            macro
89
            (fun x -> pp_static_alloc_macro x)
90
            macro
91
        else
92
          (* Dynamic allocation *)
93
          fprintf
94
            fmt
95
            "extern %a;@,extern %a"
96
            pp_alloc_prototype
97
            (m.mname.node_id, m.mstatic)
98
            pp_dealloc_prototype
99
            m.mname.node_id
100

    
101
    let pp_machine_struct_top_decl_from_header fmt tdecl =
102
      let inode = imported_node_of_top tdecl in
103
      if not inode.nodei_stateless then
104
        (* Declare struct *)
105
        fprintf fmt "%a;" (pp_machine_memtype_name ~ghost:false) inode.nodei_id
106

    
107
    let pp_stateless_C_prototype fmt (name, inputs, outputs) =
108
      let output = match outputs with [ hd ] -> hd | _ -> assert false in
109
      fprintf
110
        fmt
111
        "%a %s %a"
112
        (fun x -> pp_basic_c_type ~pp_c_basic_type_desc x)
113
        output.var_type
114
        name
115
        (pp_print_parenthesized pp_c_decl_input_var)
116
        inputs
117

    
118
    let pp_machine_decl_top_decl_from_header fmt tdecl =
119
      let inode = imported_node_of_top tdecl in
120
      (*Mod.print_machine_decl_prefix fmt m;*)
121
      let prototype = inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs in
122
      if inode.nodei_prototype = Some "C" then
123
        if inode.nodei_stateless then
124
          fprintf fmt "extern %a;" pp_stateless_C_prototype prototype
125
        else (
126
          (* TODO: raise proper error *)
127
          Format.eprintf "internal error: pp_machine_decl_top_decl_from_header";
128
          assert false)
129
      else if inode.nodei_stateless then
130
        fprintf fmt "extern %a;" Protos.pp_stateless_prototype prototype
131
      else
132
        let static_inputs =
133
          List.filter (fun v -> v.var_dec_const) inode.nodei_inputs
134
        in
135
        let used name =
136
          List.exists
137
            (fun v -> v.var_id = name)
138
            (inode.nodei_inputs @ inode.nodei_outputs)
139
        in
140
        let self = mk_new_name used "self" in
141
        let mem = mk_new_name used "mem" in
142
        let static_prototype = inode.nodei_id, static_inputs in
143
        fprintf
144
          fmt
145
          "extern %a;@,extern %a;@,extern %a;@,extern %a;@,extern %a;"
146
          (Protos.pp_set_reset_prototype self mem)
147
          static_prototype
148
          (Protos.pp_clear_reset_prototype self mem)
149
          static_prototype
150
          (Protos.pp_init_prototype self)
151
          static_prototype
152
          (Protos.pp_clear_prototype self)
153
          static_prototype
154
          (Protos.pp_step_prototype self mem)
155
          prototype
156

    
157
    let pp_const_top_decl fmt tdecl =
158
      let cdecl = const_of_top tdecl in
159
      fprintf
160
        fmt
161
        "extern %a;"
162
        (pp_c_type cdecl.const_id)
163
        (if
164
         !Options.mpfr
165
         && Types.(is_real_type (array_base_type cdecl.const_type))
166
        then Types.dynamic_type cdecl.const_type
167
        else cdecl.const_type)
168

    
169
    let rec pp_c_type_decl filename cpt var fmt tdecl =
170
      match tdecl with
171
      | Tydec_any ->
172
        assert false
173
      | Tydec_int ->
174
        fprintf fmt "int %s" var
175
      | Tydec_real when !Options.mpfr ->
176
        fprintf fmt "%s %s" Mpfr.mpfr_t var
177
      | Tydec_real ->
178
        fprintf fmt "double %s" var
179
      (* | Tydec_float -> fprintf fmt "float %s" var *)
180
      | Tydec_bool ->
181
        fprintf fmt "_Bool %s" var
182
      | Tydec_clock ty ->
183
        pp_c_type_decl filename cpt var fmt ty
184
      | Tydec_const c ->
185
        fprintf fmt "%s %s" c var
186
      | Tydec_array (d, ty) ->
187
        fprintf
188
          fmt
189
          "%a[%a]"
190
          (pp_c_type_decl filename cpt var)
191
          ty
192
          pp_c_dimension
193
          d
194
      | Tydec_enum tl ->
195
        incr cpt;
196
        fprintf
197
          fmt
198
          "enum _enum_%s_%d %a %s"
199
          (protect_filename filename)
200
          !cpt
201
          (pp_print_braced pp_print_string)
202
          tl
203
          var
204
      | Tydec_struct fl ->
205
        incr cpt;
206
        fprintf
207
          fmt
208
          "struct _struct_%s_%d %a %s"
209
          (protect_filename filename)
210
          !cpt
211
          (pp_print_braced ~pp_sep:pp_print_semicolon (fun fmt (label, tdesc) ->
212
               pp_c_type_decl filename cpt label fmt tdesc))
213
          fl
214
          var
215

    
216
    (* let print_type_definitions fmt filename =
217
     *   let cpt_type = ref 0 in
218
     *   Hashtbl.iter (fun typ decl ->
219
     *       match typ with
220
     *       | Tydec_const var ->
221
     *         begin match decl.top_decl_desc with
222
     *           | TypeDef tdef ->
223
     *             fprintf fmt "typedef %a;@.@."
224
     *               (pp_c_type_decl filename cpt_type var) tdef.tydef_desc
225
     *           | _ -> assert false
226
     *         end
227
     *       | _ -> ()) type_table *)
228

    
229
    let reset_type_definitions, pp_type_definition_top_decl_from_header =
230
      let cpt_type = ref 0 in
231
      ( (fun () -> cpt_type := 0),
232
        fun filename fmt tdecl ->
233
          let typ = typedef_of_top tdecl in
234
          fprintf
235
            fmt
236
            "typedef %a;"
237
            (pp_c_type_decl filename cpt_type typ.tydef_id)
238
            typ.tydef_desc )
239

    
240
    (********************************************************************************************)
241
    (* MAIN Header Printing functions *)
242
    (********************************************************************************************)
243

    
244
    let pp_alloc_header header_fmt basename machines dependencies =
245
      (* Include once: start *)
246
      let baseNAME = file_to_module_name basename in
247
      fprintf
248
        header_fmt
249
        "@[<v>%a@,\
250
         #ifndef _%s_alloc@,\
251
         #define _%s_alloc@,\
252
         @,\
253
         /* Import header from %s */@,\
254
         %a@,\
255
         @,\
256
         %a%a%a%a%a#endif@]@."
257
        (* Print the svn version number and the supported C standard (C90 or
258
           C99) *)
259
        pp_print_version
260
        ()
261
        baseNAME
262
        baseNAME
263
        (* Import the header *) basename
264
        pp_import_prototype
265
        {
266
          local = true;
267
          name = basename;
268
          content = [];
269
          is_stateful = true (* assuming it is staful *);
270
        }
271
        (* Print dependencies *)
272
        (pp_print_list
273
           ~pp_open_box:pp_open_vbox0
274
           ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
275
           pp_import_alloc_prototype
276
           ~pp_epilogue:pp_print_cutcut)
277
        dependencies
278
        (* Print the struct definitions of all machines. *)
279
        (pp_print_list
280
           ~pp_open_box:pp_open_vbox0
281
           ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
282
           ~pp_sep:pp_print_cutcut
283
           pp_machine_struct
284
           ~pp_epilogue:pp_print_cutcut)
285
        machines
286
        (* Copy the spec (valid and memory packs predicates). *)
287
        Mod.pp_predicates
288
        machines
289
        (* Print the prototypes of all machines *)
290
        (pp_print_list
291
           ~pp_open_box:pp_open_vbox0
292
           ~pp_prologue:
293
             (pp_print_endcut "/* Node allocation function/macro prototypes */")
294
           ~pp_sep:pp_print_cutcut
295
           pp_machine_alloc_decl
296
           ~pp_epilogue:pp_print_cutcut)
297
        machines
298
        (* Print the spec prototypes of all machines *)
299
        (pp_print_list
300
           ~pp_open_box:pp_open_vbox0
301
           ~pp_prologue:
302
             (pp_print_endcut
303
                "/* Node allocation function/macro ghost prototypes */")
304
           ~pp_sep:pp_print_cutcut
305
           Mod.pp_machine_alloc_decl
306
           ~pp_epilogue:pp_print_cutcut)
307
        machines
308
    (* Include once: end *)
309

    
310
    (* Function called when compiling a lusi file and generating the associated
311
       C header. *)
312
    let pp_header_from_header header_fmt basename header =
313
      (* Include once: start *)
314
      let baseNAME = file_to_module_name basename in
315
      let types = get_typedefs header in
316
      let consts = get_consts header in
317
      let nodes = get_imported_nodes header in
318
      let dependencies = get_dependencies header in
319
      reset_type_definitions ();
320
      fprintf
321
        header_fmt
322
        "@[<v>%a@,\
323
         #ifndef _%s@,\
324
         #define _%s@,\
325
         @,\
326
         /* Import standard library */@,\
327
         %a@,\
328
         @,\
329
         %a%a%a%a%a%a#endif@]@."
330
        (* Print the version number and the supported C standard (C90 or C99) *)
331
        pp_print_version
332
        ()
333
        baseNAME
334
        baseNAME
335
        (* imports standard library definitions (arrow) *)
336
        pp_import_standard
337
        ()
338
        (* imports dependencies *)
339
        (pp_print_list
340
           ~pp_open_box:pp_open_vbox0
341
           ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
342
           (fun fmt dep ->
343
             let local, name = dependency_of_top dep in
344
             pp_import_prototype
345
               fmt
346
               {
347
                 local;
348
                 name;
349
                 content = [];
350
                 is_stateful = true (* assuming it is stateful *);
351
               })
352
           ~pp_epilogue:pp_print_cutcut)
353
        dependencies
354
        (* Print the type definitions from the type table *)
355
        (pp_print_list
356
           ~pp_open_box:pp_open_vbox0
357
           ~pp_prologue:(pp_print_endcut "/* Types definitions */")
358
           (pp_type_definition_top_decl_from_header basename)
359
           ~pp_epilogue:pp_print_cutcut)
360
        types
361
        (* Print the global constant declarations. *)
362
        (pp_print_list
363
           ~pp_open_box:pp_open_vbox0
364
           ~pp_prologue:
365
             (pp_print_endcut
366
                "/* Global constants (declarations, definitions are in C file) \
367
                 */")
368
           pp_const_top_decl
369
           ~pp_epilogue:pp_print_cutcut)
370
        consts
371
        (* MPFR *)
372
        (if !Options.mpfr then fun fmt () ->
373
         fprintf
374
           fmt
375
           "/* Global initialization declaration */@,\
376
            extern %a;@,\
377
            @,\
378
            /* Global clear declaration */@,\
379
            extern %a;@,\
380
            @,"
381
           pp_global_init_prototype
382
           baseNAME
383
           pp_global_clear_prototype
384
           baseNAME
385
        else pp_print_nothing)
386
        ()
387
        (* Print the struct declarations of all machines. *)
388
        (pp_print_list
389
           ~pp_open_box:pp_open_vbox0
390
           ~pp_prologue:(pp_print_endcut "/* Struct declarations */")
391
           pp_machine_struct_top_decl_from_header
392
           ~pp_epilogue:pp_print_cutcut)
393
        nodes
394
        (* Print the prototypes of all machines *)
395
        (pp_print_list
396
           ~pp_open_box:pp_open_vbox0
397
           ~pp_prologue:(pp_print_endcut "/* Nodes declarations */")
398
           ~pp_sep:pp_print_cutcut
399
           pp_machine_decl_top_decl_from_header
400
           ~pp_epilogue:pp_print_cutcut)
401
        nodes
402
  end
403
(* Local Variables: *)
404
(* compile-command:"make -C ../../.." *)
405
(* End: *)
(7-7/18)