Project

General

Profile

Revision 521e2a6b

View differences:

src/backends/C/c_backend_common.ml
474 474
    pp_c_val self pp_var fmt (mk_val (StateVar var) var.var_type)
475 475
  else
476 476
    pp_c_val self pp_var fmt (mk_val (LocalVar var) var.var_type)
477
  
477 478

  
478 479
let pp_array_suffix fmt loop_vars =
479 480
  Utils.fprintf_list ~sep:"" (fun fmt v -> fprintf fmt "[%s]" v) fmt loop_vars
src/backends/C/c_backend_src.ml
141 141

  
142 142
(* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
143 143
let rec pp_value_suffix self var_type loop_vars pp_value fmt value =
144
 (*Format.eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)
145
 match loop_vars, value.value_desc with
146
 | (x, LAcc i) :: q, _ when is_const_index i ->
147
   let r = ref (Dimension.size_const_dimension (Machine_code.dimension_of_value i)) in
148
   pp_value_suffix self var_type ((x, LInt r)::q) pp_value fmt value
149
 | (_, LInt r) :: q, Cst (Const_array cl) ->
150
   let var_type = Types.array_element_type var_type in
151
   pp_value_suffix self var_type q pp_value fmt (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)
152
 | (_, LInt r) :: q, Array vl      ->
153
   let var_type = Types.array_element_type var_type in
154
   pp_value_suffix self var_type q pp_value fmt (List.nth vl !r)
155
 | loop_var    :: q, Array vl      ->
156
   let var_type = Types.array_element_type var_type in
157
   Format.fprintf fmt "(%a[]){%a }%a" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix self var_type q pp_value)) vl pp_suffix [loop_var]
158
 | []              , Array vl      ->
159
   let var_type = Types.array_element_type var_type in
160
   Format.fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix self var_type [] pp_value)) vl
161
 | _           :: q, Power (v, n)  ->
162
   pp_value_suffix self var_type q pp_value fmt v
163
 | _               , Fun (n, vl)   ->
164
   Basic_library.pp_c n (pp_value_suffix self var_type loop_vars pp_value) fmt vl
165
 | _               , Access (v, i) ->
166
   let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
167
   pp_value_suffix self var_type ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_value fmt v
168
 | _               , LocalVar v    -> Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars
169
 | _               , StateVar v    ->
170
    (* array memory vars are represented by an indirection to a local var with the right type,
171
       in order to avoid casting everywhere. *)
172
   if Types.is_array_type v.var_type
173
   then Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars
174
   else Format.fprintf fmt "%s->_reg.%a%a" self pp_value v pp_suffix loop_vars
175
 | _               , Cst cst       -> pp_c_const_suffix var_type fmt cst
176
 | _               , _             -> (Format.eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars; assert false)
177

  
144
  (*Format.eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)
145
  (
146
    match loop_vars, value.value_desc with
147
    | (x, LAcc i) :: q, _ when is_const_index i ->
148
       let r = ref (Dimension.size_const_dimension (Machine_code.dimension_of_value i)) in
149
       pp_value_suffix self var_type ((x, LInt r)::q) pp_value fmt value
150
    | (_, LInt r) :: q, Cst (Const_array cl) ->
151
       let var_type = Types.array_element_type var_type in
152
       pp_value_suffix self var_type q pp_value fmt (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)
153
    | (_, LInt r) :: q, Array vl      ->
154
       let var_type = Types.array_element_type var_type in
155
       pp_value_suffix self var_type q pp_value fmt (List.nth vl !r)
156
    | loop_var    :: q, Array vl      ->
157
       let var_type = Types.array_element_type var_type in
158
       Format.fprintf fmt "(%a[]){%a }%a" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix self var_type q pp_value)) vl pp_suffix [loop_var]
159
    | []              , Array vl      ->
160
       let var_type = Types.array_element_type var_type in
161
       Format.fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix self var_type [] pp_value)) vl
162
    | _           :: q, Power (v, n)  ->
163
       pp_value_suffix self var_type q pp_value fmt v
164
    | _               , Fun (n, vl)   ->
165
       Basic_library.pp_c n (pp_value_suffix self var_type loop_vars pp_value) fmt vl
166
    | _               , Access (v, i) ->
167
       let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
168
       pp_value_suffix self var_type ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_value fmt v
169
    | _               , LocalVar v    -> Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars
170
    | _               , StateVar v    ->
171
       (* array memory vars are represented by an indirection to a local var with the right type,
172
	  in order to avoid casting everywhere. *)
173
       if Types.is_array_type v.var_type
