]> matita.cs.unibo.it Git - pkg-cerco/acc.git/blob - src/RTLabs/RTLabsToRTL.ml
Package description and copyright added.
[pkg-cerco/acc.git] / src / RTLabs / RTLabsToRTL.ml
1
2 (** This module provides a translation of [RTLabs] programs to [RTL]
3     programs. *)
4
5
6 let error_prefix = "RTLabs to RTL"
7 let error = Error.global_error error_prefix
8
9 let error_int () = error "int16 and int32 not supported."
10 let error_float () = error "float not supported."
11 let error_shift () = error "Shift operations not supported."
12
13
14 let change_entry def f_entry = { def with RTL.f_entry }
15
16 let add_graph lbl stmt def =
17   { def with RTL.f_graph = Label.Map.add lbl stmt def.RTL.f_graph }
18
19 let fresh_label def = Label.Gen.fresh def.RTL.f_luniverse
20
21 let fresh_reg def =
22   let r = Register.fresh def.RTL.f_runiverse in
23   let locals = Register.Set.add r def.RTL.f_locals in
24   ({ def with RTL.f_locals = locals }, r)
25
26 let rec fresh_regs def n =
27   if n = 0 then (def, [])
28   else
29     let (def, res) = fresh_regs def (n-1) in
30     let (def, r) = fresh_reg def in
31     (def, r :: res) 
32
33 let addr_regs regs = match regs with
34   | r1 :: r2 :: _ -> (r1, r2)
35   | _ -> error "registers are not an address."
36
37 let rec register_freshes runiverse n =
38   if n <= 0 then []
39   else (Register.fresh runiverse) :: (register_freshes runiverse (n-1)) 
40
41 let choose_rest rest1 rest2 = match rest1, rest2 with
42   | [], _ -> rest2
43   | _, [] -> rest1
44   | _ -> assert false (* do not use on these arguments *)
45
46 let complete_regs def srcrs1 srcrs2 =
47   let nb_added = (List.length srcrs1) - (List.length srcrs2) in
48   let (def, added_regs) = fresh_regs def nb_added in
49   if nb_added > 0 then (srcrs1, srcrs2 @ added_regs, added_regs)
50   else (srcrs1 @ added_regs, srcrs2, added_regs)
51
52
53 let size_of_sig_type = function
54   | AST.Sig_int (i, _) -> i / Driver.TargetArch.int_size
55   | AST.Sig_float _ -> error_float ()
56   | AST.Sig_offset -> Driver.TargetArch.int_size
57   | AST.Sig_ptr -> Driver.TargetArch.ptr_size
58
59 let concrete_size = Driver.RTLMemory.concrete_size
60
61 let concrete_offset = Driver.RTLMemory.concrete_offset
62
63
64 (* Local environments *)
65
66 type local_env = Register.t list Register.Map.t
67
68 let mem_local_env = Register.Map.mem
69 let add_local_env = Register.Map.add
70 let find_local_env = Register.Map.find
71
72 let initialize_local_env runiverse registers result =
73   let registers =
74     registers @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
75   let f lenv (r, t) =
76     let rs = register_freshes runiverse (size_of_sig_type t) in
77     add_local_env r rs lenv in
78   List.fold_left f Register.Map.empty registers
79
80 let map_list_local_env lenv regs =
81   let f res r = res @ (find_local_env r lenv) in
82   List.fold_left f [] regs
83
84 let make_addr = function
85   | r1 :: r2 :: _ -> (r1, r2)
86   | _ -> assert false (* do not use on these arguments *)
87
88 let find_and_addr r lenv = make_addr (find_local_env r lenv)
89
90 let rtl_args regs_list lenv =
91   List.flatten (List.map (fun r -> find_local_env r lenv) regs_list)
92
93
94 let change_label lbl = function
95   | RTL.St_skip _ -> RTL.St_skip lbl
96   | RTL.St_cost (cost_lbl, _) -> RTL.St_cost (cost_lbl, lbl)
97   | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl)
98   | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl)
99   | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl)
100   | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl)
101   | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, _) ->
102     RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl)
103   | RTL.St_op1 (op1, dstr, srcr, _) -> RTL.St_op1 (op1, dstr, srcr, lbl)
104   | RTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
105     RTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
106   | RTL.St_clear_carry _ -> RTL.St_clear_carry lbl
107   | RTL.St_set_carry _ -> RTL.St_set_carry lbl
108   | RTL.St_load (dstrs, addr1, addr2, _) ->
109     RTL.St_load (dstrs, addr1, addr2, lbl)
110   | RTL.St_store (addr1, addr2, srcrs, _) ->
111     RTL.St_store (addr1, addr2, srcrs, lbl)
112   | RTL.St_call_id (f, args, retrs, _) -> RTL.St_call_id (f, args, retrs, lbl)
113   | RTL.St_call_ptr (f1, f2, args, retrs, _) ->
114     RTL.St_call_ptr (f1, f2, args, retrs, lbl)
115   | RTL.St_tailcall_id (f, args) -> RTL.St_tailcall_id (f, args)
116   | RTL.St_tailcall_ptr (f1, f2, args) -> RTL.St_tailcall_ptr (f1, f2, args)
117   | RTL.St_cond _ as inst -> inst
118   | RTL.St_return regs -> RTL.St_return regs
119
120 (* Add a list of instruction in a graph, from one label to another, by creating
121    fresh labels inbetween. *)
122
123 let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with
124   | [] -> 
125     add_graph start_lbl (RTL.St_skip dest_lbl) def
126   | [stmt] ->
127     add_graph start_lbl (change_label dest_lbl stmt) def
128   | stmt :: stmt_list ->
129     let tmp_lbl = fresh_label def in
130     let stmt = change_label tmp_lbl stmt in
131     let def = add_graph start_lbl stmt def in
132     adds_graph stmt_list tmp_lbl dest_lbl def
133
134 let generates_graph stmt_list def =
135   let start_lbl = fresh_label def in
136   let dest_lbl = def.RTL.f_entry in
137   change_entry (adds_graph stmt_list start_lbl dest_lbl def) start_lbl
138
139 (* Process a list of function that adds a list of instructions to a graph, from
140    one label to another, and by creating fresh labels inbetween. *)
141
142 let rec add_translates translate_list start_lbl dest_lbl def =
143   match translate_list with
144     | [] -> 
145       add_graph start_lbl (RTL.St_skip dest_lbl) def
146     | [trans] -> 
147       trans start_lbl dest_lbl def
148     | trans :: translate_list ->
149       let tmp_lbl = fresh_label def in
150       let def = trans start_lbl tmp_lbl def in
151       add_translates translate_list tmp_lbl dest_lbl def
152
153
154 let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with
155
156   | AST.Cst_int _ when destrs = [] ->
157     add_graph start_lbl (RTL.St_skip dest_lbl) def
158
159   | AST.Cst_int i ->
160     let size = List.length destrs in
161     let module M = IntValue.Make (struct let size = size end) in
162     let is = List.map M.to_int (M.break (M.of_int i) size) in
163     let f r i = RTL.St_int (r, i, dest_lbl) in
164     let l = List.map2 f destrs is in
165     adds_graph l start_lbl dest_lbl def
166
167   | AST.Cst_float _ -> error_float ()
168
169   | AST.Cst_addrsymbol id ->
170     let (r1, r2) = make_addr destrs in
171     add_graph start_lbl (RTL.St_addr (r1, r2, id, dest_lbl)) def
172
173   | AST.Cst_stack ->
174     let (r1, r2) = make_addr destrs in
175     add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def
176
177   | AST.Cst_offset off ->
178     let i = concrete_offset off in
179     translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
180
181   | AST.Cst_sizeof size ->
182     let i = concrete_size size in
183     translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
184
185
186 (** Adds zeros if destination is bigger than source, or truncates if source is
187     bigger than destination. *)
188
189 let translate_move destrs srcrs start_lbl =
190   let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
191   let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
192   let translates1 = adds_graph (List.map2 f_common common1 common2) in
193   let translates2 = translate_cst (AST.Cst_int 0) rest1 in
194   add_translates [translates1 ; translates2] start_lbl
195
196 let translate_cast_unsigned destrs start_lbl dest_lbl def =
197   let (def, tmp_zero) = fresh_reg def in
198   let zeros = MiscPottier.make tmp_zero (List.length destrs) in
199   add_translates
200     [adds_graph [RTL.St_int (tmp_zero, 0, start_lbl)] ;
201      translate_move destrs zeros]
202     start_lbl dest_lbl def
203
204 (** [srcr] will be copied in the first register of [destrs]. The remaining
205     registers of [destrs] needs to be set either to zeros or to ones, depending
206     on the most significant bit of [srcr]. Since 8051 is a 8 bits architecture,
207     we fetch the most significant bit with [src & 10000000]. Let [tmpr] be the
208     result. Then we build zeros or ones with [tmpr * 11111111]. *)
209
210 let translate_cast_signed destrs srcr start_lbl dest_lbl def =
211   let (def, tmp_128) = fresh_reg def in
212   let (def, tmp_255) = fresh_reg def in
213   let (def, tmpr) = fresh_reg def in
214   let (def, dummy) = fresh_reg def in
215   let insts =
216     [RTL.St_int (tmp_128, 128, start_lbl) ;
217      RTL.St_op2 (I8051.And, tmpr, tmp_128, srcr, start_lbl) ;
218      RTL.St_opaccs (I8051.DivuModu, tmpr, dummy, tmpr, tmp_128, start_lbl) ;
219      RTL.St_int (tmp_255, 255, start_lbl) ;
220      RTL.St_opaccs (I8051.Mul, tmpr, dummy, tmpr, tmp_255, start_lbl)] in
221   let srcrs = MiscPottier.make tmpr (List.length destrs) in
222   add_translates [adds_graph insts ; translate_move destrs srcrs]
223     start_lbl dest_lbl def
224
225 (** Depending on [src_sign], perform either a signed or an unsigned cast. For
226     the signed case, we need the most significant bit of the source. *)
227
228 let translate_cast src_size src_sign dest_size destrs srcrs =
229   if List.length srcrs = 0 then adds_graph []
230   else
231     if dest_size < src_size then translate_move destrs srcrs
232     else
233       let ((common1, rest1), (common2, rest2)) =
234         MiscPottier.reduce destrs srcrs in
235       (* dest_size >= src_size, so there will be no rest2 *)
236       assert (rest2 = []) ;
237       let insts_common = translate_move common1 common2 in
238       let sign_reg = MiscPottier.last srcrs in
239       let insts_sign = match src_sign with
240         | AST.Unsigned -> translate_cast_unsigned rest1
241         | AST.Signed -> translate_cast_signed rest1 sign_reg in
242       add_translates [insts_common ; insts_sign]
243
244
245 (** [-x] is [~x] (the complement of [x]), and then propagating the carry if some
246     register of the result is greater or equal to 128 (10000000 in binary). *)
247
248 (** FIXME Nicolas: why is this correct? *)
249
250 let translate_negint destrs srcrs start_lbl dest_lbl def =
251   assert (List.length destrs = List.length srcrs) ;
252   let (def, tmpr) = fresh_reg def in
253   let f_cmpl destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
254   let insts_cmpl = List.map2 f_cmpl destrs srcrs in
255   let insts_init =
256     [RTL.St_set_carry start_lbl ;
257      RTL.St_int (tmpr, 0, start_lbl)] in
258   let f_add destr = RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl) in
259   let insts_add = List.map f_add destrs in
260   adds_graph (insts_cmpl @ insts_init @ insts_add)
261     start_lbl dest_lbl def
262
263
264 (** In order to know if a register is different from 0 or not, we can simply
265     substract it from 0 and fetch the carry bit: it is 0 if the register
266     contains 0, and 1 otherwise. By doing a | on the result of
267     the previous operation on every source register and starting with 0, the
268     result is either 0 if all the source registers contained 0, and 1
269     otherwise. Let [tmp_res] be this number; then, the result of [notbool] is
270     simply [tmp_res ^ 1]. *)
271
272 let translate_notbool destrs srcrs start_lbl dest_lbl def = match destrs with
273   | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
274   | destr :: destrs ->
275     (* [destr] will be set to either 0 or 1 (depending on [srcrs]), the
276        remaining destination registers [destrs] will be set to 0. *)
277     let (def, tmpr) = fresh_reg def in
278     let (def, tmp_srcrs) = fresh_regs def (List.length srcrs) in
279     let save_srcrs = translate_move tmp_srcrs srcrs in
280     let prologue = translate_cst (AST.Cst_int 0) (destr :: destrs) in
281     let f tmp_srcr =
282       [RTL.St_clear_carry start_lbl ;
283        RTL.St_int (tmpr, 0, start_lbl) ;
284        RTL.St_op2 (I8051.Sub, tmpr, tmpr, tmp_srcr, start_lbl) ;
285        RTL.St_int (tmpr, 0, start_lbl) ;
286        RTL.St_op2 (I8051.Addc, tmpr, tmpr, tmpr, start_lbl) ;
287        RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in
288     let insts = List.flatten (List.map f tmp_srcrs) in
289     let epilogue =
290       [RTL.St_int (tmpr, 1, start_lbl) ;
291        RTL.St_op2 (I8051.Xor, destr, destr, tmpr, start_lbl)] in
292     add_translates
293       [save_srcrs ; prologue ; adds_graph insts ; adds_graph epilogue]
294       start_lbl dest_lbl def
295
296
297 let translate_op1 op1 destrs srcrs start_lbl dest_lbl def = match op1 with
298
299   | AST.Op_cast ((src_size, src_sign), dest_size) ->
300     translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl
301       def
302
303   | AST.Op_negint ->
304     translate_negint destrs srcrs start_lbl dest_lbl def
305
306   | AST.Op_notbool ->
307     translate_notbool destrs srcrs start_lbl dest_lbl def
308
309   | AST.Op_notint ->
310     let f destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
311     let l = List.map2 f destrs srcrs in
312     adds_graph l start_lbl dest_lbl def
313
314   | AST.Op_ptrofint | AST.Op_intofptr | AST.Op_id ->
315     translate_move destrs srcrs start_lbl dest_lbl def
316
317
318 (** Apply a binary operation. The sources and destination registers may not have
319     the same size. When they do not, zero registers will be considered if
320     needed. Considers given a temporary register [tmpr] that plays the role of
321     the zero register. The destination registers can be one of the sources
322     registers. *)
323
324 let translate_op_ tmpr op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
325   (* The next few instructions allows to decompose the sources and destination
326      registers in sub-lists of the same size, and creating the remainings at
327      the same time. *)
328   let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) =
329     MiscPottier.reduce srcrs1 srcrs2 in
330   let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in
331   let ((destrs_common, destrs_rest), _) =
332     MiscPottier.reduce destrs srcrs1_common in
333   (* srcrs1_common and srcrs2_common have the same size, which is exactly the
334      one of the shortest list between srcrs1 and srcrs2. destrs_common and
335      destrs_rest are either destrs and empty if destrs is bigger than
336      srcrs1_common (and thus srcrs2_common), or destrs_common has the size of
337      srcrs1_common (and srcrs2_common) and destrs_rest is the remainings of
338      destrs. *)
339   let ((destrs_cted, destrs_rest), (srcrs_cted, _)) =
340     MiscPottier.reduce destrs_rest srcrs_rest in
341   (* destrs_cted is either empty or is the remainings of destrs that has the
342      same size of the remainings between the srcrs1 and srcrs2 when removed the
343      number of elements of the size of the shortest one. destrs_rest are the
344      remainings, if any. *)
345   let insts_init =
346     [RTL.St_clear_carry start_lbl ;
347      RTL.St_int (tmpr, 0, start_lbl)] in
348   let f_op destr srcr1 srcr2 =
349     RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
350   let insts_op =
351     MiscPottier.map3 f_op destrs_common srcrs1_common srcrs2_common in
352   let f_op_cted destr srcr =
353     RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in
354   let insts_op_cted = List.map2 f_op_cted destrs_cted srcrs_cted in
355   let f_rest destr =
356     RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in
357   let insts_rest = List.map f_rest destrs_rest in
358   adds_graph (insts_init @ insts_op @ insts_op_cted @ insts_rest)
359     start_lbl dest_lbl def
360
361 (** Same as [translate_op], but creates the zero register. *)
362
363 let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
364   let (def, tmpr) = fresh_reg def in
365   translate_op_ tmpr op destrs srcrs1 srcrs2 start_lbl dest_lbl def
366
367
368 (** Multiply a list of registers (list significant bits first) by a
369     register. The multiplication in 8051 of two registers is two registers: the
370     least and most significant bits of the result. When pultiplying a list of
371     registers with one register, we need to propagate the most significant bits
372     of an operation to the next one for addition. Example:
373
374     (i1 i2) * j = res11 (res12 + res21) 
375
376     where (res11, res12) = i1 * j and (res21, res22) = i2 * j. The result is
377     truncated by just forgetting about res22. *)
378
379 (* [dummy] is used to discard the most significant bits *)
380
381 let rec translate_mul1 dummy tmpr destrs srcrs1 srcr2 start_lbl =
382   match destrs, srcrs1 with
383     | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl
384     | [destr], [] ->
385       (* if there are no source register left, and only one destination
386          register, simply add the carry bit of a potential previous addition *)
387       adds_graph [RTL.St_int (tmpr, 0, start_lbl) ;
388                   RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]
389         start_lbl
390     | destr1 :: destr2 :: _, [] ->
391       (* if there are no source register left, but at least two destination
392          registers, adding the carry of the potential previous addition
393          may lead to another carry that needs to be propagated *)
394       add_translates
395         [adds_graph [RTL.St_int (tmpr, 0, start_lbl) ;
396                      RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl) ;
397                      RTL.St_op2 (I8051.Addc, destr2, tmpr, tmpr, start_lbl)]]
398         start_lbl
399     | [destr], srcr1 :: _ ->
400       (* if there are at least one source register, but only one destination
401          register, discard the most significant bits of the multiplication *)
402       adds_graph
403         [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ;
404          RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]
405         start_lbl
406     | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 ->
407       (* if there are at least one source register, and at least two destination
408          registers, the first destination register should hold the most
409          significant bits of the previous atomic multiplication. We need to add
410          to it the least significant bits of the current operation, and store
411          the most significant bits in the next destination register for the next
412          multiplication. *)
413       add_translates
414         [adds_graph
415             [RTL.St_opaccs
416                 (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ;
417              RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl)] ;
418          translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2]
419         start_lbl
420
421 (** Multiply the ith register of some source registers. The registers up to the
422     ith of the result should be set to 0, and the multiplication really starts
423     at the next one. The result of this operation is then added to the current
424     result of the full multiplication. *)
425
426 let translate_muli
427     dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates srcr2i =
428   let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in
429   translates @
430     (match tmp_destrs2 with
431       | [] -> []
432       | tmp_destr2 :: tmp_destrs2 ->
433         [adds_graph [RTL.St_clear_carry dummy_lbl] ;
434          translate_cst (AST.Cst_int 0) [tmpr] ;
435          translate_cst (AST.Cst_int 0) tmp_destrs ;
436          translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
437          translate_cst (AST.Cst_int 0) tmp_destrs1 ;
438          adds_graph [RTL.St_clear_carry dummy_lbl] ;
439          translate_op I8051.Addc destrs destrs tmp_destrs])
440
441 (** Multiplication, school-style: 
442
443     i1n ... i11 * j1m ... j11 =
444     i1n ... i11 * j11 +
445     i1n ... i12 0 * j12 +
446     i1n ... i13 0 0 * j13 +
447     ... *)
448
449 let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
450   (* dummy will be used to discard some unused results *)
451   let (def, dummy) = fresh_reg def in
452   let (def, tmpr) = fresh_reg def in
453   (* One line of the multiplication is stored in tmp_destrs. The result of the
454      full multiplication is accumulated in destrs. *)
455   let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
456   (* Source registers are copied into fresh source registers to avoid
457      overwriting if one of them is also the destination registers. *)
458   let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
459   let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in
460   let insts_init =
461     [translate_move fresh_srcrs1 srcrs1 ;
462      translate_move fresh_srcrs2 srcrs2 ;
463      translate_cst (AST.Cst_int 0) destrs] in
464   let f = translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
465   let insts_mul = MiscPottier.foldi f [] fresh_srcrs2 in
466   add_translates (insts_init @ insts_mul) start_lbl dest_lbl def
467
468
469 (** The 8051 performs division and modulo in a single operation. Depending on
470     the one we need (boolean [order]), we discard the other. *)
471
472 let translate_divumodu8 order destrs srcr1 srcr2 start_lbl dest_lbl def =
473   match destrs with
474     | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
475     | destr :: destrs ->
476       let (def, dummy) = fresh_reg def in
477       let (destr1, destr2) = if order then (destr, dummy) else (dummy, destr) in
478       let inst_div =
479         adds_graph [RTL.St_opaccs (I8051.DivuModu, destr1, destr2,
480                                    srcr1, srcr2, start_lbl)] in
481       let insts_rest = translate_cst (AST.Cst_int 0) destrs in
482       add_translates [inst_div ; insts_rest] start_lbl dest_lbl def
483
484
485 (** Only the first register of [destrs] will be used, the others will be set to
486     0. We compare in order the registers of both source registers and accumulate
487     the results in the first register of [destrs], with a | and initially set to
488     0. Two registers are equal if and only if substracting one with the other
489     and substracting the other with the one both lead to no carry. If one of the
490     source registers is bigger than the other, we compare the remainings with
491     0. We first copy the source registers into fresh ones, in case the
492     destination registers share some source registers. Example:
493
494     srcr11 ... srcr1n != srcr21 ... srcr2m =
495     carry(srcr11 - srcr21) | carry (srcr21 - srcr11) |
496     carry(srcr12 - srcr22) | carry (srcr22 - srcr12) |
497     ... *)
498
499 let translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def =
500   match destrs with
501     | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
502     | destr :: destrs ->
503       let (def, dummy) = fresh_reg def in
504       let (def, tmp_zero) = fresh_reg def in
505       let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in
506       let save_srcrs1 = translate_move tmp_srcrs1 srcrs1 in
507       let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in
508       let save_srcrs2 = translate_move tmp_srcrs2 srcrs2 in
509       let ((common1, rest1), (common2, rest2)) =
510         MiscPottier.reduce tmp_srcrs1 tmp_srcrs2 in
511       let rest = choose_rest rest1 rest2 in
512       let inits =
513         [RTL.St_int (destr, 0, start_lbl) ;
514          RTL.St_int (tmp_zero, 0, start_lbl)] in
515       let f tmp_srcr1 tmp_srcr2 =
516         [RTL.St_clear_carry start_lbl ;
517          RTL.St_op2 (I8051.Sub, dummy, tmp_srcr1, tmp_srcr2, start_lbl) ;
518          RTL.St_op2 (I8051.Or, destr, destr, tmp_zero, start_lbl) ;
519          RTL.St_op2 (I8051.Sub, dummy, tmp_srcr2, tmp_srcr1, start_lbl) ;
520          RTL.St_op2 (I8051.Or, destr, destr, tmp_zero, start_lbl)] in
521       let insts_common = List.flatten (List.map2 f common1 common2) in
522       let insts_rest = List.flatten (List.map (f tmp_zero) rest) in
523       let insts = inits @ insts_common @ insts_rest in
524       let epilogue = translate_cst (AST.Cst_int 0) destrs in
525       add_translates [save_srcrs1 ; save_srcrs2 ; adds_graph insts ; epilogue]
526         start_lbl dest_lbl def
527
528
529 (** Are two given registers equal? We substract the one with the other, and then
530     the other with the one. They are equal if and only if both carry are 0,
531     i.e., a bitwise 'or' on the carries is 1 if and only if they are
532     different. We simply do a bitwise xor with this result and 1 to have our
533     answer:
534
535     r1 == r2 = (carry(r1 - r2) | carry(r2 - r1)) ^ 1 *)
536
537 let translate_eq_reg
538     tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl (srcr1, srcr2) =
539   [RTL.St_clear_carry dummy_lbl ;
540    RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ;
541    RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ;
542    RTL.St_clear_carry dummy_lbl ;
543    RTL.St_op2 (I8051.Sub, tmpr2, srcr2, srcr1, dummy_lbl) ;
544    RTL.St_op2 (I8051.Addc, tmpr2, tmp_zero, tmp_zero, dummy_lbl) ;
545    RTL.St_op2 (I8051.Or, tmpr1, tmpr1, tmpr2, dummy_lbl) ;
546    RTL.St_op2 (I8051.Xor, tmpr1, tmpr1, tmp_one, dummy_lbl) ;
547    RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)]
548
549 let translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 destr leq dummy_lbl =
550   let f = translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
551   (RTL.St_int (destr, 1, dummy_lbl)) :: (List.flatten (List.map f leq))
552
553 (** Translation of unsigned LT: we proceed by successively comparing the source
554     registers most significant bits first (if one of the two source lists is
555     smaller than the other, we complete it with zeros). At each step, a register
556     ([tmpr3]) holds 1 if the previous registers are all equal, and 0
557     otherwise. The result of the comparison is 1 if there is a step where all
558     the previous registers are equal and the first current register is lower
559     than the second (which is checked by substracting the second to the first
560     and fetching the carry). *)
561
562 let translate_atom
563     tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 =
564   (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @
565     [RTL.St_clear_carry dummy_lbl ;
566      RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ;
567      RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ;
568      RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ;
569      RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)]
570
571 let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl
572     srcrs1 srcrs2 =
573   let f (insts, leq) srcr1 srcr2 =
574     let added_insts =
575       translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq
576         srcr1 srcr2 in
577     (insts @ added_insts, leq @ [(srcr1, srcr2)]) in
578   fst (List.fold_left2 f ([], []) srcrs1 srcrs2)
579
580 let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def =
581   match destrs with
582     | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
583     | _ ->
584       let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
585       let tmp_destr = List.hd tmp_destrs in
586       let (def, tmp_zero) = fresh_reg def in
587       let (def, tmp_one) = fresh_reg def in
588       let (def, tmpr1) = fresh_reg def in
589       let (def, tmpr2) = fresh_reg def in
590       let (def, tmpr3) = fresh_reg def in
591       let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in
592       let srcrs1 = List.rev srcrs1 in
593       let srcrs2 = List.rev srcrs2 in
594       let insts_init =
595         [translate_cst (AST.Cst_int 0) tmp_destrs ;
596          translate_cst (AST.Cst_int 0) added ;
597          adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ;
598                      RTL.St_int (tmp_one, 1, start_lbl)]] in
599       let insts_main =
600         translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl
601           srcrs1 srcrs2 in
602       let insts_main = [adds_graph insts_main] in
603       let insts_exit = [translate_move destrs tmp_destrs] in
604       add_translates (insts_init @ insts_main @ insts_exit )
605         start_lbl dest_lbl def
606
607
608 (** Translation of signed LT: exactly unsigned LT when the signed bit is
609     changed: positive numbers become greater than the half bound as unsigned,
610     negative numbers become between 0 and the half bound as unsigned. The sign
611     bit is changed with a bitwise xor between the register holding the bit sign
612     (the most significant register, i.e. the last register in the list of
613     registers) and 10000000. *)
614
615 let add_128_to_last tmp_128 rs start_lbl = match rs with
616   | [] -> adds_graph [] start_lbl
617   | _ ->
618     let r = MiscPottier.last rs in
619     adds_graph [RTL.St_op2 (I8051.Xor, r, r, tmp_128, start_lbl)] start_lbl
620
621 let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def =
622   let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in
623   let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in
624   let (def, tmp_128) = fresh_reg def in
625   add_translates
626     [translate_move tmp_srcrs1 srcrs1 ;
627      translate_move tmp_srcrs2 srcrs2 ;
628      adds_graph [RTL.St_int (tmp_128, 128, start_lbl)] ;
629      add_128_to_last tmp_128 tmp_srcrs1 ;
630      add_128_to_last tmp_128 tmp_srcrs2 ;
631      translate_lt destrs tmp_srcrs1 tmp_srcrs2]
632     start_lbl dest_lbl def
633
634
635 let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
636   match op2 with
637
638     | AST.Op_add | AST.Op_addp ->
639       translate_op I8051.Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
640
641     | AST.Op_sub | AST.Op_subp | AST.Op_subpp ->
642       translate_op I8051.Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
643
644     | AST.Op_mul ->
645       translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
646
647     | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
648       translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2)
649         start_lbl dest_lbl def
650
651     | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
652       translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2)
653         start_lbl dest_lbl def
654
655     | AST.Op_and ->
656       translate_op I8051.And destrs srcrs1 srcrs2 start_lbl dest_lbl def
657
658     | AST.Op_or ->
659       translate_op I8051.Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
660
661     | AST.Op_xor ->
662       translate_op I8051.Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
663
664     | AST.Op_cmp AST.Cmp_eq
665     | AST.Op_cmpu AST.Cmp_eq
666     | AST.Op_cmpp AST.Cmp_eq ->
667       add_translates
668         [translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ;
669          translate_op1 AST.Op_notbool destrs destrs]
670         start_lbl dest_lbl def
671
672     | AST.Op_cmp AST.Cmp_ne
673     | AST.Op_cmpu AST.Cmp_ne
674     | AST.Op_cmpp AST.Cmp_ne ->
675       translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
676
677     | AST.Op_cmp AST.Cmp_lt ->
678       translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def
679
680     | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
681       translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def
682
683     | AST.Op_cmp AST.Cmp_le ->
684       add_translates
685         [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
686          translate_op1 AST.Op_notbool destrs destrs]
687         start_lbl dest_lbl def
688
689     | AST.Op_cmpu AST.Cmp_le ->
690       add_translates
691         [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ;
692          translate_op1 AST.Op_notbool destrs destrs]
693         start_lbl dest_lbl def
694
695     | AST.Op_cmpp AST.Cmp_le ->
696       add_translates
697         [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
698          translate_op1 AST.Op_notbool destrs destrs]
699         start_lbl dest_lbl def
700
701     | AST.Op_cmp AST.Cmp_gt ->
702       translate_op2 (AST.Op_cmp AST.Cmp_lt)
703         destrs srcrs2 srcrs1 start_lbl dest_lbl def
704
705     | AST.Op_cmpu AST.Cmp_gt ->
706       translate_op2 (AST.Op_cmpu AST.Cmp_lt)
707         destrs srcrs2 srcrs1 start_lbl dest_lbl def
708
709     | AST.Op_cmpp AST.Cmp_gt ->
710       translate_op2 (AST.Op_cmpp AST.Cmp_lt)
711         destrs srcrs2 srcrs1 start_lbl dest_lbl def
712
713     | AST.Op_cmp AST.Cmp_ge ->
714       add_translates
715         [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
716          translate_op1 AST.Op_notbool destrs destrs]
717         start_lbl dest_lbl def
718
719     | AST.Op_cmpu AST.Cmp_ge ->
720       add_translates
721         [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
722          translate_op1 AST.Op_notbool destrs destrs]
723         start_lbl dest_lbl def
724
725     | AST.Op_cmpp AST.Cmp_ge ->
726       add_translates
727         [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
728          translate_op1 AST.Op_notbool destrs destrs]
729         start_lbl dest_lbl def
730
731     | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
732     | AST.Op_shr | AST.Op_shru ->
733       (* Unsupported, should have been replaced by a runtime function. *)
734       assert false
735
736
737 (** The RTL.St_cond construction is based on a single register. We accumulate
738     with a bitwise or the value of the source registers. In the end, the result
739     is 0 if and only if all registers contained 0. *)
740
741 let translate_cond srcrs start_lbl lbl_true lbl_false def =
742   let (def, tmpr) = fresh_reg def in
743   let tmp_lbl = fresh_label def in
744   let init = RTL.St_int (tmpr, 0, start_lbl) in
745   let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, srcr, start_lbl) in
746   let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
747   add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def
748
749
750 (** Loading or storing may ask to load or store several memory cells. We
751     consider the base address shifted by successive offsets until every data has
752     been loaded or stored. *)
753
754 let translate_load addr destrs start_lbl dest_lbl def =
755   let (def, save_addr) = fresh_regs def (List.length addr) in
756   let (def, tmp_addr) = fresh_regs def (List.length addr) in
757   let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
758   let (def, tmpr) = fresh_reg def in
759   let insts_save_addr = translate_move save_addr addr in
760   let f (translates, off) r =
761     let translates =
762       translates @
763         [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
764          translate_op2 AST.Op_addp tmp_addr save_addr [tmpr] ;
765          adds_graph [RTL.St_load (r, tmp_addr1, tmp_addr2, dest_lbl)]] in
766     (translates, off + Driver.TargetArch.int_size) in
767   let (translates, _) = List.fold_left f ([], 0) destrs in
768   add_translates (insts_save_addr :: translates) start_lbl dest_lbl def
769
770
771 let translate_store addr srcrs start_lbl dest_lbl def =
772   let (def, tmp_addr) = fresh_regs def (List.length addr) in
773   let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
774   let (def, tmpr) = fresh_reg def in
775   let f (translates, off) srcr =
776     let translates =
777       translates @
778         [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
779          translate_op2 AST.Op_addp tmp_addr addr [tmpr] ;
780          adds_graph [RTL.St_store (tmp_addr1, tmp_addr2, srcr, dest_lbl)]] in
781     (translates, off + Driver.TargetArch.int_size) in
782   let (translates, _) = List.fold_left f ([], 0) srcrs in
783   add_translates translates start_lbl dest_lbl def
784
785
786 let translate_stmt lenv lbl stmt def = match stmt with
787
788   | RTLabs.St_skip lbl' ->
789     add_graph lbl (RTL.St_skip lbl') def
790
791   | RTLabs.St_cost (cost_lbl, lbl') ->
792     add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
793
794   | RTLabs.St_cst (destr, cst, lbl') ->
795     translate_cst cst (find_local_env destr lenv) lbl lbl' def
796
797   | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
798     translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
799       lbl lbl' def
800
801   | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
802     translate_op2 op2 (find_local_env destr lenv)
803       (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def
804
805   | RTLabs.St_load (_, addr, destr, lbl') ->
806     translate_load (find_local_env addr lenv) (find_local_env destr lenv)
807       lbl lbl' def
808
809   | RTLabs.St_store (_, addr, srcr, lbl') ->
810     translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
811       lbl lbl' def
812
813   | RTLabs.St_call_id (f, args, None, _, lbl') ->
814     add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def
815
816   | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
817     add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
818                                    find_local_env retr lenv, lbl')) def
819
820   | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
821     let (f1, f2) = find_and_addr f lenv in
822     add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def
823
824   | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
825     let (f1, f2) = find_and_addr f lenv in
826     add_graph lbl
827       (RTL.St_call_ptr
828          (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def
829
830   | RTLabs.St_tailcall_id (f, args, _) ->
831     add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
832
833   | RTLabs.St_tailcall_ptr (f, args, _) ->
834     let (f1, f2) = find_and_addr f lenv in
835     add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
836
837   | RTLabs.St_cond (r, lbl_true, lbl_false) ->
838     translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
839
840   | RTLabs.St_jumptable _ ->
841     error "Jump tables not supported yet."
842
843   | RTLabs.St_return None ->
844     add_graph lbl (RTL.St_return []) def
845
846   | RTLabs.St_return (Some r) ->
847     add_graph lbl (RTL.St_return (find_local_env r lenv)) def
848
849
850 let translate_internal def =
851   let runiverse = def.RTLabs.f_runiverse in
852   let lenv =
853     initialize_local_env runiverse
854       (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in
855   let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
856   let params = map_list_local_env lenv (List.map fst def.RTLabs.f_params) in
857   let locals = map_list_local_env lenv (List.map fst def.RTLabs.f_locals) in
858   let locals = set_of_list locals in
859   let result = match def.RTLabs.f_result with
860     | None -> []
861     | Some (r, _) -> find_local_env r lenv in
862   let res =
863     { RTL.f_luniverse = def.RTLabs.f_luniverse ;
864       RTL.f_runiverse = runiverse ;
865       RTL.f_result    = result ;
866       RTL.f_params    = params ;
867       RTL.f_locals    = locals ;
868       RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ;
869       RTL.f_graph     = Label.Map.empty ;
870       RTL.f_entry     = def.RTLabs.f_entry ;
871       RTL.f_exit      = def.RTLabs.f_exit } in
872   Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res
873
874
875 let translate_fun_def = function
876   | RTLabs.F_int def -> RTL.F_int (translate_internal def)
877   | RTLabs.F_ext def -> RTL.F_ext def
878
879
880 (* Add global initializations *)
881
882 let sum_offsets =
883   let f res off = res + (concrete_offset off) in
884   List.fold_left f 0
885
886 let assign_data addr1 addr2 addr1' addr2' off_r data_r tmpr def (offset, data) =
887   if offset < 256 then
888     let def =
889       generates_graph
890         [RTL.St_store (addr1', addr2', data_r, Label.dummy)] def in
891     let start_lbl = fresh_label def in
892     let dest_lbl = def.RTL.f_entry in
893     let def =
894       translate_op_ tmpr I8051.Addc
895         [addr1' ; addr2'] [addr1 ; addr2] [off_r] start_lbl dest_lbl def in
896     let def = change_entry def start_lbl in
897     generates_graph
898       [RTL.St_int (off_r, offset, Label.dummy) ;
899        RTL.St_int (data_r, data, Label.dummy)] def
900   else error ("offset too big to fit in a register when initializing globals.")
901
902 let assign_datas
903     addr1 addr2 addr1' addr2' off_r data_r tmpr x def (offsets, data) =
904   let base_offset = sum_offsets offsets in
905   let (data, quantity) = match data with
906     | AST.Data_int8  i -> (i, 1)
907     | AST.Data_int16 i -> (i, 2)
908     | AST.Data_int32 i -> (i, 4)
909     | AST.Data_float32 f | AST.Data_float64 f -> error_float () in
910   let data = IntValue.Int32.of_int data in
911   let datas = IntValue.Int32.break data quantity in
912   let datas = List.map IntValue.Int8.to_int datas in
913   let added_offs = MiscPottier.make 0 (List.length datas) in
914   let offs = MiscPottier.mapi (fun i _ -> base_offset + i) added_offs in
915   assert (List.length offs = List.length datas) ;
916   let offs_datas = List.combine offs datas in
917   let def =
918     List.fold_left (assign_data addr1 addr2 addr1' addr2' off_r data_r tmpr)
919       def offs_datas in
920   generates_graph [RTL.St_addr (addr1, addr2, x, Label.dummy)] def
921
922 let add_global_initializations_def globals def =
923   let (def, addr1, addr2, addr1', addr2', off_r, data_r, tmpr) =
924     match fresh_regs def 7 with
925       | (def, [addr1 ; addr2 ; addr1' ; addr2' ; off_r ; data_r ; tmpr]) ->
926         (def, addr1, addr2, addr1', addr2', off_r, data_r, tmpr)
927       | _ ->
928       (* should be impossible: [fresh_regs _ 7] returns 7 regs *)
929       assert false in
930   let f def (x, size, datas_opt) = match datas_opt with
931     | None -> def
932     | Some datas ->
933       let offsets = Memory.all_offsets size in
934       if List.length offsets <> List.length datas then
935         error "bad global initialization style."
936       else
937         let offs_datas = List.combine offsets datas in
938         List.fold_left
939           (assign_datas addr1 addr2 addr1' addr2' off_r data_r tmpr x)
940           def offs_datas in
941   List.fold_left f def globals
942
943 let add_global_initializations_funct globals = function
944   | RTL.F_int def ->
945     let def = add_global_initializations_def globals def in
946     RTL.F_int def
947   | def -> def
948
949 (* [add_global_initializations p] moves the initializations of the globals of
950    [p] to the beginning of the main function, if any. *)
951
952 let add_global_initializations globals main functs = match main with
953   | None -> functs
954   | Some main ->
955     let main_def = List.assoc main functs in
956     let main_def = add_global_initializations_funct globals main_def in
957     MiscPottier.update_list_assoc main main_def functs
958
959
960 let translate p = 
961   let f_global (id, size, _) = (id, concrete_size size) in
962   let f_funct (id, fun_def) = (id, translate_fun_def fun_def) in
963   let functs = List.map f_funct p.RTLabs.functs in
964   let functs = add_global_initializations p.RTLabs.vars p.RTLabs.main functs in
965   { RTL.vars   = List.map f_global p.RTLabs.vars ;
966     RTL.functs = functs ;
967     RTL.main   = p.RTLabs.main }