(** This module provides a translation of [RTLabs] programs to [RTL]
    programs. *)


let error_prefix = "RTLabs to RTL"
let error = Error.global_error error_prefix

let error_int () = error "int16 and int32 not supported."
let error_float () = error "float not supported."
let error_shift () = error "Shift operations not supported."


let change_entry def f_entry = { def with RTL.f_entry }

let add_graph lbl stmt def =
  { def with RTL.f_graph = Label.Map.add lbl stmt def.RTL.f_graph }

let fresh_label def = Label.Gen.fresh def.RTL.f_luniverse

let fresh_reg def =
  let r = Register.fresh def.RTL.f_runiverse in
  let locals = Register.Set.add r def.RTL.f_locals in
  ({ def with RTL.f_locals = locals }, r)

let rec fresh_regs def n =
  if n = 0 then (def, [])
  else
    let (def, res) = fresh_regs def (n-1) in
    let (def, r) = fresh_reg def in
    (def, r :: res) 

let addr_regs regs = match regs with
  | r1 :: r2 :: _ -> (r1, r2)
  | _ -> error "registers are not an address."

let rec register_freshes runiverse n =
  if n <= 0 then []
  else (Register.fresh runiverse) :: (register_freshes runiverse (n-1)) 

let choose_rest rest1 rest2 = match rest1, rest2 with
  | [], _ -> rest2
  | _, [] -> rest1
  | _ -> assert false (* do not use on these arguments *)

let complete_regs def srcrs1 srcrs2 =
  let nb_added = (List.length srcrs1) - (List.length srcrs2) in
  let (def, added_regs) = fresh_regs def nb_added in
  if nb_added > 0 then (srcrs1, srcrs2 @ added_regs, added_regs)
  else (srcrs1 @ added_regs, srcrs2, added_regs)


let size_of_sig_type = function
  | AST.Sig_int (i, _) -> i / Driver.TargetArch.int_size
  | AST.Sig_float _ -> error_float ()
  | AST.Sig_offset -> Driver.TargetArch.int_size
  | AST.Sig_ptr -> Driver.TargetArch.ptr_size

let concrete_size = Driver.RTLMemory.concrete_size

let concrete_offset = Driver.RTLMemory.concrete_offset


(* Local environments *)

type local_env = Register.t list Register.Map.t

let mem_local_env = Register.Map.mem
let add_local_env = Register.Map.add
let find_local_env = Register.Map.find

let initialize_local_env runiverse registers result =
  let registers =
    registers @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
  let f lenv (r, t) =
    let rs = register_freshes runiverse (size_of_sig_type t) in
    add_local_env r rs lenv in
  List.fold_left f Register.Map.empty registers

let map_list_local_env lenv regs =
  let f res r = res @ (find_local_env r lenv) in
  List.fold_left f [] regs

let make_addr = function
  | r1 :: r2 :: _ -> (r1, r2)
  | _ -> assert false (* do not use on these arguments *)

let find_and_addr r lenv = make_addr (find_local_env r lenv)

let rtl_args regs_list lenv =
  List.flatten (List.map (fun r -> find_local_env r lenv) regs_list)


let change_label lbl = function
  | RTL.St_skip _ -> RTL.St_skip lbl
  | RTL.St_cost (cost_lbl, _) -> RTL.St_cost (cost_lbl, lbl)
  | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl)
  | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl)
  | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl)
  | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl)
  | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, _) ->
    RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl)
  | RTL.St_op1 (op1, dstr, srcr, _) -> RTL.St_op1 (op1, dstr, srcr, lbl)
  | RTL.St_op2 (op2, dstr, srcr1, srcr2, _) ->
    RTL.St_op2 (op2, dstr, srcr1, srcr2, lbl)
  | RTL.St_clear_carry _ -> RTL.St_clear_carry lbl
  | RTL.St_set_carry _ -> RTL.St_set_carry lbl
  | RTL.St_load (dstrs, addr1, addr2, _) ->
    RTL.St_load (dstrs, addr1, addr2, lbl)
  | RTL.St_store (addr1, addr2, srcrs, _) ->
    RTL.St_store (addr1, addr2, srcrs, lbl)
  | RTL.St_call_id (f, args, retrs, _) -> RTL.St_call_id (f, args, retrs, lbl)
  | RTL.St_call_ptr (f1, f2, args, retrs, _) ->
    RTL.St_call_ptr (f1, f2, args, retrs, lbl)
  | RTL.St_tailcall_id (f, args) -> RTL.St_tailcall_id (f, args)
  | RTL.St_tailcall_ptr (f1, f2, args) -> RTL.St_tailcall_ptr (f1, f2, args)
  | RTL.St_cond _ as inst -> inst
  | RTL.St_return regs -> RTL.St_return regs

(* Add a list of instruction in a graph, from one label to another, by creating
   fresh labels inbetween. *)

