Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

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

  
19 19
module type MODIFIERS_SRC = sig
20
  module GhostProto: MODIFIERS_GHOST_PROTO
21
  val pp_predicates: formatter -> machine_t list -> unit
22
  val pp_set_reset_spec: formatter -> ident -> ident -> machine_t -> unit
23
  val pp_clear_reset_spec: formatter -> ident -> ident -> machine_t -> unit
24
  val pp_step_spec: formatter -> machine_t list -> ident -> ident -> machine_t -> unit
25
  val pp_step_instr_spec: machine_t -> ident -> ident -> formatter -> instr_t -> unit
26
  val pp_ghost_parameter: ident -> formatter -> ident option -> unit
20
  module GhostProto : MODIFIERS_GHOST_PROTO
21

  
22
  val pp_predicates : formatter -> machine_t list -> unit
23

  
24
  val pp_set_reset_spec : formatter -> ident -> ident -> machine_t -> unit
25

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

  
28
  val pp_step_spec :
29
    formatter -> machine_t list -> ident -> ident -> machine_t -> unit
30

  
31
  val pp_step_instr_spec :
32
    machine_t -> ident -> ident -> formatter -> instr_t -> unit
33

  
34
  val pp_ghost_parameter : ident -> formatter -> ident option -> unit
27 35
end
28 36

  
29 37
module EmptyMod = struct
30 38
  module GhostProto = EmptyGhostProto
39

  
31 40
  let pp_predicates _ _ = ()
41

  
32 42
  let pp_set_reset_spec _ _ _ _ = ()
43

  
33 44
  let pp_clear_reset_spec _ _ _ _ = ()
45

  
34 46
  let pp_step_spec _ _ _ _ _ = ()
47

  
35 48
  let pp_step_instr_spec _ _ _ _ _ = ()
49

  
36 50
  let pp_ghost_parameter _ _ _ = ()
37 51
end
38 52

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

  
41
  module Protos = Protos(Mod.GhostProto)
42

  
43
  (********************************************************************************************)
44
  (*                    Instruction Printing functions                                        *)
45
  (********************************************************************************************)
46

  
47

  
48
  let rec merge_static_loop_profiles lp1 lp2 =
49
    match lp1, lp2 with
50
    | []      , _        -> lp2
51
    | _       , []       -> lp1
52
    | p1 :: q1, p2 :: q2 -> (p1 || p2) :: merge_static_loop_profiles q1 q2
53

  
54
  (* Returns a list of bool values, indicating whether the indices must be static or not *)
55
  let rec static_loop_profile v =
56
    match v.value_desc with
57
    | Cst cst  -> static_loop_profile_cst cst
58
    | Var _  | ResetFlag -> []
59
    | Fun (_, vl) ->
60
      List.fold_right
61
        (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
62
    | Array vl    ->
63
      true :: List.fold_right
64
        (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
65
    | Access (v, _) ->
66
      begin match static_loop_profile v with [] -> [] | _ :: q -> q end
67
    | Power (v, _) -> false :: static_loop_profile v
68
  and static_loop_profile_cst cst =
69
    match cst with
70
      Const_array cl ->
71
      List.fold_right
72
        (fun c lp -> merge_static_loop_profiles lp (static_loop_profile_cst c))
73
        cl []
74
    | _ -> [] 
75

  
76

  
77
  (* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
78
     which may yield constant arrays in expressions.
79
     Type is needed to correctly print constant arrays.
80
  *)
81
  let pp_c_val m self pp_var fmt v =
82
    pp_value_suffix m self v.value_type [] pp_var fmt v
83

  
84
  let pp_machine_ pp_machine_name fn_name m fmt ?inst self mem =
85
    let name, is_arrow, static =
86
      match inst with
87
      | Some inst ->
88
        let node, static = try List.assoc inst m.minstances with Not_found ->
89
          eprintf "internal error: %s %s %s %s:@."
90
            fn_name m.mname.node_id self inst;
91
          raise Not_found
92
        in
93
        node_name node, Arrow.td_is_arrow node, static
94
      | None ->
95
        m.mname.node_id, false, []
96
    in
97
    let is_arrow_reset = is_arrow && fn_name = "pp_machine_set_reset" in
98
    fprintf fmt "%a(%a%s%a)%a;"
99
      (if is_arrow_reset then
100
         (fun fmt -> fprintf fmt "%s_reset")
101
       else
102
         pp_machine_name) name
103
      (pp_comma_list ~pp_eol:pp_print_comma Dimension.pp_dimension) static
104
      self
105
      (pp_print_option (fun fmt -> fprintf fmt "->%s")) inst
106
      (if is_arrow_reset then pp_print_nothing else Mod.pp_ghost_parameter mem)
107
      inst
108

  
109
  let pp_machine_set_reset m self mem fmt inst =
110
    pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst
111
      self mem
112

  
113
  let pp_machine_clear_reset m self mem fmt =
114
    pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt
115
      self mem
116

  
117
  let pp_machine_init m self mem fmt inst =
118
    pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self mem
119

  
120
  let pp_machine_clear m self mem fmt inst =
121
    pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self mem
122

  
123
  let pp_call m self mem pp_read pp_write fmt i inputs outputs =
124
    try (* stateful node instance *)
125
      let n, _ = List.assoc i m.minstances in
126
      fprintf fmt "%a(%a%a%s->%s)%a;"
127
        pp_machine_step_name (node_name n)
128
        (pp_comma_list ~pp_eol:pp_print_comma
129
           (pp_c_val m self pp_read)) inputs
130
        (pp_comma_list ~pp_eol:pp_print_comma
131
           pp_write) outputs
132
        self
133
        i
134
        (Mod.pp_ghost_parameter mem) (Some i)
135
    with Not_found -> (* stateless node instance *)
136
      let n, _ = List.assoc i m.mcalls in
137
      fprintf fmt "%a(%a%a);"
138
        pp_machine_step_name (node_name n)
139
        (pp_comma_list ~pp_eol:pp_print_comma
140
           (pp_c_val m self pp_read)) inputs
141
        (pp_comma_list pp_write) outputs
142

  
143
  let pp_basic_instance_call m self mem =
144
    pp_call m self mem (pp_c_var_read m) (pp_c_var_write m)
145

  
146
  let pp_arrow_call m self mem fmt i outputs =
147
    match outputs with
148
    | [x] ->
149
      fprintf fmt "%a = %a(%s->%s)%a;"
150
        (pp_c_var_read m) x
151
        pp_machine_step_name Arrow.arrow_id
152
        self
153
        i
154
        (Mod.pp_ghost_parameter mem) (Some i)
155
    | _ -> assert false
156

  
157
  let pp_instance_call m self mem fmt i inputs outputs =
158
    let pp_offset pp_var indices fmt var =
159
      fprintf fmt "%a%a"
160
        pp_var var
161
        (pp_print_list ~pp_sep:pp_print_nothing (fun fmt -> fprintf fmt "[%s]"))
162
        indices
163
    in
164
    let rec aux indices fmt typ =
165
      if Types.is_array_type typ
53
module Main =
54
functor
55
  (Mod : MODIFIERS_SRC)
56
  ->
57
  struct
58
    module Protos = Protos (Mod.GhostProto)
59

  
60
    (********************************************************************************************)
61
    (* Instruction Printing functions *)
62
    (********************************************************************************************)
63

  
64
    let rec merge_static_loop_profiles lp1 lp2 =
65
      match lp1, lp2 with
66
      | [], _ ->
67
        lp2
68
      | _, [] ->
69
        lp1
70
      | p1 :: q1, p2 :: q2 ->
71
        (p1 || p2) :: merge_static_loop_profiles q1 q2
72

  
73
    (* Returns a list of bool values, indicating whether the indices must be
74
       static or not *)
75
    let rec static_loop_profile v =
76
      match v.value_desc with
77
      | Cst cst ->
78
        static_loop_profile_cst cst
79
      | Var _ | ResetFlag ->
80
        []
81
      | Fun (_, vl) ->
82
        List.fold_right
83
          (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v))
84
          vl []
85
      | Array vl ->
86
        true
87
        ::
88
        List.fold_right
89
          (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v))
