Require Export Marksweep_concrete. Require Import Events. Require Import Cmconstrproof. Load param. Ltac redenv_hyp := match goal with | H : (PTree.set ?a _ _) ! ?a = _ |- _ => rewrite PTree.gss in H | H : (PTree.set ?a ?v ?e) ! ?b = _ |- _ => rewrite (PTree.gso (i := b) (j := a) v e) in H ; auto end. Ltac redenv := match goal with | |- (PTree.set ?a _ _) ! ?a = _ => rewrite PTree.gss | |- (PTree.set ?a ?v ?e) ! ?b = _ => rewrite (PTree.gso (i := b) (j := a) v e) ; auto end. Ltac endsubst0 := match goal with | _ : ?m1 = ?m2 |- _ => (subst m1 || subst m2) end. Ltac endsubst := repeat endsubst0. Ltac invclear H := inversion H ; clear H ; endsubst. Ltac run0 := match goal with | H : eval_expr _ _ _ _ _ ?e _ _ _ |- _ => match e with | Cmconstr.and _ _ => unfold Cmconstr.and in H ; invclear H | Cmconstr.or _ _ => unfold Cmconstr.or in H ; invclear H | Evar _ => invclear H | Eop _ _ => invclear H | Eload _ _ _ => invclear H | Estore _ _ _ _ => invclear H | Ecall _ _ _ => invclear H | Econdition _ _ _ => invclear H | Elet _ _ => invclear H | Eletvar _ => invclear H | Ealloc _ => invclear H end | H : exec_stmt _ _ _ _ ?stmt _ _ _ _ |- _ => match stmt with | Cmconstr.ifthenelse _ _ _ => unfold Cmconstr.ifthenelse in H ; invclear H | Sseq _ _ => invclear H (* | Sloop _ => invclear H *) | Sreturn _ => invclear H | Sskip => invclear H | Sexpr _ => invclear H | Sassign _ _ => invclear H | Sifthenelse _ _ _ => invclear H | Sblock _ => invclear H | Sexit _ => invclear H | Sswitch _ _ _ => invclear H end | H : eval_condexpr _ _ _ _ _ ?c _ _ _ |- _ => match c with | CEtrue => invclear H | CEfalse => invclear H | CEcond _ _ => invclear H | CEcondition _ _ _ => invclear H end | H : eval_exprlist _ _ _ _ _ Enil _ _ _ |- _ => invclear H | H : eval_exprlist _ _ _ _ _ (Econs _ _) _ _ _ |- _ => invclear H end. Ltac run := repeat run0. Ltac injopt := match goal with | A : Some _ = Some _ |- _ => generalize (option_inj A) ; clear A ; intro A ; endsubst end. Ltac dereq0 := match goal with | A : ?a = ?a |- _ => clear A | A : Some _ = Some _ |- _ => injopt | A : ?a = Some _, B : ?a = Some _ |- _ => rewrite A in B ; injopt | A : ?a = Some _, B : Some _ = ?a |- _ => rewrite A in B ; injopt | _ => redenv_hyp end. Ltac dereq := repeat dereq0. Module Marksweep_cminor_equivalence (MP : Marksweep_parameters) (MH : Marksweep_hypotheses). Export MP. Export MH. Module algos := Marksweep_algorithms MP MH. Export algos. Module progs := Marksweep_programs MP CV MV. Export progs. Section mark_block_matches_cminor. Variable m : mem. Variable bi : option (block * int). Variable val_b : val. Hypothesis val_b_bi : val_is_pointer_or_dumb val_b bi. Theorem mark_block_matches_cminor : forall m', Some m' = mark_block m bi -> eval_funcall genv m mark_block_cminor_function (val_b :: nil) E0 m' Vundef. Proof. intros m'. unfold mark_block. unfold mark_block_body. unfold mark_block_cminor_function. (* stack pointer allocation *) case_eq (alloc m 0 0). intros m0 sp. intros Hsp. (* pointer argument *) destruct bi. (* case not null *) destruct p as [b i]. inversion val_b_bi. (* header *) case_eq (load Mint32 m0 b (signed (sub i four))); try discriminate 2. destruct v as [ | v | | ]; try discriminate 2. subst. intros Hv. (* color *) case_eq (negb (eq (Color_header v) COLOR_WHITE)). (* case not white *) intros H_not_white. injection 1; intros; subst. eapply eval_funcall_internal. simpl ; eassumption. simpl. reflexivity. simpl. unfold mark_block_cminor_prog. eapply exec_Sseq_continue. eapply exec_ifthenelse_false. eapply eval_cmp_null_r. eapply eval_Evar. redenv. redenv. redenv. reflexivity. eapply eval_Eop. eapply eval_Enil. simpl; trivial. left; split; reflexivity. simpl; trivial. eapply exec_Sskip. eapply exec_Sseq_continue. (* eapply exec_Sassign. # fails. Need assert (and explicit witnesses) here. *) assert ( let env := (PTree.set mb_header Vundef (PTree.set mb_cache Vundef (PTree.set mb_b (Vptr b i) (PTree.empty val)))) in exec_stmt genv (Vptr sp zero) env m0 (Sassign mb_header (Eload Mint32 (Aindexed (neg four)) (Econs (Evar mb_b) Enil))) (E0 ** E0) (PTree.set mb_header (Vint v) env) m0 Out_normal ). simpl. eapply exec_Sassign. eapply eval_Eload. eapply eval_Econs. eapply eval_Evar. repeat redenv. reflexivity. eapply eval_Enil. trivial. simpl. reflexivity. simpl. rewrite <- sub_add_opp. auto. eassumption. eapply exec_Sseq_stop. eapply exec_ifthenelse_true. eapply eval_cmp. eapply eval_and. eapply eval_Evar. eapply PTree.gss. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. unfold cmp. unfold Color_header in H_not_white. rewrite H_not_white. simpl. exact one_not_zero. eapply exec_Sreturn_none. intro; discriminate. reflexivity. repeat rewrite E0_left. trivial. simpl. trivial. (* case white *) intro Hwhite. (* kind *) case_eq (eq (Kind_header v) KIND_RAWDATA). (* case raw *) intro Hraw. case_eq (store Mint32 m0 b (signed (sub i four)) (Vint (or v COLOR_BLACK))); try (intros; discriminate). intros m1 Hm1. injection 1; intros; subst. unfold mark_block_cminor_prog. eapply eval_funcall_internal. simpl. eassumption. simpl. reflexivity. simpl. unfold mark_block_cminor_prog. eapply exec_Sseq_continue. eapply exec_ifthenelse_false. eapply eval_cmp_null_r. eapply eval_Evar. repeat redenv. reflexivity. eapply eval_Eop. eapply eval_Enil. simpl; trivial. left; split; reflexivity. simpl; trivial. eapply exec_Sskip. eapply exec_Sseq_continue. (* eapply exec_Sassign. # fails. Need assert (and explicit witnesses) here. *) assert ( let env := (PTree.set mb_header Vundef (PTree.set mb_cache Vundef (PTree.set mb_b (Vptr b i) (PTree.empty val)))) in exec_stmt genv (Vptr sp zero) env m0 (Sassign mb_header (Eload Mint32 (Aindexed (neg four)) (Econs (Evar mb_b) Enil))) (E0 ** E0) (PTree.set mb_header (Vint v) env) m0 Out_normal ). simpl. eapply exec_Sassign. eapply eval_Eload. eapply eval_Econs. eapply eval_Evar. repeat redenv. reflexivity. eapply eval_Enil. trivial. simpl. reflexivity. subst. simpl. rewrite <- sub_add_opp. auto. eassumption. eapply exec_Sseq_continue. eapply exec_ifthenelse_false. eapply eval_cmp. eapply eval_and. eapply eval_Evar. eapply PTree.gss. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. unfold cmp. unfold Color_header in Hwhite. rewrite Hwhite. simpl. trivial. eapply exec_Sskip. eapply exec_ifthenelse_true. eapply eval_cmp. eapply eval_and. eapply eval_Evar. eapply PTree.gss. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. unfold cmp. unfold Kind_header in Hraw. rewrite Hraw. simpl. exact one_not_zero. eapply exec_Sexpr. eapply eval_Estore. eapply eval_Econs. eapply eval_Evar. repeat redenv. reflexivity. eapply eval_Enil. reflexivity. eapply eval_or. eapply eval_Evar. eapply PTree.gss. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. simpl. reflexivity. simpl. subst. rewrite <- sub_add_opp. auto. reflexivity. reflexivity. reflexivity. repeat rewrite E0_left; trivial. simpl. trivial. (* case not raw *) intro H_not_raw. case_eq (store Mint32 m0 b (signed (sub i four)) (Vint (or v COLOR_GRAY))); try discriminate 2. intros m1 hM1. case_eq (load Mint32 m1 gray_cache_offset_block 0); try discriminate 2. destruct v0 as [ | cache | | ]; try discriminate 2. intro Hcache. (* cache full ? *) case_eq (eq cache GRAY_CACHE_SIZE); intro Hfull. (* case full *) case_eq (store Mint32 m1 gray_cache_overflow_block 0 (Vint one)) ; try (intros; discriminate). intros m2 Hm2. injection 1; intros; subst. eapply eval_funcall_internal. simpl. eassumption. simpl. reflexivity. simpl. unfold mark_block_cminor_prog. eapply exec_Sseq_continue. eapply exec_ifthenelse_false. eapply eval_cmp_null_r. eapply eval_Evar. repeat redenv; reflexivity. eapply eval_Eop. eapply eval_Enil. simpl. trivial. left. split ; reflexivity. simpl; trivial. eapply exec_Sskip; eauto. eapply exec_Sseq_continue. (* eapply exec_Sassign. # fails. Need assert (and explicit witnesses) here. *) assert ( let env := (PTree.set mb_header Vundef (PTree.set mb_cache Vundef (PTree.set mb_b (Vptr b i) (PTree.empty val)))) in exec_stmt genv (Vptr sp zero) env m0 (Sassign mb_header (Eload Mint32 (Aindexed (neg four)) (Econs (Evar mb_b) Enil))) (E0 ** E0) (PTree.set mb_header (Vint v) env) m0 Out_normal ). simpl. eapply exec_Sassign. eapply eval_Eload. eapply eval_Econs. eapply eval_Evar. repeat redenv; reflexivity. eapply eval_Enil. trivial. simpl. reflexivity. subst. simpl. rewrite <- sub_add_opp. auto. eassumption. eapply exec_Sseq_continue. eapply exec_ifthenelse_false. eapply eval_cmp. eapply eval_and. eapply eval_Evar. eapply PTree.gss. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. unfold cmp. unfold Color_header in Hwhite. rewrite Hwhite. simpl. trivial. eapply exec_Sskip. eapply exec_ifthenelse_false. eapply eval_cmp. eapply eval_and. eapply eval_Evar. eapply PTree.gss. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. unfold cmp. unfold Kind_header in H_not_raw. rewrite H_not_raw. simpl. trivial. eapply exec_Sseq_continue. eapply exec_Sexpr. eapply eval_Estore. eapply eval_Econs. eapply eval_Evar. repeat redenv; reflexivity. eapply eval_Enil. reflexivity. eapply eval_or. eapply eval_Evar. eapply PTree.gss. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. simpl. reflexivity. simpl. rewrite <- sub_add_opp. eauto. reflexivity. eapply exec_Sseq_continue. (* eapply exec_Sassign. # fails *) assert ( let env1 := (PTree.set mb_header (Vint v) (PTree.set mb_header Vundef (PTree.set mb_cache Vundef (PTree.set mb_b (Vptr b i) (PTree.empty val))))) in exec_stmt genv (Vptr sp zero) env1 m1 (Sassign mb_cache (Eload Mint32 (Aglobal gray_cache_offset zero) Enil)) E0 (PTree.set mb_cache (Vint cache) env1) m1 Out_normal ). simpl. apply exec_Sassign. eapply eval_Eload. eapply eval_Enil. simpl. rewrite genv_gray_cache_offset. reflexivity. simpl. change (signed zero) with 0. assumption. eassumption. eapply exec_ifthenelse_true. eapply eval_cmp. eapply eval_Evar. eapply PTree.gss. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. unfold cmp. rewrite Hfull. simpl. exact one_not_zero. eapply exec_Sexpr. eapply eval_Estore. eapply eval_Enil. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. simpl. rewrite genv_gray_cache_overflow. reflexivity. simpl. change (signed zero) with 0. auto. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. repeat rewrite E0_left; trivial. simpl. trivial. (* case not full *) case_eq (store Mint32 m1 gray_cache_block (signed cache) (Vptr b i)); try discriminate 2. intros m2 Hm2. case_eq (store Mint32 m2 gray_cache_offset_block 0 (Vint (add cache four))); try (intros ; discriminate). intros m3 Hm3. injection 1; intros; subst. eapply eval_funcall_internal. simpl. eassumption. simpl. reflexivity. simpl. unfold mark_block_cminor_prog. eapply exec_Sseq_continue. eapply exec_ifthenelse_false. eapply eval_cmp_null_r. eapply eval_Evar. repeat redenv; reflexivity. eapply eval_Eop. eapply eval_Enil. simpl. trivial. left. split ; reflexivity. simpl; trivial. eapply exec_Sskip; eauto. eapply exec_Sseq_continue. (* eapply exec_Sassign. # fails. Need assert (and explicit witnesses) here. *) assert ( let env := (PTree.set mb_header Vundef (PTree.set mb_cache Vundef (PTree.set mb_b (Vptr b i) (PTree.empty val)))) in exec_stmt genv (Vptr sp zero) env m0 (Sassign mb_header (Eload Mint32 (Aindexed (neg four)) (Econs (Evar mb_b) Enil))) (E0 ** E0) (PTree.set mb_header (Vint v) env) m0 Out_normal ). simpl. eapply exec_Sassign. eapply eval_Eload. eapply eval_Econs. eapply eval_Evar. repeat redenv; reflexivity. eapply eval_Enil. reflexivity. simpl. reflexivity. subst. simpl. rewrite <- sub_add_opp. auto. eassumption. eapply exec_Sseq_continue. eapply exec_ifthenelse_false. eapply eval_cmp. eapply eval_and. eapply eval_Evar. eapply PTree.gss. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. unfold cmp. unfold Color_header in Hwhite. rewrite Hwhite. simpl. trivial. eapply exec_Sskip. eapply exec_ifthenelse_false. eapply eval_cmp. eapply eval_and. eapply eval_Evar. eapply PTree.gss. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. unfold cmp. unfold Kind_header in H_not_raw. rewrite H_not_raw. simpl. trivial. eapply exec_Sseq_continue. eapply exec_Sexpr. eapply eval_Estore. eapply eval_Econs. eapply eval_Evar. repeat redenv; reflexivity. eapply eval_Enil. reflexivity. eapply eval_or. eapply eval_Evar. eapply PTree.gss. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. simpl. reflexivity. simpl. rewrite <- sub_add_opp. eauto. reflexivity. eapply exec_Sseq_continue. (* eapply exec_Sassign. # fails *) assert ( let env1 := (PTree.set mb_header (Vint v) (PTree.set mb_header Vundef (PTree.set mb_cache Vundef (PTree.set mb_b (Vptr b i) (PTree.empty val))))) in exec_stmt genv (Vptr sp zero) env1 m1 (Sassign mb_cache (Eload Mint32 (Aglobal gray_cache_offset zero) Enil)) E0 (PTree.set mb_cache (Vint cache) env1) m1 Out_normal ). simpl. apply exec_Sassign. eapply eval_Eload. eapply eval_Enil. simpl. rewrite genv_gray_cache_offset. reflexivity. simpl. change (signed zero) with 0. assumption. eassumption. eapply exec_ifthenelse_false. eapply eval_cmp. eapply eval_Evar. eapply PTree.gss. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. unfold cmp. rewrite Hfull. simpl. trivial. eapply exec_Sseq_continue. eapply exec_Sexpr. eapply eval_Estore. eapply eval_Econs. eapply eval_Evar. eapply PTree.gss. eapply eval_Enil. reflexivity. eapply eval_Evar. repeat redenv; reflexivity. simpl. rewrite genv_gray_cache. rewrite add_commut. rewrite add_zero. reflexivity. simpl. eassumption. reflexivity. eapply exec_Sexpr. eapply eval_Estore. eapply eval_Enil. eapply eval_addimm. eapply eval_Evar. eapply PTree.gss. simpl. rewrite genv_gray_cache_offset. reflexivity. simpl. change (signed zero) with 0. auto. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. repeat rewrite E0_left; trivial. simpl. trivial. (* case null pointer *) injection 1; intros; subst. inversion val_b_bi. subst. eapply eval_funcall_internal. simpl. eassumption. simpl. reflexivity. simpl. unfold mark_block_cminor_prog. eapply exec_Sseq_stop. rewrite <- (E0_left E0). eapply exec_ifthenelse_true. rewrite <- (E0_left E0). eapply eval_cmp. eapply eval_Evar. repeat redenv; reflexivity. eapply eval_Eop. eapply eval_Enil. simpl. reflexivity. simpl. exact one_not_zero. eapply exec_Sreturn_none. intro; discriminate. simpl. trivial. Qed. Theorem cminor_matches_mark_block : forall t m' vout, eval_funcall genv m (mark_block_cminor_function) (val_b :: nil) t m' vout -> Some m' = mark_block m bi. Proof. introvars. unfold mark_block_cminor_function. intro H. invclear H. simpl in *. unfold mark_block_cminor_prog in *. unfold mark_block. unfold mark_block_body. rewrite H1. run. (* case continue on first Sseq (b not null) *) simpl in *. unfold loadv in *. dereq. (* what is mb_b ? *) inversion val_b_bi ; subst. (* Vptr *) unfold eval_compare_null in *. match goal with H : context [eq zero zero] |- _ => compute in H end. dereq. run. dereq. rewrite <- sub_add_opp in *. match goal with H : load Mint32 m7 b (signed (sub i four)) = Some v7 |- _ => rewrite H ; destruct v7 ; try discriminate end. dereq. unfold Color_header. unfold rolm in *. rewrite rol_zero in *. destruct (negb (eq (and i0 color_mask) COLOR_WHITE)). (* case not white *) run. (* absurd case, return with Normal *) (* case white *) run. dereq. unfold rolm in *. rewrite rol_zero in *. unfold Kind_header. destruct (eq (and i0 kind_mask) KIND_RAWDATA). (* case raw *) run. dereq. simpl in *. dereq. unfold storev in *. rewrite sub_add_opp. match goal with H : store Mint32 _ b (signed (add i (neg four))) _ = _ |- _ => rewrite H end. trivial. (* case not raw *) run. dereq. simpl in *. dereq. unfold storev in *. rewrite sub_add_opp. match goal with H : store Mint32 _ b (signed (add i (neg four))) _ = _ |- _ => rewrite H end. rewrite genv_gray_cache_offset in *. dereq. unfold loadv in *. change 0 with (signed zero). match goal with H : load Mint32 _ gray_cache_offset_block (signed zero) = Some ?v2 |- _ => rewrite H ; destruct v2 ; try discriminate end. dereq. destruct (eq i1 GRAY_CACHE_SIZE). (* case full *) run. simpl in *. rewrite genv_gray_cache_overflow in *. dereq. unfold storev in *. match goal with H : store Mint32 _ gray_cache_overflow_block (signed zero) _ = _ |- _ => rewrite H end. trivial. (* case not full *) run. dereq. simpl in *. rewrite genv_gray_cache_offset in *. rewrite genv_gray_cache in *. dereq. unfold storev in *. rewrite (add_commut zero) in *. rewrite add_zero in *. match goal with H : store Mint32 _ gray_cache_block _ _ = _ |- _ => rewrite H end. unfold Cmconstr.addimm in *. match goal with H : context [eq four zero] |- _ => change (eq four zero) with false in H end. simpl in *. run. dereq. simpl in *. dereq. match goal with H : store Mint32 _ gray_cache_offset_block _ _ = _ |- _ => rewrite H end. trivial. (* absurd case, Out_normal <> Out_normal, on a Sseq *) congruence. (* absurd case (???) when gray_cache_offset stores a Vptr *) unfold eval_compare_null in *. case_eq (eq GRAY_CACHE_SIZE zero); intro Heq; rewrite Heq in *; simpl in *. (* case null cache *) dereq. run. dereq. simpl in *. rewrite genv_gray_cache_offset in *. dereq. discriminate. congruence. (* case cache not null *) discriminate. (* ok, that case was actually absurd. *) (* other absurd cases, due to assumed Sseq_stop whereas they were actually continuing *) congruence. congruence. (* mb_b is Vint zero *) dereq. match goal with H : context [eq zero zero] |- _ => change (eq zero zero) with true in H end. simpl in *. run. (* was absurd *) (* case stop at 3rd Sseq *) simpl in *. dereq. inversion val_b_bi; subst; dereq. (* case mb_b is a Vptr *) unfold eval_compare_null in *. match goal with H : context [eq zero zero] |- _ => change (eq zero zero) with true in H end. simpl in *. dereq. run. dereq. unfold loadv in *. rewrite sub_add_opp. match goal with H : load Mint32 _ b (signed (add i (neg four))) = Some ?v3 |- _ => rewrite H ; destruct v3 ; try discriminate end. dereq. (* it is actually the non-white case, a non absurd case *) unfold Color_header. unfold rolm in *. rewrite rol_zero in *. destruct (negb (eq (and i0 color_mask) COLOR_WHITE)). run. trivial. run. congruence. (* case stop at 3nd Sseq when mb_b is zero : absurd *) match goal with H : context [eq zero zero] |- _ => change (eq zero zero) with true in H end. simpl in *. dereq. run. (* case stop at 2nd Sseq : absurd *) congruence. (* case stop at 1st Sseq : b null *) simpl in *. dereq. inversion val_b_bi ; subst. (* case vptr *) unfold eval_compare_null in *. match goal with H : context [eq zero zero] |- _ => change (eq zero zero) with true in H end. simpl in *. dereq. run. congruence. match goal with H : context [eq zero zero] |- _ => change (eq zero zero) with true in H end. dereq. run. trivial. (* Qed. # works but takes a long time *) Admitted. End mark_block_matches_cminor. Parameter mark_block_funblock : block. Axiom genv_mark_block_funblock : Genv.find_symbol genv gm_mark_block = Some mark_block_funblock. Axiom genv_mark_block : Genv.find_funct genv (Vptr mark_block_funblock zero) = Some mark_block_cminor_function. Section mark_root_list_matches_cminor. Record env_mark_root_list (e : env) (p : mark_root_list_param) : Prop := env_mark_root_list_intro { env_mark_root_list_numroots : PTree.get gm_numroots e = Some (Vint (mark_root_list_numroots p)); env_mark_root_list_p : PTree.get gm_p e = Some (mark_root_list_p p) }. Section body. Variable p : mark_root_list_param. Variable sp : val. Variable env : env. Hypothesis Henv : env_mark_root_list env p. Theorem mark_root_list_body_matches_cminor : forall v p', (v, Some p') = mark_root_list_body (Some p) -> exists o, exists env', exists t, exec_stmt genv sp env (mark_root_list_mem p) mark_root_list_body_cminor t env' (mark_root_list_mem p') o /\ env_mark_root_list env' p' /\ (v = true -> o = Out_normal) /\ (v = false -> o = Out_exit O). Proof. intros v p'. unfold mark_root_list_body. unfold mark_root_list_body_cminor. inversion Henv. (* is numroots zero *) case_eq (eq (mark_root_list_numroots p) zero). intro Hnull_bool. generalize (eq_bool_eq_prop Hnull_bool). intro Hnull. injection 1. intros ; subst. repeat eapply ex_intro. split. eapply exec_Sseq_stop. eapply exec_ifthenelse_true. eapply eval_cmp. eapply eval_Evar. eassumption. eapply eval_Eop. eapply eval_Enil. unfold eval_operation. reflexivity. rewrite Hnull. compute. inversion 1. eapply exec_Sexit. intro ; discriminate. repeat split; congruence. (* case non zero... *) intro Hnonnull_bool. generalize (neq_bool_neq_prop Hnonnull_bool). intro Hnonnull. case_eq (mark_root_list_p p); try (intros; discriminate). intros b i Hbi. case_eq (load Mint32 (mark_root_list_mem p) b (signed i)); try (intros; discriminate). destruct v0 ; try (intros; discriminate). (* case integer *) intro Hi0. case_eq (eq i0 zero); try (intros; discriminate). intro Hi0_null. generalize (eq_bool_eq_prop Hi0_null). intro Hi0_null_2. subst. case_eq (mark_block (mark_root_list_mem p) None); try (intros; discriminate). intros m' Hm'. injection 1 ; intros; subst. symmetry in Hm'. repeat eapply ex_intro. split. eapply exec_Sseq_continue. eapply exec_ifthenelse_false. eapply eval_cmp. eapply eval_Evar. eassumption. eapply eval_Eop. eapply eval_Enil. unfold eval_operation. reflexivity. unfold cmp. rewrite Hnonnull_bool. compute. trivial. eapply exec_Sskip. eapply exec_Sseq_continue. eapply exec_Sexpr. eapply eval_Ecall. eapply eval_Eop. eapply eval_Enil. unfold eval_operation. rewrite genv_mark_block_funblock. reflexivity. eapply eval_Econs. eapply eval_Eload. eapply eval_Econs. eapply eval_Evar. eassumption. eapply eval_Enil. reflexivity. simpl. rewrite Hbi. reflexivity. unfold loadv. rewrite add_zero. eassumption. eapply eval_Enil. reflexivity. eexact genv_mark_block. reflexivity. eapply mark_block_matches_cminor. eauto. eassumption. reflexivity. eapply exec_Sseq_continue. (* eapply exec_Sassign. # fails, as usual *) assert ( exec_stmt genv sp env m' (Sassign gm_p (Cmconstr.addimm four (Evar gm_p))) E0 (PTree.set gm_p (Vptr b (add i four)) env) m' Out_normal ). eapply exec_Sassign. eapply eval_addimm_ptr. eapply eval_Evar. rewrite Hbi in env_mark_root_list_p0. eassumption. eassumption. (* eapply exec_Sassign. # fails, as usual *) assert ( let env' := (PTree.set gm_p (Vptr b (add i four)) env) in exec_stmt genv sp env' m' (Sassign gm_numroots (Cmconstr.addimm (neg one) (Evar gm_numroots))) E0 (PTree.set gm_numroots (Vint (sub (mark_root_list_numroots p) one)) env') m' Out_normal ). simpl. eapply exec_Sassign. rewrite sub_add_opp. eapply eval_addimm. eapply eval_Evar. rewrite PTree.gso; auto. intro ; congruence. eassumption. reflexivity. reflexivity. reflexivity. split. eapply env_mark_root_list_intro; simpl; auto. rewrite PTree.gss; auto. rewrite PTree.gso; try rewrite PTree.gss; congruence. split; congruence. intro Hb0i0. case_eq (mark_block (mark_root_list_mem p) (Some (b0, i0))); try (intros; discriminate). intros m' Hm'. injection 1; intros; subst. repeat eapply ex_intro. split. eapply exec_Sseq_continue. eapply exec_ifthenelse_false. eapply eval_cmp. eapply eval_Evar. eassumption. eapply eval_Eop. eapply eval_Enil. unfold eval_operation. reflexivity. unfold cmp. rewrite Hnonnull_bool. compute; reflexivity. eapply exec_Sskip. eapply exec_Sseq_continue. eapply exec_Sexpr. eapply eval_Ecall. eapply eval_Eop. eapply eval_Enil. simpl. rewrite genv_mark_block_funblock. reflexivity. eapply eval_Econs. eapply eval_Eload. eapply eval_Econs. eapply eval_Evar. eassumption. eapply eval_Enil. reflexivity. simpl. rewrite Hbi; reflexivity. unfold loadv. rewrite add_zero. eassumption. eapply eval_Enil. reflexivity. eexact genv_mark_block. reflexivity. eapply mark_block_matches_cminor. eauto. symmetry. eassumption. reflexivity. eapply exec_Sseq_continue. assert ( exec_stmt genv sp env m' (Sassign gm_p (Cmconstr.addimm four (Evar gm_p))) E0 (PTree.set gm_p (Vptr b (add i four)) env) m' Out_normal ). eapply exec_Sassign. eapply eval_addimm_ptr. eapply eval_Evar. rewrite <- Hbi. eassumption. eassumption. simpl. assert ( let env' :=(PTree.set gm_p (Vptr b (add i four)) env) in exec_stmt genv sp env' m' (Sassign gm_numroots (Cmconstr.addimm (neg one) (Evar gm_numroots))) E0 (PTree.set gm_numroots (Vint (add (mark_root_list_numroots p) (neg one))) env') m' Out_normal ). eapply exec_Sassign. eapply eval_addimm. eapply eval_Evar. rewrite PTree.gso. assumption. congruence. eassumption. reflexivity. reflexivity. reflexivity. split. eapply env_mark_root_list_intro; auto. simpl. rewrite sub_add_opp. apply PTree.gss. rewrite PTree.gso. apply PTree.gss. congruence. split; congruence. Qed. Theorem cminor_matches_mark_root_list_body : forall o m' t env', exec_stmt genv sp env (mark_root_list_mem p) mark_root_list_body_cminor t env' m' o -> exists v, exists p', (v, Some p') = mark_root_list_body (Some p) /\ m' = mark_root_list_mem p' /\ env_mark_root_list env' p' /\ (v = true -> o = Out_normal) /\ (v = false -> o = Out_exit O). Proof. introvars. inversion Henv. unfold mark_root_list_body_cminor. unfold mark_root_list_body. intro H. run. (* case continue on first Sseq *) dereq. simpl in *. rewrite genv_mark_block_funblock in *. dereq. rewrite genv_mark_block in *. dereq. (* HERE *) case_eq (eq (mark_root_list_numroots p) zero). intros Hzero ; rewrite Hzero in *. run. (* absurd, is Sexit 0, should be Sskip *) intros Hnonzero; rewrite Hnonzero in *. run. dereq. case_eq (mark_root_list_p p). intro Habs; rewrite Habs in *; discriminate. intros ? Habs; rewrite Habs in *; discriminate. intros ? Habs; rewrite Habs in *; discriminate. intros b i Hbi. rewrite Hbi in *. dereq. unfold loadv in *. rewrite add_zero in *. run. unfold Cmconstr.addimm in *. change (eq four zero) with false in H10. change (eq (neg one) zero) with false in H12. simpl in *. run. rewrite PTree.gso in H6. 2 : congruence. dereq. simpl in *. dereq. (* HERE ; remember to change hypotheses about argument of Mark_block *) dereq0. dereq0. simpl in H22. unfold loadv in *. dereq. (* what is mb_b ? *) inversion val_b_bi ; subst. (* Vptr *) End body. End mark_root_list_matches_cminor. Section body. End Marksweep_cminor_equivalence.