source: Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml @ 2169

(** 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 dummy = Label.dummy

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 rec int_to_args (size : int) = function

  | AST.Cst_int i ->
    let module M = IntValue.Make (struct let size = size end) in
    let chunks = M.break (M.of_int i) size in
    List.map (fun x -> RTL.Imm (M.to_int x)) chunks

  | AST.Cst_float _ -> error_float ()

  | AST.Cst_offset off ->
    let i = concrete_offset off in
    int_to_args size (AST.Cst_int i)

  | AST.Cst_sizeof size' ->
    let i = concrete_size size' in
    int_to_args size (AST.Cst_int i)

  | _ -> assert false (* should not be called on non-int arguments *)

let find_local_env_reg = Register.Map.find

let find_local_env a env = match a with
  | RTLabs.Reg r -> List.map (fun r -> RTL.Reg r) (Register.Map.find r env)
  | RTLabs.Imm (k, t) -> int_to_args (size_of_sig_type t) k

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_reg lenv regs =
  let f res r = res @ (find_local_env_reg 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_reg 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_cond _ | RTL.St_return _) as inst -> inst
  | stmt -> RTLGraph.fill_succs stmt [lbl]

(* 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

(* 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_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

(* translate non-int constants *)
and translate_cst cst destrs start_lbl = match destrs, cst with

  | [], _ -> adds_graph [] start_lbl

  | _, AST.Cst_float _ -> error_float ()

  | _, AST.Cst_addrsymbol id ->
    let (r1, r2) = make_addr destrs in
    adds_graph [RTL.St_addr (r1, r2, id, start_lbl)] start_lbl

  | _, AST.Cst_stack ->
    let (r1, r2) = make_addr destrs in
    adds_graph [RTL.St_stackaddr (r1, r2, start_lbl)] start_lbl

  | _ ->
    let srcrs = int_to_args (List.length destrs) cst in
    translate_move destrs srcrs start_lbl


let translate_cast_unsigned destrs start_lbl dest_lbl def =
  translate_cst (AST.Cst_int 0) destrs start_lbl dest_lbl def

let sign_mask destr srcr =
    (* this sets tmpr to 0xFF if s is neg, 0x00 o.w. Done like that:
       byte in tmpr if srcr is: neg   |  pos
       tmpr ← srcr | 127       11...1 | 01...1
       tmpr ← tmpr <rot< 1     1...11 | 1...10
       tmpr ← INC tmpr         0....0 | 1....1
       tmpr ← CPL tmpr         1....1 | 0....0

     *)
  [RTL.St_op2 (I8051.Or, destr, srcr, RTL.Imm 127, dummy) ;
   RTL.St_op1 (I8051.Rl, destr, destr, dummy) ;
   RTL.St_op1 (I8051.Inc, destr, destr, dummy) ;
   RTL.St_op1 (I8051.Cmpl, destr, destr, dummy) ]


let translate_cast_signed destrs srcr start_lbl dest_lbl def =
  let (def, tmpr) = fresh_reg def in
  let srcrs = MiscPottier.make (RTL.Reg tmpr) (List.length destrs) in
  add_translates [adds_graph (sign_mask tmpr srcr); translate_move destrs srcrs]
    start_lbl dest_lbl def

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, _)) = MiscPottier.reduce destrs srcrs in
      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]


let translate_negint destrs srcrs start_lbl dest_lbl def =
  let f_cmpl destr = function
    | RTL.Reg r -> RTL.St_op1 (I8051.Cmpl, destr, r, start_lbl)
    | RTL.Imm k -> RTL.St_move (destr, RTL.Imm (lnot k), start_lbl) in
  let insts_cmpl = List.map2 f_cmpl destrs srcrs in
  match destrs with
    | destr :: destrs ->
      let inst_init =
        RTL.St_op2 (I8051.Add, destr, RTL.Reg destr, RTL.Imm 1, start_lbl) in
      let f_add destr =
        RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Imm 0, start_lbl) in
      let insts_add = List.map f_add destrs in
      adds_graph (insts_cmpl @ inst_init :: insts_add)
        start_lbl dest_lbl def
    | [] ->
      adds_graph [] start_lbl dest_lbl def


