From 82f9d1f96b30106a338e77ec83b7321c2c65f929 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 17 May 2016 15:37:56 +0200 Subject: 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. --- backend/Locations.v | 34 ++++++++++++++++++++++++++-------- 1 file changed, 26 insertions(+), 8 deletions(-) (limited to 'backend/Locations.v') diff --git a/backend/Locations.v b/backend/Locations.v index 6ca84ea7..52abfc46 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -386,17 +386,35 @@ Module Locmap. auto. Qed. - Fixpoint setlist (ll: list loc) (vl: list val) (m: t) {struct ll} : t := - match ll, vl with - | l1 :: ls, v1 :: vs => setlist ls vs (set l1 v1 m) - | _, _ => m + Definition getpair (p: rpair loc) (m: t) : val := + match p with + | One l => m l + | Twolong l1 l2 => Val.longofwords (m l1) (m l2) end. - Lemma gsetlisto: forall l ll vl m, Loc.notin l ll -> (setlist ll vl m) l = m l. + Definition setpair (p: rpair mreg) (v: val) (m: t) : t := + match p with + | One r => set (R r) v m + | Twolong hi lo => set (R lo) (Val.loword v) (set (R hi) (Val.hiword v) m) + end. + + Lemma getpair_exten: + forall p ls1 ls2, + (forall l, In l (regs_of_rpair p) -> ls2 l = ls1 l) -> + getpair p ls2 = getpair p ls1. Proof. - induction ll; simpl; intros. - auto. - destruct vl; auto. destruct H. rewrite IHll; auto. apply gso; auto. apply Loc.diff_sym; auto. + intros. destruct p; simpl. + apply H; simpl; auto. + f_equal; apply H; simpl; auto. + Qed. + + Lemma gpo: + forall p v m l, + forall_rpair (fun r => Loc.diff l (R r)) p -> setpair p v m l = m l. + Proof. + intros; destruct p; simpl in *. + - apply gso. apply Loc.diff_sym; auto. + - destruct H. rewrite ! gso by (apply Loc.diff_sym; auto). auto. Qed. Fixpoint setres (res: builtin_res mreg) (v: val) (m: t) : t := -- cgit