Project

General

Profile

Download (34.8 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
13
open Format
14
open Lustre_types
15
open Machine_code_types
16
open Corelang
17
open Machine_code_common
18
open C_backend_common
19
module Mpfr = Lustrec_mpfr
20

    
21
module type MODIFIERS_SRC = sig
22
  module GhostProto : MODIFIERS_GHOST_PROTO
23

    
24
  val pp_predicates : formatter -> machine_t list -> unit
25

    
26
  val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
27

    
28
  val pp_clear_reset_spec : formatter -> ident -> ident -> machine_t -> unit
29

    
30
  val pp_step_spec :
31
    formatter -> machine_t list -> ident -> ident -> machine_t -> unit
32

    
33
  val pp_step_instr_spec :
34
    machine_t -> ident -> ident -> formatter -> instr_t -> unit
35

    
36
  val pp_ghost_parameter : ident -> formatter -> ident option -> unit
37

    
38
  val pp_contract :
39
    formatter -> machine_t list -> ident -> ident -> machine_t -> unit
40
end
41

    
42
module EmptyMod = struct
43
  module GhostProto = EmptyGhostProto
44

    
45
  let pp_predicates _ _ = ()
46

    
47
  let pp_set_reset_spec _ _ _ _ = ()
48

    
49
  let pp_clear_reset_spec _ _ _ _ = ()
50

    
51
  let pp_step_spec _ _ _ _ _ = ()
52

    
53
  let pp_step_instr_spec _ _ _ _ _ = ()
54

    
55
  let pp_ghost_parameter _ _ _ = ()
56

    
57
  let pp_contract _ _ _ _ _ = ()
58
end
59

    
60
module Main (Mod : MODIFIERS_SRC) = struct
61
  module Protos = Protos (Mod.GhostProto)
62

    
63
  (********************************************************************************************)
64
  (* Instruction Printing functions *)
65
  (********************************************************************************************)
66

    
67
  (* XXX: UNUSED *)
68
  (* let rec merge_static_loop_profiles lp1 lp2 =
69
   *   match lp1, lp2 with
70
   *   | [], _ ->
71
   *     lp2
72
   *   | _, [] ->
73
   *     lp1
74
   *   | p1 :: q1, p2 :: q2 ->
75
   *     (p1 || p2) :: merge_static_loop_profiles q1 q2 *)
76

    
77
  (* XXX: UNUSED *)
78
  (* Returns a list of bool values, indicating whether the indices must be
79
     static or not *)
80
  (* let rec static_loop_profile v =
81
   *   match v.value_desc with
82
   *   | Cst cst ->
83
   *     static_loop_profile_cst cst
84
   *   | Var _ | ResetFlag ->
85
   *     []
86
   *   | Fun (_, vl) ->
87
   *     List.fold_right
88
   *       (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v))
89
   *       vl []
90
   *   | Array vl ->
91
   *     true
92
   *     ::
93
   *     List.fold_right
94
   *       (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v))
95
   *       vl []
96
   *   | Access (v, _) -> (
97
   *       match static_loop_profile v with [] -> [] | _ :: q -> q)
98
   *   | Power (v, _) ->
99
   *     false :: static_loop_profile v
100
   *
101
   * and static_loop_profile_cst cst =
102
   *   match cst with
103
   *   | Const_array cl ->
104
   *     List.fold_right
105
   *       (fun c lp ->
106
   *          merge_static_loop_profiles lp (static_loop_profile_cst c))
107
   *       cl []
108
   *   | _ ->
109
   *     [] *)
110

    
111
  (* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
112
     which may yield constant arrays in expressions. Type is needed to correctly
113
     print constant arrays. *)
114
  let pp_c_val m self pp_var fmt v =
115
    pp_value_suffix m self v.value_type [] pp_var fmt v
116

    
117
  let pp_machine_ pp_machine_name fn_name m fmt ?inst self mem =
118
    let name, is_arrow, static =
119
      match inst with
120
      | Some inst ->
121
        let node, static =
122
          try List.assoc inst m.minstances
123
          with Not_found ->
124
            eprintf
125
              "internal error: %s %s %s %s:@."
126
              fn_name
127
              m.mname.node_id
128
              self
129
              inst;
130
            raise Not_found
131
        in
132
        node_name node, Arrow.td_is_arrow node, static
133
      | None ->
134
        m.mname.node_id, false, []
135
    in
136
    let is_arrow_reset = is_arrow && fn_name = "pp_machine_set_reset" in
137
    fprintf
138
      fmt
139
      "%a(%a%s%a)%a;"
140
      (if is_arrow_reset then fun fmt -> fprintf fmt "%s_reset"
141
      else pp_machine_name)
142
      name
143
      (pp_comma_list ~pp_eol:pp_print_comma Dimension.pp)
144
      static
145
      self
146
      (pp_print_option (fun fmt -> fprintf fmt "->%s"))
147
      inst
148
      (if is_arrow_reset then pp_print_nothing else Mod.pp_ghost_parameter mem)
149
      inst
150

    
151
  let pp_machine_set_reset m self mem fmt inst =
152
    pp_machine_
