diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-05-17 15:37:56 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-05-17 15:37:56 +0200 |
commit | 82f9d1f96b30106a338e77ec83b7321c2c65f929 (patch) | |
tree | 6b8bb30473b1385f8b84fe1600f592c2bd4abed7 /common/AST.v | |
parent | 672393ef623acb3e230a8019d51c87e051a7567a (diff) | |
download | compcert-82f9d1f96b30106a338e77ec83b7321c2c65f929.tar.gz compcert-82f9d1f96b30106a338e77ec83b7321c2c65f929.zip |
Introduce register pairs to describe calling conventions more precisely
This commit changes the loc_arguments and loc_result functions that describe calling conventions so that each argument/result can be mapped either to a single location or (in the case of a 64-bit integer) to a pair of two 32-bit locations.
In the current CompCert, all arguments/results of type Tlong are systematically split in two 32-bit halves. We will need to change this in the future to support 64-bit processors. The alternative approach implemented by this commit enables the loc_arguments and loc_result functions to describe precisely which arguments need splitting. Eventually, the remainder of CompCert should not assume anything about splitting 64-bit types in two halves.
Summary of changes:
- AST: introduce the type "rpair A" of register pairs
- Conventions1, Conventions: use it when describing calling conventions
- LTL, Linear, Mach, Asm: honor the new calling conventions when observing external calls
- Events: suppress external_call', no longer useful
- All passes from Allocation to Asmgen: adapt accordingly.
Diffstat (limited to 'common/AST.v')
-rw-r--r-- | common/AST.v | 57 |
1 files changed, 56 insertions, 1 deletions
diff --git a/common/AST.v b/common/AST.v index 415e90e2..0b524eb8 100644 --- a/common/AST.v +++ b/common/AST.v @@ -544,10 +544,65 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) := End TRANSF_PARTIAL_FUNDEF. -(** * Arguments and results to builtin functions *) +(** * Register pairs *) Set Contextual Implicit. +(** In some intermediate languages (LTL, Mach), 64-bit integers can be + split into two 32-bit halves and held in a pair of registers. + Syntactically, this is captured by the type [rpair] below. *) + +Inductive rpair (A: Type) : Type := + | One (r: A) + | Twolong (rhi rlo: A). + +Definition typ_rpair (A: Type) (typ_of: A -> typ) (p: rpair A): typ := + match p with + | One r => typ_of r + | Twolong rhi rlo => Tlong + end. + +Definition map_rpair (A B: Type) (f: A -> B) (p: rpair A): rpair B := + match p with + | One r => One (f r) + | Twolong rhi rlo => Twolong (f rhi) (f rlo) + end. + +Definition regs_of_rpair (A: Type) (p: rpair A): list A := + match p with + | One r => r :: nil + | Twolong rhi rlo => rhi :: rlo :: nil + end. + +Fixpoint regs_of_rpairs (A: Type) (l: list (rpair A)): list A := + match l with + | nil => nil + | p :: l => regs_of_rpair p ++ regs_of_rpairs l + end. + +Lemma in_regs_of_rpairs: + forall (A: Type) (x: A) p, In x (regs_of_rpair p) -> forall l, In p l -> In x (regs_of_rpairs l). +Proof. + induction l; simpl; intros. auto. apply in_app. destruct H0; auto. subst a. auto. +Qed. + +Lemma in_regs_of_rpairs_inv: + forall (A: Type) (x: A) l, In x (regs_of_rpairs l) -> exists p, In p l /\ In x (regs_of_rpair p). +Proof. + induction l; simpl; intros. contradiction. + rewrite in_app_iff in H; destruct H. + exists a; auto. + apply IHl in H. firstorder auto. +Qed. + +Definition forall_rpair (A: Type) (P: A -> Prop) (p: rpair A): Prop := + match p with + | One r => P r + | Twolong rhi rlo => P rhi /\ P rlo + end. + +(** * Arguments and results to builtin functions *) + Inductive builtin_arg (A: Type) : Type := | BA (x: A) | BA_int (n: int) |