End of Asmblock translation

1 files changed, 36 insertions, 38 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index 8e095553..fc356d52 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -298,12 +298,23 @@ Definition make_epilogue (f: Machblock.function) : bcode :=
 
 (** Add immediate *)
 
+Definition addimm_aux (insn: Z -> arith_pp)
+                        (rd r1: iregsp) (n: Z) (k: bcode) :=
+  let nlo := Zzero_ext 12 n in
+  let nhi := n - nlo in
+  if Z.eqb nhi 0 then
+    insn nlo rd r1 ::bi k
+  else if Z.eqb nlo 0 then
+    insn nhi rd r1 ::bi k
+  else
+    insn nhi rd r1 ::bi insn nlo rd rd ::bi k.
+
 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
+    addimm_aux (Paddimm W) rd r1 (Int.unsigned n) k
   else if Int.eq m (Int.zero_ext 24 m) then
-    Psubimm W (Int.unsigned m) rd r1 ::bi k
+    addimm_aux (Psubimm W) rd r1 (Int.unsigned m) k
   else if Int.lt n Int.zero then
     loadimm32 X16 m (Psub W SOnone rd r1 X16 ::bi k)
   else
@@ -312,9 +323,9 @@ Definition addimm32 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
 Definition addimm64 (rd r1: iregsp) (n: int64) (k: bcode) : bcode :=
   let m := Int64.neg n in
   if Int64.eq n (Int64.zero_ext 24 n) then
-    Paddimm X (Int64.unsigned n) rd r1 ::bi k
+    addimm_aux (Paddimm X) rd r1 (Int64.unsigned n) k
   else if Int64.eq m (Int64.zero_ext 24 m) then
-    Psubimm X (Int64.unsigned m) rd r1 ::bi k
+    addimm_aux (Psubimm X) rd r1 (Int64.unsigned m) k
   else if Int64.lt n Int64.zero then
     loadimm64 X16 m (Psubext (EOuxtx Int.zero) rd r1 X16 ::bi k)
   else
@@ -1120,42 +1131,26 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst)
       loadind XSP ofs ty dst k
   | MBsetstack src ofs ty =>
       storeind src XSP ofs ty k
+  | MBgetparam ofs ty dst =>
+      do c <- loadind X29 ofs ty dst k;
+      OK (if ep then c else loadptr_bc XSP f.(fn_link_ofs) X29 c)
   | MBop op args res =>
       transl_op op args res k
   | MBload _ chunk addr args dst =>
       transl_load chunk addr args dst k
-  (*| MBstore chunk addr args src =>*)
-      (*transl_store chunk addr args src k*)
-  | _ => Error(msg "Not implemented yet")
-  (*| 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*)
+  | 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
-  | MBgetstack ofs ty dst => before && negb (mreg_eq dst R29)
-  (*| Msetstack src ofs ty => before*)
-  (*| Mgetparam ofs ty dst => negb (mreg_eq dst R29)*)
+  (*| MBgetstack ofs ty dst => before && negb (mreg_eq dst R29)*)
+  | MBsetstack src ofs ty => before
+  | MBgetparam ofs ty dst => negb (mreg_eq dst R29)
   | MBop op args res => before && negb (mreg_eq res R29)
-  | MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst R29)
+  (*| MBload trapping_mode chunk addr args dst => before && negb (mreg_eq dst R29)*)
   | _ => false
   end.
 
@@ -1204,28 +1199,31 @@ Obligation 1.
   rewrite <- Heq_anonymous. constructor.
 Qed.
 
-Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep: bool) : res (bcode*control) :=
+Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) : res (bcode*control) :=
   match ctl with
-  | MBcall sig (inl r) => do r1 <- ireg_of r; OK (nil, PCtlFlow (Pblr r1 sig))
+  | MBcall sig (inl r) => do r1 <- ireg_of r;
+      OK (nil, PCtlFlow (Pblr r1 sig))
   | MBcall sig (inr symb) => OK (nil, PCtlFlow (Pbl symb sig))
-  | 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")
+  | MBtailcall sig (inr symb) => OK(make_epilogue f, PCtlFlow (Pbs symb sig))
+  | MBtailcall sig (inl r) => do r1 <- ireg_of r;
+      OK (make_epilogue f, PCtlFlow (Pbr r1 sig))
+  | MBbuiltin ef args res => OK (nil, Pbuiltin ef (List.map (map_builtin_arg dreg_of) args) (map_builtin_res dreg_of res))
   | MBgoto lbl => OK (nil, PCtlFlow (Pb lbl))
   | MBcond cond args lbl => transl_cond_branch cond args lbl nil
   | MBreturn => OK (make_epilogue f, PCtlFlow (Pret RA))
-  | MBjumptable arg tbl => Error (msg "NYI MBjumptable arg tbl")
+  | MBjumptable arg tbl => do r <- ireg_of arg;
+      OK (nil, PCtlFlow (Pbtbl r tbl))
   end.
 
-Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) (ep: bool) : res (bcode*option control) :=
+Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) : 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; OK (b, Some c)
   | None => OK (nil, None)
   end.
 
 Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) (k:bblocks): res (list bblock) :=
   let stub := false in (* TODO: FIXME *) 
-  do (bdy, ex) <- transl_exit f fb.(Machblock.exit) stub;
+  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) 
   .