From b708486d60c4c0aa695dca4ee46861c87cebb9e1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 29 Jan 2021 19:20:07 +0000 Subject: Fix definitions of proofs some more --- src/hls/RTLBlockInstr.v | 10 ---- src/hls/RTLPar.v | 12 +++- src/hls/RTLPargen.v | 98 ++++++++++++++++--------------- src/hls/RTLPargenproof.v | 148 ++++++++++++++++++++++++++++++++--------------- 4 files changed, 162 insertions(+), 106 deletions(-) (limited to 'src') diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 2744527..90edc2e 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -202,16 +202,6 @@ Section RELSEM. (RBstore chunk addr args src) (InstrState rs m'). - Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop := - | exec_RBcons: - forall state i state' state'' instrs sp, - step_instr sp state i state' -> - step_instr_list sp state' instrs state'' -> - step_instr_list sp state (i :: instrs) state'' - | exec_RBnil: - forall state sp, - step_instr_list sp state nil state. - Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop := | exec_RBcall: forall s f sp rs m res fd ros sig args pc pc', diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 3ad54f5..be9ff22 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -46,11 +46,21 @@ Section RELSEM. Context (ge: genv). + Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop := + | exec_RBcons: + forall state i state' state'' instrs sp, + step_instr ge sp state i state' -> + step_instr_list sp state' instrs state'' -> + step_instr_list sp state (i :: instrs) state'' + | exec_RBnil: + forall state sp, + step_instr_list sp state nil state. + Inductive step_instr_block (sp : val) : instr_state -> bb -> instr_state -> Prop := | exec_instr_block_cons: forall state i state' state'' instrs, - step_instr_list ge sp state i state' -> + step_instr_list sp state i state' -> step_instr_block sp state' instrs state'' -> step_instr_block sp state (i :: instrs) state'' | exec_instr_block_nil: diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 4fdd308..7acf6d2 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -16,7 +16,7 @@ * along with this program. If not, see . *) -Require compcert.backend.Registers. +Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Globalenvs. Require compcert.common.Memory. @@ -449,19 +449,34 @@ Lemma tri1: Reg x <> Reg y -> x <> y. Proof. crush. Qed. +Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Prop := + (forall sp op vl, Op.eval_operation ge sp op vl = + Op.eval_operation tge sp op vl) + /\ (forall sp addr vl, Op.eval_addressing ge sp addr vl = + Op.eval_addressing tge sp addr vl). + +Lemma ge_preserved_same: + forall A B ge, @ge_preserved A B A B ge ge. +Proof. unfold ge_preserved; auto. Qed. +Hint Resolve ge_preserved_same : rtlpar. + +Definition reg_lessdef (rs rs': regset) := forall x, rs !! x = rs' !! x. + +Lemma regs_lessdef_regs: + forall rs1 rs2, reg_lessdef rs1 rs2 -> + forall rl, rs1##rl = rs2##rl. +Proof. induction rl; crush. Qed. + Inductive sem_state_ld : sem_state -> sem_state -> Prop := | sem_state_ld_intro: forall rs rs' m m', - (forall x, rs !! x = rs' !! x) -> + reg_lessdef rs rs' -> m = m' -> sem_state_ld (mk_sem_state rs m) (mk_sem_state rs' m'). Lemma sems_det: forall A ge tge sp st f, - (forall sp op vl, Op.eval_operation ge sp op vl = - Op.eval_operation tge sp op vl) -> - (forall sp addr vl, Op.eval_addressing ge sp addr vl = - Op.eval_addressing tge sp addr vl) -> + ge_preserved ge tge -> forall v v' mv mv', (sem_value A ge sp st f v /\ sem_value A tge sp st f v' -> v = v') /\ (sem_mem A ge sp st f mv /\ sem_mem A tge sp st f mv' -> mv = mv'). @@ -469,19 +484,17 @@ Proof. Admitted. Lemma sem_value_det: forall A ge tge sp st f v v', - (forall sp op vl, Op.eval_operation ge sp op vl = - Op.eval_operation tge sp op vl) -> - (forall sp addr vl, Op.eval_addressing ge sp addr vl = - Op.eval_addressing tge sp addr vl) -> + ge_preserved ge tge -> sem_value A ge sp st f v -> sem_value A tge sp st f v' -> v = v'. Proof. intros; - generalize (sems_det A ge tge sp st f H H0 v v' + generalize (sems_det A ge tge sp st f H v v' st.(sem_state_memory) st.(sem_state_memory)); crush. Qed. +Hint Resolve sem_value_det : rtlpar. Lemma sem_value_det': forall FF ge sp s f v v', @@ -489,75 +502,64 @@ Lemma sem_value_det': sem_value FF ge sp s f v' -> v = v'. Proof. - simplify; eauto using sem_value_det. + simplify; eauto with rtlpar. Qed. Lemma sem_mem_det: forall A ge tge sp st f m m', - (forall sp op vl, Op.eval_operation ge sp op vl = - Op.eval_operation tge sp op vl) -> - (forall sp addr vl, Op.eval_addressing ge sp addr vl = - Op.eval_addressing tge sp addr vl) -> + ge_preserved ge tge -> sem_mem A ge sp st f m -> sem_mem A tge sp st f m' -> m = m'. Proof. intros; - generalize (sems_det A ge tge sp st f H H0 sp sp m m'); + generalize (sems_det A ge tge sp st f H sp sp m m'); crush. Qed. +Hint Resolve sem_mem_det : rtlpar. Lemma sem_mem_det': forall FF ge sp s f m m', - sem_mem FF ge sp s f m -> - sem_mem FF ge sp s f m' -> - m = m'. + sem_mem FF ge sp s f m -> + sem_mem FF ge sp s f m' -> + m = m'. Proof. - simplify; eauto using sem_mem_det. + simplify; eauto with rtlpar. Qed. Lemma sem_regset_det: forall FF ge tge sp st f v v', - (forall sp op vl, Op.eval_operation ge sp op vl = - Op.eval_operation tge sp op vl) -> - (forall sp addr vl, Op.eval_addressing ge sp addr vl = - Op.eval_addressing tge sp addr vl) -> - sem_regset FF ge sp st f v -> - sem_regset FF tge sp st f v' -> - (forall x, v !! x = v' !! x). + ge_preserved ge tge -> + sem_regset FF ge sp st f v -> + sem_regset FF tge sp st f v' -> + reg_lessdef v v'. Proof. - intros. - inversion H1; subst. inversion H2; subst. - generalize (H3 x); intro. generalize (H4 x); intro. - eapply sem_value_det; eauto. + intros; unfold reg_lessdef; + inv H0; inv H1; + eauto with rtlpar. Qed. - -Hint Resolve sem_value_det : rtlpar. -Hint Resolve sem_mem_det : rtlpar. Hint Resolve sem_regset_det : rtlpar. Lemma sem_det: forall FF ge tge sp st f st' st'', - (forall sp op vl, Op.eval_operation ge sp op vl = - Op.eval_operation tge sp op vl) -> - (forall sp addr vl, Op.eval_addressing ge sp addr vl = - Op.eval_addressing tge sp addr vl) -> - sem FF ge sp st f st' -> - sem FF tge sp st f st'' -> - sem_state_ld st' st''. + ge_preserved ge tge -> + sem FF ge sp st f st' -> + sem FF tge sp st f st'' -> + sem_state_ld st' st''. Proof. intros. destruct st; destruct st'; destruct st''. - inv H1; inv H2. + inv H0; inv H1. constructor; eauto with rtlpar. Qed. +Hint Resolve sem_det : rtlpar. Lemma sem_det': forall FF ge sp st f st' st'', sem FF ge sp st f st' -> sem FF ge sp st f st'' -> sem_state_ld st' st''. -Proof. eauto using sem_det. Qed. +Proof. eauto with rtlpar. Qed. (*| Update functions. @@ -660,9 +662,11 @@ Abstract computations Lemma abstract_execution_correct: forall bb bb' cfi ge tge sp rs m rs' m', - schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true -> - @step_instr_list RTLBlock.fundef ge sp (InstrState rs m) bb (InstrState rs' m') -> - step_instr_block tge sp (InstrState rs m) bb' (InstrState rs' m'). + ge_preserved ge tge -> + schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true -> + RTLBlock.step_instr_list ge sp (InstrState rs m) bb (InstrState rs' m') -> + exists rs'', RTLPar.step_instr_block tge sp (InstrState rs m) bb' (InstrState rs'' m') + /\ reg_lessdef rs' rs''. Proof. Admitted. (*| diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 157d734..01d4542 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -16,6 +16,7 @@ * along with this program. If not, see . *) +Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Errors. Require Import compcert.common.Linking. @@ -33,24 +34,26 @@ Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) := Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := | match_stackframe: - forall f tf res sp pc rs, + forall f tf res sp pc rs rs', transl_function f = OK tf -> + reg_lessdef rs rs' -> match_stackframes (Stackframe res f sp pc rs) - (Stackframe res tf sp pc rs). + (Stackframe res tf sp pc rs'). Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := | match_state: - forall sf f sp pc rs mem sf' tf + forall sf f sp pc rs rs' mem sf' tf (TRANSL: transl_function f = OK tf) - (STACKS: list_forall2 match_stackframes sf sf'), + (STACKS: list_forall2 match_stackframes sf sf') + (REG: reg_lessdef rs rs'), match_states (State sf f sp pc rs mem) - (State sf' tf sp pc rs mem) + (State sf' tf sp pc rs' mem) | match_returnstate: forall stack stack' v mem (STACKS: list_forall2 match_stackframes stack stack'), match_states (Returnstate stack v mem) (Returnstate stack' v mem) -| match_initial_call: +| match_callstate: forall stack stack' f tf args m (TRANSL: transl_fundef f = OK tf) (STACKS: list_forall2 match_stackframes stack stack'), @@ -67,14 +70,15 @@ Section CORRECTNESS. Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. - Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed. + Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed. + Hint Resolve symbols_preserved : rtlgp. Lemma function_ptr_translated: forall (b: Values.block) (f: RTLBlock.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. - Proof. + Proof using TRANSL. intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. @@ -84,7 +88,7 @@ Section CORRECTNESS. Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. - Proof. + Proof using TRANSL. intros. exploit (Genv.find_funct_match TRANSL); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. @@ -92,24 +96,27 @@ Section CORRECTNESS. Lemma senv_preserved: Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). Proof (Genv.senv_transf_partial TRANSL). + Hint Resolve senv_preserved : rtlgp. Lemma sig_transl_function: forall (f: RTLBlock.fundef) (tf: RTLPar.fundef), transl_fundef f = OK tf -> funsig tf = funsig f. - Proof. + Proof using . unfold transl_fundef, transf_partial_fundef, transl_function; intros; repeat destruct_match; crush; match goal with H: OK _ = OK _ |- _ => inv H end; auto. Qed. + Hint Resolve sig_transl_function : rtlgp. Lemma find_function_translated: - forall ros rs f, + forall ros rs rs' f, + reg_lessdef rs rs' -> find_function ge ros rs = Some f -> - exists tf, find_function tge ros rs = Some tf + exists tf, find_function tge ros rs' = Some tf /\ transl_fundef f = OK tf. - Proof. - destruct ros; simplify; + Proof using TRANSL. + unfold reg_lessdef; destruct ros; simplify; try rewrite <- H; [ exploit functions_translated; eauto | rewrite symbols_preserved; destruct_match; try (apply function_ptr_translated); crush ]. @@ -119,7 +126,7 @@ Section CORRECTNESS. forall bb cfi, schedule_oracle {| bb_body := nil; bb_exit := cfi |} bb = true -> bb_body bb = nil /\ bb_exit bb = cfi. - Proof. + Proof using . unfold schedule_oracle, check_control_flow_instr. simplify; repeat destruct_match; crush. Qed. @@ -128,17 +135,74 @@ Section CORRECTNESS. forall cfi, schedule_oracle {| bb_body := nil; bb_exit := cfi |} {| bb_body := nil; bb_exit := cfi |} = true. - Proof. + Proof using . unfold schedule_oracle, check_control_flow_instr. simplify; repeat destruct_match; crush. Qed. - Lemma schedule_sem_correct: - forall bb bb' cfi sp rs m rs' m', - schedule_oracle {| bb_body := bb; bb_exit := cfi |} {| bb_body := bb'; bb_exit := cfi |} = true -> - step_instr_list ge sp (InstrState rs m) bb (InstrState rs' m') -> - step_instr_block tge sp (InstrState rs m) bb' (InstrState rs' m'). - Proof. Admitted. + Lemma eval_op_eq: + forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val), + Op.eval_operation ge sp0 op vl = Op.eval_operation tge sp0 op vl. + 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. + Hint Resolve eval_op_eq : rtlgp. + + 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. + Hint Resolve eval_addressing_eq : rtlgp. + + Ltac semantics_simpl := + match goal with + | [ H: match_states _ _ |- _ ] => + let H2 := fresh "H" in + learn H as H2; inv H2 + | [ H: transl_function ?f = OK _ |- _ ] => + let H2 := fresh "TRANSL" in + learn H as H2; + unfold transl_function in H2; + destruct (check_scheduled_trees (@fn_code RTLBlock.bb f) (@fn_code RTLPar.bb (schedule f))) eqn:?; + [| discriminate ]; inv H2 + | [ H: context[check_scheduled_trees] |- _ ] => + let H2 := fresh "CHECK" in + learn H as H2; + eapply check_scheduled_trees_correct in H2; [| solve [eauto] ] + | [ H: schedule_oracle {| bb_body := nil; bb_exit := _ |} ?bb = true |- _ ] => + let H2 := fresh "SCHED" in + learn H as H2; + apply schedule_oracle_nil in H2 + | [ H: find_function _ _ _ = Some _ |- _ ] => + learn H; exploit find_function_translated; eauto; inversion 1 + | [ H: exists _, _ |- _ ] => inv H + | _ => progress simplify + end. + + Hint Resolve Events.eval_builtin_args_preserved : rtlgp. + Hint Resolve Events.external_call_symbols_preserved : rtlgp. + + Lemma step_cf_instr_correct: + forall cfi t s s', + step_cf_instr ge s cfi t s' -> + forall r, + match_states s r -> + exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'. + Proof using TRANSL. + induction 1; repeat semantics_simpl. + + { repeat econstructor. eauto with rtlgp. } + repeat econstructor; eauto with rtlgp. + Qed. Theorem transl_step_correct : forall (S1 : RTLBlock.state) t S2, @@ -147,32 +211,20 @@ Section CORRECTNESS. match_states S1 R1 -> exists R2, Smallstep.plus RTLPar.step tge R1 t R2 /\ match_states S2 R2. Proof. - Ltac t := - match goal with - | [ H: context[match_states _ _] |- _ ] => inv H - | [ H: transl_function ?f = OK _ |- _ ] => - let H2 := fresh "TRANSL" in - learn H as H2; - unfold transl_function in H2; - destruct (check_scheduled_trees (fn_code f) (fn_code (schedule f))) eqn:?; - [| discriminate ]; inv H2 - | [ H: context[check_scheduled_trees] |- _ ] => - let H2 := fresh "CHECK" in - learn H as H2; - eapply check_scheduled_trees_correct in H2; [| solve [eauto] ] - | [ H: schedule_oracle {| bb_body := nil; bb_exit := _ |} ?bb = true |- _ ] => - let H2 := fresh "SCHED" in - learn H as H2; - apply schedule_oracle_nil in H2 - | [ H: exists _, _ |- _ ] => inv H - | _ => progress simplify - end. - - induction 1; repeat t. - - admit. - { unfold bind in *. destruct_match; try discriminate. repeat t. inv TRANSL0. + + induction 1; repeat semantics_simpl. + + { destruct bb as [bbc bbe]; destruct x as [bbc' bbe']. + assert (bbe = bbe') by admit. + rewrite H3 in H5. + eapply abstract_execution_correct in H5; eauto with rtlgp. + repeat econstructor; eauto with rtlgp. simplify. + exploit step_cf_instr_correct. eauto. + } step_instr_block ?tge@{bbe:=bbe'; bbe':=bbe'} sp (InstrState rs m) bbc' (InstrState x m') + H5 : reg_lessdef rs' x + RTLBlock.step_instr_list ge sp (InstrState rs m) bbc (InstrState rs' m') + { unfold bind in *. destruct_match; try discriminate. repeat semantics_simpl. inv TRANSL0. repeat econstructor; eauto. } { inv TRANSL0. repeat econstructor; eauto using Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. } - { inv STACKS. inv H1. repeat econstructor; eauto. } + { inv STACKS. inv H2. repeat econstructor; eauto. } Qed. -- cgit