From a7c5db0d19778ad337e632214e7ec67080862453 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Wed, 5 Jun 2024 13:48:53 +0200 Subject: [PATCH] Add x86 instructions RORX, SARX, SHRX, SHLX --- CHANGELOG.md | 4 +++ compiler/tests/success/x86-64/shift.jazz | 26 ++++++++++++++ eclib/JWord.ec | 14 +++++++- proofs/compiler/x86_instr_decl.v | 45 ++++++++++++++++++++++++ 4 files changed, 88 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 40e81790d..faa81d171 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3,6 +3,10 @@ ## New features +- The following x86 BMI2 instructions are now available: + `RORX`, `SARX`, `SHRX`, and `SHLX` + ([PR #824](https://github.com/jasmin-lang/jasmin/pull/824)). + - ARM now compiles `x = imm;` smartly: for small immediates, a single `MOV`; for immediates whose negation is small, a single `MVN`; and for large immediates a pair of `MOV` and `MOVT`. diff --git a/compiler/tests/success/x86-64/shift.jazz b/compiler/tests/success/x86-64/shift.jazz index ed924dd7a..15a7ba02c 100644 --- a/compiler/tests/success/x86-64/shift.jazz +++ b/compiler/tests/success/x86-64/shift.jazz @@ -69,3 +69,29 @@ n = 11; [p + 0] = f; } + +export +fn test_rorx(reg u64 x) -> reg u32 { + x = #RORX_64(x, 0); + x = #RORX_64(x, 1); + x = #RORX_64(x, -193); + reg u32 y; + y = #RORX_32(x, 1); + y = #RORX_32(y, 17); + return y; +} + +u64[1] g = {0x536764457835516b}; +export +fn test_bmi_shifts(reg u64 x) -> reg u32 { + stack u64 y; + y = x; + reg u32 z; + x = #SARX_64(g[0], x); + x = #SHRX_64(y, x); + x = #SHLX_64(x, x); + z = #SARX_32(g[u32 0], x); + z = #SHRX_32(z, x); + z = #SHLX_32(x, z); + return z; +} diff --git a/eclib/JWord.ec b/eclib/JWord.ec index 9b7580dd1..76b8e42ed 100644 --- a/eclib/JWord.ec +++ b/eclib/JWord.ec @@ -2497,8 +2497,20 @@ abstract theory BitWordSH. let r = sar v i in rflags_OF i r rc false. + op RORX_XX (v: t) (i: W8.t) : t = + v `|>>>|` shift_mask i. + + op SARX_XX (v i: t) : t = + sar v (to_uint i %% size). + + op SHRX_XX (v i: t) : t = + v `>>>` to_uint i %% size. + + op SHLX_XX (v i: t) : t = + v `<<<` to_uint i %% size. + end SHIFT. - + end BitWordSH. theory W16. diff --git a/proofs/compiler/x86_instr_decl.v b/proofs/compiler/x86_instr_decl.v index 9265452f0..b092bf266 100644 --- a/proofs/compiler/x86_instr_decl.v +++ b/proofs/compiler/x86_instr_decl.v @@ -72,6 +72,12 @@ Variant x86_op : Type := | SAR of wsize (* signed / right *) | SHLD of wsize (* unsigned (double) / left *) | SHRD of wsize (* unsigned (double) / right *) + +| RORX of wsize (* rotate right w/o affecting flags *) +| SARX of wsize (* arithmetic shift right w/o affecting flags *) +| SHRX of wsize (* logical shift right w/o affecting flags *) +| SHLX of wsize (* logical shift left w/o affecting flags *) + | MULX_lo_hi of wsize (* mul unsigned, doesn't affect arithmetic flags *) | ADCX of wsize (* add with carry flag, only writes carry flag *) | ADOX of wsize (* add with overflow flag, only writes overflow flag *) @@ -679,6 +685,21 @@ Definition x86_SAR sz (v: word sz) (i: u8) : ex_tpl (b5w_ty sz) := let r := wsar v (wunsigned i) in rflags_OF i r rc false. +(* ---------------------------------------------------------------- *) +Definition x86_RORX sz (v: word sz) (i: u8) : exec (word sz) := + Let _ := check_size_32_64 sz in + let i := wand i (x86_shift_mask sz) in + ok (wror v (wunsigned i)). + +Definition x86_bmi_shift sz (op: word sz → Z → word sz) (v i: word sz) : exec (word sz) := + Let _ := check_size_32_64 sz in + let i := Z.land (wunsigned i) (wunsigned (x86_shift_mask sz)) in + ok (op v i). + +Definition x86_SARX sz := x86_bmi_shift (@wsar sz). +Definition x86_SHRX sz := x86_bmi_shift (@wshr sz). +Definition x86_SHLX sz := x86_bmi_shift (@wshl sz). + (* ---------------------------------------------------------------- *) Definition x86_BSWAP sz (v: word sz) : ex_tpl (w_ty sz) := Let _ := check_size_32_64 sz in @@ -1456,6 +1477,22 @@ Definition Ox86_SHLD_instr := Definition Ox86_SHRD_instr := mk_instr_w2w8_b5w_01c0 "SHRD" x86_SHRD check_shld safe_shxd (prim_16_64 SHRD) (pp_iname_ww_8 "shrd"). +Definition check_rorx of wsize := [::[::r ; rm true; i U8]]. + +Definition Ox86_RORX_instr := + mk_instr_ww8_w_120 "RORX" x86_RORX check_rorx (prim_32_64 RORX) (pp_name "rorx"). + +Definition check_sarx of wsize := [::[::r ; rm true; r]]. + +Definition Ox86_SARX_instr := + mk_instr_w2_w_120 "SARX" x86_SARX check_sarx (prim_32_64 SARX) (pp_name "sarx"). + +Definition Ox86_SHRX_instr := + mk_instr_w2_w_120 "SHRX" x86_SHRX check_sarx (prim_32_64 SHRX) (pp_name "shrx"). + +Definition Ox86_SHLX_instr := + mk_instr_w2_w_120 "SHLX" x86_SHLX check_sarx (prim_32_64 SHLX) (pp_name "shlx"). + Definition Ox86_BSWAP_instr := mk_instr_w_w "BSWAP" x86_BSWAP [:: Eu 0] [:: Eu 0] 1 (fun _ => [:: [::r]]) (prim_32_64 BSWAP) (pp_iname "bswap"). @@ -1952,6 +1989,10 @@ Definition x86_instr_desc o : instr_desc_t := | SAL sz => Ox86_SAL_instr.1 sz | SHLD sz => Ox86_SHLD_instr.1 sz | SHRD sz => Ox86_SHRD_instr.1 sz + | RORX sz => Ox86_RORX_instr.1 sz + | SARX sz => Ox86_SARX_instr.1 sz + | SHRX sz => Ox86_SHRX_instr.1 sz + | SHLX sz => Ox86_SHLX_instr.1 sz | MOVX sz => Ox86_MOVX_instr.1 sz | MOVD sz => Ox86_MOVD_instr.1 sz | MOVV sz => Ox86_MOVV_instr.1 sz @@ -2090,6 +2131,10 @@ Definition x86_prim_string := Ox86_SAL_instr.2; Ox86_SHLD_instr.2; Ox86_SHRD_instr.2; + Ox86_RORX_instr.2; + Ox86_SARX_instr.2; + Ox86_SHRX_instr.2; + Ox86_SHLX_instr.2; Ox86_MOVX_instr.2; Ox86_MOVD_instr.2; Ox86_MOVV_instr.2;