diff options
Diffstat (limited to 'backend/RTLTunnelingproof.v')
| -rw-r--r-- | backend/RTLTunnelingproof.v | 83 |
1 files changed, 11 insertions, 72 deletions
diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index 51ef0f7a..0861143b 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -3,7 +3,8 @@ (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* TODO: Proper author information *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Pierre Goutagny ENS-Lyon, VERIMAG *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -23,7 +24,7 @@ Require Import Conventions1. Local Open Scope nat. -(**) Definition check_included_spec (c:code) (td:UF) (ok: option instruction) := +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): @@ -37,7 +38,7 @@ Proof. + contradiction. Qed. -(**) Inductive target_bounds (target: node -> node) (bound: node -> nat) (pc: node) : option instruction -> Prop := +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 @@ -65,7 +66,7 @@ Proof. Qed. Local Hint Resolve get_nonneg: core. -(**) Definition bound (td: UF) (pc: node) := Z.to_nat (snd (get td pc)). +Definition bound (td: UF) (pc: node) := Z.to_nat (snd (get td pc)). (* TODO: à réécrire proprement *) @@ -117,18 +118,6 @@ Theorem branch_target_bounds: 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. @@ -144,12 +133,8 @@ Qed. Definition match_prog (p tp: program) := match_program (fun _ f tf => tunnel_fundef f = OK tf) eq p tp. - (* rq: `(fun _ ...)` est la fonction pour matcher des fonctions - * `eq` la fonction pour matcher les variables ? (`varinfo` dans la def) - * `p` et `tp` sont les programmes donc on doit dire s'ils match - *) - (**) Lemma transf_program_match: +Lemma transf_program_match: forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. Proof. intros. eapply match_transform_partial_program_contextual; eauto. @@ -160,12 +145,10 @@ Section PRESERVATION. Variables prog tprog: program. -Hypothesis TRANSL: match_prog prog tprog. (* rq: on suppose que les programmes match *) +Hypothesis TRANSL: match_prog prog tprog. 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 -> @@ -174,12 +157,7 @@ Proof. intros. exploit (Genv.find_funct_match TRANSL). apply H. intros (cu & tf & A & B & C). - (* 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: @@ -196,25 +174,13 @@ Qed. Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. 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. - - - (* - unfold bind in H. - destruct (tunnel_function _) as [x|] eqn:EQ; try congruence. - inversion H. - unfold tunnel_function in EQ. - 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... *) + - monadInv H. unfold tunnel_function in EQ. destruct (check_included _ _) in EQ; try congruence. monadInv EQ. auto. @@ -227,7 +193,6 @@ 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 *) Qed. -(* TODO: vérifier s'il faut faire quelque chose avec le `res` ? *) Inductive match_stackframes: stackframe -> stackframe -> Prop := | match_stackframes_intro: forall res f tf sp pc rs trs @@ -237,7 +202,6 @@ Inductive match_stackframes: stackframe -> stackframe -> Prop := (Stackframe res f sp pc rs) (Stackframe res tf sp (branch_target f pc) trs). -(* rq: `match_states s1 s2` correspond à s1 ~ s2 *) Inductive match_states: state -> state -> Prop := | match_states_intro: forall s ts f tf sp pc rs trs m tm @@ -266,24 +230,6 @@ 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 _ => (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 @@ -292,9 +238,7 @@ Definition measure (st: state): nat := 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. @@ -316,15 +260,13 @@ 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 -> final_state s1 r -> final_state s2 r. Proof. - (* 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. @@ -366,8 +308,7 @@ Proof. intro TB. inversion TB as [BT|s|cond args ifso ifnot info]; try (rewrite FATPC in H; congruence). Qed. -(* rq: utilisée pour `tunnel_step_correct` mais je ne comprends pas tout *) -(**) Lemma find_function_translated: +Lemma find_function_translated: forall ros rs trs fd, regs_lessdef rs trs -> find_function ge ros rs = Some fd -> @@ -484,8 +425,6 @@ Proof. intros args ta H. induction H. apply Val.lessdef_list_nil. apply Val.lessdef_list_cons. apply H. apply IHlist_forall2. 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'), |