diff options
Diffstat (limited to 'backend/Tunneling.v')
| -rw-r--r-- | backend/Tunneling.v | 138 |
1 files changed, 100 insertions, 38 deletions
diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 78458582..269ebb6f 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -3,6 +3,7 @@ (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -12,7 +13,7 @@ (** Branch tunneling (optimization of branches to branches). *) -Require Import Coqlib Maps UnionFind. +Require Import Coqlib Maps Errors. Require Import AST. Require Import LTL. @@ -21,10 +22,10 @@ Require Import LTL. so that they jump directly to the end of the branch sequence. For example: << - L1: nop L2; L1: nop L3; - L2; nop L3; becomes L2: nop L3; + L1: if (cond) 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; + L4: if (cond) goto L1; L4: if (cond) nop L1; >> This optimization can be applied to several of our intermediate languages. We choose to perform it on the [LTL] language, @@ -37,11 +38,14 @@ Require Import LTL. dead code (as the "nop L3" in the example above). *) -(** 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: +(** The implementation consists in two passes: the first pass + records the branch t of each "nop" + and the second pass replace any "nop" node to [pc] + by a branch to a "nop" at [branch_t f pc] + +Naively, we may define [branch_t f pc] as follows: << - branch_target f pc = branch_target f pc' if f(pc) = nop pc' + branch_t f pc = branch_t f pc' if f(pc) = nop pc' = pc otherwise >> However, this definition can fail to terminate if @@ -50,56 +54,114 @@ Require Import LTL. L1: nop L1; >> or -<< L1: nop L2; +<< + L1: nop L2; L2: nop L1; >> Coq warns us of this fact by not accepting the definition - of [branch_target] above. + of [branch_t] above. + + To handle this problem, we use a union-find data structure, adding equalities [pc = pc'] + for every instruction [pc: nop pc'] in the function. + + Moreover, because the elimination of "useless" [Lcond] depends on the current [uf] datastructure, + we need to iterate until we reach a fixpoint. + + Actually, it is simpler and more efficient to perform this in an external oracle, that also returns a measure + in order to help the proof. + + A verifier checks that this data-structure is correct. +*) + +Definition UF := PTree.t (node * Z). - 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. *) +(* 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: LTL.function -> UF. +Extract Constant branch_target => "Tunnelingaux.branch_target". -Module U := UnionFind.UF(PTree). +Local Open Scope error_monad_scope. -Definition record_goto (uf: U.t) (pc: node) (b: bblock) : U.t := - match b with - | Lbranch s :: _ => U.union uf pc s - | _ => uf +Definition get (td: UF) pc:node*Z := + match td!pc with + | Some (t,d) => (t,Z.abs d) + | _ => (pc,0) end. -Definition record_gotos (f: LTL.function) : U.t := - PTree.fold record_goto f.(fn_code) U.empty. +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] *) +Definition check_included (td: UF) (c: code): option bblock + := PTree.fold (fun (ok:option bblock) pc _ => if ok then c!pc else None) td (Some nil). + +(* 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_bblock (td: UF) (pc:node) (bb: bblock): res unit + := match td!pc with + | None => OK tt + | Some (tpc, dpc) => + let dpc := Z.abs dpc in + match bb with + | Lbranch 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 Lbranch") + else Error (msg "invalid skip of Lbranch") + | Lcond _ _ s1 s2 _ :: _ => + let (ts1, ds1) := get td s1 in + let (ts2, ds2) := get td s2 in + if peq tpc ts1 then + if peq tpc ts2 then + if zlt ds1 dpc then + if zlt ds2 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 block") + end + end. + +Definition check_code (td: UF) (c:code): res unit + := PTree.fold (fun ok pc bb => do _ <- ok; check_bblock td pc bb) c (OK tt). (** The second pass rewrites all LTL instructions, replacing every - successor [s] of every instruction by the canonical representative + successor [s] of every instruction by [t s], the canonical representative of its equivalence class in the union-find data structure. *) -Definition tunnel_instr (uf: U.t) (i: instruction) : instruction := +Definition tunnel_instr (t: node -> node) (i: instruction) : instruction := match i with - | Lbranch s => Lbranch (U.repr uf s) + | Lbranch s => Lbranch (t s) | Lcond cond args s1 s2 info => - let s1' := U.repr uf s1 in let s2' := U.repr uf s2 in + let s1' := t s1 in let s2' := t s2 in if peq s1' s2' then Lbranch s1' else Lcond cond args s1' s2' info - | Ljumptable arg tbl => Ljumptable arg (List.map (U.repr uf) tbl) + | Ljumptable arg tbl => Ljumptable arg (List.map t tbl) | _ => i end. -Definition tunnel_block (uf: U.t) (b: bblock) : bblock := - List.map (tunnel_instr uf) b. +Definition tunnel_block (t: node -> node) (b: bblock) : bblock := + List.map (tunnel_instr t) b. -Definition tunnel_function (f: LTL.function) : LTL.function := - let uf := record_gotos f in - mkfunction - (fn_sig f) - (fn_stacksize f) - (PTree.map1 (tunnel_block uf) (fn_code f)) - (U.repr uf (fn_entrypoint f)). +Definition tunnel_function (f: LTL.function) : res LTL.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 + (fn_sig f) + (fn_stacksize f) + (PTree.map1 (tunnel_block td) c) + (td (fn_entrypoint f))) + else + Error (msg "Some node of the union-find is not in the CFG") + . -Definition tunnel_fundef (f: LTL.fundef) : LTL.fundef := - transf_fundef tunnel_function f. +Definition tunnel_fundef (f: fundef) : res fundef := + transf_partial_fundef tunnel_function f. -Definition transf_program (p: LTL.program) : LTL.program := - transform_program tunnel_fundef p. +Definition transf_program (p: program) : res program := + transform_partial_program tunnel_fundef p. |