153
      pp_machine_set_reset_name
154
      "pp_machine_set_reset"
155
      m
156
      fmt
157
      ~inst
158
      self
159
      mem
160

    
161
  let pp_machine_clear_reset m self mem fmt =
162
    pp_machine_
163
      pp_machine_clear_reset_name
164
      "pp_machine_clear_reset"
165
      m
166
      fmt
167
      self
168
      mem
169

    
170
  let pp_machine_init m self mem fmt inst =
171
    pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self mem
172

    
173
  let pp_machine_clear m self mem fmt inst =
174
    pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self mem
175

    
176
  let pp_call m self mem pp_read pp_write fmt i inputs outputs =
177
    try
178
      (* stateful node instance *)
179
      let n, _ = List.assoc i m.minstances in
180
      fprintf
181
        fmt
182
        "%a(%a%a%s->%s)%a;"
183
        pp_machine_step_name
184
        (node_name n)
185
        (pp_comma_list ~pp_eol:pp_print_comma (pp_c_val m self pp_read))
186
        inputs
187
        (pp_comma_list ~pp_eol:pp_print_comma pp_write)
188
        outputs
189
        self
190
        i
191
        (Mod.pp_ghost_parameter mem)
192
        (Some i)
193
    with Not_found ->
194
      (* stateless node instance *)
195
      let n, _ = List.assoc i m.mcalls in
196
      fprintf
197
        fmt
198
        "%a(%a%a);"
199
        pp_machine_step_name
200
        (node_name n)
201
        (pp_comma_list ~pp_eol:pp_print_comma (pp_c_val m self pp_read))
202
        inputs
203
        (pp_comma_list pp_write)
204
        outputs
205

    
206
  let pp_basic_instance_call m self mem =
207
    pp_call m self mem (pp_c_var_read m) (pp_c_var_write m)
208

    
209
  let pp_arrow_call m self mem fmt i outputs =
210
    match outputs with
211
    | [ x ] ->
212
      fprintf
213
        fmt
214
        "%a = %a(%s->%s)%a;"
215
        (pp_c_var_read m)
216
        x
217
        pp_machine_step_name
218
        Arrow.arrow_id
219
        self
220
        i
221
        (Mod.pp_ghost_parameter mem)
222
        (Some i)
223
    | _ ->
224
      assert false
225

    
226
  let pp_instance_call m self mem fmt i inputs outputs =
227
    let pp_offset pp_var indices fmt var =
228
      fprintf
229
        fmt
230
        "%a%a"
231
        pp_var
232
        var
233
        (pp_print_list ~pp_sep:pp_print_nothing (fun fmt -> fprintf fmt "[%s]"))
234
        indices
235
    in
236
    let rec aux indices fmt typ =
237
      if Types.is_array_type typ then
238
        let dim = Types.array_type_dimension typ in
239
        let idx = mk_loop_var m () in
240
        fprintf
241
          fmt
242
          "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
243
          idx
244
          idx
245
          idx
246
          pp_c_dimension
247
          dim
248
          idx
249
          (aux (idx :: indices))
250
          (Types.array_element_type typ)
251
      else
252
        let pp_read = pp_offset (pp_c_var_read m) indices in
253
        let pp_write = pp_offset (pp_c_var_write m) indices in
254
        pp_call m self mem pp_read pp_write fmt i inputs outputs
255
    in
256
    reset_loop_counter ();
257
    aux [] fmt (List.hd inputs).Machine_code_types.value_type
258

    
259
  let rec pp_conditional dependencies m self mem fmt c tl el =
260
    let pp_machine_instrs =
261
      pp_print_list
262
        ~pp_open_box:pp_open_vbox0
263
        ~pp_prologue:pp_print_cut
264
        (pp_machine_instr dependencies m self mem)
265
    in
266
    let pp_cond = pp_c_val m self (pp_c_var_read m) in
267
    match tl, el with
268
    | [], _ :: _ ->
269
      fprintf fmt "@[<v 2>if (!%a) {%a@]@,}" pp_cond c pp_machine_instrs el
270
    | _, [] ->
271
      fprintf fmt "@[<v 2>if (%a) {%a@]@,}" pp_cond c pp_machine_instrs tl
272
    | _, _ ->
273
      fprintf
274
        fmt
275
        "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
276
        pp_cond
277
        c
278
        pp_machine_instrs
279
        tl
280
        pp_machine_instrs
281
        el
282

    
283
  and pp_machine_instr dependencies m self mem fmt instr =
284
    let pp_instr fmt instr =
285
      match get_instr_desc instr with
286
      | MNoReset _ ->
287
        ()
288
      | MSetReset inst ->
289
        pp_machine_set_reset m self mem fmt inst
290
      | MClearReset ->
291
        if not (fst (get_stateless_status m)) then
292
          fprintf
293
            fmt
294
            "%t@,%a"
295
            (pp_machine_clear_reset m self mem)
296
            pp_label
297
            reset_label
298
      | MResetAssign b ->
299
        pp_reset_assign self fmt b
300
      | MLocalAssign (i, v) ->
