diff options
Diffstat (limited to 'arm/Conventions1.v')
| -rw-r--r-- | arm/Conventions1.v | 50 |
1 files changed, 37 insertions, 13 deletions
diff --git a/arm/Conventions1.v b/arm/Conventions1.v index 3eae50ef..888861a5 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -85,15 +85,21 @@ Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) For the "softfloat" convention, results of FP types should be passed in [R0] or [R0,R1]. This doesn't fit the CompCert register model, - so we have code in [arm/PrintAsm.ml] that inserts additional moves - to/from [F0]. *) + so we have code in [arm/TargetPrinter.ml] that inserts additional moves + to/from [F0]. + + Concerning endianness for 64bit values in register pairs, the contents + of the registers is as if the value had been loaded from memory + representation with a single LDM instruction. *) Definition loc_result (s: signature) : rpair mreg := match s.(sig_res) with | None => One R0 | Some (Tint | Tany32) => One R0 | Some (Tfloat | Tsingle | Tany64) => One F0 - | Some Tlong => Twolong R1 R0 + | Some Tlong => if Archi.big_endian + then Twolong R0 R1 + else Twolong R1 R0 end. (** The result registers have types compatible with that given in the signature. *) @@ -102,7 +108,7 @@ Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto. + intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; destruct Archi.big_endian; auto. Qed. (** The result locations are caller-save registers *) @@ -112,7 +118,7 @@ Lemma loc_result_caller_save: forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. intros. - unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto. + unfold loc_result. destruct (sig_res s) as [[]|]; destruct Archi.big_endian; simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -124,7 +130,9 @@ Lemma loc_result_pair: | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true end. Proof. - intros; unfold loc_result; destruct (sig_res sg) as [[]|]; auto. intuition congruence. + intros; unfold loc_result; destruct (sig_res sg) as [[]|]; destruct Archi.big_endian; auto. + intuition congruence. + intuition congruence. Qed. (** ** Location of function arguments *) @@ -176,11 +184,13 @@ Fixpoint loc_arguments_hf then One (R (freg_param fr)) :: loc_arguments_hf tys ir (fr + 1) ofs else One (S Outgoing ofs Tsingle) :: loc_arguments_hf tys ir fr (ofs + 1) | Tlong :: tys => + let ohi := if Archi.big_endian then 0 else 1 in + let olo := if Archi.big_endian then 1 else 0 in let ir := align ir 2 in if zlt ir 4 - then Twolong (R (ireg_param (ir + 1))) (R (ireg_param ir)) :: loc_arguments_hf tys (ir + 2) fr ofs + then Twolong (R (ireg_param (ir + ohi))) (R (ireg_param (ir + olo))) :: loc_arguments_hf tys (ir + 2) fr ofs else let ofs := align ofs 2 in - Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) :: loc_arguments_hf tys ir fr (ofs + 2) + Twolong (S Outgoing (ofs + ohi) Tint) (S Outgoing (ofs + olo) Tint) :: loc_arguments_hf tys ir fr (ofs + 2) end. (** For the "softfloat" configuration, as well as for variable-argument functions @@ -218,9 +228,11 @@ Fixpoint loc_arguments_sf One (if zlt ofs 0 then R (freg_param (ofs + 4)) else S Outgoing ofs Tsingle) :: loc_arguments_sf tys (ofs + 1) | Tlong :: tys => + let ohi := if Archi.big_endian then 0 else 1 in + let olo := if Archi.big_endian then 1 else 0 in let ofs := align ofs 2 in - Twolong (if zlt ofs 0 then R (ireg_param (ofs+1+4)) else S Outgoing (ofs+1) Tint) - (if zlt ofs 0 then R (ireg_param (ofs+4)) else S Outgoing ofs Tint) + Twolong (if zlt ofs 0 then R (ireg_param (ofs+ohi+4)) else S Outgoing (ofs+ohi) Tint) + (if zlt ofs 0 then R (ireg_param (ofs+olo+4)) else S Outgoing (ofs+olo) Tint) :: loc_arguments_sf tys (ofs + 2) end. @@ -341,9 +353,9 @@ Proof. set (ir' := align ir 2) in *. assert (ofs <= align ofs 2) by (apply align_le; omega). destruct (zlt ir' 4). - destruct H. subst p. split; apply ireg_param_caller_save. + destruct H. subst p. split; apply ireg_param_caller_save. eapply IHtyl; eauto. - destruct H. subst p. split; (split; [ omega | auto ]). + destruct H. subst p. split; destruct Archi.big_endian; (split; [ omega | auto ]). eapply Y. eapply IHtyl; eauto. omega. - (* single *) destruct (zlt fr 8); destruct H. @@ -396,7 +408,7 @@ Proof. destruct H. destruct (zlt ofs' 0); subst p. split; apply ireg_param_caller_save. - split; (split; [xomega|auto]). + split; destruct Archi.big_endian; (split; [xomega|auto]). eapply Y. eapply IHtyl; eauto. omega. - (* single *) destruct H. @@ -513,6 +525,12 @@ Proof. - (* long *) destruct (zlt (align ir 2) 4). destruct H. discriminate. destruct H. discriminate. eauto. + destruct Archi.big_endian. + destruct H. inv H. + eapply Zle_trans. 2: apply size_arguments_hf_above. simpl; omega. + destruct H. inv H. + rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above. + eauto. destruct H. inv H. rewrite <- Zplus_assoc. simpl. apply size_arguments_hf_above. destruct H. inv H. @@ -556,9 +574,15 @@ Proof. eauto. - (* long *) destruct H. + destruct Archi.big_endian. + destruct (zlt (align ofs0 2) 0); inv H. + eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega. destruct (zlt (align ofs0 2) 0); inv H. rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above. destruct H. + destruct Archi.big_endian. + destruct (zlt (align ofs0 2) 0); inv H. + rewrite <- Zplus_assoc. simpl. apply size_arguments_sf_above. destruct (zlt (align ofs0 2) 0); inv H. eapply Zle_trans. 2: apply size_arguments_sf_above. simpl; xomega. eauto. |