source: Deliverables/D2.3/8051-memoryspaces-branch/src/languages.ml @ 460

Last change on this file since 460 was 460, checked in by campbell, 9 years ago

Port memory spaces changes to latest prototype compiler.

File size: 7.4 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"
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  compose [] src tgt (subchain compilation_chain)
167   
168
169let compute_costs = function
170  | AstClight p -> 
171  (* Computing costs on Clight programs cannot be done directly
172     because the control-flow is not explicit. Yet, for
173     incremental construction and test of the compiler, we
174     build a stupid mapping from labels to costs for a Clight
175     program that gives cost 1 to every label. *)
176    CostLabel.constant_map (ClightAnnotator.cost_labels p) 1
177
178  | AstCminor p -> 
179  (* Computing costs on Cminor programs cannot be done directly
180     because the control-flow is not explicit. Yet, for
181     incremental construction and test of the compiler, we
182     build a stupid mapping from labels to costs for a Cminor
183     program that gives cost 1 to every label. *)
184    CostLabel.constant_map (CminorAnnotator.cost_labels p) 1
185
186  | AstASM p ->
187    ASMCosts.compute p
188
189  | ast -> 
190    Error.global_error "during cost computing"
191      (Printf.sprintf
192         "Cost computing is not implemented for language `%s'\ 
193          Please compile to ASM if you want to annotate the input \
194          file or deactivate annotation using the '-no-annotation' flag."
195         (to_string (language_of_ast ast)))
196
197(* FIXME *)
198let instrument costs_mapping = function
199  | AstClight p -> 
200    AstClight (ClightAnnotator.instrument p costs_mapping)
201  | AstCminor p ->
202    AstCminor (CminorAnnotator.instrument p costs_mapping)
203  | p -> 
204    Error.warning "during instrumentation"
205      (Printf.sprintf
206         "Instrumentation is not implemented for source language `%s'."
207         (to_string (language_of_ast p)));
208    p
209
210let annotate input_ast final = 
211  let costs_mapping = compute_costs final in 
212  instrument costs_mapping input_ast
213
214let string_output = function
215  | AstClight p -> 
216    ClightPrinter.print_program p
217  | AstCminor p ->
218    CminorPrinter.print_program p
219  | AstRTLabs p ->
220    RTLabsPrinter.print_program p
221  | AstRTL p ->
222    RTLPrinter.print_program p
223  | AstERTL p ->
224    ERTLPrinter.print_program p
225  | AstLTL p ->
226    LTLPrinter.print_program p
227  | AstLIN p ->
228    LINPrinter.print_program p
229  | AstASM p ->
230    ASMPrinter.print_program p
231
232let save filename ast =
233  let output_filename = 
234    Misc.SysExt.alternative
235      (Filename.chop_extension filename
236       ^ "." ^ extension (language_of_ast ast))
237  in
238  let cout = open_out output_filename in
239  output_string cout (string_output ast);
240  flush cout;
241  close_out cout
242
243let rec find_clight = function
244| [] -> None
245| AstClight p :: t -> Some p
246| _::t -> find_clight t
247
248let save_matita filename asts =
249  match find_clight asts with
250  | None -> Error.warning "during matita output" "No Clight AST."
251  | Some prog -> begin
252    let output_filename = 
253      Misc.SysExt.alternative
254        (Filename.chop_extension filename
255         ^ ".ma")
256    in
257    let cout = open_out output_filename in
258    let fout = Format.formatter_of_out_channel cout in
259    ClightPrintMatita.print_program fout prog;
260    flush cout;
261    close_out cout
262  end
263
264let interpret = function
265  | AstClight p ->
266    ClightInterpret.interpret false p
267  | AstCminor p ->
268    CminorInterpret.interpret false p 
269  | AstRTLabs p ->
270    RTLabsInterpret.interpret p
271  | AstRTL p ->
272    RTLInterpret.interpret p
273  | AstERTL p ->
274    ERTLInterpret.interpret p
275  | AstLTL p ->
276    LTLInterpret.interpret p
277  | AstLIN p ->
278    LINInterpret.interpret p
279  | AstASM p ->
280    ASMInterpret.interpret p
Note: See TracBrowser for help on using the repository browser.