301
        pp_assign m self (pp_c_var_read m) fmt (i, v)
302
      | MStateAssign (i, v) ->
303
        pp_assign m self (pp_c_var_read m) fmt (i, v)
304
      | MStep ([ i0 ], i, vl)
305
        when Basic_library.is_value_internal_fun
306
               (mk_val (Fun (i, vl)) i0.var_type) ->
307
        pp_machine_instr
308
          dependencies
309
          m
310
          self
311
          mem
312
          fmt
313
          (update_instr_desc
314
             instr
315
             (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
316
      | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
317
        pp_instance_call m self mem fmt i vl il
318
      | MStep ([ i0 ], i, vl) when has_c_prototype i dependencies ->
319
        fprintf
320
          fmt
321
          "%a = %s%a;"
322
          (pp_c_val m self (pp_c_var_read m))
323
          (mk_val (Var i0) i0.var_type)
324
          i
325
          (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m)))
326
          vl
327
      | MStep (il, i, vl) -> (
328
        match List.assoc_opt i m.minstances with
329
        | Some (td, _) when Arrow.td_is_arrow td ->
330
          pp_arrow_call m self mem fmt i il
331
        | _ ->
332
          pp_basic_instance_call m self mem fmt i vl il)
333
      | MBranch (_, []) ->
334
        eprintf
335
          "internal error: C_backend_src.pp_machine_instr %a@."
336
          (pp_instr m)
337
          instr;
338
        assert false
339
      | MBranch (g, hl) ->
340
        if
341
          let t = fst (List.hd hl) in
342
          t = tag_true || t = tag_false
343
        then
344
          (* boolean case, needs special treatment in C because truth value is
345
             not unique *)
346
          (* may disappear if we optimize code by replacing last branch test
347
             with default *)
348
          let tl = try List.assoc tag_true hl with Not_found -> [] in
349
          let el = try List.assoc tag_false hl with Not_found -> [] in
350
          let no_noreset =
351
            List.filter (fun i ->
352
                match i.instr_desc with MNoReset _ -> false | _ -> true)
353
          in
354
          pp_conditional
355
            dependencies
356
            m
357
            self
358
            mem
359
            fmt
360
            g
361
            (no_noreset tl)
362
            (no_noreset el)
363
        else
364
          (* enum type case *)
365
          (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst
366
            (List.hd hl))) in*)
367
          fprintf
368
            fmt
369
            "@[<v 2>switch(%a) {@,%a@,}@]"
370
            (pp_c_val m self (pp_c_var_read m))
371
            g
372
            (pp_print_list_i
373
               ~pp_open_box:pp_open_vbox0
374
               (pp_machine_branch dependencies m self mem (List.length hl)))
375
            hl
376
      | MSpec s ->
377
        fprintf fmt "@[/*@@ %s */@]@ " s
378
      | MComment s ->
379
        fprintf fmt "/*%s*/@ " s
380
    in
381
    fprintf fmt "%a%a" pp_instr instr (Mod.pp_step_instr_spec m self mem) instr
382

    
383
  and pp_machine_branch dependencies m self mem n fmt i (t, h) =
384
    fprintf
385
      fmt
386
      (if i = n - 1
387
       then "@[<v 2>default: // %a@,%a@]"
388
       else "@[<v 2>case %a:@,%a@,break;@]")
389
      pp_c_tag
390
      t
391
      (pp_print_list
392
         ~pp_open_box:pp_open_vbox0
393
         (pp_machine_instr dependencies m self mem))
394
      h
395

    
396
  (* let pp_machine_nospec_instr dependencies m self fmt instr =
397
   *   pp_machine_instr dependencies m self fmt instr
398
   *
399
   * let pp_machine_step_instr dependencies m self mem fmt instr =
400
   *   fprintf fmt "%a%a"
401
   *     (pp_machine_instr dependencies m self) instr
402
   *     (Mod.pp_step_instr_spec m self mem) instr *)
403

    
404
  (********************************************************************************************)
405
  (* C file Printing functions *)
406
  (********************************************************************************************)
407

    
408
  let pp_const_def fmt tdecl =
409
    let cdecl = const_of_top tdecl in
410
    if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
411
    then
412
      fprintf
413
        fmt
414
        "%a;"
415
        (pp_c_type cdecl.const_id)
416
        (Types.dynamic_type cdecl.const_type)
417
    else
418
      fprintf
419
        fmt
420
        "%a = %a;"
421
        (pp_c_type cdecl.const_id)
422
        cdecl.const_type
423
        pp_c_const
424
        cdecl.const_value
425

    
426
  let pp_alloc_instance fmt (i, (m, static)) =
427
    fprintf
428
      fmt
429
      "_alloc->%s = %a %a;"
430
      i
431
      pp_machine_alloc_name
432
      (node_name m)
433
      (pp_print_parenthesized Dimension.pp)
434
      static
435

    
436
  let pp_dealloc_instance fmt (i, (m, _)) =
437
    fprintf fmt "%a (_alloc->%s);" pp_machine_dealloc_name (node_name m) i
438

    
439
  let const_locals m =
440
    List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals
441

    
442
  let pp_c_decl_array_mem self fmt id =
443
    fprintf
444
      fmt
445
      "%a = (%a) (%s->_reg.%s)"
446
      (pp_c_type (sprintf "(*%s)" id.var_id))
447
      id.var_type
448
      (pp_c_type "(*)")
449
      id.var_type
450
      self
451
      id.var_id
452

    
453
  let pp_alloc_const fmt m =
454
    pp_print_list
455
      ~pp_sep:(pp_print_endcut ";")
456
      ~pp_eol:(pp_print_endcut ";")
457
      (pp_c_decl_local_var m)
458
      fmt
459
      (const_locals m)
460

    
461
  let pp_alloc_array fmt vdecl =
462
    let base_type = Types.array_base_type vdecl.var_type in
463
    let size_types = Types.array_type_multi_dimension vdecl.var_type in
464
    let size_type = Dimension.multi_product vdecl.var_loc size_types in
465
    fprintf
466
      fmt
467
      "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,assert(_alloc->%s);"
468
      vdecl.var_id
469
      (pp_c_type "")
470
      base_type
471
      Dimension.pp
472
      size_type
473
      (pp_c_type "")
474
      base_type
475
      vdecl.var_id
476

    
477
  let pp_dealloc_array fmt vdecl =
478
    fprintf fmt "free (_alloc->_reg.%s);" vdecl.var_id
479

    
480
  let array_mems m =
481
    List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
482

    
483
  let pp_alloc_code fmt m =
484
    fprintf
485
      fmt
486
      "%a *_alloc;@,\
487
       _alloc = (%a *) malloc(sizeof(%a));@,\
488
       assert(_alloc);@,\
489
       %a%areturn _alloc;"
490
      (pp_machine_memtype_name ~ghost:false)
491
      m.mname.node_id
492
      (pp_machine_memtype_name ~ghost:false)
493
      m.mname.node_id
494
      (pp_machine_memtype_name ~ghost:false)
495
      m.mname.node_id
496
      (pp_print_list ~pp_sep:pp_print_nothing pp_alloc_array)
497
      (array_mems m)
498
      (pp_print_list ~pp_sep:pp_print_nothing pp_alloc_instance)
499
      m.minstances
500

    
501
  let pp_dealloc_code fmt m =
502
    fprintf
503
      fmt
504
      "%a%afree (_alloc);@,return;"
505
      (pp_print_list ~pp_sep:pp_print_nothing pp_dealloc_array)
506
      (array_mems m)
507
      (pp_print_list ~pp_sep:pp_print_nothing pp_dealloc_instance)
508
      m.minstances
