path: root/aarch64/Asmblockgen.v

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

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

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

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

Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: larith) : larith :=
  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: larith) : larith :=
  if is_logical_imm32 n
  then IArithRR0 (Porrimm W (Int.unsigned n))
  else loadimm W (Int.unsigned n) k.

Definition loadimm64 (rd: ireg) (n: int64) (k: code) : code :=
  if is_logical_imm64 n
  then Porrimm X rd XZR (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: list basic) :=
  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: list basic) :=
  match i with
  | Mop 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.

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' (fp_is_parent it1p i1);
      transl_instr_basic f i1 it1p k
  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 <- 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.