diff options
Diffstat (limited to 'mppa_k1c/Asmblockgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 52 |
1 files changed, 26 insertions, 26 deletions
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 70f188ec..e3be258a 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -19,9 +19,9 @@ Require Import Op Locations Machblock Conventions Asmblock. Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1.
Module MB := Machblock.
-Module AB := Asmblock.
+Module AB := Asmvliw.
-Definition match_prog (p: Machblock.program) (tp: Asmblock.program) :=
+Definition match_prog (p: Machblock.program) (tp: Asmvliw.program) :=
match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
Lemma transf_program_match:
@@ -33,7 +33,7 @@ Qed. Section PRESERVATION.
Variable prog: Machblock.program.
-Variable tprog: Asmblock.program.
+Variable tprog: Asmvliw.program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
@@ -259,7 +259,7 @@ Proof. exploit label_pos_code_tail; eauto. instantiate (1 := 0).
intros [pos' [P [Q R]]].
exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))).
- split. unfold goto_label. rewrite P. rewrite H1. auto.
+ split. unfold goto_label. unfold par_goto_label. rewrite P. rewrite H1. auto.
split. rewrite Pregmap.gss. constructor; auto.
rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
auto. omega.
@@ -318,7 +318,7 @@ Proof. exploit preg_of_injective; eauto. intros; subst r; discriminate.
Qed.
-Inductive match_states: Machblock.state -> Asmblock.state -> Prop :=
+Inductive match_states: Machblock.state -> Asmvliw.state -> Prop :=
| match_states_intro:
forall s fb sp c ep ms m m' rs f tf tc
(STACKS: match_stack ge s)
@@ -328,7 +328,7 @@ Inductive match_states: Machblock.state -> Asmblock.state -> Prop := (AG: agree ms sp rs)
(DXP: ep = true -> rs#FP = parent_sp s),
match_states (Machblock.State s fb sp c ms m)
- (Asmblock.State rs m')
+ (Asmvliw.State rs m')
| match_states_call:
forall s fb ms m m' rs
(STACKS: match_stack ge s)
@@ -337,7 +337,7 @@ Inductive match_states: Machblock.state -> Asmblock.state -> Prop := (ATPC: rs PC = Vptr fb Ptrofs.zero)
(ATLR: rs RA = parent_ra s),
match_states (Machblock.Callstate s fb ms m)
- (Asmblock.State rs m')
+ (Asmvliw.State rs m')
| match_states_return:
forall s ms m m' rs
(STACKS: match_stack ge s)
@@ -345,7 +345,7 @@ Inductive match_states: Machblock.state -> Asmblock.state -> Prop := (AG: agree ms (parent_sp s) rs)
(ATPC: rs PC = parent_ra s),
match_states (Machblock.Returnstate s ms m)
- (Asmblock.State rs m').
+ (Asmvliw.State rs m').
Record codestate :=
Codestate { pstate: state;
@@ -373,7 +373,7 @@ Inductive match_codestate fb: Machblock.state -> codestate -> Prop := (DXP: (if MB.header bb then ep else false) = true -> rs0#FP = parent_sp s)
,
match_codestate fb (Machblock.State s fb sp (bb::c) ms m)
- {| pstate := (Asmblock.State rs0 m0);
+ {| pstate := (Asmvliw.State rs0 m0);
pheader := (MB.header bb);
pbody1 := tbc;
pbody2 := (extract_basic tbi);
@@ -384,7 +384,7 @@ Inductive match_codestate fb: Machblock.state -> codestate -> Prop := |}
.
-Inductive match_asmstate fb: codestate -> Asmblock.state -> Prop :=
+Inductive match_asmstate fb: codestate -> Asmvliw.state -> Prop :=
| match_asmstate_some:
forall rs f tf tc m tbb ofs ep tbdy tex lhd
(FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
@@ -394,7 +394,7 @@ Inductive match_asmstate fb: codestate -> Asmblock.state -> Prop := (* (HDROK: header tbb = lhd) *)
,
match_asmstate fb
- {| pstate := (Asmblock.State rs m);
+ {| pstate := (Asmvliw.State rs m);
pheader := lhd;
pbody1 := tbdy;
pbody2 := extract_basic tex;
@@ -402,7 +402,7 @@ Inductive match_asmstate fb: codestate -> Asmblock.state -> Prop := fpok := ep;
rem := tc;
cur := Some tbb |}
- (Asmblock.State rs m)
+ (Asmvliw.State rs m)
.
Ltac exploreInst :=
@@ -716,11 +716,11 @@ Theorem step_simu_control: MB.body bb' = nil ->
(forall ef args res, MB.exit bb' <> Some (MBbuiltin ef args res)) ->
Genv.find_funct_ptr tge fb = Some (Internal fn) ->
- pstate cs2 = (Asmblock.State rs2 m2) ->
+ pstate cs2 = (Asmvliw.State rs2 m2) ->
pbody1 cs2 = nil -> pbody2 cs2 = tbdy2 -> pctl cs2 = tex ->
cur cs2 = Some tbb ->
match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2 ->
- match_asmstate fb cs2 (Asmblock.State rs1 m1) ->
+ match_asmstate fb cs2 (Asmvliw.State rs1 m1) ->
exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') E0 S'' ->
(exists rs3 m3 rs4 m4,
exec_body tge tbdy2 rs2 m2 = Next rs3 m3
@@ -839,7 +839,7 @@ Proof. exploit find_label_goto_label.
eauto. eauto.
instantiate (2 := rs2').
- { subst. unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. eauto. }
+ { subst. unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. eauto. }
eauto.
intros (tc' & rs' & GOTO & AT2 & INV).
@@ -847,7 +847,7 @@ Proof. rewrite H6. simpl extract_basic. simpl. eauto.
rewrite H7. simpl extract_ctl. simpl. rewrite <- Heqrs2'. eauto.
econstructor; eauto.
- rewrite Heqrs2' in INV. unfold nextblock in INV.
+ rewrite Heqrs2' in INV. unfold nextblock, incrPC in INV.
eapply agree_exten; eauto with asmgen.
assert (forall r : preg, r <> PC -> rs' r = rs2 r).
{ intros. destruct r.
@@ -886,7 +886,7 @@ Proof. econstructor; eauto.
eapply agree_exten with rs2; eauto with asmgen.
{ intros. destruct r; try destruct g; try discriminate.
- all: rewrite Hrs3; try discriminate; unfold nextblock; Simpl. }
+ all: rewrite Hrs3; try discriminate; unfold nextblock, incrPC; Simpl. }
intros. discriminate.
* (* MBcond false *)
@@ -912,10 +912,10 @@ Proof. rewrite H7. rewrite <- BTC. rewrite extract_ctl_basics_to_code. simpl extract_ctl. rewrite B. eauto.
econstructor; eauto.
- unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto.
+ unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto.
eapply agree_exten with rs2; eauto with asmgen.
{ intros. destruct r; try destruct g; try discriminate.
- all: rewrite <- C; try discriminate; unfold nextblock; Simpl. }
+ all: rewrite <- C; try discriminate; unfold nextblock, incrPC; Simpl. }
intros. discriminate.
+ (* MBjumptable *)
destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
@@ -926,7 +926,7 @@ Proof. generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV.
assert (f1 = f) by congruence. subst f1.
exploit find_label_goto_label. 4: eapply H16. 1-2: eauto. instantiate (2 := (nextblock tbb rs2) # GPR62 <- Vundef # GPR63 <- Vundef).
- unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity.
+ unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity.
exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn.
intros [tc' [rs' [A [B C]]]].
@@ -959,7 +959,7 @@ Proof. rewrite H6. simpl extract_basic. eauto.
rewrite H7. simpl extract_ctl. simpl. reflexivity.
econstructor; eauto.
- unfold nextblock. repeat apply agree_set_other; auto with asmgen.
+ unfold nextblock, incrPC. repeat apply agree_set_other; auto with asmgen.
- inv MCS. inv MAS. simpl in *. subst. inv Hpstate. inv Hcur.
(* exploit transl_blocks_distrib; eauto. (* rewrite <- H2. discriminate. *)
@@ -969,7 +969,7 @@ Proof. monadInv TBC. monadInv TIC. simpl in *. rewrite H5. rewrite H6.
simpl. repeat eexists.
econstructor. 4: instantiate (3 := false). all:eauto.
- unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq.
+ unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq.
assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
eapply transf_function_no_overflow; eauto.
assert (f = f0) by congruence. subst f0. econstructor; eauto.
@@ -1398,7 +1398,7 @@ Proof. eapply exec_step_internal; eauto. eapply find_bblock_tail; eauto.
unfold exec_bblock. simpl. eauto.
econstructor. eauto. eauto. eauto.
- unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite <- H.
+ unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite <- H.
assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
eapply transf_function_no_overflow; eauto.
econstructor; eauto.
@@ -1581,7 +1581,7 @@ Proof. eauto.
econstructor; eauto.
instantiate (2 := tf); instantiate (1 := x0).
- unfold nextblock. rewrite Pregmap.gss.
+ unfold nextblock, incrPC. rewrite Pregmap.gss.
rewrite set_res_other. rewrite undef_regs_other_2. rewrite Pregmap.gso by congruence.
rewrite <- H. simpl. econstructor; eauto.
eapply code_tail_next_int; eauto.
@@ -1680,7 +1680,7 @@ Proof. { change (fn_blocks tf) with tfbody; unfold tfbody.
apply exec_straight_blocks_step with rs2 m2'.
unfold exec_bblock. simpl exec_body. rewrite C. fold sp. simpl exec_control.
- rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. reflexivity.
+ rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. rewrite regset_same_assign. reflexivity.
reflexivity.
eapply exec_straight_blocks_trans.
- eexact W'.
@@ -1775,7 +1775,7 @@ Definition return_address_offset : Machblock.function -> Machblock.code -> ptrof Asmblockgenproof0.return_address_offset.
Theorem transf_program_correct:
- forward_simulation (MB.semantics return_address_offset prog) (AB.semantics tprog).
+ forward_simulation (MB.semantics return_address_offset prog) (Asmblock.semantics tprog).
Proof.
eapply forward_simulation_star with (measure := measure).
- apply senv_preserved.
|