Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / c_backend.ml @ df647a81

History | View | Annotate | Download (75.9 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 "_Bool %s%a" var pp_suffix ()
212
  | Types.Treal           -> fprintf fmt "double %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 Machine_code.get_val_type (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 Machine_code.get_val_type (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
    | [] -> fprintf fmt "%a = %a;" (pp_value_suffix self loop_vars pp_var) var_name
348
      (pp_value_suffix self loop_vars pp_var) value
349
    | (d, LVar i) :: q ->
350
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
351
      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
352
	i i i Dimension.pp_dimension d i
353
	aux q
354
    | (d, LInt r) :: q ->
355
(*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
356
      let szl = Utils.enumerate (Dimension.size_const_dimension d) in
357
      fprintf fmt "@[<v 2>{@,%a@]@,}"
358
	(Utils.fprintf_list ~sep:"@," (fun fmt i -> r := i; aux fmt q)) szl
359
  in
360
  begin
361
    reset_loop_counter ();
362
    (*reset_addr_counter ();*)
363
    aux fmt reordered_loop_vars
364
  end
365

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

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

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

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

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

    
466

    
467
(**************************************************************************)
468
(*     Printing spec for c *)
469
(**************************************************************************)
470

    
471
let pp_ident is_output fmt id =
472
  if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
473

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

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

    
507
and pp_tuple is_output fmt el =
508
 Utils.fprintf_list ~sep:"," (pp_expr is_output) fmt el
509

    
510
and pp_handler is_output fmt (t, h) =
511
 fprintf fmt "(%s -> %a)" t (pp_expr is_output)  h
512

    
513
and pp_handlers is_output fmt hl =
514
 Utils.fprintf_list ~sep:" " (pp_handler is_output) fmt hl
515

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

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

    
562
(* Access to the value of a variable:
563
   - if it's not a scalar output, then its name is enough
564
   - otherwise, dereference it (it has been declared as a pointer,
565
     despite its scalar Lustre type)
566
   - moreover, cast arrays variables into their original array type.
567
*)
568
let pp_acsl_var_read outputs pre fmt id =
569
  if Types.is_array_type id.var_type
570
  then
571
    assert false (* no array *)
572
  else ( (* Hack to cast boolean variables as int for ACSL predicates *)
573
    (* This hack doesn't work because of int equality != bool equality and _Bool
574
        is supported now*)
575
    (*if (Types.repr id.var_type).Types.tdesc = Types.Tbool then
576
      fprintf fmt "(int)" 
577
    ;*)
578
    if List.exists (fun o -> o.var_id = id.var_id) outputs (* id is output *)
579
    then fprintf fmt "%s*%s" pre id.var_id
580
    else fprintf fmt "%s%s" pre id.var_id
581
  )
582

    
583
let rec pp_eexpr_logic_instr 
584
    ((node_id, inputs, outputs, locals, memory) as m) self fmt instr =
585
  match instr with 
586
  | MReset i -> assert false (* should not happen, calls were inlined *)
587
  | MLocalAssign (i,v) -> (
588
    match outputs with 
589
    | [o] -> if i = o then
590
	fprintf fmt "%a;" (pp_acsl_val self (pp_acsl_var_read outputs)) v
591
      else
592
	fprintf fmt "\\let %a = %a;" 
593
	  (pp_c_var_read outputs (* TODO no variable shold be treated as output *)) i
594
	  (pp_acsl_val self (pp_acsl_var_read outputs)) v
595

    
596
    | _ -> assert false (* should not happen: only a single output *)
597
)
598
  | MStateAssign (i,v) -> assert false (* should not happen, no side effects in logical predicates *)
599
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
600
    pp_eexpr_logic_instr m self fmt (MLocalAssign (i0, Fun (i, vl)))
601
  | MStep ([i0], "ite", vl) ->
602
    pp_eexpr_logic_instr m self fmt (MLocalAssign (i0, Fun ("ite", vl)))
603
  | MStep (il, i, vl) ->
604
    Format.eprintf "Illegal function call %s@.%a@.@?" i pp_instr instr; 
605
    assert false (* should not happen, calls were inlined *)
606
  | MBranch (g,hl) -> assert false (* should not happen. Oder ??? TODO *)
607

    
608

    
609
let pp_logic_eexpr node_id self fmt ee =
610
  fprintf fmt "%a%t%a"
611
    (Utils.fprintf_list ~sep:"@ " pp_quantifiers) ee.mquantifiers
612
    (Utils.pp_final_char_if_non_empty " " ee.mquantifiers) 
613
    (Utils.fprintf_list ~sep:"@;" 
614
       (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
615
    
616

    
617
let pp_acsl_spec_logics m outputs fmt spec = 
618
  let self = mk_self m in
619
  let pp_expr_def fmt ee =
620
    match ee.mmstep_logic.step_instrs with
621
    (*| [MStep([o], i, vl)] -> () (* We do nothing, the expression is simple and 
622
				   was introduced directly in the contract *) *)
623
    | _ -> ((* We define a new ACSL predicate *)
624
      fprintf fmt "/*@@ @[<v 3>predicate spec_%i(%a%t%a %s) =@;%a@]@;*/@." 
625
	ee.muid   
626
	(Utils.fprintf_list ~sep:", " pp_acsl_var_decl) ee.mmstep_logic.step_inputs
627
	(Utils.pp_final_char_if_non_empty ", " ee.mmstep_logic.step_inputs)
628
	pp_machine_memtype_name m.mname.node_id
629
	self
630
	(pp_logic_eexpr m.mname.node_id self) ee
631
    )
632

    
633
  in
634
  List.iter (pp_expr_def fmt) 
635
    (spec.m_requires@
636
       spec.m_ensures@
637
       (List.fold_left 
638
	  (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
639
	  [] spec.m_behaviors)
640
    )
641

    
642
let pp_requires_mem machines fmt m =
643
  let self = mk_self m in
644
  List.iter (fun v -> fprintf fmt "requires \\valid(%s);@;" v.var_id) m.mstep.step_outputs;
645
  fprintf fmt "requires \\valid(%s);@;" self;
646
  let mems = Machine_code.get_mems m machines in
647
  (*List.iter (fun prefix -> fprintf fmt "requires \\valid(%s%a);@;" self
648
    (Utils.fprintf_list ~sep:"" (fun fmt s -> fprintf fmt "->%s" s)) prefix
649
  )
650
    (Machine_code.get_instances m machines);*)
651
  if List.length mems + List.length m.mstep.step_outputs > 1 then
652
    fprintf fmt "requires \\separated(@[<hov>%a%t%s@]);@;" 
653
      (Utils.fprintf_list ~sep:",@ " 
654
	 (fun fmt v -> pp_print_string fmt v.var_id))
655
      m.mstep.step_outputs 
656
      (Utils.pp_final_char_if_non_empty ",@ " m.mstep.step_outputs)
657
      self
658

    
659
      (*(Utils.fprintf_list ~sep:",@ " 
660
	 (fun fmt (prefix, var) -> fprintf fmt "&%s%a->_reg.%s"
661
	   self 
662
	   (Utils.fprintf_list ~sep:"" (fun fmt s -> fprintf fmt "->%s" s)) prefix
663
	   var.var_id	 
664
	 ))
665
      mems*)
666

    
667
let pp_assigns machines fmt m =
668
  let self = mk_self m in
669
  let mems = Machine_code.get_mems m machines in
670
  fprintf fmt "assigns @[<hov>%a%t*%s@];@;" 
671
    (Utils.fprintf_list ~sep:",@ " 
672
       (fun fmt v -> fprintf fmt "*%s" v.var_id))
673
    m.mstep.step_outputs 
674
    (Utils.pp_final_char_if_non_empty ",@ " m.mstep.step_outputs)
675
    self
676
(*
677
    (Utils.fprintf_list ~sep:",@ " 
678
       (fun fmt (prefix, var) -> fprintf fmt "%s%a->_reg.%s"
679
	 self 
680
	 (Utils.fprintf_list ~sep:"" 
681
	    (fun fmt s -> fprintf fmt "->%s" s)) prefix
682
	 var.var_id	 
683
       ))
684
    mems*)
685

    
686
(*TODO: BEGIN*)
687

    
688
(* concat two lists and remove duplicates *)
689
let rec concat_uniq l1 l2 =
690
  match l1 with
691
    | [] -> l2
692
    | t::q -> let l = concat_uniq q l2 in
693
      if List.mem t l2 then l else t::l
694

    
695
(* A type for dependance, it can be a node or a variable *)
696
type dep_t = Dep_Var of string | Dep_Node of string
697

    
698
(* Take a machine and output the list of all dependance *)
699
let gen_dep instrs =
700
  let rec gen_dep_val = function
701
    | Cst c         -> []
702
    | Array vl      -> assert false
703
    | Access (t, i) -> assert false
704
    | Power (v, n)  -> assert false
705
    | LocalVar v    -> []
706
    | StateVar v    -> [Dep_Var v.var_id]
707
    | Fun (n, vl)   -> List.fold_left (fun l x-> concat_uniq (gen_dep_val x) l) [] vl
708
  and gen_dep_instr = function
709
    | MReset i -> assert false
710
    | MLocalAssign (i,v) -> gen_dep_val v
711
    | MStateAssign (i,v) -> concat_uniq (gen_dep_val (StateVar i)) (gen_dep_val v)
712
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> gen_dep_instr (MLocalAssign (i0, Fun (i, vl)))
713
    | MStep (il, i, vl) -> List.fold_left (fun l x-> concat_uniq (gen_dep_val x) l) [Dep_Node i] vl
714
    | MBranch (g,hl) -> List.fold_left (fun l (x, y)-> concat_uniq (gen_dep_instrs y) l) (gen_dep_val g) hl
715
  and gen_dep_instrs instrs =
716
    List.fold_left (fun l x-> concat_uniq (gen_dep_instr x) l) [] instrs
717
  in
718
  gen_dep_instrs instrs
719

    
720
(* Print a function call/declaration in acsl *) 
721
let pp_acsl_fun name fmt args =
722
    fprintf fmt "%s(@[<v>%a@])"
723
      name
724
      (Utils.fprintf_list ~sep:",@ " (fun fmt f-> f fmt)) args
725

    
726
(* Print an invariant call/decl in acsl *)
727
let pp_acsl_fun_init name self inst fmt mem =
728
  let arg = fun fmt-> (match inst, mem with
729
    | x,  None    -> fprintf fmt "%a %s" pp_machine_memtype_name name self
730
    | "", Some "" -> fprintf fmt "%s" self
731
    | "", Some m  -> fprintf fmt "\\at(*%s, %s)" self m
732
    | x,  Some "" -> fprintf fmt "%s.%s" self inst
733
    | x,  Some m  -> fprintf fmt "\\at(%s->%s, %s)" self inst m)
734
  in
735
  pp_acsl_fun ("init_"^name) fmt [arg]
736

    
737

    
738
(* Print a machine instruction in acsl for transition lemma *) 
739
let preprocess_acsl_instr instances outputs instr =
740
  match instr with 
741
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i && (not (List.mem i0 outputs)) ->
742
      Some (i0, Fun (i, vl))
743
    | MStep ([i0], i, vl) when (not (Basic_library.is_internal_fun i)) && node_name (fst (List.assoc i instances)) = "_arrow" ->
744
      assert (List.length vl == 2);
745
      Some (i0, Fun ("arrow_"^i, vl))
746
    | MLocalAssign (i,v) when not (List.mem i outputs) ->
747
      Some (i, v)
748
    | _ -> None
749

    
750

    
751
let pp_cast fmt = function
752
  | Types.Tbool           -> fprintf fmt "(_Bool)"
753
  | Types.Treal           -> fprintf fmt "(double)"
754
  | Types.Tint            -> fprintf fmt "(int)"
755
  | _ -> assert false
756

    
757
let getFunType i args =
758
  match i, args with
759
  | "ite", [v1; v2; v3] -> v2
760
  | "uminus", [v] -> v
761
  | "not", [v] -> v
762
  | "impl", [v1; v2] -> v1
763
  | "=", [v1; v2] -> Types.Tbool
764
  | "mod", [v1; v2] -> v1
765
  | "xor", [v1; v2] -> v1
766
  | _, [v1; v2] -> v1
767
  | _ -> assert false
768

    
769
let rec get_val_type v =
770
match v with 
771
| Cst _
772
| LocalVar _ 
773
| StateVar _-> Machine_code.get_val_type v
774
| Fun (n, vl) -> getFunType n (List.map get_val_type vl)
775
| Array _
776
| Access _
777
| Power _ -> assert false
778

    
779
let get_var_type t = (Types.repr t.var_type).Types.tdesc
780

    
781
(* Print a machine instruction in acsl for transition lemma *) 
782
let rec pp_acsl_instr vars instances self pointer fmt instr =
783
  match instr with 
784
    | MReset i ->
785
      let (node, static) = List.assoc i instances in
786
      assert (List.length static == 0);
787
      if node_name node = "_arrow" then
788
        fprintf fmt "%s.%s._reg._first==1" self i
789
      else
790
        pp_acsl_fun_init (node_name node) self i fmt (Some "")
791
    | MLocalAssign (i,v) -> fprintf fmt "%a == %a"
792
      (pp_acsl_var_read pointer "") i
793
      (pp_acsl_val (self^"1") (pp_acsl_var_read pointer)) v
794
    | MStateAssign (i,v) -> fprintf fmt "%a == %a"
795
      (pp_acsl_val (self^"2") (pp_acsl_var_read pointer)) (StateVar i)
796
      (pp_acsl_val (self^"1") (pp_acsl_var_read pointer)) v
797
    | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
798
      pp_acsl_instr vars instances self pointer fmt (MLocalAssign (i0, Fun (i, vl)))
799
    | MStep (il, i, vl) ->
800
      let pp_val fmt x = (match get_val_type x with Types.Tbool -> fprintf fmt "((%a)?1:0)" | _ -> fprintf fmt "%a") (pp_acsl_val (self^"1") (pp_acsl_var_read [])) x in
801
      pp_acsl_fun ("Ctrans_"^(node_name (fst (List.assoc i instances)))) fmt
802
      ((List.map (fun x fmt-> fprintf fmt "%a %a" pp_cast (get_val_type x) pp_val x) vl)@
803
      (List.map (fun x fmt-> fprintf fmt "%a" (*pp_cast (get_var_type x)*) (pp_acsl_var_read [] "") x) il)@
804
        [(fun fmt->fprintf fmt "%s1.%s" self i);(fun fmt->fprintf fmt "%s2.%s" self i)])
805
    | MBranch (g,hl) ->
806
      let t = fst (List.hd hl) in
807
      if hl <> [] && (t = tag_true || t = tag_false) then
808
        let tl = try List.assoc tag_true  hl with Not_found -> [] in
809
        let el = try List.assoc tag_false hl with Not_found -> [] in
810
        fprintf fmt "(%a)?(%a):(%a)"
811
          (pp_acsl_val self (pp_acsl_var_read pointer)) g
812
          (Utils.fprintf_list ~sep:"&& " (pp_acsl_instr vars instances self pointer)) tl
813
          (Utils.fprintf_list ~sep:"&& " (pp_acsl_instr vars instances self pointer)) el
814
      else assert false
815

    
816
(* Print all machine instructions in acsl for transition lemma *) 
817
let pp_acsl_instrs outputs self pointer instances vars fmt instrs =
818
  if List.length instrs == 0 then fprintf fmt "\\true" else
819
  let handle (locals, instrs) i =
820
    match preprocess_acsl_instr instances outputs i with
821
      | None    -> (locals, i::instrs)
822
      | Some l  -> (l::locals, instrs)
823
  in
824
  let pp_let fmt (i, v) =
825
    match v with
826
      | Fun (s, [x;y]) when String.length s >= 6 && String.sub s 0 6 = "arrow_" ->
827
        let var = String.sub s 6 (String.length s - 6) in
828
        fprintf fmt "\\let %a = %s1.%s._reg._first?%a:%a; (%s2.%s._reg._first==0) &&"
829
          (pp_acsl_var_read pointer "") i
830
          self var
831
          (pp_acsl_val (self^"1") (pp_acsl_var_read [])) x
832
          (pp_acsl_val (self^"1") (pp_acsl_var_read [])) y
833
          self var
834
      | _ ->
835
        fprintf fmt "\\let %a = %a;"
836
          (pp_acsl_var_read pointer "") i
837
          (pp_acsl_val (self^"1") (pp_acsl_var_read pointer)) v
838
  in
839
  let (locals, instrs) = List.fold_left handle ([], []) instrs in
840
  fprintf fmt "%a@,%a"
841
    (Utils.fprintf_list ~sep:"@," pp_let)
842
    (List.rev locals)
843
    (Utils.fprintf_list ~sep:" &&@," (pp_acsl_instr vars instances self pointer))
844
    instrs
845

    
846
(* Take a dependance and print it for invariant predicate *)
847
(*
848
let pp_acsl_dep self instances fmt = function
849
  | Dep_Var s -> fprintf fmt "%s2._reg.%s == %s1._reg.%s" self s self s
850
  | Dep_Node s ->
851
    pp_acsl_fun ("inv_"^(node_name (fst (List.assoc s instances)))) fmt [fun fmt->fprintf fmt "%s1.%s" self i];
852
    fprintf fmt "&&@, %t == %t" (pp_acsl_at self s)
853
      (pp_acsl_at self s)
854
*)
855

    
856
(* Print a transition call/decl in acsl *)
857
let pp_acsl_fun_trans infos pre name inputs outputs suffix flag_output self flag_mem locals fmt existential =
858
  let (locals, existential) = (*([], match existential with None -> None | Some x -> Some []) in*)
859
  match infos with
860
    | None -> (locals, existential)
861
    | Some (instrs, instances) ->
862
      let nonlocals = List.fold_left (fun l x-> match preprocess_acsl_instr instances outputs x with | Some (i, _) -> i::l | None -> l) [] instrs in
863
      (
864
        List.filter (fun x-> not (List.mem x nonlocals)) locals,
865
        match existential with None -> None | Some existential -> Some (List.filter (fun x-> not (List.mem x nonlocals)) existential)
866
      )
867
  in
868
  let mems = function 1 -> "Pre" | 2 -> "Here" | _ -> assert false in
869
  let pp_self_read =
870
    if flag_mem then fun i fmt-> fprintf fmt "\\at(*%s, %s)" self (mems i)
871
    else fun i fmt-> fprintf fmt "%s%i" self (match suffix with None -> i | Some s -> s+i-1)
872
  in
873
  let (pp_var, pp_self) =
874
    match existential with
875
      | None    -> (pp_acsl_var_decl, (fun i fmt-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i))
876
      | Some ex -> (if List.length ex != 0 then fprintf fmt "\\exists %a;@," (Utils.fprintf_list ~sep:";@,\\exists " pp_acsl_var_decl) ex);
877
                   (pp_acsl_var_read (if flag_output then outputs else []) "", pp_self_read)
878
  in
879
  let pp_vars = List.map (fun x fmt-> match suffix with None-> pp_var fmt x | Some i -> fprintf fmt "%a%i" pp_var x (i+1)) in
880
    (pp_acsl_fun (pre^"trans_"^name)) fmt
881
    ((pp_vars (inputs@outputs))@[pp_self 1;pp_self 2]@(pp_vars locals))
882

    
883
let depth = 1
884

    
885
(* Print an invariant call/decl in acsl *)
886
let pp_acsl_fun_inv name self fmt mem =
887
  let arg = fun fmt-> (match mem with
888
    | None -> fprintf fmt "%a %s%i" pp_machine_memtype_name name self depth
889
    | Some "" -> fprintf fmt "%s" self
890
    | Some "Here" -> fprintf fmt "*%s" self
891
    | Some m -> fprintf fmt "\\at(*%s, %s)" self m)
892
  in
893
  pp_acsl_fun ("inv_"^name) fmt [arg]
894

    
895
(* Print an invariant call/decl in acsl *)
896
let pp_acsl_inv name inputs outputs self fmt spec =
897
  let rec iter base x = function
898
    | i when i = base-1 -> []
899
    | i -> (i, x)::(iter base x (i-1))
900
  in
901
  let rec iterList base = function
902
    | []   -> []
903
    | t::q -> (iter base t depth)@(iterList base q)
904
  in
905
  let trans_pred fmt i =
906
    fprintf fmt "%a" (pp_acsl_fun_trans  None "C" name inputs outputs (Some i) false self false []) (Some [])
907
  in
908
  let spec_pred fmt i =
909
    let pp_eexpr_expr self j fmt ee = 
910
      fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (fun fmt x-> fprintf fmt "%a%i" (pp_acsl_var_read [] "") x i)) ee.mmstep_logic.step_inputs self j
911
    in
912
    fprintf fmt "%a%t%a"
913
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self (i))) spec.m_requires
914
    (Utils.pp_final_char_if_non_empty "&&@," spec.m_requires)
915
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self (i))) spec.m_ensures
916
  in
