From 587f0505f2331b8edc94a187575a8f124c3cb4ef Mon Sep 17 00:00:00 2001 From: Pierre Goutagny Date: Wed, 9 Jun 2021 19:34:23 +0200 Subject: Starts proof for `tunnel_step_correct` --- backend/RTLTunnelingproof.v | 135 +++++++++++++++++++++++++++++++++++++++----- 1 file changed, 120 insertions(+), 15 deletions(-) (limited to 'backend') diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index f63c3b35..c54667a4 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -16,7 +16,7 @@ Require Import Coqlib Maps Errors. Require Import AST Linking. -Require Import Values Memory Events Globalenvs Smallstep. +Require Import Values Memory Registers Events Globalenvs Smallstep. Require Import Op Locations RTL. Require Import RTLTunneling. Require Import Conventions1. @@ -41,25 +41,29 @@ Qed. | TB_default (TB: target pc = pc) oi: target_bounds target bound pc oi | TB_nop s - (EQ: target pc = target s) - (DEC: bound s < bound pc): - target_bounds target bound pc (Some (Inop s)) + (EQ: target pc = target s) + (DEC: bound s < bound pc): + target_bounds target bound pc (Some (Inop s)) | TB_cond cond args ifso ifnot info (EQSO: target pc = target ifso) (EQNOT: target pc = target ifnot) (DECSO: bound ifso < bound pc) (DECNOT: bound ifnot < bound pc): - target_bounds target bound pc (Some (Icond cond args ifso ifnot info)). + target_bounds target bound pc (Some (Icond cond args ifso ifnot info)) +. +Local Hint Resolve TB_default: core. Lemma target_None (td: UF) (pc: node): td!pc = None -> td pc = pc. Proof. unfold target, get. intro EQ. rewrite EQ. auto. Qed. +Local Hint Resolve target_None Z.abs_nonneg: core. Lemma get_nonneg td pc t d: get td pc = (t,d) -> (0 <= d)%Z. Proof. unfold get. destruct td!pc as [(tpc,dpc)|]; intro H; inv H; lia. Qed. +Local Hint Resolve get_nonneg: core. (**) Definition bound (td: UF) (pc: node) := Z.to_nat (snd (get td pc)). @@ -93,6 +97,48 @@ Proof. - intros _. apply TB_default. unfold target. unfold get. rewrite EQ. auto. Qed. +Definition check_code_spec (td:UF) (c:code) (ok: res unit) := + ok = OK tt -> forall pc i, c!pc = Some i -> target_bounds (target td) (bound td) pc (Some i). + +Lemma check_code_correct (td:UF) c: + check_code_spec td c (check_code td c). +Proof. + unfold check_code. apply PTree_Properties.fold_rec; unfold check_code_spec. + - intros. rewrite <- H in H2. apply H0; auto. + - intros. rewrite PTree.gempty in H0. congruence. + - intros m [[]|e] pc i N S IND; simpl; try congruence. + intros H pc0 i0. rewrite PTree.gsspec. destruct (peq _ _). + subst. intro. inv H0. apply check_instr_correct. apply H. + auto. +Qed. + +Theorem branch_target_bounds: + forall f tf pc, + tunnel_function f = OK tf -> + target_bounds (branch_target f) (bound (branch_target f)) pc (f.(fn_code)!pc). +Proof. +(* ~old + intros t tf pc. unfold tunnel_function. + destruct (check_included _ _) eqn:HI; try congruence. + destruct (check_code _ _) eqn: HC. + - intros _. destruct ((fn_code t) ! pc) eqn:EQ. + + exploit check_code_correct; eauto. + replace tt with u. auto. {destruct u; auto. } + + exploit check_included_correct; eauto. rewrite HI. congruence. + intro. apply TB_default. unfold target. unfold get. rewrite H. debug auto. + - simpl. congruence. +*) + + intros. unfold tunnel_function in H. + destruct (check_included _ _) eqn:EQinc; try congruence. + monadInv H. rename EQ into EQcode. + destruct (_ ! _) eqn:EQ. + - exploit check_code_correct. destruct x. apply EQcode. apply EQ. auto. + - exploit check_included_correct. + rewrite EQinc. congruence. + apply EQ. + intro. apply TB_default. apply target_None. apply H. +Qed. (** Preservation of semantics *) @@ -137,7 +183,7 @@ Lemma function_ptr_translated: exists tf, Genv.find_funct_ptr tge v = Some tf /\ tunnel_fundef f = OK tf. Proof. - intros. exploit (Genv.find_funct_ptr_match TRANSL). + intros. exploit (Genv.find_funct_ptr_match TRANSL). - apply H. - intros (cu & tf & A & B & C). exists tf. split. apply A. apply B. Qed. @@ -170,7 +216,7 @@ Proof. - monadInv H. auto. Qed. -(**) Lemma senv_preserved: +Lemma senv_preserved: Senv.equiv ge tge. Proof. eapply (Genv.senv_match TRANSL). (* Il y a déjà une preuve de cette propriété très exactement, je ne vais pas réinventer la roue ici *) @@ -216,32 +262,41 @@ Inductive match_states: state -> state -> Prop := (Returnstate ts tv tm). (* TODO: il faut définir une bonne mesure *) -(**) Definition measure (st: state) : nat := +(* (**) Definition measure (st: state) : nat := match st with | State s f sp pc rs m => match (fn_code f)!pc with - | Some (Inop pc) => (bound (branch_target f) pc) * 2 + 1 + | Some (Inop pc') => (bound (branch_target f) pc') * 2 + 1 | Some (Icond _ _ ifso ifnot _) => (max (bound (branch_target f) ifso) (bound (branch_target f) ifnot) ) * 2 + 1 - | Some _ => 0 + | Some _ => (bound (branch_target f) pc) * 2 | None => 0 end | Callstate s f v m => 0 | Returnstate s v m => 0 end. +*) + +Definition measure (st: state): nat := + match st with + | State s f sp pc rs m => bound (branch_target f) pc + | Callstate s f v m => 0 + | Returnstate s v m => 0 + end. + (* rq: sans les lemmes définis au-dessus je ne vois pas trop comment j'aurais * fait... ni comment j'aurais eu l'idée d'en faire des lemmes ? *) -Lemma transf_initial_states: +(**) Lemma transf_initial_states: forall s1: state, initial_state prog s1 -> exists s2: state, initial_state tprog s2 /\ match_states s1 s2. Proof. intros. inversion H as [b f m0 ge0 MEM SYM PTR SIG CALL]. exploit function_ptr_translated. - apply PTR. - - intros (tf & TPTR & TUN). + - intros (tf & TPTR & TUN). exists (Callstate nil tf nil m0). split. + apply initial_state_intro with b. * apply (Genv.init_mem_match TRANSL). apply MEM. @@ -256,7 +311,7 @@ Proof. * apply Mem.extends_refl. Qed. -Lemma transf_final_states: +(**) Lemma transf_final_states: forall (s1 : state) (s2 : state) (r : Integers.Int.int), match_states s1 s2 -> @@ -268,6 +323,27 @@ Proof. intros. inv H0. inv H. inv VAL. inversion STK. apply final_state_intro. Qed. +Lemma tunnel_function_unfold: + forall f tf pc, + tunnel_function f = OK tf -> + (fn_code tf) ! pc = + option_map (tunnel_instr (branch_target f)) (fn_code f) ! pc. +Proof. + intros f tf pc. + unfold tunnel_function. + destruct (check_included _ _) eqn:EQinc; try congruence. + destruct (check_code _ _) eqn:EQcode; simpl; try congruence. + intro. inv H. simpl. rewrite PTree.gmap1. reflexivity. +Qed. + +Lemma reglist_lessdef: + forall (rs trs: Registers.Regmap.t val) (args: list Registers.reg), + regs_lessdef rs trs -> Val.lessdef_list (rs##args) (trs##args). +Proof. + intros. induction args; simpl; constructor. + apply H. apply IHargs. +Qed. + (* `Lemma tunnel_step_correct` correspond au diagramme "option simulation" *) Lemma tunnel_step_correct: forall st1 t st2, step ge st1 t st2 -> @@ -275,8 +351,37 @@ Lemma tunnel_step_correct: (exists st2', step tge st1' t st2' /\ match_states st2 st2') \/ (measure st2 < measure st1 /\ t = E0 /\ match_states st2 st1')%nat. Proof. - intros st1 t st2 H. induction H; intros; inv MS. -Admitted. + intros st1 t st2 H. induction H; intros; try (inv MS). + - (* Inop *) + exploit branch_target_bounds. apply TF. + rewrite H. intro. inv H0. + + (* TB_default *) + rewrite TB. left. eexists. split. + * apply exec_Inop. rewrite (tunnel_function_unfold f tf pc). rewrite H. simpl. eauto. apply TF. + * constructor; try assumption. + + (* TB_nop *) + simpl. right. repeat split. apply DEC. + rewrite EQ. apply match_states_intro; assumption. + - (* Iop *) + exploit eval_operation_lessdef; try eassumption. + apply reglist_lessdef. apply RS. + intros (tv & EVAL & LD). + left; eexists; split. + + eapply exec_Iop with (v:=tv). + assert ((fn_code tf) ! pc = Some (Iop op args res (branch_target f pc'))). + rewrite (tunnel_function_unfold f tf pc); eauto. + rewrite H. simpl. reflexivity. + (* TODO: refaire ça joliment *) + assert (target_bounds (branch_target f) (bound (branch_target f)) pc (fn_code f)! pc). + apply (branch_target_bounds) with tf. apply TF. + inv H2. rewrite TB. apply H1. rewrite H in H4. congruence. + rewrite H in H4. congruence. + rewrite <- EVAL. apply eval_operation_preserved. apply symbols_preserved. + + apply match_states_intro; eauto. apply set_reg_lessdef. apply LD. apply RS. + - (* Iload *) + + +Qed. Theorem transf_program_correct: -- cgit