Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / compiler_stages.ml @ f9f06e7d

History | View | Annotate | Download (10.8 KB)

1
open Format
2
open Utils
3
open Compiler_common
4
open Lustre_types
5

    
6
exception StopPhase1 of program_t
7

    
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
	if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext
26
      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
	  if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext
35
	end
36
      else
37
	begin
38
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
39
	  Modules.check_dependency lusic destname;
40
	  let header = lusic.Lusic.contents in
41
	  let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in
42
	  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
let stage1 params prog dirname basename =
51
  (* Updating parent node information for variables *)
52
  Compiler_common.update_vdecl_parents_prog prog;
53

    
54
  (* 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
  let _ = Modules.load ~is_header:false ISet.empty prog in
60

    
61
  (* Extracting dependencies (and updating Global.(type_env/clock_env) *)
62
  let dependencies = import_dependencies prog in
63

    
64
  (* Sorting nodes *)
65
  let prog = SortProg.sort prog in
66

    
67
  (* Perform inlining before any analysis *)
68
  let orig, prog =
69
    if !Options.global_inline && !Options.main_node <> "" then
70
      (if !Options.witnesses then prog else []),
71
      Inliner.global_inline basename prog 
72
    else (* if !Option.has_local_inline *)
73
      [],
74
      Inliner.local_inline prog (* type_env clock_env *)
75
  in
76

    
77
  (* Checking stateless/stateful status *)
78
  if Plugins.check_force_stateful () then
79
    force_stateful_decls prog
80
  else
81
    check_stateless_decls prog;
82

    
83
  (* Typing *)
84
  Global.type_env := type_decls !Global.type_env prog;
85

    
86
  (* Clock calculus *)
87
  Global.clock_env := clock_decls !Global.clock_env prog;
88

    
89
  (* Registering and checking machine types *)
90
  if Machine_types.is_active then Machine_types.load prog;
91
  
92

    
93
  (* Generating a .lusi header file only *)
94
  if !Options.lusi then
95
    (* We stop here the processing and produce the current prog. It will be
96
       exported as a lusi *)
97
    raise (StopPhase1 prog);
98

    
99
  (* Optimization of prog: 
100
     - Unfold consts 
101
     - eliminate trivial expressions
102
  *)
103
  (*
104
    let prog = 
105
    if !Options.const_unfold || !Options.optimization >= 5 then
106
    begin
107
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
108
    Optimize_prog.prog_unfold_consts prog
109
    end
110
    else
111
    prog
112
    in
113
  *)
114
  (* Delay calculus *)
115
  (* TO BE DONE LATER (Xavier)
116
     if(!Options.delay_calculus)
117
     then
118
     begin
119
     Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
120
     try
121
     Delay_calculus.delay_prog Basic_library.delay_env prog
122
     with (Delay.Error (loc,err)) as exc ->
123
     Location.print loc;
124
     eprintf "%a" Delay.pp_error err;
125
     Utils.track_exception ();
126
     raise exc
127
     end;
128
  *)
129

    
130
  (* Creating destination directory if needed *)
131
  create_dest_dir ();
132

    
133
  (* Compatibility with Lusi *)
134
  (* Checking the existence of a lusi (Lustre Interface file) *)
135
  let extension = ".lusi" in
136
  compile_source_to_header prog !Global.type_env !Global.clock_env dirname basename extension;
137

    
138
  Typing.uneval_prog_generics prog;
139
  Clock_calculus.uneval_prog_generics prog;
140

    
141

    
142
(* Disabling witness option. Could but reactivated later 
143
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
144
    begin
145
      let orig = Corelang.copy_prog orig in
146
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
147
      check_stateless_decls orig;
148
      let _ = Typing.type_prog type_env orig in
149
      let _ = Clock_calculus.clock_prog clock_env orig in
150
      Typing.uneval_prog_generics orig;
151
      Clock_calculus.uneval_prog_generics orig;
152
      Inliner.witness
153
	basename
154
	!Options.main_node
155
	orig prog type_env clock_env
156
    end;
157
*)  
158

    
159
  (* Computes and stores generic calls for each node,
160
     only useful for ANSI C90 compliant generic node compilation *)
161
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
162
  (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with
163
    Corelang.Node nd -> Format.eprintf "%s calls %a" id
164
    Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
165

    
166
  (* If some backend involving dynamic checks are active, then node annotations become runtime checks *)
167
  let prog =
168
    if dynamic_checks () then
169
      Spec.enforce_spec_prog prog
170
    else
171
      prog
172
  in
173

    
174

    
175
  (* (\* Registering and checking machine types *\) *)
176
  (* Machine_types.load prog; *)
177

    
178
  (* Normalization phase *)
179
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
180
  let prog = Normalization.normalize_prog params prog in
181
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
182

    
183
  let prog =
184
    if !Options.mpfr
185
    then
186
      begin
187
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
188
	Mpfr.inject_prog prog
189
      end
190
    else
191
      begin
192
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
193
	prog
194
      end in
195
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
196

    
197
  (* Checking array accesses *)
198
  if !Options.check then
199
    begin
200
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
201
      Access.check_prog prog;
202
    end;
203

    
204
  
205
  let prog = SortProg.sort_nodes_locals prog in
206
  
207
  prog, dependencies
208

    
209

    
210
    (* from source to machine code, with optimization *)
211
let stage2 prog =    
212
  (* Computation of node equation scheduling. It also breaks dependency cycles
213
     and warns about unused input or memory variables *)
214
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
215
  let prog, node_schs =
216
    try 
217
      Scheduling.schedule_prog prog
218
    with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
219
				 systemtic way in AlgebraicLoop module *)
220
      AlgebraicLoop.analyze prog
221
  in
222
  Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
223
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
224
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
225
  Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
226
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
227
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
228

    
229
  (* TODO Salsa optimize prog: 
230
     - emits warning for programs with pre inside expressions
231
     - make sure each node arguments and memory is bounded by a local annotation
232
     - introduce fresh local variables for each real pure subexpression
233
  *)
234
  (* DFS with modular code generation *)
235
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
236
  let machine_code = Machine_code.translate_prog prog node_schs in
237

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

    
240
  (* Optimize machine code *)
241
  Optimize_machine.optimize prog node_schs machine_code   
242

    
243

    
244
(* printing code *)
245
let stage3 prog machine_code dependencies basename =
246
  let basename    =  Filename.basename basename in
247
  match !Options.output with
248
    "C" -> 
249
      begin
250
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
251
	C_backend.translate_to_c
252
	  (* alloc_header_file source_lib_file source_main_file makefile_file *)
253
	  basename prog machine_code dependencies
254
      end
255
  | "java" ->
256
     begin
257
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
258
     (*let source_file = basename ^ ".java" in
259
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
260
       let source_out = open_out source_file in
261
       let source_fmt = formatter_of_out_channel source_out in
262
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
263
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
264
     end
265
  | "horn" ->
266
     begin
267
       let destname = !Options.dest_dir ^ "/" ^ basename in
268
       let source_file = destname ^ ".smt2" in (* Could be changed *)
269
       let source_out = open_out source_file in
270
       let fmt = formatter_of_out_channel source_out in
271
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
272
       Horn_backend.translate fmt basename prog (Machine_code_common.arrow_machine::machine_code);
273
       (* Tracability file if option is activated *)
274
       if !Options.traces then (
275
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
276
	 let traces_out = open_out traces_file in
277
	 let fmt = formatter_of_out_channel traces_out in
278
         Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
279
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
280
       )
281
     end
282
  | "lustre" ->
283
     begin
284
       let destname = !Options.dest_dir ^ "/" ^ basename in
285
       let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
286
       let source_out = open_out source_file in
287
       let fmt = formatter_of_out_channel source_out in
288
       Printers.pp_prog fmt prog;
289
       Format.fprintf fmt "@.@?";
290
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
291
       ()
292
     end
293
  | "emf" ->
294
     begin
295
       let destname = !Options.dest_dir ^ "/" ^ basename in
296
       let source_file = destname ^ ".emf" in (* Could be changed *)
297
       let source_out = open_out source_file in
298
       let fmt = formatter_of_out_channel source_out in
299
       EMF_backend.translate fmt basename prog machine_code;
300
       ()
301
     end
302

    
303
  | _ -> assert false