Project

General

Profile

Revision 3769b712 src/compiler_stages.ml

View differences:

src/compiler_stages.ml
1
open Lustrec
1 2
open Format
2
open Utils
3
open Lustrec.Utils
3 4
open Compiler_common
4
open Lustre_types
5
open Lustrec.Lustre_types
5 6
module Mpfr = Lustrec_mpfr
6 7

  
7 8
exception StopPhase1 of program_t
8 9

  
9 10
let dynamic_checks () =
10
  match !Options.output, !Options.spec with
11
  match !Lustrec.Options.output, !Lustrec.Options.spec with
11 12
  | "C", "C" -> true
12 13
  | _ -> false
13 14

  
......
15 16
(* check whether a source file has a compiled header, if not, generate the
16 17
   compiled header *)
17 18
let compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension =
18
  let destname = !Options.dest_dir ^ "/" ^ basename in
19
  let destname = !Lustrec.Options.dest_dir ^ "/" ^ basename in
19 20
  let lusic_ext = ".lusic" in
20 21
  let header_name = destname ^ lusic_ext in
21 22
  begin
......
30 31
            has te be regenerated *)
31 32
    then
32 33
      begin
33
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
34
	Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
34 35
	Lusic.write_lusic
35 36
          (extension = ".lusi") (* is it a lusi file ? *)
36 37
          (if extension = ".lusi" then prog else Lusic.extract_header dirname basename prog)
37 38
          destname
38 39
          lusic_ext;
39 40
        let _ =
40
          match !Options.output with
41
          match !Lustrec.Options.output with
41 42
          | "C" -> C_backend_lusic.print_lusic_to_h destname lusic_ext
42 43
          | _ -> ()
43 44
        in
......
45 46
      end
46 47
    else (* Lusic exists and is usable. Checking compatibility *)
47 48
      begin
48
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
49
	Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
49 50
        let lusic = Lusic.read_lusic destname lusic_ext in
50 51
        Lusic.check_obsolete lusic destname;
51 52
	let header = lusic.Lusic.contents in
......
64 65

  
65 66
  (* Removing automata *)
66 67
  let prog = expand_automata prog in
67
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@,  @[<v 2>@,%a@]@ " Printers.pp_prog prog);
68
  Lustrec.Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@,  @[<v 2>@,%a@]@ " Lustrec.Printers.pp_prog prog);
68 69

  
69 70
  (* Importing source *)
70 71
  let prog, dependencies, (typ_env, clk_env) = Modules.load ~is_header:(extension = ".lusi") prog in
71 72
  (* Registering types and clocks for future checks *)
72
  Global.type_env := Env.overwrite !Global.type_env typ_env;
73
  Global.clock_env := Env.overwrite !Global.clock_env clk_env;
73
  Lustrec.Global.type_env := Lustrec.Env.overwrite !Lustrec.Global.type_env typ_env;
74
  Lustrec.Global.clock_env := Lustrec.Env.overwrite !Lustrec.Global.clock_env clk_env;
74 75
  
