include "LTL/LTL.ma".
include "ERTL/Interference.ma".
include "ASM/Arithmetic.ma".
include "joint/TranslateUtils.ma".

(* Note: translation is complicated by having to preserve the carry bit and
  wanting to do it with as less boilerplate as possible. It could be somewhat
  simplified if constant and copy propagation was to be done after this pass:
  those optimisations would take care of the boilerplate for us.*)

coercion Reg_to_dec : ∀r:Register.decision ≝ decision_colour on _r : Register to decision.

inductive arg_decision : Type[0] ≝
  | arg_decision_colour : Register → arg_decision
  | arg_decision_spill : ℕ → arg_decision
  | arg_decision_imm : Byte → arg_decision.

coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision.

(* Paolo: I'm changing the following: before, spilled registers were
  assigned stack addresses going from SP + #frame_size - #stack_params
  excluded down to SP included. I am turning it upside down, so that
  the offset does not need the stack size to be computed *)

definition preserve_carry_bit :
  ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝
  λglobals,do_it,steps.
  if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.

(* for notation *)
definition A ≝ it.

coercion beval_of_byte : ∀b : Byte.beval ≝ BVByte on _b : Byte to beval.

(* spill should be byte-based from the start *)
definition set_dp_by_offset :
  ∀globals.nat → list (joint_seq LTL globals) ≝
  λglobals,off.
  [ A ← byte_of_nat off
  ; A ← A .Add. RegisterSPL
  ; RegisterDPL ← A
  ; A ← zero_byte
  ; A ← A .Addc. RegisterSPH
  ; RegisterDPH ← A
  ].

definition get_stack:
 ∀globals.nat → Register → nat → list (joint_seq LTL globals) ≝
 λglobals,localss,r,off.
 let off ≝ localss + off in
 set_dp_by_offset ? off @
 [ LOAD … A it it ] @
 if eq_Register r RegisterA then [ ] else [ r ← A ].

definition set_stack_not_a :
 ∀globals.nat → nat → Register → list (joint_seq LTL globals) ≝
 λglobals,localss,off,r.
 let off ≝ localss + off in
 set_dp_by_offset ? off @
 [ A ← r
 ; STORE … it it A ].

definition set_stack_a :
 ∀globals.nat → nat → list (joint_seq LTL globals) ≝
 λglobals,localss,off.
 [ RegisterST1 ← A ] @
 set_stack_not_a ? localss off RegisterST1.

definition set_stack :
 ∀globals.nat → nat → Register → list (joint_seq LTL globals) ≝
 λglobals,localss,off,r.
 if eq_Register r RegisterA then
   set_stack_a ? localss off
 else
   set_stack_not_a ? localss off r.
 
definition set_stack_int :
  ∀globals.nat → nat → Byte →  list (joint_seq LTL globals) ≝
  λglobals,localss,off,int.
  let off ≝ localss + off in
  set_dp_by_offset ? off @
  [ A ← int
  ; STORE … it it A ].

definition move :
  ∀globals.nat → bool → decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,localss,carry_lives_after,dst,src.
  match dst with
  [ decision_colour dstr ⇒
    match src with
    [ arg_decision_colour srcr ⇒
      if eq_Register dstr srcr then [ ] else
      if eq_Register dstr RegisterA then [ A ← srcr ] else
      if eq_Register srcr RegisterA then [ dstr ← A ] else
      [ A ← srcr ; dstr ← A]
    | arg_decision_spill srco ⇒
      preserve_carry_bit ? carry_lives_after
        (get_stack ? localss dstr srco)
    | arg_decision_imm int ⇒
      [ A ← int ] @
      if eq_Register dstr RegisterA then [ ] else
      [ dstr ← A ]
    ]
  | decision_spill dsto ⇒
    match src with
    [ arg_decision_colour srcr ⇒
      preserve_carry_bit ? carry_lives_after
        (set_stack ? localss dsto srcr)
    | arg_decision_spill srco ⇒
      if eqb srco dsto then [ ] else
      preserve_carry_bit ? carry_lives_after
        (get_stack ? localss RegisterA srco @
         set_stack ? localss dsto RegisterA)
    | arg_decision_imm int ⇒
      preserve_carry_bit ? carry_lives_after
        (set_stack_int ? localss dsto int)
    ]
  ].

