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 --- powerpc/Asmgen.v | 4 ++-- powerpc/Asmgenproof.v | 5 ++--- powerpc/Machregs.v | 8 +++++++- powerpc/Op.v | 21 ++++----------------- powerpc/eabi/Conventions1.v | 26 +++++++++++++++++++++----- 5 files changed, 36 insertions(+), 28 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 6a1d07e..2b6d80d 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -136,7 +136,7 @@ Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := Plfd r (Cint ofs) base :: k else loadimm GPR0 ofs (Plfdx r base GPR0 :: k)) - | Tlong => + | Tlong | Tsingle => Error (msg "Asmgen.loadind") end. @@ -154,7 +154,7 @@ Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := Pstfd r (Cint ofs) base :: k else loadimm GPR0 ofs (Pstfdx r base GPR0 :: k)) - | Tlong => + | Tlong | Tsingle => Error (msg "Asmgen.storeind") end. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index e723c86..2c155ea 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -526,9 +526,8 @@ 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. - simpl; intros. rewrite Q; auto with asmgen. + split. eapply agree_undef_regs; eauto with asmgen. + simpl; intros. rewrite Q; auto with asmgen. - (* Mgetparam *) assert (f0 = f) by congruence; subst f0. diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index ce66e6a..d057dce 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -143,6 +143,12 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := | _ => nil end. +Definition destroyed_by_setstack (ty: typ): list mreg := + match ty with + | Tsingle => F13 :: nil + | _ => nil + end. + Definition destroyed_at_function_entry: list mreg := nil. @@ -158,7 +164,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/powerpc/Op.v b/powerpc/Op.v index 5835717..3963c6b 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -265,7 +265,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) | Ocast8signed => (Tint :: nil, Tint) @@ -303,7 +303,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) | Ofloatofwords => (Tint :: Tint :: nil, Tfloat) | Omakelong => (Tint :: Tint :: nil, Tlong) @@ -340,7 +340,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 sp... destruct v0... @@ -380,7 +380,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); inv H2... destruct v0; destruct v1... destruct v0; destruct v1... @@ -389,19 +389,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/powerpc/eabi/Conventions1.v b/powerpc/eabi/Conventions1.v index 369a81a..2db1f73 100644 --- a/powerpc/eabi/Conventions1.v +++ b/powerpc/eabi/Conventions1.v @@ -240,7 +240,7 @@ Definition loc_result (s: signature) : list mreg := match s.(sig_res) with | None => R3 :: nil | Some Tint => R3 :: nil - | Some Tfloat => F1 :: nil + | Some (Tfloat | Tsingle) => F1 :: nil | Some Tlong => R3 :: R4 :: nil end. @@ -285,7 +285,7 @@ Fixpoint loc_arguments_rec | Some ireg => R ireg :: loc_arguments_rec tys (ir + 1) fr ofs end - | Tfloat :: tys => + | (Tfloat | Tsingle) :: tys => match list_nth_z float_param_regs fr with | None => let ofs := align ofs 2 in @@ -321,7 +321,7 @@ Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := | None => size_arguments_rec tys ir fr (ofs + 1) | Some ireg => size_arguments_rec tys (ir + 1) fr ofs end - | Tfloat :: tys => + | (Tfloat | Tsingle) :: tys => match list_nth_z float_param_regs fr with | None => size_arguments_rec tys ir fr (align ofs 2 + 2) | Some freg => size_arguments_rec tys ir (fr + 1) ofs @@ -396,6 +396,14 @@ Opaque list_nth_z. destruct H. subst. split. omega. congruence. destruct H. subst. split. omega. congruence. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. +- (* single *) + destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. + subst. right. eapply list_nth_z_in; eauto. + eapply IHtyl; eauto. + subst. split. apply Zle_ge. apply align_le. omega. congruence. + exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. + assert (ofs <= align ofs 2) by (apply align_le; omega). + intuition omega. Qed. Lemma loc_arguments_acceptable: @@ -430,6 +438,9 @@ Proof. apply Zle_trans with (align ofs0 2 + 2); auto; omega. apply Zle_trans with (align ofs0 2). apply align_le; omega. apply Zle_trans with (align ofs0 2 + 2); auto; omega. + destruct (list_nth_z float_param_regs fr); eauto. + apply Zle_trans with (align ofs0 2). apply align_le; omega. + apply Zle_trans with (align ofs0 2 + 2); auto; omega. Qed. Lemma size_arguments_above: @@ -477,7 +488,12 @@ Proof. transitivity (align ofs0 2 + 2). simpl; omega. eauto. apply size_arguments_rec_above. destruct H0. inv H0. transitivity (align ofs0 2 + 2). simpl; omega. eauto. apply size_arguments_rec_above. - eauto. -} + eauto. +- (* single *) + destruct (list_nth_z float_param_regs fr); destruct H0. + congruence. + eauto. + inv H0. apply size_arguments_rec_above. eauto. + } eauto. Qed. -- cgit v1.2.3