174
       then Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars
175
       else Format.fprintf fmt "%s->_reg.%a%a" self pp_value v pp_suffix loop_vars
176
    | _               , Cst cst       -> pp_c_const_suffix var_type fmt cst
177
    | _               , _             -> (Format.eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars; assert false)
178
  )
179
   
178 180
(* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
179 181
   which may yield constant arrays in expressions.
180 182
   Type is needed to correctly print constant arrays.
src/compiler_common.ml
25 25
  begin
26 26
    if not (Sys.file_exists !Options.dest_dir) then
27 27
      begin
28
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. creating destination directory@,");
28
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. creating destination directory@ ");
29 29
	Unix.mkdir !Options.dest_dir (Unix.stat ".").Unix.st_perm
30 30
      end;
31 31
    if (Unix.stat !Options.dest_dir).Unix.st_kind <> Unix.S_DIR then
......
69 69

  
70 70
  (* Parsing *)
71 71
  Log.report ~level:1 
72
    (fun fmt -> fprintf fmt ".. parsing source file %s@," source_name);
72
    (fun fmt -> fprintf fmt ".. parsing source file %s@ " source_name);
73 73
  try
74 74
    let prog = Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf in
75 75
    (*ignore (Modules.load_program ISet.empty prog);*)
src/log.ml
13 13
if !Options.verbose_level >= level then
14 14
  begin
15 15
    Format.eprintf "%t" p;
16
    Format.pp_print_flush Format.err_formatter ()
16
  (* Removed the flush since it was breaking most open/close boxes *)
17
  (* Format.pp_print_flush Format.err_formatter () *)
17 18
  end
18 19

  
19 20
(* Local Variables: *)
src/main_lustre_compiler.ml
50 50
      (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension));
51 51
    Lusic.write_lusic true header destname lusic_ext;
52 52
    Lusic.print_lusic_to_h destname lusic_ext;
53
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.")
53
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@ ")
54 54
  end
55 55

  
56 56
(* check whether a source file has a compiled header,
......
91 91

  
92 92
(* From prog to prog *)
93 93
let stage1 prog dirname basename =
94
  (* Removing automata *) 
94
  (* Removing automata *)
95 95
  let prog = expand_automata prog in
96

  
97
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog);
96
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@,  @[<v 2>@,%a@]@ " Printers.pp_prog prog);
98 97

  
99 98
  (* Importing source *)
100 99
  let _ = Modules.load_program ISet.empty prog in
......
247 246
     - introduce fresh local variables for each real pure subexpression
248 247
  *)
249 248
  (* DFS with modular code generation *)
250
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@ ");
249
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
251 250
  let machine_code = Machine_code.translate_prog prog node_schs in
252 251

  
253
   (* Optimize machine code *)
252
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ "Machine_code.pp_machines machine_code);
253

  
254
  (* Optimize machine code *)
254 255
  let machine_code =
255 256
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
256 257
      begin
257 258
	Log.report ~level:1 
258 259
	  (fun fmt -> fprintf fmt ".. machines optimization: sub-expression elimination@,");
259
	Optimize_machine.machines_cse machine_code
260
	let machine_code = Optimize_machine.machines_cse machine_code in
261
	Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "Machine_code.pp_machines machine_code);
262
	machine_code
260 263
      end
261 264
    else
262 265
      machine_code
......
266 269
    if !Options.optimization >= 2 (*&& !Options.output <> "horn"*) then
267 270
      begin
268 271
	Log.report ~level:1 (fun fmt -> fprintf fmt 
269
    ".. machines optimization: const. inlining (partial eval. with const)@,");
270
	Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code
272
	  ".. machines optimization: const. inlining (partial eval. with const)@,");
273
	let machine_code, removed_table = Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code in
274
	Log.report ~level:3 (fun fmt -> fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ "
275
	  (pp_imap Optimize_machine.pp_elim) removed_table);
276
	Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (const inlining):@ %a@ "Machine_code.pp_machines machine_code);	
277
	machine_code, removed_table
271 278
      end
272 279
    else
273 280
      machine_code, IMap.empty
......
370 377
let rec compile_source dirname basename extension =
371 378
  let source_name = dirname ^ "/" ^ basename ^ extension in
372 379

  
373
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
380
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
374 381

  
375 382
  (* Parsing source *)
376 383
  let prog = parse_source source_name in
......
382 389
      prog
383 390
  in
384 391
  let prog, dependencies = 
392
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
385 393
    try 
386 394
      stage1 prog dirname basename