509

    
510
  (* let print_stateless_init_code fmt m self =
511
   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
512
   *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
513
   *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
514
   *     (print_init_prototype self) (m.mname.node_id, m.mstatic)
515
   *     (\* array mems *\)
516
   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
517
   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
518
   *     (\* memory initialization *\)
519
   *     (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
520
   *     (Utils.pp_newline_if_non_empty m.mmemory)
521
   *     (\* sub-machines initialization *\)
522
   *     (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
523
   *     (Utils.pp_newline_if_non_empty m.minit)
524
   *
525
   * let print_stateless_clear_code fmt m self =
526
   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
527
   *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
528
   *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
529
   *     (print_clear_prototype self) (m.mname.node_id, m.mstatic)
530
   *     (\* array mems *\)
531
   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
532
   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
533
   *     (\* memory clear *\)
534
   *     (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
535
   *     (Utils.pp_newline_if_non_empty m.mmemory)
536
   *     (\* sub-machines clear*\)
537
   *     (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
538
   *     (Utils.pp_newline_if_non_empty m.minit) *)
539

    
540
  let pp_c_check m self fmt (loc, check) =
541
    fprintf
542
      fmt
543
      "@[<v>%a@,assert (%a);@]"
544
      Location.pp_c
545
      loc
546
      (pp_c_val m self (pp_c_var_read m))
547
      check
548

    
549
  let pp_print_function ~pp_prototype ~prototype ?(is_contract = false)
550
      ?(pp_spec = pp_print_nothing) ?(pp_local = pp_print_nothing)
551
      ?(base_locals = []) ?(pp_array_mem = pp_print_nothing) ?(array_mems = [])
552
      ?(pp_init_mpfr_local = pp_print_nothing)
553
      ?(pp_clear_mpfr_local = pp_print_nothing) ?(mpfr_locals = [])
554
      ?(pp_check = pp_print_nothing) ?(checks = [])
555
      ?(pp_extra = pp_print_nothing)
556
      ?(pp_instr = fun fmt _ -> pp_print_nothing fmt ()) ?(instrs = []) fmt =
557
    if not is_contract then
558
      fprintf
559
        fmt
560
        "%a@[<v 2>%a {@,%a%a%a%a%a%a%areturn;@]@,}"
561
        pp_spec
562
        ()
563
        pp_prototype
564
        prototype
565
        (* locals *)
566
        (pp_print_list
567
           ~pp_open_box:pp_open_vbox0
568
           ~pp_sep:pp_print_semicolon
569
           ~pp_eol:pp_print_semicolon
570
           pp_local)
571
        base_locals
572
        (* array mems *)
573
        (pp_print_list
574
           ~pp_open_box:pp_open_vbox0
575
           ~pp_sep:pp_print_semicolon
576
           ~pp_eol:pp_print_semicolon
577
           pp_array_mem)
578
        array_mems
579
        (* locals initialization *)
580
        (pp_print_list ~pp_epilogue:pp_print_cut pp_init_mpfr_local)
581
        (mpfr_vars mpfr_locals)
582
        (* check assertions *)
583
        (pp_print_list pp_check)
584
        checks
585
        (* instrs *)
586
        (pp_print_list
587
           ~pp_open_box:pp_open_vbox0
588
           ~pp_epilogue:pp_print_cut
589
           pp_instr)
590
        instrs
591
        (* locals clear *)
592
        (pp_print_list ~pp_epilogue:pp_print_cut pp_clear_mpfr_local)
593
        (mpfr_vars mpfr_locals) (* extra *)
594
        pp_extra
595
        ()
596

    
597
  let node_of_machine m =
598
    {
599
      top_decl_desc = Node m.mname;
600
      top_decl_loc = Location.dummy;
601
      top_decl_owner = "";
602
      top_decl_itf = false;
603
    }
604

    
605
  let pp_stateless_code machines dependencies fmt m =
606
    let self = "__ERROR__" in
607
    let is_contract = m.mis_contract in
608
    if not (!Options.ansi && is_generic_node (node_of_machine m)) then
609
      (* C99 code *)
610
      pp_print_function
611
        ~is_contract
612
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self self m)
613
        ~pp_prototype:Protos.pp_stateless_prototype
614
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
615
        ~pp_local:(pp_c_decl_local_var m)
616
        ~base_locals:m.mstep.step_locals
617
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
618
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
619
        ~mpfr_locals:m.mstep.step_locals
620
        ~pp_check:(pp_c_check m self)
621
        ~checks:m.mstep.step_checks
622
        ~pp_instr:(pp_machine_instr dependencies m self self)
623
        ~instrs:m.mstep.step_instrs
624
        ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self self m)
625
        fmt
626
    else
627
      (* C90 code *)
628
      let gen_locals, base_locals =
629
        List.partition
630
          (fun v -> Types.is_generic_type v.var_type)
631
          m.mstep.step_locals
632
      in
633
      let gen_calls =
634
        List.map
635
          (fun e ->
636
            let id, _, _ = call_of_expr e in
637
            mk_call_var_decl e.expr_loc id)
638
          m.mname.node_gencalls
639
      in
640
      pp_print_function
641
        ~is_contract
642
        ~pp_prototype:Protos.pp_stateless_prototype
643
        ~prototype:
644
          ( m.mname.node_id,
645
            m.mstep.step_inputs @ gen_locals @ gen_calls,
646
            m.mstep.step_outputs )
647
        ~pp_local:(pp_c_decl_local_var m)
648
        ~base_locals
649
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
650
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
651
        ~mpfr_locals:m.mstep.step_locals
652
        ~pp_check:(pp_c_check m self)
653
        ~checks:m.mstep.step_checks
654
        ~pp_instr:(pp_machine_instr dependencies m self self)
655
        ~instrs:m.mstep.step_instrs
656
        ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self self m)
657
        fmt
658

    
659
  let pp_clear_reset_code dependencies self mem fmt m =
660
    let is_contract = m.mis_contract in
661
    pp_print_function
662
      ~is_contract
663
      ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt self mem m)
664
      ~pp_prototype:(Protos.pp_clear_reset_prototype self mem)
665
      ~prototype:(m.mname.node_id, m.mstatic)
666
      ~pp_local:(pp_c_decl_local_var m)
667
      ~base_locals:(const_locals m)
668
      ~pp_instr:(pp_machine_instr dependencies m self mem)
669
      ~instrs:
670
        [
671
          mk_branch
672
            (mk_val ResetFlag Type_predef.type_bool)
673
            [ "true", mkinstr (MResetAssign false) :: m.minit ];
674
        ]
675
      fmt
676

    
677
  let pp_set_reset_code dependencies self mem fmt m =
678
    let is_contract = m.mis_contract in
679
    pp_print_function
680
      ~is_contract
681
      ~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m)
682
      ~pp_prototype:(Protos.pp_set_reset_prototype self mem)
683
      ~prototype:(m.mname.node_id, m.mstatic)
684
      ~pp_instr:(pp_machine_instr dependencies m self mem)
685
      ~instrs:[ mkinstr (MResetAssign true) ]
686
      fmt
687

    
688
  let pp_init_code self fmt m =
689
    let minit =
690
      List.map
691
        (fun i ->
692
          match get_instr_desc i with MSetReset i -> i | _ -> assert false)
693
        m.minit
694
    in
695
    pp_print_function
696
      ~pp_prototype:(Protos.pp_init_prototype self)
697
      ~prototype:(m.mname.node_id, m.mstatic)
698
      ~pp_array_mem:(pp_c_decl_array_mem self)
699
      ~array_mems:(array_mems m)