75
  (* (\* Extracting dependencies (and updating Global.(type_env/clock_env) *\)
76
  (* (\* Extracting dependencies (and updating Lustrec.Global.(type_env/clock_env) *\)
76 77
   * let dependencies = import_dependencies prog in *)
77 78

  
78 79
  (* Sorting nodes *)
......
80 81
  (* Consolidating contracts *)
81 82
  let prog = resolve_contracts prog in
82 83
  let prog = SortProg.sort prog in
83
  Log.report ~level:3 (fun fmt ->
84
      Format.fprintf fmt "@[<v 0>Contracts resolved:@ %a@ @]@ " Printers.pp_prog prog);
84
  Lustrec.Log.report ~level:3 (fun fmt ->
85
      Format.fprintf fmt "@[<v 0>Contracts resolved:@ %a@ @]@ " Lustrec.Printers.pp_prog prog);
85 86

  
86 87
  (* Consolidating main node *)
87 88
  let _ =
88
    match !Options.main_node with
89
    match !Lustrec.Options.main_node with
89 90
    | "" -> ()
90 91
    | main_node -> (
91
      Global.main_node := main_node;
92
      Lustrec.Global.main_node := main_node;
92 93
      try
93
        ignore (Corelang.node_from_name main_node)
94
        ignore (Lustrec.Corelang.node_from_name main_node)
94 95
      with Not_found -> (
95
        Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
96
        raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
96
        Format.eprintf "Code generation error: %a@." Lustrec.Error.pp_error_msg Lustrec.Error.Main_not_found;
97
        raise (Error.Error (Lustrec.Location.dummy_loc,Lustrec.Error.Main_not_found))
97 98
    ))
98 99
  in
99 100
  
100 101
  (* Perform inlining before any analysis *)
101 102
  let orig, prog =
102
    if !Options.global_inline && !Global.main_node <> "" then
103
      (if !Options.witnesses then prog else []),
103
    if !Lustrec.Options.global_inline && !Lustrec.Global.main_node <> "" then
104
      (if !Lustrec.Options.witnesses then prog else []),
104 105
      Inliner.global_inline basename prog
105 106
    else (* if !Option.has_local_inline *)
106 107
      [],
......
114 115
    check_stateless_decls prog;
115 116

  
116 117
  (* Typing *)
117
  Global.type_env := type_decls !Global.type_env prog;
118
  Lustrec.Global.type_env := type_decls !Lustrec.Global.type_env prog;
118 119

  
119 120
  (* Clock calculus *)
120
  Global.clock_env := clock_decls !Global.clock_env prog;
121
  Lustrec.Global.clock_env := clock_decls !Lustrec.Global.clock_env prog;
121 122

  
122 123
  (* Registering and checking machine types *)
123 124
  if Machine_types.is_active then Machine_types.load prog;
124 125

  
125 126

  
126 127
  (* Generating a .lusi header file only *)
127
  if !Options.lusi || !Options.print_nodes then
128
  if !Lustrec.Options.lusi || !Lustrec.Options.print_nodes then
128 129
    (* We stop here the processing and produce the current prog. It will be
129 130
       exported as a lusi *)
130 131
    raise (StopPhase1 prog);
......
135 136
   *)
136 137
  
137 138
  let prog =
138
    if !Options.const_unfold || !Options.optimization >= 5 then
139
    if !Lustrec.Options.const_unfold || !Lustrec.Options.optimization >= 5 then
139 140
      begin
140
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
141
        Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
141 142
        Optimize_prog.prog_unfold_consts prog
142 143
      end
143 144
    else
......
146 147
  
147 148
  (* Delay calculus *)
148 149
  (* TO BE DONE LATER (Xavier)
149
     if(!Options.delay_calculus)
150
     if(!Lustrec.Options.delay_calculus)
150 151
     then
151 152
     begin
152
     Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
153
     Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
153 154
     try
154
     Delay_calculus.delay_prog Basic_library.delay_env prog
155
     with (Delay.Error (loc,err)) as exc ->
156
     Location.print loc;
157
     eprintf "%a" Delay.pp_error err;
158
     Utils.track_exception ();
155
     Delay_calculus.delay_prog Lustrec.Basic_library.delay_env prog
156
     with (Lustrec.Delay.Error (loc,err)) as exc ->
157
     Lustrec.Location.print loc;
158
     eprintf "%a" Lustrec.Delay.pp_error err;
159
     Lustrec.Utils.track_exception ();
159 160
     raise exc
160 161
     end;
161 162
   *)
......
168 169

  
169 170

  
170 171
  (* Disabling witness option. Could but reactivated later
171
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
172
  if !Lustrec.Options.global_inline && !Lustrec.Options.main_node <> "" && !Lustrec.Options.witnesses then
172 173
    begin
173
      let orig = Corelang.copy_prog orig in
174
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
174
      let orig = Lustrec.Corelang.copy_prog orig in
175
      Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
175 176
      check_stateless_decls orig;
176 177
      let _ = Typing.type_prog type_env orig in
177 178
      let _ = Clock_calculus.clock_prog clock_env orig in
......
179 180
      Clock_calculus.uneval_prog_generics orig;
180 181
      Inliner.witness
181 182
	basename
182
	!Options.main_node
183
	!Lustrec.Options.main_node
183 184
	orig prog type_env clock_env
184 185
    end;
185 186
   *)
186 187

  
187 188
  (* Computes and stores generic calls for each node,
188 189
     only useful for ANSI C90 compliant generic node compilation *)
189
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
190
  (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with
191
    Corelang.Node nd -> Format.eprintf "%s calls %a" id
192
    Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
190
  if !Lustrec.Options.ansi then Lustrec.Causality.NodeDep.compute_generic_calls prog;
191
  (*Hashtbl.iter (fun id td -> match td.Lustrec.Corelang.top_decl_desc with
192
    Lustrec.Corelang.Node nd -> Format.eprintf "%s calls %a" id
193
    Lustrec.Causality.NodeDep.pp_generic_calls nd | _ -> ()) Lustrec.Corelang.node_table;*)
193 194

  
194 195
  (* If some backend involving dynamic checks are active, then node annotations become runtime checks *)
195 196
  let prog =
......
203 204
  (* (\* Registering and checking machine types *\) *)
204 205
  (* Machine_types.load prog; *)
205 206

  
206
  (* Normalization phase *)
207
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
208
  let prog = Normalization.normalize_prog params prog in
209
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog_short prog);
210
  Log.report ~level:3  (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
207
  (* Lustrec.Normalization phase *)
208
  Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
209
  let prog = Lustrec.Normalization.normalize_prog params prog in
210
  Lustrec.Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Lustrec.Printers.pp_prog_short prog);
211
  Lustrec.Log.report ~level:3  (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Lustrec.Printers.pp_prog prog);
211 212
  
212 213
  (* Compatibility with Lusi *)
213 214
  (* If compiling a lusi, generate the lusic. If this is a lus file, Check the existence of a lusi (Lustre Interface file) *)
214
  if !Options.compile_header then
215
  if !Lustrec.Options.compile_header then
215 216
    compile_source_to_header
216
      prog !Global.type_env !Global.clock_env dirname basename extension;
217
      prog !Lustrec.Global.type_env !Lustrec.Global.clock_env dirname basename extension;
217 218

  
218 219

  
219 220
  let prog =
220
    if !Options.mpfr
221
    if !Lustrec.Options.mpfr
221 222
    then
222 223
      begin
223
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
224
	Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
224 225
	Mpfr.inject_prog prog
225 226
      end
226 227
    else
227 228
      begin
228
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
229
	Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
229 230
	prog
230 231
      end in
231
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
232
  Lustrec.Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Lustrec.Printers.pp_prog prog);
232 233

  
233 234
  (* Checking array accesses *)
234
  if !Options.check then
235
  if !Lustrec.Options.check then
235 236
    begin
236
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
237
      Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
237 238
      Access.check_prog prog;
238 239
    end;
239 240

  
......
247 248
let stage2 params prog =
248 249
  (* Computation of node equation scheduling. It also breaks dependency cycles
249 250
     and warns about unused input or memory variables *)
250
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
251
  Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
251 252
  let prog, node_schs =
252 253
    try
253 254
      Scheduling.schedule_prog prog
254
    with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
255
    with Lustrec.Causality.Error _ -> (*Lustrec.Error is not kept. It is recomputed in a more
255 256
				 systemtic way in AlgebraicLoop module *)
256 257
      AlgebraicLoop.analyze prog
257 258
  in
258
  Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
259
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
260
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
261
  Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
262
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
263
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
259
  Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
260
  Lustrec.Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
261
  Lustrec.Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
262
  Lustrec.Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
263
  Lustrec.Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Lustrec.Printers.pp_prog prog);