let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with
  | [] -> 
    add_graph start_lbl (RTL.St_skip dest_lbl) def
  | [stmt] ->
    add_graph start_lbl (change_label dest_lbl stmt) def
  | stmt :: stmt_list ->
    let tmp_lbl = fresh_label def in
    let stmt = change_label tmp_lbl stmt in
    let def = add_graph start_lbl stmt def in
    adds_graph stmt_list tmp_lbl dest_lbl def

let generates_graph stmt_list def =
  let start_lbl = fresh_label def in
  let dest_lbl = def.RTL.f_entry in
  change_entry (adds_graph stmt_list start_lbl dest_lbl def) start_lbl

(* Process a list of function that adds a list of instructions to a graph, from
   one label to another, and by creating fresh labels inbetween. *)

let rec add_translates translate_list start_lbl dest_lbl def =
  match translate_list with
    | [] -> 
      add_graph start_lbl (RTL.St_skip dest_lbl) def
    | [trans] -> 
      trans start_lbl dest_lbl def
    | trans :: translate_list ->
      let tmp_lbl = fresh_label def in
      let def = trans start_lbl tmp_lbl def in
      add_translates translate_list tmp_lbl dest_lbl def


let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with

  | AST.Cst_int _ when destrs = [] ->
    add_graph start_lbl (RTL.St_skip dest_lbl) def

  | AST.Cst_int i ->
    let size = List.length destrs in
    let module M = IntValue.Make (struct let size = size end) in
    let is = List.map M.to_int (M.break (M.of_int i) size) in
    let f r i = RTL.St_int (r, i, dest_lbl) in
    let l = List.map2 f destrs is in
    adds_graph l start_lbl dest_lbl def

  | AST.Cst_float _ -> error_float ()

  | AST.Cst_addrsymbol id ->
    let (r1, r2) = make_addr destrs in
    add_graph start_lbl (RTL.St_addr (r1, r2, id, dest_lbl)) def

  | AST.Cst_stack ->
    let (r1, r2) = make_addr destrs in
    add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def

  | AST.Cst_offset off ->
    let i = concrete_offset off in
    translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def

  | AST.Cst_sizeof size ->
    let i = concrete_size size in
    translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def


(** Adds zeros if destination is bigger than source, or truncates if source is
    bigger than destination. *)

let translate_move destrs srcrs start_lbl =
  let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
  let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
  let translates1 = adds_graph (List.map2 f_common common1 common2) in
  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
  add_translates [translates1 ; translates2] start_lbl

let translate_cast_unsigned destrs start_lbl dest_lbl def =
  let (def, tmp_zero) = fresh_reg def in
  let zeros = MiscPottier.make tmp_zero (List.length destrs) in
  add_translates
    [adds_graph [RTL.St_int (tmp_zero, 0, start_lbl)] ;
     translate_move destrs zeros]
    start_lbl dest_lbl def

(** [srcr] will be copied in the first register of [destrs]. The remaining
    registers of [destrs] needs to be set either to zeros or to ones, depending
    on the most significant bit of [srcr]. Since 8051 is a 8 bits architecture,
    we fetch the most significant bit with [src & 10000000]. Let [tmpr] be the
    result. Then we build zeros or ones with [tmpr * 11111111]. *)

let translate_cast_signed destrs srcr start_lbl dest_lbl def =
  let (def, tmp_128) = fresh_reg def in
  let (def, tmp_255) = fresh_reg def in
  let (def, tmpr) = fresh_reg def in
  let (def, dummy) = fresh_reg def in
  let insts =
    [RTL.St_int (tmp_128, 128, start_lbl) ;
     RTL.St_op2 (I8051.And, tmpr, tmp_128, srcr, start_lbl) ;
     RTL.St_opaccs (I8051.DivuModu, tmpr, dummy, tmpr, tmp_128, start_lbl) ;
     RTL.St_int (tmp_255, 255, start_lbl) ;
     RTL.St_opaccs (I8051.Mul, tmpr, dummy, tmpr, tmp_255, start_lbl)] in
  let srcrs = MiscPottier.make tmpr (List.length destrs) in
  add_translates [adds_graph insts ; translate_move destrs srcrs]
    start_lbl dest_lbl def

(** Depending on [src_sign], perform either a signed or an unsigned cast. For
    the signed case, we need the most significant bit of the source. *)

let translate_cast src_size src_sign dest_size destrs srcrs =
  if List.length srcrs = 0 then adds_graph []
  else
    if dest_size < src_size then translate_move destrs srcrs
    else
      let ((common1, rest1), (common2, rest2)) =
	MiscPottier.reduce destrs srcrs in
      (* dest_size >= src_size, so there will be no rest2 *)
      assert (rest2 = []) ;
      let insts_common = translate_move common1 common2 in
      let sign_reg = MiscPottier.last srcrs in
      let insts_sign = match src_sign with
	| AST.Unsigned -> translate_cast_unsigned rest1
	| AST.Signed -> translate_cast_signed rest1 sign_reg in
      add_translates [insts_common ; insts_sign]