700
      ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
701
      ~mpfr_locals:m.mmemory
702
      ~pp_extra:(fun fmt () ->
703
        pp_print_list
704
          ~pp_open_box:pp_open_vbox0
705
          ~pp_epilogue:pp_print_cut
706
          (pp_machine_init m self self)
707
          fmt
708
          minit)
709
      fmt
710

    
711
  let pp_clear_code self fmt m =
712
    let minit =
713
      List.map
714
        (fun i ->
715
          match get_instr_desc i with MSetReset i -> i | _ -> assert false)
716
        m.minit
717
    in
718
    pp_print_function
719
      ~pp_prototype:(Protos.pp_clear_prototype self)
720
      ~prototype:(m.mname.node_id, m.mstatic)
721
      ~pp_array_mem:(pp_c_decl_array_mem self)
722
      ~array_mems:(array_mems m)
723
      ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
724
      ~mpfr_locals:m.mmemory
725
      ~pp_extra:(fun fmt () ->
726
        pp_print_list
727
          ~pp_open_box:pp_open_vbox0
728
          ~pp_epilogue:pp_print_cut
729
          (pp_machine_clear m self self)
730
          fmt
731
          minit)
732
      fmt
733

    
734
  let pp_step_code machines dependencies self mem fmt m =
735
    let is_contract = m.mis_contract in
736
    if not (!Options.ansi && is_generic_node (node_of_machine m)) then
737
      (* C99 code *)
738
      pp_print_function
739
        ~is_contract
740
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
741
        ~pp_prototype:(Protos.pp_step_prototype self mem)
742
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
743
        ~pp_local:(pp_c_decl_local_var m)
744
        ~base_locals:m.mstep.step_locals
745
        ~pp_array_mem:(pp_c_decl_array_mem self)
746
        ~array_mems:(array_mems m)
747
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
748
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
749
        ~mpfr_locals:m.mstep.step_locals
750
        ~pp_check:(pp_c_check m self)
751
        ~checks:m.mstep.step_checks
752
        ~pp_instr:(pp_machine_instr dependencies m self mem)
753
        ~instrs:m.mstep.step_instrs
754
        ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self mem m)
755
        fmt
756
    else
757
      (* C90 code *)
758
      let gen_locals, base_locals =
759
        List.partition
760
          (fun v -> Types.is_generic_type v.var_type)
761
          m.mstep.step_locals
762
      in
763
      let gen_calls =
764
        List.map
765
          (fun e ->
766
            let id, _, _ = call_of_expr e in
767
            mk_call_var_decl e.expr_loc id)
768
          m.mname.node_gencalls
769
      in
770
      pp_print_function
771
        ~is_contract
772
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
773
        ~pp_prototype:(Protos.pp_step_prototype self mem)
774
        ~prototype:
775
          ( m.mname.node_id,
776
            m.mstep.step_inputs @ gen_locals @ gen_calls,
777
            m.mstep.step_outputs )
778
        ~pp_local:(pp_c_decl_local_var m)
779
        ~base_locals
780
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
781
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
782
        ~mpfr_locals:m.mstep.step_locals
783
        ~pp_check:(pp_c_check m self)
784
        ~checks:m.mstep.step_checks
785
        ~pp_instr:(pp_machine_instr dependencies m self mem)
786
        ~instrs:m.mstep.step_instrs
787
        ~pp_extra:(fun fmt () -> Mod.pp_contract fmt machines self mem m)
788
        fmt
789

    
790
  (********************************************************************************************)
791
  (* MAIN C file Printing functions *)
792
  (********************************************************************************************)
793

    
794
  let pp_const_initialize m pp_var fmt const =
795
    let var =
796
      Machine_code_common.mk_val
797
        (Var (Corelang.var_decl_of_const const))
798
        const.const_type
799
    in
800
    let rec aux indices value fmt typ =
801
      if Types.is_array_type typ then
802
        let dim = Types.array_type_dimension typ in
803
        let szl = Utils.enumerate (Dimension.size_const dim) in
804
        let typ' = Types.array_element_type typ in
805
        let value =
806
          match value with Const_array ca -> List.nth ca | _ -> assert false
807
        in
808
        pp_print_list