definition arg_is_spilled : arg_decision → bool ≝
  λx.match x with [ arg_decision_spill _ ⇒ true | _ ⇒ false ].
definition is_spilled : decision → bool ≝
  λx.match x with [ decision_spill _ ⇒ true | _ ⇒ false ].

definition newframe :
  ∀globals.ℕ → list (joint_seq LTL globals) ≝
  λglobals,stack_sz.
  [ CLEAR_CARRY …
  ; A ← RegisterSPL
  ; A ← A .Sub. byte_of_nat stack_sz
  ; RegisterSPL ← A
  ; A ← RegisterSPH
  ; A ← A .Sub. zero_byte
  ; RegisterSPH ← A
  ].

definition delframe :
  ∀globals.ℕ → list (joint_seq LTL globals) ≝
  λglobals,stack_sz.
  [ A ← RegisterSPL
  ; A ← A .Add. byte_of_nat stack_sz
  ; RegisterSPL ← A
  ; A ← RegisterSPH
  ; A ← A .Addc. zero_byte
  ; RegisterSPH ← A
  ].

definition commutative : Op2 → bool ≝
λop.match op with
[ Add ⇒ true
| Addc ⇒ true
| Or ⇒ true
| Xor ⇒ true
| And ⇒ true
| _ ⇒ false
].

definition uses_carry : Op2 → bool ≝
λop.match op with
[ Addc ⇒ true
| Sub ⇒ true
| _ ⇒ false
].

definition sets_carry : Op2 → bool ≝
λop.match op with
[ Add ⇒ true
| Addc ⇒ true
| Sub ⇒ true
| _ ⇒ false
].