90
          vl []
91
      | Access (v, _) -> (
92
        match static_loop_profile v with [] -> [] | _ :: q -> q)
93
      | Power (v, _) ->
94
        false :: static_loop_profile v
95

  
96
    and static_loop_profile_cst cst =
97
      match cst with
98
      | Const_array cl ->
99
        List.fold_right
100
          (fun c lp ->
101
            merge_static_loop_profiles lp (static_loop_profile_cst c))
102
          cl []
103
      | _ ->
104
        []
105

  
106
    (* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
107
       which may yield constant arrays in expressions. Type is needed to
108
       correctly print constant arrays. *)
109
    let pp_c_val m self pp_var fmt v =
110
      pp_value_suffix m self v.value_type [] pp_var fmt v
111

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

  
140
    let pp_machine_set_reset m self mem fmt inst =
141
      pp_machine_ pp_machine_set_reset_name "pp_machine_set_reset" m fmt ~inst
142
        self mem
143

  
144
    let pp_machine_clear_reset m self mem fmt =
145
      pp_machine_ pp_machine_clear_reset_name "pp_machine_clear_reset" m fmt
146
        self mem
147

  
148
    let pp_machine_init m self mem fmt inst =
149
      pp_machine_ pp_machine_init_name "pp_machine_init" m fmt ~inst self mem
150

  
151
    let pp_machine_clear m self mem fmt inst =
152
      pp_machine_ pp_machine_clear_name "pp_machine_clear" m fmt ~inst self mem
153

  
154
    let pp_call m self mem pp_read pp_write fmt i inputs outputs =
155
      try
156
        (* stateful node instance *)
157
        let n, _ = List.assoc i m.minstances in
158
        fprintf fmt "%a(%a%a%s->%s)%a;" pp_machine_step_name (node_name n)
159
          (pp_comma_list ~pp_eol:pp_print_comma (pp_c_val m self pp_read))
160
          inputs
161
          (pp_comma_list ~pp_eol:pp_print_comma pp_write)
162
          outputs self i
163
          (Mod.pp_ghost_parameter mem)
164
          (Some i)
165
      with Not_found ->
166
        (* stateless node instance *)
167
        let n, _ = List.assoc i m.mcalls in
168
        fprintf fmt "%a(%a%a);" pp_machine_step_name (node_name n)
169
          (pp_comma_list ~pp_eol:pp_print_comma (pp_c_val m self pp_read))
170
          inputs (pp_comma_list pp_write) outputs
171

  
172
    let pp_basic_instance_call m self mem =
173
      pp_call m self mem (pp_c_var_read m) (pp_c_var_write m)
174

  
175
    let pp_arrow_call m self mem fmt i outputs =
176
      match outputs with
177
      | [ x ] ->
178
        fprintf fmt "%a = %a(%s->%s)%a;" (pp_c_var_read m) x
179
          pp_machine_step_name Arrow.arrow_id self i
180
          (Mod.pp_ghost_parameter mem)
181
          (Some i)
182
      | _ ->
183
        assert false
184

  
185
    let pp_instance_call m self mem fmt i inputs outputs =
186
      let pp_offset pp_var indices fmt var =
187
        fprintf fmt "%a%a" pp_var var
188
          (pp_print_list ~pp_sep:pp_print_nothing (fun fmt ->
189
               fprintf fmt "[%s]"))
190
          indices
191
      in
192
      let rec aux indices fmt typ =
193
        if Types.is_array_type typ then
194
          let dim = Types.array_type_dimension typ in
195
          let idx = mk_loop_var m () in
196
          fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}" idx
197
            idx idx pp_c_dimension dim idx
198
            (aux (idx :: indices))
199
            (Types.array_element_type typ)
200
        else
201
          let pp_read = pp_offset (pp_c_var_read m) indices in
202
          let pp_write = pp_offset (pp_c_var_write m) indices in
203
          pp_call m self mem pp_read pp_write fmt i inputs outputs
204
      in
205
      reset_loop_counter ();
206
      aux [] fmt (List.hd inputs).Machine_code_types.value_type
207

  
208
    let rec pp_conditional dependencies m self mem fmt c tl el =
209
      let pp_machine_instrs =
210
        pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
211
          (pp_machine_instr dependencies m self mem)
212
      in
213
      let pp_cond = pp_c_val m self (pp_c_var_read m) in
214
      match tl, el with
215
      | [], _ :: _ ->
216
        fprintf fmt "@[<v 2>if (!%a) {%a@]@,}" pp_cond c pp_machine_instrs el
217
      | _, [] ->
218
        fprintf fmt "@[<v 2>if (%a) {%a@]@,}" pp_cond c pp_machine_instrs tl
219
      | _, _ ->
220
        fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}" pp_cond c
221
          pp_machine_instrs tl pp_machine_instrs el
222

  
223
    and pp_machine_instr dependencies m self mem fmt instr =
224
      let pp_instr fmt instr =
225
        match get_instr_desc instr with
226
        | MNoReset _ ->
227
          ()
228
        | MSetReset inst ->
229
          pp_machine_set_reset m self mem fmt inst
230
        | MClearReset ->
231
          fprintf fmt "%t@,%a"
232
            (pp_machine_clear_reset m self mem)
233
            pp_label reset_label
234
        | MResetAssign b ->
235
          pp_reset_assign self fmt b
236
        | MLocalAssign (i, v) ->
237
          pp_assign m self (pp_c_var_read m) fmt (i, v)
238
        | MStateAssign (i, v) ->
239
          pp_assign m self (pp_c_var_read m) fmt (i, v)
240
        | MStep ([ i0 ], i, vl)
241
          when Basic_library.is_value_internal_fun
242
                 (mk_val (Fun (i, vl)) i0.var_type) ->
243
          pp_machine_instr dependencies m self mem fmt
244
            (update_instr_desc instr
245
               (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
246
        | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
247
          pp_instance_call m self mem fmt i vl il
248
        | MStep ([ i0 ], i, vl) when has_c_prototype i dependencies ->
249
          fprintf fmt "%a = %s%a;"
250
            (pp_c_val m self (pp_c_var_read m))
251
            (mk_val (Var i0) i0.var_type)
252
            i
253
            (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m)))
254
            vl
255
        | MStep (il, i, vl) ->
256
          let td, _ = List.assoc i m.minstances in
257
          if Arrow.td_is_arrow td then pp_arrow_call m self mem fmt i il
258
          else pp_basic_instance_call m self mem fmt i vl il
259
        | MBranch (_, []) ->
260
          eprintf "internal error: C_backend_src.pp_machine_instr %a@."
261
            (pp_instr m) instr;
262
          assert false
263
        | MBranch (g, hl) ->
264
          if
265
            let t = fst (List.hd hl) in
266
            t = tag_true || t = tag_false
267
          then
268
            (* boolean case, needs special treatment in C because truth value is
269
               not unique *)
270
            (* may disappear if we optimize code by replacing last branch test
271
               with default *)
272
            let tl = try List.assoc tag_true hl with Not_found -> [] in
273
            let el = try List.assoc tag_false hl with Not_found -> [] in
274
            let no_noreset =
275
              List.filter (fun i ->
276
                  match i.instr_desc with MNoReset _ -> false | _ -> true)
277
            in
278
            pp_conditional dependencies m self mem fmt g (no_noreset tl)
279
              (no_noreset el)
280
          else
281
            (* enum type case *)
282
            (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst
283
              (List.hd hl))) in*)