(** [-x] is [~x] (the complement of [x]), and then propagating the carry if some
    register of the result is greater or equal to 128 (10000000 in binary). *)

(** FIXME Nicolas: why is this correct? *)

let translate_negint destrs srcrs start_lbl dest_lbl def =
  assert (List.length destrs = List.length srcrs) ;
  let (def, tmpr) = fresh_reg def in
  let f_cmpl destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
  let insts_cmpl = List.map2 f_cmpl destrs srcrs in
  let insts_init =
    [RTL.St_set_carry start_lbl ;
     RTL.St_int (tmpr, 0, start_lbl)] in
  let f_add destr = RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl) in
  let insts_add = List.map f_add destrs in
  adds_graph (insts_cmpl @ insts_init @ insts_add)
    start_lbl dest_lbl def


(** In order to know if a register is different from 0 or not, we can simply
    substract it from 0 and fetch the carry bit: it is 0 if the register
    contains 0, and 1 otherwise. By doing a | on the result of
    the previous operation on every source register and starting with 0, the
    result is either 0 if all the source registers contained 0, and 1
    otherwise. Let [tmp_res] be this number; then, the result of [notbool] is
    simply [tmp_res ^ 1]. *)

let translate_notbool destrs srcrs start_lbl dest_lbl def = match destrs with
  | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
  | destr :: destrs ->
    (* [destr] will be set to either 0 or 1 (depending on [srcrs]), the
       remaining destination registers [destrs] will be set to 0. *)
    let (def, tmpr) = fresh_reg def in
    let (def, tmp_srcrs) = fresh_regs def (List.length srcrs) in
    let save_srcrs = translate_move tmp_srcrs srcrs in
    let prologue = translate_cst (AST.Cst_int 0) (destr :: destrs) in
    let f tmp_srcr =
      [RTL.St_clear_carry start_lbl ;
       RTL.St_int (tmpr, 0, start_lbl) ;
       RTL.St_op2 (I8051.Sub, tmpr, tmpr, tmp_srcr, start_lbl) ;
       RTL.St_int (tmpr, 0, start_lbl) ;
       RTL.St_op2 (I8051.Addc, tmpr, tmpr, tmpr, start_lbl) ;
       RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in
    let insts = List.flatten (List.map f tmp_srcrs) in
    let epilogue =
      [RTL.St_int (tmpr, 1, start_lbl) ;
       RTL.St_op2 (I8051.Xor, destr, destr, tmpr, start_lbl)] in
    add_translates
      [save_srcrs ; prologue ; adds_graph insts ; adds_graph epilogue]
      start_lbl dest_lbl def


let translate_op1 op1 destrs srcrs start_lbl dest_lbl def = match op1 with

  | AST.Op_cast ((src_size, src_sign), dest_size) ->
    translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl
      def

  | AST.Op_negint ->
    translate_negint destrs srcrs start_lbl dest_lbl def

  | AST.Op_notbool ->
    translate_notbool destrs srcrs start_lbl dest_lbl def

  | AST.Op_notint ->
    let f destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
    let l = List.map2 f destrs srcrs in
    adds_graph l start_lbl dest_lbl def

  | AST.Op_ptrofint | AST.Op_intofptr | AST.Op_id ->
    translate_move destrs srcrs start_lbl dest_lbl def


(** Apply a binary operation. The sources and destination registers may not have
    the same size. When they do not, zero registers will be considered if
    needed. Considers given a temporary register [tmpr] that plays the role of
    the zero register. The destination registers can be one of the sources
    registers. *)

let translate_op_ tmpr op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
  (* The next few instructions allows to decompose the sources and destination
     registers in sub-lists of the same size, and creating the remainings at
     the same time. *)
  let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) =
    MiscPottier.reduce srcrs1 srcrs2 in
  let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in
  let ((destrs_common, destrs_rest), _) =
    MiscPottier.reduce destrs srcrs1_common in
  (* srcrs1_common and srcrs2_common have the same size, which is exactly the
     one of the shortest list between srcrs1 and srcrs2. destrs_common and
     destrs_rest are either destrs and empty if destrs is bigger than
     srcrs1_common (and thus srcrs2_common), or destrs_common has the size of
     srcrs1_common (and srcrs2_common) and destrs_rest is the remainings of
     destrs. *)
  let ((destrs_cted, destrs_rest), (srcrs_cted, _)) =
    MiscPottier.reduce destrs_rest srcrs_rest in
  (* destrs_cted is either empty or is the remainings of destrs that has the
     same size of the remainings between the srcrs1 and srcrs2 when removed the
     number of elements of the size of the shortest one. destrs_rest are the
     remainings, if any. *)
  let insts_init =
    [RTL.St_clear_carry start_lbl ;
     RTL.St_int (tmpr, 0, start_lbl)] in
  let f_op destr srcr1 srcr2 =
    RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
  let insts_op =
    MiscPottier.map3 f_op destrs_common srcrs1_common srcrs2_common in
  let f_op_cted destr srcr =
    RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in
  let insts_op_cted = List.map2 f_op_cted destrs_cted srcrs_cted in
  let f_rest destr =
    RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in
  let insts_rest = List.map f_rest destrs_rest in
  adds_graph (insts_init @ insts_op @ insts_op_cted @ insts_rest)
    start_lbl dest_lbl def

