(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
(*           Léo Gourdin        UGA, VERIMAG                   *)
(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
(*           David Monniaux     CNRS, VERIMAG                  *)
(*           Cyril Six          Kalray                         *)
(*                                                             *)
(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)

(** * Translation from Machblock to AArch64 assembly block language (Asmblock) 
    Inspired from the Mach->Asm pass of original Leroy's backend, but adapted to the block structure like the KVX backend. *)

Require Import Recdef Coqlib Zwf Zbits.
Require Import Errors AST Integers Floats Op.
Require Import Locations Machblock Asm Asmblock.

Local Open Scope string_scope.
Local Open Scope list_scope.
Local Open Scope error_monad_scope.

(** Extracting integer or float registers. *)

Definition ireg_of (r: mreg) : res ireg :=
  match preg_of r with
  |  IR' irs => match irs with
                | RR1 mr => OK mr
                | _ => Error(msg "Asmgenblock.ireg_of")
                end
  | _ => Error(msg "Asmgenblock.iregsp_of")
  end.

Definition freg_of (r: mreg) : res freg :=
  match preg_of r with FR' mr => OK mr | _ => Error(msg "Asmgenblock.freg_of") end.

(** Recognition of immediate arguments for logical integer operations.*)

(** Valid immediate arguments are repetitions of a bit pattern [B]
  of length [e] = 2, 4, 8, 16, 32 or 64.
  The bit pattern [B] must be of the form [0*1*0*] or [1*0*1*]
  but must not be all zeros or all ones. *)

(** The following automaton recognizes [0*1*0*|1*0*1*].
<<
               0          1          0
              / \        / \        / \
              \ /        \ /        \ /
        -0--> [B] --1--> [D] --0--> [F]
       /
     [A]
       \
        -1--> [C] --0--> [E] --1--> [G]
              / \        / \        / \
              \ /        \ /        \ /
               1          0          1
>>
*)

Module Automaton.

Inductive state : Type := SA | SB | SC | SD | SE | SF | SG | Sbad.

Definition start := SA.

Definition next (s: state) (b: bool) :=
  match s, b with
    | SA,false => SB      | SA,true => SC
    | SB,false => SB      | SB,true => SD
    | SC,false => SE      | SC,true => SC
    | SD,false => SF      | SD,true => SD
    | SE,false => SE      | SE,true => SG
    | SF,false => SF      | SF,true => Sbad
    | SG,false => Sbad    | SG,true => SG
    | Sbad,_ => Sbad
  end.

Definition accepting (s: state) :=
  match s with
  | SA | SB | SC | SD | SE | SF | SG => true
  | Sbad => false
  end.

Fixpoint run (len: nat) (s: state) (x: Z) : bool :=
  match len with
  | Datatypes.O => accepting s
  | Datatypes.S len => run len (next s (Z.odd x)) (Z.div2 x)
  end.

End Automaton.

(** The following function determines the candidate length [e],
    ensuring that [x] is a repetition [BB...B] 
    of a bit pattern [B] of length [e]. *)

Definition logical_imm_length (x: Z) (sixtyfour: bool) : nat :=
  (** [test n] checks that the low [2n] bits of [x] are of the
      form [BB], that is, two occurrences of the same [n] bits *)
  let test (n: Z) : bool :=
    Z.eqb (Zzero_ext n x) (Zzero_ext n (Z.shiftr x n)) in
  (** If [test n] fails, we know that the candidate length [e] is
      at least [2n].  Hence we test with decreasing values of [n]:
      32, 16, 8, 4, 2. *)
  if sixtyfour && negb (test 32) then 64%nat
  else if negb (test 16) then 32%nat
  else if negb (test 8) then 16%nat
  else if negb (test 4) then 8%nat
  else if negb (test 2) then 4%nat
  else 2%nat.

(** A valid logical immediate is 
- neither [0] nor [-1];
- composed of a repetition [BBBBB] of a bit-pattern [B] of length [e]
- the low [e] bits of the number, that is, [B], match [0*1*0*] or [1*0*1*].
*)

Definition is_logical_imm32 (x: int) : bool :=
  negb (Int.eq x Int.zero) && negb (Int.eq x Int.mone) &&
  Automaton.run (logical_imm_length (Int.unsigned x) false)
                Automaton.start (Int.unsigned x).

Definition is_logical_imm64 (x: int64) : bool :=
  negb (Int64.eq x Int64.zero) && negb (Int64.eq x Int64.mone) &&
  Automaton.run (logical_imm_length (Int64.unsigned x) true)
                Automaton.start (Int64.unsigned x).

Program Definition single_basic (bi: basic): bblock :=
  {| header := nil; body:= bi::nil; exit := None |}.

(* insert [bi] at the head of [k] *)
Program Definition insert_basic (bi: basic) (k:bblocks): bblocks :=
  match k with
  | bb::k' =>
    match bb.(header) with
    | nil => {| header := nil; body := bi :: (body bb); exit := exit bb |}::k'
    | _ => (single_basic bi)::k
    end
  | _ => (single_basic bi)::k
  end.

Notation "bi ::b k" := (insert_basic bi k) (at level 49, right associativity).

(* insert [ctl] at the head of [k] *)
Program Definition insert_ctl (ctl: control) (k:bblocks): bblocks :=
  {| header := nil; body := nil; exit := Some ctl |}::k.

Notation "ctl ::c k" := (insert_ctl ctl k) (at level 49, right associativity).


(** Alignment check for symbols *)

Parameter symbol_is_aligned : ident -> Z -> bool.
(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *)

(***************************************************************************************)
(* STUB inspired from kvx/Asmblockgen.v and the reference aarch64/Asmgen.v (see below) *)

Definition indexed_memory_access (insn: addressing -> basic)
                                 (sz: Z) (base: iregsp) (ofs: ptrofs) (k: bblocks) : bblocks :=
  let ofs := Ptrofs.to_int64 ofs in
  insn (ADimm base ofs) ::b k. (* STUB: change me ! See Asmgen below *)


Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bblocks): bblocks :=
  indexed_memory_access (PLoad Pldrx dst) 8 base ofs k.

Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bblocks): bblocks :=
  indexed_memory_access (PStore Pstrx src) 8 base ofs k.

(** Function epilogue *)

Definition make_epilogue (f: Machblock.function) (k: bblocks) : bblocks :=
  (* FIXME
     Cannot be used because memcpy destroys X30;
     issue being discussed with X. Leroy *)
  (* if is_leaf_function f
  then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k
  else*) loadptr XSP f.(fn_retaddr_ofs) RA
         (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::b k).

(** Decompose integer literals into 16-bit fragments *)

Fixpoint decompose_int (N: nat) (n p: Z) {struct N} : list (Z * Z) :=
  match N with
  | Datatypes.O => nil
  | Datatypes.S N =>
    let frag := Zzero_ext 16 (Z.shiftr n p) in
    if Z.eqb frag 0 then
      decompose_int N n (p + 16)
    else
      (frag, p) :: decompose_int N (Z.ldiff n (Z.shiftl 65535 p)) (p + 16)
  end.

Definition negate_decomposition (l: list (Z * Z)) :=
  List.map (fun np => (Z.lxor (fst np) 65535, snd np)) l.

(* XXX Que faire des rd ici ? inutiles ? *)
(* XXX Faudra-t-il remplacer arith_pp par un type abstrait ? *)

(* XXX Move this in Asmblock.v ? *)

(*Inductive iar: Type :=*)
  (*| IArithP (i: arith_p)*)
  (*| IArithPP (i: arith_pp)*)
  (*| IArithRR0 (i: arith_rr0).*)

(*Coercion IArithP: arith_p >-> iar.*)
(*Coercion IArithPP: arith_pp >-> iar.*)
(*Definition larith := list iar.*)

(*Fixpoint extract_larith_p (l: larith) :=*)
  (*match l with*)
  (*| nil => nil*)
  (*| IArithP i :: l' => i :: extract_larith_p l'*)
  (*| _ => nil*)
  (*end.*)

(*Fixpoint extract_larith_pp (l: larith) :=*)
  (*match l with*)
  (*| nil => nil*)
  (*| IArithPP i :: l' => i :: extract_larith_pp l'*)
  (*| _ => nil*)
  (*end.*)

(*Fixpoint larith_p_to_larith (l: list arith_p): larith :=*)
  (*match l with*)
  (*| nil => nil*)
  (*| ar :: l' => IArithP ar :: (larith_p_to_larith l')*)
  (*end.*)

