From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Linearize.v | 75 ++++++++++++++++++++++++++++------------------------- 1 file changed, 40 insertions(+), 35 deletions(-) (limited to 'backend/Linearize.v') diff --git a/backend/Linearize.v b/backend/Linearize.v index 6fc8e489..388f459d 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -10,8 +10,7 @@ (* *) (* *********************************************************************) -(** Linearization of the control-flow graph: - translation from LTL to LTLin *) +(** Linearization of the control-flow graph: translation from LTL to Linear *) Require Import Coqlib. Require Import Maps. @@ -23,26 +22,26 @@ Require Import Errors. Require Import Op. Require Import Locations. Require Import LTL. -Require Import LTLin. +Require Import Linear. Require Import Kildall. Require Import Lattice. Open Scope error_monad_scope. -(** To translate from LTL to LTLin, we must lay out the nodes +(** To translate from LTL to Linear, we must lay out the nodes of the LTL control-flow graph in some linear order, and insert explicit branches and conditional branches to make sure that each node jumps to its successors as prescribed by the LTL control-flow graph. However, branches are not necessary if the fall-through behaviour of LTLin instructions already implements the desired flow of control. For instance, - consider the two LTL instructions + consider the two LTL blocks << - L1: Lop op args res L2 + L1: Lop op args res; Lbranch L2 L2: ... >> If the instructions [L1] and [L2] are laid out consecutively in the LTLin - code, we can generate the following LTLin code: + code, we can generate the following Linear code: << L1: Lop op args res L2: ... @@ -65,7 +64,7 @@ Open Scope error_monad_scope. - Choosing an order for the nodes. This returns an enumeration of CFG nodes stating that they must be laid out in the order shown in the list. -- Generate LTLin code where each node branches explicitly to its +- Generate Linear code where each node branches explicitly to its successors, except if one of these successors is the immediately following instruction. @@ -102,7 +101,7 @@ Definition reachable (f: LTL.function) : PMap.t bool := | Some rs => rs end. -(** We then enumerate the nodes of reachable instructions. +(** We then enumerate the nodes of reachable blocks. This task is performed by external, untrusted Caml code. *) Parameter enumerate_aux: LTL.function -> PMap.t bool -> list node. @@ -126,7 +125,7 @@ Fixpoint nodeset_of_list (l: list node) (s: Nodeset.t) Definition check_reachable_aux (reach: PMap.t bool) (s: Nodeset.t) - (ok: bool) (pc: node) (i: LTL.instruction) : bool := + (ok: bool) (pc: node) (bb: LTL.bblock) : bool := if reach!!pc then ok && Nodeset.mem pc s else ok. Definition check_reachable @@ -141,10 +140,10 @@ Definition enumerate (f: LTL.function) : res (list node) := then OK enum else Error (msg "Linearize: wrong enumeration"). -(** * Translation from LTL to LTLin *) +(** * Translation from LTL to Linear *) (** We now flatten the structure of the CFG graph, laying out - LTL instructions consecutively in the order computed by [enumerate], + LTL blocks consecutively in the order computed by [enumerate], and inserting branches to the labels of sucessors if necessary. Whether to insert a branch or not is determined by the [starts_with] function below. @@ -169,31 +168,38 @@ Fixpoint starts_with (lbl: label) (k: code) {struct k} : bool := Definition add_branch (s: label) (k: code) : code := if starts_with s k then k else Lgoto s :: k. -Definition linearize_instr (b: LTL.instruction) (k: code) : code := +Fixpoint linearize_block (b: LTL.bblock) (k: code) : code := match b with - | LTL.Lnop s => + | nil => k + | LTL.Lop op args res :: b' => + Lop op args res :: linearize_block b' k + | LTL.Lload chunk addr args dst :: b' => + Lload chunk addr args dst :: linearize_block b' k + | LTL.Lgetstack sl ofs ty dst :: b' => + Lgetstack sl ofs ty dst :: linearize_block b' k + | LTL.Lsetstack src sl ofs ty :: b' => + Lsetstack src sl ofs ty :: linearize_block b' k + | LTL.Lstore chunk addr args src :: b' => + Lstore chunk addr args src :: linearize_block b' k + | LTL.Lcall sig ros :: b' => + Lcall sig ros :: linearize_block b' k + | LTL.Ltailcall sig ros :: b' => + Ltailcall sig ros :: k + | LTL.Lbuiltin ef args res :: b' => + Lbuiltin ef args res :: linearize_block b' k + | LTL.Lannot ef args :: b' => + Lannot ef args :: linearize_block b' k + | LTL.Lbranch s :: b' => add_branch s k - | LTL.Lop op args res s => - Lop op args res :: add_branch s k - | LTL.Lload chunk addr args dst s => - Lload chunk addr args dst :: add_branch s k - | LTL.Lstore chunk addr args src s => - Lstore chunk addr args src :: add_branch s k - | LTL.Lcall sig ros args res s => - Lcall sig ros args res :: add_branch s k - | LTL.Ltailcall sig ros args => - Ltailcall sig ros args :: k - | LTL.Lbuiltin ef args res s => - Lbuiltin ef args res :: add_branch s k - | LTL.Lcond cond args s1 s2 => + | LTL.Lcond cond args s1 s2 :: b' => if starts_with s1 k then Lcond (negate_condition cond) args s2 :: add_branch s1 k else Lcond cond args s1 :: add_branch s2 k - | LTL.Ljumptable arg tbl => + | LTL.Ljumptable arg tbl :: b' => Ljumptable arg tbl :: k - | LTL.Lreturn or => - Lreturn or :: k + | LTL.Lreturn :: b' => + Lreturn :: k end. (** Linearize a function body according to an enumeration of its nodes. *) @@ -201,7 +207,7 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code := Definition linearize_node (f: LTL.function) (pc: node) (k: code) : code := match f.(LTL.fn_code)!pc with | None => k - | Some b => Llabel pc :: linearize_instr b k + | Some b => Llabel pc :: linearize_block b k end. Definition linearize_body (f: LTL.function) (enum: list node) : code := @@ -209,16 +215,15 @@ Definition linearize_body (f: LTL.function) (enum: list node) : code := (** * Entry points for code linearization *) -Definition transf_function (f: LTL.function) : res LTLin.function := +Definition transf_function (f: LTL.function) : res Linear.function := do enum <- enumerate f; OK (mkfunction (LTL.fn_sig f) - (LTL.fn_params f) (LTL.fn_stacksize f) (add_branch (LTL.fn_entrypoint f) (linearize_body f enum))). -Definition transf_fundef (f: LTL.fundef) : res LTLin.fundef := +Definition transf_fundef (f: LTL.fundef) : res Linear.fundef := AST.transf_partial_fundef transf_function f. -Definition transf_program (p: LTL.program) : res LTLin.program := +Definition transf_program (p: LTL.program) : res Linear.program := transform_partial_program transf_fundef p. -- cgit