This commit fix the issue #226

- adding two functions to manage special bblock case
- adding movz size specifications

1 files changed, 57 insertions, 50 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index 0a21485c..268cd7fc 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -139,6 +139,8 @@ Definition is_arith_imm64 (x: int64) : bool :=
   Int64.eq x (Int64.zero_ext 12 x)
   || Int64.eq x (Int64.shl (Int64.zero_ext 12 (Int64.shru x (Int64.repr 12))) (Int64.repr 12)).
 
+Definition bcode := list basic.
+
 Program Definition single_basic (bi: basic): bblock :=
   {| header := nil; body:= bi::nil; exit := None |}.
 
@@ -155,12 +157,6 @@ Program Definition insert_basic (bi: basic) (k:bblocks): bblocks :=
 
 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).
-
 (* TODO: Coercions to move in Asmblock ? *)
 Coercion PArithP: arith_p >-> Funclass.
 Coercion PArithPP: arith_pp >-> Funclass.
@@ -173,11 +169,45 @@ Coercion PArithComparisonPP: arith_comparison_pp >-> Funclass.
 Coercion PArithComparisonR0R: arith_comparison_r0r >-> Funclass.
 Coercion PArith: ar_instruction >-> basic.
 
-Definition bcode := list basic.
-
-Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity).
 (* NB: this notation helps the Coq typechecker to infer coercion [PArith] in [bcode] expressions *)
 (** Alignment check for symbols *)
+Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity).
+
+(* The pop_bc and push_bc functions are used to adapt the output of some definitions
+   in bblocks format and avoid some redefinitions. *)
+
+(* pop_bc takes the body of the first bblock in the list if it does not have a header. *)
+Definition pop_bc (k: bblocks): bcode :=
+  match k with
+  | bb :: k' => match bb.(header) with
+                | nil => (body bb)
+                | _ => nil
+                end
+  | _ => nil
+  end.
+
+(* push_bc tries to overwrite code in the first bblock if it does not have a header,
+   otherwise, a new bblock is created and appended to the list. *)
+Program Definition push_bc (bc: bcode) (k:bblocks): bblocks :=
+  match bc with
+  | bi :: bc' => match k with
+                 | bb :: k' => match bb.(header) with
+                               | nil => {| header := nil; body := bc; exit := exit bb |} :: k'
+                               | _ => {| header := nil; body := bc; exit := None |} :: k
+                               end
+                 | _ => {| header := nil; body := bc; exit := None |} :: nil
+                 end
+  | nil => k
+  end.
+Next Obligation.
+  simpl; auto.
+Qed.
+Next Obligation.
+  simpl; auto.
+Qed.
+Next Obligation.
+  simpl; auto.
+Qed.
 
 Parameter symbol_is_aligned : ident -> Z -> bool.
 (** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *)
@@ -233,17 +263,20 @@ Definition loadimm64 (rd: ireg) (n: int64) (k: bcode) : bcode :=
   then Porrimm X (Int64.unsigned n) rd XZR ::bi k
   else loadimm X rd (Int64.unsigned n) k.
 
-(* 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 offset_representable (sz: Z) (ofs: int64) : bool :=
+  let isz := Int64.repr sz in
+  (** either unscaled 9-bit signed *)
+  Int64.eq ofs (Int64.sign_ext 9 ofs) ||
+  (** or scaled 12-bit unsigned *)
+  (Int64.eq (Int64.modu ofs isz) Int64.zero
+   && Int64.ltu ofs (Int64.shl isz (Int64.repr 12))).
 
 Definition indexed_memory_access_bc (insn: addressing -> basic)
                                  (sz: Z) (base: iregsp) (ofs: ptrofs) (k: bcode) : bcode :=
   let ofs := Ptrofs.to_int64 ofs in
-  insn (ADimm base ofs) :: k.
+  if offset_representable sz ofs
+  then insn (ADimm base ofs) :: k
+  else loadimm64 X16 ofs (insn (ADreg base X16) :: k).
 
 Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) :=
   match ty, preg_of dst with
@@ -269,32 +302,17 @@ Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: bcode
   | _, _           => Error (msg "Asmgen.storeind")
   end.
 
-Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bblocks): bblocks :=
-  indexed_memory_access (PLoad Pldrx dst) 8 base ofs k.
-
 Definition loadptr_bc (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bcode): bcode :=
   indexed_memory_access_bc (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.
-
-(*Definition storeptr_bc (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bcode): bcode :=*)
-  (*indexed_memory_access_bc (PStore Pstrx src) 8 base ofs k.*)
+Definition storeptr_bc (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bcode): bcode :=
+  indexed_memory_access_bc (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).*)
-
 Definition make_epilogue (f: Machblock.function) : bcode :=
   loadptr_bc XSP f.(fn_retaddr_ofs) RA
-  (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs)::nil). 
+  (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs)::nil).
 
 (** Add immediate *)
 
@@ -1022,14 +1040,6 @@ Definition transl_op
   end.
 
 (** Translation of addressing modes *)
-
-Definition offset_representable (sz: Z) (ofs: int64) : bool :=
-  let isz := Int64.repr sz in
-  (** either unscaled 9-bit signed *)
-  Int64.eq ofs (Int64.sign_ext 9 ofs) ||
-  (** or scaled 12-bit unsigned *)
-  (Int64.eq (Int64.modu ofs isz) Int64.zero
-   && Int64.ltu ofs (Int64.shl isz (Int64.repr 12))).
  
 Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg)
                              (insn: Asm.addressing -> basic) (k: bcode) : res bcode :=
@@ -1222,7 +1232,7 @@ Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) :
   end.
 
 Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) (k:bblocks): res (list bblock) :=
-  let stub := false in (* TODO: FIXME *) 
+  let stub := false in
   do (bdy, ex) <- transl_exit f fb.(Machblock.exit);
   do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy;
   OK (cons_bblocks fb.(Machblock.header) bdy' ex k) 
@@ -1232,18 +1242,15 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool):
   match lmb with
   | nil => OK nil
   | mb :: lmb => 
-      do lb <- transl_blocks f lmb false; (* TODO: check [false] here *)
-      transl_block f mb (if Machblock.header mb then ep else false) lb  (* TODO: check this *)
+      do lb <- transl_blocks f lmb false;
+      transl_block f mb (if Machblock.header mb then ep else false) lb
   end.
-  (* OK (make_epilogue f ((Pret X0)::c nil)). (* STUB: TODO CHANGE ME ! *)*)
+  (* OK (make_epilogue f ((Pret X0)::c nil))*)
 
 (* Currently, we assume to be after the PseudoAsmblockproof.transf_program pass... *)
 Program Definition make_prologue (f:  Machblock.function) (k:bblocks) :=
-  (*({| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::*)
-         (*storeptr_bc RA XSP f.(fn_retaddr_ofs) nil;*)
-      (*exit := None |} :: k).*)
    Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b
-   storeptr RA XSP f.(fn_retaddr_ofs) k.
+   push_bc (storeptr_bc RA XSP f.(fn_retaddr_ofs) (pop_bc k)) k.
 
 Definition transl_function (f: Machblock.function) : res Asmblock.function :=
   do lb <- transl_blocks f f.(Machblock.fn_code) true;