From 403f2dd49dfc6948df31e08f60655de3091816d6 Mon Sep 17 00:00:00 2001 From: Pierre Goutagny Date: Mon, 7 Jun 2021 21:41:36 +0200 Subject: Monday's work on RTLTunnelingproof --- backend/RTLTunnelingproof.v | 184 ++++++++++++++++++++++++++++++++++++-------- 1 file changed, 153 insertions(+), 31 deletions(-) (limited to 'backend') diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index 57f14b9f..f63c3b35 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -23,6 +23,77 @@ Require Import Conventions1. Local Open Scope nat. +(**) Definition check_included_spec (c:code) (td:UF) (ok: option instruction) := + ok <> None -> forall pc, c!pc = None -> td!pc = None. + +Lemma check_included_correct (td:UF) (c:code): + check_included_spec c td (check_included td c). +Proof. + apply PTree_Properties.fold_rec with (P:=check_included_spec c); unfold check_included_spec. + - intros m m' oi EQ IND N pc. rewrite <- EQ. apply IND. apply N. + - intros N pc. rewrite PTree.gempty. auto. + - intros m oi pc v N S IND. destruct oi. + + intros. rewrite PTree.gsspec. destruct (peq _ _); try congruence. apply IND. congruence. apply H0. + + contradiction. +Qed. + +(**) Inductive target_bounds (target: node -> node) (bound: node -> nat) (pc: node) : option instruction -> Prop := + | 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)) + | 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)). + +Lemma target_None (td: UF) (pc: node): td!pc = None -> td pc = pc. +Proof. + unfold target, get. intro EQ. rewrite EQ. auto. +Qed. + +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. + +(**) Definition bound (td: UF) (pc: node) := Z.to_nat (snd (get td pc)). + + +(* TODO: à réécrire proprement *) +Lemma check_instr_correct (td: UF) (pc: node) (i: instruction): + check_instr td pc i = OK tt -> + target_bounds (target td) (bound td) pc (Some i). +Proof. + unfold check_instr. destruct (td!pc) as [(tpc,dpc)|] eqn:EQ. + assert (DPC: snd (get td pc) = Z.abs dpc). { unfold get. rewrite EQ. auto. } + - destruct i; try congruence. + + destruct (get td n) as (ts,ds) eqn:EQs. + destruct (peq _ _); try congruence. + destruct (zlt _ _); try congruence. intros _. + apply TB_nop. replace (td pc) with tpc. + unfold target. rewrite EQs. auto. + unfold target. unfold get. rewrite EQ. auto. + unfold bound. rewrite DPC. rewrite EQs; simpl. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n ts. apply EQs. + + destruct (get td n) as (tso,dso) eqn:EQSO. + destruct (get td n0) as (tnot,dnot) eqn:EQNOT. + intro H. + repeat ((destruct (peq _ _) in H || destruct (zlt _ _) in H); try congruence). + apply TB_cond; subst. + * unfold target. replace (fst (get td pc)) with tnot. rewrite EQSO. auto. + unfold get. rewrite EQ. auto. + * unfold target. replace (fst (get td pc)) with tnot. rewrite EQNOT. auto. + unfold get. rewrite EQ. auto. + * unfold bound. rewrite DPC. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n tnot. rewrite EQSO. auto. rewrite EQSO. auto. + * unfold bound. rewrite DPC. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n0 tnot. rewrite EQNOT; auto. rewrite EQNOT; auto. + - intros _. apply TB_default. unfold target. unfold get. rewrite EQ. auto. +Qed. + + (** Preservation of semantics *) Definition match_prog (p tp: program) := @@ -32,6 +103,8 @@ Definition match_prog (p tp: program) := * `p` et `tp` sont les programmes donc on doit dire s'ils match *) + + Section PRESERVATION. @@ -41,14 +114,21 @@ Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. (* rq: pour les deux lemmes suivants, j'ai recopié les preuves, mais je ne les comprends pas du tout... D'où vient `exploit` ?? *) +(* rq: `exploit` vient de Coqlib! Mais je comprends pas encore vraiment ce qui se passe... *) Lemma functions_translated: forall (v: val) (f: fundef), Genv.find_funct ge v = Some f -> exists tf, tunnel_fundef f = OK tf /\ Genv.find_funct tge v = Some tf. Proof. - intros. exploit (Genv.find_funct_match TRANSL). eauto. + intros. + exploit (Genv.find_funct_match TRANSL). apply H. intros (cu & tf & A & B & C). - repeat eexists; intuition eauto. + (* exists tf. split. apply B. apply A. *) + (* rq: on peut remplacer les `split` et `apply` par `eauto`, et ne pas spécifier le + * `exists`, avec un `eexists` *) + eexists. eauto. + (* rq: Je ne comprends pas à quoi sert le `intuition`... *) + (* repeat eexists; intuition eauto. *) Qed. Lemma function_ptr_translated: @@ -57,30 +137,43 @@ 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_transf_partial TRANSL); eauto. + intros. exploit (Genv.find_funct_ptr_match TRANSL). + - apply H. + - intros (cu & tf & A & B & C). exists tf. split. apply A. apply B. Qed. Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. - rewrite (Genv.find_symbol_match TRANSL). auto. + apply (Genv.find_symbol_match TRANSL). + (* rq: ici pas de `exploit` mais un `apply` parce que `Genv.find_symbol_match + * prouve vraiment pile ce qu'on veut *) Qed. Lemma sig_preserved: forall f tf, tunnel_fundef f = OK tf -> funsig tf = funsig f. Proof. - intros. destruct f. - - simpl in H. monadInv H. (* rq: c'est une tactique maison... *) + intros. destruct f; simpl in H. + - + (* + unfold bind in H. + destruct (tunnel_function _) as [x|] eqn:EQ; try congruence. + inversion H. unfold tunnel_function in EQ. - destruct (check_included _ _) as [_|] in EQ; try congruence. + destruct (check_included _ _) in EQ; try congruence. + unfold bind in EQ. destruct (check_code _ _) in EQ; try congruence. inversion EQ. auto. + *) + + monadInv H. (* rq: c'est une tactique maison... *) + unfold tunnel_function in EQ. + destruct (check_included _ _) in EQ; try congruence. monadInv EQ. auto. - - simpl in H. monadInv H. auto. + - 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, je ne vais pas réinventer la roue ici *) + 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 *) Qed. (* TODO: vérifier s'il faut faire quelque chose avec le `res` ? *) @@ -122,27 +215,47 @@ Inductive match_states: state -> state -> Prop := (Returnstate s v m) (Returnstate ts tv tm). +(* TODO: il faut définir une bonne mesure *) +(**) 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 (Icond _ _ ifso ifnot _) => (max + (bound (branch_target f) ifso) + (bound (branch_target f) ifnot) + ) * 2 + 1 + | Some _ => 0 + | None => 0 + end + | 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: forall s1: state, initial_state prog s1 -> exists s2: state, initial_state tprog s2 /\ match_states s1 s2. Proof. - intros. inversion H. - exploit function_ptr_translated; eauto. - intro Htf. destruct Htf as (tf & Htf & Hf). - exists (Callstate nil tf nil m0). split. - - econstructor. - + apply (Genv.init_mem_transf_partial TRANSL). auto. - + rewrite (match_program_main TRANSL). - rewrite symbols_preserved. eauto. - + apply Htf. - + rewrite <- H3. apply sig_preserved. apply Hf. - - constructor. - + constructor. - + apply Hf. - + constructor. - + apply Mem.extends_refl. + intros. inversion H as [b f m0 ge0 MEM SYM PTR SIG CALL]. + exploit function_ptr_translated. + - apply PTR. + - 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. + * rewrite (match_program_main TRANSL). + rewrite symbols_preserved. apply SYM. + * apply TPTR. + * rewrite <- SIG. apply sig_preserved. apply TUN. + + apply match_states_call. + * apply list_forall2_nil. + * apply TUN. + * apply list_forall2_nil. + * apply Mem.extends_refl. Qed. - + Lemma transf_final_states: forall (s1 : state) (s2 : state) (r : Integers.Int.int), @@ -150,12 +263,22 @@ Lemma transf_final_states: final_state s1 r -> final_state s2 r. Proof. - intros s1 s2 r HM H1. inv H1. inv HM. inv STK. inv VAL. constructor. + (* rq: `inv` au lieu de `inversion` fait beaucoup de nettoyage dans les + * hypothèses, mais je sais pas trop ce que ça fait exactement *) + intros. inv H0. inv H. inv VAL. inversion STK. apply final_state_intro. Qed. (* `Lemma tunnel_step_correct` correspond au diagramme "option simulation" *) +Lemma tunnel_step_correct: + forall st1 t st2, step ge st1 t st2 -> + forall st1' (MS: match_states st1 st1'), + (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. + -(* Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. @@ -163,8 +286,7 @@ Proof. apply senv_preserved. apply transf_initial_states. apply transf_final_states. - apply tunnel_step_correct. + exact tunnel_step_correct. Qed. -*) End PRESERVATION. -- cgit