917
  let aux fmt base =
918
    let selfs = iter base self (depth-1) in
919
    let ios = iterList (if base == 0 then 0 else base + 1) (inputs@outputs) in
920
    (if List.length selfs == 0 && List.length ios == 0 then 
921
      fprintf fmt "(%a%t%t)"
922
     else
923
      fprintf fmt "(\\exists %a%t%a;@,%a%t%t)"
924
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a %s%i" pp_machine_memtype_name name self i)) selfs
925
        (Utils.pp_final_char_if_non_empty ", " (iter base self (depth-1)))
926
        (Utils.fprintf_list ~sep:", "   (fun fmt (i, x)-> fprintf fmt "%a%i" pp_acsl_var_decl x i)) ios
927
    )
928
      (Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i)) (iter base trans_pred (depth-1))
929
      (Utils.pp_final_char_if_non_empty "&&@," (iter base trans_pred (depth-1))) 
930
      (fun fmt->
931
        if base == 0 then
932
          Utils.fprintf_list ~sep:"&&@," (fun fmt (i, f)-> fprintf fmt "%a" f i) fmt (iter base spec_pred depth)
933
        else
934
          pp_acsl_fun_init name (self^(string_of_int base)) "" fmt (Some "")
935
      )
936
  in
937
  Utils.fprintf_list ~sep:"||@," (fun fmt (i, f)-> fprintf fmt "%a" f i) fmt (iter 0 aux depth)
