From a56e0c65b08f0f7123630f3a1b415e67ef48c38e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 25 Jul 2020 18:27:04 +0200 Subject: AArch64 implementation of __builtin_ctz* Using the "rbit" instruction (reverse bits). --- aarch64/Asm.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'aarch64/Asm.v') diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 47cd3051..79232783 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -237,6 +237,7 @@ Inductive instruction: Type := | Pclz (sz: isize) (rd r1: ireg) (**r count leading zero bits *) | Prev (sz: isize) (rd r1: ireg) (**r reverse bytes *) | Prev16 (sz: isize) (rd r1: ireg) (**r reverse bytes in each 16-bit word *) + | Prbit (sz: isize) (rd r1: ireg) (**r reverse bits *) (** Conditional data processing *) | Pcsel (rd: ireg) (r1 r2: ireg) (c: testcond) (**r int conditional move *) | Pcset (rd: ireg) (c: testcond) (**r set to 1/0 if cond is true/false *) @@ -1107,6 +1108,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pclz _ _ _ | Prev _ _ _ | Prev16 _ _ _ + | Prbit _ _ _ | Pfsqrt _ _ _ | Pfmadd _ _ _ _ _ | Pfmsub _ _ _ _ _ -- cgit