(** Same as [translate_op], but creates the zero register. *)

let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
  let (def, tmpr) = fresh_reg def in
  translate_op_ tmpr op destrs srcrs1 srcrs2 start_lbl dest_lbl def


(** Multiply a list of registers (list significant bits first) by a
    register. The multiplication in 8051 of two registers is two registers: the
    least and most significant bits of the result. When pultiplying a list of
    registers with one register, we need to propagate the most significant bits
    of an operation to the next one for addition. Example:

    (i1 i2) * j = res11 (res12 + res21) 

    where (res11, res12) = i1 * j and (res21, res22) = i2 * j. The result is
    truncated by just forgetting about res22. *)

(* [dummy] is used to discard the most significant bits *)

let rec translate_mul1 dummy tmpr destrs srcrs1 srcr2 start_lbl =
  match destrs, srcrs1 with
    | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl
    | [destr], [] ->
      (* if there are no source register left, and only one destination
	 register, simply add the carry bit of a potential previous addition *)
      adds_graph [RTL.St_int (tmpr, 0, start_lbl) ;
		  RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]
	start_lbl
    | destr1 :: destr2 :: _, [] ->
      (* if there are no source register left, but at least two destination
	 registers, adding the carry of the potential previous addition
	 may lead to another carry that needs to be propagated *)
      add_translates
	[adds_graph [RTL.St_int (tmpr, 0, start_lbl) ;
		     RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl) ;
		     RTL.St_op2 (I8051.Addc, destr2, tmpr, tmpr, start_lbl)]]
	start_lbl
    | [destr], srcr1 :: _ ->
      (* if there are at least one source register, but only one destination
	 register, discard the most significant bits of the multiplication *)
      adds_graph
	[RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ;
	 RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]
	start_lbl
    | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 ->
      (* if there are at least one source register, and at least two destination
	 registers, the first destination register should hold the most
	 significant bits of the previous atomic multiplication. We need to add
	 to it the least significant bits of the current operation, and store
	 the most significant bits in the next destination register for the next
	 multiplication. *)
      add_translates
	[adds_graph
	    [RTL.St_opaccs
		(I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ;
	     RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl)] ;
	 translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2]
	start_lbl

(** Multiply the ith register of some source registers. The registers up to the
    ith of the result should be set to 0, and the multiplication really starts
    at the next one. The result of this operation is then added to the current
    result of the full multiplication. *)

let translate_muli
    dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates srcr2i =
  let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in
  translates @
    (match tmp_destrs2 with
      | [] -> []
      | tmp_destr2 :: tmp_destrs2 ->
	[adds_graph [RTL.St_clear_carry dummy_lbl] ;
	 translate_cst (AST.Cst_int 0) [tmpr] ;
	 translate_cst (AST.Cst_int 0) tmp_destrs ;
	 translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
	 translate_cst (AST.Cst_int 0) tmp_destrs1 ;
	 adds_graph [RTL.St_clear_carry dummy_lbl] ;
	 translate_op I8051.Addc destrs destrs tmp_destrs])

(** Multiplication, school-style: 

    i1n ... i11 * j1m ... j11 =
    i1n ... i11 * j11 +
    i1n ... i12 0 * j12 +
    i1n ... i13 0 0 * j13 +
    ... *)

let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
  (* dummy will be used to discard some unused results *)
  let (def, dummy) = fresh_reg def in
  let (def, tmpr) = fresh_reg def in
  (* One line of the multiplication is stored in tmp_destrs. The result of the
     full multiplication is accumulated in destrs. *)
  let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
  (* Source registers are copied into fresh source registers to avoid
     overwriting if one of them is also the destination registers. *)
  let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
  let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in
  let insts_init =
    [translate_move fresh_srcrs1 srcrs1 ;
     translate_move fresh_srcrs2 srcrs2 ;
     translate_cst (AST.Cst_int 0) destrs] in
  let f = translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
  let insts_mul = MiscPottier.foldi f [] fresh_srcrs2 in
  add_translates (insts_init @ insts_mul) start_lbl dest_lbl def


(** The 8051 performs division and modulo in a single operation. Depending on
    the one we need (boolean [order]), we discard the other. *)