definition translate_op2 :
  ∀globals.nat → bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,localss,carry_lives_after,op,dst,arg1,arg2.
  (* this won't preserve the carry bit if op does not set it: left to next function *)
  (* if op uses carry bit (⇒ it sets it too) it must be preserved before the op *)
  (preserve_carry_bit ?
    (uses_carry op ∧ (arg_is_spilled arg1 ∨ arg_is_spilled arg2))
    (move ? localss false RegisterB arg2 @
     move ? localss false RegisterA arg1) @
    [ A ← A .op. RegisterB ] @
    (* it op sets the carry bit and it is needed afterwards it must be preserved here *)
    move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA).

definition translate_op2_smart :
  ∀globals.nat → bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,localss,carry_lives_after,op,dst,arg1,arg2.
  (* if op does not set carry bit (⇒ it does not use it either) then it must be
    preserved *)
  preserve_carry_bit ?
    (¬sets_carry op ∧ carry_lives_after ∧
      (arg_is_spilled arg1 ∨ arg_is_spilled arg2 ∨ is_spilled dst))
    (match arg2 with
    [ arg_decision_colour arg2r ⇒
      move ? localss (uses_carry op) RegisterA arg1 @
      [ A ← A .op. arg2r ] @
      move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA
    | arg_decision_imm arg2i ⇒
      move ? localss (uses_carry op) RegisterA arg1 @
      [ A ← A .op. arg2i ] @
      move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA
    | _ ⇒
      if commutative op then
        match arg1 with
        [ arg_decision_colour arg1r ⇒
          move ? localss (uses_carry op) RegisterA arg2 @
          [ A ← A .op. arg1r ] @
          move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA
        | arg_decision_imm arg1i ⇒
          move ? localss (uses_carry op) RegisterA arg2 @
          [ A ← A .op. arg1i ] @
          move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA
        | _ ⇒
          translate_op2 ? localss carry_lives_after op dst arg1 arg2
        ]
      else
        translate_op2 ? localss carry_lives_after op dst arg1 arg2
    ]).

definition dec_to_arg_dec : decision → arg_decision ≝
  λd.match d with
  [ decision_colour r ⇒ arg_decision_colour r
  | decision_spill n ⇒ arg_decision_spill n
  ].

coercion dec_arg_dec : ∀d:decision.arg_decision ≝ dec_to_arg_dec on _d : decision to arg_decision.

definition translate_op1 :
  ∀globals.nat → bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝
  λglobals,localss,carry_lives_after,op,dst,arg.
  let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in
  preserve_carry_bit ? preserve_carry
    (move ? localss false RegisterA arg @
     OP1 … op it it ::
     move ? localss false dst RegisterA).

definition translate_opaccs :
  ∀globals.nat → bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,localss,carry_lives_after,op,dst1,dst2,arg1,arg2.
  (* OPACCS always has dead carry bit and sets it to zero *)
  move ? localss false RegisterB arg2 @
  move ? localss false RegisterA arg1 @
  OPACCS … op it it it it ::
  move ? localss false dst1 RegisterA @
  move ? localss false dst2 RegisterB @
  if carry_lives_after ∧ (is_spilled dst1 ∨ is_spilled dst2) then
    [CLEAR_CARRY ??]
  else [ ].

(* does not preserve carry bit *)
definition move_to_dp :
  ∀globals.nat → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,localss,arg1,arg2.
  if ¬arg_is_spilled arg1 then
    move ? localss false RegisterDPH arg2 @
    (* does not change dph because arg1 is not spilled *)
    move ? localss false RegisterDPL arg1
  else if ¬arg_is_spilled arg2 then
    move ? localss false RegisterDPL arg1 @
    (* does not change dpl because arg2 is not spilled *)
    move ? localss false RegisterDPH arg2
  else
    (* using B as temporary, as moving spilled registers tampers with DPTR *)
    move ? localss false RegisterB arg1 @
    move ? localss false RegisterDPH arg2 @
    move ? localss false RegisterDPL RegisterB.

definition translate_store :  
  ∀globals.nat → bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,localss,carry_lives_after,addr1,addr2,src.
  (* requires src != RegisterA and RegisterB *)
  preserve_carry_bit ? (carry_lives_after ∧
    (arg_is_spilled addr1 ∨ arg_is_spilled addr1 ∨ arg_is_spilled src))
    (let move_to_dptr ≝ move_to_dp ? localss addr1 addr2 in
     (if arg_is_spilled src then
        move ? localss false RegisterST0 src @
        move_to_dptr @
        [ A ← RegisterST0]
      else move_to_dptr) @
     [STORE … it it A]). 

definition translate_load :  
  ∀globals.nat → bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
  λglobals,localss,carry_lives_after,dst,addr1,addr2.
  preserve_carry_bit ? (carry_lives_after ∧
    (is_spilled dst ∨ arg_is_spilled addr1 ∨ arg_is_spilled addr1))
    (move_to_dp ? localss addr1 addr2 @
     [ LOAD … A it it ] @
     move ? localss false dst RegisterA).

definition translate_address :
  ∀globals.nat → bool → ∀i.i ∈ globals → Word → decision → decision →
  list (joint_seq LTL globals) ≝
  λglobals,localss,carry_lives_after,id,prf,off,addr1,addr2.
  preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2))
    (ADDRESS LTL ? id prf off it it ::
     move ? localss false addr1 RegisterDPL @
     move ? localss false addr2 RegisterDPH).

