From f91e562a66ebbcac7fab5871ab6189e79653757c Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Aug 2012 06:28:28 +0000 Subject: Updated documentation git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1989 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Tunneling.v | 47 +++++++++++++++++++---------------------------- 1 file changed, 19 insertions(+), 28 deletions(-) (limited to 'backend/Tunneling.v') diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 6646f11..8dd1fe2 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -27,10 +27,10 @@ Require Import LTL. so that they jump directly to the end of the branch sequence. For example: << - L1: goto L2; L1: goto L3; - L2; goto L3; becomes L2: goto L3; - L3: instr; L3: instr; - L4: if (cond) goto L1; L4: if (cond) goto L3; + L1: nop L2; L1: nop L3; + L2; nop L3; becomes L2: nop L3; + L3: instr; L3: instr; + L4: if (cond) goto L1; L4: if (cond) goto L3; >> This optimization can be applied to several of our intermediate languages. We choose to perform it on the [LTL] language, @@ -39,41 +39,32 @@ Require Import LTL. computations or useless moves), therefore there are more opportunities for tunneling after allocation than before. Symmetrically, prior tunneling helps linearization to produce - better code, e.g. by revealing that some [goto] instructions are - dead code (as the "goto L3" in the example above). + better code, e.g. by revealing that some [nop] instructions are + dead code (as the "nop L3" in the example above). *) -(** [branch_target f pc] returns the node of the CFG that is at - the end of the branch sequence starting at [pc]. If the instruction - at [pc] is not a [goto], [pc] itself is returned. - The naive definition of [branch_target] is: +(** The naive implementation of branch tunneling would replace + any branch to a node [pc] by a branch to the node + [branch_target f pc], defined as follows: << - branch_target f pc = branch_target f pc' if f(pc) = goto pc' + branch_target f pc = branch_target f pc' if f(pc) = nop pc' = pc otherwise >> However, this definition can fail to terminate if the program can contain loops consisting only of branches, as in << - L1: goto L1; + L1: nop L1; >> or -<< L1: goto L2; - L2: goto L1; +<< L1: nop L2; + L2: nop L1; >> Coq warns us of this fact by not accepting the definition of [branch_target] above. - The proper way to handle this problem is to detect [goto] cycles - in the control-flow graph. For simplicity, we just bound arbitrarily - the number of iterations performed by [branch_target], - never chasing more than 10 [goto] instructions. (This many - consecutive branches is rarely, if even, encountered.) - - For a sequence of more than 10 [goto] instructions, we can return - (as branch target) any of the labels of the [goto] instructions. - This is semantically correct in any case. However, the proof - is simpler if we return the label of the first [goto] in the sequence. -*) + To handle this problem, we proceed in two passes. The first pass + populates a union-find data structure, adding equalities [pc = pc'] + for every instruction [pc: nop pc'] in the function. *) Module U := UnionFind.UF(PTree). @@ -86,9 +77,9 @@ Definition record_goto (uf: U.t) (pc: node) (i: instruction) : U.t := Definition record_gotos (f: LTL.function) : U.t := PTree.fold record_goto f.(fn_code) U.empty. -(** The tunneling optimization simply rewrites all LTL basic blocks, - replacing the destinations of the [Bgoto] and [Bcond] instructions - with their final target, as computed by [branch_target]. *) +(** The second pass rewrites all LTL instructions, replacing every + successor [s] of every instruction by the canonical representative + of its equivalence class in the union-find data structure. *) Definition tunnel_instr (uf: U.t) (b: instruction) : instruction := match b with -- cgit v1.2.3