(*Fixpoint larith_pp_to_larith (l: list arith_pp): larith :=*)
  (*match l with*)
  (*| nil => nil*)
  (*| ar :: l' => IArithPP ar :: (larith_pp_to_larith l')*)
  (*end.*)

(*Coercion PArithP: arith_p >-> Funclass.*)
(*Coercion PArithPP: arith_pp >-> Funclass.*)
(*Coercion PArithRR0: arith_rr0 >-> Funclass.*)

(*Definition bcode := list basic.*)
(*Definition larith := list ar_instruction.*)
(*Definition larith_p := list arith_p.*)
(*Definition larith_pp := list arith_pp.*)
(*Definition larith_rr0 := list arith_rr0.*)

(*Coercion PBasic:    basic >-> instruction.*)
(*Coercion PControl:  control >-> instruction.*)
(*Coercion PArith:    ar_instruction >-> basic.*)

Inductive basic : Type :=
  | I_BI (i: basic)
  | I_Arith (i: ar_instruction)
  | I_ArithP (i : arith_p)
  | I_ArithPP (i : arith_pp)
  | I_ArithRR0 (i : arith_rr0).

Inductive instruction : Type :=
  | PBasic    (i: basic)
  | PControl  (i: control)
.

Definition code := list instruction.
Definition bcode := list basic.