264
  Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
264 265

  
265 266
  (* TODO Salsa optimize prog:
266 267
     - emits warning for programs with pre inside expressions
......
268 269
     - introduce fresh local variables for each real pure subexpression
269 270
  *)
270 271
  (* DFS with modular code generation *)
271
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
272
  Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
272 273
  let machine_code = Machine_code.translate_prog prog node_schs in
273 274

  
274
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ " Machine_code_common.pp_machines machine_code);
275
  Lustrec.Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ " Lustrec.Machine_code_common.pp_machines machine_code);
275 276

  
276 277
  (* Optimize machine code *)
277 278
  Optimize_machine.optimize params prog node_schs machine_code
......
280 281
(* printing code *)
281 282
let stage3 prog machine_code dependencies basename extension =
282 283
  let basename    =  Filename.basename basename in
283
  match !Options.output, extension with
284
  match !Lustrec.Options.output, extension with
284 285
    "C", ".lus" -> 
285 286
     begin
286
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
287
       Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
287 288
       C_backend.translate_to_c
288 289
	 (* alloc_header_file source_lib_file source_main_file makefile_file *)
289 290
	 basename prog machine_code dependencies
290 291
     end
291 292
  |  "C", _ -> 
292 293
      begin
293
      	Log.report ~level:1 (fun fmt -> fprintf fmt ".. no C code generation for lusi@,");
