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/IRC.mli | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 backend/IRC.mli (limited to 'backend/IRC.mli') diff --git a/backend/IRC.mli b/backend/IRC.mli new file mode 100644 index 00000000..e81b6dc5 --- /dev/null +++ b/backend/IRC.mli @@ -0,0 +1,44 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Iterated Register Coalescing: George and Appel's graph coloring algorithm *) + +open AST +open Registers +open Machregs +open Locations +open XTL + +(* The abstract type of interference and preference graphs. *) +type graph + +(* Information associated to every variable. *) +type var_stats = { + mutable cost: int; (* estimated cost of a spill *) + mutable usedefs: int (* number of uses and defs *) +} + +(* Create an empty graph. The given function associates statistics to + every variable. *) +val init: (reg -> var_stats) -> graph + +(* Add an interference between two variables. *) +val add_interf: graph -> var -> var -> unit + +(* Add a preference between two variables. *) +val add_pref: graph -> var -> var -> unit + +(* Color the graph. Return an assignment of locations to variables. *) +val coloring: graph -> (var -> loc) + +(* Machine registers that are reserved and not available for allocation. *) +val reserved_registers: mreg list ref -- cgit