let translate_divumodu8 order destrs srcr1 srcr2 start_lbl dest_lbl def =
  match destrs with
    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
    | destr :: destrs ->
      let (def, dummy) = fresh_reg def in
      let (destr1, destr2) = if order then (destr, dummy) else (dummy, destr) in
      let inst_div =
	adds_graph [RTL.St_opaccs (I8051.DivuModu, destr1, destr2,
				   srcr1, srcr2, start_lbl)] in
      let insts_rest = translate_cst (AST.Cst_int 0) destrs in
      add_translates [inst_div ; insts_rest] start_lbl dest_lbl def


(** Only the first register of [destrs] will be used, the others will be set to
    0. We compare in order the registers of both source registers and accumulate
    the results in the first register of [destrs], with a | and initially set to
    0. Two registers are equal if and only if substracting one with the other
    and substracting the other with the one both lead to no carry. If one of the
    source registers is bigger than the other, we compare the remainings with
    0. We first copy the source registers into fresh ones, in case the
    destination registers share some source registers. Example:

    srcr11 ... srcr1n != srcr21 ... srcr2m =
    carry(srcr11 - srcr21) | carry (srcr21 - srcr11) |
    carry(srcr12 - srcr22) | carry (srcr22 - srcr12) |
    ... *)

let translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def =
  match destrs with
    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
    | destr :: destrs ->
      let (def, dummy) = fresh_reg def in
      let (def, tmp_zero) = fresh_reg def in
      let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in
      let save_srcrs1 = translate_move tmp_srcrs1 srcrs1 in
      let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in
      let save_srcrs2 = translate_move tmp_srcrs2 srcrs2 in
      let ((common1, rest1), (common2, rest2)) =
	MiscPottier.reduce tmp_srcrs1 tmp_srcrs2 in
      let rest = choose_rest rest1 rest2 in
      let inits =
	[RTL.St_int (destr, 0, start_lbl) ;
	 RTL.St_int (tmp_zero, 0, start_lbl)] in
      let f tmp_srcr1 tmp_srcr2 =
	[RTL.St_clear_carry start_lbl ;
	 RTL.St_op2 (I8051.Sub, dummy, tmp_srcr1, tmp_srcr2, start_lbl) ;
	 RTL.St_op2 (I8051.Or, destr, destr, tmp_zero, start_lbl) ;
	 RTL.St_op2 (I8051.Sub, dummy, tmp_srcr2, tmp_srcr1, start_lbl) ;
	 RTL.St_op2 (I8051.Or, destr, destr, tmp_zero, start_lbl)] in
      let insts_common = List.flatten (List.map2 f common1 common2) in
      let insts_rest = List.flatten (List.map (f tmp_zero) rest) in
      let insts = inits @ insts_common @ insts_rest in
      let epilogue = translate_cst (AST.Cst_int 0) destrs in
      add_translates [save_srcrs1 ; save_srcrs2 ; adds_graph insts ; epilogue]
	start_lbl dest_lbl def


(** Are two given registers equal? We substract the one with the other, and then
    the other with the one. They are equal if and only if both carry are 0,
    i.e., a bitwise 'or' on the carries is 1 if and only if they are
    different. We simply do a bitwise xor with this result and 1 to have our
    answer:

    r1 == r2 = (carry(r1 - r2) | carry(r2 - r1)) ^ 1 *)

let translate_eq_reg
    tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl (srcr1, srcr2) =
  [RTL.St_clear_carry dummy_lbl ;
   RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ;
   RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ;
   RTL.St_clear_carry dummy_lbl ;
   RTL.St_op2 (I8051.Sub, tmpr2, srcr2, srcr1, dummy_lbl) ;
   RTL.St_op2 (I8051.Addc, tmpr2, tmp_zero, tmp_zero, dummy_lbl) ;
   RTL.St_op2 (I8051.Or, tmpr1, tmpr1, tmpr2, dummy_lbl) ;
   RTL.St_op2 (I8051.Xor, tmpr1, tmpr1, tmp_one, dummy_lbl) ;
   RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)]

let translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 destr leq dummy_lbl =
  let f = translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
  (RTL.St_int (destr, 1, dummy_lbl)) :: (List.flatten (List.map f leq))

(** Translation of unsigned LT: we proceed by successively comparing the source
    registers most significant bits first (if one of the two source lists is
    smaller than the other, we complete it with zeros). At each step, a register
    ([tmpr3]) holds 1 if the previous registers are all equal, and 0
    otherwise. The result of the comparison is 1 if there is a step where all
    the previous registers are equal and the first current register is lower
    than the second (which is checked by substracting the second to the first
    and fetching the carry). *)

let translate_atom
    tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 =
  (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @
    [RTL.St_clear_carry dummy_lbl ;
     RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ;
     RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ;
     RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ;
     RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)]

