If, op, and some tests with a script

1 files changed, 701 insertions, 6 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index aa6df96f..c7170edc 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -129,6 +129,16 @@ Definition is_logical_imm64 (x: int64) : bool :=
   Automaton.run (logical_imm_length (Int64.unsigned x) true)
                 Automaton.start (Int64.unsigned x).
 
+(** Arithmetic immediates are 12-bit unsigned numbers, possibly shifted left 12 bits *)
+
+Definition is_arith_imm32 (x: int) : bool :=
+  Int.eq x (Int.zero_ext 12 x)
+  || Int.eq x (Int.shl (Int.zero_ext 12 (Int.shru x (Int.repr 12))) (Int.repr 12)).
+
+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)).
+
 Program Definition single_basic (bi: basic): bblock :=
   {| header := nil; body:= bi::nil; exit := None |}.
 
@@ -154,8 +164,13 @@ 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 PArithPPP: arith_ppp >-> Funclass.
 Coercion PArithRR0: arith_rr0 >-> Funclass.
 Coercion PArithRR0R: arith_rr0r >-> Funclass.
+Coercion PArithARRRR0: arith_arrrr0 >-> Funclass.
+Coercion PArithComparisonP: arith_comparison_p >-> Funclass.
+Coercion PArithComparisonPP: arith_comparison_pp >-> Funclass.
+Coercion PArithComparisonR0R: arith_comparison_r0r >-> Funclass.
 Coercion PArith: ar_instruction >-> basic.
 
 Definition bcode := list basic.
@@ -280,6 +295,299 @@ Definition addimm32 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
   else
     loadimm32 X16 n (Padd W SOnone rd r1 X16 ::bi k).
 
