Commit 91a07b5e authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Cleanup

parent 3d1aea48
......@@ -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)
......
......@@ -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.
......@@ -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.
This diff is collapsed.
......@@ -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.
*)