let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl
    srcrs1 srcrs2 =
  let f (insts, leq) srcr1 srcr2 =
    let added_insts =
      translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq
	srcr1 srcr2 in
    (insts @ added_insts, leq @ [(srcr1, srcr2)]) in
  fst (List.fold_left2 f ([], []) srcrs1 srcrs2)

let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def =
  match destrs with
    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
    | _ ->
      let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
      let tmp_destr = List.hd tmp_destrs in
      let (def, tmp_zero) = fresh_reg def in
      let (def, tmp_one) = fresh_reg def in
      let (def, tmpr1) = fresh_reg def in
      let (def, tmpr2) = fresh_reg def in
      let (def, tmpr3) = fresh_reg def in
      let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in
      let srcrs1 = List.rev srcrs1 in
      let srcrs2 = List.rev srcrs2 in
      let insts_init =
	[translate_cst (AST.Cst_int 0) tmp_destrs ;
	 translate_cst (AST.Cst_int 0) added ;
	 adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ;
		     RTL.St_int (tmp_one, 1, start_lbl)]] in
      let insts_main =
	translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl
	  srcrs1 srcrs2 in
      let insts_main = [adds_graph insts_main] in
      let insts_exit = [translate_move destrs tmp_destrs] in
      add_translates (insts_init @ insts_main @ insts_exit )
	start_lbl dest_lbl def


(** Translation of signed LT: exactly unsigned LT when the signed bit is
    changed: positive numbers become greater than the half bound as unsigned,
    negative numbers become between 0 and the half bound as unsigned. The sign
    bit is changed with a bitwise xor between the register holding the bit sign
    (the most significant register, i.e. the last register in the list of
    registers) and 10000000. *)

let add_128_to_last tmp_128 rs start_lbl = match rs with
  | [] -> adds_graph [] start_lbl
  | _ ->
    let r = MiscPottier.last rs in
    adds_graph [RTL.St_op2 (I8051.Xor, r, r, tmp_128, start_lbl)] start_lbl

let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def =
  let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in
  let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in
  let (def, tmp_128) = fresh_reg def in
  add_translates
    [translate_move tmp_srcrs1 srcrs1 ;
     translate_move tmp_srcrs2 srcrs2 ;
     adds_graph [RTL.St_int (tmp_128, 128, start_lbl)] ;
     add_128_to_last tmp_128 tmp_srcrs1 ;
     add_128_to_last tmp_128 tmp_srcrs2 ;
     translate_lt destrs tmp_srcrs1 tmp_srcrs2]
    start_lbl dest_lbl def


let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
  match op2 with

    | AST.Op_add | AST.Op_addp ->
      translate_op I8051.Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def

    | AST.Op_sub | AST.Op_subp | AST.Op_subpp ->
      translate_op I8051.Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def

    | AST.Op_mul ->
      translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def

    | AST.Op_divu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
      translate_divumodu8 true destrs (List.hd srcrs1) (List.hd srcrs2)
	start_lbl dest_lbl def

    | AST.Op_modu when List.length srcrs1 = 1 && List.length srcrs2 = 1 ->
      translate_divumodu8 false destrs (List.hd srcrs1) (List.hd srcrs2)
	start_lbl dest_lbl def

    | AST.Op_and ->
      translate_op I8051.And destrs srcrs1 srcrs2 start_lbl dest_lbl def

    | AST.Op_or ->
      translate_op I8051.Or destrs srcrs1 srcrs2 start_lbl dest_lbl def

    | AST.Op_xor ->
      translate_op I8051.Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def

    | AST.Op_cmp AST.Cmp_eq
    | AST.Op_cmpu AST.Cmp_eq
    | AST.Op_cmpp AST.Cmp_eq ->
      add_translates
	[translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ;
	 translate_op1 AST.Op_notbool destrs destrs]
	start_lbl dest_lbl def

    | AST.Op_cmp AST.Cmp_ne
    | AST.Op_cmpu AST.Cmp_ne
    | AST.Op_cmpp AST.Cmp_ne ->
      translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def

    | AST.Op_cmp AST.Cmp_lt ->
      translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def

    | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
      translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def

    | AST.Op_cmp AST.Cmp_le ->
      add_translates
	[translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
	 translate_op1 AST.Op_notbool destrs destrs]
	start_lbl dest_lbl def

    | AST.Op_cmpu AST.Cmp_le ->
      add_translates
	[translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ;
	 translate_op1 AST.Op_notbool destrs destrs]
	start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_le ->
      add_translates
	[translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
	 translate_op1 AST.Op_notbool destrs destrs]
	start_lbl dest_lbl def

    | AST.Op_cmp AST.Cmp_gt ->
      translate_op2 (AST.Op_cmp AST.Cmp_lt)
	destrs srcrs2 srcrs1 start_lbl dest_lbl def

    | AST.Op_cmpu AST.Cmp_gt ->
      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
	destrs srcrs2 srcrs1 start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_gt ->
      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
	destrs srcrs2 srcrs1 start_lbl dest_lbl def

    | AST.Op_cmp AST.Cmp_ge ->
      add_translates
	[translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
	 translate_op1 AST.Op_notbool destrs destrs]
	start_lbl dest_lbl def

    | AST.Op_cmpu AST.Cmp_ge ->
      add_translates
	[translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
	 translate_op1 AST.Op_notbool destrs destrs]
	start_lbl dest_lbl def

    | AST.Op_cmpp AST.Cmp_ge ->
      add_translates
	[translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
	 translate_op1 AST.Op_notbool destrs destrs]
	start_lbl dest_lbl def

    | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
    | AST.Op_shr | AST.Op_shru ->
      (* Unsupported, should have been replaced by a runtime function. *)
      assert false


