diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-25 15:11:30 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-25 15:11:30 +0200 |
| commit | 1f004665758e26e6e48d13f5702fe55af8944448 (patch) | |
| tree | e3ccaee73c86ec1aef94ef66341610ed4436f93a /arm/Conventions1.v | |
| parent | 271a6f98809fbeac6cb04fb29fccbcf9c1e18335 (diff) | |
| download | compcert-kvx-1f004665758e26e6e48d13f5702fe55af8944448.tar.gz compcert-kvx-1f004665758e26e6e48d13f5702fe55af8944448.zip | |
Update ARM port. Not tested yet.
Diffstat (limited to 'arm/Conventions1.v')
| -rw-r--r-- | arm/Conventions1.v | 19 |
1 files changed, 18 insertions, 1 deletions
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, |