diff options
-rw-r--r-- | ia32/Asm.v | 25 | ||||
-rw-r--r-- | ia32/Asmgen.v | 8 | ||||
-rw-r--r-- | ia32/Asmgenproof1.v | 108 | ||||
-rw-r--r-- | ia32/TargetPrinter.ml | 4 | ||||
-rw-r--r-- | lib/Integers.v | 92 |
5 files changed, 187 insertions, 50 deletions
@@ -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 diff --git a/lib/Integers.v b/lib/Integers.v index 316dfb52..16c95e01 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -403,6 +403,18 @@ Definition is_false (x: int) : Prop := x = zero. Definition is_true (x: int) : Prop := x <> zero. Definition notbool (x: int) : int := if eq x zero then one else zero. +(** x86-style extended division and modulus *) + +Definition divmodu2 (nhi nlo: int) (d: int) : option (int * int) := + if eq_dec d zero then None else + (let (q, r) := Z.div_eucl (unsigned nhi * modulus + unsigned nlo) (unsigned d) in + if zle q max_unsigned then Some(repr q, repr r) else None). + +Definition divmods2 (nhi nlo: int) (d: int) : option (int * int) := + if eq_dec d zero then None else + (let (q, r) := Z.quotrem (signed nhi * modulus + unsigned nlo) (signed d) in + if zle min_signed q && zle q max_signed then Some(repr q, repr r) else None). + (** * Properties of integers and integer arithmetic *) (** ** Properties of [modulus], [max_unsigned], etc. *) @@ -1193,6 +1205,86 @@ Proof. rewrite <- neg_mul_distr_l. rewrite mul_mone. rewrite neg_involutive. apply sub_idem. Qed. +Theorem divmodu2_divu_modu: + forall n d, + d <> zero -> divmodu2 zero n d = Some (divu n d, modu n d). +Proof. + unfold divmodu2, divu, modu; intros. + rewrite dec_eq_false by auto. + set (N := unsigned zero * modulus + unsigned n). + assert (E1: unsigned n = N) by (unfold N; rewrite unsigned_zero; ring). rewrite ! E1. + set (D := unsigned d). + set (Q := N / D); set (R := N mod D). + assert (E2: Z.div_eucl N D = (Q, R)). + { unfold Q, R, Z.div, Z.modulo. destruct (Z.div_eucl N D); auto. } + rewrite E2. rewrite zle_true. auto. + assert (unsigned d <> 0). + { red; intros. elim H. rewrite <- (repr_unsigned d). rewrite H0; auto. } + assert (0 < D). + { unfold D. generalize (unsigned_range d); intros. omega. } + assert (0 <= Q <= max_unsigned). + { unfold Q. apply Zdiv_interval_2. + rewrite <- E1; apply unsigned_range_2. + omega. unfold max_unsigned; generalize modulus_pos; omega. omega. } + omega. +Qed. + +Lemma unsigned_signed: + forall n, unsigned n = if lt n zero then signed n + modulus else signed n. +Proof. + intros. unfold lt. rewrite signed_zero. unfold signed. + generalize (unsigned_range n). rewrite half_modulus_modulus. intros. + destruct (zlt (unsigned n) half_modulus). +- rewrite zlt_false by omega. auto. +- rewrite zlt_true by omega. ring. +Qed. + +Theorem divmods2_divs_mods: + forall n d, + d <> zero -> n <> repr min_signed \/ d <> mone -> + divmods2 (if lt n zero then mone else zero) n d = Some (divs n d, mods n d). +Proof. + unfold divmods2, divs, mods; intros. + rewrite dec_eq_false by auto. + set (N := signed (if lt n zero then mone else zero) * modulus + unsigned n). + set (D := signed d). + assert (D <> 0). + { unfold D; red; intros. elim H. rewrite <- (repr_signed d). rewrite H1; auto. } + assert (N = signed n). + { unfold N. rewrite unsigned_signed. destruct (lt n zero). + rewrite signed_mone. ring. + rewrite signed_zero. ring. } + set (Q := Z.quot N D); set (R := Z.rem N D). + assert (E2: Z.quotrem N D = (Q, R)). + { unfold Q, R, Z.quot, Z.rem. destruct (Z.quotrem N D); auto. } + rewrite E2. + assert (min_signed <= N <= max_signed) by (rewrite H2; apply signed_range). + assert (min_signed <= Q <= max_signed). + { unfold Q. destruct (zeq D 1); [ | destruct (zeq D (-1))]. + - (* D = 1 *) + rewrite e. rewrite Z.quot_1_r; auto. + - (* D = -1 *) + rewrite e. change (-1) with (Z.opp 1). rewrite Z.quot_opp_r by omega. + rewrite Z.quot_1_r. + assert (N <> min_signed). + { red; intros; destruct H0. + + elim H0. rewrite <- (repr_signed n). rewrite <- H2. rewrite H4. auto. + + elim H0. rewrite <- (repr_signed d). unfold D in e; rewrite e; auto. } + unfold min_signed, max_signed in *. omega. + - (* |D| > 1 *) + assert (Z.abs (Z.quot N D) < half_modulus). + { rewrite <- Z.quot_abs by omega. apply Zquot_lt_upper_bound. + xomega. xomega. + apply Zle_lt_trans with (half_modulus * 1). + rewrite Z.mul_1_r. unfold min_signed, max_signed in H3; xomega. + apply Zmult_lt_compat_l. generalize half_modulus_pos; omega. xomega. } + rewrite Z.abs_lt in H4. + unfold min_signed, max_signed; omega. + } + unfold proj_sumbool; rewrite ! zle_true by omega; simpl. + unfold Q, R; rewrite H2; auto. +Qed. + (** ** Bit-level properties *) (** ** Properties of bit-level operations over [Z] *) |