definition translate_step:
  ∀globals,fn.nat → ∀after : valuation register_lattice.
  coloured_graph (livebefore globals fn after) →
  ℕ → label → joint_step ERTL globals → bind_step_block LTL globals ≝
  λglobals,fn,localss,after,grph,stack_sz,lbl,s.
  bret … (
  let lookup ≝ λr.colouring … grph (inl … r) in
  let lookup_arg ≝ λa.match a with
    [ Reg r ⇒ lookup r
    | Imm b ⇒ arg_decision_imm b
    ] in
  let carry_lives_after ≝ hlives RegisterCarry (after lbl) in
  let move ≝ move globals localss carry_lives_after in
  if eliminable_step … (after lbl) s then ([ ] : step_block LTL globals) else
  match s with
  [ step_seq s' ⇒
    match s' return λ_.step_block LTL globals with
    [ COMMENT c ⇒ [COMMENT … c]
    | POP r ⇒
      POP … A ::
      move (lookup r) RegisterA
    | PUSH a ⇒
      move RegisterA (lookup_arg a) @
      [ PUSH … A ]
    | STORE addr1 addr2 srcr ⇒
      translate_store ? localss carry_lives_after
        (lookup_arg addr1)
        (lookup_arg addr2)
        (lookup_arg srcr)
    | LOAD dstr addr1 addr2 ⇒
      translate_load ? localss carry_lives_after
        (lookup dstr)
        (lookup_arg addr1)
        (lookup_arg addr2)
    | CLEAR_CARRY ⇒ [CLEAR_CARRY ??]
    | SET_CARRY ⇒ [SET_CARRY ??]
    | OP2 op dst arg1 arg2 ⇒
      translate_op2_smart ? localss carry_lives_after op
        (lookup dst)
        (lookup_arg arg1)
        (lookup_arg arg2)
    | OP1 op dst arg ⇒
      translate_op1 ? localss carry_lives_after op
        (lookup dst)
        (lookup arg)
    | MOVE pair_regs ⇒
      let lookup_move_dst ≝ λx.match x return λ_.decision with
        [ PSD r ⇒ lookup r
        | HDW r ⇒ r
        ] in
      let dst ≝ lookup_move_dst (\fst pair_regs) in
      let src ≝
        match \snd pair_regs return λ_.arg_decision with
        [ Reg r ⇒ lookup_move_dst r
        | Imm b ⇒ arg_decision_imm b
        ] in
      move dst src
    | ADDRESS lbl prf off dpl dph ⇒
      translate_address ? localss carry_lives_after
        lbl prf off (lookup dpl) (lookup dph)
    | OPACCS op dst1 dst2 arg1 arg2 ⇒
      translate_opaccs ? localss carry_lives_after op
        (lookup dst1) (lookup dst2)
        (lookup_arg arg1) (lookup_arg arg2)
    | extension_seq ext ⇒
      match ext with
      [ ertl_new_frame ⇒ newframe ? stack_sz
      | ertl_del_frame ⇒ delframe ? stack_sz
      | ertl_frame_size r ⇒
        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
      ]
    ]
  | COST_LABEL cost_lbl ⇒ 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉
  | COND r ltrue ⇒
    〈add_dummy_variance … (move RegisterA (lookup r)),λ_.COND … it ltrue, [ ]〉
  | CALL f n_args _ ⇒
      match f with
      [ inl f ⇒
        〈[ ],λ_.CALL LTL ? (inl … f) n_args it, [ ]〉
      | inr dp ⇒
        let 〈dpl, dph〉 ≝ dp in
        〈add_dummy_variance … (move_to_dp ? localss (lookup_arg dpl) (lookup_arg dph)) @
         [λl.(LOW_ADDRESS l : joint_seq ??);
          λ_.PUSH LTL ? it;
          λl.HIGH_ADDRESS l;
          λ_.PUSH LTL ? it ;
          (* necessary as ptr CALL will be JMP A+DPTR *)
          λ_.A ← zero_byte ],
         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
      ]
  ]).

definition translate_fin_step:
  ∀globals.label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
  λglobals,lbl,s.
  bret … (〈[ ],
  match s with
  [ RETURN ⇒ RETURN ?
  | GOTO l ⇒ GOTO ? l
  | TAILCALL abs _ _ ⇒ Ⓧabs
  ]〉).

definition translate_data :
 fixpoint_computer → coloured_graph_computer →
 ∀globals.
  joint_closed_internal_function ERTL globals →
  bind_new register (b_graph_translate_data ERTL LTL globals) ≝
λthe_fixpoint,build,globals,int_fun.
(* colour registers *)
let after ≝ analyse_liveness the_fixpoint globals int_fun in
let coloured_graph ≝ build … int_fun after in
(* compute new stack size *)
let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
bret … 
  (mk_b_graph_translate_data ERTL LTL globals
    (* init_ret ≝ *) it
    (* init_params ≝ *) it
    (* init_stack_size ≝ *) stack_sz
    (* added_prologue ≝ *) [ ]
    (* new_regs ≝ *) [ ]
    (* f_step ≝ *) (translate_step ? int_fun (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz)
    (* f_fin ≝ *) (translate_fin_step globals)
    ????).
@hide_prf
[
| #l #c % ]
cases daemon (* TODO *)
qed.

(* Paolo: does it really have sense to do here the first stack address computation,
   when it is an info easily available from any program in the back end?
   Also, is it really 2^16 - |globals|, or should there also be a -1? *)
definition ertl_to_ltl:
 fixpoint_computer → coloured_graph_computer → ertl_program →
  ltl_program × stack_cost_model × nat ≝
  λthe_fixpoint,build,pr.
   let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in
   〈ltlprog, stack_cost … ltlprog, 2^16 - globals_stacksize … ltlprog〉.
%
qed.