Fixpoint extract_basic (c: code) :=
  match c with
  | nil => nil
  | PBasic i :: c => i :: (extract_basic c)
  | PControl i :: c => nil
  end.

Fixpoint extract_ctl (c: code) :=
  match c with
  | nil => None
  | PBasic i :: c => extract_ctl c
  | PControl i :: nil => Some i
  | PControl i :: _ => None (* if the first found control instruction isn't the last *)
  end.

(*Definition code := list instruction.*)

(*Coercion PArith: ar_instruction >-> basic.*)
(*Coercion I_bi: bcode >-> code.*)
(*Coercion I_larith: larith >-> code.*)
(*Coercion I_larith_p: larith_p >-> code.*)
(*Coercion I_larith_pp: larith_pp >-> code.*)
(*Coercion I_larith_rr0: larith_rr0 >-> code.*)

(*Fixpoint extract_larith (c: code) :=*)
  (*match c with*)
  (*| nil => nil*)
  (*| PArith i :: l' => i :: extract_larith l'*)
  (*| _ => nil*)
  (*end.*)

(*Fixpoint extract_larith_p (c: code) :=*)
  (*match c with*)
  (*| I_larith_p i :: l => i :: extract_larith_p l*)
  (*| _ => nil*)
  (*end.*)

(*Fixpoint extract_arith_pp (ar: arith_pp) :=*)
  (*match ar with*)
  (*| Pmovk i  => i :: extract_larith_pp l*)
  (*| _ => nil*)
  (*end.*)

Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode :=
    List.fold_right (
      fun np k => (I_ArithPP (Pmovk sz (fst np) (snd np))) :: k) k l.

Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z))  (k: bcode) : bcode :=
  match l with
  | nil => I_ArithP (Pmovz sz 0 0) :: k
  | (n1, p1) :: l => I_ArithP (Pmovz sz n1 p1) :: loadimm_k sz rd l k
  end.

Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode :=
  match l with
  | nil => I_ArithP (Pmovn sz 0 0) :: k
  | (n1, p1) :: l => I_ArithP (Pmovn sz n1 p1) :: loadimm_k sz rd (negate_decomposition l) k
  end.

Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: bcode) : bcode :=
  let N := match sz with W => 2%nat | X => 4%nat end in
  let dz := decompose_int N n 0 in
  let dn := decompose_int N (Z.lnot n) 0 in
  if Nat.leb (List.length dz) (List.length dn)
  then loadimm_z sz rd dz k
  else loadimm_n sz rd dn k.

Definition loadimm32 (rd: ireg) (n: int) (k: bcode) : bcode :=
  if is_logical_imm32 n
  then I_ArithRR0 (Porrimm W (Int.unsigned n)) :: k
  else loadimm W rd (Int.unsigned n) k.

Definition loadimm64 (rd: ireg) (n: int64) (k: bcode) : bcode :=
  if is_logical_imm64 n
  then I_ArithRR0 (Porrimm X (Int64.unsigned n)) :: k
  else loadimm X rd (Int64.unsigned n) k.

(** Translation of the arithmetic operation [r <- op(args)].
  The corresponding instructions are prepended to [k]. *)

Definition transl_op
              (op: operation) (args: list mreg) (res: mreg) (k: bcode) :=
  match op, args with
  | Ointconst n, nil =>
      do rd <- ireg_of res;
      OK (loadimm32 rd n k)
  | _, _ => Error(msg "Not implemented yet")
  end.