284
            fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
285
              (pp_c_val m self (pp_c_var_read m))
286
              g
287
              (pp_print_list ~pp_open_box:pp_open_vbox0
288
                 (pp_machine_branch dependencies m self mem))
289
              hl
290
        | MSpec s ->
291
          fprintf fmt "@[/*@@ %s */@]@ " s
292
        | MComment s ->
293
          fprintf fmt "/*%s*/@ " s
294
      in
295
      fprintf fmt "%a%a" pp_instr instr
296
        (Mod.pp_step_instr_spec m self mem)
297
        instr
298

  
299
    and pp_machine_branch dependencies m self mem fmt (t, h) =
300
      fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" pp_c_tag t
301
        (pp_print_list ~pp_open_box:pp_open_vbox0
302
           (pp_machine_instr dependencies m self mem))
303
        h
304

  
305
    (* let pp_machine_nospec_instr dependencies m self fmt instr =
306
     *   pp_machine_instr dependencies m self fmt instr
307
     *
308
     * let pp_machine_step_instr dependencies m self mem fmt instr =
309
     *   fprintf fmt "%a%a"
310
     *     (pp_machine_instr dependencies m self) instr
311
     *     (Mod.pp_step_instr_spec m self mem) instr *)
312

  
313
    (********************************************************************************************)
314
    (* C file Printing functions *)
315
    (********************************************************************************************)
316

  
317
    let print_const_def fmt tdecl =
318
      let cdecl = const_of_top tdecl in
319
      if
320
        !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
166 321
      then
167
        let dim = Types.array_type_dimension typ in
168
        let idx = mk_loop_var m () in
169
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
170
          idx idx idx pp_c_dimension dim idx
171
          (aux (idx::indices)) (Types.array_element_type typ)
322
        fprintf fmt "%a;" (pp_c_type cdecl.const_id)
323
          (Types.dynamic_type cdecl.const_type)
172 324
      else
173
        let pp_read  = pp_offset (pp_c_var_read  m) indices in
174
        let pp_write = pp_offset (pp_c_var_write m) indices in
175
        pp_call m self mem pp_read pp_write fmt i inputs outputs
176
    in
177
    reset_loop_counter ();
178
    aux [] fmt (List.hd inputs).Machine_code_types.value_type
179

  
180
  let rec pp_conditional dependencies m self mem fmt c tl el =
181
    let pp_machine_instrs =
182
      pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
183
        (pp_machine_instr dependencies m self mem) in
184
    let pp_cond = pp_c_val m self (pp_c_var_read m) in
185
    match tl, el with
186
    | [], _ :: _ ->
187
      fprintf fmt "@[<v 2>if (!%a) {%a@]@,}"
188
        pp_cond c
189
        pp_machine_instrs el
190
    | _, [] ->
191
      fprintf fmt "@[<v 2>if (%a) {%a@]@,}"
192
        pp_cond c
193
        pp_machine_instrs tl
194
    | _, _ ->
195
      fprintf fmt "@[<v 2>if (%a) {%a@]@,@[<v 2>} else {%a@]@,}"
196
        pp_cond c
197
        pp_machine_instrs tl
198
        pp_machine_instrs el
199

  
200
  and pp_machine_instr dependencies m self mem fmt instr =
201
    let pp_instr fmt instr = match get_instr_desc instr with
202
      | MNoReset _ -> ()
203
      | MSetReset inst ->
204
        pp_machine_set_reset m self mem fmt inst
205
      | MClearReset ->
206
        fprintf fmt "%t@,%a"
207
          (pp_machine_clear_reset m self mem) pp_label reset_label
208
      | MResetAssign b ->
209
        pp_reset_assign self fmt b
210
      | MLocalAssign (i, v) ->
211
        pp_assign m self (pp_c_var_read m) fmt (i, v)
212
      | MStateAssign (i, v) ->
213
        pp_assign m self (pp_c_var_read m) fmt (i, v)
214
      | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type)  ->
215
        pp_machine_instr dependencies m self mem fmt
216
          (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type)))
217
      | MStep (il, i, vl) when !Options.mpfr && Mpfr.is_homomorphic_fun i ->
218
        pp_instance_call m self mem fmt i vl il
219
      | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
220
        fprintf fmt "%a = %s%a;"
221
          (pp_c_val m self (pp_c_var_read m)) (mk_val (Var i0) i0.var_type)
222
          i
223
          (pp_print_parenthesized (pp_c_val m self (pp_c_var_read m))) vl
224
      | MStep (il, i, vl) ->
225
        let td, _ = List.assoc i m.minstances in
226
        if Arrow.td_is_arrow td then
227
          pp_arrow_call m self mem fmt i il
228
        else
229
          pp_basic_instance_call m self mem fmt i vl il
230
      | MBranch (_, []) ->
231
        eprintf "internal error: C_backend_src.pp_machine_instr %a@."
232
          (pp_instr m) instr;
233
        assert false
234
      | MBranch (g, hl) ->
235
        if let t = fst (List.hd hl) in t = tag_true || t = tag_false
236
        then (* boolean case, needs special treatment in C because truth value is not unique *)
237
          (* may disappear if we optimize code by replacing last branch test with default *)
238
          let tl = try List.assoc tag_true  hl with Not_found -> [] in
239
          let el = try List.assoc tag_false hl with Not_found -> [] in
240
          let no_noreset = List.filter (fun i -> match i.instr_desc with
241
              | MNoReset _ -> false
242
              | _ -> true)
243
          in
244
          pp_conditional dependencies m self mem fmt g
245
            (no_noreset tl) (no_noreset el)
246
        else (* enum type case *)
247
          (*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*)
248
          fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
249
            (pp_c_val m self (pp_c_var_read m)) g
250
            (pp_print_list ~pp_open_box:pp_open_vbox0
251
               (pp_machine_branch dependencies m self mem)) hl
252
      | MSpec s ->
253
        fprintf fmt "@[/*@@ %s */@]@ " s
254
      | MComment s  ->
255
        fprintf fmt "/*%s*/@ " s
256
    in
257
    fprintf fmt "%a%a" pp_instr instr (Mod.pp_step_instr_spec m self mem) instr
258

  
259
  and pp_machine_branch dependencies m self mem fmt (t, h) =
260
    fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
261
      pp_c_tag t
262
      (pp_print_list ~pp_open_box:pp_open_vbox0
263
         (pp_machine_instr dependencies m self mem)) h
264

  
265
  (* let pp_machine_nospec_instr dependencies m self fmt instr =
266
   *   pp_machine_instr dependencies m self fmt instr
267
   *
268
   * let pp_machine_step_instr dependencies m self mem fmt instr =
269
   *   fprintf fmt "%a%a"
270
   *     (pp_machine_instr dependencies m self) instr
271
   *     (Mod.pp_step_instr_spec m self mem) instr *)
272

  
273
  (********************************************************************************************)
274
  (*                         C file Printing functions                                        *)
275
  (********************************************************************************************)
276

  
277
  let print_const_def fmt tdecl =
278
    let cdecl = const_of_top tdecl in
279
    if !Options.mpfr && Types.(is_real_type (array_base_type cdecl.const_type))
280
    then
281
      fprintf fmt "%a;"
282
        (pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type)
283
    else
284
      fprintf fmt "%a = %a;"
285
        (pp_c_type cdecl.const_id) cdecl.const_type
286
        pp_c_const cdecl.const_value
287

  
288
  let print_alloc_instance fmt (i, (m, static)) =
289
    fprintf fmt "_alloc->%s = %a %a;"
290
      i
291
      pp_machine_alloc_name (node_name m)
292
      (pp_print_parenthesized Dimension.pp_dimension) static
293

  
294
  let print_dealloc_instance fmt (i, (m, _)) =
295
    fprintf fmt "%a (_alloc->%s);"
