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. --- backend/Linear.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/Linear.v') diff --git a/backend/Linear.v b/backend/Linear.v index 55f92d16..447c6ba6 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -239,7 +239,7 @@ Inductive step: state -> trace -> state -> Prop := forall s ef args res rs1 rs2 m t m', args = map (fun p => Locmap.getpair p rs1) (loc_arguments (ef_sig ef)) -> external_call ef ge args m t res m' -> - rs2 = Locmap.setpair (loc_result (ef_sig ef)) res rs1 -> + rs2 = Locmap.setpair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs1) -> step (Callstate s (External ef) rs1 m) t (Returnstate s rs2 m') | exec_return: -- cgit