diff options
| author | tvdd <tvdd@debian.lan> | 2019-03-05 11:09:52 +0100 |
|---|---|---|
| committer | tvdd <tvdd@debian.lan> | 2019-03-05 11:09:52 +0100 |
| commit | 6c51fda9e503953a4f8ca3e2448b8040158ddc94 (patch) | |
| tree | 06576c6a47514c8dd14f86cc665c7eb447118e68 | |
| parent | a86b505f9c392a558315df2d7acd08e914795f38 (diff) | |
| download | compcert-kvx-6c51fda9e503953a4f8ca3e2448b8040158ddc94.tar.gz compcert-kvx-6c51fda9e503953a4f8ca3e2448b8040158ddc94.zip | |
add_to_code_is_trans_code proof
| -rw-r--r-- | mppa_k1c/Machblockgen.v | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v index 18abb927..7206fb51 100644 --- a/mppa_k1c/Machblockgen.v +++ b/mppa_k1c/Machblockgen.v @@ -126,7 +126,15 @@ Inductive is_trans_code: Mach.code -> code -> Prop := is_trans_code c (bh::bl) -> trans_inst i = MB_basic bi -> header bh = nil -> - is_trans_code (i::c) (add_basic bi bh::bl). + is_trans_code (i::c) (add_basic bi bh::bl) + | Tr_empty_bblock c bh bl: + is_trans_code c bl -> + bh = empty_bblock -> + is_trans_code c (bh::bl) + | Tr_cfi i bi c bl: + is_trans_code c bl -> + trans_inst i = MB_cfi bi -> + is_trans_code (i::c) (cfi_bblock bi :: bl). Local Hint Resolve Tr_nil Tr_end_block. @@ -135,12 +143,15 @@ Lemma add_to_code_is_trans_code i c bl: is_trans_code (i::c) (add_to_code (trans_inst i) bl). Proof. destruct bl as [|bh0 bl]; simpl. - - intro H; inversion H; subst; eauto. + - intro H. inversion H. subst. eauto. - remember (trans_inst i) as ti. destruct ti as [l|bi|cfi]. + intros; eapply Tr_add_label; eauto. destruct i; simpl in * |- *; congruence. - + -Admitted. (* A FINIR *) + + intros. remember (header bh0) as hbh0. destruct hbh0 as [|b]. + * eapply Tr_add_basic; eauto. + * eapply Tr_add_basic; eauto. eapply Tr_empty_bblock. eauto. reflexivity. + + intros. eapply Tr_cfi. eauto. symmetry in Heqti. eauto. +Qed. (* A FINIR *) Local Hint Resolve add_to_code_is_trans_code. |