open Preamble

open Order

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open Registers

open Exp

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Russell

open Types

open List

open Util

open FoldStuff

open BitVector

open Arithmetic

open Jmeq

open Bool

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Nat

open I8051

open RegisterSet

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open GenMem

open FrontEndMem

open Globalenvs

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open CostLabel

open Hide

open Integers

open AST

open Division

open Z

open BitVectorZ

open Pointers

open ByteValues

open BackEndOps

open Joint

open RTL

open ERTL

open Deqsets_extra

open State

open Bind_new

open BindLists

open Blocks

open TranslateUtils

(** val save_hdws :
    AST.ident List.list -> (Registers.register, I8051.register) Types.prod
    List.list -> Joint.joint_seq List.list **)
let save_hdws globals =
  let save_hdws_internal = fun destr_srcr -> Joint.MOVE
    (Obj.magic { Types.fst = (ERTL.PSD destr_srcr.Types.fst); Types.snd =
      (ERTL.move_src_from_dst (ERTL.HDW destr_srcr.Types.snd)) })
  in
  List.map save_hdws_internal

(** val restore_hdws :
    AST.ident List.list -> (Joint.psd_argument, I8051.register) Types.prod
    List.list -> Joint.joint_seq List.list **)
let restore_hdws globals =
  let restore_hdws_internal = fun destr_srcr -> Joint.MOVE
    (Obj.magic { Types.fst = (ERTL.HDW destr_srcr.Types.snd); Types.snd =
      (ERTL.psd_argument_move_src destr_srcr.Types.fst) })
  in
  List.map restore_hdws_internal

(** val get_params_hdw :
    AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
    List.list **)
let get_params_hdw globals params =
  save_hdws globals (Util.zip_pottier params I8051.registerParams)

(** val get_param_stack :
    AST.ident List.list -> Registers.register -> Registers.register ->
    Registers.register -> Joint.joint_seq List.list **)
let get_param_stack globals addr1 addr2 destr =
  List.Cons ((Joint.LOAD ((Obj.magic destr),
    (Obj.magic (Joint.psd_argument_from_reg addr1)),
    (Obj.magic (Joint.psd_argument_from_reg addr2)))), (List.Cons ((Joint.OP2
    (BackEndOps.Add, (Obj.magic addr1),
    (Obj.magic (Joint.psd_argument_from_reg addr1)),
    (let x = I8051.int_size in Obj.magic (Joint.psd_argument_from_byte x)))),
    (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic addr2),
    (Obj.magic (Joint.psd_argument_from_reg addr2)),
    (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
    List.Nil)))))

(** val get_params_stack :
    AST.ident List.list -> Registers.register -> Registers.register ->
    Registers.register -> Registers.register List.list -> Joint.joint_seq
    List.list **)
let get_params_stack globals tmpr addr1 addr2 params =
  let params_length_byte =
    Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
      (Nat.S (Nat.S Nat.O)))))))) (List.length params)
  in
  List.append (List.Cons
    ((let x =
        ERTL.ertl_seq_joint globals (Obj.magic (ERTL.Ertl_frame_size tmpr))
      in
     x), (List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.OP2
    (BackEndOps.Sub, (Obj.magic tmpr),
    (Obj.magic (Joint.psd_argument_from_reg tmpr)),
    (Obj.magic (Joint.psd_argument_from_byte params_length_byte)))),
    (List.Cons ((Joint.MOVE
    (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
      (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })), (List.Cons
    ((Joint.MOVE
    (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
      (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })), (List.Cons
    ((Joint.OP2 (BackEndOps.Add, (Obj.magic addr1),
    (Obj.magic (Joint.psd_argument_from_reg addr1)),
    (Obj.magic (Joint.psd_argument_from_reg tmpr)))), (List.Cons ((Joint.OP2
    (BackEndOps.Addc, (Obj.magic addr2),
    (Obj.magic (Joint.psd_argument_from_reg addr2)),
    (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
    List.Nil))))))))))))))
    (List.flatten (List.map (get_param_stack globals addr1 addr2) params))

(** val get_params :
    AST.ident List.list -> Registers.register -> Registers.register ->
    Registers.register -> Registers.register List.list -> Joint.joint_seq
    List.list **)
let get_params globals tmpr addr1 addr2 params =
  let n = Nat.min (List.length params) (List.length I8051.registerParams) in
  let { Types.fst = hdw_params; Types.snd = stack_params } =
    Util.list_split n params
  in
  List.append (get_params_hdw globals hdw_params)
    (get_params_stack globals tmpr addr1 addr2 stack_params)

