diff options
Diffstat (limited to 'backend/RTLTunneling.v')
| -rw-r--r-- | backend/RTLTunneling.v | 23 |
1 files changed, 9 insertions, 14 deletions
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"). |