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/XTL.ml | 213 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 213 insertions(+) create mode 100644 backend/XTL.ml (limited to 'backend/XTL.ml') diff --git a/backend/XTL.ml b/backend/XTL.ml new file mode 100644 index 0000000..93cab36 --- /dev/null +++ b/backend/XTL.ml @@ -0,0 +1,213 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** The XTL intermediate language for register allocation *) + +open Datatypes +open Camlcoq +open Maps +open AST +open Registers +open Op +open Locations + +type var = V of reg * typ | L of loc + +type node = P.t + +type instruction = + | Xmove of var * var + | Xreload of var * var + | Xspill of var * var + | Xparmove of var list * var list * var * var + | Xop of operation * var list * var + | Xload of memory_chunk * addressing * var list * var + | Xstore of memory_chunk * addressing * var list * var + | Xcall of signature * (var, ident) sum * var list * var list + | Xtailcall of signature * (var, ident) sum * var list + | Xbuiltin of external_function * var list * var list + | Xbranch of node + | Xcond of condition * var list * node * node + | Xjumptable of var * node list + | Xreturn of var list + +type block = instruction list + (* terminated by one of Xbranch, Xcond, Xjumptable, Xtailcall or Xreturn *) + +type code = block PTree.t + (* mapping node -> block *) + +type xfunction = { + fn_sig: signature; + fn_stacksize: Z.t; + fn_code: code; + fn_entrypoint: node +} + +(* Type of a variable *) + +let typeof = function V(_, ty) -> ty | L l -> Loc.coq_type l + +(* Constructors for type [var] *) + +let vloc l = L l +let vlocs ll = List.map vloc ll +let vmreg mr = L(R mr) +let vmregs mrl = List.map vmreg mrl + +(* Sets of variables *) + +module VSet = Set.Make(struct type t = var let compare = compare end) + +(*** Generation of fresh registers and fresh register variables *) + +let next_temp = ref P.one + +let twin_table : (int32, P.t) Hashtbl.t = Hashtbl.create 27 + +let reset_temps () = + next_temp := P.one; Hashtbl.clear twin_table + +let new_reg() = + let r = !next_temp in next_temp := P.succ !next_temp; r + +let new_temp ty = V (new_reg(), ty) + +let twin_reg r = + let r = P.to_int32 r in + try + Hashtbl.find twin_table r + with Not_found -> + let t = new_reg() in Hashtbl.add twin_table r t; t + +(*** Successors (for dataflow analysis) *) + +let rec successors_block = function + | Xbranch s :: _ -> [s] + | Xtailcall(sg, vos, args) :: _ -> [] + | Xcond(cond, args, s1, s2) :: _ -> [s1; s2] + | Xjumptable(arg, tbl) :: _ -> tbl + | Xreturn _:: _ -> [] + | instr :: blk -> successors_block blk + | [] -> assert false + +let successors fn = + PTree.map1 successors_block fn.fn_code + +(**** Type checking for XTL *) + +exception Type_error + +exception Type_error_at of node + +let set_var_type v ty = + if typeof v <> ty then raise Type_error + +let rec set_vars_type vl tyl = + match vl, tyl with + | [], [] -> () + | v1 :: vl, ty1 :: tyl -> set_var_type v1 ty1; set_vars_type vl tyl + | _, _ -> raise Type_error + +let unify_var_type v1 v2 = + if typeof v1 <> typeof v2 then raise Type_error + +let type_instr = function + | Xmove(src, dst) | Xspill(src, dst) | Xreload(src, dst) -> + unify_var_type src dst + | Xparmove(srcs, dsts, itmp, ftmp) -> + List.iter2 unify_var_type srcs dsts; + set_var_type itmp Tint; + set_var_type ftmp Tfloat + | Xop(op, args, res) -> + let (targs, tres) = type_of_operation op in + set_vars_type args targs; + set_var_type res tres + | Xload(chunk, addr, args, dst) -> + set_vars_type args (type_of_addressing addr); + set_var_type dst (type_of_chunk chunk) + | Xstore(chunk, addr, args, src) -> + set_vars_type args (type_of_addressing addr); + set_var_type src (type_of_chunk chunk) + | Xcall(sg, Coq_inl v, args, res) -> + set_var_type v Tint + | Xcall(sg, Coq_inr id, args, res) -> + () + | Xtailcall(sg, Coq_inl v, args) -> + set_var_type v Tint + | Xtailcall(sg, Coq_inr id, args) -> + () + | Xbuiltin(ef, args, res) -> + let sg = ef_sig ef in + set_vars_type args sg.sig_args; + set_vars_type res (Events.proj_sig_res' sg) + | Xbranch s -> + () + | Xcond(cond, args, s1, s2) -> + set_vars_type args (type_of_condition cond) + | Xjumptable(arg, tbl) -> + set_var_type arg Tint + | Xreturn args -> + () + +let type_block blk = + List.iter type_instr blk + +let type_function f = + PTree.fold + (fun () pc blk -> + try + type_block blk + with Type_error -> + raise (Type_error_at pc)) + f.fn_code () + +(*** A generic framework for transforming extended basic blocks *) + +(* Determine instructions that start an extended basic block. + These are instructions that have >= 2 predecessors. *) + +let basic_blocks_map f = (* return mapping pc -> number of predecessors *) + let add_successor map s = + PMap.set s (1 + PMap.get s map) map in + let add_successors_block map pc blk = + List.fold_left add_successor map (successors_block blk) in + PTree.fold add_successors_block f.fn_code + (PMap.set f.fn_entrypoint 2 (PMap.init 0)) + +let transform_basic_blocks + (transf: node -> block -> 'state -> block * 'state) + (top: 'state) + f = + let bbmap = basic_blocks_map f in + let rec transform_block st newcode pc bb = + assert (PTree.get pc newcode = None); + let (bb', st') = transf pc bb st in + (* Record new code after transformation *) + let newcode' = PTree.set pc bb' newcode in + (* Propagate outgoing state to all successors *) + List.fold_left (transform_successor st') newcode' (successors_block bb) + and transform_successor st newcode pc = + if PMap.get pc bbmap <> 1 then newcode else begin + match PTree.get pc f.fn_code with + | None -> newcode + | Some bb -> transform_block st newcode pc bb + end in + (* Iterate over all extended basic block heads *) + let newcode = + PTree.fold + (fun newcode pc bb -> + if PMap.get pc bbmap >= 2 + then transform_block top newcode pc bb + else newcode) + f.fn_code PTree.empty + in {f with fn_code = newcode} -- cgit v1.2.3