938

    
939
(* Print an invariant call/decl in acsl *)
940
let pp_acsl_lem_inv name inputs outputs fmt self =
941
  fprintf fmt "\\forall %a %s1, %s2, %a;@,%a==>@,%a==>@,%a"
942
    pp_machine_memtype_name name self self
943
    (Utils.fprintf_list ~sep:", " pp_acsl_var_decl) (inputs@outputs)
944
    (pp_acsl_fun_inv name (self^"1")) (Some "")
945
    (pp_acsl_fun_trans None "C" name inputs outputs None false self false []) (Some [])
946
    (pp_acsl_fun_inv name (self^"2")) (Some "")
947

    
948
(* Print an invariant call/decl in acsl *)
949
let pp_acsl_lem_spec name inputs outputs self fmt spec =
950
  let pp_eexpr_expr self j fmt ee =
951
    fprintf fmt "spec_%i(%a, %s%i)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) ee.mmstep_logic.step_inputs self j
952
  in
953
  fprintf fmt "\\forall %a %s1, %s2, %a;@,%a==>@,%a==>@,%a%t%a"
954
    pp_machine_memtype_name name self self
955
    (Utils.fprintf_list ~sep:", " pp_acsl_var_decl) (inputs@outputs)
956
    (pp_acsl_fun_inv name (self^"1")) (Some "")
957
    (pp_acsl_fun_trans None "C" name inputs outputs None false self false []) (Some [])
958
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self 1)) spec.m_requires
959
    (Utils.pp_final_char_if_non_empty "&&@," spec.m_requires)
960
    (Utils.fprintf_list ~sep:"&&@," (pp_eexpr_expr self 2)) spec.m_ensures
961

    
962
(* Print the definition of the transition in acsl *)
963
let pp_acsl_def_trans fmt m =
964
  let name = m.mname.node_id in
965
  let inputs = m.mstep.step_inputs in
966
  let outputs = m.mstep.step_outputs in
967
  let locals = m.mstep.step_locals in
968
  let memory = m.mmemory in
969
  let vars = inputs@outputs@locals@memory in
970
  if m.mname.node_id <> arrow_id then (
971
    let self = mk_self m in
972
    fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
973
      (pp_acsl_fun_trans (Some (m.mstep.step_instrs, m.minstances)) "" name inputs outputs None false self false locals) None
974
	    (pp_acsl_instrs outputs self [] m.minstances vars) m.mstep.step_instrs;
975
    fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
976
      (pp_acsl_fun_init name self "") None
977
	    (pp_acsl_instrs [] self [] m.minstances vars) m.minit;
978
    fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
979
      (pp_acsl_fun_trans None "C" name inputs outputs None false self false []) None
980
	    (pp_acsl_fun_trans (Some (m.mstep.step_instrs, m.minstances)) "" name inputs outputs None false self false locals) (Some locals);
981
    match m.mspec with None -> () | Some spec -> fprintf fmt "/*@@ @[<v 3>predicate %a =@;%a;@]@;*/@."
982
      (pp_acsl_fun_inv name self) None (pp_acsl_inv name inputs outputs self) spec;
983
    fprintf fmt "/*@@ @[<v 3>lemma inv_spec_%s : @;%a;@]@;*/@." name (pp_acsl_lem_spec name inputs outputs self) spec;
984
    fprintf fmt "/*@@ @[<v 3>lemma inv_inv_%s : @;%a;@]@;*/@." name (pp_acsl_lem_inv name inputs outputs) self
985
  )