296
      pp_machine_dealloc_name (node_name m)
297
      i
298

  
299
  let const_locals m =
300
    List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals
301

  
302
  let pp_c_decl_array_mem self fmt id =
303
    fprintf fmt "%a = (%a) (%s->_reg.%s)"
304
      (pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type
305
      (pp_c_type "(*)") id.var_type
306
      self
307
      id.var_id
308

  
309
  let print_alloc_const fmt m =
310
    pp_print_list
311
      ~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";")
312
      (pp_c_decl_local_var m) fmt (const_locals m)
313

  
314
  let print_alloc_array fmt vdecl =
315
    let base_type = Types.array_base_type vdecl.var_type in
316
    let size_types = Types.array_type_multi_dimension vdecl.var_type in
317
    let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in
318
    fprintf fmt
319
      "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,\
320
       assert(_alloc->%s);"
321
      vdecl.var_id
322
      (pp_c_type "") base_type
323
      Dimension.pp_dimension size_type
324
      (pp_c_type "") base_type
325
      vdecl.var_id
326

  
327
  let print_dealloc_array fmt vdecl =
328
    fprintf fmt "free (_alloc->_reg.%s);"
329
      vdecl.var_id
330

  
331
  let array_mems m =
332
    List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
333

  
334
  let print_alloc_code fmt m =
335
    fprintf fmt
336
      "%a *_alloc;@,\
337
       _alloc = (%a *) malloc(sizeof(%a));@,\
338
       assert(_alloc);@,\
339
       %a%areturn _alloc;"
340
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
341
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
342
      (pp_machine_memtype_name ~ghost:false) m.mname.node_id
343
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m)
344
      (pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances
345

  
346
  let print_dealloc_code fmt m =
347
    fprintf fmt
348
      "%a%afree (_alloc);@,\
349
       return;"
350
      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array) (array_mems m)
351
      (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance) m.minstances
