Merge branch 'master' into add-file

6 files changed, 50 insertions, 17 deletions

diff --git a/arm/Archi.v b/arm/Archi.v
index e4abf009..6b282022 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -26,7 +26,7 @@ Notation align_int64 := 8%Z (only parsing).
 Notation align_float64 := 8%Z (only parsing).
 
 Program Definition default_pl_64 : bool * nan_pl 53 :=
-  (false, nat_iter 51 xO xH).
+  (false, iter_nat 51 _ xO xH).
 
 Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
   (** Choose second NaN if pl2 is sNaN but pl1 is qNan.
@@ -35,7 +35,7 @@ Definition choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_p
    negb (Pos.testbit (proj1_sig pl2) 51))%bool.
 
 Program Definition default_pl_32 : bool * nan_pl 24 :=
-  (false, nat_iter 22 xO xH).
+  (false, iter_nat 22 _ xO xH).
 
 Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) :=
   (** Choose second NaN if pl2 is sNaN but pl1 is qNan.
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 8aef64e4..855ca9ad 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -30,6 +30,9 @@ let _2 = coqint_of_camlint 2l
 let _4 = coqint_of_camlint 4l
 let _8 = coqint_of_camlint 8l
 let _16 = coqint_of_camlint 16l
+let _32 = coqint_of_camlint 32l
+let _64 = coqint_of_camlint 64l
+let _m1 = coqint_of_camlint (-1l)
 
 (* Emit instruction sequences that set or offset a register by a constant. *)
 (* No S suffix because they are applied to SP most of the time. *)
@@ -294,6 +297,33 @@ let expand_builtin_inline name args res =
      emit (Pmovite (TCeq, IR14, SOreg IR14, SOimm _0));
      emit (Pclz (res, ah));
      emit (Padd (res, res, SOreg IR14))
+  | ("__builtin_ctz" | "__builtin_ctzl"), [BA(IR a1)], BR(IR res) ->
+     emit (Padd(IR14, a1, SOimm _m1));   (* tmp := x-1 *)
+     emit (Pmvn(res, SOreg a1));         (* res := ~(x) *)
+     emit (Pand(res, IR14, SOreg res));  (* res := tmp & ~(x) *)
+     emit (Pclz(res, res));              (* res := #leading zeros *)
+     emit (Prsb(res, res, SOimm _32))    (* res := 32 - #leading zeros *)
+  | "__builtin_ctzll", [BA_splitlong(BA(IR ah), BA(IR al))], BR(IR res) ->
+     let lbl1 = new_label () in
+     let lbl2 = new_label () in
+     (* low word equal to zero? *)
+     emit (Pcmp (al, SOimm _0));
+     emit (Pbne lbl1);
+     (* low word is zero, count trailing zeros in high word and increment by 32 *)
+     emit (Padd(IR14, ah, SOimm _m1));
+     emit (Pmvn(res, SOreg ah));
+     emit (Pand(res, IR14, SOreg res));
+     emit (Pclz(res, res));
+     emit (Prsb(res, res, SOimm _64));
+     emit (Pb lbl2);
+     (* count trailing zeros in low word *)
+     emit (Plabel lbl1);
+     emit (Padd(IR14, al, SOimm _m1));
+     emit (Pmvn(res, SOreg al));
+     emit (Pand(res, IR14, SOreg res));
+     emit (Pclz(res, res));
+     emit (Prsb(res, res, SOimm _32));
+     emit (Plabel lbl2)
   (* Float arithmetic *)
   | "__builtin_fabs",  [BA(FR a1)], BR(FR res) ->
      emit (Pfabsd (res,a1))
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 7b3f2fdc..90d3b189 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -173,13 +173,13 @@ Definition loadimm (r: ireg) (n: int) (k: code) :=
   let d2 := decompose_int (Int.not n) in
   let l1 := List.length d1 in
   let l2 := List.length d2 in
-  if NPeano.leb l1 1%nat then
+  if Nat.leb l1 1%nat then
     Pmov r (SOimm n) :: k
-  else if NPeano.leb l2 1%nat then
+  else if Nat.leb l2 1%nat then
     Pmvn r (SOimm (Int.not n)) :: k
   else if thumb tt then
     loadimm_thumb r n k
-  else if NPeano.leb l1 l2 then
+  else if Nat.leb l1 l2 then
     iterate_op (Pmov r) (Porr r r) d1 k
   else
     iterate_op (Pmvn r) (Pbic r r) d2 k.
@@ -190,7 +190,7 @@ Definition addimm (r1 r2: ireg) (n: int) (k: code) :=
   else
    (let d1 := decompose_int n in
     let d2 := decompose_int (Int.neg n) in
-    if NPeano.leb (List.length d1) (List.length d2)
+    if Nat.leb (List.length d1) (List.length d2)
     then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k
     else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k).
 
@@ -801,4 +801,3 @@ Definition transf_fundef (f: Mach.fundef) : res Asm.fundef :=
 
 Definition transf_program (p: Mach.program) : res Asm.program :=
   transform_partial_program transf_fundef p.
-
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 5bd2b54f..431743c6 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -166,11 +166,11 @@ Proof.
   intros. unfold loadimm.
   set (l1 := length (decompose_int n)).
   set (l2 := length (decompose_int (Int.not n))).
-  destruct (NPeano.leb l1 1%nat). TailNoLabel.
-  destruct (NPeano.leb l2 1%nat). TailNoLabel.
+  destruct (Nat.leb l1 1%nat). TailNoLabel.
+  destruct (Nat.leb l2 1%nat). TailNoLabel.
   destruct (thumb tt). unfold loadimm_thumb.
   destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero); TailNoLabel.
-  destruct (NPeano.leb l1 l2); auto with labels.
+  destruct (Nat.leb l1 l2); auto with labels.
 Qed.
 Hint Resolve loadimm_label: labels.
 
@@ -179,7 +179,7 @@ Remark addimm_label:
 Proof.
   intros; unfold addimm.
   destruct (Int.ltu (Int.repr (-256)) n). TailNoLabel.
-  destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n))));
+  destruct (Nat.leb (length (decompose_int n)) (length (decompose_int (Int.neg n))));
   auto with labels.
 Qed.
 Hint Resolve addimm_label: labels.
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 3e222ba4..76a7b080 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -333,11 +333,11 @@ Proof.
   intros. unfold loadimm.
   set (l1 := length (decompose_int n)).
   set (l2 := length (decompose_int (Int.not n))).
