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/Mach.v | 31 ++++++++++++++++++++----------- 1 file changed, 20 insertions(+), 11 deletions(-) (limited to 'backend/Mach.v') diff --git a/backend/Mach.v b/backend/Mach.v index 739c8212..3e15c97c 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -156,10 +156,10 @@ Proof. unfold Regmap.set. destruct (RegEq.eq r a); auto. Qed. -Fixpoint set_regs (rl: list mreg) (vl: list val) (rs: regset) : regset := - match rl, vl with - | r1 :: rl', v1 :: vl' => set_regs rl' vl' (Regmap.set r1 v1 rs) - | _, _ => rs +Definition set_pair (p: rpair mreg) (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. Fixpoint set_res (res: builtin_res mreg) (v: val) (rs: regset) : regset := @@ -216,16 +216,25 @@ Definition find_function_ptr (** Extract the values of the arguments to an external call. *) -Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop := - | extcall_arg_reg: forall rs m sp r, +Inductive extcall_arg (rs: regset) (m: mem) (sp: val): loc -> val -> Prop := + | extcall_arg_reg: forall r, extcall_arg rs m sp (R r) (rs r) - | extcall_arg_stack: forall rs m sp ofs ty v, + | extcall_arg_stack: forall ofs ty v, load_stack m sp ty (Int.repr (Stacklayout.fe_ofs_arg + 4 * ofs)) = Some v -> extcall_arg rs m sp (S Outgoing ofs ty) v. +Inductive extcall_arg_pair (rs: regset) (m: mem) (sp: val): rpair loc -> val -> Prop := + | extcall_arg_one: forall l v, + extcall_arg rs m sp l v -> + extcall_arg_pair rs m sp (One l) v + | extcall_arg_twolong: forall hi lo vhi vlo, + extcall_arg rs m sp hi vhi -> + extcall_arg rs m sp lo vlo -> + extcall_arg_pair rs m sp (Twolong hi lo) (Val.longofwords vhi vlo). + Definition extcall_arguments (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := - list_forall2 (extcall_arg rs m sp) (loc_arguments sg) args. + list_forall2 (extcall_arg_pair rs m sp) (loc_arguments sg) args. (** Mach execution states. *) @@ -391,8 +400,8 @@ Inductive step: state -> trace -> state -> Prop := forall s fb rs m t rs' ef args res m', Genv.find_funct_ptr ge fb = Some (External ef) -> extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> - external_call' ef ge args m t res m' -> - rs' = set_regs (loc_result (ef_sig ef)) res rs -> + external_call ef ge args m t res m' -> + rs' = set_pair (loc_result (ef_sig ef)) res rs -> step (Callstate s fb rs m) t (Returnstate s rs' m') | exec_return: @@ -411,7 +420,7 @@ Inductive initial_state (p: program): state -> Prop := Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r retcode, - loc_result signature_main = r :: nil -> + loc_result signature_main = One r -> rs r = Vint retcode -> final_state (Returnstate nil rs m) retcode. -- cgit