Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / c_backend.ml @ 2196a0a6

History | View | Annotate | Download (55.3 KB)

1
(* ----------------------------------------------------------------------------
2
 * SchedMCore - A MultiCore Scheduling Framework
3
 * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4
 * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
5
 *
6
 * This file is part of Prelude
7
 *
8
 * Prelude is free software; you can redistribute it and/or
9
 * modify it under the terms of the GNU Lesser General Public License
10
 * as published by the Free Software Foundation ; either version 2 of
11
 * the License, or (at your option) any later version.
12
 *
13
 * Prelude is distributed in the hope that it will be useful, but
14
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
15
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
16
 * Lesser General Public License for more details.
17
 *
18
 * You should have received a copy of the GNU Lesser General Public
19
 * License along with this program ; if not, write to the Free Software
20
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
21
 * USA
22
 *---------------------------------------------------------------------------- *)
23

    
24
(* This module is used for the lustre to C compiler *)
25

    
26
open Format
27
open Corelang
28
open Machine_code
29

    
30
(********************************************************************************************)
31
(*                     Basic      Printing functions                                        *)
32
(********************************************************************************************)
33

    
34
let print_version fmt =
35
  Format.fprintf fmt "/* @[<v>C code generated by %s@,SVN version number %s@,Code is %s compliant */@,@]@."
36
    (Filename.basename Sys.executable_name) Version.number (if !Options.ansi then "ANSI C90" else "C99")
37

    
38
(* Generation of a non-clashing name for the self memory variable (for step and reset functions) *)
39
let mk_self m =
40
  mk_new_name (m.mstep.step_inputs@m.mstep.step_outputs@m.mstep.step_locals@m.mmemory) "self"
41

    
42
(* Generation of a non-clashing name for the instance variable of static allocation macro *)
43
let mk_instance m =
44
  mk_new_name (m.mstep.step_inputs@m.mmemory) "inst"
45

    
46
(* Generation of a non-clashing name for the attribute variable of static allocation macro *)
47
let mk_attribute m =
48
  mk_new_name (m.mstep.step_inputs@m.mmemory) "attr"
49

    
50
let mk_call_var_decl loc id =
51
  { var_id = id;
52
    var_dec_type = mktyp Location.dummy_loc Tydec_any;
53
    var_dec_clock = mkclock Location.dummy_loc Ckdec_any;
54
    var_dec_const = false;
55
    var_type = Type_predef.type_arrow (Types.new_var ()) (Types.new_var ());
56
    var_clock = Clocks.new_var true;
57
    var_loc = loc }
58

    
59
(* counter for loop variable creation *)
60
let loop_cpt = ref (-1)
61

    
62
let reset_loop_counter () =
63
 loop_cpt := -1
64

    
65
let mk_loop_var vars () =
66
  let rec aux () =
67
    incr loop_cpt;
68
    let s = Printf.sprintf "__%s_%d" "i" !loop_cpt in
69
    if List.exists (fun v -> v.var_id = s) vars then aux () else s
70
  in aux ()
71
(*
72
let addr_cpt = ref (-1)
73

    
74
let reset_addr_counter () =
75
 addr_cpt := -1
76

    
77
let mk_addr_var m var =
78
  let vars = m.mmemory in
79
  let rec aux () =
80
    incr addr_cpt;
81
    let s = Printf.sprintf "%s_%s_%d" var "addr" !addr_cpt in
82
    if List.exists (fun v -> v.var_id = s) vars then aux () else s
83
  in aux ()
84
*)
85
let pp_machine_memtype_name fmt id = fprintf fmt "struct %s_mem" id
86
let pp_machine_regtype_name fmt id = fprintf fmt "struct %s_reg" id
87
let pp_machine_alloc_name fmt id = fprintf fmt "%s_alloc" id
88
let pp_machine_static_declare_name fmt id = fprintf fmt "%s_DECLARE" id
89
let pp_machine_static_link_name fmt id = fprintf fmt "%s_LINK" id
90
let pp_machine_static_alloc_name fmt id = fprintf fmt "%s_ALLOC" id
91
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
92
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
93

    
94
let pp_c_dimension fmt d =
95
 fprintf fmt "%a" Dimension.pp_dimension d
96

    
97
let pp_c_type var fmt t =
98
  let rec aux t pp_suffix =
99
  match (Types.repr t).Types.tdesc with
100
  | Types.Tclock t'       -> aux t' pp_suffix
101
  | Types.Tbool           -> fprintf fmt "_Bool %s%a" var pp_suffix ()
102
  | Types.Treal           -> fprintf fmt "double %s%a" var pp_suffix ()
103
  | Types.Tint            -> fprintf fmt "int %s%a" var pp_suffix ()