(** val save_return :
    AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
    List.list **)
let save_return globals ret_regs =
  let crl = Util.reduce_strong I8051.registerSTS ret_regs in
  let commonl = crl.Types.fst.Types.fst in
  let commonr = crl.Types.snd.Types.fst in
  let restl = crl.Types.fst.Types.snd in
  List.append
    (Util.map2 (fun st r -> Joint.MOVE
      (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
        (ERTL.psd_argument_move_src r) })) commonl commonr)
    (List.map (fun st -> Joint.MOVE
      (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
        (ERTL.byte_to_ertl_snd_argument__o__psd_argument_to_move_src
          Joint.zero_byte) })) restl)

(** val assign_result : AST.ident List.list -> Joint.joint_seq List.list **)
let assign_result globals =
  let crl = Util.reduce_strong I8051.registerRets I8051.registerSTS in
  let commonl = crl.Types.fst.Types.fst in
  let commonr = crl.Types.snd.Types.fst in
  Util.map2 (fun ret st -> Joint.MOVE
    (Obj.magic { Types.fst = (ERTL.HDW ret); Types.snd =
      (ERTL.move_src_from_dst (ERTL.HDW st)) })) commonl commonr

(** val epilogue :
    AST.ident List.list -> Registers.register List.list -> Registers.register
    -> Registers.register -> (Registers.register, I8051.register) Types.prod
    List.list -> Joint.joint_seq List.list Types.sig0 **)
let epilogue globals ret_regs sral srah sregs =
  List.append
    (save_return globals (List.map (fun x -> Joint.Reg x) ret_regs))
    (List.append
      (restore_hdws globals
        (List.map (fun pr -> { Types.fst = (Joint.Reg pr.Types.fst);
          Types.snd = pr.Types.snd }) sregs))
      (List.append (List.Cons ((Joint.PUSH
        (Obj.magic (Joint.psd_argument_from_reg sral))), (List.Cons
        ((Joint.PUSH (Obj.magic (Joint.psd_argument_from_reg srah))),
        (List.Cons
        ((ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_del_frame)),
        List.Nil)))))) (assign_result globals)))

(** val prologue :
    AST.ident List.list -> Registers.register List.list -> Registers.register
    -> Registers.register -> Registers.register -> Registers.register ->
    Registers.register -> (Registers.register, I8051.register) Types.prod
    List.list -> (Registers.register, Joint.joint_seq List.list)
    Bind_new.bind_new **)
let prologue globals params sral srah tmpr addr1 addr2 sregs =
  let l =
    List.append (List.Cons
      ((let x = ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_new_frame)
        in
       x), (List.Cons ((Joint.POP (Obj.magic srah)), (List.Cons ((Joint.POP
      (Obj.magic sral)), List.Nil))))))
      (List.append (save_hdws globals sregs)
        (get_params globals tmpr addr1 addr2 params))
  in
  Bind_new.Bret l

(** val set_params_hdw :
    AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
    List.list **)
let set_params_hdw globals params =
  restore_hdws globals (Util.zip_pottier params I8051.registerParams)

(** val set_param_stack :
    AST.ident List.list -> Registers.register -> Registers.register ->
    Joint.psd_argument -> Joint.joint_seq List.list **)
let set_param_stack globals addr1 addr2 arg =
  List.Cons ((Joint.STORE ((Obj.magic (Joint.psd_argument_from_reg addr1)),
    (Obj.magic (Joint.psd_argument_from_reg addr2)), (Obj.magic arg))),
    (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic addr1),
    (Obj.magic (Joint.psd_argument_from_reg addr1)),
    (let x = I8051.int_size in Obj.magic (Joint.psd_argument_from_byte x)))),
    (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic addr2),
    (Obj.magic (Joint.psd_argument_from_reg addr2)),
    (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
    List.Nil)))))

