Remove the PowerPC/MacOS X port, as MacOS no longer supports PowerPC.

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

4 files changed, 21 insertions, 937 deletions

diff --git a/configure b/configure
index 38f7f33..9c3d6a7 100755
--- a/configure
+++ b/configure
@@ -21,7 +21,6 @@ target=''
 usage='Usage: ./configure [options] target
 
 Supported targets:
-  ppc-macosx       (PowerPC, MacOS X)
   ppc-linux        (PowerPC, Linux)
   ppc-eabi         (PowerPC, EABI with GNU/Unix tools)
   ppc-eabi-diab    (PowerPC, EABI with Diab tools)
@@ -65,15 +64,6 @@ cchecklink=false
 has_runtime_lib=false
 
 case "$target" in
-  powerpc-macosx|ppc-macosx)
-    arch="powerpc"
-    variant="macosx"
-    system="macosx"
-    cc="${toolprefix}gcc -arch ppc"
-    cprepro="${toolprefix}gcc -arch ppc -U__GNUC__ -U__BLOCKS__ -E"
-    casm="${toolprefix}gcc -arch ppc -c"
-    clinker="${toolprefix}gcc -arch ppc"
-    libmath="";;
   powerpc-linux|ppc-linux|powerpc-eabi|ppc-eabi)
     arch="powerpc"
     variant="eabi"
@@ -194,7 +184,6 @@ cat >> Makefile.config <<'EOF'
 ARCH=
 
 # Target ABI
-# VARIANT=macosx   # for PowerPC / MacOS X
 # VARIANT=eabi     # for PowerPC / Linux and other SVR4 or EABI platforms
 # VARIANT=linux    # for ARM
 # VARIANT=standard # for IA32
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 9d23ad9..3331a1c 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -23,11 +23,10 @@ open Asm
 
 (* Recognition of target ABI and asm syntax *)
 
-type target = MacOS | Linux | Diab
+type target = Linux | Diab
 
 let target = 
   match Configuration.system with
-  | "macosx" -> MacOS
   | "linux"  -> Linux
   | "diab"   -> Diab
   | _        -> invalid_arg ("System " ^ Configuration.system ^ " not supported")
@@ -61,43 +60,28 @@ let coqint oc n =
   fprintf oc "%ld" (camlint_of_coqint n)
 
 let raw_symbol oc s =
-  match target with
-  | MacOS      -> fprintf oc "_%s" s
-  | Linux|Diab -> fprintf oc "%s" s
+  fprintf oc "%s" s
 
 let symbol oc symb =
-  match target with
-  | MacOS ->
-      if IdentSet.mem symb !stubbed_functions
-      then fprintf oc "L%s$stub" (extern_atom symb)
-      else fprintf oc "_%s" (extern_atom symb)
-  | Linux | Diab ->
-      if IdentSet.mem symb !stubbed_functions
-      then fprintf oc ".L%s$stub" (extern_atom symb)
-      else fprintf oc "%s" (extern_atom symb)
+  if IdentSet.mem symb !stubbed_functions
+  then fprintf oc ".L%s$stub" (extern_atom symb)
+  else fprintf oc "%s" (extern_atom symb)
 
 let symbol_offset oc (symb, ofs) =
   symbol oc symb;
   if ofs <> 0l then fprintf oc " + %ld" ofs
 
 let label oc lbl =
-  match target with
-  | MacOS      -> fprintf oc "L%d" lbl
-  | Linux|Diab -> fprintf oc ".L%d" lbl
+  fprintf oc ".L%d" lbl
 
 let label_low oc lbl =
-  match target with
-  | MacOS      -> fprintf oc "lo16(L%d)" lbl
-  | Linux|Diab -> fprintf oc ".L%d@l" lbl
+  fprintf oc ".L%d@l" lbl
 
 let label_high oc lbl =
-  match target with
-  | MacOS      -> fprintf oc "ha16(L%d)" lbl
-  | Linux|Diab -> fprintf oc ".L%d@ha" lbl
+  fprintf oc ".L%d@ha" lbl
 
 let comment =
   match target with
-  | MacOS -> ";"
   | Linux -> "#"
   | Diab -> ";"
 
@@ -106,23 +90,11 @@ let constant oc cst =
   | Cint n ->
       fprintf oc "%ld" (camlint_of_coqint n)
   | Csymbol_low(s, n) ->
-      begin match target with
-      | MacOS -> 
-          fprintf oc "lo16(%a)" symbol_offset (s, camlint_of_coqint n)
-      | Linux|Diab ->
-          fprintf oc "(%a)@l" symbol_offset (s, camlint_of_coqint n)
-      end
+      fprintf oc "(%a)@l" symbol_offset (s, camlint_of_coqint n)
   | Csymbol_high(s, n) ->
-      begin match target with
-      | MacOS ->
-          fprintf oc "ha16(%a)" symbol_offset (s, camlint_of_coqint n)
-      | Linux|Diab ->
-          fprintf oc "(%a)@ha" symbol_offset (s, camlint_of_coqint n)
-      end
+      fprintf oc "(%a)@ha" symbol_offset (s, camlint_of_coqint n)
   | Csymbol_sda(s, n) ->
       begin match target with
-      | MacOS ->
-          assert false
       | Linux ->
           fprintf oc "(%a)@sda21" symbol_offset (s, camlint_of_coqint n)
       | Diab ->
@@ -160,8 +132,8 @@ let float_reg_name = function
 
 let ireg oc r =
   begin match target with
-  | MacOS|Diab -> output_char oc 'r'
-  | Linux      -> ()
+  | Diab  -> output_char oc 'r'
+  | Linux -> ()
   end;
   output_string oc (int_reg_name r)
 
