diff options
Diffstat (limited to 'riscV/Asmgenproof1.v')
| -rw-r--r-- | riscV/Asmgenproof1.v | 919 |
1 files changed, 895 insertions, 24 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index faa066b0..2293e001 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -129,6 +129,22 @@ 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) @@ -179,6 +195,27 @@ 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) @@ -253,6 +290,102 @@ 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 @@ -284,46 +417,219 @@ 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. - 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; + - 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. rewrite HB; destruct b; simpl; auto. - - assert (HB: (Int.eq i Int.zero) = b) by congruence. + + rewrite EQRS; + assert (HB: (Int.eq i Int.zero) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - - destruct (rs x0); try congruence. + + rewrite EQRS; + destruct (rs x0); try congruence. assert (HB: (Int.eq i i0) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - - assert (HB: negb (Int.eq Int.zero i) = b) by congruence. +- 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. rewrite HB; destruct b; simpl; auto. - - assert (HB: negb (Int.eq i Int.zero) = b) by congruence. + + rewrite EQRS; + assert (HB: negb (Int.eq i Int.zero) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - - destruct (rs x0); try congruence. + + rewrite EQRS; + destruct (rs x0); try congruence. assert (HB: negb (Int.eq i i0) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - - assert (HB: (Int64.eq Int64.zero i) = b) by congruence. +- 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. rewrite HB; destruct b; simpl; auto. - - assert (HB: (Int64.eq i Int64.zero) = b) by congruence. + + rewrite EQRS; + assert (HB: (Int64.eq i Int64.zero) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - - destruct (rs x0); try congruence. + + rewrite EQRS; + destruct (rs x0); try congruence. assert (HB: (Int64.eq i i0) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - - assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence. +- 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. rewrite HB; destruct b; simpl; auto. - - assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. + + rewrite EQRS; + assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. rewrite <- HB; destruct b; simpl; auto. - - destruct (rs x0); try congruence. + + rewrite EQRS; + 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: @@ -357,6 +663,417 @@ 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 := @@ -386,6 +1103,28 @@ 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))). @@ -402,6 +1141,138 @@ 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; |