IA32: model integer division and modulus closer to the machine

lib/Integers.v: define division-remainder of a double word by a word
ia32/Asm.v: use it to give Pdiv and Pidiv their "true" semantics like in the processor; add Pcltd as an instruction
ia32/*: adapt accordingly

Additional benefit: Pcltd could be used for an alternate implementation of shrximm.

4 files changed, 95 insertions, 50 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 12d164a6..b4fc950b 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -151,6 +151,7 @@ Inductive instruction: Type :=
   | Pimul_ri (rd: ireg) (n: int)
   | Pimul_r (r1: ireg)
   | Pmul_r (r1: ireg)
+  | Pcltd
   | Pdiv (r1: ireg)
   | Pidiv (r1: ireg)
   | Pand_rr (rd: ireg) (r1: ireg)
@@ -618,17 +619,25 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pmul_r r1 =>
       Next (nextinstr_nf (rs#EAX <- (Val.mul rs#EAX rs#r1)
                             #EDX <- (Val.mulhu rs#EAX rs#r1))) m
+  | Pcltd =>
+      Next (nextinstr_nf (rs#EDX <- (Val.shr rs#EAX (Vint (Int.repr 31))))) m
   | Pdiv r1 =>
-      let vn := rs#EAX in let vd := (rs#EDX <- Vundef)#r1 in
-      match Val.divu vn vd, Val.modu vn vd with
-      | Some vq, Some vr => Next (nextinstr_nf (rs#EAX <- vq #EDX <- vr)) m
-      | _, _ => Stuck
+      match rs#EDX, rs#EAX, rs#r1 with
+      | Vint nh, Vint nl, Vint d =>
+          match Int.divmodu2 nh nl d with
+          | Some(q, r) => Next (nextinstr_nf (rs#EAX <- (Vint q) #EDX <- (Vint r))) m
+          | None => Stuck
+          end
+      | _, _, _ => Stuck
       end
   | Pidiv r1 =>
-      let vn := rs#EAX in let vd := (rs#EDX <- Vundef)#r1 in
-      match Val.divs vn vd, Val.mods vn vd with
-      | Some vq, Some vr => Next (nextinstr_nf (rs#EAX <- vq #EDX <- vr)) m
-      | _, _ => Stuck
+      match rs#EDX, rs#EAX, rs#r1 with
+      | Vint nh, Vint nl, Vint d =>
+          match Int.divmods2 nh nl d with
+          | Some(q, r) => Next (nextinstr_nf (rs#EAX <- (Vint q) #EDX <- (Vint r))) m
+          | None => Stuck
+          end
+      | _, _, _ => Stuck
       end
   | Pand_rr rd r1 =>
       Next (nextinstr_nf (rs#rd <- (Val.and rs#rd rs#r1))) m
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index fd0d5bc5..1d718c26 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -315,22 +315,22 @@ Definition transl_op
       assertion (mreg_eq a1 AX);
       assertion (mreg_eq a2 CX);
       assertion (mreg_eq res AX);
-      OK(Pidiv ECX :: k)
+      OK(Pcltd :: Pidiv ECX :: k)
   | Odivu, a1 :: a2 :: nil =>
       assertion (mreg_eq a1 AX);
       assertion (mreg_eq a2 CX);
       assertion (mreg_eq res AX);
-      OK(Pdiv ECX :: k)
+      OK(Pxor_r EDX :: Pdiv ECX :: k)
   | Omod, a1 :: a2 :: nil =>
       assertion (mreg_eq a1 AX);
       assertion (mreg_eq a2 CX);
       assertion (mreg_eq res DX);
-      OK(Pidiv ECX :: k)
+      OK(Pcltd :: Pidiv ECX :: k)
   | Omodu, a1 :: a2 :: nil =>
       assertion (mreg_eq a1 AX);
       assertion (mreg_eq a2 CX);
       assertion (mreg_eq res DX);
-      OK(Pdiv ECX :: k)
+      OK(Pxor_r EDX :: Pdiv ECX :: k)
   | Oand, a1 :: a2 :: nil =>
       assertion (mreg_eq a1 res);
       do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pand_rr r r2 :: k)
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 60cc266e..9703d419 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -121,28 +121,44 @@ Qed.
 
 (** Properties of division *)
 
-Remark divs_mods_exist:
+Lemma divu_modu_exists:
   forall v1 v2,
-  match Val.divs v1 v2, Val.mods v1 v2 with
-  | Some _, Some _ => True
-  | None, None => True
-  | _, _ => False
-  end.
+  Val.divu v1 v2 <> None \/ Val.modu v1 v2 <> None ->
+  exists n d q r,
+     v1 = Vint n /\ v2 = Vint d
+  /\ Int.divmodu2 Int.zero n d = Some(q, r)
+  /\ Val.divu v1 v2 = Some (Vint q) /\ Val.modu v1 v2 = Some (Vint r).
 Proof.
-  intros. unfold Val.divs, Val.mods. destruct v1; auto. destruct v2; auto.
-  destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); auto.
+  intros v1 v2; unfold Val.divu, Val.modu.
+  destruct v1; try (intuition discriminate).
+  destruct v2; try (intuition discriminate).
+  predSpec Int.eq Int.eq_spec i0 Int.zero ; try (intuition discriminate).
+  intros _. exists i, i0, (Int.divu i i0), (Int.modu i i0); intuition auto.
+  apply Int.divmodu2_divu_modu; auto.
 Qed.
 
-Remark divu_modu_exist:
+Lemma divs_mods_exists:
   forall v1 v2,
-  match Val.divu v1 v2, Val.modu v1 v2 with
-  | Some _, Some _ => True
-  | None, None => True
-  | _, _ => False
-  end.
+  Val.divs v1 v2 <> None \/ Val.mods v1 v2 <> None ->
+  exists nh nl d q r,
+     Val.shr v1 (Vint (Int.repr 31)) = Vint nh /\ v1 = Vint nl /\ v2 = Vint d
+  /\ Int.divmods2 nh nl d = Some(q, r)
+  /\ Val.divs v1 v2 = Some (Vint q) /\ Val.mods v1 v2 = Some (Vint r).
 Proof.
-  intros. unfold Val.divu, Val.modu. destruct v1; auto. destruct v2; auto.
-  destruct (Int.eq i0 Int.zero); auto.
+  intros v1 v2; unfold Val.divs, Val.mods.
+  destruct v1; try (intuition discriminate).
+  destruct v2; try (intuition discriminate).
+  destruct (Int.eq i0 Int.zero
+            || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone) eqn:OK;
+  try (intuition discriminate).
+  intros _.
+  InvBooleans. 
+  exists (Int.shr i (Int.repr 31)), i, i0, (Int.divs i i0), (Int.mods i i0); intuition auto.
+  rewrite Int.shr_lt_zero. apply Int.divmods2_divs_mods.
+  red; intros; subst i0; rewrite Int.eq_true in H; discriminate.
+  revert H0. predSpec Int.eq Int.eq_spec i (Int.repr Int.min_signed); auto.
+  predSpec Int.eq Int.eq_spec i0 Int.mone; auto.
+  discriminate.
 Qed.
 
 (** Smart constructor for [shrx] *)
@@ -1031,32 +1047,52 @@ Transparent destroyed_by_op.
   apply SAME. TranslOp. destruct H1. Simplifs.
 (* div *)
   apply SAME.
-  specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0.
-  destruct (Val.mods (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction.
-  TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto.
-  auto. auto.
-  simpl in H3. destruct H3; Simplifs.
+  exploit (divs_mods_exists (rs EAX) (rs ECX)). left; congruence.
+  intros (nh & nl & d & q & r & A & B & C & D & E & F).
+  set (rs1 := nextinstr_nf (rs#EDX <- (Vint nh))).
+  econstructor; split.
+  eapply exec_straight_two with (rs2 := rs1). simpl. rewrite A. reflexivity.
+  simpl. change (rs1 EAX) with (rs EAX); rewrite B.
+  change (rs1 ECX) with (rs ECX); rewrite C.
+  rewrite D. reflexivity. auto. auto.
+  split. change (Vint q = v). congruence.
+  simpl; intros. destruct H2. unfold rs1; Simplifs.
 (* divu *)
   apply SAME.
-  specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0.
-  destruct (Val.modu (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction.
-  TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto.
-  auto. auto.
-  simpl in H3. destruct H3; Simplifs.
+  exploit (divu_modu_exists (rs EAX) (rs ECX)). left; congruence.
+  intros (n & d & q & r & B & C & D & E & F).
+  set (rs1 := nextinstr_nf (rs#EDX <- Vzero)).
+  econstructor; split.
+  eapply exec_straight_two with (rs2 := rs1). reflexivity.
+  simpl. change (rs1 EAX) with (rs EAX); rewrite B.
+  change (rs1 ECX) with (rs ECX); rewrite C.
+  rewrite D. reflexivity. auto. auto.
+  split. change (Vint q = v). congruence.
+  simpl; intros. destruct H2. unfold rs1; Simplifs.
 (* mod *)
   apply SAME.
-  specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0.
-  destruct (Val.divs (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction.
-  TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto.
-  auto. auto.
-  simpl in H3. destruct H3; Simplifs.
+  exploit (divs_mods_exists (rs EAX) (rs ECX)). right; congruence.
+  intros (nh & nl & d & q & r & A & B & C & D & E & F).
+  set (rs1 := nextinstr_nf (rs#EDX <- (Vint nh))).
+  econstructor; split.
+  eapply exec_straight_two with (rs2 := rs1). simpl. rewrite A. reflexivity.
+  simpl. change (rs1 EAX) with (rs EAX); rewrite B.
+  change (rs1 ECX) with (rs ECX); rewrite C.
+  rewrite D. reflexivity. auto. auto.
+  split. change (Vint r = v). congruence.
+  simpl; intros. destruct H2. unfold rs1; Simplifs.
 (* modu *)
   apply SAME.
-  specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0.
-  destruct (Val.divu (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction.
-  TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto.
-  auto. auto.
-  simpl in H3. destruct H3; Simplifs.
+  exploit (divu_modu_exists (rs EAX) (rs ECX)). right; congruence.
+  intros (n & d & q & r & B & C & D & E & F).
+  set (rs1 := nextinstr_nf (rs#EDX <- Vzero)).
+  econstructor; split.
+  eapply exec_straight_two with (rs2 := rs1). reflexivity.
+  simpl. change (rs1 EAX) with (rs EAX); rewrite B.
+  change (rs1 ECX) with (rs ECX); rewrite C.
+  rewrite D. reflexivity. auto. auto.
+  split. change (Vint r = v). congruence.
+  simpl; intros. destruct H2. unfold rs1; Simplifs.
 (* shrximm *)
   apply SAME. eapply mk_shrximm_correct; eauto.
 (* lea *)
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 979ac800..4ffb701b 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -421,11 +421,11 @@ module Target(System: SYSTEM):TARGET =
           fprintf oc "	imull	%a\n" ireg r1
       | Pmul_r(r1) ->
           fprintf oc "	mull	%a\n" ireg r1
+      | Pcltd ->
+          fprintf oc "	cltd\n"
       | Pdiv(r1) ->
-          fprintf oc "	xorl	%%edx, %%edx\n";
           fprintf oc "	divl	%a\n" ireg r1
       | Pidiv(r1) ->
-          fprintf oc "	cltd\n";
           fprintf oc "	idivl	%a\n" ireg r1
       | Pand_rr(rd, r1) ->
           fprintf oc "	andl	%a, %a\n" ireg r1 ireg rd