Reworked constraints for Odiv/Odivu for ARM

The instructions should only have the constraints on argument and result registers if no hardware division is available. In this case, floating point caller save registers must be marked as destroyed by Odiv/Odivu.
AbsInt · Apr 28, 2023 · 94d2111 · 94d2111
1 parent c38688f
commit 94d2111
Show file tree

Hide file tree

Showing 8 changed files with 96 additions and 66 deletions.
diff --git a/arm/Archi.v b/arm/Archi.v
@@ -100,3 +100,6 @@ Parameter abi: abi_kind.
 (** Whether instructions added with Thumb2 are supported. True for ARMv6T2
   and above. *)
 Parameter thumb2_support: bool.
+
+(** Whether the hardware supports sdiv and udiv *)
+Parameter hardware_idiv : unit -> bool.
diff --git a/arm/Asm.v b/arm/Asm.v
@@ -173,10 +173,10 @@ Inductive instruction : Type :=
   | Pstr_a: ireg -> ireg -> shift_op -> instruction (**r any32 store from int register *)
   | Pstrb: ireg -> ireg -> shift_op -> instruction (**r int8 store *)
   | Pstrh: ireg -> ireg -> shift_op -> instruction (**r int16 store *)
-  | Psdiv: instruction                              (**r signed division *)
+  | Psdiv: ireg -> ireg -> ireg -> instruction     (**r signed division *)
   | Psmull: ireg -> ireg -> ireg -> ireg -> instruction (**r signed multiply long *)
   | Psub: ireg -> ireg -> shift_op -> instruction  (**r integer subtraction *)
-  | Pudiv: instruction                             (**r unsigned division *)
+  | Pudiv: ireg -> ireg -> ireg ->  instruction    (**r unsigned division *)
   | Pumull: ireg -> ireg -> ireg -> ireg -> instruction (**r unsigned multiply long *)
   (* Floating-point coprocessor instructions (VFP double scalar operations) *)
   | Pfcpyd: freg -> freg -> instruction             (**r float move *)
