From 99554c986d023d00192eb3d1fbfe1c0cc138596e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 18 Sep 2016 10:29:11 +0200 Subject: 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. --- ia32/Asm.v | 25 ++++++++---- ia32/Asmgen.v | 8 ++-- ia32/Asmgenproof1.v | 108 +++++++++++++++++++++++++++++++++----------------- ia32/TargetPrinter.ml | 4 +- 4 files changed, 95 insertions(+), 50 deletions(-) (limited to 'ia32') 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 -- cgit