let translate_notbool destrs srcrs start_lbl dest_lbl def =
  match destrs,srcrs with
    | [], _ -> adds_graph [] start_lbl dest_lbl def
    | destr :: destrs, srcr :: srcrs ->
      let (def, tmpr) = fresh_reg def in
      let init_destr = RTL.St_move (destr, srcr, start_lbl) in
      let f r =
        RTL.St_op2 (I8051.Or, destr, RTL.Reg destr, r, start_lbl) in
      let big_or = List.map f srcrs in
      let finalize_destr =
        [RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
         RTL.St_clear_carry start_lbl ;
         RTL.St_op2 (I8051.Sub, tmpr, RTL.Reg tmpr, RTL.Reg destr, start_lbl) ;
         (* carry bit is set iff destr is non-zero iff destrs was non-zero *)
         RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
         RTL.St_op2 (I8051.Addc, destr, RTL.Reg tmpr, RTL.Reg tmpr, start_lbl) ;
         (* destr = carry bit = bigor of old destrs *)
         RTL.St_op2 (I8051.Xor, destr, RTL.Reg destr, RTL.Imm 1, start_lbl)] in
      let epilogue = translate_cst (AST.Cst_int 0) destrs in
      add_translates [adds_graph (init_destr :: big_or @ finalize_destr) ;
                      epilogue]
        start_lbl dest_lbl def
    | destr :: destrs, [] ->
      translate_cst (AST.Cst_int 1) destrs 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 = function
      | RTL.Reg srcr ->  RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl)
      | RTL.Imm k -> RTL.St_move (destr, RTL.Imm (lnot k), 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


let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
  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
  let ((destrs_cted, destrs_rest), (srcrs_cted, _)) =
    MiscPottier.reduce destrs_rest srcrs_rest in
  let carry_init = match op with
    | I8051.Sub | I8051.Addc ->
      (* depend on carry bit *)
      [RTL.St_clear_carry start_lbl]
    | _ -> [] in
  let f_add op destr srcr1 srcr2 =
    RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
  let insts_add =
    match op with
      | I8051.Add ->
        (* we perform a first add followed by Addc's *)
        begin match destrs_common, srcrs1_common, srcrs2_common with
          | destr :: destrs, srcr1 :: srcrs1, srcr2 :: srcrs2 ->
            f_add op destr srcr1 srcr2 ::
              MiscPottier.map3 (f_add I8051.Addc) destrs srcrs1 srcrs2
          | [], [], [] -> []
          | _ -> assert false
        end
      | _ ->
        (* we just do the same operation on all *)
        MiscPottier.map3 (f_add op) destrs_common srcrs1_common srcrs2_common in
  let f_add_cted destr srcr =
    RTL.St_op2 (op, destr, srcr, RTL.Imm 0, start_lbl) in
  let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
  let f_rest destr =
    match op with
      | I8051.Addc | I8051.Sub ->
        (* propagate carry bit *)
        RTL.St_op2 (op, destr, RTL.Imm 0, RTL.Imm 0, start_lbl)
      | _ ->
        RTL.St_move (destr, RTL.Imm 0, start_lbl) in
  let insts_rest = List.map f_rest destrs_rest in
  adds_graph (carry_init @ insts_add @ insts_add_cted @ insts_rest)
    start_lbl dest_lbl def


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], [] ->
      adds_graph
        [RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Imm 0, start_lbl)]
        start_lbl
    | destr1 :: destr2 :: destrs, [] ->
      add_translates
        [adds_graph
            [RTL.St_op2 (I8051.Addc, destr1,
                         RTL.Reg destr1, RTL.Imm 0, start_lbl) ;
             RTL.St_op2 (I8051.Addc, destr2, RTL.Imm 0, RTL.Imm 0, start_lbl)] ;
         translate_cst (AST.Cst_int 0) destrs]
        start_lbl
    | [destr], srcr1 :: _ ->
      adds_graph
        [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ;
         RTL.St_op2 (I8051.Addc, destr, RTL.Reg destr, RTL.Reg tmpr, start_lbl)]
        start_lbl
    | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 ->
      add_translates
        [adds_graph
            [RTL.St_opaccs
                (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ;
             RTL.St_op2 (I8051.Addc, destr1, RTL.Reg destr1,
                         RTL.Reg tmpr, start_lbl)] ;
         translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2]
        start_lbl

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 ;
                     RTL.St_move (tmp_destr2, RTL.Imm 0, dummy_lbl)] ;
         translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
         translate_cst (AST.Cst_int 0) tmp_destrs1 ;
         let reg_destrs = List.map (fun r -> RTL.Reg r) destrs in
         let tmp_destrs = List.map (fun r -> RTL.Reg r) tmp_destrs in
         translate_op I8051.Addc destrs reg_destrs tmp_destrs])