387 395
    with StopPhase1 prog -> (
388 396
      if !Options.lusi then
389 397
	begin
390 398
	  let lusi_ext = extension ^ "i" in
391
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@," (basename ^ lusi_ext));
399
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@ " (basename ^ lusi_ext));
392 400
	  print_lusi prog dirname basename lusi_ext;
393 401
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
394 402
	  exit 0
......
397 405
        assert false
398 406
    )
399 407
  in
408
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@,");
409
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Normalized program:@ %a@ "Printers.pp_prog prog);
410

  
411
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
400 412

  
401 413
  let machine_code = 
402 414
    stage2 prog 
403 415
  in
416

  
417
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
418
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ "Machine_code.pp_machines machine_code);
419

  
404 420
  if Scopes.Plugin.show_scopes () then
405 421
    begin
406 422
      let all_scopes = Scopes.compute_scopes prog !Options.main_node in
407 423
      (* Printing scopes *)
408 424
      if !Options.verbose_level >= 1 then
409 425
	Format.printf "Possible scopes are:@   ";
410
      Format.printf "@[<v>%a@ @]@.@?" Scopes.print_scopes all_scopes;
426
      Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes;
411 427
      exit 0
412 428
	
413 429
    end;
src/optimize_machine.ml
19 19

  
20 20
let pp_elim fmt elim =
21 21
  begin
22
    Format.fprintf fmt "{ /* elim table: */@.";
23
    IMap.iter (fun v expr -> Format.fprintf fmt "%s |-> %a@." v pp_val expr) elim;
24
    Format.fprintf fmt "}@.";
22
    Format.fprintf fmt "@[{ /* elim table: */@ ";
23
    IMap.iter (fun v expr -> Format.fprintf fmt "%s |-> %a@ " v pp_val expr) elim;
24
    Format.fprintf fmt "}@ @]";
25 25
  end
26 26

  
27 27
let rec eliminate elim instr =
src/printers.ml
71 71
let rec pp_expr fmt expr =
72 72
  (match expr.expr_annot with 
73 73
  | None -> fprintf fmt "%t" 
74
  | Some ann -> fprintf fmt "(%a %t)" pp_expr_annot ann)
74
  | Some ann -> fprintf fmt "@[(%a %t)@]" pp_expr_annot ann)
75 75
    (fun fmt -> 
76 76
      match expr.expr_desc with
77 77
    | Expr_const c -> pp_const fmt c
78
    | Expr_ident id -> Format.fprintf fmt "%s" id
78
    | Expr_ident id -> fprintf fmt "%s" id
79 79
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
80 80
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
81 81
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
82 82
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
83
    | Expr_ite (c, t, e) -> fprintf fmt "(if %a then %a else %a)" pp_expr c pp_expr t pp_expr e
83
    | Expr_ite (c, t, e) -> fprintf fmt "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])" pp_expr c pp_expr t pp_expr e
84 84
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
85 85
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
86 86
    | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
......
257 257

  
258 258
let pp_spec fmt spec =
259 259
  fprintf fmt "@[<hov 2>(*@@ ";
260
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;
261
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.ensures;
262
  fprintf_list ~sep:"@;" (fun fmt (name, assumes, ensures, _) -> 
260
  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;
261
  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.ensures;
262
  fprintf_list ~sep:"@," (fun fmt (name, assumes, ensures, _) -> 
263 263
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
264 264
      name
265 265
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
......
281 281
  | _ -> ()
282 282
    
283 283
let pp_node fmt nd = 
284
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[<v>%a@ %a@ %a@]@ @]@.tel@]@."
284
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@ %a%alet@[<h 2>   @ @[<v>%a@ %a@ %a@]@]@ tel@]@ "
285 285
  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
286
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.")
286
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@ ")
287 287
  (if nd.node_dec_stateless then "function" else "node")
288 288
  nd.node_id
289 289
  pp_node_args nd.node_inputs
......
349 349
  | Node _ -> assert false
350 350

  
351 351
let pp_lusi_header fmt basename prog =
352
  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@." basename;
353
  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@." Version.number pp_date (Unix.gmtime (Unix.time ()));
354
  fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@.@.";
355
  List.iter (fprintf fmt "%a@." pp_lusi) prog    
352
  fprintf fmt "@[<v 0>";
353
  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@ " basename;
354
  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@ " Version.number pp_date (Unix.gmtime (Unix.time ()));
355
  fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@ @ ";
356
  List.iter (fprintf fmt "%a@ " pp_lusi) prog;
357
  fprintf fmt "@]"
356 358

  
357 359
let pp_offset fmt offset =
358 360
  match offset with

Also available in: Unified diff