Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/backends/C/c_backend_header.ml
17 17
open C_backend_common
18 18

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

  
23

  
24 23
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_arrow: formatter -> unit -> unit
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
28 29
end
29 30

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

  
34
  let print_machine_decl_prefix _ _ = ()
35

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

  
39
module Main = functor (Mod: MODIFIERS_HDR) -> struct
40

  
41
  module Protos = Protos(Mod.GhostProto)
42

  
43
  let print_import_standard fmt () =
44
    (* if Machine_types.has_machine_type () then *)
45
    fprintf fmt
46
      "#include <stdint.h>@,\
47
       %a\
48
       %a"
49
      (if !Options.mpfr then
50
         pp_print_endcut "#include <mpfr.h>"
51
       else pp_print_nothing) ()
52
      Mod.pp_import_arrow ()
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
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
      | _ ->
233 67
        (* TODO: raise proper error *)
234
        Format.eprintf "internal error: print_machine_decl_top_decl_from_header";
68
        eprintf "Internal error: C_backend_header.print_static_val";
235 69
        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 70

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

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

Also available in: Unified diff