+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
+  else if Int64.eq m (Int64.zero_ext 24 m) then
+    Psubimm X (Int64.unsigned m) rd r1 ::bi k
+  else if Int64.lt n Int64.zero then
+    loadimm64 X16 m (Psubext (EOuxtx Int.zero) rd r1 X16 ::bi k)
+  else
+    loadimm64 X16 n (Paddext (EOuxtx Int.zero) rd r1 X16 ::bi k).
+
+(** Logical immediate *)
+
+Definition logicalimm32
+              (insn1: Z -> arith_rr0)
+              (insn2: shift_op -> arith_rr0r)
+              (rd r1: ireg) (n: int) (k: bcode) : bcode :=
+  if is_logical_imm32 n
+  then insn1 (Int.unsigned n) rd r1 ::bi k
+  else loadimm32 X16 n (insn2 SOnone rd r1 X16 ::bi k).
+
+Definition logicalimm64
+              (insn1: Z -> arith_rr0)
+              (insn2: shift_op -> arith_rr0r)
+              (rd r1: ireg) (n: int64) (k: bcode) : bcode :=
+  if is_logical_imm64 n
+  then insn1 (Int64.unsigned n) rd r1 ::bi k
+  else loadimm64 X16 n (insn2 SOnone rd r1 X16 ::bi k).
+
+(** Sign- or zero-extended arithmetic *)
+
+Definition transl_extension (ex: extension) (a: int) : extend_op :=
+  match ex with Xsgn32 => EOsxtw a | Xuns32 => EOuxtw a end.
+
+Definition move_extended_base
+              (rd: ireg) (r1: ireg) (ex: extension) (k: bcode) : bcode :=
+  match ex with
+  | Xsgn32 => Pcvtsw2x rd r1 ::bi k
+  | Xuns32 => Pcvtuw2x rd r1 ::bi k
+  end.
+
+Definition move_extended
+              (rd: ireg) (r1: ireg) (ex: extension) (a: int) (k: bcode) : bcode :=
+  if Int.eq a Int.zero then
+    move_extended_base rd r1 ex k
+  else
+    move_extended_base rd r1 ex (Padd X (SOlsl a) rd XZR rd ::bi k).
+
+Definition arith_extended 
+              (insnX: extend_op -> arith_ppp)
+              (insnS: shift_op -> arith_rr0r)
+              (rd r1 r2: ireg) (ex: extension) (a: int) (k: bcode) : bcode :=
+  if Int.ltu a (Int.repr 5) then
+    insnX (transl_extension ex a) rd r1 r2 ::bi k
+  else
+    move_extended_base X16 r2 ex (insnS (SOlsl a) rd r1 X16 ::bi k).
+
+(** Extended right shift *)
+
+Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
+  if Int.eq n Int.zero then
+    Pmov rd r1 ::bi k
+  else
+    Porr W (SOasr (Int.repr 31)) X16 XZR r1 ::bi
+    Padd W (SOlsr (Int.sub Int.iwordsize n)) X16 r1 X16 ::bi
+    Porr W (SOasr n) rd XZR X16 ::bi k.
+
+Definition shrx64 (rd r1: ireg) (n: int) (k: bcode) : bcode :=
+  if Int.eq n Int.zero then
+    Pmov rd r1 ::bi k
+  else
+    Porr X (SOasr (Int.repr 63)) X16 XZR r1 ::bi
+    Padd X (SOlsr (Int.sub Int64.iwordsize' n)) X16 r1 X16 ::bi
+    Porr X (SOasr n) rd XZR X16 ::bi k.
+
+(** Load the address [id + ofs] in [rd] *)
+
+Definition loadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (k: bcode) : bcode :=
+  if Archi.pic_code tt then
+    if Ptrofs.eq ofs Ptrofs.zero then
+      Ploadsymbol rd id ::bi k
+    else
+      Ploadsymbol rd id :: addimm64 rd rd (Ptrofs.to_int64 ofs) k
+  else
+    Padrp id ofs rd ::bi Paddadr id ofs rd rd ::bi k.
+
+(** Translate a shifted operand *)
+
+Definition transl_shift (s: Op.shift) (a: int): Asm.shift_op :=
+  match s with
+  | Slsl => SOlsl a
+  | Slsr => SOlsr a
+  | Sasr => SOasr a
+  | Sror => SOror a
+  end.
+
+(** Translation of a condition.  Prepends to [k] the instructions
+  that evaluate the condition and leave its boolean result in one of
+  the bits of the condition register.  The bit in question is
+  determined by the [crbit_for_cond] function. *)
+
+Definition transl_cond
+              (cond: condition) (args: list mreg) (k: bcode) :=
+  match cond, args with
+  | (Ccomp c | Ccompu c), a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pcmp W SOnone r1 r2 ::bi k)
+  | (Ccompshift c s a | Ccompushift c s a), a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pcmp W (transl_shift s a) r1 r2 ::bi k)
+  | (Ccompimm c n | Ccompuimm c n), a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if is_arith_imm32 n then
+            Pcmpimm W (Int.unsigned n) r1 ::bi k
+          else if is_arith_imm32 (Int.neg n) then
+            Pcmnimm W (Int.unsigned (Int.neg n)) r1 ::bi k
+          else
+            loadimm32 X16 n (Pcmp W SOnone r1 X16 ::bi k))
+  | (Cmaskzero n | Cmasknotzero n), a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if is_logical_imm32 n then
+            Ptstimm W (Int.unsigned n) r1 ::bi k
+          else
+            loadimm32 X16 n (Ptst W SOnone r1 X16 ::bi k))
+  | (Ccompl c | Ccomplu c), a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pcmp X SOnone r1 r2 ::bi k)
+  | (Ccomplshift c s a | Ccomplushift c s a), a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pcmp X (transl_shift s a) r1 r2 ::bi k)
+  | (Ccomplimm c n | Ccompluimm c n), a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if is_arith_imm64 n then
+            Pcmpimm X (Int64.unsigned n) r1 ::bi k
+          else if is_arith_imm64 (Int64.neg n) then
+            Pcmnimm X (Int64.unsigned (Int64.neg n)) r1 ::bi k
+          else
+            loadimm64 X16 n (Pcmp X SOnone r1 X16 ::bi k))
+  | (Cmasklzero n | Cmasklnotzero n), a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if is_logical_imm64 n then
+            Ptstimm X (Int64.unsigned n) r1 ::bi k
+          else
+            loadimm64 X16 n (Ptst X SOnone r1 X16 ::bi k))
+  | Ccompf cmp, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2;
+      OK (Pfcmp D r1 r2 ::bi k)
+  | Cnotcompf cmp, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2;
+      OK (Pfcmp D r1 r2 ::bi k)
+  | Ccompfzero cmp, a1 :: nil =>
+      do r1 <- freg_of a1;
+      OK (Pfcmp0 D r1 ::bi k)
+  | Cnotcompfzero cmp, a1 :: nil =>
+      do r1 <- freg_of a1;
+      OK (Pfcmp0 D r1 ::bi k)
+  | Ccompfs cmp, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2;
+      OK (Pfcmp S r1 r2 ::bi k)
+  | Cnotcompfs cmp, a1 :: a2 :: nil =>
+      do r1 <- freg_of a1; do r2 <- freg_of a2;
+      OK (Pfcmp S r1 r2 ::bi k)
+  | Ccompfszero cmp, a1 :: nil =>
+      do r1 <- freg_of a1;
+      OK (Pfcmp0 S r1 ::bi k)
+  | Cnotcompfszero cmp, a1 :: nil =>
+      do r1 <- freg_of a1;
+      OK (Pfcmp0 S r1 ::bi k)
+  | _, _ =>
+      Error(msg "Asmgenblock.transl_cond")
+  end.
+
+Definition cond_for_signed_cmp (cmp: comparison) :=
+  match cmp with
+  | Ceq => TCeq
+  | Cne => TCne
+  | Clt => TClt
+  | Cle => TCle
+  | Cgt => TCgt
+  | Cge => TCge
+  end.
+
+Definition cond_for_unsigned_cmp (cmp: comparison) :=
+  match cmp with
+  | Ceq => TCeq
+  | Cne => TCne
+  | Clt => TClo
+  | Cle => TCls
+  | Cgt => TChi
+  | Cge => TChs
+  end.
+
+Definition cond_for_float_cmp (cmp: comparison) :=
+  match cmp with
+  | Ceq => TCeq
+  | Cne => TCne
+  | Clt => TCmi
+  | Cle => TCls
+  | Cgt => TCgt
+  | Cge => TCge
+  end.
+
+Definition cond_for_float_not_cmp (cmp: comparison) :=
+  match cmp with
+  | Ceq => TCne
+  | Cne => TCeq
+  | Clt => TCpl
+  | Cle => TChi
+  | Cgt => TCle
+  | Cge => TClt
+  end.
+
+Definition cond_for_cond (cond: condition) :=
+  match cond with
+  | Ccomp cmp => cond_for_signed_cmp cmp
+  | Ccompu cmp => cond_for_unsigned_cmp cmp
+  | Ccompshift cmp s a => cond_for_signed_cmp cmp
+  | Ccompushift cmp s a => cond_for_unsigned_cmp cmp
+  | Ccompimm cmp n => cond_for_signed_cmp cmp
+  | Ccompuimm cmp n => cond_for_unsigned_cmp cmp
+  | Cmaskzero n => TCeq
+  | Cmasknotzero n => TCne
+  | Ccompl cmp => cond_for_signed_cmp cmp
+  | Ccomplu cmp => cond_for_unsigned_cmp cmp
+  | Ccomplshift cmp s a => cond_for_signed_cmp cmp
+  | Ccomplushift cmp s a => cond_for_unsigned_cmp cmp
+  | Ccomplimm cmp n => cond_for_signed_cmp cmp
+  | Ccompluimm cmp n => cond_for_unsigned_cmp cmp
+  | Cmasklzero n => TCeq
+  | Cmasklnotzero n => TCne
+  | Ccompf cmp => cond_for_float_cmp cmp
+  | Cnotcompf cmp => cond_for_float_not_cmp cmp
+  | Ccompfzero cmp => cond_for_float_cmp cmp
+  | Cnotcompfzero cmp => cond_for_float_not_cmp cmp
+  | Ccompfs cmp => cond_for_float_cmp cmp
+  | Cnotcompfs cmp => cond_for_float_not_cmp cmp
+  | Ccompfszero cmp => cond_for_float_cmp cmp
+  | Cnotcompfszero cmp => cond_for_float_not_cmp cmp
+  end.
+
+(** Translation of a conditional branch.  Prepends to [k] the instructions
+  that evaluate the condition and ranch to [lbl] if it holds.
+  We recognize some conditional branches that can be implemented
+  without setting then testing condition flags.  *)
+
+Definition transl_cond_branch_default
+  (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*control) :=
+  do ccode <- transl_cond c args k;
+  OK(ccode, PCtlFlow (Pbc (cond_for_cond c) lbl)).
+ 
+Definition transl_cond_branch
+  (c: condition) (args: list mreg) (lbl: label) (k: bcode) : res (bcode*control) :=
+  match args, c with
+  | a1 :: nil, (Ccompimm Cne n | Ccompuimm Cne n) =>
+      if Int.eq n Int.zero
+      then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbnz W r1 lbl)))
+      else transl_cond_branch_default c args lbl k
+  | a1 :: nil, (Ccompimm Ceq n | Ccompuimm Ceq n) =>
+      if Int.eq n Int.zero
+      then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbz W r1 lbl)))
+      else transl_cond_branch_default c args lbl k
+  | a1 :: nil, (Ccomplimm Cne n | Ccompluimm Cne n) =>
+      if Int64.eq n Int64.zero
+      then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbnz X r1 lbl)))
+      else transl_cond_branch_default c args lbl k
+  | a1 :: nil, (Ccomplimm Ceq n | Ccompluimm Ceq n) =>
+      if Int64.eq n Int64.zero
+      then (do r1 <- ireg_of a1; OK (k, PCtlFlow (Pcbz X r1 lbl)))
+      else transl_cond_branch_default c args lbl k
+  | a1 :: nil, Cmaskzero n =>
+      match Int.is_power2 n with
+      | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbz W r1 bit lbl))
+      | None => transl_cond_branch_default c args lbl k
+      end
+  | a1 :: nil, Cmasknotzero n =>
+      match Int.is_power2 n with
+      | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbnz W r1 bit lbl))
+      | None => transl_cond_branch_default c args lbl k
+      end
+  | a1 :: nil, Cmasklzero n =>
+      match Int64.is_power2' n with
+      | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbz X r1 bit lbl))
+      | None => transl_cond_branch_default c args lbl k
+      end
+  | a1 :: nil, Cmasklnotzero n =>
+      match Int64.is_power2' n with
+      | Some bit => do r1 <- ireg_of a1; OK (k, PCtlFlow (Ptbnz X r1 bit lbl))
+      | None => transl_cond_branch_default c args lbl k
+      end
+  | _, _ =>
+      transl_cond_branch_default c args lbl k
+  end.
+
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
 
