ARM: Add BFI and BFC

CHANGELOG.md

@@ -44,6 +44,9 @@
 - Add instruction `CMN` to arm-m4:
   ([PR #642](https://github.com/jasmin-lang/jasmin/pull/642)).
 
+- Add instructions `BFC` and `BFI` to arm-m4
+  ([PR #643](https://github.com/jasmin-lang/jasmin/pull/643)).
+
 ## Bug fixes
 
 - Type-checking rejects wrongly casted primitive operators

compiler/tests/success/arm-m4/intrinsic_bfc.jazz

@@ -0,0 +1,12 @@
+export
+fn bfc(reg u32 x) -> reg u32 {
+    x = #BFC(x, 0, 1);
+    x = #BFC(x, 31, 1);
+    x = #BFC(x, 0, 32);
+
+    inline bool b;
+    ?{ "<s" = b } = #CMP(x, 5);
+    x = #BFCcc(x, 0, 32, b, x);
+
+    return x;
+}

compiler/tests/success/arm-m4/intrinsic_bfi.jazz

@@ -0,0 +1,15 @@
+export
+fn bfi(reg u32 x) -> reg u32 {
+    reg u32 y;
+    y = 0;
+    y = #BFI(y, x, 0, 1);
+    y = #BFI(y, x, 31, 1);
+    y = #BFI(y, x, 0, 32);
+
+    inline bool b;
+    ?{ "<s" = b } = #CMP(y, 5);
+    y = #BFIcc(y, x, 0, 32, b, y);
+
+    y = y;
+    return y;
+}

eclib/JModel_m4.ec

@@ -48,6 +48,18 @@ op AND x y = let (_n, _z, _c, r) = ANDS x y in r.
 op ANDScc x y g n z c o = if g then ANDS x y else (n, z, c, o).
 op ANDcc x y g o = if g then AND x y else o.
 
+op BFC (x: W32.t) (lsb width: W8.t) : W32.t =
+  let lsbit = to_uint lsb in
+  let msbit = lsbit + to_uint width - 1 in
+  W32.init (fun i => if lsbit <= i <= msbit then false else x.[i]).
+op BFCcc x lsb width g o = if g then BFC x lsb width else o.
+
+op BFI (x y: W32.t) (lsb width: W8.t) : W32.t =
+  let lsbit = to_uint lsb in
+  let msbit = lsbit + to_uint width - 1 in
+  W32.init (fun i => if lsbit <= i <= msbit then y.[i - lsbit] else x.[i]).
+op BFIcc x y lsb width g o = if g then BFI x y lsb width else o.
+
 op BICS (x y: W32.t) : bool * bool * bool * W32.t =
   with_nzc (andw x (invw y)).
 op BIC x y = let (_n, _z, _c, r) = BICS x y in r.

proofs/arch/arch_utils.v

@@ -63,6 +63,8 @@ Definition ak_reg_imm16 : i_args_kinds :=
   [:: [:: [:: CAreg ]; [:: CAimm U16 ] ] ].
 Definition ak_reg_addr : i_args_kinds :=
   [:: [:: [:: CAreg ]; [:: CAmem true ] ] ].
+Definition ak_reg_imm8_imm8 : i_args_kinds :=
+  [:: [:: [:: CAreg ]; [:: CAimm U8 ]; [:: CAimm U8 ] ] ].
 
 Definition ak_reg_reg_reg : i_args_kinds :=
     [:: [:: [:: CAreg ]; [:: CAreg ]; [:: CAreg ] ] ].
@@ -72,6 +74,8 @@ Definition ak_reg_reg_imm8 : i_args_kinds :=
   [:: [:: [:: CAreg ]; [:: CAreg ]; [:: CAimm U8 ] ] ].
 Definition ak_reg_reg_imm16 : i_args_kinds :=
   [:: [:: [:: CAreg ]; [:: CAreg ]; [:: CAimm U16 ] ] ].
+Definition ak_reg_reg_imm8_imm8 : i_args_kinds :=
+  [:: [:: [:: CAreg ]; [:: CAreg ]; [:: CAimm U8 ]; [:: CAimm U8 ] ] ].
 
 Definition ak_reg_reg_reg_reg : i_args_kinds :=
   [:: [:: [:: CAreg ]; [:: CAreg ]; [:: CAreg ] ; [:: CAreg ] ] ].

proofs/compiler/arm_instr_decl.v

@@ -26,6 +26,11 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 
+Module E.
+  Definition no_semantics : error := ErrType.
+End E.
+
+
 (* -------------------------------------------------------------------- *)
 (* ARM instruction options. *)
 
@@ -118,6 +123,8 @@ Variant arm_mnemonic : Type :=
 
 (* Logical *)
 | AND                            (* Bitwise AND *)
+| BFC                            (* Bit Field Clear *)
+| BFI                            (* Bit Field Insert *)
 | BIC                            (* Bitwise AND with bitwise NOT *)
 | EOR                            (* Bitwise XOR *)
 | MVN                            (* Bitwise NOT *)
@@ -177,7 +184,7 @@ Canonical arm_mnemonic_eqType := @ceqT_eqType _ eqTC_arm_mnemonic.
 
 Definition arm_mnemonics : seq arm_mnemonic :=
   [:: ADD; ADC; MUL; MLA; MLS; SDIV; SUB; RSB; UDIV; UMULL; UMAAL; UMLAL; SMULL; SMLAL; SMMUL; SMMULR
-    ; AND; BIC; EOR; MVN; ORR
+    ; AND; BFC; BFI; BIC; EOR; MVN; ORR
     ; ASR; LSL; LSR; ROR; REV; REV16; REVSH
     ; ADR; MOV; MOVT; UBFX; UXTB; UXTH; SBFX; CLZ
     ; CMP; TST; CMN
@@ -267,6 +274,8 @@ Definition string_of_arm_mnemonic (mn : arm_mnemonic) : string :=
   | SMMUL => "SMMUL"
   | SMMULR => "SMMULR" 
   | AND => "AND"
+  | BFC => "BFC"
+  | BFI => "BFI"
   | BIC => "BIC"
   | EOR => "EOR"
   | MVN => "MVN"
@@ -1088,6 +1097,74 @@ Definition arm_AND_instr : instr_desc_t :=
   then x
   else drop_nzc x.
 
+Definition arm_BFC_semi (x : wreg) (lsb width : word U8) : exec wreg :=
+  let lsbit := wunsigned lsb in
+  let nbits := wunsigned width in
+  Let _ := assert (lsbit <? 32)%Z E.no_semantics in
+  Let _ := assert (1 <=? nbits)%Z E.no_semantics in
+  Let _ := assert (nbits <=? 32 - lsbit)%Z E.no_semantics in
+  let msbit := (lsbit + nbits - 1)%Z in
+  let mk i :=
+    if [&& Z.to_nat lsbit <=? i & i <=? Z.to_nat msbit ]
+    then false
+    else wbit_n x i
+  in
+  ok (winit reg_size mk).
+
+Definition arm_BFC_instr : instr_desc_t :=
+  let mn := BFC in
+  {|
+    id_msb_flag := MSB_MERGE;
+    id_tin := [:: sreg; sword8; sword8 ];
+    id_in := [:: E 0; E 1; E 2 ];
+    id_tout := [:: sreg ];
+    id_out := [:: E 0 ];
+    id_semi := arm_BFC_semi;
+    id_nargs := 3;
+    id_args_kinds := ak_reg_imm8_imm8;
+    id_eq_size := refl_equal;
+    id_tin_narr := refl_equal;
+    id_tout_narr := refl_equal;
+    id_check_dest := refl_equal;
+    id_str_jas := pp_s (string_of_arm_mnemonic mn);
+    id_safe := [::];
+    id_pp_asm := pp_arm_op mn opts;
+  |}.
+
+Definition arm_BFI_semi (x y : wreg) (lsb width : word U8) : exec wreg :=
+  let lsbit := wunsigned lsb in
+  let nbits := wunsigned width in
+  Let _ := assert (lsbit <? 32)%Z E.no_semantics in
+  Let _ := assert (1 <=? nbits)%Z E.no_semantics in
+  Let _ := assert (nbits <=? 32 - lsbit)%Z E.no_semantics in
+  let msbit := (lsbit + nbits - 1)%Z in
+  let mk i :=
+    if [&& Z.to_nat lsbit <=? i & i <=? Z.to_nat msbit ]
+    then wbit_n y (i - Z.to_nat lsbit)
+    else wbit_n x i
+  in
+  ok (winit reg_size mk).
+
+Definition arm_BFI_instr : instr_desc_t :=
+  let mn := BFI in
+  {|
+    id_msb_flag := MSB_MERGE;
+    id_tin := [:: sreg; sreg; sword8; sword8 ];
+    id_in := [:: E 0; E 1; E 2; E 3 ];
+    id_tout := [:: sreg ];
+    id_out := [:: E 0 ];
+    id_semi := arm_BFI_semi;
+    id_nargs := 4;
+    id_args_kinds := ak_reg_reg_imm8_imm8;
+    id_eq_size := refl_equal;
+    id_tin_narr := refl_equal;
+    id_tout_narr := refl_equal;
+    id_check_dest := refl_equal;
+    id_str_jas := pp_s (string_of_arm_mnemonic mn);
+    id_safe := [::];
+    id_pp_asm := pp_arm_op mn opts;
+  |}.
+
 Definition arm_BIC_instr : instr_desc_t :=
   let mn := BIC in
   let x :=
@@ -1754,6 +1831,8 @@ Definition mn_desc (mn : arm_mnemonic) : instr_desc_t :=
   | SMMUL => arm_SMMUL_instr
   | SMMULR => arm_SMMULR_instr
   | AND => arm_AND_instr
+  | BFC => arm_BFC_instr
+  | BFI => arm_BFI_instr
   | BIC => arm_BIC_instr
   | EOR => arm_EOR_instr
   | MVN => arm_MVN_instr

proofs/compiler/arm_instr_decl_lemmas.v

@@ -64,6 +64,7 @@ Proof.
   all: case: mn.
   all: rewrite /truncate_args /truncate_val.
 
+  (* Destruct [vprev]. *)
   all:
     repeat (
       case: vprev => [| ? vprev ] //=;
@@ -79,6 +80,7 @@ Proof.
   all: try move=> <-.
   all: subst.
 
+  (* Destruct [vargs]. *)
   all: rewrite /exec_sopn /=.
   all: case: vargs => [| ? vargs ] //; t_xrbindP => // v.
   all:
@@ -98,8 +100,15 @@ Proof.
       end
     ).
 
+  (* Introduce and rewrite all semantic checks. *)
   all: move: hsemop.
-  all: move=> [?]; subst v.
+  all: cbn.
+  all:
+    try match goal with
+    | [ |- ?f _ = ok _ -> _ ] => rewrite /f
+    end.
+  all: t_xrbindP=> *; subst v; t_eq_rewrites.
+
   all: by case: b.
 Qed.
 

proofs/lang/utils.v

@@ -1780,6 +1780,7 @@ Ltac t_do_rewrites tac :=
     match goal with
     | [ h : ?lhs = ?rhs |- _ ] => tac h lhs rhs
     | [ h : is_true (?lhs == ?rhs) |- _ ] => move: h => /eqP h; tac h lhs rhs
+    | [ h : is_true ?lhs |- _ ] => tac h lhs true
     end.
 
 #[local]

proofs/lang/word.v

@@ -195,6 +195,10 @@ Definition word := fun sz =>
 
 Global Opaque word.
 
+Definition winit (ws : wsize) (f : nat -> bool) : word ws :=
+  let bits := map f (iota 0 (wsize_size_minus_1 ws).+1) in
+  t2w (Tuple (tval := bits) ltac:(by rewrite size_map size_iota)).
+
 Definition wand {s} (x y: word s) : word s := wand x y.
 Definition wor {s} (x y: word s) : word s := wor x y.
 Definition wxor {s} (x y: word s) : word s := wxor x y.