@@ -170,15 +142,15 @@ let ireg_or_zero oc r =
 
 let freg oc r =
   begin match target with
-  | MacOS|Diab -> output_char oc 'f'
-  | Linux      -> ()
+  | Diab  -> output_char oc 'f'
+  | Linux -> ()
   end;
   output_string oc (float_reg_name r)
 
 let creg oc r =
   match target with
-  | MacOS|Diab -> fprintf oc "cr%d" r
-  | Linux      -> fprintf oc "%d" r
+  | Diab  -> fprintf oc "cr%d" r
+  | Linux -> fprintf oc "%d" r
 
 let preg oc = function
   | IR r -> ireg oc r
@@ -187,20 +159,6 @@ let preg oc = function
 
 (* Names of sections *)
 
-let name_of_section_MacOS = function
-  | Section_text -> ".text"
-  | Section_data _ -> ".data"
-  | Section_small_data _ -> ".data"
-  | Section_const -> ".const"
-  | Section_small_const -> ".const"
-  | Section_string -> ".const"
-  | Section_literal -> ".literal8"
-  | Section_jumptable -> ".const"
-  | Section_user(s, wr, ex) ->
-       sprintf ".section	\"%s\", %s, %s"
-               (if wr then "__DATA" else "__TEXT") s
-               (if ex then "regular, pure_instructions" else "regular")
-
 let name_of_section_Linux = function
   | Section_text -> ".text"
   | Section_data i -> if i then ".data" else "COMM"
@@ -234,7 +192,6 @@ let name_of_section_Diab = function
 
 let name_of_section =
   match target with
-  | MacOS -> name_of_section_MacOS
   | Linux -> name_of_section_Linux
   | Diab  -> name_of_section_Diab
 
@@ -882,10 +839,8 @@ let print_function oc name code =
     fprintf oc "	.globl %a\n" symbol name;
   fprintf oc "%a:\n" symbol name;
   print_instructions oc (label_positions PTree.empty 0 code) 0 code;
-  if target <> MacOS then begin
-    fprintf oc "	.type	%a, @function\n" symbol name;
-    fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
-  end;
+  fprintf oc "	.type	%a, @function\n" symbol name;
+  fprintf oc "	.size	%a, . - %a\n" symbol name symbol name;
   if !float_literals <> [] then begin
     section oc lit;
     fprintf oc "	.align 3\n";
@@ -903,119 +858,8 @@ let print_function oc name code =
 
 let re_variadic_stub = Str.regexp "\\(.*\\)\\$[if]*$"
 
-(* Stubs for MacOS X *)
-
-module Stubs_MacOS = struct
-
-(* Generation of stub code for variadic functions, e.g. printf.
-   Calling conventions for variadic functions are:
-     - always reserve 8 stack words (offsets 24 to 52) so that the
-       variadic function can save there the integer registers parameters
-       r3 ... r10
-     - treat float arguments as pairs of integers, i.e. if we
-       must pass them in registers, use a pair of integer registers
-       for this purpose.
-   The code we generate is:
-     - allocate large enough stack frame
-     - save return address
-     - copy our arguments (registers and stack) to the stack frame,
-       starting at offset 24
-     - load relevant integer parameter registers r3...r10 from the
-       stack frame, limited by the actual number of arguments
-     - call the variadic thing
-     - deallocate stack frame and return
-*)
-
-let variadic_stub oc stub_name fun_name ty_args =
-  (* Compute total size of arguments *)
-  let arg_size =
-    List.fold_left
-     (fun sz ty -> match ty with Tint -> sz + 4 | Tfloat -> sz + 8)
-     0 ty_args in
-  (* Stack size is linkage area + argument size, with a minimum of 56 bytes *)
-  let frame_size = max 56 (24 + arg_size) in
-  fprintf oc "	mflr	r0\n";
-  fprintf oc "	stwu	r1, %d(r1)\n" (-frame_size);
-  fprintf oc "	stw	r0, %d(r1)\n" (frame_size + 4);
-  (* Copy our parameters to our stack frame.
-     As an optimization, don't copy parameters that are already in
-     integer registers, since these stay in place. *)
-  let rec copy gpr fpr src_ofs dst_ofs = function
-    | [] -> ()
-    | Tint :: rem ->
-        if gpr > 10 then begin
-          fprintf oc "	lwz	r0, %d(r1)\n" src_ofs;
-          fprintf oc "	stw	r0, %d(r1)\n" dst_ofs
-        end;
-        copy (gpr + 1) fpr (src_ofs + 4) (dst_ofs + 4) rem
-    | Tfloat :: rem ->
-        if fpr <= 10 then begin
-          fprintf oc "	stfd	f%d, %d(r1)\n" fpr dst_ofs
-        end else begin
-          fprintf oc "	lfd	f0, %d(r1)\n" src_ofs;
-          fprintf oc "	stfd	f0, %d(r1)\n" dst_ofs
-        end;
-        copy (gpr + 2) (fpr + 1) (src_ofs + 8) (dst_ofs + 8) rem
-  in copy 3 1 (frame_size + 24) 24 ty_args;
-  (* Load the first parameters into integer registers.
-     As an optimization, don't load parameters that are already
-     in the correct integer registers. *)
-  let rec load gpr ofs = function
-    | [] -> ()
-    | Tint :: rem ->
-        load (gpr + 1) (ofs + 4) rem
-    | Tfloat :: rem ->
-        if gpr <= 10 then
-          fprintf oc "	lwz	r%d, %d(r1)\n" gpr ofs;
-        if gpr + 1 <= 10 then
-          fprintf oc "	lwz	r%d, %d(r1)\n" (gpr + 1) (ofs + 4);
-        load (gpr + 2) (ofs + 8) rem
-  in load 3 24 ty_args;
-  (* Call the function *)
-  fprintf oc "	addis	r11, 0, ha16(L%s$ptr)\n" stub_name;
-  fprintf oc "	lwz	r11, lo16(L%s$ptr)(r11)\n" stub_name;
-  fprintf oc "	mtctr	r11\n";
-  fprintf oc "	bctrl\n";
-  (* Free our frame and return *)
-  fprintf oc "	lwz	r0, %d(r1)\n" (frame_size + 4);
-  fprintf oc "	mtlr	r0\n";
-  fprintf oc "	addi	r1, r1, %d\n" frame_size;
-  fprintf oc "	blr\n";
-  (* The function pointer *)
-  fprintf oc "	.non_lazy_symbol_pointer\n";
-  fprintf oc "L%s$ptr:\n" stub_name;
-  fprintf oc "	.indirect_symbol _%s\n" fun_name;
-  fprintf oc "	.long	0\n"
-
-(* Stubs for fixed-type functions are much simpler *)
-
-let non_variadic_stub oc name =
-  fprintf oc "	addis	r11, 0, ha16(L%s$ptr)\n" name;
-  fprintf oc "	lwz	r11, lo16(L%s$ptr)(r11)\n" name;
-  fprintf oc "	mtctr	r11\n";
-  fprintf oc "	bctr\n";
-  fprintf oc "	.non_lazy_symbol_pointer\n";
-  fprintf oc "L%s$ptr:\n" name;
-  fprintf oc "	.indirect_symbol _%s\n" name;
-  fprintf oc "	.long	0\n"
-
-let stub_function oc name sg =
-  let name = extern_atom name in
-  section oc Section_text;
-  fprintf oc "	.align 2\n";
-  fprintf oc "L%s$stub:\n" name;
-  if Str.string_match re_variadic_stub name 0
-  then variadic_stub oc name (Str.matched_group 1 name) sg.sig_args
-  else non_variadic_stub oc name
-
-let function_needs_stub name = true
-
-end
-
 (* Stubs for EABI *)
 
