Project

General

Profile

Revision c02d255e src/c_backend.ml

View differences:

src/c_backend.ml
28 28
open Corelang
29 29
open Machine_code
30 30

  
31

  
32 31
(********************************************************************************************)
33 32
(*                     Basic      Printing functions                                        *)
34 33
(********************************************************************************************)
......
92 91
  let rec aux t pp_suffix =
93 92
  match (Types.repr t).Types.tdesc with
94 93
  | Types.Tclock t'       -> aux t' pp_suffix
95
  | Types.Tbool           -> Format.fprintf fmt "_Bool %s%a" var pp_suffix ()
96
  | Types.Treal           -> Format.fprintf fmt "double %s%a" var pp_suffix ()
97
  | Types.Tint            -> Format.fprintf fmt "int %s%a" var pp_suffix ()
94
  | Types.Tbool           -> fprintf fmt "_Bool %s%a" var pp_suffix ()
95
  | Types.Treal           -> fprintf fmt "double %s%a" var pp_suffix ()
96
  | Types.Tint            -> fprintf fmt "int %s%a" var pp_suffix ()
98 97
  | Types.Tarray (d, t')  ->
99
    let pp_suffix' fmt () = Format.fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
98
    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
100 99
    aux t' pp_suffix'
101
  | Types.Tstatic (_, t') -> Format.fprintf fmt "const "; aux t' pp_suffix
102
  | Types.Tconst ty       -> Format.fprintf fmt "%s %s" ty var
103
  | Types.Tarrow (_, _)   -> Format.fprintf fmt "void (*%s)()" var
104
  | _                     -> Format.eprintf "internal error: pp_c_type %a@." Types.print_ty t; assert false
100
  | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix
101
  | Types.Tconst ty       -> fprintf fmt "%s %s" ty var
102
  | Types.Tarrow (_, _)   -> fprintf fmt "void (*%s)()" var
103
  | _                     -> eprintf "internal error: pp_c_type %a@." Types.print_ty t; assert false
105 104
  in aux t (fun fmt () -> ())
106 105

  
107 106
let rec pp_c_initialize fmt t = 
......
111 110
  | Types.Tbool -> pp_print_string fmt "0" 
112 111
  | Types.Treal -> pp_print_string fmt "0."
113 112
  | Types.Tarray (d, t') when Dimension.is_dimension_const d ->
114
    Format.fprintf fmt "{%a}"
113
    fprintf fmt "{%a}"
115 114
      (Utils.fprintf_list ~sep:"," (fun fmt _ -> pp_c_initialize fmt t'))
116 115
      (Utils.duplicate 0 (Dimension.size_const_dimension d))
117 116
  | _ -> assert false
......
146 145
  pp_c_type id.var_id fmt id.var_type
147 146

  
148 147
let pp_c_decl_array_mem self fmt id =
149
  Format.fprintf fmt "%a = (%a) (%s->_reg.%s)"
148
  fprintf fmt "%a = (%a) (%s->_reg.%s)"
150 149
    (pp_c_type (sprintf "(*%s)" id.var_id)) id.var_type
151 150
    (pp_c_type "(*)") id.var_type
152 151
    self
......
169 168
let pp_c_var_read m fmt id =
170 169
  if Types.is_array_type id.var_type
171 170
  then
172
    Format.fprintf fmt "%s" id.var_id
171
    fprintf fmt "%s" id.var_id
173 172
  else
174 173
    if List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs (* id is output *)
175
    then Format.fprintf fmt "*%s" id.var_id
176
    else Format.fprintf fmt "%s" id.var_id
174
    then fprintf fmt "*%s" id.var_id
175
    else fprintf fmt "%s" id.var_id
177 176

  
178 177
(* Addressable value of a variable, the one that is passed around in calls:
179 178
   - if it's not a scalar non-output, then its name is enough
......
183 182
let pp_c_var_write m fmt id =
184 183
  if Types.is_array_type id.var_type
185 184
  then
186
    Format.fprintf fmt "%s" id.var_id
185
    fprintf fmt "%s" id.var_id
187 186
  else
188 187
    if List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs (* id is output *)
189 188
    then
190
      Format.fprintf fmt "%s" id.var_id
189
      fprintf fmt "%s" id.var_id
191 190
    else
192
      Format.fprintf fmt "&%s" id.var_id
191
      fprintf fmt "&%s" id.var_id
193 192

  
194 193
let pp_c_decl_instance_var fmt (name, (node, static)) = 
195
  Format.fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
194
  fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
196 195

  
197 196
let pp_c_tag fmt t =
198 197
 pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
......
204 203
    | Const_real r   -> pp_print_string fmt r
205 204
    | Const_float r  -> pp_print_float fmt r
206 205
    | Const_tag t    -> pp_c_tag fmt t
207
    | Const_array ca -> Format.fprintf fmt "{%a}" (Utils.fprintf_list ~sep:"," pp_c_const) ca
206
    | Const_array ca -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:"," pp_c_const) ca
208 207

  
209 208
(* Prints a value expression [v], with internal function calls only.
210 209
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
......
213 212
let rec pp_c_val self pp_var fmt v =
214 213
  match v with
215 214
    | Cst c         -> pp_c_const fmt c
216
    | Array vl      -> Format.fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
217
    | Access (t, i) -> Format.fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
215
    | Array vl      -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
216
    | Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
218 217
    | Power (v, n)  -> assert false
219 218
    | LocalVar v    -> pp_var fmt v
220 219
    | StateVar v    ->
221 220
      if Types.is_array_type v.var_type
222
      then Format.fprintf fmt "*%a" pp_var v
223
      else Format.fprintf fmt "%s->_reg.%a" self pp_var v
221
      then fprintf fmt "*%a" pp_var v
222
      else fprintf fmt "%s->_reg.%a" self pp_var v
224 223
    | Fun (n, vl)   -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl
225 224

  
226 225
let pp_c_checks self fmt m =
227
  Utils.fprintf_list ~sep:"" (fun fmt (loc, check) -> Format.fprintf fmt "@[<v>%a@,assert (%a);@]@," Location.pp_c_loc loc (pp_c_val self (pp_c_var_read m)) check) fmt m.mstep.step_checks
226
  Utils.fprintf_list ~sep:"" (fun fmt (loc, check) -> fprintf fmt "@[<v>%a@,assert (%a);@]@," Location.pp_c_loc loc (pp_c_val self (pp_c_var_read m)) check) fmt m.mstep.step_checks
228 227

  
229 228

  
230 229
(********************************************************************************************)
......
269 268
(* Prints a one loop variable suffix for arrays *)
270 269
let pp_loop_var fmt lv =
271 270
 match snd lv with
272
 | LVar v -> Format.fprintf fmt "[%s]" v
273
 | LInt r -> Format.fprintf fmt "[%d]" !r
271
 | LVar v -> fprintf fmt "[%s]" v
272
 | LInt r -> fprintf fmt "[%d]" !r
274 273

  
275 274
(* Prints a suffix of loop variables for arrays *)
276 275
let pp_suffix fmt loop_vars =
......
286 285
 | _               , Fun (n, vl)  ->
287 286
   Basic_library.pp_c n (pp_value_suffix self loop_vars pp_value) fmt vl
288 287
 | _               , _            ->
289
   let pp_var_suffix fmt v = Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in
288
   let pp_var_suffix fmt v = fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in
290 289
   pp_c_val self pp_var_suffix fmt value
291 290

  
292 291
(* type_directed assignment: array vs. statically sized type
......
297 296
*)
298 297
let pp_assign m self pp_var fmt var_type var_name value =
299 298
  let depth = expansion_depth value in
300
(*Format.eprintf "pp_assign %a %a %d@." Types.print_ty var_type pp_val value depth;*)
299
(*eprintf "pp_assign %a %a %d@." Types.print_ty var_type pp_val value depth;*)
301 300
  let loop_vars = mk_loop_variables m var_type depth in
302 301
  let reordered_loop_vars = reorder_loop_variables loop_vars in
303 302
  let rec aux fmt vars =
......
305 304
    | [] ->
306 305
      fprintf fmt "%a = %a;" (pp_value_suffix self loop_vars pp_var) var_name (pp_value_suffix self loop_vars pp_var) value
307 306
    | (d, LVar i) :: q ->
308
(*Format.eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
309
      Format.fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
307
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
308
      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
310 309
	i i i Dimension.pp_dimension d i
311 310
	aux q
312 311
    | (d, LInt r) :: q ->
313
(*Format.eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
312
(*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
314 313
      let szl = Utils.enumerate (Dimension.size_const_dimension d) in
315
      Format.fprintf fmt "@[<v 2>{@,%a@]@,}"
314
      fprintf fmt "@[<v 2>{@,%a@]@,}"
316 315
	(Utils.fprintf_list ~sep:"@," (fun fmt i -> r := i; aux fmt q)) szl
317 316
  in
318 317
  begin
......
324 323
let pp_instance_call m self fmt i (inputs: value_t list) (outputs: var_decl list) =
325 324
 try (* stateful node instance *)
326 325
   let (n,_) = List.assoc i m.minstances in
327
   Format.fprintf fmt "%s_step (%a%t%a%t%s->%s);"
326
   fprintf fmt "%s_step (%a%t%a%t%s->%s);"
328 327
     (node_name n)
329 328
     (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
330 329
     (Utils.pp_final_char_if_non_empty ", " inputs) 
......
334 333
     i
335 334
 with Not_found -> (* stateless node instance *)
336 335
   let (n,_) = List.assoc i m.mcalls in
337
   Format.fprintf fmt "%s (%a%t%a);"
336
   fprintf fmt "%s (%a%t%a);"
338 337
     (node_name n)
339 338
     (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
340 339
     (Utils.pp_final_char_if_non_empty ", " inputs) 
......
385 384
	(Utils.fprintf_list ~sep:"@," (pp_machine_branch m self)) hl
386 385

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

  
389

  
390
(**************************************************************************)
391
(*     Printing spec for c *)
392

  
393
(**************************************************************************)
394

  
395

  
396
let pp_econst fmt c = 
397
  match c with
398
    | EConst_int i -> pp_print_int fmt i
399
    | EConst_real r -> pp_print_string fmt r
400
    | EConst_float r -> pp_print_float fmt r
401
    | EConst_bool b -> pp_print_bool fmt b
402
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
403

  
404
let rec pp_eexpr is_output fmt eexpr = 
405
  let pp_eexpr = pp_eexpr is_output in
406
  match eexpr.eexpr_desc with
407
    | EExpr_const c -> pp_econst fmt c
408
    | EExpr_ident id -> 
409
      if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
410
    | EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el
411
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
412
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
413
    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
414
    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
415
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
416
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
417
    | EExpr_merge (id, e1, e2) -> 
418
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
419
    | EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r
420
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" Printers.pp_node_args vars pp_eexpr e 
421
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" Printers.pp_node_args vars pp_eexpr e 
422

  
423

  
424
    (* | EExpr_whennot _ *)
425
    (* | EExpr_uclock _ *)
426
    (* | EExpr_dclock _ *)
427
    (* | EExpr_phclock _ -> assert false *)
428
and pp_eapp is_output fmt id e r =
429
  let pp_eexpr = pp_eexpr is_output in
430
  match r with
431
  | None ->
432
    (match id, e.eexpr_desc with
433
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
434
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
435
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
436
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
437
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
438
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
439
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
440
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
441
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
442
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
443
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
444
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
445
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
446
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
447
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
448
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
449
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
450
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
451
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
452
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
453

  
454
let pp_ensures is_output fmt e =
455
  match e with
456
    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " (pp_eexpr is_output) e
457
    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (Utils.fprintf_list ~sep:", " (pp_eexpr is_output)) args
458

  
459
let pp_acsl_spec outputs fmt spec =
460
  let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in
461
  let pp_eexpr = pp_eexpr is_output in
462
  fprintf fmt "@[<v 2>/*@@ ";
463
  Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
464
  Utils.fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures;
465
  fprintf fmt "@ ";
466
  (* fprintf fmt "assigns *self%t%a;@ "  *)
467
  (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)
468
  (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)
469
  Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 
470
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
471
      name
472
      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
473
      (Utils.fprintf_list ~sep:"@ " (pp_ensures is_output)) requires
474
  ) fmt spec.behaviors;
475
  fprintf fmt "@]@ */@.";
476
  ()
389 477

  
390 478
(********************************************************************************************)
391 479
(*                      Prototype Printing functions                                        *)
......
567 655
    (match m.mspec with
568 656
      | None -> ()
569 657
      | Some spec -> 
570
	Printers.pp_acsl_spec m.mstep.step_outputs fmt spec
658
	pp_acsl_spec m.mstep.step_outputs fmt spec
571 659
    );
572 660
    fprintf fmt "extern %a;@.@."
573 661
      (print_step_prototype self)
......
772 860

  
773 861
let print_makefile basename nodename fmt =
774 862
  fprintf fmt "GCC=gcc@.";
775
  fprintf fmt "INC=/usr/local/include/lustrec@.";
863
  fprintf fmt "LUSTREC=%s@." Sys.executable_name;
864
  fprintf fmt "LUSTREC_BASE=%s@." (Filename.dirname (Filename.dirname Sys.executable_name));
865
  fprintf fmt "INC=${LUSTREC_BASE}/include/lustrec@.";
776 866
  fprintf fmt "@.";
777 867
  fprintf fmt "%s_%s:@." basename nodename;
778 868
  fprintf fmt "\t${GCC} -I${INC} -I. -c %s.c@." basename;    
779 869
  fprintf fmt "\t${GCC} -I${INC} -c ${INC}/io_frontend.c@.";    
780 870
(*  fprintf fmt "\t${GCC} -I${INC} -c ${INC}/StdLibrary.c@."; *)
781 871
(*  fprintf fmt "\t${GCC} -o %s_%s io_frontend.o StdLibrary.o -lm %s.o@." basename nodename basename*)
782
 fprintf fmt "\t${GCC} -o %s_%s io_frontend.o -lm %s.o@." basename nodename basename
872
 fprintf fmt "\t${GCC} -o %s_%s io_frontend.o -lm %s.o@." basename nodename basename;
873
 fprintf fmt "@.";
874
 fprintf fmt "clean:@.";
875
 fprintf fmt "\t\\rm -f *.o %s_%s@." basename nodename
783 876

  
784 877

  
785 878

  

Also available in: Unified diff