diff options
Diffstat (limited to 'kvx/lib')
| -rw-r--r-- | kvx/lib/ForwardSimulationBlock.v | 30 | ||||
| -rw-r--r-- | kvx/lib/Machblock.v | 29 | ||||
| -rw-r--r-- | kvx/lib/Machblockgen.v | 27 | ||||
| -rw-r--r-- | kvx/lib/Machblockgenproof.v | 138 |
4 files changed, 118 insertions, 106 deletions
diff --git a/kvx/lib/ForwardSimulationBlock.v b/kvx/lib/ForwardSimulationBlock.v index f79814f2..61466dad 100644 --- a/kvx/lib/ForwardSimulationBlock.v +++ b/kvx/lib/ForwardSimulationBlock.v @@ -42,11 +42,11 @@ Lemma starN_split n s t s': forall m k, n=m+k -> exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2. Proof. - induction 1; simpl. + induction 1; cbn. + intros m k H; assert (X: m=0); try omega. assert (X0: k=0); try omega. subst; repeat (eapply ex_intro); intuition eauto. - + intros m; destruct m as [| m']; simpl. + + intros m; destruct m as [| m']; cbn. - intros k H2; subst; repeat (eapply ex_intro); intuition eauto. - intros k H2. inversion H2. exploit (IHstarN m' k); eauto. intro. @@ -61,7 +61,7 @@ Lemma starN_tailstep n s t1 s': forall (t t2:trace) s'', Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''. Proof. - induction 1; simpl. + induction 1; cbn. + intros t t1 s0; autorewrite with trace_rewrite. intros; subst; eapply starN_step; eauto. autorewrite with trace_rewrite; auto. @@ -153,8 +153,8 @@ Definition head (s: memostate): state L1 := Lemma head_followed (s: memostate): follows_in_block (head s) (real s). Proof. - destruct s as [rs ms Hs]. simpl. - destruct ms as [ms|]; unfold head; simpl; auto. + destruct s as [rs ms Hs]. cbn. + destruct ms as [ms|]; unfold head; cbn; auto. constructor 1. omega. cutrewrite ((dist_end_block rs - dist_end_block rs)%nat=O). @@ -198,21 +198,21 @@ Definition memoL1 := {| Lemma discr_dist_end s: {dist_end_block s = O} + {dist_end_block s <> O}. Proof. - destruct (dist_end_block s); simpl; intuition. + destruct (dist_end_block s); cbn; intuition. Qed. Lemma memo_simulation_step: forall s1 t s1', Step L1 s1 t s1' -> forall s2, s1 = (real s2) -> exists s2', Step memoL1 s2 t s2' /\ s1' = (real s2'). Proof. - intros s1 t s1' H1 [rs2 ms2 Hmoi] H2. simpl in H2; subst. + intros s1 t s1' H1 [rs2 ms2 Hmoi] H2. cbn in H2; subst. destruct (discr_dist_end rs2) as [H3 | H3]. - + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); simpl. + + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); cbn. intuition. + destruct ms2 as [s|]. - - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); simpl. + - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); cbn. intuition. - - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); simpl. + - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); cbn. intuition. Unshelve. * intros; discriminate. @@ -228,7 +228,7 @@ Qed. Lemma forward_memo_simulation_1: forward_simulation L1 memoL1. Proof. apply forward_simulation_step with (match_states:=fun s1 s2 => s1 = (real s2)); auto. - + intros s1 H; eapply ex_intro with (x:={|real:=s1; memorized:=None |}); simpl. + + intros s1 H; eapply ex_intro with (x:={|real:=s1; memorized:=None |}); cbn. intuition. + intros; subst; auto. + intros; exploit memo_simulation_step; eauto. @@ -239,8 +239,8 @@ Qed. Lemma forward_memo_simulation_2: forward_simulation memoL1 L2. Proof. - unfold memoL1; simpl. - apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => match_states (head s1) s2); simpl; auto. + unfold memoL1; cbn. + apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => match_states (head s1) s2); cbn; auto. + intros s1 [H0 H1]; destruct (match_initial_states (real s1) H0). unfold head; rewrite H1. intuition eauto. @@ -254,14 +254,14 @@ Proof. - (* MidBloc *) constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto. unfold head in * |- *. rewrite H3. rewrite H4. intuition. - destruct (memorized s1); simpl; auto. tauto. + destruct (memorized s1); cbn; auto. tauto. - (* EndBloc *) constructor 1. destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto. * destruct (head_followed s1) as [H4 H3]. cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3; try omega. eapply starN_tailstep; eauto. - * unfold head; rewrite H2; simpl. intuition eauto. + * unfold head; rewrite H2; cbn. intuition eauto. Qed. Lemma forward_simulation_block_rel: forward_simulation L1 L2. diff --git a/kvx/lib/Machblock.v b/kvx/lib/Machblock.v index 08e0eba2..404c2a96 100644 --- a/kvx/lib/Machblock.v +++ b/kvx/lib/Machblock.v @@ -12,6 +12,8 @@ (* *) (* *************************************************************) +(** Abstract syntax and semantics of a Mach variant, structured with basic-blocks. *) + Require Import Coqlib. Require Import Maps. Require Import AST. @@ -28,7 +30,9 @@ Require Stacklayout. Require Import Mach. Require Import Linking. -(** basic instructions (ie no control-flow) *) +(** * Abstract Syntax *) + +(** ** basic instructions (ie no control-flow) *) Inductive basic_inst: Type := | MBgetstack: ptrofs -> typ -> mreg -> basic_inst | MBsetstack: mreg -> ptrofs -> typ -> basic_inst @@ -40,7 +44,7 @@ Inductive basic_inst: Type := Definition bblock_body := list basic_inst. -(** control flow instructions *) +(** ** control flow instructions *) Inductive control_flow_inst: Type := | MBcall: signature -> mreg + ident -> control_flow_inst | MBtailcall: signature -> mreg + ident -> control_flow_inst @@ -51,6 +55,7 @@ Inductive control_flow_inst: Type := | MBreturn: control_flow_inst . +(** ** basic block *) Record bblock := mk_bblock { header: list label; body: bblock_body; @@ -65,7 +70,7 @@ Lemma bblock_eq: b1 = b2. Proof. intros. destruct b1. destruct b2. - simpl in *. subst. auto. + cbn in *. subst. auto. Qed. Definition length_opt {A} (o: option A) : nat := @@ -80,17 +85,19 @@ Lemma size_null b: size b = 0%nat -> header b = nil /\ body b = nil /\ exit b = None. Proof. - destruct b as [h b e]. simpl. unfold size. simpl. + destruct b as [h b e]. cbn. unfold size. cbn. intros H. assert (length h = 0%nat) as Hh; [ omega |]. assert (length b = 0%nat) as Hb; [ omega |]. assert (length_opt e = 0%nat) as He; [ omega|]. repeat split. - destruct h; try (simpl in Hh; discriminate); auto. - destruct b; try (simpl in Hb; discriminate); auto. - destruct e; try (simpl in He; discriminate); auto. + destruct h; try (cbn in Hh; discriminate); auto. + destruct b; try (cbn in Hb; discriminate); auto. + destruct e; try (cbn in He; discriminate); auto. Qed. +(** ** programs *) + Definition code := list bblock. Record function: Type := mkfunction @@ -106,7 +113,7 @@ Definition program := AST.program fundef unit. Definition genv := Genv.t fundef unit. -(*** sémantique ***) +(** * Operational (blockstep) semantics ***) Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }. Proof. @@ -120,13 +127,13 @@ Definition is_label (lbl: label) (bb: bblock) : bool := Lemma is_label_correct_true lbl bb: List.In lbl (header bb) <-> is_label lbl bb = true. Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. Qed. Lemma is_label_correct_false lbl bb: ~(List.In lbl (header bb)) <-> is_label lbl bb = false. Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. Qed. @@ -155,7 +162,7 @@ Definition find_function_ptr Genv.find_symbol ge symb end. -(** Machblock execution states. *) +(** ** Machblock execution states. *) Inductive stackframe: Type := | Stackframe: 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. diff --git a/kvx/lib/Machblockgenproof.v b/kvx/lib/Machblockgenproof.v index dfb97bfe..fc722887 100644 --- a/kvx/lib/Machblockgenproof.v +++ b/kvx/lib/Machblockgenproof.v @@ -146,16 +146,16 @@ Lemma parent_sp_preserved: forall s, Mach.parent_sp s = parent_sp (trans_stack s). Proof. - unfold parent_sp. unfold Mach.parent_sp. destruct s; simpl; auto. - unfold trans_stackframe. destruct s; simpl; auto. + unfold parent_sp. unfold Mach.parent_sp. destruct s; cbn; auto. + unfold trans_stackframe. destruct s; cbn; auto. Qed. Lemma parent_ra_preserved: forall s, Mach.parent_ra s = parent_ra (trans_stack s). Proof. - unfold parent_ra. unfold Mach.parent_ra. destruct s; simpl; auto. - unfold trans_stackframe. destruct s; simpl; auto. + unfold parent_ra. unfold Mach.parent_ra. destruct s; cbn; auto. + unfold trans_stackframe. destruct s; cbn; auto. Qed. Lemma external_call_preserved: @@ -175,11 +175,11 @@ Proof. destruct i; try (constructor 2; split; auto; discriminate ). destruct (peq l0 l) as [P|P]. - constructor. subst l0; split; auto. - revert H. unfold Mach.find_label. simpl. rewrite peq_true. + revert H. unfold Mach.find_label. cbn. rewrite peq_true. intros H; injection H; auto. - constructor 2. split. + intro F. injection F. intros. contradict P; auto. - + revert H. unfold Mach.find_label. simpl. rewrite peq_false; auto. + + revert H. unfold Mach.find_label. cbn. rewrite peq_false; auto. Qed. Lemma find_label_is_end_block_not_label i l c bl: @@ -192,24 +192,24 @@ Proof. remember (is_label l _) as b. cutrewrite (b = false); auto. subst; unfold is_label. - destruct i; simpl in * |- *; try (destruct (in_dec l nil); intuition). + destruct i; cbn in * |- *; try (destruct (in_dec l nil); intuition). inversion H. destruct (in_dec l (l0::nil)) as [H6|H6]; auto. - simpl in H6; intuition try congruence. + cbn in H6; intuition try congruence. Qed. Lemma find_label_at_begin l bh bl: In l (header bh) -> find_label l (bh :: bl) = Some (bh::bl). Proof. - unfold find_label; rewrite is_label_correct_true; intro H; rewrite H; simpl; auto. + unfold find_label; rewrite is_label_correct_true; intro H; rewrite H; cbn; auto. Qed. Lemma find_label_add_label_diff l bh bl: ~(In l (header bh)) -> find_label l (bh::bl) = find_label l bl. Proof. - unfold find_label; rewrite is_label_correct_false; intro H; rewrite H; simpl; auto. + unfold find_label; rewrite is_label_correct_false; intro H; rewrite H; cbn; auto. Qed. Definition concat (h: list label) (c: code): code := @@ -227,18 +227,18 @@ Proof. rewrite <- is_trans_code_inv in * |-. induction Heqbl. + (* Tr_nil *) - intros; exists (l::nil); simpl in * |- *; intuition. + intros; exists (l::nil); cbn in * |- *; intuition. discriminate. + (* Tr_end_block *) intros. exploit Mach_find_label_split; eauto. clear H0; destruct 1 as [(H0&H2)|(H0&H2)]. - - subst. rewrite find_label_at_begin; simpl; auto. + - subst. rewrite find_label_at_begin; cbn; auto. inversion H as [mbi H1 H2| | ]. subst. inversion Heqbl. subst. - exists (l :: nil); simpl; eauto. + exists (l :: nil); cbn; eauto. - exploit IHHeqbl; eauto. destruct 1 as (h & H3 & H4). exists h. @@ -251,21 +251,21 @@ Proof. - subst. inversion H0 as [H1]. clear H0. - erewrite find_label_at_begin; simpl; eauto. + erewrite find_label_at_begin; cbn; eauto. subst_is_trans_code Heqbl. - exists (l :: nil); simpl; eauto. + exists (l :: nil); cbn; eauto. - subst; assert (H: l0 <> l); try congruence; clear H0. exploit IHHeqbl; eauto. clear IHHeqbl Heqbl. intros (h & H3 & H4). - simpl; unfold is_label, add_label; simpl. - destruct (in_dec l (l0::header bh)) as [H5|H5]; simpl in H5. + cbn; unfold is_label, add_label; cbn. + destruct (in_dec l (l0::header bh)) as [H5|H5]; cbn in H5. * destruct H5; try congruence. - exists (l0::h); simpl; intuition. + exists (l0::h); cbn; intuition. rewrite find_label_at_begin in H4; auto. apply f_equal. inversion H4 as [H5]. clear H4. - destruct (trans_code c'); simpl in * |- *; - inversion H5; subst; simpl; auto. + destruct (trans_code c'); cbn in * |- *; + inversion H5; subst; cbn; auto. * exists h. intuition. erewrite <- find_label_add_label_diff; eauto. + (* Tr_add_basic *) @@ -318,12 +318,12 @@ Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exe Lemma size_add_label l bh: size (add_label l bh) = size bh + 1. Proof. - unfold add_label, size; simpl; omega. + unfold add_label, size; cbn; omega. Qed. Lemma size_add_basic bi bh: header bh = nil -> size (add_basic bi bh) = size bh + 1. Proof. - intro H. unfold add_basic, size; rewrite H; simpl. omega. + intro H. unfold add_basic, size; rewrite H; cbn. omega. Qed. @@ -418,8 +418,8 @@ Proof. + exists lbl. unfold trans_inst in H1. destruct i; congruence. - + unfold add_basic in H; simpl in H; congruence. - + unfold cfi_bblock in H; simpl in H; congruence. + + unfold add_basic in H; cbn in H; congruence. + + unfold cfi_bblock in H; cbn in H; congruence. Qed. Local Hint Resolve Mlabel_is_not_basic: core. @@ -433,11 +433,11 @@ Proof. intros b bl H; remember (trans_inst i) as ti. destruct ti as [lbl|bi|cfi]; inversion H as [|d0 d1 d2 H0 H1| |]; subst; - try (rewrite <- Heqti in * |- *); simpl in * |- *; + try (rewrite <- Heqti in * |- *); cbn in * |- *; try congruence. + (* label at end block *) inversion H1; subst. inversion H0; subst. - assert (X:i=Mlabel lbl). { destruct i; simpl in Heqti; congruence. } + assert (X:i=Mlabel lbl). { destruct i; cbn in Heqti; congruence. } subst. repeat econstructor; eauto. + (* label at mid block *) exploit IHc; eauto. @@ -451,12 +451,12 @@ Proof. assert (X:(trans_inst i) = MB_basic bi ). { repeat econstructor; congruence. } repeat econstructor; congruence. - exists (i::c), c, c. - repeat econstructor; eauto; inversion H0; subst; repeat econstructor; simpl; try congruence. + repeat econstructor; eauto; inversion H0; subst; repeat econstructor; cbn; try congruence. * exploit (add_to_new_block_is_label i0); eauto. - intros (l & H8); subst; simpl; congruence. + intros (l & H8); subst; cbn; congruence. * exploit H3; eauto. * exploit (add_to_new_block_is_label i0); eauto. - intros (l & H8); subst; simpl; congruence. + intros (l & H8); subst; cbn; congruence. + (* basic at mid block *) inversion H1; subst. exploit IHc; eauto. @@ -476,7 +476,7 @@ Lemma step_simu_header st f sp rs m s c h c' t: starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length h) (Mach.State st f sp c rs m) t s -> s = Mach.State st f sp c' rs m /\ t = E0. Proof. - induction 1; simpl; intros hs; try (inversion hs; tauto). + induction 1; cbn; intros hs; try (inversion hs; tauto). inversion hs as [|n1 s1 t1 t2 s2 t3 s3 H1]. inversion H1. subst. auto. Qed. @@ -487,21 +487,21 @@ Lemma step_simu_basic_step (i: Mach.instruction) (bi: basic_inst) (c: Mach.code) Mach.step (inv_trans_rao rao) ge (Mach.State s f sp (i::c) rs m) t s' -> exists rs' m', s'=Mach.State s f sp c rs' m' /\ t=E0 /\ basic_step tge (trans_stack s) f sp rs m bi rs' m'. Proof. - destruct i; simpl in * |-; + destruct i; cbn in * |-; (discriminate || (intro H; inversion_clear H; intro X; inversion_clear X; eapply ex_intro; eapply ex_intro; intuition eauto)). - eapply exec_MBgetparam; eauto. exploit (functions_translated); eauto. intro. destruct H3 as (tf & A & B). subst. eapply A. - all: simpl; rewrite <- parent_sp_preserved; auto. - - eapply exec_MBop; eauto. rewrite <- H. destruct o; simpl; auto. destruct (rs ## l); simpl; auto. + all: cbn; rewrite <- parent_sp_preserved; auto. + - eapply exec_MBop; eauto. rewrite <- H. destruct o; cbn; auto. destruct (rs ## l); cbn; auto. unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBload; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + - eapply exec_MBload; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. - - eapply exec_MBstore; eauto; rewrite <- H; destruct a; simpl; auto; destruct (rs ## l); simpl; auto; + - eapply exec_MBstore; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; unfold Genv.symbol_address; rewrite symbols_preserved; auto. Qed. @@ -511,7 +511,7 @@ Lemma star_step_simu_body_step s f sp c bdy c': starN (Mach.step (inv_trans_rao rao)) ge (length bdy) (Mach.State s f sp c rs m) t s' -> exists rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp bdy rs m rs' m'. Proof. - induction 1; simpl. + induction 1; cbn. + intros. inversion H. exists rs. exists m. auto. + intros. inversion H0. exists rs. exists m. auto. + intros. inversion H1; subst. @@ -531,15 +531,15 @@ Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved f Lemma match_states_concat_trans_code st f sp c rs m h: match_states (Mach.State st f sp c rs m) (State (trans_stack st) f sp (concat h (trans_code c)) rs m). Proof. - intros; constructor 1; simpl. + intros; constructor 1; cbn. + intros (t0 & s1' & H0) t s'. remember (trans_code _) as bl. destruct bl as [|bh bl]. { rewrite <- is_trans_code_inv in Heqbl; inversion Heqbl; inversion H0; congruence. } clear H0. - simpl; constructor 1; - intros X; inversion X as [d1 d2 d3 d4 d5 d6 d7 rs' m' d10 d11 X1 X2| | | ]; subst; simpl in * |- *; - eapply exec_bblock; eauto; simpl; + cbn; constructor 1; + intros X; inversion X as [d1 d2 d3 d4 d5 d6 d7 rs' m' d10 d11 X1 X2| | | ]; subst; cbn in * |- *; + eapply exec_bblock; eauto; cbn; inversion X2 as [cfi d1 d2 d3 H1|]; subst; eauto; inversion H1; subst; eauto. + intros H r; constructor 1; intro X; inversion X. @@ -551,7 +551,7 @@ Lemma step_simu_cfi_step (i: Mach.instruction) (cfi: control_flow_inst) (c: Mach Mach.step (inv_trans_rao rao) ge (Mach.State stk f sp (i::c) rs m) t s' -> exists s2, cfi_step rao tge cfi (State (trans_stack stk) f sp (b::blc) rs m) t s2 /\ match_states s' s2. Proof. - destruct i; simpl in * |-; + destruct i; cbn in * |-; (intro H; intro Htc;apply is_trans_code_inv in Htc;rewrite Htc;inversion_clear H;intro X; inversion_clear X). * eapply ex_intro. intuition auto. @@ -561,8 +561,8 @@ Proof. intuition auto. eapply exec_MBtailcall;eauto. - rewrite <-H; exploit (find_function_ptr_same); eauto. - - simpl; rewrite <- parent_sp_preserved; auto. - - simpl; rewrite <- parent_ra_preserved; auto. + - cbn; rewrite <- parent_sp_preserved; auto. + - cbn; rewrite <- parent_ra_preserved; auto. * eapply ex_intro. intuition auto. eapply exec_MBbuiltin ;eauto. @@ -605,7 +605,7 @@ Proof. inversion H1; subst. exploit (step_simu_cfi_step); eauto. intros [s2 [Hcfi1 Hcfi3]]. - inversion H4. subst; simpl. + inversion H4. subst; cbn. autorewrite with trace_rewrite. exists s2. split;eauto. @@ -616,7 +616,7 @@ Lemma simu_end_block: starN (Mach.step (inv_trans_rao rao)) ge (Datatypes.S (dist_end_block s1)) s1 t s1' -> exists s2', step rao tge (trans_state s1) t s2' /\ match_states s1' s2'. Proof. - destruct s1; simpl. + destruct s1; cbn. + (* State *) remember (trans_code _) as tc. rewrite <- is_trans_code_inv in Heqtc. @@ -624,7 +624,7 @@ Proof. destruct tc as [|b bl]. { (* nil => absurd *) inversion Heqtc. subst. - unfold dist_end_block_code; simpl. + unfold dist_end_block_code; cbn. inversion_clear H; inversion_clear H0. } @@ -659,7 +659,7 @@ Proof. intros t s1' H; inversion_clear H. eapply ex_intro; constructor 1; eauto. inversion H1; subst; clear H1. - inversion_clear H0; simpl. + inversion_clear H0; cbn. - (* function_internal*) cutrewrite (trans_code (Mach.fn_code f0) = fn_code (transf_function f0)); eauto. eapply exec_function_internal; eauto. @@ -674,7 +674,7 @@ Proof. intros t s1' H; inversion_clear H. eapply ex_intro; constructor 1; eauto. inversion H1; subst; clear H1. - inversion_clear H0; simpl. + inversion_clear H0; cbn. eapply exec_return. Qed. @@ -685,10 +685,10 @@ dist_end_block_code (i :: c) = 0. Proof. unfold dist_end_block_code. intro H. destruct H as [cfi H]. - destruct i;simpl in H;try(congruence); ( + destruct i;cbn in H;try(congruence); ( remember (trans_code _) as bl; rewrite <- is_trans_code_inv in Heqbl; - inversion Heqbl; subst; simpl in * |- *; try (congruence)). + inversion Heqbl; subst; cbn in * |- *; try (congruence)). Qed. Theorem transf_program_correct: @@ -697,23 +697,23 @@ Proof. apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := trans_state). (* simu_mid_block *) - intros s1 t s1' H1 H2. - destruct H1; simpl in * |- *; omega || (intuition auto); - destruct H2; eapply cfi_dist_end_block; simpl; eauto. + destruct H1; cbn in * |- *; omega || (intuition auto); + destruct H2; eapply cfi_dist_end_block; cbn; eauto. (* public_preserved *) - apply senv_preserved. (* match_initial_states *) - - intros. simpl. + - intros. cbn. eapply ex_intro; constructor 1. eapply match_states_trans_state. destruct H. split. apply init_mem_preserved; auto. rewrite prog_main_preserved. rewrite <- H0. apply symbols_preserved. (* match_final_states *) - - intros. simpl. destruct H. split with (r := r); auto. + - intros. cbn. destruct H. split with (r := r); auto. (* final_states_end_block *) - - intros. simpl in H0. + - intros. cbn in H0. inversion H0. - inversion H; simpl; auto. + inversion H; cbn; auto. all: try (subst; discriminate). apply cfi_dist_end_block; exists MBreturn; eauto. (* simu_end_block *) @@ -733,8 +733,8 @@ Proof. intro H; destruct c as [|i' c]. { inversion H. } remember (trans_inst i) as ti. destruct ti as [lbl|bi|cfi]. - - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; simpl in * |- *; try congruence ). - exists nil; simpl; eexists. eapply Tr_add_label; eauto. + - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ). + exists nil; cbn; eexists. eapply Tr_add_label; eauto. - (*i=basic*) destruct i'. 10: { exists (add_to_new_bblock (MB_basic bi)::nil). exists b. @@ -742,11 +742,11 @@ Proof. rewrite Heqti. eapply Tr_end_block; eauto. rewrite <-Heqti. - eapply End_basic. inversion H; try(simpl; congruence). - simpl in H5; congruence. } - all: try(exists nil; simpl; eexists; eapply Tr_add_basic; eauto; inversion H; try(eauto || congruence)). + eapply End_basic. inversion H; try(cbn; congruence). + cbn in H5; congruence. } + all: try(exists nil; cbn; eexists; eapply Tr_add_basic; eauto; inversion H; try(eauto || congruence)). - (*i=cfi*) - destruct i; try(simpl in Heqti; congruence). + destruct i; try(cbn in Heqti; congruence). all: exists (add_to_new_bblock (MB_cfi cfi)::nil); exists b; cutrewrite ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto; rewrite Heqti; @@ -768,13 +768,13 @@ Qed. (* FIXME: these two lemma should go into [Coqlib.v] *) Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2). Proof. - induction l1; simpl; auto with coqlib. + induction l1; cbn; auto with coqlib. Qed. Hint Resolve is_tail_app: coqlib. Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3. Proof. - induction l1; simpl; auto with coqlib. + induction l1; cbn; auto with coqlib. intros l2 l3 H; inversion H; eauto with coqlib. Qed. Hint Resolve is_tail_app_inv: coqlib. @@ -787,17 +787,17 @@ Proof. - intros; subst. remember (trans_code (Mcall _ _::c)) as tc2. rewrite <- is_trans_code_inv in Heqtc2. - inversion Heqtc2; simpl in * |- *; subst; try congruence. + inversion Heqtc2; cbn in * |- *; subst; try congruence. subst_is_trans_code H1. eapply ex_intro; eauto with coqlib. - intros; exploit IHis_tail; eauto. clear IHis_tail. intros (b & Hb). inversion Hb; clear Hb. * exploit (trans_code_monotonic i c2); eauto. intros (l' & b' & Hl'); rewrite Hl'. - exists b'; simpl; eauto with coqlib. + exists b'; cbn; eauto with coqlib. * exploit (trans_code_monotonic i c2); eauto. intros (l' & b' & Hl'); rewrite Hl'. - simpl; eapply ex_intro. + cbn; eapply ex_intro. eapply is_tail_trans; eauto with coqlib. Qed. |