diff options
Diffstat (limited to 'aarch64/Asmgenproof1.v')
| -rw-r--r-- | aarch64/Asmgenproof1.v | 637 |
1 files changed, 197 insertions, 440 deletions
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v index 35f1f2d7..869d1a31 100644 --- a/aarch64/Asmgenproof1.v +++ b/aarch64/Asmgenproof1.v @@ -22,51 +22,6 @@ Local Transparent Archi.ptr64. (** Properties of registers *) -Lemma preg_of_not_RA: - forall r, (preg_of r) <> RA. -Proof. - destruct r; discriminate. -Qed. - -Lemma RA_not_written: - forall (rs : regset) dst v, - rs # (preg_of dst) <- v RA = rs RA. -Proof. - intros. - apply Pregmap.gso. - intro. - symmetry in H. - exact (preg_of_not_RA dst H). -Qed. - -Hint Resolve RA_not_written : asmgen. - -Lemma RA_not_written2: - forall (rs : regset) dst v i, - preg_of dst = i -> - rs # i <- v RA = rs RA. -Proof. - intros. - subst i. - apply RA_not_written. -Qed. - -Hint Resolve RA_not_written2 : asmgen. - -Lemma RA_not_written3: - forall (rs : regset) dst v i, - ireg_of dst = OK i -> - rs # i <- v RA = rs RA. -Proof. - intros. - unfold ireg_of in H. - destruct preg_of eqn:PREG; try discriminate. - replace i0 with i in * by congruence. - eapply RA_not_written2; eassumption. -Qed. - -Hint Resolve RA_not_written3 : asmgen. - Lemma preg_of_iregsp_not_PC: forall r, preg_of_iregsp r <> PC. Proof. destruct r; simpl; congruence. @@ -84,6 +39,19 @@ Proof. red; intros; subst x. elim (preg_of_not_X16 r); auto. Qed. +Lemma ireg_of_not_X16': forall r x, ireg_of r = OK x -> IR x <> IR X16. +Proof. + intros. apply ireg_of_not_X16 in H. congruence. +Qed. + +Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16': asmgen. + +Lemma preg_of_not_RA: + forall r, (preg_of r) <> RA. +Proof. + destruct r; discriminate. +Qed. + Lemma ireg_of_not_RA: forall r x, ireg_of r = OK x -> x <> RA. Proof. unfold ireg_of; intros. destruct (preg_of r) eqn:E; inv H. @@ -104,13 +72,6 @@ Qed. Hint Resolve ireg_of_not_RA ireg_of_not_RA' ireg_of_not_RA'' : asmgen. -Lemma ireg_of_not_X16': forall r x, ireg_of r = OK x -> IR x <> IR X16. -Proof. - intros. apply ireg_of_not_X16 in H. congruence. -Qed. - -Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16': asmgen. - (** Useful simplification tactic *) @@ -270,49 +231,42 @@ Qed. Lemma exec_loadimm_k_w: forall (rd: ireg) k m l, wf_decomposition l -> - rd <> RA -> forall (rs: regset) accu, rs#rd = Vint (Int.repr accu) -> exists rs', exec_straight_opt ge fn (loadimm_k W rd l k) rs m k rs' m /\ rs'#rd = Vint (Int.repr (recompose_int accu l)) - /\ (forall r, r <> PC -> r <> rd -> rs'#r = rs#r) - /\ rs' # RA = rs # RA. + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. - induction 1; intros RD_NOT_RA rs accu ACCU; simpl. + induction 1; intros rs accu ACCU; simpl. - exists rs; split. apply exec_straight_opt_refl. auto. -- destruct (IHwf_decomposition RD_NOT_RA +- destruct (IHwf_decomposition (nextinstr (rs#rd <- (insert_in_int rs#rd n p 16))) (Zinsert accu n p 16)) - as (rs' & P & Q & R & S). + 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. exact P. - split. exact Q. - split. - { intros; Simpl. - rewrite R by auto. Simpl. } - { rewrite S. Simpl. } + split. exact Q. intros; Simpl. rewrite R by auto. Simpl. Qed. Lemma exec_loadimm_z_w: forall rd l k rs m, wf_decomposition l -> - rd <> RA -> exists rs', exec_straight ge fn (loadimm_z W rd l k) rs m k rs' m /\ rs'#rd = Vint (Int.repr (recompose_int 0 l)) /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. - unfold loadimm_z; destruct 1; intro RD_NOT_RA. + 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 := nextinstr (rs#rd <- (Vint (Int.repr accu0)))). - destruct (exec_loadimm_k_w rd k m l H1 RD_NOT_RA rs1 accu0) as (rs2 & P & Q & R & S); auto. + 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. @@ -325,13 +279,12 @@ Qed. Lemma exec_loadimm_n_w: forall rd l k rs m, wf_decomposition l -> - rd <> RA -> exists rs', exec_straight ge fn (loadimm_n W rd l k) rs m k rs' m /\ rs'#rd = Vint (Int.repr (Z.lnot (recompose_int 0 l))) /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. - unfold loadimm_n; destruct 1; intro RD_NOT_RA. + unfold loadimm_n; destruct 1. - econstructor; split. apply exec_straight_one. simpl; eauto. auto. split. Simpl. @@ -340,8 +293,7 @@ Proof. set (rs1 := nextinstr (rs#rd <- (Vint (Int.repr accu0)))). destruct (exec_loadimm_k_w rd k m (negate_decomposition l) (negate_decomposition_wf l H1) - RD_NOT_RA rs1 accu0) - as (rs2 & P & Q & R & S). + rs1 accu0) as (rs2 & P & Q & R). unfold rs1; Simpl. exists rs2; split. eapply exec_straight_opt_step; eauto. @@ -353,8 +305,7 @@ Proof. Qed. Lemma exec_loadimm32: - forall rd n k rs m - (RD_NOT_RA : rd <> RA), + forall rd n k rs m, exists rs', exec_straight ge fn (loadimm32 rd n k) rs m k rs' m /\ rs'#rd = Vint n @@ -377,14 +328,13 @@ Proof. 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. trivial. -+ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega. trivial. ++ 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: forall (rd: ireg) k m l, - wf_decomposition l -> - rd <> RA -> + wf_decomposition l -> forall (rs: regset) accu, rs#rd = Vlong (Int64.repr accu) -> exists rs', @@ -392,9 +342,9 @@ Lemma exec_loadimm_k_x: /\ rs'#rd = Vlong (Int64.repr (recompose_int accu l)) /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. - induction 1; intros RD_NOT_RA rs accu ACCU; simpl. + induction 1; intros rs accu ACCU; simpl. - exists rs; split. apply exec_straight_opt_refl. auto. -- destruct (IHwf_decomposition RD_NOT_RA +- destruct (IHwf_decomposition (nextinstr (rs#rd <- (insert_in_long rs#rd n p 16))) (Zinsert accu n p 16)) as (rs' & P & Q & R). @@ -408,20 +358,19 @@ Qed. Lemma exec_loadimm_z_x: forall rd l k rs m, wf_decomposition l -> - rd <> RA -> exists rs', exec_straight ge fn (loadimm_z X rd l k) rs m k rs' m /\ rs'#rd = Vlong (Int64.repr (recompose_int 0 l)) /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. - unfold loadimm_z; destruct 1; intro RD_NOT_RA. + 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 := nextinstr (rs#rd <- (Vlong (Int64.repr accu0)))). - destruct (exec_loadimm_k_x rd k m l H1 RD_NOT_RA rs1 accu0) as (rs2 & P & Q & R); auto. + 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. @@ -434,13 +383,12 @@ Qed. Lemma exec_loadimm_n_x: forall rd l k rs m, wf_decomposition l -> - rd <> RA -> exists rs', exec_straight ge fn (loadimm_n X rd l k) rs m k rs' m /\ rs'#rd = Vlong (Int64.repr (Z.lnot (recompose_int 0 l))) /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. - unfold loadimm_n; destruct 1; intro RD_NOT_RA. + unfold loadimm_n; destruct 1. - econstructor; split. apply exec_straight_one. simpl; eauto. auto. split. Simpl. @@ -449,7 +397,7 @@ Proof. set (rs1 := nextinstr (rs#rd <- (Vlong (Int64.repr accu0)))). destruct (exec_loadimm_k_x rd k m (negate_decomposition l) (negate_decomposition_wf l H1) - RD_NOT_RA rs1 accu0) as (rs2 & P & Q & R). + rs1 accu0) as (rs2 & P & Q & R). unfold rs1; Simpl. exists rs2; split. eapply exec_straight_opt_step; eauto. @@ -462,13 +410,12 @@ Qed. Lemma exec_loadimm64: forall rd n k rs m, - rd <> RA -> exists rs', exec_straight ge fn (loadimm64 rd n k) rs m k rs' m /\ rs'#rd = Vlong n /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. - unfold loadimm64, loadimm; intros until m; intro RD_NOT_RA. + unfold loadimm64, loadimm; intros. destruct (is_logical_imm64 n). - econstructor; split. apply exec_straight_one. simpl; eauto. auto. @@ -485,8 +432,8 @@ Proof. 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. trivial. -+ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega. trivial. ++ 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 *) @@ -498,59 +445,55 @@ Lemma exec_addimm_aux_32: Next (nextinstr (rs#rd <- (sem rs#r1 (Vint (Int.repr n))))) m) -> (forall v n1 n2, sem (sem v (Vint n1)) (Vint n2) = sem v (Vint (Int.add n1 n2))) -> forall rd r1 n k rs m, - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> exists rs', exec_straight ge fn (addimm_aux insn rd r1 (Int.unsigned n) k) rs m k rs' m /\ rs'#rd = sem rs#r1 (Vint n) - /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r) - /\ rs' # RA = rs # RA. + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. - intros insn sem SEM ASSOC; intros until m; intro RD_NOT_RA. unfold addimm_aux. + intros insn sem SEM ASSOC; intros. unfold addimm_aux. set (nlo := Zzero_ext 12 (Int.unsigned n)). set (nhi := Int.unsigned n - nlo). 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. - split; intros; Simpl. + intros; Simpl. - econstructor; split. apply exec_straight_one. apply SEM. Simpl. split. Simpl. do 3 f_equal; omega. - split; intros; Simpl. + intros; Simpl. - econstructor; split. eapply exec_straight_two. apply SEM. apply SEM. Simpl. Simpl. split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int.eqm_samerepr. rewrite E. auto with ints. - split; intros; Simpl. + intros; Simpl. Qed. Lemma exec_addimm32: forall rd r1 n k rs m, r1 <> X16 -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> exists rs', exec_straight ge fn (addimm32 rd r1 n k) rs m k rs' m /\ rs'#rd = Val.add rs#r1 (Vint n) - /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r) - /\ rs' # RA = rs # RA. + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. 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. +- 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. + 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). congruence. + 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. - split; intros; Simpl. -+ edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). congruence. + 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. - split; intros; Simpl. + intros; Simpl. Qed. Lemma exec_addimm_aux_64: @@ -560,12 +503,10 @@ Lemma exec_addimm_aux_64: Next (nextinstr (rs#rd <- (sem rs#r1 (Vlong (Int64.repr n))))) m) -> (forall v n1 n2, sem (sem v (Vlong n1)) (Vlong n2) = sem v (Vlong (Int64.add n1 n2))) -> forall rd r1 n k rs m, - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> exists rs', exec_straight ge fn (addimm_aux insn rd r1 (Int64.unsigned n) k) rs m k rs' m /\ rs'#rd = sem rs#r1 (Vlong n) - /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r) - /\ rs' # RA = rs # RA. + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. intros insn sem SEM ASSOC; intros. unfold addimm_aux. set (nlo := Zzero_ext 12 (Int64.unsigned n)). set (nhi := Int64.unsigned n - nlo). @@ -574,46 +515,44 @@ Proof. 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. - split; intros; Simpl. + intros; Simpl. - econstructor; split. apply exec_straight_one. apply SEM. Simpl. split. Simpl. do 3 f_equal; omega. - split; intros; Simpl. + 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. - split; intros; Simpl. + intros; Simpl. Qed. Lemma exec_addimm64: forall rd r1 n k rs m, preg_of_iregsp r1 <> X16 -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> exists rs', exec_straight ge fn (addimm64 rd r1 n k) rs m k rs' m /\ rs'#rd = Val.addl rs#r1 (Vlong n) - /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r) - /\ rs' # RA = rs # RA. + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. 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. +- 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. + 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). congruence. + 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. - split; intros; Simpl. -+ edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). congruence. + 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. - split; intros; Simpl. + intros; Simpl. Qed. (** Logical immediate *) @@ -630,25 +569,22 @@ Lemma exec_logicalimm32: Next (nextinstr (rs#rd <- (sem rs##r1 (eval_shift_op_int rs#r2 s)))) m) -> forall rd r1 n k rs m, r1 <> X16 -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> exists rs', exec_straight ge fn (logicalimm32 insn1 insn2 rd r1 n k) rs m k rs' m /\ rs'#rd = sem rs#r1 (Vint n) - /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r) - /\ rs' # RA = rs # RA. + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. intros until sem; intros SEM1 SEM2; intros. unfold logicalimm32. destruct (is_logical_imm32 n). - econstructor; split. apply exec_straight_one. apply SEM1. reflexivity. - split. Simpl. rewrite Int.repr_unsigned; auto. - split; intros; Simpl. -- edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). congruence. + 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. reflexivity. split. Simpl. f_equal; auto. apply C; auto with asmgen. - split; intros; Simpl. + intros; Simpl. Qed. Lemma exec_logicalimm64: @@ -663,58 +599,50 @@ Lemma exec_logicalimm64: Next (nextinstr (rs#rd <- (sem rs###r1 (eval_shift_op_long rs#r2 s)))) m) -> forall rd r1 n k rs m, r1 <> X16 -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> exists rs', exec_straight ge fn (logicalimm64 insn1 insn2 rd r1 n k) rs m k rs' m /\ rs'#rd = sem rs#r1 (Vlong n) - /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r) - /\ rs' # RA = rs # RA. + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. intros until sem; intros SEM1 SEM2; intros. unfold logicalimm64. destruct (is_logical_imm64 n). - econstructor; split. apply exec_straight_one. apply SEM1. reflexivity. - split. Simpl. rewrite Int64.repr_unsigned. auto. - split; intros; Simpl. -- edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). congruence. + 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. reflexivity. split. Simpl. f_equal; auto. apply C; auto with asmgen. - split; intros; Simpl. + intros; Simpl. Qed. (** Load address of symbol *) Lemma exec_loadsymbol: forall rd s ofs k rs m, - rd <> X16 \/ Archi.pic_code tt = false -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> + rd <> X16 \/ Archi.pic_code tt = false -> exists rs', exec_straight ge fn (loadsymbol rd s ofs k) rs m k rs' m /\ rs'#rd = Genv.symbol_address ge s ofs - /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r) - /\ rs'#RA = rs#RA. + /\ 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 | reflexivity]. - split. Simpl. split; intros; Simpl. - + split. Simpl. intros; Simpl. + exploit exec_addimm64. instantiate (1 := rd). simpl. destruct H; congruence. - instantiate (1 := rd). assumption. - intros (rs1 & A & B & C & D). + 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. - split; intros. rewrite C by auto; Simpl. - rewrite D. Simpl. + intros. rewrite C by auto. Simpl. - econstructor; split. eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. split. Simpl. rewrite symbol_high_low; auto. - split; intros; Simpl. + intros; Simpl. Qed. (** Shifted operands *) @@ -823,25 +751,23 @@ Lemma exec_arith_extended: Next (nextinstr (rs#rd <- (sem rs###r1 (eval_shift_op_long rs#r2 s)))) m) -> forall (rd r1 r2: ireg) (ex: extension) (a: amount64) (k: code) rs m, r1 <> X16 -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> exists rs', exec_straight ge fn (arith_extended insnX insnS rd r1 r2 ex a k) rs m k rs' m /\ rs'#rd = sem rs#r1 (Op.eval_extend ex rs#r2 a) - /\ (forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r) - /\ rs' # RA = rs # RA. + /\ 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. - split; intros; Simpl. + 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 ir0x. rewrite C by eauto with asmgen. f_equal. rewrite B. destruct ex; auto. - split; intros; Simpl. + intros; Simpl. Qed. (** Extended right shift *) @@ -1236,56 +1162,6 @@ Ltac ArgsInv := | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in * end). -Lemma compare_int_RA: - forall rs a b m, - compare_int rs a b m X30 = rs X30. -Proof. - unfold compare_int. - intros. - repeat rewrite Pregmap.gso by congruence. - trivial. -Qed. - -Hint Resolve compare_int_RA : asmgen. - -Lemma compare_long_RA: - forall rs a b m, - compare_long rs a b m X30 = rs X30. -Proof. - unfold compare_long. - intros. - repeat rewrite Pregmap.gso by congruence. - trivial. -Qed. - -Hint Resolve compare_long_RA : asmgen. - -Lemma compare_float_RA: - forall rs a b, - compare_float rs a b X30 = rs X30. -Proof. - unfold compare_float. - intros. - destruct a; destruct b. - all: repeat rewrite Pregmap.gso by congruence; trivial. -Qed. - -Hint Resolve compare_float_RA : asmgen. - - -Lemma compare_single_RA: - forall rs a b, - compare_single rs a b X30 = rs X30. -Proof. - unfold compare_single. - intros. - destruct a; destruct b. - all: repeat rewrite Pregmap.gso by congruence; trivial. -Qed. - -Hint Resolve compare_single_RA : asmgen. - - Lemma transl_cond_correct: forall cond args k c rs m, transl_cond cond args k = OK c -> @@ -1294,218 +1170,185 @@ Lemma transl_cond_correct: /\ (forall b, eval_condition cond (map rs (map preg_of args)) m = Some b -> eval_testcond (cond_for_cond cond) rs' = Some b) - /\ (forall r, data_preg r = true -> rs'#r = rs#r) - /\ rs' # RA = rs # RA. + /\ 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. auto. - repeat split; intros. apply eval_testcond_compare_sint; auto. + split; intros. apply eval_testcond_compare_sint; auto. destruct r; reflexivity || discriminate. - (* Ccompu *) econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. apply eval_testcond_compare_uint; 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. - repeat split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; 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. - repeat split; intros. apply eval_testcond_compare_sint; auto. + split; intros. apply eval_testcond_compare_sint; auto. destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). congruence. intros (rs' & A & B & C). ++ 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. - repeat split; intros. apply eval_testcond_compare_sint; auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. - auto with asmgen. - Simpl. rewrite compare_int_RA. - apply C; congruence. + 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. - repeat split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_uint; 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. - repeat split; intros. apply eval_testcond_compare_uint; auto. + split; intros. apply eval_testcond_compare_uint; auto. destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). congruence. intros (rs' & A & B & C). ++ 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. - repeat split; intros. apply eval_testcond_compare_uint; auto. + split; intros. apply eval_testcond_compare_uint; auto. transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_int_RA. - apply C; congruence. - (* Ccompshift *) econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; 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. - repeat split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; 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. - repeat split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto. + split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto. destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). congruence. intros (rs' & A & B & C). ++ 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. - repeat split; intros. apply (eval_testcond_compare_sint Ceq); auto. + split; intros. apply (eval_testcond_compare_sint Ceq); auto. transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_int_RA. - apply C; congruence. - - (* Cmasknotzero *) destruct (is_logical_imm32 n). + econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto. + split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto. destruct r; reflexivity || discriminate. - -+ exploit (exec_loadimm32 X16 n). congruence. intros (rs' & A & B & C). ++ 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. - repeat split; intros. apply (eval_testcond_compare_sint Cne); auto. + split; intros. apply (eval_testcond_compare_sint Cne); auto. transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_int_RA. - apply C; congruence. - - (* Ccompl *) econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. apply eval_testcond_compare_slong; auto. + split; intros. apply eval_testcond_compare_slong; auto. destruct r; reflexivity || discriminate. - (* Ccomplu *) econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. apply eval_testcond_compare_ulong; auto. + split; intros. apply eval_testcond_compare_ulong; auto. 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. - repeat split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; 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. auto. - repeat split; intros. apply eval_testcond_compare_slong; auto. + split; intros. apply eval_testcond_compare_slong; auto. destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). congruence. intros (rs' & A & B & C). ++ 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. - repeat split; intros. apply eval_testcond_compare_slong; auto. + split; intros. apply eval_testcond_compare_slong; auto. transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_long_RA. - apply C; congruence. - - (* Ccompluimm *) destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto. + split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto. destruct r; reflexivity || discriminate. + econstructor; split. apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. auto. - repeat split; intros. apply eval_testcond_compare_ulong; auto. + split; intros. apply eval_testcond_compare_ulong; auto. destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). congruence. intros (rs' & A & B & C). ++ 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. - repeat split; intros. apply eval_testcond_compare_ulong; auto. + split; intros. apply eval_testcond_compare_ulong; auto. transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_long_RA. - apply C; congruence. - - (* Ccomplshift *) econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto. + 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. auto. - repeat split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto. + split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto. destruct r; reflexivity || discriminate. - (* Cmasklzero *) destruct (is_logical_imm64 n). + econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto. + split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto. destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). congruence. intros (rs' & A & B & C). ++ 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. - repeat split; intros. apply (eval_testcond_compare_slong Ceq); auto. + split; intros. apply (eval_testcond_compare_slong Ceq); auto. transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_long_RA. - apply C; congruence. - - (* Cmasknotzero *) destruct (is_logical_imm64 n). + econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto. + split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto. destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). congruence. intros (rs' & A & B & C). ++ 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. - repeat split; intros. apply (eval_testcond_compare_slong Cne); auto. + split; intros. apply (eval_testcond_compare_slong Cne); auto. transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_long_RA. - apply C; congruence. - - (* Ccompf *) econstructor; split. apply exec_straight_one. simpl; eauto. rewrite compare_float_inv; auto. - repeat split; intros. apply eval_testcond_compare_float; auto. + split; intros. apply eval_testcond_compare_float; auto. destruct r; discriminate || rewrite compare_float_inv; auto. - Simpl. - (* Cnotcompf *) econstructor; split. apply exec_straight_one. simpl; eauto. rewrite compare_float_inv; auto. - repeat split; intros. apply eval_testcond_compare_not_float; auto. + split; intros. apply eval_testcond_compare_not_float; auto. destruct r; discriminate || rewrite compare_float_inv; auto. - Simpl. - (* Ccompfzero *) econstructor; split. apply exec_straight_one. simpl; eauto. rewrite compare_float_inv; auto. - repeat split; intros. apply eval_testcond_compare_float; auto. + split; intros. apply eval_testcond_compare_float; auto. destruct r; discriminate || rewrite compare_float_inv; auto. - Simpl. - (* Cnotcompfzero *) econstructor; split. apply exec_straight_one. simpl; eauto. rewrite compare_float_inv; auto. - repeat split; intros. apply eval_testcond_compare_not_float; auto. + split; intros. apply eval_testcond_compare_not_float; auto. destruct r; discriminate || rewrite compare_float_inv; auto. - Simpl. - (* Ccompfs *) econstructor; split. apply exec_straight_one. simpl; eauto. rewrite compare_single_inv; auto. - repeat split; intros. apply eval_testcond_compare_single; auto. + split; intros. apply eval_testcond_compare_single; auto. destruct r; discriminate || rewrite compare_single_inv; auto. - Simpl. - (* Cnotcompfs *) econstructor; split. apply exec_straight_one. simpl; eauto. rewrite compare_single_inv; auto. - repeat split; intros. apply eval_testcond_compare_not_single; auto. + split; intros. apply eval_testcond_compare_not_single; auto. destruct r; discriminate || rewrite compare_single_inv; auto. - Simpl. - (* Ccompfszero *) econstructor; split. apply exec_straight_one. simpl; eauto. rewrite compare_single_inv; auto. - repeat split; intros. apply eval_testcond_compare_single; auto. + split; intros. apply eval_testcond_compare_single; auto. destruct r; discriminate || rewrite compare_single_inv; auto. - Simpl. - (* Cnotcompfszero *) econstructor; split. apply exec_straight_one. simpl; eauto. rewrite compare_single_inv; auto. - repeat split; intros. apply eval_testcond_compare_not_single; auto. + split; intros. apply eval_testcond_compare_not_single; auto. destruct r; discriminate || rewrite compare_single_inv; auto. - Simpl. Qed. (** Translation of conditional branches *) @@ -1518,8 +1361,7 @@ Lemma transl_cond_branch_correct: exec_straight_opt ge fn c rs m (insn :: k) rs' m /\ exec_instr ge fn insn rs' m = (if b then goto_label fn lbl rs' m else Next (nextinstr rs') m) - /\ (forall r, data_preg r = true -> rs'#r = rs#r) - /\ rs' # RA = rs # RA. + /\ forall r, data_preg r = true -> rs'#r = rs#r. Proof. intros until b; intros TR EV. assert (DFL: @@ -1528,14 +1370,13 @@ Proof. exec_straight_opt ge fn c rs m (insn :: k) rs' m /\ exec_instr ge fn insn rs' m = (if b then goto_label fn lbl rs' m else Next (nextinstr rs') m) - /\ (forall r, data_preg r = true -> rs'#r = rs#r) - /\ rs' # RA = rs # RA ). + /\ forall r, data_preg r = true -> rs'#r = rs#r). { unfold transl_cond_branch_default; intros. - exploit transl_cond_correct; eauto. intros (rs' & A & B & C & D). + exploit transl_cond_correct; eauto. intros (rs' & A & B & C). exists rs', (Pbc (cond_for_cond cond) lbl); split. apply exec_straight_opt_intro. eexact A. - repeat split; auto. simpl. rewrite (B b) by auto. auto. + split; auto. simpl. rewrite (B b) by auto. auto. } Local Opaque transl_cond transl_cond_branch_default. destruct args as [ | a1 args]; simpl in TR; auto. @@ -1629,15 +1470,13 @@ Ltac TranslOpSimpl := [ apply exec_straight_one; [simpl; eauto | reflexivity] | split; [ rewrite ? transl_eval_shift, ? transl_eval_shiftl; apply Val.lessdef_same; Simpl; fail - | split; [ intros; Simpl; fail - | intros; Simpl; eauto with asmgen; fail] ]]. + | intros; Simpl; fail ] ]. Ltac TranslOpBase := econstructor; split; [ apply exec_straight_one; [simpl; eauto | reflexivity] | split; [ rewrite ? transl_eval_shift, ? transl_eval_shiftl; Simpl - | split; [ intros; Simpl; fail - | intros; Simpl; eapply RA_not_written2; eauto] ]]. + | intros; Simpl; fail ] ]. Lemma transl_op_correct: forall op args res k (rs: regset) m v c, @@ -1646,29 +1485,21 @@ Lemma transl_op_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ Val.lessdef v rs'#(preg_of res) - /\ (forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r) - /\ rs' RA = rs RA. + /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r. Proof. 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. - (* move *) destruct (preg_of res) eqn:RR; try discriminate; destruct (preg_of m0) eqn:R1; inv TR. - all: TranslOpSimpl. ++ TranslOpSimpl. ++ TranslOpSimpl. - (* intconst *) - exploit exec_loadimm32. apply (ireg_of_not_RA res); eassumption. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. - split. intros; auto with asmgen. - apply C. congruence. - eapply ireg_of_not_RA''; eauto. + 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. apply (ireg_of_not_RA res); eassumption. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. - split. intros; auto with asmgen. - apply C. congruence. - eapply ireg_of_not_RA''; eauto. + 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. @@ -1678,15 +1509,11 @@ Local Opaque Int.eq Int64.eq Val.add Val.addl Int.zwordsize Int64.zwordsize. + subst n. TranslOpSimpl. + TranslOpSimpl. - (* loadsymbol *) - exploit (exec_loadsymbol x id ofs). eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - exists rs'; split. eexact A. split. rewrite B; auto. - split; auto. + 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)). simpl; eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). + intros (rs' & A & B & C). exists rs'; split. eexact A. split. simpl in B; rewrite B. Local Transparent Val.addl. destruct (rs SP); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto. @@ -1694,8 +1521,7 @@ Local Transparent Val.addl. - (* shift *) rewrite <- transl_eval_shift'. TranslOpSimpl. - (* addimm *) - exploit (exec_addimm32 x x0 n). eauto with asmgen. eapply ireg_of_not_RA''; eassumption. - intros (rs' & A & B & C & D). + 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. @@ -1703,20 +1529,18 @@ 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. apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - exists rs'; split. eexact A. split. rewrite B; auto. - split; auto. + 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. apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - exists rs'; split. eexact A. split. rewrite B; auto. - split; auto. + 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. apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). + 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. @@ -1728,16 +1552,15 @@ Local Transparent Val.add. destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL. { exploit (exec_shrx32 x x0 n); eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - econstructor; split. eexact A. split. rewrite B; auto. - split; auto. + intros (rs' & A & B & C & D). + econstructor; split. eexact A. split. rewrite B; auto. + auto. } exploit (exec_shrx32_none x x0 n); eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption. intros (rs' & A & B & C). econstructor; split. { eexact A. } split. { cbn. constructor. } - split; auto. - + auto. - (* zero-ext *) TranslOpBase. destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto. @@ -1761,47 +1584,36 @@ Local Transparent Val.add. - (* extend *) exploit (exec_move_extended x0 x1 x a k). intros (rs' & A & B & C). econstructor; split. eexact A. - split. rewrite B; auto. - split; eauto with asmgen. + split. rewrite B; auto. eauto with asmgen. - (* addext *) exploit (exec_arith_extended Val.addl Paddext (Padd X)). - auto. auto. instantiate (1 := x1). eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - econstructor; split. eexact A. split. rewrite B; auto. - split; auto. + 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. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). + intros (rs' & A & B & C). exists rs'; split. eexact A. split. simpl in B; rewrite B; auto. auto. - (* subext *) exploit (exec_arith_extended Val.subl Psubext (Psub X)). - auto. auto. instantiate (1 := x1). eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - econstructor; split. eexact A. split. rewrite B; auto. - split; auto. + 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. - (* andlimm *) exploit (exec_logicalimm64 (Pandimm X) (Pand X)). intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). + intros (rs' & A & B & C). exists rs'; split. eexact A. split. rewrite B; auto. auto. - (* orlimm *) exploit (exec_logicalimm64 (Porrimm X) (Porr X)). intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). + intros (rs' & A & B & C). exists rs'; split. eexact A. split. rewrite B; auto. auto. - (* xorlimm *) exploit (exec_logicalimm64 (Peorimm X) (Peor X)). intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). + intros (rs' & A & B & C). exists rs'; split. eexact A. split. rewrite B; auto. auto. - (* notl *) TranslOpBase. @@ -1809,7 +1621,7 @@ Local Transparent Val.add. - (* notlshift *) TranslOpBase. destruct (eval_shiftl s (rs x0) a); auto. simpl. rewrite Int64.or_zero_l; auto. -- (* shrx *) +- (* shrxl *) destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL. { exploit (exec_shrx64 x x0 n); eauto with asmgen. @@ -1820,8 +1632,7 @@ Local Transparent Val.add. intros (rs' & A & B & C). econstructor; split. { eexact A. } split. { cbn. constructor. } - split; auto. - + auto. - (* zero-ext-l *) TranslOpBase. destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto. @@ -1841,37 +1652,35 @@ Local Transparent Val.add. 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 & D). + 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. - split; intros; Simpl. + intros; Simpl. - (* select *) destruct (preg_of res) 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 & D). + 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. rewrite !C. apply Val.lessdef_normalize. rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. auto. - split; intros; Simpl. - rewrite <- D. - eapply RA_not_written2; eassumption. + 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 & D). + 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. rewrite !C. apply Val.lessdef_normalize. rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. auto. - split; intros; Simpl. + intros; Simpl. Qed. (** Translation of addressing modes, loads, stores *) @@ -1883,8 +1692,7 @@ Lemma transl_addressing_correct: exists ad rs', exec_straight_opt ge fn c rs m (insn ad :: k) rs' m /\ Asm.eval_addressing ge ad rs' = Vptr b o - /\ (forall r, data_preg r = true -> rs' r = rs r) - /\ rs' # RA = rs # RA. + /\ forall r, data_preg r = true -> rs' r = rs r. Proof. intros until o; intros TR EV. unfold transl_addressing in TR; destruct addr; ArgsInv; SimplEval EV. @@ -1892,10 +1700,10 @@ Proof. destruct (offset_representable sz ofs); inv EQ0. + econstructor; econstructor; split. apply exec_straight_opt_refl. auto. -+ exploit (exec_loadimm64 X16 ofs). congruence. intros (rs' & A & B & C). ++ 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. - split; eauto with asmgen. + eauto with asmgen. - (* Aindexed2 *) econstructor; econstructor; split. apply exec_straight_opt_refl. auto. @@ -1911,38 +1719,33 @@ Proof. + econstructor; econstructor; split. apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. auto. split. simpl. Simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero. auto. - split; intros; Simpl. + 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. - instantiate (1 := X16). simpl. congruence. - intros (rs' & A & B & C & D). + 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. - split; intros. - apply C; eauto with asmgen. - trivial. + 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. auto. split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence. - split; intros; Simpl. -+ exploit (exec_loadsymbol X16 id ofs). auto. - simpl. congruence. - intros (rs' & A & B & C & D). + 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. - split; auto with asmgen. + 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. @@ -1950,9 +1753,7 @@ Proof. 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)). - simpl. congruence. - intros (rs' & A & B & C). ++ 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. @@ -1967,10 +1768,9 @@ Lemma transl_load_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of dst) = v - /\ (forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r) - /\ rs' # RA = rs # RA. + /\ forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r. Proof. - intros. destruct vaddr; try discriminate. + intros. destruct vaddr; try discriminate. assert (A: exists sz insn, transl_addressing sz addr args insn k = OK c /\ (forall ad rs', exec_instr ge fn (insn ad) rs' m = @@ -1981,17 +1781,14 @@ Proof. do 2 econstructor; (split; [eassumption|auto]). } destruct A as (sz & insn & B & C). - exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R & S). + exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R). assert (X: exec_load ge chunk (fun v => v) ad (preg_of dst) rs' m = Next (nextinstr (rs'#(preg_of dst) <- v)) m). { unfold exec_load. rewrite Q, H1. auto. } econstructor; split. eapply exec_straight_opt_right. eexact P. apply exec_straight_one. rewrite C, X; eauto. Simpl. - split. Simpl. - split; intros; Simpl. - rewrite <- S. - apply RA_not_written. + split. Simpl. intros; Simpl. Qed. Lemma transl_store_correct: @@ -2001,8 +1798,7 @@ Lemma transl_store_correct: Mem.storev chunk m vaddr rs#(preg_of src) = Some m' -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ (forall r, data_preg r = true -> rs' r = rs r) - /\ rs' # RA = rs # RA. + /\ forall r, data_preg r = true -> rs' r = rs r. Proof. intros. destruct vaddr; try discriminate. set (chunk' := match chunk with Mint8signed => Mint8unsigned @@ -2018,7 +1814,7 @@ Proof. do 2 econstructor; (split; [eassumption|auto]). } destruct A as (sz & insn & B & C). - exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R & S). + exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R). assert (X: Mem.storev chunk' m (Vptr b i) rs#(preg_of src) = Some m'). { rewrite <- H1. unfold chunk'. destruct chunk; auto; simpl; symmetry. apply Mem.store_signed_unsigned_8. @@ -2029,7 +1825,7 @@ Proof. econstructor; split. eapply exec_straight_opt_right. eexact P. apply exec_straight_one. rewrite C, Y; eauto. Simpl. - split; intros; Simpl. + intros; Simpl. Qed. (** Translation of indexed memory accesses *) @@ -2047,9 +1843,7 @@ Proof. { 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. - simpl. congruence. - intros (rs' & A & B & C). +- 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 by eauto with asmgen. auto. auto. Qed. @@ -2060,7 +1854,7 @@ Lemma loadptr_correct: forall (base: iregsp) ofs dst k m v (rs: regset), exists rs', exec_straight ge fn (loadptr base ofs dst k) rs m k rs' m /\ rs'#dst = v - /\ (forall r, r <> PC -> r <> X16 -> r <> dst -> rs' r = rs r). + /\ forall r, r <> PC -> r <> X16 -> r <> dst -> rs' r = rs r. Proof. intros. destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate. @@ -2068,8 +1862,7 @@ Proof. econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. simpl. unfold exec_load. rewrite B, H. eauto. auto. - split. Simpl. - intros; Simpl. + split. Simpl. intros; Simpl. Qed. Lemma storeptr_correct: forall (base: iregsp) ofs (src: ireg) k m m' (rs: regset), @@ -2078,8 +1871,7 @@ Lemma storeptr_correct: forall (base: iregsp) ofs (src: ireg) k m m' (rs: regset src <> X16 -> exists rs', exec_straight ge fn (storeptr src base ofs k) rs m k rs' m' - /\ (forall r, r <> PC -> r <> X16 -> rs' r = rs r) - /\ rs' RA = rs RA. + /\ forall r, r <> PC -> r <> X16 -> rs' r = rs r. Proof. intros. destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate. @@ -2087,7 +1879,7 @@ Proof. econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. simpl. unfold exec_store. rewrite B, C, H by eauto with asmgen. eauto. auto. - split; intros; Simpl. + intros; Simpl. Qed. Lemma loadind_correct: forall (base: iregsp) ofs ty dst k c (rs: regset) m v, @@ -2097,8 +1889,7 @@ Lemma loadind_correct: forall (base: iregsp) ofs ty dst k c (rs: regset) m v, exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of dst) = v - /\ (forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r) - /\ rs' RA = rs RA. + /\ forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r. Proof. intros. destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate. @@ -2114,10 +1905,7 @@ Proof. econstructor; split. eapply exec_straight_opt_right. eexact A. apply exec_straight_one. rewrite SEM. unfold exec_load. rewrite B, H0. eauto. Simpl. - split. Simpl. - split. intros; Simpl. - Simpl. rewrite RA_not_written. - apply C; congruence. + split. Simpl. intros; Simpl. Qed. Lemma storeind_correct: forall (base: iregsp) ofs ty src k c (rs: regset) m m', @@ -2126,8 +1914,7 @@ Lemma storeind_correct: forall (base: iregsp) ofs ty src k c (rs: regset) m m', preg_of_iregsp base <> IR X16 -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ (forall r, data_preg r = true -> rs' r = rs r) - /\ rs' RA = rs RA. + /\ forall r, data_preg r = true -> rs' r = rs r. Proof. intros. destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate. @@ -2145,15 +1932,13 @@ Proof. apply exec_straight_one. rewrite SEM. unfold exec_store. rewrite B, C, H0 by eauto with asmgen. eauto. Simpl. - split. intros; Simpl. - Simpl. + intros; Simpl. Qed. Lemma make_epilogue_correct: forall ge0 f m stk soff cs m' ms rs k tm, - (is_leaf_function f = true -> rs # (IR RA) = parent_ra cs) -> load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) -> - ((* FIXME is_leaf_function f = false -> *) load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs)) -> + load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> agree ms (Vptr stk soff) rs -> Mem.extends m tm -> @@ -2164,46 +1949,18 @@ Lemma make_epilogue_correct: /\ Mem.extends m' tm' /\ rs'#RA = parent_ra cs /\ rs'#SP = parent_sp cs - /\ (forall r, r <> PC -> r <> SP -> r <> RA -> r <> X16 -> rs'#r = rs#r). + /\ (forall r, r <> PC -> r <> SP -> r <> X30 -> r <> X16 -> rs'#r = rs#r). Proof. - intros until tm; intros LEAF_RA LP LRA FREE AG MEXT MCS. - - (* FIXME - Cannot be used at this point - destruct (is_leaf_function f) eqn:IS_LEAF. - { - exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP'). - exploit lessdef_parent_sp; eauto. intros EQ; subst parent'; clear LDP'. - exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT'). - unfold make_epilogue. - rewrite IS_LEAF. - - econstructor; econstructor; split. - apply exec_straight_one. simpl. - rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'. - rewrite FREE'. eauto. auto. - split. apply agree_nextinstr. apply agree_set_other; auto. - apply agree_change_sp with (Vptr stk soff). - apply agree_exten with rs; auto. - eapply parent_sp_def; eauto. - split. auto. - split. Simpl. - split. Simpl. - intros. Simpl. - } - lapply LRA. 2: reflexivity. - clear LRA. intro LRA. *) + intros until tm; intros LP LRA FREE AG MEXT MCS. exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP'). exploit Mem.loadv_extends. eauto. eexact LRA. auto. simpl. intros (ra' & LRA' & LDRA'). exploit lessdef_parent_sp; eauto. intros EQ; subst parent'; clear LDP'. exploit lessdef_parent_ra; eauto. intros EQ; subst ra'; clear LDRA'. exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT'). - unfold make_epilogue. - (* FIXME rewrite IS_LEAF. *) + unfold make_epilogue. exploit (loadptr_correct XSP (fn_retaddr_ofs f)). instantiate (2 := rs). simpl. rewrite <- (sp_val _ _ _ AG). simpl. eexact LRA'. simpl; congruence. intros (rs1 & A1 & B1 & C1). - econstructor; econstructor; split. eapply exec_straight_trans. eexact A1. apply exec_straight_one. simpl. simpl; rewrite (C1 SP) by auto with asmgen. rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'. |