(** The RTL.St_cond construction is based on a single register. We accumulate
    with a bitwise or the value of the source registers. In the end, the result
    is 0 if and only if all registers contained 0. *)

let translate_cond srcrs start_lbl lbl_true lbl_false def =
  let (def, tmpr) = fresh_reg def in
  let tmp_lbl = fresh_label def in
  let init = RTL.St_int (tmpr, 0, start_lbl) in
  let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, srcr, start_lbl) in
  let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
  add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def


(** Loading or storing may ask to load or store several memory cells. We
    consider the base address shifted by successive offsets until every data has
    been loaded or stored. *)

let translate_load addr destrs start_lbl dest_lbl def =
  let (def, save_addr) = fresh_regs def (List.length addr) in
  let (def, tmp_addr) = fresh_regs def (List.length addr) in
  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
  let (def, tmpr) = fresh_reg def in
  let insts_save_addr = translate_move save_addr addr in
  let f (translates, off) r =
    let translates =
      translates @
	[adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
	 translate_op2 AST.Op_addp tmp_addr save_addr [tmpr] ;
	 adds_graph [RTL.St_load (r, tmp_addr1, tmp_addr2, dest_lbl)]] in
    (translates, off + Driver.TargetArch.int_size) in
  let (translates, _) = List.fold_left f ([], 0) destrs in
  add_translates (insts_save_addr :: translates) start_lbl dest_lbl def


let translate_store addr srcrs start_lbl dest_lbl def =
  let (def, tmp_addr) = fresh_regs def (List.length addr) in
  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
  let (def, tmpr) = fresh_reg def in
  let f (translates, off) srcr =
    let translates =
      translates @
	[adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
	 translate_op2 AST.Op_addp tmp_addr addr [tmpr] ;
	 adds_graph [RTL.St_store (tmp_addr1, tmp_addr2, srcr, dest_lbl)]] in
    (translates, off + Driver.TargetArch.int_size) in
  let (translates, _) = List.fold_left f ([], 0) srcrs in
  add_translates translates start_lbl dest_lbl def