352

  
353
  (* let print_stateless_init_code fmt m self =
354
   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
355
   *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
356
   *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
357
   *     (print_init_prototype self) (m.mname.node_id, m.mstatic)
358
   *     (\* array mems *\)
359
   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
360
   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
361
   *     (\* memory initialization *\)
362
   *     (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
363
   *     (Utils.pp_newline_if_non_empty m.mmemory)
364
   *     (\* sub-machines initialization *\)
365
   *     (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
366
   *     (Utils.pp_newline_if_non_empty m.minit)
367
   *
368
   * let print_stateless_clear_code fmt m self =
369
   *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
370
   *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
371
   *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
372
   *     (print_clear_prototype self) (m.mname.node_id, m.mstatic)
373
   *     (\* array mems *\)
374
   *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
375
   *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
376
   *     (\* memory clear *\)
377
   *     (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
378
   *     (Utils.pp_newline_if_non_empty m.mmemory)
379
   *     (\* sub-machines clear*\)
380
   *     (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
381
   *     (Utils.pp_newline_if_non_empty m.minit) *)
382

  
383
  let pp_c_check m self fmt (loc, check) =
384
    fprintf fmt "@[<v>%a@,assert (%a);@]"
385
      Location.pp_c_loc loc
386
      (pp_c_val m self (pp_c_var_read m)) check
387

  
388
  let pp_print_function
389
      ~pp_prototype ~prototype
390
      ?(pp_spec=pp_print_nothing)
391
      ?(pp_local=pp_print_nothing) ?(base_locals=[])
392
      ?(pp_array_mem=pp_print_nothing) ?(array_mems=[])
393
      ?(pp_init_mpfr_local=pp_print_nothing)
394
      ?(pp_clear_mpfr_local=pp_print_nothing)
395
      ?(mpfr_locals=[])
396
      ?(pp_check=pp_print_nothing) ?(checks=[])
397
      ?(pp_extra=pp_print_nothing)
398
      ?(pp_instr=fun fmt _ -> pp_print_nothing fmt ()) ?(instrs=[])
399
      fmt =
400
    fprintf fmt
401
      "%a@[<v 2>%a {@,\
402
       %a%a\
403
       %a%a%a%a%areturn;@]@,\
404
       }"
405
      pp_spec ()
406
      pp_prototype prototype
407
      (* locals *)
408
      (pp_print_list
409
         ~pp_open_box:pp_open_vbox0
410
         ~pp_sep:pp_print_semicolon
411
         ~pp_eol:pp_print_semicolon
412
         pp_local)
413
      base_locals
414
      (* array mems *)
415
      (pp_print_list
416
         ~pp_open_box:pp_open_vbox0
417
         ~pp_sep:pp_print_semicolon
418
         ~pp_eol:pp_print_semicolon
419
         pp_array_mem)
420
      array_mems
421
      (* locals initialization *)
422
      (pp_print_list
423
         ~pp_epilogue:pp_print_cut
424
         pp_init_mpfr_local) (mpfr_vars mpfr_locals)
425
      (* check assertions *)
426
      (pp_print_list pp_check) checks
427
      (* instrs *)
428
      (pp_print_list
429
         ~pp_open_box:pp_open_vbox0
430
         ~pp_epilogue:pp_print_cut
431
         pp_instr) instrs
432
      (* locals clear *)
433
      (pp_print_list
434
         ~pp_epilogue:pp_print_cut
435
         pp_clear_mpfr_local) (mpfr_vars mpfr_locals)
436
      (* extra *)
437
      pp_extra ()
438

  
439
  let node_of_machine m = {
440
    top_decl_desc = Node m.mname;
441
    top_decl_loc = Location.dummy_loc;
442
    top_decl_owner = "";
443
    top_decl_itf = false
444
  }
445

  
446
  let print_stateless_code machines dependencies fmt m =
447
    let self = "__ERROR__" in
448
    if not (!Options.ansi && is_generic_node (node_of_machine m))
449
    then
450
      (* C99 code *)
325
        fprintf fmt "%a = %a;" (pp_c_type cdecl.const_id) cdecl.const_type
326
          pp_c_const cdecl.const_value
327

  
328
    let print_alloc_instance fmt (i, (m, static)) =
329
      fprintf fmt "_alloc->%s = %a %a;" i pp_machine_alloc_name (node_name m)
330
        (pp_print_parenthesized Dimension.pp_dimension)
331
        static
332

  
333
    let print_dealloc_instance fmt (i, (m, _)) =
334
      fprintf fmt "%a (_alloc->%s);" pp_machine_dealloc_name (node_name m) i
335

  
336
    let const_locals m =
337
      List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals
338

  
339
    let pp_c_decl_array_mem self fmt id =
340
      fprintf fmt "%a = (%a) (%s->_reg.%s)"
341
        (pp_c_type (sprintf "(*%s)" id.var_id))
342
        id.var_type (pp_c_type "(*)") id.var_type self id.var_id
343

  
344
    let print_alloc_const fmt m =
345
      pp_print_list ~pp_sep:(pp_print_endcut ";") ~pp_eol:(pp_print_endcut ";")
346
        (pp_c_decl_local_var m) fmt (const_locals m)
347

  
348
    let print_alloc_array fmt vdecl =
349
      let base_type = Types.array_base_type vdecl.var_type in
350
      let size_types = Types.array_type_multi_dimension vdecl.var_type in
351
      let size_type =
352
        Dimension.multi_dimension_product vdecl.var_loc size_types
353
      in
354
      fprintf fmt
355
        "_alloc->_reg.%s = (%a*) malloc((%a)*sizeof(%a));@,assert(_alloc->%s);"
356
        vdecl.var_id (pp_c_type "") base_type Dimension.pp_dimension size_type
357
        (pp_c_type "") base_type vdecl.var_id
358

  
359
    let print_dealloc_array fmt vdecl =
360
      fprintf fmt "free (_alloc->_reg.%s);" vdecl.var_id
361

  
362
    let array_mems m =
363
      List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory
364

  
365
    let print_alloc_code fmt m =
366
      fprintf fmt
367
        "%a *_alloc;@,\
368
         _alloc = (%a *) malloc(sizeof(%a));@,\
369
         assert(_alloc);@,\
370
         %a%areturn _alloc;"
371
        (pp_machine_memtype_name ~ghost:false)
372
        m.mname.node_id
373
        (pp_machine_memtype_name ~ghost:false)
374
        m.mname.node_id
375
        (pp_machine_memtype_name ~ghost:false)
376
        m.mname.node_id
377
        (pp_print_list ~pp_sep:pp_print_nothing print_alloc_array)
378
        (array_mems m)
379
        (pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance)
380
        m.minstances
381

  
382
    let print_dealloc_code fmt m =
383
      fprintf fmt "%a%afree (_alloc);@,return;"
384
        (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_array)
385
        (array_mems m)
386
        (pp_print_list ~pp_sep:pp_print_nothing print_dealloc_instance)
387
        m.minstances
388

  
389
    (* let print_stateless_init_code fmt m self =
390
     *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
391
     *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
392
     *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
393
     *     (print_init_prototype self) (m.mname.node_id, m.mstatic)
394
     *     (\* array mems *\)
395
     *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
396
     *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
397
     *     (\* memory initialization *\)
398
     *     (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
399
     *     (Utils.pp_newline_if_non_empty m.mmemory)
400
     *     (\* sub-machines initialization *\)
401
     *     (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
402
     *     (Utils.pp_newline_if_non_empty m.minit)
403
     *
404
     * let print_stateless_clear_code fmt m self =
405
     *   let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
406
     *   let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
407
     *   fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
408
     *     (print_clear_prototype self) (m.mname.node_id, m.mstatic)
409
     *     (\* array mems *\)
410
     *     (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
411
     *     (Utils.pp_final_char_if_non_empty ";@," array_mems)
412
     *     (\* memory clear *\)
413
     *     (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
414
     *     (Utils.pp_newline_if_non_empty m.mmemory)
415
     *     (\* sub-machines clear*\)
416
     *     (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
417
     *     (Utils.pp_newline_if_non_empty m.minit) *)
418

  
419
    let pp_c_check m self fmt (loc, check) =
420
      fprintf fmt "@[<v>%a@,assert (%a);@]" Location.pp_c_loc loc
421
        (pp_c_val m self (pp_c_var_read m))
422
        check
423

  
424
    let pp_print_function ~pp_prototype ~prototype ?(pp_spec = pp_print_nothing)
425
        ?(pp_local = pp_print_nothing) ?(base_locals = [])
426
        ?(pp_array_mem = pp_print_nothing) ?(array_mems = [])
427
        ?(pp_init_mpfr_local = pp_print_nothing)
428
        ?(pp_clear_mpfr_local = pp_print_nothing) ?(mpfr_locals = [])
429
        ?(pp_check = pp_print_nothing) ?(checks = [])
430
        ?(pp_extra = pp_print_nothing)
431
        ?(pp_instr = fun fmt _ -> pp_print_nothing fmt ()) ?(instrs = []) fmt =
432
      fprintf fmt "%a@[<v 2>%a {@,%a%a%a%a%a%a%areturn;@]@,}" pp_spec ()
433
        pp_prototype prototype
434
        (* locals *)
435
        (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon
436
           ~pp_eol:pp_print_semicolon pp_local)
437
        base_locals
438
        (* array mems *)
439
        (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_semicolon
440
           ~pp_eol:pp_print_semicolon pp_array_mem)
441
        array_mems
442
        (* locals initialization *)
443
        (pp_print_list ~pp_epilogue:pp_print_cut pp_init_mpfr_local)
444
        (mpfr_vars mpfr_locals)
445
        (* check assertions *)
446
        (pp_print_list pp_check)
447
        checks
448
        (* instrs *)
449
        (pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_epilogue:pp_print_cut
450
           pp_instr)
451
        instrs
452
        (* locals clear *)
453
        (pp_print_list ~pp_epilogue:pp_print_cut pp_clear_mpfr_local)
454
        (mpfr_vars mpfr_locals) (* extra *)
455
        pp_extra ()
456

  
457
    let node_of_machine m =
458
      {
459
        top_decl_desc = Node m.mname;
460
        top_decl_loc = Location.dummy_loc;
461
        top_decl_owner = "";
462
        top_decl_itf = false;
463
      }
464

  
465
    let print_stateless_code machines dependencies fmt m =
466
      let self = "__ERROR__" in
467
      if not (!Options.ansi && is_generic_node (node_of_machine m)) then
468
        (* C99 code *)
469
        pp_print_function
470
          ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self self m)
471
          ~pp_prototype:Protos.print_stateless_prototype
472
          ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
473
          ~pp_local:(pp_c_decl_local_var m) ~base_locals:m.mstep.step_locals
474
          ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
475
          ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
476
          ~mpfr_locals:m.mstep.step_locals ~pp_check:(pp_c_check m self)
477
          ~checks:m.mstep.step_checks
478
          ~pp_instr:(pp_machine_instr dependencies m self self)
479
          ~instrs:m.mstep.step_instrs fmt
480
      else
481
        (* C90 code *)
482
        let gen_locals, base_locals =
483
          List.partition
484
            (fun v -> Types.is_generic_type v.var_type)
485
            m.mstep.step_locals
486
        in
487
        let gen_calls =
488
          List.map
489
            (fun e ->
490
              let id, _, _ = call_of_expr e in
491
              mk_call_var_decl e.expr_loc id)
492
            m.mname.node_gencalls
493
        in
494
        pp_print_function ~pp_prototype:Protos.print_stateless_prototype
495
          ~prototype:
496
            ( m.mname.node_id,
497
              m.mstep.step_inputs @ gen_locals @ gen_calls,
498
              m.mstep.step_outputs )
499
          ~pp_local:(pp_c_decl_local_var m) ~base_locals
500
          ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
501
          ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
502
          ~mpfr_locals:m.mstep.step_locals ~pp_check:(pp_c_check m self)
503
          ~checks:m.mstep.step_checks
504
          ~pp_instr:(pp_machine_instr dependencies m self self)
505
          ~instrs:m.mstep.step_instrs fmt
506

  
507
    let print_clear_reset_code dependencies self mem fmt m =
451 508
      pp_print_function
452
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self self m)
453
        ~pp_prototype:Protos.print_stateless_prototype
454
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
455
        ~pp_local:(pp_c_decl_local_var m)
456
        ~base_locals:m.mstep.step_locals
457
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
458
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
459
        ~mpfr_locals:m.mstep.step_locals
460
        ~pp_check:(pp_c_check m self)
461
        ~checks:m.mstep.step_checks
462
        ~pp_instr:(pp_machine_instr dependencies m self self)
463
        ~instrs:m.mstep.step_instrs
509
        ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt self mem m)
510
        ~pp_prototype:(Protos.print_clear_reset_prototype self mem)
511
        ~prototype:(m.mname.node_id, m.mstatic)
512
        ~pp_local:(pp_c_decl_local_var m) ~base_locals:(const_locals m)
513
        ~pp_instr:(pp_machine_instr dependencies m self mem)
514
        ~instrs:
515
          [
516
            mk_branch
517
              (mk_val ResetFlag Type_predef.type_bool)
518
              [ "true", mkinstr (MResetAssign false) :: m.minit ];
519
          ]
464 520
        fmt
465
    else
466
      (* C90 code *)
467
      let gen_locals, base_locals = List.partition (fun v ->
468
          Types.is_generic_type v.var_type) m.mstep.step_locals in
469
      let gen_calls = List.map (fun e ->
470
          let (id, _, _) = call_of_expr e
471
          in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
521

  
522
    let print_set_reset_code dependencies self mem fmt m =
472 523
      pp_print_function
473
        ~pp_prototype:Protos.print_stateless_prototype
474
        ~prototype:(m.mname.node_id,
475
                    m.mstep.step_inputs @ gen_locals @ gen_calls,
476
                    m.mstep.step_outputs)
477
        ~pp_local:(pp_c_decl_local_var m)
478
        ~base_locals
479
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
480
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
481
        ~mpfr_locals:m.mstep.step_locals
482
        ~pp_check:(pp_c_check m self)
483
        ~checks:m.mstep.step_checks
484
        ~pp_instr:(pp_machine_instr dependencies m self self)
485
        ~instrs:m.mstep.step_instrs
524
        ~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m)
525
        ~pp_prototype:(Protos.print_set_reset_prototype self mem)
526
        ~prototype:(m.mname.node_id, m.mstatic)
527
        ~pp_instr:(pp_machine_instr dependencies m self mem)
528
        ~instrs:[ mkinstr (MResetAssign true) ]
486 529
        fmt
487 530

  
488
  let print_clear_reset_code dependencies self mem fmt m =
489
    pp_print_function
490
      ~pp_spec:(fun fmt () -> Mod.pp_clear_reset_spec fmt self mem m)
491
      ~pp_prototype:(Protos.print_clear_reset_prototype self mem)
492
      ~prototype:(m.mname.node_id, m.mstatic)
493
      ~pp_local:(pp_c_decl_local_var m)
494
      ~base_locals:(const_locals m)
495
      ~pp_instr:(pp_machine_instr dependencies m self mem)
496
      ~instrs:[mk_branch
497
                 (mk_val ResetFlag Type_predef.type_bool)
498
                 ["true", mkinstr (MResetAssign false) :: m.minit]]
499
      fmt
500

  
501
  let print_set_reset_code dependencies self mem fmt m =
502
    pp_print_function
503
      ~pp_spec:(fun fmt () -> Mod.pp_set_reset_spec fmt self mem m)
504
      ~pp_prototype:(Protos.print_set_reset_prototype self mem)
505
      ~prototype:(m.mname.node_id, m.mstatic)
506
      ~pp_instr:(pp_machine_instr dependencies m self mem)
507
      ~instrs:[mkinstr (MResetAssign true)]
508
      fmt
509

  
510
  let print_init_code self fmt m =
511
    let minit = List.map (fun i ->
512
        match get_instr_desc i with
513
        | MSetReset i -> i
514
        | _ -> assert false)
515
        m.minit in
516
    pp_print_function
517
      ~pp_prototype:(Protos.print_init_prototype self)
518
      ~prototype:(m.mname.node_id, m.mstatic)
519
      ~pp_array_mem:(pp_c_decl_array_mem self)
520
      ~array_mems:(array_mems m)
521
      ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
522
      ~mpfr_locals:m.mmemory
523
      ~pp_extra:(fun fmt () ->
524
          pp_print_list
525
            ~pp_open_box:pp_open_vbox0
526
            ~pp_epilogue:pp_print_cut
527
            (pp_machine_init m self self)
528
            fmt minit)
529
      fmt
530

  
531
  let print_clear_code self fmt m =
532
    let minit = List.map (fun i ->
533
        match get_instr_desc i with
534
        | MSetReset i -> i
535
        | _ -> assert false) m.minit in
536
    pp_print_function
537
      ~pp_prototype:(Protos.print_clear_prototype self)
538
      ~prototype:(m.mname.node_id, m.mstatic)
539
      ~pp_array_mem:(pp_c_decl_array_mem self)
540
      ~array_mems:(array_mems m)
541
      ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
542
      ~mpfr_locals:m.mmemory
543
      ~pp_extra:(fun fmt () ->
544
          pp_print_list
545
            ~pp_open_box:pp_open_vbox0
546
            ~pp_epilogue:pp_print_cut
547
            (pp_machine_clear m self self)
548
            fmt minit)
549
      fmt
550

  
551
  let print_step_code machines dependencies self mem fmt m =
552
    if not (!Options.ansi && is_generic_node (node_of_machine m))
553
    then
554
      (* C99 code *)
531
    let print_init_code self fmt m =
532
      let minit =
533
        List.map
534
          (fun i ->
535
            match get_instr_desc i with MSetReset i -> i | _ -> assert false)
536
          m.minit
537
      in
555 538
      pp_print_function
556
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
557
        ~pp_prototype:(Protos.print_step_prototype self mem)
558
        ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
559
        ~pp_local:(pp_c_decl_local_var m)
560
        ~base_locals:m.mstep.step_locals
561
        ~pp_array_mem:(pp_c_decl_array_mem self)
562
        ~array_mems:(array_mems m)
539
        ~pp_prototype:(Protos.print_init_prototype self)
540
        ~prototype:(m.mname.node_id, m.mstatic)
541
        ~pp_array_mem:(pp_c_decl_array_mem self) ~array_mems:(array_mems m)
563 542
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
564
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
565
        ~mpfr_locals:m.mstep.step_locals
566
        ~pp_check:(pp_c_check m self)
567
        ~checks:m.mstep.step_checks
568
        ~pp_instr:(pp_machine_instr dependencies m self mem)
569
        ~instrs:m.mstep.step_instrs
543
        ~mpfr_locals:m.mmemory
544
        ~pp_extra:(fun fmt () ->
545
          pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_epilogue:pp_print_cut
546
            (pp_machine_init m self self)
547
            fmt minit)
570 548
        fmt
571
    else
572
      (* C90 code *)
573
      let gen_locals, base_locals = List.partition (fun v ->
574
          Types.is_generic_type v.var_type) m.mstep.step_locals in
575
      let gen_calls = List.map (fun e ->
576
          let id, _, _ = call_of_expr e in
577
          mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
549

  
550
    let print_clear_code self fmt m =
551
      let minit =
552
        List.map
553
          (fun i ->
554
            match get_instr_desc i with MSetReset i -> i | _ -> assert false)
555
          m.minit
556
      in
578 557
      pp_print_function
579
        ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
580
        ~pp_prototype:(Protos.print_step_prototype self mem)
581
        ~prototype:(m.mname.node_id,
582
                    m.mstep.step_inputs @ gen_locals @ gen_calls,
583
                    m.mstep.step_outputs)
584
        ~pp_local:(pp_c_decl_local_var m)
585
        ~base_locals
586
        ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
558
        ~pp_prototype:(Protos.print_clear_prototype self)
559
        ~prototype:(m.mname.node_id, m.mstatic)
560
        ~pp_array_mem:(pp_c_decl_array_mem self) ~array_mems:(array_mems m)
587 561
        ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
588
        ~mpfr_locals:m.mstep.step_locals
589
        ~pp_check:(pp_c_check m self)
590
        ~checks:m.mstep.step_checks
591
        ~pp_instr:(pp_machine_instr dependencies m self mem)
592
        ~instrs:m.mstep.step_instrs
562
        ~mpfr_locals:m.mmemory
563
        ~pp_extra:(fun fmt () ->
564
          pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_epilogue:pp_print_cut
565
            (pp_machine_clear m self self)
566
            fmt minit)
593 567
        fmt
594 568

  
595
  (********************************************************************************************)
596
  (*                     MAIN C file Printing functions                                       *)
597
  (********************************************************************************************)
598

  
599
  let pp_const_initialize m pp_var fmt const =
600
    let var = Machine_code_common.mk_val
601
        (Var (Corelang.var_decl_of_const const)) const.const_type in
602
    let rec aux indices value fmt typ =
603
      if Types.is_array_type typ
604
      then
605
        let dim = Types.array_type_dimension typ in
606
        let szl = Utils.enumerate (Dimension.size_const_dimension dim) in
607
        let typ' = Types.array_element_type typ in
608
        let value = match value with
609
          | Const_array ca -> List.nth ca
610
          | _ -> assert false in
611
        pp_print_list
612
          (fun fmt i -> aux (string_of_int i :: indices) (value i) fmt typ') fmt szl
569
    let print_step_code machines dependencies self mem fmt m =
570
      if not (!Options.ansi && is_generic_node (node_of_machine m)) then
571
        (* C99 code *)
572
        pp_print_function
573
          ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
574
          ~pp_prototype:(Protos.print_step_prototype self mem)
575
          ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
576
          ~pp_local:(pp_c_decl_local_var m) ~base_locals:m.mstep.step_locals
577
          ~pp_array_mem:(pp_c_decl_array_mem self) ~array_mems:(array_mems m)
578
          ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
579
          ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
580
          ~mpfr_locals:m.mstep.step_locals ~pp_check:(pp_c_check m self)
581
          ~checks:m.mstep.step_checks
582
          ~pp_instr:(pp_machine_instr dependencies m self mem)
583
          ~instrs:m.mstep.step_instrs fmt
613 584
      else
614
        let indices = List.rev indices in
615
        let pp_var_suffix fmt var =
616
          fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix indices in
617
        fprintf fmt "%a@,%a"
618
          (Mpfr.pp_inject_init pp_var_suffix) var
619
          (Mpfr.pp_inject_real pp_var_suffix pp_c_const) (var, value)
620
    in
621
    reset_loop_counter ();
622
    aux [] const.const_value fmt const.const_type
623

  
624
  let pp_const_clear pp_var fmt const =
625
    let m = Machine_code_common.empty_machine in
626
    let var = Corelang.var_decl_of_const const in
627
    let rec aux indices fmt typ =
628
      if Types.is_array_type typ
629
      then
630
        let dim = Types.array_type_dimension typ in
631
        let idx = mk_loop_var m () in
632
        fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
633
          idx idx idx pp_c_dimension dim idx
634
          (aux (idx::indices)) (Types.array_element_type typ)
635
      else
636
        let indices = List.rev indices in
637
        let pp_var_suffix fmt var =
638
          fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix indices in
639
        Mpfr.pp_inject_clear pp_var_suffix fmt var
640
    in
641
    reset_loop_counter ();
642
    aux [] fmt var.var_type
643

  
644
  let print_import_init fmt dep =
645
    let baseNAME = file_to_module_name dep.name in
646
    fprintf fmt "%a();" pp_global_init_name baseNAME
647

  
648
  let print_import_clear fmt dep =
649
    let baseNAME = file_to_module_name dep.name in
650
    fprintf fmt "%a();" pp_global_clear_name baseNAME
651

  
652
  let print_global_init_code fmt (basename, prog, dependencies) =
653
    let baseNAME = file_to_module_name basename in
654
    let constants = List.map const_of_top (get_consts prog) in
655
    fprintf fmt
656
      "@[<v 2>%a {@,\
657
       static %s init = 0;@,\
658
       @[<v 2>if (!init) { @,\
659
       init = 1;%a%a@]@,\
660
       }@,\
661
       return;@]@,\
662
       }"
663
      print_global_init_prototype baseNAME
664
      (pp_c_basic_type_desc Type_predef.type_bool)
665
      (* constants *)
666
      (pp_print_list
667
         ~pp_prologue:pp_print_cut
668
         (pp_const_initialize empty_machine (pp_c_var_read empty_machine)))
669
      (mpfr_consts constants)
670
      (* dependencies initialization *)
671
      (pp_print_list
672
         ~pp_prologue:pp_print_cut
673
         print_import_init) (List.filter (fun dep -> dep.local) dependencies)
674

  
675
  let print_global_clear_code fmt (basename, prog, dependencies) =
676
    let baseNAME = file_to_module_name basename in
677
    let constants = List.map const_of_top (get_consts prog) in
678
    fprintf fmt
679
      "@[<v 2>%a {@,\
680
       static %s clear = 0;@,\
681
       @[<v 2>if (!clear) { @,\
682
       clear = 1;%a%a@]@,\
683
       }@,\
684
       return;@]@,\
685
       }"
686
      print_global_clear_prototype baseNAME
687
      (pp_c_basic_type_desc Type_predef.type_bool)
688
      (* constants *)
689
      (pp_print_list
690
         ~pp_prologue:pp_print_cut
691
         (pp_const_clear (pp_c_var_read empty_machine))) (mpfr_consts constants)
692
      (* dependencies initialization *)
693
      (pp_print_list
694
         ~pp_prologue:pp_print_cut
695
         print_import_clear) (List.filter (fun dep -> dep.local) dependencies)
696

  
697
  let print_alloc_function fmt m =
698
    if (not !Options.static_mem) then
699
      (* Alloc functions, only if non static mode *)
585
        (* C90 code *)
586
        let gen_locals, base_locals =
587
          List.partition
588
            (fun v -> Types.is_generic_type v.var_type)
589
            m.mstep.step_locals
590
        in
591
        let gen_calls =
592
          List.map
593
            (fun e ->
594
              let id, _, _ = call_of_expr e in
595
              mk_call_var_decl e.expr_loc id)
596
            m.mname.node_gencalls
597
        in
598
        pp_print_function
599
          ~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt machines self mem m)
600
          ~pp_prototype:(Protos.print_step_prototype self mem)
601
          ~prototype:
602
            ( m.mname.node_id,
603
              m.mstep.step_inputs @ gen_locals @ gen_calls,
604
              m.mstep.step_outputs )
605
          ~pp_local:(pp_c_decl_local_var m) ~base_locals
606
          ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
607
          ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
608
          ~mpfr_locals:m.mstep.step_locals ~pp_check:(pp_c_check m self)
609
          ~checks:m.mstep.step_checks
610
          ~pp_instr:(pp_machine_instr dependencies m self mem)
611
          ~instrs:m.mstep.step_instrs fmt
612

  
613
    (********************************************************************************************)
614
    (* MAIN C file Printing functions *)
615
    (********************************************************************************************)
616

  
617
    let pp_const_initialize m pp_var fmt const =
618
      let var =
619
        Machine_code_common.mk_val
620
          (Var (Corelang.var_decl_of_const const))
621
          const.const_type
622
      in
623
      let rec aux indices value fmt typ =
624
        if Types.is_array_type typ then
625
          let dim = Types.array_type_dimension typ in
626
          let szl = Utils.enumerate (Dimension.size_const_dimension dim) in
627
          let typ' = Types.array_element_type typ in
628
          let value =
629
            match value with Const_array ca -> List.nth ca | _ -> assert false
630
          in
631
          pp_print_list
632
            (fun fmt i -> aux (string_of_int i :: indices) (value i) fmt typ')
633
            fmt szl
634
        else
635
          let indices = List.rev indices in
636
          let pp_var_suffix fmt var =
637
            fprintf fmt "%a%a" (pp_c_val m "" pp_var) var pp_array_suffix
638
              indices
639
          in
640
          fprintf fmt "%a@,%a"
641
            (Mpfr.pp_inject_init pp_var_suffix)
642
            var
643
            (Mpfr.pp_inject_real pp_var_suffix pp_c_const)
644
            (var, value)
645
      in
646
      reset_loop_counter ();
647
      aux [] const.const_value fmt const.const_type
648

  
649
    let pp_const_clear pp_var fmt const =
650
      let m = Machine_code_common.empty_machine in
651
      let var = Corelang.var_decl_of_const const in
652
      let rec aux indices fmt typ =
653
        if Types.is_array_type typ then
654
          let dim = Types.array_type_dimension typ in
655
          let idx = mk_loop_var m () in
656
          fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}" idx
657
            idx idx pp_c_dimension dim idx
658
            (aux (idx :: indices))
659
            (Types.array_element_type typ)
660
        else
661
          let indices = List.rev indices in
662
          let pp_var_suffix fmt var =
663
            fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix
664
              indices
665
          in
666
          Mpfr.pp_inject_clear pp_var_suffix fmt var
667
      in
668
      reset_loop_counter ();
669
      aux [] fmt var.var_type
670

  
671
    let print_import_init fmt dep =
672
      let baseNAME = file_to_module_name dep.name in
673
      fprintf fmt "%a();" pp_global_init_name baseNAME
674

  
675
    let print_import_clear fmt dep =
676
      let baseNAME = file_to_module_name dep.name in
677
      fprintf fmt "%a();" pp_global_clear_name baseNAME
678

  
679
    let print_global_init_code fmt (basename, prog, dependencies) =
680
      let baseNAME = file_to_module_name basename in
681
      let constants = List.map const_of_top (get_consts prog) in
700 682
      fprintf fmt
701 683
        "@[<v 2>%a {@,\
702
         %a%a@]@,\
