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

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

Update of D2.2 from Paris.

File size: 7.5 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  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_incr) = ClightAnnotator.instrument p costs_mapping in
203    (AstClight p', cost_incr)
204  | AstCminor p ->
205    let (p', cost_incr) = CminorAnnotator.instrument p costs_mapping in
206    (AstCminor p', 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    ASMPrinter.print_program p
235
236let save exact_output filename 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_filename =
243    ext_chopped_filename ^ "." ^ extension (language_of_ast ast) in
244  let output_filename =
245    if exact_output then ext_filename
246    else Misc.SysExt.alternative ext_filename in
247  let cout = open_out output_filename in
248  output_string cout (string_output ast);
249  flush cout;
250  close_out cout
251
252let save_cost_incr filename cost_incr =
253  let cout = open_out (filename ^ ".cerco") in
254  output_string cout cost_incr;
255  flush cout;
256  close_out cout
257
258let interpret print_result = function
259  | AstClight p ->
260    ClightInterpret.interpret print_result p
261  | AstCminor p ->
262    CminorInterpret.interpret print_result p 
263  | AstRTLabs p ->
264    RTLabsInterpret.interpret print_result p
265  | AstRTL p ->
266    RTLInterpret.interpret print_result p
267  | AstERTL p ->
268    ERTLInterpret.interpret print_result p
269  | AstLTL p ->
270    LTLInterpret.interpret print_result p
271  | AstLIN p ->
272    LINInterpret.interpret print_result p
273  | AstASM p ->
274    ASMInterpret.interpret print_result p
Note: See TracBrowser for help on using the repository browser.