Merge of the float32 branch:

- added RTL type "Tsingle"
- ABI-compatible passing of single-precision floats on ARM and x86


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

7 files changed, 162 insertions, 75 deletions

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 1ff28d9..d160b2d 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -419,27 +419,33 @@ Definition indexed_memory_access
 Definition loadind_int (base: ireg) (ofs: int) (dst: ireg) (k: code) :=
   indexed_memory_access (fun base n => Pldr dst base (SAimm n)) mk_immed_mem_word base ofs k.
 
-Definition loadind_float (base: ireg) (ofs: int) (dst: freg) (k: code) :=
-  indexed_memory_access (Pfldd dst) mk_immed_mem_float base ofs k.
-
 Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
   match ty with
-  | Tint   => do r <- ireg_of dst; OK (loadind_int base ofs r k)
-  | Tfloat => do r <- freg_of dst; OK (loadind_float base ofs r k)
-  | Tlong => Error (msg "Asmgen.loadind")
+  | Tint =>
+      do r <- ireg_of dst; OK (loadind_int base ofs r k)
+  | Tfloat =>
+      do r <- freg_of dst;
+      OK (indexed_memory_access (Pfldd r) mk_immed_mem_float base ofs k)
+  | Tsingle =>
+      do r <- freg_of dst;
+      OK (indexed_memory_access (Pflds r) mk_immed_mem_float base ofs k)
+  | Tlong =>
+      Error (msg "Asmgen.loadind")
   end.
 
-Definition storeind_int (src: ireg) (base: ireg) (ofs: int) (k: code) :=
-  indexed_memory_access (fun base n => Pstr src base (SAimm n)) mk_immed_mem_word base ofs k.
-
-Definition storeind_float (src: freg) (base: ireg) (ofs: int) (k: code) :=
-  indexed_memory_access (Pfstd src) mk_immed_mem_float base ofs k.
-
 Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
   match ty with
-  | Tint   => do r <- ireg_of src; OK (storeind_int r base ofs k)
-  | Tfloat => do r <- freg_of src; OK (storeind_float r base ofs k)
-  | Tlong => Error (msg "Asmgen.storeind")
+  | Tint =>
+      do r <- ireg_of src;
+      OK (indexed_memory_access (fun base n => Pstr r base (SAimm n)) mk_immed_mem_word base ofs k)
+  | Tfloat =>
+      do r <- freg_of src;
+      OK (indexed_memory_access (Pfstd r) mk_immed_mem_float base ofs k)
+  | Tsingle =>
+      do r <- freg_of src;
+      OK (indexed_memory_access (Pfsts r) mk_immed_mem_float base ofs k)
+  | Tlong =>
+      Error (msg "Asmgen.storeind")
   end.
 
 (** Translation of memory accesses *)
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 6899040..18f905a 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -239,15 +239,14 @@ Remark loadind_label:
 Proof.
   intros. destruct ty; monadInv H.
   unfold loadind_int; TailNoLabel.
-  unfold loadind_float; TailNoLabel.
+  TailNoLabel.
+  TailNoLabel.
 Qed.
 
 Remark storeind_label:
   forall base ofs ty src k c, storeind src base ofs ty k = OK c -> tail_nolabel k c.
 Proof.
-  intros. destruct ty; monadInv H.
-  unfold storeind_int; TailNoLabel.
-  unfold storeind_float; TailNoLabel.
+  intros. destruct ty; monadInv H; TailNoLabel.
 Qed.
 
 Remark transl_cond_label:
@@ -556,8 +555,10 @@ Proof.
   rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
   exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
   exists rs'; split. eauto.
-  split. change (Mach.undef_regs (destroyed_by_op Omove) rs) with rs. apply agree_exten with rs0; auto with asmgen.
+  split. eapply agree_undef_regs; eauto with asmgen.
   simpl; intros. rewrite Q; auto with asmgen.
+Local Transparent destroyed_by_setstack.
+  destruct ty; simpl; auto with asmgen.
 
 - (* Mgetparam *)
   assert (f0 = f) by congruence; subst f0.
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index e27ee80..2f5f868 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -405,6 +405,7 @@ Proof.
   split. Simpl. intros; Simpl.
 Qed.
 
+(*
 Lemma loadind_float_correct:
   forall (base: ireg) ofs dst (rs: regset) m v k,
   Mem.loadv Mfloat64al32 m (Val.add rs#base (Vint ofs)) = Some v ->
@@ -418,6 +419,7 @@ Proof.
   apply exec_straight_one. simpl. unfold exec_load. rewrite H0; rewrite H; eauto. auto.
   split. Simpl. intros; Simpl.
 Qed.
+*)
 
 Lemma loadind_correct:
   forall (base: ireg) ofs ty dst k c (rs: regset) m v,
@@ -430,12 +432,25 @@ Lemma loadind_correct:
 Proof.
   unfold loadind; intros.
   destruct ty; monadInv H.
+- (* int *)
   erewrite ireg_of_eq by eauto. apply loadind_int_correct; auto. 
-  erewrite freg_of_eq by eauto. apply loadind_float_correct; auto. 
+- (* float *)
+  erewrite freg_of_eq by eauto. simpl in H0.
+  apply indexed_memory_access_correct; intros.
+  econstructor; split. 
+  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. 
+  split. Simpl. intros; Simpl.
+- (* single *)
+  erewrite freg_of_eq by eauto. simpl in H0.
+  apply indexed_memory_access_correct; intros.
+  econstructor; split. 
+  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. 
+  split. Simpl. intros; Simpl.
 Qed.
 
 (** Indexed memory stores. *)
 
+(*
 Lemma storeind_int_correct:
   forall (base: ireg) ofs (src: ireg) (rs: regset) m m' k,
   Mem.storev Mint32 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' ->
@@ -464,6 +479,7 @@ Proof.
   rewrite H0. rewrite H1; auto with asmgen. rewrite H; eauto. auto.
   intros; Simpl.
 Qed.
+*)
 
 Lemma storeind_correct:
   forall (base: ireg) ofs ty src k c (rs: regset) m m',
@@ -471,13 +487,32 @@ Lemma storeind_correct:
   Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' ->
   exists rs',
      exec_straight ge fn c rs m k rs' m'
-  /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r.
+  /\ forall r, r <> PC -> r <> IR14 -> preg_notin r (destroyed_by_setstack ty) -> rs'#r = rs#r.
 Proof.
   unfold storeind; intros.
-  destruct ty; monadInv H.
-  erewrite ireg_of_eq  in H0 by eauto. apply storeind_int_correct; auto.
+  destruct ty; monadInv H; simpl in H0.
+- (* int *)
+  erewrite ireg_of_eq  in H0 by eauto.
+  apply indexed_memory_access_correct; intros.
+  econstructor; split. 
+  apply exec_straight_one. simpl. unfold exec_store. 
+  rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto.
   assert (IR x <> IR IR14) by eauto with asmgen. congruence.
-  erewrite freg_of_eq in H0 by eauto. apply storeind_float_correct; auto. 
+  auto. intros; Simpl.
+- (* float *)
+  erewrite freg_of_eq  in H0 by eauto.
+  apply indexed_memory_access_correct; intros.
+  econstructor; split. 
+  apply exec_straight_one. simpl. unfold exec_store. 
+  rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto.
+  auto. intros; Simpl.
+- (* single *)
+  erewrite freg_of_eq  in H0 by eauto.
+  apply indexed_memory_access_correct; intros.
+  econstructor; split. 
+  apply exec_straight_one. simpl. unfold exec_store. 
+  rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto.
+  auto. intros; Simpl.
 Qed.
 
 (** Translation of shift immediates *)
diff --git a/arm/Machregs.v b/arm/Machregs.v
index 50535f0..d4439ef 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -109,6 +109,12 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
   | _ => nil
   end.
 
+Definition destroyed_by_setstack (ty: typ): list mreg :=
+  match ty with
+  | Tsingle => F6 :: nil
+  | _ => nil
+  end.
+
 Definition destroyed_at_function_entry: list mreg :=
   R12 :: nil.
 
@@ -131,7 +137,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list(
 Global Opaque
     destroyed_by_op destroyed_by_load destroyed_by_store
     destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin
-    destroyed_at_function_entry temp_for_parent_frame
+    destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame
     mregs_for_operation mregs_for_builtin.
 
 (** Two-address operations.  Return [true] if the first argument and
diff --git a/arm/Op.v b/arm/Op.v
index 2c84d90..a55c3f5 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -307,7 +307,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   match op with
   | Omove => (nil, Tint)   (* treated specially *)
   | Ointconst _ => (nil, Tint)
-  | Ofloatconst _ => (nil, Tfloat)
+  | Ofloatconst f => (nil, if Float.is_single_dec f then Tsingle else Tfloat)
   | Oaddrsymbol _ _ => (nil, Tint)
   | Oaddrstack _ => (nil, Tint)
   | Oadd => (Tint :: Tint :: nil, Tint)
@@ -345,7 +345,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osubf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Omulf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Odivf => (Tfloat :: Tfloat :: nil, Tfloat)
-  | Osingleoffloat => (Tfloat :: nil, Tfloat)
+  | Osingleoffloat => (Tfloat :: nil, Tsingle)
   | Ointoffloat => (Tfloat :: nil, Tint)
   | Ointuoffloat => (Tfloat :: nil, Tint)
   | Ofloatofint => (Tint :: nil, Tfloat)
@@ -384,6 +384,7 @@ Proof with (try exact I).
   intros.
   destruct op; simpl; simpl in H0; FuncInv; try subst v...
   congruence.
+  destruct (Float.is_single_dec f); red; auto. 
   unfold symbol_address. destruct (Genv.find_symbol genv i)...
   destruct sp...
   destruct v0; destruct v1...
@@ -422,7 +423,7 @@ Proof with (try exact I).
   destruct v0; destruct v1...
   destruct v0; destruct v1...
   destruct v0; destruct v1...
-  destruct v0...
+  destruct v0... simpl. apply Float.singleoffloat_is_single.  
   destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); simpl in H2; inv H2...
   destruct v0; simpl in H0; inv H0. destruct (Float.intuoffloat f); simpl in H2; inv H2...
   destruct v0; simpl in H0; inv H0...
@@ -433,19 +434,6 @@ Proof with (try exact I).
   destruct (eval_condition c vl m)... destruct b...
 Qed.
 
-Lemma type_of_chunk_correct:
-  forall chunk m addr v,
-  Mem.loadv chunk m addr = Some v ->
-  Val.has_type v (type_of_chunk chunk).
-Proof.
-  intro chunk.
-  assert (forall v, Val.has_type (Val.load_result chunk v) (type_of_chunk chunk)).
-  destruct v; destruct chunk; exact I.
-  intros until v. unfold Mem.loadv. 
-  destruct addr; intros; try discriminate.
-  eapply Mem.load_type; eauto.
-Qed.
-
 End SOUNDNESS.
 
 (** * Manipulating and transforming operations *)
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index cb3ce4d..97ed19a 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -457,22 +457,47 @@ let print_builtin_inline oc name args res =
 
 type direction = Incoming | Outgoing
 
+let ireg_param = function
+  | 0 -> IR0 | 1 -> IR1 | 2 -> IR2 | 3 -> IR3 | _ -> assert false
+
+let freg_param = function
+  | 0 -> FR0 | 1 -> FR1 | 2 -> FR2 | 3 -> FR3 | _ -> assert false
+
+let fixup_double oc dir f i1 i2 =
+  match dir with
+  | Incoming ->     (* f <- (i1, i2)  *)
+      fprintf oc "	fmdrr	%a, %a, %a\n" freg f ireg i1 ireg i2
+  | Outgoing ->     (* (i1, i2) <- f *)
+      fprintf oc "	fmrrd	%a, %a, %a\n" ireg i1 ireg i2 freg f
+
+let fixup_single oc dir f i =
+  match dir with
+  | Incoming ->     (* f <- i; f <- double_of_single f *)
+      fprintf oc "	fmsr	%a, %a\n" freg_single f ireg i;
+      fprintf oc "	fcvtds	%a, %a\n" freg f freg_single f
+  | Outgoing ->     (* f <- single_of_double f; i <- f *)
+      fprintf oc "	fcvtsd	%a, %a\n" freg_single f freg f;
+      fprintf oc "	fmrs	%a, %a\n" ireg i freg_single f
+
 let fixup_conventions oc dir tyl =
-  let fixup f i1 i2 =
-    match dir with
-    | Incoming ->     (* f <- (i1, i2)  *)
-        fprintf oc "	fmdrr	%a, %a, %a\n" freg f ireg i1 ireg i2
-    | Outgoing ->      (* (i1, i2) <- f *)
-        fprintf oc "	fmrrd	%a, %a, %a\n" ireg i1 ireg i2 freg f in
-  match tyl with
-  | Tfloat :: Tfloat :: _ ->
-      fixup FR0 IR0 IR1; fixup FR1 IR2 IR3; 4
-  | Tfloat :: _ ->
-      fixup FR0 IR0 IR1; 2
-  | Tint :: Tfloat :: _ | Tint :: Tint :: Tfloat :: _ ->
-      fixup FR1 IR2 IR3; 2
-  | _ ->
-      0
+  let rec fixup i tyl =
+    if i >= 4 then 0 else
+      match tyl with
+      | [] -> 0
+      | Tint :: tyl' ->
+          fixup (i+1) tyl'
+      | Tlong :: tyl' ->
+          fixup (((i + 1) land (-2)) + 2) tyl'
+      | Tfloat :: tyl' ->
+          let i = (i + 1) land (-2) in
+          if i >= 4 then 0 else begin
+            fixup_double oc dir (freg_param i) (ireg_param i) (ireg_param (i+1));
+            1 + fixup (i+2) tyl'
+          end
+      | Tsingle :: tyl' ->
+          fixup_single oc dir (freg_param i) (ireg_param i);
+          2 + fixup (i+1) tyl'
+  in fixup 0 tyl
 
 let fixup_arguments oc dir sg =
   fixup_conventions oc dir sg.sig_args
diff --git a/arm/eabi/Conventions1.v b/arm/eabi/Conventions1.v
index 1731eba..9fc9a50 100644
--- a/arm/eabi/Conventions1.v
+++ b/arm/eabi/Conventions1.v
@@ -236,7 +236,7 @@ Definition loc_result (s: signature) : list mreg :=
   match s.(sig_res) with
   | None => R0 :: nil
   | Some Tint => R0 :: nil
-  | Some Tfloat => F0 :: nil
+  | Some (Tfloat | Tsingle) => F0 :: nil
   | Some Tlong => R1 :: R0 :: nil
   end.
 
@@ -256,15 +256,23 @@ Qed.
 
 (** We use the following calling conventions, adapted from the ARM EABI:
 - The first 4 integer arguments are passed in registers [R0] to [R3].
-- The first 2 float arguments are passed in registers [F0] and [F1].
+- The first 2 float arguments are passed in registers [F0] and [F2].
+- The first 4 float arguments are passed in registers [F0] to [F3].
+- The first 2 integer arguments are passed in an aligned pair of two integer
+  registers.
 - Each float argument passed in a float register ``consumes'' an aligned pair
   of two integer registers.
-- Each long integer argument is passed in an aligned pair of two integer
-  registers.
+- Each single argument passed in a float register ``consumes'' an integer
+  register.
 - Extra arguments are passed on the stack, in [Outgoing] slots, consecutively
-  assigned (1 word for an integer argument, 2 words for a float or a long),
-  starting at word offset 0.
-*)
+  assigned (1 word for an integer or single argument, 2 words for a float
+  or a long), starting at word offset 0.
+
+This convention is not quite that of the ARM EABI, whereas every float
+argument are passed in one or two integer registers.  Unfortunately,
+this does not fit the data model of CompCert.  In [PrintAsm.ml]
+we insert additional code around function calls and returns that moves
+data appropriately. *)
 
 Definition ireg_param (n: Z) : mreg :=
   if zeq n (-4) then R0
@@ -273,7 +281,13 @@ Definition ireg_param (n: Z) : mreg :=
   else R3.
 
 Definition freg_param (n: Z) : mreg :=
-  if zeq n (-4) then F0 else F1.
+  if zeq n (-4) then F0 else F2.
+
+Definition sreg_param (n: Z) : mreg :=
+  if zeq n (-4) then F0
+  else if zeq n (-3) then F1
+  else if zeq n (-2) then F2
+  else F3.
 
 Fixpoint loc_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : list loc :=
   match tyl with
@@ -285,6 +299,9 @@ Fixpoint loc_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : list loc :=
       let ofs := align ofs 2 in
       (if zle 0 ofs then S Outgoing ofs Tfloat else R (freg_param ofs))
       :: loc_arguments_rec tys (ofs + 2)
+  | Tsingle :: tys =>
+      (if zle 0 ofs then S Outgoing ofs Tsingle else R (sreg_param ofs))
+      :: loc_arguments_rec tys (ofs + 1)
   | Tlong :: tys =>
       let ofs := align ofs 2 in
       (if zle 0 ofs then S Outgoing (ofs + 1) Tint else R (ireg_param (ofs + 1)))
@@ -304,7 +321,7 @@ Definition loc_arguments (s: signature) : list loc :=
 Fixpoint size_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : Z :=
   match tyl with
   | nil => ofs
-  | Tint :: tys => size_arguments_rec tys (ofs + 1)
+  | (Tint | Tsingle) :: tys => size_arguments_rec tys (ofs + 1)
   | (Tfloat | Tlong) :: tys => size_arguments_rec tys (align ofs 2 + 2)
   end.
 
@@ -321,15 +338,6 @@ Definition loc_argument_acceptable (l: loc) : Prop :=
   | _ => False
   end.
 
-(*
-Lemma align_monotone:
-  forall x1 x2 y, y > 0 -> x1 <= x2 -> align x1 y <= align x2 y.
-Proof.
-  intros. unfold align. apply Zmult_le_compat_r. apply Z_div_le. 
-  omega. omega. omega.
-Qed.
-*)
-
 Remark ireg_param_caller_save:
   forall n, In (ireg_param n) destroyed_at_call.
 Proof.
@@ -345,6 +353,15 @@ Proof.
   unfold freg_param; intros. destruct (zeq n (-4)); simpl; OrEq.
 Qed.
 
+Remark sreg_param_caller_save:
+  forall n, In (sreg_param n) destroyed_at_call.
+Proof.
+  unfold sreg_param; intros.
+  destruct (zeq n (-4)). simpl; tauto. 
+  destruct (zeq n (-3)). simpl; tauto. 
+  destruct (zeq n (-2)); simpl; tauto.
+Qed.
+
 Remark loc_arguments_rec_charact:
   forall tyl ofs l,
   In l (loc_arguments_rec tyl ofs) ->
@@ -381,6 +398,12 @@ Proof.
   split. omega. split. omega. congruence.
   apply ireg_param_caller_save.
   exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
+- (* Tsingle *)
+  destruct H.
+  subst l. destruct (zle 0 ofs).
+  split. omega. split. omega. congruence.
+  apply sreg_param_caller_save.
+  exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
 Qed.
 
 Lemma loc_arguments_acceptable:
@@ -409,6 +432,7 @@ Proof.
   apply Zle_trans with (align ofs 2 + 2); auto; omega.
   assert (ofs <= align ofs 2) by (apply align_le; omega).
   apply Zle_trans with (align ofs 2 + 2); auto; omega.
+  apply Zle_trans with (ofs + 1); auto; omega.
 Qed.
 
 Lemma size_arguments_above:
@@ -448,6 +472,8 @@ Proof.
     destruct H1; auto.
     destruct (zle 0 (align ofs0 2)); inv H1.
     eapply Zle_trans. 2: apply H0. simpl typesize; omega. omega.
+  - (* Tsingle *)
+    destruct H1; auto. destruct (zle 0 ofs0); inv H1. apply H0. omega. 
   }
   unfold size_arguments. apply H1. auto.  
 Qed.