Support for inlined built-ins.

AST: add ef_inline flag to external functions.
Selection: recognize calls to inlined built-ins and inline them as Sbuiltin.
CminorSel to Asm: added Sbuiltin/Ibuiltin instruction.
PrintAsm: adapted expansion of builtins.
C2Clight: adapted detection of builtins.
Conventions: refactored in a machine-independent part (backend/Conventions)
  and a machine-dependent part (ARCH/SYS/Conventions1).


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

6 files changed, 130 insertions, 279 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 44e35b00..d160be78 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -24,7 +24,7 @@ Require Import Globalenvs.
 Require Import Smallstep.
 Require Import Locations.
 Require Stacklayout.
-Require Conventions.
+Require Import Conventions.
 
 (** * Abstract syntax *)
 
@@ -65,6 +65,28 @@ Inductive crbit: Type :=
 Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}.
 Proof. decide equality. Defined.
 
+(** We model the following registers of the ARM architecture. *)
+
+Inductive preg: Type :=
+  | IR: ireg -> preg                    (**r integer registers *)
+  | FR: freg -> preg                    (**r float registers *)
+  | CR: crbit -> preg                   (**r bits in the condition register *)
+  | PC: preg.                           (**r program counter *)
+
+Coercion IR: ireg >-> preg.
+Coercion FR: freg >-> preg.
+Coercion CR: crbit >-> preg.
+
+Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
+Proof. decide equality. apply ireg_eq. apply freg_eq. apply crbit_eq. Defined.
+
+Module PregEq.
+  Definition t := preg.
+  Definition eq := preg_eq.
+End PregEq.
+
+Module Pregmap := EMap(PregEq).
+
 (** The instruction set.  Most instructions correspond exactly to
   actual instructions of the PowerPC processor. See the PowerPC
   reference manuals for more details.  Some instructions,
@@ -149,7 +171,8 @@ Inductive instruction : Type :=
   | Pfreeframe: Z -> Z -> int -> instruction       (**r deallocate stack frame and restore previous frame *)
   | Plabel: label -> instruction                   (**r define a code label *)
   | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *)
