From c58b421571b0354eea602adbdae674bd1f4847e3 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 1 Jun 2018 16:52:02 +0200 Subject: 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. --- riscV/Asm.v | 11 ++++++++++- riscV/Asmgenproof.v | 4 ++-- 2 files changed, 12 insertions(+), 3 deletions(-) (limited to 'riscV') diff --git a/riscV/Asm.v b/riscV/Asm.v index 4cd3b1fd..6d223c1d 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -1013,6 +1013,15 @@ Definition preg_of (r: mreg) : preg := | Machregs.F28 => F28 | Machregs.F29 => F29 | Machregs.F30 => F30 | Machregs.F31 => F31 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 RISC-V registers instead of locations. *) @@ -1073,7 +1082,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. diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index cc45a8de..5ec57886 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -975,8 +975,8 @@ Local Transparent destroyed_at_function_entry. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. - unfold loc_external_result. - apply agree_set_other; auto. apply agree_set_pair; auto. + unfold loc_external_result. apply agree_set_other; auto. apply agree_set_pair; auto. + apply agree_undef_caller_save_regs; auto. - (* return *) inv STACKS. simpl in *. -- cgit