294
      	Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. no C code generation for lusi@,");
294 295
      end
295 296
  | "java", _ ->
296 297
     begin
297 298
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
298 299
     (*let source_file = basename ^ ".java" in
299
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
300
       Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
300 301
       let source_out = open_out source_file in
301 302
       let source_fmt = formatter_of_out_channel source_out in
302
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
303
       Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
303 304
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
304 305
     end
305 306
  | "Ada", _ ->
306 307
    begin
307
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. Ada code generation@.");
308
      Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. Ada code generation@.");
308 309
      Ada_backend.translate_to_ada
309
      basename prog (Machine_code_common.arrow_machine::machine_code) dependencies
310
      basename prog (Lustrec.Machine_code_common.arrow_machine::machine_code) dependencies
310 311
    end
311 312
  | "horn", _ ->
312 313
     begin
313
       let destname = !Options.dest_dir ^ "/" ^ basename in
314
       let destname = !Lustrec.Options.dest_dir ^ "/" ^ basename in
314 315
       let source_file = destname ^ ".smt2" in (* Could be changed *)
315 316
       let source_out = open_out source_file in
316 317
       let fmt = formatter_of_out_channel source_out in
317
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
318
       Horn_backend.translate fmt basename prog (Machine_code_common.arrow_machine::machine_code);
318
       Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
319
       Horn_backend.translate fmt basename prog (Lustrec.Machine_code_common.arrow_machine::machine_code);
319 320
       (* Tracability file if option is activated *)
320
       if !Options.traces then (
321
       if !Lustrec.Options.traces then (
321 322
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
322 323
	 let traces_out = open_out traces_file in
323 324
	 let fmt = formatter_of_out_channel traces_out in
324
         Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
325
         Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
325 326
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
326 327
       )
327 328
     end
328 329
  | "lustre", _ ->
329 330
     begin
330
       let destname = !Options.dest_dir ^ "/" ^ basename in
331
       let destname = !Lustrec.Options.dest_dir ^ "/" ^ basename in
331 332
       let source_file = destname ^ ".lustrec" ^ extension  in (* Could be changed *)
332
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. exporting processed file as %s@," source_file);
333
       Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. exporting processed file as %s@," source_file);
333 334
       let source_out = open_out source_file in
334 335
       let fmt = formatter_of_out_channel source_out in
335
       Printers.pp_prog fmt prog;
336
       Lustrec.Printers.pp_prog fmt prog;
336 337
       Format.fprintf fmt "@.@?";
337 338
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
338 339
       ()
339 340
     end
340 341
  | "emf", _ ->
341 342
     begin
342
       let destname = !Options.dest_dir ^ "/" ^ basename in
343
       let destname = !Lustrec.Options.dest_dir ^ "/" ^ basename in
343 344
       let source_file = destname ^ ".json" in (* Could be changed *)
344 345
       let source_out = open_out source_file in
345 346
       let fmt = formatter_of_out_channel source_out in

Also available in: Unified diff