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. --- arm/Asm.v | 51 ++++++++++++++++++++++++++++++++++----------------- 1 file changed, 34 insertions(+), 17 deletions(-) (limited to 'arm/Asm.v') diff --git a/arm/Asm.v b/arm/Asm.v index b350b047..010d5d7b 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -310,12 +310,12 @@ Fixpoint undef_regs (l: list preg) (rs: regset) : regset := Definition undef_flags (rs: regset) : regset := fun r => match r with CR _ => Vundef | _ => rs r end. -(** Assigning multiple registers *) +(** Assigning a register pair *) -Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset := - match rl, vl with - | r1 :: rl', v1 :: vl' => set_regs rl' vl' (rs#r1 <- v1) - | _, _ => rs +Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset := + match p with + | One r => rs#r <- v + | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v) end. (** Assigning the result of a builtin *) @@ -813,12 +813,21 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := (Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v -> extcall_arg rs m (S Outgoing ofs ty) v. +Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop := + | extcall_arg_one: forall l v, + extcall_arg rs m l v -> + extcall_arg_pair rs m (One l) v + | extcall_arg_twolong: forall hi lo vhi vlo, + extcall_arg rs m hi vhi -> + extcall_arg rs m lo vlo -> + extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo). + Definition extcall_arguments (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := - list_forall2 (extcall_arg rs m) (loc_arguments sg) args. + list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args. -Definition loc_external_result (sg: signature) : list preg := - map preg_of (loc_result sg). +Definition loc_external_result (sg: signature) : rpair preg := + map_rpair preg_of (loc_result sg). (** Execution of the instruction at [rs#PC]. *) @@ -848,9 +857,9 @@ Inductive step: state -> trace -> state -> Prop := forall b ef args res rs m t rs' m', rs PC = Vptr b Int.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> - external_call' ef ge args m t res m' -> + external_call ef ge args m t res m' -> extcall_arguments rs m (ef_sig ef) args -> - rs' = (set_regs (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs IR14) -> + rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs IR14) -> step (State rs m) t (State rs' m'). End RELSEM. @@ -884,13 +893,21 @@ Remark extcall_arguments_determ: extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2. Proof. intros until m. - assert (forall ll vl1, list_forall2 (extcall_arg rs m) ll vl1 -> - forall vl2, list_forall2 (extcall_arg rs m) ll vl2 -> vl1 = vl2). + assert (A: forall l v1 v2, + extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2). + { intros. inv H; inv H0; congruence. } + assert (B: forall p v1 v2, + extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2). + { intros. inv H; inv H0. + eapply A; eauto. + f_equal; eapply A; eauto. } + assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 -> + forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2). + { induction 1; intros vl2 EA; inv EA. auto. - f_equal; auto. - inv H; inv H3; congruence. - intros. red in H0; red in H1. eauto. + f_equal; eauto. } + intros. eapply C; eauto. Qed. Lemma semantics_determinate: forall p, determinate (semantics p). @@ -911,13 +928,13 @@ Ltac Equalities := exploit external_call_determ. eexact H5. eexact H11. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. - exploit external_call_determ'. eexact H3. eexact H8. intros [A B]. + exploit external_call_determ. eexact H3. eexact H8. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. (* trace length *) red; intros; inv H; simpl. omega. inv H3; eapply external_call_trace_length; eauto. - inv H2; eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. (* initial states *) inv H; inv H0. f_equal. congruence. (* final no step *) -- cgit