From 74901c6df6ceb92da58ef5db2592fc05561dce01 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 24 Aug 2021 11:35:58 +0200 Subject: RTLTunneling: fix comments and authors information --- backend/LTLTunnelingaux.ml | 1 + backend/RTLTunneling.v | 23 +++++-------- backend/RTLTunnelingaux.ml | 2 +- backend/RTLTunnelingproof.v | 83 ++++++--------------------------------------- backend/Tunnelinglibs.ml | 4 +-- 5 files changed, 24 insertions(+), 89 deletions(-) (limited to 'backend') diff --git a/backend/LTLTunnelingaux.ml b/backend/LTLTunnelingaux.ml index c3b8cf82..66540bc1 100644 --- a/backend/LTLTunnelingaux.ml +++ b/backend/LTLTunnelingaux.ml @@ -3,6 +3,7 @@ (* The Compcert verified compiler *) (* *) (* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Pierre Goutagny ENS-Lyon, VERIMAG *) (* *) (* Copyright VERIMAG. All rights reserved. *) (* This file is distributed under the terms of the INRIA *) diff --git a/backend/RTLTunneling.v b/backend/RTLTunneling.v index df663f48..878e079f 100644 --- a/backend/RTLTunneling.v +++ b/backend/RTLTunneling.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 *) @@ -13,8 +14,6 @@ (** Branch tunneling for the RTL representation *) -(* rq: ce code est commenté avec des remarques sur des éléments du code pas évidents, sur lequels j'ai buté, ou qui changent du tunneling LTL. Ils pourront être enlevés ultérieurement *) - Require Import Coqlib Maps Errors. Require Import AST. Require Import RTL. @@ -26,32 +25,30 @@ Definition UF := PTree.t (node * Z). (* The oracle returns a map of "nop" node to their target with a distance (ie the number of the "nop" node on the path) to the target. *) Axiom branch_target: RTL.function -> UF. Extract Constant branch_target => "RTLTunnelingaux.branch_target". -(* TODO: add an extraction command to link branch_target with its implementation *) Local Open Scope error_monad_scope. Definition get (td: UF) (pc: node): node*Z := - match td!pc with (* rq: notation pour `PTree.get pc td` *) + match td!pc with | Some (t,d) => (t,Z.abs d) | None => (pc,0) end. -(* rq: "coerce" la structure d'abre UF en une fonction qui retrouve le représentant canonique de la classe d'un noeud *) + Definition target (td: UF) (pc: node): node := fst (get td pc). Coercion target: UF >-> Funclass. (* we check that the domain of [td] is included in the domain of [c] *) -(* rq: pas de basic block en RTL *) + Definition check_included (td: UF) (c: code): option instruction := PTree.fold (fun (ok:option instruction) pc _ => if ok then c!pc else None) td (Some (Inop xH)). -(* rq: PTree.fold replie l'arbre avec un parcours préfixe. La fonction qui prend en argument l'accumulateur, le label du noeud et le pointeur (`positive`) vers ce noeud *) (* we check the validity of targets and their bound: * the distance of a "nop" node (w.r.t to the target) must be greater than the one of its parents. *) Definition check_instr (td: UF) (pc: node) (i: instruction): res unit := match td!pc with - | None => OK tt (* rq: le type `unit` est le singleton {`tt`} *) + | None => OK tt | Some (tpc, dpc) => let dpc := Z.abs dpc in match i with @@ -78,14 +75,12 @@ Definition check_instr (td: UF) (pc: node) (i: instruction): res unit := Definition check_code (td: UF) (c: code): res unit := PTree.fold (fun ok pc i => do _ <- ok; check_instr td pc i) c (OK tt). -(* rq: `do _ <- ok; ...` exécute le bloc à droite du ';' si `ok` est un `OK _`, sinon il passe simplement l'erreur *) (* The second pass rewrites all LTL instructions, replacing every * successor [s] of every instruction by [t s], the canonical representative * of its equivalence class in the union-find data structure. *) -(* rq: beaucoup plus de cas que pour LTL, car plein d'instructions ont des successeurs *) Definition tunnel_instr (t: node -> node) (i: instruction) : instruction := match i with | Inop s => Inop (t s) @@ -98,7 +93,7 @@ Definition tunnel_instr (t: node -> node) (i: instruction) : instruction := let ifso' := t ifso in let ifnot' := t ifnot in if peq ifso' ifnot' - (* rq: si les deux branches se rejoignent, le if ne sert à rien *) + then Inop ifso' else Icond cond args ifso' ifnot' info | Ijumptable arg tbl => Ijumptable arg (List.map t tbl) @@ -110,11 +105,11 @@ Definition tunnel_function (f: RTL.function): res RTL.function := let c := fn_code f in if check_included td c then do _ <- check_code td c ; OK - (mkfunction (* rq: mkfunction construit un "Record" `RTL.function` *) + (mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) - (PTree.map1 (tunnel_instr td) c) (* rq: `map1` est un map sans le pointeur *) + (PTree.map1 (tunnel_instr td) c) (td (fn_entrypoint f))) else Error (msg "Some node of the union-find is not in the CFG"). diff --git a/backend/RTLTunnelingaux.ml b/backend/RTLTunnelingaux.ml index 9333e357..43d4bf9f 100644 --- a/backend/RTLTunnelingaux.ml +++ b/backend/RTLTunnelingaux.ml @@ -3,7 +3,7 @@ (* The Compcert verified compiler *) (* *) (* Sylvain Boulmé Grenoble-INP, VERIMAG *) -(* TODO: Proper author information *) +(* Pierre Goutagny ENS-Lyon, VERIMAG *) (* *) (* Copyright VERIMAG. All rights reserved. *) (* This file is distributed under the terms of the INRIA *) 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'), diff --git a/backend/Tunnelinglibs.ml b/backend/Tunnelinglibs.ml index 7c826ba4..010595be 100644 --- a/backend/Tunnelinglibs.ml +++ b/backend/Tunnelinglibs.ml @@ -3,7 +3,7 @@ (* The Compcert verified compiler *) (* *) (* Sylvain Boulmé Grenoble-INP, VERIMAG *) -(* TODO: Proper author information *) +(* Pierre Goutagny ENS-Lyon, VERIMAG *) (* *) (* Copyright VERIMAG. All rights reserved. *) (* This file is distributed under the terms of the INRIA *) @@ -16,7 +16,7 @@ This file implements the core functions of the tunneling passes, for both RTL and LTL, by using a simplified CFG as a transparent interface -See [LTLTunneling.v] and [RTLTunneling.v] +See [LTLTunneling.v]/[LTLTunnelingaux.ml] and [RTLTunneling.v]/[RTLTunnelingaux.ml]. *) -- cgit