aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2018-09-05 11:40:07 +0200
committerCyril SIX <cyril.six@kalray.eu>2018-09-06 15:59:07 +0200
commit3a244908dd9233100075ffe889b3da493cdf9c38 (patch)
tree8c0a40b71d66729e07a52482ead28a0f45c2e59b /mppa_k1c
parent1412a262c0bb95ebc78ac7c4d79e0fa81954c82a (diff)
downloadcompcert-kvx-3a244908dd9233100075ffe889b3da493cdf9c38.tar.gz
compcert-kvx-3a244908dd9233100075ffe889b3da493cdf9c38.zip
Remplacement de match_prog par un plus classique
Diffstat (limited to 'mppa_k1c')
-rw-r--r--mppa_k1c/Asm.v85
-rw-r--r--mppa_k1c/Asmgenproof.v23
-rw-r--r--mppa_k1c/Machblockgenproof.v4
3 files changed, 70 insertions, 42 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index d71304fa..f0284c26 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -359,11 +359,7 @@ Proof.
intros f. destruct f as [sig blks]. unfold function_proj. simpl. auto.
Qed.
-Definition transf_fundef (f: Asmblock.fundef) : fundef :=
- match f with
- | Internal f => Internal (transf_function f)
- | External ef => External ef
- end.
+Definition transf_fundef : Asmblock.fundef -> fundef := AST.transf_fundef transf_function.
Lemma transf_fundef_proj: forall f, fundef_proj (transf_fundef f) = f.
Proof.
@@ -371,7 +367,7 @@ Proof.
rewrite transf_function_proj. auto.
Qed.
-Definition transf_globdef (gd: globdef Asmblock.fundef unit) : globdef fundef unit :=
+(* Definition transf_globdef (gd: globdef Asmblock.fundef unit) : globdef fundef unit :=
match gd with
| Gfun f => Gfun (transf_fundef f)
| Gvar gu => Gvar gu
@@ -398,16 +394,11 @@ Proof.
rewrite transf_globdef_proj.
congruence.
Qed.
+ *)
-Definition transf_program (p: Asmblock.program) : program :=
- {| prog_defs := transf_prog_defs (prog_defs p);
- prog_public := prog_public p;
- prog_main := prog_main p
- |}.
-
-Definition match_prog (p: Asmblock.program) (tp: program) := (p = program_proj tp).
+Definition transf_program : Asmblock.program -> program := transform_program transf_fundef.
-Lemma asmblock_program_equals: forall (p1 p2: Asmblock.program),
+Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B),
prog_defs p1 = prog_defs p2 ->
prog_public p1 = prog_public p2 ->
prog_main p1 = prog_main p2 ->
@@ -416,14 +407,47 @@ Proof.
intros. destruct p1. destruct p2. simpl in *. subst. auto.
Qed.
+Lemma transf_program_proj: forall p, program_proj (transf_program p) = p.
+Proof.
+ intros p. destruct p as [defs pub main]. unfold program_proj. simpl.
+ apply program_equals; simpl; auto.
+ induction defs.
+ - simpl; auto.
+ - simpl. rewrite IHdefs.
+ destruct a as [id gd]; simpl.
+ destruct gd as [f|v]; simpl; auto.
+ rewrite transf_fundef_proj. auto.
+Qed.
+
+Definition match_prog (p: Asmblock.program) (tp: program) :=
+ match_program (fun _ f tf => tf = transf_fundef f) eq p tp.
+
Lemma transf_program_match:
forall p tp, transf_program p = tp -> match_prog p tp.
Proof.
- intros p tp H. unfold match_prog.
- unfold transf_program in H.
- destruct tp as [tdefs tpub tmain]. inv H.
- unfold program_proj. simpl. apply asmblock_program_equals; simpl; auto.
- apply transf_prog_proj.
+ intros. rewrite <- H. eapply match_transform_program; eauto.
+Qed.
+
+Lemma cons_extract {A: Type} : forall (l: list A) a b, a = b -> a::l = b::l.
+Proof.
+ intros. congruence.
+Qed.
+
+(* I think it is a special case of Asmblock -> Asm. Very handy to have *)
+Lemma match_program_transf:
+ forall p tp, match_prog p tp -> transf_program p = tp.
+Proof.
+ intros p tp H. inversion_clear H. inv H1.
+ destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. simpl in *.
+ subst. unfold transf_program. unfold transform_program. simpl.
+ apply program_equals; simpl; auto.
+ induction H0; simpl; auto.
+ rewrite IHlist_forall2. apply cons_extract.
+ destruct a1 as [ida gda]. destruct b1 as [idb gdb].
+ simpl in *.
+ inv H. inv H2.
+ - simpl in *. subst. auto.
+ - simpl in *. subst. inv H. auto.
Qed.
Section PRESERVATION.
@@ -436,16 +460,25 @@ Let tge := Genv.globalenv tprog.
Definition match_states (s1 s2: state) := s1 = s2.
+Lemma symbols_preserved:
+ forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof (Genv.find_symbol_match TRANSF).
+
+Lemma senv_preserved:
+ Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSF).
+
+
Theorem transf_program_correct:
forward_simulation (Asmblock.semantics prog) (semantics tprog).
Proof.
- inversion TRANSF. (* inv H0. *)
- eapply forward_simulation_step with (match_states := match_states).
- all: try (simpl; congruence).
- - simpl. intros s1 H1. exists s1. split; auto. congruence.
- - simpl. intros s1 t s1' H1 s2 H2. exists s1'. split.
- + congruence.
- + unfold match_states. auto.
+ pose proof (match_program_transf prog tprog TRANSF) as TR.
+ subst. unfold semantics. rewrite transf_program_proj.
+
+ eapply forward_simulation_step with (match_states := match_states); simpl; auto.
+ - intros. exists s1. split; auto. congruence.
+ - intros. inv H. auto.
+ - intros. exists s1'. inv H0. split; auto. congruence.
Qed.
End PRESERVATION. \ No newline at end of file
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 87c4184b..20691183 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -18,32 +18,26 @@ Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Mach Conventions Asm Asmgen Machblockgen Asmblockgen.
Require Import Machblockgenproof Asmblockgenproof.
-(* Local Open Scope linking_scope.
+Local Open Scope linking_scope.
Definition block_passes :=
mkpass Machblockgenproof.match_prog
::: mkpass Asmblockgenproof.match_prog
::: mkpass Asm.match_prog
::: pass_nil _.
- *)
-Inductive match_prog : Mach.program -> Asm.program -> Prop :=
- | mk_match_prog: forall p mbp abp tp,
- Machblockgen.transf_program p = mbp -> Machblockgenproof.match_prog p mbp ->
- Asmblockgen.transf_program mbp = OK abp -> Asmblockgenproof.match_prog mbp abp ->
- Asm.match_prog abp tp ->
- match_prog p tp.
+Definition match_prog := pass_match (compose_passes block_passes).
Lemma transf_program_match:
forall p tp, Asmgen.transf_program p = OK tp -> match_prog p tp.
Proof.
intros p tp H.
unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
- inversion_clear H. inversion_clear H1. remember (Machblockgen.transf_program p) as mbp.
- constructor 1 with (mbp:=mbp) (abp:=x); auto.
- subst. apply Machblockgenproof.transf_program_match.
- apply Asmblockgenproof.transf_program_match. auto.
- apply Asm.transf_program_match. auto.
+ inversion_clear H. inversion H1. remember (Machblockgen.transf_program p) as mbp.
+ unfold match_prog; simpl.
+ exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
+ exists x; split. apply Asmblockgenproof.transf_program_match; auto.
+ exists tp; split. apply Asm.transf_program_match; auto. auto.
Qed.
Section PRESERVATION.
@@ -57,7 +51,8 @@ Let tge := Genv.globalenv tprog.
Theorem transf_program_correct:
forward_simulation (Mach.semantics (inv_trans_rao return_address_offset) prog) (Asm.semantics tprog).
Proof.
- inv TRANSF.
+ unfold match_prog in TRANSF. simpl in TRANSF.
+ inv TRANSF. inv H. inv H1. inv H. inv H2. inv H.
eapply compose_forward_simulations. apply Machblockgenproof.transf_program_correct; eauto.
eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
apply Asm.transf_program_correct. eauto.
diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v
index ff9c29d3..45ea53cc 100644
--- a/mppa_k1c/Machblockgenproof.v
+++ b/mppa_k1c/Machblockgenproof.v
@@ -23,9 +23,9 @@ Definition inv_trans_rao (rao: function -> code -> ptrofs -> Prop) (f: Mach.func
Definition match_prog (p: Mach.program) (tp: Machblock.program) :=
match_program (fun _ f tf => tf = trans_fundef f) eq p tp.
-Lemma transf_program_match: forall p, match_prog p (transf_program p).
+Lemma transf_program_match: forall p tp, transf_program p = tp -> match_prog p tp.
Proof.
- intros. eapply match_transform_program; eauto.
+ intros. rewrite <- H. eapply match_transform_program; eauto.
Qed.
Definition trans_stackframe (msf: Mach.stackframe) : stackframe :=