let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
  let (def, dummy) = fresh_reg def in
  let (def, tmpr) = fresh_reg def in
  let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
  let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
  (* let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in *)
  let reg r = RTL.Reg r in
  let insts_init =
    [translate_move fresh_srcrs1 srcrs1 ;
     (* translate_move fresh_srcrs2 srcrs2 ; *)
     translate_cst (AST.Cst_int 0) destrs] in
  let fresh_srcrs1 = List.map reg fresh_srcrs1 in
  let f = translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
  let insts_mul = MiscPottier.foldi f [] srcrs2 in
  add_translates (insts_init @ insts_mul) start_lbl dest_lbl def


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

let translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def =
  match destrs with
    | [] -> adds_graph [] start_lbl dest_lbl def
    | destr :: destrs ->
      let (def, tmpr) = fresh_reg def in
      let ((common1, rest1), (common2, rest2)) =
        MiscPottier.reduce srcrs1 srcrs2 in
      let rest = choose_rest rest1 rest2 in
      let firsts = match common1, common2 with
        | c1hd :: c1tl, c2hd :: c2tl ->
          let init =
            RTL.St_op2 (I8051.Xor, destr, c1hd, c2hd, start_lbl) in
          let f_common tmp_srcr1 tmp_srcr2 =
            [RTL.St_op2 (I8051.Xor, tmpr, tmp_srcr1, tmp_srcr2, start_lbl) ;
             RTL.St_op2 (I8051.Or, destr, RTL.Reg destr,
                         RTL.Reg tmpr, start_lbl)] in
          let insts_common = List.flatten (List.map2 f_common c1tl c2tl) in
          init :: insts_common
        | [], [] ->
          [RTL.St_move (destr, RTL.Imm 0, start_lbl)]
        (* common1 and common2 have the same length *)
        | _ -> assert false in
      let f_rest tmp_srcr =
        RTL.St_op2 (I8051.Xor, destr, RTL.Reg destr,
                    tmp_srcr, start_lbl) in
      let insts_rest = List.map f_rest rest in
      let insts = firsts @ insts_rest in
      let epilogue = translate_cst (AST.Cst_int 0) destrs in
      add_translates [ adds_graph insts ; epilogue] start_lbl dest_lbl def

(* this requires destrs to be either 0 or 1 to be truly correct
   to be used after translations that ensure this *)
let translate_toggle_bool destrs start_lbl =
  match destrs with
    | [] -> adds_graph [] start_lbl
    | destr :: _ ->
      adds_graph [RTL.St_op2 (I8051.Xor, destr, RTL.Reg destr,
                              RTL.Imm 1, start_lbl)] start_lbl

let rec pad_with p l1 l2 = match l1, l2 with
  | [], [] -> ([], [])
  | x :: xs, y :: ys ->
    let (xs', ys') = pad_with p xs ys in
    (x :: xs', y :: ys')
  | [], _ -> (MiscPottier.make p (List.length l2), l2)
  | _, [] -> (l1, MiscPottier.make p (List.length l1))

let translate_ltu desrtrs srcrs1 srcrs2 start_lbl dest_lbl def =
  match desrtrs with
    | [] -> adds_graph [] start_lbl dest_lbl def
    | destr :: destrs ->
      let (srcrs1, srcrs2) = pad_with (RTL.Imm 0) srcrs1 srcrs2 in
      let init = RTL.St_clear_carry start_lbl in
      let f srcr1 srcr2 =
        RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) in
      (* not interested in result, just the carry bit
         the following is safe even if destrs = srcrsi *)
      let iter_sub = List.map2 f srcrs1 srcrs2 in
      let extract_carry =
        [RTL.St_op2 (I8051.Addc, destr, RTL.Imm 0,
                     RTL.Imm 0, start_lbl)] in
      let epilogue = translate_cst (AST.Cst_int 0) destrs in
      add_translates [adds_graph (init :: iter_sub @ extract_carry);
                      epilogue] start_lbl dest_lbl def

