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/Splitting.ml | 184 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 184 insertions(+) create mode 100644 backend/Splitting.ml (limited to 'backend/Splitting.ml') diff --git a/backend/Splitting.ml b/backend/Splitting.ml new file mode 100644 index 00000000..60f6818b --- /dev/null +++ b/backend/Splitting.ml @@ -0,0 +1,184 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Live range splitting over RTL *) + +open Camlcoq +open Datatypes +open Coqlib +open Maps +open AST +open Kildall +open Registers +open RTL + +(* We represent live ranges by the following unification variables. + Live range inference manipulates only variable live ranges. + Code rewriting assigns fresh RTL registers to live ranges. *) + +type live_range = { source: reg; mutable kind: live_range_kind } + +and live_range_kind = + | Link of live_range + | Var + | Reg of reg + +let new_range r = { source = r; kind = Var } + +let rec repr lr = + match lr.kind with + | Link lr' -> let lr'' = repr lr' in lr.kind <- Link lr''; lr'' + | _ -> lr + +let same_range lr1 lr2 = + lr1 == lr2 || (* quick test for speed *) + repr lr1 == repr lr2 (* the real test *) + +let unify lr1 lr2 = + let lr1 = repr lr1 and lr2 = repr lr2 in + if lr1 != lr2 then begin + match lr1.kind, lr2.kind with + | Var, _ -> lr1.kind <- Link lr2 + | _, Var -> lr2.kind <- Link lr1 + | _, _ -> assert false + end + +let reg_for lr = + let lr = repr lr in + match lr.kind with + | Link _ -> assert false + | Reg r -> r + | Var -> let r = XTL.new_reg() in lr.kind <- Reg r; r + +(* Live range inference is a variant on liveness analysis. + At each PC and for each register, liveness analysis determines + whether the reg is live or not. Live range inference associates + a live range to the reg if it is live, and no live range if it + is dead. *) + +module LRMap = struct + + type t = live_range PTree.t (* live register -> live range *) + + let beq m1 m2 = PTree.beq same_range m1 m2 + + let bot : t = PTree.empty + + let lub_opt_range olr1 olr2 = + match olr1, olr2 with + | Some lr1, Some lr2 -> unify lr1 lr2; olr1 + | Some _, None -> olr1 + | None, _ -> olr2 + + let lub m1 m2 = + PTree.combine lub_opt_range m1 m2 + +end + +module Solver = Backward_Dataflow_Solver(LRMap)(NodeSetBackward) + +(* A cache of live ranges associated to (pc, used reg) pairs. *) + +let live_range_cache = + (Hashtbl.create 123 : (int32 * int32, live_range) Hashtbl.t) + +let live_range_for pc r = + let pc' = P.to_int32 pc + and r' = P.to_int32 r in + try + Hashtbl.find live_range_cache (pc',r') + with Not_found -> + let lr = new_range r in + Hashtbl.add live_range_cache (pc', r') lr; + lr + +(* The transfer function *) + +let reg_live pc r map = + match PTree.get r map with + | Some lr -> map (* already live *) + | None -> PTree.set r (live_range_for pc r) map (* becomes live *) + +let reg_list_live pc rl map = List.fold_right (reg_live pc) rl map + +let reg_dead r map = + PTree.remove r map + +let transfer f pc after = + match PTree.get pc f.fn_code with + | None -> + LRMap.bot + | Some i -> + let across = + match instr_defs i with + | None -> after + | Some r -> reg_dead r after in + reg_list_live pc (instr_uses i) across + +(* The live range analysis *) + +let analysis f = Solver.fixpoint (successors f) (transfer f) [] + +(* Produce renamed registers for each instruction. *) + +let ren_reg map r = + match PTree.get r map with + | Some lr -> reg_for lr + | None -> XTL.new_reg() + +let ren_regs map rl = + List.map (ren_reg map) rl + +let ren_ros map ros = + sum_left_map (ren_reg map) ros + +(* Rename in an instruction *) + +let ren_instr f maps pc i = + let after = PMap.get pc maps in + let before = transfer f pc after in + match i with + | Inop s -> Inop s + | Iop(op, args, res, s) -> + Iop(op, ren_regs before args, ren_reg after res, s) + | Iload(chunk, addr, args, dst, s) -> + Iload(chunk, addr, ren_regs before args, ren_reg after dst, s) + | Istore(chunk, addr, args, src, s) -> + Istore(chunk, addr, ren_regs before args, ren_reg before src, s) + | Icall(sg, ros, args, res, s) -> + Icall(sg, ren_ros before ros, ren_regs before args, ren_reg after res, s) + | Itailcall(sg, ros, args) -> + Itailcall(sg, ren_ros before ros, ren_regs before args) + | Ibuiltin(ef, args, res, s) -> + Ibuiltin(ef, ren_regs before args, ren_reg after res, s) + | Icond(cond, args, s1, s2) -> + Icond(cond, ren_regs before args, s1, s2) + | Ijumptable(arg, tbl) -> + Ijumptable(ren_reg before arg, tbl) + | Ireturn optarg -> + Ireturn(option_map (ren_reg before) optarg) + +(* Rename live ranges in a function *) + +let rename_function f = + Hashtbl.clear live_range_cache; + let maps = + match analysis f with + | None -> assert false + | Some maps -> maps in + let before_entrypoint = + transfer f f.fn_entrypoint (PMap.get f.fn_entrypoint maps) in + { fn_sig = f.fn_sig; + fn_params = ren_regs before_entrypoint f.fn_params; + fn_stacksize = f.fn_stacksize; + fn_code = PTree.map (ren_instr f maps) f.fn_code; + fn_entrypoint = f.fn_entrypoint } -- cgit