684
         static %s init = 0;@,\
685
         @[<v 2>if (!init) { @,\
686
         init = 1;%a%a@]@,\
703 687
         }@,\
704
         @[<v 2>%a {@,\
705
         %a%a@]@,\
706
         @,"
707
        print_alloc_prototype (m.mname.node_id, m.mstatic)
708
        print_alloc_const m
709
        print_alloc_code m
710
        print_dealloc_prototype m.mname.node_id
711
        print_alloc_const m
712
        print_dealloc_code m
713

  
714
  let print_mpfr_code self fmt m =
715
    if !Options.mpfr then
716
      fprintf fmt "@,@[<v>%a@,%a@]"
717
        (* Init function *)
718
        (print_init_code self) m
719
        (* Clear function *)
720
        (print_clear_code self) m
721

  
722
  (* TODO: ACSL
723
     - a contract machine shall not be directly printed in the C source
724
     - but a regular machine associated to a contract machine shall integrate
725
       the associated statements, updating its memories, at the end of the
726
       function body.
727
     - last one may print intermediate comment/acsl if/when they are present in
728
       the sequence of instruction
729
  *)
730
  let print_machine machines dependencies fmt m =
731
    if fst (get_stateless_status m) then
732
      (* Step function *)
733
      print_stateless_code machines dependencies fmt m
734
    else
735
      let self = mk_self m in
736
      let mem = mk_mem m in
737
      fprintf fmt "@[<v>%a%a@,@,%a@,@,%a%a@]"
738
        print_alloc_function m
739
        (* Reset functions *)
740
        (print_clear_reset_code dependencies self mem) m
741
        (print_set_reset_code dependencies self mem) m
688
         return;@]@,\
