diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-01 16:52:02 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-01 16:52:02 +0200 |
commit | c58b421571b0354eea602adbdae674bd1f4847e3 (patch) | |
tree | 8c83d3d7428097523d8af00b9abdcf117532be30 /powerpc/Asm.v | |
parent | 24951d885fbadb8f2fa96ea44a6d3b2a397eab00 (diff) | |
download | compcert-c58b421571b0354eea602adbdae674bd1f4847e3.tar.gz compcert-c58b421571b0354eea602adbdae674bd1f4847e3.zip |
Model external calls as destroying all caller-save registers
The semantics of external function calls in LTL, Linear, Mach and Asm
now consider that all caller-save registers are set to Vundef by the call.
This models that fact that the external function can modify those registers
arbitrarily.
Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes
accordingly.
Diffstat (limited to 'powerpc/Asm.v')
-rw-r--r-- | powerpc/Asm.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index ff580f01..aa15547b 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -1130,6 +1130,15 @@ Definition preg_of (r: mreg) : preg := | F28 => FPR28 | F29 => FPR29 | F30 => FPR30 | F31 => FPR31 end. +(** Undefine all registers except SP and callee-save registers *) + +Definition undef_caller_save_regs (rs: regset) : regset := + fun r => + if preg_eq r SP + || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs)) + then rs r + else Vundef. + (** Extract the values of the arguments of an external call. We exploit the calling conventions from module [Conventions], except that we use PPC registers instead of locations. *) @@ -1189,7 +1198,7 @@ Inductive step: state -> trace -> state -> Prop := Genv.find_funct_ptr ge b = Some (External ef) -> external_call ef ge args m t res m' -> extcall_arguments rs m (ef_sig ef) args -> - rs' = (set_pair (loc_external_result (ef_sig ef)) res rs) #PC <- (rs RA) -> + rs' = (set_pair (loc_external_result (ef_sig ef)) res (undef_caller_save_regs rs)) #PC <- (rs RA) -> step (State rs m) t (State rs' m'). End RELSEM. |