(** val set_params_stack :
    AST.ident List.list -> Joint.psd_argument List.list ->
    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
let set_params_stack globals params =
  Bind_new.Bnew (fun addr1 -> Bind_new.Bnew (fun addr2 ->
    let params_length_byte =
      Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
        (Nat.S (Nat.S Nat.O)))))))) (List.length params)
    in
    let l =
      List.append (List.Cons ((Joint.MOVE
        (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
          (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
        (List.Cons ((Joint.MOVE
        (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
          (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
        (List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.OP2
        (BackEndOps.Sub, (Obj.magic addr1),
        (Obj.magic (Joint.psd_argument_from_reg addr1)),
        (Obj.magic (Joint.psd_argument_from_byte params_length_byte)))),
        (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic addr2),
        (Obj.magic (Joint.psd_argument_from_reg addr2)),
        (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
        List.Nil))))))))))
        (List.flatten
          (List.map (set_param_stack globals addr1 addr2) params))
    in
    Bind_new.Bret l))

(** val set_params :
    AST.ident List.list -> Joint.psd_argument List.list ->
    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
    Types.sig0 **)
let set_params globals params =
  let n = Nat.min (List.length params) (List.length I8051.registerParams) in
  let hdw_stack_params = List.split params n in
  let hdw_params = hdw_stack_params.Types.fst in
  let stack_params = hdw_stack_params.Types.snd in
  BindLists.bappend
    (let l = set_params_hdw globals hdw_params in Bind_new.Bret l)
    (set_params_stack globals stack_params)

(** val fetch_result :
    AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
    List.list Types.sig0 **)
let fetch_result globals ret_regs =
  (let crl = Util.reduce_strong I8051.registerSTS I8051.registerRets in
    (fun _ ->
    let commonl = crl.Types.fst.Types.fst in
    let commonr = crl.Types.snd.Types.fst in
    List.append
      (Util.map2 (fun st r -> Joint.MOVE
        (Obj.magic { Types.fst = (ERTL.HDW st); Types.snd =
          (ERTL.move_src_from_dst (ERTL.HDW r)) })) commonl commonr)
      (let crl0 = Util.reduce_strong ret_regs I8051.registerSTS in
      let commonl0 = crl0.Types.fst.Types.fst in
      let commonr0 = crl0.Types.snd.Types.fst in
      Util.map2 (fun ret st -> Joint.MOVE
        (Obj.magic { Types.fst = (ERTL.PSD ret); Types.snd =
          (ERTL.move_src_from_dst (ERTL.HDW st)) })) commonl0 commonr0))) __

(** val translate_step :
    AST.ident List.list -> Graphs.label -> Joint.joint_step ->
    Blocks.bind_step_block **)
let translate_step globals x = function
| Joint.COST_LABEL lbl ->
  Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
    Joint.COST_LABEL lbl) }; Types.snd = List.Nil }
| Joint.CALL (f, args, ret_regs) ->
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
      (Types.pi1 (Obj.magic (set_params globals (Obj.magic args))))
      (fun pref ->
      Obj.magic (Bind_new.Bret { Types.fst = { Types.fst =
        (Blocks.add_dummy_variance pref); Types.snd = (fun x0 -> Joint.CALL
        (f, (Obj.magic (List.length (Obj.magic args))),
        (Obj.magic Types.It))) }; Types.snd =
        (Types.pi1 (fetch_result globals (Obj.magic ret_regs))) })))
| Joint.COND (r, ltrue) ->
  Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
    Joint.COND (r, ltrue)) }; Types.snd = List.Nil }
