From 18312f0470cfb96e44ae1a26a24710cc1df3440d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 9 Apr 2021 15:15:57 +0200 Subject: Removing expansions from Asmgen --- riscV/Asmgenproof1.v | 919 ++------------------------------------------------- 1 file changed, 24 insertions(+), 895 deletions(-) (limited to 'riscV/Asmgenproof1.v') diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 2293e001..faa066b0 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -129,22 +129,6 @@ Proof. intros; Simpl. Qed. -Lemma loadimm32_correct: - 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 - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - unfold loadimm32; intros. generalize (make_immed32_sound n); intros E. - destruct (make_immed32 n). -- subst imm. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. rewrite Int.add_zero_l; Simpl. - intros; Simpl. -- rewrite E. apply load_hilo32_correct. -Qed. - Lemma opimm32_correct: forall (op: ireg -> ireg0 -> ireg0 -> instruction) (opi: ireg -> ireg0 -> int -> instruction) @@ -195,27 +179,6 @@ Proof. intros; Simpl. Qed. -Lemma loadimm64_correct: - forall rd n k rs m, - 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 -> r <> X31 -> rs'#r = rs#r. -Proof. - unfold loadimm64; intros. generalize (make_immed64_sound n); intros E. - destruct (make_immed64 n). -- subst imm. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. rewrite Int64.add_zero_l; Simpl. - intros; Simpl. -- exploit load_hilo64_correct; eauto. intros (rs' & A & B & C). - rewrite E. exists rs'; eauto. -- subst imm. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -Qed. - Lemma opimm64_correct: forall (op: ireg -> ireg0 -> ireg0 -> instruction) (opi: ireg -> ireg0 -> int64 -> instruction) @@ -290,102 +253,6 @@ Proof. rewrite H0 in B. inv B. auto. Qed. -(** Translation of conditional branches *) - -Lemma transl_cbranch_int32s_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmp_bool cmp rs##r1 rs##r2 = Some b -> - exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H. -- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H. - simpl; auto. -- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H. - simpl; auto. -- auto. -- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto. -- auto. -Qed. - -Lemma transl_cbranch_int32u_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2 = Some b -> - exec_instr ge fn (transl_cbranch_int32u cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H; auto. -- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto. -Qed. - -Lemma transl_cbranch_int64s_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmpl_bool cmp rs###r1 rs###r2 = Some b -> - exec_instr ge fn (transl_cbranch_int64s cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H. -- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H. - simpl; auto. -- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H. - simpl; auto. -- auto. -- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto. -- auto. -Qed. - -Lemma transl_cbranch_int64u_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b -> - exec_instr ge fn (transl_cbranch_int64u cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H; auto. -- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto. -Qed. - -Lemma transl_cond_float_correct: - forall (rs: regset) m cmp rd r1 r2 insn normal v, - transl_cond_float cmp rd r1 r2 = (insn, normal) -> - v = (if normal then Val.cmpf cmp rs#r1 rs#r2 else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)) -> - exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m. -Proof. - intros. destruct cmp; simpl in H; inv H; auto. -- rewrite Val.negate_cmpf_eq. auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool. - rewrite <- Float.cmp_swap. auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool. - rewrite <- Float.cmp_swap. auto. -Qed. - -Lemma transl_cond_single_correct: - forall (rs: regset) m cmp rd r1 r2 insn normal v, - transl_cond_single cmp rd r1 r2 = (insn, normal) -> - v = (if normal then Val.cmpfs cmp rs#r1 rs#r2 else Val.notbool (Val.cmpfs cmp rs#r1 rs#r2)) -> - exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m. -Proof. - intros. destruct cmp; simpl in H; inv H; auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f0 f); auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite <- Float32.cmp_swap. auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite <- Float32.cmp_swap. auto. - Qed. - -(* TODO gourdinl UNUSUED ? Remark branch_on_X31: - forall normal lbl (rs: regset) m b, - rs#X31 = Val.of_bool (eqb normal b) -> - exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. - Qed.*) - Ltac ArgsInv := repeat (match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -417,219 +284,46 @@ Proof. { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. } clear EVAL MEXT AG. destruct cond; simpl in TRANSL; ArgsInv. - - exists rs, (transl_cbranch_int32s c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int32s_correct; auto. -- exists rs, (transl_cbranch_int32u c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int32u_correct; auto. -- predSpec Int.eq Int.eq_spec n Int.zero. -+ subst n. exists rs, (transl_cbranch_int32s c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int32s_correct; auto. -+ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int32s c0 x X31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int32s_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- predSpec Int.eq Int.eq_spec n Int.zero. -+ subst n. exists rs, (transl_cbranch_int32u c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int32u_correct; auto. -+ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int32u c0 x X31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int32u_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- exists rs, (transl_cbranch_int64s c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int64s_correct; auto. -- exists rs, (transl_cbranch_int64u c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int64u_correct; auto. -- predSpec Int64.eq Int64.eq_spec n Int64.zero. -+ subst n. exists rs, (transl_cbranch_int64s c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int64s_correct; auto. -+ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int64s c0 x X31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int64s_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- predSpec Int64.eq Int64.eq_spec n Int64.zero. -+ subst n. exists rs, (transl_cbranch_int64u c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int64u_correct; auto. -+ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int64u c0 x X31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int64u_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (eqb normal b)). - { unfold v, Val.cmpf. rewrite EVAL'. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. -- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - assert (EVAL'': Val.cmpf_bool c0 (rs x) (rs x0) = Some (negb b)). - { destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. } - set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (xorb normal b)). - { unfold v, Val.cmpf. rewrite EVAL''. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (eqb normal b)). - { unfold v, Val.cmpfs. rewrite EVAL'. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - assert (EVAL'': Val.cmpfs_bool c0 (rs x) (rs x0) = Some (negb b)). - { destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. } - set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (xorb normal b)). - { unfold v, Val.cmpfs. rewrite EVAL''. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. - -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; - destruct (rs x) eqn:EQRS; simpl in *; try congruence; - inv EQ2; eexists; eexists; eauto; split; constructor; auto; - simpl in *. - + rewrite EQRS; - assert (HB: (Int.eq Int.zero i) = b) by congruence. + all: + destruct optR as [[]|]; + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; + unfold zero32, Op.zero32 in *; + unfold zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); + try (eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto; fail). + all: + destruct (rs x) eqn:EQRS; simpl in *; try congruence; + eexists; eexists; eauto; split; constructor; auto; + simpl in *; rewrite EQRS. + - assert (HB: (Int.eq Int.zero i) = b) by congruence; rewrite HB; destruct b; simpl; auto. - + rewrite EQRS; - assert (HB: (Int.eq i Int.zero) = b) by congruence. + - assert (HB: (Int.eq i Int.zero) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - + rewrite EQRS; - destruct (rs x0); try congruence. + - destruct (rs x0); try congruence. assert (HB: (Int.eq i i0) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; - destruct (rs x) eqn:EQRS; simpl in *; try congruence; - inv EQ2; eexists; eexists; eauto; split; constructor; auto; - simpl in *. - + rewrite EQRS; - assert (HB: negb (Int.eq Int.zero i) = b) by congruence. + - assert (HB: negb (Int.eq Int.zero i) = b) by congruence. rewrite HB; destruct b; simpl; auto. - + rewrite EQRS; - assert (HB: negb (Int.eq i Int.zero) = b) by congruence. + - assert (HB: negb (Int.eq i Int.zero) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - + rewrite EQRS; - destruct (rs x0); try congruence. + - destruct (rs x0); try congruence. assert (HB: negb (Int.eq i i0) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - destruct (rs x) eqn:EQRS; simpl in *; try congruence; - eexists; eexists; eauto; split; constructor; - simpl in *; auto. - + rewrite EQRS; - assert (HB: (Int64.eq Int64.zero i) = b) by congruence. + - assert (HB: (Int64.eq Int64.zero i) = b) by congruence. rewrite HB; destruct b; simpl; auto. - + rewrite EQRS; - assert (HB: (Int64.eq i Int64.zero) = b) by congruence. + - assert (HB: (Int64.eq i Int64.zero) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - + rewrite EQRS; - destruct (rs x0); try congruence. + - destruct (rs x0); try congruence. assert (HB: (Int64.eq i i0) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32 in *; inv EQ2; - destruct (rs x) eqn:EQRS; simpl in *; try congruence; - eexists; eexists; eauto; split; constructor; - simpl in *; auto. - + rewrite EQRS; - assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence. + - assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence. rewrite HB; destruct b; simpl; auto. - + rewrite EQRS; - assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. + - assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - + rewrite EQRS; - destruct (rs x0); try congruence. + - destruct (rs x0); try congruence. assert (HB: negb (Int64.eq i i0) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR as [[]|]; - unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; - unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; - try (destruct (rs x); simpl in EVAL'; discriminate; fail); - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. Qed. Lemma transl_cbranch_correct_true: @@ -663,417 +357,6 @@ Proof. intros; Simpl. Qed. -(** Translation of condition operators *) - -Lemma transl_cond_int32s_correct: - forall cmp rd r1 r2 k rs m, - exists rs', - exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m - /\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. - simpl. rewrite (Val.negate_cmp_bool Clt). - destruct (Val.cmp_bool Clt rs##r2 rs##r1) as [[]|]; auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. auto. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmp. rewrite (Val.negate_cmp_bool Clt). - destruct (Val.cmp_bool Clt rs##r1 rs##r2) as [[]|]; auto. -Qed. - -Lemma transl_cond_int32u_correct: - forall cmp rd r1 r2 k rs m, - exists rs', - exec_straight ge fn (transl_cond_int32u cmp rd r1 r2 k) rs m k rs' m - /\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs##r1 rs##r2 - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. - simpl. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cle). - destruct (Val.cmpu_bool (Mem.valid_pointer m) Cle rs##r1 rs##r2) as [[]|]; auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. auto. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmpu. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Clt). - destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt rs##r1 rs##r2) as [[]|]; auto. -Qed. - -Lemma transl_cond_int64s_correct: - forall cmp rd r1 r2 k rs m, - exists rs', - exec_straight ge fn (transl_cond_int64s cmp rd r1 r2 k) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs###r1 rs###r2)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. - simpl. rewrite (Val.negate_cmpl_bool Clt). - destruct (Val.cmpl_bool Clt rs###r2 rs###r1) as [[]|]; auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. auto. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmpl. rewrite (Val.negate_cmpl_bool Clt). - destruct (Val.cmpl_bool Clt rs###r1 rs###r2) as [[]|]; auto. -Qed. - -Lemma transl_cond_int64u_correct: - forall cmp rd r1 r2 k rs m, - exists rs', - exec_straight ge fn (transl_cond_int64u cmp rd r1 r2 k) rs m k rs' m - /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs###r1 rs###r2) - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. - simpl. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Cle). - destruct (Val.cmplu_bool (Mem.valid_pointer m) Cle rs###r1 rs###r2) as [[]|]; auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. auto. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmplu. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Clt). - destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt rs###r1 rs###r2) as [[]|]; auto. -Qed. - -Lemma transl_condimm_int32s_correct: - forall cmp rd r1 n k rs m, - r1 <> X31 -> - exists rs', - exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m - /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - intros. unfold transl_condimm_int32s. - predSpec Int.eq Int.eq_spec n Int.zero. -- subst n. exploit transl_cond_int32s_correct. intros (rs' & A & B & C). - exists rs'; eauto. -- assert (DFL: - exists rs', - exec_straight ge fn (loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)) rs m k rs' m - /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). - { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto. - intros; transitivity (rs1 r); auto. } - destruct cmp. -+ unfold xorimm32. - exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto. - unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2. - intros; transitivity (rs1 r); auto. -+ unfold xorimm32. - exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto. - unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2. - intros; transitivity (rs1 r); auto. -+ exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. rewrite B1; auto. -+ predSpec Int.eq Int.eq_spec n (Int.repr Int.max_signed). -* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. - unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. - unfold Int.lt. rewrite zlt_false. auto. - change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed. - generalize (Int.signed_range i); omega. -* exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. - rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto. - unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). - destruct (zlt (Int.signed n) (Int.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. - rewrite Int.add_signed. symmetry; apply Int.signed_repr. - assert (Int.signed n <> Int.max_signed). - { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. } - generalize (Int.signed_range n); omega. -+ apply DFL. -+ apply DFL. -Qed. - -Lemma transl_condimm_int32u_correct: - forall cmp rd r1 n k rs m, - r1 <> X31 -> - exists rs', - exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m - /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - intros. unfold transl_condimm_int32u. - predSpec Int.eq Int.eq_spec n Int.zero. -- subst n. exploit transl_cond_int32u_correct. intros (rs' & A & B & C). - exists rs'; split. eexact A. split; auto. rewrite B; auto. -- assert (DFL: - exists rs', - exec_straight ge fn (loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)) rs m k rs' m - /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). - { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int32u_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto. - intros; transitivity (rs1 r); auto. } - destruct cmp. -+ apply DFL. -+ apply DFL. -+ exploit (opimm32_correct Psltuw Psltiuw (Val.cmpu (Mem.valid_pointer m) Clt) m); eauto. - intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. rewrite B1; auto. -+ apply DFL. -+ apply DFL. -+ apply DFL. -Qed. - -Lemma transl_condimm_int64s_correct: - forall cmp rd r1 n k rs m, - r1 <> X31 -> - exists rs', - exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - intros. unfold transl_condimm_int64s. - predSpec Int64.eq Int64.eq_spec n Int64.zero. -- subst n. exploit transl_cond_int64s_correct. intros (rs' & A & B & C). - exists rs'; eauto. -- assert (DFL: - exists rs', - exec_straight ge fn (loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). - { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto. - intros; transitivity (rs1 r); auto. } - destruct cmp. -+ unfold xorimm64. - exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto. - unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2. - intros; transitivity (rs1 r); auto. -+ unfold xorimm64. - exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto. - unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2. - intros; transitivity (rs1 r); auto. -+ exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. rewrite B1; auto. -+ predSpec Int64.eq Int64.eq_spec n (Int64.repr Int64.max_signed). -* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. - unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. - unfold Int64.lt. rewrite zlt_false. auto. - change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed. - generalize (Int64.signed_range i); omega. -* exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. - rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto. - unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). - destruct (zlt (Int64.signed n) (Int64.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. - rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. - assert (Int64.signed n <> Int64.max_signed). - { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. } - generalize (Int64.signed_range n); omega. -+ apply DFL. -+ apply DFL. -Qed. - -Lemma transl_condimm_int64u_correct: - forall cmp rd r1 n k rs m, - r1 <> X31 -> - exists rs', - exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - intros. unfold transl_condimm_int64u. - predSpec Int64.eq Int64.eq_spec n Int64.zero. -- subst n. exploit transl_cond_int64u_correct. intros (rs' & A & B & C). - exists rs'; split. eexact A. split; auto. rewrite B; auto. -- assert (DFL: - exists rs', - exec_straight ge fn (loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). - { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int64u_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto. - intros; transitivity (rs1 r); auto. } - destruct cmp. -+ apply DFL. -+ apply DFL. -+ exploit (opimm64_correct Psltul Psltiul (fun v1 v2 => Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 v2)) m); eauto. - intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. rewrite B1; auto. -+ apply DFL. -+ apply DFL. -+ apply DFL. - Qed. - -Lemma transl_cond_op_correct: - forall cond rd args k c rs m, - transl_cond_op cond rd args k = OK c -> - exists rs', - exec_straight ge fn c rs m k rs' m - /\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - assert (MKTOT: forall ob, Val.of_optbool ob = Val.maketotal (option_map Val.of_bool ob)). - { destruct ob as [[]|]; reflexivity. } - intros until m; intros TR. - destruct cond; simpl in TR; ArgsInv. -+ (* cmp *) - exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. -+ (* cmpu *) - exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite B; auto. -+ (* cmpimm *) - apply transl_condimm_int32s_correct; eauto with asmgen. -+ (* cmpuimm *) - apply transl_condimm_int32u_correct; eauto with asmgen. -+ (* cmpl *) - exploit transl_cond_int64s_correct; eauto. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite MKTOT; eauto. -+ (* cmplu *) - exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto. -+ (* cmplimm *) - exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite MKTOT; eauto. -+ (* cmpluimm *) - exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite MKTOT; eauto. -+ (* cmpf *) - destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. - fold (Val.cmpf c0 (rs x) (rs x0)). - set (v := Val.cmpf c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split; intros; Simpl. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_float_correct with (v := Val.notbool v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto. -+ (* notcmpf *) - destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. - rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)). - set (v := Val.cmpf c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_float_correct with (v := v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto. - split; intros; Simpl. -+ (* cmpfs *) - destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR. - fold (Val.cmpfs c0 (rs x) (rs x0)). - set (v := Val.cmpfs c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split; intros; Simpl. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_single_correct with (v := Val.notbool v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto. -+ (* notcmpfs *) - destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR. - rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)). - set (v := Val.cmpfs c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_single_correct with (v := v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto. - split; intros; Simpl. - Qed. - -(** Some arithmetic properties. *) - -Remark cast32unsigned_from_cast32signed: - forall i, Int64.repr (Int.unsigned i) = Int64.zero_ext 32 (Int64.repr (Int.signed i)). -Proof. - intros. apply Int64.same_bits_eq; intros. - rewrite Int64.bits_zero_ext, !Int64.testbit_repr by tauto. - rewrite Int.bits_signed by tauto. fold (Int.testbit i i0). - change Int.zwordsize with 32. - destruct (zlt i0 32). auto. apply Int.bits_above. auto. -Qed. - (* Translation of arithmetic operations *) Ltac SimplEval H := @@ -1103,28 +386,6 @@ Opaque Int.eq. unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl. (* move *) { destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl. } - (* intconst *) - { exploit loadimm32_correct; eauto. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* longconst *) - { exploit loadimm64_correct; eauto. intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* floatconst *) - { destruct (Float.eq_dec n Float.zero). - + subst n. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. - + econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. } - (* singleconst *) - { destruct (Float32.eq_dec n Float32.zero). - + subst n. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. - + econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. } (* addrsymbol *) { destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)). + set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))). @@ -1141,138 +402,6 @@ Opaque Int.eq. (* stackoffset *) { exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C). exists rs'; split; eauto. auto with asmgen. } - (* cast8signed *) - { econstructor; split. - eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. - split; intros; Simpl. - assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto. - destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. } - (* cast16signed *) - { econstructor; split. - eapply exec_straight_two. simpl;eauto. simpl;eauto. auto. auto. - split; intros; Simpl. - assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. - destruct (rs x0); auto; simpl. rewrite A; simpl. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. } - (* addimm *) - { exploit (opimm32_correct Paddw Paddiw Val.add); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* andimm *) - { exploit (opimm32_correct Pandw Pandiw Val.and); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* orimm *) - exploit (opimm32_correct Porw Poriw Val.or); auto. instantiate (1 := x0); eauto with asmgen. - { intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* xorimm *) - { exploit (opimm32_correct Pxorw Pxoriw Val.xor); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* shrximm *) - { destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn. - { - exploit Val.shrx_shr_3; eauto. intros E; subst v. - destruct (Int.eq n Int.zero). - + econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. - + destruct (Int.eq n Int.one). - * econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - } - destruct (Int.eq n Int.zero). - + econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. - + destruct (Int.eq n Int.one). - * econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. } - (* longofintu *) - { econstructor; split. - eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto. - split; intros; Simpl. destruct (rs x0); auto. simpl. - assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto. - rewrite A; simpl. rewrite A. apply Val.lessdef_same. f_equal. - rewrite cast32unsigned_from_cast32signed. apply Int64.zero_ext_shru_shl. compute; auto. } - (* addlimm *) - { exploit (opimm64_correct Paddl Paddil Val.addl); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* andimm *) - { exploit (opimm64_correct Pandl Pandil Val.andl); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* orimm *) - { exploit (opimm64_correct Porl Poril Val.orl); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* xorimm *) - { exploit (opimm64_correct Pxorl Pxoril Val.xorl); auto. instantiate (1 := x0); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split; eauto. rewrite B; auto with asmgen. } - (* shrxlimm *) - { destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL. - { - exploit Val.shrxl_shrl_3; eauto. intros E; subst v. - destruct (Int.eq n Int.zero). - + econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. - + destruct (Int.eq n Int.one). - * econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - - * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - } - destruct (Int.eq n Int.zero). - + econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. - + destruct (Int.eq n Int.one). - * econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - - * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. } - (* cond *) - { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). - exists rs'; split. eexact A. eauto with asmgen. } (* Expanded instructions from RTL *) 9,10,19,20: econstructor; split; try apply exec_straight_one; simpl; eauto; -- cgit