From be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 19 May 2013 09:54:40 +0000 Subject: 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 --- arm/Asmgen.v | 36 ++++++++++++++++------------ arm/Asmgenproof.v | 11 +++++---- arm/Asmgenproof1.v | 45 +++++++++++++++++++++++++++++++---- arm/Machregs.v | 8 ++++++- arm/Op.v | 20 ++++------------ arm/PrintAsm.ml | 55 +++++++++++++++++++++++++++++++------------ arm/eabi/Conventions1.v | 62 +++++++++++++++++++++++++++++++++++-------------- 7 files changed, 162 insertions(+), 75 deletions(-) (limited to 'arm') 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. -- cgit v1.2.3