diff options
| -rw-r--r-- | ia32/Asmgen.v | 14 | ||||
| -rw-r--r-- | ia32/Asmgenproof.v | 4 | ||||
| -rw-r--r-- | ia32/Asmgenproof1.v | 44 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 2 |
4 files changed, 53 insertions, 11 deletions
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 70929ff..f53ec81 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -124,13 +124,21 @@ Definition mk_intconv (mk: ireg -> ireg -> instruction) (rd rs: ireg) (k: code) else OK (Pmov_rr EDX rs :: mk rd EDX :: k). +Definition addressing_mentions (addr: addrmode) (r: ireg) : bool := + match addr with Addrmode base displ const => + match base with Some r' => ireg_eq r r' | None => false end + || match displ with Some(r', sc) => ireg_eq r r' | None => false end + end. + Definition mk_smallstore (sto: addrmode -> ireg ->instruction) (addr: addrmode) (rs: ireg) (k: code) := if low_ireg rs then OK (sto addr rs :: k) - else + else if addressing_mentions addr ECX then OK (Plea ECX addr :: Pmov_rr EDX rs :: - sto (Addrmode (Some ECX) None (inl _ Int.zero)) EDX :: k). + sto (Addrmode (Some ECX) None (inl _ Int.zero)) EDX :: k) + else + OK (Pmov_rr ECX rs :: sto addr ECX :: k). (** Accessing slots in the stack frame. *) @@ -424,7 +432,7 @@ Definition transl_store (chunk: memory_chunk) | Mint8unsigned | Mint8signed => do r <- ireg_of src; mk_smallstore Pmovb_mr am r k | Mint16unsigned | Mint16signed => - do r <- ireg_of src; mk_smallstore Pmovw_mr am r k + do r <- ireg_of src; OK(Pmovw_mr am r :: k) | Mint32 => do r <- ireg_of src; OK(Pmov_mr am r :: k) | Mfloat32 => diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index ddf2769..543028f 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -376,7 +376,9 @@ Remark mk_smallstore_label: (forall r addr, is_label lbl (f r addr) = false) -> find_label lbl c = find_label lbl k. Proof. - unfold mk_smallstore; intros. destruct (low_ireg r); monadInv H; simpl; rewrite H0; auto. + unfold mk_smallstore; intros. destruct (low_ireg r). + monadInv H; simpl; rewrite H0; auto. + destruct (addressing_mentions addr ECX); monadInv H; simpl; rewrite H0; auto. Qed. Remark loadind_label: diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 498bb4e..aef03db 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -754,6 +754,18 @@ Qed. (** Smart constructor for small stores *) +Lemma addressing_mentions_correct: + forall a r (rs1 rs2: regset), + (forall (r': ireg), r' <> r -> rs1 r' = rs2 r') -> + addressing_mentions a r = false -> + eval_addrmode ge a rs1 = eval_addrmode ge a rs2. +Proof. + intros until rs2; intro AG. unfold addressing_mentions, eval_addrmode. + destruct a. intros. destruct (orb_false_elim _ _ H). unfold proj_sumbool in *. + decEq. destruct base; auto. apply AG. destruct (ireg_eq r i); congruence. + decEq. destruct ofs as [[r' sc] | ]; auto. rewrite AG; auto. destruct (ireg_eq r r'); congruence. +Qed. + Lemma mk_smallstore_correct: forall chunk sto addr r k c rs1 m1 m2, mk_smallstore sto addr r k = OK c -> @@ -765,12 +777,14 @@ Lemma mk_smallstore_correct: /\ forall r, nontemp_preg r = true -> rs2#r = rs1#r. Proof. unfold mk_smallstore; intros. - remember (low_ireg r) as low. destruct low; monadInv H. + remember (low_ireg r) as low. destruct low. (* low reg *) - econstructor; split. apply exec_straight_one. rewrite H1. + monadInv H. econstructor; split. apply exec_straight_one. rewrite H1. unfold exec_store. rewrite H0. eauto. auto. intros. SOther. (* high reg *) + remember (addressing_mentions addr ECX) as mentions. destruct mentions; monadInv H. +(* ECX is mentioned. *) assert (r <> ECX). red; intros; subst r; discriminate. set (rs2 := nextinstr (rs1#ECX <- (eval_addrmode ge addr rs1))). set (rs3 := nextinstr (rs2#EDX <- (rs1 r))). @@ -788,6 +802,17 @@ Proof. simpl. rewrite Int.add_zero; auto. auto. auto. auto. intros. repeat SOther. unfold rs3. repeat SOther. unfold rs2. repeat SOther. +(* ECX is not mentioned *) + set (rs2 := nextinstr (rs1#ECX <- (rs1 r))). + econstructor; split. + apply exec_straight_two with rs2 m1. + simpl. auto. + rewrite H1. unfold exec_store. + rewrite (addressing_mentions_correct addr ECX rs2 rs1); auto. + change (rs2 ECX) with (rs1 r). rewrite H0. eauto. + intros. unfold rs2. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gso; auto with ppcgen. + auto. auto. + intros. repeat SOther. unfold rs2. repeat SOther. Qed. (** Accessing slots in the stack frame *) @@ -1413,11 +1438,18 @@ Proof. (* int8unsigned *) eapply mk_smallstore_correct; eauto. (* int16signed *) - eapply mk_smallstore_correct; eauto. - intros. simpl. unfold exec_store. - destruct (eval_addrmode ge addr0 rs0); simpl; auto. rewrite Mem.store_signed_unsigned_16; auto. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. + replace (Mem.storev Mint16unsigned m (eval_addrmode ge x rs) (rs x0)) + with (Mem.storev Mint16signed m (eval_addrmode ge x rs) (rs x0)). + rewrite H1. eauto. + destruct (eval_addrmode ge x rs); simpl; auto. rewrite Mem.store_signed_unsigned_16; auto. + auto. + intros. SOther. (* int16unsigned *) - eapply mk_smallstore_correct; eauto. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto. + intros. SOther. (* int32 *) econstructor; split. apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto. diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index f3cb519..7d75048 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -86,7 +86,7 @@ let int8_reg_name = function let int16_reg_name = function | EAX -> "%ax" | EBX -> "%bx" | ECX -> "%cx" | EDX -> "%dx" - | _ -> assert false + | ESI -> "%si" | EDI -> "%di" | EBP -> "%bp" | ESP -> "%sp" let float_reg_name = function | XMM0 -> "%xmm0" | XMM1 -> "%xmm1" | XMM2 -> "%xmm2" | XMM3 -> "%xmm3" |