diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-28 14:28:56 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-28 14:28:56 +0200 |
commit | 25595a7b34b70011dcb77aae277ee1cdb8920c60 (patch) | |
tree | 6b8269b22eca57b51986593f8646f652d8598e09 /scheduling/BTLtoRTLproof.v | |
parent | 8752cea89f862d92d49183fe10d1918588143ab1 (diff) | |
download | compcert-kvx-25595a7b34b70011dcb77aae277ee1cdb8920c60.tar.gz compcert-kvx-25595a7b34b70011dcb77aae277ee1cdb8920c60.zip |
splitting BTL by introducing BTLmatchRTL
reduce also copy-paste between BTLtoRTLproof and RTLtoBTLproof
sharing is done in BTLmatchRTL
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
-rw-r--r-- | scheduling/BTLtoRTLproof.v | 42 |
1 files changed, 5 insertions, 37 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 46f360c5..765f9cad 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -1,31 +1,12 @@ Require Import Coqlib Maps. Require Import AST Integers Values Events Memory Globalenvs Smallstep. -Require Import RTL Op Registers OptionMonad BTL. +Require Import RTL Op Registers OptionMonad. Require Import Errors Linking BTLtoRTL. Require Import Linking. -Record match_function dupmap f f': Prop := { - dupmap_correct: match_cfg dupmap (fn_code f) (RTL.fn_code f'); - dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f'); - preserv_fnsig: fn_sig f = RTL.fn_sig f'; - preserv_fnparams: fn_params f = RTL.fn_params f'; - preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f' -}. - -Inductive match_fundef: fundef -> RTL.fundef -> Prop := - | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f') - | match_External ef: match_fundef (External ef) (External ef). - -Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop := - | match_stackframe_intro - dupmap res f sp pc rs f' pc' - (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc = Some pc') - : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). - -Inductive match_states: state -> RTL.state -> Prop := +Inductive match_states: BTL.state -> RTL.state -> Prop := | match_states_intro dupmap st f sp pc rs m st' f' pc' (STACKS: list_forall2 match_stackframes st st') @@ -43,26 +24,13 @@ Inductive match_states: state -> RTL.state -> Prop := : match_states (Returnstate st v m) (RTL.Returnstate st' v m) . -Lemma verify_function_correct dupmap f f' tt: - verify_function dupmap f f' = OK tt -> - fn_sig f = RTL.fn_sig f' -> - fn_params f = RTL.fn_params f' -> - fn_stacksize f = RTL.fn_stacksize f' -> - match_function dupmap f f'. -Proof. - unfold verify_function; intro VERIF. monadInv VERIF. - constructor; eauto. - - eapply verify_cfg_correct; eauto. - - eapply verify_is_copy_correct; eauto. -Qed. - Lemma transf_function_correct f f': transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. -Proof. Admitted. (* +Proof. unfold transf_function; unfold bind. repeat autodestruct. intros H _ _ X. inversion X; subst; clear X. eexists; eapply verify_function_correct; simpl; eauto. - Qed.*) +Qed. Lemma transf_fundef_correct f f': transf_fundef f = OK f' -> match_fundef f f'. @@ -402,7 +370,7 @@ Proof. Qed. Theorem transf_program_correct_cfg: - forward_simulation (BTL.cfgsem prog) (RTL.semantics tprog). + forward_simulation (BTLmatchRTL.cfgsem prog) (RTL.semantics tprog). Proof. eapply forward_simulation_plus with match_states. - eapply senv_preserved. |