Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / compiler_stages.ml @ 5fccce23

History | View | Annotate | Download (11 KB)

1 04257b1e ploc
open Format
2
open Utils
3
open Compiler_common
4 8446bf03 ploc
open Lustre_types
5 04257b1e ploc
6 ad4774b0 ploc
exception StopPhase1 of program_t
7 04257b1e ploc
8
let dynamic_checks () =
9
  match !Options.output, !Options.spec with
10
  | "C", "C" -> true
11
  | _ -> false
12
     
13
14
(* check whether a source file has a compiled header, if not, generate the
15
   compiled header *)
16
let compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension =
17
  let destname = !Options.dest_dir ^ "/" ^ basename in
18
  let lusic_ext = extension ^ "c" in
19
  let header_name = destname ^ lusic_ext in
20
  begin
21
    if not (Sys.file_exists header_name) then
22
      begin
23
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
24
	Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
25 ad4774b0 ploc
	if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext
26 04257b1e ploc
      end
27
    else
28
      let lusic = Lusic.read_lusic destname lusic_ext in
29
      if not lusic.Lusic.from_lusi then
30
	begin
31
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
32
       	  Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
33
	  (*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
34 ad4774b0 ploc
	  if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext
35 04257b1e ploc
	end
36
      else
37
	begin
38
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
39 5fccce23 ploc
	  Lusic.check_obsolete lusic destname;
40 04257b1e ploc
	  let header = lusic.Lusic.contents in
41 5fccce23 ploc
	  let (declared_types_env, declared_clocks_env) = Modules.get_envs_from_top_decls header in
42 04257b1e ploc
	  check_compatibility
43
	    (prog, computed_types_env, computed_clocks_env)
44
	    (header, declared_types_env, declared_clocks_env)
45
	end
46
  end
47
48
49
(* From prog to prog *)
50 ad4774b0 ploc
let stage1 params prog dirname basename =
51 66359a5e ploc
  (* Updating parent node information for variables *)
52
  Compiler_common.update_vdecl_parents_prog prog;
53
54 04257b1e ploc
  (* Removing automata *)
55
  let prog = expand_automata prog in
56
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@,  @[<v 2>@,%a@]@ " Printers.pp_prog prog);
57
58
  (* Importing source *)
59 5fccce23 ploc
  let prog, dependencies, (typ_env, clk_env) = Modules.load ~is_header:false prog in
60 04257b1e ploc
61 5fccce23 ploc
  (* Registering types and clocks for future checks *)
62
  Global.type_env := Env.overwrite !Global.type_env typ_env;
63
  Global.clock_env := Env.overwrite !Global.clock_env clk_env;
64
  
65
  (* (\* Extracting dependencies (and updating Global.(type_env/clock_env) *\)
66
   * let dependencies = import_dependencies prog in *)
67 04257b1e ploc
68
  (* Sorting nodes *)
69
  let prog = SortProg.sort prog in
70
71
  (* Perform inlining before any analysis *)
72
  let orig, prog =
73
    if !Options.global_inline && !Options.main_node <> "" then
74
      (if !Options.witnesses then prog else []),
75 2d27eedd ploc
      Inliner.global_inline basename prog 
76 04257b1e ploc
    else (* if !Option.has_local_inline *)
77
      [],
78
      Inliner.local_inline prog (* type_env clock_env *)
79
  in
80
81
  (* Checking stateless/stateful status *)
82
  if Plugins.check_force_stateful () then
83
    force_stateful_decls prog
84
  else
85
    check_stateless_decls prog;
86
87
  (* Typing *)
88 2d27eedd ploc
  Global.type_env := type_decls !Global.type_env prog;
89 04257b1e ploc
90
  (* Clock calculus *)
91 2d27eedd ploc
  Global.clock_env := clock_decls !Global.clock_env prog;
92 04257b1e ploc
93 66359a5e ploc
  (* Registering and checking machine types *)
94 f4050bef ploc
  if Machine_types.is_active then Machine_types.load prog;
95 66359a5e ploc
  
96
97 04257b1e ploc
  (* Generating a .lusi header file only *)
98
  if !Options.lusi then
99
    (* We stop here the processing and produce the current prog. It will be
100
       exported as a lusi *)
101
    raise (StopPhase1 prog);
102
103
  (* Optimization of prog: 
104
     - Unfold consts 
105
     - eliminate trivial expressions
106
  *)
107
  (*
108
    let prog = 
109
    if !Options.const_unfold || !Options.optimization >= 5 then
110
    begin
111
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
112
    Optimize_prog.prog_unfold_consts prog
113
    end
114
    else
115
    prog
116
    in
117
  *)
118
  (* Delay calculus *)
119
  (* TO BE DONE LATER (Xavier)
120
     if(!Options.delay_calculus)
121
     then
122
     begin
123
     Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
124
     try
125
     Delay_calculus.delay_prog Basic_library.delay_env prog
126
     with (Delay.Error (loc,err)) as exc ->
127
     Location.print loc;
128
     eprintf "%a" Delay.pp_error err;
129
     Utils.track_exception ();
130
     raise exc
131
     end;
132
  *)
133
134
  (* Creating destination directory if needed *)
135
  create_dest_dir ();
136
137
  (* Compatibility with Lusi *)
138
  (* Checking the existence of a lusi (Lustre Interface file) *)
139
  let extension = ".lusi" in
140 2d27eedd ploc
  compile_source_to_header prog !Global.type_env !Global.clock_env dirname basename extension;
141 04257b1e ploc
142
  Typing.uneval_prog_generics prog;
143
  Clock_calculus.uneval_prog_generics prog;
144
145 66359a5e ploc
146 2d27eedd ploc
(* Disabling witness option. Could but reactivated later 
147 04257b1e ploc
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
148
    begin
149
      let orig = Corelang.copy_prog orig in
150
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
151
      check_stateless_decls orig;
152
      let _ = Typing.type_prog type_env orig in
153
      let _ = Clock_calculus.clock_prog clock_env orig in
154
      Typing.uneval_prog_generics orig;
155
      Clock_calculus.uneval_prog_generics orig;
156
      Inliner.witness
157
	basename
158
	!Options.main_node
159
	orig prog type_env clock_env
160
    end;
161 2d27eedd ploc
*)  
162
163 04257b1e ploc
  (* Computes and stores generic calls for each node,
164
     only useful for ANSI C90 compliant generic node compilation *)
165
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
166
  (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with
167
    Corelang.Node nd -> Format.eprintf "%s calls %a" id
168
    Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
169
170
  (* If some backend involving dynamic checks are active, then node annotations become runtime checks *)
171
  let prog =
172
    if dynamic_checks () then
173
      Spec.enforce_spec_prog prog
174
    else
175
      prog
176
  in
177 66359a5e ploc
178
179
  (* (\* Registering and checking machine types *\) *)
180
  (* Machine_types.load prog; *)
181
182 04257b1e ploc
  (* Normalization phase *)
183
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
184 ad4774b0 ploc
  let prog = Normalization.normalize_prog params prog in
185 04257b1e ploc
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
186
187
  let prog =
188
    if !Options.mpfr
189
    then
190
      begin
191
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
192
	Mpfr.inject_prog prog
193
      end
194
    else
195
      begin
196
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
197
	prog
198
      end in
199
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
200
201
  (* Checking array accesses *)
202
  if !Options.check then
203
    begin
204
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
205
      Access.check_prog prog;
206
    end;
207
208 66359a5e ploc
  
209 70466917 ploc
  let prog = SortProg.sort_nodes_locals prog in
210
  
211 04257b1e ploc
  prog, dependencies
212 66359a5e ploc
213
214
    (* from source to machine code, with optimization *)
215
let stage2 prog =    
216
  (* Computation of node equation scheduling. It also breaks dependency cycles
217
     and warns about unused input or memory variables *)
218
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
219
  let prog, node_schs =
220
    try 
221
      Scheduling.schedule_prog prog
222
    with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
223
				 systemtic way in AlgebraicLoop module *)
224
      AlgebraicLoop.analyze prog
225
  in
226
  Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
227
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
228
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
229
  Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
230
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
231
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
232
233
  (* TODO Salsa optimize prog: 
234
     - emits warning for programs with pre inside expressions
235
     - make sure each node arguments and memory is bounded by a local annotation
236
     - introduce fresh local variables for each real pure subexpression
237
  *)
238
  (* DFS with modular code generation *)
239
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
240
  let machine_code = Machine_code.translate_prog prog node_schs in
241
242 2863281f ploc
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ " Machine_code_common.pp_machines machine_code);
243 66359a5e ploc
244
  (* Optimize machine code *)
245 8e6cab20 ploc
  Optimize_machine.optimize prog node_schs machine_code   
246 66359a5e ploc
247
248
(* printing code *)
249
let stage3 prog machine_code dependencies basename =
250
  let basename    =  Filename.basename basename in
251
  match !Options.output with
252
    "C" -> 
253
      begin
254
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
255
	C_backend.translate_to_c
256
	  (* alloc_header_file source_lib_file source_main_file makefile_file *)
257
	  basename prog machine_code dependencies
258
      end
259
  | "java" ->
260
     begin
261
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
262
     (*let source_file = basename ^ ".java" in
263
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
264
       let source_out = open_out source_file in
265
       let source_fmt = formatter_of_out_channel source_out in
266
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
267
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
268
     end
269
  | "horn" ->
270
     begin
271
       let destname = !Options.dest_dir ^ "/" ^ basename in
272
       let source_file = destname ^ ".smt2" in (* Could be changed *)
273
       let source_out = open_out source_file in
274
       let fmt = formatter_of_out_channel source_out in
275
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
276 2863281f ploc
       Horn_backend.translate fmt basename prog (Machine_code_common.arrow_machine::machine_code);
277 66359a5e ploc
       (* Tracability file if option is activated *)
278
       if !Options.traces then (
279
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
280
	 let traces_out = open_out traces_file in
281
	 let fmt = formatter_of_out_channel traces_out in
282
         Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
283
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
284
       )
285
     end
286
  | "lustre" ->
287
     begin
288
       let destname = !Options.dest_dir ^ "/" ^ basename in
289
       let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
290
       let source_out = open_out source_file in
291
       let fmt = formatter_of_out_channel source_out in
292
       Printers.pp_prog fmt prog;
293
       Format.fprintf fmt "@.@?";
294
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
295
       ()
296
     end
297
  | "emf" ->
298
     begin
299
       let destname = !Options.dest_dir ^ "/" ^ basename in
300
       let source_file = destname ^ ".emf" in (* Could be changed *)
301
       let source_out = open_out source_file in
302
       let fmt = formatter_of_out_channel source_out in
303
       EMF_backend.translate fmt basename prog machine_code;
304
       ()
305
     end
306
307
  | _ -> assert false