Revision 66359a5e
Added by Pierre-Loïc Garoche about 7 years ago
src/main_lustre_compiler.ml | ||
---|---|---|
55 | 55 |
|
56 | 56 |
|
57 | 57 |
|
58 |
(* from source to machine code, with optimization *) |
|
59 |
let stage2 prog = |
|
60 |
(* Computation of node equation scheduling. It also breaks dependency cycles |
|
61 |
and warns about unused input or memory variables *) |
|
62 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ "); |
|
63 |
let prog, node_schs = |
|
64 |
try |
|
65 |
Scheduling.schedule_prog prog |
|
66 |
with Causality.Error _ -> (* Error is not kept. It is recomputed in a more |
|
67 |
systemtic way in AlgebraicLoop module *) |
|
68 |
AlgebraicLoop.analyze prog |
|
69 |
in |
|
70 |
Log.report ~level:1 (fun fmt -> fprintf fmt "%a" Scheduling.pp_warning_unused node_schs); |
|
71 |
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs); |
|
72 |
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs); |
|
73 |
Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs); |
|
74 |
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog); |
|
75 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ "); |
|
76 |
|
|
77 |
(* TODO Salsa optimize prog: |
|
78 |
- emits warning for programs with pre inside expressions |
|
79 |
- make sure each node arguments and memory is bounded by a local annotation |
|
80 |
- introduce fresh local variables for each real pure subexpression |
|
81 |
*) |
|
82 |
(* DFS with modular code generation *) |
|
83 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,"); |
|
84 |
let machine_code = Machine_code.translate_prog prog node_schs in |
|
85 |
|
|
86 |
Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ "Machine_code.pp_machines machine_code); |
|
87 |
|
|
88 |
(* Optimize machine code *) |
|
89 |
Optimize_machine.optimize prog node_schs machine_code |
|
90 |
|
|
91 |
|
|
92 |
(* printing code *) |
|
93 |
let stage3 prog machine_code dependencies basename = |
|
94 |
let basename = Filename.basename basename in |
|
95 |
match !Options.output with |
|
96 |
"C" -> |
|
97 |
begin |
|
98 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,"); |
|
99 |
C_backend.translate_to_c |
|
100 |
(* alloc_header_file source_lib_file source_main_file makefile_file *) |
|
101 |
basename prog machine_code dependencies |
|
102 |
end |
|
103 |
| "java" -> |
|
104 |
begin |
|
105 |
(Format.eprintf "internal error: sorry, but not yet supported !"; assert false) |
|
106 |
(*let source_file = basename ^ ".java" in |
|
107 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file); |
|
108 |
let source_out = open_out source_file in |
|
109 |
let source_fmt = formatter_of_out_channel source_out in |
|
110 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?"); |
|
111 |
Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*) |
|
112 |
end |
|
113 |
| "horn" -> |
|
114 |
begin |
|
115 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
|
116 |
let source_file = destname ^ ".smt2" in (* Could be changed *) |
|
117 |
let source_out = open_out source_file in |
|
118 |
let fmt = formatter_of_out_channel source_out in |
|
119 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,"); |
|
120 |
Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code); |
|
121 |
(* Tracability file if option is activated *) |
|
122 |
if !Options.traces then ( |
|
123 |
let traces_file = destname ^ ".traces.xml" in (* Could be changed *) |
|
124 |
let traces_out = open_out traces_file in |
|
125 |
let fmt = formatter_of_out_channel traces_out in |
|
126 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,"); |
|
127 |
Horn_backend_traces.traces_file fmt basename prog machine_code; |
|
128 |
) |
|
129 |
end |
|
130 |
| "lustre" -> |
|
131 |
begin |
|
132 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
|
133 |
let source_file = destname ^ ".lustrec.lus" in (* Could be changed *) |
|
134 |
let source_out = open_out source_file in |
|
135 |
let fmt = formatter_of_out_channel source_out in |
|
136 |
Printers.pp_prog fmt prog; |
|
137 |
Format.fprintf fmt "@.@?"; |
|
138 |
(* Lustre_backend.translate fmt basename normalized_prog machine_code *) |
|
139 |
() |
|
140 |
end |
|
141 |
| "emf" -> |
|
142 |
begin |
|
143 |
let destname = !Options.dest_dir ^ "/" ^ basename in |
|
144 |
let source_file = destname ^ ".emf" in (* Could be changed *) |
|
145 |
let source_out = open_out source_file in |
|
146 |
let fmt = formatter_of_out_channel source_out in |
|
147 |
EMF_backend.translate fmt basename prog machine_code; |
|
148 |
() |
|
149 |
end |
|
150 |
|
|
151 |
| _ -> assert false |
|
152 | 58 |
|
153 | 59 |
(* compile a .lus source file *) |
154 | 60 |
let rec compile_source dirname basename extension = |
... | ... | |
188 | 94 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,"); |
189 | 95 |
|
190 | 96 |
let machine_code = |
191 |
stage2 prog |
|
97 |
Compiler_stages.stage2 prog
|
|
192 | 98 |
in |
193 | 99 |
|
194 | 100 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ "); |
... | ... | |
207 | 113 |
|
208 | 114 |
let machine_code = Plugins.refine_machine_code prog machine_code in |
209 | 115 |
|
210 |
stage3 prog machine_code dependencies basename; |
|
116 |
Compiler_stages.stage3 prog machine_code dependencies basename;
|
|
211 | 117 |
begin |
212 | 118 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@."); |
213 | 119 |
(* We stop the process here *) |
Also available in: Unified diff
[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program