source: Deliverables/D2.2/8051/src/languages.ml @ 1462

Last change on this file since 1462 was 1462, checked in by ayache, 9 years ago

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size: 9.0 KB
Line 
1type name = 
2  | Clight
3  | Cminor
4  | RTLabs
5  | RTL
6  | ERTL
7  | LTL
8  | LIN
9  | ASM
10
11let strings = [
12  "Clight", Clight;
13  "Cminor", Cminor;
14  "RTLabs", RTLabs;
15  "RTL"   , RTL;
16  "ERTL"  , ERTL;
17  "LTL"   , LTL;
18  "LIN"   , LIN;
19  "ASM"   , ASM;
20]
21
22let from_string s = 
23  List.assoc s strings
24
25let to_string l = 
26  List.assoc l (Misc.ListExt.inv_assoc strings)
27
28type ast = 
29  | AstClight of Clight.program
30  | AstCminor of Cminor.program
31  | AstRTLabs of RTLabs.program
32  | AstRTL    of RTL.program
33  | AstERTL   of ERTL.program
34  | AstLTL    of LTL.program
35  | AstLIN    of LIN.program
36  | AstASM    of ASM.program
37
38let language_of_ast = function
39  | AstClight _ -> Clight
40  | AstCminor _ -> Cminor
41  | AstRTLabs _ -> RTLabs
42  | AstRTL _    -> RTL
43  | AstERTL _   -> ERTL
44  | AstLTL _    -> LTL
45  | AstLIN _    -> LIN
46  | AstASM _    -> ASM
47
48let extension = function
49  | ASM      -> ["s" ; "hex"]
50  | Clight   -> ["c"]
51  | language -> [to_string language]
52
53let parse ?is_lustre_file ?remove_lustre_externals = function
54  | Clight -> 
55    fun filename ->
56      AstClight
57        (ClightParser.process ?is_lustre_file ?remove_lustre_externals filename)
58
59(*
60  | Cminor ->
61    fun filename ->
62      AstCminor
63        (SyntacticAnalysis.process
64           ~lexer_init: (fun filename -> Lexing.from_channel (open_in filename))
65           ~lexer_fun:  CminorLexer.token
66           ~parser_fun: CminorParser.program
67           ~input:      filename)
68*)
69
70  | _ ->
71    (* FIXME: Will be completed in the next commits. *)
72    assert false
73
74
75let labelize = function
76  | AstClight p -> 
77    AstClight (ClightLabelling.add_cost_labels p)
78
79(*
80  | AstCminor p ->
81    AstCminor (CminorLabelling.add_cost_labels p)
82*)
83
84  | x -> 
85    (* For the other languages, no labelling is defined. *)
86    x
87
88
89let clight_to_cminor = function
90  | AstClight p ->
91    AstCminor (ClightToCminor.translate p)
92  | _ -> assert false
93
94let cminor_to_rtlabs = function
95  | AstCminor p -> 
96    AstRTLabs (CminorToRTLabs.translate p)
97  | _ -> assert false
98
99let rtlabs_to_rtl = function
100  | AstRTLabs p -> 
101    AstRTL (RTLabsToRTL.translate p)
102  | _ -> assert false
103
104let rtl_to_ertl = function
105  | AstRTL p -> 
106    AstERTL (RTLToERTL.translate p)
107  | _ -> assert false
108
109let ertl_to_ltl = function
110  | AstERTL p -> 
111    AstLTL (ERTLToLTL.translate p)
112  | _ -> assert false
113
114let ltl_to_lin = function
115  | AstLTL p ->
116    AstLIN (LTLToLIN.translate p)
117  | _ -> assert false
118
119let lin_to_asm = function
120  | AstLIN p ->
121    AstASM (LINToASM.translate p)
122  | _ -> assert false
123
124(* We explicitly denote the compilation chain as a list of
125   passes that must be composed to translate a program
126   from a source language to a target language. *)
127let compilation_chain = [
128  (* Source language | Target language | Compilation function *) 
129  Clight,              Cminor,           clight_to_cminor;
130  Cminor,              RTLabs,           cminor_to_rtlabs;
131  RTLabs,              RTL,              rtlabs_to_rtl;
132  RTL,                 ERTL,             rtl_to_ertl;
133  ERTL,                LTL,              ertl_to_ltl;
134  LTL,                 LIN,              ltl_to_lin;
135  LIN,                 ASM,              lin_to_asm;
136]
137
138let compile debug src tgt = 
139  (* Find the maximal suffix of the chain that starts with the
140     language [src]. *)
141  let rec subchain = function
142    | [] -> 
143      (* The chain is assumed to be well-formed: such a suffix
144         exists. *)
145      assert false 
146    | ((l, _, _) :: _) as chain when l = src -> chain
147    | _ :: chain -> subchain chain
148  in
149  (* Compose the atomic translations to build a compilation function
150     from [src] to [tgt]. Again, we assume that the compilation chain
151     is well-formed. Thus, if we cannot find [tgt] in the compilation
152     chain then the user must have made a mistake to ask for a
153     translation from [src] to [tgt]. *)
154  let rec compose iprogs src tgt chains ast = 
155    if src = tgt then List.rev (ast :: iprogs)
156    else 
157      match chains with
158        | [] -> 
159          Error.global_error "During compilation configuration"
160            (Printf.sprintf "It is not possible to compile from `%s' to `%s'."
161               (to_string src)
162               (to_string tgt))
163           
164        | (l1, l2, src_to_l2) :: chain ->
165          assert (l1 = src);
166          let l2_to_tgt = compose iprogs l2 tgt chain in
167          let iprog = src_to_l2 ast in
168          ast :: l2_to_tgt iprog
169  in
170  compose [] src tgt (subchain compilation_chain)
171
172
173(** [add_runtime ast] adds runtime functions for the operations not supported by
174    the target processor. *)
175let add_runtime = function
176  | AstClight p ->
177    AstClight (Runtime.replace_unsupported (ClightSwitch.simplify p))
178  | x -> 
179    (* For the other languages, no runtime functios are defined. *)
180    x
181
182
183let compute_costs = function
184  | AstClight p -> 
185  (* Computing costs on Clight programs cannot be done directly
186     because the control-flow is not explicit. Yet, for
187     incremental construction and test of the compiler, we
188     build a stupid mapping from labels to costs for a Clight
189     program that gives cost 1 to every label. *)
190    CostLabel.constant_map (ClightAnnotator.cost_labels p) 1
191
192  | AstCminor p -> 
193  (* Computing costs on Cminor programs cannot be done directly
194     because the control-flow is not explicit. Yet, for
195     incremental construction and test of the compiler, we
196     build a stupid mapping from labels to costs for a Cminor
197     program that gives cost 1 to every label. *)
198    CostLabel.constant_map (CminorAnnotator.cost_labels p) 1
199
200  | AstASM p ->
201    ASMCosts.compute p
202
203  | ast -> 
204    Error.global_error "during cost computing"
205      (Printf.sprintf
206         "Cost computing is not implemented for language `%s'\ 
207          Please compile to ASM if you want to annotate the input \
208          file or deactivate annotation using the '-no-annotation' flag."
209         (to_string (language_of_ast ast)))
210
211(* FIXME *)
212let instrument costs_mapping = function
213  | AstClight p ->
214    let (p', cost_id, cost_incr, extern_cost_variables) =
215      ClightAnnotator.instrument p costs_mapping in
216    (AstClight p', cost_id, cost_incr, extern_cost_variables)
217(*
218  | AstCminor p ->
219    let (p', cost_id, cost_incr) = CminorAnnotator.instrument p costs_mapping in
220    (AstCminor p', cost_id, cost_incr)
221*)
222  | p -> 
223    Error.warning "during instrumentation"
224      (Printf.sprintf
225         "Instrumentation is not implemented for source language `%s'."
226         (to_string (language_of_ast p)));
227    (p, "", "", StringTools.Map.empty)
228
229let annotate input_ast final =
230  let costs_mapping = compute_costs final in 
231  instrument costs_mapping input_ast
232
233let string_output asm_pretty = function
234  | AstClight p -> 
235    [ClightPrinter.print_program p]
236  | AstCminor p ->
237    [CminorPrinter.print_program p]
238  | AstRTLabs p ->
239    [RTLabsPrinter.print_program p]
240  | AstRTL p ->
241    [RTLPrinter.print_program p]
242  | AstERTL p ->
243    [ERTLPrinter.print_program p]
244  | AstLTL p ->
245    [LTLPrinter.print_program p]
246  | AstLIN p ->
247    [LINPrinter.print_program p]
248  | AstASM p ->
249    (if asm_pretty then [Pretty.print_program p]
250     else ["Pretty print not requested"]) @
251    [ASMPrinter.print_program p]
252
253let save asm_pretty exact_output filename suffix ast =
254  let ext_chopped_filename =
255    if exact_output then filename
256    else
257      try Filename.chop_extension filename
258      with Invalid_argument ("Filename.chop_extension") -> filename in
259  let ext_chopped_filename = ext_chopped_filename ^ suffix in
260  let ext_filenames =
261    List.map (fun ext -> ext_chopped_filename ^ "." ^ ext)
262      (extension (language_of_ast ast)) in
263  let output_filenames =
264    if exact_output then ext_filenames
265    else List.map Misc.SysExt.alternative ext_filenames in
266  let output_strings = string_output asm_pretty ast in
267  let f filename s =
268    let cout = open_out filename in
269    output_string cout s;
270    flush cout;
271    close_out cout in
272  List.iter2 f output_filenames output_strings
273
274let save_cost exact_name filename cost_id cost_incr extern_cost_variables =
275  let filename =
276    if exact_name then filename
277    else
278      try Filename.chop_extension filename
279      with Invalid_argument ("Filename.chop_extension") -> filename in
280  let cout = open_out (filename ^ ".cerco") in
281  let f fun_name cost_var =
282    output_string cout (fun_name ^ " " ^ cost_var ^ "\n") in
283  output_string cout (cost_id ^ "\n");
284  output_string cout (cost_incr ^ "\n");
285  StringTools.Map.iter f extern_cost_variables;
286  flush cout;
287  close_out cout
288
289let interpret debug = function
290  | AstClight p ->
291    ClightInterpret.interpret debug p
292  | AstCminor p ->
293    CminorInterpret.interpret debug p 
294  | AstRTLabs p ->
295    RTLabsInterpret.interpret debug p
296  | AstRTL p ->
297    RTLInterpret.interpret debug p
298  | AstERTL p ->
299    ERTLInterpret.interpret debug p
300  | AstLTL p ->
301    LTLInterpret.interpret debug p
302  | AstLIN p ->
303    LINInterpret.interpret debug p
304  | AstASM p ->
305    ASMInterpret.interpret debug p
306
307let add_lustre_main
308    lustre_test lustre_test_cases lustre_test_cycles
309    lustre_test_min_int lustre_test_max_int = function
310  | AstClight p ->
311    AstClight
312      (ClightLustreMain.add lustre_test lustre_test_cases lustre_test_cycles
313         lustre_test_min_int lustre_test_max_int p)
314  | _ ->
315    Error.global_error "during main generation"
316      "Lustre testing is only available with C programs."
Note: See TracBrowser for help on using the repository browser.