From 21f6353cfbed8192c63bc44551ab3c1b5bf7d85a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 14 Dec 2020 08:59:48 +0100 Subject: Generals lemmas for asmblockgenproof --- aarch64/Asmblock.v | 2 + aarch64/Asmblockgen.v | 40 ++- aarch64/Asmblockgenproof.v | 750 ++++++++++++++++++++++++++++++++++++++++++++ aarch64/Asmblockgenproof0.v | 117 ++++++- 4 files changed, 896 insertions(+), 13 deletions(-) diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 5e41d96a..c163ea10 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -41,6 +41,8 @@ Require Export Asm. Local Open Scope option_monad_scope. +Notation regset := Asm.regset. + (** * Abstract syntax *) (* First task: splitting the big [instruction] type below into CFI and basic instructions. diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index d68cd7ac..96e7db4b 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -1159,11 +1159,11 @@ Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool := | _ => false end. -Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) (k: bcode):= +Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_inst) (it1p: bool) := match il with - | nil => OK (k) + | nil => OK (nil) | i1 :: il' => - do k1 <- transl_basic_code f il' (it1_is_parent it1p i1) k; + do k1 <- transl_basic_code f il' (it1_is_parent it1p i1); transl_instr_basic f i1 it1p k1 end. @@ -1196,12 +1196,29 @@ Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instructio (* XXX: the simulation proof may be complex with this pattern. We may fix this later *) Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control): bblocks := - match non_empty_bblockb bdy ex with - | true => {| header := ll; body:= bdy; exit := ex |} :: nil - | false => {| header := ll; body:= Pnop::nil; exit := None |} :: nil + match ex with + | None => + match bdy with + | nil => {| header := ll; body:= Pnop::nil; exit := None |} :: nil + | _ => {| header := ll; body:= bdy; exit := None |} :: nil + end + | _ => + match bdy with + | nil => {| header := ll; body:= nil; exit := ex |} :: nil + | _ => {| header := ll; body:= bdy; exit := ex |} :: nil + end end. -Obligation 1. - rewrite <- Heq_anonymous. constructor. +Next Obligation. + induction bdy. congruence. + simpl. auto. +Qed. +Next Obligation. + destruct ex. simpl. auto. + congruence. +Qed. +Next Obligation. + induction bdy. congruence. + simpl. auto. Qed. Definition transl_control (f: Machblock.function) (ctl: control_flow_inst) : res (bcode*control) := @@ -1227,10 +1244,9 @@ Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) : end. Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) := - let stub := false in - do (bdy, ex) <- transl_exit f fb.(Machblock.exit); - do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy; - OK (cons_bblocks fb.(Machblock.header) bdy' ex) + do (bdy2, ex) <- transl_exit f fb.(Machblock.exit); + do bdy1 <- transl_basic_code f fb.(Machblock.body) ep; + OK (cons_bblocks fb.(Machblock.header) (bdy1 @@ bdy2) ex) . Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) := diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v index bd96ff3b..33acc110 100644 --- a/aarch64/Asmblockgenproof.v +++ b/aarch64/Asmblockgenproof.v @@ -29,6 +29,20 @@ Hypothesis TRANSF: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. +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). + +Lemma functions_translated: + forall b f, + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. +Proof (Genv.find_funct_ptr_transf_partial TRANSF). Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs), Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs. @@ -46,6 +60,64 @@ Proof. omega. Qed. +(** * Proof of semantic preservation *) + +(** Semantic preservation is proved using a complex simulation diagram + of the following form. +<< + MB.step + ----------------------------------------> + header body exit + st1 -----> st2 -----> st3 ------------------> st4 + | | | | + | (A) | (B) | (C) | + match_codestate | | | | + | header | body1 | body2 | match_states + cs1 -----> cs2 -----> cs3 ------> cs4 | + | / \ exit | + match_asmstate | --------------- --->--- | + | / match_asmstate \ | + st'1 ---------------------------------------> st'2 + AB.step * +>> + The invariant between each MB.step/AB.step is the [match_states] predicate below. + However, we also need to introduce an intermediary state [Codestate] which allows + us to reason on a finer grain, executing header, body and exit separately. + + This [Codestate] consists in a state like [Asmblock.State], except that the + code is directly stored in the state, much like [Machblock.State]. It also features + additional useful elements to keep track of while executing a bblock. +*) + +Inductive match_states: Machblock.state -> Asm.state -> Prop := + | match_states_intro: + forall s fb sp c ep ms m m' rs f tf tc + (STACKS: match_stack ge s) + (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) + (MEXT: Mem.extends m m') + (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc) + (AG: agree ms sp rs) + (DXP: ep = true -> rs#X29 = parent_sp s), + match_states (Machblock.State s fb sp c ms m) + (Asm.State rs m') + | match_states_call: + forall s fb ms m m' rs + (STACKS: match_stack ge s) + (MEXT: Mem.extends m m') + (AG: agree ms (parent_sp s) rs) + (ATPC: rs PC = Vptr fb Ptrofs.zero) + (ATLR: rs RA = parent_ra s), + match_states (Machblock.Callstate s fb ms m) + (Asm.State rs m') + | match_states_return: + forall s ms m m' rs + (STACKS: match_stack ge s) + (MEXT: Mem.extends m m') + (AG: agree ms (parent_sp s) rs) + (ATPC: rs PC = parent_ra s), + match_states (Machblock.Returnstate s ms m) + (Asm.State rs m'). + (** Existence of return addresses *) Lemma return_address_exists: @@ -61,11 +133,689 @@ Proof. - exact transf_function_no_overflow. Qed. +(* Useful for dealing with the many cases in some proofs *) +Ltac exploreInst := + repeat match goal with + | [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var + | [ H : OK _ = OK _ |- _ ] => monadInv H + | [ |- context[if ?b then _ else _] ] => destruct b + | [ |- context[match ?m with | _ => _ end] ] => destruct m + | [ |- context[match ?m as _ return _ with | _ => _ end]] => destruct m + | [ H : bind _ _ = OK _ |- _ ] => monadInv H + | [ H : Error _ = OK _ |- _ ] => inversion H + end. + +Ltac desif := + repeat match goal with + | [ |- context[if ?f then _ else _ ] ] => destruct f + end. + +(** Some translation properties *) + +Lemma no_builtin_preserved: + forall f ex x1 x2, + (forall ef args res, ex <> Some (MBbuiltin ef args res)) -> + transl_exit f ex = OK(x1, x2) -> + (exists i, x2 = Some (PCtlFlow i)) + \/ x2 = None. +Proof. + intros until x2. intros Hbuiltin TIC. + destruct ex. + - destruct c. + (* MBcall *) + + simpl in TIC. monadInv TIC. exploreInst; simpl; eauto. + (* MBtailcall *) + + simpl in TIC. monadInv TIC. exploreInst; simpl; eauto. + (* MBbuiltin *) + + assert (H: Some (MBbuiltin e l b) <> Some (MBbuiltin e l b)). + apply Hbuiltin. contradict H; auto. + (* MBgoto *) + + simpl in TIC. exploreInst; simpl; eauto. + (* MBcond *) + + simpl in TIC. unfold transl_cond_branch, transl_cond_branch_default in TIC. + monadInv TIC; exploreInst; simpl; eauto. + (* MBjumptable *) + + simpl in TIC. monadInv TIC. exploreInst; simpl; eauto. + (* MBreturn *) + + simpl in TIC. monadInv TIC. simpl. eauto. + - monadInv TIC. simpl; auto. +Qed. + +Lemma transl_blocks_distrib: + forall c f bb tbb tc ep, + transl_blocks f (bb::c) ep = OK (tbb::tc) + -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) + -> transl_block f bb (if MB.header bb then ep else false) = OK (tbb :: nil) + /\ transl_blocks f c false = OK tc. +Proof. + intros until ep. intros TLBS Hbuiltin. + destruct bb as [hd bdy ex]. + monadInv TLBS. monadInv EQ. + exploit no_builtin_preserved; eauto. intros Hectl. destruct Hectl. + - destruct H as [i Hectl]. + unfold cons_bblocks in H0. rewrite Hectl in H0. + destruct (x3 @@ x1) eqn: CBDY; inv H0; inv EQ0; + simpl in *; unfold transl_block; simpl; rewrite H0; simpl; + rewrite EQ; simpl; rewrite CBDY; auto. + - unfold cons_bblocks in H0. rewrite H in H0. + destruct (x3 @@ x1) eqn: CBDY; inv H0; inv EQ0; + simpl in *; unfold transl_block; simpl; rewrite H0; simpl; + rewrite EQ; simpl; rewrite CBDY; auto. +Qed. + +Lemma cons_bblocks_nobuiltin: + forall thd tbdy tex tbb, + (tbdy <> nil \/ tex <> None) -> + (forall ef args res, tex <> Some (Pbuiltin ef args res)) -> + cons_bblocks thd tbdy tex = tbb :: nil -> + header tbb = thd + /\ body tbb = tbdy + /\ exit tbb = tex. +Proof. + intros until tbb. intros Hnonil Hnobuiltin CONSB. unfold cons_bblocks in CONSB. + destruct (tex) eqn:ECTL. + - destruct tbdy; inv CONSB; simpl; auto. + - inversion Hnonil. + + destruct tbdy as [|bi tbdy]; [ contradiction H; auto | inv CONSB; auto]. + + contradict H; simpl; auto. +Qed. + +Lemma transl_blocks_nonil: + forall f bb c tc ep, + transl_blocks f (bb::c) ep = OK tc -> + exists tbb tc', tc = tbb :: tc'. +Proof. + intros until ep. intros TLBS. monadInv TLBS. monadInv EQ. unfold cons_bblocks. + destruct (x2); + destruct (x3 @@ x1); simpl; eauto. +Qed. + +Definition mb_remove_header bb := {| MB.header := nil; MB.body := MB.body bb; MB.exit := MB.exit bb |}. + +Definition mb_remove_body (bb: MB.bblock) := + {| MB.header := MB.header bb; MB.body := nil; MB.exit := MB.exit bb |}. + +Definition mbsize (bb: MB.bblock) := (length (MB.body bb) + length_opt (MB.exit bb))%nat. + +Lemma mbsize_eqz: + forall bb, mbsize bb = 0%nat -> MB.body bb = nil /\ MB.exit bb = None. +Proof. + intros. destruct bb as [hd bdy ex]; simpl in *. unfold mbsize in H. + remember (length _) as a. remember (length_opt _) as b. + assert (a = 0%nat) by omega. assert (b = 0%nat) by omega. subst. clear H. + inv H0. inv H1. destruct bdy; destruct ex; auto. + all: try discriminate. +Qed. + +Lemma mbsize_neqz: + forall bb, mbsize bb <> 0%nat -> (MB.body bb <> nil \/ MB.exit bb <> None). +Proof. + intros. destruct bb as [hd bdy ex]; simpl in *. + destruct bdy; destruct ex; try (right; discriminate); try (left; discriminate). + contradict H. unfold mbsize. simpl. auto. +Qed. + +Record codestate := + Codestate { pstate: state; (**r projection to Asmblock.state *) + pheader: list label; + pbody1: list basic; (**r list of basic instructions coming from the translation of the Machblock body *) + pbody2: list basic; (**r list of basic instructions coming from the translation of the Machblock exit *) + pctl: option control; (**r exit instruction, coming from the translation of the Machblock exit *) + ep: bool; (**r reflects the [ep] variable used in the translation *) + rem: list AB.bblock; (**r remaining bblocks to execute *) + cur: bblock (**r current bblock to execute - to keep track of its size when incrementing PC *) + }. + +(* The part that deals with Machblock <-> Codestate agreement + * Note about DXP: the property of [ep] only matters if the current block doesn't have a header, hence the condition *) +Inductive match_codestate fb: Machblock.state -> codestate -> Prop := + | match_codestate_intro: + forall s sp ms m rs0 m0 f tc ep c bb tbb tbc1 tbc2 ex + (STACKS: match_stack ge s) + (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) + (MEXT: Mem.extends m m0) + (TBC: transl_basic_code f (MB.body bb) (if MB.header bb then ep else false) = OK tbc1) + (TIC: transl_exit f (MB.exit bb) = OK (tbc2, ex)) + (TBLS: transl_blocks f c false = OK tc) + (AG: agree ms sp rs0) + (DXP: (if MB.header bb then ep else false) = true -> rs0#X29 = parent_sp s) + , + match_codestate fb (Machblock.State s fb sp (bb::c) ms m) + {| pstate := (Asm.State rs0 m0); + pheader := (MB.header bb); + pbody1 := tbc1; + pbody2 := tbc2; + pctl := ex; + ep := ep; + rem := tc; + cur := tbb + |} +. + +(* The part ensuring that the code in Codestate actually resides at [rs PC] *) +Inductive match_asmstate fb: codestate -> Asm.state -> Prop := + | match_asmstate_some: + forall rs f tf tc m tbb ofs ep tbdy1 tbdy2 tex lhd + (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) + (TRANSF: transf_function f = OK tf) + (PCeq: rs PC = Vptr fb ofs) + (TAIL: code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (tbb::tc)) + , + match_asmstate fb + {| pstate := (Asm.State rs m); + pheader := lhd; + pbody1 := tbdy1; + pbody2 := tbdy2; + pctl := tex; + ep := ep; + rem := tc; + cur := tbb |} + (Asm.State rs m) +. + +Lemma indexed_memory_access_nonil: forall f ofs r i k, + indexed_memory_access_bc f ofs r i k <> nil. +Proof. + intros. + unfold indexed_memory_access_bc, loadimm64, loadimm, loadimm_z, loadimm_n; + desif; try congruence. + all: destruct decompose_int; try destruct p; try congruence. +Qed. + +Lemma loadimm_nonil: forall sz x n k, + loadimm sz x n k <> nil. +Proof. + intros. + unfold loadimm. desif; + unfold loadimm_n, loadimm_z. + all: destruct decompose_int; try destruct p; try congruence. +Qed. + +Lemma loadimm32_nonil: forall sz x n, + loadimm32 sz x n <> nil. +Proof. + intros. + unfold loadimm32. desif; try congruence. + apply loadimm_nonil. +Qed. + +Lemma loadimm64_nonil: forall sz x n, + loadimm64 sz x n <> nil. +Proof. + intros. + unfold loadimm64. desif; try congruence. + apply loadimm_nonil. +Qed. + +Lemma loadsymbol_nonil: forall sz x n k, + loadsymbol sz x n k <> nil. +Proof. + intros. + unfold loadsymbol. desif; try congruence. +Qed. + +Lemma move_extended_nonil: forall x0 x1 x2 a k, + move_extended x1 x2 x0 a k <> nil. +Proof. + intros. unfold move_extended, move_extended_base. + desif; try congruence. +Qed. + +Lemma arith_extended_nonil: forall insnX insnS x0 x1 x2 x3 a k, + arith_extended insnX insnS x1 x2 x3 x0 a k <> nil. +Proof. + intros. unfold arith_extended, move_extended_base. + desif; try congruence. +Qed. + +Lemma transl_instr_basic_nonil: + forall k f bi ep x, + transl_instr_basic f bi ep k = OK x -> + x <> nil. +Proof. + intros until x. intros TIB. + destruct bi. + - simpl in TIB. unfold loadind in TIB; + exploreInst; try discriminate; apply indexed_memory_access_nonil. + - simpl in TIB. unfold storeind in TIB; + exploreInst; try discriminate; apply indexed_memory_access_nonil. + - simpl in TIB. monadInv TIB. unfold loadind in EQ. exploreInst; try discriminate; + unfold loadptr_bc; apply indexed_memory_access_nonil. + - simpl in TIB. unfold transl_op in TIB. exploreInst; try discriminate; + unfold addimm32, addimm64, shrx32, shrx64, + logicalimm32, logicalimm64, addimm_aux. + all: desif; try congruence; + try apply loadimm32_nonil; try apply loadimm64_nonil; try apply loadsymbol_nonil; + try apply move_extended_nonil; try apply arith_extended_nonil. + all: unfold transl_cond in *; exploreInst; try discriminate; + try apply loadimm32_nonil; try apply loadimm64_nonil. + - simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate; + unfold transl_addressing in *; exploreInst; try discriminate. + all: try apply loadimm64_nonil; try apply arith_extended_nonil; try apply loadsymbol_nonil. + - simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate; + unfold transl_addressing in *; exploreInst; try discriminate. + all: try apply loadimm64_nonil; try apply arith_extended_nonil; try apply loadsymbol_nonil. +Qed. + +Lemma transl_basic_code_nonil: + forall bdy f x ep, + bdy <> nil -> + transl_basic_code f bdy ep = OK x -> + x <> nil. +Proof. + induction bdy as [|bi bdy]. + intros. contradict H0; auto. + destruct bdy as [|bi2 bdy]. + - clear IHbdy. intros f x b _ TBC. simpl in TBC. eapply transl_instr_basic_nonil; eauto. + - intros f x b Hnonil TBC. remember (bi2 :: bdy) as bdy'. + monadInv TBC. + assert (x0 <> nil). + eapply IHbdy; eauto. subst bdy'. discriminate. + eapply transl_instr_basic_nonil; eauto. +Qed. + +Lemma transl_exit_nonil: + forall ex f bdy x, + ex <> None -> + transl_exit f ex = OK(bdy, x) -> + x <> None. +Proof. + intros ex f bdy x Hnonil TIC. + destruct ex as [ex|]. + - clear Hnonil. destruct ex. + all: try (simpl in TIC; try monadInv TIC; exploreInst; discriminate). + - contradict Hnonil; auto. +Qed. + +Lemma transl_exit_nobuiltin: + forall f ex bdy x, + (forall ef args res, ex <> Some (MBbuiltin ef args res)) -> + transl_exit f ex = OK (bdy, x) -> + (forall ef args res, x <> Some (Pbuiltin ef args res)). +Proof. + intros until x. intros Hnobuiltin TIC. intros until res. + unfold transl_exit, transl_control in TIC. exploreInst. monadInv TIC. + exploreInst. + all: try discriminate. + - assert False. eapply Hnobuiltin; eauto. destruct H. + - unfold transl_cond_branch, transl_cond_branch_default in EQ. exploreInst. + all: try discriminate. +Qed. + +Theorem app_nonil: forall A (l1 l2: list A), + l1 <> nil -> + l1 @@ l2 <> nil. +Proof. + induction l2. + - intros; rewrite app_nil_r; auto. + - intros. unfold not. intros. symmetry in H0. + generalize (app_cons_not_nil); intros. unfold not in H1. + generalize (H0). apply H1. +Qed. + +Theorem match_state_codestate: + forall mbs abs s fb sp bb c ms m, + (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> + (MB.body bb <> nil \/ MB.exit bb <> None) -> + mbs = (Machblock.State s fb sp (bb::c) ms m) -> + match_states mbs abs -> + exists cs fb f tbb tc ep, + match_codestate fb mbs cs /\ match_asmstate fb cs abs + /\ Genv.find_funct_ptr ge fb = Some (Internal f) + /\ transl_blocks f (bb::c) ep = OK (tbb::tc) + /\ body tbb = pbody1 cs ++ pbody2 cs + /\ exit tbb = pctl cs + /\ cur cs = tbb /\ rem cs = tc + /\ pstate cs = abs. +Proof. + intros until m. intros Hnobuiltin Hnotempty Hmbs MS. subst. inv MS. + inv AT. clear H0. exploit transl_blocks_nonil; eauto. intros (tbb & tc' & Htc). subst. + exploit transl_blocks_distrib; eauto. intros (TLB & TLBS). clear H2. + monadInv TLB. exploit cons_bblocks_nobuiltin; eauto. + { inversion Hnotempty. + - destruct (MB.body bb) as [|bi bdy]; try (contradict H0; simpl; auto; fail). + left. apply app_nonil. eapply transl_basic_code_nonil; eauto. + - destruct (MB.exit bb) as [ei|]; try (contradict H0; simpl; auto; fail). + right. eapply transl_exit_nonil; eauto. } + eapply transl_exit_nobuiltin; eauto. + intros (Hth & Htbdy & Htexit). + exists {| pstate := (State rs m'); pheader := (Machblock.header bb); pbody1 := x1; pbody2 := x; + pctl := x0; ep := ep0; rem := tc'; cur := tbb |}, fb, f, tbb, tc', ep0. + repeat split. 1-2: econstructor; eauto. + { destruct (MB.header bb). eauto. discriminate. } eauto. + unfold transl_blocks. fold transl_blocks. unfold transl_block. rewrite EQ. simpl. rewrite EQ1; simpl. + rewrite TLBS. simpl. rewrite H2. + all: simpl; auto. +Qed. + +(* Bringing theorems (A), (B) and (C) together, for the case of the absence of builtin instruction *) +(* This more general form is easier to prove, but the actual theorem is step_simulation_bblock further below *) +Lemma step_simulation_bblock': + forall sf f sp bb bb' bb'' rs m rs' m' s'' c S1, + bb' = mb_remove_header bb -> + body_step ge sf f sp (Machblock.body bb') rs m rs' m' -> + bb'' = mb_remove_body bb' -> + (forall ef args res, MB.exit bb'' <> Some (MBbuiltin ef args res)) -> + exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') E0 s'' -> + match_states (Machblock.State sf f sp (bb :: c) rs m) S1 -> + exists S2 : state, plus (step lk) tge S1 E0 S2 /\ match_states s'' S2. +Proof. + intros until S1. intros Hbb' BSTEP Hbb'' Hbuiltin ESTEP MS. + destruct (mbsize bb) eqn:SIZE. + - apply mbsize_eqz in SIZE. destruct SIZE as (Hbody & Hexit). + destruct bb as [hd bdy ex]; simpl in *; subst. + inv MS. inv AT. exploit transl_blocks_nonil; eauto. intros (tbb & tc' & Htc). subst. rename tc' into tc. + monadInv H2. simpl in *. inv ESTEP. inv BSTEP. + eexists. split. + + eapply plus_one. + exploit functions_translated; eauto. intros (tf0 & FIND' & TRANSF'). monadInv TRANSF'. + assert (x = tf). { unfold transf_function in H1. monadInv H1. + destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x0))); try congruence. } + subst x. + eapply exec_step_internal; eauto. eapply find_bblock_tail; eauto. + unfold exec_bblock. simpl. + eexists; eexists; split; eauto. + econstructor. + + econstructor. + 1,2,3: eauto. + * + unfold incrPC. rewrite Pregmap.gss. + unfold Val.offset_ptr. rewrite <- H. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + { eapply transf_function_no_overflow; eauto. } + econstructor; eauto. + generalize (code_tail_next_int _ _ _ _ NOOV H3). intro CT1. eauto. + * + eapply agree_exten; eauto. intros. unfold incrPC. rewrite Pregmap.gso; auto. + unfold data_preg in H2. destruct r; try congruence. + * + intros. discriminate. + - subst. exploit mbsize_neqz. { instantiate (1 := bb). rewrite SIZE. discriminate. } + intros Hnotempty. + + (* initial setting *) + exploit match_state_codestate. + 2: eapply Hnotempty. + all: eauto. + intros (cs1 & fb & f0 & tbb & tc & ep & MCS & MAS & FIND & TLBS & Hbody & Hexit & Hcur & Hrem & Hpstate). + + (* step_simu_header part *) + assert (exists rs1 m1, pstate cs1 = State rs1 m1). { inv MAS. simpl. eauto. } + destruct H as (rs1 & m1 & Hpstate2). subst. + assert (f = fb). { inv MCS. auto. } subst fb. + all: admit. + (*exploit step_simu_header. + 2: eapply MCS. + all: eauto. + intros (cs1' & EXEH & MCS2). + + (* step_simu_body part *) + assert (Hpstate': pstate cs1' = pstate cs1). { inv EXEH; auto. } + exploit step_simu_body. + 3: eapply BSTEP. + 4: eapply MCS2. + all: eauto. rewrite Hpstate'. eauto. + intros (rs2 & m2 & cs2 & ep' & Hcs2 & EXEB & MCS'). + + (* step_simu_control part *) + assert (exists tf, Genv.find_funct_ptr tge f = Some (Internal tf)). + { exploit functions_translated; eauto. intros (tf & FIND' & TRANSF'). monadInv TRANSF'. eauto. } + destruct H as (tf & FIND'). + assert (exists tex, pbody2 cs1 = extract_basic tex /\ pctl cs1 = extract_ctl tex). + { inv MAS. simpl in *. eauto. } + destruct H as (tex & Hpbody2 & Hpctl). + inv EXEH. simpl in *. + subst. exploit step_simu_control. + 9: eapply MCS'. all: simpl. + 10: eapply ESTEP. + all: simpl; eauto. + rewrite Hpbody2. rewrite Hpctl. + { inv MAS; simpl in *. inv Hpstate2. eapply match_asmstate_some; eauto. + erewrite exec_body_pc; eauto. } + intros (rs3 & m3 & rs4 & m4 & EXEB' & EXECTL' & MS'). + + (* bringing the pieces together *) + exploit exec_body_trans. + eapply EXEB. + eauto. + intros EXEB2. + exploit exec_body_control; eauto. + rewrite <- Hpbody2 in EXEB2. rewrite <- Hbody in EXEB2. eauto. + rewrite Hexit. rewrite Hpctl. eauto. + intros EXECB. inv EXECB. + exists (State rs4 m4). + split; auto. eapply plus_one. rewrite Hpstate2. + assert (exists ofs, rs1 PC = Vptr f ofs). + { rewrite Hpstate2 in MAS. inv MAS. simpl in *. eauto. } + destruct H0 as (ofs & Hrs1pc). + eapply exec_step_internal; eauto. + + (* proving the initial find_bblock *) + rewrite Hpstate2 in MAS. inv MAS. simpl in *. + assert (f1 = f0) by congruence. subst f0. + rewrite PCeq in Hrs1pc. inv Hrs1pc. + exploit functions_translated; eauto. intros (tf1 & FIND'' & TRANS''). rewrite FIND' in FIND''. + inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ. + eapply find_bblock_tail; eauto. +Qed.*) +Admitted. + +Theorem step_simulation_bblock: + forall sf f sp bb ms m ms' m' S2 c, + body_step ge sf f sp (Machblock.body bb) ms m ms' m' -> + (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> + exit_step return_address_offset ge (Machblock.exit bb) (Machblock.State sf f sp (bb :: c) ms' m') E0 S2 -> + forall S1', match_states (Machblock.State sf f sp (bb :: c) ms m) S1' -> + exists S2' : state, plus (step lk) tge S1' E0 S2' /\ match_states S2 S2'. +Proof. + intros until c. intros BSTEP Hbuiltin ESTEP S1' MS. + eapply step_simulation_bblock'; eauto. + all: destruct bb as [hd bdy ex]; simpl in *; eauto. + inv ESTEP. + - econstructor. inv H; try (econstructor; eauto; fail). + - econstructor. +Qed. + +(* Measure to prove finite stuttering, see the other backends *) +Definition measure (s: MB.state) : nat := + match s with + | MB.State _ _ _ _ _ _ => 0%nat + | MB.Callstate _ _ _ _ => 0%nat + | MB.Returnstate _ _ _ => 1%nat + end. + +(* The actual MB.step/AB.step simulation, using the above theorems, plus extra proofs + for the internal and external function cases *) +Theorem step_simulation: + forall S1 t S2, MB.step return_address_offset ge S1 t S2 -> + forall S1' (MS: match_states S1 S1'), + (exists S2', plus (step lk) tge S1' t S2' /\ match_states S2 S2') + \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. +Proof. + induction 1; intros. + +- (* bblock *) + left. destruct (Machblock.exit bb) eqn:MBE; try destruct c0. + all: admit. +all: admit. +Admitted. + (*all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; + try (rewrite MBE; try discriminate); eauto). + + (* MBbuiltin *) + destruct (MB.body bb) eqn:MBB. + * inv H. eapply step_simulation_builtin; eauto. rewrite MBE. eauto. + * eapply match_states_split_builtin in MS; eauto. + 2: rewrite MBB; discriminate. + simpl split in MS. + rewrite <- MBB in H. + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb1. + assert (MB.body bb = MB.body bb1). { subst. simpl. auto. } + rewrite H1 in H. subst. + exploit step_simulation_bblock. eapply H. + discriminate. + simpl. constructor. + eauto. + intros (S2' & PLUS1 & MS'). + rewrite MBE in MS'. + assert (exit_step return_address_offset ge (Some (MBbuiltin e l b)) + (MB.State sf f sp ({| MB.header := nil; MB.body := nil; MB.exit := Some (MBbuiltin e l b) |}::c) + rs' m') t s'). + { inv H0. inv H3. econstructor. econstructor; eauto. } + exploit step_simulation_builtin. + 4: eapply MS'. + all: simpl; eauto. + intros (S3' & PLUS'' & MS''). + exists S3'. split; eauto. + eapply plus_trans. eapply PLUS1. eapply PLUS''. eauto. + + inversion H0. subst. eapply step_simulation_bblock; try (rewrite MBE; try discriminate); eauto. + +- (* internal function *) + inv MS. + exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. + generalize EQ; intros EQ'. monadInv EQ'. + destruct (zlt Ptrofs.max_unsigned (size_blocks x0.(fn_blocks))); inversion EQ1. clear EQ1. subst x0. + unfold Mach.store_stack in *. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. + intros [m1' [C D]]. + exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. + intros [m2' [F G]]. + simpl chunk_of_type in F. + exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. + intros [m3' [P Q]]. + (* Execution of function prologue *) + monadInv EQ0. + set (tfbody := make_prologue f x0) in *. + set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *. + set (rs2 := rs0#FP <- (parent_sp s) #SP <- sp #RTMP <- Vundef). + exploit (Pget_correct tge GPRA RA nil rs2 m2'); auto. + intros (rs' & U' & V'). + exploit (storeind_ptr_correct tge SP (fn_retaddr_ofs f) GPRA nil rs' m2'). + { rewrite chunk_of_Tptr in P. + assert (rs' GPRA = rs0 RA). { apply V'. } + assert (rs' SP = rs2 SP). { apply V'; discriminate. } + rewrite H4. rewrite H3. + rewrite ATLR. + change (rs2 SP) with sp. eexact P. } + intros (rs3 & U & V). + assert (EXEC_PROLOGUE: exists rs3', + exec_straight_blocks tge tf + tf.(fn_blocks) rs0 m' + x0 rs3' m3' + /\ forall r, r <> PC -> rs3' r = rs3 r). + { eexists. split. + - change (fn_blocks tf) with tfbody; unfold tfbody. + econstructor; eauto. unfold exec_bblock. simpl exec_body. + rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. simpl in F. rewrite F. + Simpl. unfold parexec_store_offset. rewrite Ptrofs.of_int64_to_int64. unfold eval_offset. + rewrite chunk_of_Tptr in P. Simpl. rewrite ATLR. unfold Mptr in P. assert (Archi.ptr64 = true) by auto. 2: auto. rewrite H3 in P. rewrite P. + simpl. apply next_sep; eauto. reflexivity. + - intros. destruct V' as (V'' & V'). destruct r. + + Simpl. + destruct (gpreg_eq g0 GPR16). { subst. Simpl. rewrite V; try discriminate. rewrite V''. subst rs2. Simpl. } + destruct (gpreg_eq g0 GPR32). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. } + destruct (gpreg_eq g0 GPR12). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. } + destruct (gpreg_eq g0 GPR17). { subst. Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. } + Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. { destruct g0; try discriminate. contradiction. } + + Simpl. rewrite V; try discriminate. rewrite V'; try discriminate. subst rs2. Simpl. + + contradiction. + } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3'). + exploit exec_straight_steps_2; eauto using functions_transl. + simpl fn_blocks. simpl fn_blocks in g. omega. constructor. + intros (ofs' & X & Y). + left; exists (State rs3' m3'); split. + eapply exec_straight_steps_1; eauto. + simpl fn_blocks. simpl fn_blocks in g. omega. + constructor. + econstructor; eauto. + rewrite X; econstructor; eauto. + apply agree_exten with rs2; eauto with asmgen. + unfold rs2. + apply agree_set_other; auto with asmgen. + apply agree_change_sp with (parent_sp s). + apply agree_undef_regs with rs0. auto. +Local Transparent destroyed_at_function_entry. + simpl; intros; Simpl. + unfold sp; congruence. + + intros. + assert (r <> RTMP). { contradict H3; rewrite H3; unfold data_preg; auto. } + rewrite Heqrs3'. Simpl. rewrite V. inversion V'. rewrite H6. auto. + assert (r <> GPRA). { contradict H3; rewrite H3; unfold data_preg; auto. } + assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. } + contradict H3; rewrite H3; unfold data_preg; auto. + contradict H3; rewrite H3; unfold data_preg; auto. + contradict H3; rewrite H3; unfold data_preg; auto. + contradict H3; rewrite H3; unfold data_preg; auto. + intros. rewrite Heqrs3'. rewrite V by auto with asmgen. + assert (forall r : preg, r <> PC -> r <> GPRA -> rs' r = rs2 r). { apply V'. } + rewrite H4 by auto with asmgen. reflexivity. discriminate. + +- (* external function *) + inv MS. + exploit functions_translated; eauto. + intros [tf [A B]]. simpl in B. inv B. + exploit extcall_arguments_match; eauto. + intros [args' [C D]]. + exploit external_call_mem_extends; eauto. + intros [res' [m2' [P [Q [R S]]]]]. + left; econstructor; split. + apply plus_one. eapply exec_step_external; eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + econstructor; eauto. + unfold loc_external_result. + apply agree_set_other; auto. + apply agree_set_pair; auto. + apply agree_undef_caller_save_regs; auto. + +- (* return *) + inv MS. + inv STACKS. simpl in *. + right. split. omega. split. auto. + rewrite <- ATPC in H5. + econstructor; eauto. congruence. +Qed.*) + +Lemma transf_initial_states: + forall st1, MB.initial_state prog st1 -> + exists st2, AB.initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inversion H. unfold ge0 in *. + econstructor; split. + econstructor. + eapply (Genv.init_mem_transf_partial TRANSF); eauto. + replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero) + with (Vptr fb Ptrofs.zero). + econstructor; eauto. + constructor. + apply Mem.extends_refl. + split. auto. simpl. unfold Vnullptr; destruct Archi.ptr64; congruence. + intros. rewrite Mach.Regmap.gi. auto. + unfold Genv.symbol_address. + rewrite (match_program_main TRANSF). + rewrite symbols_preserved. + unfold ge; rewrite H1. auto. +Qed. + +Lemma transf_final_states: + forall st1 st2 r, + match_states st1 st2 -> MB.final_state st1 r -> AB.final_state st2 r. +Proof. + intros. inv H0. inv H. constructor. assumption. + compute in H1. inv H1. + generalize (preg_val _ _ _ R0 AG). rewrite H2. intros LD; inv LD. auto. +Qed. + Definition return_address_offset : Machblock.function -> Machblock.code -> ptrofs -> Prop := Asmblockgenproof0.return_address_offset. Lemma transf_program_correct: forward_simulation (MB.semantics return_address_offset prog) (AB.semantics lk tprog). +Proof. + eapply forward_simulation_star with (measure := measure). + - apply senv_preserved. + - eexact transf_initial_states. + - eexact transf_final_states. + - exact step_simulation. Admitted. End PRESERVATION. diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v index 0187a494..69d6037c 100644 --- a/aarch64/Asmblockgenproof0.v +++ b/aarch64/Asmblockgenproof0.v @@ -42,6 +42,31 @@ Require Import Asmblockprops. Module MB:=Machblock. Module AB:=Asmblock. +(** * Agreement between Mach registers and processor registers *) + +Record agree (ms: Mach.regset) (sp: val) (rs: AB.regset) : Prop := mkagree { + agree_sp: rs#SP = sp; + agree_sp_def: sp <> Vundef; + agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r)) +}. + +Lemma agree_exten: + forall ms sp rs rs', + agree ms sp rs -> + (forall r, data_preg r = true -> rs'#r = rs#r) -> + agree ms sp rs'. +Proof. + intros. destruct H. split; auto. + rewrite H0; auto. auto. + intros. rewrite H0; auto. apply preg_of_data. +Qed. + +Lemma preg_val: + forall ms sp rs r, agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r). +Proof. + intros. destruct H. auto. +Qed. + Inductive code_tail: Z -> bblocks -> bblocks -> Prop := | code_tail_0: forall c, code_tail 0 c c @@ -211,4 +236,94 @@ Proof. + exists Ptrofs.zero; red; intros. congruence. Qed. -End RETADDR_EXISTS. \ No newline at end of file +End RETADDR_EXISTS. + +(** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points + within the Asmblock code generated by translating Machblock function [f], + and [tc] is the tail of the generated code at the position corresponding + to the code pointer [pc]. *) + +Inductive transl_code_at_pc (ge: MB.genv): + val -> block -> MB.function -> MB.code -> bool -> AB.function -> AB.bblocks -> Prop := + transl_code_at_pc_intro: + forall b ofs f c ep tf tc, + Genv.find_funct_ptr ge b = Some(Internal f) -> + transf_function f = Errors.OK tf -> + transl_blocks f c ep = OK tc -> + code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc -> + transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc. + +Remark code_tail_no_bigger: + forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat. +Proof. + induction 1; simpl; omega. +Qed. + +Remark code_tail_unique: + forall fn c pos pos', + code_tail pos fn c -> code_tail pos' fn c -> pos = pos'. +Proof. + induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto. + generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. + generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. + f_equal. eauto. +Qed. + +Lemma return_address_offset_correct: + forall ge b ofs fb f c tf tc ofs', + transl_code_at_pc ge (Vptr b ofs) fb f c false tf tc -> + return_address_offset f c ofs' -> + ofs' = ofs. +Proof. + intros. inv H. red in H0. + exploit code_tail_unique. eexact H12. eapply H0; eauto. intro. + rewrite <- (Ptrofs.repr_unsigned ofs). + rewrite <- (Ptrofs.repr_unsigned ofs'). + congruence. +Qed. + +(** * Properties of the Machblock call stack *) + +Section MATCH_STACK. + +Variable ge: MB.genv. + +Inductive match_stack: list MB.stackframe -> Prop := + | match_stack_nil: + match_stack nil + | match_stack_cons: forall fb sp ra c s f tf tc, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transl_code_at_pc ge ra fb f c false tf tc -> + sp <> Vundef -> + match_stack s -> + match_stack (Stackframe fb sp ra c :: s). + +Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. +Proof. + induction 1; simpl. + unfold Vnullptr; destruct Archi.ptr64; congruence. + auto. +Qed. + +Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef. +Proof. + induction 1; simpl. + unfold Vnullptr; destruct Archi.ptr64; congruence. + inv H0. congruence. +Qed. + +Lemma lessdef_parent_sp: + forall s v, + match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s. +Proof. + intros. inv H0. auto. exploit parent_sp_def; eauto. tauto. +Qed. + +Lemma lessdef_parent_ra: + forall s v, + match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s. +Proof. + intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. +Qed. + +End MATCH_STACK. \ No newline at end of file -- cgit