@@ -657,11 +657,16 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       exec_store Mint8unsigned (Val.add rs#r2 (eval_shift_op sa rs)) r1 rs m
   | Pstrh r1 r2 sa =>
       exec_store Mint16unsigned (Val.add rs#r2 (eval_shift_op sa rs)) r1 rs m
-  | Psdiv =>
-      match Val.divs rs#IR0 rs#IR1 with
-      | Some v => Next (nextinstr (rs#IR0 <- v
-                                     #IR1 <- Vundef #IR2 <- Vundef
-                                     #IR3 <- Vundef #IR12 <- Vundef)) m
+  | Psdiv rd r1 r2 =>
+      match Val.divs rs#r1 rs#r2 with
+      | Some v => if Archi.hardware_idiv tt then
+                    Next (nextinstr (rs#rd <- v)) m
+                 else
+                    let rs := undef_regs
+                       (IR IR0 :: IR IR1 :: IR IR2 :: IR IR3 :: IR IR12
+                        :: FR FR0 :: FR FR1 :: FR FR2 :: FR FR3
+                        :: FR FR4 :: FR FR5 :: FR FR6 :: FR FR7 :: nil) rs in
+                    Next (nextinstr (rs#rd <- v)) m
       | None => Stuck
       end
   | Psbfx r1 r2 lsb sz =>
@@ -671,11 +676,16 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
                          #rdh <- (Val.mulhs rs#r1 rs#r2))) m
   | Psub r1 r2 so =>
       Next (nextinstr_nf (rs#r1 <- (Val.sub rs#r2 (eval_shift_op so rs)))) m
-  | Pudiv =>
-      match Val.divu rs#IR0 rs#IR1 with
-      | Some v => Next (nextinstr (rs#IR0 <- v
-                                     #IR1 <- Vundef #IR2 <- Vundef
-                                     #IR3 <- Vundef #IR12 <- Vundef)) m
+  | Pudiv rd r1 r2 =>
+      match Val.divu rs#r1 rs#r2 with
+      | Some v => if Archi.hardware_idiv tt then
+                    Next (nextinstr (rs#rd <- v)) m
+                 else
+                    let rs := undef_regs
+                       (IR IR0 :: IR IR1 :: IR IR2 :: IR IR3 :: IR IR12
+                        :: FR FR0 :: FR FR1 :: FR FR2 :: FR FR3
+                        :: FR FR4 :: FR FR5 :: FR FR6 :: FR FR7 :: nil) rs in
+                    Next (nextinstr (rs#rd <- v)) m
       | None => Stuck
       end
   | Pumull rdl rdh r1 r2 =>

diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml
@@ -278,7 +278,7 @@ let pp_instructions pp ic =
     | Prsc(r1, r2, so) -> instruction pp "Prsc" [Ireg r1; Ireg r2; Shift so]
     | Psbc(r1, r2, so) -> instruction pp "Psbc" [Ireg r1; Ireg r2; Shift so]
     | Psbfx(r1, r2, lsb, sz) -> instruction pp "Psbfx" [Ireg r1; Ireg r2; Long lsb; Long sz]
-    | Psdiv -> instruction pp "Psdiv" [Ireg IR0; Ireg IR0; Ireg IR1]
+    | Psdiv (r1, r2, r3) -> instruction pp "Psdiv" [Ireg r1; Ireg r2; Ireg r3]
     | Psmull(r1, r2, r3, r4) -> instruction pp "Psmull" [Ireg r1; Ireg r2; Ireg r3; Ireg r4]
     | Pstr(r1, r2, so) | Pstr_a(r1, r2, so) -> instruction pp "Pstr" [Ireg r1; Ireg r2; Shift so]
     | Pstr_p(r1, r2, so) -> instruction pp "Pstr_p" [Ireg r1; Ireg r2; Shift so]
@@ -288,7 +288,7 @@ let pp_instructions pp ic =
     | Pstrh_p(r1, r2, so) -> instruction pp "Pstrh_p" [Ireg r1; Ireg r2; Shift so]
     | Psub(r1, r2, so) -> instruction pp "Psub" [Ireg r1; Ireg r2; Shift so]
     | Psubs(r1, r2, so) -> instruction pp "Psubs" [Ireg r1; Ireg r2; Shift so]
-    | Pudiv -> instruction pp "Pudiv" [Ireg IR0; Ireg IR0; Ireg IR1]
+    | Pudiv (r1, r2, r3) -> instruction pp "Pudiv" [Ireg r1; Ireg r2; Ireg r3]
     | Pumull(r1, r2, r3, r4) -> instruction pp "Pumull" [Ireg r1; Ireg r2; Ireg r3; Ireg r4]
     (* Fixup instructions for calling conventions *)
     | Pfcpy_fs(r1, r2) -> instruction pp "Pfcpy_fs" [SFreg r1; SPreg r2]

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
@@ -417,15 +417,23 @@ Definition transl_op
       do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (Pumull IR14 r r1 r2 :: k)
   | Odiv, a1 :: a2 :: nil =>
-      assertion (mreg_eq res R0);
-      assertion (mreg_eq a1 R0);
-      assertion (mreg_eq a2 R1);
-      OK (Psdiv :: k)
+      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      if Archi.hardware_idiv tt then
+        OK (Psdiv r r1 r2 :: k)
+      else
+        assertion (mreg_eq res R0);
+        assertion (mreg_eq a1 R0);
+        assertion (mreg_eq a2 R1);
+        OK (Psdiv r r1 r2 :: k)
   | Odivu, a1 :: a2 :: nil =>
-      assertion (mreg_eq res R0);
-      assertion (mreg_eq a1 R0);
-      assertion (mreg_eq a2 R1);
-      OK (Pudiv :: k)
+      do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      if Archi.hardware_idiv tt then
+        OK (Pudiv r r1 r2 :: k)
+      else
+        assertion (mreg_eq res R0);
+        assertion (mreg_eq a1 R0);
+        assertion (mreg_eq a2 R1);
+        OK (Pudiv r r1 r2 :: k)
   | Oand, a1 :: a2 :: nil =>
       do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (Pand r r1 (SOreg r2) :: k)

diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
@@ -1197,17 +1197,17 @@ Lemma transl_op_correct_same:
 Proof.
   intros until v; intros TR EV NOCMP.
   unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; inv EV; try (TranslOpSimpl; fail).
-  (* Omove *)
+- (* Omove *)
   destruct (preg_of res) eqn:RES; try discriminate;
   destruct (preg_of m0) eqn:ARG; inv TR.
   econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl.
   econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl.
-  (* Ointconst *)
+- (* Ointconst *)
   generalize (loadimm_correct x i k rs m). intros [rs' [A [B C]]].
   exists rs'; auto with asmgen.
-  (* Oaddrstack *)
+- (* Oaddrstack *)
   contradiction.
-  (* Ocast8signed *)
+- (* Ocast8signed *)
   destruct Archi.thumb2_support.
   econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl.
   destruct (rs x0); auto; simpl. rewrite Int.shru_zero. reflexivity.
@@ -1220,7 +1220,7 @@ Proof.
   change (Int.ltu (Int.repr 24) Int.iwordsize) with true; simpl.
   f_equal. symmetry. apply (Int.sign_ext_shr_shl 8). compute; intuition congruence.
   intros. unfold rs2, rs1; Simpl.
-  (* Ocast16signed *)
+- (* Ocast16signed *)
   destruct Archi.thumb2_support.
   econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl.
   destruct (rs x0); auto; simpl. rewrite Int.shru_zero. reflexivity.
@@ -1233,44 +1233,48 @@ Proof.
   change (Int.ltu (Int.repr 16) Int.iwordsize) with true; simpl.
   f_equal. symmetry. apply (Int.sign_ext_shr_shl 16). compute; intuition congruence.
   intros. unfold rs2, rs1; Simpl.
-  (* Oaddimm *)
+- (* Oaddimm *)
   generalize (addimm_correct x x0 i k rs m).
   intros [rs' [A [B C]]].
   exists rs'; auto with asmgen.
-  (* Orsbimm *)
+- (* Orsbimm *)
   generalize (rsubimm_correct x x0 i k rs m).
   intros [rs' [A [B C]]].
   exists rs'; auto with asmgen.
-  (* divs *)
-Local Transparent destroyed_by_op.
-  econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto.
-  split. Simpl. simpl; intros. intuition Simpl.
-  (* divu *)
-  econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto.
-  split. Simpl. simpl; intros. intuition Simpl.
-  (* Oandimm *)
+- (* divs *)
+  Local Transparent destroyed_by_op.
+  unfold destroyed_by_op.
+  destruct (Archi.hardware_idiv tt) eqn:?; monadInv EQ3;
+  econstructor; split; try apply exec_straight_one; simpl; try rewrite H0; try rewrite Heqb; auto;split; Simpl;
+  intros; intuition Simpl.
+- (* divu *)
+  unfold destroyed_by_op.
+  destruct (Archi.hardware_idiv tt) eqn:?; monadInv EQ3;
+  econstructor; split; try apply exec_straight_one; simpl; try rewrite H0; try rewrite Heqb; auto;split; Simpl;
+  intros; intuition Simpl.
+- (* Oandimm *)
   generalize (andimm_correct x x0 i k rs m).
   intros [rs' [A [B C]]].
   exists rs'; auto with asmgen.
-  (* Oorimm *)
+- (* Oorimm *)
   generalize (orimm_correct x x0 i k rs m).
   intros [rs' [A [B C]]].
   exists rs'; auto with asmgen.
-  (* Oxorimm *)
+- (* Oxorimm *)
   generalize (xorimm_correct x x0 i k rs m).
   intros [rs' [A [B C]]].
   exists rs'; auto with asmgen.
-  (* Oshrximm *)
+- (* Oshrximm *)
   destruct (rs x0) eqn: X0; simpl in H0; try discriminate.
   destruct (Int.ltu i (Int.repr 31)) eqn: LTU; inv H0.
   revert EQ2. predSpec Int.eq Int.eq_spec i Int.zero; intros EQ2.
-  (* i = 0 *)
++ (* i = 0 *)
   inv EQ2. econstructor.
   split. apply exec_straight_one. simpl. reflexivity. auto.
   split. Simpl. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs.
   change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto.
   intros. Simpl.
-  (* i <> 0 *)
++ (* i <> 0 *)
   inv EQ2.
   assert (LTU': Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize = true).
   {
@@ -1306,34 +1310,34 @@ Local Transparent destroyed_by_op.
   rewrite LTU'; simpl. rewrite LTU''; simpl.
   f_equal. symmetry. apply Int.shrx_shr_2. assumption.
   intros. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl.
-  (* intoffloat *)
+- (* intoffloat *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
 Transparent destroyed_by_op.
   simpl. intuition Simpl.
-  (* intuoffloat *)
+- (* intuoffloat *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
   simpl. intuition Simpl.
-  (* floatofint *)
+- (* floatofint *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
   intuition Simpl.
-  (* floatofintu *)
+- (* floatofintu *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
   intuition Simpl.
-  (* intofsingle *)
+- (* intofsingle *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
   simpl. intuition Simpl.
-  (* intuofsingle *)
+- (* intuofsingle *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
   simpl. intuition Simpl.
-  (* singleofint *)
+- (* singleofint *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
   intuition Simpl.
-  (* singleofintu *)
+- (* singleofintu *)
   econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto.
   intuition Simpl.
-  (* Ocmp *)
+- (* Ocmp *)
   contradiction.
-  (* Osel *)
+- (* Osel *)
   contradiction.
 Qed.
 

diff --git a/arm/Machregs.v b/arm/Machregs.v
@@ -123,7 +123,11 @@ Definition register_by_name (s: string) : option mreg :=
 
 Definition destroyed_by_op (op: operation): list mreg :=
   match op with
-  | Odiv | Odivu => R0 :: R1 :: R2 :: R3 :: R12 :: nil
+  | Odiv | Odivu =>
+             if Archi.hardware_idiv tt then
+              nil
+             else
+              R0 :: R1 :: R2 :: R3 :: R12 :: F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: nil
   | Ointoffloat | Ointuoffloat | Ointofsingle | Ointuofsingle => F6 :: nil
   | _ => nil
   end.
@@ -169,7 +173,7 @@ Definition temp_for_parent_frame: mreg :=
 
 Definition mregs_for_operation (op: operation): list (option mreg) * option mreg :=
   match op with
-  | Odiv | Odivu => (Some R0 :: Some R1 :: nil, Some R0)
+  | Odiv | Odivu => if Archi.hardware_idiv tt then (nil, None) else (Some R0 :: Some R1 :: nil, Some R0)
   | _ => (nil, None)
   end.
 

diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
@@ -24,7 +24,6 @@ open Fileinfo
 module type PRINTER_OPTIONS =
 sig
   val vfpv3: bool
-  val hardware_idiv: bool
 end
 
 (* Basic printing functions *)
@@ -323,9 +322,9 @@ struct
       fprintf oc "	strb	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa
     | Pstrh_p(r1, r2, sa) ->
       fprintf oc "	strh	%a, [%a], %a\n" ireg r1 ireg r2 shift_op sa
-    | Psdiv ->
-      if Opt.hardware_idiv then
-        fprintf oc "	sdiv	r0, r0, r1\n"
+    | Psdiv (r, r1, r2) ->
+      if Archi.hardware_idiv () then
+        fprintf oc "	sdiv	%a, %a, %a\n" ireg r ireg r1 ireg r2
       else
         fprintf oc "	bl	__aeabi_idiv\n"
     | Psbfx(r1, r2, lsb, sz) ->
@@ -339,9 +338,9 @@ struct
     | Psubs(r1, r2, so) ->
       fprintf oc "	subs	%a, %a, %a\n"
         ireg r1 ireg r2 shift_op so
-    | Pudiv ->
-      if Opt.hardware_idiv then
-        fprintf oc "	udiv	r0, r0, r1\n"
+    | Pudiv (r, r1, r2) ->
+      if Archi.hardware_idiv () then
+        fprintf oc "	udiv	%a, %a, %a\n" ireg r ireg r1 ireg r2
       else
          fprintf oc "	bl	__aeabi_uidiv\n"
     | Pumull(r1, r2, r3, r4) ->
@@ -607,10 +606,5 @@ let sel_target () =
 
     let vfpv3 = Configuration.model >= "armv7"
 
-    let hardware_idiv  =
-      match  Configuration.model with
-      | "armv7r" | "armv7m" -> !Clflags.option_mthumb
-      | _ -> false
-
   end in
   (module Target(S):TARGET)
diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v
@@ -36,3 +36,10 @@ Extract Constant Archi.big_endian =>
 (* Whether the model is ARMv6T2 or above and hence supports Thumb2. *)
 Extract Constant Archi.thumb2_support =>
   "(Configuration.model = ""armv6t2"" || Configuration.model >= ""armv7"")".
+
+(* Whether the model has hardware supports sdiv and udiv *)
+Extract Constant Archi.hardware_idiv =>
+  "fun () -> begin match  Configuration.model with
+   | ""armv7r"" | ""armv7m"" -> !Clflags.option_mthumb
+   | _ -> false
+   end".