-  destruct (NPeano.leb l1 1%nat).
+  destruct (Nat.leb l1 1%nat).
 { (* single mov *)
   econstructor; split. apply exec_straight_one. simpl; reflexivity. auto.
   split; intros; Simpl. }
-  destruct (NPeano.leb l2 1%nat).
+  destruct (Nat.leb l2 1%nat).
 { (* single movn *)
   econstructor; split. apply exec_straight_one.
   simpl. rewrite Int.not_involutive. reflexivity. auto.
@@ -359,7 +359,7 @@ Proof.
   rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega.
   change (Int.unsigned (Int.repr 16)) with 16. rewrite zlt_true by omega. f_equal; omega.
 }
-  destruct (NPeano.leb l1 l2).
+  destruct (Nat.leb l1 l2).
 { (* mov - orr* *)
   replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero).
   apply iterate_op_correct.
@@ -390,7 +390,7 @@ Proof.
   (* sub *)
   econstructor; split. apply exec_straight_one; simpl; auto.
   split; intros; Simpl. apply Val.sub_opp_add.
-  destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))).
+  destruct (Nat.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))).
   (* add - add* *)
   replace (Val.add (rs r2) (Vint n))
      with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (rs r2)).
@@ -1498,5 +1498,3 @@ Proof.
 Qed.
 
 End CONSTRUCTORS.
-
-
diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index 1b06b93b..2015607a 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -35,6 +35,12 @@ let builtins = {
       (TInt(IInt, []), [TInt(IULong, [])], false);
     "__builtin_clzll",
       (TInt(IInt, []), [TInt(IULongLong, [])], false);
+    "__builtin_ctz",
+      (TInt(IInt, []), [TInt(IUInt, [])], false);
+    "__builtin_ctzl",
+      (TInt(IInt, []), [TInt(IULong, [])], false);
+    "__builtin_ctzll",
+      (TInt(IInt, []), [TInt(IULongLong, [])], false);
     (* Float arithmetic *)
     "__builtin_fsqrt",
       (TFloat(FDouble, []), [TFloat(FDouble, [])], false);