809
          (fun fmt i -> aux (string_of_int i :: indices) (value i) fmt typ')
810
          fmt
811
          szl
812
      else
813
        let indices = List.rev indices in
814
        let pp_var_suffix fmt var =
815
          fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix indices
816
        in
817
        fprintf
818
          fmt
819
          "%a@,%a"
820
          (Mpfr.pp_inject_init pp_var_suffix)
821
          var
822
          (Mpfr.pp_inject_real pp_var_suffix pp_c_const)
823
          (var, value)
824
    in
825
    reset_loop_counter ();
826
    aux [] const.const_value fmt const.const_type
827

    
828
  let pp_const_clear pp_var fmt const =
829
    let m = Machine_code_common.empty_machine in
830
    let var = Corelang.var_decl_of_const const in
831
    let rec aux indices fmt typ =
832
      if Types.is_array_type typ then
833
        let dim = Types.array_type_dimension typ in
834
        let idx = mk_loop_var m () in
835
        fprintf
836
          fmt
837
          "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
838
          idx
839
          idx
840
          idx
841
          pp_c_dimension
842
          dim
843
          idx
844
          (aux (idx :: indices))
845
          (Types.array_element_type typ)
846
      else
847
        let indices = List.rev indices in
848
        let pp_var_suffix fmt var =
849
          fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix indices
850
        in
851
        Mpfr.pp_inject_clear pp_var_suffix fmt var
852
    in
853
    reset_loop_counter ();
854
    aux [] fmt var.var_type
855

    
856
  let pp_import_init fmt dep =
857
    let baseNAME = file_to_module_name dep.name in
858
    fprintf fmt "%a();" pp_global_init_name baseNAME
859

    
860
  let pp_import_clear fmt dep =
861
    let baseNAME = file_to_module_name dep.name in
862
    fprintf fmt "%a();" pp_global_clear_name baseNAME
863

    
864
  let pp_global_init_code fmt (basename, prog, dependencies) =
865
    let baseNAME = file_to_module_name basename in
866
    let constants = List.map const_of_top (get_consts prog) in
867
    fprintf
868
      fmt
869
      "@[<v 2>%a {@,\
870
       static %s init = 0;@,\
871
       @[<v 2>if (!init) { @,\
872
       init = 1;%a%a@]@,\
873
       }@,\
874
       return;@]@,\
875
       }"
876
      pp_global_init_prototype
877
      baseNAME
878
      (pp_c_basic_type_desc Type_predef.type_bool)
879
      (* constants *)
880
      (pp_print_list
881
         ~pp_prologue:pp_print_cut
882
         (pp_const_initialize empty_machine (pp_c_var_read empty_machine)))
883
      (mpfr_consts constants)
884
      (* dependencies initialization *)
885
      (pp_print_list ~pp_prologue:pp_print_cut pp_import_init)
886
      (List.filter (fun dep -> dep.local) dependencies)
887

    
888
  let pp_global_clear_code fmt (basename, prog, dependencies) =
889
    let baseNAME = file_to_module_name basename in
890
    let constants = List.map const_of_top (get_consts prog) in
891
    fprintf
892
      fmt
893
      "@[<v 2>%a {@,\
894
       static %s clear = 0;@,\
895
       @[<v 2>if (!clear) { @,\
896
       clear = 1;%a%a@]@,\
897
       }@,\
898
       return;@]@,\
899
       }"
900
      pp_global_clear_prototype
901
      baseNAME
902
      (pp_c_basic_type_desc Type_predef.type_bool)
903
      (* constants *)
904
      (pp_print_list
905
         ~pp_prologue:pp_print_cut
906
         (pp_const_clear (pp_c_var_read empty_machine)))
907
      (mpfr_consts constants)
908
      (* dependencies initialization *)
909
      (pp_print_list ~pp_prologue:pp_print_cut pp_import_clear)
910
      (List.filter (fun dep -> dep.local) dependencies)
911

    
912
  let pp_alloc_function fmt m =
913
    if not !Options.static_mem then
914
      (* Alloc functions, only if non static mode *)
915
      fprintf
916
        fmt
917
        "@[<v 2>%a {@,%a%a@]@,}@,@[<v 2>%a {@,%a%a@]@,@,"
918
        pp_alloc_prototype
919
        (m.mname.node_id, m.mstatic)
920
        pp_alloc_const
921
        m
922
        pp_alloc_code
923
        m
924
        pp_dealloc_prototype
925
        m.mname.node_id
926
        pp_alloc_const
927
        m
928
        pp_dealloc_code
929
        m
930

    
931
  let pp_mpfr_code self fmt m =
932
    if !Options.mpfr then
933
      fprintf
934
        fmt
935
        "@,@[<v>%a@,%a@]"
936
        (* Init function *)
937
        (pp_init_code self)
938
        m
939
        (* Clear function *)
940
        (pp_clear_code self)
941
        m
942

    
943
  (* TODO: ACSL - a contract machine shall not be directly printed in the C
944
     source - but a regular machine associated to a contract machine shall
945
     integrate the associated statements, updating its memories, at the end of
946
     the function body. - last one may print intermediate comment/acsl if/when
947
     they are present in the sequence of instruction *)
948
  let pp_machine machines dependencies fmt m =
949
    if fst (get_stateless_status m) then
950
      (* Step function *)
951
      pp_stateless_code machines dependencies fmt m
952
    else
953
      let self = mk_self m in
954
      let mem = mk_mem m in
955
      fprintf
956
        fmt
957
        "@[<v>%a%a@,@,%a@,@,%a%a@]"
958
        pp_alloc_function
959
        m
960
        (* Reset functions *)
961
        (pp_clear_reset_code dependencies self mem)
962
        m
963
        (pp_set_reset_code dependencies self mem)
964
        m
965
        (* Step function *)
966
        (pp_step_code machines dependencies self mem)
967
        m
968
        (pp_mpfr_code self)
969
        m
970

    
971
  let pp_import_standard source_fmt () =
972
    fprintf
973
      source_fmt