104
  | Types.Tarray (d, t')  ->
105
    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
106
    aux t' pp_suffix'
107
  | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix
108
  | Types.Tconst ty       -> fprintf fmt "%s %s" ty var
109
  | Types.Tarrow (_, _)   -> fprintf fmt "void (*%s)()" var
110
  | _                     -> eprintf "internal error: pp_c_type %a@." Types.print_ty t; assert false
111
  in aux t (fun fmt () -> ())
112

    
113
let rec pp_c_initialize fmt t = 
114
  match (Types.repr t).Types.tdesc with
115
  | Types.Tint -> pp_print_string fmt "0"
116
  | Types.Tclock t' -> pp_c_initialize fmt t'
117
  | Types.Tbool -> pp_print_string fmt "0" 
118
  | Types.Treal -> pp_print_string fmt "0."
119
  | Types.Tarray (d, t') when Dimension.is_dimension_const d ->
120
    fprintf fmt "{%a}"
121
      (Utils.fprintf_list ~sep:"," (fun fmt _ -> pp_c_initialize fmt t'))
122
      (Utils.duplicate 0 (Dimension.size_const_dimension d))
123
  | _ -> assert false
124

    
125
(* Declaration of an input variable:
126
   - if its type is array/matrix/etc, then declare it as a mere pointer,
127
     in order to cope with unknown/parametric array dimensions, 
128
     as it is the case for generics
129
*)
130
let pp_c_decl_input_var fmt id =
131
  if !Options.ansi && Types.is_address_type id.var_type
132
  then pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
133
  else pp_c_type id.var_id fmt id.var_type
134

    
135
(* Declaration of an output variable:
136
   - if its type is scalar, then pass its address
137
   - if its type is array/matrix/struct/etc, then declare it as a mere pointer,
138
     in order to cope with unknown/parametric array dimensions, 
139
     as it is the case for generics
140
*)
141
let pp_c_decl_output_var fmt id =
142
  if (not !Options.ansi) && Types.is_address_type id.var_type
143
  then pp_c_type                  id.var_id  fmt id.var_type
144
  else pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
145

    
146
(* Declaration of a local/mem variable:
147
   - if it's an array/matrix/etc, its size(s) should be
148
     known in order to statically allocate memory, 
149
     so we print the full type
150
*)
151
let pp_c_decl_local_var fmt id =
152
  pp_c_type id.var_id fmt id.var_type
153

    
154
let pp_c_decl_array_mem self fmt id =
155
  fprintf fmt "%a = (%a) (%s->_reg.%s)"
156
    (pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type
157
    (pp_c_type "(*)") id.var_type
158
    self
159
    id.var_id
160

    
161
(* Declaration of a struct variable:
162
   - if it's an array/matrix/etc, we declare it as a pointer
163
*)
164
let pp_c_decl_struct_var fmt id =
165
  if Types.is_array_type id.var_type
166
  then fprintf fmt "%a;" (pp_c_type (sprintf "(*%s)" id.var_id)) (Types.array_base_type id.var_type)
167
  else fprintf fmt "%a;" (pp_c_type                  id.var_id)  id.var_type
168

    
169
let pp_c_decl_struct_spec_var fmt id =
170
  if !Options.ghost_mode then
171
    fprintf fmt "/*@@ ghost %a */" pp_c_decl_struct_var id
172
 else 
173
    fprintf fmt "%a" pp_c_decl_struct_var id
174

    
175
(* Access to the value of a variable:
176
   - if it's not a scalar output, then its name is enough
177
   - otherwise, dereference it (it has been declared as a pointer,
178
     despite its scalar Lustre type)
179
   - moreover, cast arrays variables into their original array type.
180
*)
181
let pp_c_var_read outputs fmt id =
182
  if Types.is_address_type id.var_type
183
  then
184
    fprintf fmt "%s" id.var_id
185
  else
186
    if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
187
    then fprintf fmt "*%s" id.var_id
188
    else fprintf fmt "%s" id.var_id
189

    
190
(* Addressable value of a variable, the one that is passed around in calls:
191
   - if it's not a scalar non-output, then its name is enough
192
   - otherwise, reference it (it must be passed as a pointer,
193
     despite its scalar Lustre type)
194
*)
195
let pp_c_var_write outputs fmt id =
196
  if Types.is_address_type id.var_type
197
  then
198
    fprintf fmt "%s" id.var_id
199
  else (
200
    (* Format.eprintf "pp_c_var_write: %s , outputs are %a@.@?" id.var_id (Utils.fprintf_list ~sep:", " Printers.pp_var) outputs; *)
201
    if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
202
    then
203
      fprintf fmt "%s" id.var_id
204
    else
205
      fprintf fmt "&%s" id.var_id
206
  )
207
let pp_acsl_type var fmt t =
208
  let rec aux t pp_suffix =
209
  match (Types.repr t).Types.tdesc with
210
  | Types.Tclock t'       -> aux t' pp_suffix
211
  | Types.Tbool           -> fprintf fmt "int %s%a" var pp_suffix ()
212
  | Types.Treal           -> fprintf fmt "real %s%a" var pp_suffix ()
213
  | Types.Tint            -> fprintf fmt "int %s%a" var pp_suffix ()
214
  | Types.Tarray (d, t')  ->
215
    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
216
    aux t' pp_suffix'
217
  (* | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix *)
218
  (* | Types.Tconst ty       -> fprintf fmt "%s %s" ty var *)
219
  (* | Types.Tarrow (_, _)   -> fprintf fmt "void (\*%s)()" var *)
220
  | _                     -> eprintf "internal error: pp_acsl_type %a@." Types.print_ty t; assert false
221
  in aux t (fun fmt () -> ())
222

    
223
let pp_acsl_var_decl fmt id =
224
  pp_acsl_type id.var_id fmt id.var_type
225

    
226

    
227
let pp_c_decl_instance_var fmt (name, (node, static)) = 
228
  fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
229

    
230
let pp_c_tag fmt t =
231
 pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
232

    
233
(* Prints a constant value *)
234
let rec pp_c_const fmt c =
235
  match c with
236
    | Const_int i     -> pp_print_int fmt i
237
    | Const_real r    -> pp_print_string fmt r
238
    | Const_float r   -> pp_print_float fmt r
239
    | Const_tag t     -> pp_c_tag fmt t
240
    | Const_array ca  -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
241
    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
242
    | Const_string s -> Format.fprintf fmt "\"%s\"" s
243
 
244
(* Prints a value expression [v], with internal function calls only.
245
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
246
   but an offset suffix may be added for array variables
247
*)
248
let rec pp_c_val self pp_var fmt v =
249
  match v with
250
    | Cst c         -> pp_c_const fmt c
251
    | Array vl      -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
252
    | Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
253
    | Power (v, n)  -> assert false
254
    | LocalVar v    -> pp_var fmt v
255
    | StateVar v    ->
256
      if Types.is_array_type v.var_type
257
      then fprintf fmt "*%a" pp_var v
258
      else fprintf fmt "%s->_reg.%a" self pp_var v
259
    | Fun (n, vl)   -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl
260

    
261
let pp_c_checks self outputs fmt checks =
262
  Utils.fprintf_list ~sep:"" 
263
    (fun fmt (loc, check) -> 
264
      fprintf fmt "@[<v>%a@,assert (%a);@]@," 
265
	Location.pp_c_loc loc 
266
	(pp_c_val self (pp_c_var_read outputs)) check
267
    ) fmt checks
268

    
269

    
270
(********************************************************************************************)
271
(*                    Instruction Printing functions                                        *)
272
(********************************************************************************************)
273

    
274
(* Computes the depth to which multi-dimension array assignments should be expanded.
275
   It equals the maximum number of nested static array constructions accessible from root [v].
276
*)
277
let rec expansion_depth v =
278
 match v with
279
 | Cst (Const_array cl) -> 1 + List.fold_right (fun c -> max (expansion_depth (Cst c))) cl 0
280
 | Cst _
281
 | LocalVar _
282
 | StateVar _  -> 0
283
 | Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0
284
 | Array vl    -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0
285
 | Access (v, i) -> max 0 (expansion_depth v - 1)
286
 | Power (v, n)  -> 0 (*1 + expansion_depth v*)
287

    
288
type loop_index = LVar of ident | LInt of int ref
289

    
290
(* Computes the list of nested loop variables together with their dimension bounds.
291
   - LInt r stands for loop expansion (no loop variable, but int loop index)
292
   - LVar v stands for loop variable v
293
*)
294
let rec mk_loop_variables (vars:var_decl list) ty depth =
295
 match (Types.repr ty).Types.tdesc, depth with
296
 | Types.Tarray (d, ty'), 0       ->
297
   let v = mk_loop_var vars () in
298
   (d, LVar v) :: mk_loop_variables vars ty' 0
299
 | Types.Tarray (d, ty'), _       ->
300
   let r = ref (-1) in
301
   (d, LInt r) :: mk_loop_variables vars ty' (depth - 1)
302
 | _                    , 0       -> []
303
 | _                              -> assert false
304

    
305
let reorder_loop_variables loop_vars =
306
  let (int_loops, var_loops) = 
307
    List.partition (function (d, LInt _) -> true | _ -> false) loop_vars 
308
  in
309
  var_loops @ int_loops
310

    
311
(* Prints a one loop variable suffix for arrays *)
312
let pp_loop_var fmt lv =
313
 match snd lv with
314
 | LVar v -> fprintf fmt "[%s]" v
315
 | LInt r -> fprintf fmt "[%d]" !r
316

    
317
(* Prints a suffix of loop variables for arrays *)
318
let pp_suffix fmt loop_vars =
319
 Utils.fprintf_list ~sep:"" pp_loop_var fmt loop_vars
320

    
321
(* Prints a [value] indexed by the suffix list [loop_vars] *)
322
let rec pp_value_suffix self loop_vars pp_value fmt value =
323
 match loop_vars, value with
324
 | (_, LInt r) :: q, Array vl     ->
325
   pp_value_suffix self q pp_value fmt (List.nth vl !r)
326
 | _           :: q, Power (v, n) ->
327
   pp_value_suffix self loop_vars pp_value fmt v
328
 | _               , Fun (n, vl)  ->
329
   Basic_library.pp_c n (pp_value_suffix self loop_vars pp_value) fmt vl
330
 | _               , _            ->
331
   let pp_var_suffix fmt v = fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in
332
   pp_c_val self pp_var_suffix fmt value
333

    
334
(* type_directed assignment: array vs. statically sized type
335
   - [var_type]: type of variable to be assigned
336
   - [var_name]: name of variable to be assigned
337
   - [value]: assigned value
338
   - [pp_var]: printer for variables
339
*)
340
let pp_assign vars self pp_var var_type var_name value fmt =
341
  let depth = expansion_depth value in
342
(*eprintf "pp_assign %a %a %d@." Types.print_ty var_type pp_val value depth;*)
343
  let loop_vars = mk_loop_variables vars var_type depth in
344
  let reordered_loop_vars = reorder_loop_variables loop_vars in
345
  let rec aux fmt vars =
346
    match vars with
347
    | [] ->
348
      fprintf fmt "%a = %a;" 
349
	(pp_value_suffix self loop_vars pp_var) var_name
350
	(pp_value_suffix self loop_vars pp_var) value
351
    | (d, LVar i) :: q ->
352
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
353
      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
354
	i i i Dimension.pp_dimension d i
355
	aux q
356
    | (d, LInt r) :: q ->
357
(*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
358
      let szl = Utils.enumerate (Dimension.size_const_dimension d) in
359
      fprintf fmt "@[<v 2>{@,%a@]@,}"
360
	(Utils.fprintf_list ~sep:"@," (fun fmt i -> r := i; aux fmt q)) szl
361
  in
362
  begin
363
    reset_loop_counter ();
364
    (*reset_addr_counter ();*)
365
    aux fmt reordered_loop_vars
366
  end
367

    
368
let pp_expr_rhs vars self pp_var fmt var_type value =
369
  let depth = expansion_depth value in
370
(*eprintf "pp_assign %a %a %d@." Types.print_ty var_type pp_val value depth;*)
371
  let loop_vars = mk_loop_variables vars var_type depth in
372
  let reordered_loop_vars = reorder_loop_variables loop_vars in
373
  let rec aux fmt vars =
374
    match vars with
375
    | [] ->
376
      fprintf fmt "%a;" 
377
	(pp_value_suffix self loop_vars pp_var) value
378
    | _ -> assert false
379
  in
380
  begin
381
    reset_loop_counter ();
382
    (*reset_addr_counter ();*)
383
    aux fmt reordered_loop_vars
384
  end
385

    
386
let pp_instance_call machine_id machine_outputs instances calls self fmt i (inputs: value_t list) (outputs: var_decl list) =
387
  
388
 try (* stateful node instance *)
389
   let (n,_) = List.assoc i instances in
390
  (* Format.eprintf "pp_instance_call: %s , outputs are %a@.@?" (node_name n) (Utils.fprintf_list ~sep:", " Printers.pp_var) outputs; *)
391
 fprintf fmt "%s_step (%a%t%a%t%s->%s);"
392
     (node_name n)
393
     (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read machine_outputs))) inputs
394
     (Utils.pp_final_char_if_non_empty ", " inputs) 
395
     (Utils.fprintf_list ~sep:", " (pp_c_var_write machine_outputs)) outputs
396
     (Utils.pp_final_char_if_non_empty ", " outputs)
397
     self
398
     i
399
 with Not_found -> ((* stateless node instance *)
400
  try 
401
    let (n,_) = List.assoc i calls in
402
  (* Format.eprintf "pp_instance_call: %s , outputs are %a@.@?" (node_name n) (Utils.fprintf_list ~sep:", " Printers.pp_var) outputs; *)
403
    fprintf fmt "%s (%a%t%a);"
404
      (node_name n)
405
      (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read machine_outputs))) inputs
406
      (Utils.pp_final_char_if_non_empty ", " inputs) 
407
      (Utils.fprintf_list ~sep:", " (pp_c_var_write machine_outputs)) outputs 
408
  with Not_found -> (
409
    Format.eprintf "Machine %s: Impossible to find a node named %s in instances (%a) or calls (%a)@.@?"
410
      machine_id
411
      i
412
      (Utils.fprintf_list ~sep:", " (fun fmt (id, _) -> Format.fprintf fmt "%s" id))
413
      instances
414
      (Utils.fprintf_list ~sep:", " (fun fmt (id, _) -> Format.fprintf fmt "%s" id))
415
      calls
416
    ;
417
    assert false
418
  )
419
 )
420
let pp_machine_reset instances self fmt inst =
421
  let (node, static) = List.assoc inst instances in
422
  fprintf fmt "%a(%a%t%s->%s);"
423
    pp_machine_reset_name (node_name node)
424
    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
425
    (Utils.pp_final_char_if_non_empty ", " static)
426
    self inst
427

    
428
let rec pp_conditional ((_, _, outputs, _, _, _, _) as m) self fmt c tl el =
429
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
430
    (pp_c_val self (pp_c_var_read outputs)) c
431
    (Utils.pp_newline_if_non_empty tl)
432
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) tl
433
    (Utils.pp_newline_if_non_empty el)
434
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) el
435

    
436
and pp_machine_instr ((node_id, inputs, outputs, locals, memory, calls, instances) as m) self fmt instr =
437
  let vars = inputs@outputs@locals@memory in 
438
  match instr with 
439
  | MReset i ->
440
    pp_machine_reset instances self fmt i
441
  | MLocalAssign (i,v) ->
442
    pp_assign
443
      vars self (pp_c_var_read outputs) 
444
      i.var_type (LocalVar i) v fmt
445
  | MStateAssign (i,v) ->
446
    pp_assign
447
      vars self (pp_c_var_read outputs) 
448
      i.var_type (StateVar i) v fmt
449
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
450
    pp_machine_instr m self fmt (MLocalAssign (i0, Fun (i, vl)))
451
  | MStep (il, i, vl) ->
452
    pp_instance_call node_id outputs instances calls self fmt i vl il
453
  | MBranch (g,hl) ->
454
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
455
    then (* boolean case, needs special treatment in C because truth value is not unique *)
456
	 (* may disappear if we optimize code by replacing last branch test with default *)
457
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
458
      let el = try List.assoc tag_false hl with Not_found -> [] in
459
      pp_conditional m self fmt g tl el
460
    else (* enum type case *)
461
      fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
462
	(pp_c_val self (pp_c_var_read outputs)) g
463
	(Utils.fprintf_list ~sep:"@," (pp_machine_branch m self)) hl
464

    
465
and pp_machine_branch m self fmt (t, h) =
466
  fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" pp_c_tag t (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) h
467

    
468

    
469
(**************************************************************************)
470
(*     Printing spec for c *)
471

    
472
(**************************************************************************)
473

    
474
let pp_ident is_output fmt id =
475
  if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
476

    
477
let rec pp_const fmt c = 
478
  match c with
479
    | Const_int i -> pp_print_int fmt i
480
    | Const_real r -> pp_print_string fmt r
481
    | Const_float r -> pp_print_float fmt r
482
    | Const_tag  t -> pp_print_string fmt t
483
    | Const_array ca -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
484
    | Const_string s -> Format.fprintf fmt "\"%s\"" s
485
 
486
and pp_var fmt id = fprintf fmt "%s: %a" id.var_id Types.print_ty id.var_type
487

    
488
and pp_expr is_output fmt expr =
489
  let pp_expr = pp_expr is_output in
490
  match expr.expr_desc with
491
    | Expr_const c -> pp_const fmt c
492
    | Expr_ident id -> pp_ident is_output fmt id
493
(*    | Expr_cst_array (c, e) -> fprintf fmt "%a^%a" pp_expr e pp_const c *)
494
    | Expr_array a -> fprintf fmt "[%a]" (pp_tuple is_output) a
495
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
496
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
497
    | Expr_tuple el -> fprintf fmt "(%a)" (pp_tuple is_output) el
498
    | Expr_ite (c, t, e) -> fprintf fmt "(if %a then %a else %a)" pp_expr c pp_expr t pp_expr e
499
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
500
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
501
    | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
502
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
503
    | Expr_merge (id, hl) -> 
504
      fprintf fmt "merge %s %a" id (pp_handlers is_output) hl
505
    | Expr_appl (id, e, r) -> pp_app is_output fmt id e r
506
    | Expr_uclock _
507
    | Expr_dclock _
508
    | Expr_phclock _ -> assert false
509

    
510
and pp_tuple is_output fmt el =
511
 Utils.fprintf_list ~sep:"," (pp_expr is_output) fmt el
512

    
513
and pp_handler is_output fmt (t, h) =
514
 fprintf fmt "(%s -> %a)" t (pp_expr is_output)  h
515

    
516
and pp_handlers is_output fmt hl =
517
 Utils.fprintf_list ~sep:" " (pp_handler is_output) fmt hl
518

    
519
and pp_app is_output fmt id e r =
520
  let pp_expr = pp_expr is_output in
521
  match r with
522
  | None ->
523
    (match id, e.expr_desc with
524
    | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
525
    | "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
526
    | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
527
    | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
528
    | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
529
    | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
530
    | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_expr e1 pp_expr e2
531
    | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_expr e1 pp_expr e2
532
    | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_expr e1 pp_expr e2
533
    | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_expr e1 pp_expr e2
534
    | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
535
    | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
536
    | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
537
    | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
538
    | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_expr e1 pp_expr e2
539
    | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_expr e1 pp_expr e2
540
    | "not", _ -> fprintf fmt "(! %a)" pp_expr e
541
    | "ite", Expr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_expr e1 pp_expr e2 pp_expr e3
542
    | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
543
    | _ -> fprintf fmt "%s (%a)" id pp_expr e
544
)
545
  | Some (x, l) -> fprintf fmt "%s (%a) every %s(%s)" id pp_expr e l x 
546
	
547
let pp_quantifiers fmt (q, vars) =
548
  match q with
549
    | Forall -> fprintf fmt "\\forall %a;" (Utils.fprintf_list ~sep:", " pp_acsl_var_decl) vars 
550
    | Exists -> fprintf fmt "\\exists %a;" (Utils.fprintf_list ~sep:", " pp_acsl_var_decl) vars 
551

    
552
let rec pp_acsl_val ?(is_lhs=false) self pp_var fmt v =
553
  match v with
554
    | Cst c         -> pp_c_const fmt c
555
    | Array _      
556
    | Access _       -> assert false (* no arrays *)
557
    | Power (v, n)  -> assert false
558
    | LocalVar v    -> pp_var fmt v
559
    | StateVar v    ->     
560
      if Types.is_array_type v.var_type
561
      then assert false
562
      else fprintf fmt "%s->_reg.%a" self pp_var v
563
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_acsl n Machine_code.get_val_type (pp_acsl_val self pp_var)) vl
564

    
565

    
566
let rec pp_eexpr_logic_instr 
567
    ((node_id, inputs, outputs, locals, memory) as m) self fmt instr =
568
  match instr with 
569
  | MReset i -> assert false (* should not happen, calls were inlined *)
570
  | MLocalAssign (i,v) -> (
571
    match outputs with 
572
    | [o] -> if i = o then
573
	fprintf fmt "%a;" (pp_acsl_val self (pp_c_var_read outputs)) v
574
      else
575
	fprintf fmt "\\let %a = %a;" 
576
	  (pp_c_var_read outputs (* TODO no variable shold be treated as output *)) i
577
	  (pp_acsl_val self (pp_c_var_read outputs)) v
578

    
579
    | _ -> assert false (* should not happen: only a single output *)
580
)
581
  | MStateAssign (i,v) -> assert false (* should not happen, no side effects in logical predicates *)
582
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
583
    pp_eexpr_logic_instr m self fmt (MLocalAssign (i0, Fun (i, vl)))
584
  | MStep ([i0], "ite", vl) ->
585
    pp_eexpr_logic_instr m self fmt (MLocalAssign (i0, Fun ("ite", vl)))
586
  | MStep (il, i, vl) ->
587
    Format.eprintf "Illegal function call %s@.%a@.@?" i pp_instr instr; 
588
    assert false (* should not happen, calls were inlined *)
589
  | MBranch (g,hl) -> assert false (* should not happen. Oder ??? TODO *)
590

    
591

    
592
let pp_logic_eexpr node_id self is_output fmt ee =
593
(* TODO deal with output * *)
594
  fprintf fmt "%a%t%a"
595
    (Utils.fprintf_list ~sep:"@ " pp_quantifiers) ee.mquantifiers
596
    (Utils.pp_final_char_if_non_empty " " ee.mquantifiers) 
597
    (Utils.fprintf_list ~sep:"@;" 
598
       (pp_eexpr_logic_instr (node_id, ee.mmstep_logic.step_inputs, ee.mmstep_logic.step_outputs, ee.mmstep_logic.step_locals, ee.mmmemory) self)) ee.mmstep_logic.step_instrs
599
    
600

    
601
(* TODO:
602
   - faire les fonctions: logics, contracts (done) , side effect 
603
   - gerer l'extension des structs avec des ghosts -- done
604
   - gerer l'appel aux noeuds: structs + logics + side effect pour le contenu du noeud
605
*)
606
let pp_acsl_spec_logics m outputs fmt spec = 
607
  let self = mk_self m in
608
  let pp_expr_def fmt ee =
609
    match ee.mmstep_logic.step_instrs with
610
    | [MStep([o], i, vl)] -> () (* We do nothing, the expression is simple and 
611
				   was introduced directly in the contract *)
612
    | _ -> ((* We define a new ACSL predicate *)
613
      fprintf fmt "/*@@ @[<v 3>predicate spec_%i(%a%t%a *%s) =@;%a@]@;*/@." 
614
	ee.muid   
615
	(Utils.fprintf_list ~sep:", " pp_acsl_var_decl) ee.mmstep_logic.step_inputs
616
	(Utils.pp_final_char_if_non_empty ", " ee.mmstep_logic.step_inputs)
617
	pp_machine_memtype_name m.mname.node_id
618
	self
619
	(* (Utils.fprintf_list ~sep:", " pp_acsl_var_decl) ee.mmstep.step_inputs *)
620
	(pp_logic_eexpr m.mname.node_id self is_output) ee
621
    )
622

    
623
  in
624
  List.iter (pp_expr_def fmt) 
625
    (spec.m_requires@
626
       spec.m_ensures@
627
       (List.fold_left 
628
	  (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
629
	  [] spec.m_behaviors)
630
    )
631

    
632
(* Access to the value of a variable:
633
   - if it's not a scalar output, then its name is enough
634
   - otherwise, dereference it (it has been declared as a pointer,
635
     despite its scalar Lustre type)
636
   - moreover, cast arrays variables into their original array type.
637
*)
638
let pp_acsl_var_read outputs fmt id =
639
  if Types.is_array_type id.var_type
640
  then
641
    assert false (* no array *)
642
  else ( (* Hack to cast boolean variables as int for ACSL predicates *)
643
    if (Types.repr id.var_type).Types.tdesc = Types.Tbool then
644
      fprintf fmt "(int)" 
645
    ;
646
    if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
647
    then fprintf fmt "*%s" id.var_id
648
    else fprintf fmt "%s" id.var_id
649
  )
650
let pp_acsl_spec_contracts m outputs fmt spec = 
651
  let self = mk_self m in
652
    (* let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in *)
653
  let pp_eexpr_expr fmt ee = 
654
      (* If the eexpr contains a single definition we use it directly. Otherwise,
655
	 we rely on an external predicate *)
656
    match ee.mmstep_logic.step_instrs with
657
    | [MStep([o], i, vl)] -> 
658
      fprintf fmt "%a %t"
659
	(Utils.fprintf_list ~sep:" " pp_quantifiers) ee.mquantifiers
660
	(fun fmt ->
661
	  let value = Fun (i, vl) in
662
	  let vars : var_decl list = 
663
	    ee.mmstep_logic.step_inputs@ee.mmstep_logic.step_outputs@ee.mmstep_logic.step_locals@ee.mmmemory 
664
	  in 
665
	  pp_expr_rhs vars self (pp_c_var_read outputs) fmt o.var_type value 
666
	)
667
    | _ -> fprintf fmt "spec_%i(%a, %s);" 
668
      ee.muid   
669
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read outputs)) ee.mmstep_logic.step_inputs
670
      self
671
  in
672
  fprintf fmt "@[<v 2>/*@@ ";
673
  Utils.fprintf_list ~sep:"" 
674
    (fun fmt r -> fprintf fmt "requires %a@ " pp_eexpr_expr r) 
675
    fmt 
676
    spec.m_requires;
677
  Utils.fprintf_list ~sep:"" 
678
    (fun fmt r -> fprintf fmt "ensures %a@ " pp_eexpr_expr r) 
679
    fmt 
680
    spec.m_ensures;
681
  fprintf fmt "@ ";
682
    (* TODO assigns + separated *)
683
    (* fprintf fmt "assigns *self%t%a;@ "  *)
684
    (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
685
    (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
686
    Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, ensures) -> 
687
      fprintf fmt "behavior %s:@[@ %a@ %a@]" 
688
	name
689
	(Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a" pp_eexpr_expr r)) assumes
690
	(Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a" pp_eexpr_expr r)) ensures
691
    ) fmt spec.m_behaviors;
692
    fprintf fmt "@]@ */@.";
693
    ()
694

    
695

    
696
(*
697
  let self = mk_self m in
698
  let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in
699
  let pp_eexpr_expr ee = pp_eexpr_expr (m.mname.node_id, ee.mmstep.step_inputs, ee.mmstep.step_outputs, ee.mmstep.step_locals, ee.mmmemory, ee.mminstances, ee.mmcalls) self is_output in
700
  fprintf fmt "@[<v 2>/*@@ ";
701
  Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " (pp_eexpr_expr r) r) fmt spec.m_requires;
702
  Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "ensures %a;@ " (pp_eexpr_expr r) r) fmt spec.m_ensures;
703
  fprintf fmt "@ ";
704
  (* TODO assigns + separated *)
705
  (* fprintf fmt "assigns *self%t%a;@ "  *)
706
  (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
707
  (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
708
  Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, ensures) -> 
709
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
710
      name
711
      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" (pp_eexpr_expr r) r)) assumes
712
      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a;" (pp_eexpr_expr r) r)) ensures
713
  ) fmt spec.m_behaviors;
714
  fprintf fmt "@]@ */@.";
715
  ()
716

    
717
*)
718

    
719
let pp_acsl_spec_side_effects m outputs fmt spec = 
720
  let self = mk_self m in
721
  let pp_side_effects fmt ee =  
722
    (* Declare local vars *)
723
    let locals = List.filter (fun l -> not (List.mem l m.mstep.step_locals)) ee.mmstep_effects.step_locals in
724
    (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) fmt locals;
725
    Utils.pp_final_char_if_non_empty ";@," locals fmt ;
726
      
727
    (* Print instructions *)
728
    Utils.fprintf_list ~sep:"@;" 
729
      (pp_machine_instr (m.mname.node_id, ee.mmstep_effects.step_inputs, outputs, ee.mmstep_effects.step_locals, ee.mmmemory, ee.mminstances, ee.mmcalls) self)
730
      fmt 
731
      ee.mmstep_effects.step_instrs
732
in
733
  let effects = spec.m_requires@spec.m_ensures@
734
    (List.fold_left 
735
       (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
736
	  [] spec.m_behaviors)
737
  in
738
  let effects = List.filter (fun ee -> ee.mmstep_effects.step_instrs <> []) effects in
739
  let all_instrs = List.flatten (List.map (fun e -> e.mmstep_effects.step_instrs) effects) in
740
  if all_instrs <> [] then (
741
    fprintf fmt "// Begin of specification memory update block@;";
742
    if !Options.ghost_mode then
743
      fprintf fmt "@[<v 3>/*@@ ghost %a@]@;*/@;" 
744
	(Utils.fprintf_list ~sep:"@;" pp_side_effects)
745
	effects
746
    else (
747
      Utils.fprintf_list ~sep:"@;" pp_side_effects fmt effects;
748
      fprintf fmt "@;"
749
    )
750
    ;
751
    fprintf fmt "// End of specification memory update block@."
752
  )
753

    
754

    
755
(********************************************************************************************)
756
(*                      Prototype Printing functions                                        *)
757
(********************************************************************************************)
758

    
759
let print_alloc_prototype fmt (name, static) =
760
  fprintf fmt "%a * %a (%a)"
761
    pp_machine_memtype_name name
762
    pp_machine_alloc_name name
763
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static
764

    
765
let print_reset_prototype self fmt (name, static) =
766
  fprintf fmt "void %a (@[<v>%a%t%a *%s@])"
767
    pp_machine_reset_name name
768
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static
769
    (Utils.pp_final_char_if_non_empty ",@," static) 
770
    pp_machine_memtype_name name
771
    self
772

    
773
let print_stateless_prototype fmt (name, inputs, outputs) =
774
match outputs with
775
(* DOESN'T WORK FOR ARRAYS
776
  | [o] -> fprintf fmt "%a (@[<v>%a@])"
777
    (pp_c_type name) o.var_type
778
    (Utils.fprintf_list ~sep:",@ " pp_c_var) inputs
779
*)  
780
  | _ -> fprintf fmt "void %s (@[<v>@[%a%t@]@,@[%a@]@,@])"
781
    name
782
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs
783
    (Utils.pp_final_char_if_non_empty ",@ " inputs) 
784
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_output_var) outputs
785

    
786
let print_step_prototype self fmt (name, inputs, outputs) =
787
  fprintf fmt "void %a (@[<v>@[%a%t@]@,@[%a@]%t@[%a *%s@]@])"
788
    pp_machine_step_name name
789
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs
790
    (Utils.pp_final_char_if_non_empty ",@ " inputs) 
791
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_output_var) outputs
792
    (Utils.pp_final_char_if_non_empty ",@," outputs) 
793
    pp_machine_memtype_name name
794
    self
795

    
796
(********************************************************************************************)
797
(*                         Header Printing functions                                        *)
798
(********************************************************************************************)
799

    
800
(* Removed because of "open" constructs. No more extern functions *)
801
(*
802
let print_prototype fmt decl =
803
  match decl.top_decl_desc with
804
    | ImportedFun m -> (
805
        fprintf fmt "extern %a;@,"
806
	  print_stateless_prototype 
807
	  (m.fun_id, m.fun_inputs, m.fun_outputs)
808
    )
809
    | ImportedNode m -> (
810
      if m.nodei_stateless then (* It's a function not a node *)
811
        fprintf fmt "extern %a;@,"
812
	  print_stateless_prototype 
813
	  (m.nodei_id, m.nodei_inputs, m.nodei_outputs)
814
      else (
815
	let static = List.filter (fun v -> v.var_dec_const) m.nodei_inputs in
816
        fprintf fmt "extern %a;@,"
817
	  print_alloc_prototype (m.nodei_id, static);
818
	fprintf fmt "extern %a;@,"
819
	  (print_reset_prototype "self") (m.nodei_id, static);
820
	fprintf fmt "extern %a;@,"
821
	  (print_step_prototype "self") (m.nodei_id, m.nodei_inputs, m.nodei_outputs);
822
      )
823
    )
824
    | _ -> () (* We don't do anything here *)
825
      *)
826

    
827
let print_import_standard fmt =
828
  fprintf fmt "#include \"%s/include/lustrec/arrow.h\"@.@." Version.prefix
829

    
830
let print_prototype fmt decl =
831
  match decl.top_decl_desc with
832
  | Open m -> fprintf fmt "#include \"%s.h\"@," m
833
  | _ -> () (* We don't do anything here *)
834

    
835
(* TODO: what to do when the _reg struct only contains ghost code ? It is
836
   considered as empty for gcc. Is this a problem? *)
837
let pp_registers_struct fmt m =
838
  let spec_memories = match m.mspec with
839
      None -> []
840
    | Some s -> List.flatten (
841
      List.map (fun ee -> ee.mmmemory) 
842
	(s.m_requires@
843
	   s.m_ensures@
844
	   (List.fold_left 
845
	      (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
846
	      [] s.m_behaviors)
847
	))
848
  in
849
  if m.mmemory <> [] || spec_memories <> [] 
850
  then
851
    fprintf fmt "@[%a {@[<v>%a%a@]}@] _reg; "
852
      pp_machine_regtype_name m.mname.node_id
853
      (Utils.fprintf_list ~sep:"@;" pp_c_decl_struct_var) m.mmemory
854
      (Utils.fprintf_list ~sep:"@;" pp_c_decl_struct_spec_var) spec_memories
855
      
856
      
857
  else
858
    ()
859

    
860
let print_machine_struct fmt m =
861
  if m.mname.node_id != arrow_id
862
  then (
863
    (* We don't print arrow function *)
864
    (* Define struct *)
865
    fprintf fmt "@[%a {@[%a%a%t@]};@]@."
866
      pp_machine_memtype_name m.mname.node_id
867
      pp_registers_struct m
868
      (Utils.fprintf_list ~sep:"; " pp_c_decl_instance_var) m.minstances
869
      (Utils.pp_final_char_if_non_empty "; " m.minstances)
870
  )
871

    
872
(*
873
let pp_static_array_instance fmt m (v, m) =
874
 fprintf fmt "%s" (mk_addr_var m v)
875
*)
876
let print_static_declare_instance attr fmt (i, (m, static)) =
877
  fprintf fmt "%a(%s, %a%t%s)"
878
    pp_machine_static_declare_name (node_name m)
879
    attr
880
    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
881
    (Utils.pp_final_char_if_non_empty ", " static)
882
    i
883

    
884
let print_static_declare_macro fmt m =
885
  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
886
  let inst = mk_instance m in
887
  let attr = mk_attribute m in
888
  fprintf fmt "@[<v 2>#define %a(%s, %a%t%s)\\@,%s %a %s;\\@,%a%t%a;@,@]"
889
    pp_machine_static_declare_name m.mname.node_id
890
    attr
891
    (Utils.fprintf_list ~sep:", " (pp_c_var_read m.mstep.step_outputs)) m.mstatic
892
    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
893
    inst
894
    attr
895
    pp_machine_memtype_name m.mname.node_id
896
    inst
897
    (Utils.fprintf_list ~sep:";\\@," pp_c_decl_local_var) array_mem
898
    (Utils.pp_final_char_if_non_empty ";\\@," array_mem)
899
    (Utils.fprintf_list ~sep:";\\@,"
900
       (fun fmt (i',m') ->
901
	 let path = sprintf "inst ## _%s" i' in
902
	 fprintf fmt "%a"
903
	   (print_static_declare_instance attr) (path,m')
904
       )) m.minstances
905

    
906
      
907
let print_static_link_instance fmt (i, (m, _)) =
908
 fprintf fmt "%a(%s)" pp_machine_static_link_name (node_name m) i
909

    
910
let print_static_link_macro fmt m =
911
  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
912
  fprintf fmt "@[<v>@[<v 2>#define %a(inst) do {\\@,%a%t%a;\\@]@,} while (0)@.@]"
913
    pp_machine_static_link_name m.mname.node_id
914
    (Utils.fprintf_list ~sep:";\\@,"
915
       (fun fmt v ->
916
	 fprintf fmt "inst.%s = &%s"
917
	   v.var_id
918
	   v.var_id
919
       )) array_mem
920
    (Utils.pp_final_char_if_non_empty ";\\@," array_mem)
921
    (Utils.fprintf_list ~sep:";\\@,"
922
       (fun fmt (i',m') ->
923
	 let path = sprintf "inst ## _%s" i' in
924
	 fprintf fmt "%a;\\@,inst.%s = &%s"
925
	   print_static_link_instance (path,m')
926
	   i'
927
	   path
928
       )) m.minstances
929
      
930
let print_static_alloc_macro fmt m =
931
  fprintf fmt "@[<v>@[<v 2>#define %a(attr,%a%tinst)\\@,%a(attr,%a%tinst);\\@,%a(inst);@]@,@]@."
932
    pp_machine_static_alloc_name m.mname.node_id
933
    (Utils.fprintf_list ~sep:", " (pp_c_var_read m.mstep.step_outputs)) m.mstatic
934
    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
935
    pp_machine_static_declare_name m.mname.node_id
936
    (Utils.fprintf_list ~sep:", " (pp_c_var_read m.mstep.step_outputs)) m.mstatic
937
    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
938
    pp_machine_static_link_name m.mname.node_id
939

    
940
let print_machine_decl fmt m =
941
  if m.mname.node_id <> arrow_id then 
942
    (
943
      (* We don't print arrow function *)
944
      
945
      (* Print specification if any: insert logic definition before the function  *)
946
      (match m.mspec with
947
      | None -> ()
948
      | Some spec -> 
949
	pp_acsl_spec_logics m m.mstep.step_outputs fmt spec
950
      );
951
      
952
      (* Static allocation *)
953
      if !Options.static_mem
954
      then (
955
	fprintf fmt "%a@.%a@.%a@."
956
	  print_static_declare_macro m
957
	  print_static_link_macro m
958
	  print_static_alloc_macro m
959
      )
960
      else ( 
961
      (* Dynamic allocation *)
962
	fprintf fmt "extern %a;@.@."
963
	  print_alloc_prototype (m.mname.node_id, m.mstatic)
964
      );
965
      let self = mk_self m in
966
      fprintf fmt "extern %a;@.@."
967
	(print_reset_prototype self) (m.mname.node_id, m.mstatic);
968
    (* Print specification contracts if any *)
969
      (match m.mspec with
970
      | None -> ()
971
      | Some spec -> 
972
	pp_acsl_spec_contracts m m.mstep.step_outputs fmt spec
973
      );
974
      fprintf fmt "extern %a;@.@."
975
	(print_step_prototype self)
976
	(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
977
    )
978

    
979

    
980
(********************************************************************************************)
981
(*                         C file Printing functions                                        *)
982
(********************************************************************************************)
983

    
984
let print_const_def fmt cdecl =
985
  fprintf fmt "%a = %a;@." (pp_c_type cdecl.const_id) cdecl.const_type pp_c_const cdecl.const_value 
986

    
987
let print_const_decl fmt cdecl =
988
  fprintf fmt "extern %a;@." (pp_c_type cdecl.const_id) cdecl.const_type
989

    
990
let print_alloc_instance fmt (i, (m, static)) =
991
  fprintf fmt "_alloc->%s = %a (%a);@,"
992
    i
993
    pp_machine_alloc_name (node_name m)
994
    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
995

    
996
let print_alloc_array fmt vdecl =
997
  let base_type = Types.array_base_type vdecl.var_type in
998
  let size_types = Types.array_type_multi_dimension vdecl.var_type in
999
  let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in
1000
  fprintf fmt "_alloc->%s = (%a*) malloc((%a)*sizeof(%a));@,assert(_alloc->%s);@,"
1001
    vdecl.var_id
1002
    (pp_c_type "") base_type
1003
    Dimension.pp_dimension size_type
1004
    (pp_c_type "") base_type
1005
    vdecl.var_id
1006

    
1007
let print_alloc_code fmt m =
1008
  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
1009
  fprintf fmt "%a *_alloc;@,_alloc = (%a *) malloc(sizeof(%a));@,assert(_alloc);@,%a%areturn _alloc;"
1010
    pp_machine_memtype_name m.mname.node_id
1011
    pp_machine_memtype_name m.mname.node_id
1012
    pp_machine_memtype_name m.mname.node_id
1013
    (Utils.fprintf_list ~sep:"" print_alloc_array) array_mem
1014
    (Utils.fprintf_list ~sep:"" print_alloc_instance) m.minstances
1015

    
1016
let print_step_code fmt m self =
1017
  if not (!Options.ansi && 
1018
	     is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc })
1019
  then
1020
    (* C99 code *)
1021
    let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
1022
    fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%t%t@]@,}@.@."
1023
      (print_step_prototype self) (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
1024
      (* locals *)
1025
      (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals
1026
      (Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals)
1027
      (* array mems *)
1028
      (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
1029
      (Utils.pp_final_char_if_non_empty ";@," array_mems)
1030
      (* check assertions *)
1031
      (pp_c_checks self m.mstep.step_outputs) m.mstep.step_checks
1032
      (* instrs *)
1033
      (Utils.fprintf_list ~sep:"@," (pp_machine_instr (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, m.mstep.step_locals, m.mmemory, m.minstances, m.mcalls) self)) m.mstep.step_instrs
1034
      (Utils.pp_newline_if_non_empty m.mstep.step_instrs)
1035
      (* Print specification if any: insert side effect at the end of the function body  *)
1036
      (fun fmt -> match m.mspec with
1037
      | None -> ()
1038
      | Some spec -> pp_acsl_spec_side_effects m m.mstep.step_outputs fmt spec
1039
      )
1040
      (fun fmt -> fprintf fmt "return;")
1041
  else
1042
    (* C90 code *)
1043
    let (gen_locals, base_locals) = List.partition (fun v -> Types.is_generic_type v.var_type) m.mstep.step_locals in
1044
    let gen_calls = List.map (fun e -> let (id, _, _) = call_of_expr e in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
1045
    fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t%t@]@,}@.@."
1046
      (print_step_prototype self) 
1047
         (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
1048
      (* locals *)
1049
      (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) base_locals
1050
      (Utils.pp_final_char_if_non_empty ";" base_locals)
1051
      (* check assertions *)
1052
      (pp_c_checks self m.mstep.step_outputs) m.mstep.step_checks
1053
      (* instrs *)
1054
      (Utils.fprintf_list ~sep:"@," 
1055
	 (pp_machine_instr 
1056
	    (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, m.mstep.step_locals, m.mmemory, m.minstances, m.mcalls) self)
1057
      ) m.mstep.step_instrs
1058
      (Utils.pp_newline_if_non_empty m.mstep.step_instrs)
1059
      (* Print specification if any: insert side effect at the end of the function body  *)
1060
      (fun fmt -> match m.mspec with
1061
      | None -> ()
1062
      | Some spec -> pp_acsl_spec_side_effects m m.mstep.step_outputs fmt spec
1063
      )
1064
      (fun fmt -> fprintf fmt "return;")
1065

    
1066
let print_machine fmt m =
1067
  if m.mname.node_id <> arrow_id
1068
  then (
1069
  (* We don't print arrow function *)
1070
  (* Alloc function, only if non static mode *)
1071
    if (not !Options.static_mem) then  
1072
      (
1073
	fprintf fmt "@[<v 2>%a {@,%a@]@,}@.@."
1074
	  print_alloc_prototype (m.mname.node_id, m.mstatic)
1075
	  print_alloc_code m;
1076
      );
1077
    let self = mk_self m in
1078
    (* Reset function *)
1079
    fprintf fmt "@[<v 2>%a {@,%a%treturn;@]@,}@.@."
1080
      (print_reset_prototype self) (m.mname.node_id, m.mstatic)
1081
      (Utils.fprintf_list ~sep:"@," 
1082
	 (pp_machine_instr 
1083
	    (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, m.mstep.step_locals, m.mmemory, m.minstances, m.mcalls) self)) 
1084
      m.minit
1085
      (Utils.pp_newline_if_non_empty m.minit);
1086
    
1087
    (* Step function *)
1088
    print_step_code fmt m self
1089
  )
1090

    
1091
(********************************************************************************************)
1092
(*                         Main related functions                                           *)
1093
(********************************************************************************************)
1094

    
1095
let print_get_input fmt v =
1096
  match v.var_type.Types.tdesc with
1097
    | Types.Tint -> fprintf fmt "_get_int(\"%s\")" v.var_id
1098
    | Types.Tbool -> fprintf fmt "_get_bool(\"%s\")" v.var_id
1099
    | Types.Treal -> fprintf fmt "_get_double(\"%s\")" v.var_id
1100
    | _ -> assert false
1101

    
1102
let print_put_outputs fmt ol = 
1103
  let po fmt o =
1104
    match o.var_type.Types.tdesc with
1105
    | Types.Tint -> fprintf fmt "_put_int(\"%s\", %s)" o.var_id o.var_id
1106
    | Types.Tbool -> fprintf fmt "_put_bool(\"%s\", %s)" o.var_id o.var_id
1107
    | Types.Treal -> fprintf fmt "_put_double(\"%s\", %s)" o.var_id o.var_id
1108
    | _ -> assert false
1109
  in
1110
  List.iter (fprintf fmt "@ %a;" po) ol
1111

    
1112
let print_main_fun machines m fmt =
1113
  let mname = m.mname.node_id in
1114
  let main_mem =
1115
    if (!Options.static_mem && !Options.main_node <> "")
1116
    then "&main_mem"
1117
    else "main_mem" in
1118
  fprintf fmt "@[<v 2>int main (int argc, char *argv[]) {@ ";
1119
  fprintf fmt "/* Declaration of inputs/outputs variables */@ ";
1120
  List.iter 
1121
    (fun v -> fprintf fmt "%a = %a;@ " (pp_c_type v.var_id) v.var_type pp_c_initialize v.var_type
1122
    ) m.mstep.step_inputs;
1123
  List.iter 
1124
    (fun v -> fprintf fmt "%a = %a;@ " (pp_c_type v.var_id) v.var_type pp_c_initialize v.var_type
1125
    ) m.mstep.step_outputs;
1126
  fprintf fmt "@ /* Main memory allocation */@ ";
1127
  if (!Options.static_mem && !Options.main_node <> "")
1128
  then (fprintf fmt "%a(static,main_mem);@ " pp_machine_static_alloc_name mname)
1129
  else (fprintf fmt "%a *main_mem = %a();@ " pp_machine_memtype_name mname pp_machine_alloc_name mname);
1130
  fprintf fmt "@ /* Initialize the main memory */@ ";
1131
  fprintf fmt "%a(%s);@ " pp_machine_reset_name mname main_mem;
1132
  fprintf fmt "@ ISATTY = isatty(0);@ ";
1133
  fprintf fmt "@ /* Infinite loop */@ ";
1134
  fprintf fmt "@[<v 2>while(1){@ ";
1135
  fprintf fmt  "fflush(stdout);@ ";
1136
  List.iter 
1137
    (fun v -> fprintf fmt "%s = %a;@ "
1138
      v.var_id
1139
      print_get_input v
1140
    ) m.mstep.step_inputs;
1141
  (match m.mstep.step_outputs with
1142
    (* | [] -> ( *)
1143
    (*   fprintf fmt "%a(%a%t%s);@ "  *)
1144
    (* 	pp_machine_step_name mname *)
1145
    (* 	(Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs *)
1146
    (* 	(pp_final_char_if_non_empty ", " m.mstep.step_inputs) *)
1147
    (* 	main_mem *)
1148
    (* ) *)
1149
    (* | [o] -> ( *)
1150
    (*   fprintf fmt "%s = %a(%a%t%a, %s);%a" *)
1151
    (* 	o.var_id *)
1152
    (* 	pp_machine_step_name mname *)
1153
    (* 	(Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs *)
1154
    (* 	(pp_final_char_if_non_empty ", " m.mstep.step_inputs) *)
1155
    (* 	(Utils.fprintf_list ~sep:", " (fun fmt v -> fprintf fmt "&%s" v.var_id)) m.mstep.step_outputs *)
1156
    (* 	main_mem *)
1157
    (* 	print_put_outputs [o]) *)
1158
    | _ -> (
1159
      fprintf fmt "%a(%a%t%a, %s);%a"
1160
	pp_machine_step_name mname
1161
	(Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs
1162
	(Utils.pp_final_char_if_non_empty ", " m.mstep.step_inputs)
1163
	(Utils.fprintf_list ~sep:", " (fun fmt v -> fprintf fmt "&%s" v.var_id)) m.mstep.step_outputs
1164
	main_mem
1165
	print_put_outputs m.mstep.step_outputs)
1166
  );
1167
  fprintf fmt "@]@ }@ ";
1168
  fprintf fmt "return 1;";
1169
  fprintf fmt "@]@ }@."       
1170

    
1171
let print_main_header fmt =
1172
  fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/include/lustrec/io_frontend.h\"@." Version.prefix
1173

    
1174
let rec pp_c_struct_type_field filename cpt fmt (label, tdesc) =
1175
  fprintf fmt "%a;" (pp_c_type_decl filename cpt label) tdesc
1176
and pp_c_type_decl filename cpt var fmt tdecl =
1177
  match tdecl with
1178
  | Tydec_any           -> assert false
1179
  | Tydec_int           -> fprintf fmt "int %s" var
1180
  | Tydec_real          -> fprintf fmt "double %s" var
1181
  | Tydec_float         -> fprintf fmt "float %s" var
1182
  | Tydec_bool          -> fprintf fmt "_Bool %s" var
1183
  | Tydec_clock ty      -> pp_c_type_decl filename cpt var fmt ty
1184
  | Tydec_const c       -> fprintf fmt "%s %s" c var
1185
  | Tydec_array (d, ty) -> fprintf fmt "%a[%a]" (pp_c_type_decl filename cpt var) ty pp_c_dimension d
1186
  | Tydec_enum tl ->
1187
    begin
1188
      incr cpt;
1189
      fprintf fmt "enum _enum_%s_%d { %a } %s" filename !cpt (Utils.fprintf_list ~sep:", " pp_print_string) tl var
1190
    end
1191
  | Tydec_struct fl ->
1192
    begin
1193
      incr cpt;
1194
      fprintf fmt "struct _struct_%s_%d { %a } %s" filename !cpt (Utils.fprintf_list ~sep:" " (pp_c_struct_type_field filename cpt)) fl var
1195
    end
1196

    
1197
let print_type_definitions fmt filename =
1198
  let cpt_type = ref 0 in
1199
  Hashtbl.iter (fun typ def ->
1200
    match typ with
1201
    | Tydec_const var ->
1202
      fprintf fmt "typedef %a;@.@."
1203
	(pp_c_type_decl filename cpt_type var) def
1204
    | _        -> ()) type_table
1205

    
1206
let print_makefile basename nodename dependencies fmt =
1207
  fprintf fmt "GCC=gcc@.";
1208
  fprintf fmt "LUSTREC=%s@." Sys.executable_name;
1209
  fprintf fmt "LUSTREC_BASE=%s@." (Filename.dirname (Filename.dirname Sys.executable_name));
1210
  fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
1211
  fprintf fmt "INC=${LUSTREC_BASE}/include/lustrec@.";
1212
  fprintf fmt "@.";
1213

    
1214
  (* main binary *)
1215
  fprintf fmt "%s_%s:@." basename nodename;
1216
  fprintf fmt "\t${GCC} -I${INC} -I. -c %s.c@." basename;    
1217
  fprintf fmt "\t${GCC} -I${INC} -I. -c %s_%s.c@." basename nodename;    
1218
  List.iter (fun s -> (* Format.eprintf "Adding dependency: %s@." s;  *)
1219
    fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
1220
    (("${INC}/io_frontend.c")::(List.map (fun s -> s ^ ".c") dependencies));    
1221
  (*  fprintf fmt "\t${GCC} -I${INC} -c ${INC}/StdLibrary.c@."; *)
1222
  (*  fprintf fmt "\t${GCC} -o %s_%s io_frontend.o StdLibrary.o -lm %s.o@." basename nodename basename*)
1223
  fprintf fmt "\t${GCC} -o %s_%s io_frontend.o %a -lm %s.o %s_%s.o@." 
1224
    basename nodename (* executable name *)
1225
    (Utils.fprintf_list ~sep:" " (fun fmt s -> Format.fprintf fmt "%s.o" s)) dependencies 
1226
    basename (* library .o *)
1227
    basename nodename (* main function . o *) ;
1228
  fprintf fmt "@.";
1229
  fprintf fmt "@.";
1230

    
1231
  (* EACSL version of library file . c *)
1232
  fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
1233
  fprintf fmt "\tframa-c -e-acsl-full-mmodel -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@." basename basename; 
1234
  fprintf fmt "@.";
1235
  fprintf fmt "@.";
1236

    
1237
  (* EACSL version of binary *)
1238
  fprintf fmt "%s_%s_eacsl: %s_eacsl.c %s_%s.c @." basename nodename basename basename nodename;
1239
  fprintf fmt "\t${GCC} -I${INC} -I. -c %s_eacsl.c@." basename; (* compiling instrumented lib *)
1240
  fprintf fmt "\t${GCC} -I${INC} -I. -c %s_%s.c@." basename nodename; (* compiling main *)   
1241
  List.iter (fun s -> (* Format.eprintf "Adding dependency: %s@." s;  *)
1242
    fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
1243
    (("${INC}/io_frontend.c")::(List.map (fun s -> s ^ ".c") dependencies));    
1244
  fprintf fmt "\t${GCC} -Wno-attributes -o %s_%s_eacsl io_frontend.o %a %s -lm %s_eacsl.o %s_%s.o@." 
1245
    basename nodename 
1246
    (Utils.fprintf_list ~sep:" " (fun fmt s -> Format.fprintf fmt "%s.o" s)) dependencies 
1247
    ("${FRAMACEACSL}/e_acsl.c " 
1248
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c " 
1249
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
1250
    basename
1251
    basename nodename;
1252
  fprintf fmt "@.";
1253
  fprintf fmt "@.";
1254

    
1255
  fprintf fmt "clean:@.";
1256
  fprintf fmt "\t\\rm -f *.o %s_%s@." basename nodename
1257

    
1258

    
1259

    
1260

    
1261
(********************************************************************************************)
1262
(*                         Translation function                                             *)
1263
(********************************************************************************************)
1264

    
1265
let translate_to_c destname basename prog machines dependencies =
1266

    
1267
  let header_file = destname ^ ".h" in (* Could be changed *)
1268
  let header_out = open_out header_file in
1269
  let header_fmt = formatter_of_out_channel header_out in
1270

    
1271
  let source_file = destname ^ ".c" in (* Could be changed *)
1272
  let source_out = open_out source_file in
1273
  let source_fmt = formatter_of_out_channel source_out in
1274

    
1275
  let main_machine = Machine_code.get_machine_opt !Options.main_node machines in
1276

    
1277
  Log.report ~level:1 
1278
    (fun fmt -> fprintf fmt ".. opening files %s and %s@.@?" header_file source_file);
1279
  
1280
  (* Generating H file *)
1281

    
1282
  (* Include once: start *)
1283
  let baseNAME = String.uppercase basename in
1284
  let baseNAME = Str.global_replace (Str.regexp "\\.\\|\\ ") "_" baseNAME in
1285
  (* Print the svn version number and the supported C standard (C90 or C99) *)
1286
  print_version header_fmt;
1287
  fprintf header_fmt "#ifndef _%s@.#define _%s@." baseNAME baseNAME;
1288
  pp_print_newline header_fmt ();
1289
  fprintf header_fmt "/* Imports standard library */@.";
1290
  (* imports standard library definitions (arrow) *)
1291
  print_import_standard header_fmt;
1292
  pp_print_newline header_fmt ();
1293
  fprintf header_fmt "/* Types definitions */@.";
1294
  (* Print the type definitions from the type table *)
1295
  print_type_definitions header_fmt basename;
1296
  pp_print_newline header_fmt ();
1297
  (* Print the global constant declarations. *)
1298
  fprintf header_fmt "/* Global constant (declarations, definitions are in C file) */@.";
1299
  List.iter (fun c -> print_const_decl header_fmt c) (get_consts prog);
1300
  pp_print_newline header_fmt ();
1301
  (* Print the struct declarations of all machines. *)
1302
  fprintf header_fmt "/* Struct declarations */@.";
1303
  List.iter (print_machine_struct header_fmt) machines;
1304
  pp_print_newline header_fmt ();
1305
  (* Print the prototypes of all machines *)
1306
  fprintf header_fmt "/* Nodes declarations */@.";
1307
  List.iter (print_machine_decl header_fmt) machines;
1308
  pp_print_newline header_fmt ();
1309
  (* Include once: end *)
1310
  fprintf header_fmt "#endif@.";
1311
  pp_print_newline header_fmt ();
1312

    
1313
  (* Generating lib C file *)
1314
  fprintf source_fmt "#include <stdlib.h>@.#include <assert.h>@.#include \"%s\"@.@." (basename^".h");
1315
  (* Print the svn version number and the supported C standard (C90 or C99) *)
1316
  print_version source_fmt;
1317
  (* Print the prototype of imported nodes *)
1318
  fprintf source_fmt "/* Imported nodes declarations */@.";
1319
  fprintf source_fmt "@[<v>";
1320
  List.iter (print_prototype source_fmt) prog;
1321
  fprintf source_fmt "@]@.";
1322
  (* Print consts *)
1323
  fprintf source_fmt "/* Global constants (definitions) */@.";
1324
  List.iter (fun c -> print_const_def source_fmt c) (get_consts prog);
1325
  pp_print_newline source_fmt ();
1326
  (* Print nodes one by one (in the previous order) *)
1327
  List.iter (print_machine source_fmt) machines;
1328
  
1329
  (* If a main node is specified, generate additional files *)
1330
  match main_machine with 
1331
    None -> ()
1332
  | Some m -> (
1333

    
1334
    let makefile_file = destname ^ ".makefile" in (* Could be changed *)
1335
    let makefile_out = open_out makefile_file in
1336
    let makefile_fmt = formatter_of_out_channel makefile_out in
1337

    
1338
    let source_main_file = destname ^ "_" ^ m.mname.node_id ^ ".c" in (* Could be changed *)
1339
    let source_main_out = open_out source_main_file in
1340
    let source_main_fmt = formatter_of_out_channel source_main_out in
1341

    
1342
    Log.report ~level:1 
1343
      (fun fmt -> fprintf fmt ".. opening files %s and %s@.@?" 
1344
	header_file source_main_file);
1345
    
1346
    (* Generating main C file *)
1347
    
1348
    print_main_header source_main_fmt;
1349
    fprintf source_main_fmt "#include <stdlib.h>@.#include <assert.h>@.#include \"%s\"@.@." (basename^".h");
1350
    (* Print the svn version number and the supported C standard (C90 or C99) *)
1351
    print_version source_main_fmt;
1352
    print_main_fun machines m source_main_fmt;
1353

    
1354

    
1355
    (* Generating Makefile *)
1356

    
1357
    print_makefile basename !Options.main_node dependencies makefile_fmt
1358
  )
1359

    
1360
(* Local Variables: *)
1361
(* compile-command:"make -C .." *)
1362
(* End: *)