| Joint.Step_seq s0 ->
  Bind_new.Bret
    (match s0 with
     | Joint.COMMENT msg ->
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals (List.Cons ((Joint.COMMENT msg), List.Nil))
     | Joint.MOVE rs ->
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals (List.Cons ((Joint.MOVE
         (Obj.magic { Types.fst = (ERTL.PSD (Obj.magic rs).Types.fst);
           Types.snd =
           (ERTL.psd_argument_move_src (Obj.magic rs).Types.snd) })),
         List.Nil))
     | Joint.POP x0 ->
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals List.Nil
     | Joint.PUSH x0 ->
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals List.Nil
     | Joint.ADDRESS (x0, off, r1, r2) ->
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals (List.Cons ((Joint.ADDRESS (x0, off, r1, r2)), List.Nil))
     | Joint.OPACCS (op, destr1, destr2, srcr1, srcr2) ->
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals (List.Cons ((Joint.OPACCS (op, destr1, destr2, srcr1,
         srcr2)), List.Nil))
     | Joint.OP1 (op1, destr, srcr) ->
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals (List.Cons ((Joint.OP1 (op1, destr, srcr)), List.Nil))
     | Joint.OP2 (op2, destr, srcr1, srcr2) ->
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals (List.Cons ((Joint.OP2 (op2, destr, srcr1, srcr2)),
         List.Nil))
     | Joint.CLEAR_CARRY ->
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
     | Joint.SET_CARRY ->
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals (List.Cons (Joint.SET_CARRY, List.Nil))
     | Joint.LOAD (destr, addr1, addr2) ->
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals (List.Cons ((Joint.LOAD (destr, addr1, addr2)), List.Nil))
     | Joint.STORE (addr1, addr2, srcr) ->
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals (List.Cons ((Joint.STORE (addr1, addr2, srcr)), List.Nil))
     | Joint.Extension_seq ext ->
       let RTL.Rtl_stack_address (addr1, addr2) = Obj.magic ext in
       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
         globals (List.Cons ((Joint.MOVE
         (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
           (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
         (List.Cons ((Joint.MOVE
         (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
           (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
         List.Nil)))))

(** val translate_fin_step :
    AST.ident List.list -> Registers.register List.list -> Registers.register
    -> Registers.register -> (Registers.register, I8051.register) Types.prod
    List.list -> Graphs.label -> Joint.joint_fin_step ->
    Blocks.bind_fin_block **)
let translate_fin_step globals ret_regs ral rah to_restore x = function
| Joint.GOTO lbl' ->
  Bind_new.Bret { Types.fst = List.Nil; Types.snd = (Joint.GOTO lbl') }
| Joint.RETURN ->
  Bind_new.Bret { Types.fst =
    (Types.pi1 (epilogue globals ret_regs ral rah to_restore)); Types.snd =
    Joint.RETURN }
| Joint.TAILCALL (x0, x1) -> assert false (* absurd case *)

(** val allocate_regs :
    ((Registers.register, I8051.register) Types.prod List.list ->
    (Registers.register, 'a1) Bind_new.bind_new) -> (Registers.register, 'a1)
    Bind_new.bind_new **)
let allocate_regs f =
  let allocate_regs_internal = fun acc r ->
    Monad.m_bind0 (Monad.max_def Bind_new.bindNew) acc (fun tl ->
      Obj.magic (Bind_new.Bnew (fun r' ->
        Obj.magic
          (Monad.m_return0 (Monad.max_def Bind_new.bindNew) (List.Cons
            ({ Types.fst = r'; Types.snd = r }, tl))))))
  in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
      (Util.foldl allocate_regs_internal
        (Monad.m_return0 (Monad.max_def Bind_new.bindNew) List.Nil)
        I8051.registerCalleeSaved) (fun to_save -> Obj.magic f to_save))

(** val translate_data :
    AST.ident List.list -> Joint.joint_closed_internal_function ->
    TranslateUtils.bound_b_graph_translate_data **)
let translate_data globals def =
  let params = (Types.pi1 def).Joint.joint_if_params in
  let new_stacksize =
    Nat.plus (Types.pi1 def).Joint.joint_if_stacksize
      (Nat.minus (List.length (Obj.magic params))
        (List.length I8051.registerParams))
  in
  allocate_regs (fun to_save -> Bind_new.Bnew (fun ral -> Bind_new.Bnew
    (fun rah -> Bind_new.Bnew (fun tmpr -> Bind_new.Bnew (fun addr1 ->
    Bind_new.Bnew (fun addr2 ->
    Obj.magic
      (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
        (Obj.magic
          (prologue globals (Obj.magic params) ral rah tmpr addr1 addr2
            to_save)) (fun prologue0 ->
        Monad.m_return0 (Monad.max_def Bind_new.bindNew)
          { TranslateUtils.init_ret = (Obj.magic Types.It);
          TranslateUtils.init_params =
          (Obj.magic (List.length (Obj.magic params)));
          TranslateUtils.init_stack_size = new_stacksize;
          TranslateUtils.added_prologue = prologue0;
          TranslateUtils.new_regs =
          (List.reverse (List.Cons (addr2, (List.Cons (addr1, (List.Cons
            (tmpr, (List.Cons (rah, (List.Cons (ral,
            (List.map (fun x -> x.Types.fst) to_save))))))))))));
          TranslateUtils.f_step = (translate_step globals);
          TranslateUtils.f_fin =
          (translate_fin_step globals
            (Obj.magic (Types.pi1 def).Joint.joint_if_result) ral rah
            to_save) }))))))))

(** val rtl_to_ertl : RTL.rtl_program -> ERTL.ertl_program **)
let rtl_to_ertl =
  TranslateUtils.b_graph_transform_program RTL.rTL ERTL.eRTL translate_data