let translate_stmt lenv lbl stmt def = match stmt with

  | RTLabs.St_skip lbl' ->
    add_graph lbl (RTL.St_skip lbl') def

  | RTLabs.St_cost (cost_lbl, lbl') ->
    add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def

  | RTLabs.St_cst (destr, cst, lbl') ->
    translate_cst cst (find_local_env destr lenv) lbl lbl' def

  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv)
      lbl lbl' def

  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
    translate_op2 op2 (find_local_env destr lenv)
      (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def

  | RTLabs.St_load (_, addr, destr, lbl') ->
    translate_load (find_local_env addr lenv) (find_local_env destr lenv)
      lbl lbl' def

  | RTLabs.St_store (_, addr, srcr, lbl') ->
    translate_store (find_local_env addr lenv) (find_local_env srcr lenv)
      lbl lbl' def

  | RTLabs.St_call_id (f, args, None, _, lbl') ->
    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def

  | RTLabs.St_call_id (f, args, Some retr, _, lbl') ->
    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
				   find_local_env retr lenv, lbl')) def

  | RTLabs.St_call_ptr (f, args, None, _, lbl') ->
    let (f1, f2) = find_and_addr f lenv in
    add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def

  | RTLabs.St_call_ptr (f, args, Some retr, _, lbl') ->
    let (f1, f2) = find_and_addr f lenv in
    add_graph lbl
      (RTL.St_call_ptr
	 (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def

  | RTLabs.St_tailcall_id (f, args, _) ->
    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def

  | RTLabs.St_tailcall_ptr (f, args, _) ->
    let (f1, f2) = find_and_addr f lenv in
    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def

  | RTLabs.St_cond (r, lbl_true, lbl_false) ->
    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def

  | RTLabs.St_jumptable _ ->
    error "Jump tables not supported yet."

  | RTLabs.St_return None ->
    add_graph lbl (RTL.St_return []) def

  | RTLabs.St_return (Some r) ->
    add_graph lbl (RTL.St_return (find_local_env r lenv)) def


let translate_internal def =
  let runiverse = def.RTLabs.f_runiverse in
  let lenv =
    initialize_local_env runiverse
      (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in
  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
  let params = map_list_local_env lenv (List.map fst def.RTLabs.f_params) in
  let locals = map_list_local_env lenv (List.map fst def.RTLabs.f_locals) in
  let locals = set_of_list locals in
  let result = match def.RTLabs.f_result with
    | None -> []
    | Some (r, _) -> find_local_env r lenv in
  let res =
    { RTL.f_luniverse = def.RTLabs.f_luniverse ;
      RTL.f_runiverse = runiverse ;
      RTL.f_result    = result ;
      RTL.f_params    = params ;
      RTL.f_locals    = locals ;
      RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ;
      RTL.f_graph     = Label.Map.empty ;
      RTL.f_entry     = def.RTLabs.f_entry ;
      RTL.f_exit      = def.RTLabs.f_exit } in
  Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res


let translate_fun_def = function
  | RTLabs.F_int def -> RTL.F_int (translate_internal def)
  | RTLabs.F_ext def -> RTL.F_ext def


(* Add global initializations *)

let sum_offsets =
  let f res off = res + (concrete_offset off) in
  List.fold_left f 0

let assign_data addr1 addr2 addr1' addr2' off_r data_r tmpr def (offset, data) =
  if offset < 256 then
    let def =
      generates_graph
	[RTL.St_store (addr1', addr2', data_r, Label.dummy)] def in
    let start_lbl = fresh_label def in
    let dest_lbl = def.RTL.f_entry in
    let def =
      translate_op_ tmpr I8051.Addc
	[addr1' ; addr2'] [addr1 ; addr2] [off_r] start_lbl dest_lbl def in
    let def = change_entry def start_lbl in
    generates_graph
      [RTL.St_int (off_r, offset, Label.dummy) ;
       RTL.St_int (data_r, data, Label.dummy)] def
  else error ("offset too big to fit in a register when initializing globals.")

let assign_datas
    addr1 addr2 addr1' addr2' off_r data_r tmpr x def (offsets, data) =
  let base_offset = sum_offsets offsets in
  let (data, quantity) = match data with
    | AST.Data_int8  i -> (i, 1)
    | AST.Data_int16 i -> (i, 2)
    | AST.Data_int32 i -> (i, 4)
    | AST.Data_float32 f | AST.Data_float64 f -> error_float () in
  let data = IntValue.Int32.of_int data in
  let datas = IntValue.Int32.break data quantity in
  let datas = List.map IntValue.Int8.to_int datas in
  let added_offs = MiscPottier.make 0 (List.length datas) in
  let offs = MiscPottier.mapi (fun i _ -> base_offset + i) added_offs in
  assert (List.length offs = List.length datas) ;
  let offs_datas = List.combine offs datas in
  let def =
    List.fold_left (assign_data addr1 addr2 addr1' addr2' off_r data_r tmpr)
      def offs_datas in
  generates_graph [RTL.St_addr (addr1, addr2, x, Label.dummy)] def

let add_global_initializations_def globals def =
  let (def, addr1, addr2, addr1', addr2', off_r, data_r, tmpr) =
    match fresh_regs def 7 with
      | (def, [addr1 ; addr2 ; addr1' ; addr2' ; off_r ; data_r ; tmpr]) ->
	(def, addr1, addr2, addr1', addr2', off_r, data_r, tmpr)
      | _ ->
      (* should be impossible: [fresh_regs _ 7] returns 7 regs *)
      assert false in
  let f def (x, size, datas_opt) = match datas_opt with
    | None -> def
    | Some datas ->
      let offsets = Memory.all_offsets size in
      if List.length offsets <> List.length datas then
	error "bad global initialization style."
      else
	let offs_datas = List.combine offsets datas in
	List.fold_left
	  (assign_datas addr1 addr2 addr1' addr2' off_r data_r tmpr x)
	  def offs_datas in
  List.fold_left f def globals

let add_global_initializations_funct globals = function
  | RTL.F_int def ->
    let def = add_global_initializations_def globals def in
    RTL.F_int def
  | def -> def

(* [add_global_initializations p] moves the initializations of the globals of
   [p] to the beginning of the main function, if any. *)

let add_global_initializations globals main functs = match main with
  | None -> functs
  | Some main ->
    let main_def = List.assoc main functs in
    let main_def = add_global_initializations_funct globals main_def in
    MiscPottier.update_list_assoc main main_def functs


let translate p = 
  let f_global (id, size, _) = (id, concrete_size size) in
  let f_funct (id, fun_def) = (id, translate_fun_def fun_def) in
  let functs = List.map f_funct p.RTLabs.functs in
  let functs = add_global_initializations p.RTLabs.vars p.RTLabs.main functs in
  { RTL.vars   = List.map f_global p.RTLabs.vars ;
    RTL.functs = functs ;
    RTL.main   = p.RTLabs.main }