-module Stubs_EABI = struct
-
 let variadic_stub oc stub_name fun_name args =
   section oc Section_text;
   fprintf oc "	.align 2\n";
@@ -1035,17 +879,7 @@ let stub_function oc name sg =
 let function_needs_stub name =
   Str.string_match re_variadic_stub (extern_atom name) 0
 
-end
-
-let function_needs_stub =
-  match target with
-  | MacOS      -> Stubs_MacOS.function_needs_stub
-  | Linux|Diab -> Stubs_EABI.function_needs_stub
-
-let stub_function =
-  match target with
-  | MacOS       -> Stubs_MacOS.stub_function
-  | Linux|Diab  -> Stubs_EABI.stub_function
+(* Generation of whole programs *)
 
 let print_fundef oc (name, defn) =
   match defn with
@@ -1117,10 +951,8 @@ let print_var oc (name, v) =
           fprintf oc "	.globl	%a\n" symbol name;
         fprintf oc "%a:\n" symbol name;
         print_init_data oc name v.gvar_init;
-        if target <> MacOS then begin
-          fprintf oc "	.type	%a, @object\n" symbol name;
-          fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
-        end
+        fprintf oc "	.type	%a, @object\n" symbol name;
+        fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
       end else begin
         let sz =
           match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
diff --git a/powerpc/macosx/Conventions1.v b/powerpc/macosx/Conventions1.v
deleted file mode 100644
index 1ec6e88..0000000
--- a/powerpc/macosx/Conventions1.v
+++ /dev/null
@@ -1,599 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Function calling conventions and other conventions regarding the use of 
-    machine registers and stack slots. *)
-
-Require Import Coqlib.
-Require Import AST.
-Require Import Locations.
-
-(** * Classification of machine registers *)
-
-(** Machine registers (type [mreg] in module [Locations]) are divided in
-  the following groups:
-- Temporaries used for spilling, reloading, and parallel move operations.
-- Allocatable registers, that can be assigned to RTL pseudo-registers.
-  These are further divided into:
--- Callee-save registers, whose value is preserved across a function call.
--- Caller-save registers that can be modified during a function call.
-
-  We follow the PowerPC/MacOSX application binary interface (ABI) in our choice
-  of callee- and caller-save registers.
-*)
-
-Definition int_caller_save_regs :=
-  R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: nil.
-
-Definition float_caller_save_regs :=
-  F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: F11 :: nil.
-
-Definition int_callee_save_regs :=
-  R14 :: R15 :: R16 :: R17 :: R18 :: R19 :: R20 :: R21 :: R22 :: 
-  R23 :: R24 :: R25 :: R26 :: R27 :: R28 :: R29 :: R30 :: R31 :: nil.
-
-Definition float_callee_save_regs :=
-  F14 :: F15 :: F16 :: F17 :: F18 :: F19 :: F20 :: F21 :: F22 :: 
-  F23 :: F24 :: F25 :: F26 :: F27 :: F28 :: F29 :: F30 :: F31 :: nil.
-
-Definition destroyed_at_call_regs :=
-  int_caller_save_regs ++ float_caller_save_regs.
-
-Definition destroyed_at_call :=
-  List.map R destroyed_at_call_regs.
-
-Definition int_temporaries := IT1 :: IT2 :: nil.
-
-Definition float_temporaries := FT1 :: FT2 :: FT3 :: nil.
-  
-Definition temporary_regs := int_temporaries ++ float_temporaries.
-
-Definition temporaries := List.map R temporary_regs.
-
-Definition destroyed_at_move_regs: list mreg := nil.
-
-Definition destroyed_at_move := List.map R destroyed_at_move_regs.
-
-Definition dummy_int_reg := R3.     (**r Used in [Coloring]. *)
-Definition dummy_float_reg := F1.   (**r Used in [Coloring]. *)
-
-(** The [index_int_callee_save] and [index_float_callee_save] associate
-  a unique positive integer to callee-save registers.  This integer is
-  used in [Stacking] to determine where to save these registers in
-  the activation record if they are used by the current function. *)
-
-Definition index_int_callee_save (r: mreg) :=
-  match r with
-  | R14 => 0  | R15 => 1  | R16 => 2  | R17 => 3
-  | R18 => 4  | R19 => 5  | R20 => 6  | R21 => 7
-  | R22 => 8  | R23 => 9  | R24 => 10 | R25 => 11
-  | R26 => 12 | R27 => 13 | R28 => 14 | R29 => 15
-  | R30 => 16 | R31 => 17 | _ => -1
-  end.
-
-Definition index_float_callee_save (r: mreg) :=
-  match r with
-  | F14 => 0  | F15 => 1  | F16 => 2  | F17 => 3
-  | F18 => 4  | F19 => 5  | F20 => 6  | F21 => 7
-  | F22 => 8  | F23 => 9  | F24 => 10 | F25 => 11
-  | F26 => 12 | F27 => 13 | F28 => 14 | F29 => 15
-  | F30 => 16 | F31 => 17 | _ => -1
-  end.
-
-Ltac ElimOrEq :=
-  match goal with
-  |  |- (?x = ?y) \/ _ -> _ =>
-       let H := fresh in
-       (intro H; elim H; clear H;
-        [intro H; rewrite <- H; clear H | ElimOrEq])
-  |  |- False -> _ =>
-       let H := fresh in (intro H; contradiction)
-  end.
-
-Ltac OrEq :=
-  match goal with
-  | |- (?x = ?x) \/ _ => left; reflexivity
-  | |- (?x = ?y) \/ _ => right; OrEq
-  | |- False => fail
-  end.
-
-Ltac NotOrEq :=
-  match goal with
-  | |- (?x = ?y) \/ _ -> False =>
-       let H := fresh in (
-       intro H; elim H; clear H; [intro; discriminate | NotOrEq])
-  | |- False -> False =>
-       contradiction
-  end.
-
-Lemma index_int_callee_save_pos:
-  forall r, In r int_callee_save_regs -> index_int_callee_save r >= 0.
-Proof.
-  intro r. simpl; ElimOrEq; unfold index_int_callee_save; omega.
-Qed.
-
-Lemma index_float_callee_save_pos:
-  forall r, In r float_callee_save_regs -> index_float_callee_save r >= 0.
-Proof.
-  intro r. simpl; ElimOrEq; unfold index_float_callee_save; omega.
-Qed.
-
-Lemma index_int_callee_save_pos2:
-  forall r, index_int_callee_save r >= 0 -> In r int_callee_save_regs.
-Proof.
-  destruct r; simpl; intro; omegaContradiction || OrEq.
-Qed.
-
-Lemma index_float_callee_save_pos2:
-  forall r, index_float_callee_save r >= 0 -> In r float_callee_save_regs.
-Proof.
-  destruct r; simpl; intro; omegaContradiction || OrEq.
-Qed.
-
-Lemma index_int_callee_save_inj:
-  forall r1 r2, 
-  In r1 int_callee_save_regs ->
-  In r2 int_callee_save_regs ->
-  r1 <> r2 ->
-  index_int_callee_save r1 <> index_int_callee_save r2.
-Proof.
-  intros r1 r2. 
-  simpl; ElimOrEq; ElimOrEq; unfold index_int_callee_save;
-  intros; congruence.
-Qed.
-
-Lemma index_float_callee_save_inj:
-  forall r1 r2, 
-  In r1 float_callee_save_regs ->
-  In r2 float_callee_save_regs ->
-  r1 <> r2 ->
-  index_float_callee_save r1 <> index_float_callee_save r2.
-Proof.
-  intros r1 r2. 
-  simpl; ElimOrEq; ElimOrEq; unfold index_float_callee_save;
-  intros; congruence.
-Qed.
-
-(** The following lemmas show that
-    (temporaries, destroyed at call, integer callee-save, float callee-save)
-    is a partition of the set of machine registers. *)
-
-Lemma int_float_callee_save_disjoint:
-  list_disjoint int_callee_save_regs float_callee_save_regs.
-Proof.
-  red; intros r1 r2. simpl; ElimOrEq; ElimOrEq; discriminate.
-Qed.
-
-Lemma register_classification:
-  forall r, 
-  (In (R r) temporaries \/ In (R r) destroyed_at_call) \/
-  (In r int_callee_save_regs \/ In r float_callee_save_regs).
-Proof.
-  destruct r; 
-  try (left; left; simpl; OrEq);
-  try (left; right; simpl; OrEq);
-  try (right; left; simpl; OrEq);
-  try (right; right; simpl; OrEq).
-Qed.
-
-Lemma int_callee_save_not_destroyed:
-  forall r, 
-    In (R r) temporaries \/ In (R r) destroyed_at_call ->
-    ~(In r int_callee_save_regs).
-Proof.
-  intros; red; intros. elim H.
-  generalize H0. simpl; ElimOrEq; NotOrEq.
-  generalize H0. simpl; ElimOrEq; NotOrEq.
-Qed.
-
-Lemma float_callee_save_not_destroyed:
-  forall r, 
-    In (R r) temporaries \/ In (R r) destroyed_at_call ->
-    ~(In r float_callee_save_regs).
-Proof.
-  intros; red; intros. elim H.
-  generalize H0. simpl; ElimOrEq; NotOrEq.
-  generalize H0. simpl; ElimOrEq; NotOrEq.
-Qed.
-
-Lemma int_callee_save_type:
-  forall r, In r int_callee_save_regs -> mreg_type r = Tint.
-Proof.
-  intro. simpl; ElimOrEq; reflexivity.
-Qed.
-
-Lemma float_callee_save_type:
-  forall r, In r float_callee_save_regs -> mreg_type r = Tfloat.
-Proof.
-  intro. simpl; ElimOrEq; reflexivity.
-Qed.
-
-Ltac NoRepet :=
-  match goal with
-  | |- list_norepet nil =>
-      apply list_norepet_nil
-  | |- list_norepet (?a :: ?b) =>
-      apply list_norepet_cons; [simpl; intuition discriminate | NoRepet]
-  end.
-
-Lemma int_callee_save_norepet:
-  list_norepet int_callee_save_regs.
-Proof.
-  unfold int_callee_save_regs; NoRepet.
-Qed.
-
-Lemma float_callee_save_norepet:
-  list_norepet float_callee_save_regs.
-Proof.
-  unfold float_callee_save_regs; NoRepet.
-Qed.
-
-(** * Function calling conventions *)
-
-(** The functions in this section determine the locations (machine registers
-  and stack slots) used to communicate arguments and results between the
-  caller and the callee during function calls.  These locations are functions
-  of the signature of the function and of the call instruction.  
-  Agreement between the caller and the callee on the locations to use
-  is guaranteed by our dynamic semantics for Cminor and RTL, which demand 
-  that the signature of the call instruction is identical to that of the
-  called function.
-
-  Calling conventions are largely arbitrary: they must respect the properties
-  proved in this section (such as no overlapping between the locations
-  of function arguments), but this leaves much liberty in choosing actual
-  locations.  To ensure binary interoperability of code generated by our
-  compiler with libraries compiled by another PowerPC compiler, we
-  implement the standard conventions defined in the PowerPC/MacOS X
-  application binary interface. *)
-
-(** ** Location of function result *)
-
-(** The result value of a function is passed back to the caller in
-  registers [R3] or [F1], depending on the type of the returned value.
-  We treat a function without result as a function with one integer result. *)
-
-Definition loc_result (s: signature) : mreg :=
-  match s.(sig_res) with
-  | None => R3
-  | Some Tint => R3
-  | Some Tfloat => F1
-  end.
-
-(** The result location has the type stated in the signature. *)
-
-Lemma loc_result_type:
-  forall sig,
-  mreg_type (loc_result sig) =
-  match sig.(sig_res) with None => Tint | Some ty => ty end.
-Proof.
-  intros; unfold loc_result.
-  destruct (sig_res sig). 
-  destruct t; reflexivity.
-  reflexivity.
-Qed.
-
-(** The result location is a caller-save register or a temporary *)
-
-Lemma loc_result_caller_save:
-  forall (s: signature), 
-  In (R (loc_result s)) destroyed_at_call \/ In (R (loc_result s)) temporaries.
-Proof.
-  intros; unfold loc_result. left;
-  destruct (sig_res s). 
-  destruct t; simpl; OrEq.
-  simpl; OrEq.
-Qed.
-
-(** ** Location of function arguments *)
-
-(** The PowerPC ABI states the following convention for passing arguments
-  to a function:
-- The first 8 integer arguments are passed in registers [R3] to [R10].
-- The first 11 float arguments are passed in registers [F1] to [F11].
-- Each float argument passed in a float register ``consumes'' two
-  integer arguments.
-- Extra arguments are passed on the stack, in [Outgoing] slots, consecutively
-  assigned (1 word for an integer argument, 2 words for a float),
-  starting at word offset 0.
-- Stack space is reserved (as unused [Outgoing] slots) for the arguments
-  that are passed in registers.
-
-These conventions are somewhat baroque, but they are mandated by the ABI.
-*)
-
-Fixpoint loc_arguments_rec
-    (tyl: list typ) (iregl: list mreg) (fregl: list mreg)
-    (ofs: Z) {struct tyl} : list loc :=
-  match tyl with
-  | nil => nil
-  | Tint :: tys =>
-      match iregl with
-      | nil =>
-          S (Outgoing ofs Tint) :: loc_arguments_rec tys nil fregl (ofs + 1)
-      | ireg :: iregs =>
-          R ireg :: loc_arguments_rec tys iregs fregl ofs
-      end
-  | Tfloat :: tys =>
-      match fregl with
-      | nil =>
-          S (Outgoing ofs Tfloat) :: loc_arguments_rec tys iregl nil (ofs + 2)
-      | freg :: fregs =>
-          R freg :: loc_arguments_rec tys (list_drop 2%nat iregl) fregs ofs
-      end
-  end.
-
-Definition int_param_regs :=
-  R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: nil.
-Definition float_param_regs :=
-  F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: F8 :: F9 :: F10 :: F11 :: nil.
-
-(** [loc_arguments s] returns the list of locations where to store arguments
-  when calling a function with signature [s].  *)
-
-Definition loc_arguments (s: signature) : list loc :=
-  loc_arguments_rec s.(sig_args) int_param_regs float_param_regs 8.
-
-(** [size_arguments s] returns the number of [Outgoing] slots used
-  to call a function with signature [s]. *)
-
-Fixpoint size_arguments_rec
-    (tyl: list typ) (iregl: list mreg) (fregl: list mreg)
-    (ofs: Z) {struct tyl} : Z :=
-  match tyl with
-  | nil => ofs
-  | Tint :: tys =>
-      match iregl with
-      | nil => size_arguments_rec tys nil fregl (ofs + 1)
-      | ireg :: iregs => size_arguments_rec tys iregs fregl ofs
-      end
-  | Tfloat :: tys =>
-      match fregl with
-      | nil => size_arguments_rec tys iregl nil (ofs + 2)
-      | freg :: fregs => size_arguments_rec tys (list_drop 2%nat iregl) fregs ofs
-      end
-  end.
-
-Definition size_arguments (s: signature) : Z :=
-  size_arguments_rec s.(sig_args) int_param_regs float_param_regs 8.
-
-(** Argument locations are either non-temporary registers or [Outgoing] 
-  stack slots at nonnegative offsets. *)
-
-Definition loc_argument_acceptable (l: loc) : Prop :=
-  match l with
-  | R r => ~(In l temporaries)
-  | S (Outgoing ofs ty) => ofs >= 0
-  | _ => False
-  end.
-
-Remark loc_arguments_rec_charact:
-  forall tyl iregl fregl ofs l,
-  In l (loc_arguments_rec tyl iregl fregl ofs) ->
-  match l with
-  | R r => In r iregl \/ In r fregl
-  | S (Outgoing ofs' ty) => ofs' >= ofs
-  | S _ => False
-  end.
-Proof.
-Opaque list_drop.
-  induction tyl; simpl loc_arguments_rec; intros.
-  elim H.
-  destruct a. 
-  destruct iregl; elim H; intro. 
-  subst l. omega.
-  generalize (IHtyl _ _ _ _ H0). destruct l; auto. destruct s; auto. omega.
-  subst l. auto with coqlib.
-  generalize (IHtyl _ _ _ _ H0). destruct l; auto. simpl; intuition.
-  destruct fregl; elim H; intro. 
-  subst l. omega.
-  generalize (IHtyl _ _ _ _ H0). destruct l; auto. destruct s; auto. omega.
-  subst l. auto with coqlib.
-  generalize (IHtyl _ _ _ _ H0). destruct l; auto.
-  intros [A|B]. left; eapply list_drop_incl; eauto. right; auto with coqlib.
-Qed.
-
-Lemma loc_arguments_acceptable:
-  forall (s: signature) (r: loc),
-  In r (loc_arguments s) -> loc_argument_acceptable r.
-Proof.
-  unfold loc_arguments; intros.
-  generalize (loc_arguments_rec_charact _ _ _ _ _ H).
-  destruct r.
-  intro H0; elim H0. simpl. unfold not. ElimOrEq; NotOrEq.
-  simpl. unfold not. ElimOrEq; NotOrEq.
-  destruct s0; try contradiction.
-  simpl. omega. 
-Qed. 
-Hint Resolve loc_arguments_acceptable: locs.
-
-(** Arguments are parwise disjoint (in the sense of [Loc.norepet]). *)
-
-Remark loc_arguments_rec_notin_reg:
-  forall tyl iregl fregl ofs r,
-  ~(In r iregl) -> ~(In r fregl) ->
-  Loc.notin (R r) (loc_arguments_rec tyl iregl fregl ofs).
-Proof.
-  induction tyl; simpl; intros.
-  auto.
-  destruct a. 
-  destruct iregl; simpl. auto.
-  simpl in H. split. apply sym_not_equal. tauto.
-  apply IHtyl. tauto. tauto.
-  destruct fregl; simpl. auto.
-  simpl in H0. split. apply sym_not_equal. tauto.
-  apply IHtyl. 
-  red; intro. apply H. eapply list_drop_incl. eauto.
-  tauto.
-Qed.
-
-Remark loc_arguments_rec_notin_local:
-  forall tyl iregl fregl ofs ofs0 ty0,
-  Loc.notin (S (Local ofs0 ty0)) (loc_arguments_rec tyl iregl fregl ofs).
-Proof.
-  induction tyl; simpl; intros.
-  auto.
-  destruct a.
-  destruct iregl; simpl; auto.
-  destruct fregl; simpl; auto.
-Qed.
-
-Remark loc_arguments_rec_notin_outgoing:
-  forall tyl iregl fregl ofs ofs0 ty0,
-  ofs0 + typesize ty0 <= ofs ->
-  Loc.notin (S (Outgoing ofs0 ty0)) (loc_arguments_rec tyl iregl fregl ofs).
-Proof.
-  induction tyl; simpl; intros.
-  auto.
-  destruct a.
-  destruct iregl; simpl. 
-  split. omega. eapply IHtyl. omega.
-  auto.
-  destruct fregl; simpl. 
-  split. omega. eapply IHtyl. omega.
-  auto.
-Qed.
-
-Lemma loc_arguments_norepet:
-  forall (s: signature), Loc.norepet (loc_arguments s).
-Proof.
-  assert (forall tyl iregl fregl ofs,
-    list_norepet iregl ->
-    list_norepet fregl ->
-    list_disjoint iregl fregl ->
-    Loc.norepet (loc_arguments_rec tyl iregl fregl ofs)).
-  induction tyl; simpl; intros.
-  constructor.
-  destruct a. 
-  destruct iregl; constructor.
-  apply loc_arguments_rec_notin_outgoing. simpl; omega. auto.
-  apply loc_arguments_rec_notin_reg. inversion H. auto.
-  apply list_disjoint_notin with (m :: iregl); auto with coqlib.
-  apply IHtyl. inv H; auto. auto.
-  eapply list_disjoint_cons_left; eauto.
-  destruct fregl; constructor.
-  apply loc_arguments_rec_notin_outgoing. simpl; omega. auto.
-  apply loc_arguments_rec_notin_reg.
-  red; intro. apply (H1 m m). eapply list_drop_incl; eauto. 
-  auto with coqlib. auto. inv H0; auto.
-  apply IHtyl. eapply list_drop_norepet; eauto.
-  inv H0; auto. 
-  red; intros. apply H1. eapply list_drop_incl; eauto. auto with coqlib.
-
-  intro. unfold loc_arguments. apply H.
-  unfold int_param_regs. NoRepet.
-  unfold float_param_regs. NoRepet.
-  red; intros x y; simpl. ElimOrEq; ElimOrEq; discriminate.
-Qed.
-
-(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
-
-Remark size_arguments_rec_above:
-  forall tyl iregl fregl ofs0,
-  ofs0 <= size_arguments_rec tyl iregl fregl ofs0.
-Proof.
-  induction tyl; simpl; intros.
-  omega.
-  destruct a.
-  destruct iregl. apply Zle_trans with (ofs0 + 1); auto; omega. auto.
-  destruct fregl. apply Zle_trans with (ofs0 + 2); auto; omega. auto.
-Qed.
-
-Lemma size_arguments_above:
-  forall s, size_arguments s >= 0.
-Proof.
-  intros; unfold size_arguments. apply Zle_ge. apply Zle_trans with 8. omega. 
-  apply size_arguments_rec_above.
-Qed.
-
-Lemma loc_arguments_bounded:
-  forall (s: signature) (ofs: Z) (ty: typ),
-  In (S (Outgoing ofs ty)) (loc_arguments s) ->
-  ofs + typesize ty <= size_arguments s.
-Proof.
-  intros.
-  assert (forall tyl iregl fregl ofs0,
-    In (S (Outgoing ofs ty)) (loc_arguments_rec tyl iregl fregl ofs0) ->
-    ofs + typesize ty <= size_arguments_rec tyl iregl fregl ofs0).
-  induction tyl; simpl; intros.
-  elim H0.
-  destruct a. destruct iregl; elim H0; intro.
-  inv H1. simpl. apply size_arguments_rec_above. auto.
-  discriminate. auto. 
-  destruct fregl; elim H0; intro.
-  inv H1. simpl. apply size_arguments_rec_above. auto.
-  discriminate. auto. 
-  unfold size_arguments. eapply H0. unfold loc_arguments in H. eauto.
-Qed.
-
-(** Temporary registers do not overlap with argument locations. *)
-
-Lemma loc_arguments_not_temporaries:
-  forall sig, Loc.disjoint (loc_arguments sig) temporaries.
-Proof.
-  intros; red; intros x1 x2 H.
-  generalize (loc_arguments_rec_charact _ _ _ _ _ H).
-  destruct x1. 
-  intro H0; elim H0; simpl; (ElimOrEq; ElimOrEq; congruence).
-  destruct s; try contradiction. intro.
-  simpl; ElimOrEq; auto.
-Qed.
-Hint Resolve loc_arguments_not_temporaries: locs.
-
-(** Argument registers are caller-save. *)
-
-Lemma arguments_caller_save:
-  forall sig r,
-  In (R r) (loc_arguments sig) -> In (R r) destroyed_at_call.
-Proof.
-  unfold loc_arguments; intros.
-  elim (loc_arguments_rec_charact _ _ _ _ _ H); simpl.
-  ElimOrEq; intuition.
-  ElimOrEq; intuition.
-Qed.
-
-(** Argument locations agree in number with the function signature. *)
-
-Lemma loc_arguments_length:
-  forall sig,
-  List.length (loc_arguments sig) = List.length sig.(sig_args).
-Proof.
-  assert (forall tyl iregl fregl ofs,
-    List.length (loc_arguments_rec tyl iregl fregl ofs) = List.length tyl).
-  induction tyl; simpl; intros.
-  auto.
-  destruct a. 
-  destruct iregl; simpl; decEq; auto.
-  destruct fregl; simpl; decEq; auto.
-  intros. unfold loc_arguments. auto.
-Qed.
-
-(** Argument locations agree in types with the function signature. *)
-
-Lemma loc_arguments_type:
-  forall sig, List.map Loc.type (loc_arguments sig) = sig.(sig_args).
-Proof.
-  assert (forall tyl iregl fregl ofs,
-    (forall r, In r iregl -> mreg_type r = Tint) ->
-    (forall r, In r fregl -> mreg_type r = Tfloat) ->
-    List.map Loc.type (loc_arguments_rec tyl iregl fregl ofs) = tyl).
-  induction tyl; simpl; intros.
-  auto.
-  destruct a; [destruct iregl|destruct fregl]; simpl;
-  f_equal; eauto with coqlib.
-  apply IHtyl. intros. apply H. eapply list_drop_incl; eauto.
-  eauto with coqlib.
-
-  intros. unfold loc_arguments. apply H. 
-  intro; simpl. ElimOrEq; reflexivity.
-  intro; simpl. ElimOrEq; reflexivity.
-Qed.
diff --git a/powerpc/macosx/Stacklayout.v b/powerpc/macosx/Stacklayout.v
deleted file mode 100644
index 57592a8..0000000
--- a/powerpc/macosx/Stacklayout.v
+++ /dev/null
@@ -1,138 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Machine- and ABI-dependent layout information for activation records. *)
-
-Require Import Coqlib.
-Require Import Bounds.
-
-(** The general shape of activation records is as follows,
-  from bottom (lowest offsets) to top:
-- 24 reserved bytes.  The first 4 bytes hold the back pointer to the
-  activation record of the caller.  We use the 4 bytes at offset 12
-  to store the return address.  (These are reserved by the PowerPC
-  application binary interface.)  The remaining bytes are unused.
-- Space for outgoing arguments to function calls.
-- Local stack slots of integer type.
-- Saved values of integer callee-save registers used by the function.
-- One word of padding, if necessary to align the following data
-  on a 8-byte boundary.
-- Local stack slots of float type.
-- Saved values of float callee-save registers used by the function.
-- Space for the stack-allocated data declared in Cminor.
-
-The [frame_env] compilation environment records the positions of
-the boundaries between areas in the frame part.
-*)
-
-Definition fe_ofs_arg := 24.
-
-Record frame_env : Type := mk_frame_env {
-  fe_size: Z;
-  fe_ofs_link: Z;
-  fe_ofs_retaddr: Z;
-  fe_ofs_int_local: Z;
-  fe_ofs_int_callee_save: Z;
-  fe_num_int_callee_save: Z;
-  fe_ofs_float_local: Z;
-  fe_ofs_float_callee_save: Z;
-  fe_num_float_callee_save: Z;
-  fe_stack_data: Z
-}.
-
-(** Computation of the frame environment from the bounds of the current
-  function. *)
-
-Definition make_env (b: bounds) :=
-  let oil := 24 + 4 * b.(bound_outgoing) in    (* integer locals *)
-  let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *)
-  let oendi := oics + 4 * b.(bound_int_callee_save) in
-  let ofl := align oendi 8 in       (* float locals *)
-  let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *)
-  let ostkdata := ofcs + 8 * b.(bound_float_callee_save) in (* stack data *)
-  let sz := align (ostkdata + b.(bound_stack_data)) 16 in
-  mk_frame_env sz 0 12
-                  oil oics b.(bound_int_callee_save)
-                  ofl ofcs b.(bound_float_callee_save)
-                  ostkdata.
-
-(** Separation property *)
-
-Remark frame_env_separated:
-  forall b,
-  let fe := make_env b in
-  0 <= fe.(fe_ofs_link)
-  /\ fe.(fe_ofs_link) + 4 <= fe.(fe_ofs_retaddr)
-  /\ fe.(fe_ofs_retaddr) + 4 <= fe_ofs_arg
-  /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_int_local)
-  /\ fe.(fe_ofs_int_local) + 4 * b.(bound_int_local) <= fe.(fe_ofs_int_callee_save)
-  /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_local)
-  /\ fe.(fe_ofs_float_local) + 8 * b.(bound_float_local) <= fe.(fe_ofs_float_callee_save)
-  /\ fe.(fe_ofs_float_callee_save) + 8 * b.(bound_float_callee_save) <= fe.(fe_stack_data)
-  /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_size).
-Proof.
-  intros.
-  generalize (align_le (fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)).
-  generalize (align_le (fe.(fe_stack_data) + b.(bound_stack_data)) 16 (refl_equal _)).
-  unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr,
-    fe_ofs_int_local, fe_ofs_int_callee_save,
-    fe_num_int_callee_save,
-    fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save,
-    fe_stack_data, fe_ofs_arg.
-  intros.
-  generalize (bound_int_local_pos b); intro;
-  generalize (bound_float_local_pos b); intro;
-  generalize (bound_int_callee_save_pos b); intro;
-  generalize (bound_float_callee_save_pos b); intro;
-  generalize (bound_outgoing_pos b); intro;
-  generalize (bound_stack_data_pos b); intro.
-  omega.
-Qed.
-
-(** Alignment property *)
-
-Remark frame_env_aligned:
-  forall b,
-  let fe := make_env b in
-  (4 | fe.(fe_ofs_link))
-  /\ (4 | fe.(fe_ofs_int_local))
-  /\ (4 | fe.(fe_ofs_int_callee_save))
-  /\ (8 | fe.(fe_ofs_float_local))
-  /\ (8 | fe.(fe_ofs_float_callee_save))
-  /\ (4 | fe.(fe_ofs_retaddr))
-  /\ (4 | fe.(fe_stack_data))
-  /\ (16 | fe.(fe_size)).
-Proof.
-  intros.
-  unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr,
-    fe_ofs_int_local, fe_ofs_int_callee_save,
-    fe_num_int_callee_save,
-    fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save,
-    fe_stack_data.
-  set (x1 := 24 + 4 * bound_outgoing b).
-  assert (4 | x1). unfold x1; apply Zdivide_plus_r. exists 6; auto. exists (bound_outgoing b); ring.
-  set (x2 := x1 + 4 * bound_int_local b).
-  assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. exists (bound_int_local b); ring.
-  set (x3 := x2 + 4 * bound_int_callee_save b).
-  set (x4 := align x3 8).
-  assert (8 | x4). unfold x4. apply align_divides. omega.
-  set (x5 := x4 + 8 * bound_float_local b).
-  assert (8 | x5). unfold x5. apply Zdivide_plus_r; auto. exists (bound_float_local b); ring.
-  set (x6 := x5 + 8 * bound_float_callee_save b).
-  assert (4 | x6).
-    apply Zdivides_trans with 8. exists 2; auto.
-    unfold x6. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring.
-  set (x7 := align (x6 + bound_stack_data b) 16).
-  assert (16 | x7). unfold x7; apply align_divides. omega.
-  intuition.
-  exists 3; auto.
-Qed.