From 73ab7968d862c4d4d883fb3d3215353eba905b0f Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Fri, 15 Dec 2017 00:01:30 +0100 Subject: Introduce 'cmn' instruction and optimize compare-with-immediate when negated immediates can be encoded. --- arm/Asm.v | 3 +++ arm/AsmToJSON.ml | 3 ++- arm/Asmgen.v | 4 ++++ arm/Asmgenproof.v | 2 ++ arm/Asmgenproof1.v | 14 ++++++++++++++ arm/TargetPrinter.ml | 2 ++ 6 files changed, 27 insertions(+), 1 deletion(-) diff --git a/arm/Asm.v b/arm/Asm.v index c05ec3e9..184dbc9b 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -148,6 +148,7 @@ Inductive instruction : Type := | Pblreg: ireg -> signature -> instruction (**r computed branch and link *) | Pbic: ireg -> ireg -> shift_op -> instruction (**r bitwise bit-clear *) | Pcmp: ireg -> shift_op -> instruction (**r integer comparison *) + | Pcmn: ireg -> shift_op -> instruction (**r integer comparison with opposite *) | Peor: ireg -> ireg -> shift_op -> instruction (**r bitwise exclusive or *) | Pldr: ireg -> ireg -> shift_op -> instruction (**r int32 load *) | Pldr_a: ireg -> ireg -> shift_op -> instruction (**r any32 load to int register *) @@ -608,6 +609,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr_nf (rs#r1 <- (Val.and rs#r2 (Val.notint (eval_shift_op so rs))))) m | Pcmp r1 so => Next (nextinstr (compare_int rs rs#r1 (eval_shift_op so rs) m)) m + | Pcmn r1 so => + Next (nextinstr (compare_int rs rs#r1 (Val.neg (eval_shift_op so rs)) m)) m | Peor r1 r2 so => Next (nextinstr_nf (rs#r1 <- (Val.xor rs#r2 (eval_shift_op so rs)))) m | Pldr r1 r2 sa => diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml index e105ea20..85ef0603 100644 --- a/arm/AsmToJSON.ml +++ b/arm/AsmToJSON.ml @@ -20,7 +20,7 @@ open Camlcoq open Json let mnemonic_names = [ "Padc"; "Padd"; "Padds"; "Pand";"Pannot"; "Pasr"; "Pb"; "Pbc"; "Pbic"; "Pblreg"; - "Pblsymb"; "Pbne"; "Pbreg"; "Pbsymb"; "Pbtbl"; "Pclz"; "Pcmp"; "Pconstants";"Pfcpy_iif"; + "Pblsymb"; "Pbne"; "Pbreg"; "Pbsymb"; "Pbtbl"; "Pclz"; "Pcmp"; "Pcmn"; "Pconstants"; "Pfcpy_iif"; "Pfcpy_fii"; "Pfcpy_fi"; "Pfcpy_sf"; "Pflid_lbl"; "Pflis_lbl"; "Pdmb"; "Pdsb"; "Peor"; "Pfabsd"; "Pfabss"; "Pfaddd"; "Pfadds"; "Pfcmpd"; "Pfcmps"; "Pfcmpzd"; "Pfcmpzs"; "Pfcpyd"; "Pfcpy_fs"; "Pfcpy_if";"Pfcvtds"; "Pfcvtsd"; "Pfdivd"; "Pfdivs"; "Pfldd"; @@ -207,6 +207,7 @@ let pp_instructions pp ic = | Pbtbl(r, tbl) -> instruction pp "Pbtbl" ((Ireg r)::(List.map (fun a -> ALabel a) tbl)) | Pclz(r1, r2) -> instruction pp "Pclz" [Ireg r1; Ireg r2] | Pcmp(r1,so) -> instruction pp "Pcmp" [Ireg r1; Shift so] + | Pcmn(r1,so) -> instruction pp "Pcmn" [Ireg r1; Shift so] | Pdmb -> instruction pp "Pdmb" [] | Pdsb -> instruction pp "Pdsb" [] | Peor(r1, r2, so) -> instruction pp "Peor" [Ireg r1; Ireg r2; Shift so] diff --git a/arm/Asmgen.v b/arm/Asmgen.v index ed64e2f0..1d2f360f 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -242,12 +242,16 @@ Definition transl_cond do r1 <- ireg_of a1; OK (if is_immed_arith n then Pcmp r1 (SOimm n) :: k + else if is_immed_arith (Int.neg n) then + Pcmn r1 (SOimm (Int.neg n)) :: k else loadimm IR14 n (Pcmp r1 (SOreg IR14) :: k)) | Ccompuimm c n, a1 :: nil => do r1 <- ireg_of a1; OK (if is_immed_arith n then Pcmp r1 (SOimm n) :: k + else if is_immed_arith (Int.neg n) then + Pcmn r1 (SOimm (Int.neg n)) :: k else loadimm IR14 n (Pcmp r1 (SOreg IR14) :: k)) | Ccompf cmp, a1 :: a2 :: nil => diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 9e6b2c98..abec6815 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -255,7 +255,9 @@ Remark transl_cond_label: Proof. unfold transl_cond; intros; destruct cond; TailNoLabel. destruct (is_immed_arith i). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. + destruct (is_immed_arith (Int.neg i)). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. destruct (is_immed_arith i). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. + destruct (is_immed_arith (Int.neg i)). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. Qed. Remark transl_op_label: diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index c1015a8c..98cd5eea 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -1069,6 +1069,13 @@ Proof. split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:CMP; auto. split; apply cond_for_signed_cmp_correct; auto. rewrite Val.negate_cmp_bool, CMP; auto. apply compare_int_inv. + destruct (is_immed_arith (Int.neg i)). + econstructor. + split. apply exec_straight_one. simpl. eauto. auto. + split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:CMP; auto. + split; apply cond_for_signed_cmp_correct; rewrite Int.neg_involutive; auto. + rewrite Val.negate_cmp_bool, CMP; auto. + apply compare_int_inv. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. @@ -1084,6 +1091,13 @@ Proof. split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint i)) eqn:CMP; auto. split; apply cond_for_unsigned_cmp_correct; auto. rewrite Val.negate_cmpu_bool, CMP; auto. apply compare_int_inv. + destruct (is_immed_arith (Int.neg i)). + econstructor. + split. apply exec_straight_one. simpl. eauto. auto. + split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint i)) eqn:CMP; auto. + split; apply cond_for_unsigned_cmp_correct; rewrite Int.neg_involutive; auto. + rewrite Val.negate_cmpu_bool, CMP; auto. + apply compare_int_inv. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 93733f56..bb7f24df 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -239,6 +239,8 @@ struct fprintf oc " clz %a, %a\n" ireg r1 ireg r2 | Pcmp(r1, so) -> fprintf oc " cmp %a, %a\n" ireg r1 shift_op so + | Pcmn(r1, so) -> + fprintf oc " cmn %a, %a\n" ireg r1 shift_op so | Pdmb -> fprintf oc " dmb\n" | Pdsb -> -- cgit