From 245f4f86865ce62b82242af81897936b5034438a Mon Sep 17 00:00:00 2001 From: Pierre Goutagny Date: Thu, 3 Jun 2021 17:13:49 +0200 Subject: Write RTLTunneling.v --- backend/RTLTunneling.v | 125 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 125 insertions(+) (limited to 'backend') diff --git a/backend/RTLTunneling.v b/backend/RTLTunneling.v index e69de29b..4885002f 100644 --- a/backend/RTLTunneling.v +++ b/backend/RTLTunneling.v @@ -0,0 +1,125 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* TODO: Proper author information *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** 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. + +(* This is a port of tunneling for LTL. See Tunneling.v *) + +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. +(* 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` *) + | 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`} *) + | Some (tpc, dpc) => + let dpc := Z.abs dpc in + match i with + | Inop s => + let (ts,ds) := get td s in + if peq tpc ts then + if zlt ds dpc then OK tt + else Error (msg "bad distance in Inop") + else Error (msg "invalid skip of Inop") + | Icond _ _ ifso ifnot _ => + let (tso,dso) := get td ifso in + let (tnot,dnot) := get td ifnot in + if peq tpc ifso then + if peq tpc ifnot then + if zlt dso dpc then + if zlt dnot dpc then OK tt + else Error (msg "bad distance on else branch") + else Error (msg "bad distance on then branch") + else Error (msg "invalid skip of else branch") + else Error (msg "invalid skip of then branch") + | _ => Error (msg "cannot skip this instruction") + end + end. + +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) + | Iop op args res s => Iop op args res (t s) + | Iload trap chunk addr args dst s => Iload trap chunk addr args dst (t s) + | Istore chunk addr args src s => Istore chunk addr args src (t s) + | Icall sig ros args res s => Icall sig ros args res (t s) + | Ibuiltin ef args res s => Ibuiltin ef args res (t s) + | Icond cond args ifso ifnot info => + 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) + | _ => i + end. + +Definition tunnel_function (f: RTL.function): res RTL.function := + let td := branch_target f in + 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` *) + (fn_sig f) + (fn_params f) + (fn_stacksize f) + (PTree.map1 (tunnel_instr td) c) (* rq: `map1` est un map sans le pointeur *) + (td (fn_entrypoint f))) + else Error (msg "Some node of the union-find is not in the CFG"). + +Definition tunnel_fundef (f: fundef): res fundef := + transf_partial_fundef tunnel_function f. + +Definition transf_program (p: program): res program := + transform_partial_program tunnel_fundef p. + -- cgit