diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-19 18:40:04 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-19 18:40:04 +0100 |
| commit | 91a07b5ef9935780942a53108ac80ef354a76248 (patch) | |
| tree | 3aeed2d658b7fc897b7ab049b9c3d57cb8c2200d | |
| parent | 3d1aea4821fb8e12d4cc99cb853befec878645da (diff) | |
| download | compcert-kvx-91a07b5ef9935780942a53108ac80ef354a76248.tar.gz compcert-kvx-91a07b5ef9935780942a53108ac80ef354a76248.zip | |
Cleanup
| -rw-r--r-- | aarch64/Asmblockgen.v | 46 | ||||
| -rw-r--r-- | aarch64/Asmblockgenproof.v | 102 | ||||
| -rw-r--r-- | aarch64/Asmblockgenproof0.v | 56 | ||||
| -rw-r--r-- | aarch64/Asmblockgenproof1.v | 1740 | ||||
| -rw-r--r-- | aarch64/Asmblockprops.v | 244 |
5 files changed, 919 insertions, 1269 deletions
diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index 325f238c..b55a1195 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -389,9 +389,6 @@ Definition arith_extended Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode := if Int.eq n Int.zero then Pmov rd r1 ::bi k -(* else if Int.eq n Int.one then - Padd W (SOlsr (Int.repr 31)) X16 r1 r1 ::bi - Porr W (SOasr n) rd XZR X16 ::bi k *) else Porr W (SOasr (Int.repr 31)) X16 XZR r1 ::bi Padd W (SOlsr (Int.sub Int.iwordsize n)) X16 r1 X16 ::bi @@ -400,9 +397,6 @@ Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode := Definition shrx64 (rd r1: ireg) (n: int) (k: bcode) : bcode := if Int.eq n Int.zero then Pmov rd r1 ::bi k -(* else if Int.eq n Int.one then - Padd X (SOlsr (Int.repr 63)) X16 r1 r1 ::bi - Porr X (SOasr n) rd XZR X16 ::bi k *) else Porr X (SOasr (Int.repr 63)) X16 XZR r1 ::bi Padd X (SOlsr (Int.sub Int64.iwordsize' n)) X16 r1 X16 ::bi @@ -1170,34 +1164,6 @@ Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_ins transl_instr_basic f i1 it1p k1 end. -(** Translation of a whole function. Note that we must check - that the generated code contains less than [2^64] instructions, - otherwise the offset part of the [PC] code pointer could wrap - around, leading to incorrect executions. *) - -(* NB Sylvain: this issue with PExpand seems specific to kvx -- and not necessary here *) -(* gen_bblocks can generate two bblocks if the ctl is a PExpand (since the PExpand must be alone in its block) *) -(* -Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instruction) := - match (extract_ctl ctl) with - | None => - (* XXX Que faire du Pnop ? *) - match c with - | nil => {| header := hd; body := Pnop::nil; exit := None |} :: nil - | i :: c => {| header := hd; body := ((i :: c) ++ extract_basic ctl); exit := None |} :: nil - end - (*| Some (i) =>*) - (*match c with*) - (*| nil => {| header := hd; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil*) - (*| _ => {| header := hd; body := c; exit := None |} *) - (*:: {| header := nil; body := nil; exit := Some (PExpand (Pbuiltin ef args res)) |} :: nil*) - (*end*) - | Some ex => {| header := hd; body := (c ++ extract_basic ctl); exit := Some ex |} :: nil - end -. -*) - -(* XXX: the simulation proof may be complex with this pattern. We may fix this later *) Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control): bblocks := match ex with | None => @@ -1262,23 +1228,11 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: end . -(* match lmb with - | nil => OK nil - | mb :: lmb => - do lb <- transl_blocks f lmb false; - transl_block f mb (if Machblock.header mb then ep else false) lb - end. *) - (* OK (make_epilogue f ((Pret X0)::c nil))*) - Program Definition make_prologue (f: Machblock.function) (k:bblocks) := {| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::bi -(* storeptr_bc RA XSP f.(fn_retaddr_ofs) nil; *) ((PSt_rs_a Pstrx RA) (ADimm XSP (Ptrofs.to_int64 (f.(fn_retaddr_ofs))))) ::bi nil; exit := None |} :: k. -(* Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b - push_bc (storeptr_bc RA XSP f.(fn_retaddr_ofs) (pop_bc k)) k. *) - Definition transl_function (f: Machblock.function) : res Asmblock.function := do lb <- transl_blocks f f.(Machblock.fn_code) true; OK (mkfunction f.(Machblock.fn_sig) diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v index 1abcb570..0b1123f7 100644 --- a/aarch64/Asmblockgenproof.v +++ b/aarch64/Asmblockgenproof.v @@ -188,16 +188,6 @@ Proof. apply is_label_correct_false. simpl. auto. Qed. -(* -Lemma transl_is_label2: - forall f bb ep tbb1 tbb2 lbl, - transl_block f bb ep = OK (tbb1::tbb2::nil) -> - is_label lbl tbb1 = MB.is_label lbl bb - /\ is_label lbl tbb2 = false. -Proof. - intros. split. eapply transl_is_label; eauto. eapply transl_is_label_false2; eauto. -Qed. *) - Lemma transl_block_nonil: forall f c ep tc, transl_block f c ep = OK tc -> @@ -285,6 +275,7 @@ Proof. Qed. End TRANSL_LABEL. + (** A valid branch in a piece of Machblock code translates to a valid ``go to'' transition in the generated Asmblock code. *) @@ -808,38 +799,33 @@ Proof. + intro r. destruct r; apply V; auto. - eauto with asmgen. } { rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H11. auto. } - + (* MBbuiltin (contradiction) *) + + (* MBbuiltin *) destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. assert (f0 = f) by congruence. subst f0. assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). - eapply transf_function_no_overflow; eauto. - generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. - remember (Ptrofs.add _ _) as ofs'. - assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc). - econstructor; eauto. - (* exploit return_address_offset_correct; eauto. intros; subst ra. - repeat eexists. - econstructor; eauto. econstructor. *) + eapply transf_function_no_overflow; eauto. + generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. + remember (Ptrofs.add _ _) as ofs'. + assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc). + econstructor; eauto. monadInv TBC. monadInv TIC. inv H0. - -exploit builtin_args_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends; eauto. - intros [vres' [m2' [A [B [C D]]]]]. - + exploit builtin_args_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. + intros [vres' [m2' [A [B [C D]]]]]. - repeat eexists. econstructor. erewrite <- sp_val by eauto. - eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. eauto. - econstructor; eauto. - unfold incrPC. rewrite Pregmap.gss. - rewrite set_res_other. rewrite undef_regs_other_2. unfold Val.offset_ptr. rewrite PCeq. - eauto. rewrite preg_notin_charact. intros. auto with asmgen. - auto with asmgen. apply agree_nextblock. eapply agree_set_res; auto. - eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. - intros. discriminate. + repeat eexists. econstructor. erewrite <- sp_val by eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. eauto. + econstructor; eauto. + unfold incrPC. rewrite Pregmap.gss. + rewrite set_res_other. rewrite undef_regs_other_2. unfold Val.offset_ptr. rewrite PCeq. + eauto. rewrite preg_notin_charact. intros. auto with asmgen. + auto with asmgen. apply agree_nextblock. eapply agree_set_res; auto. + eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. + intros. discriminate. + (* MBgoto *) destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. inv TBC. inv TIC. inv H0. @@ -1373,52 +1359,6 @@ Proof. - econstructor. Qed. -(* Theorem step_simulation_builtin: - forall t sf f sp bb bb' bb'' rs m rs' m' s'' c ef args res S1, - bb' = mb_remove_header bb -> - body_step ge sf f sp (Machblock.body bb') rs m rs' m' -> - bb'' = mb_remove_body bb' -> - MB.exit bb = Some (MBbuiltin ef args res) -> - exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') t s'' -> - match_states (Machblock.State sf f sp (bb :: c) rs m) S1 -> - exists S2 : state, plus (step lk) tge S1 E0 S2 /\ match_states s'' S2. -Proof. - intros until S1. intros Hbb' BSTEP Hbb'' Hexit ESTEP MS. - inv MS. inv AT. monadInv H2. monadInv EQ. - rewrite Hexit in EQ0. monadInv EQ0. simpl in ESTEP. - rewrite Hexit in ESTEP. inv ESTEP. inv H4. - - exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H1); intro NOOV. - exploit builtin_args_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends; eauto. - intros [vres' [m2' [A [B [C D]]]]]. - econstructor; split. apply plus_one. - simpl in H3. - eapply exec_step_internal. eauto. eauto. - eapply find_bblock_tail; eauto. - destruct (x3 @@ nil). - - eauto. - - eauto. - simpl. eauto. eexists. simpl. split; eauto. - econstructor. - erewrite <- sp_val by eauto. - eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eauto. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - eauto. - econstructor; eauto. - instantiate (2 := tf); instantiate (1 := x0). - unfold incrPC. rewrite Pregmap.gss. - rewrite set_res_other. rewrite undef_regs_other_2. - rewrite <- H. simpl. econstructor; eauto. - eapply code_tail_next_int; eauto. - rewrite preg_notin_charact. intros. auto with asmgen. - auto with asmgen. - apply agree_nextblock. eapply agree_set_res; auto. - eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. - congruence. -Qed. *) - (* Measure to prove finite stuttering, see the other backends *) Definition measure (s: MB.state) : nat := match s with @@ -1591,4 +1531,4 @@ Proof. - exact step_simulation. Qed. -End PRESERVATION.
\ No newline at end of file +End PRESERVATION. diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v index a47654b8..4217f526 100644 --- a/aarch64/Asmblockgenproof0.v +++ b/aarch64/Asmblockgenproof0.v @@ -200,9 +200,9 @@ Lemma agree_set_pair: agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs). Proof. intros. destruct p; simpl. -- apply agree_set_mreg_parallel; auto. -- apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto. - apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto. + - apply agree_set_mreg_parallel; auto. + - apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto. + apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto. Qed. Lemma agree_set_res: @@ -212,12 +212,12 @@ Lemma agree_set_res: agree (Mach.set_res res v ms) sp (set_res (map_builtin_res DR (map_builtin_res dreg_of res)) v' rs). Proof. induction res; simpl; intros. -- eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto. - intros. apply Pregmap.gso; auto. -- auto. -- apply IHres2. apply IHres1. auto. - apply Val.hiword_lessdef; auto. - apply Val.loword_lessdef; auto. + - eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto. + intros. apply Pregmap.gso; auto. + - auto. + - apply IHres2. apply IHres1. auto. + apply Val.hiword_lessdef; auto. + apply Val.loword_lessdef; auto. Qed. Lemma agree_undef_regs: @@ -257,15 +257,15 @@ Lemma agree_undef_caller_save_regs: agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs). Proof. intros. destruct H. unfold Mach.undef_caller_save_regs, undef_caller_save_regs; split. -- unfold proj_sumbool; rewrite dec_eq_true. auto. -- auto. -- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). - destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl. -+ apply list_in_map_inv in i. destruct i as (mr & A & B). - assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A. - apply List.filter_In in B. destruct B as [C D]. rewrite D. auto. -+ destruct (is_callee_save r) eqn:CS; auto. - elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. + - unfold proj_sumbool; rewrite dec_eq_true. auto. + - auto. + - intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). + destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl. + + apply list_in_map_inv in i. destruct i as (mr & A & B). + assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A. + apply List.filter_In in B. destruct B as [C D]. rewrite D. auto. + + destruct (is_callee_save r) eqn:CS; auto. + elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. Qed. Lemma agree_change_sp: @@ -327,10 +327,10 @@ Lemma extcall_arg_pair_match: exists v', extcall_arg_pair rs m' p v' /\ Val.lessdef v v'. Proof. intros. inv H1. -- exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto. -- exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1). - exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2). - exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto. + - exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto. + - exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1). + exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2). + exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto. Qed. Lemma extcall_args_match: @@ -362,9 +362,9 @@ Lemma set_res_other: set_res (map_builtin_res DR (map_builtin_res dreg_of res)) v rs r = rs r. Proof. induction res; simpl; intros. -- apply Pregmap.gso. red; intros; subst r. rewrite dreg_of_data in H; discriminate. -- auto. -- rewrite IHres2, IHres1; auto. + - apply Pregmap.gso. red; intros; subst r. rewrite dreg_of_data in H; discriminate. + - auto. + - rewrite IHres2, IHres1; auto. Qed. Lemma undef_regs_other: @@ -720,8 +720,8 @@ Lemma exec_straight_opt_step: exec_straight (i :: c) rs1 m1 c' rs3 m3. Proof. intros. inv H0. -- apply exec_straight_one; auto. -- eapply exec_straight_step; eauto. + - apply exec_straight_one; auto. + - eapply exec_straight_step; eauto. Qed. Lemma exec_straight_opt_step_opt: @@ -882,4 +882,4 @@ Proof. intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. Qed. -End MATCH_STACK.
\ No newline at end of file +End MATCH_STACK. diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v index dd7803cd..e26c24e7 100644 --- a/aarch64/Asmblockgenproof1.v +++ b/aarch64/Asmblockgenproof1.v @@ -137,10 +137,10 @@ Lemma decompose_int_wf: Proof. Local Opaque Zzero_ext. induction N as [ | N]; simpl; intros. -- constructor. -- set (frag := Zzero_ext 16 (Z.shiftr n p)) in *. destruct (Z.eqb frag 0). -+ apply IHN. omega. -+ econstructor. reflexivity. omega. apply IHN; omega. + - constructor. + - set (frag := Zzero_ext 16 (Z.shiftr n p)) in *. destruct (Z.eqb frag 0). + + apply IHN. omega. + + econstructor. reflexivity. omega. apply IHN; omega. Qed. Fixpoint recompose_int (accu: Z) (l: list (Z * Z)) : Z := @@ -158,35 +158,35 @@ Lemma decompose_int_correct: if zlt i p then Z.testbit accu i else Z.testbit n i). Proof. induction N as [ | N]; intros until accu; intros PPOS ABOVE i RANGE. -- simpl. rewrite zlt_true; auto. xomega. -- rewrite inj_S in RANGE. simpl. - set (frag := Zzero_ext 16 (Z.shiftr n p)). - assert (FRAG: forall i, p <= i < p + 16 -> Z.testbit n i = Z.testbit frag (i - p)). - { unfold frag; intros. rewrite Zzero_ext_spec by omega. rewrite zlt_true by omega. - rewrite Z.shiftr_spec by omega. f_equal; omega. } - destruct (Z.eqb_spec frag 0). -+ rewrite IHN. -* destruct (zlt i p). rewrite zlt_true by omega. auto. - destruct (zlt i (p + 16)); auto. - rewrite ABOVE by omega. rewrite FRAG by omega. rewrite e, Z.testbit_0_l. auto. -* omega. -* intros; apply ABOVE; omega. -* xomega. -+ simpl. rewrite IHN. -* destruct (zlt i (p + 16)). -** rewrite Zinsert_spec by omega. unfold proj_sumbool. - rewrite zlt_true by omega. - destruct (zlt i p). - rewrite zle_false by omega. auto. - rewrite zle_true by omega. simpl. symmetry; apply FRAG; omega. -** rewrite Z.ldiff_spec, Z.shiftl_spec by omega. - change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by omega. - rewrite zlt_false by omega. rewrite zlt_false by omega. apply andb_true_r. -* omega. -* intros. rewrite Zinsert_spec by omega. unfold proj_sumbool. - rewrite zle_true by omega. rewrite zlt_false by omega. simpl. - apply ABOVE. omega. -* xomega. + - simpl. rewrite zlt_true; auto. xomega. + - rewrite inj_S in RANGE. simpl. + set (frag := Zzero_ext 16 (Z.shiftr n p)). + assert (FRAG: forall i, p <= i < p + 16 -> Z.testbit n i = Z.testbit frag (i - p)). + { unfold frag; intros. rewrite Zzero_ext_spec by omega. rewrite zlt_true by omega. + rewrite Z.shiftr_spec by omega. f_equal; omega. } + destruct (Z.eqb_spec frag 0). + + rewrite IHN. + * destruct (zlt i p). rewrite zlt_true by omega. auto. + destruct (zlt i (p + 16)); auto. + rewrite ABOVE by omega. rewrite FRAG by omega. rewrite e, Z.testbit_0_l. auto. + * omega. + * intros; apply ABOVE; omega. + * xomega. + + simpl. rewrite IHN. + * destruct (zlt i (p + 16)). + ** rewrite Zinsert_spec by omega. unfold proj_sumbool. + rewrite zlt_true by omega. + destruct (zlt i p). + rewrite zle_false by omega. auto. + rewrite zle_true by omega. simpl. symmetry; apply FRAG; omega. + ** rewrite Z.ldiff_spec, Z.shiftl_spec by omega. + change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by omega. + rewrite zlt_false by omega. rewrite zlt_false by omega. apply andb_true_r. + * omega. + * intros. rewrite Zinsert_spec by omega. unfold proj_sumbool. + rewrite zle_true by omega. rewrite zlt_false by omega. simpl. + apply ABOVE. omega. + * xomega. Qed. Corollary decompose_int_eqmod: forall N n, @@ -238,10 +238,10 @@ Proof. intros. apply equal_same_bits; intros. rewrite Zinsert_spec by omega. unfold proj_sumbool. destruct (zlt i p); [rewrite zle_false by omega|rewrite zle_true by omega]; simpl. -- rewrite Z.testbit_0_l, Z.shiftl_spec_low by auto. auto. -- rewrite Z.shiftl_spec by omega. - destruct (zlt i (p + l)); auto. - rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by omega. auto. + - rewrite Z.testbit_0_l, Z.shiftl_spec_low by auto. auto. + - rewrite Z.shiftl_spec by omega. + destruct (zlt i (p + l)); auto. + rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by omega. auto. Qed. Lemma recompose_int_negated: @@ -249,15 +249,15 @@ Lemma recompose_int_negated: forall accu, recompose_int (Z.lnot accu) (negate_decomposition l) = Z.lnot (recompose_int accu l). Proof. induction 1; intros accu; simpl. -- auto. -- rewrite <- IHwf_decomposition. f_equal. apply equal_same_bits; intros. - rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by omega. - unfold proj_sumbool. - destruct (zle p i); simpl; auto. - destruct (zlt i (p + 16)); simpl; auto. - change 65535 with (two_p 16 - 1). - rewrite Ztestbit_two_p_m1 by omega. rewrite zlt_true by omega. - apply xorb_true_r. + - auto. + - rewrite <- IHwf_decomposition. f_equal. apply equal_same_bits; intros. + rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by omega. + unfold proj_sumbool. + destruct (zle p i); simpl; auto. + destruct (zlt i (p + 16)); simpl; auto. + change 65535 with (two_p 16 - 1). + rewrite Ztestbit_two_p_m1 by omega. rewrite zlt_true by omega. + apply xorb_true_r. Qed. Lemma exec_loadimm_k_w: @@ -271,16 +271,16 @@ Lemma exec_loadimm_k_w: /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. induction 1; intros rs accu ACCU; simpl. -- exists rs; split. apply exec_straight_opt_refl. auto. -- destruct (IHwf_decomposition - ((rs#rd <- (insert_in_int rs#rd n p 16))) - (Zinsert accu n p 16)) - as (rs' & P & Q & R). - Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr. - apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. - exists rs'; split. - eapply exec_straight_opt_step_opt. simpl. eauto. auto. - split. exact Q. intros; Simpl. rewrite R by auto. Simpl. + - exists rs; split. apply exec_straight_opt_refl. auto. + - destruct (IHwf_decomposition + ((rs#rd <- (insert_in_int rs#rd n p 16))) + (Zinsert accu n p 16)) + as (rs' & P & Q & R). + Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr. + apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + exists rs'; split. + eapply exec_straight_opt_step_opt. simpl. eauto. auto. + split. exact Q. intros; Simpl. rewrite R by auto. Simpl. Qed. Lemma exec_loadimm_z_w: @@ -292,19 +292,19 @@ Lemma exec_loadimm_z_w: /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. unfold loadimm_z; destruct 1. -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -- set (accu0 := Zinsert 0 n p 16). - set (rs1 := rs#rd <- (Vint (Int.repr accu0))). - destruct (exec_loadimm_k_w rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto. - unfold rs1; Simpl. - exists rs2; split. - eapply exec_straight_opt_step; eauto. - simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega. - split. exact Q. - intros. rewrite R by auto. unfold rs1; Simpl. + - econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. + - set (accu0 := Zinsert 0 n p 16). + set (rs1 := rs#rd <- (Vint (Int.repr accu0))). + destruct (exec_loadimm_k_w rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto. + unfold rs1; Simpl. + exists rs2; split. + eapply exec_straight_opt_step; eauto. + simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega. + split. exact Q. + intros. rewrite R by auto. unfold rs1; Simpl. Qed. Lemma exec_loadimm_n_w: @@ -316,22 +316,22 @@ Lemma exec_loadimm_n_w: /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. unfold loadimm_n; destruct 1. -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -- set (accu0 := Z.lnot (Zinsert 0 n p 16)). - set (rs1 := rs#rd <- (Vint (Int.repr accu0))). - destruct (exec_loadimm_k_w rd k m (negate_decomposition l) - (negate_decomposition_wf l H1) - rs1 accu0) as (rs2 & P & Q & R). - unfold rs1; Simpl. - exists rs2; split. - eapply exec_straight_opt_step; eauto. - simpl. unfold rs1. do 5 f_equal. - unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega. - split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q. - intros. rewrite R by auto. unfold rs1; Simpl. + - econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. + - set (accu0 := Z.lnot (Zinsert 0 n p 16)). + set (rs1 := rs#rd <- (Vint (Int.repr accu0))). + destruct (exec_loadimm_k_w rd k m (negate_decomposition l) + (negate_decomposition_wf l H1) + rs1 accu0) as (rs2 & P & Q & R). + unfold rs1; Simpl. + exists rs2; split. + eapply exec_straight_opt_step; eauto. + simpl. unfold rs1. do 5 f_equal. + unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega. + split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q. + intros. rewrite R by auto. unfold rs1; Simpl. Qed. Lemma exec_loadimm32: @@ -343,23 +343,23 @@ Lemma exec_loadimm32: Proof. unfold loadimm32, loadimm; intros. destruct (is_logical_imm32 n). -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. rewrite Int.repr_unsigned, Int.or_zero_l; auto. - intros; Simpl. -- set (dz := decompose_int 2%nat (Int.unsigned n) 0). - set (dn := decompose_int 2%nat (Z.lnot (Int.unsigned n)) 0). - assert (A: Int.repr (recompose_int 0 dz) = n). - { transitivity (Int.repr (Int.unsigned n)). - apply Int.eqm_samerepr. apply decompose_int_eqmod. - apply Int.repr_unsigned. } - assert (B: Int.repr (Z.lnot (recompose_int 0 dn)) = n). - { transitivity (Int.repr (Int.unsigned n)). - apply Int.eqm_samerepr. apply decompose_notint_eqmod. - apply Int.repr_unsigned. } - destruct Nat.leb. -+ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega. -+ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega. + - econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. rewrite Int.repr_unsigned, Int.or_zero_l; auto. + intros; Simpl. + - set (dz := decompose_int 2%nat (Int.unsigned n) 0). + set (dn := decompose_int 2%nat (Z.lnot (Int.unsigned n)) 0). + assert (A: Int.repr (recompose_int 0 dz) = n). + { transitivity (Int.repr (Int.unsigned n)). + apply Int.eqm_samerepr. apply decompose_int_eqmod. + apply Int.repr_unsigned. } + assert (B: Int.repr (Z.lnot (recompose_int 0 dn)) = n). + { transitivity (Int.repr (Int.unsigned n)). + apply Int.eqm_samerepr. apply decompose_notint_eqmod. + apply Int.repr_unsigned. } + destruct Nat.leb. + + rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega. + + rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega. Qed. Lemma exec_loadimm_k_x: @@ -373,16 +373,16 @@ Lemma exec_loadimm_k_x: /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. induction 1; intros rs accu ACCU; simpl. -- exists rs; split. apply exec_straight_opt_refl. auto. -- destruct (IHwf_decomposition - (rs#rd <- (insert_in_long rs#rd n p 16)) - (Zinsert accu n p 16)) - as (rs' & P & Q & R). - Simpl. rewrite ACCU. simpl. f_equal. apply Int64.eqm_samerepr. - apply Zinsert_eqmod. auto. omega. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr. - exists rs'; split. - eapply exec_straight_opt_step_opt. simpl; eauto. auto. - split. exact Q. intros; Simpl. rewrite R by auto. Simpl. + - exists rs; split. apply exec_straight_opt_refl. auto. + - destruct (IHwf_decomposition + (rs#rd <- (insert_in_long rs#rd n p 16)) + (Zinsert accu n p 16)) + as (rs' & P & Q & R). + Simpl. rewrite ACCU. simpl. f_equal. apply Int64.eqm_samerepr. + apply Zinsert_eqmod. auto. omega. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr. + exists rs'; split. + eapply exec_straight_opt_step_opt. simpl; eauto. auto. + split. exact Q. intros; Simpl. rewrite R by auto. Simpl. Qed. Lemma exec_loadimm_z_x: @@ -394,19 +394,19 @@ Lemma exec_loadimm_z_x: /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. unfold loadimm_z; destruct 1. -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -- set (accu0 := Zinsert 0 n p 16). - set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))). - destruct (exec_loadimm_k_x rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto. - unfold rs1; Simpl. - exists rs2; split. - eapply exec_straight_opt_step; eauto. - simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega. - split. exact Q. - intros. rewrite R by auto. unfold rs1; Simpl. + - econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. + - set (accu0 := Zinsert 0 n p 16). + set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))). + destruct (exec_loadimm_k_x rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto. + unfold rs1; Simpl. + exists rs2; split. + eapply exec_straight_opt_step; eauto. + simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega. + split. exact Q. + intros. rewrite R by auto. unfold rs1; Simpl. Qed. Lemma exec_loadimm_n_x: @@ -418,22 +418,22 @@ Lemma exec_loadimm_n_x: /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. unfold loadimm_n; destruct 1. -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -- set (accu0 := Z.lnot (Zinsert 0 n p 16)). - set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))). - destruct (exec_loadimm_k_x rd k m (negate_decomposition l) - (negate_decomposition_wf l H1) - rs1 accu0) as (rs2 & P & Q & R). - unfold rs1; Simpl. - exists rs2; split. - eapply exec_straight_opt_step; eauto. - simpl. unfold rs1. do 5 f_equal. - unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega. - split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q. - intros. rewrite R by auto. unfold rs1; Simpl. + - econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. + - set (accu0 := Z.lnot (Zinsert 0 n p 16)). + set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))). + destruct (exec_loadimm_k_x rd k m (negate_decomposition l) + (negate_decomposition_wf l H1) + rs1 accu0) as (rs2 & P & Q & R). + unfold rs1; Simpl. + exists rs2; split. + eapply exec_straight_opt_step; eauto. + simpl. unfold rs1. do 5 f_equal. + unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega. + split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q. + intros. rewrite R by auto. unfold rs1; Simpl. Qed. Lemma exec_loadimm64: @@ -445,23 +445,23 @@ Lemma exec_loadimm64: Proof. unfold loadimm64, loadimm; intros. destruct (is_logical_imm64 n). -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. rewrite Int64.repr_unsigned, Int64.or_zero_l; auto. - intros; Simpl. -- set (dz := decompose_int 4%nat (Int64.unsigned n) 0). - set (dn := decompose_int 4%nat (Z.lnot (Int64.unsigned n)) 0). - assert (A: Int64.repr (recompose_int 0 dz) = n). - { transitivity (Int64.repr (Int64.unsigned n)). - apply Int64.eqm_samerepr. apply decompose_int_eqmod. - apply Int64.repr_unsigned. } - assert (B: Int64.repr (Z.lnot (recompose_int 0 dn)) = n). - { transitivity (Int64.repr (Int64.unsigned n)). - apply Int64.eqm_samerepr. apply decompose_notint_eqmod. - apply Int64.repr_unsigned. } - destruct Nat.leb. -+ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega. -+ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega. + - econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. rewrite Int64.repr_unsigned, Int64.or_zero_l; auto. + intros; Simpl. + - set (dz := decompose_int 4%nat (Int64.unsigned n) 0). + set (dn := decompose_int 4%nat (Z.lnot (Int64.unsigned n)) 0). + assert (A: Int64.repr (recompose_int 0 dz) = n). + { transitivity (Int64.repr (Int64.unsigned n)). + apply Int64.eqm_samerepr. apply decompose_int_eqmod. + apply Int64.repr_unsigned. } + assert (B: Int64.repr (Z.lnot (recompose_int 0 dn)) = n). + { transitivity (Int64.repr (Int64.unsigned n)). + apply Int64.eqm_samerepr. apply decompose_notint_eqmod. + apply Int64.repr_unsigned. } + destruct Nat.leb. + + rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega. + + rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega. Qed. (** Add immediate *) @@ -483,17 +483,17 @@ Proof. assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; omega). rewrite <- (Int.repr_unsigned n). destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)]. -- econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. - intros; Simpl. -- econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. - intros; Simpl. -- econstructor; split. eapply exec_straight_two. - apply SEM. apply SEM. simpl. Simpl. - split. Simpl. simpl. rewrite ASSOC. do 2 f_equal. apply Int.eqm_samerepr. - rewrite E. auto with ints. - intros; Simpl. + - econstructor; split. apply exec_straight_one. apply SEM. Simpl. + split. Simpl. do 3 f_equal; omega. + intros; Simpl. + - econstructor; split. apply exec_straight_one. apply SEM. Simpl. + split. Simpl. do 3 f_equal; omega. + intros; Simpl. + - econstructor; split. eapply exec_straight_two. + apply SEM. apply SEM. simpl. Simpl. + split. Simpl. simpl. rewrite ASSOC. do 2 f_equal. apply Int.eqm_samerepr. + rewrite E. auto with ints. + intros; Simpl. Qed. Lemma exec_addimm32: @@ -506,22 +506,22 @@ Lemma exec_addimm32: Proof. intros. unfold addimm32. set (nn := Int.neg n). destruct (Int.eq n (Int.zero_ext 24 n)); [| destruct (Int.eq nn (Int.zero_ext 24 nn))]. -- apply exec_addimm_aux_32 with (sem := Val.add). auto. intros; apply Val.add_assoc. -- rewrite <- Val.sub_opp_add. - apply exec_addimm_aux_32 with (sem := Val.sub). auto. - intros. rewrite ! Val.sub_add_opp, Val.add_assoc. rewrite Int.neg_add_distr. auto. -- destruct (Int.lt n Int.zero). -+ rewrite <- Val.sub_opp_add; fold nn. - edestruct (exec_loadimm32 X16 nn) as (rs1 & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto. - split. Simpl. rewrite B, C; eauto with asmgen. - intros; Simpl. -+ edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto. - split. Simpl. rewrite B, C; eauto with asmgen. - intros; Simpl. + - apply exec_addimm_aux_32 with (sem := Val.add). auto. intros; apply Val.add_assoc. + - rewrite <- Val.sub_opp_add. + apply exec_addimm_aux_32 with (sem := Val.sub). auto. + intros. rewrite ! Val.sub_add_opp, Val.add_assoc. rewrite Int.neg_add_distr. auto. + - destruct (Int.lt n Int.zero). + + rewrite <- Val.sub_opp_add; fold nn. + edestruct (exec_loadimm32 X16 nn) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto. + split. Simpl. rewrite B, C; eauto with asmgen. + intros; Simpl. + + edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto. + split. Simpl. rewrite B, C; eauto with asmgen. + intros; Simpl. Qed. Lemma exec_addimm_aux_64: @@ -541,17 +541,17 @@ Proof. assert (E: Int64.unsigned n = nhi + nlo) by (unfold nhi; omega). rewrite <- (Int64.repr_unsigned n). destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)]. -- econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. - intros; Simpl. -- econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. - intros; Simpl. -- econstructor; split. eapply exec_straight_two. - apply SEM. apply SEM. Simpl. Simpl. - split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int64.eqm_samerepr. - rewrite E. auto with ints. - intros; Simpl. + - econstructor; split. apply exec_straight_one. apply SEM. Simpl. + split. Simpl. do 3 f_equal; omega. + intros; Simpl. + - econstructor; split. apply exec_straight_one. apply SEM. Simpl. + split. Simpl. do 3 f_equal; omega. + intros; Simpl. + - econstructor; split. eapply exec_straight_two. + apply SEM. apply SEM. Simpl. Simpl. + split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int64.eqm_samerepr. + rewrite E. auto with ints. + intros; Simpl. Qed. Lemma exec_addimm64: @@ -565,22 +565,22 @@ Proof. intros. unfold addimm64. set (nn := Int64.neg n). destruct (Int64.eq n (Int64.zero_ext 24 n)); [| destruct (Int64.eq nn (Int64.zero_ext 24 nn))]. -- apply exec_addimm_aux_64 with (sem := Val.addl). auto. intros; apply Val.addl_assoc. -- rewrite <- Val.subl_opp_addl. - apply exec_addimm_aux_64 with (sem := Val.subl). auto. - intros. rewrite ! Val.subl_addl_opp, Val.addl_assoc. rewrite Int64.neg_add_distr. auto. -- destruct (Int64.lt n Int64.zero). -+ rewrite <- Val.subl_opp_addl; fold nn. - edestruct (exec_loadimm64 X16 nn) as (rs1 & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. - split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto. - intros; Simpl. -+ edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. - split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto. - intros; Simpl. + - apply exec_addimm_aux_64 with (sem := Val.addl). auto. intros; apply Val.addl_assoc. + - rewrite <- Val.subl_opp_addl. + apply exec_addimm_aux_64 with (sem := Val.subl). auto. + intros. rewrite ! Val.subl_addl_opp, Val.addl_assoc. rewrite Int64.neg_add_distr. auto. + - destruct (Int64.lt n Int64.zero). + + rewrite <- Val.subl_opp_addl; fold nn. + edestruct (exec_loadimm64 X16 nn) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. + split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto. + intros; Simpl. + + edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. + split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto. + intros; Simpl. Qed. (** Logical immediate *) @@ -604,15 +604,15 @@ Lemma exec_logicalimm32: Proof. intros until sem; intros SEM1 SEM2; intros. unfold logicalimm32. destruct (is_logical_imm32 n). -- econstructor; split. - apply exec_straight_one. apply SEM1. - split. Simpl. rewrite Int.repr_unsigned; auto. intros; Simpl. -- edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. apply SEM2. - split. Simpl. f_equal; auto. apply C; auto with asmgen. - intros; Simpl. + - econstructor; split. + apply exec_straight_one. apply SEM1. + split. Simpl. rewrite Int.repr_unsigned; auto. intros; Simpl. + - edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. apply SEM2. + split. Simpl. f_equal; auto. apply C; auto with asmgen. + intros; Simpl. Qed. Lemma exec_logicalimm64: @@ -634,15 +634,15 @@ Lemma exec_logicalimm64: Proof. intros until sem; intros SEM1 SEM2; intros. unfold logicalimm64. destruct (is_logical_imm64 n). -- econstructor; split. - apply exec_straight_one. apply SEM1. - split. Simpl. rewrite Int64.repr_unsigned. auto. intros; Simpl. -- edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. apply SEM2. - split. Simpl. f_equal; auto. apply C; auto with asmgen. - intros; Simpl. + - econstructor; split. + apply exec_straight_one. apply SEM1. + split. Simpl. rewrite Int64.repr_unsigned. auto. intros; Simpl. + - edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. apply SEM2. + split. Simpl. f_equal; auto. apply C; auto with asmgen. + intros; Simpl. Qed. (** Load address of symbol *) @@ -655,22 +655,22 @@ Lemma exec_loadsymbol: forall rd s ofs k rs m, /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. unfold loadsymbol; intros. destruct (Archi.pic_code tt). -- predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero. -+ subst ofs. econstructor; split. - apply exec_straight_one. simpl; eauto. - split. Simpl. intros; Simpl. -+ exploit exec_addimm64. instantiate (1 := rd). simpl. destruct H; congruence. - intros (rs1 & A & B & C). - econstructor; split. - econstructor. simpl; eauto. auto. eexact A. - split. simpl in B; rewrite B. Simpl. - rewrite <- Genv.shift_symbol_address_64 by auto. - rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto. - intros. rewrite C by auto. Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split. Simpl. - intros; Simpl. + - predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero. + + subst ofs. econstructor; split. + apply exec_straight_one. simpl; eauto. + split. Simpl. intros; Simpl. + + exploit exec_addimm64. instantiate (1 := rd). simpl. destruct H; congruence. + intros (rs1 & A & B & C). + econstructor; split. + econstructor. simpl; eauto. auto. eexact A. + split. simpl in B; rewrite B. Simpl. + rewrite <- Genv.shift_symbol_address_64 by auto. + rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto. + intros. rewrite C by auto. Simpl. + - econstructor; split. + eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. + split. Simpl. + intros; Simpl. Qed. (** Shifted operands *) @@ -754,18 +754,18 @@ Lemma exec_move_extended: forall rd r1 ex (a: amount64) k rs m, /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. unfold move_extended; intros. predSpec Int.eq Int.eq_spec a Int.zero. -- exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C). - exists rs'; split. eexact A. split. unfold Op.eval_extend. rewrite H. rewrite B. - destruct ex, (rs r1); simpl; auto; rewrite Int64.shl'_zero; auto. - auto. -- Local Opaque Val.addl. - exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - change (SOlsl a) with (transl_shift Slsl a). rewrite transl_eval_shiftl''. eauto. auto. - split. Simpl. rewrite B. auto. - intros; Simpl. + - exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C). + exists rs'; split. eexact A. split. unfold Op.eval_extend. rewrite H. rewrite B. + destruct ex, (rs r1); simpl; auto; rewrite Int64.shl'_zero; auto. + auto. + - Local Opaque Val.addl. + exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + change (SOlsl a) with (transl_shift Slsl a). rewrite transl_eval_shiftl''. eauto. auto. + split. Simpl. rewrite B. auto. + intros; Simpl. Qed. Lemma exec_arith_extended: @@ -786,17 +786,17 @@ Lemma exec_arith_extended: /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. intros sem insnX insnS EX ES; intros. unfold arith_extended. destruct (Int.ltu a (Int.repr 5)). -- econstructor; split. - apply exec_straight_one. rewrite EX; eauto. auto. - split. Simpl. f_equal. destruct ex; auto. - intros; Simpl. -- exploit (exec_move_extended_base X16 r2 ex). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - rewrite ES. eauto. auto. - split. Simpl. unfold ir0. rewrite C by eauto with asmgen. f_equal. - rewrite B. destruct ex; auto. - intros; Simpl. + - econstructor; split. + apply exec_straight_one. rewrite EX; eauto. auto. + split. Simpl. f_equal. destruct ex; auto. + intros; Simpl. + - exploit (exec_move_extended_base X16 r2 ex). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + rewrite ES. eauto. auto. + split. Simpl. unfold ir0. rewrite C by eauto with asmgen. f_equal. + rewrite B. destruct ex; auto. + intros; Simpl. Qed. (** Extended right shift *) @@ -811,15 +811,15 @@ Lemma exec_shrx32: forall (rd r1: ireg) (n: int) k v (rs: regset) m, Proof. unfold shrx32; intros. apply Val.shrx_shr_2 in H. destruct (Int.eq n Int.zero) eqn:E0. -- econstructor; split. apply exec_straight_one; simpl; eauto. - split. Simpl. subst v; auto. intros; Simpl. -- econstructor; split. eapply exec_straight_three. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_int by congruence. eauto. - simpl; eauto. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_int by congruence. eauto. - split. subst v; Simpl. intros; Simpl. + - econstructor; split. apply exec_straight_one; simpl; eauto. + split. Simpl. subst v; auto. intros; Simpl. + - econstructor; split. eapply exec_straight_three. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_int by congruence. eauto. + simpl; eauto. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_int by congruence. eauto. + split. subst v; Simpl. intros; Simpl. Qed. Lemma exec_shrx32_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m, @@ -832,15 +832,15 @@ Lemma exec_shrx32_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m, Proof. unfold shrx32; intros. destruct (Int.eq n Int.zero) eqn:E0. -- econstructor; split. apply exec_straight_one; simpl; eauto. - split. Simpl. auto. intros; Simpl. -- econstructor; split. eapply exec_straight_three. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_int by congruence. eauto. - simpl; eauto. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_int by congruence. eauto. - split. Simpl. intros; Simpl. + - econstructor; split. apply exec_straight_one; simpl; eauto. + split. Simpl. auto. intros; Simpl. + - econstructor; split. eapply exec_straight_three. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_int by congruence. eauto. + simpl; eauto. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_int by congruence. eauto. + split. Simpl. intros; Simpl. Qed. Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m, @@ -853,15 +853,15 @@ Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m, Proof. unfold shrx64; intros. apply Val.shrxl_shrl_2 in H. destruct (Int.eq n Int.zero) eqn:E. -- econstructor; split. apply exec_straight_one; simpl; eauto. - split. Simpl. subst v; auto. intros; Simpl. -- econstructor; split. eapply exec_straight_three. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_long by congruence. eauto. - simpl; eauto. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_long by congruence. eauto. - split. subst v; Simpl. intros; Simpl. + - econstructor; split. apply exec_straight_one; simpl; eauto. + split. Simpl. subst v; auto. intros; Simpl. + - econstructor; split. eapply exec_straight_three. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_long by congruence. eauto. + simpl; eauto. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_long by congruence. eauto. + split. subst v; Simpl. intros; Simpl. Qed. Lemma exec_shrx64_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m, @@ -874,15 +874,15 @@ Lemma exec_shrx64_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m, Proof. unfold shrx64; intros. destruct (Int.eq n Int.zero) eqn:E. -- econstructor; split. apply exec_straight_one; simpl; eauto. - split. Simpl. auto. intros; Simpl. -- econstructor; split. eapply exec_straight_three. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_long by congruence. eauto. - simpl; eauto. - unfold exec_basic, exec_arith_instr, arith_eval_rr0r. - rewrite or_zero_eval_shift_op_long by congruence. eauto. - split. Simpl. intros; Simpl. + - econstructor; split. apply exec_straight_one; simpl; eauto. + split. Simpl. auto. intros; Simpl. + - econstructor; split. eapply exec_straight_three. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_long by congruence. eauto. + simpl; eauto. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_long by congruence. eauto. + split. Simpl. intros; Simpl. Qed. Ltac TranslOpBase := @@ -913,14 +913,14 @@ Proof. destruct v1; try discriminate; destruct v2; try discriminate. simpl in H; inv H. unfold Val_cmpu; simpl. destruct c; simpl. -- destruct (Int.eq i i0); auto. -- destruct (Int.eq i i0); auto. -- rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto. -- rewrite Int.lt_sub_overflow, Int.not_lt. - destruct (Int.eq i i0), (Int.lt i i0); auto. -- rewrite Int.lt_sub_overflow, (Int.lt_not i). - destruct (Int.eq i i0), (Int.lt i i0); auto. -- rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto. + - destruct (Int.eq i i0); auto. + - destruct (Int.eq i i0); auto. + - rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto. + - rewrite Int.lt_sub_overflow, Int.not_lt. + destruct (Int.eq i i0), (Int.lt i i0); auto. + - rewrite Int.lt_sub_overflow, (Int.lt_not i). + destruct (Int.eq i i0), (Int.lt i i0); auto. + - rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto. Qed. Lemma eval_testcond_compare_uint: forall c v1 v2 b rs, @@ -933,12 +933,12 @@ Proof. destruct v1; try discriminate; destruct v2; try discriminate. simpl in H; inv H. unfold Val_cmpu; simpl. destruct c; simpl. -- destruct (Int.eq i i0); auto. -- destruct (Int.eq i i0); auto. -- destruct (Int.ltu i i0); auto. -- rewrite (Int.not_ltu i). destruct (Int.eq i i0), (Int.ltu i i0); auto. -- rewrite (Int.ltu_not i). destruct (Int.eq i i0), (Int.ltu i i0); auto. -- destruct (Int.ltu i i0); auto. + - destruct (Int.eq i i0); auto. + - destruct (Int.eq i i0); auto. + - destruct (Int.ltu i i0); auto. + - rewrite (Int.not_ltu i). destruct (Int.eq i i0), (Int.ltu i i0); auto. + - rewrite (Int.ltu_not i). destruct (Int.eq i i0), (Int.ltu i i0); auto. + - destruct (Int.ltu i i0); auto. Qed. Lemma compare_long_spec: forall rs v1 v2, @@ -978,14 +978,14 @@ Proof. destruct v1; try discriminate; destruct v2; try discriminate. simpl in H; inv H. unfold Val_cmplu; simpl. destruct c; simpl. -- destruct (Int64.eq i i0); auto. -- destruct (Int64.eq i i0); auto. -- rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto. -- rewrite int64_sub_overflow, Int64.not_lt. - destruct (Int64.eq i i0), (Int64.lt i i0); auto. -- rewrite int64_sub_overflow, (Int64.lt_not i). - destruct (Int64.eq i i0), (Int64.lt i i0); auto. -- rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto. + - destruct (Int64.eq i i0); auto. + - destruct (Int64.eq i i0); auto. + - rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto. + - rewrite int64_sub_overflow, Int64.not_lt. + destruct (Int64.eq i i0), (Int64.lt i i0); auto. + - rewrite int64_sub_overflow, (Int64.lt_not i). + destruct (Int64.eq i i0), (Int64.lt i i0); auto. + - rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto. Qed. Lemma eval_testcond_compare_ulong: forall c v1 v2 b rs, @@ -996,37 +996,37 @@ Proof. set (rs' := compare_long rs v1 v2). intros (B & C & D & E). unfold eval_testcond; rewrite B, C, D, E; unfold Val_cmplu. destruct v1; try discriminate; destruct v2; try discriminate; simpl in H. -- (* int-int *) - inv H. destruct c; simpl. -+ destruct (Int64.eq i i0); auto. -+ destruct (Int64.eq i i0); auto. -+ destruct (Int64.ltu i i0); auto. -+ rewrite (Int64.not_ltu i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto. -+ rewrite (Int64.ltu_not i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto. -+ destruct (Int64.ltu i i0); auto. -- (* int-ptr *) - simpl. - destruct (Archi.ptr64); simpl; try discriminate. - destruct (Int64.eq i Int64.zero); simpl; try discriminate. - destruct c; simpl in H; inv H; reflexivity. -- (* ptr-int *) - simpl. - destruct (Archi.ptr64); simpl; try discriminate. - destruct (Int64.eq i0 Int64.zero); try discriminate. - destruct c; simpl in H; inv H; reflexivity. -- (* ptr-ptr *) - simpl. - destruct (eq_block b0 b1). - destruct (Archi.ptr64); simpl; try discriminate. - inv H. - destruct c; simpl. -* destruct (Ptrofs.eq i i0); auto. -* destruct (Ptrofs.eq i i0); auto. -* destruct (Ptrofs.ltu i i0); auto. -* rewrite (Ptrofs.not_ltu i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto. -* rewrite (Ptrofs.ltu_not i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto. -* destruct (Ptrofs.ltu i i0); auto. -* destruct c; simpl in H; inv H; reflexivity. + - (* int-int *) + inv H. destruct c; simpl. + + destruct (Int64.eq i i0); auto. + + destruct (Int64.eq i i0); auto. + + destruct (Int64.ltu i i0); auto. + + rewrite (Int64.not_ltu i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto. + + rewrite (Int64.ltu_not i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto. + + destruct (Int64.ltu i i0); auto. + - (* int-ptr *) + simpl. + destruct (Archi.ptr64); simpl; try discriminate. + destruct (Int64.eq i Int64.zero); simpl; try discriminate. + destruct c; simpl in H; inv H; reflexivity. + - (* ptr-int *) + simpl. + destruct (Archi.ptr64); simpl; try discriminate. + destruct (Int64.eq i0 Int64.zero); try discriminate. + destruct c; simpl in H; inv H; reflexivity. + - (* ptr-ptr *) + simpl. + destruct (eq_block b0 b1). + destruct (Archi.ptr64); simpl; try discriminate. + inv H. + destruct c; simpl. + * destruct (Ptrofs.eq i i0); auto. + * destruct (Ptrofs.eq i i0); auto. + * destruct (Ptrofs.ltu i i0); auto. + * rewrite (Ptrofs.not_ltu i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto. + * rewrite (Ptrofs.ltu_not i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto. + * destruct (Ptrofs.ltu i i0); auto. + * destruct c; simpl in H; inv H; reflexivity. Qed. Lemma compare_float_spec: forall rs f1 f2, @@ -1132,179 +1132,179 @@ Lemma transl_cond_correct: /\ forall r, data_preg r = true -> rs'#r = rs#r. Proof. intros until m; intros TR. destruct cond; simpl in TR; ArgsInv. -- (* Ccomp *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_sint; auto. - destruct r; reflexivity || discriminate. -- (* Ccompu *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. apply eval_testcond_compare_uint; auto. - destruct r; reflexivity || discriminate. -- (* Ccompimm *) - destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. - destruct r; reflexivity || discriminate. -+ econstructor; split. - apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto. - split; intros. apply eval_testcond_compare_sint; auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - simpl. rewrite B, C by eauto with asmgen. eauto. - split; intros. apply eval_testcond_compare_sint; auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Ccompuimm *) - destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_uint; auto. - destruct r; reflexivity || discriminate. -+ econstructor; split. - apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto. - split; intros. apply eval_testcond_compare_uint; auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - simpl. rewrite B, C by eauto with asmgen. eauto. auto. - split; intros. apply eval_testcond_compare_uint; auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Ccompshift *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; auto. - destruct r; reflexivity || discriminate. -- (* Ccompushift *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; auto. - destruct r; reflexivity || discriminate. -- (* Cmaskzero *) - destruct (is_logical_imm32 n). -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto. - split; intros. apply (eval_testcond_compare_sint Ceq); auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Cmasknotzero *) - destruct (is_logical_imm32 n). -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto. - split; intros. apply (eval_testcond_compare_sint Cne); auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Ccompl *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_slong; auto. - destruct r; reflexivity || discriminate. -- (* Ccomplu *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. - destruct r; reflexivity || discriminate. -- (* Ccomplimm *) - destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; auto. - destruct r; reflexivity || discriminate. -+ econstructor; split. - apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. - split; intros. apply eval_testcond_compare_slong; auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - simpl. rewrite B, C by eauto with asmgen. eauto. auto. - split; intros. apply eval_testcond_compare_slong; auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Ccompluimm *) - destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. - destruct r; reflexivity || discriminate. -+ econstructor; split. - apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. - split; intros. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. - simpl. rewrite B, C by eauto with asmgen. eauto. - split; intros. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Ccomplshift *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto. - destruct r; reflexivity || discriminate. -- (* Ccomplushift *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. - destruct r; reflexivity || discriminate. -- (* Cmasklzero *) - destruct (is_logical_imm64 n). -+ econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. - split; intros. apply (eval_testcond_compare_slong Ceq); auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Cmasknotzero *) - destruct (is_logical_imm64 n). -+ econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. - split; intros. apply (eval_testcond_compare_slong Cne); auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. -- (* Ccompf *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_float; auto. - destruct r; discriminate || rewrite compare_float_inv; auto. -- (* Cnotcompf *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_not_float; auto. - destruct r; discriminate || rewrite compare_float_inv; auto. -- (* Ccompfzero *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_float; auto. - destruct r; discriminate || rewrite compare_float_inv; auto. -- (* Cnotcompfzero *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_not_float; auto. - destruct r; discriminate || rewrite compare_float_inv; auto. -- (* Ccompfs *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_single; auto. - destruct r; discriminate || rewrite compare_single_inv; auto. -- (* Cnotcompfs *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_not_single; auto. - destruct r; discriminate || rewrite compare_single_inv; auto. -- (* Ccompfszero *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_single; auto. - destruct r; discriminate || rewrite compare_single_inv; auto. -- (* Cnotcompfszero *) - econstructor; split. apply exec_straight_one. simpl; eauto. - split; intros. apply eval_testcond_compare_not_single; auto. - destruct r; discriminate || rewrite compare_single_inv; auto. + - (* Ccomp *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. + - (* Ccompu *) + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. apply eval_testcond_compare_uint; auto. + destruct r; reflexivity || discriminate. + - (* Ccompimm *) + destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. + + econstructor; split. + apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto. + split; intros. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. + split; intros. apply eval_testcond_compare_sint; auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Ccompuimm *) + destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_uint; auto. + destruct r; reflexivity || discriminate. + + econstructor; split. + apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto. + split; intros. apply eval_testcond_compare_uint; auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply eval_testcond_compare_uint; auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Ccompshift *) + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. + - (* Ccompushift *) + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; auto. + destruct r; reflexivity || discriminate. + - (* Cmaskzero *) + destruct (is_logical_imm32 n). + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply (eval_testcond_compare_sint Ceq); auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Cmasknotzero *) + destruct (is_logical_imm32 n). + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply (eval_testcond_compare_sint Cne); auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Ccompl *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_slong; auto. + destruct r; reflexivity || discriminate. + - (* Ccomplu *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + destruct r; reflexivity || discriminate. + - (* Ccomplimm *) + destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; auto. + destruct r; reflexivity || discriminate. + + econstructor; split. + apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. + split; intros. apply eval_testcond_compare_slong; auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply eval_testcond_compare_slong; auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Ccompluimm *) + destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. + + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + destruct r; reflexivity || discriminate. + + econstructor; split. + apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. + split; intros. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. + split; intros. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Ccomplshift *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto. + destruct r; reflexivity || discriminate. + - (* Ccomplushift *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + destruct r; reflexivity || discriminate. + - (* Cmasklzero *) + destruct (is_logical_imm64 n). + + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. + split; intros. apply (eval_testcond_compare_slong Ceq); auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Cmasknotzero *) + destruct (is_logical_imm64 n). + + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto. + destruct r; reflexivity || discriminate. + + exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. + split; intros. apply (eval_testcond_compare_slong Cne); auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. + - (* Ccompf *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_float; auto. + destruct r; discriminate || rewrite compare_float_inv; auto. + - (* Cnotcompf *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_not_float; auto. + destruct r; discriminate || rewrite compare_float_inv; auto. + - (* Ccompfzero *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_float; auto. + destruct r; discriminate || rewrite compare_float_inv; auto. + - (* Cnotcompfzero *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_not_float; auto. + destruct r; discriminate || rewrite compare_float_inv; auto. + - (* Ccompfs *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_single; auto. + destruct r; discriminate || rewrite compare_single_inv; auto. + - (* Cnotcompfs *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_not_single; auto. + destruct r; discriminate || rewrite compare_single_inv; auto. + - (* Ccompfszero *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_single; auto. + destruct r; discriminate || rewrite compare_single_inv; auto. + - (* Cnotcompfszero *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_not_single; auto. + destruct r; discriminate || rewrite compare_single_inv; auto. Qed. Lemma transl_cond_correct': @@ -1351,90 +1351,90 @@ Local Opaque transl_cond transl_cond_branch_default. destruct args as [ | a1 args]; simpl in TR; auto. destruct args as [ | a2 args]; simpl in TR; auto. destruct cond; simpl in TR; auto. -- (* Ccompimm *) - destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto; - apply Int.same_if_eq in N0; subst n; ArgsInv. -+ (* Ccompimm Cne 0 *) - econstructor; split. econstructor. - split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. - unfold incrPC. Simpl. rewrite EQRSX. simpl. auto. -+ (* Ccompimm Ceq 0 *) - econstructor; split. econstructor. - split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. - unfold incrPC. Simpl. rewrite EQRSX. simpl. - destruct (Int.eq i Int.zero); auto. -- (* Ccompuimm *) - destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto. - apply Int.same_if_eq in N0; subst n; ArgsInv. -+ (* Ccompuimm Cne 0 *) - econstructor; split. econstructor. - split; auto. simpl. apply Val_cmpu_bool_correct in EV. - unfold incrPC. Simpl. rewrite EV. auto. -+ (* Ccompuimm Ceq 0 *) - monadInv TR. ArgsInv. simpl in *. - econstructor; split. econstructor. - split; auto. simpl. unfold incrPC. Simpl. - apply Int.same_if_eq in N0; subst. - rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cne), EV. - destruct b; auto. -- (* Cmaskzero *) - destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv. - econstructor; split. econstructor. - split; auto. simpl. - erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto. - unfold incrPC. Simpl. - rewrite (Val.negate_cmp_bool Ceq), EV. destruct b; auto. -- (* Cmasknotzero *) - destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv. - econstructor; split. econstructor. - split; auto. simpl. - erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto. - unfold incrPC. Simpl. - rewrite EV. auto. -- (* Ccomplimm *) - destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; - apply Int64.same_if_eq in N0; subst n; ArgsInv. -+ (* Ccomplimm Cne 0 *) - econstructor; split. econstructor. - split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. - unfold incrPC. Simpl. rewrite EQRSX. simpl. auto. -+ (* Ccomplimm Ceq 0 *) - econstructor; split. econstructor. - split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. - unfold incrPC. Simpl. rewrite EQRSX. simpl. - destruct (Int64.eq i Int64.zero); auto. -- (* Ccompluimm *) - destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; - apply Int64.same_if_eq in N0; subst n; ArgsInv. -+ (* Ccompluimm Cne 0 *) - econstructor; split. econstructor. - split; auto. simpl. apply Val_cmplu_bool_correct in EV. - unfold incrPC. Simpl. rewrite EV. auto. -+ (* Ccompluimm Ceq 0 *) - econstructor; split. econstructor. - split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. - unfold incrPC. Simpl. rewrite EQRSX. simpl. - destruct (Int64.eq i Int64.zero); auto. - unfold incrPC. Simpl. rewrite EQRSX. simpl. - rewrite SF in *; simpl in *. - rewrite Int64.eq_true in *. - destruct ((Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); simpl in *. - assert (b = true). { destruct b; try congruence. } - rewrite H; auto. discriminate. -- (* Cmasklzero *) - destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv. - econstructor; split. econstructor. - split; auto. - erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto. - unfold incrPC. Simpl. - rewrite (Val.negate_cmpl_bool Ceq), EV. destruct b; auto. -- (* Cmasklnotzero *) - destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv. - econstructor; split. econstructor. - split; auto. - erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto. - unfold incrPC. Simpl. - rewrite EV. auto. + - (* Ccompimm *) + destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto; + apply Int.same_if_eq in N0; subst n; ArgsInv. + + (* Ccompimm Cne 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. + unfold incrPC. Simpl. rewrite EQRSX. simpl. auto. + + (* Ccompimm Ceq 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. + unfold incrPC. Simpl. rewrite EQRSX. simpl. + destruct (Int.eq i Int.zero); auto. + - (* Ccompuimm *) + destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto. + apply Int.same_if_eq in N0; subst n; ArgsInv. + + (* Ccompuimm Cne 0 *) + econstructor; split. econstructor. + split; auto. simpl. apply Val_cmpu_bool_correct in EV. + unfold incrPC. Simpl. rewrite EV. auto. + + (* Ccompuimm Ceq 0 *) + monadInv TR. ArgsInv. simpl in *. + econstructor; split. econstructor. + split; auto. simpl. unfold incrPC. Simpl. + apply Int.same_if_eq in N0; subst. + rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cne), EV. + destruct b; auto. + - (* Cmaskzero *) + destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv. + econstructor; split. econstructor. + split; auto. simpl. + erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto. + unfold incrPC. Simpl. + rewrite (Val.negate_cmp_bool Ceq), EV. destruct b; auto. + - (* Cmasknotzero *) + destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv. + econstructor; split. econstructor. + split; auto. simpl. + erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto. + unfold incrPC. Simpl. + rewrite EV. auto. + - (* Ccomplimm *) + destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; + apply Int64.same_if_eq in N0; subst n; ArgsInv. + + (* Ccomplimm Cne 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. + unfold incrPC. Simpl. rewrite EQRSX. simpl. auto. + + (* Ccomplimm Ceq 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. + unfold incrPC. Simpl. rewrite EQRSX. simpl. + destruct (Int64.eq i Int64.zero); auto. + - (* Ccompluimm *) + destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; + apply Int64.same_if_eq in N0; subst n; ArgsInv. + + (* Ccompluimm Cne 0 *) + econstructor; split. econstructor. + split; auto. simpl. apply Val_cmplu_bool_correct in EV. + unfold incrPC. Simpl. rewrite EV. auto. + + (* Ccompluimm Ceq 0 *) + econstructor; split. econstructor. + split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl. + unfold incrPC. Simpl. rewrite EQRSX. simpl. + destruct (Int64.eq i Int64.zero); auto. + unfold incrPC. Simpl. rewrite EQRSX. simpl. + rewrite SF in *; simpl in *. + rewrite Int64.eq_true in *. + destruct ((Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); simpl in *. + assert (b = true). { destruct b; try congruence. } + rewrite H; auto. discriminate. + - (* Cmasklzero *) + destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv. + econstructor; split. econstructor. + split; auto. + erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto. + unfold incrPC. Simpl. + rewrite (Val.negate_cmpl_bool Ceq), EV. destruct b; auto. + - (* Cmasklnotzero *) + destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv. + econstructor; split. econstructor. + split; auto. + erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto. + unfold incrPC. Simpl. + rewrite EV. auto. Qed. Lemma transl_op_correct: @@ -1451,200 +1451,200 @@ Local Opaque Int.eq Int64.eq Val.add Val.addl Int.zwordsize Int64.zwordsize. intros until c; intros TR EV. unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl; try (rewrite <- transl_eval_shift; TranslOpSimpl). -- (* move *) - destruct (preg_of res), (preg_of m0); try destruct d; try destruct d0; inv TR; TranslOpSimpl. -- (* intconst *) - exploit exec_loadimm32. intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen. -- (* longconst *) - exploit exec_loadimm64. intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen. -- (* floatconst *) - destruct (Float.eq_dec n Float.zero). -+ subst n. TranslOpSimpl. -+ TranslOpSimplN. -- (* singleconst *) - destruct (Float32.eq_dec n Float32.zero). -+ subst n. TranslOpSimpl. -+ TranslOpSimplN. -- (* loadsymbol *) - exploit (exec_loadsymbol x id ofs). eauto with asmgen. intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* addrstack *) - exploit (exec_addimm64 x XSP (Ptrofs.to_int64 ofs)); try discriminate. simpl; eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. replace (DR XSP) with (SP) in B by auto. rewrite B. -Local Transparent Val.addl. - destruct (rs SP); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto. - auto. -- (* shift *) - rewrite <- transl_eval_shift'. TranslOpSimpl. -- (* addimm *) - exploit (exec_addimm32 x x0 n). eauto with asmgen. intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* mul *) - TranslOpBase. -Local Transparent Val.add. - destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int.add_zero_l; auto. -- (* andimm *) - exploit (exec_logicalimm32 (Pandimm W) (Pand W)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* orimm *) - exploit (exec_logicalimm32 (Porrimm W) (Porr W)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* xorimm *) - exploit (exec_logicalimm32 (Peorimm W) (Peor W)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* not *) - TranslOpBase. - destruct (rs x0); auto. simpl. rewrite Int.or_zero_l; auto. -- (* notshift *) - TranslOpBase. - destruct (eval_shift s (rs x0) a); auto. simpl. rewrite Int.or_zero_l; auto. -- (* shrx *) - assert (Val.maketotal (Val.shrx (rs x0) (Vint n)) = Val.maketotal (Val.shrx (rs x0) (Vint n))) by eauto. - destruct (Val.shrx) eqn:E. - + exploit (exec_shrx32 x x0 n); eauto with asmgen. intros (rs' & A & B & C). + - (* move *) + destruct (preg_of res), (preg_of m0); try destruct d; try destruct d0; inv TR; TranslOpSimpl. + - (* intconst *) + exploit exec_loadimm32. intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen. + - (* longconst *) + exploit exec_loadimm64. intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen. + - (* floatconst *) + destruct (Float.eq_dec n Float.zero). + + subst n. TranslOpSimpl. + + TranslOpSimplN. + - (* singleconst *) + destruct (Float32.eq_dec n Float32.zero). + + subst n. TranslOpSimpl. + + TranslOpSimplN. + - (* loadsymbol *) + exploit (exec_loadsymbol x id ofs). eauto with asmgen. intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* addrstack *) + exploit (exec_addimm64 x XSP (Ptrofs.to_int64 ofs)); try discriminate. simpl; eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. replace (DR XSP) with (SP) in B by auto. rewrite B. + Local Transparent Val.addl. + destruct (rs SP); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto. + auto. + - (* shift *) + rewrite <- transl_eval_shift'. TranslOpSimpl. + - (* addimm *) + exploit (exec_addimm32 x x0 n). eauto with asmgen. intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* mul *) + TranslOpBase. + Local Transparent Val.add. + destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int.add_zero_l; auto. + - (* andimm *) + exploit (exec_logicalimm32 (Pandimm W) (Pand W)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* orimm *) + exploit (exec_logicalimm32 (Porrimm W) (Porr W)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* xorimm *) + exploit (exec_logicalimm32 (Peorimm W) (Peor W)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* not *) + TranslOpBase. + destruct (rs x0); auto. simpl. rewrite Int.or_zero_l; auto. + - (* notshift *) + TranslOpBase. + destruct (eval_shift s (rs x0) a); auto. simpl. rewrite Int.or_zero_l; auto. + - (* shrx *) + assert (Val.maketotal (Val.shrx (rs x0) (Vint n)) = Val.maketotal (Val.shrx (rs x0) (Vint n))) by eauto. + destruct (Val.shrx) eqn:E. + + exploit (exec_shrx32 x x0 n); eauto with asmgen. intros (rs' & A & B & C). + econstructor; split. eexact A. split. rewrite B; auto. auto. + + exploit (exec_shrx32_none x x0 n); eauto with asmgen. + - (* zero-ext *) + TranslOpBase. + destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto. + - (* sign-ext *) + TranslOpBase. + destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto. + - (* shlzext *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite <- Int.shl_zero_ext_min; auto using a32_range. + - (* shlsext *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite <- Int.shl_sign_ext_min; auto using a32_range. + - (* zextshr *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.zero_ext_shru_min; auto using a32_range. + - (* sextshr *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.sign_ext_shr_min; auto using a32_range. + - (* shiftl *) + rewrite <- transl_eval_shiftl'. TranslOpSimpl. + - (* extend *) + exploit (exec_move_extended x0 x1 x a k). intros (rs' & A & B & C). + econstructor; split. eexact A. + split. rewrite B; auto. eauto with asmgen. + - (* addlshift *) + TranslOpBase. + - (* addext *) + exploit (exec_arith_extended Val.addl Paddext (Padd X)). + auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C). econstructor; split. eexact A. split. rewrite B; auto. auto. - + exploit (exec_shrx32_none x x0 n); eauto with asmgen. -- (* zero-ext *) - TranslOpBase. - destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto. -- (* sign-ext *) - TranslOpBase. - destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto. -- (* shlzext *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite <- Int.shl_zero_ext_min; auto using a32_range. -- (* shlsext *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite <- Int.shl_sign_ext_min; auto using a32_range. -- (* zextshr *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.zero_ext_shru_min; auto using a32_range. -- (* sextshr *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.sign_ext_shr_min; auto using a32_range. -- (* shiftl *) - rewrite <- transl_eval_shiftl'. TranslOpSimpl. -- (* extend *) - exploit (exec_move_extended x0 x1 x a k). intros (rs' & A & B & C). - econstructor; split. eexact A. - split. rewrite B; auto. eauto with asmgen. -- (* addlshift *) - TranslOpBase. -- (* addext *) - exploit (exec_arith_extended Val.addl Paddext (Padd X)). - auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C). - econstructor; split. eexact A. split. rewrite B; auto. auto. -- (* addlimm *) - exploit (exec_addimm64 x x0 n). simpl. generalize (ireg_of_not_X16 _ _ EQ1). congruence. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. simpl in B; rewrite B; auto. auto. -- (* neglshift *) - TranslOpBase. -- (* sublshift *) - TranslOpBase. -- (* subext *) - exploit (exec_arith_extended Val.subl Psubext (Psub X)). - auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C). - econstructor; split. eexact A. split. rewrite B; auto. auto. -- (* mull *) - TranslOpBase. - destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int64.add_zero_l; auto. -- (* andlshift *) - TranslOpBase. -- (* andlimm *) - exploit (exec_logicalimm64 (Pandimm X) (Pand X)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* orlshift *) - TranslOpBase. -- (* orlimm *) - exploit (exec_logicalimm64 (Porrimm X) (Porr X)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* orlshift *) - TranslOpBase. -- (* xorlimm *) - exploit (exec_logicalimm64 (Peorimm X) (Peor X)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* notl *) - TranslOpBase. - destruct (rs x0); auto. simpl. rewrite Int64.or_zero_l; auto. -- (* notlshift *) - TranslOpBase. - destruct (eval_shiftl s (rs x0) a); auto. simpl. rewrite Int64.or_zero_l; auto. -- (* biclshift *) - TranslOpBase. -- (* ornlshift *) - TranslOpBase. -- (* eqvlshift *) - TranslOpBase. -- (* shrx *) - assert (Val.maketotal (Val.shrxl (rs x0) (Vint n)) = Val.maketotal (Val.shrxl (rs x0) (Vint n))) by eauto. - destruct (Val.shrxl) eqn:E. - + exploit (exec_shrx64 x x0 n); eauto with asmgen. intros (rs' & A & B & C). + - (* addlimm *) + exploit (exec_addimm64 x x0 n). simpl. generalize (ireg_of_not_X16 _ _ EQ1). congruence. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. simpl in B; rewrite B; auto. auto. + - (* neglshift *) + TranslOpBase. + - (* sublshift *) + TranslOpBase. + - (* subext *) + exploit (exec_arith_extended Val.subl Psubext (Psub X)). + auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C). econstructor; split. eexact A. split. rewrite B; auto. auto. - + exploit (exec_shrx64_none x x0 n); eauto with asmgen. -- (* zero-ext-l *) - TranslOpBase. - destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto. -- (* sign-ext-l *) - TranslOpBase. - destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto. -- (* shllzext *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_zero_ext_min; auto using a64_range. -- (* shllsext *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_sign_ext_min; auto using a64_range. -- (* zextshrl *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.zero_ext_shru'_min; auto using a64_range. -- (* sextshrl *) - TranslOpBase. - destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.sign_ext_shr'_min; auto using a64_range. -- (* condition *) - exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. - split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. - rewrite (B b) by auto. auto. - auto. - intros; Simpl. -- (* select *) - destruct (preg_of res) as [[ir|fr]|cr|] eqn:RES; monadInv TR. - + (* integer *) - generalize (ireg_of_eq _ _ EQ) (ireg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2. + - (* mull *) + TranslOpBase. + destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int64.add_zero_l; auto. + - (* andlshift *) + TranslOpBase. + - (* andlimm *) + exploit (exec_logicalimm64 (Pandimm X) (Pand X)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* orlshift *) + TranslOpBase. + - (* orlimm *) + exploit (exec_logicalimm64 (Porrimm X) (Porr X)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* orlshift *) + TranslOpBase. + - (* xorlimm *) + exploit (exec_logicalimm64 (Peorimm X) (Peor X)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. + - (* notl *) + TranslOpBase. + destruct (rs x0); auto. simpl. rewrite Int64.or_zero_l; auto. + - (* notlshift *) + TranslOpBase. + destruct (eval_shiftl s (rs x0) a); auto. simpl. rewrite Int64.or_zero_l; auto. + - (* biclshift *) + TranslOpBase. + - (* ornlshift *) + TranslOpBase. + - (* eqvlshift *) + TranslOpBase. + - (* shrx *) + assert (Val.maketotal (Val.shrxl (rs x0) (Vint n)) = Val.maketotal (Val.shrxl (rs x0) (Vint n))) by eauto. + destruct (Val.shrxl) eqn:E. + + exploit (exec_shrx64 x x0 n); eauto with asmgen. intros (rs' & A & B & C). + econstructor; split. eexact A. split. rewrite B; auto. auto. + + exploit (exec_shrx64_none x x0 n); eauto with asmgen. + - (* zero-ext-l *) + TranslOpBase. + destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto. + - (* sign-ext-l *) + TranslOpBase. + destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto. + - (* shllzext *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_zero_ext_min; auto using a64_range. + - (* shllsext *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_sign_ext_min; auto using a64_range. + - (* zextshrl *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.zero_ext_shru'_min; auto using a64_range. + - (* sextshrl *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.sign_ext_shr'_min; auto using a64_range. + - (* condition *) exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. - rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize. - rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. - auto. - intros; Simpl. - + (* FP *) - generalize (freg_of_eq _ _ EQ) (freg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2. - exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). - econstructor; split. - eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. - split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. - rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize. - rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. + rewrite (B b) by auto. auto. auto. intros; Simpl. + - (* select *) + destruct (preg_of res) as [[ir|fr]|cr|] eqn:RES; monadInv TR. + + (* integer *) + generalize (ireg_of_eq _ _ EQ) (ireg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2. + exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. + split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. + rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize. + rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. + auto. + intros; Simpl. + + (* FP *) + generalize (freg_of_eq _ _ EQ) (freg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2. + exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. + split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. + rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize. + rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. + auto. + intros; Simpl. Qed. (** Translation of addressing modes, loads, stores *) @@ -1660,68 +1660,68 @@ Lemma transl_addressing_correct: Proof. intros until o; intros TR EV. unfold transl_addressing in TR; destruct addr; ArgsInv; SimplEval EV. -- (* Aindexed *) - destruct (offset_representable sz ofs); inv EQ0. -+ econstructor; econstructor; split. apply exec_straight_opt_refl. - auto. -+ exploit (exec_loadimm64 X16 ofs). intros (rs' & A & B & C). - econstructor; exists rs'; split. apply exec_straight_opt_intro; eexact A. - split. simpl. rewrite B, C by eauto with asmgen. auto. - eauto with asmgen. -- (* Aindexed2 *) - econstructor; econstructor; split. apply exec_straight_opt_refl. - auto. -- (* Aindexed2shift *) - destruct (Int.eq a Int.zero) eqn:E; [|destruct (Int.eq (Int.shl Int.one a) (Int.repr sz))]; inv EQ2. -+ apply Int.same_if_eq in E. rewrite E. - econstructor; econstructor; split. apply exec_straight_opt_refl. - split; auto. simpl. - rewrite Val.addl_commut in H0. destruct (rs x0); try discriminate. - unfold Val.shll. rewrite Int64.shl'_zero. auto. -+ econstructor; econstructor; split. apply exec_straight_opt_refl. - auto. -+ econstructor; econstructor; split. - apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. - split. simpl. Simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero. auto. - intros; Simpl. -- (* Aindexed2ext *) - destruct (Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz)); inv EQ2. -+ econstructor; econstructor; split. apply exec_straight_opt_refl. - split; auto. destruct x; auto. -+ exploit (exec_arith_extended Val.addl Paddext (Padd X)); auto. - instantiate (1 := x0). eauto with asmgen. - intros (rs' & A & B & C). - econstructor; exists rs'; split. - apply exec_straight_opt_intro. eexact A. - split. simpl. rewrite B. rewrite Val.addl_assoc. f_equal. - unfold Op.eval_extend; destruct x, (rs x1); simpl; auto; rewrite ! a64_range; - simpl; rewrite Int64.add_zero; auto. - intros. apply C; eauto with asmgen. -- (* Aglobal *) - destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR. -+ econstructor; econstructor; split. - apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. - split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence. - intros; Simpl. -+ exploit (exec_loadsymbol X16 id ofs). auto. intros (rs' & A & B & C). - econstructor; exists rs'; split. - apply exec_straight_opt_intro. eexact A. - split. simpl. - rewrite B. rewrite <- Genv.shift_symbol_address_64, Ptrofs.add_zero by auto. - simpl in EV. congruence. - auto with asmgen. -- (* Ainstrack *) - assert (E: Val.addl (rs SP) (Vlong (Ptrofs.to_int64 ofs)) = Vptr b o). - { simpl in EV. inv EV. destruct (rs SP); simpl in H1; inv H1. simpl. - rewrite Ptrofs.of_int64_to_int64 by auto. auto. } - destruct (offset_representable sz (Ptrofs.to_int64 ofs)); inv TR. -+ econstructor; econstructor; split. apply exec_straight_opt_refl. - auto. -+ exploit (exec_loadimm64 X16 (Ptrofs.to_int64 ofs)). intros (rs' & A & B & C). - econstructor; exists rs'; split. - apply exec_straight_opt_intro. eexact A. - split. simpl. rewrite B, C by eauto with asmgen. auto. - auto with asmgen. + - (* Aindexed *) + destruct (offset_representable sz ofs); inv EQ0. + + econstructor; econstructor; split. apply exec_straight_opt_refl. + auto. + + exploit (exec_loadimm64 X16 ofs). intros (rs' & A & B & C). + econstructor; exists rs'; split. apply exec_straight_opt_intro; eexact A. + split. simpl. rewrite B, C by eauto with asmgen. auto. + eauto with asmgen. + - (* Aindexed2 *) + econstructor; econstructor; split. apply exec_straight_opt_refl. + auto. + - (* Aindexed2shift *) + destruct (Int.eq a Int.zero) eqn:E; [|destruct (Int.eq (Int.shl Int.one a) (Int.repr sz))]; inv EQ2. + + apply Int.same_if_eq in E. rewrite E. + econstructor; econstructor; split. apply exec_straight_opt_refl. + split; auto. simpl. + rewrite Val.addl_commut in H0. destruct (rs x0); try discriminate. + unfold Val.shll. rewrite Int64.shl'_zero. auto. + + econstructor; econstructor; split. apply exec_straight_opt_refl. + auto. + + econstructor; econstructor; split. + apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. + split. simpl. Simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero. auto. + intros; Simpl. + - (* Aindexed2ext *) + destruct (Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz)); inv EQ2. + + econstructor; econstructor; split. apply exec_straight_opt_refl. + split; auto. destruct x; auto. + + exploit (exec_arith_extended Val.addl Paddext (Padd X)); auto. + instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + econstructor; exists rs'; split. + apply exec_straight_opt_intro. eexact A. + split. simpl. rewrite B. rewrite Val.addl_assoc. f_equal. + unfold Op.eval_extend; destruct x, (rs x1); simpl; auto; rewrite ! a64_range; + simpl; rewrite Int64.add_zero; auto. + intros. apply C; eauto with asmgen. + - (* Aglobal *) + destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR. + + econstructor; econstructor; split. + apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. + split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence. + intros; Simpl. + + exploit (exec_loadsymbol X16 id ofs). auto. intros (rs' & A & B & C). + econstructor; exists rs'; split. + apply exec_straight_opt_intro. eexact A. + split. simpl. + rewrite B. rewrite <- Genv.shift_symbol_address_64, Ptrofs.add_zero by auto. + simpl in EV. congruence. + auto with asmgen. + - (* Ainstrack *) + assert (E: Val.addl (rs SP) (Vlong (Ptrofs.to_int64 ofs)) = Vptr b o). + { simpl in EV. inv EV. destruct (rs SP); simpl in H1; inv H1. simpl. + rewrite Ptrofs.of_int64_to_int64 by auto. auto. } + destruct (offset_representable sz (Ptrofs.to_int64 ofs)); inv TR. + + econstructor; econstructor; split. apply exec_straight_opt_refl. + auto. + + exploit (exec_loadimm64 X16 (Ptrofs.to_int64 ofs)). intros (rs' & A & B & C). + econstructor; exists rs'; split. + apply exec_straight_opt_intro. eexact A. + split. simpl. rewrite B, C by eauto with asmgen. auto. + auto with asmgen. Qed. Lemma transl_load_correct: @@ -1806,11 +1806,11 @@ Proof. assert (Val.addl rs#base (Vlong (Ptrofs.to_int64 ofs)) = Vptr b i). { destruct (rs base); try discriminate. simpl in *. rewrite Ptrofs.of_int64_to_int64 by auto. auto. } destruct offset_representable. -- econstructor; econstructor; split. apply exec_straight_opt_refl. auto. -- exploit (exec_loadimm64 X16); eauto. intros (rs' & A & B & C). - econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A. - split. simpl. rewrite B, C; eauto; try discriminate. - unfold preg_of_iregsp in H. destruct base; auto. auto. + - econstructor; econstructor; split. apply exec_straight_opt_refl. auto. + - exploit (exec_loadimm64 X16); eauto. intros (rs' & A & B & C). + econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A. + split. simpl. rewrite B, C; eauto; try discriminate. + unfold preg_of_iregsp in H. destruct base; auto. auto. Qed. Lemma loadptr_correct: forall (base: iregsp) ofs dst k m v (rs: regset), @@ -1952,4 +1952,4 @@ Proof. intros. Simpl. Qed. -End CONSTRUCTORS.
\ No newline at end of file +End CONSTRUCTORS. diff --git a/aarch64/Asmblockprops.v b/aarch64/Asmblockprops.v index cef95aad..38fbd6d3 100644 --- a/aarch64/Asmblockprops.v +++ b/aarch64/Asmblockprops.v @@ -67,34 +67,6 @@ Proof. intros. unfold preg_of; destruct r; simpl; try discriminate. Qed. -(* -Lemma preg_of_not_SP: - forall r, preg_of r <> SP. -Proof. - intros. unfold preg_of; destruct r; cbn; congruence. -Qed. - -Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. - - -Lemma nextblock_pc: - forall b rs, (nextblock b rs)#PC = Val.offset_ptr rs#PC (Ptrofs.repr (size b)). -Proof. - intros. apply Pregmap.gss. -Qed. - -Lemma nextblock_inv: - forall b r rs, r <> PC -> (nextblock b rs)#r = rs#r. -Proof. - intros. unfold nextblock. apply Pregmap.gso. red; intro; subst. auto. -Qed. - -Lemma nextblock_inv1: - forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r. -Proof. - intros. apply nextblock_inv. red; intro; subst; discriminate. -Qed.*) - Ltac desif := repeat match goal with | [ |- context[ if ?f then _ else _ ] ] => destruct f @@ -145,219 +117,3 @@ Proof. Qed. End EPC. - -(* - -(* For PostpassSchedulingproof *) - -Lemma regset_double_set: - forall r1 r2 (rs: regset) v1 v2, - r1 <> r2 -> - (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1). -Proof. - intros. apply functional_extensionality. intros r. destruct (preg_eq r r1). - - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto. - - destruct (preg_eq r r2). - + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto. - + repeat (rewrite Pregmap.gso; auto). -Qed. - -Lemma next_eq: - forall (rs rs': regset) m m', - rs = rs' -> m = m' -> Next rs m = Next rs' m'. -Proof. - intros; apply f_equal2; auto. -Qed. - -Lemma exec_load_offset_pc_var: - forall trap t rs m rd ra ofs rs' m' v, - exec_load_offset trap t rs m rd ra ofs = Next rs' m' -> - exec_load_offset trap t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ofs); try discriminate. - destruct (Mem.loadv _ _ _). - - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - unfold parexec_incorrect_load in *. - destruct trap; try discriminate. - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. -Qed. - -Lemma exec_load_reg_pc_var: - forall trap t rs m rd ra ro rs' m' v, - exec_load_reg trap t rs m rd ra ro = Next rs' m' -> - exec_load_reg trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_load_reg in *. unfold parexec_load_reg in *. rewrite Pregmap.gso; try discriminate. - destruct (Mem.loadv _ _ _). - - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - unfold parexec_incorrect_load in *. - destruct trap; try discriminate. - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. -Qed. - -Lemma exec_load_regxs_pc_var: - forall trap t rs m rd ra ro rs' m' v, - exec_load_regxs trap t rs m rd ra ro = Next rs' m' -> - exec_load_regxs trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate. - destruct (Mem.loadv _ _ _). - - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. - - unfold parexec_incorrect_load in *. - destruct trap; try discriminate. - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate. -Qed. - -Lemma exec_load_offset_q_pc_var: - forall rs m rd ra ofs rs' m' v, - exec_load_q_offset rs m rd ra ofs = Next rs' m' -> - exec_load_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_load_q_offset in *. unfold parexec_load_q_offset in *. - destruct (gpreg_q_expand rd) as [rd0 rd1]. - (* destruct (ireg_eq rd0 ra); try discriminate. *) - rewrite Pregmap.gso; try discriminate. - destruct (Mem.loadv _ _ _); try discriminate. - inv H. - destruct (Mem.loadv _ _ _); try discriminate. - inv H1. f_equal. - rewrite (regset_double_set PC rd0) by discriminate. - rewrite (regset_double_set PC rd1) by discriminate. - reflexivity. -Qed. - -Lemma exec_load_offset_o_pc_var: - forall rs m rd ra ofs rs' m' v, - exec_load_o_offset rs m rd ra ofs = Next rs' m' -> - exec_load_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_load_o_offset in *. unfold parexec_load_o_offset in *. - destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3]. -(* - destruct (ireg_eq rd0 ra); try discriminate. - destruct (ireg_eq rd1 ra); try discriminate. - destruct (ireg_eq rd2 ra); try discriminate. -*) - rewrite Pregmap.gso; try discriminate. - cbn in *. - destruct (Mem.loadv _ _ _); try discriminate. - destruct (Mem.loadv _ _ _); try discriminate. - destruct (Mem.loadv _ _ _); try discriminate. - destruct (Mem.loadv _ _ _); try discriminate. - rewrite (regset_double_set PC rd0) by discriminate. - rewrite (regset_double_set PC rd1) by discriminate. - rewrite (regset_double_set PC rd2) by discriminate. - rewrite (regset_double_set PC rd3) by discriminate. - inv H. - trivial. -Qed. - -Lemma exec_store_offset_pc_var: - forall t rs m rd ra ofs rs' m' v, - exec_store_offset t rs m rd ra ofs = Next rs' m' -> - exec_store_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_store_offset in *. unfold parexec_store_offset in *. rewrite Pregmap.gso; try discriminate. - destruct (eval_offset ofs); try discriminate. - destruct (Mem.storev _ _ _). - - inv H. apply next_eq; auto. - - discriminate. -Qed. - -Lemma exec_store_q_offset_pc_var: - forall rs m rd ra ofs rs' m' v, - exec_store_q_offset rs m rd ra ofs = Next rs' m' -> - exec_store_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_store_q_offset in *. unfold parexec_store_q_offset in *. rewrite Pregmap.gso; try discriminate. - cbn in *. - destruct (gpreg_q_expand _) as [s0 s1]. - destruct (Mem.storev _ _ _); try discriminate. - destruct (Mem.storev _ _ _); try discriminate. - inv H. apply next_eq; auto. -Qed. - -Lemma exec_store_o_offset_pc_var: - forall rs m rd ra ofs rs' m' v, - exec_store_o_offset rs m rd ra ofs = Next rs' m' -> - exec_store_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. -Proof. - intros. - unfold exec_store_o_offset in *. unfold parexec_store_o_offset in *. - destruct (gpreg_o_expand _) as [[[s0 s1] s2] s3]. - destruct (Mem.storev _ _ _); try discriminate. - destruct (Mem.storev _ _ _); try discriminate. - destruct (Mem.storev _ _ _); try discriminate. - destruct (Mem.storev _ _ _); try discriminate. - inv H. - trivial. -Qed. - -Lemma exec_store_reg_pc_var: - forall t rs m rd ra ro rs' m' v, - exec_store_reg t rs m rd ra ro = Next rs' m' -> - exec_store_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_store_reg in *. unfold parexec_store_reg in *. rewrite Pregmap.gso; try discriminate. - destruct (Mem.storev _ _ _). - - inv H. apply next_eq; auto. - - discriminate. -Qed. - -Lemma exec_store_regxs_pc_var: - forall t rs m rd ra ro rs' m' v, - exec_store_regxs t rs m rd ra ro = Next rs' m' -> - exec_store_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. -Proof. - intros. unfold exec_store_regxs in *. unfold parexec_store_regxs in *. rewrite Pregmap.gso; try discriminate. - destruct (Mem.storev _ _ _). - - inv H. apply next_eq; auto. - - discriminate. -Qed. - -Theorem exec_basic_instr_pc_var: - forall ge i rs m rs' m' v, - exec_basic_instr ge i rs m = Next rs' m' -> - exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'. -Proof. - intros. unfold exec_basic_instr in *. unfold bstep in *. destruct i. - - unfold exec_arith_instr in *. destruct i; destruct i. - all: try (exploreInst; inv H; apply next_eq; auto; - apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). -(* - (* Some cases treated seperately because exploreInst destructs too much *) - all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). *) - - destruct i. - + exploreInst; apply exec_load_offset_pc_var; auto. - + exploreInst; apply exec_load_reg_pc_var; auto. - + exploreInst; apply exec_load_regxs_pc_var; auto. - + apply exec_load_offset_q_pc_var; auto. - + apply exec_load_offset_o_pc_var; auto. - - destruct i. - + exploreInst; apply exec_store_offset_pc_var; auto. - + exploreInst; apply exec_store_reg_pc_var; auto. - + exploreInst; apply exec_store_regxs_pc_var; auto. - + apply exec_store_q_offset_pc_var; auto. - + apply exec_store_o_offset_pc_var; auto. - - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate). - destruct (Mem.storev _ _ _ _); try discriminate. - inv H. apply next_eq; auto. apply functional_extensionality. intros. - rewrite (regset_double_set GPR32 PC); try discriminate. - rewrite (regset_double_set GPR12 PC); try discriminate. - rewrite (regset_double_set FP PC); try discriminate. reflexivity. - - repeat (rewrite Pregmap.gso; try discriminate). - destruct (Mem.loadv _ _ _); try discriminate. - destruct (rs GPR12); try discriminate. - destruct (Mem.free _ _ _ _); try discriminate. - inv H. apply next_eq; auto. - rewrite (regset_double_set GPR32 PC). - rewrite (regset_double_set GPR12 PC). reflexivity. - all: discriminate. - - destruct rs0; try discriminate. inv H. apply next_eq; auto. - repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate. - - destruct rd; try discriminate. inv H. apply next_eq; auto. - repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate. - - inv H. apply next_eq; auto. -Qed. - -*) |