986

    
987
(*;
988
  fprintf fmt "/*@@ @[<v 3>predicate inv_%s{L1, L2}(@[<v>@[%a *%s@]@]) =@;%a;@]@;*/@."
989
    m.mname.node_id
990
	  pp_machine_memtype_name m.mname.node_id
991
	  self
992
    (Utils.fprintf_list ~sep:" &&@," (printDep self "L1" "L2" m.minstances)) (gen_dep m.mstep.step_instrs);
993
  fprintf fmt "/*@@ @[<v 3>lemma transitivity_%s{L1, L2, L3, L4} :@, \forall @[<v>@[%a%t@]@,@[%a@]%t@[%a *%s@]@];@, %t;@]@;*/@."
994
    m.mname.node_id
995
    (Utils.fprintf_list ~sep:",@ " pp_acsl_var_decl) m.mstep.step_inputs
996
    (Utils.pp_final_char_if_non_empty ",@ " m.mstep.step_inputs) 
997
    (Utils.fprintf_list ~sep:",@ " pp_acsl_var_decl) m.mstep.step_outputs
998
    (Utils.pp_final_char_if_non_empty ",@," m.mstep.step_outputs)
999
	pp_machine_memtype_name m.mname.node_id
1000
	self
1001
  (fun fmt->
1002
    fprintf fmt "inv_%s{L1, L2}(%s) ==>@," m.mname.node_id self;
1003
    fprintf fmt "inv_%s{L3, L4}(%s) ==>@," m.mname.node_id self;
1004
    fprintf fmt "trans_%s{L2, L3}(%a%t%a%t\\at(%s, L2)) ==>@,"
1005
      m.mname.node_id
1006
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) m.mstep.step_inputs
1007
      (Utils.pp_final_char_if_non_empty ", " m.mstep.step_inputs) 
1008
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) m.mstep.step_outputs
1009
      (Utils.pp_final_char_if_non_empty ", " m.mstep.step_outputs)
1010
      self;
1011
    fprintf fmt "trans_%s{L1, L4}(%a%t%a%t\\at(%s, L1)@]@])"
1012
      m.mname.node_id
1013
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) m.mstep.step_inputs
1014
      (Utils.pp_final_char_if_non_empty ", " m.mstep.step_inputs) 
1015
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read [] "")) m.mstep.step_outputs
1016
      (Utils.pp_final_char_if_non_empty ", " m.mstep.step_outputs)
1017
      self)
1018
*)
1019

    
1020
(*
1021
    (print_reset_prototype self) (m.mname.node_id, m.mstatic)
1022
    (Utils.fprintf_list ~sep:"@," 
1023
       (pp_machine_instr 
1024
	  (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, m.mstep.step_locals, m.mmemory, m.minstances, m.mcalls) self)) 
1025
    m.minit
1026
    (Utils.pp_newline_if_non_empty m.minit)
1027
    (* Print specification if any: insert side effect at the end of the function body  *)
1028
    (fun fmt -> match m.mspec with
1029
    | None -> ()
1030
    | Some spec -> pp_acsl_spec_init_side_effects m m.mstep.step_outputs fmt spec
1031
    )*)
1032

    
1033
(*TODO: END*)
1034

    
1035
let pp_acsl_mem_valid machines fmt m =
1036
  let self = mk_self m in
1037
  fprintf fmt "@[<v 2>/*@@ ";
1038
  pp_requires_mem machines fmt m;
1039
	fprintf fmt "ensures %a;@," (pp_acsl_fun_trans None "C" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true self true []) (Some []);
1040
  pp_assigns machines fmt m;
1041
  fprintf fmt "@]*/@.";
1042
  ()
1043

    
1044
let pp_acsl_spec_contracts machines m outputs fmt spec = 
1045
  let self = mk_self m in
1046
    (* let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in *)
1047
  let pp_eexpr_expr fmt ee = 
1048
      (* If the eexpr contains a single definition we use it directly. Otherwise,
1049
	 we rely on an external predicate *)
1050
    match ee.mmstep_logic.step_instrs with
1051
    (*| [MStep([o], i, vl)] -> 
1052
      fprintf fmt "%a %t"
1053
	(Utils.fprintf_list ~sep:" " pp_quantifiers) ee.mquantifiers
1054
	(fun fmt ->
1055
	  let value = Fun (i, vl) in
1056
	  let vars : var_decl list = 
1057
	    ee.mmstep_logic.step_inputs@ee.mmstep_logic.step_outputs@ee.mmstep_logic.step_locals@ee.mmmemory 
1058
	  in 
1059
	  pp_expr_rhs vars self (pp_c_var_read outputs) fmt o.var_type value 
1060
	)*)
1061
    | _ -> fprintf fmt "spec_%i(%a, *%s);" 
1062
      ee.muid   
1063
      (Utils.fprintf_list ~sep:", " (pp_acsl_var_read outputs "")) ee.mmstep_logic.step_inputs
1064
      self
1065
  in
1066
  fprintf fmt "@[<v 2>/*@@ ";
1067
  (* Valid pointers *)
1068
  pp_requires_mem machines fmt m;
1069
  (* Spec requires *)
1070
  Utils.fprintf_list ~sep:"" 
1071
    (fun fmt r -> fprintf fmt "requires %a@ " pp_eexpr_expr r) 
1072
    fmt 
1073
    spec.m_requires;
1074
  fprintf fmt "requires %a;@," (pp_acsl_fun_inv m.mname.node_id self) (Some "Here");
1075
  Utils.fprintf_list ~sep:"" 
1076
    (fun fmt r -> fprintf fmt "ensures %a@ " pp_eexpr_expr r) 
1077
    fmt 
1078
    spec.m_ensures;
1079
  fprintf fmt "ensures %a;@," (pp_acsl_fun_inv m.mname.node_id self) (Some "Here");
1080
	fprintf fmt "ensures %a;@," (pp_acsl_fun_trans None "C" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true self true []) (Some []);
1081
  fprintf fmt "@ ";
1082
    (* TODO assigns + separated *)
1083
    (* fprintf fmt "assigns *self%t%a;@ "  *)