let rec add_128_to_last
    (last_subst : Register.t)
    (rs : RTL.argument list)
    (dummy_lbl : Label.t) = match rs with
  | [] -> ([], adds_graph [])
  | [last] ->
    let insts =
      [RTL.St_move (last_subst, last, dummy_lbl) ;
       RTL.St_op2 (I8051.Add, last_subst, RTL.Reg last_subst,
                   RTL.Imm 128, dummy_lbl)] in
    ([RTL.Reg last_subst], adds_graph insts)
  | hd :: tail ->
    let (tail', trans) = add_128_to_last last_subst tail dummy_lbl in
    (hd :: tail', trans)

(* Paolo: what happens if srcrs1 and srcrs2 have different length? seems to me
   128 is added at the wrong place then *)
let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def =
  let (def, tmp_last_srcr1) = fresh_reg def in
  let (def, tmp_last_srcr2) = fresh_reg def in
  (* I save just the last registers *)
  let (srcrs1, add_128_to_srcrs1) =
    add_128_to_last tmp_last_srcr1 srcrs1 start_lbl in
  let (srcrs2, add_128_to_srcrs2) =
    add_128_to_last tmp_last_srcr2 srcrs2 start_lbl in
  add_translates
    [add_128_to_srcrs1;
     add_128_to_srcrs2;
     translate_ltu destrs srcrs1 srcrs2]
    start_lbl dest_lbl def


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

    | AST.Op_add | AST.Op_addp ->
      translate_op I8051.Add 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_ne destrs srcrs1 srcrs2 ;
         translate_toggle_bool 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_ltu destrs srcrs1 srcrs2 start_lbl dest_lbl def

    | AST.Op_cmp AST.Cmp_le ->
      add_translates
        [translate_lts destrs srcrs2 srcrs1 ;
         translate_toggle_bool destrs] start_lbl dest_lbl def

    | AST.Op_cmpu AST.Cmp_le | AST.Op_cmpp AST.Cmp_le ->
      add_translates
        [translate_ltu destrs srcrs2 srcrs1 ;
         translate_toggle_bool destrs] start_lbl dest_lbl def

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

    | AST.Op_cmpu AST.Cmp_gt | AST.Op_cmpp AST.Cmp_gt ->
      translate_ltu destrs srcrs2 srcrs1 start_lbl dest_lbl def

    | AST.Op_cmp AST.Cmp_ge ->
      add_translates
        [translate_lts destrs srcrs1 srcrs2 ;
         translate_toggle_bool destrs] start_lbl dest_lbl def

    | AST.Op_cmpu AST.Cmp_ge | AST.Op_cmpp AST.Cmp_ge ->
      add_translates
        [translate_ltu destrs srcrs1 srcrs2 ;
         translate_toggle_bool 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


let translate_cond srcrs start_lbl lbl_true lbl_false def =
  match srcrs with
    | [] -> add_graph start_lbl (RTL.St_skip lbl_false) def
    | srcr :: srcrs ->
      let (def, tmpr) = fresh_reg def in
      let tmp_lbl = fresh_label def in
      let init = RTL.St_move (tmpr, RTL.Reg srcr, start_lbl) in
      let f srcr = RTL.St_op2 (I8051.Or, tmpr, RTL.Reg tmpr,
                               RTL.Reg 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


let translate_load addr destrs start_lbl dest_lbl def =
  let (def, tmp_addr) = fresh_regs def 2 in
  let (tmp_addr1, tmp_addr2) = make_addr tmp_addr in
  let save_addr a (saves, def, rs) = match a with
    | RTL.Reg r when List.exists (Register.equal r) destrs ->
      let (def, tmp) = fresh_reg def in
      (RTL.St_move (tmp, RTL.Reg r, start_lbl) :: saves, def, RTL.Reg tmp :: rs)
    | _ as a -> (saves, def, a :: rs) in
  let (saves, def, addr) = List.fold_right save_addr addr ([], def, []) in
  let (def, tmpr) = fresh_reg def in
  let f (translates, off) r =
    let translates =
      translates @
        [translate_op2 AST.Op_addp tmp_addr addr [RTL.Imm off] ;
         adds_graph [RTL.St_load (r, RTL.Reg tmp_addr1,
                                  RTL.Reg tmp_addr2, dest_lbl)]] in
    (translates, off + Driver.TargetArch.int_size) in
  let (translates, _) = List.fold_left f ([], 0) destrs in
  add_translates 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 @
        [translate_op2 AST.Op_addp tmp_addr addr [RTL.Imm off] ;
         adds_graph [RTL.St_store (RTL.Reg tmp_addr1,
                                   RTL.Reg 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_ind_0 (i, lbl') ->
    add_graph lbl (RTL.St_ind_0 (i, lbl')) def

  | RTLabs.St_ind_inc (i, lbl') ->
    add_graph lbl (RTL.St_ind_inc (i, lbl')) def

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

  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
    translate_op1 op1
      (find_local_env_reg destr lenv)
      (List.map (fun r -> RTL.Reg r) (find_local_env_reg srcr lenv))
      lbl lbl' def

  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
    translate_op2 op2 (find_local_env_reg 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_reg 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_reg 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_reg 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_reg r lenv) lbl lbl_true lbl_false def

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

  | RTLabs.St_return ->
    add_graph lbl RTL.St_return def

open BList.Notation

open BList.Notation

let remove_non_int_immediates def =
  let load_arg a f = match a with
    | RTLabs.Imm ((AST.Cst_stack _ | AST.Cst_addrsymbol _) as c, t) ->
      fresh_t t (fun tmp ->
      RTLabs.St_cst (tmp, c, Label.dummy) ^:: f (RTLabs.Reg tmp))
    | _ -> f a in
  let rec load_args args f = match args with
    | [] -> f []
    | a :: args ->
      load_arg a (fun a -> load_args args (fun l -> f (a :: l))) in
  let trans lbl = function
    | RTLabs.St_op2(op, r, a1, a2, l) ->
      load_arg a1 (fun a1 ->
        load_arg a2 (fun a2 ->
          RTLabs.St_op2 (op, r, a1, a2, l) ^:: bnil))
    | RTLabs.St_store(q, a1, a2, l) ->
      load_arg a1 (fun a1 ->
        load_arg a2 (fun a2 ->
          RTLabs.St_store (q, a1, a2, l) ^:: bnil))
    | RTLabs.St_load (q, a, r, l) ->
      load_arg a (fun a ->
        RTLabs.St_load (q, a, r, l) ^:: bnil)
    | RTLabs.St_call_id (f, args, ret, s, l) ->
      load_args args (fun args ->
        RTLabs.St_call_id (f, args, ret, s, l) ^:: bnil)
    | RTLabs.St_tailcall_id (f, args, s) ->
      load_args args (fun args ->
        RTLabs.St_tailcall_id (f, args, s) ^:: bnil)
    | RTLabs.St_call_ptr (f, args, ret, s, l) ->
      load_args args (fun args ->
        RTLabs.St_call_ptr (f, args, ret, s, l) ^:: bnil)
    | RTLabs.St_tailcall_ptr (f, args, s) ->
      load_args args (fun args ->
        RTLabs.St_tailcall_ptr (f, args, s) ^:: bnil)
    | stmt -> stmt ^:: bnil in
  let module T = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph) in
  let g = def.RTLabs.f_graph in
  let fresh_reg def t =
    let r = Register.fresh def.RTLabs.f_runiverse in
    let locals = (r, t) :: def.RTLabs.f_locals in
    ({ def with RTLabs.f_locals = locals }, r) in
  let fresh_lbl () = Label.Gen.fresh def.RTLabs.f_luniverse in
  let (def, g) = T.translate' fresh_lbl fresh_reg trans def g in
  { def with RTLabs.f_graph = g }
 
let translate_internal def =
  let def = remove_non_int_immediates def in
  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_reg lenv (List.map fst def.RTLabs.f_params) in
  let locals = map_list_local_env_reg 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_reg 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


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
  { RTL.vars   = List.map f_global p.RTLabs.vars ;
    RTL.functs = List.map f_funct p.RTLabs.functs ;
    RTL.main   = p.RTLabs.main }