diff options
Diffstat (limited to 'src/hls/GibleSeqgenproof.v')
-rw-r--r-- | src/hls/GibleSeqgenproof.v | 1011 |
1 files changed, 1011 insertions, 0 deletions
diff --git a/src/hls/GibleSeqgenproof.v b/src/hls/GibleSeqgenproof.v new file mode 100644 index 0000000..55b25d1 --- /dev/null +++ b/src/hls/GibleSeqgenproof.v @@ -0,0 +1,1011 @@ +(*| +.. + Vericert: Verified high-level synthesis. + Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see <https://www.gnu.org/licenses/>. + +================ +RTLBlockgenproof +================ + +.. coq:: none +|*) + +Require compcert.backend.RTL. +Require Import compcert.common.AST. +Require Import compcert.common.Errors. +Require Import compcert.common.Globalenvs. +Require Import compcert.lib.Maps. +Require Import compcert.backend.Registers. +Require Import compcert.common.Smallstep. +Require Import compcert.common.Events. +Require Import compcert.common.Memory. +Require Import compcert.common.Values. + +Require Import vericert.common.Vericertlib. +Require Import vericert.common.DecEq. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GibleSeq. +Require Import vericert.hls.GibleSeqgen. + +#[local] Open Scope positive. + +(*| +Defining a find block specification +=================================== + +Basically, it should be able to find the location of the block without using the +``find_block`` function, so that this is more useful for the proofs. There are +various different types of options that could come up though: + +1. The instruction is a standard instruction present inside of a basic block. +2. The instruction is a standard instruction which ends with a ``goto``. +3. The instruction is a control-flow instruction. + +For case number 1, there should exist a value in the list of instructions, such +that the instructions match exactly, and the indices match as well. In the +original code, this instruction must have been going from the current node to +the node - 1. + +For case number 2, there should be an instruction at the right index again, +however, this time there will also be a ``goto`` instruction in the control-flow +part of the basic block. + +For case number 3, there should be a ``nop`` instruction in the basic block, and +then the equivalent control-flow instruction ending the basic block. + +In the end though, it seems like two cases are actually enough, as the last two +cases are similar enough that they can be merged into one. +|*) + +Definition all_max {A} (c: PTree.t A) p: Prop := + Forall (fun x => x <= p) (map fst (PTree.elements c)). + +Definition offset (pc pc': positive): nat := Pos.to_nat pc' - Pos.to_nat pc. + +Section CORRECTNESS. + + Context (prog : RTL.program). + Context (tprog : GibleSeq.program). + + Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. + Let tge : genv := Globalenvs.Genv.globalenv tprog. + +(*| +Matches the basic block that should be present in the state. This simulates the +small step execution of the basic block from the big step semantics that are +currently present. + +Why does it not need to find the pc' value using ``find_block``? + +It doesn't have to find the value because it's given as an input, and the +finding is actually done at that higher level already. +|*) + +(* Variant match_bblock (tc: code) (pc pc': node): list instr -> Prop := + | match_bblock_intro : + forall bb cf, + tc ! pc' = Some (mk_bblock bb cf) -> + match_bblock tc pc pc' (list_drop (offset pc pc') bb).*) + + Definition imm_succ (pc pc': node) : Prop := pc' = Pos.pred pc. + + Definition valid_succ (tc: code) (pc: node) : Prop := exists b, tc ! pc = Some b. + + Inductive match_block (c: RTL.code) (tc: code) (pc: node): BB.t -> Prop := + (* + * Basic Block Instructions + *) + | match_block_nop b pc': + c ! pc = Some (RTL.Inop pc') -> + match_block c tc pc' b -> + match_block c tc pc (RBnop :: b) + | match_block_op b op args dst pc': + c ! pc = Some (RTL.Iop op args dst pc') -> + match_block c tc pc' b -> + match_block c tc pc (RBop None op args dst :: b) + | match_block_load b chunk addr args dst pc': + c ! pc = Some (RTL.Iload chunk addr args dst pc') -> + match_block c tc pc' b -> + match_block c tc pc (RBload None chunk addr args dst :: b) + | match_block_store b chunk addr args src pc': + c ! pc = Some (RTL.Istore chunk addr args src pc') -> + match_block c tc pc' b -> + match_block c tc pc (RBstore None chunk addr args src :: b) + (* + * Control flow instructions using goto + *) + | match_block_goto pc': + c ! pc = Some (RTL.Inop pc') -> + valid_succ tc pc' -> + match_block c tc pc (RBnop :: RBexit None (RBgoto pc') :: nil) + | match_block_op_cf pc' op args dst: + c ! pc = Some (RTL.Iop op args dst pc') -> + valid_succ tc pc' -> + match_block c tc pc (RBop None op args dst :: RBexit None (RBgoto pc') :: nil) + | match_block_load_cf pc' chunk addr args dst: + c ! pc = Some (RTL.Iload chunk addr args dst pc') -> + valid_succ tc pc' -> + match_block c tc pc (RBload None chunk addr args dst :: RBexit None (RBgoto pc') :: nil) + | match_block_store_cf pc' chunk addr args src: + c ! pc = Some (RTL.Istore chunk addr args src pc') -> + valid_succ tc pc' -> + match_block c tc pc (RBstore None chunk addr args src :: RBexit None (RBgoto pc') :: nil) + (* + * Standard control flow instructions + *) + | match_block_call sig ident args dst pc' : + c ! pc = Some (RTL.Icall sig ident args dst pc') -> + valid_succ tc pc' -> + match_block c tc pc (RBnop :: RBexit None (RBcall sig ident args dst pc') :: nil) + | match_block_tailcall sig ident args : + c ! pc = Some (RTL.Itailcall sig ident args) -> + match_block c tc pc (RBnop :: RBexit None (RBtailcall sig ident args) :: nil) + | match_block_builtin ident args dst pc' : + c ! pc = Some (RTL.Ibuiltin ident args dst pc') -> + valid_succ tc pc' -> + match_block c tc pc (RBnop :: RBexit None (RBbuiltin ident args dst pc') :: nil) + | match_block_cond cond args pct pcf : + c ! pc = Some (RTL.Icond cond args pct pcf) -> + valid_succ tc pct -> + valid_succ tc pcf -> + match_block c tc pc (RBnop :: RBexit None (RBcond cond args pct pcf) :: nil) + | match_block_jumptable r ns : + c ! pc = Some (RTL.Ijumptable r ns) -> + Forall (valid_succ tc) ns -> + match_block c tc pc (RBnop :: RBexit None (RBjumptable r ns) :: nil) + | match_block_return r : + c ! pc = Some (RTL.Ireturn r) -> + match_block c tc pc (RBnop :: RBexit None (RBreturn r) :: nil) + . + +(*| +Match the code +~~~~~~~~~~~~~~ + +The ``match_code`` predicate asserts that for any node in the original +control-flow graph, there is now a basic block in the new control- and data-flow +graph that contains the same instruction, but also that the whole basic block +matches some sequence of instructions starting at the node that corresponds to +the basic block. +|*) + + Definition match_code (c: RTL.code) (tc: code) : Prop := + forall pc b, tc ! pc = Some b -> match_block c tc pc b. + + Variant match_stackframe : RTL.stackframe -> stackframe -> Prop := + | match_stackframe_init : + forall res f tf sp pc rs + (TF: transl_function f = OK tf) + (VALID: valid_succ tf.(fn_code) pc), + match_stackframe (RTL.Stackframe res f sp pc rs) + (Stackframe res tf sp pc rs (PMap.init false)). + + Definition sem_extrap f pc sp in_s in_s' block := + forall out_s block2, + BB.step tge sp in_s block out_s -> + f.(fn_code) ! pc = Some block2 -> + BB.step tge sp in_s' block2 out_s. + + Lemma match_block_exists_instr : + forall c tc pc a, + match_block c tc pc a -> + exists i, c ! pc = Some i. + Proof. inversion 1; eexists; eauto. Qed. + + Lemma match_block_not_nil : + forall c tc pc a, + match_block c tc pc a -> a <> nil. + Proof. inversion 1; crush. Qed. + +(*| +Matching states +~~~~~~~~~~~~~~~ + +Initially, the idea was to define the ``match_states`` predicate normally to +defines how to find the correct ``bb`` that should be executed, as well as the +value of ``pc``. However, this does not quite work when proving the equivalence +of the translation from ``RTL`` to ``RTLBlock``, because one cannot match one +transition to a transition in RTLBlock. The alternative to this is to include a +proof inside of the ``match_states`` that shows that the execution from the +``pc`` of the start of the basic block to the current point is the same as the +whole execution (in one big step) of the basic block. +|*) + + Variant match_states : option BB.t -> RTL.state -> state -> Prop := + | match_state : + forall stk stk' f tf sp pc rs m pc0 b rs0 m0 + (TF: transl_function f = OK tf) + (* TODO: I can remove the following [match_code]. *) + (CODE: match_code f.(RTL.fn_code) tf.(fn_code)) + (BLOCK: exists b', tf.(fn_code) ! pc0 = Some b' + /\ match_block f.(RTL.fn_code) tf.(fn_code) pc b) + (STK: Forall2 match_stackframe stk stk') + (STARSIMU: star RTL.step ge (RTL.State stk f sp pc0 rs0 m0) + E0 (RTL.State stk f sp pc rs m)) + (BB: sem_extrap tf pc0 sp (Iexec (mk_instr_state rs (PMap.init false) m)) + (Iexec (mk_instr_state rs0 (PMap.init false) m0)) b), + match_states (Some b) (RTL.State stk f sp pc rs m) + (State stk' tf sp pc0 rs0 (PMap.init false) m0) + | match_callstate : + forall cs cs' f tf args m + (TF: transl_fundef f = OK tf) + (STK: Forall2 match_stackframe cs cs'), + match_states None (RTL.Callstate cs f args m) (Callstate cs' tf args m) + | match_returnstate : + forall cs cs' v m + (STK: Forall2 match_stackframe cs cs'), + match_states None (RTL.Returnstate cs v m) (Returnstate cs' v m) + . + + Definition match_prog (p: RTL.program) (tp: GibleSeq.program) := + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + + Context (TRANSL : match_prog prog tprog). + + Lemma symbols_preserved: + forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. + Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed. + + Lemma senv_preserved: + Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). + Proof using TRANSL. intros; eapply (Genv.senv_transf_partial TRANSL). Qed. + #[local] Hint Resolve senv_preserved : rtlbg. + + Lemma function_ptr_translated: + forall b f, + Genv.find_funct_ptr ge b = Some f -> + exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. + Proof (Genv.find_funct_ptr_transf_partial TRANSL). + + Lemma sig_transl_function: + forall (f: RTL.fundef) (tf: GibleSeq.fundef), + transl_fundef f = OK tf -> + GibleSeq.funsig tf = RTL.funsig f. + Proof using. + unfold transl_fundef. unfold transf_partial_fundef. + intros. destruct_match. unfold bind in *. destruct_match; try discriminate. + inv H. unfold transl_function in Heqr. + repeat (destruct_match; try discriminate). inv Heqr. auto. + inv H; auto. + Qed. + + Definition measure (b: option BB.t): nat := + match b with + | None => 0 + | Some b' => 1 + length b' + end. + + Lemma check_valid_node_correct : + forall a b, check_valid_node a b = true -> valid_succ a b. + Proof. + intros. unfold valid_succ, check_valid_node in *. + destruct_match; try discriminate; eauto. + Qed. + + Lemma transl_entrypoint_exists : + forall f tf, + transl_function f = OK tf -> + valid_succ (fn_code tf) (fn_entrypoint tf). + Proof. + unfold transl_function; intros. + repeat (destruct_match; try discriminate; []). inv H. simplify. + eauto using check_valid_node_correct. + Qed. + + Lemma ceq_eq : + forall A a (b: A) c, + ceq a b c = true -> + b = c. + Proof. + intros. unfold ceq in H. destruct_match; try discriminate. auto. + Qed. + + Ltac unfold_ands := + repeat match goal with + | H: _ && _ = true |- _ => apply andb_prop in H + | H: _ /\ _ |- _ => inv H + | H: ceq _ _ _ = true |- _ => apply ceq_eq in H; subst + end. + + Lemma transl_match_code' : + forall c tc b pc, + check_code c tc pc b = true -> + match_block c tc pc b. + Proof. + induction b; [crush|]. + - repeat (destruct_match; try discriminate). + - intros. + unfold check_code in H. + do 2 (destruct_match; try discriminate); subst; fold check_code in H. + + repeat (destruct_match; try discriminate); try solve [econstructor; eauto]. + unfold_ands. + eapply match_block_goto; eauto. eauto using check_valid_node_correct. + + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto]. + unfold_ands. + eapply match_block_op_cf; eauto. eauto using check_valid_node_correct. + + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto]. + unfold_ands. + eapply match_block_load_cf; eauto. eauto using check_valid_node_correct. + + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto]. + unfold_ands. + eapply match_block_store_cf; eauto. eauto using check_valid_node_correct. + + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto]. + unfold_ands. eapply match_block_call; eauto using check_valid_node_correct. + unfold_ands. eapply match_block_call; eauto using check_valid_node_correct. + + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto]. + + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto]. + unfold_ands. eapply match_block_cond; eauto using check_valid_node_correct. + + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto]. + unfold_ands. eapply match_block_jumptable; eauto using check_valid_node_correct. + apply Forall_forall; intros. eapply forallb_forall in H1; eauto using check_valid_node_correct. + + repeat (destruct_match; try discriminate); subst; try solve [unfold_ands; econstructor; eauto]. + Qed. + + Lemma transl_match_code : + forall f tf, + transl_function f = OK tf -> + match_code f.(RTL.fn_code) tf.(fn_code). + Proof. + unfold transl_function; intros. + repeat (destruct_match; try discriminate; []). inv H. simplify. + unfold match_code; intros. + eapply forall_ptree_true in Heqb0; eauto. + unfold check_code in *. + eauto using transl_match_code'. + Qed. + + Lemma transl_initial_states : + forall s1, RTL.initial_state prog s1 -> + exists s2, GibleSeq.initial_state tprog s2 /\ match_states None s1 s2. + Proof using TRANSL. + induction 1. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + do 2 econstructor. simplify. econstructor. + apply (Genv.init_mem_transf_partial TRANSL); eauto. + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto. + symmetry; eapply Linking.match_program_main; eauto. eauto. + erewrite sig_transl_function; eauto. constructor. auto. auto. + Qed. + + Lemma transl_final_states : + forall s1 s2 r b, + match_states b s1 s2 -> + RTL.final_state s1 r -> + GibleSeq.final_state s2 r. + Proof using. + inversion 2; crush. subst. inv H. inv STK. econstructor. + Qed. + + Lemma hd_nth_equiv: + forall A n (l: list A), hd_error (list_drop n l) = nth_error l n. + Proof. induction n; destruct l; crush. Qed. + + Lemma hd_error_Some_exists: + forall A (l: list A) n, hd_error l = Some n -> l = n :: tl l. + Proof. induction l; crush. Qed. + + Definition imm_succ_dec pc pc' : {imm_succ pc pc'} + {~ imm_succ pc pc'}. + Proof. + unfold imm_succ. pose proof peq. + decide equality. + Defined. + + Lemma imm_succ_refl pc : imm_succ pc (Pos.pred pc). + Proof. unfold imm_succ; auto. Qed. + + Lemma imm_succ_refl2 pc : imm_succ (Pos.succ pc) pc. + Proof. unfold imm_succ; auto using Pos.pred_succ. Qed. + + Lemma sim_star : + forall s1 b t s, + (exists b' s2, + star step tge s1 t s2 /\ ltof _ measure b' b + /\ match_states b' s s2) -> + exists b' s2, + (plus step tge s1 t s2 \/ + star step tge s1 t s2 /\ ltof _ measure b' b) /\ + match_states b' s s2. + Proof. intros; simplify. do 3 econstructor; eauto. Qed. + + Lemma sim_plus : + forall s1 b t s, + (exists b' s2, plus step tge s1 t s2 /\ match_states b' s s2) -> + exists b' s2, + (plus step tge s1 t s2 \/ + star step tge s1 t s2 /\ ltof _ measure b' b) /\ + match_states b' s s2. + Proof. intros; simplify. do 3 econstructor; eauto. Qed. + + Lemma transl_Inop_correct: + forall s f sp pc rs m pc', + (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> + forall b s2, match_states b (RTL.State s f sp pc rs m) s2 -> + exists b' s2', + (plus step tge s2 E0 s2' + \/ star step tge s2 E0 s2' /\ ltof _ measure b' b) + /\ match_states b' (RTL.State s f sp pc' rs m) s2'. + Proof. + intros * H. + inversion 1; subst; simplify. + unfold match_code in *. + match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify. + { apply sim_star. + do 3 econstructor. eapply star_refl. constructor. + instantiate (1 := Some b); unfold ltof; auto. + + constructor; try eassumption. econstructor; eauto. + eapply star_right; eauto. + eapply RTL.exec_Inop; eauto. auto. + + unfold sem_extrap in *. intros. + eapply BB. econstructor; eauto. + econstructor; eauto. auto. + } + { apply sim_plus. + inv H0. simplify. + unfold valid_succ in *; simplify. + do 3 econstructor. apply plus_one. econstructor. + eassumption. eapply BB; [| eassumption ]. + econstructor; econstructor; eauto. + econstructor. econstructor. econstructor. + + econstructor; try eassumption. eauto. + eapply star_refl. + unfold sem_extrap. intros. setoid_rewrite H6 in H0. + crush. + } + Qed. + + Lemma eval_op_eq: + forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val) m, + Op.eval_operation ge sp0 op vl m = Op.eval_operation tge sp0 op vl m. + Proof using TRANSL. + intros. + destruct op; auto; unfold Op.eval_operation, Genv.symbol_address, Op.eval_addressing32; + [| destruct a; unfold Genv.symbol_address ]; + try rewrite symbols_preserved; auto. + Qed. + + Lemma eval_addressing_eq: + forall sp addr vl, + Op.eval_addressing ge sp addr vl = Op.eval_addressing tge sp addr vl. + Proof using TRANSL. + intros. + destruct addr; + unfold Op.eval_addressing, Op.eval_addressing32; + unfold Genv.symbol_address; + try rewrite symbols_preserved; auto. + Qed. + + Lemma transl_Iop_correct_nj: + forall s f sp pc rs m op args res pc' v stk' tf pc1 rs1 m1 b x, + (RTL.fn_code f) ! pc = Some (RTL.Iop op args res pc') -> + Op.eval_operation ge sp op rs ## args m = Some v -> + transl_function f = OK tf -> + (forall pc0 b0, + (fn_code tf) ! pc0 = Some b0 -> match_block (RTL.fn_code f) (fn_code tf) pc0 b0) -> + Forall2 match_stackframe s stk' -> + star RTL.step ge (RTL.State s f sp pc1 rs1 m1) E0 (RTL.State s f sp pc rs m) -> + sem_extrap tf pc1 sp (Iexec {| is_rs := rs; is_ps := PMap.init false; is_mem := m |}) + (Iexec {| is_rs := rs1; is_ps := PMap.init false; is_mem := m1 |}) (RBop None op args res :: b) -> + (fn_code tf) ! pc1 = Some x -> + match_block (RTL.fn_code f) (fn_code tf) pc' b -> + exists b' s2', + star step tge (State stk' tf sp pc1 rs1 (PMap.init false) m1) E0 s2' + /\ ltof _ measure b' (Some (RBop None op args res :: b)) + /\ match_states b' (RTL.State s f sp pc' rs # res <- v m) s2'. + Proof. + intros * IOP EVAL TR MATCHB STK STAR BB INCODE MATCHB2. + do 3 econstructor. eapply star_refl. constructor. + instantiate (1 := Some b); unfold ltof; auto. + + constructor; try eassumption. econstructor; eauto. + eapply star_right; eauto. + eapply RTL.exec_Iop; eauto. auto. + + unfold sem_extrap in *. intros. + eapply BB. econstructor; eauto. + econstructor; eauto. + rewrite <- eval_op_eq; eassumption. + constructor. auto. + Qed. + + Lemma transl_Iop_correct_j: + forall s f sp pc rs m op args res pc' v stk' tf pc1 rs1 m1 x, + (RTL.fn_code f) ! pc = Some (RTL.Iop op args res pc') -> + Op.eval_operation ge sp op rs ## args m = Some v -> + transl_function f = OK tf -> + (forall (pc0 : positive) (b : BB.t), + (fn_code tf) ! pc0 = Some b -> match_block (RTL.fn_code f) (fn_code tf) pc0 b) -> + Forall2 match_stackframe s stk' -> + star RTL.step ge (RTL.State s f sp pc1 rs1 m1) E0 (RTL.State s f sp pc rs m) -> + sem_extrap tf pc1 sp (Iexec {| is_rs := rs; is_ps := PMap.init false; is_mem := m |}) + (Iexec {| is_rs := rs1; is_ps := PMap.init false; is_mem := m1 |}) (RBop None op args res :: RBexit None (RBgoto pc') :: nil) -> + (fn_code tf) ! pc1 = Some x -> + valid_succ (fn_code tf) pc' -> + exists b' s2, + plus step tge (State stk' tf sp pc1 rs1 (PMap.init false) m1) E0 s2 /\ + match_states b' (RTL.State s f sp pc' rs # res <- v m) s2. + Proof. + intros * H H0 TF CODE STK STARSIMU BB H3 H7. + inv H0. simplify. + unfold valid_succ in H7; simplify. + do 3 econstructor. apply plus_one. econstructor. + eassumption. eapply BB; [| eassumption ]. + econstructor; econstructor; eauto. + rewrite <- eval_op_eq; eassumption. + constructor. econstructor. econstructor. + econstructor. + + econstructor; try eassumption. eauto. + eapply star_refl. + unfold sem_extrap. intros. setoid_rewrite H0 in H4. + crush. + Qed. + + Lemma transl_Iop_correct: + forall s f sp pc rs m op args res pc' v, + (RTL.fn_code f) ! pc = Some (RTL.Iop op args res pc') -> + Op.eval_operation ge sp op rs##args m = Some v -> + forall b s2, match_states b (RTL.State s f sp pc rs m) s2 -> + exists b' s2', + (plus step tge s2 E0 s2' + \/ star step tge s2 E0 s2' /\ ltof _ measure b' b) + /\ match_states b' (RTL.State s f sp pc' (rs # res <- v) m) s2'. + Proof. + intros * H H0. + inversion 1; subst; simplify. + unfold match_code in *. + match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify. + { apply sim_star; eapply transl_Iop_correct_nj; eassumption. } + { apply sim_plus. eapply transl_Iop_correct_j; eassumption. } + Qed. + + Lemma transl_Iload_correct: + forall s f sp pc rs m chunk addr args dst pc' a v, + (RTL.fn_code f) ! pc = Some (RTL.Iload chunk addr args dst pc') -> + Op.eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + forall b s2, match_states b (RTL.State s f sp pc rs m) s2 -> + exists b' s2', + (plus step tge s2 E0 s2' + \/ star step tge s2 E0 s2' /\ ltof _ measure b' b) + /\ match_states b' (RTL.State s f sp pc' (rs # dst <- v) m) s2'. + Proof. + intros * H H0 H1. + inversion 1; subst; simplify. + unfold match_code in *. + match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify. + { apply sim_star. + do 3 econstructor. eapply star_refl. constructor. + instantiate (1 := Some b); unfold ltof; auto. + + constructor; try eassumption. econstructor; eauto. + eapply star_right; eauto. + eapply RTL.exec_Iload; eauto. auto. + + unfold sem_extrap in *. intros. + eapply BB. econstructor; eauto. + econstructor; eauto. + rewrite <- eval_addressing_eq; eassumption. + constructor. auto. + } + { apply sim_plus. + inv H0. simplify. + unfold valid_succ in H6; simplify. + do 3 econstructor. apply plus_one. econstructor. + eassumption. eapply BB; [| eassumption ]. + econstructor; econstructor; eauto. + rewrite <- eval_addressing_eq; eassumption. + constructor. econstructor. econstructor. + econstructor. + + econstructor; try eassumption. eauto. + eapply star_refl. + unfold sem_extrap. intros. setoid_rewrite H0 in H6. + crush. + } + Qed. + + Lemma transl_Istore_correct: + forall s f sp pc rs m chunk addr args src pc' a m', + (RTL.fn_code f) ! pc = Some (RTL.Istore chunk addr args src pc') -> + Op.eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a rs#src = Some m' -> + forall b s2, match_states b (RTL.State s f sp pc rs m) s2 -> + exists b' s2', + (plus step tge s2 E0 s2' + \/ star step tge s2 E0 s2' /\ ltof _ measure b' b) + /\ match_states b' (RTL.State s f sp pc' rs m') s2'. + Proof. + intros * H H0 H1. + inversion 1; subst; simplify. + unfold match_code in *. + match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify. + { apply sim_star. + do 3 econstructor. eapply star_refl. constructor. + instantiate (1 := Some b); unfold ltof; auto. + + constructor; try eassumption. econstructor; eauto. + eapply star_right; eauto. + eapply RTL.exec_Istore; eauto. auto. + + unfold sem_extrap in *. intros. + eapply BB. econstructor; eauto. + econstructor; eauto. + rewrite <- eval_addressing_eq; eassumption. + constructor. auto. + } + { apply sim_plus. + inv H0. simplify. + unfold valid_succ in H6; simplify. + do 3 econstructor. apply plus_one. econstructor. + eassumption. eapply BB; [| eassumption ]. + econstructor; econstructor; eauto. + rewrite <- eval_addressing_eq; eassumption. + constructor. econstructor. econstructor. + econstructor. + + econstructor; try eassumption. eauto. + eapply star_refl. + unfold sem_extrap. intros. setoid_rewrite H0 in H6. + crush. + } + Qed. + + Lemma functions_translated: + forall (v: Values.val) (f: RTL.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. + Proof using TRANSL. + intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. + Qed. + + Lemma find_function_translated: + forall ros rs rs' f, + (forall x, rs !! x = rs' !! x) -> + RTL.find_function ge ros rs = Some f -> + exists tf, find_function tge ros rs' = Some tf + /\ transl_fundef f = OK tf. + Proof using TRANSL. + Ltac ffts := match goal with + | [ H: forall _, Val.lessdef _ _, r: Registers.reg |- _ ] => + specialize (H r); inv H + | [ H: Vundef = ?r, H1: Genv.find_funct _ ?r = Some _ |- _ ] => + rewrite <- H in H1 + | [ H: Genv.find_funct _ Vundef = Some _ |- _] => solve [inv H] + | _ => solve [exploit functions_translated; eauto] + end. + destruct ros; simplify; try rewrite <- H; + [| rewrite symbols_preserved; destruct_match; + try (apply function_ptr_translated); crush ]; + intros; + repeat ffts. + Qed. + + Lemma transl_Icall_correct: + forall s f sp pc rs m sig ros args res pc' fd, + (RTL.fn_code f) ! pc = Some (RTL.Icall sig ros args res pc') -> + RTL.find_function ge ros rs = Some fd -> + RTL.funsig fd = sig -> + forall b s2, match_states b (RTL.State s f sp pc rs m) s2 -> + exists b' s2', + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof _ measure b' b) /\ + match_states b' (RTL.Callstate (RTL.Stackframe res f sp pc' rs :: s) fd rs ## args m) s2'. + Proof. + intros * H H0 H1. + inversion 1; subst; simplify. + unfold match_code in *. + match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify; + apply sim_plus. + inv H0. simplify. + unfold valid_succ in H5; simplify. + exploit find_function_translated; eauto; simplify. + do 3 econstructor. apply plus_one. econstructor. + eassumption. eapply BB; [| eassumption ]. + econstructor; econstructor; eauto. + econstructor. econstructor. + econstructor; eauto. + apply sig_transl_function; auto. + + econstructor; try eassumption. + constructor. constructor; auto. + unfold valid_succ; eauto. auto. + Qed. + + Lemma transl_Itailcall_correct: + forall s f stk pc rs m sig ros args fd m', + (RTL.fn_code f) ! pc = Some (RTL.Itailcall sig ros args) -> + RTL.find_function ge ros rs = Some fd -> + RTL.funsig fd = sig -> + Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> + forall b s2, + match_states b (RTL.State s f (Vptr stk Integers.Ptrofs.zero) pc rs m) s2 -> + exists b' s2', + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\ + match_states b' (RTL.Callstate s fd rs ## args m') s2'. + Proof. + intros * H H0 H1 H2. + inversion 1; subst; simplify. + unfold match_code in *. + match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify; + apply sim_plus. + inv H0. simplify. + unfold valid_succ in H6; simplify. + exploit find_function_translated; eauto; simplify. + do 3 econstructor. apply plus_one. econstructor. + eassumption. eapply BB; [| eassumption ]. + econstructor; econstructor; eauto. + econstructor. econstructor. + econstructor; eauto. + apply sig_transl_function; auto. + assert (fn_stacksize tf = RTL.fn_stacksize f). + { unfold transl_function in TF. + repeat (destruct_match; try discriminate; []). + inv TF; auto. } + rewrite H5. eassumption. + + econstructor; try eassumption. + Qed. + + Lemma transl_Ibuiltin_correct: + forall s f sp pc rs m ef args res pc' vargs t vres m', + (RTL.fn_code f) ! pc = Some (RTL.Ibuiltin ef args res pc') -> + eval_builtin_args ge (fun r : positive => rs # r) sp m args vargs -> + external_call ef ge vargs m t vres m' -> + forall b s2, + match_states b (RTL.State s f sp pc rs m) s2 -> + exists b' s2', + (plus step tge s2 t s2' \/ star step tge s2 t s2' /\ ltof _ measure b' b) /\ + match_states b' (RTL.State s f sp pc' (regmap_setres res vres rs) m') s2'. + Proof. + intros * H H0 H1. + inversion 1; subst; simplify. + unfold match_code in *. + match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify. + eapply sim_plus. + unfold valid_succ in H6; simplify. + do 3 econstructor. apply plus_one. econstructor. + eassumption. eapply BB; [| eassumption ]. + econstructor; econstructor; eauto. + econstructor. econstructor. econstructor; eauto. + eauto using eval_builtin_args_preserved, symbols_preserved. + eauto using external_call_symbols_preserved, senv_preserved. + + econstructor; try eassumption. eauto. + eapply star_refl. + unfold sem_extrap. intros. setoid_rewrite H5 in H7. crush. + Qed. + + Lemma init_regs_equiv : + forall b a, init_regs a b = RTL.init_regs a b. + Proof. induction b; crush. Qed. + + Lemma transl_initcall_correct: + forall s f args m m' stk, + Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) -> + forall b s2, + match_states b (RTL.Callstate s (Internal f) args m) s2 -> + exists b' s2', + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\ + match_states b' + (RTL.State s f (Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) (RTL.init_regs args (RTL.fn_params f)) m') s2'. + Proof. + intros * H. + inversion 1; subst; simplify. + monadInv TF. inv H0. + pose proof (transl_match_code _ _ EQ). + pose proof (transl_entrypoint_exists _ _ EQ). unfold valid_succ in H1. + simplify. + apply sim_plus. do 3 econstructor. + assert (fn_stacksize x = RTL.fn_stacksize f). + { unfold transl_function in EQ. + repeat (destruct_match; try discriminate; []). + inv EQ; auto. } + apply plus_one. econstructor; eauto. + rewrite H1. eauto. + + assert (fn_entrypoint x = RTL.fn_entrypoint f). + { unfold transl_function in EQ. + repeat (destruct_match; try discriminate; []). + inv EQ; auto. } + assert (fn_params x = RTL.fn_params f). + { unfold transl_function in EQ. + repeat (destruct_match; try discriminate; []). + inv EQ; auto. } + unfold match_code in H0. + pose proof (H0 _ _ H2). + econstructor; eauto. + rewrite <- H1. eauto. + rewrite H1. + rewrite init_regs_equiv. rewrite H3. eapply star_refl. + unfold sem_extrap; intros. + setoid_rewrite H2 in H6; simplify. + rewrite H3. eauto. + Qed. + + Lemma transl_externalcall_correct: + forall s ef args res t m m', + external_call ef ge args m t res m' -> + forall b s2, + match_states b (RTL.Callstate s (External ef) args m) s2 -> + exists b' s2', + (plus step tge s2 t s2' \/ star step tge s2 t s2' /\ ltof (option BB.t) measure b' b) /\ + match_states b' (RTL.Returnstate s res m') s2'. + Proof. + intros * H. + inversion 1; subst; simplify. + inv TF. + apply sim_plus. do 3 econstructor. + apply plus_one. + econstructor; eauto using external_call_symbols_preserved, senv_preserved. + econstructor; eauto. + Qed. + + Lemma transl_returnstate_correct: + forall res f sp pc rs s vres m b s2, + match_states b (RTL.Returnstate (RTL.Stackframe res f sp pc rs :: s) vres m) s2 -> + exists b' s2', + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\ + match_states b' (RTL.State s f sp pc rs # res <- vres m) s2'. + Proof. + intros. + inv H. inv STK. inv H1. + pose proof (transl_match_code _ _ TF). + unfold valid_succ in VALID. simplify. + unfold match_code in H. + pose proof (H _ _ H0). + apply sim_plus. do 3 econstructor. apply plus_one. + constructor. constructor; eauto using star_refl. + unfold sem_extrap; intros. + setoid_rewrite H0 in H4; crush. + Qed. + + Lemma transl_Icond_correct: + forall s f sp pc rs m cond args ifso ifnot b pc', + (RTL.fn_code f) ! pc = Some (RTL.Icond cond args ifso ifnot) -> + Op.eval_condition cond rs ## args m = Some b -> + pc' = (if b then ifso else ifnot) -> + forall b0 s2, + match_states b0 (RTL.State s f sp pc rs m) s2 -> + exists b' s2', + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b0) /\ + match_states b' (RTL.State s f sp pc' rs m) s2'. + Proof. + intros * H H0 H1. + inversion 1; subst; simplify. + unfold match_code in *. + match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify; + apply sim_plus. + inv H0. simplify. + unfold valid_succ in *; simplify. + destruct b. + { do 3 econstructor. apply plus_one. + econstructor; eauto. eapply BB. econstructor. econstructor. + econstructor. econstructor. econstructor. eauto. + econstructor; eauto. + constructor; eauto using star_refl. + unfold sem_extrap; intros. setoid_rewrite H4 in H6. inv H6. auto. + } + { do 3 econstructor. apply plus_one. + econstructor; eauto. eapply BB. + econstructor. econstructor. + econstructor. econstructor. econstructor. eauto. + econstructor; eauto. + constructor; eauto using star_refl. + unfold sem_extrap; intros. setoid_rewrite H0 in H6. inv H6. auto. + } + Qed. + + Lemma transl_Ijumptable_correct: + forall s f sp pc rs m arg tbl n pc', + (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) -> + rs # arg = Vint n -> + list_nth_z tbl (Integers.Int.unsigned n) = Some pc' -> + forall b s2, + match_states b (RTL.State s f sp pc rs m) s2 -> + exists b' s2', + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\ + match_states b' (RTL.State s f sp pc' rs m) s2'. + Proof. + intros * H H0 H1. + inversion 1; subst; simplify. + unfold match_code in *. + match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify; + apply sim_plus. + eapply Forall_forall with (x:=pc') in H6; eauto using list_nth_z_in. + unfold valid_succ in H6; simplify. + do 3 econstructor. apply plus_one. + econstructor; eauto. eapply BB. + econstructor. econstructor. econstructor. econstructor. econstructor. + eauto. + econstructor; eauto. + + constructor; eauto using star_refl. + unfold sem_extrap; intros. setoid_rewrite H5 in H7. inv H7. auto. + Qed. + + Lemma transl_Ireturn_correct: + forall s f stk pc rs m or m', + (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> + Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> + forall b s2, + match_states b (RTL.State s f (Vptr stk Integers.Ptrofs.zero) pc rs m) s2 -> + exists b' s2', + (plus step tge s2 E0 s2' \/ star step tge s2 E0 s2' /\ ltof (option BB.t) measure b' b) /\ + match_states b' (RTL.Returnstate s (regmap_optget or Vundef rs) m') s2'. + Proof. + intros * H H0. + inversion 1; subst; simplify. + unfold match_code in *. + match goal with H: match_block _ _ _ _ |- _ => inv H end; simplify; + apply sim_plus. + assert (fn_stacksize tf = RTL.fn_stacksize f). + { unfold transl_function in TF. + repeat (destruct_match; try discriminate; []). + inv TF; auto. } + do 3 econstructor. apply plus_one. econstructor; eauto. + eapply BB. + econstructor. econstructor. econstructor. econstructor. + econstructor. eauto. + econstructor; eauto. + rewrite H4. eauto. + constructor; eauto. + Qed. + + Lemma transl_correct: + forall s1 t s1', + RTL.step ge s1 t s1' -> + forall b s2, match_states b s1 s2 -> + exists b' s2', + (plus step tge s2 t s2' \/ + (star step tge s2 t s2' /\ ltof _ measure b' b)) + /\ match_states b' s1' s2'. + Proof. + induction 1. + - eauto using transl_Inop_correct. + - eauto using transl_Iop_correct. + - eauto using transl_Iload_correct. + - eauto using transl_Istore_correct. + - eauto using transl_Icall_correct. + - eauto using transl_Itailcall_correct. + - eauto using transl_Ibuiltin_correct. + - eauto using transl_Icond_correct. + - eauto using transl_Ijumptable_correct. + - eauto using transl_Ireturn_correct. + - eauto using transl_initcall_correct. + - eauto using transl_externalcall_correct. + - eauto using transl_returnstate_correct. + Qed. + + Theorem transf_program_correct: + forward_simulation (RTL.semantics prog) (GibleSeq.semantics tprog). + Proof using TRANSL. + eapply (Forward_simulation + (L1:=RTL.semantics prog) + (L2:=GibleSeq.semantics tprog) + (ltof _ measure) match_states). + constructor. + - apply well_founded_ltof. + - eauto using transl_initial_states. + - intros; eapply transl_final_states; eauto. + - eapply transl_correct. + - apply senv_preserved. + Qed. + +End CORRECTNESS. |