From 1f004665758e26e6e48d13f5702fe55af8944448 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 25 Oct 2016 15:11:30 +0200 Subject: Update ARM port. Not tested yet. --- arm/Conventions1.v | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) (limited to 'arm/Conventions1.v') diff --git a/arm/Conventions1.v b/arm/Conventions1.v index 888861a5..ecf03e1d 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -60,6 +60,15 @@ Definition destroyed_at_call := Definition dummy_int_reg := R0. (**r Used in [Coloring]. *) Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) +Definition is_float_reg (r: mreg): bool := + match r with + | R0 | R1 | R2 | R3 + | R4 | R5 | R6 | R7 + | R8 | R9 | R10 | R11 | R12 => false + | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 + | F8 | F9 | F10 | F11 | F12 | F13 | F14 | F15 => true + end. + (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -127,7 +136,7 @@ Lemma loc_result_pair: forall sg, match loc_result sg with | One _ => True - | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true + | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.splitlong = true end. Proof. intros; unfold loc_result; destruct (sig_res sg) as [[]|]; destruct Archi.big_endian; auto. @@ -135,6 +144,14 @@ Proof. intuition congruence. Qed. +(** The location of the result depends only on the result part of the signature *) + +Lemma loc_result_exten: + forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. +Proof. + intros. unfold loc_result. rewrite H; auto. +Qed. + (** ** Location of function arguments *) (** For the "hardfloat" configuration, we use the following calling conventions, -- cgit