diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-19 18:40:04 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-19 18:40:04 +0100 |
| commit | 91a07b5ef9935780942a53108ac80ef354a76248 (patch) | |
| tree | 3aeed2d658b7fc897b7ab049b9c3d57cb8c2200d /aarch64/Asmblockgenproof1.v | |
| parent | 3d1aea4821fb8e12d4cc99cb853befec878645da (diff) | |
| download | compcert-kvx-91a07b5ef9935780942a53108ac80ef354a76248.tar.gz compcert-kvx-91a07b5ef9935780942a53108ac80ef354a76248.zip | |
Cleanup
Diffstat (limited to 'aarch64/Asmblockgenproof1.v')
| -rw-r--r-- | aarch64/Asmblockgenproof1.v | 1740 |
1 files changed, 870 insertions, 870 deletions
diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v index dd7803cd..e26c24e7 100644 --- a/aarch64/Asmblockgenproof1.v +++ b/aarch64/Asmblockgenproof1.v @@ -137,10 +137,10 @@ Lemma decompose_int_wf: Proof. Local Opaque Zzero_ext. induction N as [ | N]; simpl; intros. -- constructor. -- set (frag := Zzero_ext 16 (Z.shiftr n p)) in *. destruct (Z.eqb frag 0). -+ apply IHN. omega. -+ econstructor. reflexivity. omega. apply IHN; omega. + - constructor. + - set (frag := Zzero_ext 16 (Z.shiftr n p)) in *. destruct (Z.eqb frag 0). + + apply IHN. omega. + + econstructor. reflexivity. omega. apply IHN; omega. Qed. Fixpoint recompose_int (accu: Z) (l: list (Z * Z)) : Z := @@ -158,35 +158,35 @@ Lemma decompose_int_correct: if zlt i p then Z.testbit accu i else Z.testbit n i). Proof. induction N as [ | N]; intros until accu; intros PPOS ABOVE i RANGE. -- simpl. rewrite zlt_true; auto. xomega. -- rewrite inj_S in RANGE. simpl. - set (frag := Zzero_ext 16 (Z.shiftr n p)). - assert (FRAG: forall i, p <= i < p + 16 -> Z.testbit n i = Z.testbit frag (i - p)). - { unfold frag; intros. rewrite Zzero_ext_spec by omega. rewrite zlt_true by omega. - rewrite Z.shiftr_spec by omega. f_equal; omega. } - destruct (Z.eqb_spec frag 0). -+ rewrite IHN. -* destruct (zlt i p). rewrite zlt_true by omega. auto. - destruct (zlt i (p + 16)); auto. - rewrite ABOVE by omega. rewrite FRAG by omega. rewrite e, Z.testbit_0_l. auto. -* omega. -* intros; apply ABOVE; omega. -* xomega. -+ simpl. rewrite IHN. -* destruct (zlt i (p + 16)). -** rewrite Zinsert_spec by omega. unfold proj_sumbool. - rewrite zlt_true by omega. - destruct (zlt i p). - rewrite zle_false by omega. auto. - rewrite zle_true by omega. simpl. symmetry; apply FRAG; omega. -** rewrite Z.ldiff_spec, Z.shiftl_spec by omega. - change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by omega. - rewrite zlt_false by omega. rewrite zlt_false by omega. apply andb_true_r. -* omega. -* intros. rewrite Zinsert_spec by omega. unfold proj_sumbool. - rewrite zle_true by omega. rewrite zlt_false by omega. simpl. - apply ABOVE. omega. -* xomega. + - simpl. rewrite zlt_true; auto. xomega. + - rewrite inj_S in RANGE. simpl. + set (frag := Zzero_ext 16 (Z.shiftr n p)). + assert (FRAG: forall i, p <= i < p + 16 -> Z.testbit n i = Z.testbit frag (i - p)). + { unfold frag; intros. rewrite Zzero_ext_spec by omega. rewrite zlt_true by omega. + rewrite Z.shiftr_spec by omega. f_equal; omega. } + destruct (Z.eqb_spec frag 0). + + rewrite IHN. + * destruct (zlt i p). rewrite zlt_true by omega. auto. + destruct (zlt i (p + 16)); auto. + rewrite ABOVE by omega. rewrite FRAG by omega. rewrite e, Z.testbit_0_l. auto. + * omega. + * intros; apply ABOVE; omega. + * xomega. + + simpl. rewrite IHN. + * destruct (zlt i (p + 16)). + ** rewrite Zinsert_spec by omega. unfold proj_sumbool. + rewrite zlt_true by omega. + destruct (zlt i p). + rewrite zle_false by omega. auto. + rewrite zle_true by omega. simpl. symmetry; apply FRAG; omega. + ** rewrite Z.ldiff_spec, Z.shiftl_spec by omega. + change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by omega. + rewrite zlt_false by omega. rewrite zlt_false by omega. apply andb_true_r. + * omega. + * intros. rewrite Zinsert_spec by omega. unfold proj_sumbool. + rewrite zle_true by omega. rewrite zlt_false by omega. simpl. + apply ABOVE. omega. + * xomega. Qed. Corollary decompose_int_eqmod: forall N n, @@ -238,10 +238,10 @@ Proof. intros. apply equal_same_bits; intros. rewrite Zinsert_spec by omega. unfold proj_sumbool. destruct (zlt i p); [rewrite zle_false by omega|rewrite zle_true by omega]; simpl. -- rewrite Z.testbit_0_l, Z.shiftl_spec_low by auto. auto. -- rewrite Z.shiftl_spec by omega. - destruct (zlt i (p + l)); auto. - rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by omega. auto. + - rewrite Z.testbit_0_l, Z.shiftl_spec_low by auto. auto. + - rewrite Z.shiftl_spec by omega. + destruct (zlt i (p + l)); auto. + rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by omega. auto. Qed. Lemma recompose_int_negated: @@ -249,15 +249,15 @@ Lemma recompose_int_negated: forall accu, recompose_int (Z.lnot accu) (negate_decomposition l) = Z.lnot (recompose_int accu l). Proof. induction 1; intros accu; simpl. -- auto. -- rewrite <- IHwf_decomposition. f_equal. apply equal_same_bits; intros. - rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by omega. - unfold proj_sumbool. - destruct (zle p i); simpl; auto. - destruct (zlt i (p + 16)); simpl; auto. - change 65535 with (two_p 16 - 1). - rewrite Ztestbit_two_p_m1 by omega. rewrite zlt_true by omega. - apply xorb_true_r. + - auto. + - rewrite <- IHwf_decomposition. f_equal. apply equal_same_bits; intros. + rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by omega. + unfold proj_sumbool. + destruct (zle p i); simpl; auto. + destruct (zlt i (p + 16)); simpl; auto. + change 65535 with (two_p 16 - 1). + rewrite Ztestbit_two_p_m1 by omega. rewrite zlt_true by omega. + apply xorb_true_r. Qed. Lemma exec_loadimm_k_w: @@ -271,16 +271,16 @@ Lemma exec_loadimm_k_w: /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. induction 1; intros rs accu ACCU; simpl. -- exists rs; split. apply exec_straight_opt_refl. auto. -- destruct (IHwf_decomposition - ((rs#rd <- (insert_in_int rs#rd n p 16))) - (Zinsert accu n p 16)) - as (rs' & P & Q & R). - Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr. - apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. - exists rs'; split. - eapply exec_straight_opt_step_opt. simpl. eauto. auto. - split. exact Q. intros; Simpl. rewrite R by auto. Simpl. + - exists rs; split. apply exec_straight_opt_refl. auto. + - destruct (IHwf_decomposition + ((rs#rd <- (insert_in_int rs#rd n p 16))) + (Zinsert accu n p 16)) + as (rs' & P & Q & R). + Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr. + apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + exists rs'; split. + eapply exec_straight_opt_step_opt. simpl. eauto. auto. + split. exact Q. intros; Simpl. rewrite R by auto. Simpl. Qed. Lemma exec_loadimm_z_w: @@ -292,19 +292,19 @@ Lemma exec_loadimm_z_w: /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. unfold loadimm_z; destruct 1. -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -- set (accu0 := Zinsert 0 n p 16). - set (rs1 := rs#rd <- (Vint (Int.repr accu0))). - destruct (exec_loadimm_k_w rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto. - unfold rs1; Simpl. - exists rs2; split. - eapply exec_straight_opt_step; eauto. - simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega. - split. exact Q. - intros. rewrite R by auto. unfold rs1; Simpl. + - econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. + - set (accu0 := Zinsert 0 n p 16). + set (rs1 := rs#rd <- (Vint (Int.repr accu0))). + destruct (exec_loadimm_k_w rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto. + unfold rs1; Simpl. + exists rs2; split. + eapply exec_straight_opt_step; eauto. + simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega. + split. exact Q. + intros. rewrite R by auto. unfold rs1; Simpl. Qed. Lemma exec_loadimm_n_w: @@ -316,22 +316,22 @@ Lemma exec_loadimm_n_w: /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. unfold loadimm_n; destruct 1. -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -- set (accu0 := Z.lnot (Zinsert 0 n p 16)). - set (rs1 := rs#rd <- (Vint (Int.repr accu0))). - destruct (exec_loadimm_k_w rd k m (negate_decomposition l) - (negate_decomposition_wf l H1) - rs1 accu0) as (rs2 & P & Q & R). - unfold rs1; Simpl. - exists rs2; split. - eapply exec_straight_opt_step; eauto. - simpl. unfold rs1. do 5 f_equal. - unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega. - split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q. - intros. rewrite R by auto. unfold rs1; Simpl. + - econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. + - set (accu0 := Z.lnot (Zinsert 0 n p 16)). + set (rs1 := rs#rd <- (Vint (Int.repr accu0))). + destruct (exec_loadimm_k_w rd k m (negate_decomposition l) + (negate_decomposition_wf l H1) + rs1 accu0) as (rs2 & P & Q & R). + unfold rs1; Simpl. + exists rs2; split. + eapply exec_straight_opt_step; eauto. + simpl. unfold rs1. do 5 f_equal. + unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega. + split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q. + intros. rewrite R by auto. unfold rs1; Simpl. Qed. Lemma exec_loadimm32: @@ -343,23 +343,23 @@ Lemma exec_loadimm32: Proof. unfold loadimm32, loadimm; intros. destruct (is_logical_imm32 n). -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. rewrite Int.repr_unsigned, Int.or_zero_l; auto. - intros; Simpl. -- set (dz := decompose_int 2%nat (Int.unsigned n) 0). - set (dn := decompose_int 2%nat (Z.lnot (Int.unsigned n)) 0). - assert (A: Int.repr (recompose_int 0 dz) = n). - { transitivity (Int.repr (Int.unsigned n)). - apply Int.eqm_samerepr. apply decompose_int_eqmod. - apply Int.repr_unsigned. } - assert (B: Int.repr (Z.lnot (recompose_int 0 dn)) = n). - { transitivity (Int.repr (Int.unsigned n)). - apply Int.eqm_samerepr. apply decompose_notint_eqmod. - apply Int.repr_unsigned. } - destruct Nat.leb. -+ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega. -+ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega. + - econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. rewrite Int.repr_unsigned, Int.or_zero_l; auto. + intros; Simpl. + - set (dz := decompose_int 2%nat (Int.unsigned n) 0). + set (dn := decompose_int 2%nat (Z.lnot (Int.unsigned n)) 0). + assert (A: Int.repr (recompose_int 0 dz) = n). + { transitivity (Int.repr (Int.unsigned n)). + apply Int.eqm_samerepr. apply decompose_int_eqmod. + apply Int.repr_unsigned. } + assert (B: Int.repr (Z.lnot (recompose_int 0 dn)) = n). + { transitivity (Int.repr (Int.unsigned n)). + apply Int.eqm_samerepr. apply decompose_notint_eqmod. + apply Int.repr_unsigned. } + destruct Nat.leb. + + rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega. + + rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega. Qed. Lemma exec_loadimm_k_x: @@ -373,16 +373,16 @@ Lemma exec_loadimm_k_x: /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. induction 1; intros rs accu ACCU; simpl. -- exists rs; split. apply exec_straight_opt_refl. auto. -- destruct (IHwf_decomposition - (rs#rd <- (insert_in_long rs#rd n p 16)) - (Zinsert accu n p 16)) - as (rs' & P & Q & R). - Simpl. rewrite ACCU. simpl. f_equal. apply Int64.eqm_samerepr. - apply Zinsert_eqmod. auto. omega. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr. - exists rs'; split. - eapply exec_straight_opt_step_opt. simpl; eauto. auto. - split. exact Q. intros; Simpl. rewrite R by auto. Simpl. + - exists rs; split. apply exec_straight_opt_refl. auto. + - destruct (IHwf_decomposition + (rs#rd <- (insert_in_long rs#rd n p 16)) + (Zinsert accu n p 16)) + as (rs' & P & Q & R). + Simpl. rewrite ACCU. simpl. f_equal. apply Int64.eqm_samerepr. + apply Zinsert_eqmod. auto. omega. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr. + exists rs'; split. + eapply exec_straight_opt_step_opt. simpl; eauto. auto. + split. exact Q. intros; Simpl. rewrite R by auto. Simpl. Qed. Lemma exec_loadimm_z_x: @@ -394,19 +394,19 @@ Lemma exec_loadimm_z_x: /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. unfold loadimm_z; destruct 1. -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -- set (accu0 := Zinsert 0 n p 16). - set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))). - destruct (exec_loadimm_k_x rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto. - unfold rs1; Simpl. - exists rs2; split. - eapply exec_straight_opt_step; eauto. - simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega. - split. exact Q. - intros. rewrite R by auto. unfold rs1; Simpl. + - econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. + - set (accu0 := Zinsert 0 n p 16). + set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))). + destruct (exec_loadimm_k_x rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto. + unfold rs1; Simpl. + exists rs2; split. + eapply exec_straight_opt_step; eauto. + simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega. + split. exact Q. + intros. rewrite R by auto. unfold rs1; Simpl. Qed. Lemma exec_loadimm_n_x: @@ -418,22 +418,22 @@ Lemma exec_loadimm_n_x: /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. unfold loadimm_n; destruct 1. -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -- set (accu0 := Z.lnot (Zinsert 0 n p 16)). - set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))). - destruct (exec_loadimm_k_x rd k m (negate_decomposition l) - (negate_decomposition_wf l H1) - rs1 accu0) as (rs2 & P & Q & R). - unfold rs1; Simpl. - exists rs2; split. - eapply exec_straight_opt_step; eauto. - simpl. unfold rs1. do 5 f_equal. - unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega. - split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q. - intros. rewrite R by auto. unfold rs1; Simpl. + - econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. + - set (accu0 := Z.lnot (Zinsert 0 n p 16)). + set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))). + destruct (exec_loadimm_k_x rd k m (negate_decomposition l) + (negate_decomposition_wf l H1) + rs1 accu0) as (rs2 & P & Q & R). + unfold rs1; Simpl. + exists rs2; split. + eapply exec_straight_opt_step; eauto. + simpl. unfold rs1. do 5 f_equal. + unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega. + split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q. + intros. rewrite R by auto. unfold rs1; Simpl. Qed. Lemma exec_loadimm64: @@ -445,23 +445,23 @@ Lemma exec_loadimm64: Proof. unfold loadimm64, loadimm; intros. destruct (is_logical_imm64 n). -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. rewrite Int64.repr_unsigned, Int64.or_zero_l; auto. - intros; Simpl. -- set (dz := decompose_int 4%nat (Int64.unsigned n) 0). - set (dn := decompose_int 4%nat (Z.lnot (Int64.unsigned n)) 0). - assert (A: Int64.repr (recompose_int 0 dz) = n). - { transitivity (Int64.repr (Int64.unsigned n)). - apply Int64.eqm_samerepr. apply decompose_int_eqmod. - apply Int64.repr_unsigned. } - assert (B: Int64.repr (Z.lnot (recompose_int 0 dn)) = n). - { transitivity (Int64.repr (Int64.unsigned n)). - apply Int64.eqm_samerepr. apply decompose_notint_eqmod. - apply Int64.repr_unsigned. } - destruct Nat.leb. -+ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega. -+ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega. + - econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. rewrite Int64.repr_unsigned, Int64.or_zero_l; auto. + intros; Simpl. + - set (dz := decompose_int 4%nat (Int64.unsigned n) 0). + set (dn := decompose_int 4%nat (Z.lnot (Int64.unsigned n)) 0). + assert (A: Int64.repr (recompose_int 0 dz) = n). + { transitivity (Int64.repr (Int64.unsigned n)). + apply Int64.eqm_samerepr. apply decompose_int_eqmod. + apply Int64.repr_unsigned. } + assert (B: Int64.repr (Z.lnot (recompose_int 0 dn)) = n). + { transitivity (Int64.repr (Int64.unsigned n)). + apply Int64.eqm_samerepr. apply decompose_notint_eqmod. + apply Int64.repr_unsigned. } + destruct Nat.leb. + + rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega. + + rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega. Qed. (** Add immediate *) @@ -483,17 +483,17 @@ Proof. assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; omega). rewrite <- (Int.repr_unsigned n). destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)]. -- econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. - intros; Simpl. -- econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. - intros; Simpl. -- econstructor; split. eapply exec_straight_two. - apply SEM. apply SEM. simpl. Simpl. - split. Simpl. simpl. rewrite ASSOC. do 2 f_equal. apply Int.eqm_samerepr. - rewrite E. auto with ints. - intros; Simpl. + - econstructor; split. apply exec_straight_one. apply SEM. Simpl. + split. Simpl. do 3 f_equal; omega. + intros; Simpl. + - econstructor; split. apply exec_straight_one. apply SEM. Simpl. + split. Simpl. do 3 f_equal; omega. + intros; Simpl. + - econstructor; split. eapply exec_straight_two. + apply SEM. apply SEM. simpl. Simpl. + split. Simpl. simpl. rewrite ASSOC. do 2 f_equal. apply Int.eqm_samerepr. + rewrite E. auto with ints. + intros; Simpl. Qed. Lemma exec_addimm32: @@ -506,22 +506,22 @@ Lemma exec_addimm32: Proof. intros. unfold addimm32. set (nn := Int.neg n). destruct (Int.eq n (Int.zero_ext 24 n)); [| destruct (Int.eq nn (Int.zero_ext 24 nn))]. -- apply exec_addimm_aux_32 with (sem := Val.add). auto. intros; apply Val.add_assoc. -- rewrite <- Val.sub_opp_add. - apply exec_addimm_aux_32 with (sem := Val.sub). auto. - intros. rewrite ! Val.sub_add_opp, Val.add_assoc. rewrite Int.neg_add_distr. auto. -- destruct (Int.lt n Int.zero). -+ rewrite <- Val.sub_opp_add; fold nn. - edestruct (exec_loadimm32 X16 nn) as (rs1 & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto. - split. Simpl. rewrite B, C; eauto with asmgen. - intros; Simpl. -+ edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto. - split. Simpl. rewrite B, C; eauto with asmgen. - intros; Simpl. + - apply exec_addimm_aux_32 with (sem := Val.add). auto. intros; apply Val.add_assoc. + - rewrite <- Val.sub_opp_add. + apply exec_addimm_aux_32 with (sem := Val.sub). auto. + intros. rewrite ! Val.sub_add_opp, Val.add_assoc. rewrite Int.neg_add_distr. auto. + - destruct (Int.lt n Int.zero). + + rewrite <- Val.sub_opp_add; fold nn. + edestruct (exec_loadimm32 X16 nn) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto. + split. Simpl. rewrite B, C; eauto with asmgen. + intros; Simpl. + + edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto. + split. Simpl. rewrite B, C; eauto with asmgen. + intros; Simpl. Qed. Lemma exec_addimm_aux_64: @@ -541,17 +541,17 @@ Proof. assert (E: Int64.unsigned n = nhi + nlo) by (unfold nhi; omega). rewrite <- (Int64.repr_unsigned n). destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)]. -- econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. - intros; Simpl. -- econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. - intros; Simpl. -- econstructor; split. eapply exec_straight_two. - apply SEM. apply SEM. Simpl. Simpl. - split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int64.eqm_samerepr. - rewrite E. auto with ints. - intros; Simpl. + - econstructor; split. apply exec_straight_one. apply SEM. Simpl. + split. Simpl. do 3 f_equal; omega. + intros; Simpl. + - econstructor; split. apply exec_straight_one. apply SEM. Simpl. + split. Simpl. do 3 f_equal; omega. + intros; Simpl. + - econstructor; split. eapply exec_straight_two. + apply SEM. apply SEM. Simpl. Simpl. + split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int64.eqm_samerepr. + rewrite E. auto with ints. + intros; Simpl. Qed. Lemma exec_addimm64: @@ -565,22 +565,22 @@ Proof. intros. unfold addimm64. set (nn := Int64.neg n). destruct (Int64.eq n (Int64.zero_ext 24 n)); [| destruct (Int64.eq nn (Int64.zero_ext 24 nn))]. -- apply exec_addimm_aux_64 with (sem := Val.addl). auto. intros; apply Val.addl_assoc. -- rewrite <- Val.subl_opp_addl. - apply exec_addimm_aux_64 with (sem := Val.subl). auto. - intros. rewrite ! Val.subl_addl_opp, Val.addl_assoc. rewrite Int64.neg_add_distr. auto. -- destruct (Int64.lt n Int64.zero). -+ rewrite <- Val.subl_opp_addl; fold nn. - edestruct (exec_loadimm64 X16 nn) as (rs1 & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. - split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto. - intros; Simpl. -+ edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. - split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto. - intros; Simpl. + - apply exec_addimm_aux_64 with (sem := Val.addl). auto. intros; apply Val.addl_assoc. + - rewrite <- Val.subl_opp_addl. + apply exec_addimm_aux_64 with (sem := Val.subl). auto. + intros. rewrite ! Val.subl_addl_opp, Val.addl_assoc. rewrite Int64.neg_add_distr. auto. + - destruct (Int64.lt n Int64.zero). + + rewrite <- Val.subl_opp_addl; fold nn. + edestruct (exec_loadimm64 X16 nn) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. + split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto. + intros; Simpl. + + edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. + split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto. + intros; Simpl. Qed. (** Logical immediate *) @@ -604,15 +604,15 @@ Lemma exec_logicalimm32: Proof. intros until sem; intros SEM1 SEM2; intros. unfold logicalimm32. destruct (is_logical_imm32 n). -- econstructor; split. - apply exec_straight_one. apply SEM1. - split. Simpl. rewrite Int.repr_unsigned; auto. intros; Simpl. -- edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. apply SEM2. - split. Simpl. f_equal; auto. apply C; auto with asmgen. - intros; Simpl. + - econstructor; split. + apply exec_straight_one. apply SEM1. + split. Simpl. rewrite Int.repr_unsigned; auto. intros; Simpl. + - edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. apply SEM2. + split. Simpl. f_equal; auto. apply C; auto with asmgen. + intros; Simpl. Qed. Lemma exec_logicalimm64: @@ -634,15 +634,15 @@ Lemma exec_logicalimm64: Proof. intros until sem; intros SEM1 SEM2; intros. unfold logicalimm64. destruct (is_logical_imm64 n). -- econstructor; split. - apply exec_straight_one. apply SEM1. - split. Simpl. rewrite Int64.repr_unsigned. auto. intros; Simpl. -- edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. apply SEM2. - split. Simpl. f_equal; auto. apply C; auto with asmgen. - intros; Simpl. + - econstructor; split. + apply exec_straight_one. apply SEM1. + split. Simpl. rewrite Int64.repr_unsigned. auto. intros; Simpl. + - edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. apply SEM2. + split. Simpl. f_equal; auto. apply C; auto with asmgen. + intros; Simpl. Qed. (** Load address of symbol *) @@ -655,22 +655,22 @@ Lemma exec_loadsymbol: forall rd s ofs k rs m, /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. unfold loadsymbol; intros. destruct (Archi.pic_code tt). -- predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero. -+ subst ofs. econstructor; split. - apply exec_straight_one. simpl; eauto. - split. Simpl. intros; Simpl. -+ exploit exec_addimm64. instantiate (1 := rd). simpl. destruct H; congruence. - intros (rs1 & A & B & C). - econstructor; split. - econstructor. simpl; eauto. auto. eexact A. - split. simpl in B; rewrite B. Simpl. - rewrite <- Genv.shift_symbol_address_64 by auto. - rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto. - intros. rewrite C by auto. Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split. Simpl. - intros; Simpl. + - predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero. + + subst ofs. econstructor; split. + apply exec_straight_one. simpl; eauto. + split. Simpl. intros; Simpl. + + exploit exec_addimm64. instantiate (1 := rd). simpl. destruct H; congruence. + intros (rs1 & A & B & C). + econstructor; split. + econstructor. simpl; eauto. auto. eexact A. + split. simpl in B; rewrite B. Simpl. + rewrite <- Genv.shift_symbol_address_64 by auto. + rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto. + intros. rewrite C by auto. Simpl. + - econstructor; split. + eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. + split. Simpl. + intros; Simpl. Qed. (** Shifted operands *) @@ -754,18 +754,18 @@ Lemma exec_move_extended: forall rd r1 ex (a: amount64) k rs m, /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. unfold move_extended; intros. predSpec Int.eq Int.eq_spec a Int.zero. -- exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C). - exists rs'; split. eexact A. split. unfold Op.eval_extend. rewrite H. rewrite B. - destruct ex, (rs r1); simpl; auto; rewrite Int64.shl'_zero; auto. - auto. -- Local Opaque Val.addl. - exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - change (SOlsl a) with (transl_shift Slsl a). rewrite transl_eval_shiftl''. eauto. auto. - split. Simpl. rewrite B. auto. - intros; Simpl. + - exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C). + exists rs'; split. eexact A. split. unfold Op.eval_extend. rewrite H. rewrite B. + destruct ex, (rs r1); simpl; auto; rewrite Int64.shl'_zero; auto. + auto. + - Local Opaque Val.addl. + exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + change (SOlsl a) with (transl_shift Slsl a). rewrite transl_eval_shiftl''. eauto. auto. + split. Simpl. rewrite B. auto. + intros; Simpl. Qed. Lemma exec_arith_extended: @@ -786,17 +786,17 @@ Lemma exec_arith_extended: /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. intros sem insnX insnS EX ES; intros. unfold arith_extended. destruct (Int.ltu a (Int.repr 5)). -- econstructor; split. - apply exec_straight_one. rewrite EX; eauto. auto. - split. Simpl. f_equal. destruct ex; auto. - intros; Simpl. -- exploit (exec_move_extended_base X16 r2 ex). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - rewrite ES. eauto. auto. - split. Simpl. unfold ir0. rewrite C by eauto with asmgen. f_equal. - rewrite B. destruct ex; auto. - intros; Simpl. + - econstructor; split. + apply exec_straight_one. rewrite EX; eauto. auto. + split. Simpl. f_equal. destruct ex; auto. + intros; Simpl. + - exploit (exec_move_extended_base X16 r2 ex). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + rewrite ES. eauto. auto. + split. Simpl. unfold ir0. rewrite C by eauto with asmgen. f_equal. + rewrite B. destruct ex; auto. + intros; Simpl. Qed. (** Extended right shift *) @@ -811,15 +811,15 @@ Lemma exec_shrx32: forall (rd r1: ireg) (n: int) k v (rs: regset) m, Proof. unfold shrx32; intros. apply Val.shrx_shr_2 in H. destruct (Int.eq n Int.zero) eqn:E0. -- econstructor; split. apply exec_straight_one; simpl; eauto. - split. Simpl. subst v; auto. intros; Simpl. -- econstructor; split. eapply exec_straight_three. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_int by congruence. eauto. - simpl; eauto. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_int by congruence. eauto. - split. subst v; Simpl. intros; Simpl. + - econstructor; split. apply exec_straight_one; simpl; eauto. + split. Simpl. subst v; auto. intros; Simpl. + - econstructor; split. eapply exec_straight_three. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_int by congruence. eauto. + simpl; eauto. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_int by congruence. eauto. + split. subst v; Simpl. intros; Simpl. Qed. Lemma exec_shrx32_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m, @@ -832,15 +832,15 @@ Lemma exec_shrx32_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m, Proof. unfold shrx32; intros. destruct (Int.eq n Int.zero) eqn:E0. -- econstructor; split. apply exec_straight_one; simpl; eauto. - split. Simpl. auto. intros; Simpl. -- econstructor; split. eapply exec_straight_three. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_int by congruence. eauto. - simpl; eauto. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_int by congruence. eauto. - split. Simpl. intros; Simpl. + - econstructor; split. apply exec_straight_one; simpl; eauto. + split. Simpl. auto. intros; Simpl. + - econstructor; split. eapply exec_straight_three. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_int by congruence. eauto. + simpl; eauto. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_int by congruence. eauto. + split. Simpl. intros; Simpl. Qed. Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m, @@ -853,15 +853,15 @@ Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m, Proof. unfold shrx64; intros. apply Val.shrxl_shrl_2 in H. destruct (Int.eq n Int.zero) eqn:E. -- econstructor; split. apply exec_straight_one; simpl; eauto. - split. Simpl. subst v; auto. intros; Simpl. -- econstructor; split. eapply exec_straight_three. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_long by congruence. eauto. - simpl; eauto. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_long by congruence. eauto. - split. subst v; Simpl. intros; Simpl. + - econstructor; split. apply exec_straight_one; simpl; eauto. + split. Simpl. subst v; auto. intros; Simpl. + - econstructor; split. eapply exec_straight_three. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_long by congruence. eauto. + simpl; eauto. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_long by congruence. eauto. + split. subst v; Simpl. intros; Simpl. Qed. Lemma exec_shrx64_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m, @@ -874,15 +874,15 @@ Lemma exec_shrx64_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m, Proof. unfold shrx64; intros. destruct (Int.eq n Int.zero) eqn:E. -- econstructor; split. apply exec_straight_one; simpl; eauto. - split. Simpl. auto. intros; Simpl. -- econstructor; split. eapply exec_straight_three. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_long by congruence. eauto. - simpl; eauto. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_long by congruence. eauto. - split. Simpl. intros; Simpl. + - econstructor; split. apply exec_straight_one; simpl; eauto. + split. Simpl. auto. intros; Simpl. + - econstructor; split. eapply exec_straight_three. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_long by congruence. eauto. + simpl; eauto. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_long by congruence. eauto. + split. Simpl. intros; Simpl. Qed. Ltac TranslOpBase := @@ -913,14 +913,14 @@ Proof. destruct v1; try discriminate; destruct v2; try discriminate. simpl in H; inv H. unfold Val_cmpu; simpl. destruct c; simpl. -- destruct (Int.eq i i0); auto. -- destruct (Int.eq i i0); auto. -- rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto. -- rewrite Int.lt_sub_overflow, Int.not_lt. - destruct (Int.eq i i0), (Int.lt i i0); auto. -- rewrite Int.lt_sub_overflow, (Int.lt_not i). - destruct (Int.eq i i0), (Int.lt i i0); auto. -- rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto. + - destruct (Int.eq i i0); auto. + - destruct (Int.eq i i0); auto. + - rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto. + - rewrite Int.lt_sub_overflow, Int.not_lt. + destruct (Int.eq i i0), (Int.lt i i0); auto. + - rewrite Int.lt_sub_overflow, (Int.lt_not i). + destruct (Int.eq i i0), (Int.lt i i0); auto. + - rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto. Qed. Lemma eval_testcond_compare_uint: forall c v1 v2 b rs, @@ -933,12 +933,12 @@ Proof. destruct v1; try discriminate; destruct v2; try discriminate. simpl in H; inv H. unfold Val_cmpu; simpl. destruct c; simpl. -- destruct (Int.eq i i0); auto. -- destruct (Int.eq i i0); auto. -- destruct (Int.ltu i i0); auto. -- rewrite (Int.not_ltu i). destruct (Int.eq i i0), (Int.ltu i i0); auto. -- rewrite (Int.ltu_not i). destruct (Int.eq i i0), (Int.ltu i i0); auto. -- destruct (Int.ltu i i0); auto. + - destruct (Int.eq i i0); auto. + - destruct (Int.eq i i0); auto. + - destruct (Int.ltu i i0); auto. + - rewrite (Int.not_ltu i). destruct (Int.eq i i0), (Int.ltu i i0); auto. + - rewrite (Int.ltu_not i). destruct (Int.eq i i0), (Int.ltu i i0); auto. + - destruct (Int.ltu i i0); auto. Qed. Lemma compare_long_spec: forall rs v1 v2, @@ -978,14 +978,14 @@ Proof. destruct v1; try discriminate; destruct v2; try discriminate. simpl in H; inv H. unfold Val_cmplu; simpl. destruct c; simpl. -- destruct (Int64.eq i i0); auto. -- destruct (Int64.eq i i0); auto. -- rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto. -- rewrite int64_sub_overflow, Int64.not_lt. - destruct (Int64.eq i i0), (Int64.lt i i0); auto. -- rewrite int64_sub_overflow, (Int64.lt_not i). - destruct (Int64.eq i i0), (Int64.lt i i0); auto. -- rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto. + - destruct (Int64.eq i i0); auto. + - destruct (Int64.eq i i0); auto. + - rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto. + - rewrite int64_sub_overflow, Int64.not_lt. + destruct (Int64.eq i i0), (Int64.lt i i0); auto. + - rewrite int64_sub_overflow, (Int64.lt_not i). + destruct (Int64.eq i i0), (Int64.lt i i0); auto. + - rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto. Qed. Lemma eval_testcond_compare_ulong: forall c v1 v2 b rs, @@ -996,37 +996,37 @@ Proof. set (rs' := compare_long rs v1 v2). intros (B & C & D & E). unfold eval_testcond; rewrite B, C, D, E; unfold Val_cmplu. destruct v1; try discriminate; destruct v2; try discriminate; simpl in H. -- (* int-int *) - inv H. destruct c; simpl. -+ destruct (Int64.eq i i0); auto. -+ destruct (Int64.eq i i0); auto. -+ destruct (Int64.ltu i i0); auto. -+ rewrite (Int64.not_ltu i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto. -+ rewrite (Int64.ltu_not i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto. -+ destruct (Int64.ltu i i0); auto. -- (* int-ptr *) - simpl. - destruct (Archi.ptr64); simpl; try discriminate. - destruct (Int64.eq i Int64.zero); simpl; try discriminate. - destruct c; simpl in H; inv H; reflexivity. -- (* ptr-int *) - simpl. - destruct (Archi.ptr64); simpl; try discriminate. - destruct (Int64.eq i0 Int64.zero); try discriminate. - destruct c; simpl in H; inv H; reflexivity. -- (* ptr-ptr *) - simpl. - destruct (eq_block b0 b1). - destruct (Archi.ptr64); simpl; try discriminate. - inv H. - destruct c; simpl. -* destruct (Ptrofs.eq i i0); auto. -* destruct (Ptrofs.eq i i0); auto. -* destruct (Ptrofs.ltu i i0); auto. -* rewrite (Ptrofs.not_ltu i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto. -* rewrite (Ptrofs.ltu_not i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto. -* destruct (Ptrofs.ltu i i0); auto. -* destruct c; simpl in H; inv H; reflexivity. + - (* int-int *) + inv H. destruct c; simpl. + + destruct (Int64.eq i i0); auto. + + destruct (Int64.eq i i0); auto. + + destruct (Int64.ltu i i0); auto. + + rewrite (Int64.not_ltu i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto. + + rewrite (Int64.ltu_not i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto. + + destruct (Int64.ltu i i0); auto. + - (* int-ptr *) + simpl. + destruct (Archi.ptr64); simpl; try discriminate. + destruct (Int64.eq i Int64.zero); simpl; try discriminate. + destruct c; simpl in H; inv H; reflexivity. + - (* ptr-int *) + simpl. + destruct (Archi.ptr64); simpl; try discriminate. + destruct (Int64.eq i0 Int64.zero); try discriminate. + destruct c; simpl in H; inv H; reflexivity. + - (* ptr-ptr *) + simpl. + destruct (eq_block b0 b1). + destruct (Archi.ptr64); simpl; try discriminate. + inv H. + destruct c; simpl. + * destruct (Ptrofs.eq i i0); auto. + * destruct (Ptrofs.eq i i0); auto. + * destruct (Ptrofs.ltu i i0); auto. + * rewrite (Ptrofs.not_ltu i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto. + * rewrite (Ptrofs.ltu_not i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto. + * destruct (Ptrofs.ltu i i0); auto. + * destruct c; simpl in H; inv H; reflexivity. Qed. Lemma compare_float_spec: forall rs f1 f2, @@ -1132,179 +1132,179 @@ Lemma transl_cond_correct: /\ forall r, data_preg r = true -> rs'#r = rs#r. Proof. intros until m; intros TR. destruct cond; simpl in TR; ArgsInv. -- (* Ccomp *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_sint; auto. - destruct r; reflexivity || discriminate. -- (* Ccompu *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. apply eval_testcond_compare_uint; auto. - destruct r; reflexivity || discriminate. -- (* Ccompimm *) - destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. - destruct r; reflexivity || discriminate. -+ econstructor; split. - apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto. - split; intros. apply eval_testcond_compare_sint; auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - simpl. rewrite B, C by eauto with asmgen. eauto. - split; intros. apply eval_testcond_compare_sint; auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Ccompuimm *) - destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_uint; auto. - destruct r; reflexivity || discriminate. -+ econstructor; split. - apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto. - split; intros. apply eval_testcond_compare_uint; auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - simpl. rewrite B, C by eauto with asmgen. eauto. auto. - split; intros. apply eval_testcond_compare_uint; auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Ccompshift *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; auto. - destruct r; reflexivity || discriminate. -- (* Ccompushift *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; auto. - destruct r; reflexivity || discriminate. -- (* Cmaskzero *) - destruct (is_logical_imm32 n). -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto. - split; intros. apply (eval_testcond_compare_sint Ceq); auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Cmasknotzero *) - destruct (is_logical_imm32 n). -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto. - split; intros. apply (eval_testcond_compare_sint Cne); auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Ccompl *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_slong; auto. - destruct r; reflexivity || discriminate. -- (* Ccomplu *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. - destruct r; reflexivity || discriminate. -- (* Ccomplimm *) - destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; auto. - destruct r; reflexivity || discriminate. -+ econstructor; split. - apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. - split; intros. apply eval_testcond_compare_slong; auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - simpl. rewrite B, C by eauto with asmgen. eauto. auto. - split; intros. apply eval_testcond_compare_slong; auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Ccompluimm *) - destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. - destruct r; reflexivity || discriminate. -+ econstructor; split. - apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. - split; intros. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - simpl. rewrite B, C by eauto with asmgen. eauto. - split; intros. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Ccomplshift *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto. - destruct r; reflexivity || discriminate. -- (* Ccomplushift *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. - destruct r; reflexivity || discriminate. -- (* Cmasklzero *) - destruct (is_logical_imm64 n). -+ econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. - split; intros. apply (eval_testcond_compare_slong Ceq); auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Cmasknotzero *) - destruct (is_logical_imm64 n). -+ econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. - split; intros. apply (eval_testcond_compare_slong Cne); auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Ccompf *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_float; auto. - destruct r; discriminate || rewrite compare_float_inv; auto. -- (* Cnotcompf *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_not_float; auto. - destruct r; discriminate || rewrite compare_float_inv; auto. -- (* Ccompfzero *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_float; auto. - destruct r; discriminate || rewrite compare_float_inv; auto. -- (* Cnotcompfzero *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_not_float; auto. - destruct r; discriminate || rewrite compare_float_inv; auto. -- (* Ccompfs *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_single; auto. - destruct r; discriminate || rewrite compare_single_inv; auto. -- (* Cnotcompfs *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_not_single; auto. - destruct r; discriminate || rewrite compare_single_inv; auto. -- (* Ccompfszero *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_single; auto. - destruct r; discriminate || rewrite compare_single_inv; auto. -- (* Cnotcompfszero *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_not_single; auto. - destruct r; discriminate || rewrite compare_single_inv; auto. + - (* Ccomp *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. + - (* Ccompu *) + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. apply eval_testcond_compare_uint; auto. + destruct r; reflexivity || discriminate. + - (* Ccompimm *) + destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. + + econstructor; split. + apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto. + split; intros. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. + split; intros. apply eval_testcond_compare_sint; auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Ccompuimm *) + destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_uint; auto. + destruct r; reflexivity || discriminate. + + econstructor; split. + apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto. + split; intros. apply eval_testcond_compare_uint; auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply eval_testcond_compare_uint; auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Ccompshift *) + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. + - (* Ccompushift *) + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; auto. + destruct r; reflexivity || discriminate. + - (* Cmaskzero *) + destruct (is_logical_imm32 n). + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply (eval_testcond_compare_sint Ceq); auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Cmasknotzero *) + destruct (is_logical_imm32 n). + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply (eval_testcond_compare_sint Cne); auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Ccompl *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_slong; auto. + destruct r; reflexivity || discriminate. + - (* Ccomplu *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + destruct r; reflexivity || discriminate. + - (* Ccomplimm *) + destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; auto. + destruct r; reflexivity || discriminate. + + econstructor; split. + apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. + split; intros. apply eval_testcond_compare_slong; auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply eval_testcond_compare_slong; auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Ccompluimm *) + destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + destruct r; reflexivity || discriminate. + + econstructor; split. + apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. + split; intros. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. + split; intros. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Ccomplshift *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto. + destruct r; reflexivity || discriminate. + - (* Ccomplushift *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + destruct r; reflexivity || discriminate. + - (* Cmasklzero *) + destruct (is_logical_imm64 n). + + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. + split; intros. apply (eval_testcond_compare_slong Ceq); auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Cmasknotzero *) + destruct (is_logical_imm64 n). + + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. + split; intros. apply (eval_testcond_compare_slong Cne); auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Ccompf *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_float; auto. + destruct r; discriminate || rewrite compare_float_inv; auto. + - (* Cnotcompf *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_not_float; auto. + destruct r; discriminate || rewrite compare_float_inv; auto. + - (* Ccompfzero *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_float; auto. + destruct r; discriminate || rewrite compare_float_inv; auto. + - (* Cnotcompfzero *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_not_float; auto. + destruct r; discriminate || rewrite compare_float_inv; auto. + - (* Ccompfs *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_single; auto. + destruct r; discriminate || rewrite compare_single_inv; auto. + - (* Cnotcompfs *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_not_single; auto. + destruct r; discriminate || rewrite compare_single_inv; auto. + - (* Ccompfszero *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_single; auto. + destruct r; discriminate || rewrite compare_single_inv; auto. + - (* Cnotcompfszero *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_not_single; auto. + destruct r; discriminate || rewrite compare_single_inv; auto. Qed. Lemma transl_cond_correct': @@ -1351,90 +1351,90 @@ Local Opaque transl_cond transl_cond_branch_default. destruct args as [ | a1 args]; simpl in TR; auto. destruct args as [ | a2 args]; simpl in TR; auto. destruct cond; simpl in TR; auto. -- (* Ccompimm *) - destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto; - apply Int.same_if_eq in N0; subst n; ArgsInv. -+ (* Ccompimm Cne 0 *) - econstructor; split. econstructor. - split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. - unfold incrPC. Simpl. rewrite EQRSX. simpl. auto. -+ (* Ccompimm Ceq 0 *) - econstructor; split. econstructor. - split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. - unfold incrPC. Simpl. rewrite EQRSX. simpl. - destruct (Int.eq i Int.zero); auto. -- (* Ccompuimm *) - destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto. - apply Int.same_if_eq in N0; subst n; ArgsInv. -+ (* Ccompuimm Cne 0 *) - econstructor; split. econstructor. - split; auto. simpl. apply Val_cmpu_bool_correct in EV. - unfold incrPC. Simpl. rewrite EV. auto. -+ (* Ccompuimm Ceq 0 *) - monadInv TR. ArgsInv. simpl in *. - econstructor; split. econstructor. - split; auto. simpl. unfold incrPC. Simpl. - apply Int.same_if_eq in N0; subst. - rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cne), EV. - destruct b; auto. -- (* Cmaskzero *) - destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv. - econstructor; split. econstructor. - split; auto. simpl. - erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto. - unfold incrPC. Simpl. - rewrite (Val.negate_cmp_bool Ceq), EV. destruct b; auto. -- (* Cmasknotzero *) - destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv. - econstructor; split. econstructor. - split; auto. simpl. - erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto. - unfold incrPC. Simpl. - rewrite EV. auto. -- (* Ccomplimm *) - destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; - apply Int64.same_if_eq in N0; subst n; ArgsInv. -+ (* Ccomplimm Cne 0 *) - econstructor; split. econstructor. - split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. - unfold incrPC. Simpl. rewrite EQRSX. simpl. auto. -+ (* Ccomplimm Ceq 0 *) - econstructor; split. econstructor. - split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. - unfold incrPC. Simpl. rewrite EQRSX. simpl. - destruct (Int64.eq i Int64.zero); auto. -- (* Ccompluimm *) - destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; - apply Int64.same_if_eq in N0; subst n; ArgsInv. -+ (* Ccompluimm Cne 0 *) - econstructor; split. econstructor. - split; auto. simpl. apply Val_cmplu_bool_correct in EV. - unfold incrPC. Simpl. rewrite EV. auto. -+ (* Ccompluimm Ceq 0 *) - econstructor; split. econstructor. - split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. - unfold incrPC. Simpl. rewrite EQRSX. simpl. - destruct (Int64.eq i Int64.zero); auto. - unfold incrPC. Simpl. rewrite EQRSX. simpl. - rewrite SF in *; simpl in *. - rewrite Int64.eq_true in *. - destruct ((Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); simpl in *. - assert (b = true). { destruct b; try congruence. } - rewrite H; auto. discriminate. -- (* Cmasklzero *) - destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv. - econstructor; split. econstructor. - split; auto. - erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto. - unfold incrPC. Simpl. - rewrite (Val.negate_cmpl_bool Ceq), EV. destruct b; auto. -- (* Cmasklnotzero *) - destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv. - econstructor; split. econstructor. - split; auto. - erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto. - unfold incrPC. Simpl. - rewrite EV. auto. + - (* Ccompimm *) + destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto; + apply Int.same_if_eq in N0; subst n; ArgsInv. + + (* Ccompimm Cne 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. + unfold incrPC. Simpl. rewrite EQRSX. simpl. auto. + + (* Ccompimm Ceq 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. + unfold incrPC. Simpl. rewrite EQRSX. simpl. + destruct (Int.eq i Int.zero); auto. + - (* Ccompuimm *) + destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto. + apply Int.same_if_eq in N0; subst n; ArgsInv. + + (* Ccompuimm Cne 0 *) + econstructor; split. econstructor. + split; auto. simpl. apply Val_cmpu_bool_correct in EV. + unfold incrPC. Simpl. rewrite EV. auto. + + (* Ccompuimm Ceq 0 *) + monadInv TR. ArgsInv. simpl in *. + econstructor; split. econstructor. + split; auto. simpl. unfold incrPC. Simpl. + apply Int.same_if_eq in N0; subst. + rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cne), EV. + destruct b; auto. + - (* Cmaskzero *) + destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv. + econstructor; split. econstructor. + split; auto. simpl. + erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto. + unfold incrPC. Simpl. + rewrite (Val.negate_cmp_bool Ceq), EV. destruct b; auto. + - (* Cmasknotzero *) + destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv. + econstructor; split. econstructor. + split; auto. simpl. + erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto. + unfold incrPC. Simpl. + rewrite EV. auto. + - (* Ccomplimm *) + destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; + apply Int64.same_if_eq in N0; subst n; ArgsInv. + + (* Ccomplimm Cne 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. + unfold incrPC. Simpl. rewrite EQRSX. simpl. auto. + + (* Ccomplimm Ceq 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. + unfold incrPC. Simpl. rewrite EQRSX. simpl. + destruct (Int64.eq i Int64.zero); auto. + - (* Ccompluimm *) + destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; + apply Int64.same_if_eq in N0; subst n; ArgsInv. + + (* Ccompluimm Cne 0 *) + econstructor; split. econstructor. + split; auto. simpl. apply Val_cmplu_bool_correct in EV. + unfold incrPC. Simpl. rewrite EV. auto. + + (* Ccompluimm Ceq 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. + unfold incrPC. Simpl. rewrite EQRSX. simpl. + destruct (Int64.eq i Int64.zero); auto. + unfold incrPC. Simpl. rewrite EQRSX. simpl. + rewrite SF in *; simpl in *. + rewrite Int64.eq_true in *. + destruct ((Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); simpl in *. + assert (b = true). { destruct b; try congruence. } + rewrite H; auto. discriminate. + - (* Cmasklzero *) + destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv. + econstructor; split. econstructor. + split; auto. + erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto. + unfold incrPC. Simpl. + rewrite (Val.negate_cmpl_bool Ceq), EV. destruct b; auto. + - (* Cmasklnotzero *) + destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv. + econstructor; split. econstructor. + split; auto. + erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto. + unfold incrPC. Simpl. + rewrite EV. auto. Qed. Lemma transl_op_correct: @@ -1451,200 +1451,200 @@ Local Opaque Int.eq Int64.eq Val.add Val.addl Int.zwordsize Int64.zwordsize. intros until c; intros TR EV. unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl; try (rewrite <- transl_eval_shift; TranslOpSimpl). -- (* move *) - destruct (preg_of res), (preg_of m0); try destruct d; try destruct d0; inv TR; TranslOpSimpl. -- (* intconst *) - exploit exec_loadimm32. intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen. -- (* longconst *) - exploit exec_loadimm64. intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen. -- (* floatconst *) - destruct (Float.eq_dec n Float.zero). -+ subst n. TranslOpSimpl. -+ TranslOpSimplN. -- (* singleconst *) - destruct (Float32.eq_dec n Float32.zero). -+ subst n. TranslOpSimpl. -+ TranslOpSimplN. -- (* loadsymbol *) - exploit (exec_loadsymbol x id ofs). eauto with asmgen. intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* addrstack *) - exploit (exec_addimm64 x XSP (Ptrofs.to_int64 ofs)); try discriminate. simpl; eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. replace (DR XSP) with (SP) in B by auto. rewrite B. -Local Transparent Val.addl. - destruct (rs SP); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto. - auto. -- (* shift *) - rewrite <- transl_eval_shift'. TranslOpSimpl. -- (* addimm *) - exploit (exec_addimm32 x x0 n). eauto with asmgen. intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* mul *) - TranslOpBase. -Local Transparent Val.add. - destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int.add_zero_l; auto. -- (* andimm *) - exploit (exec_logicalimm32 (Pandimm W) (Pand W)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* orimm *) - exploit (exec_logicalimm32 (Porrimm W) (Porr W)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* xorimm *) - exploit (exec_logicalimm32 (Peorimm W) (Peor W)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* not *) - TranslOpBase. - destruct (rs x0); auto. simpl. rewrite Int.or_zero_l; auto. -- (* notshift *) - TranslOpBase. - destruct (eval_shift s (rs x0) a); auto. simpl. rewrite Int.or_zero_l; auto. -- (* shrx *) - assert (Val.maketotal (Val.shrx (rs x0) (Vint n)) = Val.maketotal (Val.shrx (rs x0) (Vint n))) by eauto. - destruct (Val.shrx) eqn:E. - + exploit (exec_shrx32 x x0 n); eauto with asmgen. intros (rs' & A & B & C). + - (* move *) + destruct (preg_of res), (preg_of m0); try destruct d; try destruct d0; inv TR; TranslOpSimpl. + - (* intconst *) + exploit exec_loadimm32. intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen. + - (* longconst *) + exploit exec_loadimm64. intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen. + - (* floatconst *) + destruct (Float.eq_dec n Float.zero). + + subst n. TranslOpSimpl. + + TranslOpSimplN. + - (* singleconst *) + destruct (Float32.eq_dec n Float32.zero). + + subst n. TranslOpSimpl. + + TranslOpSimplN. + - (* loadsymbol *) + exploit (exec_loadsymbol x id ofs). eauto with asmgen. intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* addrstack *) + exploit (exec_addimm64 x XSP (Ptrofs.to_int64 ofs)); try discriminate. simpl; eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. replace (DR XSP) with (SP) in B by auto. rewrite B. + Local Transparent Val.addl. + destruct (rs SP); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto. + auto. + - (* shift *) + rewrite <- transl_eval_shift'. TranslOpSimpl. + - (* addimm *) + exploit (exec_addimm32 x x0 n). eauto with asmgen. intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* mul *) + TranslOpBase. + Local Transparent Val.add. + destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int.add_zero_l; auto. + - (* andimm *) + exploit (exec_logicalimm32 (Pandimm W) (Pand W)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* orimm *) + exploit (exec_logicalimm32 (Porrimm W) (Porr W)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* xorimm *) + exploit (exec_logicalimm32 (Peorimm W) (Peor W)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* not *) + TranslOpBase. + destruct (rs x0); auto. simpl. rewrite Int.or_zero_l; auto. + - (* notshift *) + TranslOpBase. + destruct (eval_shift s (rs x0) a); auto. simpl. rewrite Int.or_zero_l; auto. + - (* shrx *) + assert (Val.maketotal (Val.shrx (rs x0) (Vint n)) = Val.maketotal (Val.shrx (rs x0) (Vint n))) by eauto. + destruct (Val.shrx) eqn:E. + + exploit (exec_shrx32 x x0 n); eauto with asmgen. intros (rs' & A & B & C). + econstructor; split. eexact A. split. rewrite B; auto. auto. + + exploit (exec_shrx32_none x x0 n); eauto with asmgen. + - (* zero-ext *) + TranslOpBase. + destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto. + - (* sign-ext *) + TranslOpBase. + destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto. + - (* shlzext *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite <- Int.shl_zero_ext_min; auto using a32_range. + - (* shlsext *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite <- Int.shl_sign_ext_min; auto using a32_range. + - (* zextshr *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.zero_ext_shru_min; auto using a32_range. + - (* sextshr *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.sign_ext_shr_min; auto using a32_range. + - (* shiftl *) + rewrite <- transl_eval_shiftl'. TranslOpSimpl. + - (* extend *) + exploit (exec_move_extended x0 x1 x a k). intros (rs' & A & B & C). + econstructor; split. eexact A. + split. rewrite B; auto. eauto with asmgen. + - (* addlshift *) + TranslOpBase. + - (* addext *) + exploit (exec_arith_extended Val.addl Paddext (Padd X)). + auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C). econstructor; split. eexact A. split. rewrite B; auto. auto. - + exploit (exec_shrx32_none x x0 n); eauto with asmgen. -- (* zero-ext *) - TranslOpBase. - destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto. -- (* sign-ext *) - TranslOpBase. - destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto. -- (* shlzext *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite <- Int.shl_zero_ext_min; auto using a32_range. -- (* shlsext *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite <- Int.shl_sign_ext_min; auto using a32_range. -- (* zextshr *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.zero_ext_shru_min; auto using a32_range. -- (* sextshr *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.sign_ext_shr_min; auto using a32_range. -- (* shiftl *) - rewrite <- transl_eval_shiftl'. TranslOpSimpl. -- (* extend *) - exploit (exec_move_extended x0 x1 x a k). intros (rs' & A & B & C). - econstructor; split. eexact A. - split. rewrite B; auto. eauto with asmgen. -- (* addlshift *) - TranslOpBase. -- (* addext *) - exploit (exec_arith_extended Val.addl Paddext (Padd X)). - auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C). - econstructor; split. eexact A. split. rewrite B; auto. auto. -- (* addlimm *) - exploit (exec_addimm64 x x0 n). simpl. generalize (ireg_of_not_X16 _ _ EQ1). congruence. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. simpl in B; rewrite B; auto. auto. -- (* neglshift *) - TranslOpBase. -- (* sublshift *) - TranslOpBase. -- (* subext *) - exploit (exec_arith_extended Val.subl Psubext (Psub X)). - auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C). - econstructor; split. eexact A. split. rewrite B; auto. auto. -- (* mull *) - TranslOpBase. - destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int64.add_zero_l; auto. -- (* andlshift *) - TranslOpBase. -- (* andlimm *) - exploit (exec_logicalimm64 (Pandimm X) (Pand X)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* orlshift *) - TranslOpBase. -- (* orlimm *) - exploit (exec_logicalimm64 (Porrimm X) (Porr X)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* orlshift *) - TranslOpBase. -- (* xorlimm *) - exploit (exec_logicalimm64 (Peorimm X) (Peor X)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* notl *) - TranslOpBase. - destruct (rs x0); auto. simpl. rewrite Int64.or_zero_l; auto. -- (* notlshift *) - TranslOpBase. - destruct (eval_shiftl s (rs x0) a); auto. simpl. rewrite Int64.or_zero_l; auto. -- (* biclshift *) - TranslOpBase. -- (* ornlshift *) - TranslOpBase. -- (* eqvlshift *) - TranslOpBase. -- (* shrx *) - assert (Val.maketotal (Val.shrxl (rs x0) (Vint n)) = Val.maketotal (Val.shrxl (rs x0) (Vint n))) by eauto. - destruct (Val.shrxl) eqn:E. - + exploit (exec_shrx64 x x0 n); eauto with asmgen. intros (rs' & A & B & C). + - (* addlimm *) + exploit (exec_addimm64 x x0 n). simpl. generalize (ireg_of_not_X16 _ _ EQ1). congruence. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. simpl in B; rewrite B; auto. auto. + - (* neglshift *) + TranslOpBase. + - (* sublshift *) + TranslOpBase. + - (* subext *) + exploit (exec_arith_extended Val.subl Psubext (Psub X)). + auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C). econstructor; split. eexact A. split. rewrite B; auto. auto. - + exploit (exec_shrx64_none x x0 n); eauto with asmgen. -- (* zero-ext-l *) - TranslOpBase. - destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto. -- (* sign-ext-l *) - TranslOpBase. - destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto. -- (* shllzext *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_zero_ext_min; auto using a64_range. -- (* shllsext *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_sign_ext_min; auto using a64_range. -- (* zextshrl *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.zero_ext_shru'_min; auto using a64_range. -- (* sextshrl *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.sign_ext_shr'_min; auto using a64_range. -- (* condition *) - exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. - split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. - rewrite (B b) by auto. auto. - auto. - intros; Simpl. -- (* select *) - destruct (preg_of res) as [[ir|fr]|cr|] eqn:RES; monadInv TR. - + (* integer *) - generalize (ireg_of_eq _ _ EQ) (ireg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2. + - (* mull *) + TranslOpBase. + destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int64.add_zero_l; auto. + - (* andlshift *) + TranslOpBase. + - (* andlimm *) + exploit (exec_logicalimm64 (Pandimm X) (Pand X)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* orlshift *) + TranslOpBase. + - (* orlimm *) + exploit (exec_logicalimm64 (Porrimm X) (Porr X)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* orlshift *) + TranslOpBase. + - (* xorlimm *) + exploit (exec_logicalimm64 (Peorimm X) (Peor X)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* notl *) + TranslOpBase. + destruct (rs x0); auto. simpl. rewrite Int64.or_zero_l; auto. + - (* notlshift *) + TranslOpBase. + destruct (eval_shiftl s (rs x0) a); auto. simpl. rewrite Int64.or_zero_l; auto. + - (* biclshift *) + TranslOpBase. + - (* ornlshift *) + TranslOpBase. + - (* eqvlshift *) + TranslOpBase. + - (* shrx *) + assert (Val.maketotal (Val.shrxl (rs x0) (Vint n)) = Val.maketotal (Val.shrxl (rs x0) (Vint n))) by eauto. + destruct (Val.shrxl) eqn:E. + + exploit (exec_shrx64 x x0 n); eauto with asmgen. intros (rs' & A & B & C). + econstructor; split. eexact A. split. rewrite B; auto. auto. + + exploit (exec_shrx64_none x x0 n); eauto with asmgen. + - (* zero-ext-l *) + TranslOpBase. + destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto. + - (* sign-ext-l *) + TranslOpBase. + destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto. + - (* shllzext *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_zero_ext_min; auto using a64_range. + - (* shllsext *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_sign_ext_min; auto using a64_range. + - (* zextshrl *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.zero_ext_shru'_min; auto using a64_range. + - (* sextshrl *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.sign_ext_shr'_min; auto using a64_range. + - (* condition *) exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. - rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize. - rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. - auto. - intros; Simpl. - + (* FP *) - generalize (freg_of_eq _ _ EQ) (freg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2. - exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. - split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. - rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize. - rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. + rewrite (B b) by auto. auto. auto. intros; Simpl. + - (* select *) + destruct (preg_of res) as [[ir|fr]|cr|] eqn:RES; monadInv TR. + + (* integer *) + generalize (ireg_of_eq _ _ EQ) (ireg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2. + exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. + split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. + rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize. + rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. + auto. + intros; Simpl. + + (* FP *) + generalize (freg_of_eq _ _ EQ) (freg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2. + exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. + split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. + rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize. + rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. + auto. + intros; Simpl. Qed. (** Translation of addressing modes, loads, stores *) @@ -1660,68 +1660,68 @@ Lemma transl_addressing_correct: Proof. intros until o; intros TR EV. unfold transl_addressing in TR; destruct addr; ArgsInv; SimplEval EV. -- (* Aindexed *) - destruct (offset_representable sz ofs); inv EQ0. -+ econstructor; econstructor; split. apply exec_straight_opt_refl. - auto. -+ exploit (exec_loadimm64 X16 ofs). intros (rs' & A & B & C). - econstructor; exists rs'; split. apply exec_straight_opt_intro; eexact A. - split. simpl. rewrite B, C by eauto with asmgen. auto. - eauto with asmgen. -- (* Aindexed2 *) - econstructor; econstructor; split. apply exec_straight_opt_refl. - auto. -- (* Aindexed2shift *) - destruct (Int.eq a Int.zero) eqn:E; [|destruct (Int.eq (Int.shl Int.one a) (Int.repr sz))]; inv EQ2. -+ apply Int.same_if_eq in E. rewrite E. - econstructor; econstructor; split. apply exec_straight_opt_refl. - split; auto. simpl. - rewrite Val.addl_commut in H0. destruct (rs x0); try discriminate. - unfold Val.shll. rewrite Int64.shl'_zero. auto. -+ econstructor; econstructor; split. apply exec_straight_opt_refl. - auto. -+ econstructor; econstructor; split. - apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. - split. simpl. Simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero. auto. - intros; Simpl. -- (* Aindexed2ext *) - destruct (Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz)); inv EQ2. -+ econstructor; econstructor; split. apply exec_straight_opt_refl. - split; auto. destruct x; auto. -+ exploit (exec_arith_extended Val.addl Paddext (Padd X)); auto. - instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - econstructor; exists rs'; split. - apply exec_straight_opt_intro. eexact A. - split. simpl. rewrite B. rewrite Val.addl_assoc. f_equal. - unfold Op.eval_extend; destruct x, (rs x1); simpl; auto; rewrite ! a64_range; - simpl; rewrite Int64.add_zero; auto. - intros. apply C; eauto with asmgen. -- (* Aglobal *) - destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR. -+ econstructor; econstructor; split. - apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. - split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence. - intros; Simpl. -+ exploit (exec_loadsymbol X16 id ofs). auto. intros (rs' & A & B & C). - econstructor; exists rs'; split. - apply exec_straight_opt_intro. eexact A. - split. simpl. - rewrite B. rewrite <- Genv.shift_symbol_address_64, Ptrofs.add_zero by auto. - simpl in EV. congruence. - auto with asmgen. -- (* Ainstrack *) - assert (E: Val.addl (rs SP) (Vlong (Ptrofs.to_int64 ofs)) = Vptr b o). - { simpl in EV. inv EV. destruct (rs SP); simpl in H1; inv H1. simpl. - rewrite Ptrofs.of_int64_to_int64 by auto. auto. } - destruct (offset_representable sz (Ptrofs.to_int64 ofs)); inv TR. -+ econstructor; econstructor; split. apply exec_straight_opt_refl. - auto. -+ exploit (exec_loadimm64 X16 (Ptrofs.to_int64 ofs)). intros (rs' & A & B & C). - econstructor; exists rs'; split. - apply exec_straight_opt_intro. eexact A. - split. simpl. rewrite B, C by eauto with asmgen. auto. - auto with asmgen. + - (* Aindexed *) + destruct (offset_representable sz ofs); inv EQ0. + + econstructor; econstructor; split. apply exec_straight_opt_refl. + auto. + + exploit (exec_loadimm64 X16 ofs). intros (rs' & A & B & C). + econstructor; exists rs'; split. apply exec_straight_opt_intro; eexact A. + split. simpl. rewrite B, C by eauto with asmgen. auto. + eauto with asmgen. + - (* Aindexed2 *) + econstructor; econstructor; split. apply exec_straight_opt_refl. + auto. + - (* Aindexed2shift *) + destruct (Int.eq a Int.zero) eqn:E; [|destruct (Int.eq (Int.shl Int.one a) (Int.repr sz))]; inv EQ2. + + apply Int.same_if_eq in E. rewrite E. + econstructor; econstructor; split. apply exec_straight_opt_refl. + split; auto. simpl. + rewrite Val.addl_commut in H0. destruct (rs x0); try discriminate. + unfold Val.shll. rewrite Int64.shl'_zero. auto. + + econstructor; econstructor; split. apply exec_straight_opt_refl. + auto. + + econstructor; econstructor; split. + apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. + split. simpl. Simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero. auto. + intros; Simpl. + - (* Aindexed2ext *) + destruct (Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz)); inv EQ2. + + econstructor; econstructor; split. apply exec_straight_opt_refl. + split; auto. destruct x; auto. + + exploit (exec_arith_extended Val.addl Paddext (Padd X)); auto. + instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + econstructor; exists rs'; split. + apply exec_straight_opt_intro. eexact A. + split. simpl. rewrite B. rewrite Val.addl_assoc. f_equal. + unfold Op.eval_extend; destruct x, (rs x1); simpl; auto; rewrite ! a64_range; + simpl; rewrite Int64.add_zero; auto. + intros. apply C; eauto with asmgen. + - (* Aglobal *) + destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR. + + econstructor; econstructor; split. + apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. + split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence. + intros; Simpl. + + exploit (exec_loadsymbol X16 id ofs). auto. intros (rs' & A & B & C). + econstructor; exists rs'; split. + apply exec_straight_opt_intro. eexact A. + split. simpl. + rewrite B. rewrite <- Genv.shift_symbol_address_64, Ptrofs.add_zero by auto. + simpl in EV. congruence. + auto with asmgen. + - (* Ainstrack *) + assert (E: Val.addl (rs SP) (Vlong (Ptrofs.to_int64 ofs)) = Vptr b o). + { simpl in EV. inv EV. destruct (rs SP); simpl in H1; inv H1. simpl. + rewrite Ptrofs.of_int64_to_int64 by auto. auto. } + destruct (offset_representable sz (Ptrofs.to_int64 ofs)); inv TR. + + econstructor; econstructor; split. apply exec_straight_opt_refl. + auto. + + exploit (exec_loadimm64 X16 (Ptrofs.to_int64 ofs)). intros (rs' & A & B & C). + econstructor; exists rs'; split. + apply exec_straight_opt_intro. eexact A. + split. simpl. rewrite B, C by eauto with asmgen. auto. + auto with asmgen. Qed. Lemma transl_load_correct: @@ -1806,11 +1806,11 @@ Proof. assert (Val.addl rs#base (Vlong (Ptrofs.to_int64 ofs)) = Vptr b i). { destruct (rs base); try discriminate. simpl in *. rewrite Ptrofs.of_int64_to_int64 by auto. auto. } destruct offset_representable. -- econstructor; econstructor; split. apply exec_straight_opt_refl. auto. -- exploit (exec_loadimm64 X16); eauto. intros (rs' & A & B & C). - econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A. - split. simpl. rewrite B, C; eauto; try discriminate. - unfold preg_of_iregsp in H. destruct base; auto. auto. + - econstructor; econstructor; split. apply exec_straight_opt_refl. auto. + - exploit (exec_loadimm64 X16); eauto. intros (rs' & A & B & C). + econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A. + split. simpl. rewrite B, C; eauto; try discriminate. + unfold preg_of_iregsp in H. destruct base; auto. auto. Qed. Lemma loadptr_correct: forall (base: iregsp) ofs dst k m v (rs: regset), @@ -1952,4 +1952,4 @@ Proof. intros. Simpl. Qed. -End CONSTRUCTORS.
\ No newline at end of file +End CONSTRUCTORS. |