1084
    (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
1085
    (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
1086
    Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, ensures) -> 
1087
      fprintf fmt "behavior %s:@[@ %a@ %a@]" 
1088
	name
1089
	(Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a" pp_eexpr_expr r)) assumes
1090
	(Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a" pp_eexpr_expr r)) ensures
1091
    ) fmt spec.m_behaviors;
1092
    (* Assings *)
1093
    pp_assigns machines fmt m;
1094
    fprintf fmt "@]@ */@.";
1095
    ()
1096

    
1097
let pp_acsl_spec_side_effects m outputs fmt spec = 
1098
  let self = mk_self m in
1099
  let pp_side_effects fmt ee =  
1100
    (* Declare local vars *)
1101
    let locals = List.filter (fun l -> not (List.mem l m.mstep.step_locals)) ee.mmstep_effects.step_locals in
1102
    (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) fmt locals;
1103
    Utils.pp_final_char_if_non_empty ";@," locals fmt ;
1104
      
1105
    (* Print instructions *)
1106
    Utils.fprintf_list ~sep:"@;" 
1107
      (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)
1108
      fmt 
1109
      ee.mmstep_effects.step_instrs
1110
in
1111
  let effects = spec.m_requires@spec.m_ensures@
1112
    (List.fold_left 
1113
       (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
1114
	  [] spec.m_behaviors)
1115
  in
1116
  let effects = List.filter (fun ee -> ee.mmstep_effects.step_instrs <> []) effects in
1117
  let all_instrs = List.flatten (List.map (fun e -> e.mmstep_effects.step_instrs) effects) in
1118
  if all_instrs <> [] then (
1119
    fprintf fmt "// Begin of specification memory update block@;";
1120
    if !Options.ghost_mode then
1121
      fprintf fmt "@[<v 3>/*@@ ghost %a@]@;*/@;" 
1122
	(Utils.fprintf_list ~sep:"@;" pp_side_effects)
1123
	effects
1124
    else (
1125
      Utils.fprintf_list ~sep:"@;" pp_side_effects fmt effects;
1126
      fprintf fmt "@;"
1127
    )
1128
    ;
1129
    fprintf fmt "// End of specification memory update block@."
1130
  )
1131

    
1132
let pp_acsl_spec_init_side_effects m outputs fmt spec = 
1133
  let self = mk_self m in
1134
  
1135
  let pp_side_effects fmt ee =  
1136
    (* Print instructions *)
1137
    Utils.fprintf_list ~sep:"@;" 
1138
      (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)
1139
      fmt 
1140
      ee.mminit
1141
  in
1142
  
1143
  let effects = spec.m_requires@spec.m_ensures@
1144
    (List.fold_left 
1145
       (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
1146
       [] spec.m_behaviors)
1147
  in
1148
  
1149
  let effects = List.filter (fun ee -> ee.mminit <> []) effects in
1150
  let all_instrs = List.flatten (List.map (fun e -> e.mminit) effects) in
1151
  if all_instrs <> [] then (
1152
    fprintf fmt "// Begin of specification memory init block@;";
1153
    if !Options.ghost_mode then
1154
      fprintf fmt "@[<v 3>/*@@ ghost %a@]@;*/@;" 
1155
	(Utils.fprintf_list ~sep:"@;" pp_side_effects)
1156
	effects
1157
    else (
1158
      Utils.fprintf_list ~sep:"@;" pp_side_effects fmt effects;
1159
      fprintf fmt "@;"
1160
    )
1161
    ;
1162
    fprintf fmt "// End of specification memory init block@."
1163
  )
1164

    
1165

    
1166
(********************************************************************************************)
1167
(*                      Prototype Printing functions                                        *)
1168
(********************************************************************************************)
1169

    
1170
let print_alloc_prototype fmt (name, static) =
1171
  fprintf fmt "%a * %a (%a)"
1172
    pp_machine_memtype_name name
1173
    pp_machine_alloc_name name
1174
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static
1175

    
1176
let print_reset_prototype self fmt (name, static) =
1177
  fprintf fmt "void %a (@[<v>%a%t%a *%s@])"
1178
    pp_machine_reset_name name
1179
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static
1180
    (Utils.pp_final_char_if_non_empty ",@," static) 
1181
    pp_machine_memtype_name name
1182
    self
1183

    
1184
let print_stateless_prototype fmt (name, inputs, outputs) =
1185
match outputs with
1186
(* DOESN'T WORK FOR ARRAYS
1187
  | [o] -> fprintf fmt "%a (@[<v>%a@])"
1188
    (pp_c_type name) o.var_type
1189
    (Utils.fprintf_list ~sep:",@ " pp_c_var) inputs
1190
*)  
1191
  | _ -> fprintf fmt "void %s (@[<v>@[%a%t@]@,@[%a@]@,@])"
1192
    name
1193
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs
1194
    (Utils.pp_final_char_if_non_empty ",@ " inputs) 
1195
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_output_var) outputs
1196

    
1197
let print_step_prototype self fmt (name, inputs, outputs) =
1198
  fprintf fmt "void %a (@[<v>@[%a%t@]@,@[%a@]%t@[%a *%s@]@])"
1199
    pp_machine_step_name name
1200
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs
1201
    (Utils.pp_final_char_if_non_empty ",@ " inputs) 
1202
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_output_var) outputs
1203
    (Utils.pp_final_char_if_non_empty ",@," outputs) 
1204
    pp_machine_memtype_name name
1205
    self
1206

    
1207
(********************************************************************************************)
1208
(*                         Header Printing functions                                        *)
1209
(********************************************************************************************)
1210

    
1211
(* Removed because of "open" constructs. No more extern functions *)
1212
(*
1213
let print_prototype fmt decl =
1214
  match decl.top_decl_desc with
1215
    | ImportedFun m -> (
1216
        fprintf fmt "extern %a;@,"
1217
	  print_stateless_prototype 
1218
	  (m.fun_id, m.fun_inputs, m.fun_outputs)
1219
    )
1220
    | ImportedNode m -> (
1221
      if m.nodei_stateless then (* It's a function not a node *)
1222
        fprintf fmt "extern %a;@,"
1223
	  print_stateless_prototype 
1224
	  (m.nodei_id, m.nodei_inputs, m.nodei_outputs)
1225
      else (
1226
	let static = List.filter (fun v -> v.var_dec_const) m.nodei_inputs in
1227
        fprintf fmt "extern %a;@,"
1228
	  print_alloc_prototype (m.nodei_id, static);
1229
	fprintf fmt "extern %a;@,"
1230
	  (print_reset_prototype "self") (m.nodei_id, static);
1231
	fprintf fmt "extern %a;@,"
1232
	  (print_step_prototype "self") (m.nodei_id, m.nodei_inputs, m.nodei_outputs);
1233
      )
1234
    )
1235
    | _ -> () (* We don't do anything here *)
1236
      *)
1237

    
1238
let print_import_standard fmt =
1239
  fprintf fmt "#include \"%s/include/lustrec/arrow.h\"@.@." Version.prefix
1240

    
1241
let print_prototype fmt decl =
1242
  match decl.top_decl_desc with
1243
  | Open m -> fprintf fmt "#include \"%s.h\"@," m
1244
  | _ -> () (* We don't do anything here *)
1245

    
1246
(* TODO: what to do when the _reg struct only contains ghost code ? It is
1247
   considered as empty for gcc. Is this a problem? *)
1248
let pp_registers_struct fmt m =
1249
  let spec_memories = match m.mspec with
1250
      None -> []
1251
    | Some s -> List.flatten (
1252
      List.map (fun ee -> ee.mmmemory) 
1253
	(s.m_requires@
1254
	   s.m_ensures@
1255
	   (List.fold_left 
1256
	      (fun accu (_,assumes, ensures) -> assumes@ensures@accu) 
1257
	      [] s.m_behaviors)
1258
	))
1259
  in
1260
  if m.mmemory <> [] || spec_memories <> [] 
1261
  then
1262
    fprintf fmt "@[%a {@[<v>%a%a@]}@] _reg; "
1263
      pp_machine_regtype_name m.mname.node_id
1264
      (Utils.fprintf_list ~sep:"@;" pp_c_decl_struct_var) m.mmemory
1265
      (Utils.fprintf_list ~sep:"@;" pp_c_decl_struct_spec_var) spec_memories
1266
      
1267
      
1268
  else (* TODO : remove this hack. This is to avoid silly frama-c errors *)
1269
    fprintf fmt "@[%a {@[<v>int dummy;@]}@] _reg; "
1270
      pp_machine_regtype_name m.mname.node_id;
1271
  ()
1272

    
1273
let print_machine_struct fmt m =
1274
  if m.mname.node_id != arrow_id
1275
  then (
1276
    (* We don't print arrow function *)
1277
    (* Define struct *)
1278
    fprintf fmt "@[%a {@[%a%a%t@]};@]@."
1279
      pp_machine_memtype_name m.mname.node_id
1280
      pp_registers_struct m
1281
      (Utils.fprintf_list ~sep:"; " pp_c_decl_instance_var) m.minstances
1282
      (Utils.pp_final_char_if_non_empty "; " m.minstances)
1283
  )
1284

    
1285
(*
1286
let pp_static_array_instance fmt m (v, m) =
1287
 fprintf fmt "%s" (mk_addr_var m v)
1288
*)
1289
let print_static_declare_instance attr fmt (i, (m, static)) =
1290
  fprintf fmt "%a(%s, %a%t%s)"
1291
    pp_machine_static_declare_name (node_name m)
1292
    attr
1293
    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
1294
    (Utils.pp_final_char_if_non_empty ", " static)
1295
    i
1296

    
1297
let print_static_declare_macro fmt m =
1298
  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
1299
  let inst = mk_instance m in
1300
  let attr = mk_attribute m in
1301
  fprintf fmt "@[<v 2>#define %a(%s, %a%t%s)\\@,%s %a %s;\\@,%a%t%a;@,@]"
1302
    pp_machine_static_declare_name m.mname.node_id
1303
    attr
1304
    (Utils.fprintf_list ~sep:", " (pp_c_var_read m.mstep.step_outputs)) m.mstatic
1305
    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
1306
    inst
1307
    attr
1308
    pp_machine_memtype_name m.mname.node_id
1309
    inst
1310
    (Utils.fprintf_list ~sep:";\\@," pp_c_decl_local_var) array_mem
1311
    (Utils.pp_final_char_if_non_empty ";\\@," array_mem)
1312
    (Utils.fprintf_list ~sep:";\\@,"
1313
       (fun fmt (i',m') ->
1314
	 let path = sprintf "inst ## _%s" i' in
1315
	 fprintf fmt "%a"
1316
	   (print_static_declare_instance attr) (path,m')
1317
       )) m.minstances
1318

    
1319
      
1320
let print_static_link_instance fmt (i, (m, _)) =
1321
 fprintf fmt "%a(%s)" pp_machine_static_link_name (node_name m) i
1322

    
1323
let print_static_link_macro fmt m =
1324
  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
1325
  fprintf fmt "@[<v>@[<v 2>#define %a(inst) do {\\@,%a%t%a;\\@]@,} while (0)@.@]"
1326
    pp_machine_static_link_name m.mname.node_id
1327
    (Utils.fprintf_list ~sep:";\\@,"
1328
       (fun fmt v ->
1329
	 fprintf fmt "inst.%s = &%s"
1330
	   v.var_id
1331
	   v.var_id
1332
       )) array_mem
1333
    (Utils.pp_final_char_if_non_empty ";\\@," array_mem)
1334
    (Utils.fprintf_list ~sep:";\\@,"
1335
       (fun fmt (i',m') ->
1336
	 let path = sprintf "inst ## _%s" i' in
1337
	 fprintf fmt "%a;\\@,inst.%s = &%s"
1338
	   print_static_link_instance (path,m')
1339
	   i'
1340
	   path
1341
       )) m.minstances
1342
      
1343
let print_static_alloc_macro fmt m =
1344
  fprintf fmt "@[<v>@[<v 2>#define %a(attr,%a%tinst)\\@,%a(attr,%a%tinst);\\@,%a(inst);@]@,@]@."
1345
    pp_machine_static_alloc_name m.mname.node_id
1346
    (Utils.fprintf_list ~sep:", " (pp_c_var_read m.mstep.step_outputs)) m.mstatic
1347
    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
1348
    pp_machine_static_declare_name m.mname.node_id
1349
    (Utils.fprintf_list ~sep:", " (pp_c_var_read m.mstep.step_outputs)) m.mstatic
1350
    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
1351
    pp_machine_static_link_name m.mname.node_id
1352

    
1353
let print_machine_spec machines fmt m =
1354
  if m.mname.node_id <> arrow_id then 
1355
    (
1356
      (* We don't print arrow function *)
1357

    
1358
      (* Print specification if any: insert logic definition before the function  *)
1359
      match m.mspec with
1360
      | None -> ()
1361
      | Some spec -> 
1362
	pp_acsl_spec_logics m m.mstep.step_outputs fmt spec
1363
    )
1364

    
1365
let print_machine_decl machines fmt m =
1366
  if m.mname.node_id <> arrow_id then 
1367
    (
1368
   (*   (* We don't print arrow function *)
1369

    
1370
      (* Static allocation *)
1371
      if !Options.static_mem
1372
      then (
1373
	fprintf fmt "%a@.%a@.%a@."
1374
	  print_static_declare_macro m
1375
	  print_static_link_macro m
1376
	  print_static_alloc_macro m
1377
      )
1378
      else ( 
1379
      (* Dynamic allocation *)
1380
	fprintf fmt "extern %a;@.@."
1381
	  print_alloc_prototype (m.mname.node_id, m.mstatic)
1382
      );*)
1383
      let self = mk_self m in
1384
	    fprintf fmt "/*@@ensures %a;@." (pp_acsl_fun_init m.mname.node_id self "") (Some "Here");
1385
	    fprintf fmt "assigns *%s;*/@." self;
1386
      fprintf fmt "extern %a;@.@."
1387
	(print_reset_prototype self) (m.mname.node_id, m.mstatic);
1388
    (* Print specification contracts if any *)
1389
      (match m.mspec with
1390
      | None -> pp_acsl_mem_valid machines fmt m
1391
      | Some spec -> pp_acsl_spec_contracts machines m m.mstep.step_outputs fmt spec
1392
      );
1393
      fprintf fmt "extern %a;@.@."
1394
	(print_step_prototype self)
1395
	(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
1396
    )
1397

    
1398

    
1399
(********************************************************************************************)
1400
(*                         C file Printing functions                                        *)
1401
(********************************************************************************************)
1402

    
1403
let print_const_def fmt cdecl =
1404
  fprintf fmt "%a = %a;@." (pp_c_type cdecl.const_id) cdecl.const_type pp_c_const cdecl.const_value 
1405

    
1406
let print_const_decl fmt cdecl =
1407
  fprintf fmt "extern %a;@." (pp_c_type cdecl.const_id) cdecl.const_type
1408

    
1409
let print_alloc_instance fmt (i, (m, static)) =
1410
  fprintf fmt "_alloc->%s = %a (%a);@,"
1411
    i
1412
    pp_machine_alloc_name (node_name m)
1413
    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
1414

    
1415
let print_alloc_array fmt vdecl =
1416
  let base_type = Types.array_base_type vdecl.var_type in
1417
  let size_types = Types.array_type_multi_dimension vdecl.var_type in
1418
  let size_type = Dimension.multi_dimension_product vdecl.var_loc size_types in
1419
  fprintf fmt "_alloc->%s = (%a*) malloc((%a)*sizeof(%a));@,assert(_alloc->%s);@,"
1420
    vdecl.var_id
1421
    (pp_c_type "") base_type
1422
    Dimension.pp_dimension size_type
1423
    (pp_c_type "") base_type
1424
    vdecl.var_id
1425

    
1426
let rec list_to_partial l = match l with
1427
  | []   -> [[]]
1428
  | _::q -> l::(list_to_partial q)
1429

    
1430
let print_alloc_code fmt m =
1431
  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
1432
  fprintf fmt "%a *_alloc;@,_alloc = (%a *) malloc(sizeof(%a));@,assert(_alloc);@,%a%areturn _alloc;"
1433
    pp_machine_memtype_name m.mname.node_id
1434
    pp_machine_memtype_name m.mname.node_id
1435
    pp_machine_memtype_name m.mname.node_id
1436
    (Utils.fprintf_list ~sep:"" print_alloc_array) array_mem
1437
    (Utils.fprintf_list ~sep:"" print_alloc_instance) m.minstances
1438

    
1439
let print_step_code fmt m self =
1440
  if not (!Options.ansi && 
1441
	     is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc })
1442
  then
1443
    (* C99 code *)
1444
    let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
1445
    fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%t%a%t%t%t@]@,}@.@."
1446
      (print_step_prototype self) (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
1447
      (* locals *)
1448
      (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals
1449
      (Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals)
1450
      (* array mems *)
1451
      (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
1452
      (Utils.pp_final_char_if_non_empty ";@," array_mems)
1453
      (* check assertions *)
1454
      (pp_c_checks self m.mstep.step_outputs) m.mstep.step_checks
1455
      (* instrs *)
1456
      (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
1457
      (Utils.pp_newline_if_non_empty m.mstep.step_instrs)
1458
      (* Print specification if any: insert side effect at the end of the function body  *)
1459
      (fun fmt -> match m.mspec with
1460
      | None -> ()
1461
      | Some spec -> pp_acsl_spec_side_effects m m.mstep.step_outputs fmt spec
1462
      )
1463
      (let f = fun fmt x-> fprintf fmt "/*@@assert (%a);*/@," (pp_acsl_fun_trans (Some (m.mstep.step_instrs, m.minstances)) "" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true self true m.mstep.step_locals) (Some x) in
1464
      (Utils.fprintf_list ~sep:"@," f)) (List.rev (list_to_partial m.mstep.step_locals))
1465
      (fun fmt-> fprintf fmt "/*@@assert (%a);*/@," (pp_acsl_fun_trans None "C" m.mname.node_id m.mstep.step_inputs m.mstep.step_outputs None true self true []) (Some []))
1466
      (let pp_eexpr_expr fmt ee = 
1467
        fprintf fmt "spec_%i(%a, *%s)" ee.muid (Utils.fprintf_list ~sep:", " (pp_acsl_var_read m.mstep.step_outputs "")) ee.mmstep_logic.step_inputs self
1468
       in
1469
       fun fmt -> match m.mspec with
1470
        | Some spec when 0 < List.length spec.m_ensures-> fprintf fmt "/*@@assert (%a);*/@," (Utils.fprintf_list ~sep:"&&@," pp_eexpr_expr) spec.m_ensures
1471
        | None ->fprintf fmt ""
1472
      )
1473
      (fun fmt -> fprintf fmt "return;")
1474
  else
1475
    (* C90 code *)
1476
    let (gen_locals, base_locals) = List.partition (fun v -> Types.is_generic_type v.var_type) m.mstep.step_locals in
1477
    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
1478
    fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t%t@]@,}@.@."
1479
      (print_step_prototype self) 
1480
         (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
1481
      (* locals *)
1482
      (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) base_locals
1483
      (Utils.pp_final_char_if_non_empty ";" base_locals)
1484
      (* check assertions *)
1485
      (pp_c_checks self m.mstep.step_outputs) m.mstep.step_checks
1486
      (* instrs *)
1487
      (Utils.fprintf_list ~sep:"@," 
1488
	 (pp_machine_instr 
1489
	    (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, m.mstep.step_locals, m.mmemory, m.minstances, m.mcalls) self)
1490
      ) m.mstep.step_instrs
1491
      (Utils.pp_newline_if_non_empty m.mstep.step_instrs)
1492
      (* Print specification if any: insert side effect at the end of the function body  *)
1493
      (fun fmt -> match m.mspec with
1494
      | None -> ()
1495
      | Some spec -> pp_acsl_spec_side_effects m m.mstep.step_outputs fmt spec
1496
      )
1497
      (fun fmt -> fprintf fmt "return;")
1498

    
1499
let print_reset_code fmt m self =
1500
  fprintf fmt "@[<v 2>%a {@,%a%t%treturn;@]@,}@.@."
1501
    (print_reset_prototype self) (m.mname.node_id, m.mstatic)
1502
    (Utils.fprintf_list ~sep:"@," 
1503
       (pp_machine_instr 
1504
	  (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs, m.mstep.step_locals, m.mmemory, m.minstances, m.mcalls) self)) 
1505
    m.minit
1506
    (Utils.pp_newline_if_non_empty m.minit)
1507
    (* Print specification if any: insert side effect at the end of the function body  *)
1508
    (fun fmt -> match m.mspec with
1509
    | None -> ()
1510
    | Some spec -> pp_acsl_spec_init_side_effects m m.mstep.step_outputs fmt spec
1511
    )
1512

    
1513

    
1514
let print_machine fmt m =
1515
  if m.mname.node_id <> arrow_id
1516
  then (
1517
  (* We don't print arrow function *)
1518
  (* Alloc function, only if non static mode *)
1519
    if (not !Options.static_mem) then  
1520
      (
1521
	fprintf fmt "@[<v 2>%a {@,%a@]@,}@.@."
1522
	  print_alloc_prototype (m.mname.node_id, m.mstatic)
1523
	  print_alloc_code m;
1524
      );
1525
    let self = mk_self m in
1526
    (* Reset function *)
1527
    print_reset_code fmt m self;
1528
    (* Step function *)
1529
    print_step_code fmt m self
1530
  )
1531

    
1532
(********************************************************************************************)
1533
(*                         Main related functions                                           *)
1534
(********************************************************************************************)
1535

    
1536
let print_get_input fmt v =
1537
  match v.var_type.Types.tdesc with
1538
    | Types.Tint -> fprintf fmt "_get_int(\"%s\")" v.var_id
1539
    | Types.Tbool -> fprintf fmt "_get_bool(\"%s\")" v.var_id
1540
    | Types.Treal -> fprintf fmt "_get_double(\"%s\")" v.var_id
1541
    | _ -> assert false
1542

    
1543
let print_put_outputs fmt ol = 
1544
  let po fmt o =
1545
    match o.var_type.Types.tdesc with
1546
    | Types.Tint -> fprintf fmt "_put_int(\"%s\", %s)" o.var_id o.var_id
1547
    | Types.Tbool -> fprintf fmt "_put_bool(\"%s\", %s)" o.var_id o.var_id
1548
    | Types.Treal -> fprintf fmt "_put_double(\"%s\", %s)" o.var_id o.var_id
1549
    | _ -> assert false
1550
  in
1551
  List.iter (fprintf fmt "@ %a;" po) ol
1552

    
1553
let print_main_fun machines m fmt =
1554
  let mname = m.mname.node_id in
1555
  let main_mem =
1556
    if (!Options.static_mem && !Options.main_node <> "")
1557
    then "&main_mem"
1558
    else "main_mem" in
1559
  fprintf fmt "@[<v 2>int main (int argc, char *argv[]) {@ ";
1560
  fprintf fmt "/* Declaration of inputs/outputs variables */@ ";
1561
  List.iter 
1562
    (fun v -> fprintf fmt "%a = %a;@ " (pp_c_type v.var_id) v.var_type pp_c_initialize v.var_type
1563
    ) m.mstep.step_inputs;
1564
  List.iter 
1565
    (fun v -> fprintf fmt "%a = %a;@ " (pp_c_type v.var_id) v.var_type pp_c_initialize v.var_type
1566
    ) m.mstep.step_outputs;
1567
  fprintf fmt "@ /* Main memory allocation */@ ";
1568
  if (!Options.static_mem && !Options.main_node <> "")
1569
  then (*(fprintf fmt "%a(static,main_mem);@ " pp_machine_static_alloc_name mname)*) (fprintf fmt "%a main_mem;@ " pp_machine_memtype_name mname)
1570
  else (fprintf fmt "%a *main_mem = %a();@ " pp_machine_memtype_name mname pp_machine_alloc_name mname);
1571
  fprintf fmt "@ /* Initialize the main memory */@ ";
1572
  fprintf fmt "%a(%s);@ " pp_machine_reset_name mname main_mem;
1573
  fprintf fmt "@ ISATTY = isatty(0);@ ";
1574
  fprintf fmt "@ /* Infinite loop */@ ";
1575
  (match m.mspec with
1576
      | None -> ()
1577
      | Some spec -> fprintf fmt "/*@@ loop invariant %a;*/@," (pp_acsl_fun_inv m.mname.node_id "main_mem") (Some "")
1578
  );
1579
  fprintf fmt "@[<v 2>while(1){@ ";
1580
  (*fprintf fmt  "fflush(stdout);@ ";*)
1581
  List.iter 
1582
    (fun v -> fprintf fmt "%s = %a;@ "
1583
      v.var_id
1584
      print_get_input v
1585
    ) m.mstep.step_inputs;
1586
  (match m.mstep.step_outputs with
1587
    (* | [] -> ( *)
1588
    (*   fprintf fmt "%a(%a%t%s);@ "  *)
1589
    (* 	pp_machine_step_name mname *)
1590
    (* 	(Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs *)
1591
    (* 	(pp_final_char_if_non_empty ", " m.mstep.step_inputs) *)
1592
    (* 	main_mem *)
1593
    (* ) *)
1594
    (* | [o] -> ( *)
1595
    (*   fprintf fmt "%s = %a(%a%t%a, %s);%a" *)
1596
    (* 	o.var_id *)
1597
    (* 	pp_machine_step_name mname *)
1598
    (* 	(Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs *)
1599
    (* 	(pp_final_char_if_non_empty ", " m.mstep.step_inputs) *)
1600
    (* 	(Utils.fprintf_list ~sep:", " (fun fmt v -> fprintf fmt "&%s" v.var_id)) m.mstep.step_outputs *)
1601
    (* 	main_mem *)
1602
    (* 	print_put_outputs [o]) *)
1603
    | _ -> (
1604
      fprintf fmt "%a(%a%t%a, %s);%a"
1605
	pp_machine_step_name mname
1606
	(Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs
1607
	(Utils.pp_final_char_if_non_empty ", " m.mstep.step_inputs)
1608
	(Utils.fprintf_list ~sep:", " (fun fmt v -> fprintf fmt "&%s" v.var_id)) m.mstep.step_outputs
1609
	main_mem
1610
	print_put_outputs m.mstep.step_outputs)
1611
  );
1612
  fprintf fmt "@]@ }@ ";
1613
  fprintf fmt "return 1;";
1614
  fprintf fmt "@]@ }@."       
1615

    
1616
let print_main_header fmt =
1617
  fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/include/lustrec/io_frontend.h\"@." Version.prefix
1618

    
1619
let rec pp_c_struct_type_field filename cpt fmt (label, tdesc) =
1620
  fprintf fmt "%a;" (pp_c_type_decl filename cpt label) tdesc
1621
and pp_c_type_decl filename cpt var fmt tdecl =
1622
  match tdecl with
1623
  | Tydec_any           -> assert false
1624
  | Tydec_int           -> fprintf fmt "int %s" var
1625
  | Tydec_real          -> fprintf fmt "double %s" var
1626
  | Tydec_float         -> fprintf fmt "float %s" var
1627
  | Tydec_bool          -> fprintf fmt "_Bool %s" var
1628
  | Tydec_clock ty      -> pp_c_type_decl filename cpt var fmt ty
1629
  | Tydec_const c       -> fprintf fmt "%s %s" c var
1630
  | Tydec_array (d, ty) -> fprintf fmt "%a[%a]" (pp_c_type_decl filename cpt var) ty pp_c_dimension d
1631
  | Tydec_enum tl ->
1632
    begin
1633
      incr cpt;
1634
      fprintf fmt "enum _enum_%s_%d { %a } %s" filename !cpt (Utils.fprintf_list ~sep:", " pp_print_string) tl var
1635
    end
1636
  | Tydec_struct fl ->
1637
    begin
1638
      incr cpt;
1639
      fprintf fmt "struct _struct_%s_%d { %a } %s" filename !cpt (Utils.fprintf_list ~sep:" " (pp_c_struct_type_field filename cpt)) fl var
1640
    end
1641

    
1642
let print_type_definitions fmt filename =
1643
  let cpt_type = ref 0 in
1644
  Hashtbl.iter (fun typ def ->
1645
    match typ with
1646
    | Tydec_const var ->
1647
      fprintf fmt "typedef %a;@.@."
1648
	(pp_c_type_decl filename cpt_type var) def
1649
    | _        -> ()) type_table
1650

    
1651
let print_makefile basename nodename dependencies fmt =
1652
  fprintf fmt "GCC=gcc@.";
1653
  fprintf fmt "LUSTREC=%s@." Sys.executable_name;
1654
  fprintf fmt "LUSTREC_BASE=%s@." (Filename.dirname (Filename.dirname Sys.executable_name));
1655
  fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
1656
  fprintf fmt "INC=${LUSTREC_BASE}/include/lustrec@.";
1657
  fprintf fmt "@.";
1658

    
1659
  (* main binary *)
1660
  fprintf fmt "%s_%s:@." basename nodename;
1661
  fprintf fmt "\t${GCC} -I${INC} -I. -c %s.c@." basename;    
1662
  fprintf fmt "\t${GCC} -I${INC} -I. -c %s_%s.c@." basename nodename;    
1663
  List.iter (fun s -> (* Format.eprintf "Adding dependency: %s@." s;  *)
1664
    fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
1665
    (("${INC}/io_frontend.c")::(List.map (fun s -> s ^ ".c") dependencies));    
1666
  (*  fprintf fmt "\t${GCC} -I${INC} -c ${INC}/StdLibrary.c@."; *)
1667
  (*  fprintf fmt "\t${GCC} -o %s_%s io_frontend.o StdLibrary.o -lm %s.o@." basename nodename basename*)
1668
  fprintf fmt "\t${GCC} -o %s_%s io_frontend.o %a -lm %s.o %s_%s.o@." 
1669
    basename nodename (* executable name *)
1670
    (Utils.fprintf_list ~sep:" " (fun fmt s -> Format.fprintf fmt "%s.o" s)) dependencies 
1671
    basename (* library .o *)
1672
    basename nodename (* main function . o *) ;
1673
  fprintf fmt "@.";
1674
  fprintf fmt "@.";
1675

    
1676
  (* EACSL version of library file . c *)
1677
  fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
1678
  fprintf fmt "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c -then-on e-acsl -print -ocode %s_eacsl.c@." basename basename; 
1679
  fprintf fmt "@.";
1680
  fprintf fmt "@.";
1681

    
1682
  (* EACSL version of library file . c + main .c  *)
1683
  fprintf fmt "%s_%s_eacsl.c: %s.c %s.h %s_%s.c@." basename nodename basename basename basename nodename;
1684
  fprintf fmt "\tframa-c -e-acsl-full-mmodel -machdep x86_64 -e-acsl %s.c %s_%s.c -then-on e-acsl -print -ocode %s_%s_eacsl.i@." 
1685
    basename basename nodename basename nodename; 
1686
  (* Ugly hack to deal with eacsl bugs *)
1687
  fprintf fmt "\tgrep -v _fc_stdout %s_%s_eacsl.i > %s_%s_eacsl.c" basename nodename basename nodename;
1688
  fprintf fmt "@.";
1689
  fprintf fmt "@.";
1690

    
1691
  (* EACSL version of binary *)
1692
  fprintf fmt "%s_%s_eacsl: %s_%s_eacsl.c@." basename nodename basename nodename;
1693
  fprintf fmt "\t${GCC} -Wno-attributes -I${INC} -I. -c %s_%s_eacsl.c@." basename nodename; (* compiling instrumented lib + main *)
1694
  List.iter (fun s -> (* Format.eprintf "Adding dependency: %s@." s;  *)
1695
    fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
1696
    (("${INC}/io_frontend.c")::(List.map (fun s -> s ^ ".c") dependencies));    
1697
  fprintf fmt "\t${GCC} -Wno-attributes -o %s_%s_eacsl io_frontend.o %a %s -lm %s_%s_eacsl.o@." 
1698
    basename nodename 
1699
    (Utils.fprintf_list ~sep:" " (fun fmt s -> Format.fprintf fmt "%s.o" s)) dependencies 
1700
    ("${FRAMACEACSL}/e_acsl.c " 
1701
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c " 
1702
     ^ "${FRAMACEACSL}/memory_model/e_acsl_mmodel.c")
1703
    basename nodename;
1704
  fprintf fmt "@.";
1705
  fprintf fmt "@.";
1706

    
1707
  fprintf fmt "clean:@.";
1708
  fprintf fmt "\t\\rm -f *.o %s_%s@." basename nodename
1709

    
1710

    
1711

    
1712

    
1713
(********************************************************************************************)
1714
(*                         Translation function                                             *)
1715
(********************************************************************************************)
1716

    
1717
let translate_to_c destname basename prog machines dependencies =
1718

    
1719
  let header_file = destname ^ ".h" in (* Could be changed *)
1720
  let header_out = open_out header_file in
1721
  let header_fmt = formatter_of_out_channel header_out in
1722

    
1723
  let source_file = destname ^ ".c" in (* Could be changed *)
1724
  let source_out = open_out source_file in
1725
  let source_fmt = formatter_of_out_channel source_out in
1726

    
1727
  let main_machine = Machine_code.get_machine_opt !Options.main_node machines in
1728

    
1729
  Log.report ~level:1 
1730
    (fun fmt -> fprintf fmt ".. opening files %s and %s@.@?" header_file source_file);
1731
  
1732
  (* Generating H file *)
1733

    
1734
  (* Include once: start *)
1735
  let baseNAME = String.uppercase basename in
1736
  let baseNAME = Str.global_replace (Str.regexp "\\.\\|\\ ") "_" baseNAME in
1737
  (* Print the svn version number and the supported C standard (C90 or C99) *)
1738
  print_version header_fmt;
1739
  fprintf header_fmt "#ifndef _%s@.#define _%s@." baseNAME baseNAME;
1740
  pp_print_newline header_fmt ();
1741
  fprintf header_fmt "/* Imports standard library */@.";
1742
  (* imports standard library definitions (arrow) *)
1743
  print_import_standard header_fmt;
1744
  pp_print_newline header_fmt ();
1745
  fprintf header_fmt "/* Types definitions */@.";
1746
  (* Print the type definitions from the type table *)
1747
  print_type_definitions header_fmt basename;
1748
  pp_print_newline header_fmt ();
1749
  (* Print the global constant declarations. *)
1750
  fprintf header_fmt "/* Global constant (declarations, definitions are in C file) */@.";
1751
  List.iter (fun c -> print_const_decl header_fmt c) (get_consts prog);
1752
  pp_print_newline header_fmt ();
1753

    
1754
  (* Print the struct declarations of all machines. *)
1755
  fprintf header_fmt "/* Struct declarations */@.";
1756
  List.iter (print_machine_struct header_fmt) (List.rev machines);
1757
  pp_print_newline header_fmt ();
1758

    
1759
  (* Print the spec of all machines *)
1760
  fprintf header_fmt "/* Spec declarations */@.";
1761
  List.iter (print_machine_spec machines header_fmt) machines;
1762
  pp_print_newline header_fmt ();
1763

    
1764
  (* Print the transition of all machines *)
1765
  fprintf header_fmt "/* Transitions declarations */@.";
1766
  List.iter (pp_acsl_def_trans header_fmt) (List.rev machines);
1767
  pp_print_newline header_fmt ();
1768

    
1769
  (* Print the prototypes of all machines *)
1770
  fprintf header_fmt "/* Nodes declarations */@.";
1771
  List.iter (print_machine_decl machines header_fmt) machines;
1772
  pp_print_newline header_fmt ();
1773
  (* Include once: end *)
1774
  fprintf header_fmt "#endif@.";
1775
  pp_print_newline header_fmt ();
1776

    
1777
  (* Generating lib C file *)
1778
  fprintf source_fmt "#include <stdlib.h>@.#include <assert.h>@.#include \"%s\"@.@." (basename^".h");
1779
  (* Print the svn version number and the supported C standard (C90 or C99) *)
1780
  print_version source_fmt;
1781
  (* Print the prototype of imported nodes *)
1782
  fprintf source_fmt "/* Imported nodes declarations */@.";
1783
  fprintf source_fmt "@[<v>";
1784
  List.iter (print_prototype source_fmt) prog;
1785
  fprintf source_fmt "@]@.";
1786
  (* Print consts *)
1787
  fprintf source_fmt "/* Global constants (definitions) */@.";
1788
  List.iter (fun c -> print_const_def source_fmt c) (get_consts prog);
1789
  pp_print_newline source_fmt ();
1790
  (* Print nodes one by one (in the previous order) *)
1791
  List.iter (print_machine source_fmt) machines;
1792
  
1793
  (* If a main node is specified, generate additional files *)
1794
  match main_machine with 
1795
    None -> ()
1796
  | Some m -> (
1797

    
1798
    let makefile_file = destname ^ ".makefile" in (* Could be changed *)
1799
    let makefile_out = open_out makefile_file in
1800
    let makefile_fmt = formatter_of_out_channel makefile_out in
1801

    
1802
    let source_main_file = destname ^ "_" ^ m.mname.node_id ^ ".c" in (* Could be changed *)
1803
    let source_main_out = open_out source_main_file in
1804
    let source_main_fmt = formatter_of_out_channel source_main_out in
1805

    
1806
    Log.report ~level:1 
1807
      (fun fmt -> fprintf fmt ".. opening files %s and %s@.@?" 
1808
	header_file source_main_file);
1809
    
1810
    (* Generating main C file *)
1811
    
1812
    print_main_header source_main_fmt;
1813
    fprintf source_main_fmt "#include <stdlib.h>@.#include <assert.h>@.#include \"%s\"@.@." (basename^".h");
1814
    (* Print the svn version number and the supported C standard (C90 or C99) *)
1815
    print_version source_main_fmt;
1816
    print_main_fun machines m source_main_fmt;
1817

    
1818

    
1819
    (* Generating Makefile *)
1820

    
1821
    print_makefile basename !Options.main_node dependencies makefile_fmt
1822
  )
1823

    
1824
(* Local Variables: *)
1825
(* compile-command:"make -C .." *)
1826
(* End: *)