Introduce 'cmn' instruction and optimize compare-with-immediate when negated immediates can be encoded.

6 files changed, 27 insertions, 1 deletions

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 ->