From b1b7c49cb70486cb68f9e30da7f770ae7efd932a Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 1 May 2010 14:32:32 +0000 Subject: ARM version of Machregsaux git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1327 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Machregsaux.ml | 42 ++++++++++++++++++++++++++++++++++++++++++ arm/Machregsaux.mli | 17 +++++++++++++++++ 2 files changed, 59 insertions(+) create mode 100644 arm/Machregsaux.ml create mode 100644 arm/Machregsaux.mli diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml new file mode 100644 index 00000000..a06adf11 --- /dev/null +++ b/arm/Machregsaux.ml @@ -0,0 +1,42 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Auxiliary functions on machine registers *) + +open Machregs + +let register_names = [ + ("R0", R0); ("R1", R1); ("R2", R2); ("R3", R3); + ("R4", R4); ("R5", R5); ("R6", R6); ("R7", R7); + ("R8", R8); ("R9", R9); ("R11", R11); + ("F0", F0); ("F1", F1); + ("F4", F4); ("F5", F5); ("F6", F6); ("F7", F7); + ("R10", IT1); ("R12", IT2); + ("F2", FT1); ("F3", FT2) +] + +let name_of_register r = + let rec rev_assoc = function + | [] -> None + | (a, b) :: rem -> if b = r then Some a else rev_assoc rem + in rev_assoc register_names + +let register_by_name s = + try + Some(List.assoc (String.uppercase s) register_names) + with Not_found -> + None + +let can_reserve_register r = + List.mem r Conventions.int_callee_save_regs + || List.mem r Conventions.float_callee_save_regs + diff --git a/arm/Machregsaux.mli b/arm/Machregsaux.mli new file mode 100644 index 00000000..400c5abb --- /dev/null +++ b/arm/Machregsaux.mli @@ -0,0 +1,17 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Auxiliary functions on machine registers *) + +val register_by_name: string -> Machregs.mreg option +val can_reserve_register: Machregs.mreg -> bool +val name_of_register: Machregs.mreg -> string option -- cgit