(** Translation of a Machblock instruction. *)

Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
                              (ep: bool) (k: bcode) :=
  match i with
  | MBop op args res =>
      transl_op op args res k
  | _ => Error(msg "Not implemented yet")
  (*| MBgetstack ofs ty dst =>*)
      (*loadind SP ofs ty dst k*)
  (*| MBsetstack src ofs ty =>*)
      (*storeind src SP ofs ty k*)
  (*| MBgetparam ofs ty dst =>*)
      (*[> load via the frame pointer if it is valid <]*)
      (*do c <- loadind FP ofs ty dst k;*)
      (*OK (if ep then c*)
                (*else (loadind_ptr SP f.(fn_link_ofs) FP) ::i c)*)
  (*| MBop op args res =>*)
      (*transl_op op args res k*)
  (*| MBload trap chunk addr args dst =>*)
      (*transl_load trap chunk addr args dst k*)
  (*| MBstore chunk addr args src =>*)
      (*transl_store chunk addr args src k*)
  end.

(** Translation of a code sequence *)

(* TODO to remove ? *)
(*Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=*)
  (*match i with*)
  (*| MBgetstack ofs ty dst => before && negb (mreg_eq dst MFP)*)
  (*| MBsetstack src ofs ty => before*)
  (*| MBgetparam ofs ty dst => negb (mreg_eq dst MFP)*)
  (*| MBop op args res => before && negb (mreg_eq res MFP)*)
  (*| MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst MFP)*)
  (*| MBstore chunk addr args res => before*)
  (*end.*)

Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
  match i with
  (*| Msetstack src ofs ty => before*)
  (*| Mgetparam ofs ty dst => negb (mreg_eq dst R29)*)
  | MBop op args res => before && negb (mreg_eq res R29)
  | _ => false
  end.

(** This is an equivalent definition in continuation-passing style
  that runs in constant stack space. *)

Fixpoint transl_code_rec (f: Machblock.function) (il: list Machblock.basic_inst)
                         (it1p: bool) (k: bcode -> res bcode) :=
  match il with
  | nil => k nil
  | i1 :: il' =>
      transl_code_rec f il' (it1_is_parent it1p i1)
        (fun c1 => do c2 <- transl_instr_basic f i1 it1p c1; k c2)
  end.

Definition transl_code' (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) :=
  transl_code_rec f il it1p (fun c => OK c).


Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) :=
  match il with
  | nil => OK nil
  | i1 :: il' =>
      do k <- transl_basic_code f il' (it1_is_parent it1p i1);
      transl_instr_basic f i1 it1p k
  end.

(** Translation of a whole function.  Note that we must check
  that the generated code contains less than [2^64] instructions,
  otherwise the offset part of the [PC] code pointer could wrap
  around, leading to incorrect executions. *)

(* gen_bblocks can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *)
Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instruction) :=
  match (extract_ctl ctl) with
  | None => 
      match c with
      | nil => {| header := hd; body := Pnop::nil; exit := None |} :: nil
      | i::c => {| header := hd; body := ((i::c) ++ extract_basic ctl); exit := None |} :: nil
      end
  | Some (PExpand (Pbuiltin ef args res)) =>
      match c with
      | nil => {| header := hd; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil
      | _ => {| header := hd; body := c; exit := None |} 
              :: {| header := nil; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil
      end
  | Some ex => {| header := hd; body := (c ++ extract_basic ctl); exit := Some ex |} :: nil
  end
.

Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) :=
  do c <- transl_basic_code f fb.(Machblock.body) ep;
  do ctl <- nil; (*transl_instr_control f fb.(Machblock.exit);*)
  OK (gen_bblocks fb.(Machblock.header) c ctl)
.

Program Definition transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks :=
  match lmb with
  | nil => OK nil
  | mb :: lmb => 
      do lb <- transl_block f mb (if Machblock.header mb then ep else false);
      do lb' <- transl_blocks f lmb false;
      OK (lb @@ lb')
  end
  (* OK (make_epilogue f ((Pret X0)::c nil)). (* STUB: TODO CHANGE ME ! *)*)

(* Currently, we assume to be after the PseudoAsmblockproof.transf_program pass... *)
Program Definition make_prologue (f:  Machblock.function) (k:bblocks) :=
   Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b
   storeptr RA XSP f.(fn_retaddr_ofs) k.

Definition transl_function (f: Machblock.function) : res Asmblock.function :=
  do lb <- transl_blocks f f.(Machblock.fn_code) true;
  OK (mkfunction f.(Machblock.fn_sig)
        (make_prologue f lb)).

Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef :=
  transf_partial_fundef transl_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *)

Definition transf_program (p: Machblock.program) : res Asmblock.program :=
  transform_partial_program transf_fundef p.