diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-02-09 14:55:48 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-02-09 14:55:48 +0000 |
commit | 2ae43be7b9d4118335c9d2cef6e098f9b9f807fe (patch) | |
tree | bbb5e49ccbf7e3614966571acc317f8d318fecad /backend/Linearize.v | |
download | compcert-2ae43be7b9d4118335c9d2cef6e098f9b9f807fe.tar.gz compcert-2ae43be7b9d4118335c9d2cef6e098f9b9f807fe.zip |
Initial import of compcert
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Linearize.v')
-rw-r--r-- | backend/Linearize.v | 212 |
1 files changed, 212 insertions, 0 deletions
diff --git a/backend/Linearize.v b/backend/Linearize.v new file mode 100644 index 00000000..af70b0fd --- /dev/null +++ b/backend/Linearize.v @@ -0,0 +1,212 @@ +(** Linearization of the control-flow graph: + translation from LTL to Linear *) + +Require Import Coqlib. +Require Import Maps. +Require Import Sets. +Require Import AST. +Require Import Values. +Require Import Globalenvs. +Require Import Op. +Require Import Locations. +Require Import LTL. +Require Import Linear. +Require Import Kildall. +Require Import Lattice. + +(** To translate from LTL to Linear, we must layout the basic blocks + of the LTL control-flow graph in some linear order, and insert + explicit branches and conditional branches to make sure that + each basic block jumps to its successors as prescribed by the + LTL control-flow graph. However, branches are not necessary + if the fall-through behaviour of Linear instructions already + implements the desired flow of control. For instance, + consider the two LTL basic blocks +<< + L1: Bop op args res (Bgoto L2) + L2: ... +>> + If the blocks [L1] and [L2] are laid out consecutively in the Linear + code, we can generate the following Linear code: +<< + L1: Lop op args res + L2: ... +>> + However, if this is not possible, an explicit [Lgoto] is needed: +<< + L1: Lop op args res + Lgoto L2 + ... + L2: ... +>> + The main challenge in code linearization is therefore to pick a + ``good'' order for the basic blocks that exploits well the + fall-through behavior. Many clever trace picking heuristics + have been developed for this purpose. + + In this file, we present linearization in a way that clearly + separates the heuristic part (choosing an order for the basic blocks) + from the actual code transformation parts. We proceed in three passes: +- Choosing an order for the basic blocks. This returns an enumeration + of CFG nodes stating that the basic blocks must be laid out in + the order shown in the list. +- Generate naive Linear code where each basic block branches explicitly + to its successors, even if one of these successors is the next basic + block. +- Simplify the naive Linear code, removing unconditional branches to + a label that immediately follows: +<< + ... ... + Igoto L1; becomes L1: ... + L1: ... +>> + The beauty of this approach is that correct code is generated + under surprisingly weak hypotheses on the enumeration of + CFG nodes: it suffices that every reachable basic block occurs + exactly once in the enumeration. While the enumeration heuristic we use + is quite trivial, it is easy to implement more sophisticated + trace picking heuristics: as long as they satisfy the property above, + we do not need to re-do the proof of semantic preservation. + The enumeration could even be performed by external, untrusted + Caml code, then verified (for the property above) by certified Coq code. +*) + +(** * Determination of the order of basic blocks *) + +(** We first compute a mapping from CFG nodes to booleans, + indicating whether a CFG basic block is reachable or not. + This computation is a trivial forward dataflow analysis + where the transfer function is the identity: the successors + of a reachable block are reachable, by the very + definition of reachability. *) + +Module DS := Dataflow_Solver(LBoolean). + +Definition reachable_aux (f: LTL.function) : option (PMap.t bool) := + DS.fixpoint + (successors f) + (Psucc f.(fn_entrypoint)) + (fun pc r => r) + ((f.(fn_entrypoint), true) :: nil). + +Definition reachable (f: LTL.function) : PMap.t bool := + match reachable_aux f with + | None => PMap.init true + | Some rs => rs + end. + +(** We then enumerate the nodes of reachable basic blocks. The heuristic + we take is trivial: nodes are enumerated in decreasing numerical + order. Remember that CFG nodes are positive integers, and that + the [RTLgen] pass allocated fresh nodes 1, 2, 3, ..., but generated + instructions in roughly reverse control-flow order: often, + a basic block at label [n] has [n-1] as its only successor. + Therefore, by enumerating reachable nodes in decreasing order, + we recover a reasonable layout of basic blocks that globally respects + the structure of the original Cminor code. *) + +Definition enumerate (f: LTL.function) : list node := + let reach := reachable f in + positive_rec (list node) nil + (fun pc nodes => if reach!!pc then pc :: nodes else nodes) + (Psucc f.(fn_entrypoint)). + +(** * Translation from LTL to Linear *) + +(** We now flatten the structure of the CFG graph, laying out + basic blocks consecutively in the order computed by [enumerate], + and inserting a branch at the end of every basic block. + + For blocks ending in a conditional branch [Bcond cond args s1 s2], + we have two possible translations: +<< + Lcond cond args s1; or Lcond (not cond) args s2; + Lgoto s2 Lgoto s1 +>> + We favour the first translation if [s2] is the label of the + next instruction, and the second if [s1] is the label of the + next instruction, thus exhibiting more opportunities for + fall-through optimization later. *) + +Fixpoint starts_with (lbl: label) (k: code) {struct k} : bool := + match k with + | Llabel lbl' :: k' => if peq lbl lbl' then true else starts_with lbl k' + | _ => false + end. + +Fixpoint linearize_block (b: block) (k: code) {struct b} : code := + match b with + | Bgetstack s r b => + Lgetstack s r :: linearize_block b k + | Bsetstack r s b => + Lsetstack r s :: linearize_block b k + | Bop op args res b => + Lop op args res :: linearize_block b k + | Bload chunk addr args dst b => + Lload chunk addr args dst :: linearize_block b k + | Bstore chunk addr args src b => + Lstore chunk addr args src :: linearize_block b k + | Bcall sig ros b => + Lcall sig ros :: linearize_block b k + | Bgoto s => + Lgoto s :: k + | Bcond cond args s1 s2 => + if starts_with s1 k then + Lcond (negate_condition cond) args s2 :: Lgoto s1 :: k + else + Lcond cond args s1 :: Lgoto s2 :: k + | Breturn => + Lreturn :: k + end. + +(* Linearize a function body according to an enumeration of its + nodes. *) + +Fixpoint linearize_body (f: LTL.function) (enum: list node) + {struct enum} : code := + match enum with + | nil => nil + | pc :: rem => + match f.(LTL.fn_code)!pc with + | None => linearize_body f rem + | Some b => Llabel pc :: linearize_block b (linearize_body f rem) + end + end. + +Definition linearize_function (f: LTL.function) : Linear.function := + mkfunction + (LTL.fn_sig f) + (LTL.fn_stacksize f) + (linearize_body f (enumerate f)). + +(** * Cleanup of the linearized code *) + +(** We now eliminate [Lgoto] instructions that branch to an + immediately following label: these are redundant, as the fall-through + behaviour obtained by removing the [Lgoto] instruction is + semantically equivalent. *) + +Fixpoint cleanup_code (c: code) {struct c} : code := + match c with + | nil => nil + | Lgoto lbl :: c' => + if starts_with lbl c' + then cleanup_code c' + else Lgoto lbl :: cleanup_code c' + | i :: c' => + i :: cleanup_code c' + end. + +Definition cleanup_function (f: Linear.function) : Linear.function := + mkfunction + (fn_sig f) + (fn_stacksize f) + (cleanup_code f.(fn_code)). + +(** * Entry points for code linearization *) + +Definition transf_function (f: LTL.function) : Linear.function := + cleanup_function (linearize_function f). + +Definition transf_program (p: LTL.program) : Linear.program := + transform_program transf_function p. |