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

Last change on this file since 740 was 740, checked in by ayache, 10 years ago

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

File size: 7.8 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 = function
54  | Clight -> 
55    fun filename -> AstClight (ClightParser.process filename)
56
57  | Cminor -> 
58    fun filename -> 
59      AstCminor 
60        (SyntacticAnalysis.process
61           ~lexer_init: (fun filename -> Lexing.from_channel (open_in filename))
62           ~lexer_fun:  CminorLexer.token
63           ~parser_fun: CminorParser.program
64           ~input:      filename)
65
66  | _ ->
67    (* FIXME: Will be completed in the next commits. *)
68    assert false
69
70
71let labelize = function
72  | AstClight p -> 
73    AstClight (ClightLabelling.add_cost_labels p)
74
75  | AstCminor p -> 
76    AstCminor (CminorLabelling.add_cost_labels p)
77
78  | x -> 
79    (* For the other languages, no labelling is defined. *)
80    x
81
82
83let clight_to_cminor = function
84  | AstClight p ->
85    AstCminor (ClightToCminor.translate p)
86  | _ -> assert false
87
88let cminor_to_rtlabs = function
89  | AstCminor p -> 
90    AstRTLabs (CminorToRTLabs.translate p)
91  | _ -> assert false
92
93let rtlabs_to_rtl = function
94  | AstRTLabs p -> 
95    AstRTL (RTLabsToRTL.translate p)
96  | _ -> assert false
97
98let rtl_to_ertl = function
99  | AstRTL p -> 
100    AstERTL (RTLToERTL.translate p)
101  | _ -> assert false
102
103let ertl_to_ltl = function
104  | AstERTL p -> 
105    AstLTL (ERTLToLTL.translate p)
106  | _ -> assert false
107
108let ltl_to_lin = function
109  | AstLTL p -> 
110    AstLIN (LTLToLIN.translate p)
111  | _ -> assert false
112
113let lin_to_asm = function
114  | AstLIN p -> 
115    AstASM (LINToASM.translate p)
116  | _ -> assert false
117
118(* We explicitly denote the compilation chain as a list of
119   passes that must be composed to translate a program
120   from a source language to a target language. *)
121let compilation_chain = [
122  (* Source language | Target language | Compilation function *) 
123  Clight,              Cminor,           clight_to_cminor;
124  Cminor,              RTLabs,           cminor_to_rtlabs;
125  RTLabs,              RTL,              rtlabs_to_rtl;
126  RTL,                 ERTL,             rtl_to_ertl;
127  ERTL,                LTL,              ertl_to_ltl;
128  LTL,                 LIN,              ltl_to_lin;
129  LIN,                 ASM,              lin_to_asm;
130]
131
132let compile debug src tgt = 
133  (* Find the maximal suffix of the chain that starts with the
134     language [src]. *)
135  let rec subchain = function
136    | [] -> 
137      (* The chain is assumed to be well-formed: such a suffix
138         exists. *)
139      assert false 
140    | ((l, _, _) :: _) as chain when l = src -> chain
141    | _ :: chain -> subchain chain
142  in
143  (* Compose the atomic translations to build a compilation function
144     from [src] to [tgt]. Again, we assume that the compilation chain
145     is well-formed. Thus, if we cannot find [tgt] in the compilation
146     chain then the user must have made a mistake to ask for a
147     translation from [src] to [tgt]. *)
148  let rec compose iprogs src tgt chains = 
149    if src = tgt then 
150      fun _ -> List.rev iprogs
151    else 
152      match chains with
153        | [] -> 
154          Error.global_error "During compilation configuration"
155            (Printf.sprintf "It is not possible to compile from `%s' to `%s'."
156               (to_string src)
157               (to_string tgt))
158           
159        | (l1, l2, src_to_l2) :: chain ->
160          assert (l1 = src);
161          let l2_to_tgt = compose iprogs l2 tgt chain in
162          fun ast -> 
163            let iprog = src_to_l2 ast in
164            iprog :: l2_to_tgt iprog
165  in
166  if src = tgt then (fun ast -> [ast])
167  else
168    compose [] src tgt (subchain compilation_chain)
169
170
171let compute_costs = function
172  | AstClight p -> 
173  (* Computing costs on Clight programs cannot be done directly
174     because the control-flow is not explicit. Yet, for
175     incremental construction and test of the compiler, we
176     build a stupid mapping from labels to costs for a Clight
177     program that gives cost 1 to every label. *)
178    CostLabel.constant_map (ClightAnnotator.cost_labels p) 1
179
180  | AstCminor p -> 
181  (* Computing costs on Cminor programs cannot be done directly
182     because the control-flow is not explicit. Yet, for
183     incremental construction and test of the compiler, we
184     build a stupid mapping from labels to costs for a Cminor
185     program that gives cost 1 to every label. *)
186    CostLabel.constant_map (CminorAnnotator.cost_labels p) 1
187
188  | AstASM p ->
189    ASMCosts.compute p
190
191  | ast -> 
192    Error.global_error "during cost computing"
193      (Printf.sprintf
194         "Cost computing is not implemented for language `%s'\ 
195          Please compile to ASM if you want to annotate the input \
196          file or deactivate annotation using the '-no-annotation' flag."
197         (to_string (language_of_ast ast)))
198
199(* FIXME *)
200let instrument costs_mapping = function
201  | AstClight p ->
202    let (p', cost_id, cost_incr) = ClightAnnotator.instrument p costs_mapping in
203    (AstClight p', cost_id, cost_incr)
204  | AstCminor p ->
205    let (p', cost_id, cost_incr) = CminorAnnotator.instrument p costs_mapping in
206    (AstCminor p', cost_id, cost_incr)
207  | p -> 
208    Error.warning "during instrumentation"
209      (Printf.sprintf
210         "Instrumentation is not implemented for source language `%s'."
211         (to_string (language_of_ast p)));
212    (p, "", "")
213
214let annotate input_ast final = 
215  let costs_mapping = compute_costs final in 
216  instrument costs_mapping input_ast
217
218let string_output = function
219  | AstClight p -> 
220    [ClightPrinter.print_program p]
221  | AstCminor p ->
222    [CminorPrinter.print_program p]
223  | AstRTLabs p ->
224    [RTLabsPrinter.print_program p]
225  | AstRTL p ->
226    [RTLPrinter.print_program p]
227  | AstERTL p ->
228    [ERTLPrinter.print_program p]
229  | AstLTL p ->
230    [LTLPrinter.print_program p]
231  | AstLIN p ->
232    [LINPrinter.print_program p]
233  | AstASM p ->
234    [Pretty.print_program p ; ASMPrinter.print_program p]
235
236let save exact_output filename suffix ast =
237  let ext_chopped_filename =
238    if exact_output then filename
239    else
240      try Filename.chop_extension filename
241      with Invalid_argument ("Filename.chop_extension") -> filename in
242  let ext_chopped_filename = ext_chopped_filename ^ suffix in
243  let ext_filenames =
244    List.map (fun ext -> ext_chopped_filename ^ "." ^ ext)
245      (extension (language_of_ast ast)) in
246  let output_filenames =
247    if exact_output then ext_filenames
248    else List.map Misc.SysExt.alternative ext_filenames in
249  let output_strings = string_output ast in
250  let f filename s =
251    let cout = open_out filename in
252    output_string cout s;
253    flush cout;
254    close_out cout in
255  List.iter2 f output_filenames output_strings
256
257let save_cost filename cost_id cost_incr =
258  let cout = open_out (filename ^ ".cerco") in
259  output_string cout (cost_id ^ "\n");
260  output_string cout (cost_incr ^ "\n");
261  flush cout;
262  close_out cout
263
264let interpret debug = function
265  | AstClight p ->
266    ClightInterpret.interpret debug p
267  | AstCminor p ->
268    CminorInterpret.interpret debug p 
269  | AstRTLabs p ->
270    RTLabsInterpret.interpret debug p
271  | AstRTL p ->
272    RTLInterpret.interpret debug p
273  | AstERTL p ->
274    ERTLInterpret.interpret debug p
275  | AstLTL p ->
276    LTLInterpret.interpret debug p
277  | AstLIN p ->
278    LINInterpret.interpret debug p
279  | AstASM p ->
280    ASMInterpret.interpret debug p
Note: See TracBrowser for help on using the repository browser.