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 }