689
         }"
690
        print_global_init_prototype baseNAME
691
        (pp_c_basic_type_desc Type_predef.type_bool)
692
        (* constants *)
693
        (pp_print_list ~pp_prologue:pp_print_cut
694
           (pp_const_initialize empty_machine (pp_c_var_read empty_machine)))
695
        (mpfr_consts constants)
696
        (* dependencies initialization *)
697
        (pp_print_list ~pp_prologue:pp_print_cut print_import_init)
698
        (List.filter (fun dep -> dep.local) dependencies)
699

  
700
    let print_global_clear_code fmt (basename, prog, dependencies) =
701
      let baseNAME = file_to_module_name basename in
702
      let constants = List.map const_of_top (get_consts prog) in
703
      fprintf fmt
704
        "@[<v 2>%a {@,\
705
         static %s clear = 0;@,\
706
         @[<v 2>if (!clear) { @,\
707
         clear = 1;%a%a@]@,\
708
         }@,\
709
         return;@]@,\
710
         }"
711
        print_global_clear_prototype baseNAME
712
        (pp_c_basic_type_desc Type_predef.type_bool)
713
        (* constants *)
714
        (pp_print_list ~pp_prologue:pp_print_cut
715
           (pp_const_clear (pp_c_var_read empty_machine)))
