Merge of the reuse-temps branch:

- Reload temporaries are marked as destroyed (set to Vundef) across
  operations in the semantics of LTL, LTLin, Linear and Mach, 
  allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 40 insertions, 0 deletions

diff --git a/ia32/Machregsaux.ml b/ia32/Machregsaux.ml
new file mode 100644
index 0000000..7d6df90
--- /dev/null
+++ b/ia32/Machregsaux.ml
@@ -0,0 +1,40 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 = [
+  ("AX", AX); ("BX", BX); ("SI", SI); ("DI", DI); ("BP", BP);
+  ("XMM0", X0); ("XMM1", X1); ("XMM2", X2); ("XMM3", X3);
+  ("XMM4", X4); ("XMM5", X5);
+  ("DX", IT1); ("CX", IT2);
+  ("XMM6", FT1); ("XMM7", FT2); ("ST0", FP0)
+]
+
+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 Conventions1.int_callee_save_regs
+  || List.mem r Conventions1.float_callee_save_regs
+