974
      "@[<v>#include <assert.h>@,%a%a%a@]"
975
      (if Machine_types.has_machine_type () then
976
       pp_print_endcut "#include <stdint.h>"
977
      else pp_print_nothing)
978
      ()
979
      (if not !Options.static_mem then pp_print_endcut "#include <stdlib.h>"
980
      else pp_print_nothing)
981
      ()
982
      (if !Options.mpfr then pp_print_endcut "#include <mpfr.h>"
983
      else pp_print_nothing)
984
      ()
985

    
986
  let pp_extern_alloc_prototype fmt ind =
987
    let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs in
988
    fprintf
989
      fmt
990
      "extern %a;@,extern %a;"
991
      pp_alloc_prototype
992
      (ind.nodei_id, static)
993
      pp_dealloc_prototype
994
      ind.nodei_id
995

    
996
  let pp_lib_c source_fmt basename prog machines dependencies =
997
    fprintf
998
      source_fmt
999
      "@[<v>%a%a@,@,%a@,%a%a%a%a%a%a%a@]@."
1000
      pp_import_standard
1001
      ()
1002
      pp_import_prototype
1003
      {
1004
        local = true;
1005
        name = basename;
1006
        content = [];
1007
        is_stateful = true (* assuming it is stateful *);
1008
      }
1009
      (* Print the svn version number and the supported C standard (C90 or
1010
         C99) *)
1011
      pp_print_version
1012
      ()
1013
      (* Print dependencies *)
1014
      (pp_print_list
1015
         ~pp_open_box:pp_open_vbox0
1016
         ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
1017
         pp_import_prototype
1018
         ~pp_epilogue:pp_print_cutcut)
1019
      dependencies
1020
      (* Print consts *)
1021
      (pp_print_list
1022
         ~pp_open_box:pp_open_vbox0
1023
         ~pp_prologue:(pp_print_endcut "/* Global constants (definitions) */")
1024
         pp_const_def
1025
         ~pp_epilogue:pp_print_cutcut)
1026
      (get_consts prog)
1027
      (* MPFR *)
1028
      (if !Options.mpfr then fun fmt () ->
1029
       fprintf
1030
         fmt
1031
         "@[<v>/* Global constants initialization */@,\
1032
          %a@,\
1033
          @,\
1034
          /* Global constants clearing */@,\
1035
          %a@]@,\
1036
          @,"
1037
         pp_global_init_code
1038
         (basename, prog, dependencies)
1039
         pp_global_clear_code
1040
         (basename, prog, dependencies)
1041
      else pp_print_nothing)
1042
      ()
1043
      (if not !Options.static_mem then fun fmt () ->
1044
       fprintf
1045
         fmt
1046
         "@[<v>%a%a@]@,@,"
1047
         (pp_print_list
1048
            ~pp_open_box:pp_open_vbox0
1049
            ~pp_epilogue:pp_print_cut
1050
            ~pp_prologue:
1051
              (pp_print_endcut "/* External allocation function prototypes */")
1052
            (fun fmt dep ->
1053
              pp_print_list
1054
                ~pp_open_box:pp_open_vbox0
1055
                ~pp_epilogue:pp_print_cut
1056
                pp_extern_alloc_prototype
1057
                fmt
1058
                (List.filter_map
1059
                   (fun decl ->
1060
                     match decl.top_decl_desc with
1061
                     | ImportedNode ind when not ind.nodei_stateless ->
1062
                       Some ind
1063
                     | _ ->
1064
                       None)
1065
                   dep.content)))
1066
         dependencies
1067
         (pp_print_list
1068
            ~pp_open_box:pp_open_vbox0
1069
            ~pp_prologue:
1070
              (pp_print_endcut "/* Node allocation function prototypes */")
1071
            ~pp_sep:pp_print_cutcut
1072
            (fun fmt m ->
1073
              fprintf
1074
                fmt
1075
                "%a;@,%a;"
1076
                pp_alloc_prototype
1077
                (m.mname.node_id, m.mstatic)
1078
                pp_dealloc_prototype
1079
                m.mname.node_id))
1080
         machines
1081
      else pp_print_nothing)
1082
      ()
1083
      (* Print the struct definitions of all machines. *)
1084
      (pp_print_list
1085
         ~pp_open_box:pp_open_vbox0
1086
         ~pp_prologue:(pp_print_endcut "/* Struct definitions */")
1087
         ~pp_sep:pp_print_cutcut
1088
         pp_machine_struct
1089
         ~pp_epilogue:pp_print_cutcut)
1090
      (List.filter (fun m -> not m.mis_contract) machines)
1091
      (* Print the spec predicates *) Mod.pp_predicates
1092
      machines
1093
      (* Print nodes one by one (in the previous order) *)
1094
      (pp_print_list
1095
         ~pp_open_box:pp_open_vbox0
1096
         ~pp_sep:pp_print_cutcut
1097
         (pp_machine machines dependencies))
1098
      machines
1099
end
1100

    
1101
(* Local Variables: *)
1102
(* compile-command:"make -C ../../.." *)
1103
(* End: *)
(17-17/18)