-  | Pbtbl: ireg -> list label -> instruction.      (**r N-way branch through a jump table *)
+  | Pbtbl: ireg -> list label -> instruction       (**r N-way branch through a jump table *)
+  | Pbuiltin: external_function -> list preg -> preg -> instruction. (**r built-in *)
 
 (** The pseudo-instructions are the following:
 
@@ -204,28 +227,6 @@ Definition program := AST.program fundef unit.
 
 (** * Operational semantics *)
 
-(** We model the following registers of the ARM architecture. *)
-
-Inductive preg: Type :=
-  | IR: ireg -> preg                    (**r integer registers *)
-  | FR: freg -> preg                    (**r float registers *)
-  | CR: crbit -> preg                   (**r bits in the condition register *)
-  | PC: preg.                           (**r program counter *)
-
-Coercion IR: ireg >-> preg.
-Coercion FR: freg >-> preg.
-Coercion CR: crbit >-> preg.
-
-Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
-Proof. decide equality. apply ireg_eq. apply freg_eq. apply crbit_eq. Defined.
-
-Module PregEq.
-  Definition t := preg.
-  Definition eq := preg_eq.
-End PregEq.
-
-Module Pregmap := EMap(PregEq).
-
 (** The semantics operates over a single mapping from registers
   (type [preg]) to values.  We maintain (but do not enforce)
   the convention that integer registers are mapped to values of
@@ -532,6 +533,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
           else Error
       | _ => Error
       end
+  | Pbuiltin ef args res => Error    (**r treated specially below *)
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
@@ -594,10 +596,10 @@ Inductive extcall_args (rs: regset) (m: mem): list loc -> list val -> Prop :=
 
 Definition extcall_arguments
     (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
-  extcall_args rs m (Conventions.loc_arguments sg) args.
+  extcall_args rs m (loc_arguments sg) args.
 
 Definition loc_external_result (sg: signature) : preg :=
-  preg_of (Conventions.loc_result sg).
+  preg_of (loc_result sg).
 
 (** Execution of the instruction at [rs#PC]. *)
 
@@ -612,13 +614,20 @@ Inductive step: state -> trace -> state -> Prop :=
       find_instr (Int.unsigned ofs) c = Some i ->
       exec_instr c i rs m = OK rs' m' ->
       step (State rs m) E0 (State rs' m')
+  | exec_step_builtin:
+      forall b ofs c ef args res rs m t v m',
+      rs PC = Vptr b ofs ->
+      Genv.find_funct_ptr ge b = Some (Internal c) ->
+      find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) ->
+      external_call ef ge (map rs args) m t v m' ->
+      step (State rs m) t (State (nextinstr(rs # res <- v)) m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
       rs PC = Vptr b Int.zero ->
       Genv.find_funct_ptr ge b = Some (External ef) ->
       external_call ef ge args m t res m' ->
-      extcall_arguments rs m ef.(ef_sig) args ->
-      rs' = (rs#(loc_external_result ef.(ef_sig)) <- res
+      extcall_arguments rs m (ef_sig ef) args ->
+      rs' = (rs#(loc_external_result (ef_sig ef)) <- res
                #PC <- (rs IR14)) ->
       step (State rs m) t (State rs' m').
 
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 2a3b3f36..775bb37f 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -55,7 +55,7 @@ Definition is_immed_mem_float (x: int) : bool :=
   Int.eq (Int.and x (Int.repr 3)) Int.zero
   && Int.lt x (Int.repr 1024) && Int.lt (Int.repr (-1024)) x.
   
-(** Smart constructor for integer immediate arguments. *)
+(** Smart constructors for integer immediate arguments. *)
 
 Definition loadimm (r: ireg) (n: int) (k: code) :=
   if is_immed_arith n then
@@ -479,6 +479,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
         (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
          :: Pbsymb symb :: k)
+  | Mbuiltin ef args res =>
+      Pbuiltin ef (map preg_of args) (preg_of res) :: k
   | Mlabel lbl =>
       Plabel lbl :: k
   | Mgoto lbl =>
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 99759720..cc4d7ac5 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -25,6 +25,7 @@ Require Import Globalenvs.
 Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
+Require Import Conventions.
 Require Import Mach.
 Require Import Machconcr.
 Require Import Machtyping.
@@ -896,6 +897,37 @@ Lemma exec_Mtailcall_prop:
  forall (s : list stackframe) (fb stk : block) (soff
   intros. rewrite Pregmap.gso; auto.
 Qed.
 
+Lemma exec_Mbuiltin_prop:
+  forall (s : list stackframe) (f : block) (sp : val)
+         (ms : Mach.regset) (m : mem) (ef : external_function)
+         (args : list mreg) (res : mreg) (b : list Mach.instruction)
+         (t : trace) (v : val) (m' : mem),
+  external_call ef ge ms ## args m t v m' ->
+  exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t
+                  (Machconcr.State s f sp b (Regmap.set res v ms) m').
+Proof.
+  intros; red; intros; inv MS.
+  generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
+  intro WTI. inv WTI.
+  inv AT. simpl in H3.
+  generalize (functions_transl _ _ FIND); intro FN.
+  generalize (functions_transl_no_overflow _ _ FIND); intro NOOV.
+  left. econstructor; split. apply plus_one. 
+  eapply exec_step_builtin. eauto. eauto.
+  eapply find_instr_tail; eauto. 
+  replace (rs##(preg_of##args)) with (ms##args).
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  rewrite list_map_compose. apply list_map_exten. intros. 
+  symmetry. eapply preg_val; eauto. 
+  econstructor; eauto with coqlib.
+  unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso.
+  rewrite <- H0. simpl. constructor; auto.
+  eapply code_tail_next_int; eauto. 
+  apply sym_not_equal. auto with ppcgen. 
+  auto with ppcgen.
+Qed.
+
 Lemma exec_Mgoto_prop:
   forall (s : list stackframe) (fb : block) (f : function) (sp : val)
          (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset)
@@ -1145,7 +1177,7 @@ Lemma exec_function_external_prop:
   Genv.find_funct_ptr ge fb = Some (External ef) ->
   external_call ef ge args m t0 res m' ->
   Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args ->
-  ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms ->
+  ms' = Regmap.set (loc_result (ef_sig ef)) res ms ->
   exec_instr_prop (Machconcr.Callstate s fb ms m)
                t0 (Machconcr.Returnstate s ms' m').
 Proof.
@@ -1187,6 +1219,7 @@ Proof
            exec_Mstore_prop
            exec_Mcall_prop
            exec_Mtailcall_prop
+           exec_Mbuiltin_prop
            exec_Mgoto_prop
            exec_Mcond_true_prop
            exec_Mcond_false_prop
diff --git a/arm/Op.v b/arm/Op.v
index 7a255115..5e85aaec 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -24,6 +24,7 @@
   syntax and dynamic semantics of the Cminor language.
 *)
 
+Require Import Axioms.
 Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
@@ -132,7 +133,7 @@ Proof.
   generalize Int.eq_dec; intro.
   assert (forall (x y: shift_amount), {x=y}+{x<>y}).
   destruct x as [x Px]. destruct y as [y Py]. destruct (H x y).
-  subst x. rewrite (proof_irrelevance _ Px Py). left; auto.
+  subst x. rewrite (proof_irr Px Py). left; auto.
   right. red; intro. elim n. inversion H0. auto.
   decide equality.
 Qed.
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 3184d92f..b3f49cd6 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -188,7 +188,53 @@ let call_helper oc fn dst arg1 arg2 =
   (* ... for a total of at most 7 instructions *)
   7
 
-(* Built-in functions *)
+(* Built-ins.  They come in two flavors: 
+   - inlined by the compiler: take their arguments in arbitrary
+     registers; preserve all registers except IR14
+   - inlined while printing asm code; take their arguments in
+     locations dictated by the calling conventions; preserve
+     callee-save regs only. *)
+
+let print_builtin_inlined oc name args res =
+  fprintf oc "%s begin %s\n" comment name;
+  let n = match name, args, res with
+  (* Volatile reads *)
+  | "__builtin_volatile_read_int8unsigned", [IR addr], IR res ->
+      fprintf oc "	ldrb	%a, [%a, #0]\n" ireg res ireg addr; 1
+  | "__builtin_volatile_read_int8signed", [IR addr], IR res ->
+      fprintf oc "	ldrsb	%a, [%a, #0]\n" ireg res ireg addr; 1
+  | "__builtin_volatile_read_int16unsigned", [IR addr], IR res ->
+      fprintf oc "	ldrh	%a, [%a, #0]\n" ireg res ireg addr; 1
+  | "__builtin_volatile_read_int16signed", [IR addr], IR res ->
+      fprintf oc "	ldrsh	%a, [%a, #0]\n" ireg res ireg addr; 1
+  | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res ->
+      fprintf oc "	ldr	%a, [%a, #0]\n" ireg res ireg addr; 1
+  | "__builtin_volatile_read_float32", [IR addr], FR res ->
+      fprintf oc "	ldfs	%a, [%a, #0]\n" freg res ireg addr;
+      fprintf oc "	mvfd	%a, %a\n" freg res freg res; 2
+  | "__builtin_volatile_read_float64", [IR addr], FR res ->
+      fprintf oc "	ldfd	%a, [%a, #0]\n" freg res ireg addr; 1
+  (* Volatile writes *)
+  | ("__builtin_volatile_write_int8unsigned"|"__builtin_volatile_write_int8signed"), [IR addr; IR src], _ ->
+      fprintf oc "	strb	%a, [%a, #0]\n" ireg src ireg addr; 1
+  | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ ->
+      fprintf oc "	strh	%a, [%a, #0]\n" ireg src ireg addr; 1
+  | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ ->
+      fprintf oc "	str	%a, [%a, #0]\n" ireg src ireg addr; 1
+  | "__builtin_volatile_write_float32", [IR addr; FR src], _ ->
+      fprintf oc "	mvfs	%a, %a\n" freg FR2 freg src;
+      fprintf oc "	stfs	%a, [%a, #0]\n" freg FR2 ireg addr; 2
+  | "__builtin_volatile_write_float64", [IR addr; FR src], _ ->
+      fprintf oc "	stfd	%a, [%a, #0]\n" freg src ireg addr; 1
+  (* Float arithmetic *)
+  | "__builtin_fabs", [FR a1], FR res ->
+      fprintf oc "	absd	%a, %a\n" freg res freg a1; 1
+  (* Catch-all *)
+  | _ ->
+      invalid_arg ("unrecognized builtin " ^ name)
+  in
+  fprintf oc "%s end %s\n" comment name;
+  n
 
 let re_builtin_function = Str.regexp "__builtin_"
 
@@ -200,38 +246,6 @@ let print_builtin_function oc s =
   (* int args: IR0-IR3     float args: FR0, FR1
      int res:  IR0        float res:  FR0 *)
   let n = match extern_atom s with
-  (* Volatile reads *)
-  | "__builtin_volatile_read_int8unsigned" ->
-      fprintf oc "	ldrb	%a, [%a, #0]\n" ireg IR0 ireg IR0; 1
-  | "__builtin_volatile_read_int8signed" ->
-      fprintf oc "	ldrsb	%a, [%a, #0]\n" ireg IR0 ireg IR0; 1
-  | "__builtin_volatile_read_int16unsigned" ->
-      fprintf oc "	ldrh	%a, [%a, #0]\n" ireg IR0 ireg IR0; 1
-  | "__builtin_volatile_read_int16signed" ->
-      fprintf oc "	ldrsh	%a, [%a, #0]\n" ireg IR0 ireg IR0; 1
-  | "__builtin_volatile_read_int32"
-  | "__builtin_volatile_read_pointer" ->
-      fprintf oc "	ldr	%a, [%a, #0]\n" ireg IR0 ireg IR0; 1
-  | "__builtin_volatile_read_float32" ->
-      fprintf oc "	ldfs	%a, [%a, #0]\n" freg FR0 ireg IR0;
-      fprintf oc "	mvfd	%a, %a\n" freg FR0 freg FR0; 2
-  | "__builtin_volatile_read_float64" ->
-      fprintf oc "	ldfd	%a, [%a, #0]\n" freg FR0 ireg IR0; 1
-  (* Volatile writes *)
-  | "__builtin_volatile_write_int8unsigned"
-  | "__builtin_volatile_write_int8signed" ->
-      fprintf oc "	strb	%a, [%a, #0]\n" ireg IR1 ireg IR0; 1
-  | "__builtin_volatile_write_int16unsigned"
-  | "__builtin_volatile_write_int16signed" ->
-      fprintf oc "	strh	%a, [%a, #0]\n" ireg IR1 ireg IR0; 1
-  | "__builtin_volatile_write_int32"
-  | "__builtin_volatile_write_pointer" ->
-      fprintf oc "	str	%a, [%a, #0]\n" ireg IR1 ireg IR0; 1
-  | "__builtin_volatile_write_float32" ->
-      fprintf oc "	mvfs	%a, %a\n" freg FR0 freg FR0;
-      fprintf oc "	stfs	%a, [%a, #0]\n" freg FR0 ireg IR0; 2
-  | "__builtin_volatile_write_float64" ->
-      fprintf oc "	stfd	%a, [%a, #0]\n" freg FR0 ireg IR0; 1
   (* Block copy *)
   | "__builtin_memcpy" ->
       let lbl1 = new_label() in
@@ -252,7 +266,7 @@ let print_builtin_function oc s =
       fprintf oc "	subnes	%a, %a, #1\n" ireg IR2 ireg IR2;
       fprintf oc "	bne	%a\n" label lbl
 *)
-  | "__builtin_memcpy_word" ->
+  | "__builtin_memcpy_words" ->
       let lbl1 = new_label() in
       let lbl2 = new_label() in
       fprintf oc "	movs	%a, %a, lsr #2\n" ireg IR2 ireg IR2;
@@ -467,6 +481,8 @@ let print_instruction oc labels = function
         (fun l -> fprintf oc "	.word	%a\n" print_label l)
         tbl;
       2 + List.length tbl
+  | Pbuiltin(ef, args, res) ->
+      print_builtin_inlined oc (extern_atom ef.ef_id) args res
 
 let no_fallthrough = function
   | Pb _ -> true
diff --git a/arm/linux/Conventions.v b/arm/linux/Conventions1.v
index a35162c2..703dc12d 100644
--- a/arm/linux/Conventions.v
+++ b/arm/linux/Conventions1.v
@@ -222,65 +222,6 @@ Proof.
   unfold float_callee_save_regs; NoRepet.
 Qed.
 
-(** * Acceptable locations for register allocation *)
-
-(** The following predicate describes the locations that can be assigned
-  to an RTL pseudo-register during register allocation: a non-temporary
-  machine register or a [Local] stack slot are acceptable. *)
-
-Definition loc_acceptable (l: loc) : Prop :=
-  match l with
-  | R r => ~(In l temporaries)
-  | S (Local ofs ty) => ofs >= 0
-  | S (Incoming _ _) => False
-  | S (Outgoing _ _) => False
-  end.
-
-Definition locs_acceptable (ll: list loc) : Prop :=
-  forall l, In l ll -> loc_acceptable l.
-
-Lemma temporaries_not_acceptable:
-  forall l, loc_acceptable l -> Loc.notin l temporaries.
-Proof.
-  unfold loc_acceptable; destruct l.
-  simpl. intuition congruence.
-  destruct s; try contradiction. 
-  intro. simpl. tauto.
-Qed.
-Hint Resolve temporaries_not_acceptable: locs.
-
-Lemma locs_acceptable_disj_temporaries:
-  forall ll, locs_acceptable ll -> Loc.disjoint ll temporaries.
-Proof.
-  intros. apply Loc.notin_disjoint. intros.
-  apply temporaries_not_acceptable. auto. 
-Qed.
-
-Lemma loc_acceptable_noteq_diff:
-  forall l1 l2,
-  loc_acceptable l1 -> l1 <> l2 -> Loc.diff l1 l2.
-Proof.
-  unfold loc_acceptable, Loc.diff; destruct l1; destruct l2;
-  try (destruct s); try (destruct s0); intros; auto; try congruence.
-  case (zeq z z0); intro. 
-  compare t t0; intro.
-  subst z0; subst t0; tauto.
-  tauto. tauto.
-  contradiction. contradiction.
-Qed.
-
-Lemma loc_acceptable_notin_notin:
-  forall r ll,
-  loc_acceptable r ->
-  ~(In r ll) -> Loc.notin r ll.
-Proof.
-  induction ll; simpl; intros.
-  auto.
-  split. apply loc_acceptable_noteq_diff. assumption. 
-  apply sym_not_equal. tauto. 
-  apply IHll. assumption. tauto. 
-Qed.
-
 (** * Function calling conventions *)
 
 (** The functions in this section determine the locations (machine registers
@@ -326,40 +267,18 @@ Proof.
   reflexivity.
 Qed.
 
-(** The result location is acceptable. *)
-
-Lemma loc_result_acceptable:
-  forall sig, loc_acceptable (R (loc_result sig)).
-Proof.
-  intros. unfold loc_acceptable. red.
-  unfold loc_result. destruct (sig_res sig).
-  destruct t; simpl; NotOrEq.
-  simpl; NotOrEq.
-Qed.
-
-(** The result location is a caller-save register. *)
+(** 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.
+  forall (s: signature), 
+  In (R (loc_result s)) destroyed_at_call \/ In (R (loc_result s)) temporaries.
 Proof.
-  intros; unfold loc_result.
+  intros; unfold loc_result. left;
   destruct (sig_res s). 
   destruct t; simpl; OrEq.
   simpl; OrEq.
 Qed.
 
-(** The result location is not a callee-save register. *)
-
-Lemma loc_result_not_callee_save:
-  forall (s: signature),
-  ~(In (loc_result s) int_callee_save_regs \/ In (loc_result s) float_callee_save_regs).
-Proof.
-  intros. generalize (loc_result_caller_save s).
-  generalize (int_callee_save_not_destroyed (loc_result s)).
-  generalize (float_callee_save_not_destroyed (loc_result s)).
-  tauto.
-Qed.
-
 (** ** Location of function arguments *)
 
 (** We use the following calling conventions, adapted from the ARM ABI:
@@ -449,13 +368,6 @@ Fixpoint size_arguments_rec
 Definition size_arguments (s: signature) : Z :=
   size_arguments_rec s.(sig_args) int_param_regs float_param_regs 0.
 
-(** A tail-call is possible for a signature if the corresponding
-    arguments are all passed in registers. *)
-
-Definition tailcall_possible (s: signature) : Prop :=
-  forall l, In l (loc_arguments s) ->
-  match l with R _ => True | S _ => False end.
-
 (** Argument locations are either non-temporary registers or [Outgoing] 
   stack slots at nonnegative offsets. *)
 
@@ -685,24 +597,6 @@ Proof.
   ElimOrEq; intuition.
 Qed.
 
-(** Callee-save registers do not overlap with argument locations. *)
-
-Lemma arguments_not_preserved:
-  forall sig l,
-  Loc.notin l destroyed_at_call -> loc_acceptable l ->
-  Loc.notin l (loc_arguments sig).
-Proof.
-  intros. unfold loc_arguments. destruct l.
-  apply loc_arguments_rec_notin_reg. 
-  generalize (Loc.notin_not_in _ _ H). intro; red; intro.
-  apply H1. generalize H2. simpl. ElimOrEq; OrEq. 
-  generalize (Loc.notin_not_in _ _ H). intro; red; intro.
-  apply H1. generalize H2. simpl. ElimOrEq; OrEq. 
-  destruct s; simpl in H0; try contradiction.
-  apply loc_arguments_rec_notin_local.
-Qed.
-Hint Resolve arguments_not_preserved: locs.
-
 (** Argument locations agree in number with the function signature. *)
 
 Lemma loc_arguments_length:
@@ -748,107 +642,3 @@ Proof.
   intro; simpl. ElimOrEq; reflexivity.
 Qed.
 
-(** There is no partial overlap between an argument location and an
-  acceptable location: they are either identical or disjoint. *)
-
-Lemma no_overlap_arguments:
-  forall args sg,
-  locs_acceptable args ->
-  Loc.no_overlap args (loc_arguments sg).
-Proof.
-  unfold Loc.no_overlap; intros.
-  generalize (H r H0).
-  generalize (loc_arguments_acceptable _ _ H1).
-  destruct s; destruct r; simpl.
-  intros. case (mreg_eq m0 m); intro. left; congruence. tauto.
-  intros. right; destruct s; auto.
-  intros. right. auto.
-  destruct s; try tauto. destruct s0; tauto.
-Qed.
-
-(** Decide whether a tailcall is possible. *)
-
-Definition tailcall_is_possible (sg: signature) : bool :=
-  let fix tcisp (l: list loc) :=
-    match l with
-    | nil => true
-    | R _ :: l' => tcisp l'
-    | S _ :: l' => false
-    end
-  in tcisp (loc_arguments sg).
-
-Lemma tailcall_is_possible_correct:
-  forall s, tailcall_is_possible s = true -> tailcall_possible s.
-Proof.
-  intro s. unfold tailcall_is_possible, tailcall_possible.
-  generalize (loc_arguments s). induction l; simpl; intros.
-  elim H0.
-  destruct a. 
-  destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate.
-Qed.
-
-(** ** Location of function parameters *)
-
-(** A function finds the values of its parameter in the same locations
-  where its caller stored them, except that the stack-allocated arguments,
-  viewed as [Outgoing] slots by the caller, are accessed via [Incoming]
-  slots (at the same offsets and types) in the callee. *)
-
-Definition parameter_of_argument (l: loc) : loc :=
-  match l with
-  | S (Outgoing n ty) => S (Incoming n ty)
-  | _ => l
-  end.
-
-Definition loc_parameters (s: signature) :=
-  List.map parameter_of_argument (loc_arguments s).
-
-Lemma loc_parameters_type:
-  forall sig, List.map Loc.type (loc_parameters sig) = sig.(sig_args).
-Proof.
-  intros. unfold loc_parameters.
-  rewrite list_map_compose. 
-  rewrite <- loc_arguments_type.
-  apply list_map_exten.
-  intros. destruct x; simpl. auto. 
-  destruct s; reflexivity.
-Qed.
-
-Lemma loc_parameters_length:
-  forall sg, List.length (loc_parameters sg) = List.length sg.(sig_args).
-Proof.
-  intros. unfold loc_parameters. rewrite list_length_map. 
-  apply loc_arguments_length.
-Qed.
-
-Lemma loc_parameters_not_temporaries:
-  forall sig, Loc.disjoint (loc_parameters sig) temporaries.
-Proof.
-  intro; red; intros.
-  unfold loc_parameters in H. 
-  elim (list_in_map_inv _ _ _ H). intros y [EQ IN].
-  generalize (loc_arguments_not_temporaries sig y x2 IN H0).
-  subst x1. destruct x2.
-  destruct y; simpl. auto. destruct s; auto.
-  byContradiction. generalize H0. simpl. NotOrEq.
-Qed.
-
-Lemma no_overlap_parameters:
-  forall params sg,
-  locs_acceptable params ->
-  Loc.no_overlap (loc_parameters sg) params.
-Proof.
-  unfold Loc.no_overlap; intros.
-  unfold loc_parameters in H0. 
-  elim (list_in_map_inv _ _ _ H0). intros t [EQ IN].
-  rewrite EQ. 
-  generalize (loc_arguments_acceptable _ _ IN).
-  generalize (H s H1).
-  destruct s; destruct t; simpl.
-  intros. case (mreg_eq m0 m); intro. left; congruence. tauto.
-  intros. right; destruct s; simpl; auto.
-  intros; right; auto.
-  destruct s; try tauto. destruct s0; try tauto. 
-  intros; simpl. tauto.
-Qed.
-