Epilogue OK and loadimm

1 files changed, 96 insertions, 58 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index 2bab1927..aa6df96f 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -25,8 +25,6 @@ Local Open Scope string_scope.
 Local Open Scope list_scope.
 Local Open Scope error_monad_scope.
 
-Import PArithCoercions.
-
 (** Extracting integer or float registers. *)
 
 Definition ireg_of (r: mreg) : res ireg :=
@@ -153,37 +151,23 @@ Program Definition insert_ctl (ctl: control) (k:bblocks): bblocks :=
 
 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.
+Coercion PArithRR0: arith_rr0 >-> Funclass.
+Coercion PArithRR0R: arith_rr0r >-> 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 *)
 
 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 *)
 
@@ -201,18 +185,6 @@ Fixpoint decompose_int (N: nat) (n p: Z) {struct N} : list (Z * Z) :=
 Definition negate_decomposition (l: list (Z * Z)) :=
   List.map (fun np => (Z.lxor (fst np) 65535, snd np)) l.
 
-(* TODO: Coercions to move in Asmblock ? *)
-Coercion PArithP: arith_p >-> Funclass.
-Coercion PArithPP: arith_pp >-> Funclass.
-Coercion PArithRR0: arith_rr0 >-> 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 *)
-
-
 Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: bcode) : bcode :=
     List.fold_right (fun np k => Pmovk sz (fst np) (snd np) rd rd ::bi k) k l.
 
@@ -246,6 +218,68 @@ 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) *)
+
+(** 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 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 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.
+
+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.*)
+
+(** 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). 
+
+(** Add immediate *)
+
+Definition addimm32 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
+  let m := Int.neg n in
+  if Int.eq n (Int.zero_ext 24 n) then
+    Paddimm W (Int.unsigned n) rd r1 ::bi k
+  else if Int.eq m (Int.zero_ext 24 m) then
+    Psubimm W (Int.unsigned m) rd r1 ::bi k
+  else if Int.lt n Int.zero then
+    loadimm32 X16 m (Psub W SOnone rd r1 X16 ::bi k)
+  else
+    loadimm32 X16 n (Padd W SOnone rd r1 X16 ::bi k).
+
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
 
@@ -255,6 +289,9 @@ Definition transl_op
   | Ointconst n, nil =>
       do rd <- ireg_of res;
       OK (loadimm32 rd n k)
+  | Oaddimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (addimm32 rd rs n k)
   | _, _ => Error(msg "Not implemented yet")
   end.
 
@@ -304,22 +341,6 @@ Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool :=
   | _ => 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) (k: bcode):=
   match il with
   | nil => OK nil
@@ -365,12 +386,26 @@ Obligation 1.
   rewrite <- Heq_anonymous. constructor.
 Qed.
 
-Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep: bool) : res (bcode*control) :=
-  Error (msg ("not yet implemented")).
+Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep: bool) : res (bcode*option control) :=
+  match ctl with
+  | MBcall sig (inl r) => Error (msg "NYI MBcall sig (inl r)")
+  | MBcall sig (inr symb) => Error (msg "NYI MBcall sig (inr symb)")
+  | MBtailcall sig (inr symb) => Error (msg "NYI MBtailcall sig (inr symb)")
+  | MBtailcall sig (inl r) => Error (msg "NYI MBtailcall sig (inl r)")
+  | MBbuiltin ef args res => Error (msg "NYI MBbuiltin ef args res")
+  | MBgoto lbl => Error (msg "NYI MBgoto lbl")
+  | MBcond cond args lbl => Error (msg "NYI MBcond cond args lbl")
+  | MBreturn => OK (make_epilogue f, Some (PCtlFlow (Pret RA)))
+      (*match make_epilogue f (Pret RA ::c nil) with*)
+      (*| nil => OK(nil,None)*)
+      (*| b :: k  => OK(body b,exit b)*)
+      (*end*)
+  | MBjumptable arg tbl => Error (msg "NYI MBjumptable arg tbl")
+  end.
 
 Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) (ep: bool) : res (bcode*option control) :=
   match ext with
-    Some ctl => do (b,c) <- transl_control f ctl ep; OK (b, Some c)
+    Some ctl => do (b,c) <- transl_control f ctl ep; OK (b, c)
   | None => OK (nil, None)
   end.
 
@@ -378,7 +413,7 @@ Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool
   let stub := false in (* TODO: FIXME *) 
   do (bdy, ex) <- transl_exit f fb.(Machblock.exit) stub;
   do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy;
-  OK (cons_bblocks fb.(Machblock.header) bdy' ex k) 
+  OK (cons_bblocks fb.(Machblock.header) (bdy' ++ bdy) ex k) 
   .
 
 Fixpoint transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks :=
@@ -392,6 +427,9 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool):
 
 (* 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.