diff options
| -rw-r--r-- | ia32/Asm.v | 16 | ||||
| -rw-r--r-- | ia32/Asmgen.v | 69 | ||||
| -rw-r--r-- | ia32/Asmgenproof.v | 126 | ||||
| -rw-r--r-- | ia32/Asmgenproof1.v | 134 | ||||
| -rw-r--r-- | ia32/Asmgenretaddr.v | 18 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 47 |
6 files changed, 311 insertions, 99 deletions
@@ -85,9 +85,7 @@ Inductive testcond: Type := | Cond_e | Cond_ne | Cond_b | Cond_be | Cond_ae | Cond_a | Cond_l | Cond_le | Cond_ge | Cond_g - | Cond_p | Cond_np - | Cond_nep (**r synthetic: P or (not Z) *) - | Cond_enp. (**r synthetic: (not P) and Z *) + | Cond_p | Cond_np. (** Instructions. IA32 instructions accept many combinations of registers, memory references and immediate constants as arguments. @@ -178,6 +176,7 @@ Inductive instruction: Type := | Pjmp_s (symb: ident) | Pjmp_r (r: ireg) | Pjcc (c: testcond)(l: label) + | Pjcc2 (c1 c2: testcond)(l: label) | Pjmptbl (r: ireg) (tbl: list label) (**r pseudo *) | Pcall_s (symb: ident) | Pcall_r (r: ireg) @@ -381,6 +380,7 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool := | Vint n => Some (Int.eq n Int.zero) | _ => None end +(* | Cond_nep => match rs PF, rs ZF with | Vint p, Vint z => Some (Int.eq p Int.one || Int.eq z Int.zero) @@ -391,6 +391,7 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool := | Vint p, Vint z => Some (Int.eq p Int.zero && Int.eq z Int.one) | _, _ => None end +*) end. (** The semantics is purely small-step and defined as a function @@ -580,8 +581,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome end | Psetcc c rd => match eval_testcond c rs with - | Some true => Next (nextinstr (rs#ECX <- Vundef #EDX <- Vundef #rd <- Vtrue)) m - | Some false => Next (nextinstr (rs#ECX <- Vundef #EDX <- Vundef #rd <- Vfalse)) m + | Some b => Next (nextinstr (rs#ECX <- Vundef #rd <- (Val.of_bool b))) m | None => Stuck end (** Arithmetic operations over floats *) @@ -612,6 +612,12 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Some false => Next (nextinstr rs) m | None => Stuck end + | Pjcc2 cond1 cond2 lbl => + match eval_testcond cond1 rs, eval_testcond cond2 rs with + | Some true, Some true => goto_label c lbl rs m + | Some _, Some _ => Next (nextinstr rs) m + | _, _ => Stuck + end | Pjmptbl r tbl => match rs#r with | Vint n => diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index c87167b..452f2e7 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -253,32 +253,59 @@ Definition testcond_for_unsigned_comparison (cmp: comparison) := | Cge => Cond_ae end. -Definition testcond_for_condition (cond: condition) : testcond := +Inductive extcond: Type := + | Cond_base (c: testcond) + | Cond_or (c1 c2: testcond) + | Cond_and (c1 c2: testcond). + +Definition testcond_for_condition (cond: condition) : extcond := match cond with - | Ccomp c => testcond_for_signed_comparison c - | Ccompu c => testcond_for_unsigned_comparison c - | Ccompimm c n => testcond_for_signed_comparison c - | Ccompuimm c n => testcond_for_unsigned_comparison c + | Ccomp c => Cond_base(testcond_for_signed_comparison c) + | Ccompu c => Cond_base(testcond_for_unsigned_comparison c) + | Ccompimm c n => Cond_base(testcond_for_signed_comparison c) + | Ccompuimm c n => Cond_base(testcond_for_unsigned_comparison c) | Ccompf c => match c with - | Ceq => Cond_enp - | Cne => Cond_nep - | Clt => Cond_a - | Cle => Cond_ae - | Cgt => Cond_a - | Cge => Cond_ae + | Ceq => Cond_and Cond_np Cond_e + | Cne => Cond_or Cond_p Cond_ne + | Clt => Cond_base Cond_a + | Cle => Cond_base Cond_ae + | Cgt => Cond_base Cond_a + | Cge => Cond_base Cond_ae end | Cnotcompf c => match c with - | Ceq => Cond_nep - | Cne => Cond_enp - | Clt => Cond_be - | Cle => Cond_b - | Cgt => Cond_be - | Cge => Cond_b + | Ceq => Cond_or Cond_p Cond_ne + | Cne => Cond_and Cond_np Cond_e + | Clt => Cond_base Cond_be + | Cle => Cond_base Cond_b + | Cgt => Cond_base Cond_be + | Cge => Cond_base Cond_b end - | Cmaskzero n => Cond_e - | Cmasknotzero n => Cond_ne + | Cmaskzero n => Cond_base Cond_e + | Cmasknotzero n => Cond_base Cond_ne + end. + +(** Acting upon extended conditions. *) + +Definition mk_setcc (cond: extcond) (rd: ireg) (k: code) := + match cond with + | Cond_base c => Psetcc c rd :: k + | Cond_and c1 c2 => + if ireg_eq rd EDX + then Psetcc c1 EDX :: Psetcc c2 ECX :: Pand_rr EDX ECX :: k + else Psetcc c1 EDX :: Psetcc c2 rd :: Pand_rr rd EDX :: k + | Cond_or c1 c2 => + if ireg_eq rd EDX + then Psetcc c1 EDX :: Psetcc c2 ECX :: Por_rr EDX ECX :: k + else Psetcc c1 EDX :: Psetcc c2 rd :: Por_rr rd EDX :: k + end. + +Definition mk_jcc (cond: extcond) (lbl: label) (k: code) := + match cond with + | Cond_base c => Pjcc c lbl :: k + | Cond_and c1 c2 => Pjcc2 c1 c2 lbl :: k + | Cond_or c1 c2 => Pjcc c1 lbl :: Pjcc c2 lbl :: k end. (** Translation of the arithmetic operation [r <- op(args)]. @@ -396,7 +423,7 @@ Definition transl_op do r <- freg_of res; do r1 <- ireg_of a1; OK (Pcvtsi2sd_fr r r1 :: k) | Ocmp c, args => do r <- ireg_of res; - transl_cond c args (Psetcc (testcond_for_condition c) r :: k) + transl_cond c args (mk_setcc (testcond_for_condition c) r k) | _, _ => Error(msg "Asmgen.transl_op") end. @@ -486,7 +513,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mgoto lbl => OK(Pjmp_l lbl :: k) | Mcond cond args lbl => - transl_cond cond args (Pjcc (testcond_for_condition cond) lbl :: k) + transl_cond cond args (mk_jcc (testcond_for_condition cond) lbl k) | Mjumptable arg tbl => do r <- ireg_of arg; OK (Pjmptbl r tbl :: k) | Mreturn => diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index d049737..45ac48d 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -401,6 +401,20 @@ Proof. destruct (preg_of src); inv H; auto. Qed. +Remark mk_setcc_label: + forall xc rd k, + find_label lbl (mk_setcc xc rd k) = find_label lbl k. +Proof. + intros. destruct xc; simpl; auto; destruct (ireg_eq rd EDX); auto. +Qed. + +Remark mk_jcc_label: + forall xc lbl' k, + find_label lbl (mk_jcc xc lbl' k) = find_label lbl k. +Proof. + intros. destruct xc; auto. +Qed. + Ltac ArgsInv := match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -441,7 +455,7 @@ Proof. eapply mk_shift_label; eauto. eapply mk_shrximm_label; eauto. eapply mk_shift_label; eauto. - eapply trans_eq. eapply transl_cond_label; eauto. auto. + eapply trans_eq. eapply transl_cond_label; eauto. apply mk_setcc_label. Qed. Remark transl_load_label: @@ -482,7 +496,7 @@ Opaque loadind. monadInv H; auto. inv H; simpl. destruct (peq lbl l). congruence. auto. monadInv H; auto. - eapply trans_eq. eapply transl_cond_label; eauto. auto. + eapply trans_eq. eapply transl_cond_label; eauto. apply mk_jcc_label. monadInv H; auto. monadInv H; auto. Qed. @@ -624,6 +638,43 @@ Proof. econstructor; eauto. eapply exec_straight_at; eauto. Qed. +Lemma exec_straight_steps_goto: + forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c', + match_stack s -> + Mem.extends m2 m2' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + Mach.find_label lbl f.(fn_code) = Some c' -> + transl_code_at_pc (rs1 PC) fb f (i :: c) ep tf tc -> + edx_preserved ep i = false -> + (forall k c, transl_instr f i ep k = OK c -> + exists jmp, exists k', exists rs2, + exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' + /\ agree ms2 sp rs2 + /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') -> + exists st', + plus step tge (State rs1 m1') E0 st' /\ + match_states (Machsem.State s fb sp c' ms2 m2) st'. +Proof. + intros. inversion H3. subst. monadInv H9. + exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]]. + generalize (functions_transl _ _ _ H7 H8); intro FN. + generalize (transf_function_no_overflow _ _ H8); intro NOOV. + exploit exec_straight_steps_2; eauto. + intros [ofs' [PC2 CT2]]. + exploit find_label_goto_label; eauto. + intros [tc' [rs3 [GOTO [AT' OTH]]]]. + exists (State rs3 m2'); split. + eapply plus_right'. + eapply exec_straight_steps_1; eauto. + econstructor; eauto. + eapply find_instr_tail. eauto. + rewrite C. eexact GOTO. + traceEq. + econstructor; eauto. + apply agree_exten with rs2; auto with ppcgen. + congruence. +Qed. + Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. Proof. induction 1; simpl. congruence. auto. Qed. @@ -1053,22 +1104,40 @@ Lemma exec_Mcond_true_prop: Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. - inv AT. monadInv H5. + left; eapply exec_straight_steps_goto; eauto. + intros. simpl in H2. exploit transl_cond_correct; eauto. intros [rs' [A [B C]]]. - generalize (functions_transl _ _ _ FIND H4); intro FN. - generalize (transf_function_no_overflow _ _ H4); intro NOOV. - exploit exec_straight_steps_2; eauto. - intros [ofs' [PC2 CT2]]. - exploit find_label_goto_label; eauto. - intros [tc' [rs3 [GOTO [AT3 INV3]]]]. - left; exists (State rs3 m'); split. - eapply plus_right'. - eapply exec_straight_steps_1; eauto. - econstructor; eauto. - eapply find_instr_tail. eauto. simpl. rewrite B. eauto. traceEq. - econstructor; eauto. - eapply agree_exten_temps; eauto. intros. rewrite INV3; auto with ppcgen. - congruence. + destruct (testcond_for_condition cond); simpl in *. +(* simple jcc *) + exists (Pjcc c1 lbl); exists k; exists rs'. + split. eexact A. + split. eapply agree_exten_temps; eauto. + simpl. rewrite B. auto. +(* jcc; jcc *) + destruct (eval_testcond c1 rs') as [b1|]_eqn; + destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B. + destruct b1. + (* first jcc jumps *) + exists (Pjcc c1 lbl); exists (Pjcc c2 lbl :: k); exists rs'. + split. eexact A. + split. eapply agree_exten_temps; eauto. + simpl. rewrite Heqo. auto. + (* second jcc jumps *) + exists (Pjcc c2 lbl); exists k; exists (nextinstr rs'). + split. eapply exec_straight_trans. eexact A. + eapply exec_straight_one. simpl. rewrite Heqo. auto. auto. + split. eapply agree_exten_temps; eauto. + intros. rewrite nextinstr_inv; auto with ppcgen. + simpl. rewrite eval_testcond_nextinstr. rewrite Heqo0. + destruct b2; auto || discriminate. +(* jcc2 *) + destruct (eval_testcond c1 rs') as [b1|]_eqn; + destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B. + destruct (andb_prop _ _ H4). subst. + exists (Pjcc2 c1 c2 lbl); exists k; exists rs'. + split. eexact A. + split. eapply agree_exten_temps; eauto. + simpl. rewrite Heqo; rewrite Heqo0; auto. Qed. Lemma exec_Mcond_false_prop: @@ -1083,11 +1152,34 @@ Proof. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. left; eapply exec_straight_steps; eauto. intros. simpl in H0. exploit transl_cond_correct; eauto. intros [rs' [A [B C]]]. + destruct (testcond_for_condition cond); simpl in *. +(* simple jcc *) econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl. rewrite B. eauto. auto. split. apply agree_nextinstr. eapply agree_exten_temps; eauto. simpl; congruence. +(* jcc ; jcc *) + destruct (eval_testcond c1 rs') as [b1|]_eqn; + destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B. + destruct (orb_false_elim _ _ H2); subst. + econstructor; split. + eapply exec_straight_trans. eexact A. + eapply exec_straight_two. simpl. rewrite Heqo. eauto. auto. + simpl. rewrite eval_testcond_nextinstr. rewrite Heqo0. eauto. auto. auto. + split. apply agree_nextinstr. apply agree_nextinstr. eapply agree_exten_temps; eauto. + simpl; congruence. +(* jcc2 *) + destruct (eval_testcond c1 rs') as [b1|]_eqn; + destruct (eval_testcond c2 rs') as [b2|]_eqn; inv B. + exists (nextinstr rs'); split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. + rewrite Heqo; rewrite Heqo0. + destruct b1. simpl in *. subst b2. auto. auto. + auto. + split. apply agree_nextinstr. eapply agree_exten_temps; eauto. + rewrite H2; congruence. Qed. Lemma exec_Mjumptable_prop: diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index b3e7aaa..3a91ac5 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -1147,6 +1147,22 @@ Proof. intros. repeat SOther. Qed. +Definition eval_extcond (xc: extcond) (rs: regset) : option bool := + match xc with + | Cond_base c => + eval_testcond c rs + | Cond_and c1 c2 => + match eval_testcond c1 rs, eval_testcond c2 rs with + | Some b1, Some b2 => Some (b1 && b2) + | _, _ => None + end + | Cond_or c1 c2 => + match eval_testcond c1 rs, eval_testcond c2 rs with + | Some b1, Some b2 => Some (b1 || b2) + | _, _ => None + end + end. + Definition swap_floats (c: comparison) (n1 n2: float) : float := match c with | Clt | Cle => n2 @@ -1155,9 +1171,9 @@ Definition swap_floats (c: comparison) (n1 n2: float) : float := Lemma testcond_for_float_comparison_correct: forall c n1 n2 rs, - eval_testcond (testcond_for_condition (Ccompf c)) - (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2)) - (Vfloat (swap_floats c n2 n1)) rs)) = + eval_extcond (testcond_for_condition (Ccompf c)) + (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2)) + (Vfloat (swap_floats c n2 n1)) rs)) = Some(Float.cmp c n1 n2). Proof. intros. @@ -1165,7 +1181,7 @@ Proof. set (rs' := nextinstr (compare_floats (Vfloat (swap_floats c n1 n2)) (Vfloat (swap_floats c n2 n1)) rs)). intros [A [B [C D]]]. - unfold eval_testcond. rewrite A; rewrite B; rewrite C. + unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C. destruct c; simpl. (* eq *) rewrite Float.cmp_ne_eq. @@ -1203,9 +1219,9 @@ Qed. Lemma testcond_for_neg_float_comparison_correct: forall c n1 n2 rs, - eval_testcond (testcond_for_condition (Cnotcompf c)) - (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2)) - (Vfloat (swap_floats c n2 n1)) rs)) = + eval_extcond (testcond_for_condition (Cnotcompf c)) + (nextinstr (compare_floats (Vfloat (swap_floats c n1 n2)) + (Vfloat (swap_floats c n2 n1)) rs)) = Some(negb(Float.cmp c n1 n2)). Proof. intros. @@ -1213,7 +1229,7 @@ Proof. set (rs' := nextinstr (compare_floats (Vfloat (swap_floats c n1 n2)) (Vfloat (swap_floats c n2 n1)) rs)). intros [A [B [C D]]]. - unfold eval_testcond. rewrite A; rewrite B; rewrite C. + unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C. destruct c; simpl. (* eq *) rewrite Float.cmp_ne_eq. @@ -1255,7 +1271,7 @@ Lemma transl_cond_correct: eval_condition cond (map rs (map preg_of args)) m = Some b -> exists rs', exec_straight c rs m k rs' m - /\ eval_testcond (testcond_for_condition cond) rs' = Some b + /\ eval_extcond (testcond_for_condition cond) rs' = Some b /\ forall r, nontemp_preg r = true -> rs'#r = rs r. Proof. unfold transl_cond; intros. @@ -1264,17 +1280,17 @@ Proof. simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0. rewrite (ireg_of_eq _ _ EQ1) in H0. econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. simpl in H0. FuncInv. - subst b. apply testcond_for_signed_comparison_correct_ii. + subst b. simpl. apply testcond_for_signed_comparison_correct_ii. intros. unfold compare_ints. repeat SOther. (* compu *) simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0. rewrite (ireg_of_eq _ _ EQ1) in H0. econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. simpl in H0. FuncInv. - subst b. apply testcond_for_unsigned_comparison_correct_ii. - apply testcond_for_unsigned_comparison_correct_ip; auto. - apply testcond_for_unsigned_comparison_correct_pi; auto. - eapply testcond_for_unsigned_comparison_correct_pp; eauto. + subst b. simpl; apply testcond_for_unsigned_comparison_correct_ii. + simpl; apply testcond_for_unsigned_comparison_correct_ip; auto. + simpl; apply testcond_for_unsigned_comparison_correct_pi; auto. + simpl; eapply testcond_for_unsigned_comparison_correct_pp; eauto. intros. unfold compare_ints. repeat SOther. (* compimm *) simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0. @@ -1284,14 +1300,14 @@ Proof. simpl in H0. FuncInv. simpl. rewrite Int.and_idem. auto. auto. apply exec_straight_one; auto. split. simpl in H0. FuncInv. - subst b. apply testcond_for_signed_comparison_correct_ii. + subst b. simpl; apply testcond_for_signed_comparison_correct_ii. intros. unfold compare_ints. repeat SOther. (* compuimm *) simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0. econstructor. split. apply exec_straight_one. simpl; eauto. auto. split. simpl in H0. FuncInv. - subst b. apply testcond_for_unsigned_comparison_correct_ii. - apply testcond_for_unsigned_comparison_correct_pi; auto. + subst b. simpl; apply testcond_for_unsigned_comparison_correct_ii. + simpl; apply testcond_for_unsigned_comparison_correct_pi; auto. intros. unfold compare_ints. repeat SOther. (* compf *) simpl map in H0. rewrite (freg_of_eq _ _ EQ) in H0. rewrite (freg_of_eq _ _ EQ1) in H0. @@ -1327,6 +1343,78 @@ Proof. intros. unfold compare_ints. repeat SOther. Qed. +Remark eval_testcond_nextinstr: + forall c rs, eval_testcond c (nextinstr rs) = eval_testcond c rs. +Proof. + intros. unfold eval_testcond. repeat rewrite nextinstr_inv; auto with ppcgen. +Qed. + +Remark eval_testcond_set_ireg: + forall c rs r v, eval_testcond c (rs#(IR r) <- v) = eval_testcond c rs. +Proof. + intros. unfold eval_testcond. repeat rewrite Pregmap.gso; auto with ppcgen. +Qed. + +Lemma mk_setcc_correct: + forall cond rd k rs1 m b, + eval_extcond cond rs1 = Some b -> + exists rs2, + exec_straight (mk_setcc cond rd k) rs1 m k rs2 m + /\ rs2#rd = Val.of_bool b + /\ forall r, nontemp_preg r = true -> r <> rd -> rs2#r = rs1#r. +Proof. + intros. destruct cond; simpl in *. +(* base *) + econstructor; split. + apply exec_straight_one. simpl; rewrite H. eauto. auto. + split. repeat SRes. + intros. repeat SOther. +(* or *) + destruct (eval_testcond c1 rs1) as [b1|]_eqn; + destruct (eval_testcond c2 rs1) as [b2|]_eqn; inv H. + assert (D: Val.or (Val.of_bool b1) (Val.of_bool b2) = Val.of_bool (b1 || b2)). + destruct b1; destruct b2; auto. + destruct (ireg_eq rd EDX). + subst rd. econstructor; split. + eapply exec_straight_three. + simpl; rewrite Heqo; eauto. + simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. rewrite Heqo0. eauto. + simpl. eauto. + auto. auto. auto. + split. SRes. + intros. repeat SOther. + econstructor; split. + eapply exec_straight_three. + simpl; rewrite Heqo; eauto. + simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. rewrite Heqo0. eauto. + simpl. eauto. + auto. auto. auto. + split. repeat SRes. rewrite <- D. rewrite Val.or_commut. decEq; repeat SRes. + intros. repeat SOther. +(* and *) + destruct (eval_testcond c1 rs1) as [b1|]_eqn; + destruct (eval_testcond c2 rs1) as [b2|]_eqn; inv H. + assert (D: Val.and (Val.of_bool b1) (Val.of_bool b2) = Val.of_bool (b1 && b2)). + destruct b1; destruct b2; auto. + destruct (ireg_eq rd EDX). + subst rd. econstructor; split. + eapply exec_straight_three. + simpl; rewrite Heqo; eauto. + simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. rewrite Heqo0. eauto. + simpl. eauto. + auto. auto. auto. + split. SRes. + intros. repeat SOther. + econstructor; split. + eapply exec_straight_three. + simpl; rewrite Heqo; eauto. + simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. rewrite Heqo0. eauto. + simpl. eauto. + auto. auto. auto. + split. repeat SRes. rewrite <- D. rewrite Val.and_commut. decEq; repeat SRes. + intros. repeat SOther. +Qed. + (** Translation of arithmetic operations. *) (* @@ -1367,8 +1455,6 @@ Ltac TranslOp := [ apply exec_straight_one; [ simpl; eauto | auto ] | split; [ repeat SRes | intros; repeat SOther ]]. -(* Move elsewhere *) - Lemma transl_op_correct: forall op args res k c (rs: regset) m v, transl_op op args res k = OK c -> @@ -1425,11 +1511,11 @@ Proof. remember (eval_condition c0 rs ## (preg_of ## args) m) as ob. destruct ob; inv EV. rewrite (eval_condition_weaken _ _ _ (sym_equal Heqob)). exploit transl_cond_correct; eauto. intros [rs2 [P [Q R]]]. - exists (nextinstr (rs2#ECX <- Vundef #EDX <- Vundef #x <- v)). - split. eapply exec_straight_trans. eauto. - apply exec_straight_one. simpl. rewrite Q. destruct b; inv H0; auto. auto. - split. repeat SRes. destruct b; inv H0; auto. - intros. repeat SOther. + exploit mk_setcc_correct; eauto. intros [rs3 [S [T U]]]. + exists rs3. + split. eapply exec_straight_trans. eexact P. eexact S. + split. auto. + intros. transitivity (rs2 r); auto. Qed. (** Translation of memory loads. *) diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v index 674a73e..e0787d7 100644 --- a/ia32/Asmgenretaddr.v +++ b/ia32/Asmgenretaddr.v @@ -173,8 +173,24 @@ Proof. unfold storeind; intros. destruct ty; IsTail. destruct (preg_of src); IsTail. Qed. +Lemma mk_setcc_tail: + forall cond rd k, is_tail k (mk_setcc cond rd k). +Proof. + unfold mk_setcc; intros. destruct cond. + IsTail. + destruct (ireg_eq rd EDX); IsTail. + destruct (ireg_eq rd EDX); IsTail. +Qed. + +Lemma mk_jcc_tail: + forall cond lbl k, is_tail k (mk_jcc cond lbl k). +Proof. + unfold mk_jcc; intros. destruct cond; IsTail. +Qed. + Hint Resolve mk_mov_tail mk_shift_tail mk_div_tail mk_mod_tail mk_shrximm_tail - mk_intconv_tail mk_smallstore_tail loadind_tail storeind_tail : ppcretaddr. + mk_intconv_tail mk_smallstore_tail loadind_tail storeind_tail + mk_setcc_tail mk_jcc_tail : ppcretaddr. Lemma transl_cond_tail: forall cond args k c, transl_cond cond args k = OK c -> is_tail k c. diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 6f02a8a..a6369c4 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -132,7 +132,12 @@ let name_of_condition = function | Cond_b -> "b" | Cond_be -> "be" | Cond_ae -> "ae" | Cond_a -> "a" | Cond_l -> "l" | Cond_le -> "le" | Cond_ge -> "ge" | Cond_g -> "g" | Cond_p -> "p" | Cond_np -> "np" - | Cond_nep | Cond_enp -> assert false (* treated specially *) + +let name_of_neg_condition = function + | Cond_e -> "ne" | Cond_ne -> "e" + | Cond_b -> "ae" | Cond_be -> "a" | Cond_ae -> "b" | Cond_a -> "be" + | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le" + | Cond_p -> "np" | Cond_np -> "p" let section oc name = fprintf oc " %s\n" name @@ -218,14 +223,11 @@ let need_masks = ref false (* Built-in functions *) -(* Built-ins. They come in three flavors: +(* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; - inlined by the compiler: take their arguments in arbitrary - registers; preserve all registers except ECX, EDX, XMM6 and XMM7 - - inlined while printing asm code; take their arguments in - locations dictated by the calling conventions; preserve - callee-save regs only. *) + registers; preserve all registers except ECX, EDX, XMM6 and XMM7. *) (* Handling of annotations *) @@ -588,21 +590,9 @@ let print_instruction oc = function | Ptest_ri(r1, n) -> fprintf oc " testl $%a, %a\n" coqint n ireg r1 | Pcmov(c, rd, r1) -> - assert (c <> Cond_nep && c <> Cond_enp); fprintf oc " cmov%s %a, %a\n" (name_of_condition c) ireg r1 ireg rd | Psetcc(c, rd) -> - begin match c with - | Cond_nep -> - fprintf oc " setne %%cl\n"; - fprintf oc " setp %%dl\n"; - fprintf oc " orb %%dl, %%cl\n" - | Cond_enp -> - fprintf oc " sete %%cl\n"; - fprintf oc " setnp %%dl\n"; - fprintf oc " andb %%dl, %%cl\n" - | _ -> - fprintf oc " set%s %%cl\n" (name_of_condition c) - end; + fprintf oc " set%s %%cl\n" (name_of_condition c); fprintf oc " movzbl %%cl, %a\n" ireg rd (** Arithmetic operations over floats *) | Paddd_ff(rd, r1) -> @@ -630,18 +620,13 @@ let print_instruction oc = function fprintf oc " jmp *%a\n" ireg r | Pjcc(c, l) -> let l = transl_label l in - begin match c with - | Cond_nep -> - fprintf oc " jp %a\n" label l; - fprintf oc " jne %a\n" label l - | Cond_enp -> - let l' = new_label() in - fprintf oc " jp %a\n" label l'; - fprintf oc " je %a\n" label l; - fprintf oc "%a:\n" label l' - | _ -> - fprintf oc " j%s %a\n" (name_of_condition c) label l - end + fprintf oc " j%s %a\n" (name_of_condition c) label l + | Pjcc2(c1, c2, l) -> + let l = transl_label l in + let l' = new_label() in + fprintf oc " j%s %a\n" (name_of_neg_condition c1) label l'; + fprintf oc " j%s %a\n" (name_of_condition c2) label l; + fprintf oc "%a:\n" label l' | Pjmptbl(r, tbl) -> let l = new_label() in fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r; |