diff options
Diffstat (limited to 'kvx/lib/Machblockgen.v')
| -rw-r--r-- | kvx/lib/Machblockgen.v | 27 |
1 files changed, 16 insertions, 11 deletions
diff --git a/kvx/lib/Machblockgen.v b/kvx/lib/Machblockgen.v index 287e4f7b..3d5d7b2c 100644 --- a/kvx/lib/Machblockgen.v +++ b/kvx/lib/Machblockgen.v @@ -29,6 +29,8 @@ Require Import Mach. Require Import Linking. Require Import Machblock. +(** * Tail-recursive (greedy) translation from Mach code to Machblock code *) + Inductive Machblock_inst: Type := | MB_label (lbl: label) | MB_basic (bi: basic_inst) @@ -71,9 +73,12 @@ Definition add_to_new_bblock (i:Machblock_inst) : bblock := | MB_cfi i => cfi_bblock i end. -(** Adding an instruction to the beginning of a bblock list - * Either adding the instruction to the head of the list, - * or create a new bblock with the instruction *) +(** Adding an instruction to the beginning of a bblock list by + +- either adding the instruction to the head of the list, + +- or creating a new bblock with the instruction +*) Definition add_to_code (i:Machblock_inst) (bl:code) : code := match bl with | bh::bl0 => match i with @@ -112,7 +117,7 @@ Definition transf_program (src: Mach.program) : program := transform_program transf_fundef src. -(** Abstracting trans_code *) +(** * Abstracting trans_code with a simpler inductive relation *) Inductive is_end_block: Machblock_inst -> code -> Prop := | End_empty mbi: is_end_block mbi nil @@ -143,11 +148,11 @@ Lemma add_to_code_is_trans_code i c bl: is_trans_code c bl -> is_trans_code (i::c) (add_to_code (trans_inst i) bl). Proof. - destruct bl as [|bh0 bl]; simpl. + destruct bl as [|bh0 bl]; cbn. - 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. + + intros; eapply Tr_add_label; eauto. destruct i; cbn in * |- *; congruence. + intros. remember (header bh0) as hbh0. destruct hbh0 as [|b]. * eapply Tr_add_basic; eauto. * cutrewrite (add_basic bi empty_bblock = add_to_new_bblock (MB_basic bi)); auto. @@ -165,7 +170,7 @@ Lemma trans_code_is_trans_code_rev c1: forall c2 mbi, is_trans_code c2 mbi -> is_trans_code (rev_append c1 c2) (trans_code_rev c1 mbi). Proof. - induction c1 as [| i c1]; simpl; auto. + induction c1 as [| i c1]; cbn; auto. Qed. Lemma trans_code_is_trans_code c: is_trans_code c (trans_code c). @@ -181,17 +186,17 @@ Lemma add_to_code_is_trans_code_inv i c bl: is_trans_code (i::c) bl -> exists bl0, is_trans_code c bl0 /\ bl = add_to_code (trans_inst i) bl0. Proof. intro H; inversion H as [|H0 H1 bl0| | H0 bi bh H1 bl0]; clear H; subst; (repeat econstructor); eauto. - + (* case Tr_end_block *) inversion H3; subst; simpl; auto. + + (* case Tr_end_block *) inversion H3; subst; cbn; auto. * destruct (header bh); congruence. - * destruct bl0; simpl; congruence. - + (* case Tr_add_basic *) rewrite H3. simpl. destruct (header bh); congruence. + * destruct bl0; cbn; congruence. + + (* case Tr_add_basic *) rewrite H3. cbn. destruct (header bh); congruence. Qed. Lemma trans_code_is_trans_code_rev_inv c1: forall c2 mbi, is_trans_code (rev_append c1 c2) mbi -> exists mbi0, is_trans_code c2 mbi0 /\ mbi=trans_code_rev c1 mbi0. Proof. - induction c1 as [| i c1]; simpl; eauto. + induction c1 as [| i c1]; cbn; eauto. intros; exploit IHc1; eauto. intros (mbi0 & H1 & H2); subst. exploit add_to_code_is_trans_code_inv; eauto. |