@@ -289,10 +597,397 @@ Definition transl_op
   | Ointconst n, nil =>
       do rd <- ireg_of res;
       OK (loadimm32 rd n k)
+  | Olongconst n, nil =>
+      do rd <- ireg_of res;
+      OK (loadimm64 rd n k)
+  | Ofloatconst f, nil =>
+      do rd <- freg_of res;
+      OK (if Float.eq_dec f Float.zero
+          then Pfmovi D rd XZR ::bi k
+          else Pfmovimmd f rd ::bi k)
+  | Osingleconst f, nil =>
+      do rd <- freg_of res;
+      OK (if Float32.eq_dec f Float32.zero
+          then Pfmovi S rd XZR ::bi k
+          else Pfmovimms f rd ::bi k)
+  | Oaddrsymbol id ofs, nil =>
+      do rd <- ireg_of res;
+      OK (loadsymbol rd id ofs k)
+  | Oaddrstack ofs, nil =>
+      do rd <- ireg_of res;
+      OK (addimm64 rd XSP (Ptrofs.to_int64 ofs) k)
+  (** 32-bit integer arithmetic *)
+  | Oshift s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Porr W (transl_shift s a) rd XZR r1 ::bi k)
+  | Oadd, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Padd W SOnone rd r1 r2 ::bi k)
+  | Oaddshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Padd W (transl_shift s a) rd r1 r2 ::bi 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")
+  | Oneg, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psub W SOnone rd XZR r1 ::bi k)
+  | Onegshift s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psub W (transl_shift s a) rd XZR r1 ::bi k)
+  | Osub, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psub W SOnone rd r1 r2 ::bi k)
+  | Osubshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psub W (transl_shift s a) rd r1 r2 ::bi k)
+  | Omul, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pmadd W rd rs1 rs2 XZR ::bi k)
+  | Omuladd, a1 :: a2 :: a3 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
+      OK (Pmadd W rd r2 r3 r1 ::bi k)
+  | Omulsub, a1 :: a2 :: a3 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
+      OK (Pmsub W rd r2 r3 r1 ::bi k)
+  | Odiv, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psdiv W rd r1 r2 ::bi k)
+  | Odivu, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pudiv W rd r1 r2 ::bi k)
+  | Oand, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pand W SOnone rd r1 r2 ::bi k)
+  | Oandshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pand W (transl_shift s a) rd r1 r2 ::bi k)
+  | Oandimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (logicalimm32 (Pandimm W) (Pand W) rd r1 n k)
+  | Oor, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porr W SOnone rd r1 r2 ::bi k)
+  | Oorshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porr W (transl_shift s a) rd r1 r2 ::bi k)
+  | Oorimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (logicalimm32 (Porrimm W) (Porr W) rd r1 n k)      
+  | Oxor, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peor W SOnone rd r1 r2 ::bi k)
+  | Oxorshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peor W (transl_shift s a) rd r1 r2 ::bi k)
+  | Oxorimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (logicalimm32 (Peorimm W) (Peor W) rd r1 n k)      
+  | Onot, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Porn W SOnone rd XZR r1 ::bi k)
+  | Onotshift s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Porn W (transl_shift s a) rd XZR r1 ::bi k)
+  | Obic, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pbic W SOnone rd r1 r2 ::bi k)
+  | Obicshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pbic W (transl_shift s a) rd r1 r2 ::bi k)
+  | Oorn, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porn W SOnone rd r1 r2 ::bi k)
+  | Oornshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porn W (transl_shift s a) rd r1 r2 ::bi k)
+  | Oeqv, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peon W SOnone rd r1 r2 ::bi k)
+  | Oeqvshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peon W (transl_shift s a) rd r1 r2 ::bi k)
+  | Oshl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Plslv W rd r1 r2 ::bi k)
+  | Oshr, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pasrv W rd r1 r2 ::bi k)
+  | Oshru, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Plsrv W rd r1 r2 ::bi k)
+  | Oshrximm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (shrx32 rd r1 n k)
+  | Ozext s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pubfiz W Int.zero s rd r1 ::bi k)
+  | Osext s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psbfiz W Int.zero s rd r1 ::bi k)
+  | Oshlzext s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pubfiz W a (Z.min s (Int.zwordsize - Int.unsigned a)) rd r1 ::bi k)
+  | Oshlsext s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psbfiz W a (Z.min s (Int.zwordsize - Int.unsigned a)) rd r1 ::bi k)
+  | Ozextshr a s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pubfx W a (Z.min s (Int.zwordsize - Int.unsigned a)) rd r1 ::bi k)
+  | Osextshr a s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psbfx W a (Z.min s (Int.zwordsize - Int.unsigned a)) rd r1 ::bi k)
+  (** 64-bit integer arithmetic *)
+  | Oshiftl s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Porr X (transl_shift s a) rd XZR r1 ::bi k)
+  | Oextend x a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (move_extended rd r1 x a k)
+  (* [Omakelong] and [Ohighlong] should not occur *)
+  | Olowlong, a1 :: nil => 
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      assertion (ireg_eq rd r1);
+      OK (Pcvtx2w rd ::bi k)
+  | Oaddl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Padd X SOnone rd r1 r2 ::bi k)
+  | Oaddlshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Padd X (transl_shift s a) rd r1 r2 ::bi k)
+  | Oaddlext x a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (arith_extended Paddext (Padd X) rd r1 r2 x a k)
+  | Oaddlimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (addimm64 rd r1 n k)
+  | Onegl, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psub X SOnone rd XZR r1 ::bi k)
+  | Oneglshift s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psub X (transl_shift s a) rd XZR r1 ::bi k)
+  | Osubl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psub X SOnone rd r1 r2 ::bi k)
+  | Osublshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psub X (transl_shift s a) rd r1 r2 ::bi k)
+  | Osublext x a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (arith_extended Psubext (Psub X) rd r1 r2 x a k)
+  | Omull, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pmadd X rd r1 r2 XZR ::bi k)
+  | Omulladd, a1 :: a2 :: a3 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
+      OK (Pmadd X rd r2 r3 r1 ::bi k)
+  | Omullsub, a1 :: a2 :: a3 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3;
+      OK (Pmsub X rd r2 r3 r1 ::bi k)
+  | Omullhs, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psmulh rd r1 r2 ::bi k)
+  | Omullhu, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pumulh rd r1 r2 ::bi k)
+  | Odivl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Psdiv X rd r1 r2 ::bi k)
+  | Odivlu, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pudiv X rd r1 r2 ::bi k)
+  | Oandl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pand X SOnone rd r1 r2 ::bi k)
+  | Oandlshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pand X (transl_shift s a) rd r1 r2 ::bi k)
+  | Oandlimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (logicalimm64 (Pandimm X) (Pand X) rd r1 n k)      
+  | Oorl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porr X SOnone rd r1 r2 ::bi k)
+  | Oorlshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porr X (transl_shift s a) rd r1 r2 ::bi k)
+  | Oorlimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (logicalimm64 (Porrimm X) (Porr X) rd r1 n k)      
+  | Oxorl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peor X SOnone rd r1 r2 ::bi k)
+  | Oxorlshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peor X (transl_shift s a) rd r1 r2 ::bi k)
+  | Oxorlimm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (logicalimm64 (Peorimm X) (Peor X) rd r1 n k)      
+  | Onotl, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Porn X SOnone rd XZR r1 ::bi k)
+  | Onotlshift s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Porn X (transl_shift s a) rd XZR r1 ::bi k)
+  | Obicl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pbic X SOnone rd r1 r2 ::bi k)
+  | Obiclshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pbic X (transl_shift s a) rd r1 r2 ::bi k)
+  | Oornl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porn X SOnone rd r1 r2 ::bi k)
+  | Oornlshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Porn X (transl_shift s a) rd r1 r2 ::bi k)
+  | Oeqvl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peon X SOnone rd r1 r2 ::bi k)
+  | Oeqvlshift s a, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Peon X (transl_shift s a) rd r1 r2 ::bi k)
+  | Oshll, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Plslv X rd r1 r2 ::bi k)
+  | Oshrl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Pasrv X rd r1 r2 ::bi k)
+  | Oshrlu, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (Plsrv X rd r1 r2 ::bi k)
+  | Oshrlximm n, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (shrx64 rd r1 n k)
+  | Ozextl s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pubfiz X Int.zero s rd r1 ::bi k)
+  | Osextl s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psbfiz X Int.zero s rd r1 ::bi k)
+  | Oshllzext s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pubfiz X a (Z.min s (Int64.zwordsize - Int.unsigned a)) rd r1 ::bi k)
+  | Oshllsext s a, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psbfiz X a (Z.min s (Int64.zwordsize - Int.unsigned a)) rd r1 ::bi k)
+  | Ozextshrl a s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Pubfx X a (Z.min s (Int64.zwordsize - Int.unsigned a)) rd r1 ::bi k)
+  | Osextshrl a s, a1 :: nil =>
+      do rd <- ireg_of res; do r1 <- ireg_of a1;
+      OK (Psbfx X a (Z.min s (Int64.zwordsize - Int.unsigned a)) rd r1 ::bi k)
+  (** 64-bit floating-point arithmetic *)
+  | Onegf, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfneg D rd rs ::bi k)
+  | Oabsf, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfabs D rd rs ::bi k)
+  | Oaddf, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfadd D rd rs1 rs2 ::bi k)
+  | Osubf, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfsub D rd rs1 rs2 ::bi k)
+  | Omulf, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfmul D rd rs1 rs2 ::bi k)
+  | Odivf, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfdiv D rd rs1 rs2 ::bi k)
+  (** 32-bit floating-point arithmetic *)
+  | Onegfs, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfneg S rd rs ::bi k)
+  | Oabsfs, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfabs S rd rs ::bi k)
+  | Oaddfs, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfadd S rd rs1 rs2 ::bi k)
+  | Osubfs, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfsub S rd rs1 rs2 ::bi k)
+  | Omulfs, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfmul S rd rs1 rs2 ::bi k)
+  | Odivfs, a1 :: a2 :: nil =>
+      do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2;
+      OK (Pfdiv S rd rs1 rs2 ::bi k)
+  | Osingleoffloat, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfcvtsd rd rs ::bi k)
+  | Ofloatofsingle, a1 :: nil =>
+      do rd <- freg_of res; do rs <- freg_of a1;
+      OK (Pfcvtds rd rs ::bi k)
+  (** Conversions between int and float *)
+  | Ointoffloat, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzs W D rd rs ::bi k)
+  | Ointuoffloat, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzu W D rd rs ::bi k)
+  | Ofloatofint, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pscvtf D W rd rs ::bi k)
+  | Ofloatofintu, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pucvtf D W rd rs ::bi k)
+  | Ointofsingle, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzs W S rd rs ::bi k)
+  | Ointuofsingle, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzu W S rd rs ::bi k)
+  | Osingleofint, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pscvtf S W rd rs ::bi k)
+  | Osingleofintu, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pucvtf S W rd rs ::bi k)
+  | Olongoffloat, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzs X D rd rs ::bi k)
+  | Olonguoffloat, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzu X D rd rs ::bi k)
+  | Ofloatoflong, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pscvtf D X rd rs ::bi k)
+  | Ofloatoflongu, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pucvtf D X rd rs ::bi k)
+  | Olongofsingle, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzs X S rd rs ::bi k)
+  | Olonguofsingle, a1 :: nil =>
+      do rd <- ireg_of res; do rs <- freg_of a1;
+      OK (Pfcvtzu X S rd rs ::bi k)
+  | Osingleoflong, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pscvtf S X rd rs ::bi k)
+  | Osingleoflongu, a1 :: nil =>
+      do rd <- freg_of res; do rs <- ireg_of a1;
+      OK (Pucvtf S X rd rs ::bi k)
+  (** Boolean tests *)
+  | Ocmp c, _ =>
+      do rd <- ireg_of res;
+      transl_cond c args (Pcset rd (cond_for_cond c) ::bi k)
+  (** Conditional move *)
+  | Osel cmp ty, a1 :: a2 :: args =>
+      match preg_of res with
+      | IR' r => 
+          do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+          transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) ::bi k)
+      | FR' r =>
+          do r1 <- freg_of a1; do r2 <- freg_of a2;
+          transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) ::bi k)
+      | _ =>
+          Error(msg "Asmgenblock.Osel")
+      end
+  | _, _ => Error(msg "Asmgenblock.transl_op")
   end.
 
 (** Translation of a Machblock instruction. *)
@@ -386,16 +1081,16 @@ Obligation 1.
   rewrite <- Heq_anonymous. constructor.
 Qed.
 
-Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep: bool) : res (bcode*option control) :=
+Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep: bool) : res (bcode*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)))
+  | 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))
       (*match make_epilogue f (Pret RA ::c nil) with*)
       (*| nil => OK(nil,None)*)
       (*| b :: k  => OK(body b,exit b)*)
@@ -405,7 +1100,7 @@ Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) (ep:
 
 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, c)
+    Some ctl => do (b,c) <- transl_control f ctl ep; OK (b, Some c)
   | None => OK (nil, None)
   end.