716
        (mpfr_consts constants)
717
        (* dependencies initialization *)
718
        (pp_print_list ~pp_prologue:pp_print_cut print_import_clear)
719
        (List.filter (fun dep -> dep.local) dependencies)
720

  
721
    let print_alloc_function fmt m =
722
      if not !Options.static_mem then
723
        (* Alloc functions, only if non static mode *)
724
        fprintf fmt "@[<v 2>%a {@,%a%a@]@,}@,@[<v 2>%a {@,%a%a@]@,@,"
725
          print_alloc_prototype
726
          (m.mname.node_id, m.mstatic)
727
          print_alloc_const m print_alloc_code m print_dealloc_prototype
728
          m.mname.node_id print_alloc_const m print_dealloc_code m
729

  
730
    let print_mpfr_code self fmt m =
731
      if !Options.mpfr then
732
        fprintf fmt "@,@[<v>%a@,%a@]"
733
          (* Init function *)
734
          (print_init_code self)
735
          m
736
          (* Clear function *)
737
          (print_clear_code self)
738
          m
739

  
740
    (* TODO: ACSL - a contract machine shall not be directly printed in the C
741
       source - but a regular machine associated to a contract machine shall
742
       integrate the associated statements, updating its memories, at the end of
743
       the function body. - last one may print intermediate comment/acsl if/when
744
       they are present in the sequence of instruction *)
745
    let print_machine machines dependencies fmt m =
746
      if fst (get_stateless_status m) then
742 747
        (* Step function *)
743
        (print_step_code machines dependencies self mem) m
744
        (print_mpfr_code self) m
745

  
746
  let print_import_standard source_fmt () =
747
    fprintf source_fmt
748
      "@[<v>#include <assert.h>@,%a%a%a@]"
749
      (if Machine_types.has_machine_type ()
750
       then pp_print_endcut "#include <stdint.h>"
751
       else pp_print_nothing) ()
752
      (if not !Options.static_mem
753
       then pp_print_endcut "#include <stdlib.h>"
754
       else pp_print_nothing) ()
755
      (if !Options.mpfr
756
       then pp_print_endcut "#include <mpfr.h>"
757
       else pp_print_nothing) ()
758

  
759
  let print_extern_alloc_prototype fmt ind =
760
    let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs in
761
    fprintf fmt "extern %a;@,extern %a;"
762
      print_alloc_prototype (ind.nodei_id, static)
763
      print_dealloc_prototype ind.nodei_id
764

  
765
  let print_lib_c source_fmt basename prog machines dependencies =
766
    fprintf source_fmt
767
      "@[<v>\
768
       %a\
769
       %a@,\
770
       @,\
771
       %a@,\
772
       %a\
773
       %a\
774
       %a\
775
       %a\
776
       %a\
777
       %a\
778
       %a\
779
       @]@."
780
      print_import_standard ()
781
      print_import_prototype
782
      {
783
        local = true;
784
        name = basename;
785
        content = [];
786
        is_stateful=true (* assuming it is stateful *);
787
      }
788

  
789
      (* Print the svn version number and the supported C standard (C90 or C99) *)
790
      pp_print_version ()
791

  
792
      (* Print dependencies *)
793
      (pp_print_list
794
         ~pp_open_box:pp_open_vbox0
795
         ~pp_prologue:(pp_print_endcut "/* Import dependencies */")
796
         print_import_prototype
797
         ~pp_epilogue:pp_print_cutcut) dependencies
798

  
799
      (* Print consts *)
800
      (pp_print_list
801
         ~pp_open_box:pp_open_vbox0
802
         ~pp_prologue:(pp_print_endcut "/* Global constants (definitions) */")
803
         print_const_def
804
         ~pp_epilogue:pp_print_cutcut) (get_consts prog)
805

  
806
      (* MPFR *)
807
      (if !Options.mpfr then
808
         fun fmt () ->
809
           fprintf fmt
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff