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

8 files changed, 51 insertions, 40 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index 09dead3..0609ac0 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -115,8 +115,6 @@ Inductive instruction: Type :=
   | Pmov_ra (rd: ireg) (id: ident)
   | Pmov_rm (rd: ireg) (a: addrmode)
   | Pmov_mr (a: addrmode) (rs: ireg)
-  | Pmovd_fr (rd: freg) (r1: ireg)      (**r [movd] (32-bit int) *)
-  | Pmovd_rf (rd: ireg) (rd: freg)
   | Pmovsd_ff (rd: freg) (r1: freg)     (**r [movsd] (single 64-bit float) *)
   | Pmovsd_fi (rd: freg) (n: float)     (**r (pseudo-instruction) *)
   | Pmovsd_fm (rd: freg) (a: addrmode)
@@ -129,16 +127,16 @@ Inductive instruction: Type :=
   (** Moves with conversion *)
   | Pmovb_mr (a: addrmode) (rs: ireg)   (**r [mov] (8-bit int) *)
   | Pmovw_mr (a: addrmode) (rs: ireg)   (**r [mov] (16-bit int) *)
-  | Pmovzb_rr (rd: ireg) (rs: ireg)    (**r [movzb] (8-bit zero-extension) *)
+  | Pmovzb_rr (rd: ireg) (rs: ireg)     (**r [movzb] (8-bit zero-extension) *)
   | Pmovzb_rm (rd: ireg) (a: addrmode)
-  | Pmovsb_rr (rd: ireg) (rs: ireg)    (**r [movsb] (8-bit sign-extension) *)
+  | Pmovsb_rr (rd: ireg) (rs: ireg)     (**r [movsb] (8-bit sign-extension) *)
   | Pmovsb_rm (rd: ireg) (a: addrmode)
-  | Pmovzw_rr (rd: ireg) (rs: ireg)    (**r [movzw] (16-bit zero-extension) *)
+  | Pmovzw_rr (rd: ireg) (rs: ireg)     (**r [movzw] (16-bit zero-extension) *)
   | Pmovzw_rm (rd: ireg) (a: addrmode)
-  | Pmovsw_rr (rd: ireg) (rs: ireg)    (**r [movsw] (16-bit sign-extension) *)
+  | Pmovsw_rr (rd: ireg) (rs: ireg)     (**r [movsw] (16-bit sign-extension) *)
   | Pmovsw_rm (rd: ireg) (a: addrmode)
   | Pcvtss2sd_fm (rd: freg) (a: addrmode) (**r [cvtss2sd] (single float load) *)
-  | Pcvtsd2ss_ff (rd: freg) (r1: freg) (**r pseudo (single conversion) *)
+  | Pcvtsd2ss_ff (rd: freg) (r1: freg)  (**r conversion to single (pseudo) *)
   | Pcvtsd2ss_mf (a: addrmode) (r1: freg) (**r [cvtsd2ss] (single float store *)
   | Pcvttsd2si_rf (rd: ireg) (r1: freg) (**r double to signed int *)
   | Pcvtsi2sd_fr (rd: freg) (r1: ireg)  (**r signed int to double *)
@@ -185,7 +183,7 @@ Inductive instruction: Type :=
   | Pjmp_s (symb: ident)
   | Pjmp_r (r: ireg)
   | Pjcc (c: testcond)(l: label)
-  | Pjcc2 (c1 c2: testcond)(l: label)
+  | Pjcc2 (c1 c2: testcond)(l: label)   (**r pseudo *)
   | Pjmptbl (r: ireg) (tbl: list label) (**r pseudo *)
   | Pcall_s (symb: ident)
   | Pcall_r (r: ireg)
@@ -481,10 +479,6 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       exec_load Mint32 m a rs rd
   | Pmov_mr a r1 =>
       exec_store Mint32 m a rs r1 nil
-  | Pmovd_fr rd r1 =>
-      Next (nextinstr (rs#rd <- (rs r1))) m
-  | Pmovd_rf rd r1 =>
-      Next (nextinstr (rs#rd <- (rs r1))) m
   | Pmovsd_ff rd r1 =>
       Next (nextinstr (rs#rd <- (rs r1))) m
   | Pmovsd_fi rd n =>
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 78f7d6e..4543ac9 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -103,6 +103,9 @@ Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
       | ST0  => OK (Pfld_m (Addrmode (Some base) None (inl _ ofs)) :: k)
       | _ => Error (msg "Asmgen.loadind")
       end
+  | Tsingle =>
+      do r <- freg_of dst;
+      OK (Pcvtss2sd_fm r (Addrmode (Some base) None (inl _ ofs)) :: k)
   | Tlong =>
       Error (msg "Asmgen.loadind")
   end.
@@ -118,6 +121,9 @@ Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
       | ST0  => OK (Pfstp_m (Addrmode (Some base) None (inl _ ofs)) :: k)
       | _ => Error (msg "Asmgen.loadind")
       end
+  | Tsingle =>
+      do r <- freg_of src;
+      OK (Pcvtsd2ss_mf (Addrmode (Some base) None (inl _ ofs)) r :: k)
   | Tlong =>
       Error (msg "Asmgen.storeind")
   end.
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index ca0fd18..f6eefbd 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -172,6 +172,7 @@ Proof.
   TailNoLabel.
   destruct (preg_of dst); TailNoLabel.
   discriminate.
+  TailNoLabel.
 Qed.
 
 Remark storeind_label:
@@ -183,6 +184,7 @@ Proof.
   TailNoLabel.
   destruct (preg_of src); TailNoLabel.
   discriminate.
+  TailNoLabel.
 Qed.
 
 Remark mk_setcc_base_label:
@@ -506,6 +508,8 @@ Proof.
   exists rs'; split. eauto.
   split. eapply agree_undef_regs; eauto. 
   simpl; intros. rewrite Q; auto with asmgen.
+Local Transparent destroyed_by_setstack.
+  destruct ty; simpl; intuition congruence.
 
 - (* Mgetparam *)
   assert (f0 = f) by congruence; subst f0.
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 303337e..00b706c 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -341,6 +341,12 @@ Proof.
   intuition Simplifs.
   (* long *)
   inv H.
+  (* single *)
+  monadInv H.
+  rewrite (freg_of_eq _ _ EQ). econstructor.
+  split. apply exec_straight_one. simpl. unfold exec_load. rewrite H1. rewrite H0.
+  eauto. auto.
+  intuition Simplifs.
 Qed.
 
 Lemma storeind_correct:
@@ -349,7 +355,7 @@ 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, data_preg r = true -> r <> ST0 -> rs'#r = rs#r.
+  /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_setstack ty) -> rs'#r = rs#r.
 Proof.
   unfold storeind; intros.
   set (addr := Addrmode (Some base) None (inl (ident * int) ofs)) in *.
@@ -372,6 +378,12 @@ Proof.
   intros. simpl. Simplifs.
   (* long *)
   inv H.
+  (* single *)
+  monadInv H.
+  rewrite (freg_of_eq _ _ EQ) in H0. econstructor.
+  split. apply exec_straight_one. simpl. unfold exec_store. rewrite H1. rewrite H0.
+  simpl. eauto. auto.
+  intros. destruct H2. Simplifs.
 Qed.
 
 (** Translation of addressing modes *)
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index 31ea8ee..528e9ed 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -124,6 +124,13 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
 Definition destroyed_at_function_entry: list mreg :=
   DX :: FP0 :: nil.   (* must include destroyed_by_op Omove *)
 
+Definition destroyed_by_setstack (ty: typ): list mreg :=
+  match ty with
+  | Tfloat => FP0 :: nil
+  | Tsingle => X7 :: FP0 :: nil
+  | _ => nil
+  end.
+
 Definition temp_for_parent_frame: mreg :=
   DX.
 
@@ -164,7 +171,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/ia32/Op.v b/ia32/Op.v
index 998f34d..4ac961b 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -295,7 +295,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)
   | Oindirectsymbol _ => (nil, Tint)
   | Ocast8signed => (Tint :: nil, Tint)
   | Ocast8unsigned => (Tint :: nil, Tint)
@@ -331,7 +331,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)
   | Ofloatofint => (Tint :: nil, Tfloat)
   | Omakelong => (Tint :: Tint :: nil, Tlong)
@@ -377,7 +377,7 @@ Proof with (try exact I).
   destruct op; simpl in H0; FuncInv; subst; simpl.
   congruence.
   exact I.
-  exact I.
+  destruct (Float.is_single_dec f); auto. 
   unfold symbol_address; destruct (Genv.find_symbol genv i)...
   destruct v0...
   destruct v0...
@@ -416,7 +416,7 @@ Proof with (try exact I).
   destruct v0; destruct v1...
   destruct v0; destruct v1...
   destruct v0; destruct v1...
-  destruct v0...
+  destruct v0... apply Float.singleoffloat_is_single.
   destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); inv H2...
   destruct v0; simpl in H0; inv H0...
   destruct v0; destruct v1...
@@ -425,19 +425,6 @@ Proof with (try exact I).
   destruct (eval_condition c vl m); simpl... 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/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 5ee4d01..8820515 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -281,7 +281,7 @@ let print_annot_val oc txt args res =
   | [IR src], [IR dst] ->
       if dst <> src then fprintf oc "	movl	%a, %a\n" ireg src ireg dst
   | [FR src], [FR dst] ->
-      if dst <> src then fprintf oc "	movsd	%a, %a\n" freg src freg dst
+      if dst <> src then fprintf oc "	movapd	%a, %a\n" freg src freg dst
   | _, _ -> assert false
 
 (* Handling of memcpy *)
@@ -442,7 +442,7 @@ let print_builtin_inline oc name args res =
   | "__builtin_fabs", [FR a1], [FR res] ->
       need_masks := true;
       if a1 <> res then
-        fprintf oc "	movsd	%a, %a\n" freg a1 freg res;
+        fprintf oc "	movapd	%a, %a\n" freg a1 freg res;
       fprintf oc "	andpd	%a, %a\n" raw_symbol "__absd_mask" freg res
   | "__builtin_fsqrt", [FR a1], [FR res] ->
       fprintf oc "	sqrtsd	%a, %a\n" freg a1 freg res
@@ -452,7 +452,7 @@ let print_builtin_inline oc name args res =
       else if res = a2 then
         fprintf oc "	maxsd	%a, %a\n" freg a1 freg res
       else begin
-        fprintf oc "	movsd	%a, %a\n" freg a1 freg res;
+        fprintf oc "	movapd	%a, %a\n" freg a1 freg res;
         fprintf oc "	maxsd	%a, %a\n" freg a2 freg res
       end
   | "__builtin_fmin", [FR a1; FR a2], [FR res] ->
@@ -461,7 +461,7 @@ let print_builtin_inline oc name args res =
       else if res = a2 then
         fprintf oc "	minsd	%a, %a\n" freg a1 freg res
       else begin
-        fprintf oc "	movsd	%a, %a\n" freg a1 freg res;
+        fprintf oc "	movapd	%a, %a\n" freg a1 freg res;
         fprintf oc "	minsd	%a, %a\n" freg a2 freg res
       end
   (* 64-bit integer arithmetic *)
@@ -531,10 +531,6 @@ let print_instruction oc = function
       fprintf oc "	movl	%a, %a\n" addressing a ireg rd
   | Pmov_mr(a, r1) ->
       fprintf oc "	movl	%a, %a\n" ireg r1 addressing a
-  | Pmovd_fr(rd, r1) ->
-      fprintf oc "	movd	%a, %a\n" ireg r1 freg rd
-  | Pmovd_rf(rd, r1) ->
-      fprintf oc "	movd	%a, %a\n" freg r1 ireg rd
   | Pmovsd_ff(rd, r1) ->
       fprintf oc "	movapd	%a, %a\n" freg r1 freg rd
   | Pmovsd_fi(rd, n) ->
diff --git a/ia32/standard/Conventions1.v b/ia32/standard/Conventions1.v
index cae20f6..e097e85 100644
--- a/ia32/standard/Conventions1.v
+++ b/ia32/standard/Conventions1.v
@@ -220,7 +220,7 @@ Definition loc_result (s: signature) : list mreg :=
   match s.(sig_res) with
   | None => AX :: nil
   | Some Tint => AX :: nil
-  | Some Tfloat => FP0 :: nil
+  | Some (Tfloat | Tsingle) => FP0 :: nil
   | Some Tlong => DX :: AX :: nil
   end.
 
@@ -261,6 +261,7 @@ Fixpoint loc_arguments_rec
   | nil => nil
   | Tint :: tys => S Outgoing ofs Tint :: loc_arguments_rec tys (ofs + 1)
   | Tfloat :: tys => S Outgoing ofs Tfloat :: loc_arguments_rec tys (ofs + 2)
+  | Tsingle :: tys => S Outgoing ofs Tsingle :: loc_arguments_rec tys (ofs + 1)
   | Tlong :: tys => S Outgoing (ofs + 1) Tint :: S Outgoing ofs Tint :: loc_arguments_rec tys (ofs + 2)
   end.
 
@@ -314,6 +315,9 @@ Proof.
   destruct H. subst l; split; [omega|congruence].
   exploit IHtyl; eauto.
   destruct l; auto. destruct sl; auto. intuition omega.
+- destruct H. subst l. split. omega. congruence.
+  exploit IHtyl; eauto.
+  destruct l; auto. destruct sl; auto. intuition omega.
 Qed.
 
 Lemma loc_arguments_acceptable:
@@ -362,6 +366,7 @@ Proof.
   destruct H. inv H. 
   simpl typesize. apply Zle_trans with (ofs + 2). omega. apply size_arguments_rec_above. 
   auto.
+  destruct H. inv H. apply size_arguments_rec_above. auto.
 Qed.